pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Cleanup instruction names: use Load/Store instead of Letderef/Set.

Browse Source 
Reviewed By: jberdine

Differential Revision: D3749108

fbshipit-source-id: c5aa438
master
Cristiano Calcagno 9 years ago committed by Facebook Github Bot 2
parent c0969da619
commit 91d9cd83b5
36 changed files with 259 additions and 241 deletions
Show Stats Download Patch File Download Diff File

33
infer/src/IR/Cfg.re
Unescape View File

@ -670,7 +670,7 @@ let module Node = {
};
let convert_instr instrs =>
fun
| Sil.Letderef id (Exp.Lvar origin_pvar as origin_exp) origin_typ loc => {
| Sil.Load id (Exp.Lvar origin_pvar as origin_exp) origin_typ loc => {
let (_, specialized_typ) = {
let pvar_name = Pvar.get_name origin_pvar;
try (IList.find (fun (n, _) => Mangled.equal n pvar_name) substitutions) {
@ -678,24 +678,24 @@ let module Node = {
}
};
subst_map := Ident.IdentMap.add id specialized_typ !subst_map;
[Sil.Letderef id (convert_exp origin_exp) specialized_typ loc, ...instrs]
[Sil.Load id (convert_exp origin_exp) specialized_typ loc, ...instrs]
}
| Sil.Letderef id (Exp.Var origin_id as origin_exp) origin_typ loc => {
| Sil.Load id (Exp.Var origin_id as origin_exp) origin_typ loc => {
let updated_typ =
switch (Ident.IdentMap.find origin_id !subst_map) {
| Typ.Tptr typ _ => typ
| _ => failwith "Expecting a pointer type"
| exception Not_found => origin_typ
};
[Sil.Letderef id (convert_exp origin_exp) updated_typ loc, ...instrs]
[Sil.Load id (convert_exp origin_exp) updated_typ loc, ...instrs]
}
| Sil.Letderef id origin_exp origin_typ loc => [
Sil.Letderef id (convert_exp origin_exp) origin_typ loc,
| Sil.Load id origin_exp origin_typ loc => [
Sil.Load id (convert_exp origin_exp) origin_typ loc,
...instrs
]
| Sil.Set assignee_exp origin_typ origin_exp loc => {
| Sil.Store assignee_exp origin_typ origin_exp loc => {
let set_instr =
Sil.Set (convert_exp assignee_exp) origin_typ (convert_exp origin_exp) loc;
Sil.Store (convert_exp assignee_exp) origin_typ (convert_exp origin_exp) loc;
[set_instr, ...instrs]
}
| Sil.Call
@ -1194,27 +1194,26 @@ let inline_synthetic_method ret_ids etl proc_desc loc_call :option Sil.instr =>
let do_instr _ instr =>
switch (instr, ret_ids, etl) {
| (
Sil.Letderef _ (Exp.Lfield (Exp.Var _) fn ft) bt _,
Sil.Load _ (Exp.Lfield (Exp.Var _) fn ft) bt _,
[ret_id],
[(e1, _)] /* getter for fields */
) =>
let instr' = Sil.Letderef ret_id (Exp.Lfield e1 fn ft) bt loc_call;
let instr' = Sil.Load ret_id (Exp.Lfield e1 fn ft) bt loc_call;
found instr instr'
| (Sil.Letderef _ (Exp.Lfield (Exp.Lvar pvar) fn ft) bt _, [ret_id], [])
when Pvar.is_global pvar =>
| (Sil.Load _ (Exp.Lfield (Exp.Lvar pvar) fn ft) bt _, [ret_id], []) when Pvar.is_global pvar =>
/* getter for static fields */
let instr' = Sil.Letderef ret_id (Exp.Lfield (Exp.Lvar pvar) fn ft) bt loc_call;
let instr' = Sil.Load ret_id (Exp.Lfield (Exp.Lvar pvar) fn ft) bt loc_call;
found instr instr'
| (
Sil.Set (Exp.Lfield _ fn ft) bt _ _,
Sil.Store (Exp.Lfield _ fn ft) bt _ _,
_,
[(e1, _), (e2, _)] /* setter for fields */
) =>
let instr' = Sil.Set (Exp.Lfield e1 fn ft) bt e2 loc_call;
let instr' = Sil.Store (Exp.Lfield e1 fn ft) bt e2 loc_call;
found instr instr'
| (Sil.Set (Exp.Lfield (Exp.Lvar pvar) fn ft) bt _ _, _, [(e1, _)]) when Pvar.is_global pvar =>
| (Sil.Store (Exp.Lfield (Exp.Lvar pvar) fn ft) bt _ _, _, [(e1, _)]) when Pvar.is_global pvar =>
/* setter for static fields */
let instr' = Sil.Set (Exp.Lfield (Exp.Lvar pvar) fn ft) bt e1 loc_call;
let instr' = Sil.Store (Exp.Lfield (Exp.Lvar pvar) fn ft) bt e1 loc_call;
found instr instr'
| (Sil.Call ret_ids' (Exp.Const (Const.Cfun pn)) etl' _ cf, _, _)
when IList.length ret_ids == IList.length ret_ids' && IList.length etl' == IList.length etl =>

60
infer/src/IR/Sil.re
Unescape View File

@ -41,12 +41,20 @@ type stackop =
/** An instruction. */
type instr =
/** declaration [let x = *lexp:typ] where [typ] is the root type of [lexp] */
/* note for frontend writers: [x] must be used in a subsequent instruction, otherwise the entire
`Letderef` instruction may be eliminated by copy-propagation */
| Letderef of Ident.t Exp.t Typ.t Location.t
/** assignment [*lexp1:typ = exp2] where [typ] is the root type of [lexp1] */
| Set of Exp.t Typ.t Exp.t 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]. */
/* 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
/** 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 store. */
| Store of Exp.t Typ.t Exp.t Location.t
/** prune the state based on [exp=1], the boolean indicates whether true branch */
| Prune of Exp.t Location.t bool if_kind
/** [Call (ret_id1..ret_idn, e_fun, arg_ts, loc, call_flags)] represents an instructions
@ -64,8 +72,8 @@ type instr =
/** Check if an instruction is auxiliary, or if it comes from source instructions. */
let instr_is_auxiliary =
fun
| Letderef _
| Set _
| Load _
| Store _
| Prune _
| Call _ => false
| Nullify _
@ -644,8 +652,8 @@ let pp_exp_typ pe f (e, t) => F.fprintf f "%a:%a" (pp_exp pe) e (Typ.pp pe) t;
/** Get the location of the instruction */
let instr_get_loc =
fun
| Letderef _ _ _ loc
| Set _ _ _ loc
| Load _ _ _ loc
| Store _ _ _ loc
| Prune _ loc _ _
| Call _ _ _ loc _
| Nullify _ loc
@ -658,8 +666,8 @@ let instr_get_loc =
/** get the expressions occurring in the instruction */
let instr_get_exps =
fun
| Letderef id e _ _ => [Exp.Var id, e]
| Set e1 _ e2 _ => [e1, e2]
| Load id e _ _ => [Exp.Var id, e]
| Store e1 _ e2 _ => [e1, e2]
| Prune cond _ _ _ => [cond]
| Call ret_ids e _ _ _ => [e, ...(IList.map (fun id => Exp.Var id)) ret_ids]
| Nullify pvar _ => [Exp.Lvar pvar]
@ -673,9 +681,9 @@ let instr_get_exps =
let pp_instr pe0 f instr => {
let (pe, changed) = color_pre_wrapper pe0 f instr;
switch instr {
| Letderef id e t loc =>
| Load id e t loc =>
F.fprintf f "%a=*%a:%a %a" (Ident.pp pe) id (pp_exp pe) e (Typ.pp pe) t Location.pp loc
| Set e1 t e2 loc =>
| Store e1 t e2 loc =>
F.fprintf f "*%a:%a=%a %a" (pp_exp pe) e1 (Typ.pp pe) t (pp_exp pe) e2 Location.pp loc
| Prune cond loc true_branch _ =>
F.fprintf f "PRUNE(%a, %b); %a" (pp_exp pe) cond true_branch Location.pp loc
@ -2125,7 +2133,7 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
| _ => id
};
switch instr {
| Letderef id rhs_exp typ loc =>
| Load id rhs_exp typ loc =>
let id' =
if sub_id_binders {
sub_id id
@ -2136,15 +2144,15 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
if (id' === id && rhs_exp' === rhs_exp) {
instr
} else {
Letderef id' rhs_exp' typ loc
Load id' rhs_exp' typ loc
}
| Set lhs_exp typ rhs_exp loc =>
| Store lhs_exp typ rhs_exp loc =>
let lhs_exp' = exp_sub_ids f lhs_exp;
let rhs_exp' = exp_sub_ids f rhs_exp;
if (lhs_exp' === lhs_exp && rhs_exp' === rhs_exp) {
instr
} else {
Set lhs_exp' typ rhs_exp' loc
Store lhs_exp' typ rhs_exp' loc
}
| Call ret_ids fun_exp actuals call_flags loc =>
let ret_ids' =
@ -2208,7 +2216,7 @@ let exp_typ_compare (exp1, typ1) (exp2, typ2) => {
let instr_compare instr1 instr2 =>
switch (instr1, instr2) {
| (Letderef id1 e1 t1 loc1, Letderef id2 e2 t2 loc2) =>
| (Load id1 e1 t1 loc1, Load id2 e2 t2 loc2) =>
let n = Ident.compare id1 id2;
if (n != 0) {
n
@ -2225,9 +2233,9 @@ let instr_compare instr1 instr2 =>
}
}
}
| (Letderef _, _) => (-1)
| (_, Letderef _) => 1
| (Set e11 t1 e21 loc1, Set e12 t2 e22 loc2) =>
| (Load _, _) => (-1)
| (_, Load _) => 1
| (Store e11 t1 e21 loc1, Store e12 t2 e22 loc2) =>
let n = Exp.compare e11 e12;
if (n != 0) {
n
@ -2244,8 +2252,8 @@ let instr_compare instr1 instr2 =>
}
}
}
| (Set _, _) => (-1)
| (_, Set _) => 1
| (Store _, _) => (-1)
| (_, Store _) => 1
| (Prune cond1 loc1 true_branch1 ik1, Prune cond2 loc2 true_branch2 ik2) =>
let n = Exp.compare cond1 cond2;
if (n != 0) {
@ -2453,7 +2461,7 @@ let instr_compare_structural instr1 instr2 exp_map => {
}
};
switch (instr1, instr2) {
| (Letderef id1 e1 t1 _, Letderef id2 e2 t2 _) =>
| (Load id1 e1 t1 _, Load id2 e2 t2 _) =>
let (n, exp_map) = exp_compare_structural (Var id1) (Var id2) exp_map;
if (n != 0) {
(n, exp_map)
@ -2468,7 +2476,7 @@ let instr_compare_structural instr1 instr2 exp_map => {
exp_map
)
}
| (Set e11 t1 e21 _, Set e12 t2 e22 _) =>
| (Store e11 t1 e21 _, Store e12 t2 e22 _) =>
let (n, exp_map) = exp_compare_structural e11 e12 exp_map;
if (n != 0) {
(n, exp_map)

20
infer/src/IR/Sil.rei
Unescape View File

@ -43,12 +43,20 @@ type stackop =
/** An instruction. */
type instr =
/** declaration [let x = *lexp:typ] where [typ] is the root type of [lexp] */
/* note for frontend writers: [x] must be used in a subsequent instruction, otherwise the entire
`Letderef` instruction may be eliminated by copy-propagation */
| Letderef of Ident.t Exp.t Typ.t Location.t
/** assignment [*lexp1:typ = exp2] where [typ] is the root type of [lexp1] */
| Set of Exp.t Typ.t Exp.t 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]. */
/* 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
/** 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 store. */
| Store of Exp.t Typ.t Exp.t Location.t
/** prune the state based on [exp=1], the boolean indicates whether true branch */
| Prune of Exp.t Location.t bool if_kind
/** [Call (ret_id1..ret_idn, e_fun, arg_ts, loc, call_flags)] represents an instructions

4
infer/src/backend/buckets.ml
Unescape View File

@ -62,7 +62,7 @@ let check_access access_opt de_opt =
IList.exists (Mangled.equal name) formal_names in
let formal_ids = ref [] in
let process_formal_letref = function
| Sil.Letderef (id, Exp.Lvar pvar, _, _) ->
| Sil.Load (id, Exp.Lvar pvar, _, _) ->
let is_java_this =
!Config.curr_language = Config.Java && Pvar.is_this pvar in
if not is_java_this && is_formal pvar then formal_ids := id :: !formal_ids
@ -91,7 +91,7 @@ let check_access access_opt de_opt =
| _ -> false in
if IList.exists arg_is_formal_param etl then formal_param_used_in_call := true;
true
| Sil.Set (_, _, e, _) ->
| Sil.Store (_, _, e, _) ->
exp_is_null e
| _ -> false in
IList.exists filter (Cfg.Node.get_instrs node) in

45
infer/src/backend/errdesc.ml
Unescape View File

@ -97,7 +97,7 @@ let find_in_node_or_preds start_node f_node_instr =
(** Find the Set instruction used to assign [id] to a program variable, if any *)
let find_variable_assigment node id : Sil.instr option =
let find_set _ instr = match instr with
| Sil.Set (Exp.Lvar _, _, e, _) when Exp.equal (Exp.Var id) e -> Some instr
| Sil.Store (Exp.Lvar _, _, e, _) when Exp.equal (Exp.Var id) e -> Some instr
| _ -> None in
find_in_node_or_preds node find_set
@ -126,7 +126,7 @@ let find_other_prune_node node =
(** Return true if [id] is assigned to a program variable which is then nullified *)
let id_is_assigned_then_dead node id =
match find_variable_assigment node id with
| Some (Sil.Set (Exp.Lvar pvar, _, _, _) as instr)
| Some (Sil.Store (Exp.Lvar pvar, _, _, _) as instr)
when Pvar.is_local pvar || Pvar.is_callee pvar ->
let is_prune = match Cfg.Node.get_kind node with
| Cfg.Node.Prune_node _ -> true
@ -165,7 +165,8 @@ let find_normal_variable_funcall
(** Find a program variable assignment in the current node or predecessors. *)
let find_program_variable_assignment node pvar : (Cfg.Node.t * Ident.t) option =
let find_instr node = function
| Sil.Set (Exp.Lvar _pvar, _, Exp.Var id, _) when Pvar.equal pvar _pvar && Ident.is_normal id ->
| Sil.Store (Exp.Lvar _pvar, _, Exp.Var id, _)
when Pvar.equal pvar _pvar && Ident.is_normal id ->
Some (node, id)
| _ ->
None in
@ -195,7 +196,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 : (Cfg.Node.t * Exp.t) option =
let find_instr node = function
| Sil.Letderef(_id, e, _, _) when Ident.equal _id id -> Some (node, e)
| Sil.Load (_id, e, _, _) when Ident.equal _id id -> Some (node, e)
| _ -> None in
find_in_node_or_preds node find_instr
@ -204,7 +205,7 @@ let find_ident_assignment node id : (Cfg.Node.t * Exp.t) option =
let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
let find_instr n =
let filter = function
| Sil.Set (Exp.Lvar _pvar, _, Exp.Const (Const.Cint i), _) when Pvar.equal pvar _pvar ->
| Sil.Store (Exp.Lvar _pvar, _, Exp.Const (Const.Cint i), _) when Pvar.equal pvar _pvar ->
IntLit.iszero i <> true_branch
| _ -> false in
IList.exists filter (Cfg.Node.get_instrs n) in
@ -216,29 +217,29 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
else None
| _ -> None
(** Find the Letderef instruction used to declare normal variable [id],
(** Find the Load instruction used to declare normal variable [id],
and return the expression dereferenced to initialize [id] *)
let rec _find_normal_variable_letderef (seen : Exp.Set.t) node id : DExp.t option =
let rec _find_normal_variable_load (seen : Exp.Set.t) node id : DExp.t option =
let is_infer = not (Config.checkers || Config.eradicate) in
let find_declaration node = function
| Sil.Letderef (id0, e, _, _) when Ident.equal id id0 ->
| Sil.Load (id0, e, _, _) when Ident.equal id id0 ->
if verbose
then
(L.d_str "find_normal_variable_letderef defining ";
(L.d_str "find_normal_variable_load defining ";
Sil.d_exp e; L.d_ln ());
_exp_lv_dexp seen node e
| Sil.Call ([id0], Exp.Const (Const.Cfun pn), (e, _):: _, _, _)
when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") ->
if verbose
then
(L.d_str "find_normal_variable_letderef cast on ";
(L.d_str "find_normal_variable_load cast on ";
Sil.d_exp e; L.d_ln ());
_exp_rv_dexp seen node e
| Sil.Call ([id0], (Exp.Const (Const.Cfun pname) as fun_exp), args, loc, call_flags)
when Ident.equal id id0 ->
if verbose
then
(L.d_str "find_normal_variable_letderef function call ";
(L.d_str "find_normal_variable_load function call ";
Sil.d_exp fun_exp; L.d_ln ());
let fun_dexp = DExp.Dconst (Const.Cfun pname) in
@ -250,7 +251,7 @@ let rec _find_normal_variable_letderef (seen : Exp.Set.t) node id : DExp.t optio
let unNone = function Some x -> x | None -> assert false in
IList.map unNone args_dexpo in
Some (DExp.Dretcall (fun_dexp, args_dexp, loc, call_flags))
| Sil.Set (Exp.Lvar pvar, _, Exp.Var id0, _)
| Sil.Store (Exp.Lvar pvar, _, Exp.Var id0, _)
when is_infer && 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:
@ -263,7 +264,7 @@ let rec _find_normal_variable_letderef (seen : Exp.Set.t) node id : DExp.t optio
if verbose && res == None
then
(L.d_str
("find_normal_variable_letderef could not find " ^
("find_normal_variable_load could not find " ^
Ident.to_string id ^
" in node " ^
string_of_int (Cfg.Node.get_id node :> int));
@ -287,7 +288,7 @@ and _exp_lv_dexp (_seen : Exp.Set.t) node e : DExp.t option =
| _ -> None)
| Exp.Var id when Ident.is_normal id ->
if verbose then (L.d_str "exp_lv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
(match _find_normal_variable_letderef seen node id with
(match _find_normal_variable_load seen node id with
| None -> None
| Some de -> Some (DExp.Dderef de))
| Exp.Lvar pvar ->
@ -327,7 +328,7 @@ and _exp_lv_dexp (_seen : Exp.Set.t) node e : DExp.t option =
L.d_str (" " ^ Ident.fieldname_to_string f);
L.d_ln ()
end;
(match _find_normal_variable_letderef seen node id with
(match _find_normal_variable_load seen node id with
| None -> None
| Some de -> Some (DExp.Darrow (de, f)))
| Exp.Lfield (e1, f, _) ->
@ -377,7 +378,7 @@ and _exp_rv_dexp (_seen : Exp.Set.t) node e : DExp.t option =
else Some (DExp.Dpvaraddr pv)
| Exp.Var id when Ident.is_normal id ->
if verbose then (L.d_str "exp_rv_dexp: normal var "; Sil.d_exp e; L.d_ln ());
_find_normal_variable_letderef seen node id
_find_normal_variable_load seen node id
| Exp.Lfield (e1, f, _) ->
if verbose then
begin
@ -421,7 +422,7 @@ and _exp_rv_dexp (_seen : Exp.Set.t) node e : DExp.t option =
if verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ());
None
let find_normal_variable_letderef = _find_normal_variable_letderef Exp.Set.empty
let find_normal_variable_load = _find_normal_variable_load Exp.Set.empty
let exp_lv_dexp = _exp_lv_dexp Exp.Set.empty
let exp_rv_dexp = _exp_rv_dexp Exp.Set.empty
@ -553,7 +554,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
let nullify_pvars_notmp =
IList.filter (fun pvar -> not (Pvar.is_frontend_tmp pvar)) nullify_pvars in
value_str_from_pvars_vpath nullify_pvars_notmp vpath
| Some (Sil.Set (lexp, _, _, _)) when vpath = None ->
| Some (Sil.Store (lexp, _, _, _)) when vpath = None ->
if verbose
then
(L.d_str "explain_leak: current instruction Set for ";
@ -883,7 +884,7 @@ let _explain_access
then
(L.d_str "find_outermost_dereference: normal var ";
Sil.d_exp e; L.d_ln ());
find_normal_variable_letderef node id
find_normal_variable_load node id
| Exp.Lfield (e', _, _) ->
if verbose then (L.d_str "find_outermost_dereference: Lfield "; Sil.d_exp e; L.d_ln ());
find_outermost_dereference node e'
@ -912,10 +913,10 @@ let _explain_access
Sil.d_exp e; L.d_ln ());
None in
let find_exp_dereferenced () = match State.get_instr () with
| Some Sil.Set (e, _, _, _) ->
if verbose then (L.d_str "explain_dereference Sil.Set "; Sil.d_exp e; L.d_ln ());
| Some Sil.Store (e, _, _, _) ->
if verbose then (L.d_str "explain_dereference Sil.Store "; Sil.d_exp e; L.d_ln ());
Some e
| Some Sil.Letderef (_, e, _, _) ->
| Some Sil.Load (_, e, _, _) ->
if verbose then (L.d_str "explain_dereference Binop.Leteref "; Sil.d_exp e; L.d_ln ());
Some e
| Some Sil.Call (_, Exp.Const (Const.Cfun fn), [(e, _)], _, _)

16
infer/src/backend/interproc.ml
Unescape View File

@ -374,15 +374,15 @@ let check_assignement_guard node =
IList.exists is_call instrs in
let is_set_instr i =
match i with
| Sil.Set _ -> true
| Sil.Store _ -> true
| _ -> false in
let is_prune_instr i =
match i with
| Sil.Prune _ -> true
| _ -> false in
let is_letderef_instr i =
let is_load_instr i =
match i with
| Sil.Letderef _ -> true
| Sil.Load _ -> true
| _ -> false in
let is_frontend_tmp e =
match e with
@ -397,11 +397,11 @@ let check_assignement_guard node =
let prune_var n =
let ins = Cfg.Node.get_instrs n in
let pi = IList.filter is_prune_instr ins in
let leti = IList.filter is_letderef_instr ins in
let leti = IList.filter is_load_instr ins in
match pi, leti with
| [Sil.Prune (Exp.Var(e1), _, _, _)], [Sil.Letderef(e2, e', _, _)]
| [Sil.Prune (Exp.UnOp(Unop.LNot, Exp.Var(e1), _), _, _, _)],
[Sil.Letderef(e2, e', _, _)]
| [Sil.Prune (Exp.Var (e1), _, _, _)], [Sil.Load (e2, e', _, _)]
| [Sil.Prune (Exp.UnOp (Unop.LNot, Exp.Var e1, _), _, _, _)],
[Sil.Load (e2, e', _, _)]
when (Ident.equal e1 e2) ->
if verbose
then
@ -451,7 +451,7 @@ let check_assignement_guard node =
is_set_instr i)
instr in
(match set_instr_at_succs_loc with
| [Sil.Set(e, _, _, _)] ->
| [Sil.Store (e, _, _, _)] ->
(* we now check if e is the same expression used to prune*)
if (is_prune_exp e) && not ((node_contains_call node) && (is_frontend_tmp e)) then (
let desc = Errdesc.explain_condition_is_assignment l_node in

15
infer/src/backend/modelBuiltins.ml
Unescape View File

@ -24,7 +24,7 @@ let execute___builtin_va_arg { Builtin.pdesc; tenv; prop_; path; ret_ids; args;
: Builtin.ret_typ =
match args, ret_ids with
| [_; _; (lexp3, typ3)], _ ->
let instr' = Sil.Set (lexp3, typ3, Exp.zero, loc) in
let instr' = Sil.Store (lexp3, typ3, Exp.zero, loc) in
SymExec.instrs ~mask_errors:true tenv pdesc [instr'] [(prop_, path)]
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -471,11 +471,11 @@ let execute___objc_counter_update
(* This is the case as a call f(o) it's translates as n$1=*&o; f(n$1) *)
(* n$2 = *n$1.hidden *)
let tmp = Ident.create_fresh Ident.knormal in
let hidden_field = Exp.Lfield(lexp, Ident.fieldname_hidden, typ') in
let counter_to_tmp = Sil.Letderef(tmp, hidden_field, typ', loc) in
let hidden_field = Exp.Lfield (lexp, Ident.fieldname_hidden, typ') in
let counter_to_tmp = Sil.Load (tmp, hidden_field, typ', loc) in
(* *n$1.hidden = (n$2 +/- delta) *)
let update_counter =
Sil.Set
Sil.Store
(hidden_field,
typ',
Exp.BinOp(op, Exp.Var tmp, Exp.Const (Const.Cint delta)),
@ -822,7 +822,8 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
| _ -> typ
with Not_found -> typ in
let typ_string = Typ.to_string typ in
let set_instr = Sil.Set (field_exp, Typ.Tvoid, Exp.Const (Const.Cstr typ_string), loc) in
let set_instr =
Sil.Store (field_exp, Typ.Tvoid, Exp.Const (Const.Cstr typ_string), loc) in
SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] res
| _ -> res)
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -938,7 +939,7 @@ let execute___infer_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
| _ ->
raise (Exceptions.Wrong_argument_number __POS__) in
let set_instr =
Sil.Set (Exp.Lvar Sil.custom_error, Typ.Tvoid, Exp.Const (Const.Cstr error_str), loc) in
Sil.Store (Exp.Lvar Sil.custom_error, Typ.Tvoid, Exp.Const (Const.Cstr error_str), loc) in
SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)]
(* translate builtin assertion failure *)
@ -951,7 +952,7 @@ let execute___assert_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
| _ ->
raise (Exceptions.Wrong_argument_number __POS__) in
let set_instr =
Sil.Set (Exp.Lvar Sil.custom_error, Typ.Tvoid, Exp.Const (Const.Cstr error_str), loc) in
Sil.Store (Exp.Lvar Sil.custom_error, Typ.Tvoid, Exp.Const (Const.Cstr error_str), loc) in
SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)]
let __assert_fail = Builtin.register

8
infer/src/backend/preanal.ml
Unescape View File

@ -134,7 +134,7 @@ module NullifyTransferFunctions = struct
let exec_instr ((active_defs, to_nullify) as astate) extras node instr =
let astate' = match instr with
| Sil.Letderef (lhs_id, _, _, _) ->
| Sil.Load (lhs_id, _, _, _) ->
VarDomain.add (Var.of_id lhs_id) active_defs, to_nullify
| Sil.Call (lhs_ids, _, _, _, _) ->
let active_defs' =
@ -143,9 +143,9 @@ module NullifyTransferFunctions = struct
active_defs
lhs_ids in
active_defs', to_nullify
| Sil.Set (Exp.Lvar lhs_pvar, _, _, _) ->
| Sil.Store (Exp.Lvar lhs_pvar, _, _, _) ->
VarDomain.add (Var.of_pvar lhs_pvar) active_defs, to_nullify
| Sil.Set _ | Prune _ | Declare_locals _ | Stackop _ | Remove_temps _
| Sil.Store _ | Prune _ | Declare_locals _ | Stackop _ | Remove_temps _
| Abstract _ ->
astate
| Sil.Nullify _ ->
@ -169,7 +169,7 @@ let remove_dead_frontend_stores pdesc liveness_inv_map =
| None -> true in
let is_used_store (instr, instr_id_opt) =
match instr, instr_id_opt with
| Sil.Letderef (id, _, _, _), Some instr_id when not (Ident.is_none id) ->
| Sil.Load (id, _, _, _), Some instr_id when not (Ident.is_none id) ->
is_live (Var.of_id id) instr_id liveness_inv_map
| _ -> true in
let node_remove_dead_stores node =

6
infer/src/backend/state.ml
Unescape View File

@ -125,8 +125,8 @@ let node_simple_key node =
if Sil.instr_is_auxiliary instr then ()
else
match instr with
| Sil.Letderef _ -> add_key 1
| Sil.Set _ -> add_key 2
| Sil.Load _ -> add_key 1
| Sil.Store _ -> add_key 2
| Sil.Prune _ -> add_key 3
| Sil.Call _ -> add_key 4
| Sil.Nullify _ -> add_key 5
@ -148,7 +148,7 @@ let node_key node =
let instrs_normalize instrs =
let bound_ids =
let do_instr ids = function
| Sil.Letderef (id, _, _, _) -> id :: ids
| Sil.Load (id, _, _, _) -> id :: ids
| _ -> ids in
IList.fold_left do_instr [] instrs in
let subst =

34
infer/src/backend/symExec.ml
Unescape View File

@ -100,7 +100,7 @@ let rec apply_offlist
| _ -> false in
let is_hidden_field () =
match State.get_instr () with
| Some (Sil.Letderef (_, Exp.Lfield (_, fieldname, _), _, _)) ->
| Some (Sil.Load (_, Exp.Lfield (_, fieldname, _), _, _)) ->
Ident.fieldname_is_hidden fieldname
| _ -> false in
let inst_new = match inst with
@ -888,8 +888,8 @@ let add_taint prop lhs_id rhs_exp pname tenv =
end
| _ -> prop
let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ loc prop_ =
let execute_letderef_ pdesc tenv id loc acc_in iter =
let execute_load ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ loc prop_ =
let execute_load_ pdesc tenv id loc acc_in iter =
let iter_ren = Prop.prop_iter_make_id_primed id iter in
let prop_ren = Prop.prop_iter_to_prop iter_ren in
match Prop.prop_iter_current iter_ren with
@ -916,7 +916,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
| Some pred_insts -> IList.rev (IList.fold_left update acc_in pred_insts)
end
| (Sil.Hpointsto _, _) ->
Errdesc.warning_err loc "no offset access in execute_letderef -- treating as skip@.";
Errdesc.warning_err loc "no offset access in execute_load -- treating as skip@.";
(Prop.prop_iter_to_prop iter_ren) :: acc_in
| _ ->
(* The implementation of this case means that we
@ -949,7 +949,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
else prop in
let iter_list =
Rearrange.rearrange ~report_deref_errors pdesc tenv n_rhs_exp' typ prop' loc in
IList.rev (IList.fold_left (execute_letderef_ pdesc tenv id loc) [] iter_list)
IList.rev (IList.fold_left (execute_load_ pdesc tenv id loc) [] iter_list)
with Rearrange.ARRAY_ACCESS ->
if (Config.array_level = 0) then assert false
else
@ -964,8 +964,8 @@ let load_ret_annots pname =
| None ->
Typ.item_annotation_empty
let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp loc prop_ =
let execute_set_ pdesc tenv rhs_exp acc_in iter =
let execute_store ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp loc prop_ =
let execute_store_ pdesc tenv rhs_exp acc_in iter =
let (lexp, strexp, typ, len, st, offlist) =
match Prop.prop_iter_current iter with
| (Sil.Hpointsto(lexp, strexp, Exp.Sizeof (typ, len, st)), offlist) ->
@ -988,7 +988,7 @@ let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp
let prop = Attribute.replace_objc_null prop n_lhs_exp n_rhs_exp in
let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in
let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in
IList.rev (IList.fold_left (execute_set_ pdesc tenv n_rhs_exp) [] iter_list)
IList.rev (IList.fold_left (execute_store_ pdesc tenv n_rhs_exp) [] iter_list)
with Rearrange.ARRAY_ACCESS ->
if (Config.array_level = 0) then assert false
else [prop_]
@ -1038,11 +1038,11 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let call_args prop_ proc_name args ret_ids loc = {
Builtin.pdesc = current_pdesc; instr; tenv; prop_; path; ret_ids; args; proc_name; loc; } in
match instr with
| Sil.Letderef (id, rhs_exp, typ, loc) ->
execute_letderef current_pname current_pdesc tenv id rhs_exp typ loc prop_
| Sil.Load (id, rhs_exp, typ, loc) ->
execute_load current_pname current_pdesc tenv id rhs_exp typ loc prop_
|> ret_old_path
| Sil.Set (lhs_exp, typ, rhs_exp, loc) ->
execute_set current_pname current_pdesc tenv lhs_exp typ rhs_exp loc prop_
| Sil.Store (lhs_exp, typ, 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 prop_ cond in
@ -1488,11 +1488,11 @@ and check_variadic_sentinel
(* IList.fold_left reverses the arguments *)
let non_terminal_argsi = fst (IList.fold_left mk_non_terminal_argsi ([], 0) args) in
let check_allocated result ((lexp, typ), i) =
(* simulate a Letderef for [lexp] *)
(* simulate a Load for [lexp] *)
let tmp_id_deref = Ident.create_fresh Ident.kprimed in
let letderef = Sil.Letderef (tmp_id_deref, lexp, typ, loc) in
let load_instr = Sil.Load (tmp_id_deref, lexp, typ, loc) in
try
instrs tenv pdesc [letderef] result
instrs tenv pdesc [load_instr] result
with e when SymOp.exn_not_failure e ->
if not fails_on_nil then
let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in
@ -1533,7 +1533,7 @@ and sym_exec_objc_getter field_name ret_typ tenv ret_ids pdesc pname loc args pr
| Typ.Tptr (t, _) -> Tenv.expand_type tenv t
| _ -> assert false) in
let field_access_exp = Exp.Lfield (lexp, field_name, typ') in
execute_letderef
execute_load
~report_deref_errors:false pname pdesc tenv ret_id field_access_exp ret_typ loc prop
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -1547,7 +1547,7 @@ and sym_exec_objc_setter field_name _ tenv _ pdesc pname loc args prop =
| Typ.Tptr (t, _) -> Tenv.expand_type tenv t
| _ -> assert false) in
let field_access_exp = Exp.Lfield (lexp1, field_name, typ1') in
execute_set ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop
execute_store ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
and sym_exec_objc_accessor property_accesor ret_typ tenv ret_ids pdesc _ loc args prop path

2
infer/src/checkers/BoundedCallTree.ml
Unescape View File

@ -144,7 +144,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
other potential special kinds of procedure calls to be added later,
e.g. Java reflection. *)
astate
| Sil.Letderef _ | Set _ | Prune _ | Declare_locals _
| Sil.Load _ | Store _ | Prune _ | Declare_locals _
| Stackop _ | Remove_temps _ | Abstract _ | Nullify _ ->
astate
end

4
infer/src/checkers/addressTaken.ml
Unescape View File

@ -37,14 +37,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate
let exec_instr astate _ _ = function
| Sil.Set (_, Tptr _, rhs_exp, _) ->
| Sil.Store (_, Tptr _, rhs_exp, _) ->
add_address_taken_pvars rhs_exp astate
| Sil.Call (_, _, actuals, _, _) ->
let add_actual_by_ref astate_acc = function
| actual_exp, Typ.Tptr _ -> add_address_taken_pvars actual_exp astate_acc
| _ -> astate_acc in
IList.fold_left add_actual_by_ref astate actuals
| Sil.Set _ | Letderef _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Stackop _
| Sil.Store _ | Load _ | Prune _ | Nullify _ | Abstract _ | Remove_temps _ | Stackop _
| Declare_locals _ ->
astate
end

6
infer/src/checkers/annotationReachability.ml
Unescape View File

@ -346,13 +346,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Some Domain.Bottom ->
astate
end
| Sil.Letderef (id, exp, _, _)
| Sil.Load (id, exp, _, _)
when is_tracking_exp astate exp ->
Domain.add_tracking_var (Var.of_id id) astate
| Sil.Set (Exp.Lvar pvar, _, exp, _)
| Sil.Store (Exp.Lvar pvar, _, exp, _)
when is_tracking_exp astate exp ->
Domain.add_tracking_var (Var.of_pvar pvar) astate
| Sil.Set (Exp.Lvar pvar, _, _, _) ->
| Sil.Store (Exp.Lvar pvar, _, _, _) ->
Domain.remove_tracking_var (Var.of_pvar pvar) astate
| Sil.Prune (exp, _, _, _)
when prunes_tracking_var astate exp ->

2
infer/src/checkers/checkTraceCallSequence.ml
Unescape View File

@ -276,7 +276,7 @@ module BooleanVars = struct
State.prune state name true
| None -> state in
state'
| Sil.Set (_e1, _, e2, _) ->
| Sil.Store (_e1, _, e2, _) ->
let e1 = Idenv.expand_expr idenv _e1 in
let state' = match exp_boolean_var e1 with
| Some name ->

16
infer/src/checkers/checkers.ml
Unescape View File

@ -427,11 +427,11 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p
match get_proc_desc proc_name' with
Some proc_desc' ->
let is_return_instr = function
| Sil.Set (Exp.Lvar p, _, _, _)
| Sil.Store (Exp.Lvar p, _, _, _)
when Pvar.equal p (Cfg.Procdesc.get_ret_var proc_desc') -> true
| _ -> false in
(match reverse_find_instr is_return_instr (Cfg.Procdesc.get_exit_node proc_desc') with
| Some (Sil.Set (_, _, Exp.Const (Const.Cclass n), _)) -> Ident.name_to_string n
| Some (Sil.Store (_, _, Exp.Const (Const.Cclass n), _)) -> Ident.name_to_string n
| _ -> "<" ^ (Procname.to_string proc_name') ^ ">")
| None -> "?" in
@ -444,11 +444,11 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p
| Exp.Const (Const.Cclass n) -> Ident.name_to_string n
| Exp.Lvar _ -> (
let is_call_instr set call = match set, call with
| Sil.Set (_, _, Exp.Var (i1), _), Sil.Call (i2::[], _, _, _, _)
| Sil.Store (_, _, Exp.Var (i1), _), Sil.Call (i2::[], _, _, _, _)
when Ident.equal i1 i2 -> true
| _ -> false in
let is_set_instr = function
| Sil.Set (e1, _, _, _) when Exp.equal expanded e1 -> true
| Sil.Store (e1, _, _, _) when Exp.equal expanded e1 -> true
| _ -> false in
match reverse_find_instr is_set_instr node with
(* Look for ivar := tmp *)
@ -523,9 +523,9 @@ let callback_check_field_access { Callbacks.proc_desc } =
let do_read_exp = do_exp true in
let do_write_exp = do_exp false in
let do_instr _ = function
| Sil.Letderef (_, e, _, _) ->
| Sil.Load (_, e, _, _) ->
do_read_exp e
| Sil.Set (e1, _, e2, _) ->
| Sil.Store (e1, _, e2, _) ->
do_write_exp e1;
do_read_exp e2
| Sil.Prune (e, _, _, _) ->
@ -590,9 +590,9 @@ let callback_print_access_to_globals { Callbacks.proc_desc; proc_name } =
| _ ->
None in
let do_instr _ = function
| Sil.Letderef (_, e, _, loc) when get_global_var e <> None ->
| Sil.Load (_, e, _, loc) when get_global_var e <> None ->
Option.may (fun pvar -> do_pvar true pvar loc) (get_global_var e)
| Sil.Set (e, _, _, loc) when get_global_var e <> None ->
| Sil.Store (e, _, _, loc) when get_global_var e <> None ->
Option.may (fun pvar -> do_pvar false pvar loc) (get_global_var e)
| _ -> () in
Cfg.Procdesc.iter_instrs do_instr proc_desc

6
infer/src/checkers/constantPropagation.ml
Unescape View File

@ -69,13 +69,13 @@ module ConstantFlow = Dataflow.MakeDF(struct
false in
match instr with
| Sil.Letderef (i, Exp.Lvar p, _, _) -> (* tmp = var *)
| Sil.Load (i, Exp.Lvar p, _, _) -> (* tmp = var *)
update (Exp.Var i) (ConstantMap.find (Exp.Lvar p) constants) constants
| Sil.Set (Exp.Lvar p, _, Exp.Const c, _) -> (* var = const *)
| Sil.Store (Exp.Lvar p, _, Exp.Const c, _) -> (* var = const *)
update (Exp.Lvar p) (Some c) constants
| Sil.Set (Exp.Lvar p, _, Exp.Var i, _) -> (* var = tmp *)
| Sil.Store (Exp.Lvar p, _, Exp.Var i, _) -> (* var = tmp *)
update (Exp.Lvar p) (ConstantMap.find (Exp.Var i) constants) constants
(* Handle propagation of string with StringBuilder. Does not handle null case *)

12
infer/src/checkers/copyPropagation.ml
Unescape View File

@ -84,17 +84,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
type extras = ProcData.no_extras
let exec_instr astate _ _ = function
| Sil.Letderef (lhs_id, Exp.Lvar rhs_pvar, _, _) when not (Pvar.is_global rhs_pvar) ->
| Sil.Load (lhs_id, Exp.Lvar rhs_pvar, _, _) when not (Pvar.is_global rhs_pvar) ->
Domain.gen (Var.of_id lhs_id) (Var.of_pvar rhs_pvar) astate
| Sil.Set (Exp.Lvar lhs_pvar, _, Exp.Var rhs_id, _) when not (Pvar.is_global lhs_pvar) ->
| Sil.Store (Exp.Lvar lhs_pvar, _, Exp.Var rhs_id, _) when not (Pvar.is_global lhs_pvar) ->
Domain.kill_then_gen (Var.of_pvar lhs_pvar) (Var.of_id rhs_id) astate
| Sil.Set (Exp.Lvar lhs_pvar, _, _, _) ->
| Sil.Store (Exp.Lvar lhs_pvar, _, _, _) ->
(* non-copy assignment; can only kill *)
Domain.kill_copies_with_var (Var.of_pvar lhs_pvar) astate
| Sil.Letderef _
| Sil.Load _
(* lhs = *rhs where rhs isn't a pvar (or is a global). in any case, not a copy *)
(* note: since logical vars can't be reassigned, don't need to kill bindings for lhs id *)
| Sil.Set (Var _, _, _, _) ->
| Sil.Store (Var _, _, _, _) ->
(* *lhs = rhs. not a copy, and not a write to lhs *)
astate
| Sil.Call (ret_ids, _, actuals, _, _) ->
@ -107,7 +107,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
if !Config.curr_language = Config.Java
then astate' (* Java doesn't have pass-by-reference *)
else IList.fold_left kill_actuals_by_ref astate' actuals
| Sil.Set _ | Sil.Prune _ | Sil.Nullify _ | Sil.Abstract _ | Sil.Remove_temps _
| Sil.Store _ | Sil.Prune _ | Sil.Nullify _ | Sil.Abstract _ | Sil.Remove_temps _
| Sil.Declare_locals _ | Sil.Stackop _ ->
(* none of these can assign to program vars or logical vars *)
astate

2
infer/src/checkers/dataflow.ml
Unescape View File

@ -54,7 +54,7 @@ let node_throws node (proc_throws : Procname.t -> throws) : throws =
let ret_pvar = Cfg.Procdesc.get_ret_var pdesc in
Pvar.equal pvar ret_pvar in
match instr with
| Sil.Set (Exp.Lvar pvar, _, Exp.Exn _, _) when is_return pvar ->
| Sil.Store (Exp.Lvar pvar, _, 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), _, _, _)

2
infer/src/checkers/idenv.ml
Unescape View File

@ -18,7 +18,7 @@ type t = (Exp.t Ident.IdentHash.t) Lazy.t
let create_ proc_desc =
let map = Ident.IdentHash.create 1 in
let do_instr _ = function
| Sil.Letderef (id, e, _, _) ->
| Sil.Load (id, e, _, _) ->
Ident.IdentHash.add map id e
| _ -> () in
Cfg.Procdesc.iter_instrs do_instr proc_desc;

6
infer/src/checkers/liveness.ml
Unescape View File

@ -31,16 +31,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
IList.fold_left (fun astate_acc pvar -> Domain.add (Var.of_pvar pvar) astate_acc) astate' pvars
let exec_instr astate _ _ = function
| Sil.Letderef (lhs_id, rhs_exp, _, _) ->
| Sil.Load (lhs_id, rhs_exp, _, _) ->
Domain.remove (Var.of_id lhs_id) astate
|> exp_add_live rhs_exp
| Sil.Set (Lvar lhs_pvar, _, rhs_exp, _) ->
| Sil.Store (Lvar lhs_pvar, _, rhs_exp, _) ->
let astate' =
if Pvar.is_global lhs_pvar
then astate (* never kill globals *)
else Domain.remove (Var.of_pvar lhs_pvar) astate in
exp_add_live rhs_exp astate'
| Sil.Set (lhs_exp, _, rhs_exp, _) ->
| Sil.Store (lhs_exp, _, rhs_exp, _) ->
exp_add_live lhs_exp astate
|> exp_add_live rhs_exp
| Sil.Prune (exp, _, _, _) ->

20
infer/src/checkers/patternMatch.ml
Unescape View File

@ -179,7 +179,7 @@ let get_vararg_type_names
let rec initializes_array instrs =
match instrs with
| Sil.Call ([t1], Exp.Const (Const.Cfun pn), _, _, _)::
Sil.Set (Exp.Lvar iv, _, Exp.Var t2, _):: is ->
Sil.Store (Exp.Lvar iv, _, Exp.Var t2, _):: is ->
(Pvar.equal ivar iv && Ident.equal t1 t2 &&
Procname.equal pn (Procname.from_string_c_fun "__new_array"))
|| initializes_array is
@ -190,24 +190,24 @@ let get_vararg_type_names
let added_type_name node =
let rec nvar_type_name nvar instrs =
match instrs with
| Sil.Letderef (nv, Exp.Lfield (_, id, t), _, _):: _
| Sil.Load (nv, Exp.Lfield (_, id, t), _, _):: _
when Ident.equal nv nvar -> get_field_type_name t id
| Sil.Letderef (nv, _, t, _):: _
| Sil.Load (nv, _, t, _):: _
when Ident.equal nv nvar ->
Some (get_type_name t)
| _:: is -> nvar_type_name nvar is
| _ -> None in
let rec added_nvar array_nvar instrs =
match instrs with
| Sil.Set (Exp.Lindex (Exp.Var iv, _), _, Exp.Var nvar, _):: _
| Sil.Store (Exp.Lindex (Exp.Var iv, _), _, Exp.Var nvar, _):: _
when Ident.equal iv array_nvar -> nvar_type_name nvar (Cfg.Node.get_instrs node)
| Sil.Set (Exp.Lindex (Exp.Var iv, _), _, Exp.Const c, _):: _
| Sil.Store (Exp.Lindex (Exp.Var iv, _), _, Exp.Const c, _):: _
when Ident.equal iv array_nvar -> Some (java_get_const_type_name c)
| _:: is -> added_nvar array_nvar is
| _ -> None in
let rec array_nvar instrs =
match instrs with
| Sil.Letderef (nv, Exp.Lvar iv, _, _):: _
| Sil.Load (nv, Exp.Lvar iv, _, _):: _
when Pvar.equal iv ivar ->
added_nvar nv instrs
| _:: is -> array_nvar is
@ -245,7 +245,7 @@ let is_setter pname_java =
(** Returns the signature of a field access (class name, field name, field type name) *)
let get_java_field_access_signature = function
| Sil.Letderef (_, Exp.Lfield (_, fn, ft), bt, _) ->
| Sil.Load (_, Exp.Lfield (_, fn, ft), bt, _) ->
Some (get_type_name bt, Ident.java_fieldname_get_field fn, get_type_name ft)
| _ -> None
@ -317,7 +317,7 @@ let method_is_initializer
let java_get_vararg_values node pvar idenv =
let values = ref [] in
let do_instr = function
| Sil.Set (Exp.Lindex (array_exp, _), _, content_exp, _)
| Sil.Store (Exp.Lindex (array_exp, _), _, content_exp, _)
when Exp.equal (Exp.Lvar pvar) (Idenv.expand_expr idenv array_exp) ->
(* Each vararg argument is an assigment to a pvar denoting an array of objects. *)
values := content_exp :: !values
@ -387,10 +387,10 @@ let proc_iter_overridden_methods f 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.Set (Exp.Lfield (Exp.Var lhs, fld, _), _, rhs, _)
| Sil.Store (Exp.Lfield (Exp.Var lhs, fld, _), _, rhs, _)
when Exp.is_null_literal rhs && Ident.IdentSet.mem lhs this_ids ->
(Ident.FieldSet.add fld nullified_flds, this_ids)
| Sil.Letderef (id, rhs, _, _) when Exp.is_this rhs ->
| Sil.Load (id, rhs, _, _) when Exp.is_this rhs ->
(nullified_flds, Ident.IdentSet.add id this_ids)
| _ -> (nullified_flds, this_ids) in
let (nullified_flds, _) =

4
infer/src/checkers/printfArgs.ml
Unescape View File

@ -158,7 +158,7 @@ let check_printf_args_ok
(* Get the array ivar for a given nvar *)
let rec array_ivar instrs nvar =
match instrs, nvar with
| Sil.Letderef (id, Exp.Lvar iv, _, _):: _, Exp.Var nid
| Sil.Load (id, Exp.Lvar iv, _, _):: _, Exp.Var nid
when Ident.equal id nid -> iv
| _:: is, _ -> array_ivar is nvar
| _ -> raise Not_found in
@ -167,7 +167,7 @@ let check_printf_args_ok
match nvar with
| Exp.Var nid -> (
match instrs with
| Sil.Letderef (id, Exp.Lvar _, t, _):: _
| Sil.Load (id, Exp.Lvar _, t, _):: _
when Ident.equal id nid -> PatternMatch.get_type_name t
| _:: is -> fixed_nvar_type_name is nvar
| _ -> raise Not_found)

44
infer/src/clang/cArithmetic_trans.ml
Unescape View File

@ -21,7 +21,7 @@ open CFrontend_utils
(* case we need to add proper retain/release.*)
(* See document: "Objective-C Automatic Reference Counting" describing the semantics *)
let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl =
let assign = Sil.Set (e1, typ, e2, loc) in
let assign = Sil.Store (e1, typ, e2, loc) in
let retain_pname = ModelBuiltins.__objc_retain in
let release_pname = ModelBuiltins.__objc_release in
let autorelease_pname = ModelBuiltins.__set_autorelease_attribute in
@ -34,7 +34,7 @@ let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl =
(* retain(e2); tmp=e1; e1=e2; release(tmp); *)
let retain = mk_call retain_pname e2 typ in
let id = Ident.create_fresh Ident.knormal in
let tmp_assign = Sil.Letderef(id, e1, typ, loc) in
let tmp_assign = Sil.Load (id, e1, typ, loc) in
let release = mk_call release_pname (Exp.Var id) typ in
(e1,[retain; tmp_assign; assign; release])
| Typ.Tptr (_, Typ.Pk_pointer) when not rhs_owning_method && is_e1_decl ->
@ -59,38 +59,38 @@ let assignment_arc_mode e1 typ e2 loc rhs_owning_method is_e1_decl =
(* assignment. *)
let compound_assignment_binary_operation_instruction boi e1 typ e2 loc =
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e1, typ, loc) in
let instr1 = Sil.Load (id, e1, typ, loc) in
let e_res, instr_op = match boi.Clang_ast_t.boi_kind with
| `AddAssign ->
let e1_plus_e2 = Exp.BinOp(Binop.PlusA, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_plus_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_plus_e2, loc)])
| `SubAssign ->
let e1_sub_e2 = Exp.BinOp(Binop.MinusA, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_sub_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_sub_e2, loc)])
| `MulAssign ->
let e1_mul_e2 = Exp.BinOp(Binop.Mult, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_mul_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_mul_e2, loc)])
| `DivAssign ->
let e1_div_e2 = Exp.BinOp(Binop.Div, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_div_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_div_e2, loc)])
| `ShlAssign ->
let e1_shl_e2 = Exp.BinOp(Binop.Shiftlt, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_shl_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_shl_e2, loc)])
| `ShrAssign ->
let e1_shr_e2 = Exp.BinOp(Binop.Shiftrt, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_shr_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_shr_e2, loc)])
| `RemAssign ->
let e1_mod_e2 = Exp.BinOp(Binop.Mod, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_mod_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_mod_e2, loc)])
| `AndAssign ->
let e1_and_e2 = Exp.BinOp(Binop.BAnd, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_and_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_and_e2, loc)])
| `OrAssign ->
let e1_or_e2 = Exp.BinOp(Binop.BOr, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_or_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_or_e2, loc)])
| `XorAssign ->
let e1_xor_e2 = Exp.BinOp(Binop.BXor, Exp.Var id, e2) in
(e1, [Sil.Set (e1, typ, e1_xor_e2, loc)])
(e1, [Sil.Store (e1, typ, e1_xor_e2, loc)])
| _ -> assert false in
(e_res, instr1:: instr_op)
@ -123,7 +123,7 @@ let binary_operation_instruction context boi e1 typ e2 loc rhs_owning_method =
if !Config.arc_mode && ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv typ then
assignment_arc_mode e1 typ e2 loc rhs_owning_method false
else
(e1, [Sil.Set (e1, typ, e2, loc)])
(e1, [Sil.Store (e1, typ, e2, loc)])
| `Comma -> (e2, []) (* C99 6.5.17-2 *)
| `MulAssign | `DivAssign | `RemAssign | `AddAssign | `SubAssign
| `ShlAssign | `ShrAssign | `AndAssign | `XorAssign | `OrAssign ->
@ -143,32 +143,32 @@ let unary_operation_instruction uoi e typ loc =
match uoi.Clang_ast_t.uoi_kind with
| `PostInc ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let instr1 = Sil.Load (id, e, typ, loc) in
let e_plus_1 = Exp.BinOp(Binop.PlusA, Exp.Var id, Exp.Const(Const.Cint (IntLit.one))) in
(Exp.Var id, instr1::[Sil.Set (e, typ, e_plus_1, loc)])
(Exp.Var id, instr1::[Sil.Store (e, typ, e_plus_1, loc)])
| `PreInc ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let instr1 = Sil.Load (id, e, typ, loc) in
let e_plus_1 = Exp.BinOp(Binop.PlusA, Exp.Var id, Exp.Const(Const.Cint (IntLit.one))) in
let exp = if General_utils.is_cpp_translation Config.clang_lang then
e
else
e_plus_1 in
(exp, instr1::[Sil.Set (e, typ, e_plus_1, loc)])
(exp, instr1::[Sil.Store (e, typ, e_plus_1, loc)])
| `PostDec ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let instr1 = Sil.Load (id, e, typ, loc) in
let e_minus_1 = Exp.BinOp(Binop.MinusA, Exp.Var id, Exp.Const(Const.Cint (IntLit.one))) in
(Exp.Var id, instr1::[Sil.Set (e, typ, e_minus_1, loc)])
(Exp.Var id, instr1::[Sil.Store (e, typ, e_minus_1, loc)])
| `PreDec ->
let id = Ident.create_fresh Ident.knormal in
let instr1 = Sil.Letderef (id, e, typ, loc) in
let instr1 = Sil.Load (id, e, typ, loc) in
let e_minus_1 = Exp.BinOp(Binop.MinusA, Exp.Var id, Exp.Const(Const.Cint (IntLit.one))) in
let exp = if General_utils.is_cpp_translation Config.clang_lang then
e
else
e_minus_1 in
(exp, instr1::[Sil.Set (e, typ, e_minus_1, loc)])
(exp, instr1::[Sil.Store (e, typ, e_minus_1, loc)])
| `Not -> (un_exp (Unop.BNot), [])
| `Minus -> (un_exp (Unop.Neg), [])
| `Plus -> (e, [])

30
infer/src/clang/cTrans.ml
Unescape View File

@ -147,14 +147,14 @@ struct
let block_var = Pvar.mk mblock procname in
let declare_block_local =
Sil.Declare_locals ([(block_var, Typ.Tptr (block_type, Typ.Pk_pointer))], loc) in
let set_instr = Sil.Set (Exp.Lvar block_var, block_type, Exp.Var id_block, loc) in
let set_instr = Sil.Store (Exp.Lvar block_var, block_type, Exp.Var id_block, loc) in
let create_field_exp (var, typ) =
let id = Ident.create_fresh Ident.knormal in
id, Sil.Letderef (id, Exp.Lvar var, typ, loc) in
id, Sil.Load (id, Exp.Lvar var, typ, loc) in
let ids, captured_instrs = IList.split (IList.map create_field_exp captured_vars) in
let fields_ids = IList.combine fields ids in
let set_fields = IList.map (fun ((f, t, _), id) ->
Sil.Set (Exp.Lfield (Exp.Var id_block, f, block_type), t, Exp.Var id, loc)) fields_ids in
Sil.Store (Exp.Lfield (Exp.Var id_block, f, block_type), t, Exp.Var id, loc)) fields_ids in
(declare_block_local :: trans_res.instrs) @
[set_instr] @
captured_instrs @
@ -169,7 +169,7 @@ struct
let bn''= Mangled.from_string bn' in
let block = Exp.Lvar (Pvar.mk bn'' procname) in
let id = Ident.create_fresh Ident.knormal in
insts := Sil.Letderef (id, block, typ, loc) :: !insts;
insts := Sil.Load (id, block, typ, loc) :: !insts;
(Exp.Var id, typ) in
let make_arg typ (id, _, _) = (id, typ) in
let rec f es =
@ -304,7 +304,7 @@ struct
(* equivalent of value of ret_param. Since ret_exp has type RETURN_TYPE,*)
(* we optionally add pointer there to avoid backend confusion. *)
(* It works either way *)
(* Passing by value: may cause problems - there needs to be extra Sil.Letderef, but*)
(* Passing by value: may cause problems - there needs to be extra Sil.Load, but*)
(* doing so would create problems with methods. Passing structs by*)
(* value doesn't work good anyway. This may need to be revisited later*)
let ret_param = (var_exp, param_type) in
@ -502,7 +502,7 @@ struct
(not is_constructor_init && CTypes.is_reference_type type_ptr) in
let exp, deref_instrs = if should_add_deref then
let id = Ident.create_fresh Ident.knormal in
let deref_instr = Sil.Letderef (id, field_exp, field_typ, sil_loc) in
let deref_instr = Sil.Load (id, field_exp, field_typ, sil_loc) in
Exp.Var id, [deref_instr]
else
field_exp, [] in
@ -540,7 +540,7 @@ struct
| [(exp, Typ.Tptr (typ, _) )] when decl_kind <> `CXXConstructor ->
let typ = CTypes.expand_structured_type context.tenv typ in
let no_id = Ident.create_none () in
let extra_instrs = [Sil.Letderef (no_id, exp, typ, sil_loc)] in
let extra_instrs = [Sil.Load (no_id, exp, typ, sil_loc)] in
pre_trans_result.exps, extra_instrs
| [(_, Typ.Tptr _ )] -> pre_trans_result.exps, []
| [(sil, typ)] -> [(sil, Typ.Tptr (typ, Typ.Pk_reference))], []
@ -805,7 +805,7 @@ struct
(* 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.Letderef (id, var_exp, var_exp_typ, sil_loc) in
let res_instr = Sil.Load (id, var_exp, var_exp_typ, sil_loc) in
[res_instr], Exp.Var id
) else (
[], exp_op) in
@ -1111,7 +1111,7 @@ struct
let (e', _) = extract_exp_from_list res_trans_b.exps
"\nWARNING: Missing branch expression for Conditional operator. Need to be fixed\n" in
let set_temp_var = [
Sil.Set (Exp.Lvar pvar, var_typ, e', sil_loc)
Sil.Store (Exp.Lvar pvar, var_typ, e', sil_loc)
] in
let tmp_var_res_trans = { empty_res_trans with instrs = set_temp_var } in
let trans_state'' = { trans_state' with succ_nodes = [join_node] } in
@ -1138,7 +1138,7 @@ struct
do_branch true exp1 var_typ res_trans_cond.leaf_nodes join_node pvar;
do_branch false exp2 var_typ res_trans_cond.leaf_nodes join_node pvar;
let id = Ident.create_fresh Ident.knormal in
let instrs = [Sil.Letderef (id, Exp.Lvar pvar, var_typ, sil_loc)] in
let instrs = [Sil.Load (id, Exp.Lvar pvar, var_typ, sil_loc)] in
{ empty_res_trans with
root_nodes = res_trans_cond.root_nodes;
leaf_nodes = [join_node];
@ -1620,7 +1620,7 @@ struct
else lh in
if IList.length rh_exps == IList.length lh then
(* Creating new instructions by assigning right hand side to left hand side expressions *)
let assign_instr (lh_exp, lh_t) (rh_exp, _) = Sil.Set (lh_exp, lh_t, rh_exp, sil_loc) in
let assign_instr (lh_exp, lh_t) (rh_exp, _) = Sil.Store (lh_exp, lh_t, rh_exp, sil_loc) in
let assign_instrs =
let initd_exps = collect_initid_exprs res_trans_subexpr_list in
(* If the variable var_exp is of type array, and some of its indices were initialized *)
@ -1684,7 +1684,7 @@ struct
var_exp ie_typ sil_e1' sil_loc rhs_owning_method true in
([(e, ie_typ)], instrs)
else
([], [Sil.Set (var_exp, ie_typ, sil_e1', sil_loc)]) in
([], [Sil.Store (var_exp, ie_typ, sil_e1', sil_loc)]) in
let res_trans_assign = { empty_res_trans with
instrs = instrs_assign } in
let all_res_trans = [res_trans_ie; res_trans_assign] in
@ -1881,7 +1881,7 @@ struct
let procname = Cfg.Procdesc.get_proc_name procdesc in
let pvar = Pvar.mk (Mangled.from_string name) procname in
let id = Ident.create_fresh Ident.knormal in
let instr = Sil.Letderef (id, Exp.Lvar pvar, ret_param_typ, sil_loc) in
let instr = Sil.Load (id, Exp.Lvar pvar, ret_param_typ, sil_loc) in
let ret_typ = match ret_param_typ with Typ.Tptr (t, _) -> t | _ -> assert false in
Exp.Var id, ret_typ, [instr]
| None ->
@ -1895,7 +1895,7 @@ struct
let ret_instrs = if IList.exists (Exp.equal ret_exp) res_trans_stmt.initd_exps
then []
else [Sil.Set (ret_exp, ret_type, sil_expr, sil_loc)] in
else [Sil.Store (ret_exp, ret_type, sil_expr, sil_loc)] in
let autorelease_instrs =
add_autorelease_call context sil_expr ret_type sil_loc in
let instrs = var_instrs @ res_trans_stmt.instrs @ ret_instrs @ autorelease_instrs in
@ -2009,7 +2009,7 @@ struct
(* Given a captured var, return the instruction to assign it to a temp *)
let assign_captured_var (cvar, typ) =
let id = Ident.create_fresh Ident.knormal in
let instr = Sil.Letderef (id, (Exp.Lvar cvar), typ, loc) in
let instr = Sil.Load (id, (Exp.Lvar cvar), typ, loc) in
(id, instr) in
match decl with
| Clang_ast_t.BlockDecl (_, block_decl_info) ->

6
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -389,7 +389,7 @@ let cast_trans context exps sil_loc function_type pname =
let dereference_var_sil (exp, typ) sil_loc =
let id = Ident.create_fresh Ident.knormal in
let sil_instr = Sil.Letderef (id, exp, typ, sil_loc) in
let sil_instr = Sil.Load (id, exp, typ, sil_loc) in
([sil_instr], Exp.Var id)
(** Given trans_result with ONE expression, create temporary variable with value of an expression
@ -491,7 +491,7 @@ let define_condition_side_effects e_cond instrs_cond sil_loc =
| Exp.Lvar pvar ->
let id = Ident.create_fresh Ident.knormal in
[(Exp.Var id, typ)],
[Sil.Letderef (id, Exp.Lvar pvar, typ, sil_loc)]
[Sil.Load (id, Exp.Lvar pvar, typ, sil_loc)]
| _ -> [(e', typ)], instrs_cond
let fix_param_exps_mismatch params_stmt exps_param =
@ -571,7 +571,7 @@ struct
context.CContext.tenv context.CContext.curr_class) 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.Letderef (id, e, t', loc)] in
t', Exp.Var id, [Sil.Load (id, e, t', loc)] in
{ empty_res_trans with
exps = [(self_expr, typ)];
instrs = ins }

10
infer/src/eradicate/typeCheck.ml
Unescape View File

@ -476,16 +476,16 @@ let typecheck_instr
| Sil.Declare_locals _
| Sil.Abstract _
| Sil.Nullify _ -> typestate
| Sil.Letderef (id, e, typ, loc) ->
| Sil.Load (id, e, 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.Set (Exp.Lvar pvar, _, Exp.Exn _, _) when is_return pvar ->
| Sil.Store (Exp.Lvar pvar, _, Exp.Exn _, _) when is_return pvar ->
(* skip assignment to return variable where it is an artifact of a throw instruction *)
typestate
| Sil.Set (e1, typ, e2, loc) ->
| Sil.Store (e1, 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 () = match e1 with
@ -1036,7 +1036,7 @@ let typecheck_instr
| [prev_node] ->
let found = ref None in
let do_instr i = match i with
| Sil.Set (e, _, e', _)
| Sil.Store (e, _, e', _)
when Exp.equal (Exp.Lvar pvar) (Idenv.expand_expr idenv e') ->
found := Some e
| _ -> () in
@ -1091,7 +1091,7 @@ let typecheck_node
| None -> false in
if has_exceptions then
typestates_exn := typestate :: !typestates_exn
| Sil.Set (Exp.Lvar pv, _, _, _) when
| Sil.Store (Exp.Lvar pv, _, _, _) when
Pvar.is_return pv &&
Cfg.Node.get_kind node = Cfg.Node.throw_kind ->
(* throw instruction *)

4
infer/src/harness/inhabit.ml
Unescape View File

@ -125,10 +125,10 @@ let rec inhabit_typ typ cfg env =
let fresh_local_exp =
Exp.Lvar (Pvar.mk typ_class_name (Procname.Java env.harness_name)) in
let write_to_local_instr =
Sil.Set (fresh_local_exp, ptr_to_typ, allocated_obj_exp, env.pc) in
Sil.Store (fresh_local_exp, ptr_to_typ, allocated_obj_exp, env.pc) in
let env' = env_add_instr write_to_local_instr env in
let fresh_id = Ident.create_fresh Ident.knormal in
let read_from_local_instr = Sil.Letderef (fresh_id, fresh_local_exp, ptr_to_typ, env'.pc) in
let read_from_local_instr = Sil.Load (fresh_id, fresh_local_exp, ptr_to_typ, env'.pc) in
(Exp.Var fresh_id, env_add_instr read_from_local_instr env')
| Typ.Tint (_) -> (Exp.Const (Const.Cint (IntLit.zero)), env)
| Typ.Tfloat (_) -> (Exp.Const (Const.Cfloat 0.0), env)

39
infer/src/java/jTrans.ml
Unescape View File

@ -405,7 +405,7 @@ let builtin_get_array_length =
let create_sil_deref exp typ loc =
let no_id = Ident.create_none () in
Sil.Letderef (no_id, exp, typ, loc)
Sil.Load (no_id, exp, typ, loc)
(** translate an expression used as an r-value *)
let rec expression context pc expr =
@ -417,7 +417,7 @@ let rec expression context 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.Letderef (id, Exp.Lvar pvar, type_of_expr, loc) in
let sil_instr = Sil.Load (id, Exp.Lvar pvar, type_of_expr, loc) in
([sil_instr], Exp.Var id, type_of_expr) in
match expr with
| JBir.Var (_, var) ->
@ -482,9 +482,9 @@ let rec expression context pc expr =
let array_typ = Typ.Tarray (type_of_expr, None) in
let deref_array_instr = create_sil_deref sil_ex1 array_typ loc in
let id = Ident.create_fresh Ident.knormal in
let letderef_instr =
Sil.Letderef (id, Exp.Lindex (sil_ex1, sil_ex2), type_of_expr, loc) in
let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [letderef_instr] in
let load_instr =
Sil.Load (id, Exp.Lindex (sil_ex1, sil_ex2), type_of_expr, loc) in
let instrs = (instrs1 @ (deref_array_instr :: instrs2)) @ [load_instr] in
instrs, Exp.Var id, type_of_expr
| other_binop ->
let sil_binop = get_binop other_binop in
@ -497,7 +497,7 @@ let rec expression context 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.Letderef (tmp_id, sil_expr, sil_type, loc) in
let lderef_instr = Sil.Load (tmp_id, sil_expr, sil_type, loc) in
(instrs @ [lderef_instr], Exp.Var tmp_id, type_of_expr)
| JBir.StaticField (cn, fs) ->
let class_exp =
@ -529,7 +529,7 @@ let rec expression context 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.Letderef (tmp_id, sil_expr, sil_type, loc) in
let lderef_instr = Sil.Load (tmp_id, sil_expr, sil_type, loc) in
(instrs @ [lderef_instr], Exp.Var tmp_id, type_of_expr)
let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_code method_kind =
@ -601,7 +601,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
let call_ret_instrs sil_var =
let ret_id = Ident.create_fresh Ident.knormal in
let call_instr = Sil.Call ([ret_id], callee_fun, call_args, loc, call_flags) in
let set_instr = Sil.Set (Exp.Lvar sil_var, return_type, Exp.Var ret_id, loc) in
let set_instr = Sil.Store (Exp.Lvar sil_var, return_type, Exp.Var ret_id, loc) in
(instrs @ [call_instr; set_instr]) in
match var_opt with
| None ->
@ -806,7 +806,7 @@ let rec instruction context pc instr : translation =
| JBir.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.Set (Exp.Lvar pvar, sil_type, sil_expr, loc) in
let sil_instr = Sil.Store (Exp.Lvar pvar, sil_type, sil_expr, loc) in
let node_kind = Cfg.Node.Stmt_node "method_body" in
let node = create_node node_kind (stml @ [sil_instr]) in
Instr node
@ -819,7 +819,7 @@ let rec instruction context pc instr : translation =
| Some expr ->
let (stml, sil_expr, _) = expression context pc expr in
let sil_instrs =
let return_instr = Sil.Set (Exp.Lvar ret_var, ret_type, sil_expr, loc) in
let return_instr = Sil.Store (Exp.Lvar ret_var, ret_type, sil_expr, loc) in
if return_not_null () then
[assume_not_null loc sil_expr; return_instr]
else
@ -833,7 +833,8 @@ let rec instruction context pc instr : translation =
and (instrs_value, sil_expr_value, _) = expression context pc value_ex in
let arr_type_np = JTransType.extract_cn_type_np arr_type in
let sil_instr =
Sil.Set (Exp.Lindex (sil_expr_array, sil_expr_index), arr_type_np, sil_expr_value, loc) in
Sil.Store (
Exp.Lindex (sil_expr_array, sil_expr_index), arr_type_np, sil_expr_value, loc) in
let final_instrs = instrs_array @ instrs_index @ instrs_value @ [sil_instr] in
let node_kind = Cfg.Node.Stmt_node "method_body" in
let node = create_node node_kind final_instrs in
@ -845,7 +846,7 @@ let rec instruction context 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.Set (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in
let sil_instr = Sil.Store (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in
let node_kind = Cfg.Node.Stmt_node "method_body" in
let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in
Instr node
@ -860,7 +861,7 @@ let rec instruction context 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.Set (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in
let sil_instr = Sil.Store (expr_off, type_of_the_root_of_e_lhs, sil_expr_rhs, loc) in
let node_kind = Cfg.Node.Stmt_node "method_body" in
let node = create_node node_kind (stml1 @ stml2 @ [sil_instr]) in
Instr node
@ -892,7 +893,7 @@ let rec instruction context pc instr : translation =
| JBir.Throw expr ->
let (instrs, sil_expr, _) = expression context pc expr in
let sil_exn = Exp.Exn sil_expr in
let sil_instr = Sil.Set (Exp.Lvar ret_var, ret_type, sil_exn, loc) in
let sil_instr = Sil.Store (Exp.Lvar ret_var, ret_type, sil_exn, loc) in
let node = create_node Cfg.Node.throw_kind (instrs @ [sil_instr]) in
JContext.add_goto_jump context pc JContext.Exit;
Instr node
@ -910,7 +911,7 @@ let rec instruction context pc instr : translation =
method_invocation
context loc pc None cn constr_ms ret_opt constr_arg_list I_Special Procname.Non_Static in
let pvar = JContext.set_pvar context var class_type in
let set_instr = Sil.Set (Exp.Lvar pvar, class_type, Exp.Var ret_id, loc) in
let set_instr = Sil.Store (Exp.Lvar pvar, class_type, Exp.Var ret_id, loc) in
let instrs = (new_instr :: call_instrs) @ [set_instr] in
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string constr_procname)) in
let node = create_node node_kind instrs in
@ -926,7 +927,7 @@ let rec instruction context pc instr : translation =
let call_args = [(array_size, array_type)] in
let ret_id = Ident.create_fresh Ident.knormal in
let call_instr = Sil.Call([ret_id], builtin_new_array, call_args, loc, CallFlags.default) in
let set_instr = Sil.Set (Exp.Lvar array_name, array_type, Exp.Var ret_id, loc) in
let set_instr = Sil.Store (Exp.Lvar array_name, array_type, Exp.Var ret_id, loc) in
let node_kind = Cfg.Node.Stmt_node "method_body" in
let node = create_node node_kind (instrs @ [call_instr; set_instr]) in
Instr node
@ -1023,7 +1024,7 @@ let rec instruction context pc instr : translation =
let ret_opt = Some (Exp.Var ret_id, class_type) in
method_invocation context loc pc None npe_cn constr_ms ret_opt [] I_Special Procname.Static in
let sil_exn = Exp.Exn (Exp.Var ret_id) in
let set_instr = Sil.Set (Exp.Lvar ret_var, ret_type, sil_exn, loc) in
let set_instr = Sil.Store (Exp.Lvar ret_var, ret_type, 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
Prune (not_null_node, throw_npe_node)
@ -1077,7 +1078,7 @@ let rec instruction context pc instr : translation =
context loc pc None out_of_bound_cn constr_ms
(Some (Exp.Var ret_id, class_type)) [] I_Special Procname.Static in
let sil_exn = Exp.Exn (Exp.Var ret_id) in
let set_instr = Sil.Set (Exp.Lvar ret_var, ret_type, sil_exn, loc) in
let set_instr = Sil.Store (Exp.Lvar ret_var, ret_type, sil_exn, loc) in
let out_of_bound_instrs =
instrs @ [sil_assume_out_of_bound] @ (new_instr :: call_instrs) @ [set_instr] in
create_node out_of_bound_node_kind out_of_bound_instrs in
@ -1115,7 +1116,7 @@ let rec instruction context pc instr : translation =
method_invocation context loc pc None cce_cn constr_ms
(Some (Exp.Var ret_id, class_type)) [] I_Special Procname.Static in
let sil_exn = Exp.Exn (Exp.Var ret_id) in
let set_instr = Sil.Set (Exp.Lvar ret_var, ret_type, sil_exn, loc) in
let set_instr = Sil.Store (Exp.Lvar ret_var, ret_type, sil_exn, loc) in
let cce_instrs =
instrs @ [call; asssume_not_instance_of] @ (new_instr :: call_instrs) @ [set_instr] in
create_node throw_cast_exception_kind cce_instrs in

8
infer/src/java/jTransExn.ml
Unescape View File

@ -38,9 +38,9 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table =
(* 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.Letderef (id_ret_val, Exp.Lvar ret_var, ret_type, loc) in
let instr_get_ret_val = Sil.Load (id_ret_val, Exp.Lvar ret_var, ret_type, loc) in
let id_deactivate = Ident.create_fresh Ident.knormal in
let instr_deactivate_exn = Sil.Set (Exp.Lvar ret_var, ret_type, Exp.Var id_deactivate, loc) in
let instr_deactivate_exn = Sil.Store (Exp.Lvar ret_var, ret_type, Exp.Var id_deactivate, loc) in
let instr_unwrap_ret_val =
let unwrap_builtin = Exp.Const (Const.Cfun ModelBuiltins.__unwrap_exception) in
Sil.Call
@ -79,9 +79,9 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table =
Sil.Prune (Exp.UnOp(Unop.LNot, Exp.Var id_instanceof, None), loc, false, if_kind) in
let instr_set_catch_var =
let catch_var = JContext.set_pvar context handler.JBir.e_catch_var ret_type in
Sil.Set (Exp.Lvar catch_var, ret_type, Exp.Var id_exn_val, loc) in
Sil.Store (Exp.Lvar catch_var, ret_type, Exp.Var id_exn_val, loc) in
let instr_rethrow_exn =
Sil.Set (Exp.Lvar ret_var, ret_type, Exp.Exn (Exp.Var id_exn_val), loc) in
Sil.Store (Exp.Lvar ret_var, ret_type, Exp.Exn (Exp.Var id_exn_val), loc) in
let node_kind_true = Cfg.Node.Prune_node (true, if_kind, exn_message) in
let node_kind_false = Cfg.Node.Prune_node (false, if_kind, exn_message) in
let node_true =

6
infer/src/llvm/lTrans.ml
Unescape View File

@ -73,15 +73,15 @@ let rec trans_annotated_instructions
let procname = Cfg.Procdesc.get_proc_name procdesc in
let ret_var = Pvar.get_ret_pvar procname in
let new_sil_instr =
Sil.Set (Exp.Lvar ret_var, trans_typ tp, trans_operand exp, location) in
Sil.Store (Exp.Lvar ret_var, trans_typ tp, trans_operand exp, location) in
(new_sil_instr :: sil_instrs, locals)
| Load (var, tp, ptr) ->
let new_sil_instr =
Sil.Letderef (ident_of_variable var, trans_variable ptr, trans_typ tp, location) in
Sil.Load (ident_of_variable var, trans_variable ptr, trans_typ tp, location) in
(new_sil_instr :: sil_instrs, locals)
| Store (op, tp, var) ->
let new_sil_instr =
Sil.Set (trans_variable var, trans_typ tp, trans_operand op, location) in
Sil.Store (trans_variable var, trans_typ tp, trans_operand op, location) in
(new_sil_instr :: sil_instrs, locals)
| Alloc (var, tp, _num_elems) ->
(* num_elems currently ignored *)

4
infer/src/quandary/TaintAnalysis.ml
Unescape View File

@ -146,9 +146,9 @@ module Make (TraceDomain : Trace.S) = struct
let exec_instr ({ Domain.id_map; } as astate) proc_data _ instr =
let f_resolve_id = resolve_id id_map in
match instr with
| Sil.Letderef (lhs_id, rhs_exp, rhs_typ, _) ->
| Sil.Load (lhs_id, rhs_exp, rhs_typ, _) ->
analyze_id_assignment lhs_id rhs_exp rhs_typ astate
| Sil.Set (lhs_exp, lhs_typ, rhs_exp, loc) ->
| Sil.Store (lhs_exp, lhs_typ, rhs_exp, loc) ->
let lhs_access_path =
match AccessPath.of_exp lhs_exp lhs_typ ~f_resolve_id with
| Some access_path ->

2
infer/src/unit/TaintTests.ml
Unescape View File

@ -121,7 +121,7 @@ let tests =
let rhs_exp = Exp.Var (ident_of_str rhs_id_str) in
make_store ~rhs_typ:Typ.Tvoid (Exp.Var (ident_of_str root_str)) fld_str ~rhs_exp in
let read_field_to_id lhs_id_str root_str fld_str =
make_load ~rhs_typ:Typ.Tvoid lhs_id_str fld_str (Exp.Var (ident_of_str root_str)) in
make_load_fld ~rhs_typ:Typ.Tvoid lhs_id_str fld_str (Exp.Var (ident_of_str root_str)) in
let assert_empty = invariant "{ }" in
let test_list = [
"source recorded",

4
infer/src/unit/addressTakenTests.ml
Unescape View File

@ -39,12 +39,12 @@ let tests =
var_assign_addrof_var ~rhs_typ:int_typ "a" "b";
assert_empty
];
"address_not_taken_letderef_instr1",
"address_not_taken_load_instr1",
[
id_assign_var ~rhs_typ:int_ptr_typ "a" "b";
assert_empty
];
"address_not_taken_letderef_instr2",
"address_not_taken_load_instr2",
[
id_assign_var ~rhs_typ:int_typ "a" "b";
assert_empty

14
infer/src/unit/analyzerTester.ml
Unescape View File

@ -84,11 +84,11 @@ module StructuredSil = struct
let unknown_exp =
var_of_str "__unknown__"
let make_letderef ~rhs_typ lhs_id rhs_exp =
Cmd (Sil.Letderef (lhs_id, rhs_exp, rhs_typ, dummy_loc))
let make_load ~rhs_typ lhs_id rhs_exp =
Cmd (Sil.Load (lhs_id, rhs_exp, rhs_typ, dummy_loc))
let make_set ~rhs_typ ~lhs_exp ~rhs_exp =
Cmd (Sil.Set (lhs_exp, rhs_typ, rhs_exp, dummy_loc))
Cmd (Sil.Store (lhs_exp, rhs_typ, rhs_exp, dummy_loc))
let make_call ?(procname=dummy_procname) ret_ids args =
let call_exp = Exp.Const (Const.Cfun procname) in
@ -99,14 +99,14 @@ module StructuredSil = struct
let lhs_exp = Exp.Lfield (root_exp, fld, rhs_typ) in
make_set ~rhs_typ ~lhs_exp ~rhs_exp
let make_load ~rhs_typ lhs_str fld_str root_exp =
let make_load_fld ~rhs_typ lhs_str fld_str root_exp =
let fld = AccessPathTestUtils.make_fieldname fld_str in
let rhs_exp = Exp.Lfield (root_exp, fld, rhs_typ) in
make_letderef ~rhs_typ (ident_of_str lhs_str) rhs_exp
make_load ~rhs_typ (ident_of_str lhs_str) rhs_exp
let id_assign_exp ?(rhs_typ=dummy_typ) lhs rhs_exp =
let lhs_id = ident_of_str lhs in
make_letderef ~rhs_typ lhs_id rhs_exp
make_load ~rhs_typ lhs_id rhs_exp
let id_assign_id ?(rhs_typ=dummy_typ) lhs rhs =
id_assign_exp ~rhs_typ lhs (Exp.Var (ident_of_str rhs))
@ -114,7 +114,7 @@ module StructuredSil = struct
let id_assign_var ?(rhs_typ=dummy_typ) lhs rhs =
let lhs_id = ident_of_str lhs in
let rhs_exp = var_of_str rhs in
make_letderef ~rhs_typ lhs_id rhs_exp
make_load ~rhs_typ lhs_id rhs_exp
let id_set_id ?(rhs_typ=dummy_typ) lhs_id rhs_id =
let lhs_exp = Exp.Var (ident_of_str lhs_id) in

2
infer/src/unit/copyPropagationTests.ml
Unescape View File

@ -21,7 +21,7 @@ let tests =
let open AnalyzerTester.StructuredSil in
let assert_empty = invariant "{ }" in
let test_list = [
"id_letderef_id_no_gen",
"id_load_id_no_gen",
[
id_assign_id "b" "a"; (* means b = *a *)
assert_empty

4
infer/src/unit/livenessTests.ml
Unescape View File

@ -60,12 +60,12 @@ let tests =
invariant "{ &b }";
id_assign_var "a" "b"
];
"basic_live_letderef",
"basic_live_load",
[
invariant "{ y$0 }";
id_assign_id "x" "y"
];
"basic_live_then_kill_letderef",
"basic_live_then_kill_load",
[
invariant "{ z$0 }";
id_assign_id "y" "z";

Write Preview
Loading…
Cancel
Save