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

Refactor Exp.t-keyed collections from Sil to Exp

Browse Source 
Reviewed By: cristianoc

Differential Revision: D3669397

fbshipit-source-id: cb90abc
master
Josh Berdine 8 years ago committed by Facebook Github Bot 8
parent d60965824e
commit f9ca08a9a8
15 changed files with 129 additions and 148 deletions
Show Stats Download Patch File Download Diff File

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

@ -87,7 +87,7 @@ let module Node = {
let pdescs_eq pd1 pd2 => let pdescs_eq pd1 pd2 =>
/* map of exp names in pd1 -> exp names in pd2 */ /* map of exp names in pd1 -> exp names in pd2 */
{ {
let exp_map = ref Sil.ExpMap.empty; let exp_map = ref Exp.Map.empty;
/* map of node id's in pd1 -> node id's in pd2 */ /* map of node id's in pd1 -> node id's in pd2 */
let id_map = ref IntMap.empty; let id_map = ref IntMap.empty;
/* formals are the same if their types are the same */ /* formals are the same if their types are the same */
@ -906,8 +906,8 @@ let remove_abducted_retvars p =>
let (sigma, pi) = (Prop.get_sigma p, Prop.get_pi p); let (sigma, pi) = (Prop.get_sigma p, Prop.get_pi p);
let rec collect_exps exps => let rec collect_exps exps =>
fun fun
| Sil.Eexp (Exp.Exn e) _ => Sil.ExpSet.add e exps | Sil.Eexp (Exp.Exn e) _ => Exp.Set.add e exps
| Sil.Eexp e _ => Sil.ExpSet.add e exps | Sil.Eexp e _ => Exp.Set.add e exps
| Sil.Estruct flds _ => | Sil.Estruct flds _ =>
IList.fold_left (fun exps (_, strexp) => collect_exps exps strexp) exps flds IList.fold_left (fun exps (_, strexp) => collect_exps exps strexp) exps flds
| Sil.Earray _ elems _ => | Sil.Earray _ elems _ =>
@ -915,7 +915,7 @@ let remove_abducted_retvars p =>
let rec compute_reachable_hpreds_rec sigma (reach, exps) => { let rec compute_reachable_hpreds_rec sigma (reach, exps) => {
let add_hpred_if_reachable (reach, exps) => let add_hpred_if_reachable (reach, exps) =>
fun fun
| Sil.Hpointsto lhs rhs _ as hpred when Sil.ExpSet.mem lhs exps => { | Sil.Hpointsto lhs rhs _ as hpred when Exp.Set.mem lhs exps => {
let reach' = Sil.HpredSet.add hpred reach; let reach' = Sil.HpredSet.add hpred reach;
let exps' = collect_exps exps rhs; let exps' = collect_exps exps rhs;
(reach', exps') (reach', exps')
@ -924,14 +924,14 @@ let remove_abducted_retvars p =>
let reach' = Sil.HpredSet.add hpred reach; let reach' = Sil.HpredSet.add hpred reach;
let exps' = let exps' =
IList.fold_left IList.fold_left
(fun exps_acc exp => Sil.ExpSet.add exp exps_acc) exps [exp1, exp2, ...exp_l]; (fun exps_acc exp => Exp.Set.add exp exps_acc) exps [exp1, exp2, ...exp_l];
(reach', exps') (reach', exps')
} }
| Sil.Hdllseg _ _ exp1 exp2 exp3 exp4 exp_l as hpred => { | Sil.Hdllseg _ _ exp1 exp2 exp3 exp4 exp_l as hpred => {
let reach' = Sil.HpredSet.add hpred reach; let reach' = Sil.HpredSet.add hpred reach;
let exps' = let exps' =
IList.fold_left IList.fold_left
(fun exps_acc exp => Sil.ExpSet.add exp exps_acc) (fun exps_acc exp => Exp.Set.add exp exps_acc)
exps exps
[exp1, exp2, exp3, exp4, ...exp_l]; [exp1, exp2, exp3, exp4, ...exp_l];
(reach', exps') (reach', exps')
@ -950,7 +950,7 @@ let remove_abducted_retvars p =>
let reach_pi = { let reach_pi = {
let rec exp_contains = let rec exp_contains =
fun fun
| exp when Sil.ExpSet.mem exp reach_exps => true | exp when Exp.Set.mem exp reach_exps => true
| Exp.UnOp _ e _ | Exp.UnOp _ e _
| Exp.Cast _ e | Exp.Cast _ e
| Exp.Lfield e _ _ => exp_contains e | Exp.Lfield e _ _ => exp_contains e
@ -990,8 +990,8 @@ let remove_abducted_retvars p =>
let (_, p') = Prop.deallocate_stack_vars p abducteds; let (_, p') = Prop.deallocate_stack_vars p abducteds;
let normal_pvar_set = let normal_pvar_set =
IList.fold_left IList.fold_left
(fun normal_pvar_set pvar => Sil.ExpSet.add (Exp.Lvar pvar) normal_pvar_set) (fun normal_pvar_set pvar => Exp.Set.add (Exp.Lvar pvar) normal_pvar_set)
Sil.ExpSet.empty Exp.Set.empty
normal_pvars; normal_pvars;
/* walk forward from non-abducted pvars, keep everything reachable. remove everything else */ /* walk forward from non-abducted pvars, keep everything reachable. remove everything else */
let (sigma_reach, pi_reach) = compute_reachable p' normal_pvar_set; let (sigma_reach, pi_reach) = compute_reachable p' normal_pvar_set;

18
infer/src/IR/Exp.re
Unescape View File

@ -167,3 +167,21 @@ let rec compare e1 e2 =>
}; };
let equal e1 e2 => compare e1 e2 == 0; let equal e1 e2 => compare e1 e2 == 0;
let hash = Hashtbl.hash;
let module Set = Set.Make {
type nonrec t = t;
let compare = compare;
};
let module Map = Map.Make {
type nonrec t = t;
let compare = compare;
};
let module Hash = Hashtbl.Make {
type nonrec t = t;
let equal = equal;
let hash = hash;
};

16
infer/src/IR/Exp.rei
Unescape View File

@ -58,3 +58,19 @@ let compare: t => t => int;
/** Equality for expressions. */ /** Equality for expressions. */
let equal: t => t => bool; let equal: t => t => bool;
/** Hash function for expressions. */
let hash: t => int;
/** Set of expressions. */
let module Set: Set.S with type elt = t;
/** Map with expression keys. */
let module Map: Map.S with type key = t;
/** Hashtable with expression keys. */
let module Hash: Hashtbl.S with type key = t;

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

@ -762,17 +762,7 @@ let hpara_dll_equal hpara1 hpara2 => hpara_dll_compare hpara1 hpara2 == 0;
/** {2 Sets of expressions} */ /** {2 Sets of expressions} */
let module ExpSet = Set.Make { let elist_to_eset es => IList.fold_left (fun set e => Exp.Set.add e set) Exp.Set.empty es;
type t = Exp.t;
let compare = Exp.compare;
};
let module ExpMap = Map.Make {
type t = Exp.t;
let compare = Exp.compare;
};
let elist_to_eset es => IList.fold_left (fun set e => ExpSet.add e set) ExpSet.empty es;
/** {2 Sets of heap predicates} */ /** {2 Sets of heap predicates} */
@ -2823,12 +2813,12 @@ let instr_compare instr1 instr2 =>
let rec exp_compare_structural e1 e2 exp_map => { let rec exp_compare_structural e1 e2 exp_map => {
let compare_exps_with_map e1 e2 exp_map => let compare_exps_with_map e1 e2 exp_map =>
try { try {
let e1_mapping = ExpMap.find e1 exp_map; let e1_mapping = Exp.Map.find e1 exp_map;
(Exp.compare e1_mapping e2, exp_map) (Exp.compare e1_mapping e2, exp_map)
} { } {
| Not_found => | Not_found =>
/* assume e1 and e2 equal, enforce by adding to [exp_map] */ /* assume e1 and e2 equal, enforce by adding to [exp_map] */
(0, ExpMap.add e1 e2 exp_map) (0, Exp.Map.add e1 e2 exp_map)
}; };
switch (e1: Exp.t, e2: Exp.t) { switch (e1: Exp.t, e2: Exp.t) {
| (Var _, Var _) => compare_exps_with_map e1 e2 exp_map | (Var _, Var _) => compare_exps_with_map e1 e2 exp_map
@ -3106,30 +3096,24 @@ let hpred_replace_exp epairs =>
/** {2 Compaction} */ /** {2 Compaction} */
let module ExpHash = Hashtbl.Make {
type t = Exp.t;
let equal = Exp.equal;
let hash = Hashtbl.hash;
};
let module HpredHash = Hashtbl.Make { let module HpredHash = Hashtbl.Make {
type t = hpred; type t = hpred;
let equal = hpred_equal; let equal = hpred_equal;
let hash = Hashtbl.hash; let hash = Hashtbl.hash;
}; };
type sharing_env = {exph: ExpHash.t Exp.t, hpredh: HpredHash.t hpred}; type sharing_env = {exph: Exp.Hash.t Exp.t, hpredh: HpredHash.t hpred};
/** Create a sharing env to store canonical representations */ /** Create a sharing env to store canonical representations */
let create_sharing_env () => {exph: ExpHash.create 3, hpredh: HpredHash.create 3}; let create_sharing_env () => {exph: Exp.Hash.create 3, hpredh: HpredHash.create 3};
/** Return a canonical representation of the exp */ /** Return a canonical representation of the exp */
let exp_compact sh e => let exp_compact sh e =>
try (ExpHash.find sh.exph e) { try (Exp.Hash.find sh.exph e) {
| Not_found => | Not_found =>
ExpHash.add sh.exph e e; Exp.Hash.add sh.exph e e;
e e
}; };

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

@ -103,20 +103,8 @@ type attribute =
| Aunsubscribed_observer; | Aunsubscribed_observer;
/** Sets of expressions. */
let module ExpSet: Set.S with type elt = Exp.t;
/** Maps with expression keys. */
let module ExpMap: Map.S with type key = Exp.t;
/** Hashtable with expressions as keys. */
let module ExpHash: Hashtbl.S with type key = Exp.t;
/** Convert expression lists to expression sets. */ /** Convert expression lists to expression sets. */
let elist_to_eset: list Exp.t => ExpSet.t; let elist_to_eset: list Exp.t => Exp.Set.t;
/** Kind of prune instruction */ /** Kind of prune instruction */
@ -415,7 +403,7 @@ let instr_compare: instr => instr => int;
/** compare instructions from different procedures without considering loc's, ident's, and pvar's. /** compare instructions from different procedures without considering loc's, ident's, and pvar's.
the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
used in the procedure of [instr2] */ used in the procedure of [instr2] */
let instr_compare_structural: instr => instr => ExpMap.t Exp.t => (int, ExpMap.t Exp.t); let instr_compare_structural: instr => instr => Exp.Map.t Exp.t => (int, Exp.Map.t Exp.t);
let exp_list_compare: list Exp.t => list Exp.t => int; let exp_list_compare: list Exp.t => list Exp.t => int;

38
infer/src/backend/dom.ml
Unescape View File

@ -114,7 +114,7 @@ end = struct
let lookup_equiv' tbl e = let lookup_equiv' tbl e =
lookup' tbl e e lookup' tbl e e
let lookup_const' tbl e = let lookup_const' tbl e =
lookup' tbl e Sil.ExpSet.empty lookup' tbl e Exp.Set.empty
let rec find' tbl e = let rec find' tbl e =
let e' = lookup_equiv' tbl e in let e' = lookup_equiv' tbl e in
@ -138,15 +138,15 @@ end = struct
| _ -> r2, r1 in | _ -> r2, r1 in
let new_c = lookup_const' const_tbl new_r in let new_c = lookup_const' const_tbl new_r in
let old_c = lookup_const' const_tbl old_r in let old_c = lookup_const' const_tbl old_r in
let res_c = Sil.ExpSet.union new_c old_c in let res_c = Exp.Set.union new_c old_c in
if Sil.ExpSet.cardinal res_c > 1 then (L.d_strln "failure reason 3"; raise IList.Fail); if Exp.Set.cardinal res_c > 1 then (L.d_strln "failure reason 3"; raise IList.Fail);
Hashtbl.replace tbl old_r new_r; Hashtbl.replace tbl old_r new_r;
Hashtbl.replace const_tbl new_r res_c Hashtbl.replace const_tbl new_r res_c
let replace_const' tbl const_tbl e c = let replace_const' tbl const_tbl e c =
let r = find' tbl e in let r = find' tbl e in
let set = Sil.ExpSet.add c (lookup_const' const_tbl r) in let set = Exp.Set.add c (lookup_const' const_tbl r) in
if Sil.ExpSet.cardinal set > 1 then (L.d_strln "failure reason 4"; raise IList.Fail); if Exp.Set.cardinal set > 1 then (L.d_strln "failure reason 4"; raise IList.Fail);
Hashtbl.replace const_tbl r set Hashtbl.replace const_tbl r set
let add side e e' = let add side e e' =
@ -189,7 +189,7 @@ end = struct
let r = find' tbl v in let r = find' tbl v in
let set = lookup_const' const_tbl r in let set = lookup_const' const_tbl r in
(IList.for_all (fun v' -> Exp.equal (find' tbl v') r) vars') && (IList.for_all (fun v' -> Exp.equal (find' tbl v') r) vars') &&
(IList.for_all (fun c -> Sil.ExpSet.mem c set) nonvars) (IList.for_all (fun c -> Exp.Set.mem c set) nonvars)
end end
@ -211,18 +211,18 @@ module Dangling : sig
end = struct end = struct
let lexps1 = ref Sil.ExpSet.empty let lexps1 = ref Exp.Set.empty
let lexps2 = ref Sil.ExpSet.empty let lexps2 = ref Exp.Set.empty
let get_lexp_set' sigma = let get_lexp_set' sigma =
let lexp_lst = Sil.hpred_list_get_lexps (fun _ -> true) sigma in let lexp_lst = Sil.hpred_list_get_lexps (fun _ -> true) sigma in
IList.fold_left (fun set e -> Sil.ExpSet.add e set) Sil.ExpSet.empty lexp_lst IList.fold_left (fun set e -> Exp.Set.add e set) Exp.Set.empty lexp_lst
let init sigma1 sigma2 = let init sigma1 sigma2 =
lexps1 := get_lexp_set' sigma1; lexps1 := get_lexp_set' sigma1;
lexps2 := get_lexp_set' sigma2 lexps2 := get_lexp_set' sigma2
let final () = let final () =
lexps1 := Sil.ExpSet.empty; lexps1 := Exp.Set.empty;
lexps2 := Sil.ExpSet.empty lexps2 := Exp.Set.empty
(* conservatively checks whether e is dangling *) (* conservatively checks whether e is dangling *)
let check side e = let check side e =
@ -232,9 +232,9 @@ end = struct
| Rhs -> !lexps2 | Rhs -> !lexps2
in in
match e with match e with
| Exp.Var id -> can_rename id && not (Sil.ExpSet.mem e lexps) | Exp.Var id -> can_rename id && not (Exp.Set.mem e lexps)
| Exp.Const _ -> not (Sil.ExpSet.mem e lexps) | Exp.Const _ -> not (Exp.Set.mem e lexps)
| Exp.BinOp _ -> not (Sil.ExpSet.mem e lexps) | Exp.BinOp _ -> not (Exp.Set.mem e lexps)
| _ -> false | _ -> false
end end
@ -352,8 +352,8 @@ end
module CheckMeet : InfoLossCheckerSig = struct module CheckMeet : InfoLossCheckerSig = struct
let lexps1 = ref Sil.ExpSet.empty let lexps1 = ref Exp.Set.empty
let lexps2 = ref Sil.ExpSet.empty let lexps2 = ref Exp.Set.empty
let init sigma1 sigma2 = let init sigma1 sigma2 =
let lexps1_lst = Sil.hpred_list_get_lexps (fun _ -> true) sigma1 in let lexps1_lst = Sil.hpred_list_get_lexps (fun _ -> true) sigma1 in
@ -362,8 +362,8 @@ module CheckMeet : InfoLossCheckerSig = struct
lexps2 := Sil.elist_to_eset lexps2_lst lexps2 := Sil.elist_to_eset lexps2_lst
let final () = let final () =
lexps1 := Sil.ExpSet.empty; lexps1 := Exp.Set.empty;
lexps2 := Sil.ExpSet.empty lexps2 := Exp.Set.empty
let lost_little side e es = let lost_little side e es =
let lexps = match side with let lexps = match side with
@ -376,7 +376,7 @@ module CheckMeet : InfoLossCheckerSig = struct
| [Exp.Const _], Exp.Lvar _ -> | [Exp.Const _], Exp.Lvar _ ->
false false
| [Exp.Const _], Exp.Var _ -> | [Exp.Const _], Exp.Var _ ->
not (Sil.ExpSet.mem e lexps) not (Exp.Set.mem e lexps)
| [Exp.Const _], _ -> | [Exp.Const _], _ ->
assert false assert false
| [_], Exp.Lvar _ | [_], Exp.Var _ -> | [_], Exp.Lvar _ | [_], Exp.Var _ ->

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

@ -218,7 +218,7 @@ let rec find_boolean_assignment node pvar true_branch : Cfg.Node.t option =
(** Find the Letderef instruction used to declare normal variable [id], (** Find the Letderef instruction used to declare normal variable [id],
and return the expression dereferenced to initialize [id] *) and return the expression dereferenced to initialize [id] *)
let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : DExp.t option = let rec _find_normal_variable_letderef (seen : Exp.Set.t) node id : DExp.t option =
let is_infer = not (Config.checkers || Config.eradicate) in let is_infer = not (Config.checkers || Config.eradicate) in
let find_declaration node = function let find_declaration node = function
| Sil.Letderef (id0, e, _, _) when Ident.equal id id0 -> | Sil.Letderef (id0, e, _, _) when Ident.equal id id0 ->
@ -271,11 +271,11 @@ let rec _find_normal_variable_letderef (seen : Sil.ExpSet.t) node id : DExp.t op
res res
(** describe lvalue [e] as a dexp *) (** describe lvalue [e] as a dexp *)
and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : DExp.t option = and _exp_lv_dexp (_seen : Exp.Set.t) node e : DExp.t option =
if Sil.ExpSet.mem e _seen then if Exp.Set.mem e _seen then
(L.d_str "exp_lv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None) (L.d_str "exp_lv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None)
else else
let seen = Sil.ExpSet.add e _seen in let seen = Exp.Set.add e _seen in
match Prop.exp_normalize_noabs Sil.sub_empty e with match Prop.exp_normalize_noabs Sil.sub_empty e with
| Exp.Const c -> | Exp.Const c ->
if verbose then (L.d_str "exp_lv_dexp: constant "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_lv_dexp: constant "; Sil.d_exp e; L.d_ln ());
@ -361,11 +361,11 @@ and _exp_lv_dexp (_seen : Sil.ExpSet.t) node e : DExp.t option =
None None
(** describe rvalue [e] as a dexp *) (** describe rvalue [e] as a dexp *)
and _exp_rv_dexp (_seen : Sil.ExpSet.t) node e : DExp.t option = and _exp_rv_dexp (_seen : Exp.Set.t) node e : DExp.t option =
if Sil.ExpSet.mem e _seen then if Exp.Set.mem e _seen then
(L.d_str "exp_rv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None) (L.d_str "exp_rv_dexp: cycle detected"; Sil.d_exp e; L.d_ln (); None)
else else
let seen = Sil.ExpSet.add e _seen in let seen = Exp.Set.add e _seen in
match e with match e with
| Exp.Const c -> | Exp.Const c ->
if verbose then (L.d_str "exp_rv_dexp: constant "; Sil.d_exp e; L.d_ln ()); if verbose then (L.d_str "exp_rv_dexp: constant "; Sil.d_exp e; L.d_ln ());
@ -421,9 +421,9 @@ and _exp_rv_dexp (_seen : Sil.ExpSet.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 ()); if verbose then (L.d_str "exp_rv_dexp: no match for "; Sil.d_exp e; L.d_ln ());
None None
let find_normal_variable_letderef = _find_normal_variable_letderef Sil.ExpSet.empty let find_normal_variable_letderef = _find_normal_variable_letderef Exp.Set.empty
let exp_lv_dexp = _exp_lv_dexp Sil.ExpSet.empty let exp_lv_dexp = _exp_lv_dexp Exp.Set.empty
let exp_rv_dexp = _exp_rv_dexp Sil.ExpSet.empty let exp_rv_dexp = _exp_rv_dexp Exp.Set.empty
(** Produce a description of a mismatch between an allocation function (** Produce a description of a mismatch between an allocation function
and a deallocation function *) and a deallocation function *)

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

@ -626,7 +626,7 @@ let report_context_leaks pname sigma tenv =
(* raise an error if any Context expression is in [reachable_exps] *) (* raise an error if any Context expression is in [reachable_exps] *)
IList.iter IList.iter
(fun (context_exp, struct_typ) -> (fun (context_exp, struct_typ) ->
if Sil.ExpSet.mem context_exp reachable_exps then if Exp.Set.mem context_exp reachable_exps then
let leak_path = let leak_path =
match Prop.get_fld_typ_path_opt fld_exps context_exp reachable_hpreds with match Prop.get_fld_typ_path_opt fld_exps context_exp reachable_hpreds with
| Some path -> path | Some path -> path

55
infer/src/backend/prop.ml
Unescape View File

@ -1538,32 +1538,32 @@ let prop_sigma_star (p : 'a t) (sigma : sigma) : exposed t =
(** return the set of subexpressions of [strexp] *) (** return the set of subexpressions of [strexp] *)
let strexp_get_exps strexp = let strexp_get_exps strexp =
let rec strexp_get_exps_rec exps = function let rec strexp_get_exps_rec exps = function
| Sil.Eexp (Exp.Exn e, _) -> Sil.ExpSet.add e exps | Sil.Eexp (Exp.Exn e, _) -> Exp.Set.add e exps
| Sil.Eexp (e, _) -> Sil.ExpSet.add e exps | Sil.Eexp (e, _) -> Exp.Set.add e exps
| Sil.Estruct (flds, _) -> | Sil.Estruct (flds, _) ->
IList.fold_left (fun exps (_, strexp) -> strexp_get_exps_rec exps strexp) exps flds IList.fold_left (fun exps (_, strexp) -> strexp_get_exps_rec exps strexp) exps flds
| Sil.Earray (_, elems, _) -> | Sil.Earray (_, elems, _) ->
IList.fold_left (fun exps (_, strexp) -> strexp_get_exps_rec exps strexp) exps elems in IList.fold_left (fun exps (_, strexp) -> strexp_get_exps_rec exps strexp) exps elems in
strexp_get_exps_rec Sil.ExpSet.empty strexp strexp_get_exps_rec Exp.Set.empty strexp
(** get the set of expressions on the righthand side of [hpred] *) (** get the set of expressions on the righthand side of [hpred] *)
let hpred_get_targets = function let hpred_get_targets = function
| Sil.Hpointsto (_, rhs, _) -> strexp_get_exps rhs | Sil.Hpointsto (_, rhs, _) -> strexp_get_exps rhs
| Sil.Hlseg (_, _, _, e, el) -> | Sil.Hlseg (_, _, _, e, el) ->
IList.fold_left (fun exps e -> Sil.ExpSet.add e exps) Sil.ExpSet.empty (e :: el) IList.fold_left (fun exps e -> Exp.Set.add e exps) Exp.Set.empty (e :: el)
| Sil.Hdllseg (_, _, _, oB, oF, iB, el) -> | Sil.Hdllseg (_, _, _, oB, oF, iB, el) ->
(* only one direction supported for now *) (* only one direction supported for now *)
IList.fold_left (fun exps e -> Sil.ExpSet.add e exps) Sil.ExpSet.empty (oB :: oF :: iB :: el) IList.fold_left (fun exps e -> Exp.Set.add e exps) Exp.Set.empty (oB :: oF :: iB :: el)
(** return the set of hpred's and exp's in [sigma] that are reachable from an expression in (** return the set of hpred's and exp's in [sigma] that are reachable from an expression in
[exps] *) [exps] *)
let compute_reachable_hpreds sigma exps = let compute_reachable_hpreds sigma exps =
let rec compute_reachable_hpreds_rec sigma (reach, exps) = let rec compute_reachable_hpreds_rec sigma (reach, exps) =
let add_hpred_if_reachable (reach, exps) = function let add_hpred_if_reachable (reach, exps) = function
| Sil.Hpointsto (lhs, _, _) as hpred when Sil.ExpSet.mem lhs exps-> | Sil.Hpointsto (lhs, _, _) as hpred when Exp.Set.mem lhs exps->
let reach' = Sil.HpredSet.add hpred reach in let reach' = Sil.HpredSet.add hpred reach in
let reach_exps = hpred_get_targets hpred in let reach_exps = hpred_get_targets hpred in
(reach', Sil.ExpSet.union exps reach_exps) (reach', Exp.Set.union exps reach_exps)
| _ -> reach, exps in | _ -> reach, exps in
let reach', exps' = IList.fold_left add_hpred_if_reachable (reach, exps) sigma in let reach', exps' = IList.fold_left add_hpred_if_reachable (reach, exps) sigma in
if (Sil.HpredSet.cardinal reach) = (Sil.HpredSet.cardinal reach') then (reach, exps) if (Sil.HpredSet.cardinal reach) = (Sil.HpredSet.cardinal reach') then (reach, exps)
@ -1595,7 +1595,7 @@ let get_fld_typ_path_opt src_exps snk_exp_ reachable_hpreds_ =
let rec get_fld_typ_path snk_exp path reachable_hpreds = let rec get_fld_typ_path snk_exp path reachable_hpreds =
let (snk_exp', path', reachable_hpreds') = let (snk_exp', path', reachable_hpreds') =
Sil.HpredSet.fold extend_path reachable_hpreds (snk_exp, path, reachable_hpreds) in Sil.HpredSet.fold extend_path reachable_hpreds (snk_exp, path, reachable_hpreds) in
if Sil.ExpSet.mem snk_exp' src_exps if Exp.Set.mem snk_exp' src_exps
then Some path' then Some path'
else else
if Sil.HpredSet.cardinal reachable_hpreds' >= Sil.HpredSet.cardinal reachable_hpreds if Sil.HpredSet.cardinal reachable_hpreds' >= Sil.HpredSet.cardinal reachable_hpreds
@ -1606,7 +1606,7 @@ let get_fld_typ_path_opt src_exps snk_exp_ reachable_hpreds_ =
(** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *) (** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *)
let compute_reachable_atoms pi exps = let compute_reachable_atoms pi exps =
let rec exp_contains = function let rec exp_contains = function
| exp when Sil.ExpSet.mem exp exps -> true | exp when Exp.Set.mem exp exps -> true
| Exp.UnOp (_, e, _) | Exp.Cast (_, e) | Exp.Lfield (e, _, _) -> exp_contains e | Exp.UnOp (_, e, _) | Exp.Cast (_, e) | Exp.Lfield (e, _, _) -> exp_contains e
| Exp.BinOp (_, e0, e1) | Exp.Lindex (e0, e1) -> exp_contains e0 || exp_contains e1 | Exp.BinOp (_, e0, e1) | Exp.Lindex (e0, e1) -> exp_contains e0 || exp_contains e1
| _ -> false in | _ -> false in
@ -1629,12 +1629,12 @@ let sigma_remove_emptylseg sigma =
| [] -> | [] ->
set set
| Sil.Hpointsto (e, _, _) :: sigma' | Sil.Hlseg (Sil.Lseg_NE, _, e, _, _) :: sigma' -> | Sil.Hpointsto (e, _, _) :: sigma' | Sil.Hlseg (Sil.Lseg_NE, _, e, _, _) :: sigma' ->
f_alloc (Sil.ExpSet.add e set) sigma' f_alloc (Exp.Set.add e set) sigma'
| Sil.Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _) :: sigma' -> | Sil.Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _) :: sigma' ->
f_alloc (Sil.ExpSet.add iF (Sil.ExpSet.add iB set)) sigma' f_alloc (Exp.Set.add iF (Exp.Set.add iB set)) sigma'
| _ :: sigma' -> | _ :: sigma' ->
f_alloc set sigma' in f_alloc set sigma' in
f_alloc Sil.ExpSet.empty sigma f_alloc Exp.Set.empty sigma
in in
let rec f eqs_zero sigma_passed = function let rec f eqs_zero sigma_passed = function
| [] -> | [] ->
@ -1642,13 +1642,13 @@ let sigma_remove_emptylseg sigma =
| Sil.Hpointsto _ as hpred :: sigma' -> | Sil.Hpointsto _ as hpred :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma' f eqs_zero (hpred :: sigma_passed) sigma'
| Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) :: sigma' | Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) :: sigma'
when (Exp.equal e1 Sil.exp_zero) || (Sil.ExpSet.mem e1 alloc_set) -> when (Exp.equal e1 Sil.exp_zero) || (Exp.Set.mem e1 alloc_set) ->
f (Sil.Aeq(e1, e2) :: eqs_zero) sigma_passed sigma' f (Sil.Aeq(e1, e2) :: eqs_zero) sigma_passed sigma'
| Sil.Hlseg _ as hpred :: sigma' -> | Sil.Hlseg _ as hpred :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma' f eqs_zero (hpred :: sigma_passed) sigma'
| Sil.Hdllseg (Sil.Lseg_PE, _, iF, oB, oF, iB, _) :: sigma' | Sil.Hdllseg (Sil.Lseg_PE, _, iF, oB, oF, iB, _) :: sigma'
when (Exp.equal iF Sil.exp_zero) || (Sil.ExpSet.mem iF alloc_set) when (Exp.equal iF Sil.exp_zero) || (Exp.Set.mem iF alloc_set)
|| (Exp.equal iB Sil.exp_zero) || (Sil.ExpSet.mem iB alloc_set) -> || (Exp.equal iB Sil.exp_zero) || (Exp.Set.mem iB alloc_set) ->
f (Sil.Aeq(iF, oF):: Sil.Aeq(iB, oB):: eqs_zero) sigma_passed sigma' f (Sil.Aeq(iF, oF):: Sil.Aeq(iB, oB):: eqs_zero) sigma_passed sigma'
| Sil.Hdllseg _ as hpred :: sigma' -> | Sil.Hdllseg _ as hpred :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma' f eqs_zero (hpred :: sigma_passed) sigma'
@ -2897,31 +2897,6 @@ end = struct
let prop_chain_size p = let prop_chain_size p =
let fp_size = pi_size p.foot_pi + sigma_size p.foot_sigma in let fp_size = pi_size p.foot_pi + sigma_size p.foot_sigma in
pi_size p.pi + sigma_size p.sigma + fp_size pi_size p.pi + sigma_size p.sigma + fp_size
(*
(** Approximate the size of the longest chain by counting the max
number of |-> with the same type and whose lhs is primed or
footprint *)
let sigma_chain_size sigma =
let tbl = ref Sil.ExpMap.empty in
let add t =
try
let count = Sil.ExpMap.find t !tbl in
tbl := Sil.ExpMap.add t (count + 1) !tbl
with
| Not_found ->
tbl := Sil.ExpMap.add t 1 !tbl in
let process_hpred = function
| Sil.Hpointsto (e, _, te) ->
(match e with
| Exp.Var id when Ident.is_primed id || Ident.is_footprint id -> add te
| _ -> ())
| Sil.Hlseg _ | Sil.Hdllseg _ -> () in
IList.iter process_hpred sigma;
let size = ref 0 in
Sil.ExpMap.iter (fun t n -> size := max n !size) !tbl;
!size
*)
end end
(*** END of module Metrics ***) (*** END of module Metrics ***)

10
infer/src/backend/prop.mli
Unescape View File

@ -501,23 +501,23 @@ val prop_iter_gc_fields : unit prop_iter -> unit prop_iter
val find_equal_formal_path : Exp.t -> 'a t -> Exp.t option val find_equal_formal_path : Exp.t -> 'a t -> Exp.t option
(** return the set of subexpressions of [strexp] *) (** return the set of subexpressions of [strexp] *)
val strexp_get_exps : Sil.strexp -> Sil.ExpSet.t val strexp_get_exps : Sil.strexp -> Exp.Set.t
(** get the set of expressions on the righthand side of [hpred] *) (** get the set of expressions on the righthand side of [hpred] *)
val hpred_get_targets : Sil.hpred -> Sil.ExpSet.t val hpred_get_targets : Sil.hpred -> Exp.Set.t
(** return the set of hpred's and exp's in [sigma] that are reachable from an expression in (** return the set of hpred's and exp's in [sigma] that are reachable from an expression in
[exps] *) [exps] *)
val compute_reachable_hpreds : hpred list -> Sil.ExpSet.t -> Sil.HpredSet.t * Sil.ExpSet.t val compute_reachable_hpreds : hpred list -> Exp.Set.t -> Sil.HpredSet.t * Exp.Set.t
(** if possible, produce a (fieldname, typ) path from one of the [src_exps] to [snk_exp] using (** if possible, produce a (fieldname, typ) path from one of the [src_exps] to [snk_exp] using
[reachable_hpreds]. *) [reachable_hpreds]. *)
val get_fld_typ_path_opt : Sil.ExpSet.t -> Exp.t -> Sil.HpredSet.t -> val get_fld_typ_path_opt : Exp.Set.t -> Exp.t -> Sil.HpredSet.t ->
(Ident.fieldname option * Typ.t) list option (Ident.fieldname option * Typ.t) list option
(** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *) (** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *)
val compute_reachable_atoms : pi -> Sil.ExpSet.t -> pi val compute_reachable_atoms : pi -> Exp.Set.t -> pi
(** {2 Internal modules} *) (** {2 Internal modules} *)

2
infer/src/backend/propgraph.ml
Unescape View File

@ -55,7 +55,7 @@ let edge_get_source = function
(** Return the successor nodes of the edge *) (** Return the successor nodes of the edge *)
let edge_get_succs = function let edge_get_succs = function
| Ehpred hpred -> Sil.ExpSet.elements (Prop.hpred_get_targets hpred) | Ehpred hpred -> Exp.Set.elements (Prop.hpred_get_targets hpred)
| Eatom (Sil.Aeq (_, e2)) -> [e2] | Eatom (Sil.Aeq (_, e2)) -> [e2]
| Eatom (Sil.Aneq (_, e2)) -> [e2] | Eatom (Sil.Aneq (_, e2)) -> [e2]
| Eatom (Sil.Apred _ | Anpred _) -> [] | Eatom (Sil.Apred _ | Anpred _) -> []

24
infer/src/backend/prover.ml
Unescape View File

@ -290,14 +290,14 @@ end = struct
else begin else begin
let umap_add umap e new_upper = let umap_add umap e new_upper =
try try
let old_upper = Sil.ExpMap.find e umap in let old_upper = Exp.Map.find e umap in
if IntLit.leq old_upper new_upper then umap else Sil.ExpMap.add e new_upper umap if IntLit.leq old_upper new_upper then umap else Exp.Map.add e new_upper umap
with Not_found -> Sil.ExpMap.add e new_upper umap in with Not_found -> Exp.Map.add e new_upper umap in
let lmap_add lmap e new_lower = let lmap_add lmap e new_lower =
try try
let old_lower = Sil.ExpMap.find e lmap in let old_lower = Exp.Map.find e lmap in
if IntLit.geq old_lower new_lower then lmap else Sil.ExpMap.add e new_lower lmap if IntLit.geq old_lower new_lower then lmap else Exp.Map.add e new_lower lmap
with Not_found -> Sil.ExpMap.add e new_lower lmap in with Not_found -> Exp.Map.add e new_lower lmap in
let rec umap_create_from_leqs umap = function let rec umap_create_from_leqs umap = function
| [] -> umap | [] -> umap
| (e1, Exp.Const (Const.Cint upper1)):: leqs_rest -> | (e1, Exp.Const (Const.Cint upper1)):: leqs_rest ->
@ -315,7 +315,7 @@ end = struct
| constr:: constrs_rest -> | constr:: constrs_rest ->
try try
let e1, e2, n = DiffConstr.to_triple constr (* e1 - e2 <= n *) in let e1, e2, n = DiffConstr.to_triple constr (* e1 - e2 <= n *) in
let upper2 = Sil.ExpMap.find e2 umap in let upper2 = Exp.Map.find e2 umap in
let new_upper1 = upper2 ++ n in let new_upper1 = upper2 ++ n in
let new_umap = umap_add umap e1 new_upper1 in let new_umap = umap_add umap e1 new_upper1 in
umap_improve_by_difference_constraints new_umap constrs_rest umap_improve_by_difference_constraints new_umap constrs_rest
@ -326,24 +326,24 @@ end = struct
| constr:: constrs_rest -> (* e2 - e1 > -n-1 *) | constr:: constrs_rest -> (* e2 - e1 > -n-1 *)
try try
let e1, e2, n = DiffConstr.to_triple constr (* e2 - e1 > -n-1 *) in let e1, e2, n = DiffConstr.to_triple constr (* e2 - e1 > -n-1 *) in
let lower1 = Sil.ExpMap.find e1 lmap in let lower1 = Exp.Map.find e1 lmap in
let new_lower2 = lower1 -- n -- IntLit.one in let new_lower2 = lower1 -- n -- IntLit.one in
let new_lmap = lmap_add lmap e2 new_lower2 in let new_lmap = lmap_add lmap e2 new_lower2 in
lmap_improve_by_difference_constraints new_lmap constrs_rest lmap_improve_by_difference_constraints new_lmap constrs_rest
with Not_found -> with Not_found ->
lmap_improve_by_difference_constraints lmap constrs_rest in lmap_improve_by_difference_constraints lmap constrs_rest in
let leqs_res = let leqs_res =
let umap = umap_create_from_leqs Sil.ExpMap.empty leqs in let umap = umap_create_from_leqs Exp.Map.empty leqs in
let umap' = umap_improve_by_difference_constraints umap diff_constraints2 in let umap' = umap_improve_by_difference_constraints umap diff_constraints2 in
let leqs' = Sil.ExpMap.fold let leqs' = Exp.Map.fold
(fun e upper acc_leqs -> (e, Sil.exp_int upper):: acc_leqs) (fun e upper acc_leqs -> (e, Sil.exp_int upper):: acc_leqs)
umap' [] in umap' [] in
let leqs'' = (IList.map DiffConstr.to_leq diff_constraints2) @ leqs' in let leqs'' = (IList.map DiffConstr.to_leq diff_constraints2) @ leqs' in
leqs_sort_then_remove_redundancy leqs'' in leqs_sort_then_remove_redundancy leqs'' in
let lts_res = let lts_res =
let lmap = lmap_create_from_lts Sil.ExpMap.empty lts in let lmap = lmap_create_from_lts Exp.Map.empty lts in
let lmap' = lmap_improve_by_difference_constraints lmap diff_constraints2 in let lmap' = lmap_improve_by_difference_constraints lmap diff_constraints2 in
let lts' = Sil.ExpMap.fold let lts' = Exp.Map.fold
(fun e lower acc_lts -> (Sil.exp_int lower, e):: acc_lts) (fun e lower acc_lts -> (Sil.exp_int lower, e):: acc_lts)
lmap' [] in lmap' [] in
let lts'' = (IList.map DiffConstr.to_lt diff_constraints2) @ lts' in let lts'' = (IList.map DiffConstr.to_lt diff_constraints2) @ lts' in

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

@ -938,18 +938,18 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
let collect_taint_untaint_exprs acc_map atom = let collect_taint_untaint_exprs acc_map atom =
match Prop.atom_get_attribute atom with match Prop.atom_get_attribute atom with
| Some (Apred (Ataint _, [e])) -> | Some (Apred (Ataint _, [e])) ->
let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in let taint_atoms, untaint_atoms = try Exp.Map.find e acc_map with Not_found -> ([], []) in
Sil.ExpMap.add e (atom :: taint_atoms, untaint_atoms) acc_map Exp.Map.add e (atom :: taint_atoms, untaint_atoms) acc_map
| Some (Apred (Auntaint _, [e])) -> | Some (Apred (Auntaint _, [e])) ->
let taint_atoms, untaint_atoms = try Sil.ExpMap.find e acc_map with Not_found -> ([], []) in let taint_atoms, untaint_atoms = try Exp.Map.find e acc_map with Not_found -> ([], []) in
Sil.ExpMap.add e (taint_atoms, atom :: untaint_atoms) acc_map Exp.Map.add e (taint_atoms, atom :: untaint_atoms) acc_map
| _ -> acc_map in | _ -> acc_map in
let taint_untaint_exp_map = let taint_untaint_exp_map =
IList.fold_left IList.fold_left
collect_taint_untaint_exprs collect_taint_untaint_exprs
Sil.ExpMap.empty Exp.Map.empty
combined_pi combined_pi
|> Sil.ExpMap.filter (fun _ (taint, untaint) -> taint <> [] && untaint <> []) in |> Exp.Map.filter (fun _ (taint, untaint) -> taint <> [] && untaint <> []) in
(* TODO: in the future, we will have a richer taint domain that will require making sure that the (* TODO: in the future, we will have a richer taint domain that will require making sure that the
"kind" (e.g. security, privacy) of the taint and untaint match, but for now we don't look at "kind" (e.g. security, privacy) of the taint and untaint match, but for now we don't look at
the untaint atoms *) the untaint atoms *)
@ -960,7 +960,7 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
| _ -> failwith "Expected to get taint attr on atom" in | _ -> failwith "Expected to get taint attr on atom" in
report_taint_error e taint_info callee_pname caller_pname calling_prop in report_taint_error e taint_info callee_pname caller_pname calling_prop in
IList.iter report_one_error taint_atoms in IList.iter report_one_error taint_atoms in
Sil.ExpMap.iter report_taint_errors taint_untaint_exp_map; Exp.Map.iter report_taint_errors taint_untaint_exp_map;
(* filter out UNTAINT(e) atoms from [missing_pi] such that we have already reported a taint (* filter out UNTAINT(e) atoms from [missing_pi] such that we have already reported a taint
error on e. without doing this, we will get PRECONDITION_NOT_MET (and failed spec error on e. without doing this, we will get PRECONDITION_NOT_MET (and failed spec
inference), which is bad. instead, what this does is effectively assume that the UNTAINT(e) inference), which is bad. instead, what this does is effectively assume that the UNTAINT(e)
@ -968,7 +968,7 @@ let do_taint_check caller_pname callee_pname calling_prop missing_pi sub actual_
because we are reporting the taint error, but propagating a *safe* postcondition w.r.t to because we are reporting the taint error, but propagating a *safe* postcondition w.r.t to
tainting. *) tainting. *)
let not_untaint_atom atom = not let not_untaint_atom atom = not
(Sil.ExpMap.exists (Exp.Map.exists
(fun _ (_, untaint_atoms) -> (fun _ (_, untaint_atoms) ->
IList.exists IList.exists
(fun a -> Sil.atom_equal atom a) (fun a -> Sil.atom_equal atom a)

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

@ -342,24 +342,24 @@ let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } =
| _ -> | _ ->
false in false in
let checks_to_formals = ref Sil.ExpSet.empty in let checks_to_formals = ref Exp.Set.empty in
let handle_check_of_formal e = let handle_check_of_formal e =
let repeated = Sil.ExpSet.mem e !checks_to_formals in let repeated = Exp.Set.mem e !checks_to_formals in
if repeated && !verbose then L.stdout "Repeated Null Check of Formal: %a@." (Sil.pp_exp pe_text) e if repeated && !verbose then L.stdout "Repeated Null Check of Formal: %a@." (Sil.pp_exp pe_text) e
else begin else begin
checks_to_formals := Sil.ExpSet.add e !checks_to_formals; checks_to_formals := Exp.Set.add e !checks_to_formals;
if !verbose then L.stdout "Null Check of Formal: %a@." (Sil.pp_exp pe_text) e if !verbose then L.stdout "Null Check of Formal: %a@." (Sil.pp_exp pe_text) e
end in end in
let summary_checks_of_formals () = let summary_checks_of_formals () =
let formal_names = Lazy.force class_formal_names in let formal_names = Lazy.force class_formal_names in
let nchecks = Sil.ExpSet.cardinal !checks_to_formals in let nchecks = Exp.Set.cardinal !checks_to_formals in
let nformals = IList.length formal_names in let nformals = IList.length formal_names in
if (nchecks > 0 && nchecks < nformals) then if (nchecks > 0 && nchecks < nformals) then
begin begin
let was_not_found formal_name = let was_not_found formal_name =
not (Sil.ExpSet.exists (fun exp -> equal_formal_param exp formal_name) !checks_to_formals) in not (Exp.Set.exists (fun exp -> equal_formal_param exp formal_name) !checks_to_formals) in
let missing = IList.filter was_not_found formal_names in let missing = IList.filter was_not_found formal_names in
let loc = Cfg.Procdesc.get_loc proc_desc in let loc = Cfg.Procdesc.get_loc proc_desc in
let pp_file_loc fmt () = let pp_file_loc fmt () =

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

@ -23,7 +23,7 @@ let merge_values _ c1_opt c2_opt =
| None, Some c -> Some c | None, Some c -> Some c
| _ -> Some None | _ -> Some None
module ConstantMap = Sil.ExpMap module ConstantMap = Exp.Map
(** Dataflow struct *) (** Dataflow struct *)
module ConstantFlow = Dataflow.MakeDF(struct module ConstantFlow = Dataflow.MakeDF(struct

Write Preview
Loading…
Cancel
Save