From 671727be538fc1206ab6148adf23e9949ebdd560 Mon Sep 17 00:00:00 2001
From: Gabriela Cunha Sampaio <gabrielasampaio@fb.com>
Date: Wed, 24 Feb 2021 04:21:56 -0800
Subject: [PATCH] [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                     | 14 +++++++++++++-
 .../java/pulse/InstanceOfExample.java              |  7 +++++++
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 19cf09671..9b4be27c9 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/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 ->
diff --git a/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java b/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java
index 778da668e..a94af95de 100644
--- a/infer/tests/codetoanalyze/java/pulse/InstanceOfExample.java
+++ b/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();
+    }
+  }
 }