naive early evaluation of instanceof

Summary: This is a simple-minded change to `Formula.and_equal_instaceof` that evaluates eagerly if the dynamic type is known at the point we make the assertion. It doesn't integrate with the propagation of equalities etc, as I'm now going to leave that until I've got a proper instanceof domain instead. But this should suffice to check the effects of eager solving on coverage etc.

Reviewed By: skcho

Differential Revision: D54537978

fbshipit-source-id: bb590fd76ac707c84163da14e527cfe091321ef6

Author: Nick Benton

infer/src/pulse/PulseFormula.ml

@@ -3437,14 +3437,6 @@ let and_equal_vars v1 v2 formula =
 
 let and_not_equal = and_mk_atom Ne
 
-let and_equal_instanceof v1 v2 t ~get_dynamic_type ~tenv formula =
-  ignore get_dynamic_type ;
-  ignore tenv ;
-  (* just testing the plumbing *)
-  let atom = Atom.equal (Var v1) (IsInstanceOf (v2, t)) in
-  and_atom atom formula
-
-
 let and_is_int v formula =
   let atom = Atom.equal (IsInt (Var v)) Term.one in
   and_atom atom formula
@@ -3557,6 +3549,20 @@ module DynamicTypes = struct
     else Sat (formula, RevList.empty)
 end
 
+(* Just do most naive thing of evaluating instanceof if we know the dynamic type at the time of assertion
+   Because that's pretty weak, leave existing normalisation at summary time in for now
+*)
+let and_equal_instanceof v1 v2 t ~get_dynamic_type ~tenv formula =
+  let atom =
+    match DynamicTypes.evaluate_instanceof tenv ~get_dynamic_type v2 t with
+    | None ->
+        Atom.equal (Var v1) (IsInstanceOf (v2, t))
+    | Some bool_term ->
+        Atom.equal (Var v1) bool_term
+  in
+  and_atom atom formula
+
+
 let normalize tenv ~get_dynamic_type formula =
   Debug.p "@\n@\n***NORMALIZING NOW***@\n@\n" ;
   (* normalization happens incrementally except for dynamic types (TODO) *)

infer/tests/codetoanalyze/hack/pulse/eagerprune.hack

@@ -0,0 +1,44 @@
+// 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.
+
+// These tests are all OK, but useful for looking at the debug output to confirm
+// that the eager pruning is working as expected
+class EagerTypePrune {
+  public static function testPositiveOK(): void {
+    $i = 3;
+    if ($i is int) {
+      return;
+    } else {
+      // if we're really eager, we shouldn't even analyse this call
+      // have confirmed that we do at the moment
+      $dummy = self::g();
+    }
+  }
+
+  public static function testNegativeOK(): void {
+    $i = 3;
+    if ($i is string) {
+      $dummy = self::g();
+    } else {
+      return;
+    }
+  }
+
+  public static function testBothOK(mixed $i): void {
+    if ($i is int) {
+      $dummy = self::g();
+    } else {
+      $dummy = self::f();
+    }
+  }
+
+  public static function g(): int {
+    return 42;
+  }
+
+  public static function f(): int {
+    return 42;
+  }
+}