[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
master
Sungkeun Cho 5 years ago committed by Facebook Github Bot
parent 78cfc867a5
commit a50fcaf2dd

@ -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) ->

@ -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 ->

@ -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

@ -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 *)

@ -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) -> (

@ -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)

@ -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 ;

@ -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)

@ -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

@ -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)]

@ -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 =

@ -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) ;

@ -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

@ -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

@ -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 _}, _)

@ -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 ->

@ -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

@ -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

@ -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, _) ->

@ -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. *)

@ -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), _, _, _)

@ -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 _ ->

@ -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

@ -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))
| _ ->

@ -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

@ -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
| _ ->

@ -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 )

@ -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
| _ ->

@ -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 ->

@ -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

@ -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

@ -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

@ -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)

@ -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
->

@ -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 =

@ -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

@ -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

@ -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 =

Loading…
Cancel
Save