diff --git a/infer/src/IR/Pvar.ml b/infer/src/IR/Pvar.ml index e8da4f543..40c9e2522 100644 --- a/infer/src/IR/Pvar.ml +++ b/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 diff --git a/infer/src/IR/Pvar.mli b/infer/src/IR/Pvar.mli index 612108925..b86d3b31d 100644 --- a/infer/src/IR/Pvar.mli +++ b/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 diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 11fe48d06..ced714079 100644 --- a/infer/src/backend/symExec.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/objc/errors/issues.exp b/infer/tests/codetoanalyze/objc/errors/issues.exp index c83d5069e..7f044201e 100644 --- a/infer/tests/codetoanalyze/objc/errors/issues.exp +++ b/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] diff --git a/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m b/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m index 90e3daf8c..36ab7a67f 100644 --- a/infer/tests/codetoanalyze/objc/errors/memory_leaks_benchmark/CADisplayLinkRetainCycle.m +++ b/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