[Infer][angelic] Adding angelic abduction on actuals passed by reference

infer/src/backend/cfg.ml

@@ -802,7 +802,7 @@ let remove_abducted_retvars p =
           let reach' = Sil.HpredSet.add hpred reach in
           let exps' = collect_exps exps rhs in
           (reach', exps')
-        | hpred -> reach, exps in
+        | _ -> reach, exps in
       let reach', exps' = list_fold_left add_hpred_if_reachable (reach, exps) sigma in
       if (Sil.HpredSet.cardinal reach) = (Sil.HpredSet.cardinal reach') then (reach, exps)
       else compute_reachable_hpreds_rec sigma (reach', exps') in
@@ -815,7 +815,7 @@ let remove_abducted_retvars p =
         match hpred with
         | Sil.Hpointsto (Sil.Lvar pvar, _, _) ->
           let abducted_pvars, normal_pvars = pvars in
-          if Sil.pvar_is_abducted_retvar pvar then pvar :: abducted_pvars, normal_pvars
+          if Sil.pvar_is_abducted pvar then pvar :: abducted_pvars, normal_pvars
           else abducted_pvars, pvar :: normal_pvars
         | _ -> pvars)
       ([], [])

infer/src/backend/interproc.ml

@@ -696,13 +696,11 @@ let collect_postconditions tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t =
   res
 
 let create_seed_vars sigma =
-  let sigma_seed = ref [] in
+  let hpred_add_seed sigma = function
-  let hpred_add_seed = function
+    | Sil.Hpointsto (Sil.Lvar pv, se, typ) when not (Sil.pvar_is_abducted pv) ->
-    | Sil.Hpointsto (Sil.Lvar pv, se, typ) ->
+      Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: sigma
-        sigma_seed := Sil.Hpointsto(Sil.Lvar (Sil.pvar_to_seed pv), se, typ) :: !sigma_seed
+    | _ -> sigma in
-    | _ -> () in
+  list_fold_left hpred_add_seed [] sigma
-  list_iter hpred_add_seed sigma;
-  !sigma_seed
 
 (** Initialize proposition for execution given formal and global
 parameters. The footprint is initialized according to the

infer/src/backend/prop.ml

@@ -1769,6 +1769,16 @@ let add_or_replace_exp_attribute check_attribute_change prop exp att =
   if !found then replace_pi pi' prop
   else set_exp_attribute prop nexp att
 
+(** mark Sil.Var's or Sil.Lvar's as undefined *)
+let mark_vars_as_undefined prop vars_to_mark callee_pname loc path_pos =
+  let att_undef = Sil.Aundef (callee_pname, loc, path_pos) in
+  let mark_var_as_undefined exp prop =
+    let do_nothing _ _ = () in
+    match exp with
+    | Sil.Var _ | Sil.Lvar _ -> add_or_replace_exp_attribute do_nothing prop exp att_undef
+    | _ -> prop in
+  list_fold_left (fun prop id -> mark_var_as_undefined id prop) prop vars_to_mark
+
 (** Remove an attribute from all the atoms in the heap *)
 let remove_attribute att prop =
   let atom_remove atom pi = match atom with

infer/src/backend/prop.mli

@@ -291,6 +291,10 @@ val get_all_attributes : 'a t -> (exp * attribute) list
 (** Replace an attribute associated to the expression *)
 val add_or_replace_exp_attribute : (Sil.attribute -> Sil.attribute -> unit) -> normal t -> exp -> attribute -> normal t
 
+(** mark Sil.Var's or Sil.Lvar's as undefined *)
+val mark_vars_as_undefined : normal t -> Sil.exp list -> Procname.t -> Sil.location ->
+  Sil.path_pos -> normal t
+
 (** Remove an attribute from all the atoms in the heap *)
 val remove_attribute : Sil.attribute -> 'a t -> normal t
 

infer/src/backend/sil.ml

@@ -150,11 +150,13 @@ type pvar_kind =
   | Local_var of Procname.t (** local variable belonging to a function *)
   | Callee_var of Procname.t (** local variable belonging to a callee *)
   | Abducted_retvar of Procname.t * location (** synthetic variable to represent return value *)
+  | Abducted_ref_param of Procname.t * pvar * location
+    (** synthetic variable to represent param passed by reference *)
   | Global_var (** gloval variable *)
   | Seed_var (** variable used to store the initial value of formal parameters *)
 
 (** Names for program variables. *)
-type pvar = { pv_name: Mangled.t; pv_kind: pvar_kind }
+and pvar = { pv_name: Mangled.t; pv_kind: pvar_kind }
 
 (** Unary operations *)
 type unop =
@@ -872,6 +874,11 @@ let has_objc_ref_counter hpred =
       list_exists is_objc_ref_counter_field fl
   | _ -> false
 
+(** turn a *T into a T. fails if [typ] is not a pointer type *)
+let typ_strip_ptr = function
+  | Tptr (t, _) -> t
+  | _ -> assert false
+
 let pvar_get_name pv = pv.pv_name
 
 let pvar_to_string pv = Mangled.to_string pv.pv_name
@@ -885,6 +892,12 @@ let pvar_get_simplified_name pv =
         | _ -> s)
   | _ -> s
 
+(** Check if the pvar is an abucted return var or param passed by ref *)
+let pvar_is_abducted pv =
+  match pv.pv_kind with
+  | Abducted_retvar _ | Abducted_ref_param _ -> true
+  | _ -> false
+
 (** Turn a pvar into a seed pvar (which stored the initial value) *)
 let pvar_to_seed pv = { pv with pv_kind = Seed_var }
 
@@ -900,12 +913,6 @@ let pvar_is_callee pv =
   | Callee_var _ -> true
   | _ -> false
 
-(** Check if the pvar is an abucted return var *)
-let pvar_is_abducted_retvar pv =
-  match pv.pv_kind with
-  | Abducted_retvar _ -> true
-  | _ -> false
-
 (** Check if the pvar is a seed var *)
 let pvar_is_seed pv =
   match pv.pv_kind with
@@ -942,24 +949,31 @@ let loc_compare loc1 loc2 =
 let loc_equal loc1 loc2 =
   loc_compare loc1 loc2 = 0
 
-let pv_kind_compare k1 k2 = match k1, k2 with
+let rec pv_kind_compare k1 k2 = match k1, k2 with
   | Local_var n1, Local_var n2 -> Procname.compare n1 n2
   | Local_var _, _ -> - 1
   | _, Local_var _ -> 1
   | Callee_var n1, Callee_var n2 -> Procname.compare n1 n2
   | Callee_var _, _ -> - 1
+  | _, Callee_var _ -> 1
   | Abducted_retvar (p1, l1), Abducted_retvar (p2, l2) ->
       let n = Procname.compare p1 p2 in
       if n <> 0 then n else loc_compare l1 l2
   | Abducted_retvar _, _ -> - 1
   | _, Abducted_retvar _ -> 1
-  | _, Callee_var _ -> 1
+  | Abducted_ref_param (p1, pv1, l1), Abducted_ref_param (p2, pv2, l2) ->
+      let n = Procname.compare p1 p2 in
+      if n <> 0 then n else
+        let n = pvar_compare pv1 pv2 in
+        if n <> 0 then n else loc_compare l1 l2
+  | Abducted_ref_param _, _ -> - 1
+  | _, Abducted_ref_param _ -> 1
   | Global_var, Global_var -> 0
   | Global_var, _ -> - 1
   | _, Global_var -> 1
   | Seed_var, Seed_var -> 0
 
-let pvar_compare pv1 pv2 =
+and pvar_compare pv1 pv2 =
   let n = Mangled.compare pv1.pv_name pv2.pv_name in
   if n <> 0 then n else pv_kind_compare pv1.pv_kind pv2.pv_kind
 
@@ -1768,7 +1782,7 @@ let loc_to_string loc =
 (** Dump a location *)
 let d_loc (loc: location) = L.add_print_action (L.PTloc, Obj.repr loc)
 
-let _pp_pvar f pv =
+let rec _pp_pvar f pv =
   let name = pv.pv_name in
   match pv.pv_kind with
   | Local_var n ->
@@ -1780,6 +1794,9 @@ let _pp_pvar f pv =
   | Abducted_retvar (n, l) ->
       if !Config.pp_simple then F.fprintf f "%a|abductedRetvar" Mangled.pp name
       else F.fprintf f "%a$%a%a|abductedRetvar" Procname.pp n pp_loc l Mangled.pp name
+  | Abducted_ref_param (n, pv, l) ->
+      if !Config.pp_simple then F.fprintf f "%a|%a|abductedRefParam" _pp_pvar pv Mangled.pp name
+      else F.fprintf f "%a$%a%a|abductedRefParam" Procname.pp n pp_loc l Mangled.pp name
   | Global_var -> F.fprintf f "#GB$%a" Mangled.pp name
   | Seed_var -> F.fprintf f "old_%a" Mangled.pp name
 
@@ -1795,6 +1812,9 @@ let pp_pvar_latex f pv =
   | Abducted_retvar (n, l) ->
       F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name)
         (Latex.pp_string Latex.Roman) "abductedRetvar"
+   | Abducted_ref_param (n, pv, l) ->
+      F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name)
+        (Latex.pp_string Latex.Roman) "abductedRefParam"
   | Global_var ->
       Latex.pp_string Latex.Boldface f (Mangled.to_string name)
   | Seed_var ->
@@ -3769,12 +3789,16 @@ let mk_pvar_abducted_ret (proc_name : Procname.t) (loc : location) : pvar =
   let name = Mangled.from_string ("$RET_" ^ (Procname.to_unique_id proc_name)) in
   { pv_name = name; pv_kind = Abducted_retvar (proc_name, loc) }
 
+let mk_pvar_abducted_ref_param (proc_name : Procname.t) (pv : pvar) (loc : location) : pvar =
+  let name = Mangled.from_string ("$REF_PARAM_" ^ (Procname.to_unique_id proc_name)) in
+  { pv_name = name; pv_kind = Abducted_ref_param (proc_name, pv, loc) }
+
 (** Turn an ordinary program variable into a callee program variable *)
 let pvar_to_callee pname pvar = match pvar.pv_kind with
   | Local_var _ ->
       { pvar with pv_kind = Callee_var pname }
   | Global_var -> pvar
-  | Callee_var _ | Abducted_retvar _ | Seed_var ->
+  | Callee_var _ | Abducted_retvar _ | Abducted_ref_param _ | Seed_var ->
       L.d_str "Cannot convert pvar to callee: ";
       d_pvar pvar; L.d_ln ();
       assert false

infer/src/backend/sil.mli

@@ -592,6 +592,9 @@ val loc_equal : location -> location -> bool
 
 val path_pos_equal : path_pos -> path_pos -> bool
 
+(** turn a *T into a T. fails if [typ] is not a pointer type *)
+val typ_strip_ptr : typ -> typ
+
 val pvar_get_name : pvar -> Mangled.t
 
 val pvar_to_string : pvar -> string
@@ -602,8 +605,8 @@ val pvar_to_seed : pvar -> pvar
 (** Check if the pvar is a callee var *)
 val pvar_is_callee : pvar -> bool
 
-(** Check if the pvar is an abducted return var *)
+(** Check if the pvar is an abducted return var or param passed by ref *)
-val pvar_is_abducted_retvar : pvar -> bool
+val pvar_is_abducted : pvar -> bool
 
 (** Check if the pvar is a local var *)
 val pvar_is_local : pvar -> bool
@@ -1324,6 +1327,8 @@ val mk_pvar_global : Mangled.t -> pvar
 (** create an abducted return variable for a call to [proc_name] at [loc] *)
 val mk_pvar_abducted_ret : Procname.t -> location -> pvar
 
+val mk_pvar_abducted_ref_param : Procname.t -> pvar -> location -> pvar
+
 (** Turn an ordinary program variable into a callee program variable *)
 val pvar_to_callee : Procname.t -> pvar -> pvar
 

infer/src/backend/symExec.ml

@@ -85,10 +85,6 @@ let check_block_retain_cycle cfg tenv pname _prop block_nullified =
   let _ = Abs.abstract_junk ~original_prop: _prop pname tenv _prop'' in
   ()
 
-let mark_id_as_undefined id prop att_undef =
-  let check_attr_change att_old att_new = () in
-  Prop.add_or_replace_exp_attribute check_attr_change prop (Sil.Var id) att_undef
-
 (** Apply function [f] to the expression at position [offlist] in [strexp].
 If not found, expand [strexp] and apply [f] to [None].
 The routine should maintain the invariant that strexp and typ correspond to
@@ -520,15 +516,12 @@ let call_should_be_skipped caller_pname callee_pname callee_pdesc =
     | None ->
         not (Cfg.Procdesc.is_defined callee_pdesc)
         (* treat calls with no specs as skip functions in angelic mode *)
-        (* TODO: turn angelic back on for C_CPP once we have abductive angelic analysis (t6935559) *)
+        || !Config.angelic_execution
-        || (!Config.angelic_execution && !Sil.curr_language <> Sil.C_CPP)
     | Some summary ->
         Specs.get_flag callee_pname proc_flag_skip <> None (* check skip flag *)
         || summary.Specs.attributes.Sil.is_abstract (* skip abstract methods *)
         (* treat calls with no specs as skip functions in angelic mode *)
-        (* TODO: turn angelic back on for C_CPP once we have abductive angelic analysis (t6935559) *)
+        || (!Config.angelic_execution && Specs.get_specs_from_payload summary == []) in
-        || (!Config.angelic_execution && !Sil.curr_language <> Sil.C_CPP
-          && Specs.get_specs_from_payload summary == []) in
   if !Config.intraprocedural then true
   else if should_skip () then (print_skip_warning (); true)
   else false
@@ -1040,114 +1033,158 @@ and sym_exec_generated mask_errors cfg tenv pdesc instrs ppl =
   let f plist instr = list_flatten (list_map (exe_instr instr) plist) in
   list_fold_left f ppl instrs
 
+and add_to_footprint abducted_pv typ prop =
+  let abducted_lvar = Sil.Lvar abducted_pv in
+  let fresh_fp_var = Sil.Var (Ident.create_fresh Ident.kfootprint) in
+  let lvar_pt_fpvar =
+    let sizeof_exp = Sil.Sizeof (typ, Sil.Subtype.subtypes) in
+    Prop.mk_ptsto abducted_lvar (Sil.Eexp (fresh_fp_var, Sil.Inone)) sizeof_exp in
+  let sigma_fp = Prop.get_sigma_footprint prop in
+  (Prop.normalize (Prop.replace_sigma_footprint (lvar_pt_fpvar :: sigma_fp) prop), fresh_fp_var)
+
+and add_constraints_on_retval pdesc prop ret_ids ret_type_option callee_pname =
+  if Procname.is_infer_undefined callee_pname then prop
+  else
+    match ret_ids, ret_type_option with
+    | [ret_id], Some ret_typ ->
+      (* To avoid obvious false positives, assume skip functions do not return null pointers *)
+      let add_ret_non_null ret_id ret_typ prop =
+        match ret_typ with
+        | Sil.Tptr _ -> Prop.conjoin_neq (Sil.Var ret_id) Sil.exp_zero prop
+        | _ -> prop in
+      let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *)
+        Procname.equal pname (Cfg.Procdesc.get_proc_name pdesc) 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 abducted_ret_pv = Sil.mk_pvar_abducted_ret callee_pname (State.get_loc ()) in
+        let already_has_abducted_retval p =
+          list_exists
+            (fun hpred -> match hpred with
+              | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ret_pv
+              | _ -> false)
+            (Prop.get_sigma_footprint p) in
+          (* prevent introducing multiple abducted retvals for a single call site in a loop *)
+        if already_has_abducted_retval prop then prop
+        else
+          if !Config.footprint then
+            let (prop', fresh_fp_var) = add_to_footprint abducted_ret_pv ret_typ prop in
+            let prop'' = Prop.conjoin_eq ~footprint:true (Sil.Var ret_id) fresh_fp_var prop' in
+            add_ret_non_null ret_id ret_typ prop''
+          else
+            (* find an hpred [abducted_pvar] |-> A in [prop] and add [exp] = A to prop *)
+            let bind_exp_to_abducted_val exp_to_bind abducted_pvar prop =
+              let bind_exp prop = function
+                | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (rhs, _), _)
+                  when Sil.pvar_equal pv abducted_pvar ->
+                  Prop.conjoin_eq exp_to_bind rhs prop
+                | _ -> prop in
+              list_fold_left bind_exp prop (Prop.get_sigma prop) in
+            (* bind return id to the abducted value pointed to by the pvar we introduced *)
+            bind_exp_to_abducted_val (Sil.Var ret_id) abducted_ret_pv prop
+      else add_ret_non_null ret_id ret_typ prop
+    | _ -> prop
+
+and add_constraints_on_actuals_by_ref prop actuals_by_ref callee_pname =
+  (* replace an hpred of the form actual_var |-> _ with new_hpred in prop *)
+  let replace_actual_hpred actual_var new_hpred prop =
+    let sigma' =
+      list_map
+        (function
+          | Sil.Hpointsto (lhs, _, _) when Sil.exp_equal lhs actual_var -> new_hpred
+          | hpred -> hpred)
+        (Prop.get_sigma prop) in
+    Prop.normalize (Prop.replace_sigma sigma' prop) in
+  if !Config.angelic_execution then
+    let add_actual_by_ref_to_footprint prop (actual, actual_typ) =
+      match actual with
+      | Sil.Lvar actual_pv ->
+        (* introduce a fresh program variable to allow abduction on the return value *)
+        let abducted_ref_pv =
+          Sil.mk_pvar_abducted_ref_param callee_pname actual_pv (State.get_loc ()) in
+        let already_has_abducted_retval p =
+          list_exists
+            (fun hpred -> match hpred with
+              | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv abducted_ref_pv
+              | _ -> false)
+            (Prop.get_sigma_footprint p) in
+          (* prevent introducing multiple abducted retvals for a single call site in a loop *)
+        if already_has_abducted_retval prop then prop
+        else
+          if !Config.footprint then
+            let (prop', fresh_fp_var) =
+              add_to_footprint abducted_ref_pv (Sil.typ_strip_ptr actual_typ) prop in
+            (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *)
+            let filtered_sigma =
+              list_map
+                (function
+                  | Sil.Hpointsto (lhs, _, typ_exp) when Sil.exp_equal lhs actual ->
+                    Sil.Hpointsto (lhs, Sil.Eexp (fresh_fp_var, Sil.Inone), typ_exp)
+                  | hpred -> hpred)
+                (Prop.get_sigma prop') in
+            Prop.normalize (Prop.replace_sigma filtered_sigma prop')
+          else
+            (* bind actual passed by ref to the abducted value pointed to by the synthetic pvar *)
+            let prop' =
+              let filtered_sigma =
+                list_filter
+                (function
+                  | Sil.Hpointsto (lhs, _, typ_exp) when Sil.exp_equal lhs actual ->
+                    false
+                  | _ -> true)
+                (Prop.get_sigma prop) in
+              Prop.normalize (Prop.replace_sigma filtered_sigma prop) in
+            list_fold_left
+              (fun p hpred ->
+                match hpred with
+                | Sil.Hpointsto (Sil.Lvar pv, rhs, texp) when Sil.pvar_equal pv abducted_ref_pv ->
+                  let new_hpred = Sil.Hpointsto (actual, rhs, texp) in
+                  Prop.normalize (Prop.replace_sigma (new_hpred :: (Prop.get_sigma prop')) p)
+                | _ -> p)
+              prop'
+              (Prop.get_sigma prop')
+      | _ -> assert false in
+    list_fold_left add_actual_by_ref_to_footprint prop actuals_by_ref
+  else
+    (* non-angelic mode; havoc each var passed by reference by assigning it to a fresh id *)
+    let havoc_actual_by_ref (actual, actual_typ) prop =
+      let actual_pt_havocd_var =
+        let havocd_var = Sil.Var (Ident.create_fresh Ident.kprimed) in
+        let sizeof_exp = Sil.Sizeof (Sil.typ_strip_ptr actual_typ, Sil.Subtype.subtypes) in
+        Prop.mk_ptsto actual (Sil.Eexp (havocd_var, Sil.Inone)) sizeof_exp in
+      replace_actual_hpred actual actual_pt_havocd_var prop in
+    list_fold_left (fun p var -> havoc_actual_by_ref var p) prop actuals_by_ref
+
 (** execute a call for an unknown or scan function *)
 and call_unknown_or_scan is_scan cfg pdesc tenv pre path
     ret_ids ret_type_option actual_pars callee_pname loc =
-  let instrs, undef_vars = (* instructions to set vars passed by reference to fresh ids *)
-    let gen_instrs = ref [] in
-    let gen_undef_vars = ref [] in
-    let add_instr instr = gen_instrs := instr :: !gen_instrs in
-    let add_undef_var var = gen_undef_vars := var :: !gen_undef_vars in
-    let type_is_not_structured = function
-      | Sil.Tint _ | Sil.Tfloat _ | Sil.Tvoid | Sil.Tfun _ | Sil.Tptr _ | Sil.Tenum _ -> true
-      | Sil.Tvar _ | Sil.Tstruct _ | Sil.Tarray _ -> false in
-    let expand_ptr_type t = match t with
-      | Sil.Tptr (Sil.Tvar tn, pk) ->
-          (match Sil.tenv_lookup tenv tn with
-            | Some typ -> Sil.Tptr (typ, pk)
-            | None -> t)
-      | _ -> t in
-    let do_actual_par (e, _t) =
-      let t = expand_ptr_type _t in
-      L.d_str "do_actual_par exp: "; Sil.d_exp e; L.d_str" typ: "; Sil.d_typ_full t; L.d_ln();
-      match e, t with
-      | _, Sil.Tptr (Sil.Tint ik, pk) when is_scan && Sil.ikind_is_char ik -> (* scan case "%s" *)
-          let infer_get_array_size = Procname.from_string "__get_array_size" in
-          let instr1 = Sil.Call ([], Sil.Const (Sil.Cfun infer_get_array_size), [(e, Sil.Tptr (Sil.Tint ik, pk))], loc, Sil.cf_default) in
-          let id_fresh = Ident.create_fresh Ident.kprimed in
-          let instr2 = Sil.Letderef (id_fresh, e, t, loc) in
-          add_instr instr1;
-          add_instr instr2
-      | Sil.Lvar _, Sil.Tptr (t', _) when type_is_not_structured t' ->
-          let id_fresh = Ident.create_fresh Ident.kprimed in
-          let instr = Sil.Set (e, t, Sil.Var id_fresh, loc) in
-          add_instr instr;
-          add_undef_var id_fresh
-      | Sil.Lvar _, Sil.Tptr ((Sil.Tstruct (ftal, sftal, _, _, _, _, _) as tstruct, _)) ->
-          let do_fld (f, typ, ann) =
-            let id_fresh = Ident.create_fresh Ident.kprimed in
-            let instr = Sil.Set (Sil.Lfield (e, f, tstruct), typ, Sil.Var id_fresh, loc) in
-            add_instr instr;
-            add_undef_var id_fresh in
-          list_iter do_fld ftal
-      | _ -> () in
-    list_iter do_actual_par actual_pars;
-    list_rev !gen_instrs, list_rev !gen_undef_vars in
   let remove_resource_att prop =
     let do_exp p (e, t) =
       let do_attribute q = function
         | Sil.Aresource _ as res ->
-            Prop.remove_attribute res q
+          Prop.remove_attribute res q
         | _ -> q in
       list_fold_left do_attribute p (Prop.get_exp_attributes p e) in
     list_fold_left do_exp prop actual_pars in
-  let prop =
+  let actuals_by_ref =
-    if !Sil.curr_language <> Sil.Java || Procname.is_infer_undefined callee_pname then pre
+    list_filter
-    else
+      (function
-      let prop_no_res = remove_resource_att pre in
+        | Sil.Lvar _, _ -> true
-      match ret_ids, ret_type_option with
+        | _ -> false)
-      | [ret_id], Some ret_typ ->
+      actual_pars in
-      (* To avoid obvious false positives, assume skip functions do not return null pointers *)
+  (* in Java, assume that skip functions close resources passed as params *)
-          let add_ret_non_null ret_id ret_typ prop =
+  let pre' = if !Sil.curr_language = Sil.Java then remove_resource_att pre else pre in
-            match ret_typ with
+  let pre'' = add_constraints_on_retval pdesc pre' ret_ids ret_type_option callee_pname in
-            | Sil.Tptr _ -> Prop.conjoin_neq (Sil.Var ret_id) Sil.exp_zero prop
+  let pre''' = add_constraints_on_actuals_by_ref pre'' actuals_by_ref callee_pname in
-            | _ -> prop in
+  if is_scan (* if scan function, don't mark anything with undef attributes *)
-          let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *)
+  then [(Tabulation.remove_constant_string_class pre''', path)]
-            Procname.equal pname (Cfg.Procdesc.get_proc_name pdesc) in
+  else
-          if !Config.angelic_execution && not (is_rec_call callee_pname) then
+    (* otherwise, add undefined attribute to retvals and actuals passed by ref *)
-            (* introduce a fresh program variable to allow abduction on the return value *)
+    let exps_to_mark =
-            let ret_pv = Sil.mk_pvar_abducted_ret callee_pname (State.get_loc ()) in
+      let ret_exps = list_map (fun ret_id -> Sil.Var ret_id) ret_ids in
-            let already_has_abducted_retval p =
+      list_fold_left
-              list_exists
+        (fun exps_to_mark (exp, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in
-                (fun hpred -> match hpred with
+    let path_pos = State.get_path_pos () in
-                      | Sil.Hpointsto (Sil.Lvar pv, _, _) -> Sil.pvar_equal pv ret_pv
+    [(Prop.mark_vars_as_undefined pre''' exps_to_mark callee_pname loc path_pos, path)]
-                      | _ -> false
-                )
-                (Prop.get_sigma_footprint p) in
-            (* prevent introducing multiple abducted retvals for a single call site in a loop *)
-            if already_has_abducted_retval prop_no_res then prop_no_res
-            else
-              let ret_lvar = Sil.Lvar ret_pv in
-              let sizeof_exp = Sil.Sizeof (ret_typ, Sil.Subtype.subtypes) in
-              if !Config.footprint then
-                let fresh_fp_var = Sil.Var (Ident.create_fresh Ident.kfootprint) in
-                let retval_pt_fpvar =
-                  Prop.mk_ptsto ret_lvar (Sil.Eexp (fresh_fp_var, Sil.Inone)) sizeof_exp in
-                let sigma_fp = Prop.get_sigma_footprint prop_no_res in
-                let prop = Prop.replace_sigma_footprint (retval_pt_fpvar :: sigma_fp) prop_no_res in
-                let prop' = Prop.normalize prop in
-                let prop'' = Prop.conjoin_eq ~footprint: true (Sil.Var ret_id) fresh_fp_var prop' in
-                add_ret_non_null ret_id ret_typ prop''
-              else
-                (* bind return id to the abducted value pointed to by the pvar we introduced *)
-                let bind_return_id prop = function
-                  | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (rhs, _), _)
-                  when Sil.pvar_equal pv ret_pv ->
-                      Prop.conjoin_eq (Sil.Var ret_id) rhs prop
-                  | _ -> prop in
-                list_fold_left bind_return_id prop_no_res (Prop.get_sigma prop_no_res)
-          else add_ret_non_null ret_id ret_typ prop_no_res
-      | _ -> prop_no_res in
-  let after_ref_var_instrs = (* assign fresh values to vars passed by ref *)
-    let report_error = is_scan in
-    sym_exec_generated (not report_error) cfg tenv pdesc instrs [(prop, path)] in
-  let vars_to_mark_undefined = ret_ids @ undef_vars in
-  let att_undef = Sil.Aundef (callee_pname, loc, State.get_path_pos ()) in
-  let mark_undefined_vars p = (* add undefined attribute to returned vars and new values for vars passed by ref *)
-    list_fold_left (fun p id -> mark_id_as_undefined id p att_undef) p vars_to_mark_undefined in
-  if is_scan (* if scan function, don't mark values with undef attributes *)
-  then list_map (fun (p, path) -> (Tabulation.remove_constant_string_class p, path)) after_ref_var_instrs
-  else list_map (fun (p, path) -> (mark_undefined_vars p, path)) after_ref_var_instrs
 
 (** Perform symbolic execution for a function call *)
 and sym_exe_call cfg pdesc tenv pre path ret_ids actual_pars callee_pdesc loc =

infer/tests/codetoanalyze/c/errors/null_dereference/angelism.c

@@ -40,3 +40,43 @@ struct delicious *skip_external_function(void) {
   i = cake->yum;
   return cake;
 }
+
+void by_ref_actual_already_in_footprint(struct delicious *param) {
+  int i;
+  struct delicious * ret = bakery(&param);
+  i = param->yum;
+}
+
+void call_by_ref_actual_already_in_footprint_ok() {
+  by_ref_actual_already_in_footprint(NULL); // should not report a warning
+}
+
+void by_ref_actual_already_in_footprint2(struct delicious *param) {
+  int i;
+  i = param->yum;  // should not report a warning
+  struct delicious * ret = bakery(&param);
+  i = param->yum;  // should not report a warning
+}
+
+void call_by_ref_actual_already_in_footprint_bad() {
+  by_ref_actual_already_in_footprint2(NULL); // should report a warning
+}
+
+void passByRefTwice() {
+  struct delicious *param;
+  bakery2(&param, &param); // should not report a warning
+  int i = param->yum;
+}
+
+struct delicious * returnPassByRef2() {
+  struct delicious *param = NULL;
+  bakery(&param);
+  int i = param->yum; // should not report a warning
+  return param;
+}
+
+void returnPassByRefDeref() {
+  struct delicious *ret = returnPassByRef();
+  ret->yum = 2; // should not report a warning
+  free(ret);
+}

infer/tests/endtoend/c/AngelismTest.java

@@ -37,6 +37,7 @@ public class AngelismTest {
   public void angelismTest() throws InterruptedException, IOException, InferException {
     String[] procedures = {
         "bake",
+        "call_by_ref_actual_already_in_footprint_bad"
     };
     assertThat(
         "Results should contain null pointer dereference error",