Preserve the name of abduced by-ref logical variables in re-execution phase

Reviewed By: jeremydubreil

Differential Revision: D5432727

fbshipit-source-id: cd48bf2

infer/src/IR/Pvar.ml

@@ -22,8 +22,7 @@ type pvar_kind =
   | Callee_var of Typ.Procname.t  (** local variable belonging to a callee *)
   | Abduced_retvar of Typ.Procname.t * Location.t
       (** synthetic variable to represent return value *)
-  | Abduced_ref_param of Typ.Procname.t * t * Location.t
-  | Abduced_ref_param_val of Typ.Procname.t * Ident.t * Location.t
+  | Abduced_ref_param of Typ.Procname.t * int * Location.t
       (** synthetic variable to represent param passed by reference *)
   | Global_var of (translation_unit * bool * bool * bool)
       (** global variable: translation unit + is it compile constant? + is it POD? + is it a static
@@ -42,7 +41,7 @@ let pp_translation_unit fmt = function
   | TUExtern
    -> Format.fprintf fmt "EXTERN"
 
-let rec _pp f pv =
+let _pp f pv =
   let name = pv.pv_name in
   match pv.pv_kind with
   | Local_var n
@@ -54,13 +53,9 @@ let rec _pp f pv =
   | Abduced_retvar (n, l)
    -> if !Config.pp_simple then F.fprintf f "%a|abducedRetvar" Mangled.pp name
       else F.fprintf f "%a$%a%a|abducedRetvar" Typ.Procname.pp n Location.pp l Mangled.pp name
-  | Abduced_ref_param (n, pv, l)
-   -> if !Config.pp_simple then F.fprintf f "%a|%a|abducedRefParam" _pp pv Mangled.pp name
+  | Abduced_ref_param (n, index, l)
+   -> if !Config.pp_simple then F.fprintf f "%a|abducedRefParam%d" Mangled.pp name index
       else F.fprintf f "%a$%a%a|abducedRefParam" Typ.Procname.pp n Location.pp l Mangled.pp name
-  | Abduced_ref_param_val (n, id, l)
-   -> if !Config.pp_simple then
-        F.fprintf f "%a|%a|abducedRefParamVal" (Ident.pp Pp.text) id Mangled.pp name
-      else F.fprintf f "%a$%a%a|abducedRefParamVal" Typ.Procname.pp n Location.pp l Mangled.pp name
   | Global_var (translation_unit, is_const, is_pod, _)
    -> F.fprintf f "#GB<%a%s%s>$%a" pp_translation_unit translation_unit
         (if is_const then "|const" else "")
@@ -84,9 +79,6 @@ let pp_latex f pv =
   | Abduced_ref_param _
    -> F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name)
         (Latex.pp_string Latex.Roman) "abducedRefParam"
-  | Abduced_ref_param_val _
-   -> F.fprintf f "%a_{%a}" (Latex.pp_string Latex.Roman) (Mangled.to_string name)
-        (Latex.pp_string Latex.Roman) "abducedRefParamVal"
   | Global_var _
    -> Latex.pp_string Latex.Boldface f (Mangled.to_string name)
   | Seed_var
@@ -125,11 +117,7 @@ let get_simplified_name pv =
 
 (** Check if the pvar is an abucted return var or param passed by ref *)
 let is_abduced pv =
-  match pv.pv_kind with
-  | Abduced_retvar _ | Abduced_ref_param _ | Abduced_ref_param_val _
-   -> true
-  | _
-   -> false
+  match pv.pv_kind with Abduced_retvar _ | Abduced_ref_param _ -> true | _ -> false
 
 (** Turn a pvar into a seed pvar (which stored the initial value) *)
 let to_seed pv = {pv with pv_kind= Seed_var}
@@ -193,7 +181,7 @@ let to_callee pname pvar =
    -> {pvar with pv_kind= Callee_var pname}
   | Global_var _
    -> pvar
-  | Callee_var _ | Abduced_retvar _ | Abduced_ref_param _ | Abduced_ref_param_val _ | Seed_var
+  | Callee_var _ | Abduced_retvar _ | Abduced_ref_param _ | Seed_var
    -> L.d_str "Cannot convert pvar to callee: " ;
       d pvar ;
       L.d_ln () ;
@@ -230,13 +218,9 @@ let mk_abduced_ret (proc_name: Typ.Procname.t) (loc: Location.t) : t =
   let name = Mangled.from_string ("$RET_" ^ Typ.Procname.to_unique_id proc_name) in
   {pv_hash= name_hash name; pv_name= name; pv_kind= Abduced_retvar (proc_name, loc)}
 
-let mk_abduced_ref_param (proc_name: Typ.Procname.t) (pv: t) (loc: Location.t) : t =
-  let name = Mangled.from_string ("$REF_PARAM_" ^ Typ.Procname.to_unique_id proc_name) in
-  {pv_hash= name_hash name; pv_name= name; pv_kind= Abduced_ref_param (proc_name, pv, loc)}
-
-let mk_abduced_ref_param_val (proc_name: Typ.Procname.t) (id: Ident.t) (loc: Location.t) : t =
+let mk_abduced_ref_param (proc_name: Typ.Procname.t) (index: int) (loc: Location.t) : t =
   let name = Mangled.from_string ("$REF_PARAM_VAL_" ^ Typ.Procname.to_unique_id proc_name) in
-  {pv_hash= name_hash name; pv_name= name; pv_kind= Abduced_ref_param_val (proc_name, id, loc)}
+  {pv_hash= name_hash name; pv_name= name; pv_kind= Abduced_ref_param (proc_name, index, loc)}
 
 let get_translation_unit pvar =
   match pvar.pv_kind with

infer/src/IR/Pvar.mli

@@ -78,10 +78,7 @@ val is_ssa_frontend_tmp : t -> bool
 val mk : Mangled.t -> Typ.Procname.t -> t
 (** [mk name proc_name suffix] creates a program var with the given function name and suffix *)
 
-val mk_abduced_ref_param : Typ.Procname.t -> t -> Location.t -> t
-(** create an abduced variable for a parameter passed by reference *)
-
-val mk_abduced_ref_param_val : Typ.Procname.t -> Ident.t -> Location.t -> t
+val mk_abduced_ref_param : Typ.Procname.t -> int -> Location.t -> t
 (** create an abduced variable for a parameter passed by reference *)
 
 val mk_abduced_ret : Typ.Procname.t -> Location.t -> t

infer/src/backend/symExec.ml

@@ -1437,15 +1437,13 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
     in
     Prop.normalize tenv (Prop.set prop ~sigma:sigma')
   in
-  let add_actual_by_ref_to_footprint prop (actual, actual_typ, _) =
+  let add_actual_by_ref_to_footprint prop (actual, actual_typ, actual_index) =
     let abduced =
       match actual with
-      | Exp.Lvar actual_pv
-       -> Pvar.mk_abduced_ref_param callee_pname actual_pv callee_loc
-      | Exp.Var actual_id
-       -> Pvar.mk_abduced_ref_param_val callee_pname actual_id callee_loc
+      | Exp.Lvar _ | Exp.Var _
+       -> Pvar.mk_abduced_ref_param callee_pname actual_index callee_loc
       | _
-       -> assert false
+       -> failwithf "Unexpected variable expression %a" Exp.pp actual
     in
     let already_has_abduced_retval p =
       List.exists
@@ -1473,7 +1471,6 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
         | _
          -> failwith ("No need for abduction on non-pointer type " ^ Typ.to_string actual_typ)
       in
-      (* replace [actual] |-> _ with [actual] |-> [fresh_fp_var] *)
       let filtered_sigma =
         List.map
           ~f:(function

infer/tests/codetoanalyze/objc/errors/issues.exp

@@ -3,7 +3,6 @@ codetoanalyze/objc/errors/global_const/global_const.m, SimpleRoot_doSomethingBad
 codetoanalyze/objc/errors/global_const/global_const.m, SimpleRoot_doSomethingOkWithDict:andString:, 3, NULL_DEREFERENCE, [start of procedure doSomethingOkWithDict:andString:,Message stringByAppendingString: with receiver nil returns nil.]
 codetoanalyze/objc/errors/initialization/compound_literal.c, init_with_compound_literal, 2, DIVIDE_BY_ZERO, [start of procedure init_with_compound_literal()]
 codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m, testCycle, 3, RETAIN_CYCLE, [start of procedure testCycle(),start of procedure init,return from a call to CADisplay_init]
-codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m, testNoCycle_FP, 4, MEMORY_LEAK, [start of procedure testNoCycle_FP(),start of procedure init,return from a call to CADisplay_init,start of procedure invalidate,return from a call to CADisplay_invalidate,start of procedure dealloc,Skipped call: function or method not found,return from a call to CADisplay_dealloc]
 codetoanalyze/objc/errors/memory_leaks_benchmark/RetainCycleStaticVar.m, RetainCSVycleStaticVar, 2, RETAIN_CYCLE, [start of procedure RetainCSVycleStaticVar(),start of procedure init,return from a call to RetainCSV_init,start of procedure foo,start of procedure block,start of procedure init,return from a call to RetainCSV_init,return from a call to __objc_anonymous_block_RetainCSV_foo______3,start of procedure block,start of procedure init,return from a call to RetainCSV_init,return from a call to __objc_anonymous_block_RetainCSV_foo______2,return from a call to RetainCSV_foo]
 codetoanalyze/objc/errors/npe/blockenum.m, BlockEnumA_allResultsList:, 1, MEMORY_LEAK, [start of procedure allResultsList:,Skipped call: function or method not found]
 codetoanalyze/objc/errors/npe/blockenum.m, BlockEnumA_allResultsList:, 2, RETURN_VALUE_IGNORED, [start of procedure allResultsList:,Skipped call: function or method not found,Condition is true]

infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m

@@ -45,7 +45,7 @@ void testCycle() {
   CADisplay* b = a;
 }
 
-void testNoCycle_FP() {
+void testNoCycle() {
 
   CADisplay* a = [[CADisplay alloc] init];
   [a invalidate]; // break the cycle