Skip to content

Commit

Permalink
[hack] Add $builtins.hack_bool model + tests
Browse files Browse the repository at this point in the history
Summary:
Without the model we don't understand boolean literals in Hack
(basically, treat them as nondet) which makes us explore more paths then
necessary and leads to FPs.

Reviewed By: davidpichardie

Differential Revision: D46189262

fbshipit-source-id: f1185d45be9c87e06ab2e511566b559cc9938ad7
  • Loading branch information
artempyanykh authored and facebook-github-bot committed May 26, 2023
1 parent a4104d6 commit ff7eb1b
Show file tree
Hide file tree
Showing 3 changed files with 34 additions and 8 deletions.
17 changes: 9 additions & 8 deletions infer/lib/hack/models.sil
Original file line number Diff line number Diff line change
Expand Up @@ -30,26 +30,27 @@ define $builtins.hack_int(i: int) : *HackMixed {

type HackBool = { val: int }

define $builtins.hack_make_random_bool(): *HackBool {
define $builtins.hack_bool(b: int): *HackBool {
#entry:
n0 = __sil_allocate(<HackBool>)
n1 = $builtins.nondet()
n1: int = load &b
store n0.HackBool.val <- n1 : int
ret n0
}

define $builtins.hack_make_true(): *HackBool {
#entry:
n0 = __sil_allocate(<HackBool>)
store n0.HackBool.val <- 1 : int
ret n0
ret $builtins.hack_bool(1)
}

define $builtins.hack_make_false(): *HackBool {
#entry:
n0 = __sil_allocate(<HackBool>)
store n0.HackBool.val <- 0 : int
ret n0
ret $builtins.hack_bool(0)
}

define $builtins.hack_make_random_bool(): *HackBool {
#entry:
ret $builtins.hack_bool($builtins.nondet())
}

define $builtins.hack_is_true(b: *HackMixed) : int {
Expand Down
1 change: 1 addition & 0 deletions infer/tests/codetoanalyze/hack/pulse/issues.exp
Original file line number Diff line number Diff line change
Expand Up @@ -43,4 +43,5 @@ method_resolution_trait2.hack, $root.basicFlowBad20, 3, TAINT_ERROR, no_bucket,
method_resolution_trait2.hack, $root.basicFlowBad21, 3, TAINT_ERROR, no_bucket, ERROR, [in call to `BadP.runSource`,source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,return from call to `BadP.runSource`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
method_resolution_trait2.hack, $root.basicFlowOk22, 3, TAINT_ERROR, no_bucket, ERROR, [in call to `BadP.runSource`,source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,return from call to `BadP.runSource`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $untainted
method_resolution_trait3.hack, $root.basicFlowBad30, 3, TAINT_ERROR, no_bucket, ERROR, [in call to `BadP.runSource`,source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,return from call to `BadP.runSource`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted
primitives.hack, $root.Primitives::logEnabledExplicitBad, 1, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value passed as argument `#1` to `$root.Primitives::logEnabledExplicitBad` with kind `Simple`,when calling `$root.Primitives::condLog` here,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Primitives::logEnabledExplicitBad, sink: $root.Level1::taintSink, tainted expression: $sc
shapes.hack, Shapes::C1.passViaShapeBad, 1, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value passed as argument `#1` to `Shapes::C1.passViaShapeBad` with kind `Simple`,value passed as argument `#1` to `Shapes::ShapeLogger$static.logData` with kind `Simple`], source: Shapes::C1.passViaShapeBad, sink: Shapes::ShapeLogger$static.logData, tainted expression: $sc->sensitiveField
24 changes: 24 additions & 0 deletions infer/tests/codetoanalyze/hack/pulse/primitives.hack
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
// Copyright (c) Facebook, Inc. and its affiliates.
//
// This source code is licensed under the MIT license found in the
// LICENSE file in the root directory of this source tree.

namespace Primitives;

function condLog(mixed $data, bool $should_log = false) : void {
if ($should_log) {
\Level1\taintSink($data);
}
}

function logEnabledExplicitBad(SensitiveClass $sc) : void {
condLog($sc, true);
}

function logDisabledExplicitOk(SensitiveClass $sc) : void {
condLog($sc, false);
}

function logDisabledImplicitOk(SensitiveClass $sc) : void {
condLog($sc);
}

0 comments on commit ff7eb1b

Please sign in to comment.