From c094a38d5672fba48825895382c4985a443d04d5 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 28 Sep 2016 04:38:50 -0700 Subject: [PATCH] [IR] Simplify to single return id, with type Summary: Change Sil.Call instruction to have only a single optional return identifier, insted of a list. Essentially none of the code handled multiple return identifiers. Also, add the type of the return identitifier to Call instructions. Reviewed By: sblackshear Differential Revision: D3919358 fbshipit-source-id: d2d4f72 --- infer/src/IR/Cfg.re | 27 +++-- infer/src/IR/Sil.re | 69 ++++++++---- infer/src/IR/Sil.rei | 7 +- infer/src/backend/builtin.ml | 2 +- infer/src/backend/builtin.mli | 2 +- infer/src/backend/errdesc.ml | 6 +- infer/src/backend/modelBuiltins.ml | 110 +++++++++---------- infer/src/backend/preanal.ml | 12 +- infer/src/backend/symExec.ml | 87 +++++++-------- infer/src/backend/tabulation.ml | 50 +++++---- infer/src/backend/tabulation.mli | 4 +- infer/src/checkers/annotationReachability.ml | 6 +- infer/src/checkers/checkers.ml | 2 +- infer/src/checkers/constantPropagation.ml | 4 +- infer/src/checkers/copyPropagation.ml | 8 +- infer/src/checkers/liveness.ml | 8 +- infer/src/checkers/patternMatch.ml | 2 +- infer/src/checkers/repeatedCallsChecker.ml | 6 +- infer/src/clang/cArithmetic_trans.ml | 2 +- infer/src/clang/cTrans.ml | 32 +++--- infer/src/clang/cTrans_utils.ml | 11 +- infer/src/eradicate/typeCheck.ml | 17 ++- infer/src/harness/inhabit.ml | 9 +- infer/src/java/jTrans.ml | 40 ++++--- infer/src/java/jTransExn.ml | 6 +- infer/src/java/jTransStaticField.ml | 3 +- infer/src/llvm/lTrans.ml | 3 +- infer/src/quandary/TaintAnalysis.ml | 21 ++-- infer/src/unit/BoundedCallTreeTests.ml | 22 ++-- infer/src/unit/TaintTests.ml | 6 +- infer/src/unit/analyzerTester.ml | 14 +-- infer/src/unit/livenessTests.ml | 2 +- 32 files changed, 323 insertions(+), 277 deletions(-) diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 2604dcbe8..84a33503d 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -1175,7 +1175,7 @@ let save_attributes source_file cfg => { /** Inline a synthetic (access or bridge) method. */ -let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr => { +let inline_synthetic_method ret_id etl proc_desc loc_call :option Sil.instr => { let modified = ref None; let debug = false; let found instr instr' => { @@ -1186,15 +1186,16 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr => } }; let do_instr _ instr => - switch (instr, ret_ids, etl) { + switch (instr, ret_id, etl) { | ( Sil.Load _ (Exp.Lfield (Exp.Var _) fn ft) bt _, - [ret_id], + Some (ret_id, _), [(e1, _)] /* getter for fields */ ) => let instr' = Sil.Load ret_id (Exp.Lfield e1 fn ft) bt loc_call; found instr instr' - | (Sil.Load _ (Exp.Lfield (Exp.Lvar pvar) fn ft) bt _, [ret_id], []) when Pvar.is_global pvar => + | (Sil.Load _ (Exp.Lfield (Exp.Lvar pvar) fn ft) bt _, Some (ret_id, _), []) + when Pvar.is_global pvar => /* getter for static fields */ let instr' = Sil.Load ret_id (Exp.Lfield (Exp.Lvar pvar) fn ft) bt loc_call; found instr instr' @@ -1209,21 +1210,19 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr => /* setter for static fields */ let instr' = Sil.Store (Exp.Lfield (Exp.Lvar pvar) fn ft) bt e1 loc_call; found instr instr' - | (Sil.Call ret_ids' (Exp.Const (Const.Cfun pn)) etl' _ cf, _, _) - when IList.length ret_ids == IList.length ret_ids' && IList.length etl' == IList.length etl => - let instr' = Sil.Call ret_ids (Exp.Const (Const.Cfun pn)) etl loc_call cf; + | (Sil.Call ret_id' (Exp.Const (Const.Cfun pn)) etl' _ cf, _, _) + when ret_id == None == (ret_id' == None) && IList.length etl' == IList.length etl => + let instr' = Sil.Call ret_id (Exp.Const (Const.Cfun pn)) etl loc_call cf; found instr instr' - | (Sil.Call ret_ids' (Exp.Const (Const.Cfun pn)) etl' _ cf, _, _) - when - IList.length ret_ids == IList.length ret_ids' && - IList.length etl' + 1 == IList.length etl => + | (Sil.Call ret_id' (Exp.Const (Const.Cfun pn)) etl' _ cf, _, _) + when ret_id == None == (ret_id' == None) && IList.length etl' + 1 == IList.length etl => let etl1 = switch (IList.rev etl) { /* remove last element */ | [_, ...l] => IList.rev l | [] => assert false }; - let instr' = Sil.Call ret_ids (Exp.Const (Const.Cfun pn)) etl1 loc_call cf; + let instr' = Sil.Call ret_id (Exp.Const (Const.Cfun pn)) etl1 loc_call cf; found instr instr' | _ => () }; @@ -1236,7 +1235,7 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr => let proc_inline_synthetic_methods cfg proc_desc :unit => { let instr_inline_synthetic_method = fun - | Sil.Call ret_ids (Exp.Const (Const.Cfun pn)) etl loc _ => + | Sil.Call ret_id (Exp.Const (Const.Cfun pn)) etl loc _ => switch (Procdesc.find_from_name cfg pn) { | Some pd => let is_access = Procname.java_is_access_method pn; @@ -1244,7 +1243,7 @@ let proc_inline_synthetic_methods cfg proc_desc :unit => { let is_synthetic = attributes.ProcAttributes.is_synthetic_method; let is_bridge = attributes.ProcAttributes.is_bridge_method; if (is_access || is_bridge || is_synthetic) { - inline_synthetic_method ret_ids etl pd loc + inline_synthetic_method ret_id etl pd loc } else { None } diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 95b54b7d3..a7fe4a66d 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -50,10 +50,9 @@ type instr = | Store of Exp.t Typ.t Exp.t Location.t /** prune the state based on [exp=1], the boolean indicates whether true branch */ | Prune of Exp.t Location.t bool if_kind - /** [Call (ret_id1..ret_idn, e_fun, arg_ts, loc, call_flags)] represents an instructions - [ret_id1..ret_idn = e_fun(arg_ts);] - where n = 0 for void return and n > 1 for struct return */ - | Call of (list Ident.t) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t + /** [Call (ret_id, e_fun, arg_ts, loc, call_flags)] represents an instruction + [ret_id = e_fun(arg_ts);]. The return value is ignored when [ret_id = None]. */ + | Call of (option (Ident.t, Typ.t)) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t /** nullify stack variable */ | Nullify of Pvar.t Location.t | Abstract of Location.t /** apply abstraction */ @@ -667,7 +666,7 @@ let instr_get_exps = | Load id e _ _ => [Exp.Var id, e] | Store e1 _ e2 _ => [e1, e2] | Prune cond _ _ _ => [cond] - | Call ret_ids e _ _ _ => [e, ...(IList.map (fun id => Exp.Var id)) ret_ids] + | Call ret_id e _ _ _ => [e, ...Option.map_default (fun (id, _) => [Exp.Var id]) [] ret_id] | Nullify pvar _ => [Exp.Lvar pvar] | Abstract _ => [] | Remove_temps temps _ => IList.map (fun id => Exp.Var id) temps @@ -684,10 +683,10 @@ let pp_instr pe0 f instr => { F.fprintf f "*%a:%a=%a %a" (pp_exp pe) e1 (Typ.pp pe) t (pp_exp pe) e2 Location.pp loc | Prune cond loc true_branch _ => F.fprintf f "PRUNE(%a, %b); %a" (pp_exp pe) cond true_branch Location.pp loc - | Call ret_ids e arg_ts loc cf => - switch ret_ids { - | [] => () - | _ => F.fprintf f "%a=" (pp_comma_seq (Ident.pp pe)) ret_ids + | Call ret_id e arg_ts loc cf => + switch ret_id { + | None => () + | Some (id, _) => F.fprintf f "%a=" (Ident.pp pe) id }; F.fprintf f @@ -2114,7 +2113,7 @@ let exp_sub (subst: subst) e => exp_sub_ids (apply_sub subst) e; let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr => { let sub_id id => switch (exp_sub_ids f (Var id)) { - | Var id' => id' + | Var id' when not (Ident.equal id id') => id' | _ => id }; switch instr { @@ -2139,12 +2138,17 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr => } else { Store lhs_exp' typ rhs_exp' loc } - | Call ret_ids fun_exp actuals call_flags loc => - let ret_ids' = + | Call ret_id fun_exp actuals call_flags loc => + let ret_id' = if sub_id_binders { - IList.map_changed sub_id ret_ids + switch ret_id { + | Some (id, typ) => + let id' = sub_id id; + Ident.equal id id' ? ret_id : Some (id', typ) + | None => None + } } else { - ret_ids + ret_id }; let fun_exp' = exp_sub_ids f fun_exp; let actuals' = @@ -2160,10 +2164,10 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr => } ) actuals; - if (ret_ids' === ret_ids && fun_exp' === fun_exp && actuals' === actuals) { + if (ret_id' === ret_id && fun_exp' === fun_exp && actuals' === actuals) { instr } else { - Call ret_ids' fun_exp' actuals' call_flags loc + Call ret_id' fun_exp' actuals' call_flags loc } | Prune exp loc true_branch if_kind => let exp' = exp_sub_ids f exp; @@ -2189,6 +2193,15 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr => /** apply [subst] to all id's in [instr], including binder id's */ let instr_sub (subst: subst) instr => instr_sub_ids sub_id_binders::true (apply_sub subst) instr; +let id_typ_compare (id1, typ1) (id2, typ2) => { + let n = Ident.compare id1 id2; + if (n != 0) { + n + } else { + Typ.compare typ1 typ2 + } +}; + let exp_typ_compare (exp1, typ1) (exp2, typ2) => { let n = Exp.compare exp1 exp2; if (n != 0) { @@ -2257,8 +2270,8 @@ let instr_compare instr1 instr2 => } | (Prune _, _) => (-1) | (_, Prune _) => 1 - | (Call ret_ids1 e1 arg_ts1 loc1 cf1, Call ret_ids2 e2 arg_ts2 loc2 cf2) => - let n = IList.compare Ident.compare ret_ids1 ret_ids2; + | (Call ret_id1 e1 arg_ts1 loc1 cf1, Call ret_id2 e2 arg_ts2 loc2 cf2) => + let n = opt_compare id_typ_compare ret_id1 ret_id2; if (n != 0) { n } else { @@ -2416,6 +2429,22 @@ let exp_typ_compare_structural (e1, t1) (e2, t2) exp_map => { the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers used in the procedure of [instr2] */ let instr_compare_structural instr1 instr2 exp_map => { + let id_typ_opt_compare_structural id_typ1 id_typ2 exp_map => { + let id_typ_compare_structural (id1, typ1) (id2, typ2) => { + let (n, exp_map) = exp_compare_structural (Var id1) (Var id2) exp_map; + if (n != 0) { + (n, exp_map) + } else { + (Typ.compare typ1 typ2, exp_map) + } + }; + switch (id_typ1, id_typ2) { + | (Some it1, Some it2) => id_typ_compare_structural it1 it2 + | (None, None) => (0, exp_map) + | (None, _) => ((-1), exp_map) + | (_, None) => (1, exp_map) + } + }; let id_list_compare_structural ids1 ids2 exp_map => { let n = Pervasives.compare (IList.length ids1) (IList.length ids2); if (n != 0) { @@ -2478,7 +2507,7 @@ let instr_compare_structural instr1 instr2 exp_map => { }, exp_map ) - | (Call ret_ids1 e1 arg_ts1 _ cf1, Call ret_ids2 e2 arg_ts2 _ cf2) => + | (Call ret_id1 e1 arg_ts1 _ cf1, Call ret_id2 e2 arg_ts2 _ cf2) => let args_compare_structural args1 args2 exp_map => { let n = Pervasives.compare (IList.length args1) (IList.length args2); if (n != 0) { @@ -2498,7 +2527,7 @@ let instr_compare_structural instr1 instr2 exp_map => { args2 } }; - let (n, exp_map) = id_list_compare_structural ret_ids1 ret_ids2 exp_map; + let (n, exp_map) = id_typ_opt_compare_structural ret_id1 ret_id2 exp_map; if (n != 0) { (n, exp_map) } else { diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index 7f7fe58a2..640020fd5 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -52,10 +52,9 @@ type instr = | Store of Exp.t Typ.t Exp.t Location.t /** prune the state based on [exp=1], the boolean indicates whether true branch */ | Prune of Exp.t Location.t bool if_kind - /** [Call (ret_id1..ret_idn, e_fun, arg_ts, loc, call_flags)] represents an instructions - [ret_id1..ret_idn = e_fun(arg_ts);] - where n = 0 for void return and n > 1 for struct return */ - | Call of (list Ident.t) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t + /** [Call (ret_id, e_fun, arg_ts, loc, call_flags)] represents an instruction + [ret_id = e_fun(arg_ts);]. The return value is ignored when [ret_id = None]. */ + | Call of (option (Ident.t, Typ.t)) Exp.t (list (Exp.t, Typ.t)) Location.t CallFlags.t /** nullify stack variable */ | Nullify of Pvar.t Location.t | Abstract of Location.t /** apply abstraction */ diff --git a/infer/src/backend/builtin.ml b/infer/src/backend/builtin.ml index 037cae452..67b57af69 100644 --- a/infer/src/backend/builtin.ml +++ b/infer/src/backend/builtin.ml @@ -17,7 +17,7 @@ type args = { tenv : Tenv.t; prop_ : Prop.normal Prop.t; path : Paths.Path.t; - ret_ids : Ident.t list; + ret_id : (Ident.t * Typ.t) option; args : (Exp.t * Typ.t) list; proc_name : Procname.t; loc : Location.t; diff --git a/infer/src/backend/builtin.mli b/infer/src/backend/builtin.mli index 4272bc9b3..1118754cc 100644 --- a/infer/src/backend/builtin.mli +++ b/infer/src/backend/builtin.mli @@ -17,7 +17,7 @@ type args = { tenv : Tenv.t; prop_ : Prop.normal Prop.t; path : Paths.Path.t; - ret_ids : Ident.t list; + ret_id : (Ident.t * Typ.t) option; args : (Exp.t * Typ.t) list; proc_name : Procname.t; loc : Location.t; diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 2c84a3f24..4e041c17a 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -138,7 +138,7 @@ let find_normal_variable_funcall (node: Cfg.Node.t) (id: Ident.t): (Exp.t * (Exp.t list) * Location.t * CallFlags.t) option = let find_declaration _ = function - | Sil.Call ([id0], fun_exp, args, loc, call_flags) when Ident.equal id id0 -> + | Sil.Call (Some (id0, _), fun_exp, args, loc, call_flags) when Ident.equal id id0 -> Some (fun_exp, IList.map fst args, loc, call_flags) | _ -> None in let res = find_in_node_or_preds node find_declaration in @@ -218,14 +218,14 @@ let rec _find_normal_variable_load tenv (seen : Exp.Set.t) node id : DExp.t opti (L.d_str "find_normal_variable_load defining "; Sil.d_exp e; L.d_ln ()); _exp_lv_dexp tenv seen node e - | Sil.Call ([id0], Exp.Const (Const.Cfun pn), (e, _):: _, _, _) + | Sil.Call (Some (id0, _), Exp.Const (Const.Cfun pn), (e, _):: _, _, _) when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") -> if verbose then (L.d_str "find_normal_variable_load cast on "; Sil.d_exp e; L.d_ln ()); _exp_rv_dexp tenv seen node e - | Sil.Call ([id0], (Exp.Const (Const.Cfun pname) as fun_exp), args, loc, call_flags) + | Sil.Call (Some (id0, _), (Exp.Const (Const.Cfun pname) as fun_exp), args, loc, call_flags) when Ident.equal id id0 -> if verbose then diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index c71a6f78d..081932721 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/infer/src/backend/modelBuiltins.ml @@ -20,9 +20,9 @@ let execute___no_op prop path: Builtin.ret_typ = [(prop, path)] (** model va_arg as always returning 0 *) -let execute___builtin_va_arg { Builtin.pdesc; tenv; prop_; path; ret_ids; args; loc; } +let execute___builtin_va_arg { Builtin.pdesc; tenv; prop_; path; ret_id; args; loc; } : Builtin.ret_typ = - match args, ret_ids with + match args, ret_id with | [_; _; (lexp3, typ3)], _ -> let instr' = Sil.Store (lexp3, typ3, Exp.zero, loc) in SymExec.instrs ~mask_errors:true tenv pdesc [instr'] [(prop_, path)] @@ -49,9 +49,9 @@ let extract_array_type typ = | _ -> None (** Return a result from a procedure call. *) -let return_result tenv e prop ret_ids = - match ret_ids with - | [ret_id] -> Prop.conjoin_eq tenv e (Exp.Var ret_id) prop +let return_result tenv e prop ret_id = + match ret_id with + | Some (ret_id, _) -> Prop.conjoin_eq tenv e (Exp.Var ret_id) prop | _ -> prop (* Add an array of typ pointed to by lexp to prop_ if it doesn't already exist *) @@ -85,28 +85,28 @@ let add_array_to_prop tenv pdesc prop_ lexp typ = end (* Add an array in prop if it is not allocated.*) -let execute___require_allocated_array { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } +let execute___require_allocated_array { Builtin.tenv; pdesc; prop_; path; args; } : Builtin.ret_typ = match args with - | [(lexp, typ)] when IList.length ret_ids <= 1 -> + | [(lexp, typ)] -> (match add_array_to_prop tenv pdesc prop_ lexp typ with | None -> [] | Some (_, prop) -> [(prop, path)]) | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let execute___get_array_length { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } +let execute___get_array_length { Builtin.tenv; pdesc; prop_; path; ret_id; args; } : Builtin.ret_typ = match args with - | [(lexp, typ)] when IList.length ret_ids <= 1 -> + | [(lexp, typ)] -> (match add_array_to_prop tenv pdesc prop_ lexp typ with | None -> [] - | Some (len, prop) -> [(return_result tenv len prop ret_ids, path)]) + | Some (len, prop) -> [(return_result tenv len prop ret_id, path)]) | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let execute___set_array_length { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } +let execute___set_array_length { Builtin.tenv; pdesc; prop_; path; ret_id; args; } : Builtin.ret_typ = - match args, ret_ids with - | [(lexp, typ); (len, _)], []-> + match args, ret_id with + | [(lexp, typ); (len, _)], None -> (match add_array_to_prop tenv pdesc prop_ lexp typ with | None -> [] | Some (_, prop_a) -> (* Invariant: prop_a has an array pointed to by lexp *) @@ -188,10 +188,10 @@ let create_type tenv n_lexp typ prop = non_null_case else null_case @ non_null_case -let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; } +let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_id; args; } : Builtin.ret_typ = match args with - | [(lexp, typ)] when IList.length ret_ids <= 1 -> + | [(lexp, typ)] -> let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let props = create_type tenv n_lexp typ prop in @@ -203,9 +203,9 @@ let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; } | _ -> false) prop.Prop.sigma in match hpred with | Sil.Hpointsto(_, _, texp) -> - (return_result tenv texp prop ret_ids), path + (return_result tenv texp prop ret_id), path | _ -> assert false - with Not_found -> (return_result tenv Exp.zero prop ret_ids), path + with Not_found -> (return_result tenv Exp.zero prop ret_id), path end in (IList.map aux props) | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -227,10 +227,10 @@ let replace_ptsto_texp tenv prop root_e texp = Prop.normalize tenv prop'' let execute___instanceof_cast ~instof - { Builtin.pdesc; tenv; prop_; path; ret_ids; args; } + { Builtin.pdesc; tenv; prop_; path; ret_id; args; } : Builtin.ret_typ = match args with - | [(val1_, typ1); (texp2_, _)] when IList.length ret_ids <= 1 -> + | [(val1_, typ1); (texp2_, _)] -> let pname = Cfg.Procdesc.get_proc_name pdesc in let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in @@ -247,7 +247,7 @@ let execute___instanceof_cast ~instof __POS__ None texp1 texp2 val1 in let exe_one_prop prop = if Exp.equal texp2 Exp.zero then - [(return_result tenv Exp.zero prop ret_ids, path)] + [(return_result tenv Exp.zero prop ret_id, path)] else begin try @@ -264,7 +264,7 @@ let execute___instanceof_cast ~instof let prop' = if Exp.equal texp1 texp1' then prop else replace_ptsto_texp tenv prop val1 texp1' in - [(return_result tenv res_e prop' ret_ids, path)] in + [(return_result tenv res_e prop' ret_id, path)] in if instof then (* instanceof *) begin let pos_res = mk_res pos_type_opt Exp.one in @@ -295,7 +295,7 @@ let execute___instanceof_cast ~instof end | _ -> [] with Not_found -> - [(return_result tenv val1 prop ret_ids, path)] + [(return_result tenv val1 prop ret_id, path)] end in let props = create_type tenv val1 typ1 prop in IList.flatten (IList.map exe_one_prop props) @@ -326,9 +326,9 @@ let set_resource_attribute tenv prop path n_lexp loc ra_res = [(prop', path)] (** Set the attibute of the value as file *) -let execute___set_file_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; args; loc; } +let execute___set_file_attribute { Builtin.tenv; pdesc; prop_; path; ret_id; args; loc; } : Builtin.ret_typ = - match args, ret_ids with + match args, ret_id with | [(lexp, _)], _ -> let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in @@ -336,9 +336,9 @@ let execute___set_file_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; ar | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as lock *) -let execute___set_lock_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; args; loc; } +let execute___set_lock_attribute { Builtin.tenv; pdesc; prop_; path; ret_id; args; loc; } : Builtin.ret_typ = - match args, ret_ids with + match args, ret_id with | [(lexp, _)], _ -> let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in @@ -347,9 +347,9 @@ let execute___set_lock_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; ar (** Set the resource attribute of the first real argument of method as ignore, the first argument is assumed to be "this" *) -let execute___method_set_ignore_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; args; loc; } +let execute___method_set_ignore_attribute { Builtin.tenv; pdesc; prop_; path; ret_id; args; loc; } : Builtin.ret_typ = - match args, ret_ids with + match args, ret_id with | [_ ; (lexp, _)], _ -> let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in @@ -357,9 +357,9 @@ let execute___method_set_ignore_attribute { Builtin.tenv; pdesc; prop_; path; re | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** Set the attibute of the value as memory *) -let execute___set_mem_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; args; loc; } +let execute___set_mem_attribute { Builtin.tenv; pdesc; prop_; path; ret_id; args; loc; } : Builtin.ret_typ = - match args, ret_ids with + match args, ret_id with | [(lexp, _)], _ -> let pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in @@ -368,9 +368,9 @@ let execute___set_mem_attribute { Builtin.tenv; pdesc; prop_; path; ret_ids; arg (** report an error if [lexp] is tainted; otherwise, add untained([lexp]) as a precondition *) let execute___check_untainted - { Builtin.tenv; pdesc; prop_; path; ret_ids; args; proc_name = callee_pname; } + { Builtin.tenv; pdesc; prop_; path; ret_id; args; proc_name = callee_pname; } : Builtin.ret_typ = - match args, ret_ids with + match args, ret_id with | [(lexp, _)], _ -> let caller_pname = Cfg.Procdesc.get_proc_name pdesc in let n_lexp, prop = check_arith_norm_exp tenv caller_pname lexp prop_ in @@ -378,7 +378,7 @@ let execute___check_untainted | _ -> raise (Exceptions.Wrong_argument_number __POS__) (** take a pointer to a struct, and return the value of a hidden field in the struct *) -let execute___get_hidden_field { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } +let execute___get_hidden_field { Builtin.tenv; pdesc; prop_; path; ret_id; args; } : Builtin.ret_typ = match args with | [(lexp, _)] -> @@ -386,7 +386,7 @@ let execute___get_hidden_field { Builtin.tenv; pdesc; prop_; path; ret_ids; args let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop_ in let ret_val = ref None in let return_val p = match !ret_val with - | Some e -> return_result tenv e p ret_ids + | Some e -> return_result tenv e p ret_id | None -> p in let foot_var = lazy (Exp.Var (Ident.create_fresh Ident.kfootprint)) in let filter_fld_hidden (f, _ ) = Ident.fieldname_is_hidden f in @@ -483,12 +483,12 @@ let get_suppress_npe_flag args = false, args' (* this is a CFRelease/CFRetain *) | _ -> true, args -let execute___objc_retain_impl ({ Builtin.tenv; prop_; args; ret_ids; } as builtin_args) +let execute___objc_retain_impl ({ Builtin.tenv; prop_; args; ret_id; } as builtin_args) : Builtin.ret_typ = let mask_errors, args' = get_suppress_npe_flag args in match args' with | [(lexp, _)] -> - let prop = return_result tenv lexp prop_ ret_ids in + let prop = return_result tenv lexp prop_ ret_id in execute___objc_counter_update ~mask_errors (Binop.PlusA) (IntLit.one) { builtin_args with Builtin.prop_ = prop; args = args'; } @@ -525,12 +525,12 @@ let execute___objc_release_cf builtin_args (** Set the attibute of the value as objc autoreleased *) let execute___set_autorelease_attribute - { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } + { Builtin.tenv; pdesc; prop_; path; ret_id; args; } : Builtin.ret_typ = - match args, ret_ids with + match args, ret_id with | [(lexp, _)], _ -> let pname = Cfg.Procdesc.get_proc_name pdesc in - let prop = return_result tenv lexp prop_ ret_ids in + let prop = return_result tenv lexp prop_ ret_id in if Config.objc_memory_model_on then let n_lexp, prop = check_arith_norm_exp tenv pname lexp prop in let prop' = Attribute.add_or_replace tenv prop (Apred (Aautorelease, [n_lexp])) in @@ -640,10 +640,10 @@ let execute___set_untaint_attribute | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let execute___objc_cast { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } +let execute___objc_cast { Builtin.tenv; pdesc; prop_; path; ret_id; args; } : Builtin.ret_typ = match args with - | [(val1_, _); (texp2_, _)] when IList.length ret_ids <= 1 -> + | [(val1_, _); (texp2_, _)] -> let pname = Cfg.Procdesc.get_proc_name pdesc in let val1, prop__ = check_arith_norm_exp tenv pname val1_ prop_ in let texp2, prop = check_arith_norm_exp tenv pname texp2_ prop__ in @@ -654,9 +654,9 @@ let execute___objc_cast { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } match hpred, texp2 with | Sil.Hpointsto (val1, _, _), Exp.Sizeof _ -> let prop' = replace_ptsto_texp tenv prop val1 texp2 in - [(return_result tenv val1 prop' ret_ids, path)] - | _ -> [(return_result tenv val1 prop ret_ids, path)] - with Not_found -> [(return_result tenv val1 prop ret_ids, path)]) + [(return_result tenv val1 prop' ret_id, path)] + | _ -> [(return_result tenv val1 prop ret_id, path)] + with Not_found -> [(return_result tenv val1 prop ret_id, path)]) | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute_abort { Builtin.proc_name; } @@ -731,7 +731,7 @@ let execute_free mk { Builtin.pdesc; instr; tenv; prop_; path; args; loc; } | _ -> raise (Exceptions.Wrong_argument_number __POS__) let execute_alloc mk can_return_null - { Builtin.pdesc; tenv; prop_; path; ret_ids; args; loc; } + { Builtin.pdesc; tenv; prop_; path; ret_id; args; loc; } : Builtin.ret_typ = let pname = Cfg.Procdesc.get_proc_name pdesc in let rec evaluate_char_sizeof e = match e with @@ -760,8 +760,8 @@ let execute_alloc mk can_return_null size_exp, pname | _ -> raise (Exceptions.Wrong_argument_number __POS__) in - let ret_id = match ret_ids with - | [ret_id] -> ret_id + let ret_id = match ret_id with + | Some (ret_id, _) -> ret_id | _ -> Ident.create_fresh Ident.kprimed in let size_exp', prop = let n_size_exp, prop = check_arith_norm_exp tenv pname size_exp prop_ in @@ -854,7 +854,7 @@ let execute_scan_function skip_n_arguments ({ Builtin.args } as call_args) { call_args with args = !varargs } | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let execute__unwrap_exception { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } +let execute__unwrap_exception { Builtin.tenv; pdesc; prop_; path; ret_id; args; } : Builtin.ret_typ = match args with | [(ret_exn, _)] -> @@ -863,23 +863,23 @@ let execute__unwrap_exception { Builtin.tenv; pdesc; prop_; path; ret_ids; args; let n_ret_exn, prop = check_arith_norm_exp tenv pname ret_exn prop_ in match n_ret_exn with | Exp.Exn exp -> - let prop_with_exn = return_result tenv exp prop ret_ids in + let prop_with_exn = return_result tenv exp prop ret_id in [(prop_with_exn, path)] | _ -> assert false end | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let execute_return_first_argument { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } +let execute_return_first_argument { Builtin.tenv; pdesc; prop_; path; ret_id; args; } : Builtin.ret_typ = match args with | (arg1_, _):: _ -> let pname = Cfg.Procdesc.get_proc_name pdesc in let arg1, prop = check_arith_norm_exp tenv pname arg1_ prop_ in - let prop' = return_result tenv arg1 prop ret_ids in + let prop' = return_result tenv arg1 prop ret_id in [(prop', path)] | _ -> raise (Exceptions.Wrong_argument_number __POS__) -let execute___split_get_nth { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } +let execute___split_get_nth { Builtin.tenv; pdesc; prop_; path; ret_id; args; } : Builtin.ret_typ = match args with | [(lexp1, _); (lexp2, _); (lexp3, _)] -> @@ -894,7 +894,7 @@ let execute___split_get_nth { Builtin.tenv; pdesc; prop_; path; ret_ids; args; } let parts = Str.split (Str.regexp_string str2) str1 in let n_part = IList.nth parts n in let res = Exp.Const (Const.Cstr n_part) in - [(return_result tenv res prop ret_ids, path)] + [(return_result tenv res prop ret_id, path)] with Not_found -> assert false) | _ -> [(prop, path)]) | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -1140,7 +1140,7 @@ let _ = Builtin.register let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt - { Builtin.pdesc; tenv; ret_ids; loc; } = + { Builtin.pdesc; tenv; ret_id; loc; } = let alloc_fun = Exp.Const (Const.Cfun __objc_alloc_no_fail) in let ptr_typ = Typ.Tptr (typ, Typ.Pk_pointer) in let sizeof_typ = Exp.Sizeof (typ, None, Subtype.exact) in @@ -1150,7 +1150,7 @@ let execute_objc_alloc_no_fail | None -> [] in let alloc_instr = Sil.Call - (ret_ids, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) in + (ret_id, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) in SymExec.instrs tenv pdesc [alloc_instr] symb_state let mk_objc_class_method class_name method_name = diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index d755a3cf5..ba61e2c05 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -24,7 +24,7 @@ let add_dispatch_calls pdesc cg tenv = let has_dispatch_call instrs = IList.exists instr_is_dispatch_call instrs in let replace_dispatch_calls = function - | Sil.Call (ret_ids, (Exp.Const (Const.Cfun callee_pname) as call_exp), + | Sil.Call (ret_id, (Exp.Const (Const.Cfun callee_pname) as call_exp), (((_, receiver_typ) :: _) as args), loc, call_flags) as instr when call_flags_is_dispatch call_flags -> (* the frontend should not populate the list of targets *) @@ -50,7 +50,7 @@ let add_dispatch_calls pdesc cg tenv = (fun target_pname -> Cg.add_edge cg caller_pname target_pname) targets_to_add; let call_flags' = { call_flags with CallFlags.cf_targets = targets_to_add; } in - Sil.Call (ret_ids, call_exp, args, loc, call_flags') + Sil.Call (ret_id, call_exp, args, loc, call_flags') | [] -> instr) | instr -> instr in @@ -136,12 +136,12 @@ module NullifyTransferFunctions = struct let astate' = match instr with | Sil.Load (lhs_id, _, _, _) -> VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify - | Sil.Call (lhs_ids, _, _, _, _) -> + | Sil.Call (lhs_id, _, _, _, _) -> let active_defs' = - IList.fold_left - (fun acc id -> VarDomain.add (Var.of_id id) acc) + Option.map_default + (fun (id, _) -> VarDomain.add (Var.of_id id) active_defs) active_defs - lhs_ids in + lhs_id in active_defs', to_nullify | Sil.Store (Exp.Lvar lhs_pvar, _, _, _) -> VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index c3fbe83b1..8b6cf5f6b 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -710,7 +710,7 @@ let call_constructor_url_update_args pname actual_params = (* 2. We don't know, but obj could be null, we return both options, *) (* (obj = null, res = null), (obj != null, res = [obj foo]) *) (* We want the same behavior even when we are going to skip the function. *) -let handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname pre ret_ids res = +let handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname pre ret_id res = let path_description = "Message " ^ (Procname.to_simplified_string callee_pname) ^ @@ -728,8 +728,8 @@ let handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname Option.is_some (Attribute.get_objc_null tenv pre e) -> true | _ -> false in let add_objc_null_attribute_or_nullify_result prop = - match ret_ids with - | [ret_id] -> ( + match ret_id with + | Some (ret_id, _) -> ( match Attribute.find_equal_formal_path tenv receiver prop with | Some vfs -> Attribute.add_or_replace tenv prop (Apred (Aobjc_null, [Exp.Var ret_id; vfs])) @@ -766,10 +766,10 @@ let handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname (* This method handles ObjC instance method calls, in particular the fact that calling a method *) (* with nil returns nil. The exec_call function is either standard call execution or execution *) (* of ObjC getters and setters using a builtin. *) -let handle_objc_instance_method_call actual_pars actual_params pre tenv ret_ids pdesc callee_pname +let handle_objc_instance_method_call actual_pars actual_params pre tenv ret_id pdesc callee_pname loc path exec_call = - let res () = exec_call tenv ret_ids pdesc callee_pname loc actual_params pre path in - handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname pre ret_ids res + let res () = exec_call tenv ret_id pdesc callee_pname loc actual_params pre path in + handle_objc_instance_method_call_or_skip tenv actual_pars path callee_pname pre ret_id res let normalize_params tenv pdesc prop actual_params = let norm_arg (p, args) (e, t) = @@ -1006,7 +1006,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path Sil.Call (ret, exp', par, loc, call_flags) in instr' | _ -> _instr in - let skip_call ?(is_objc_instance_method=false) prop path callee_pname ret_annots loc ret_ids + let skip_call ?(is_objc_instance_method=false) prop path callee_pname ret_annots loc ret_id ret_typ_opt actual_args = let skip_res () = let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in @@ -1021,13 +1021,14 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path summary.Specs.stats.Specs.call_stats callee_pname loc (Specs.CallStats.CR_skip) !Config.footprint); unknown_or_scan_call ~is_scan:false ret_typ_opt ret_annots Builtin.{ - pdesc= current_pdesc; instr; tenv; prop_= prop; path; ret_ids; args= actual_args; + pdesc= current_pdesc; instr; tenv; prop_= prop; path; ret_id; args= actual_args; proc_name= callee_pname; loc; } in if is_objc_instance_method then - handle_objc_instance_method_call_or_skip tenv actual_args path callee_pname prop ret_ids skip_res + handle_objc_instance_method_call_or_skip + tenv actual_args path callee_pname prop ret_id skip_res else skip_res () in - let call_args prop_ proc_name args ret_ids loc = { - Builtin.pdesc = current_pdesc; instr; tenv; prop_; path; ret_ids; args; proc_name; loc; } in + let call_args prop_ proc_name args ret_id loc = { + Builtin.pdesc = current_pdesc; instr; tenv; prop_; path; ret_id; args; proc_name; loc; } in match instr with | Sil.Load (id, rhs_exp, typ, loc) -> execute_load current_pname current_pdesc tenv id rhs_exp typ loc prop_ @@ -1062,17 +1063,17 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path check_condition_always_true_false (); let n_cond, prop = check_arith_norm_exp tenv current_pname cond prop__ in ret_old_path (Propset.to_proplist (prune tenv ~positive:true n_cond prop)) - | Sil.Call (ret_ids, Exp.Const (Const.Cfun callee_pname), args, loc, _) + | Sil.Call (ret_id, Exp.Const (Const.Cfun callee_pname), args, loc, _) when Builtin.is_registered callee_pname -> let sym_exe_builtin = Builtin.get callee_pname in - sym_exe_builtin (call_args prop_ callee_pname args ret_ids loc) - | Sil.Call (ret_ids, + sym_exe_builtin (call_args prop_ callee_pname args ret_id loc) + | Sil.Call (ret_id, Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)), actual_params, loc, call_flags) when Config.lazy_dynamic_dispatch -> let norm_prop, norm_args = normalize_params tenv current_pname prop_ actual_params in let exec_skip_call skipped_pname ret_annots ret_type = - skip_call norm_prop path skipped_pname ret_annots loc ret_ids (Some ret_type) norm_args in + skip_call norm_prop path skipped_pname ret_annots loc ret_id (Some ret_type) norm_args in let resolved_pname, summary_opt = resolve_and_analyze tenv current_pdesc norm_prop norm_args callee_pname call_flags in begin @@ -1086,10 +1087,10 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in exec_skip_call resolved_pname ret_annots proc_attrs.ProcAttributes.ret_type | Some summary -> - proc_call summary (call_args prop_ callee_pname norm_args ret_ids loc) + proc_call summary (call_args prop_ callee_pname norm_args ret_id loc) end - | Sil.Call (ret_ids, + | Sil.Call (ret_id, Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)), actual_params, loc, call_flags) -> do_error_checks tenv (Paths.Path.curr_node path) instr current_pname current_pdesc; @@ -1101,7 +1102,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let exec_one_pname pname = Ondemand.analyze_proc_name tenv ~propagate_exceptions:true current_pdesc pname; let exec_skip_call ret_annots ret_type = - skip_call norm_prop path pname ret_annots loc ret_ids (Some ret_type) url_handled_args in + skip_call norm_prop path pname ret_annots loc ret_id (Some ret_type) url_handled_args in match Specs.get_summary pname with | None -> let ret_typ = Typ.java_proc_return_typ callee_pname_java in @@ -1112,10 +1113,10 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let ret_annots, _ = proc_attrs.ProcAttributes.method_annotation in exec_skip_call ret_annots proc_attrs.ProcAttributes.ret_type | Some summary -> - proc_call summary (call_args norm_prop pname url_handled_args ret_ids loc) in + proc_call summary (call_args norm_prop pname url_handled_args ret_id loc) in IList.fold_left (fun acc pname -> exec_one_pname pname @ acc) [] resolved_pnames - | Sil.Call (ret_ids, Exp.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) -> + | Sil.Call (ret_id, Exp.Const (Const.Cfun callee_pname), actual_params, loc, call_flags) -> (* Generic fun call with known name *) let (prop_r, n_actual_params) = normalize_params tenv current_pname prop_ actual_params in let resolved_pname = @@ -1131,7 +1132,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path let sentinel_result = if !Config.curr_language = Config.Clang then check_variadic_sentinel_if_present - (call_args prop_r callee_pname actual_params ret_ids loc) + (call_args prop_r callee_pname actual_params ret_id loc) else [(prop_r, path)] in let do_call (prop, path) = let summary = Specs.get_summary resolved_pname in @@ -1157,7 +1158,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path match objc_property_accessor_ret_typ_opt with | Some (objc_property_accessor, ret_typ) -> handle_objc_instance_method_call - n_actual_params n_actual_params prop tenv ret_ids + n_actual_params n_actual_params prop tenv ret_id current_pdesc callee_pname loc path (sym_exec_objc_accessor objc_property_accessor ret_typ) | None -> @@ -1171,13 +1172,13 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path match attrs_opt with | Some attrs -> attrs.ProcAttributes.is_objc_instance_method | None -> false in - skip_call ~is_objc_instance_method prop path resolved_pname ret_annots loc ret_ids + skip_call ~is_objc_instance_method prop path resolved_pname ret_annots loc ret_id ret_typ_opt n_actual_params else proc_call (Option.get summary) - (call_args prop resolved_pname n_actual_params ret_ids loc) in + (call_args prop resolved_pname n_actual_params ret_id loc) in IList.flatten (IList.map do_call sentinel_result) - | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (* Call via function pointer *) + | Sil.Call (ret_id, fun_exp, actual_params, loc, call_flags) -> (* Call via function pointer *) let (prop_r, n_actual_params) = normalize_params tenv current_pname prop_ actual_params in if call_flags.CallFlags.cf_is_objc_block then Rearrange.check_call_to_objc_block_error tenv current_pdesc prop_r fun_exp loc; @@ -1191,7 +1192,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path L.d_strln ", returning undefined value."; let callee_pname = Procname.from_string_c_fun "__function_pointer__" in unknown_or_scan_call ~is_scan:false None Annot.Item.empty Builtin.{ - pdesc= current_pdesc; instr; tenv; prop_= prop_r; path; ret_ids; args= n_actual_params; + pdesc= current_pdesc; instr; tenv; prop_= prop_r; path; ret_id; args= n_actual_params; proc_name= callee_pname; loc; } end | Sil.Nullify (pvar, _) -> @@ -1381,7 +1382,7 @@ and check_untainted tenv exp taint_kind caller_pname callee_pname prop = (** execute a call for an unknown or scan function *) and unknown_or_scan_call ~is_scan ret_type_option ret_annots - { Builtin.tenv; pdesc; prop_= pre; path; ret_ids; + { Builtin.tenv; pdesc; prop_= pre; path; ret_id; args; proc_name= callee_pname; loc; instr; } = let remove_file_attribute prop = let do_exp p (e, _) = @@ -1428,8 +1429,9 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots if Procname.is_java callee_pname then remove_file_attribute pre else pre in - let pre_2 = match ret_ids, ret_type_option with - | [ret_id], Some ret_typ -> + let pre_2 = match ret_id, ret_type_option with + | Some (ret_id, _), Some ret_typ -> + (* TODO(jjb): Should this use the type of ret_id, or ret_type from the procedure type? *) add_constraints_on_retval tenv pdesc pre_1 (Exp.Var ret_id) ret_typ ~has_nullable_annot callee_pname loc | _ -> @@ -1442,7 +1444,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots else (* otherwise, add undefined attribute to retvals and actuals passed by ref *) let exps_to_mark = - let ret_exps = IList.map (fun ret_id -> Exp.Var ret_id) ret_ids in + let ret_exps = Option.map_default (fun (id, _) -> [Exp.Var id]) [] ret_id in IList.fold_left (fun exps_to_mark (exp, _, _) -> exp :: exps_to_mark) ret_exps actuals_by_ref in let prop_with_undef_attr = @@ -1501,13 +1503,13 @@ and check_variadic_sentinel_if_present let formals = callee_attributes.ProcAttributes.formals in check_variadic_sentinel (IList.length formals) sentinel_arg builtin_args -and sym_exec_objc_getter field_name ret_typ tenv ret_ids pdesc pname loc args prop = +and sym_exec_objc_getter field_name ret_typ tenv ret_id pdesc pname loc args prop = L.d_strln ("No custom getter found. Executing the ObjC builtin getter with ivar "^ (Ident.fieldname_to_string field_name)^"."); let ret_id = - match ret_ids with - | [ret_id] -> ret_id - | _ -> assert false in + match ret_id with + | Some (ret_id, _) -> ret_id + | None -> assert false in match args with | [(lexp, (Typ.Tstruct _ as typ | Tptr (Tstruct _ as typ, _)))] -> let field_access_exp = Exp.Lfield (lexp, field_name, typ) in @@ -1524,7 +1526,7 @@ and sym_exec_objc_setter field_name _ tenv _ pdesc pname loc args prop = execute_store ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop | _ -> raise (Exceptions.Wrong_argument_number __POS__) -and sym_exec_objc_accessor property_accesor ret_typ tenv ret_ids pdesc _ loc args prop path +and sym_exec_objc_accessor property_accesor ret_typ tenv ret_id pdesc _ loc args prop path : Builtin.ret_typ = let f_accessor = match property_accesor with @@ -1533,25 +1535,24 @@ and sym_exec_objc_accessor property_accesor ret_typ tenv ret_ids pdesc _ loc arg (* we want to execute in the context of the current procedure, not in the context of callee_pname, since this is the procname of the setter/getter method *) let cur_pname = Cfg.Procdesc.get_proc_name pdesc in - f_accessor ret_typ tenv ret_ids pdesc cur_pname loc args prop + f_accessor ret_typ tenv ret_id pdesc cur_pname loc args prop |> IList.map (fun p -> (p, path)) (** Perform symbolic execution for a function call *) -and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_ids; args= actual_pars; loc; } = +and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actual_pars; loc; } = let caller_pname = Cfg.Procdesc.get_proc_name pdesc in let callee_pname = Specs.get_proc_name summary in let ret_typ = Specs.get_ret_type summary in let check_return_value_ignored () = (* check if the return value of the call is ignored, and issue a warning *) - let is_ignored = match ret_typ, ret_ids with + let is_ignored = match ret_typ, ret_id with | Typ.Tvoid, _ -> false | Typ.Tint _, _ when not (proc_is_defined callee_pname) -> (* if the proc returns Tint and is not defined, *) (* don't report ignored return value *) false - | _, [] -> true - | _, [id] -> Errdesc.id_is_assigned_then_dead (State.get_node ()) id - | _ -> false in + | _, None -> true + | _, Some (id, _) -> Errdesc.id_is_assigned_then_dead (State.get_node ()) id in if is_ignored && Specs.get_flag callee_pname proc_flag_ignore_return = None then let err_desc = Localise.desc_return_value_ignored callee_pname loc in @@ -1593,11 +1594,11 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_ids; args= act let callee_attrs = Specs.get_attributes summary in if (!Config.curr_language <> Config.Java) && (Specs.get_attributes summary).ProcAttributes.is_objc_instance_method then - handle_objc_instance_method_call actual_pars actual_params pre tenv ret_ids pdesc + handle_objc_instance_method_call actual_pars actual_params pre tenv ret_id pdesc callee_pname loc path (Tabulation.exe_function_call callee_attrs) else (* non-objective-c method call. Standard tabulation *) Tabulation.exe_function_call - callee_attrs tenv ret_ids pdesc callee_pname loc actual_params pre path + callee_attrs tenv ret_id pdesc callee_pname loc actual_params pre path end (** perform symbolic execution for a single prop, and check for junk *) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 49fd547a0..b16490163 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -671,7 +671,7 @@ let include_subtrace callee_pname = (** combine the spec's post with a splitting and actual precondition *) let combine tenv - ret_ids (posts: ('a Prop.t * Paths.Path.t) list) + ret_id (posts: ('a Prop.t * Paths.Path.t) list) actual_pre path_pre split caller_pdesc callee_pname loc = let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in @@ -751,25 +751,27 @@ let combine tenv match Prop.prop_iter_find iter filter with | None -> post_p2 | Some iter' -> - match fst (Prop.prop_iter_current tenv iter') with - | Sil.Hpointsto (_, Sil.Eexp (e', inst), _) when exp_is_exn e' -> + match fst (Prop.prop_iter_current tenv iter'), ret_id with + | Sil.Hpointsto (_, Sil.Eexp (e', inst), _), _ when exp_is_exn e' -> (* resuls is an exception: set in caller *) let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in prop_set_exn tenv caller_pname p (Sil.Eexp (e', inst)) - | Sil.Hpointsto (_, Sil.Eexp (e', _), _) when IList.length ret_ids = 1 -> + | Sil.Hpointsto (_, Sil.Eexp (e', _), _), Some (id, _) -> let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in - Prop.conjoin_eq tenv e' (Exp.Var (IList.hd ret_ids)) p - | Sil.Hpointsto (_, Sil.Estruct (ftl, _), _) - when IList.length ftl = IList.length ret_ids -> + Prop.conjoin_eq tenv e' (Exp.Var id) p + | Sil.Hpointsto (_, Sil.Estruct (ftl, _), _), _ + when IList.length ftl = (if ret_id = None then 0 else 1) -> + (* TODO(jjb): Is this case dead? *) let rec do_ftl_ids p = function - | [], [] -> p - | (_, Sil.Eexp (e', _)):: ftl', ret_id:: ret_ids' -> + | [], None -> p + | (_, Sil.Eexp (e', _)) :: ftl', Some (ret_id, _) -> let p' = Prop.conjoin_eq tenv e' (Exp.Var ret_id) p in - do_ftl_ids p' (ftl', ret_ids') + do_ftl_ids p' (ftl', None) | _ -> p in let p = Prop.prop_iter_remove_curr_then_to_prop tenv iter' in - do_ftl_ids p (ftl, ret_ids) - | Sil.Hpointsto _ -> (* returning nothing or unexpected sexp, turning into nondet *) + do_ftl_ids p (ftl, ret_id) + | Sil.Hpointsto _, _ -> + (* returning nothing or unexpected sexp, turning into nondet *) Prop.prop_iter_remove_curr_then_to_prop tenv iter' | _ -> assert false in let post_p4 = @@ -875,9 +877,9 @@ let mk_actual_precondition tenv prop actual_params formal_params = let actual_pre = Prop.prop_sigma_star prop instantiated_formals in Prop.normalize tenv actual_pre -let mk_posts tenv ret_ids prop callee_pname callee_attrs posts = - match ret_ids with - | [ret_id] -> +let mk_posts tenv ret_id prop callee_pname callee_attrs posts = + match ret_id with + | Some (ret_id, _) -> let mk_getter_idempotent posts = (* if we have seen a previous call to the same function, only use specs whose return value is consistent with constraints on the return value of the previous call w.r.t to @@ -1005,10 +1007,10 @@ let check_uninitialize_dangling_deref tenv callee_pname actual_pre sub formal_pa (** Perform symbolic execution for a single spec *) let exe_spec - tenv ret_ids (n, nspecs) caller_pdesc callee_pname callee_attrs loc prop path_pre + tenv ret_id (n, nspecs) caller_pdesc callee_pname callee_attrs loc prop path_pre (spec : Prop.exposed Specs.spec) actual_params formal_params : abduction_res = let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in - let posts = mk_posts tenv ret_ids prop callee_pname callee_attrs spec.Specs.posts in + let posts = mk_posts tenv ret_id prop callee_pname callee_attrs spec.Specs.posts in let actual_pre = mk_actual_precondition tenv prop actual_params formal_params in let spec_pre = mk_pre tenv (Specs.Jprop.to_prop spec.Specs.pre) formal_params callee_pname callee_attrs in @@ -1036,7 +1038,7 @@ let exe_spec frame_fld missing_fld frame_typ missing_typ in let report_valid_res split = match combine tenv - ret_ids posts + ret_id posts actual_pre path_pre split caller_pdesc callee_pname loc with | None -> Invalid_res Cannot_combine @@ -1123,7 +1125,7 @@ let prop_pure_to_footprint tenv (p: 'a Prop.t) : Prop.normal Prop.t = Prop.normalize tenv (Prop.set p ~pi_fp:(p.Prop.pi_fp @ new_footprint_atoms)) (** post-process the raw result of a function call *) -let exe_call_postprocess tenv ret_ids trace_call callee_pname callee_attrs loc results = +let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc results = let filter_valid_res = function | Invalid_res _ -> false | Valid_res _ -> true in @@ -1258,8 +1260,8 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname callee_attrs loc r !Config.curr_language = Config.Java && is_likely_getter callee_pname) || returns_nullable ret_annot in - match ret_ids with - | [ret_id] when should_add_ret_attr ()-> + match ret_id with + | Some (ret_id, _) when should_add_ret_attr () -> (* add attribute to remember what function call a return id came from *) let ret_var = Exp.Var ret_id in let mark_id_as_retval (p, path) = @@ -1270,7 +1272,7 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname callee_attrs loc r (** Execute the function call and return the list of results with return value *) let exe_function_call - callee_attrs tenv ret_ids caller_pdesc callee_pname loc actual_params prop path = + callee_attrs tenv ret_id caller_pdesc callee_pname loc actual_params prop path = let caller_pname = Cfg.Procdesc.get_proc_name caller_pdesc in let trace_call res = match Specs.get_summary caller_pname with @@ -1290,7 +1292,7 @@ let exe_function_call let exe_one_spec (n, spec) = exe_spec tenv - ret_ids + ret_id (n, nspecs) caller_pdesc callee_pname @@ -1302,7 +1304,7 @@ let exe_function_call actual_params formal_params in let results = IList.map exe_one_spec spec_list in - exe_call_postprocess tenv ret_ids trace_call callee_pname callee_attrs loc results + exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc results (* let check_splitting_precondition sub1 sub2 = diff --git a/infer/src/backend/tabulation.mli b/infer/src/backend/tabulation.mli index 81caa194f..3dd075ba6 100644 --- a/infer/src/backend/tabulation.mli +++ b/infer/src/backend/tabulation.mli @@ -44,6 +44,6 @@ val d_splitting : splitting -> unit (** Execute the function call and return the list of results with return value *) val exe_function_call: - ProcAttributes.t -> Tenv.t -> Ident.t list -> Cfg.Procdesc.t -> Procname.t -> Location.t -> - (Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t -> + ProcAttributes.t -> Tenv.t -> (Ident.t * Typ.t) option -> Cfg.Procdesc.t -> Procname.t -> + Location.t -> (Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index a604f817b..c72c0ef2b 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/infer/src/checkers/annotationReachability.ml @@ -326,7 +326,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Annot.Map.fold add_call_for_annot map astate let exec_instr astate { ProcData.pdesc; tenv; } _ = function - | Sil.Call ([id], Const (Cfun callee_pname), _, _, _) + | Sil.Call (Some (id, _), Const (Cfun callee_pname), _, _, _) when is_unlikely callee_pname -> Domain.add_tracking_var (Var.of_id id) astate | Sil.Call (_, Const (Cfun callee_pname), _, call_loc, _) -> @@ -353,8 +353,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Sil.Prune (exp, _, _, _) when prunes_tracking_var astate exp -> Domain.stop_tracking astate - | Sil.Call (_::_, _, _, _, _) -> - failwith "Expecting a singleton for the return value" + | Sil.Call (None, _, _, _, _) -> + failwith "Expecting a return identifier" | _ -> astate end diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index c0fbec9d9..e678fa564 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -455,7 +455,7 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p | Exp.Const (Const.Cclass n) -> Ident.name_to_string n | Exp.Lvar _ -> ( let is_call_instr set call = match set, call with - | Sil.Store (_, _, Exp.Var (i1), _), Sil.Call (i2::[], _, _, _, _) + | Sil.Store (_, _, Exp.Var (i1), _), Sil.Call (Some (i2, _), _, _, _, _) when Ident.equal i1 i2 -> true | _ -> false in let is_set_instr = function diff --git a/infer/src/checkers/constantPropagation.ml b/infer/src/checkers/constantPropagation.ml index 330104526..5be05afb2 100644 --- a/infer/src/checkers/constantPropagation.ml +++ b/infer/src/checkers/constantPropagation.ml @@ -84,13 +84,13 @@ module ConstantFlow = Dataflow.MakeDF(struct && has_method pn "" -> (* StringBuilder. *) update (Exp.Var sb) (Some (Const.Cstr "")) constants - | Sil.Call (i:: [], Exp.Const (Const.Cfun pn), (Exp.Var i1, _):: [], _, _) + | Sil.Call (Some (i, _), Exp.Const (Const.Cfun pn), (Exp.Var i1, _):: [], _, _) when has_class pn "java.lang.StringBuilder" && has_method pn "toString" -> (* StringBuilder.toString *) update (Exp.Var i) (ConstantMap.find (Exp.Var i1) constants) constants | Sil.Call - (i:: [], Exp.Const (Const.Cfun pn), (Exp.Var i1, _):: (Exp.Var i2, _):: [], _, _) + (Some (i, _), Exp.Const (Const.Cfun pn), (Exp.Var i1, _):: (Exp.Var i2, _):: [], _, _) when has_class pn "java.lang.StringBuilder" && has_method pn "append" -> (* StringBuilder.append *) (match diff --git a/infer/src/checkers/copyPropagation.ml b/infer/src/checkers/copyPropagation.ml index a5472c870..5e7bf83ae 100644 --- a/infer/src/checkers/copyPropagation.ml +++ b/infer/src/checkers/copyPropagation.ml @@ -97,13 +97,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Sil.Store (Var _, _, _, _) -> (* *lhs = rhs. not a copy, and not a write to lhs *) astate - | Sil.Call (ret_ids, _, actuals, _, _) -> - let kill_ret_ids astate_acc id = - Domain.kill_copies_with_var (Var.of_id id) astate_acc in + | Sil.Call (ret_id, _, actuals, _, _) -> + let kill_ret_id (id,_) = + Domain.kill_copies_with_var (Var.of_id id) astate in let kill_actuals_by_ref astate_acc = function | (Exp.Lvar pvar, Typ.Tptr _) -> Domain.kill_copies_with_var (Var.of_pvar pvar) astate_acc | _ -> astate_acc in - let astate' = IList.fold_left kill_ret_ids astate ret_ids in + let astate' = Option.map_default kill_ret_id astate ret_id in if !Config.curr_language = Config.Java then astate' (* Java doesn't have pass-by-reference *) else IList.fold_left kill_actuals_by_ref astate' actuals diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index ac9c6b732..91b7dbd83 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -45,11 +45,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct |> exp_add_live rhs_exp | Sil.Prune (exp, _, _, _) -> exp_add_live exp astate - | Sil.Call (ret_ids, call_exp, params, _, _) -> - IList.fold_right - (fun ret_id astate_acc -> Domain.remove (Var.of_id ret_id) astate_acc) - ret_ids - astate + | Sil.Call (ret_id, call_exp, params, _, _) -> + Option.map_default (fun (ret_id, _) -> Domain.remove (Var.of_id ret_id) astate) + astate ret_id |> exp_add_live call_exp |> IList.fold_right exp_add_live (IList.map fst params) | Sil.Declare_locals _ | Remove_temps _ | Abstract _ | Nullify _ -> diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index fde20b564..7a3ad7861 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -145,7 +145,7 @@ let get_vararg_type_names tenv (* Is this the node creating ivar? *) let rec initializes_array instrs = match instrs with - | Sil.Call ([t1], Exp.Const (Const.Cfun pn), _, _, _):: + | Sil.Call (Some (t1, _), Exp.Const (Const.Cfun pn), _, _, _):: Sil.Store (Exp.Lvar iv, _, Exp.Var t2, _):: is -> (Pvar.equal ivar iv && Ident.equal t1 t2 && Procname.equal pn (Procname.from_string_c_fun "__new_array")) diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml index d328c4d60..243f15c2e 100644 --- a/infer/src/checkers/repeatedCallsChecker.ml +++ b/infer/src/checkers/repeatedCallsChecker.ml @@ -118,10 +118,10 @@ struct IList.for_all filter_arg args in match instr with - | Sil.Call (ret_ids, Exp.Const (Const.Cfun callee_pname), _, loc, call_flags) - when ret_ids <> [] && arguments_not_temp normalized_etl -> + | Sil.Call (Some _ as ret_id, Exp.Const (Const.Cfun callee_pname), _, loc, call_flags) + when arguments_not_temp normalized_etl -> let instr_normalized_args = Sil.Call ( - ret_ids, + ret_id, Exp.Const (Const.Cfun callee_pname), normalized_etl, loc, diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index ab6bbc040..1f89715f4 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -27,7 +27,7 @@ let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl = let autorelease_pname = ModelBuiltins.__set_autorelease_attribute in let mk_call procname e t = let bi_retain = Exp.Const (Const.Cfun procname) in - Sil.Call([], bi_retain, [(e, t)], loc, CallFlags.default) in + Sil.Call (None, bi_retain, [(e, t)], loc, CallFlags.default) in match typ with | Typ.Tptr (_, Typ.Pk_pointer) when not rhs_owning_method && not is_e1_decl -> (* for __strong e1 = e2 the semantics is*) diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 6fbe7e10b..6b32391d4 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -82,10 +82,10 @@ struct not (CTrans_utils.is_owning_name method_name) && ObjcInterface_decl.is_pointer_to_objc_class typ then let fname = ModelBuiltins.__set_autorelease_attribute in - let ret_id = Ident.create_fresh Ident.knormal in + let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in + (* TODO(jjb): change ret_id to None? *) let stmt_call = - Sil.Call - ([ret_id], Exp.Const (Const.Cfun fname), [(exp, typ)], sil_loc, CallFlags.default) in + Sil.Call (ret_id, Exp.Const (Const.Cfun fname), [(exp, typ)], sil_loc, CallFlags.default) in [stmt_call] else [] @@ -269,8 +269,8 @@ struct let create_call_instr trans_state return_type function_sil params_sil sil_loc call_flags ~is_objc_method = - let ret_id = if (Typ.equal return_type Typ.Tvoid) then [] - else [Ident.create_fresh Ident.knormal] in + let ret_id = if (Typ.equal return_type Typ.Tvoid) then None + else Some (Ident.create_fresh Ident.knormal, return_type) in let ret_id', params, initd_exps, ret_exps = (* Assumption: should_add_return_param will return true only for struct types *) if CMethod_trans.should_add_return_param return_type ~is_objc_method then @@ -298,8 +298,8 @@ struct (* value doesn't work good anyway. This may need to be revisited later*) let ret_param = (var_exp, param_type) in let ret_exp = (var_exp, return_type) in - [], params_sil @ [ret_param], [var_exp], [ret_exp] - else ret_id, params_sil, [], match ret_id with [x] -> [(Exp.Var x, return_type)] | _ -> [] in + None, params_sil @ [ret_param], [var_exp], [ret_exp] + else ret_id, params_sil, [], match ret_id with Some (i,t) -> [(Exp.Var i, t)] | None -> [] in let call_instr = Sil.Call (ret_id', function_sil, params, sil_loc, call_flags) in { empty_res_trans with instrs = [call_instr]; @@ -1998,11 +1998,13 @@ struct let context = trans_state.context in let sil_loc = CLocation.get_sil_location stmt_info context in let fname = ModelBuiltins.__objc_release_autorelease_pool in - let ret_id = Ident.create_fresh Ident.knormal in + let ret_id = Some (Ident.create_fresh Ident.knormal, Typ.Tvoid) in + (* TODO(jjb): change ret_id to None? *) let autorelease_pool_vars = CVar_decl.compute_autorelease_pool_vars context stmts in let stmt_call = - Sil.Call([ret_id], (Exp.Const (Const.Cfun fname)), - autorelease_pool_vars, sil_loc, CallFlags.default) in + Sil.Call + (ret_id, (Exp.Const (Const.Cfun fname)), + autorelease_pool_vars, sil_loc, CallFlags.default) in let node_kind = Cfg.Node.Stmt_node ("Release the autorelease pool") in let call_node = create_node node_kind [stmt_call] sil_loc context in Cfg.Node.set_succs_exn context.cfg call_node trans_state.succ_nodes []; @@ -2162,7 +2164,7 @@ struct let exp = extract_exp_from_list result_trans_param.exps "WARNING: There should be one expression to delete. \n" in let call_instr = - Sil.Call ([], Exp.Const (Const.Cfun fname), [exp], sil_loc, CallFlags.default) in + Sil.Call (None, Exp.Const (Const.Cfun fname), [exp], sil_loc, CallFlags.default) in let call_res_trans = { empty_res_trans with instrs = [call_instr] } in let all_res_trans = if false then (* FIXME (t10135167): call destructor on deleted pointer if it's not null *) @@ -2222,7 +2224,7 @@ struct let exp = match res_trans_stmt.exps with | [e] -> e | _ -> assert false in let args = [exp; (sizeof_expr, Typ.Tvoid)] in let ret_id = Ident.create_fresh Ident.knormal in - let call = Sil.Call ([ret_id], builtin, args, sil_loc, CallFlags.default) in + let call = Sil.Call (Some (ret_id, cast_type), builtin, args, sil_loc, CallFlags.default) in let res_ex = Exp.Var ret_id in let res_trans_dynamic_cast = { empty_res_trans with instrs = [call]; } in let all_res_trans = [ res_trans_stmt; res_trans_dynamic_cast ] in @@ -2244,7 +2246,7 @@ struct IList.map (exec_with_glvalue_as_reference instruction trans_state_param) stmts in let params = collect_exprs res_trans_subexpr_list in let sil_fun = Exp.Const (Const.Cfun pname) in - let call_instr = Sil.Call ([], sil_fun, params, sil_loc, CallFlags.default) in + let call_instr = Sil.Call (None, sil_fun, params, sil_loc, CallFlags.default) in let res_trans_call = { empty_res_trans with instrs = [call_instr]; exps = []; } in @@ -2283,7 +2285,7 @@ struct let ret_exp = Exp.Var ret_id in let field_exp = Exp.Lfield (ret_exp, field_name, typ) in let args = [type_info_objc; (field_exp, Typ.Tvoid)] @ res_trans_subexpr.exps in - let call_instr = Sil.Call ([ret_id], sil_fun, args, sil_loc, CallFlags.default) in + let call_instr = Sil.Call (Some (ret_id, typ), sil_fun, args, sil_loc, CallFlags.default) in let res_trans_call = { empty_res_trans with instrs = [call_instr]; exps = [(ret_exp, typ)]; } in @@ -2306,7 +2308,7 @@ struct let sil_fun = Exp.Const (Const.Cfun fun_name) in let ret_id = Ident.create_fresh Ident.knormal in let ret_exp = Exp.Var ret_id in - let call_instr = Sil.Call ([ret_id], sil_fun, params, sil_loc, CallFlags.default) in + let call_instr = Sil.Call (Some (ret_id, typ), sil_fun, params, sil_loc, CallFlags.default) in let res_trans_call = { empty_res_trans with instrs = [call_instr]; exps = [(ret_exp, typ)]; } in diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index a69446da3..6327c18a7 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -307,8 +307,9 @@ let create_alloc_instrs sil_loc function_type fname size_exp_opt procname_opt = | None -> [] in let args = exp :: procname_arg in let ret_id = Ident.create_fresh Ident.knormal in + let ret_id_typ = Some (ret_id, function_type) in let stmt_call = - Sil.Call([ret_id], Exp.Const (Const.Cfun fname), args, sil_loc, CallFlags.default) in + Sil.Call (ret_id_typ, Exp.Const (Const.Cfun fname), args, sil_loc, CallFlags.default) in (function_type, stmt_call, Exp.Var ret_id) let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc procname_opt = @@ -336,8 +337,9 @@ let objc_new_trans trans_state loc stmt_info cls_name function_type = cls_name CFrontend_config.init Procname.ObjCInstanceMethod in CMethod_trans.create_external_procdesc trans_state.context.CContext.cfg pname is_instance None; let args = [(alloc_ret_exp, alloc_ret_type)] in + let ret_id_typ = Some (init_ret_id, alloc_ret_type) in let init_stmt_call = - Sil.Call ([init_ret_id], Exp.Const (Const.Cfun pname), args, loc, call_flags) in + Sil.Call (ret_id_typ, Exp.Const (Const.Cfun pname), args, loc, call_flags) in let instrs = [alloc_stmt_call; init_stmt_call] in let res_trans_tmp = { empty_res_trans with instrs = instrs } in let res_trans = @@ -369,12 +371,13 @@ let cpp_new_trans sil_loc function_type size_exp_opt = let create_cast_instrs exp cast_from_typ cast_to_typ sil_loc = let ret_id = Ident.create_fresh Ident.knormal in + let ret_id_typ = Some (ret_id, cast_to_typ) in let typ = CTypes.remove_pointer_to_typ cast_to_typ in let sizeof_exp = Exp.Sizeof (typ, None, Subtype.exact) in let pname = ModelBuiltins.__objc_cast in let args = [(exp, cast_from_typ); (sizeof_exp, Typ.Tint Typ.IULong)] in let stmt_call = - Sil.Call ([ret_id], Exp.Const (Const.Cfun pname), args, sil_loc, CallFlags.default) in + Sil.Call (ret_id_typ, Exp.Const (Const.Cfun pname), args, sil_loc, CallFlags.default) in (stmt_call, Exp.Var ret_id) let cast_trans exps sil_loc function_type pname = @@ -439,7 +442,7 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged = let trans_assertion_failure sil_loc context = let assert_fail_builtin = Exp.Const (Const.Cfun ModelBuiltins.__infer_fail) in let args = [Exp.Const (Const.Cstr Config.default_failure_name), Typ.Tvoid] in - let call_instr = Sil.Call ([], assert_fail_builtin, args, sil_loc, CallFlags.default) in + let call_instr = Sil.Call (None, assert_fail_builtin, args, sil_loc, CallFlags.default) in let exit_node = Cfg.Procdesc.get_exit_node (CContext.get_procdesc context) and failure_node = Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [call_instr] sil_loc context in diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index 3a49c5340..a95f2db76 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -510,14 +510,14 @@ let typecheck_instr typestate1 in check_field_assign (); typestate2 - | Sil.Call ([id], Exp.Const (Const.Cfun pn), [(_, typ)], loc, _) + | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), [(_, typ)], loc, _) when Procname.equal pn ModelBuiltins.__new || Procname.equal pn ModelBuiltins.__new_array -> TypeState.add_id id (typ, TypeAnnotation.const Annotations.Nullable false TypeOrigin.New, [loc]) typestate (* new never returns null *) - | Sil.Call ([id], Exp.Const (Const.Cfun pn), (e, typ):: _, loc, _) + | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), (e, typ):: _, loc, _) when Procname.equal pn ModelBuiltins.__cast -> typecheck_expr_for_errors typestate e loc; let e', typestate' = @@ -526,7 +526,7 @@ let typecheck_instr TypeState.add_id id (typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc) typestate' - | Sil.Call ([id], Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _) + | Sil.Call (Some (id, _), Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _) when Procname.equal pn ModelBuiltins.__get_array_length -> let (_, ta, _) = typecheck_expr find_canonical_duplicate @@ -561,7 +561,7 @@ let typecheck_instr | Sil.Call (_, Exp.Const (Const.Cfun pn), _, _, _) when Builtin.is_registered pn -> typestate (* skip othe builtins *) | Sil.Call - (ret_ids, + (ret_id, Exp.Const (Const.Cfun ((Procname.Java callee_pname_java) as callee_pname)), etl_, loc, @@ -608,9 +608,9 @@ let typecheck_instr Procname.java_is_anonymous_inner_class_constructor callee_pname in let do_return loc' typestate' = - match ret_ids with - | [] -> typestate' - | [id] -> + match ret_id with + | None -> typestate' + | Some (id, _) -> let (ia, ret_typ) = annotated_signature.Annotations.ret in let is_library = Specs.proc_is_library callee_attributes in let origin = TypeOrigin.Proc @@ -627,8 +627,7 @@ let typecheck_instr TypeAnnotation.from_item_annotation ia origin, [loc'] ) - typestate' - | _ :: _ :: _ -> assert false in + typestate' in (* Handle Preconditions.checkNotNull. *) let do_preconditions_check_not_null parameter_num is_vararg typestate' = diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index a17684fd8..9168d03b7 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -75,7 +75,7 @@ let inhabit_alloc sizeof_typ sizeof_len ret_typ alloc_kind env = let fun_new = fun_exp_from_name alloc_kind in let sizeof_exp = Exp.Sizeof (sizeof_typ, sizeof_len, Subtype.exact) in let args = [(sizeof_exp, Typ.Tptr (ret_typ, Typ.Pk_pointer))] in - Sil.Call ([retval], fun_new, args, env.pc, cf_alloc) in + Sil.Call (Some (retval, ret_typ), fun_new, args, env.pc, cf_alloc) in (inhabited_exp, env_add_instr call_instr env) (** find or create a Sil expression with type typ *) @@ -166,14 +166,15 @@ and inhabit_constructor tenv constr_name (allocated_obj, obj_type) cfg env = inhabit_args tenv non_receiver_formals cfg env in let constr_instr = let fun_exp = fun_exp_from_name constr_name in - Sil.Call ([], fun_exp, (allocated_obj, obj_type) :: args, env.pc, CallFlags.default) in + Sil.Call (None, fun_exp, (allocated_obj, obj_type) :: args, env.pc, CallFlags.default) in env_add_instr constr_instr env with Not_found -> env let inhabit_call_with_args procname procdesc args env = let retval = - let is_void = Cfg.Procdesc.get_ret_type procdesc = Typ.Tvoid in - if is_void then [] else [Ident.create_fresh Ident.knormal] in + let ret_typ = Cfg.Procdesc.get_ret_type procdesc in + let is_void = ret_typ = Typ.Tvoid in + if is_void then None else Some (Ident.create_fresh Ident.knormal, ret_typ) in let call_instr = let fun_exp = fun_exp_from_name procname in let flags = diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index fd441c436..c8d7b2013 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -454,8 +454,10 @@ let rec expression (context : JContext.t) pc expr = let deref = create_sil_deref sil_ex array_typ_no_ptr loc in let args = [(sil_ex, type_of_ex)] in let ret_id = Ident.create_fresh Ident.knormal in + let ret_typ = Typ.Tint IInt in let call_instr = - Sil.Call ([ret_id], builtin_get_array_length, args, loc, CallFlags.default) in + Sil.Call + (Some (ret_id, ret_typ), builtin_get_array_length, args, loc, CallFlags.default) in (instrs @ [deref; call_instr], Exp.Var ret_id, type_of_expr) | JBir.Conv conv -> let cast_ex = Exp.Cast (JTransType.cast_type conv, sil_ex) in @@ -475,7 +477,8 @@ let rec expression (context : JContext.t) pc expr = | _ -> assert false) in let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.Tvoid)] in let ret_id = Ident.create_fresh Ident.knormal in - let call = Sil.Call([ret_id], builtin, args, loc, CallFlags.default) in + let call = + Sil.Call (Some (ret_id, Tint IBool), builtin, args, loc, CallFlags.default) in let res_ex = Exp.Var ret_id in (instrs @ [call], res_ex, type_of_expr) end @@ -608,12 +611,13 @@ let method_invocation | Some vt -> JTransType.value_type program tenv vt in let call_ret_instrs sil_var = let ret_id = Ident.create_fresh Ident.knormal in - let call_instr = Sil.Call ([ret_id], callee_fun, call_args, loc, call_flags) in + let call_instr = + Sil.Call (Some (ret_id, return_type), callee_fun, call_args, loc, call_flags) in let set_instr = Sil.Store (Exp.Lvar sil_var, return_type, Exp.Var ret_id, loc) in (instrs @ [call_instr; set_instr]) in match var_opt with | None -> - let call_instr = Sil.Call ([], callee_fun, call_args, loc, call_flags) in + let call_instr = Sil.Call (None, callee_fun, call_args, loc, call_flags) in instrs @ [call_instr] | Some var -> let sil_var = JContext.set_pvar context var return_type in @@ -628,7 +632,7 @@ let method_invocation when Procname.is_constructor callee_procname && JTransType.is_closeable program tenv typ -> let set_file_attr = let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_file_attribute) in - Sil.Call ([], set_builtin, [exp], loc, CallFlags.default) in + Sil.Call (None, set_builtin, [exp], loc, CallFlags.default) in (* Exceptions thrown in the constructor should prevent adding the resource attribute *) call_instrs @ [set_file_attr] @@ -637,7 +641,7 @@ let method_invocation when Procname.java_is_close callee_procname && JTransType.is_closeable program tenv typ -> let set_mem_attr = let set_builtin = Exp.Const (Const.Cfun ModelBuiltins.__set_mem_attribute) in - Sil.Call ([], set_builtin, [exp], loc, CallFlags.default) in + Sil.Call (None, set_builtin, [exp], loc, CallFlags.default) in (* Exceptions thrown in the close method should not prevent the resource from being *) (* considered as closed *) [set_mem_attr] @ call_instrs @@ -772,7 +776,7 @@ let assume_not_null loc sil_expr = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in let assume_call_flag = { CallFlags.default with CallFlags.cf_noreturn = true; } in let call_args = [(not_null_expr, Typ.Tint Typ.IBool)] in - Sil.Call ([], builtin_infer_assume, call_args, loc, assume_call_flag) + Sil.Call (None, builtin_infer_assume, call_args, loc, assume_call_flag) let rec instruction (context : JContext.t) pc instr : translation = let cfg = JContext.get_cfg context in @@ -803,7 +807,7 @@ let rec instruction (context : JContext.t) pc instr : translation = let trans_monitor_enter_exit context expr pc loc builtin node_desc = let instrs, sil_expr, sil_type = expression context pc expr in let builtin_const = Exp.Const (Const.Cfun builtin) in - let instr = Sil.Call ([], builtin_const, [(sil_expr, sil_type)], loc, CallFlags.default) in + let instr = Sil.Call (None, builtin_const, [(sil_expr, sil_type)], loc, CallFlags.default) in let typ_no_ptr = match sil_type with | Typ.Tptr (typ, _) -> typ | _ -> sil_type in @@ -912,7 +916,8 @@ let rec instruction (context : JContext.t) pc instr : translation = let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in let args = [(sizeof_exp, class_type)] in let ret_id = Ident.create_fresh Ident.knormal in - let new_instr = Sil.Call([ret_id], builtin_new, args, loc, CallFlags.default) in + let new_instr = + Sil.Call (Some (ret_id, class_type), builtin_new, args, loc, CallFlags.default) in let constr_ms = JBasics.make_ms JConfig.constructor_name constr_type_list None in let constr_procname, call_instrs = let ret_opt = Some (Exp.Var ret_id, class_type) in @@ -934,7 +939,9 @@ let rec instruction (context : JContext.t) pc instr : translation = let (instrs, array_size) = get_array_length context pc expr_list content_type in let call_args = [(array_size, array_type)] in let ret_id = Ident.create_fresh Ident.knormal in - let call_instr = Sil.Call([ret_id], builtin_new_array, call_args, loc, CallFlags.default) in + let call_instr = + Sil.Call + (Some (ret_id, array_type), builtin_new_array, call_args, loc, CallFlags.default) in let set_instr = Sil.Store (Exp.Lvar array_name, array_type, Exp.Var ret_id, loc) in let node_kind = Cfg.Node.Stmt_node "method_body" in let node = create_node node_kind (instrs @ [call_instr; set_instr]) in @@ -1002,7 +1009,7 @@ let rec instruction (context : JContext.t) pc instr : translation = | JBir.Check (JBir.CheckNullPointer expr) when Config.report_runtime_exceptions && is_this expr -> - (* TODO #6509339: refactor the boilterplate code in the translattion of JVM checks *) + (* TODO #6509339: refactor the boilerplate code in the translation of JVM checks *) let (instrs, sil_expr, _) = expression context pc expr in let this_not_null_node = create_node @@ -1026,7 +1033,8 @@ let rec instruction (context : JContext.t) pc instr : translation = let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in let args = [(sizeof_exp, class_type)] in let ret_id = Ident.create_fresh Ident.knormal in - let new_instr = Sil.Call([ret_id], builtin_new, args, loc, CallFlags.default) in + let new_instr = + Sil.Call (Some (ret_id, class_type), builtin_new, args, loc, CallFlags.default) in let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in let _, call_instrs = let ret_opt = Some (Exp.Var ret_id, class_type) in @@ -1079,7 +1087,8 @@ let rec instruction (context : JContext.t) pc instr : translation = let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in let args = [(sizeof_exp, class_type)] in let ret_id = Ident.create_fresh Ident.knormal in - let new_instr = Sil.Call([ret_id], builtin_new, args, loc, CallFlags.default) in + let new_instr = + Sil.Call (Some (ret_id, ret_type), builtin_new, args, loc, CallFlags.default) in let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in let _, call_instrs = method_invocation @@ -1101,7 +1110,7 @@ let rec instruction (context : JContext.t) pc instr : translation = JTransType.sizeof_of_object_type program tenv object_type Subtype.subtypes_instof in let check_cast = Exp.Const (Const.Cfun ModelBuiltins.__instanceof) in let args = [(sil_expr, sil_type); (sizeof_expr, Typ.Tvoid)] in - let call = Sil.Call([ret_id], check_cast, args, loc, CallFlags.default) in + let call = Sil.Call (Some (ret_id, ret_type), check_cast, args, loc, CallFlags.default) in let res_ex = Exp.Var ret_id in let is_instance_node = let check_is_false = Exp.BinOp (Binop.Ne, res_ex, Exp.zero) in @@ -1118,7 +1127,8 @@ let rec instruction (context : JContext.t) pc instr : translation = let sizeof_exp = Exp.Sizeof (class_type_np, None, Subtype.exact) in let args = [(sizeof_exp, class_type)] in let ret_id = Ident.create_fresh Ident.knormal in - let new_instr = Sil.Call([ret_id], builtin_new, args, loc, CallFlags.default) in + let new_instr = + Sil.Call (Some (ret_id, ret_type), builtin_new, args, loc, CallFlags.default) in let constr_ms = JBasics.make_ms JConfig.constructor_name [] None in let _, call_instrs = method_invocation context loc pc None cce_cn constr_ms diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index d8be17b80..31ca8a68b 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -43,7 +43,8 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle let instr_unwrap_ret_val = let unwrap_builtin = Exp.Const (Const.Cfun ModelBuiltins.__unwrap_exception) in Sil.Call - ([id_exn_val], unwrap_builtin, [(Exp.Var id_ret_val, ret_type)], loc, CallFlags.default) in + (Some (id_exn_val, ret_type), unwrap_builtin, [(Exp.Var id_ret_val, ret_type)], loc, + CallFlags.default) in create_node loc Cfg.Node.exn_handler_kind @@ -72,7 +73,8 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle let args = [ (Exp.Var id_exn_val, Typ.Tptr(exn_type, Typ.Pk_pointer)); (Exp.Sizeof (exn_type, None, Subtype.exact), Typ.Tvoid)] in - Sil.Call ([id_instanceof], instanceof_builtin, args, loc, CallFlags.default) in + Sil.Call + (Some (id_instanceof, Tint IBool), instanceof_builtin, args, loc, CallFlags.default) in let if_kind = Sil.Ik_switch in let instr_prune_true = Sil.Prune (Exp.Var id_instanceof, loc, true, if_kind) in let instr_prune_false = diff --git a/infer/src/java/jTransStaticField.ml b/infer/src/java/jTransStaticField.ml index 4271e4bbf..ee3bc5128 100644 --- a/infer/src/java/jTransStaticField.ml +++ b/infer/src/java/jTransStaticField.ml @@ -188,7 +188,8 @@ let translate_instr_static_field (context : JContext.t) callee_procdesc fs field let callee_fun = Exp.Const (Const.Cfun callee_procname) in let field_arg = Exp.Const (Const.Cstr (JBasics.fs_name fs)) in let call_instr = - Sil.Call ([ret_id], callee_fun, [field_arg, field_type], loc, CallFlags.default) in + Sil.Call + (Some (ret_id, field_type), callee_fun, [field_arg, field_type], loc, CallFlags.default) in Cg.add_edge cg caller_procname callee_procname; ([call_instr], Exp.Var ret_id) diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 934070bb0..1c1cbc168 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -97,7 +97,8 @@ let rec trans_annotated_instructions end | Call (ret_var, func_var, typed_args) -> let new_sil_instr = Sil.Call ( - [ident_of_variable ret_var], + (* TODO: translate type of ret_var *) + Some (ident_of_variable ret_var, Tvoid), Exp.Const (Const.Cfun (procname_of_function_variable func_var)), IList.map (fun (tp, arg) -> (trans_operand arg, trans_typ tp)) typed_args, location, CallFlags.default) in diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index f43df01c2..506e455ee 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -176,7 +176,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct { astate with Domain.access_tree = access_tree'; } let apply_summary - ret_ids + ret_id actuals summary (astate_in : Domain.astate) @@ -185,9 +185,8 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct let callee_loc = CallSite.loc callee_site in let apply_return ret_ap = function - | [ret_id] -> AccessPath.with_base_var (Var.of_id ret_id) ret_ap - | [] -> failwith "Have summary for retval, but no ret id to bind it to!" - | _ -> failwith "Unimp: summaries for function with multiple return values" in + | Some (ret_id, _) -> AccessPath.with_base_var (Var.of_id ret_id) ret_ap + | None -> failwith "Have summary for retval, but no ret id to bind it to!" in let get_actual_ap_trace formal_num formal_ap access_tree = let get_actual_ap formal_num = @@ -226,7 +225,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct let caller_ap_trace_opt = match in_out_summary.output with | Out_return ret_ap -> - Some (apply_return ret_ap ret_ids, TraceDomain.initial) + Some (apply_return ret_ap ret_id, TraceDomain.initial) | Out_formal (formal_num, formal_ap) -> get_actual_ap_trace formal_num formal_ap access_tree | Out_global global_ap -> @@ -283,7 +282,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct | _ -> astate' end - | Sil.Call ([ret_id], Const (Cfun callee_pname), args, loc, _) + | Sil.Call (Some (ret_id, _), Const (Cfun callee_pname), args, loc, _) when Builtin.is_registered callee_pname -> if Procname.equal callee_pname ModelBuiltins.__cast then @@ -298,7 +297,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct Location.pp loc else astate - | Sil.Call (ret_ids, Const (Cfun callee_pname), actuals, callee_loc, _) -> + | Sil.Call (ret_id, Const (Cfun callee_pname), actuals, callee_loc, _) -> let call_site = CallSite.make callee_pname callee_loc in let astate_with_sink = @@ -316,11 +315,11 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct failwith "Unimp: looking up return type for non-Java procedure" in let astate_with_source = - match TraceDomain.Source.get call_site, ret_ids with - | [(0, source)], [ret_id] -> + match TraceDomain.Source.get call_site, ret_id with + | [(0, source)], Some (ret_id, _) -> let access_tree = add_source source ret_id ret_typ astate_with_sink.access_tree in { astate_with_sink with access_tree; } - | [], _ | _, [] -> + | [], _ | _, None -> astate_with_sink | _ -> (* this is allowed by SIL, but not currently used in any frontends *) @@ -329,7 +328,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct let astate_with_summary = match Summary.read_summary proc_data.tenv proc_data.pdesc callee_pname with | Some summary -> - apply_summary ret_ids actuals summary astate_with_source proc_data call_site + apply_summary ret_id actuals summary astate_with_source proc_data call_site | None -> astate_with_source in diff --git a/infer/src/unit/BoundedCallTreeTests.ml b/infer/src/unit/BoundedCallTreeTests.ml index 6b9ff1d75..1502e9962 100644 --- a/infer/src/unit/BoundedCallTreeTests.ml +++ b/infer/src/unit/BoundedCallTreeTests.ml @@ -24,7 +24,7 @@ let tests = let f_proc_name = Procname.from_string_c_fun "f" in let g_proc_name = Procname.from_string_c_fun "g" in let g_args = [((Exp.Const (Const.Cint (IntLit.one))), (Typ.Tint IInt))] in - let g_ret_ids = [(ident_of_str "r")] in + let g_ret_id = Some (ident_of_str "r", Typ.Tint IInt) in let class_name = "com.example.SomeClass" in let file_name = "SomeClass.java" in let trace = Stacktrace.make "java.lang.NullPointerException" @@ -44,47 +44,47 @@ let tests = let test_list_from_foo = [ "on_call_add_proc_name", [ - make_call ~procname:f_proc_name [] []; (* means f() *) + make_call ~procname:f_proc_name None []; (* means f() *) invariant "{ f }" ]; "on_call_add_proc_name_w_args", [ - make_call ~procname:g_proc_name g_ret_ids g_args; (* means r = a.g(1) *) + make_call ~procname:g_proc_name g_ret_id g_args; (* means r = a.g(1) *) invariant "{ g }" ]; "handle_two_proc_calls", [ - make_call ~procname:f_proc_name [] []; + make_call ~procname:f_proc_name None []; invariant "{ f }"; - make_call ~procname:g_proc_name g_ret_ids g_args; + make_call ~procname:g_proc_name g_ret_id g_args; invariant "{ f, g }" ]; "dont_record_procs_twice", [ - make_call ~procname:f_proc_name [] []; + make_call ~procname:f_proc_name None []; invariant "{ f }"; - make_call ~procname:f_proc_name [] []; + make_call ~procname:f_proc_name None []; invariant "{ f }" ]; ] |> TestInterpreter.create_tests ~test_pname:caller_foo_name extras in let test_list_from_bar = [ "on_call_anywhere_on_stack_add_proc_name", [ - make_call ~procname:f_proc_name [] []; (* means f() *) + make_call ~procname:f_proc_name None []; (* means f() *) invariant "{ f }" ]; ] |> TestInterpreter.create_tests ~test_pname:caller_bar_name extras in let test_list_from_baz = [ "ignore_procs_unrelated_to_trace", [ - make_call ~procname:f_proc_name [] []; (* means f() *) + make_call ~procname:f_proc_name None []; (* means f() *) invariant "{ }" ]; ] |> TestInterpreter.create_tests ~test_pname:caller_baz_name extras in let test_list_multiple_traces_from_foo = [ "on_call_add_proc_name_in_any_stack_1", [ - make_call ~procname:f_proc_name [] []; (* means f() *) + make_call ~procname:f_proc_name None []; (* means f() *) invariant "{ f }" ]; ] |> TestInterpreter.create_tests @@ -92,7 +92,7 @@ let tests = let test_list_multiple_traces_from_bar = [ "on_call_add_proc_name_in_any_stack_2", [ - make_call ~procname:f_proc_name [] []; (* means f() *) + make_call ~procname:f_proc_name None []; (* means f() *) invariant "{ f }" ]; ] |> TestInterpreter.create_tests diff --git a/infer/src/unit/TaintTests.ml b/infer/src/unit/TaintTests.ml index 8d71b5cbc..70485114e 100644 --- a/infer/src/unit/TaintTests.ml +++ b/infer/src/unit/TaintTests.ml @@ -115,13 +115,13 @@ let tests = PrettyPrintable.pp_collection ~pp_item fmt (IList.rev trace_assocs) in let assign_to_source ret_str = let procname = Procname.from_string_c_fun "SOURCE" in - make_call ~procname [ident_of_str ret_str] [] in + make_call ~procname (Some (ident_of_str ret_str, dummy_typ)) [] in let assign_to_non_source ret_str = let procname = Procname.from_string_c_fun "NON-SOURCE" in - make_call ~procname [ident_of_str ret_str] [] in + make_call ~procname (Some (ident_of_str ret_str, dummy_typ)) [] in let call_sink_with_exp exp = let procname = Procname.from_string_c_fun "SINK" in - make_call ~procname [] [(exp, dummy_typ)] in + make_call ~procname None [(exp, dummy_typ)] in let call_sink actual_str = call_sink_with_exp (Exp.Var (ident_of_str actual_str)) in let assign_id_to_field root_str fld_str rhs_id_str = diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index 6158fadc5..fbc8523be 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -90,9 +90,9 @@ module StructuredSil = struct let make_set ~rhs_typ ~lhs_exp ~rhs_exp = Cmd (Sil.Store (lhs_exp, rhs_typ, rhs_exp, dummy_loc)) - let make_call ?(procname=dummy_procname) ret_ids args = + let make_call ?(procname=dummy_procname) ret_id args = let call_exp = Exp.Const (Const.Cfun procname) in - Cmd (Sil.Call (ret_ids, call_exp, args, dummy_loc, CallFlags.default)) + Cmd (Sil.Call (ret_id, call_exp, args, dummy_loc, CallFlags.default)) let make_store ~rhs_typ root_exp fld_str ~rhs_exp = let fld = AccessPathTestUtils.make_fieldname fld_str in @@ -124,7 +124,7 @@ module StructuredSil = struct let cast_id_to_id lhs cast_typ rhs = let lhs_id = ident_of_str lhs in let rhs_id = Exp.Var (ident_of_str rhs) in - make_call ~procname:ModelBuiltins.__cast [lhs_id] [rhs_id, cast_typ] + make_call ~procname:ModelBuiltins.__cast (Some (lhs_id, cast_typ)) [rhs_id, cast_typ] let var_assign_exp ~rhs_typ lhs rhs_exp = let lhs_exp = var_of_str lhs in @@ -146,13 +146,13 @@ module StructuredSil = struct let rhs_exp = var_of_str rhs in make_set ~rhs_typ ~lhs_exp ~rhs_exp - let call_unknown ret_id_strs arg_strs = + let call_unknown ret_id_str_opt arg_strs = let args = IList.map (fun param_str -> (var_of_str param_str, dummy_typ)) arg_strs in - let ret_ids = IList.map ident_of_str ret_id_strs in - make_call ret_ids args + let ret_id = Option.map (fun (str, typ) -> (ident_of_str str, typ)) ret_id_str_opt in + make_call ret_id args let call_unknown_no_ret arg_strs = - call_unknown [] arg_strs + call_unknown None arg_strs end module Make diff --git a/infer/src/unit/livenessTests.ml b/infer/src/unit/livenessTests.ml index 04efd4965..50d2c3487 100644 --- a/infer/src/unit/livenessTests.ml +++ b/infer/src/unit/livenessTests.ml @@ -99,7 +99,7 @@ let tests = "dead_after_call_with_retval", [ assert_empty; - call_unknown ["y"] []; + call_unknown (Some ("y", Typ.Tint IInt)) []; invariant "{ y$0 }"; id_assign_id "x" "y"; ];