[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

@@ -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(<HackBool>)
+    n1 = $builtins.nondet()
+    store n0.HackBool.val <- n1 : int
+    ret n0
+}
+
 define $builtins.hack_make_true(): *HackBool {
   #entry:
     n0 = __sil_allocate(<HackBool>)
@@ -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
-}

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

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);
+  }
+}

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

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 {