From a50fcaf2ddddee2e748fe355422f6cad2bc3e4ce Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 4 Sep 2019 07:55:36 -0700 Subject: [PATCH] [infer] Use inline record for Sil.Load and Sil.Store Summary: It uses inline record for Sil.Load and Sil.Store for preparing the following extention. Reviewed By: dulmarod Differential Revision: D17161288 fbshipit-source-id: 637ea7bfa --- infer/src/IR/Cfg.ml | 27 ++++++---- infer/src/IR/HilInstr.ml | 7 +-- infer/src/IR/Sil.ml | 47 +++++++---------- infer/src/IR/Sil.mli | 16 +++--- infer/src/IR/SpecializeProcdesc.ml | 45 +++++++++------- infer/src/absint/PatternMatch.ml | 16 +++--- infer/src/backend/errdesc.ml | 18 +++---- infer/src/backend/preanal.ml | 4 +- infer/src/biabduction/Buckets.ml | 4 +- infer/src/biabduction/BuiltinDefn.ml | 17 ++++-- infer/src/biabduction/State.ml | 2 +- infer/src/biabduction/SymExec.ml | 6 +-- .../bufferoverrun/bufferOverrunAnalysis.ml | 12 ++--- .../src/bufferoverrun/bufferOverrunChecker.ml | 4 +- infer/src/checkers/NullabilityPreanalysis.ml | 4 +- infer/src/checkers/Siof.ml | 6 +-- infer/src/checkers/addressTaken.ml | 2 +- infer/src/checkers/classLoads.ml | 4 +- infer/src/checkers/control.ml | 2 +- infer/src/checkers/cost.ml | 2 +- infer/src/checkers/dataflow.ml | 2 +- infer/src/checkers/functionPointers.ml | 7 +-- infer/src/checkers/idenv.ml | 2 +- .../src/checkers/inefficientKeysetIterator.ml | 4 +- infer/src/checkers/liveness.ml | 10 ++-- infer/src/checkers/loopInvariant.ml | 12 ++--- infer/src/checkers/printfArgs.ml | 2 +- infer/src/checkers/reachingDefs.ml | 8 +-- infer/src/clang/cArithmetic_trans.ml | 21 ++++---- infer/src/clang/cTrans.ml | 27 ++++++---- infer/src/clang/cTrans_utils.ml | 7 +-- infer/src/java/jTrans.ml | 52 +++++++++++++------ infer/src/java/jTransExn.ml | 13 +++-- infer/src/nullsafe/typeCheck.ml | 12 ++--- infer/src/pulse/Pulse.ml | 4 +- infer/src/topl/Topl.ml | 6 ++- infer/src/topl/ToplMonitor.ml | 17 +++--- infer/src/unit/analyzerTester.ml | 8 ++- 38 files changed, 260 insertions(+), 199 deletions(-) diff --git a/infer/src/IR/Cfg.ml b/infer/src/IR/Cfg.ml index 5d73f43fa..a78ee5710 100644 --- a/infer/src/IR/Cfg.ml +++ b/infer/src/IR/Cfg.ml @@ -71,20 +71,29 @@ let inline_synthetic_method ((ret_id, _) as ret) etl pdesc loc_call : Sil.instr in let do_instr instr = match (instr, etl) with - | Sil.Load (_, Exp.Lfield (Exp.Var _, fn, ft), bt, _), [(* getter for fields *) (e1, _)] -> - let instr' = Sil.Load (ret_id, Exp.Lfield (e1, fn, ft), bt, loc_call) in + | Sil.Load {e= Exp.Lfield (Exp.Var _, fn, ft); root_typ= bt}, [(* getter for fields *) (e1, _)] + -> + let instr' = + Sil.Load {id= ret_id; e= Exp.Lfield (e1, fn, ft); root_typ= bt; loc= loc_call} + in found instr instr' - | Sil.Load (_, Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, _), [] when Pvar.is_global pvar -> + | Sil.Load {e= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt}, [] 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) in + let instr' = + Sil.Load {id= ret_id; e= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt; loc= loc_call} + in found instr instr' - | Sil.Store (Exp.Lfield (_, fn, ft), bt, _, _), [(* setter for fields *) (e1, _); (e2, _)] -> - let instr' = Sil.Store (Exp.Lfield (e1, fn, ft), bt, e2, loc_call) in + | ( Sil.Store {e1= Exp.Lfield (_, fn, ft); root_typ= bt} + , [(* setter for fields *) (e1, _); (e2, _)] ) -> + let instr' = Sil.Store {e1= Exp.Lfield (e1, fn, ft); root_typ= bt; e2; loc= loc_call} in found instr instr' - | Sil.Store (Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, _, _), [(e1, _)] when Pvar.is_global pvar - -> + | Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt}, [(e1, _)] + when Pvar.is_global pvar -> (* setter for static fields *) - let instr' = Sil.Store (Exp.Lfield (Exp.Lvar pvar, fn, ft), bt, e1, loc_call) in + let instr' = + Sil.Store {e1= Exp.Lfield (Exp.Lvar pvar, fn, ft); root_typ= bt; e2= e1; loc= loc_call} + in found instr instr' | Sil.Call (_, Exp.Const (Const.Cfun pn), etl', _, cf), _ when Int.equal (List.length etl') (List.length etl) -> diff --git a/infer/src/IR/HilInstr.ml b/infer/src/IR/HilInstr.ml index 594079274..72cdece62 100644 --- a/infer/src/IR/HilInstr.ml +++ b/infer/src/IR/HilInstr.ml @@ -58,9 +58,10 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) = Instr (Assign (HilExp.AccessExpression.base (lhs_id, rhs_typ), rhs_hil_exp, loc)) in match instr with - | Load (lhs_id, rhs_exp, rhs_typ, loc) -> + | Load {id= lhs_id; e= rhs_exp; root_typ= rhs_typ; loc} -> analyze_id_assignment ~add_deref:true (Var.of_id lhs_id) rhs_exp rhs_typ loc - | Store (Lvar lhs_pvar, lhs_typ, rhs_exp, loc) when Pvar.is_ssa_frontend_tmp lhs_pvar -> + | Store {e1= Lvar lhs_pvar; root_typ= lhs_typ; e2= rhs_exp; loc} + when Pvar.is_ssa_frontend_tmp lhs_pvar -> (* do not need to add deref here as it is added implicitly in of_pvar by forgetting the & *) analyze_id_assignment (Var.of_pvar lhs_pvar) rhs_exp lhs_typ loc | Call @@ -71,7 +72,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) = , _ ) when Typ.Procname.equal callee_pname BuiltinDecl.__cast -> analyze_id_assignment (Var.of_id ret_id) target_exp cast_typ loc - | Store (lhs_exp, typ, rhs_exp, loc) -> + | Store {e1= lhs_exp; root_typ= typ; e2= rhs_exp; loc} -> let lhs_access_expr = match HilExp.access_expr_of_exp ~include_array_indexes ~f_resolve_id lhs_exp typ with | Some access_expr -> diff --git a/infer/src/IR/Sil.ml b/infer/src/IR/Sil.ml index 8c82ec3be..94601c8fb 100644 --- a/infer/src/IR/Sil.ml +++ b/infer/src/IR/Sil.ml @@ -40,24 +40,17 @@ type instr = (* Note for frontend writers: [x] must be used in a subsequent instruction, otherwise the entire `Load` instruction may be eliminated by copy-propagation. *) - | Load of Ident.t * Exp.t * Typ.t * Location.t + | Load of {id: Ident.t; e: Exp.t; root_typ: Typ.t; loc: Location.t} (** Load a value from the heap into an identifier. - - [x = *lexp:typ] where - - - [lexp] is an expression denoting a heap address - - - [typ] is the root type of [lexp]. *) - | Store of Exp.t * Typ.t * Exp.t * Location.t + [x = *exp:root_typ] where + [exp] is an expression denoting a heap address + [root_typ] is the root type of [exp]. *) + | Store of {e1: Exp.t; root_typ: Typ.t; e2: Exp.t; loc: Location.t} (** Store the value of an expression into the heap. - - [*lexp1:typ = exp2] where - - - [lexp1] is an expression denoting a heap address - - - [typ] is the root type of [lexp1] - - - [exp2] is the expression whose value is stored. *) + [*exp1:root_typ = exp2] where + [exp1] is an expression denoting a heap address + [root_typ] is the root type of [exp1] + [exp2] is the expression whose value is stored. *) | Prune of Exp.t * Location.t * bool * if_kind (** prune the state based on [exp=1], the boolean indicates whether true branch *) | Call of (Ident.t * Typ.t) * Exp.t * (Exp.t * Typ.t) list * Location.t * CallFlags.t @@ -350,7 +343,7 @@ let location_of_instr_metadata = function (** Get the location of the instruction *) let location_of_instr = function - | Load (_, _, _, loc) | Store (_, _, _, loc) | Prune (_, loc, _, _) | Call (_, _, _, loc, _) -> + | Load {loc} | Store {loc} | Prune (_, loc, _, _) | Call (_, _, _, loc, _) -> loc | Metadata metadata -> location_of_instr_metadata metadata @@ -371,9 +364,9 @@ let exps_of_instr_metadata = function (** get the expressions occurring in the instruction *) let exps_of_instr = function - | Load (id, e, _, _) -> + | Load {id; e} -> [Exp.Var id; e] - | Store (e1, _, e2, _) -> + | Store {e1; e2} -> [e1; e2] | Prune (cond, _, _, _) -> [cond] @@ -419,11 +412,11 @@ let pp_instr ~print_types pe0 f instr = let pp_typ = if print_types then Typ.pp_full else Typ.pp in color_wrapper pe0 f instr ~f:(fun pe f instr -> match instr with - | Load (id, e, t, loc) -> + | Load {id; e; root_typ; loc} -> F.fprintf f "%a=*%a:%a [%a]" Ident.pp id (pp_exp_printenv ~print_types pe) e (pp_typ pe0) - t Location.pp loc - | Store (e1, t, e2, loc) -> - F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) t + root_typ Location.pp loc + | Store {e1; root_typ; e2; loc} -> + F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) root_typ (pp_exp_printenv ~print_types pe) e2 Location.pp loc | Prune (cond, loc, true_branch, _) -> F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv ~print_types pe) cond true_branch @@ -1274,16 +1267,16 @@ let instr_sub_ids ~sub_id_binders f instr = match exp_sub_ids f (Var id) with Var id' when not (Ident.equal id id') -> id' | _ -> id in match instr with - | Load (id, rhs_exp, typ, loc) -> + | Load {id; e= rhs_exp; root_typ; loc} -> let id' = if sub_id_binders then sub_id id else id in let rhs_exp' = exp_sub_ids f rhs_exp in if phys_equal id' id && phys_equal rhs_exp' rhs_exp then instr - else Load (id', rhs_exp', typ, loc) - | Store (lhs_exp, typ, rhs_exp, loc) -> + else Load {id= id'; e= rhs_exp'; root_typ; loc} + | Store {e1= lhs_exp; root_typ; e2= rhs_exp; loc} -> let lhs_exp' = exp_sub_ids f lhs_exp in let rhs_exp' = exp_sub_ids f rhs_exp in if phys_equal lhs_exp' lhs_exp && phys_equal rhs_exp' rhs_exp then instr - else Store (lhs_exp', typ, rhs_exp', loc) + else Store {e1= lhs_exp'; root_typ; e2= rhs_exp'; loc} | Call (((id, typ) as ret_id_typ), fun_exp, actuals, call_flags, loc) -> let ret_id' = if sub_id_binders then diff --git a/infer/src/IR/Sil.mli b/infer/src/IR/Sil.mli index 9207c40f7..03c06409d 100644 --- a/infer/src/IR/Sil.mli +++ b/infer/src/IR/Sil.mli @@ -38,16 +38,16 @@ type instr = (* Note for frontend writers: [x] must be used in a subsequent instruction, otherwise the entire `Load` instruction may be eliminated by copy-propagation. *) - | Load of Ident.t * Exp.t * Typ.t * Location.t + | Load of {id: Ident.t; e: Exp.t; root_typ: Typ.t; loc: Location.t} (** Load a value from the heap into an identifier. - [x = *lexp:typ] where - [lexp] is an expression denoting a heap address - [typ] is the root type of [lexp]. *) - | Store of Exp.t * Typ.t * Exp.t * Location.t + [x = *exp:root_typ] where + [exp] is an expression denoting a heap address + [root_typ] is the root type of [exp]. *) + | Store of {e1: Exp.t; root_typ: Typ.t; e2: Exp.t; loc: Location.t} (** Store the value of an expression into the heap. - [*lexp1:typ = exp2] where - [lexp1] is an expression denoting a heap address - [typ] is the root type of [lexp1] + [*exp1:root_typ = exp2] where + [exp1] is an expression denoting a heap address + [root_typ] is the root type of [exp1] [exp2] is the expression whose value is stored. *) | Prune of Exp.t * Location.t * bool * if_kind (** prune the state based on [exp=1], the boolean indicates whether true branch *) diff --git a/infer/src/IR/SpecializeProcdesc.ml b/infer/src/IR/SpecializeProcdesc.ml index 3e7e0b35d..a398fe621 100644 --- a/infer/src/IR/SpecializeProcdesc.ml +++ b/infer/src/IR/SpecializeProcdesc.ml @@ -63,28 +63,31 @@ let with_formals_types_proc callee_pdesc resolved_pdesc substitutions = in let convert_instr = function | Sil.Load - ( id - , (Exp.Lvar origin_pvar as origin_exp) - , {Typ.desc= Tptr ({desc= Tstruct origin_typename}, Pk_pointer)} - , loc ) -> + { id + ; e= Exp.Lvar origin_pvar as origin_exp + ; root_typ= {Typ.desc= Tptr ({desc= Tstruct origin_typename}, Pk_pointer)} + ; loc } -> let specialized_typname = try Mangled.Map.find (Pvar.get_name origin_pvar) substitutions with Caml.Not_found -> origin_typename in subst_map := Ident.Map.add id specialized_typname !subst_map ; - Some (Sil.Load (id, convert_exp origin_exp, mk_ptr_typ specialized_typname, loc)) - | Sil.Load (id, (Exp.Var origin_id as origin_exp), ({Typ.desc= Tstruct _} as origin_typ), loc) + Some + (Sil.Load {id; e= convert_exp origin_exp; root_typ= mk_ptr_typ specialized_typname; loc}) + | Sil.Load + {id; e= Exp.Var origin_id as origin_exp; root_typ= {Typ.desc= Tstruct _} as origin_typ; loc} -> let updated_typ : Typ.t = try Typ.mk ~default:origin_typ (Tstruct (Ident.Map.find origin_id !subst_map)) with Caml.Not_found -> origin_typ in - Some (Sil.Load (id, convert_exp origin_exp, updated_typ, loc)) - | Sil.Load (id, origin_exp, origin_typ, loc) -> - Some (Sil.Load (id, convert_exp origin_exp, origin_typ, loc)) - | Sil.Store (assignee_exp, origin_typ, origin_exp, loc) -> + Some (Sil.Load {id; e= convert_exp origin_exp; root_typ= updated_typ; loc}) + | Sil.Load {id; e= origin_exp; root_typ= origin_typ; loc} -> + Some (Sil.Load {id; e= convert_exp origin_exp; root_typ= origin_typ; loc}) + | Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= origin_exp; loc} -> let set_instr = - Sil.Store (convert_exp assignee_exp, origin_typ, convert_exp origin_exp, loc) + Sil.Store + {e1= convert_exp assignee_exp; root_typ= origin_typ; e2= convert_exp origin_exp; loc} in Some set_instr | Sil.Call @@ -203,7 +206,9 @@ let with_block_args_instrs resolved_pdesc substitutions = List.map extra_formals ~f:(fun (var, typ) -> let id = Ident.create_fresh_specialized_with_blocks Ident.knormal in let pvar = Pvar.mk var resolved_pname in - (Var.of_id id, (Exp.Var id, pvar, typ), Sil.Load (id, Exp.Lvar pvar, typ, loc)) ) + ( Var.of_id id + , (Exp.Var id, pvar, typ) + , Sil.Load {id; e= Exp.Lvar pvar; root_typ= typ; loc} ) ) |> List.unzip3 in let remove_temps_instr = Sil.Metadata (ExitScope (dead_vars, loc)) in @@ -215,24 +220,26 @@ let with_block_args_instrs resolved_pdesc substitutions = (call_instr :: instrs, id_map) in match instr with - | Sil.Load (id, Exp.Lvar block_param, _, _) + | Sil.Load {id; e= Exp.Lvar block_param} when Mangled.Map.mem (Pvar.get_name block_param) substitutions -> let id_map = Ident.Map.add id (Pvar.get_name block_param) id_map in (* we don't need the load the block param instruction anymore *) (instrs, id_map) - | Sil.Load (id, origin_exp, origin_typ, loc) -> - (Sil.Load (id, convert_exp origin_exp, origin_typ, loc) :: instrs, id_map) - | Sil.Store (assignee_exp, origin_typ, Exp.Var id, loc) when Ident.Map.mem id id_map -> + | Sil.Load {id; e= origin_exp; root_typ= origin_typ; loc} -> + (Sil.Load {id; e= convert_exp origin_exp; root_typ= origin_typ; loc} :: instrs, id_map) + | Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= Exp.Var id; loc} + when Ident.Map.mem id id_map -> let block_param = Ident.Map.find id id_map in let block_name, id_exp_typs, load_instrs, remove_temps_instr = get_block_name_and_load_captured_vars_instrs block_param loc in let closure = Exp.Closure {name= block_name; captured_vars= id_exp_typs} in - let instr = Sil.Store (assignee_exp, origin_typ, closure, loc) in + let instr = Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= closure; loc} in ((remove_temps_instr :: instr :: load_instrs) @ instrs, id_map) - | Sil.Store (assignee_exp, origin_typ, origin_exp, loc) -> + | Sil.Store {e1= assignee_exp; root_typ= origin_typ; e2= origin_exp; loc} -> let set_instr = - Sil.Store (convert_exp assignee_exp, origin_typ, convert_exp origin_exp, loc) + Sil.Store + {e1= convert_exp assignee_exp; root_typ= origin_typ; e2= convert_exp origin_exp; loc} in (set_instr :: instrs, id_map) | Sil.Call (return_ids, Exp.Var id, origin_args, loc, call_flags) -> ( diff --git a/infer/src/absint/PatternMatch.ml b/infer/src/absint/PatternMatch.ml index 5d3e8be9a..872ed5075 100644 --- a/infer/src/absint/PatternMatch.ml +++ b/infer/src/absint/PatternMatch.ml @@ -162,7 +162,7 @@ let get_vararg_type_names tenv (call_node : Procdesc.Node.t) (ivar : Pvar.t) : s let initializes_array instrs = instrs |> Instrs.find_map ~f:(function - | Sil.Store (Exp.Lvar iv, _, Exp.Var t2, _) when Pvar.equal ivar iv -> + | Sil.Store {e1= Exp.Lvar iv; e2= Exp.Var t2} when Pvar.equal ivar iv -> Some t2 | _ -> None ) @@ -179,7 +179,7 @@ let get_vararg_type_names tenv (call_node : Procdesc.Node.t) (ivar : Pvar.t) : s let nvar_type_name nvar = instrs |> Instrs.find_map ~f:(function - | Sil.Load (nv, e, t, _) when Ident.equal nv nvar -> + | Sil.Load {id= nv; e; root_typ= t} when Ident.equal nv nvar -> Some (e, t) | _ -> None ) @@ -192,10 +192,10 @@ let get_vararg_type_names tenv (call_node : Procdesc.Node.t) (ivar : Pvar.t) : s let added_nvar array_nvar = instrs |> Instrs.find_map ~f:(function - | Sil.Store (Exp.Lindex (Exp.Var iv, _), _, Exp.Var nvar, _) + | Sil.Store {e1= Exp.Lindex (Exp.Var iv, _); e2= Exp.Var nvar} when Ident.equal iv array_nvar -> Some (nvar_type_name nvar) - | Sil.Store (Exp.Lindex (Exp.Var iv, _), _, Exp.Const c, _) + | Sil.Store {e1= Exp.Lindex (Exp.Var iv, _); e2= Exp.Const c} when Ident.equal iv array_nvar -> Some (Some (java_get_const_type_name c)) | _ -> @@ -205,7 +205,7 @@ let get_vararg_type_names tenv (call_node : Procdesc.Node.t) (ivar : Pvar.t) : s let array_nvar = instrs |> Instrs.find_map ~f:(function - | Sil.Load (nv, Exp.Lvar iv, _, _) when Pvar.equal iv ivar -> + | Sil.Load {id= nv; e= Exp.Lvar iv} when Pvar.equal iv ivar -> Some nv | _ -> None ) @@ -291,7 +291,7 @@ let method_is_initializer (tenv : Tenv.t) (proc_attributes : ProcAttributes.t) : (** Get the vararg values by looking for array assignments to the pvar. *) let java_get_vararg_values node pvar idenv = let values_of_instr acc = function - | Sil.Store (Exp.Lindex (array_exp, _), _, content_exp, _) + | Sil.Store {e1= Exp.Lindex (array_exp, _); e2= content_exp} when Exp.equal (Exp.Lvar pvar) (Idenv.expand_expr idenv array_exp) -> (* Each vararg argument is an assignment to a pvar denoting an array of objects. *) content_exp :: acc @@ -390,10 +390,10 @@ let lookup_attributes tenv proc_name = let get_fields_nullified procdesc = (* walk through the instructions and look for instance fields that are assigned to null *) let collect_nullified_flds (nullified_flds, this_ids) _ = function - | Sil.Store (Exp.Lfield (Exp.Var lhs, fld, _), _, rhs, _) + | Sil.Store {e1= Exp.Lfield (Exp.Var lhs, fld, _); e2= rhs} when Exp.is_null_literal rhs && Ident.Set.mem lhs this_ids -> (Typ.Fieldname.Set.add fld nullified_flds, this_ids) - | Sil.Load (id, rhs, _, _) when Exp.is_this rhs -> + | Sil.Load {id; e= rhs} when Exp.is_this rhs -> (nullified_flds, Ident.Set.add id this_ids) | _ -> (nullified_flds, this_ids) diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index d1cc9b714..e039dd656 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -91,8 +91,8 @@ let find_normal_variable_funcall (node : Procdesc.Node.t) (id : Ident.t) : (** Find a program variable assignment in the current node or predecessors. *) let find_program_variable_assignment node pvar : (Procdesc.Node.t * Ident.t) option = let find_instr node = function - | Sil.Store (Exp.Lvar pvar_, _, Exp.Var id, _) when Pvar.equal pvar pvar_ && Ident.is_normal id - -> + | Sil.Store {e1= Exp.Lvar pvar_; e2= Exp.Var id} + when Pvar.equal pvar pvar_ && Ident.is_normal id -> Some (node, id) | _ -> None @@ -123,7 +123,7 @@ let find_struct_by_value_assignment node pvar = (** Find a program variable assignment to id in the current node or predecessors. *) let find_ident_assignment node id : (Procdesc.Node.t * Exp.t) option = let find_instr node = function - | Sil.Load (id_, e, _, _) when Ident.equal id_ id -> + | Sil.Load {id= id_; e} when Ident.equal id_ id -> Some (node, e) | _ -> None @@ -136,7 +136,7 @@ let find_ident_assignment node id : (Procdesc.Node.t * Exp.t) option = let rec find_boolean_assignment node pvar true_branch : Procdesc.Node.t option = let find_instr n = let filter = function - | Sil.Store (Exp.Lvar pvar_, _, Exp.Const (Const.Cint i), _) when Pvar.equal pvar pvar_ -> + | Sil.Store {e1= Exp.Lvar pvar_; e2= Exp.Const (Const.Cint i)} when Pvar.equal pvar pvar_ -> IntLit.iszero i <> true_branch | _ -> false @@ -156,7 +156,7 @@ let rec find_boolean_assignment node pvar true_branch : Procdesc.Node.t option = and return the expression dereferenced to initialize [id] *) let rec find_normal_variable_load_ tenv (seen : Exp.Set.t) node id : DExp.t option = let find_declaration node = function - | Sil.Load (id0, e, _, _) when Ident.equal id id0 -> + | Sil.Load {id= id0; e} when Ident.equal id id0 -> if verbose then ( L.d_str "find_normal_variable_load defining " ; Sil.d_exp e ; @@ -184,7 +184,7 @@ let rec find_normal_variable_load_ tenv (seen : Exp.Set.t) node id : DExp.t opti List.map ~f:unNone args_dexpo in Some (DExp.Dretcall (fun_dexp, args_dexp, loc, call_flags)) - | Sil.Store (Exp.Lvar pvar, _, Exp.Var id0, _) + | Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Var id0} when Config.biabduction && Ident.equal id id0 && not (Pvar.is_frontend_tmp pvar) -> (* this case is a hack to make bucketing continue to work in the presence of copy propagation. previously, we would have code like: @@ -528,7 +528,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket = List.rev_filter ~f:(fun pvar -> not (Pvar.is_frontend_tmp pvar)) rev_nullify_pvars in value_str_from_pvars_vpath nullify_pvars_notmp vpath - | Some (Sil.Store (lexp, _, _, _)) when is_none vpath -> ( + | Some (Sil.Store {e1= lexp}) when is_none vpath -> ( if verbose then ( L.d_str "explain_leak: current instruction Set for " ; Sil.d_exp lexp ; @@ -940,13 +940,13 @@ let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = fa prop loc = let find_exp_dereferenced () = match State.get_instr () with - | Some (Sil.Store (e, _, _, _)) -> + | Some (Sil.Store {e1= e}) -> if verbose then ( L.d_str "explain_dereference Sil.Store " ; Sil.d_exp e ; L.d_ln () ) ; Some e - | Some (Sil.Load (_, e, _, _)) -> + | Some (Sil.Load {e}) -> if verbose then ( L.d_str "explain_dereference Binop.Leteref " ; Sil.d_exp e ; diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index ad845c63d..674d073aa 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -91,7 +91,7 @@ module NullifyTransferFunctions = struct let exec_instr ((active_defs, to_nullify) as astate) extras node instr = let astate' = match instr with - | Sil.Load (lhs_id, _, _, _) -> + | Sil.Load {id= lhs_id} -> (VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify) | Sil.Call ((id, _), _, actuals, _, {CallFlags.cf_assign_last_arg}) -> let active_defs = VarDomain.add (Var.of_id id) active_defs in @@ -105,7 +105,7 @@ module NullifyTransferFunctions = struct else active_defs in (active_defs, to_nullify) - | Sil.Store (Exp.Lvar lhs_pvar, _, _, _) -> + | Sil.Store {e1= Exp.Lvar lhs_pvar} -> (VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify) | Sil.Metadata (VariableLifetimeBegins (pvar, _, _)) -> (VarDomain.add (Var.of_pvar pvar) active_defs, to_nullify) diff --git a/infer/src/biabduction/Buckets.ml b/infer/src/biabduction/Buckets.ml index e5cc93c73..dda8ae668 100644 --- a/infer/src/biabduction/Buckets.ml +++ b/infer/src/biabduction/Buckets.ml @@ -75,7 +75,7 @@ let check_access access_opt de_opt = List.exists ~f:(fun (formal_name, _) -> Mangled.equal name formal_name) formals in let process_formal_letref = function - | Sil.Load (id, Exp.Lvar pvar, _, _) -> + | Sil.Load {id; e= Exp.Lvar pvar} -> let is_java_this = Language.curr_language_is Java && Pvar.is_this pvar in if (not is_java_this) && is_formal pvar then Some id else None | _ -> @@ -113,7 +113,7 @@ let check_access access_opt de_opt = let filter = function | Sil.Call _ -> true - | Sil.Store (_, _, e, _) -> + | Sil.Store {e2= e} -> exp_is_null e | _ -> false diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index fb7c46dc1..a9f57f61a 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -19,7 +19,7 @@ let execute___builtin_va_arg {Builtin.summary; tenv; prop_; path; args; loc; exe Builtin.ret_typ = match args with | [(lexp3, typ3)] -> - let instr' = Sil.Store (lexp3, typ3, Exp.zero, loc) in + let instr' = Sil.Store {e1= lexp3; root_typ= typ3; e2= Exp.zero; loc} in SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton instr') [(prop_, path)] | _ -> @@ -626,7 +626,8 @@ let execute___cxx_typeid ({Builtin.summary; tenv; prop_; args; loc; exe_env} as in let typ_string = Typ.to_string typ in let set_instr = - Sil.Store (field_exp, Typ.mk Tvoid, Exp.Const (Const.Cstr typ_string), loc) + Sil.Store + {e1= field_exp; root_typ= Typ.mk Tvoid; e2= Exp.Const (Const.Cstr typ_string); loc} in SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) res | _ -> @@ -763,7 +764,11 @@ let execute___infer_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_env raise (Exceptions.Wrong_argument_number __POS__) in let set_instr = - Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) + Sil.Store + { e1= Exp.Lvar Sil.custom_error + ; root_typ= Typ.mk Tvoid + ; e2= Exp.Const (Const.Cstr error_str) + ; loc } in SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) [(prop_, path)] @@ -779,7 +784,11 @@ let execute___assert_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_en raise (Exceptions.Wrong_argument_number __POS__) in let set_instr = - Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) + Sil.Store + { e1= Exp.Lvar Sil.custom_error + ; root_typ= Typ.mk Tvoid + ; e2= Exp.Const (Const.Cstr error_str) + ; loc } in SymExec.instrs ~mask_errors:true exe_env tenv summary (Instrs.singleton set_instr) [(prop_, path)] diff --git a/infer/src/biabduction/State.ml b/infer/src/biabduction/State.ml index 7653c8b6e..15cd5df14 100644 --- a/infer/src/biabduction/State.ml +++ b/infer/src/biabduction/State.ml @@ -104,7 +104,7 @@ let get_loc () = (** normalize the list of instructions by renaming let-bound ids *) let instrs_normalize instrs = let bound_ids = - let do_instr = function Sil.Load (id, _, _, _) -> Some id | _ -> None in + let do_instr = function Sil.Load {id} -> Some id | _ -> None in IContainer.rev_filter_map_to_list ~fold:Instrs.fold ~f:do_instr instrs in let subst = diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 4e40cfb3b..e626608a6 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1267,9 +1267,9 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t ; exe_env } in match instr with - | Sil.Load (id, rhs_exp, typ, loc) -> + | Sil.Load {id; e= rhs_exp; root_typ= typ; loc} -> execute_load current_pname current_pdesc tenv id rhs_exp typ loc prop_ |> ret_old_path - | Sil.Store (lhs_exp, typ, rhs_exp, loc) -> + | Sil.Store {e1= lhs_exp; root_typ= typ; e2= rhs_exp; loc} -> execute_store current_pname current_pdesc tenv lhs_exp typ rhs_exp loc prop_ |> ret_old_path | Sil.Prune (cond, loc, true_branch, ik) -> let prop__ = Attribute.nullify_exp_with_objc_null tenv prop_ cond in @@ -1763,7 +1763,7 @@ and check_variadic_sentinel ?(fails_on_nil = false) n_formals (sentinel, null_po let check_allocated result ((lexp, typ), i) = (* simulate a Load for [lexp] *) let tmp_id_deref = Ident.create_fresh Ident.kprimed in - let load_instr = Sil.Load (tmp_id_deref, lexp, typ, loc) in + let load_instr = Sil.Load {id= tmp_id_deref; e= lexp; root_typ= typ; loc} in try instrs exe_env tenv summary (Instrs.singleton load_instr) result with e when SymOp.exn_not_failure e -> IExn.reraise_if e ~f:(fun () -> fails_on_nil) ; diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index 9a1ed8a8f..3208e048e 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -180,10 +180,10 @@ module TransferFunctions = struct fun mem {summary; tenv; extras= {get_proc_summary_and_formals; oenv= {integer_type_widths}}} node instr -> match instr with - | Load (id, _, _, _) when Ident.is_none id -> + | Load {id} when Ident.is_none id -> mem - | Load (id, Exp.Lvar pvar, _, location) when Pvar.is_compile_constant pvar || Pvar.is_ice pvar - -> ( + | Load {id; e= Exp.Lvar pvar; loc= location} + when Pvar.is_compile_constant pvar || Pvar.is_ice pvar -> ( match Pvar.get_initializer_pname pvar with | Some callee_pname -> ( match get_proc_summary_and_formals callee_pname with @@ -198,10 +198,10 @@ module TransferFunctions = struct L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a" (Pvar.pp Pp.text) pvar ; Dom.Mem.add_unknown id ~location mem ) - | Load (id, exp, typ, _) -> + | Load {id; e= exp; root_typ= typ} -> let represents_multiple_values = is_array_access_exp exp in BoUtils.Exec.load_locs ~represents_multiple_values id typ (Sem.eval_locs exp mem) mem - | Store (exp1, _, Const (Const.Cstr s), location) -> + | Store {e1= exp1; e2= Const (Const.Cstr s); loc= location} -> let locs = Sem.eval_locs exp1 mem in let model_env = let pname = Summary.get_proc_name summary in @@ -210,7 +210,7 @@ module TransferFunctions = struct in let do_alloc = not (Sem.is_stack_exp exp1 mem) in BoUtils.Exec.decl_string model_env ~do_alloc locs s mem - | Store (exp1, typ, exp2, location) -> + | Store {e1= exp1; root_typ= typ; e2= exp2; loc= location} -> let locs = Sem.eval_locs exp1 mem in let v = Sem.eval integer_type_widths exp2 mem |> Dom.Val.add_assign_trace_elem location locs diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index cd5f43251..440f520d7 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -284,11 +284,11 @@ let check_instr : -> PO.ConditionSet.checked_t = fun get_proc_summary pdesc tenv integer_type_widths node instr mem cond_set -> match instr with - | Sil.Load (_, exp, _, location) -> + | Sil.Load {e= exp; loc= location} -> cond_set |> check_expr_for_array_access integer_type_widths exp location mem |> check_expr_for_integer_overflow integer_type_widths exp location mem - | Sil.Store (lexp, _, rexp, location) -> + | Sil.Store {e1= lexp; e2= rexp; loc= location} -> cond_set |> check_expr_for_array_access integer_type_widths lexp location mem |> check_expr_for_integer_overflow integer_type_widths lexp location mem diff --git a/infer/src/checkers/NullabilityPreanalysis.ml b/infer/src/checkers/NullabilityPreanalysis.ml index 3010bd572..9d1972923 100644 --- a/infer/src/checkers/NullabilityPreanalysis.ml +++ b/infer/src/checkers/NullabilityPreanalysis.ml @@ -40,10 +40,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let exec_instr astate (proc_data : Exp.t Ident.Hash.t ProcData.t) _ instr = match instr with - | Sil.Load (id, exp, _, _) -> + | Sil.Load {id; e= exp} -> Ident.Hash.add proc_data.extras id exp ; astate - | Sil.Store (Exp.Lfield (Exp.Var lhs_id, name, typ), exp_typ, rhs, _) -> ( + | Sil.Store {e1= Exp.Lfield (Exp.Var lhs_id, name, typ); root_typ= exp_typ; e2= rhs} -> ( match exp_typ.Typ.desc with (* block field of a ObjC class *) | Typ.Tptr ({desc= Tfun _}, _) diff --git a/infer/src/checkers/Siof.ml b/infer/src/checkers/Siof.ml index f0c111bd3..87b7cd02d 100644 --- a/infer/src/checkers/Siof.ml +++ b/infer/src/checkers/Siof.ml @@ -139,7 +139,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let exec_instr astate {ProcData.summary} _ (instr : Sil.instr) = match instr with - | Store (Lvar global, Typ.{desc= Tptr _}, Lvar _, loc) + | Store {e1= Lvar global; root_typ= Typ.{desc= Tptr _}; e2= Lvar _; loc} when (Option.equal Typ.Procname.equal) (Pvar.get_initializer_pname global) (Some (Summary.get_proc_name summary)) -> @@ -151,8 +151,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct The heuristic is limited to the case where the access sets the global being initialized in the current variable initializer function. *) add_globals astate loc (GlobalVarSet.singleton global) - | Load (_, exp, _, loc) (* dereference -> add all the dangerous variables *) - | Store (_, _, exp, loc) (* except in the case above, consider all reads as dangerous *) + | Load {e= exp; loc} (* dereference -> add all the dangerous variables *) + | Store {e2= exp; loc} (* except in the case above, consider all reads as dangerous *) | Prune (exp, loc, _, _) -> get_globals summary exp |> add_globals astate loc | Call (_, Const (Cfun callee_pname), _, _, _) when is_whitelisted callee_pname -> diff --git a/infer/src/checkers/addressTaken.ml b/infer/src/checkers/addressTaken.ml index 9e4d3d3d4..fe4b102e7 100644 --- a/infer/src/checkers/addressTaken.ml +++ b/infer/src/checkers/addressTaken.ml @@ -36,7 +36,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let exec_instr astate _ _ = function - | Sil.Store (_, {desc= Tptr _}, rhs_exp, _) -> + | Sil.Store {root_typ= {desc= Tptr _}; e2= rhs_exp} -> add_address_taken_pvars rhs_exp astate | Sil.Call (_, _, actuals, _, _) -> let add_actual_by_ref astate_acc = function diff --git a/infer/src/checkers/classLoads.ml b/infer/src/checkers/classLoads.ml index 7bdac28ce..6b24b5c10 100644 --- a/infer/src/checkers/classLoads.ml +++ b/infer/src/checkers/classLoads.ml @@ -99,11 +99,11 @@ let exec_instr summary tenv astate _ (instr : Sil.instr) = match instr with | Call (_, Const (Cfun callee), args, loc, _) -> exec_call summary tenv callee args loc astate - | Load (_, exp, _, loc) | Prune (exp, loc, _, _) -> + | Load {e= exp; loc} | Prune (exp, loc, _, _) -> (* NB the java frontend seems to always translate complex guards into a sequence of instructions plus a prune on logical vars only. So the below is only for completeness. *) add_loads_of_exp summary tenv loc exp astate - | Store (e1, _, e2, loc) -> + | Store {e1; e2; loc} -> add_loads_of_exp summary tenv loc e1 astate |> add_loads_of_exp summary tenv loc e2 | _ -> astate diff --git a/infer/src/checkers/control.ml b/infer/src/checkers/control.ml index 7b22b7f37..78aa52e36 100644 --- a/infer/src/checkers/control.ml +++ b/infer/src/checkers/control.ml @@ -65,7 +65,7 @@ module TransferFunctionsControlDeps (CFG : ProcCfg.S) = struct let find_vars_in_decl id loop_head _ = function - | Sil.Load (lhs_id, exp, _, _) when Ident.equal lhs_id id -> + | Sil.Load {id= lhs_id; e= exp} when Ident.equal lhs_id id -> collect_vars_in_exp exp loop_head |> Option.some | Sil.Call ((lhs_id, _), _, arg_list, _, _) when Ident.equal lhs_id id -> List.fold_left arg_list ~init:ControlDepSet.empty ~f:(fun deps (exp, _) -> diff --git a/infer/src/checkers/cost.ml b/infer/src/checkers/cost.ml index 23d77ba43..02c52b12a 100644 --- a/infer/src/checkers/cost.ml +++ b/infer/src/checkers/cost.ml @@ -576,7 +576,7 @@ module InstrBasicCost = struct if is_allocation_function callee_pname then CostDomain.plus CostDomain.unit_cost_allocation operation_cost else operation_cost - | Sil.Load (lhs_id, _, _, _) when Ident.is_none lhs_id -> + | Sil.Load {id= lhs_id} when Ident.is_none lhs_id -> (* dummy deref inserted by frontend--don't count as a step. In JDK 11, dummy deref disappears and causes cost differences otherwise. *) diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index 79392d65d..a9c500fa0 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -52,7 +52,7 @@ let node_throws pdesc node (proc_throws : Typ.Procname.t -> throws) : throws = Pvar.equal pvar ret_pvar in match instr with - | Sil.Store (Exp.Lvar pvar, _, Exp.Exn _, _) when is_return pvar -> + | Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Exn _} when is_return pvar -> (* assignment to return variable is an artifact of a throw instruction *) Throws | Sil.Call (_, Exp.Const (Const.Cfun callee_pn), _, _, _) diff --git a/infer/src/checkers/functionPointers.ml b/infer/src/checkers/functionPointers.ml index 05ebde1b8..299f105b8 100644 --- a/infer/src/checkers/functionPointers.ml +++ b/infer/src/checkers/functionPointers.ml @@ -24,15 +24,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type extras = ProcData.no_extras let exec_instr astate _ _ = function - | Sil.Load (lhs_id, _, _, _) when Ident.is_none lhs_id -> + | Sil.Load {id= lhs_id} when Ident.is_none lhs_id -> astate - | Sil.Load (lhs_id, Exp.Lvar rhs_pvar, Typ.{desc= Tptr ({desc= Tfun _}, _)}, _) -> + | Sil.Load {id= lhs_id; e= Exp.Lvar rhs_pvar; root_typ= Typ.{desc= Tptr ({desc= Tfun _}, _)}} + -> let fun_ptr = try Domain.find (Pvar.to_string rhs_pvar) astate with Caml.Not_found -> ProcnameSet.empty in Domain.add (Ident.to_string lhs_id) fun_ptr astate - | Sil.Store (Lvar lhs_pvar, _, Exp.Const (Const.Cfun pn), _) -> + | Sil.Store {e1= Lvar lhs_pvar; e2= Exp.Const (Const.Cfun pn)} -> (* strong update *) Domain.add (Pvar.to_string lhs_pvar) (ProcnameSet.singleton pn) astate | Sil.Load _ | Store _ | Call _ | Prune _ | Metadata _ -> diff --git a/infer/src/checkers/idenv.ml b/infer/src/checkers/idenv.ml index 9850f396b..701a95fbf 100644 --- a/infer/src/checkers/idenv.ml +++ b/infer/src/checkers/idenv.ml @@ -14,7 +14,7 @@ type t = Exp.t Ident.Hash.t Lazy.t let create_ proc_desc = let map = Ident.Hash.create 1 in - let do_instr _ = function Sil.Load (id, e, _, _) -> Ident.Hash.add map id e | _ -> () in + let do_instr _ = function Sil.Load {id; e} -> Ident.Hash.add map id e | _ -> () in Procdesc.iter_instrs do_instr proc_desc ; map diff --git a/infer/src/checkers/inefficientKeysetIterator.ml b/infer/src/checkers/inefficientKeysetIterator.ml index b0b1931a7..ae5415819 100644 --- a/infer/src/checkers/inefficientKeysetIterator.ml +++ b/infer/src/checkers/inefficientKeysetIterator.ml @@ -10,7 +10,7 @@ module CFG = ProcCfg.Normal module LoopNodes = AbstractDomain.FiniteSet (Procdesc.Node) let find_loaded_pvar id = function - | Sil.Load (lhs_id, Exp.Lvar rhs_pvar, _, _) when Ident.equal lhs_id id -> + | Sil.Load {id= lhs_id; e= Exp.Lvar rhs_pvar} when Ident.equal lhs_id id -> Some rhs_pvar | _ -> None @@ -38,7 +38,7 @@ let find_first_arg_pvar node ~fun_name ~class_name_f = if Instrs.count instrs >= 4 then let instr_arr = Instrs.get_underlying_not_reversed instrs in match instr_arr.(3) with - | Sil.Store (Exp.Lvar _, _, Exp.Var rhs_id, _) -> + | Sil.Store {e1= Exp.Lvar _; e2= Exp.Var rhs_id} -> find_first_arg_id ~fun_name ~class_name_f ~lhs_f:(Ident.equal rhs_id) instr_arr.(2) |> Option.bind ~f:(fun arg_id -> find_loaded_pvar arg_id instr_arr.(0)) | _ -> diff --git a/infer/src/checkers/liveness.ml b/infer/src/checkers/liveness.ml index 8e3db7112..c64b2b6b7 100644 --- a/infer/src/checkers/liveness.ml +++ b/infer/src/checkers/liveness.ml @@ -124,18 +124,18 @@ module TransferFunctions (LConfig : LivenessConfig) (CFG : ProcCfg.S) = struct let exec_instr astate _ _ = function - | Sil.Load (lhs_id, _, _, _) when Ident.is_none lhs_id -> + | Sil.Load {id= lhs_id} when Ident.is_none lhs_id -> (* dummy deref inserted by frontend--don't count as a read *) astate - | Sil.Load (lhs_id, rhs_exp, _, _) -> + | Sil.Load {id= lhs_id; e= rhs_exp} -> Domain.remove (Var.of_id lhs_id) astate |> exp_add_live rhs_exp - | Sil.Store (Lvar lhs_pvar, _, rhs_exp, _) -> + | Sil.Store {e1= Lvar lhs_pvar; e2= rhs_exp} -> let astate' = if is_always_in_scope lhs_pvar then astate (* never kill globals *) else Domain.remove (Var.of_pvar lhs_pvar) astate in exp_add_live rhs_exp astate' - | Sil.Store (lhs_exp, _, rhs_exp, _) -> + | Sil.Store {e1= lhs_exp; e2= rhs_exp} -> exp_add_live lhs_exp astate |> exp_add_live rhs_exp | Sil.Prune (exp, _, _, _) -> exp_add_live exp astate @@ -263,7 +263,7 @@ let checker {Callbacks.exe_env; summary} : Summary.t = Reporting.log_error summary ~loc ~ltr IssueType.dead_store message in let report_dead_store live_vars captured_by_ref_vars = function - | Sil.Store (Lvar pvar, typ, rhs_exp, loc) + | Sil.Store {e1= Lvar pvar; root_typ= typ; e2= rhs_exp; loc} when should_report pvar typ live_vars captured_by_ref_vars && not (is_sentinel_exp rhs_exp) -> log_report pvar typ loc diff --git a/infer/src/checkers/loopInvariant.ml b/infer/src/checkers/loopInvariant.ml index 4cf7a2fee..be279a3a3 100644 --- a/infer/src/checkers/loopInvariant.ml +++ b/infer/src/checkers/loopInvariant.ml @@ -52,9 +52,9 @@ let is_def_unique_and_satisfy tenv var (loop_nodes : LoopNodes.t) ~is_pure_by_de | IContainer.Singleton node -> Procdesc.Node.get_instrs node |> Instrs.exists ~f:(function - | Sil.Load (id, exp_rhs, _, _) when equals_var id && is_exp_invariant exp_rhs -> + | Sil.Load {id; e= exp_rhs} when equals_var id && is_exp_invariant exp_rhs -> true - | Sil.Store (exp_lhs, _, exp_rhs, _) + | Sil.Store {e1= exp_lhs; e2= exp_rhs} when Exp.equal exp_lhs (Var.to_exp var) && is_exp_invariant exp_rhs -> true | Sil.Call ((id, _), Const (Cfun callee_pname), args, _, _) when equals_var id -> @@ -82,12 +82,12 @@ let get_vars_in_loop loop_nodes = |> Instrs.fold ~f:(fun acc instr -> match instr with - | Sil.Load (id, exp_rhs, _, _) -> + | Sil.Load {id; e= exp_rhs} -> Var.get_all_vars_in_exp exp_rhs |> Sequence.fold ~init:(VarsInLoop.add (Var.of_id id) acc) ~f:(fun acc var -> VarsInLoop.add var acc) - | Sil.Store (exp_lhs, _, exp_rhs, _) -> + | Sil.Store {e1= exp_lhs; e2= exp_rhs} -> Var.get_all_vars_in_exp exp_rhs |> Sequence.append (Var.get_all_vars_in_exp exp_lhs) |> Sequence.fold ~init:acc ~f:(fun acc var -> VarsInLoop.add var acc) @@ -133,10 +133,10 @@ let get_ptr_vars_in_defn_path node loop_head var = Procdesc.Node.get_instrs node |> Instrs.fold ~init:InvalidatedVars.empty ~f:(fun acc instr -> match instr with - | Sil.Load (id, exp_rhs, typ, _) + | Sil.Load {id; e= exp_rhs; root_typ= typ} when Var.equal var (Var.of_id id) && is_non_primitive typ -> invalidate_exp exp_rhs acc - | Sil.Store (Exp.Lvar pvar, typ, exp_rhs, _) + | Sil.Store {e1= Exp.Lvar pvar; root_typ= typ; e2= exp_rhs} when Var.equal var (Var.of_pvar pvar) && is_non_primitive typ -> invalidate_exp exp_rhs acc | _ -> diff --git a/infer/src/checkers/printfArgs.ml b/infer/src/checkers/printfArgs.ml index 98aa4505f..d9fe222f3 100644 --- a/infer/src/checkers/printfArgs.ml +++ b/infer/src/checkers/printfArgs.ml @@ -127,7 +127,7 @@ let check_printf_args_ok tenv (node : Procdesc.Node.t) (instr : Sil.instr) match nvar with | Exp.Var nid -> Instrs.find_map instrs ~f:(function - | Sil.Load (id, Exp.Lvar iv, _, _) when Ident.equal id nid -> + | Sil.Load {id; e= Exp.Lvar iv} when Ident.equal id nid -> Some iv | _ -> None ) diff --git a/infer/src/checkers/reachingDefs.ml b/infer/src/checkers/reachingDefs.ml index b351585d0..a5b52999c 100644 --- a/infer/src/checkers/reachingDefs.ml +++ b/infer/src/checkers/reachingDefs.ml @@ -37,16 +37,16 @@ module TransferFunctionsReachingDefs (CFG : ProcCfg.S) = struct astate in match instr with - | Sil.Load (lhs_id, _, _, _) when Ident.is_none lhs_id -> + | Sil.Load {id= lhs_id} when Ident.is_none lhs_id -> (* dummy deref inserted by frontend--don't count as a read *) astate - | Sil.Load (id, _, _, _) | Sil.Call ((id, _), _, _, _, _) -> + | Sil.Load {id} | Sil.Call ((id, _), _, _, _, _) -> strong_update_def astate (Var.of_id id) (* only strong update for assigning to a pvar *) - | Sil.Store (Lvar pvar, _, _, _) -> + | Sil.Store {e1= Lvar pvar} -> strong_update_def astate (Var.of_pvar pvar) (* by default use weak update *) - | Sil.Store (exp_lhs, _, _, _) -> + | Sil.Store {e1= exp_lhs} -> let vars = Var.get_all_vars_in_exp exp_lhs in Sequence.fold ~init:astate ~f:weak_update_def vars | _ -> diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index 5c62d7a42..12714c558 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -40,7 +40,8 @@ let compound_assignment_binary_operation_instruction boi_kind (e1, t1) typ e2 lo Binop.BXor in let id = Ident.create_fresh Ident.knormal in - [Sil.Load (id, e1, typ, loc); Sil.Store (e1, typ, Exp.BinOp (bop, Exp.Var id, e2), loc)] + [ Sil.Load {id; e= e1; root_typ= typ; loc} + ; Sil.Store {e1; root_typ= typ; e2= Exp.BinOp (bop, Exp.Var id, e2); loc} ] in (e1, instrs) @@ -104,7 +105,7 @@ let binary_operation_instruction source_range boi ((e1, t1) as e1_with_typ) typ | `LOr -> (binop_exp Binop.LOr, []) | `Assign -> - (e1, [Sil.Store (e1, typ, e2, loc)]) + (e1, [Sil.Store {e1; root_typ= typ; e2; loc}]) | `Cmp -> CFrontend_errors.unimplemented __POS__ source_range "C++20 spaceship operator <=>" (* C++20 spaceship operator <=>, TODO *) @@ -128,30 +129,30 @@ let unary_operation_instruction translation_unit_context uoi e typ loc = match uoi.Clang_ast_t.uoi_kind with | `PostInc -> let id = Ident.create_fresh Ident.knormal in - let instr1 = Sil.Load (id, e, typ, loc) in + let instr1 = Sil.Load {id; e; root_typ= typ; loc} in let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in - (Exp.Var id, [instr1; Sil.Store (e, typ, e_plus_1, loc)]) + (Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_plus_1; loc}]) | `PreInc -> let id = Ident.create_fresh Ident.knormal in - let instr1 = Sil.Load (id, e, typ, loc) in + let instr1 = Sil.Load {id; e; root_typ= typ; loc} in let bop = if Typ.is_pointer typ then Binop.PlusPI else Binop.PlusA (Typ.get_ikind_opt typ) in let e_plus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in let exp = if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_plus_1 in - (exp, [instr1; Sil.Store (e, typ, e_plus_1, loc)]) + (exp, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_plus_1; loc}]) | `PostDec -> let id = Ident.create_fresh Ident.knormal in - let instr1 = Sil.Load (id, e, typ, loc) in + let instr1 = Sil.Load {id; e; root_typ= typ; loc} in let bop = if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ) in let e_minus_1 = Exp.BinOp (bop, Exp.Var id, Exp.Const (Const.Cint IntLit.one)) in - (Exp.Var id, [instr1; Sil.Store (e, typ, e_minus_1, loc)]) + (Exp.Var id, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_minus_1; loc}]) | `PreDec -> let id = Ident.create_fresh Ident.knormal in - let instr1 = Sil.Load (id, e, typ, loc) in + let instr1 = Sil.Load {id; e; root_typ= typ; loc} in let bop = if Typ.is_pointer typ then Binop.MinusPI else Binop.MinusA (Typ.get_ikind_opt typ) in @@ -159,7 +160,7 @@ let unary_operation_instruction translation_unit_context uoi e typ loc = let exp = if CGeneral_utils.is_cpp_translation translation_unit_context then e else e_minus_1 in - (exp, [instr1; Sil.Store (e, typ, e_minus_1, loc)]) + (exp, [instr1; Sil.Store {e1= e; root_typ= typ; e2= e_minus_1; loc}]) | `Not -> (un_exp Unop.BNot, []) | `Minus -> diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 59c14e982..ef303e26e 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -221,7 +221,8 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let pvar = Pvar.mk formal procname in let id = Ident.create_fresh Ident.knormal in ( (Exp.Var id, typ) :: forwarded_params - , Sil.Load (id, Exp.Lvar pvar, typ, sil_loc) :: forwarded_init_exps ) ) + , Sil.Load {id; e= Exp.Lvar pvar; root_typ= typ; loc= sil_loc} :: forwarded_init_exps ) + ) let create_call_instr trans_state (return_type : Typ.t) function_sil params_sil sil_loc @@ -290,7 +291,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (** Given a captured var, return the instruction to assign it to a temp *) let assign_captured_var loc (cvar, typ) = let id = Ident.create_fresh Ident.knormal in - let instr = Sil.Load (id, Exp.Lvar cvar, typ, loc) in + let instr = Sil.Load {id; e= Exp.Lvar cvar; root_typ= typ; loc} in ((Exp.Var id, cvar, typ), instr) @@ -422,7 +423,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s |> mk_trans_result exp_typ | Tint _ | Tfloat _ | Tptr _ -> let zero_exp = Exp.zero_of_type_exn typ in - let instrs = [Sil.Store (exp, typ, zero_exp, sil_loc)] in + let instrs = [Sil.Store {e1= exp; root_typ= typ; e2= zero_exp; loc= sil_loc}] in mk_trans_result (exp, typ) {empty_control with instrs} | Tfun _ | Tvoid | Tarray _ | TVar _ -> CFrontend_errors.unimplemented __POS__ stmt_info.Clang_ast_t.si_source_range @@ -554,7 +555,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let exp, deref_instrs = if should_add_deref then let id = Ident.create_fresh Ident.knormal in - let deref_instr = Sil.Load (id, field_exp, field_typ, sil_loc) in + let deref_instr = Sil.Load {id; e= field_exp; root_typ= field_typ; loc= sil_loc} in (Exp.Var id, [deref_instr]) else (field_exp, []) in @@ -604,7 +605,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s calling a method with null *) when decl_kind <> `CXXConstructor -> let no_id = Ident.create_none () in - let extra_instrs = [Sil.Load (no_id, exp, typ, sil_loc)] in + let extra_instrs = [Sil.Load {id= no_id; e= exp; root_typ= typ; loc= sil_loc}] in (return, extra_instrs) | MemberOrIvar {return= (_, {Typ.desc= Tptr _}) as return} -> (return, []) @@ -972,7 +973,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (* assignment. *) (* As no node is created here ids are passed to the parent *) let id = Ident.create_fresh Ident.knormal in - let res_instr = Sil.Load (id, exp1, typ1, sil_loc) in + let res_instr = Sil.Load {id; e= exp1; root_typ= typ1; loc= sil_loc} in ([res_instr], Exp.Var id) else ([], exp_op) in @@ -1503,7 +1504,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s e' in let temp_var = Exp.Lvar pvar in - let set_temp_var = [Sil.Store (temp_var, var_typ, e', sil_loc)] in + let set_temp_var = [Sil.Store {e1= temp_var; root_typ= var_typ; e2= e'; loc= sil_loc}] in let temp_return = (temp_var, var_typ) in let tmp_var_res_trans = mk_trans_result temp_return {empty_control with instrs= set_temp_var} @@ -1552,7 +1553,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s do_branch false exp2 var_typ res_trans_cond.control.leaf_nodes join_node pvar in let id = Ident.create_fresh Ident.knormal in - let instrs = [Sil.Load (id, Exp.Lvar pvar, var_typ, sil_loc)] in + let instrs = [Sil.Load {id; e= Exp.Lvar pvar; root_typ= var_typ; loc= sil_loc}] in mk_trans_result (Exp.Var id, typ) { root_nodes= res_trans_cond.control.root_nodes ; leaf_nodes= [join_node] @@ -2320,7 +2321,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s then None else let sil_e1', ie_typ = res_trans_ie.return in - Some {empty_control with instrs= [Sil.Store (var_exp, ie_typ, sil_e1', sil_loc)]} + Some + { empty_control with + instrs= [Sil.Store {e1= var_exp; root_typ= ie_typ; e2= sil_e1'; loc= sil_loc}] } in let pre_init_opt = match var_exp with @@ -2612,7 +2615,9 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let name = CFrontend_config.return_param in let pvar = Pvar.mk (Mangled.from_string name) procname in let id = Ident.create_fresh Ident.knormal in - let instr = Sil.Load (id, Exp.Lvar pvar, ret_param_typ, sil_loc) in + let instr = + Sil.Load {id; e= Exp.Lvar pvar; root_typ= ret_param_typ; loc= sil_loc} + in let ret_typ = match ret_param_typ.desc with Typ.Tptr (t, _) -> t | _ -> assert false in @@ -2628,7 +2633,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s if List.exists ~f:(Exp.equal ret_exp) res_trans_stmt.control.initd_exps then [] else let sil_expr, _ = res_trans_stmt.return in - [Sil.Store (ret_exp, ret_type, sil_expr, sil_loc)] + [Sil.Store {e1= ret_exp; root_typ= ret_type; e2= sil_expr; loc= sil_loc}] in let instrs = var_instrs @ res_trans_stmt.control.instrs @ ret_instrs in let ret_node = mk_ret_node instrs in diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index e2b5869a9..99cc82a92 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -401,7 +401,7 @@ let create_call_to_free_cf sil_loc exp typ = let dereference_var_sil (exp, typ) sil_loc = let id = Ident.create_fresh Ident.knormal in - let sil_instr = Sil.Load (id, exp, typ, sil_loc) in + let sil_instr = Sil.Load {id; e= exp; root_typ= typ; loc= sil_loc} in ([sil_instr], Exp.Var id) @@ -547,7 +547,8 @@ let define_condition_side_effects ((e_cond_exp, e_cond_typ) as e_cond) instrs_co match e_cond_exp with | Exp.Lvar pvar -> let id = Ident.create_fresh Ident.knormal in - ((Exp.Var id, e_cond_typ), [Sil.Load (id, Exp.Lvar pvar, e_cond_typ, sil_loc)]) + ( (Exp.Var id, e_cond_typ) + , [Sil.Load {id; e= Exp.Lvar pvar; root_typ= e_cond_typ; loc= sil_loc}] ) | _ -> (e_cond, instrs_cond) @@ -580,7 +581,7 @@ module Self = struct in let e = Exp.Lvar (Pvar.mk (Mangled.from_string CFrontend_config.self) procname) in let id = Ident.create_fresh Ident.knormal in - (t', Exp.Var id, [Sil.Load (id, e, t', loc)]) + (t', Exp.Var id, [Sil.Load {id; e; root_typ= t'; loc}]) in Some (mk_trans_result (self_expr, typ) {empty_control with instrs}) else None diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index 1c3aa5823..81d41fac5 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -463,7 +463,7 @@ let builtin_get_array_length = Exp.Const (Const.Cfun BuiltinDecl.__get_array_len let create_sil_deref exp typ loc = let no_id = Ident.create_none () in - Sil.Load (no_id, exp, typ, loc) + Sil.Load {id= no_id; e= exp; root_typ= typ; loc} (** translate an expression used as an r-value *) @@ -474,7 +474,7 @@ let rec expression (context : JContext.t) pc expr = let type_of_expr = JTransType.expr_type context expr in let trans_var pvar = let id = Ident.create_fresh Ident.knormal in - let sil_instr = Sil.Load (id, Exp.Lvar pvar, type_of_expr, loc) in + let sil_instr = Sil.Load {id; e= Exp.Lvar pvar; root_typ= type_of_expr; loc} in ([sil_instr], Exp.Var id, type_of_expr) in match expr with @@ -548,7 +548,9 @@ let rec expression (context : JContext.t) pc expr = let array_typ = Typ.mk_array type_of_expr in let deref_array_instr = create_sil_deref sil_ex1 array_typ loc in let id = Ident.create_fresh Ident.knormal in - let load_instr = Sil.Load (id, Exp.Lindex (sil_ex1, sil_ex2), type_of_expr, loc) in + let load_instr = + Sil.Load {id; e= Exp.Lindex (sil_ex1, sil_ex2); root_typ= type_of_expr; loc} + in let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [load_instr] in (instrs, Exp.Var id, type_of_expr) | other_binop -> @@ -561,7 +563,7 @@ let rec expression (context : JContext.t) pc expr = let sil_type = JTransType.get_class_type_no_pointer program tenv cn in let sil_expr = Exp.Lfield (sil_expr, field_name, sil_type) in let tmp_id = Ident.create_fresh Ident.knormal in - let lderef_instr = Sil.Load (tmp_id, sil_expr, sil_type, loc) in + let lderef_instr = Sil.Load {id= tmp_id; e= sil_expr; root_typ= sil_type; loc} in (instrs @ [lderef_instr], Exp.Var tmp_id, type_of_expr) | JBir.StaticField (cn, fs) -> let class_exp = @@ -579,7 +581,7 @@ let rec expression (context : JContext.t) pc expr = else let sil_expr = Exp.Lfield (sil_expr, field_name, sil_type) in let tmp_id = Ident.create_fresh Ident.knormal in - let lderef_instr = Sil.Load (tmp_id, sil_expr, sil_type, loc) in + let lderef_instr = Sil.Load {id= tmp_id; e= sil_expr; root_typ= sil_type; loc} in (instrs @ [lderef_instr], Exp.Var tmp_id, type_of_expr) @@ -667,7 +669,9 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex let call_ret_instrs sil_var = let ret_id = Ident.create_fresh Ident.knormal in let call_instr = Sil.Call ((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 + let set_instr = + Sil.Store {e1= Exp.Lvar sil_var; root_typ= return_type; e2= Exp.Var ret_id; loc} + in instrs @ [call_instr; set_instr] in match var_opt with @@ -856,7 +860,7 @@ let instruction (context : JContext.t) pc instr : translation = | AffectVar (var, expr) -> let stml, sil_expr, sil_type = expression context pc expr in let pvar = JContext.set_pvar context var sil_type in - let sil_instr = Sil.Store (Exp.Lvar pvar, sil_type, sil_expr, loc) in + let sil_instr = Sil.Store {e1= Exp.Lvar pvar; root_typ= sil_type; e2= sil_expr; loc} in let node_kind = Procdesc.Node.Stmt_node MethodBody in let node = create_node node_kind (stml @ [sil_instr]) in Instr node @@ -869,7 +873,9 @@ let instruction (context : JContext.t) pc instr : translation = | Some expr -> let stml, sil_expr, _ = expression context pc expr in let sil_instrs = - let return_instr = Sil.Store (Exp.Lvar ret_var, ret_type, sil_expr, loc) in + let return_instr = + Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_expr; loc} + in if return_not_null () then [assume_not_null loc sil_expr; return_instr] else [return_instr] in @@ -882,7 +888,11 @@ let instruction (context : JContext.t) pc instr : translation = and instrs_index, sil_expr_index, _ = expression context pc index_ex and instrs_value, sil_expr_value, value_typ = expression context pc value_ex in let sil_instr = - Sil.Store (Exp.Lindex (sil_expr_array, sil_expr_index), value_typ, sil_expr_value, loc) + Sil.Store + { e1= Exp.Lindex (sil_expr_array, sil_expr_index) + ; root_typ= value_typ + ; e2= sil_expr_value + ; loc } in let final_instrs = instrs_array @ instrs_index @ instrs_value @ [sil_instr] in let node_kind = Procdesc.Node.Stmt_node MethodBody in @@ -895,7 +905,9 @@ let instruction (context : JContext.t) pc instr : translation = let type_of_the_surrounding_class = JTransType.get_class_type_no_pointer program tenv cn in let type_of_the_root_of_e_lhs = type_of_the_surrounding_class in let expr_off = Exp.Lfield (sil_expr_lhs, field_name, type_of_the_surrounding_class) in - let sil_instr = Sil.Store (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in + let sil_instr = + Sil.Store {e1= expr_off; root_typ= type_of_the_root_of_e_lhs; e2= sil_expr_rhs; loc} + in let node_kind = Procdesc.Node.Stmt_node MethodBody in let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in Instr node @@ -911,7 +923,9 @@ let instruction (context : JContext.t) pc instr : translation = let type_of_the_surrounding_class = JTransType.get_class_type_no_pointer program tenv cn in let type_of_the_root_of_e_lhs = type_of_the_surrounding_class in let expr_off = Exp.Lfield (sil_expr_lhs, field_name, type_of_the_surrounding_class) in - let sil_instr = Sil.Store (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in + let sil_instr = + Sil.Store {e1= expr_off; root_typ= type_of_the_root_of_e_lhs; e2= sil_expr_rhs; loc} + in let node_kind = Procdesc.Node.Stmt_node MethodBody in let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in Instr node @@ -948,7 +962,7 @@ let instruction (context : JContext.t) pc instr : translation = | Throw expr -> let instrs, sil_expr, _ = expression context pc expr in let sil_exn = Exp.Exn sil_expr in - let sil_instr = Sil.Store (Exp.Lvar ret_var, ret_type, sil_exn, loc) in + let sil_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in let node = create_node Procdesc.Node.throw_kind (instrs @ [sil_instr]) in JContext.add_goto_jump context pc JContext.Exit ; Instr node @@ -972,7 +986,9 @@ let instruction (context : JContext.t) pc instr : translation = Typ.Procname.Java.Non_Static in let pvar = JContext.set_pvar context var class_type in - let set_instr = Sil.Store (Exp.Lvar pvar, class_type, Exp.Var ret_id, loc) in + let set_instr = + Sil.Store {e1= Exp.Lvar pvar; root_typ= class_type; e2= Exp.Var ret_id; loc} + in let instrs = (new_instr :: call_instrs) @ [set_instr] in let node_kind = create_node_kind constr_procname in let node = create_node node_kind instrs in @@ -988,7 +1004,9 @@ let instruction (context : JContext.t) pc instr : translation = let call_instr = Sil.Call ((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 set_instr = + Sil.Store {e1= Exp.Lvar array_name; root_typ= array_type; e2= Exp.Var ret_id; loc} + in let node_kind = Procdesc.Node.Stmt_node MethodBody in let node = create_node node_kind (instrs @ [call_instr; set_instr]) in Instr node @@ -1094,7 +1112,7 @@ let instruction (context : JContext.t) pc instr : translation = Typ.Procname.Java.Static in let sil_exn = Exp.Exn (Exp.Var ret_id) in - let set_instr = Sil.Store (Exp.Lvar ret_var, ret_type, sil_exn, loc) in + let set_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in let npe_instrs = instrs @ [sil_prune_null] @ (new_instr :: call_instrs) @ [set_instr] in create_node npe_kind npe_instrs in @@ -1154,7 +1172,7 @@ let instruction (context : JContext.t) pc instr : translation = [] I_Special Typ.Procname.Java.Static in let sil_exn = Exp.Exn (Exp.Var ret_id) in - let set_instr = Sil.Store (Exp.Lvar ret_var, ret_type, sil_exn, loc) in + let set_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in let out_of_bound_instrs = instrs @ [sil_assume_out_of_bound] @ (new_instr :: call_instrs) @ [set_instr] in @@ -1202,7 +1220,7 @@ let instruction (context : JContext.t) pc instr : translation = [] I_Special Typ.Procname.Java.Static in let sil_exn = Exp.Exn (Exp.Var ret_id) in - let set_instr = Sil.Store (Exp.Lvar ret_var, ret_type, sil_exn, loc) in + let set_instr = Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= sil_exn; loc} in let cce_instrs = instrs @ [call; asssume_not_instance_of] @ (new_instr :: call_instrs) @ [set_instr] in diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index dac7e28c3..35bd92103 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -32,8 +32,12 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle (* this is removed in the true branches, and in the false branch of the last handler *) let id_exn_val = Ident.create_fresh Ident.knormal in let create_entry_node loc = - let instr_get_ret_val = Sil.Load (id_ret_val, Exp.Lvar ret_var, ret_type, loc) in - let instr_deactivate_exn = Sil.Store (Exp.Lvar ret_var, ret_type, Exp.null, loc) in + let instr_get_ret_val = + Sil.Load {id= id_ret_val; e= Exp.Lvar ret_var; root_typ= ret_type; loc} + in + let instr_deactivate_exn = + Sil.Store {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= Exp.null; loc} + in let instr_unwrap_ret_val = let unwrap_builtin = Exp.Const (Const.Cfun BuiltinDecl.__unwrap_exception) in Sil.Call @@ -97,10 +101,11 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle in let instr_set_catch_var = let catch_var = JContext.set_pvar context handler.JBir.e_catch_var ret_type in - Sil.Store (Exp.Lvar catch_var, ret_type, Exp.Var id_exn_val, loc) + Sil.Store {e1= Exp.Lvar catch_var; root_typ= ret_type; e2= Exp.Var id_exn_val; loc} in let instr_rethrow_exn = - Sil.Store (Exp.Lvar ret_var, ret_type, Exp.Exn (Exp.Var id_exn_val), loc) + Sil.Store + {e1= Exp.Lvar ret_var; root_typ= ret_type; e2= Exp.Exn (Exp.Var id_exn_val); loc} in let node_kind_true = Procdesc.Node.Prune_node (true, if_kind, PruneNodeKind_ExceptionHandler) diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 80c0ac684..a17db06e2 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -421,14 +421,14 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p astate ) | Sil.Metadata (Abstract _ | Nullify _ | Skip | VariableLifetimeBegins _) -> typestate - | Sil.Load (id, e, typ, loc) -> + | Sil.Load {id; e; root_typ= typ; loc} -> typecheck_expr_for_errors typestate e loc ; let e', typestate' = convert_complex_exp_to_pvar node false e typestate loc in TypeState.add_id id (typecheck_expr_simple typestate' e' typ TypeOrigin.Undef loc) typestate' - | Sil.Store (Exp.Lvar pvar, _, Exp.Exn _, _) when is_return pvar -> + | Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Exn _} when is_return pvar -> (* skip assignment to return variable where it is an artifact of a throw instruction *) typestate - | Sil.Store (e1, typ, e2, loc) -> + | Sil.Store {e1; root_typ= typ; e2; loc} -> typecheck_expr_for_errors typestate e1 loc ; let e1', typestate1 = convert_complex_exp_to_pvar node true e1 typestate loc in let check_field_assign () = @@ -944,8 +944,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let found = ref None in let do_instr i = match i with - | Sil.Store (e, _, e', _) when Exp.equal (Exp.Lvar pvar) (Idenv.expand_expr idenv e') - -> + | Sil.Store {e1= e; e2= e'} + when Exp.equal (Exp.Lvar pvar) (Idenv.expand_expr idenv e') -> found := Some e | _ -> () @@ -1008,7 +1008,7 @@ let typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc find_canon false in if has_exceptions then typestates_exn := typestate :: !typestates_exn - | Sil.Store (Exp.Lvar pv, _, _, _) + | Sil.Store {e1= Exp.Lvar pv} when Pvar.is_return pv && Procdesc.Node.equal_nodekind (Procdesc.Node.get_kind node) Procdesc.Node.throw_kind -> diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 31111a3da..c439e5c42 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -157,7 +157,7 @@ module PulseTransferFunctions = struct let exec_instr (astate : Domain.t) {ProcData.summary} _cfg_node (instr : Sil.instr) = match instr with - | Load (lhs_id, rhs_exp, _typ, loc) -> + | Load {id= lhs_id; e= rhs_exp; loc} -> (* [lhs_id := *rhs_exp] *) let result = PulseOperations.eval_deref loc rhs_exp astate @@ -165,7 +165,7 @@ module PulseTransferFunctions = struct PulseOperations.write_id lhs_id (rhs_addr, rhs_history) astate in [check_error summary result] - | Store (lhs_exp, _typ, rhs_exp, loc) -> + | Store {e1= lhs_exp; e2= rhs_exp; loc} -> (* [*lhs_exp := rhs_exp] *) let event = ValueHistory.Assignment {location= loc} in let result = diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index 97b007a93..84b66cd30 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -82,7 +82,11 @@ let get_active_transitions e_fun arg_ts = let set_transitions loc active_transitions = let store i b = let value = if b then Exp.one else Exp.zero in - Sil.Store (ToplUtils.static_var (ToplName.transition i), ToplUtils.topl_class_typ, value, loc) + Sil.Store + { e1= ToplUtils.static_var (ToplName.transition i) + ; root_typ= ToplUtils.topl_class_typ + ; e2= value + ; loc } in Array.mapi ~f:store active_transitions diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml index a65ce828c..2c9917cd0 100644 --- a/infer/src/topl/ToplMonitor.ml +++ b/infer/src/topl/ToplMonitor.ml @@ -119,7 +119,9 @@ let pure_exp e : Exp.t * Sil.instr list = let pairs = List.map ~f:(fun e -> (e, Ident.create_fresh Ident.knormal)) es in let subst = List.map ~f:(function e, id -> (e, Exp.Var id)) pairs in let e' = Sil.exp_replace_exp subst e in - let mk_load (e, id) = Sil.Load (id, e, ToplUtils.any_type, sourcefile_location ()) in + let mk_load (e, id) = + Sil.Load {id; e; root_typ= ToplUtils.any_type; loc= sourcefile_location ()} + in let loads = List.map ~f:mk_load pairs in (e', loads) @@ -166,8 +168,9 @@ let stmt_node instrs : node_generator = let sil_assign lhs rhs = let tempvar = Ident.create_fresh Ident.knormal in - [ Sil.Load (tempvar, rhs, ToplUtils.any_type, sourcefile_location ()) - ; Sil.Store (lhs, ToplUtils.any_type, Exp.Var tempvar, sourcefile_location ()) ] + [ Sil.Load {id= tempvar; e= rhs; root_typ= ToplUtils.any_type; loc= sourcefile_location ()} + ; Sil.Store + {e1= lhs; root_typ= ToplUtils.any_type; e2= Exp.Var tempvar; loc= sourcefile_location ()} ] let assign lhs rhs : node_generator = stmt_node (sil_assign lhs rhs) @@ -247,10 +250,10 @@ let generate_execute_state automaton proc_name = let arg_action i pattern = step (ToplUtils.static_var (ToplName.saved_arg i)) pattern in stmt_node [ Sil.Store - ( ToplUtils.static_var ToplName.state - , Typ.mk (Tint IInt) - , Exp.int (IntLit.of_int transition.target) - , sourcefile_location () ) ] + { e1= ToplUtils.static_var ToplName.state + ; root_typ= Typ.mk (Tint IInt) + ; e2= Exp.int (IntLit.of_int transition.target) + ; loc= sourcefile_location () } ] :: step (ToplUtils.static_var ToplName.retval) transition.label.ToplAst.return :: Option.value_map ~default:[] ~f:(List.mapi ~f:arg_action) transition.label.ToplAst.arguments diff --git a/infer/src/unit/analyzerTester.ml b/infer/src/unit/analyzerTester.ml index c868299d6..35f0ef8c3 100644 --- a/infer/src/unit/analyzerTester.ml +++ b/infer/src/unit/analyzerTester.ml @@ -68,9 +68,13 @@ module StructuredSil = struct let unknown_exp = var_of_str "__unknown__" - let make_load ~rhs_typ lhs_id rhs_exp = Cmd (Sil.Load (lhs_id, rhs_exp, rhs_typ, dummy_loc)) + let make_load ~rhs_typ lhs_id rhs_exp = + Cmd (Sil.Load {id= lhs_id; e= rhs_exp; root_typ= rhs_typ; loc= dummy_loc}) + + + let make_set ~rhs_typ ~lhs_exp ~rhs_exp = + Cmd (Sil.Store {e1= lhs_exp; root_typ= rhs_typ; e2= rhs_exp; loc= dummy_loc}) - 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) ?return:return_opt args = let ret_id_typ =