From f28823fad5f9e3d1b38381b3b75bfcb2f946bfb5 Mon Sep 17 00:00:00 2001 From: Artem Pianykh Date: Mon, 15 May 2023 03:30:42 -0700 Subject: [PATCH] [hack] Clean up models a bit Summary: Having `ret null` as a model is not the best, especially for predicate functions (e.g. `is_type_struct_c`) because it confuses the analysis with false nullptr dereferences which is especially problematic when `pulse-force-continue` is not set. This diff uses `nondet` for predicate functions. We could delete models but then builtins would accumulate in `skipped_calls`. I also removed a few `ret null` models where it wasn't easy to write something reasonabe. NOTE: that there are 2 `ret null` models that we can't delete because otherwise we get a bunch of FPs in tests. These need to be looked at. Reviewed By: davidpichardie Differential Revision: D45852568 fbshipit-source-id: 3671bd024e268ce4a474978774e66435b7bd34f7 --- infer/lib/hack/models.sil | 34 +++++++++---------- infer/src/pulse/PulseModelsHack.ml | 3 +- .../hack/pulse/control_flow.hack | 13 +++++++ .../tests/codetoanalyze/hack/pulse/issues.exp | 1 + .../codetoanalyze/hack/pulse/level1.hack | 2 +- 5 files changed, 33 insertions(+), 20 deletions(-) create mode 100644 infer/tests/codetoanalyze/hack/pulse/control_flow.hack diff --git a/infer/lib/hack/models.sil b/infer/lib/hack/models.sil index 26d448bd1dd..0837df7e2e7 100644 --- a/infer/lib/hack/models.sil +++ b/infer/lib/hack/models.sil @@ -5,6 +5,9 @@ .source_language = "hack" +// This function has an OCaml model +declare $builtins.nondet() : int + type HackString = { val: *string } define $builtins.hack_string(str: *string) : *HackMixed { @@ -27,6 +30,14 @@ define $builtins.hack_int(i: int) : *HackMixed { type HackBool = { val: int } +define $builtins.hack_make_random_bool(): *HackBool { + #entry: + n0 = __sil_allocate() + n1 = $builtins.nondet() + store n0.HackBool.val <- n1 : int + ret n0 +} + define $builtins.hack_make_true(): *HackBool { #entry: n0 = __sil_allocate() @@ -86,45 +97,32 @@ define $builtins.hhbc_has_reified_parent(class: *HackMixed): *HackMixed { define $builtins.hhbc_is_type_struct_c(o: *HackMixed, dict: *HackMixed, i: *HackMixed): *HackMixed { #entry: - ret null + ret $builtins.hack_make_random_bool() } define $builtins.hhbc_is_type_int(o: *HackMixed): *HackMixed { #entry: - ret null + ret $builtins.hack_make_random_bool() } define $builtins.hhbc_is_late_bound_cls(o: *HackMixed): *HackMixed { #entry: - ret null + ret $builtins.hack_make_random_bool() } +// TODO: Treating this as unknown causes FPs define $builtins.hhbc_verify_type_pred(o: *HackMixed, typ: *HackMixed): *HackMixed { #entry: ret null } +// TODO: Treating this as unknown causes FPs define $builtins.hhbc_lock_obj(o: *HackMixed): *HackMixed { #entry: ret null } -define $builtins.hhbc_new_col_vector(): *HackMixed { - #entry: - ret null -} - -define $builtins.hhbc_cast_vec(vec: *HackMixed): *HackMixed { - #entry: - ret null -} - define $builtins.hhbc_check_this(o: *HackMixed): *HackMixed { #entry: ret null } - -define HackMixed._86reifiedinit(o: *HackMixed): *HackMixed { - #entry: - ret null -} diff --git a/infer/src/pulse/PulseModelsHack.ml b/infer/src/pulse/PulseModelsHack.ml index 5ce642caa2e..960f8d94439 100644 --- a/infer/src/pulse/PulseModelsHack.ml +++ b/infer/src/pulse/PulseModelsHack.ml @@ -96,7 +96,8 @@ let get_static_class (addr, _) : model = let matchers : matcher list = let open ProcnameDispatcher.Call in - [ +BuiltinDecl.(match_builtin __lazy_class_initialize) <>$ capt_exp $--> lazy_class_initialize + [ -"$builtins" &:: "nondet" <>$$--> Basic.nondet ~desc:"nondet" + ; +BuiltinDecl.(match_builtin __lazy_class_initialize) <>$ capt_exp $--> lazy_class_initialize ; -"$builtins" &:: "await" <>$ capt_arg_payload $--> hack_await ; -"$builtins" &:: "hack_dim_field_get" <>$ capt_arg_payload $+ capt_arg_payload $--> hack_dim_field_get diff --git a/infer/tests/codetoanalyze/hack/pulse/control_flow.hack b/infer/tests/codetoanalyze/hack/pulse/control_flow.hack new file mode 100644 index 00000000000..10a010b5a32 --- /dev/null +++ b/infer/tests/codetoanalyze/hack/pulse/control_flow.hack @@ -0,0 +1,13 @@ +// 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 ControlFlow; + + +function typeCheckDoesntConfuseTheAnalysis_maintainsTaint_Bad(mixed $arg1, SensitiveClass $sc) { + if ($arg1 is Foo) { + \Level1\taintSink($sc); + } +} diff --git a/infer/tests/codetoanalyze/hack/pulse/issues.exp b/infer/tests/codetoanalyze/hack/pulse/issues.exp index f6df71975d3..f45efcd73e5 100644 --- a/infer/tests/codetoanalyze/hack/pulse/issues.exp +++ b/infer/tests/codetoanalyze/hack/pulse/issues.exp @@ -4,6 +4,7 @@ basic_object.hack, BasicObject::Main.set_and_get_B_bad, 7, TAINT_ERROR, no_bucke basic_object.hack, BasicObject::Main.set_and_get_C_bad, 10, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted basic_object.hack, BasicObject::Main.set_and_get_Derived_bad, 7, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted basic_object.hack, BasicObject::Main.set_and_get_Derived_copy_bad, 9, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `$root.Level1::taintSource` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.Level1::taintSource, sink: $root.Level1::taintSink, tainted expression: $tainted +control_flow.hack, $root.ControlFlow::typeCheckDoesntConfuseTheAnalysis_maintainsTaint_Bad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value passed as argument `#2` to `$root.ControlFlow::typeCheckDoesntConfuseTheAnalysis_maintainsTaint_Bad` with kind `Simple`,value passed as argument `#1` to `$root.Level1::taintSink` with kind `Simple`], source: $root.ControlFlow::typeCheckDoesntConfuseTheAnalysis_maintainsTaint_Bad, sink: $root.Level1::taintSink, tainted expression: $sc cross_file_taint_flow.hack, $root.directCrossFileFlowBad, 2, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `OuterFile$static.taintSource` with kind `Simple`,value passed as argument `#1` to `OuterFile$static.taintSink` with kind `Simple`], source: OuterFile$static.taintSource, sink: OuterFile$static.taintSink, tainted expression: $tainted cross_file_taint_flow.hack, $root.indirectCrossFileFlowBad, 2, TAINT_ERROR, no_bucket, ERROR, [in call to `OuterFile$static.tainted`,source of the taint here: value returned from `OuterFile$static.taintSource` with kind `Simple`,return from call to `OuterFile$static.tainted`,value passed as argument `#1` to `OuterFile$static.taintSink` with kind `Simple`], source: OuterFile$static.taintSource, sink: OuterFile$static.taintSink, tainted expression: $tainted cross_file_taint_flow.hack, $root.inheritanceCrossFileFlowBad, 4, TAINT_ERROR, no_bucket, ERROR, [source of the taint here: value returned from `OuterFileSuper$static.superTaintSource` with kind `Simple`,value passed as argument `#1` to `OuterFile$static.taintSink` with kind `Simple`], source: OuterFileSuper$static.superTaintSource, sink: OuterFile$static.taintSink, tainted expression: $tainted diff --git a/infer/tests/codetoanalyze/hack/pulse/level1.hack b/infer/tests/codetoanalyze/hack/pulse/level1.hack index cdef53a9f40..dbd66c5a843 100644 --- a/infer/tests/codetoanalyze/hack/pulse/level1.hack +++ b/infer/tests/codetoanalyze/hack/pulse/level1.hack @@ -9,7 +9,7 @@ function taintSource(): int { return 42; } -function taintSink(int $i): void { +function taintSink(mixed... $args): void { } function basicFlowBad(): void {