[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

@@ -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 =
+    let lookup_abduced_expression p abduced_ret_pv =
-      List.exists
+      List.find_map
         ~f:(fun hpred ->
           match hpred with
-          | Sil.Hpointsto (Exp.Lvar pv, _, _)
+          | Sil.Hpointsto (Exp.Lvar pv, _, exp) when Pvar.equal pv abduced_ret_pv
-           -> 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
+      let prop_with_abduced_var =
-      (* prevent introducing multiple abduced retvals for a single call site in a loop *)
+        let abduced_ret_pv =
-      if already_has_abduced_retval prop abduced_ret_pv then prop
+          (* in Java, always re-use the same abduced ret var to prevent false alarms with repeated method calls *)
-      else
+          let loc = if Typ.Procname.is_java callee_pname then Location.dummy else callee_loc in
-        let prop' =
+          Pvar.mk_abduced_ret callee_pname loc
-          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
         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_ =

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();
   }