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