From 15a8848502b68f144fb503361751ffffbb15acb7 Mon Sep 17 00:00:00 2001
From: Jeremy Dubreil <jrm@fb.com>
Date: Tue, 1 Aug 2017 10:16:45 -0700
Subject: [PATCH] [infer][biabduction] always reuse the same abduced return
 variable for unknown methods in Java

Summary:
This is unsound but will help the analysis to report less false alarms with the common pattern:

  if (a.get() != null) {
    a.get().foo();
  }

Reviewed By: sblackshear

Differential Revision: D5528227

fbshipit-source-id: 750db4a
---
 infer/src/backend/symExec.ml                  | 39 +++++++++++--------
 .../java/infer/NullPointerExceptions.java     |  6 +++
 2 files changed, 28 insertions(+), 17 deletions(-)

diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 0c25350e7..87b30dda3 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -902,14 +902,14 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca
       (* TODO: (t7147096) extend this to detect mutual recursion *)
       Typ.Procname.equal pname (Procdesc.get_proc_name pdesc)
     in
-    let already_has_abduced_retval p abduced_ret_pv =
-      List.exists
+    let lookup_abduced_expression p abduced_ret_pv =
+      List.find_map
         ~f:(fun hpred ->
           match hpred with
-          | Sil.Hpointsto (Exp.Lvar pv, _, _)
-           -> Pvar.equal pv abduced_ret_pv
+          | Sil.Hpointsto (Exp.Lvar pv, _, exp) when Pvar.equal pv abduced_ret_pv
+           -> Some exp
           | _
-           -> false)
+           -> None)
         p.Prop.sigma_fp
     in
     (* find an hpred [abduced] |-> A in [prop] and add [exp] = A to prop *)
@@ -931,19 +931,24 @@ let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ ca
     in
     if Config.angelic_execution && not (is_rec_call callee_pname) then
       (* introduce a fresh program variable to allow abduction on the return value *)
-      let abduced_ret_pv = Pvar.mk_abduced_ret callee_pname callee_loc in
-      (* prevent introducing multiple abduced retvals for a single call site in a loop *)
-      if already_has_abduced_retval prop abduced_ret_pv then prop
-      else
-        let prop' =
-          if !Config.footprint then
-            let prop', fresh_fp_var = add_to_footprint tenv abduced_ret_pv typ prop in
-            Prop.conjoin_eq tenv ~footprint:true ret_exp fresh_fp_var prop'
-          else
-            (* bind return id to the abduced value pointed to by the pvar we introduced *)
-            bind_exp_to_abduced_val ret_exp abduced_ret_pv prop
+      let prop_with_abduced_var =
+        let abduced_ret_pv =
+          (* in Java, always re-use the same abduced ret var to prevent false alarms with repeated method calls *)
+          let loc = if Typ.Procname.is_java callee_pname then Location.dummy else callee_loc in
+          Pvar.mk_abduced_ret callee_pname loc
         in
-        add_ret_non_null ret_exp typ prop'
+        if !Config.footprint then
+          match lookup_abduced_expression prop abduced_ret_pv with
+          | None
+           -> let p, fp_var = add_to_footprint tenv abduced_ret_pv typ prop in
+              Prop.conjoin_eq tenv ~footprint:true ret_exp fp_var p
+          | Some exp
+           -> Prop.conjoin_eq tenv ~footprint:true ret_exp exp prop
+        else
+          (* bind return id to the abduced value pointed to by the pvar we introduced *)
+          bind_exp_to_abduced_val ret_exp abduced_ret_pv prop
+      in
+      add_ret_non_null ret_exp typ prop_with_abduced_var
     else add_ret_non_null ret_exp typ prop
 
 let execute_load ?(report_deref_errors= true) pname pdesc tenv id rhs_exp typ loc prop_ =
diff --git a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
index 937952bf1..b06b6adbe 100644
--- a/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
+++ b/infer/tests/codetoanalyze/java/infer/NullPointerExceptions.java
@@ -434,6 +434,12 @@ public class NullPointerExceptions {
     }
   }
 
+  void assumeUndefNullableIdempotentOk() {
+    if (undefNullableRet() != null) {
+      undefNullableRet().toString();
+    }
+  }
+
   public Object undefNullableWrapper() {
     return undefNullableRet();
   }