[pulse] Implementing temporary model for Java instanceof operator

Summary:
Providing model for Java `instanceof` operator that
avoids to return true when given object is null. This is a temporary
solution that will reduce FPs while we do not provide the correct
semantics for `instanceof`.

Reviewed By: jvillard

Differential Revision: D26608043

fbshipit-source-id: 87c82b906

infer/src/pulse/PulseModels.ml

@@ -910,6 +910,17 @@ module StdVector = struct
     PulseOperations.write_id ret_id (value_addr, crumb :: value_hist) astate
 end
 
+module Java = struct
+  let instance_of (argv, hist) _ : model =
+   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
+    let event = ValueHistory.Call {f= Model "Java.instanceof"; location; in_call= []} in
+    let res_addr = AbstractValue.mk_fresh () in
+    PulseArithmetic.prune_positive argv astate
+    |> PulseArithmetic.and_eq_int res_addr IntLit.one
+    |> PulseOperations.write_id ret_id (res_addr, event :: hist)
+    |> ok_continue
+end
+
 module JavaCollection = struct
   (* modifies arr[index]-> old_elem to arr[index]-> new_elem and returns old_elem *)
   let set coll (index, _) (new_elem, new_elem_hist) : model =
@@ -1357,7 +1368,8 @@ module ProcNameDispatcher = struct
         ; +map_context_tenv PatternMatch.Java.implements_iterator
           &:: "next" <>$ capt_arg_payload
           $!--> JavaIterator.next ~desc:"Iterator.next()"
-        ; +match_builtin BuiltinDecl.__instanceof &--> Misc.return_positive ~desc:"instanceof"
+        ; +match_builtin BuiltinDecl.__instanceof
+          <>$ capt_arg_payload $+ capt_exp $--> Java.instance_of
         ; ( +map_context_tenv PatternMatch.Java.implements_enumeration
           &:: "nextElement" <>$ capt_arg_payload
           $!--> fun x ->

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

@@ -65,4 +65,11 @@ public class InstanceOfExample {
     int arr[] = new int[10];
     checkInstanceArray(arr);
   }
+
+  public void testInstanceOfNullOk() {
+    Student s = null;
+    if (s instanceof Student) {
+      s.toString();
+    }
+  }
 }