[pulse] IsInstanceOf simplification for null obj

Summary:
Fixing `IsInstanceOf` term simplification for null case. Before, this
was only being done if value was known to be null at the moment of the
call to `instanceof`. Otherwise, the `IsInstanceOf` term would remain in
the formula unnecessarily.

Reviewed By: jvillard

Differential Revision: D27361025

fbshipit-source-id: 2d958a757

infer/src/pulse/PulseFormula.ml

@@ -545,6 +545,8 @@ module Term = struct
           match op with
           | VarSubst v' when not (Var.equal v v') ->
               IsInstanceOf (v', typ)
+          | QSubst q when Q.is_zero q ->
+              zero
           | QSubst _ | VarSubst _ | LinSubst _ ->
               t
         in

infer/src/pulse/PulseModels.ml

@@ -960,10 +960,7 @@ module Java = struct
     let res_addr = AbstractValue.mk_fresh () in
     match typeexpr with
     | Exp.Sizeof {typ} ->
-        let<+> astate =
-          PulseArithmetic.and_equal_instanceof res_addr argv typ astate
-          >>= PulseArithmetic.prune_positive argv
-        in
+        let<+> astate = PulseArithmetic.and_equal_instanceof res_addr argv typ astate in
         PulseOperations.write_id ret_id (res_addr, event :: hist) astate
     (* The type expr is sometimes a Var expr but this is not expected.
        This seems to be introduced by inline mechanism of Java synthetic methods during preanalysis *)

infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java

@@ -56,7 +56,7 @@ public class InstanceOfExample {
     }
   }
 
-  public void testInstanceOfNullOk() {
+  public void testInstanceOfNullInterOk() {
     Person p = new Professor();
     // p is null after this call
     p = updatePerson(p);
@@ -66,6 +66,22 @@ public class InstanceOfExample {
     }
   }
 
+  public void testInstanceOfNullIntraOk() {
+    Person p = null;
+    if (p instanceof Professor) {
+      Object o = null;
+      o.toString();
+    }
+  }
+
+  public void testInstanceOfNullIntraBad() {
+    Person p = null;
+    if (!(p instanceof Professor)) {
+      Object o = null;
+      o.toString();
+    }
+  }
+
   public void checkInstanceArray(Object array) {
     Object o = null;
     if (array instanceof int[]) {

infer/tests/codetoanalyze/java/pulse/issues.exp

@@ -20,6 +20,7 @@ codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapEx
 codetoanalyze/java/pulse/HashMapExample.java, codetoanalyze.java.infer.HashMapExample.getOneIntegerWithoutCheckBad():int, 6, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `Map.get()` (modelled),return from call to `Map.get()` (modelled),assigned,passed as argument to `cast` (modelled),return from call to `cast` (modelled),assigned,invalid access occurs here]
 codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.checkInstanceArray(java.lang.Object):void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfBooleanArrayBad():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `void InstanceOfExample.checkInstanceArray(Object)`,source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
+codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfNullIntraBad():void, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/InstanceOfExample.java, InstanceOfExample.testInstanceOfObjProfessorBad():void, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,when calling `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)` here,assigned,is the null pointer,null pointer dereference part of the trace starts here,passed as argument to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,return from call to `InstanceOfExample$Person InstanceOfExample.updatePerson(InstanceOfExample$Person)`,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.FP_testIntegerBuiltInEqualOperatorCachedValuesOk():void, 19, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]
 codetoanalyze/java/pulse/IntegerExample.java, codetoanalyze.java.infer.IntegerExample.testIntegerBuiltInEqualOperatorNonCachedValuesBad():void, 7, NULLPTR_DEREFERENCE, no_bucket, ERROR, [source of the null value part of the trace starts here,assigned,is the null pointer,null pointer dereference part of the trace starts here,assigned,invalid access occurs here]