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

Refactor exp_equal and exp_compare to Exp

Browse Source 
Reviewed By: cristianoc

Differential Revision: D3669395

fbshipit-source-id: 4c8805d
master
Josh Berdine 8 years ago committed by Facebook Github Bot 8
parent 701eb20f83
commit d60965824e
27 changed files with 434 additions and 424 deletions
Show Stats Download Patch File Download Diff File

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

@ -50,3 +50,120 @@ and t =
obtained from the type definition, e.g. when an array is over-allocated. For struct types,
the [dynamic_length] is that of the final extensible array, if any. */
| Sizeof of Typ.t dynamic_length Subtype.t;
/** Compare expressions. Variables come before other expressions. */
let rec compare e1 e2 =>
switch (e1, e2) {
| (Var id1, Var id2) => Ident.compare id2 id1
| (Var _, _) => (-1)
| (_, Var _) => 1
| (UnOp o1 e1 to1, UnOp o2 e2 to2) =>
let n = Unop.compare o1 o2;
if (n != 0) {
n
} else {
let n = compare e1 e2;
if (n != 0) {
n
} else {
opt_compare Typ.compare to1 to2
}
}
| (UnOp _, _) => (-1)
| (_, UnOp _) => 1
| (BinOp o1 e1 f1, BinOp o2 e2 f2) =>
let n = Binop.compare o1 o2;
if (n != 0) {
n
} else {
let n = compare e1 e2;
if (n != 0) {
n
} else {
compare f1 f2
}
}
| (BinOp _, _) => (-1)
| (_, BinOp _) => 1
| (Exn e1, Exn e2) => compare e1 e2
| (Exn _, _) => (-1)
| (_, Exn _) => 1
| (Closure {name: n1, captured_vars: c1}, Closure {name: n2, captured_vars: c2}) =>
let captured_var_compare acc (e1, pvar1, typ1) (e2, pvar2, typ2) =>
if (acc != 0) {
acc
} else {
let n = compare e1 e2;
if (n != 0) {
n
} else {
let n = Pvar.compare pvar1 pvar2;
if (n != 0) {
n
} else {
Typ.compare typ1 typ2
}
}
};
let n = Procname.compare n1 n2;
if (n != 0) {
n
} else {
IList.fold_left2 captured_var_compare 0 c1 c2
}
| (Closure _, _) => (-1)
| (_, Closure _) => 1
| (Const c1, Const c2) => Const.compare c1 c2
| (Const _, _) => (-1)
| (_, Const _) => 1
| (Cast t1 e1, Cast t2 e2) =>
let n = compare e1 e2;
if (n != 0) {
n
} else {
Typ.compare t1 t2
}
| (Cast _, _) => (-1)
| (_, Cast _) => 1
| (Lvar i1, Lvar i2) => Pvar.compare i1 i2
| (Lvar _, _) => (-1)
| (_, Lvar _) => 1
| (Lfield e1 f1 t1, Lfield e2 f2 t2) =>
let n = compare e1 e2;
if (n != 0) {
n
} else {
let n = Ident.fieldname_compare f1 f2;
if (n != 0) {
n
} else {
Typ.compare t1 t2
}
}
| (Lfield _, _) => (-1)
| (_, Lfield _) => 1
| (Lindex e1 f1, Lindex e2 f2) =>
let n = compare e1 e2;
if (n != 0) {
n
} else {
compare f1 f2
}
| (Lindex _, _) => (-1)
| (_, Lindex _) => 1
| (Sizeof t1 l1 s1, Sizeof t2 l2 s2) =>
let n = Typ.compare t1 t2;
if (n != 0) {
n
} else {
let n = opt_compare compare l1 l2;
if (n != 0) {
n
} else {
Subtype.compare s1 s2
}
}
};
let equal e1 e2 => compare e1 e2 == 0;

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

@ -50,3 +50,11 @@ and t =
obtained from the type definition, e.g. when an array is over-allocated. For struct types,
the [dynamic_length] is that of the final extensible array, if any. */
| Sizeof of Typ.t dynamic_length Subtype.t;
/** Comparison for expressions. */
let compare: t => t => int;
/** Equality for expressions. */
let equal: t => t => bool;

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

@ -516,134 +516,17 @@ let attribute_compare (att1: attribute) (att2: attribute) :int =>
| (_, Aunsubscribed_observer) => 1
};
/** Compare epressions. Variables come before other expressions. */
let rec exp_compare (e1: Exp.t) (e2: Exp.t) :int =>
switch (e1, e2) {
| (Var id1, Var id2) => Ident.compare id2 id1
| (Var _, _) => (-1)
| (_, Var _) => 1
| (UnOp o1 e1 to1, UnOp o2 e2 to2) =>
let n = Unop.compare o1 o2;
if (n != 0) {
n
} else {
let n = exp_compare e1 e2;
if (n != 0) {
n
} else {
opt_compare Typ.compare to1 to2
}
}
| (UnOp _, _) => (-1)
| (_, UnOp _) => 1
| (BinOp o1 e1 f1, BinOp o2 e2 f2) =>
let n = Binop.compare o1 o2;
if (n != 0) {
n
} else {
let n = exp_compare e1 e2;
if (n != 0) {
n
} else {
exp_compare f1 f2
}
}
| (BinOp _, _) => (-1)
| (_, BinOp _) => 1
| (Exn e1, Exn e2) => exp_compare e1 e2
| (Exn _, _) => (-1)
| (_, Exn _) => 1
| (Closure {name: n1, captured_vars: c1}, Closure {name: n2, captured_vars: c2}) =>
let captured_var_compare acc (e1, pvar1, typ1) (e2, pvar2, typ2) =>
if (acc != 0) {
acc
} else {
let n = exp_compare e1 e2;
if (n != 0) {
n
} else {
let n = Pvar.compare pvar1 pvar2;
if (n != 0) {
n
} else {
Typ.compare typ1 typ2
}
}
};
let n = Procname.compare n1 n2;
if (n != 0) {
n
} else {
IList.fold_left2 captured_var_compare 0 c1 c2
}
| (Closure _, _) => (-1)
| (_, Closure _) => 1
| (Const c1, Const c2) => Const.compare c1 c2
| (Const _, _) => (-1)
| (_, Const _) => 1
| (Cast t1 e1, Cast t2 e2) =>
let n = exp_compare e1 e2;
if (n != 0) {
n
} else {
Typ.compare t1 t2
}
| (Cast _, _) => (-1)
| (_, Cast _) => 1
| (Lvar i1, Lvar i2) => Pvar.compare i1 i2
| (Lvar _, _) => (-1)
| (_, Lvar _) => 1
| (Lfield e1 f1 t1, Lfield e2 f2 t2) =>
let n = exp_compare e1 e2;
if (n != 0) {
n
} else {
let n = Ident.fieldname_compare f1 f2;
if (n != 0) {
n
} else {
Typ.compare t1 t2
}
}
| (Lfield _, _) => (-1)
| (_, Lfield _) => 1
| (Lindex e1 f1, Lindex e2 f2) =>
let n = exp_compare e1 e2;
if (n != 0) {
n
} else {
exp_compare f1 f2
}
| (Lindex _, _) => (-1)
| (_, Lindex _) => 1
| (Sizeof t1 l1 s1, Sizeof t2 l2 s2) =>
let n = Typ.compare t1 t2;
if (n != 0) {
n
} else {
let n = opt_compare exp_compare l1 l2;
if (n != 0) {
n
} else {
Subtype.compare s1 s2
}
}
};
let exp_equal e1 e2 => exp_compare e1 e2 == 0;
let rec exp_is_array_index_of exp1 exp2 =>
switch exp1 {
| Exp.Lindex exp _ => exp_is_array_index_of exp exp2
| _ => exp_equal exp1 exp2
| _ => Exp.equal exp1 exp2
};
let ident_exp_compare = pair_compare Ident.compare exp_compare;
let ident_exp_compare = pair_compare Ident.compare Exp.compare;
let ident_exp_equal ide1 ide2 => ident_exp_compare ide1 ide2 == 0;
let exp_list_compare = IList.compare exp_compare;
let exp_list_compare = IList.compare Exp.compare;
let exp_list_equal el1 el2 => exp_list_compare el1 el2 == 0;
@ -657,20 +540,20 @@ let atom_compare a b =>
} else {
switch (a, b) {
| (Aeq e1 e2, Aeq f1 f2) =>
let n = exp_compare e1 f1;
let n = Exp.compare e1 f1;
if (n != 0) {
n
} else {
exp_compare e2 f2
Exp.compare e2 f2
}
| (Aeq _, _) => (-1)
| (_, Aeq _) => 1
| (Aneq e1 e2, Aneq f1 f2) =>
let n = exp_compare e1 f1;
let n = Exp.compare e1 f1;
if (n != 0) {
n
} else {
exp_compare e2 f2
Exp.compare e2 f2
}
| (Aneq _, _) => (-1)
| (_, Aneq _) => 1
@ -679,7 +562,7 @@ let atom_compare a b =>
if (n != 0) {
n
} else {
IList.compare exp_compare es1 es2
IList.compare Exp.compare es1 es2
}
| (Apred _, _) => (-1)
| (_, Apred _) => 1
@ -688,7 +571,7 @@ let atom_compare a b =>
if (n != 0) {
n
} else {
IList.compare exp_compare es1 es2
IList.compare Exp.compare es1 es2
}
}
};
@ -711,14 +594,14 @@ let rec strexp_compare se1 se2 =>
0
} else {
switch (se1, se2) {
| (Eexp e1 _, Eexp e2 _) => exp_compare e1 e2
| (Eexp e1 _, Eexp e2 _) => Exp.compare e1 e2
| (Eexp _, _) => (-1)
| (_, Eexp _) => 1
| (Estruct fel1 _, Estruct fel2 _) => fld_strexp_list_compare fel1 fel2
| (Estruct _, _) => (-1)
| (_, Estruct _) => 1
| (Earray e1 esel1 _, Earray e2 esel2 _) =>
let n = exp_compare e1 e2;
let n = Exp.compare e1 e2;
if (n != 0) {
n
} else {
@ -728,7 +611,7 @@ let rec strexp_compare se1 se2 =>
}
and fld_strexp_compare fse1 fse2 => pair_compare Ident.fieldname_compare strexp_compare fse1 fse2
and fld_strexp_list_compare fsel1 fsel2 => IList.compare fld_strexp_compare fsel1 fsel2
and exp_strexp_compare ese1 ese2 => pair_compare exp_compare strexp_compare ese1 ese2
and exp_strexp_compare ese1 ese2 => pair_compare Exp.compare strexp_compare ese1 ese2
and exp_strexp_list_compare esel1 esel2 => IList.compare exp_strexp_compare esel1 esel2;
@ -738,14 +621,14 @@ let rec hpred_compare hpred1 hpred2 =>
0
} else {
switch (hpred1, hpred2) {
| (Hpointsto e1 _ _, Hlseg _ _ e2 _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
| (Hpointsto e1 _ _, Hdllseg _ _ e2 _ _ _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
| (Hlseg _ _ e1 _ _, Hpointsto e2 _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
| (Hlseg _ _ e1 _ _, Hdllseg _ _ e2 _ _ _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
| (Hdllseg _ _ e1 _ _ _ _, Hpointsto e2 _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
| (Hdllseg _ _ e1 _ _ _ _, Hlseg _ _ e2 _ _) when exp_compare e2 e1 != 0 => exp_compare e2 e1
| (Hpointsto e1 _ _, Hlseg _ _ e2 _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
| (Hpointsto e1 _ _, Hdllseg _ _ e2 _ _ _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
| (Hlseg _ _ e1 _ _, Hpointsto e2 _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
| (Hlseg _ _ e1 _ _, Hdllseg _ _ e2 _ _ _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
| (Hdllseg _ _ e1 _ _ _ _, Hpointsto e2 _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
| (Hdllseg _ _ e1 _ _ _ _, Hlseg _ _ e2 _ _) when Exp.compare e2 e1 != 0 => Exp.compare e2 e1
| (Hpointsto e1 se1 te1, Hpointsto e2 se2 te2) =>
let n = exp_compare e2 e1;
let n = Exp.compare e2 e1;
if (n != 0) {
n
} else {
@ -753,13 +636,13 @@ let rec hpred_compare hpred1 hpred2 =>
if (n != 0) {
n
} else {
exp_compare te2 te1
Exp.compare te2 te1
}
}
| (Hpointsto _, _) => (-1)
| (_, Hpointsto _) => 1
| (Hlseg k1 hpar1 e1 f1 el1, Hlseg k2 hpar2 e2 f2 el2) =>
let n = exp_compare e2 e1;
let n = Exp.compare e2 e1;
if (n != 0) {
n
} else {
@ -771,7 +654,7 @@ let rec hpred_compare hpred1 hpred2 =>
if (n != 0) {
n
} else {
let n = exp_compare f2 f1;
let n = Exp.compare f2 f1;
if (n != 0) {
n
} else {
@ -783,7 +666,7 @@ let rec hpred_compare hpred1 hpred2 =>
| (Hlseg _, Hdllseg _) => (-1)
| (Hdllseg _, Hlseg _) => 1
| (Hdllseg k1 hpar1 e1 f1 g1 h1 el1, Hdllseg k2 hpar2 e2 f2 g2 h2 el2) =>
let n = exp_compare e2 e1;
let n = Exp.compare e2 e1;
if (n != 0) {
n
} else {
@ -795,15 +678,15 @@ let rec hpred_compare hpred1 hpred2 =>
if (n != 0) {
n
} else {
let n = exp_compare f2 f1;
let n = Exp.compare f2 f1;
if (n != 0) {
n
} else {
let n = exp_compare g2 g1;
let n = Exp.compare g2 g1;
if (n != 0) {
n
} else {
let n = exp_compare h2 h1;
let n = Exp.compare h2 h1;
if (n != 0) {
n
} else {
@ -881,12 +764,12 @@ let hpara_dll_equal hpara1 hpara2 => hpara_dll_compare hpara1 hpara2 == 0;
/** {2 Sets of expressions} */
let module ExpSet = Set.Make {
type t = Exp.t;
let compare = exp_compare;
let compare = Exp.compare;
};
let module ExpMap = Map.Make {
type t = Exp.t;
let compare = exp_compare;
let compare = Exp.compare;
};
let elist_to_eset es => IList.fold_left (fun set e => ExpSet.add e set) ExpSet.empty es;
@ -1032,7 +915,7 @@ let rec _pp_exp pe0 pp_t f e0 => {
| Some sub => Obj.obj (sub (Obj.repr e0)) /* apply object substitution to expression */
| None => e0
};
if (not (exp_equal e0 e)) {
if (not (Exp.equal e0 e)) {
switch e {
| Exp.Lvar pvar => Pvar.pp_value pe f pvar
| _ => assert false
@ -2449,7 +2332,7 @@ let rec sub_compare (sub1: subst) (sub2: subst) =>
if (n != 0) {
n
} else {
let n = exp_compare e1 e2;
let n = Exp.compare e1 e2;
if (n != 0) {
n
} else {
@ -2795,7 +2678,7 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
let instr_sub (subst: subst) instr => instr_sub_ids sub_id_binders::true (apply_sub subst) instr;
let exp_typ_compare (exp1, typ1) (exp2, typ2) => {
let n = exp_compare exp1 exp2;
let n = Exp.compare exp1 exp2;
if (n != 0) {
n
} else {
@ -2810,7 +2693,7 @@ let instr_compare instr1 instr2 =>
if (n != 0) {
n
} else {
let n = exp_compare e1 e2;
let n = Exp.compare e1 e2;
if (n != 0) {
n
} else {
@ -2825,7 +2708,7 @@ let instr_compare instr1 instr2 =>
| (Letderef _, _) => (-1)
| (_, Letderef _) => 1
| (Set e11 t1 e21 loc1, Set e12 t2 e22 loc2) =>
let n = exp_compare e11 e12;
let n = Exp.compare e11 e12;
if (n != 0) {
n
} else {
@ -2833,7 +2716,7 @@ let instr_compare instr1 instr2 =>
if (n != 0) {
n
} else {
let n = exp_compare e21 e22;
let n = Exp.compare e21 e22;
if (n != 0) {
n
} else {
@ -2844,7 +2727,7 @@ let instr_compare instr1 instr2 =>
| (Set _, _) => (-1)
| (_, Set _) => 1
| (Prune cond1 loc1 true_branch1 ik1, Prune cond2 loc2 true_branch2 ik2) =>
let n = exp_compare cond1 cond2;
let n = Exp.compare cond1 cond2;
if (n != 0) {
n
} else {
@ -2867,7 +2750,7 @@ let instr_compare instr1 instr2 =>
if (n != 0) {
n
} else {
let n = exp_compare e1 e2;
let n = Exp.compare e1 e2;
if (n != 0) {
n
} else {
@ -2941,7 +2824,7 @@ let rec exp_compare_structural e1 e2 exp_map => {
let compare_exps_with_map e1 e2 exp_map =>
try {
let e1_mapping = ExpMap.find e1 exp_map;
(exp_compare e1_mapping e2, exp_map)
(Exp.compare e1_mapping e2, exp_map)
} {
| Not_found =>
/* assume e1 and e2 equal, enforce by adding to [exp_map] */
@ -3009,7 +2892,7 @@ let rec exp_compare_structural e1 e2 exp_map => {
} else {
exp_compare_structural f1 f2 exp_map
}
| _ => (exp_compare e1 e2, exp_map)
| _ => (Exp.compare e1 e2, exp_map)
}
};
@ -3174,7 +3057,7 @@ let hpred_sub subst => {
/** {2 Functions for replacing occurrences of expressions.} */
let exp_replace_exp epairs e =>
try {
let (_, e') = IList.find (fun (e1, _) => exp_equal e e1) epairs;
let (_, e') = IList.find (fun (e1, _) => Exp.equal e e1) epairs;
e'
} {
| Not_found => e
@ -3225,7 +3108,7 @@ let hpred_replace_exp epairs =>
/** {2 Compaction} */
let module ExpHash = Hashtbl.Make {
type t = Exp.t;
let equal = exp_equal;
let equal = Exp.equal;
let hash = Hashtbl.hash;
};

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

@ -403,10 +403,6 @@ let attribute_to_category: attribute => attribute_category;
let attr_is_undef: attribute => bool;
let exp_compare: Exp.t => Exp.t => int;
let exp_equal: Exp.t => Exp.t => bool;
/** exp_is_array_index_of index arr returns true is index is an array index of arr. */
let exp_is_array_index_of: Exp.t => Exp.t => bool;

22
infer/src/backend/abs.ml
Unescape View File

@ -434,8 +434,8 @@ let typ_get_recursive_flds tenv typ_exp =
assert false
let discover_para_roots p root1 next1 root2 next2 : Sil.hpara option =
let eq_arg1 = Sil.exp_equal root1 next1 in
let eq_arg2 = Sil.exp_equal root2 next2 in
let eq_arg1 = Exp.equal root1 next1 in
let eq_arg2 = Exp.equal root2 next2 in
let precondition_check = (not eq_arg1 && not eq_arg2) in
if not precondition_check then None
else
@ -449,10 +449,10 @@ let discover_para_roots p root1 next1 root2 next2 : Sil.hpara option =
Some hpara
let discover_para_dll_roots p root1 blink1 flink1 root2 blink2 flink2 : Sil.hpara_dll option =
let eq_arg1 = Sil.exp_equal root1 blink1 in
let eq_arg1' = Sil.exp_equal root1 flink1 in
let eq_arg2 = Sil.exp_equal root2 blink2 in
let eq_arg2' = Sil.exp_equal root2 flink2 in
let eq_arg1 = Exp.equal root1 blink1 in
let eq_arg1' = Exp.equal root1 flink1 in
let eq_arg2 = Exp.equal root2 blink2 in
let eq_arg2' = Exp.equal root2 flink2 in
let precondition_check = not (eq_arg1 || eq_arg1' || eq_arg2 || eq_arg2') in
if not precondition_check then None
else
@ -491,7 +491,7 @@ let discover_para_candidates tenv p =
| [] -> IList.rev found
| (e1, e2) :: edges_notseen ->
let edges_others = (IList.rev edges_seen) @ edges_notseen in
let edges_matched = IList.filter (fun (e1', _) -> Sil.exp_equal e2 e1') edges_others in
let edges_matched = IList.filter (fun (e1', _) -> Exp.equal e2 e1') edges_others in
let new_found =
let f found_acc (_, e3) = (e1, e2, e3) :: found_acc in
IList.fold_left f found edges_matched in
@ -531,7 +531,7 @@ let discover_para_dll_candidates tenv p =
| [] -> IList.rev found
| (iF, blink, flink) :: edges_notseen ->
let edges_others = (IList.rev edges_seen) @ edges_notseen in
let edges_matched = IList.filter (fun (e1', _, _) -> Sil.exp_equal flink e1') edges_others in
let edges_matched = IList.filter (fun (e1', _, _) -> Exp.equal flink e1') edges_others in
let new_found =
let f found_acc (_, _, flink2) = (iF, blink, flink, flink2) :: found_acc in
IList.fold_left f found edges_matched in
@ -608,7 +608,7 @@ let eqs_solve ids_in eqs_in =
solve sub' eqs_rest' in
match eqs with
| [] -> Some sub
| (e1, e2) :: eqs_rest when Sil.exp_equal e1 e2 ->
| (e1, e2) :: eqs_rest when Exp.equal e1 e2 ->
solve sub eqs_rest
| (Exp.Var id1, (Exp.Const _ as e2)) :: eqs_rest ->
do_default id1 e2 eqs_rest
@ -884,7 +884,7 @@ let get_cycle root prop =
| Sil.Eexp(e', _) ->
(try
Some(IList.find (fun hpred -> match hpred with
| Sil.Hpointsto(e'', _, _) -> Sil.exp_equal e'' e'
| Sil.Hpointsto(e'', _, _) -> Exp.equal e'' e'
| _ -> false) sigma)
with _ -> None)
| _ -> None in
@ -959,7 +959,7 @@ let get_var_retain_cycle _prop =
let is_hpred_block v h =
match h, v with
| Sil.Hpointsto (e, _, Exp.Sizeof (typ, _, _)), Sil.Eexp (e', _)
when Sil.exp_equal e e' && Typ.is_block_type typ -> true
when Exp.equal e e' && Typ.is_block_type typ -> true
| _, _ -> false in
let find v =
try

23
infer/src/backend/absarray.ml
Unescape View File

@ -74,7 +74,7 @@ end = struct
Ident.fieldname_equal f' fld) instance_fields) in
get_strexp_at_syn_offsets se' t' syn_offs'
| Sil.Earray (_, esel, _), Typ.Tarray (t', _), Index ind :: syn_offs' ->
let se' = snd (IList.find (fun (i', _) -> Sil.exp_equal i' ind) esel) in
let se' = snd (IList.find (fun (i', _) -> Exp.equal i' ind) esel) in
get_strexp_at_syn_offsets se' t' syn_offs'
| _ ->
L.d_strln "Failure of get_strexp_at_syn_offsets";
@ -99,9 +99,10 @@ end = struct
) fsel in
Sil.Estruct (fsel', inst)
| Sil.Earray (len, esel, inst), Typ.Tarray (t', _), Index idx :: syn_offs' ->
let se' = snd (IList.find (fun (i', _) -> Sil.exp_equal i' idx) esel) in
let se' = snd (IList.find (fun (i', _) -> Exp.equal i' idx) esel) in
let se_mod = replace_strexp_at_syn_offsets se' t' syn_offs' update in
let esel' = IList.map (fun ese -> if Sil.exp_equal (fst ese) idx then (idx, se_mod) else ese) esel in
let esel' =
IList.map (fun ese -> if Exp.equal (fst ese) idx then (idx, se_mod) else ese) esel in
Sil.Earray (len, esel', inst)
| _ -> assert false
@ -136,7 +137,7 @@ end = struct
(** Find an array at the given path. Can raise [Not_found] *)
let find_path sigma (root, syn_offs) : t =
let filter = function
| Sil.Hpointsto (e, _, _) -> Sil.exp_equal root e
| Sil.Hpointsto (e, _, _) -> Exp.equal root e
| _ -> false in
let hpred = IList.find filter sigma in
(sigma, hpred, syn_offs)
@ -210,7 +211,7 @@ end = struct
match se', se_in with
| Sil.Earray (len, esel, _), Sil.Earray (_, esel_in, inst2) ->
let orig_indices = IList.map fst esel in
let index_is_not_new idx = IList.exists (Sil.exp_equal idx) orig_indices in
let index_is_not_new idx = IList.exists (Exp.equal idx) orig_indices in
let process_index idx =
if index_is_not_new idx then idx else (Sil.array_clean_new_index footprint_part idx) in
let esel_in' = IList.map (fun (idx, se) -> process_index idx, se) esel_in in
@ -236,7 +237,10 @@ end = struct
let update se' =
match se' with
| Sil.Earray (len, esel, inst) ->
let esel' = IList.map (fun (e', se') -> if Sil.exp_equal e' index then (index', se') else (e', se')) esel in
let esel' =
IList.map (fun (e', se') ->
if Exp.equal e' index then (index', se') else (e', se')
) esel in
Sil.Earray (len, esel', inst)
| _ -> assert false in
let hpred' = hpred_replace_strexp footprint_part hpred syn_offs update in
@ -273,7 +277,7 @@ let prop_replace_path_index
) [] elist_path in
let expmap_fun e' =
try
let _, fresh_e = IList.find (fun (e, _) -> Sil.exp_equal e e') expmap_list in
let _, fresh_e = IList.find (fun (e, _) -> Exp.equal e e') expmap_list in
fresh_e
with Not_found -> e' in
Prop.prop_expmap expmap_fun p
@ -358,7 +362,7 @@ let index_is_pointed_to (p: Prop.normal Prop.t) (path: StrexpMatch.path) (index:
fun i -> IList.map (add_index i) elist_path in
let pointers = IList.flatten (IList.map add_index_to_paths indices) in
let filter = function
| Sil.Hpointsto (_, Sil.Eexp (e, _), _) -> IList.exists (Sil.exp_equal e) pointers
| Sil.Hpointsto (_, Sil.Eexp (e, _), _) -> IList.exists (Exp.equal e) pointers
| _ -> false in
IList.exists filter (Prop.get_sigma p)
@ -419,7 +423,8 @@ let keep_only_indices
let (_, se, _) = StrexpMatch.get_data matched in
match se with
| Sil.Earray (len, esel, inst) ->
let esel', esel_leftover' = IList.partition (fun (e, _) -> IList.exists (Sil.exp_equal e) indices) esel in
let esel', esel_leftover' =
IList.partition (fun (e, _) -> IList.exists (Exp.equal e) indices) esel in
if esel_leftover' == [] then (sigma, false)
else begin
let se' = Sil.Earray (len, esel', inst) in

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

@ -39,7 +39,7 @@ let sigma_equal sigma1 sigma2 =
f sigma1_sorted sigma2_sorted
let sigma_get_start_lexps_sort sigma =
let exp_compare_neg e1 e2 = - (Sil.exp_compare e1 e2) in
let exp_compare_neg e1 e2 = - (Exp.compare e1 e2) in
let filter e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
let lexps = Sil.hpred_list_get_lexps filter sigma in
IList.sort exp_compare_neg lexps
@ -69,9 +69,9 @@ module EPset = Set.Make
(struct
type t = Exp.t * Exp.t
let compare (e1, e1') (e2, e2') =
match (Sil.exp_compare e1 e2) with
match (Exp.compare e1 e2) with
| i when i <> 0 -> i
| _ -> Sil.exp_compare e1' e2'
| _ -> Exp.compare e1' e2'
end)
(** {2 Module for maintaining information about noninjectivity during join} *)
@ -120,7 +120,7 @@ end = struct
let e' = lookup_equiv' tbl e in
match e' with
| Exp.Var _ ->
if Sil.exp_equal e e' then e
if Exp.equal e e' then e
else
begin
let root = find' tbl e' in
@ -133,7 +133,7 @@ end = struct
let r1 = find' tbl e1 in
let r2 = find' tbl e2 in
let new_r, old_r =
match (Sil.exp_compare r1 r2) with
match (Exp.compare r1 r2) with
| i when i <= 0 -> r1, r2
| _ -> r2, r1 in
let new_c = lookup_const' const_tbl new_r in
@ -171,7 +171,7 @@ end = struct
if (can_rename id') then replace_const' tbl const_tbl e' e
else (L.d_strln "failure reason 7"; raise IList.Fail)
| _ ->
if not (Sil.exp_equal e e') then (L.d_strln "failure reason 8"; raise IList.Fail) else ()
if not (Exp.equal e e') then (L.d_strln "failure reason 8"; raise IList.Fail) else ()
let check side es =
let f = function Exp.Var id -> can_rename id | _ -> false in
@ -188,7 +188,7 @@ end = struct
| v:: vars', _ ->
let r = find' tbl v in
let set = lookup_const' const_tbl r in
(IList.for_all (fun v' -> Sil.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)
end
@ -255,7 +255,7 @@ module CheckJoinPre : InfoLossCheckerSig = struct
| Exp.Var id when Ident.is_normal id -> IList.length es >= 1
| Exp.Var _ ->
if Config.join_cond = 0 then
IList.exists (Sil.exp_equal Sil.exp_zero) es
IList.exists (Exp.equal Sil.exp_zero) es
else if Dangling.check side e then
begin
let r = IList.exists (fun e' -> not (Dangling.check side_op e')) es in
@ -449,12 +449,12 @@ end = struct
let final () = t := []
let entry_compare (e1, e2, _) (_, e2', _) =
let n1 = Sil.exp_compare e1 e2 in
if n1 <> 0 then n1 else Sil.exp_compare e2 e2'
let n1 = Exp.compare e1 e2 in
if n1 <> 0 then n1 else Exp.compare e2 e2'
let get_fresh_exp e1 e2 =
try
let (_, _, e) = IList.find (fun (e1', e2', _) -> Sil.exp_equal e1 e1' && Sil.exp_equal e2 e2') !t in
let (_, _, e) = IList.find (fun (e1', e2', _) -> Exp.equal e1 e1' && Exp.equal e2 e2') !t in
e
with Not_found ->
let e = Sil.exp_get_undefined (JoinState.get_footprint ()) in
@ -512,7 +512,7 @@ end = struct
let lookup side e =
try
let (e1, e2, e) =
IList.find (fun (e1', e2', _) -> Sil.exp_equal e (select side e1' e2')) !t in
IList.find (fun (e1', e2', _) -> Exp.equal e (select side e1' e2')) !t in
Some (e, select (opposite side) e1 e2)
with Not_found ->
None
@ -573,7 +573,7 @@ end = struct
| Exp.Const _ -> []
| Exp.Lvar _ | Exp.Var _
| Exp.BinOp (Binop.PlusA, Exp.Var _, _) ->
let is_same_e (e1, e2, _) = Sil.exp_equal e (select side e1 e2) in
let is_same_e (e1, e2, _) = Exp.equal e (select side e1 e2) in
let assoc = IList.filter is_same_e !tbl in
IList.map (fun (e1, e2, _) -> select side_op e1 e2) assoc
| _ ->
@ -585,19 +585,19 @@ end = struct
(IList.for_all (f Rhs) rhs_es) && (IList.for_all (f Lhs) lhs_es)
let lookup_side' side e =
let f (e1, e2, _) = Sil.exp_equal e (select side e1 e2) in
let f (e1, e2, _) = Exp.equal e (select side e1 e2) in
IList.filter f !tbl
let lookup_side_induced' side e =
let res = ref [] in
let f v = match v, side with
| (Exp.BinOp (Binop.PlusA, e1', Exp.Const (Const.Cint i)), e2, e'), Lhs
when Sil.exp_equal e e1' ->
when Exp.equal e e1' ->
let c' = Sil.exp_int (IntLit.neg i) in
let v' = (e1', Exp.BinOp(Binop.PlusA, e2, c'), Exp.BinOp (Binop.PlusA, e', c')) in
res := v'::!res
| (e1, Exp.BinOp (Binop.PlusA, e2', Exp.Const (Const.Cint i)), e'), Rhs
when Sil.exp_equal e e2' ->
when Exp.equal e e2' ->
let c' = Sil.exp_int (IntLit.neg i) in
let v' = (Exp.BinOp(Binop.PlusA, e1, c'), e2', Exp.BinOp (Binop.PlusA, e', c')) in
res := v'::!res
@ -633,10 +633,10 @@ end = struct
(function (e1, e2, Exp.Var i) -> (i, select side e1 e2) | _ -> assert false)
renaming_restricted in
let sub_list_side_sorted =
IList.sort (fun (_, e) (_, e') -> Sil.exp_compare e e') sub_list_side in
IList.sort (fun (_, e) (_, e') -> Exp.compare e e') sub_list_side in
let rec find_duplicates =
function
| (_, e):: ((_, e'):: _ as t) -> Sil.exp_equal e e' || find_duplicates t
| (_, e):: ((_, e'):: _ as t) -> Exp.equal e e' || find_duplicates t
| _ -> false in
if find_duplicates sub_list_side_sorted then (L.d_strln "failure reason 11"; raise IList.Fail)
else Sil.sub_of_list sub_list_side
@ -751,7 +751,7 @@ end = struct
* should be a primed or footprint variable *)
let extend e1 e2 default_op =
try
let eq_to_e (f1, f2, _) = Sil.exp_equal e1 f1 && Sil.exp_equal e2 f2 in
let eq_to_e (f1, f2, _) = Exp.equal e1 f1 && Exp.equal e2 f2 in
let _, _, res = IList.find eq_to_e !tbl in
res
with Not_found ->
@ -762,7 +762,7 @@ end = struct
let some_primed () = Sil.fav_exists fav1 Ident.is_primed || Sil.fav_exists fav2 Ident.is_primed in
let e =
if (no_ren1 && no_ren2) then
if (Sil.exp_equal e1 e2) then e1 else (L.d_strln "failure reason 13"; raise IList.Fail)
if (Exp.equal e1 e2) then e1 else (L.d_strln "failure reason 13"; raise IList.Fail)
else
match default_op with
| ExtDefault e -> e
@ -775,7 +775,7 @@ end = struct
e
(*
let get e1 e2 =
let f (e1', e2', _) = Sil.exp_equal e1 e1' && Sil.exp_equal e2 e2' in
let f (e1', e2', _) = Exp.equal e1 e1' && Exp.equal e2 e2' in
match (IList.filter f !tbl) with
| [] -> None
| (_, _, e):: _ -> Some e
@ -1170,7 +1170,7 @@ let rec strexp_partial_meet (strexp1: Sil.strexp) (strexp2: Sil.strexp) : Sil.st
let inst = Sil.inst_partial_meet inst1 inst2 in
f_fld_se_list inst [] fld_se_list1 fld_se_list2
| Sil.Earray (len1, idx_se_list1, inst1), Sil.Earray (len2, idx_se_list2, inst2)
when Sil.exp_equal len1 len2 ->
when Exp.equal len1 len2 ->
let inst = Sil.inst_partial_meet inst1 inst2 in
f_idx_se_list inst len1 [] idx_se_list1 idx_se_list2
| _ -> (L.d_strln "failure reason 52"; raise IList.Fail)
@ -1235,8 +1235,8 @@ let hpred_partial_join mode (todo: Exp.t * Exp.t * Exp.t) (hpred1: Sil.hpred) (h
Prop.mk_lseg (kind_join k1 k2) hpara' e next' shared'
| Sil.Hdllseg (k1, para1, iF1, oB1, oF1, iB1, shared1),
Sil.Hdllseg (k2, para2, iF2, oB2, oF2, iB2, shared2) ->
let fwd1 = Sil.exp_equal e1 iF1 in
let fwd2 = Sil.exp_equal e2 iF2 in
let fwd1 = Exp.equal e1 iF1 in
let fwd2 = Exp.equal e2 iF2 in
let hpara' = hpara_dll_partial_join para1 para2 in
let iF', iB' =
if (fwd1 && fwd2) then (e, exp_partial_join iB1 iB2)
@ -1253,7 +1253,7 @@ let hpred_partial_meet (todo: Exp.t * Exp.t * Exp.t) (hpred1: Sil.hpred) (hpred2
: Sil.hpred =
let e1, e2, e = todo in
match hpred1, hpred2 with
| Sil.Hpointsto (_, se1, te1), Sil.Hpointsto (_, se2, te2) when Sil.exp_equal te1 te2 ->
| Sil.Hpointsto (_, se1, te1), Sil.Hpointsto (_, se2, te2) when Exp.equal te1 te2 ->
Prop.mk_ptsto e (strexp_partial_meet se1 se2) te1
| Sil.Hpointsto _, _ | _, Sil.Hpointsto _ ->
(L.d_strln "failure reason 58"; raise IList.Fail)
@ -1264,8 +1264,8 @@ let hpred_partial_meet (todo: Exp.t * Exp.t * Exp.t) (hpred1: Sil.hpred) (hpred2
Prop.mk_lseg (kind_meet k1 k2) hpara' e next' shared'
| Sil.Hdllseg (k1, para1, iF1, oB1, oF1, iB1, shared1),
Sil.Hdllseg (k2, para2, iF2, oB2, oF2, iB2, shared2) ->
let fwd1 = Sil.exp_equal e1 iF1 in
let fwd2 = Sil.exp_equal e2 iF2 in
let fwd1 = Exp.equal e1 iF1 in
let fwd2 = Exp.equal e2 iF2 in
let hpara' = hpara_dll_partial_meet para1 para2 in
let iF', iB' =
if (fwd1 && fwd2) then (e, exp_partial_meet iB1 iB2)
@ -1337,7 +1337,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
Sil.Hlseg (Sil.Lseg_PE, hpara, root', next', shared')
| Sil.Hdllseg (_, hpara, iF, oB, oF, iB, shared)
when Sil.exp_equal iF e ->
when Exp.equal iF e ->
let oF' = do_side side exp_partial_join oF opposite in
let shared' = Rename.lookup_list side shared in
let oB', iB' = lookup_and_expand side oB iB in
@ -1350,7 +1350,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
Sil.Hdllseg (Sil.Lseg_PE, hpara, root', oB', oF', iB', shared')
| Sil.Hdllseg (_, hpara, iF, oB, oF, iB, shared)
when Sil.exp_equal iB e ->
when Exp.equal iB e ->
let oB' = do_side side exp_partial_join oB opposite in
let shared' = Rename.lookup_list side shared in
let oF', iF' = lookup_and_expand side oF iF in
@ -1467,7 +1467,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
sigma_partial_join' mode sigma_acc' sigma1' sigma2
| Some (Sil.Hdllseg (_, _, iF1, _, _, iB1, _) as dllseg), Some (hpred2)
when Sil.exp_equal e1 iF1 ->
when Exp.equal e1 iF1 ->
let iB_res = exp_partial_join iB1 e2 in
let sigma2' = cut_dllseg Lhs todo_curr iF1 dllseg (hpred2:: sigma2) in
let sigma_acc' = update_dllseg Lhs dllseg e iB_res :: sigma_acc in
@ -1475,7 +1475,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
sigma_partial_join' mode sigma_acc' sigma1 sigma2'
| Some (Sil.Hdllseg (_, _, iF1, _, _, iB1, _) as dllseg), Some (hpred2)
(* when Sil.exp_equal e1 iB1 *) ->
(* when Exp.equal e1 iB1 *) ->
let iF_res = exp_partial_join iF1 e2 in
let sigma2' = cut_dllseg Lhs todo_curr iB1 dllseg (hpred2:: sigma2) in
let sigma_acc' = update_dllseg Lhs dllseg iF_res e :: sigma_acc in
@ -1483,7 +1483,7 @@ let rec sigma_partial_join' mode (sigma_acc: Prop.sigma)
sigma_partial_join' mode sigma_acc' sigma1 sigma2'
| Some (hpred1), Some (Sil.Hdllseg (_, _, iF2, _, _, iB2, _) as dllseg)
when Sil.exp_equal e2 iF2 ->
when Exp.equal e2 iF2 ->
let iB_res = exp_partial_join e1 iB2 in
let sigma1' = cut_dllseg Rhs todo_curr iF2 dllseg (hpred1:: sigma1) in
let sigma_acc' = update_dllseg Rhs dllseg e iB_res :: sigma_acc in
@ -1622,11 +1622,11 @@ let pi_partial_join mode
let is_stronger_le e n a =
match Prop.atom_exp_le_const a with
| None -> false
| Some (e', n') -> Sil.exp_equal e e' && IntLit.lt n' n in
| Some (e', n') -> Exp.equal e e' && IntLit.lt n' n in
let is_stronger_lt n e a =
match Prop.atom_const_lt_exp a with
| None -> false
| Some (n', e') -> Sil.exp_equal e e' && IntLit.lt n n' in
| Some (n', e') -> Exp.equal e e' && IntLit.lt n n' in
let join_atom_check_pre p a =
(* check for atoms in pre mode: fail if the negation is implied by the other side *)
let not_a = Prop.atom_negate a in
@ -1735,7 +1735,7 @@ let eprop_partial_meet (ep1: 'a Prop.t) (ep2: 'b Prop.t) : 'c Prop.t =
let es1 = sigma_get_start_lexps_sort sigma1 in
let es2 = sigma_get_start_lexps_sort sigma2 in
let es = IList.merge_sorted_nodup Sil.exp_compare [] es1 es2 in
let es = IList.merge_sorted_nodup Exp.compare [] es1 es2 in
let sub_check _ =
let sub1 = Prop.get_sub ep1 in
@ -1785,7 +1785,7 @@ let eprop_partial_join' mode (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop.
| [], [] -> true
| [], _:: _ | _:: _, [] -> false
| e1:: es1'', e2:: es2'' ->
Sil.exp_equal e1 e2 && expensive_check es1'' es2'' in
Exp.equal e1 e2 && expensive_check es1'' es2'' in
let sub_common, eqs_from_sub1, eqs_from_sub2 =
let sub1 = Prop.get_sub ep1 in
let sub2 = Prop.get_sub ep2 in

49
infer/src/backend/dotty.ml
Unescape View File

@ -173,7 +173,7 @@ and get_contents pe coo f = function
(* true if node is the sorce node of the expression e*)
let is_source_node_of_exp e node =
match node with
| Dotpointsto (_, e', _) -> Sil.exp_compare e e' = 0
| Dotpointsto (_, e', _) -> Exp.compare e e' = 0
| _ -> false
(* given a node returns its coordinates and the expression. Return -1 in case the expressio doesn.t*)
@ -203,7 +203,7 @@ let rec look_up_for_back_pointer e dotnodes lambda =
match dotnodes with
| [] -> []
| Dotdllseg(coo, _, _, _, e4, _, _, _):: dotnodes' ->
if Sil.exp_compare e e4 = 0 && lambda = coo.lambda then [coo.id + 1]
if Exp.compare e e4 = 0 && lambda = coo.lambda then [coo.id + 1]
else look_up_for_back_pointer e dotnodes' lambda
| _:: dotnodes' -> look_up_for_back_pointer e dotnodes' lambda
@ -213,7 +213,8 @@ let rec select_nodes_exp_lambda dotnodes e lambda =
| [] -> []
| node:: l' ->
let (coo, e') = get_coordinate_and_exp node in
if (Sil.exp_compare e e' = 0) && lambda = coo.lambda then node:: select_nodes_exp_lambda l' e lambda
if (Exp.compare e e' = 0) && lambda = coo.lambda
then node:: select_nodes_exp_lambda l' e lambda
else select_nodes_exp_lambda l' e lambda
(* look-up the coordinate id in the list of dotnodes those nodes which correspond to expression e*)
@ -245,19 +246,19 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
let coo = mk_coordinate n lambda in
(match hpred with
| Sil.Hpointsto (_, Sil.Eexp (e, _), _)
when not (Sil.exp_equal e Sil.exp_zero) && !print_full_prop ->
when not (Exp.equal e Sil.exp_zero) && !print_full_prop ->
let e_color_str = color_to_str (exp_color hpred e) in
[Dotdangling(coo, e, e_color_str)]
| Sil.Hlseg (_, _, _, e2, _) when not (Sil.exp_equal e2 Sil.exp_zero) ->
| Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Sil.exp_zero) ->
let e2_color_str = color_to_str (exp_color hpred e2) in
[Dotdangling(coo, e2, e2_color_str)]
| Sil.Hdllseg (_, _, _, e2, e3, _, _) ->
let e2_color_str = color_to_str (exp_color hpred e2) in
let e3_color_str = color_to_str (exp_color hpred e3) in
let ll = if not (Sil.exp_equal e2 Sil.exp_zero) then
let ll = if not (Exp.equal e2 Sil.exp_zero) then
[Dotdangling(coo, e2, e2_color_str)]
else [] in
if not (Sil.exp_equal e3 Sil.exp_zero) then Dotdangling(coo, e3, e3_color_str):: ll
if not (Exp.equal e3 Sil.exp_zero) then Dotdangling(coo, e3, e3_color_str):: ll
else ll
| Sil.Hpointsto (_, _, _)
| _ -> [] (* arrays and struct do not give danglings*)
@ -269,7 +270,7 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
| Dotpointsto(_, e', _)
| Dotarray(_, _, e', _, _, _)
| Dotlseg(_, e', _, _, _, _)
| Dotdllseg(_, e', _, _, _, _, _, _) -> Sil.exp_equal e e'
| Dotdllseg(_, e', _, _, _, _, _, _) -> Exp.equal e e'
| _ -> false
) allocated_nodes
| _ -> false (*this should never happen since d must be a dangling node *) in
@ -277,7 +278,7 @@ let make_dangling_boxes pe allocated_nodes (sigma_lambda: (Sil.hpred * int) list
match l with
| [] -> []
| Dotdangling(coo, e, color):: l' ->
if (IList.exists (Sil.exp_equal e) seen_exp) then filter_duplicate l' seen_exp
if (IList.exists (Exp.equal e) seen_exp) then filter_duplicate l' seen_exp
else Dotdangling(coo, e, color):: filter_duplicate l' (e:: seen_exp)
| box:: l' -> box:: filter_duplicate l' seen_exp (* this case cannot happen*) in
let rec subtract_allocated candidate_dangling =
@ -308,7 +309,7 @@ let rec dotty_mk_node pe sigma =
Dotstruct((mk_coordinate (n + 1) lambda), e, l, e_color_str, te);]
| (Sil.Hpointsto (e, _, _), lambda) ->
let e_color_str = color_to_str (exp_color e) in
if IList.mem Sil.exp_equal e !struct_exp_nodes then [] else
if IList.mem Exp.equal e !struct_exp_nodes then [] else
[Dotpointsto((mk_coordinate n lambda), e, e_color_str)]
| (Sil.Hlseg (k, hpara, e1, e2, _), lambda) ->
incr dotty_state_count; (* increment once more n+1 is the box for last element of the list *)
@ -336,7 +337,7 @@ let set_exps_neq_zero pi =
let box_dangling e =
let entry_e = IList.filter (fun b -> match b with
| Dotdangling(_, e', _) -> Sil.exp_equal e e' | _ -> false ) !dangling_dotboxes in
| Dotdangling(_, e', _) -> Exp.equal e e' | _ -> false ) !dangling_dotboxes in
match entry_e with
|[] -> None
| Dotdangling(coo, _, _):: _ -> Some coo.id
@ -376,7 +377,7 @@ let compute_struct_exp_nodes sigma =
let get_node_exp n = snd (get_coordinate_and_exp n)
let is_nil e prop =
(Sil.exp_equal e Sil.exp_zero) || (Prover.check_equal prop e Sil.exp_zero)
(Exp.equal e Sil.exp_zero) || (Prover.check_equal prop e Sil.exp_zero)
(* an edge is in cycle *)
let in_cycle cycle edge =
@ -413,7 +414,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
)
| [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] ->
let n = get_coordinate_id node in
if IList.mem Sil.exp_equal e !struct_exp_nodes then begin
if IList.mem Exp.equal e !struct_exp_nodes then begin
let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in
let link_kind = if (in_cycle cycle (fn, se)) && (not !print_full_prop) then
LinkRetainCycle
@ -449,7 +450,7 @@ let rec compute_target_array_elements dotnodes list_elements p f lambda =
)
| [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] ->
let n = get_coordinate_id node in
if IList.mem Sil.exp_equal e !struct_exp_nodes then begin
if IList.mem Exp.equal e !struct_exp_nodes then begin
let e_no_special_char = strip_special_chars (Sil.exp_to_string e) in
[(LinkArrayToStruct, Sil.exp_to_string idx, n, e_no_special_char)]
end else
@ -1112,7 +1113,7 @@ let atom_to_xml_string a =
(* return the dangling node corresponding to an expression it exists or None *)
let exp_dangling_node e =
let entry_e = IList.filter (fun b -> match b with
| VH_dangling(_, e') -> Sil.exp_equal e e' | _ -> false ) !set_dangling_nodes in
| VH_dangling(_, e') -> Exp.equal e e' | _ -> false ) !set_dangling_nodes in
match entry_e with
|[] -> None
| VH_dangling(n, e') :: _ -> Some (VH_dangling(n, e'))
@ -1156,7 +1157,7 @@ let rec select_node_at_address nodes e =
| [] -> None
| n:: l' ->
let e' = get_node_addr n in
if (Sil.exp_compare e e' = 0) then Some n
if (Exp.compare e e' = 0) then Some n
else select_node_at_address l' e
(* look-up the ids in the list of nodes corresponding to expression e*)
@ -1171,11 +1172,11 @@ let make_set_dangling_nodes allocated_nodes (sigma: Sil.hpred list) =
VH_dangling(n, e) in
let get_rhs_predicate hpred =
(match hpred with
| Sil.Hpointsto (_, Sil.Eexp (e, _), _) when not (Sil.exp_equal e Sil.exp_zero) -> [e]
| Sil.Hlseg (_, _, _, e2, _) when not (Sil.exp_equal e2 Sil.exp_zero) -> [e2]
| Sil.Hpointsto (_, Sil.Eexp (e, _), _) when not (Exp.equal e Sil.exp_zero) -> [e]
| Sil.Hlseg (_, _, _, e2, _) when not (Exp.equal e2 Sil.exp_zero) -> [e2]
| Sil.Hdllseg (_, _, _, e2, e3, _, _) ->
if (Sil.exp_equal e2 Sil.exp_zero) then
if (Sil.exp_equal e3 Sil.exp_zero) then []
if (Exp.equal e2 Sil.exp_zero) then
if (Exp.equal e3 Sil.exp_zero) then []
else [e3]
else [e2; e3]
| Sil.Hpointsto (_, _, _)
@ -1185,14 +1186,14 @@ let make_set_dangling_nodes allocated_nodes (sigma: Sil.hpred list) =
let allocated = IList.exists (fun a -> match a with
| VH_pointsto(_, e', _, _)
| VH_lseg(_, e', _ , _)
| VH_dllseg(_, e', _, _, _, _) -> Sil.exp_equal e e'
| VH_dllseg(_, e', _, _, _, _) -> Exp.equal e e'
| _ -> false ) allocated_nodes in
not allocated in
let rec filter_duplicate l seen_exp =
match l with
| [] -> []
| e:: l' ->
if (IList.exists (Sil.exp_equal e) seen_exp) then filter_duplicate l' seen_exp
if (IList.exists (Exp.equal e) seen_exp) then filter_duplicate l' seen_exp
else e:: filter_duplicate l' (e:: seen_exp) in
let rhs_exp_list = IList.flatten (IList.map get_rhs_predicate sigma) in
let candidate_dangling_exps = filter_duplicate rhs_exp_list [] in
@ -1408,7 +1409,7 @@ let print_specs_xml signature specs loc fmt =
(*
let exp_is_neq_zero e =
IList.exists (fun e' -> Sil.exp_equal e e') !exps_neq_zero
IList.exists (fun e' -> Exp.equal e e') !exps_neq_zero
let rec get_contents_range_single pe coo f range_se =
let (e1, e2), se = range_se in
@ -1454,5 +1455,5 @@ let rec get_color_exp dot_nodes e =
| Dotlseg(_, e', _, _, _, c):: l'
| Dotstruct(_, e', _, c, _):: l'
| Dotdllseg(_, e', _, _, _, _, _, c):: l' ->
if (Sil.exp_equal e e') then c else get_color_exp l' e
if (Exp.equal e e') then c else get_color_exp l' e
*)

20
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 Sil.exp_equal (Exp.Var id) e -> Some instr
| Sil.Set (Exp.Lvar _, _, e, _) when Exp.equal (Exp.Var id) e -> Some instr
| _ -> None in
find_in_node_or_preds node find_set
@ -453,7 +453,7 @@ let leak_from_list_abstraction hpred prop =
| _ -> None in
let found = ref false in
let check_hpred texp hp = match hpred_type hp with
| Some texp' when Sil.exp_equal texp texp' -> found := true
| Some texp' when Exp.equal texp texp' -> found := true
| _ -> () in
let check_hpara texp _ hpara =
IList.iter (check_hpred texp) hpara.Sil.body in
@ -479,7 +479,7 @@ let find_hpred_typ hpred = match hpred with
let find_typ_without_ptr prop pvar =
let res = ref None in
let do_hpred = function
| Sil.Hpointsto (e, _, te) when Sil.exp_equal e (Exp.Lvar pvar) ->
| Sil.Hpointsto (e, _, te) when Exp.equal e (Exp.Lvar pvar) ->
res := Some te
| _ -> () in
IList.iter do_hpred (Prop.get_sigma prop);
@ -586,7 +586,7 @@ let vpath_find prop _exp : DExp.t option * Typ.t option =
if verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ());
let rec find sigma_acc sigma_todo exp =
let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with
| Sil.Eexp (e, _) when Sil.exp_equal exp e ->
| Sil.Eexp (e, _) when Exp.equal exp e ->
let sigma' = (IList.rev_append sigma_acc' sigma_todo') in
(match lexp with
| Exp.Lvar pv ->
@ -612,7 +612,7 @@ let vpath_find prop _exp : DExp.t option * Typ.t option =
Sil.d_exp lexp; L.d_ln ()))
| _ -> () in
let do_sexp sigma_acc' sigma_todo' lexp sexp texp = match sexp with
| Sil.Eexp (e, _) when Sil.exp_equal exp e ->
| Sil.Eexp (e, _) when Exp.equal exp e ->
let sigma' = (IList.rev_append sigma_acc' sigma_todo') in
(match lexp with
| Exp.Lvar pv when not (Pvar.is_frontend_tmp pv) ->
@ -682,7 +682,7 @@ let explain_dexp_access prop dexp is_nullable =
let find_ptsto (e : Exp.t) : Sil.strexp option =
let res = ref None in
let do_hpred = function
| Sil.Hpointsto (e', se, _) when Sil.exp_equal e e' ->
| Sil.Hpointsto (e', se, _) when Exp.equal e e' ->
res := Some se
| _ -> () in
IList.iter do_hpred sigma;
@ -701,7 +701,7 @@ let explain_dexp_access prop dexp is_nullable =
if verbose then (L.d_str "lookup_esel: can't find index "; Sil.d_exp e; L.d_ln ());
None
| (e1, se):: esel' ->
if Sil.exp_equal e1 e then Some se
if Exp.equal e1 e then Some se
else lookup_esel esel' e in
let rec lookup : DExp.t -> Sil.strexp option = function
| DExp.Dconst c ->
@ -1006,17 +1006,17 @@ let find_with_exp prop exp =
if !res = None then res := Some (pv, Fstruct (IList.rev fld_lst)) in
let rec search_struct pv fld_lst = function
| Sil.Eexp (e, _) ->
if Sil.exp_equal e exp then found_in_struct pv fld_lst
if Exp.equal e exp then found_in_struct pv fld_lst
| Sil.Estruct (fsel, _) ->
IList.iter (fun (f, se) -> search_struct pv (f:: fld_lst) se) fsel
| _ -> () in
let do_hpred_pointed_by_pvar pv e = function
| Sil.Hpointsto(e1, se, _) ->
if Sil.exp_equal e e1 then search_struct pv [] se
if Exp.equal e e1 then search_struct pv [] se
| _ -> () in
let do_hpred = function
| Sil.Hpointsto(Exp.Lvar pv, Sil.Eexp (e, _), _) ->
if Sil.exp_equal e exp then found_in_pvar pv
if Exp.equal e exp then found_in_pvar pv
else IList.iter (do_hpred_pointed_by_pvar pv e) (Prop.get_sigma prop)
| _ -> () in
IList.iter do_hpred (Prop.get_sigma prop);

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

@ -409,7 +409,7 @@ let check_assignement_guard node =
[e']
| _ -> [] in
let prune_vars = IList.flatten(IList.map (fun n -> prune_var n) succs) in
IList.for_all (fun e' -> Sil.exp_equal e' e) prune_vars in
IList.for_all (fun e' -> Exp.equal e' e) prune_vars in
let succs_loc = IList.map (fun n -> Cfg.Node.get_loc n) succs in
let succs_are_all_prune_nodes () =
IList.for_all (fun n -> match Cfg.Node.get_kind n with
@ -1120,7 +1120,7 @@ let remove_this_not_null prop =
| hpred -> (var_option, hpred:: hpreds) in
let collect_atom var atoms = function
| Sil.Aneq (Exp.Var v, e)
when Ident.equal v var && Sil.exp_equal e Sil.exp_null -> atoms
when Ident.equal v var && Exp.equal e Sil.exp_null -> atoms
| a -> a:: atoms in
match IList.fold_left collect_hpred (None, []) (Prop.get_sigma prop) with
| None, _ -> prop

32
infer/src/backend/match.ml
Unescape View File

@ -38,7 +38,7 @@ let rec pp_hpat_list pe f = function
let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
let check_equal sub vars e1 e2 =
let e2_inst = Sil.exp_sub sub e2
in if (Sil.exp_equal e1 e2_inst) then Some(sub, vars) else None in
in if (Exp.equal e1 e2_inst) then Some(sub, vars) else None in
match e1, e2 with
| _, Exp.Var id2 when (Ident.is_primed id2 && mem_idlist id2 vars) ->
let vars_new = IList.filter (fun id -> not (Ident.equal id id2)) vars in
@ -148,7 +148,7 @@ and isel_match isel1 sub vars isel2 =
L.out "@[<4> IDX2: %a, STREXP2: %a@\n@." (Sil.pp_exp pe) idx2 (Sil.pp_sexp pe) se2';
assert false
end
else if Sil.exp_equal idx1 idx2 then begin
else if Exp.equal idx1 idx2 then begin
match strexp_match se1' sub vars se2' with
| None -> None
| Some (sub', vars') -> isel_match isel1' sub' vars' isel2'
@ -246,7 +246,7 @@ let rec iter_match_with_impl iter condition sub vars hpat hpats =
in prop_match_with_impl_sub p_rest condition sub_new vars_leftover hpat_next hpats_rest
in
let gen_filter_pointsto lexp2 strexp2 te2 = function
| Sil.Hpointsto (lexp1, strexp1, te1) when Sil.exp_equal te1 te2 ->
| Sil.Hpointsto (lexp1, strexp1, te1) when Exp.equal te1 te2 ->
(match (exp_match lexp1 sub vars lexp2) with
| None -> None
| Some (sub', vars_leftover) -> strexp_match strexp1 sub' vars_leftover strexp2)
@ -502,7 +502,7 @@ let rec generate_todos_from_strexp mode todos sexp1 sexp2 =
| Sil.Estruct _, _ ->
None
| Sil.Earray (len1, iel1, _), Sil.Earray (len2, iel2, _) ->
if (not (Sil.exp_equal len1 len2) || IList.length iel1 <> IList.length iel2)
if (not (Exp.equal len1 len2) || IList.length iel1 <> IList.length iel2)
then None
else generate_todos_from_iel mode todos iel1 iel2
| Sil.Earray _, _ ->
@ -548,22 +548,22 @@ and generate_todos_from_iel mode todos iel1 iel2 =
(** add (e1,e2) at the front of corres, if necessary. *)
let corres_extend_front e1 e2 corres =
let filter (e1', e2') = (Sil.exp_equal e1 e1') || (Sil.exp_equal e2 e2') in
let checker e1' e2' = (Sil.exp_equal e1 e1') && (Sil.exp_equal e2 e2')
let filter (e1', e2') = (Exp.equal e1 e1') || (Exp.equal e2 e2') in
let checker e1' e2' = (Exp.equal e1 e1') && (Exp.equal e2 e2')
in match (IList.filter filter corres) with
| [] -> Some ((e1, e2) :: corres)
| [(e1', e2')] when checker e1' e2' -> Some corres
| _ -> None
let corres_extensible corres e1 e2 =
let predicate (e1', e2') = (Sil.exp_equal e1 e1') || (Sil.exp_equal e2 e2')
in not (IList.exists predicate corres) && not (Sil.exp_equal e1 e2)
let predicate (e1', e2') = (Exp.equal e1 e1') || (Exp.equal e2 e2')
in not (IList.exists predicate corres) && not (Exp.equal e1 e2)
let corres_related corres e1 e2 =
let filter (e1', e2') = (Sil.exp_equal e1 e1') || (Sil.exp_equal e2 e2') in
let checker e1' e2' = (Sil.exp_equal e1 e1') && (Sil.exp_equal e2 e2') in
let filter (e1', e2') = (Exp.equal e1 e1') || (Exp.equal e2 e2') in
let checker e1' e2' = (Exp.equal e1 e1') && (Exp.equal e2 e2') in
match (IList.filter filter corres) with
| [] -> Sil.exp_equal e1 e2
| [] -> Exp.equal e1 e2
| [(e1', e2')] when checker e1' e2' -> true
| _ -> false
@ -604,7 +604,7 @@ let rec generic_find_partial_iso mode update corres sigma_corres todos sigma_tod
| None, _ | _, None ->
None
| Some (Sil.Hpointsto (_, _, te1)), Some (Sil.Hpointsto (_, _, te2))
when not (Sil.exp_equal te1 te2) ->
when not (Exp.equal te1 te2) ->
None
| Some (Sil.Hpointsto (_, se1, _) as hpred1),
Some (Sil.Hpointsto (_, se2, _) as hpred2) ->
@ -723,9 +723,9 @@ let generic_para_create corres sigma1 elist1 =
let add_fresh_id pair = (pair, Ident.create_fresh Ident.kprimed) in
IList.map add_fresh_id new_corres' in
let (es_shared, ids_shared, ids_exists) =
let not_in_elist1 ((e1, _), _) = not (IList.exists (Sil.exp_equal e1) elist1) in
let not_in_elist1 ((e1, _), _) = not (IList.exists (Exp.equal e1) elist1) in
let corres_ids_no_elist1 = IList.filter not_in_elist1 corres_ids in
let should_be_shared ((e1, e2), _) = Sil.exp_equal e1 e2 in
let should_be_shared ((e1, e2), _) = Exp.equal e1 e2 in
let shared, exists = IList.partition should_be_shared corres_ids_no_elist1 in
let es_shared = IList.map (fun ((e1, _), _) -> e1) shared in
(es_shared, IList.map snd shared, IList.map snd exists) in
@ -745,7 +745,7 @@ let hpara_create corres sigma1 root1 next1 =
generic_para_create corres sigma1 [root1; next1] in
let get_id1 e1 =
try
let is_equal_to_e1 (e1', _) = Sil.exp_equal e1 e1' in
let is_equal_to_e1 (e1', _) = Exp.equal e1 e1' in
let _, id = IList.find is_equal_to_e1 renaming in
id
with Not_found -> assert false in
@ -768,7 +768,7 @@ let hpara_dll_create corres sigma1 root1 blink1 flink1 =
generic_para_create corres sigma1 [root1; blink1; flink1] in
let get_id1 e1 =
try
let is_equal_to_e1 (e1', _) = Sil.exp_equal e1 e1' in
let is_equal_to_e1 (e1', _) = Exp.equal e1 e1' in
let _, id = IList.find is_equal_to_e1 renaming in
id
with Not_found -> assert false in

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

@ -63,7 +63,7 @@ let add_array_to_prop pdesc prop_ lexp typ =
begin
try
let hpred = IList.find (function
| Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
| Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp
| _ -> false) (Prop.get_sigma prop) in
match hpred with
| Sil.Hpointsto(_, Sil.Earray (len, _, _), _) ->
@ -114,7 +114,7 @@ let execute___set_array_length { Builtin.pdesc; prop_; path; ret_ids; args; }
let n_lexp, prop__ = check_arith_norm_exp pname lexp prop_a in
let n_len, prop = check_arith_norm_exp pname len prop__ in
let hpred, sigma' = IList.partition (function
| Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
| Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp
| _ -> false) (Prop.get_sigma prop) in
(match hpred with
| [Sil.Hpointsto(e, Sil.Earray(_, esel, inst), t)] ->
@ -146,7 +146,7 @@ let create_type tenv n_lexp typ prop =
let prop_type =
try
let _ = IList.find (function
| Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
| Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp
| _ -> false) (Prop.get_sigma prop) in
prop
with Not_found ->
@ -200,7 +200,7 @@ let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; }
begin
try
let hpred = IList.find (function
| Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
| Sil.Hpointsto(e, _, _) -> Exp.equal e n_lexp
| _ -> false) (Prop.get_sigma prop) in
match hpred with
| Sil.Hpointsto(_, _, texp) ->
@ -216,7 +216,7 @@ let replace_ptsto_texp prop root_e texp =
let process_sigma sigma =
let sigma1, sigma2 =
IList.partition (function
| Sil.Hpointsto(e, _, _) -> Sil.exp_equal e root_e
| Sil.Hpointsto(e, _, _) -> Exp.equal e root_e
| _ -> false) sigma in
match sigma1 with
| [Sil.Hpointsto(e, se, _)] -> (Sil.Hpointsto (e, se, texp)) :: sigma2
@ -247,13 +247,13 @@ let execute___instanceof_cast ~instof
Tabulation.raise_cast_exception
__POS__ None texp1 texp2 val1 in
let exe_one_prop prop =
if Sil.exp_equal texp2 Sil.exp_zero then
if Exp.equal texp2 Sil.exp_zero then
[(return_result Sil.exp_zero prop ret_ids, path)]
else
begin
try
let hpred = IList.find (function
| Sil.Hpointsto (e1, _, _) -> Sil.exp_equal e1 val1
| Sil.Hpointsto (e1, _, _) -> Exp.equal e1 val1
| _ -> false) (Prop.get_sigma prop) in
match hpred with
| Sil.Hpointsto (_, _, texp1) ->
@ -263,7 +263,7 @@ let execute___instanceof_cast ~instof
| None -> []
| Some texp1' ->
let prop' =
if Sil.exp_equal texp1 texp1' then prop
if Exp.equal texp1 texp1' then prop
else replace_ptsto_texp prop val1 texp1' in
[(return_result res_e prop' ret_ids, path)] in
if instof then (* instanceof *)
@ -395,14 +395,14 @@ let execute___get_hidden_field { Builtin.pdesc; prop_; path; ret_ids; args; }
let has_fld_hidden fsel = IList.exists filter_fld_hidden fsel in
let do_hpred in_foot hpred = match hpred with
| Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp)
when Sil.exp_equal e n_lexp && (not (has_fld_hidden fsel)) ->
when Exp.equal e n_lexp && (not (has_fld_hidden fsel)) ->
let foot_e = Lazy.force foot_var in
ret_val := Some foot_e;
let se = Sil.Eexp(foot_e, Sil.inst_none) in
let fsel' = (Ident.fieldname_hidden, se) :: fsel in
Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp)
| Sil.Hpointsto(e, Sil.Estruct (fsel, _), _)
when Sil.exp_equal e n_lexp && not in_foot && has_fld_hidden fsel ->
when Exp.equal e n_lexp && not in_foot && has_fld_hidden fsel ->
let set_ret_val () =
match IList.find filter_fld_hidden fsel with
| _, Sil.Eexp(e, _) -> ret_val := Some e
@ -431,14 +431,14 @@ let execute___set_hidden_field { Builtin.pdesc; prop_; path; args; }
let has_fld_hidden fsel = IList.exists filter_fld_hidden fsel in
let do_hpred in_foot hpred = match hpred with
| Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp)
when Sil.exp_equal e n_lexp1 && not in_foot ->
when Exp.equal e n_lexp1 && not in_foot ->
let se = Sil.Eexp(n_lexp2, Sil.inst_none) in
let fsel' =
(Ident.fieldname_hidden, se) ::
(IList.filter (fun x -> not (filter_fld_hidden x)) fsel) in
Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp)
| Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp)
when Sil.exp_equal e n_lexp1 && in_foot && not (has_fld_hidden fsel) ->
when Exp.equal e n_lexp1 && in_foot && not (has_fld_hidden fsel) ->
let foot_e = Lazy.force foot_var in
let se = Sil.Eexp(foot_e, Sil.inst_none) in
let fsel' = (Ident.fieldname_hidden, se) :: fsel in
@ -562,7 +562,7 @@ let execute___release_autorelease_pool
| ((prop', path') :: _, Sil.Apred (_, exp :: _)) ->
(try
let hpred = IList.find (function
| Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 exp
| Sil.Hpointsto(e1, _, _) -> Exp.equal e1 exp
| _ -> false) (Prop.get_sigma prop_) in
match hpred with
| Sil.Hpointsto (_, _, Exp.Sizeof (typ, _, _)) ->
@ -661,7 +661,7 @@ let execute___objc_cast { Builtin.pdesc; prop_; path; ret_ids; args; }
let texp2, prop = check_arith_norm_exp pname texp2_ prop__ in
(try
let hpred = IList.find (function
| Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1
| Sil.Hpointsto(e1, _, _) -> Exp.equal e1 val1
| _ -> false) (Prop.get_sigma prop) in
match hpred, texp2 with
| Sil.Hpointsto (val1, _, _), Exp.Sizeof _ ->
@ -815,7 +815,7 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
let typ =
try
let hpred = IList.find (function
| Sil.Hpointsto (e, _, _) -> Sil.exp_equal e n_lexp
| Sil.Hpointsto (e, _, _) -> Exp.equal e n_lexp
| _ -> false) (Prop.get_sigma prop) in
match hpred with
| Sil.Hpointsto (_, _, Exp.Sizeof (dynamic_type, _, _)) -> dynamic_type

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

@ -259,7 +259,7 @@ let create_pvar_env (sigma: sigma) : (Exp.t -> Exp.t) =
IList.iter filter sigma;
let find e =
try
snd (IList.find (fun (e1, _) -> Sil.exp_equal e1 e) !env)
snd (IList.find (fun (e1, _) -> Exp.equal e1 e) !env)
with Not_found -> e in
find
@ -663,7 +663,7 @@ let sym_eval abs e =
let oplus = if isMinusA then Binop.PlusA else Binop.PlusPI in
let (+++) x y = Exp.BinOp (oplus, x, y) in
let (---) x y = Exp.BinOp (ominus, x, y) in
if Sil.exp_equal e1' e2' then Sil.exp_zero
if Exp.equal e1' e2' then Sil.exp_zero
else begin
match e1', e2' with
| Exp.Const c, _ when iszero_int_float c ->
@ -946,11 +946,11 @@ let inequality_normalize a =
| _ -> [e],[], IntLit.zero in
(* sort and filter out expressions appearing in both the positive and negative part *)
let normalize_posnegoff (pos, neg, off) =
let pos' = IList.sort Sil.exp_compare pos in
let neg' = IList.sort Sil.exp_compare neg in
let pos' = IList.sort Exp.compare pos in
let neg' = IList.sort Exp.compare neg in
let rec combine pacc nacc = function
| x:: ps, y:: ng ->
(match Sil.exp_compare x y with
(match Exp.compare x y with
| n when n < 0 -> combine (x:: pacc) nacc (ps, y :: ng)
| 0 -> combine pacc nacc (ps, ng)
| _ -> combine pacc (y:: nacc) (x :: ps, ng))
@ -983,7 +983,7 @@ let inequality_normalize a =
mk_inequality (norm_from_exp e)
| _ -> a
let exp_reorder e1 e2 = if Sil.exp_compare e1 e2 <= 0 then (e1, e2) else (e2, e1)
let exp_reorder e1 e2 = if Exp.compare e1 e2 <= 0 then (e1, e2) else (e2, e1)
(** Normalize an atom.
We keep the convention that inequalities with constants
@ -1007,8 +1007,8 @@ let atom_normalize sub a0 =
then normalize_eq (e1', e2')
else eq
| Exp.Lindex (e1', idx1), Exp.Lindex (e2', idx2) ->
if Sil.exp_equal idx1 idx2 then normalize_eq (e1', e2')
else if Sil.exp_equal e1' e2' then normalize_eq (idx1, idx2)
if Exp.equal idx1 idx2 then normalize_eq (e1', e2')
else if Exp.equal e1' e2' then normalize_eq (idx1, idx2)
else eq
| _ -> eq in
let handle_unary_negation e1 e2 =
@ -1071,7 +1071,7 @@ let rec strexp_normalize sub se =
let len' = exp_normalize_noabs sub len in
match idx_cnts with
| [] ->
if Sil.exp_equal len len' then se else Sil.Earray (len', idx_cnts, inst)
if Exp.equal len len' then se else Sil.Earray (len', idx_cnts, inst)
| _ ->
let idx_cnts' =
IList.map (fun (idx, cnt) ->
@ -1220,7 +1220,7 @@ let pi_tighten_ineq pi =
| _ -> acc in
IList.fold_left get_disequality_info [] nonineq_list in
let is_neq e n =
IList.exists (fun (e', n') -> Sil.exp_equal e e' && IntLit.eq n n') diseq_list in
IList.exists (fun (e', n') -> Exp.equal e e' && IntLit.eq n n') diseq_list in
let le_list_tightened =
let get_le_inequality_info acc a =
match atom_exp_le_const a with
@ -1262,10 +1262,10 @@ let pi_tighten_ineq pi =
| Sil.Aneq(Exp.Const (Const.Cint n), e)
| Sil.Aneq(e, Exp.Const (Const.Cint n)) ->
(not (IList.exists
(fun (e', n') -> Sil.exp_equal e e' && IntLit.lt n' n)
(fun (e', n') -> Exp.equal e e' && IntLit.lt n' n)
le_list_tightened)) &&
(not (IList.exists
(fun (n', e') -> Sil.exp_equal e e' && IntLit.leq n n')
(fun (n', e') -> Exp.equal e e' && IntLit.leq n n')
lt_list_tightened))
| _ -> true)
nonineq_list in
@ -1277,13 +1277,13 @@ let rec pi_sorted_remove_redundant = function
Exp.Const (Const.Cint i1)) as a1) ::
Sil.Aeq (Exp.BinOp (Binop.Le, e2, Exp.Const (Const.Cint n2)),
Exp.Const (Const.Cint i2)) :: rest
when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
when IntLit.isone i1 && IntLit.isone i2 && Exp.equal e1 e2 && IntLit.lt n1 n2 ->
(* second inequality redundant *)
pi_sorted_remove_redundant (a1 :: rest)
| Sil.Aeq (Exp.BinOp (Binop.Lt, Exp.Const (Const.Cint n1), e1), Exp.Const (Const.Cint i1)) ::
(Sil.Aeq (Exp.BinOp (Binop.Lt, Exp.Const (Const.Cint n2), e2), Exp.Const (Const.Cint i2)) as a2)
:: rest
when IntLit.isone i1 && IntLit.isone i2 && Sil.exp_equal e1 e2 && IntLit.lt n1 n2 ->
when IntLit.isone i1 && IntLit.isone i2 && Exp.equal e1 e2 && IntLit.lt n1 n2 ->
(* first inequality redundant *)
pi_sorted_remove_redundant (a2 :: rest)
| a1:: a2:: rest ->
@ -1310,15 +1310,15 @@ let pi_normalize sub sigma pi0 =
let ineq_list, nonineq_list = pi_tighten_ineq pi in
let syntactically_different = function
| Exp.BinOp(op1, e1, Exp.Const(c1)), Exp.BinOp(op2, e2, Exp.Const(c2))
when Sil.exp_equal e1 e2 ->
when Exp.equal e1 e2 ->
Binop.equal op1 op2 && Binop.injective op1 && not (Const.equal c1 c2)
| e1, Exp.BinOp(op2, e2, Exp.Const(c2))
when Sil.exp_equal e1 e2 ->
when Exp.equal e1 e2 ->
Binop.injective op2 &&
Binop.is_zero_runit op2 &&
not (Const.equal (Const.Cint IntLit.zero) c2)
| Exp.BinOp(op1, e1, Exp.Const(c1)), e2
when Sil.exp_equal e1 e2 ->
when Exp.equal e1 e2 ->
Binop.injective op1 &&
Binop.is_zero_runit op1 &&
not (Const.equal (Const.Cint IntLit.zero) c1)
@ -1327,7 +1327,7 @@ let pi_normalize sub sigma pi0 =
let unsigned_exps = lazy (sigma_get_unsigned_exps sigma) in
function
| Sil.Aneq ((Exp.Var _) as e, Exp.Const (Const.Cint n)) when IntLit.isnegative n ->
not (IList.exists (Sil.exp_equal e) (Lazy.force unsigned_exps))
not (IList.exists (Exp.equal e) (Lazy.force unsigned_exps))
| Sil.Aneq(e1, e2) ->
not (syntactically_different (e1, e2))
| Sil.Aeq(Exp.Const c1, Exp.Const c2) ->
@ -1574,7 +1574,7 @@ let compute_reachable_hpreds sigma exps =
[reachable_hpreds]. *)
let get_fld_typ_path_opt src_exps snk_exp_ reachable_hpreds_ =
let strexp_matches target_exp = function
| (_, Sil.Eexp (e, _)) -> Sil.exp_equal target_exp e
| (_, Sil.Eexp (e, _)) -> Exp.equal target_exp e
| _ -> false in
let extend_path hpred (snk_exp, path, reachable_hpreds) = match hpred with
| Sil.Hpointsto (lhs, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) ->
@ -1642,13 +1642,13 @@ let sigma_remove_emptylseg sigma =
| Sil.Hpointsto _ as hpred :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma'
| Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) :: sigma'
when (Sil.exp_equal e1 Sil.exp_zero) || (Sil.ExpSet.mem e1 alloc_set) ->
when (Exp.equal e1 Sil.exp_zero) || (Sil.ExpSet.mem e1 alloc_set) ->
f (Sil.Aeq(e1, e2) :: eqs_zero) sigma_passed sigma'
| Sil.Hlseg _ as hpred :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma'
| Sil.Hdllseg (Sil.Lseg_PE, _, iF, oB, oF, iB, _) :: sigma'
when (Sil.exp_equal iF Sil.exp_zero) || (Sil.ExpSet.mem iF alloc_set)
|| (Sil.exp_equal iB Sil.exp_zero) || (Sil.ExpSet.mem iB alloc_set) ->
when (Exp.equal iF Sil.exp_zero) || (Sil.ExpSet.mem iF alloc_set)
|| (Exp.equal iB Sil.exp_zero) || (Sil.ExpSet.mem iB alloc_set) ->
f (Sil.Aeq(iF, oF):: Sil.Aeq(iB, oB):: eqs_zero) sigma_passed sigma'
| Sil.Hdllseg _ as hpred :: sigma' ->
f eqs_zero (hpred :: sigma_passed) sigma'
@ -1662,16 +1662,16 @@ let sigma_intro_nonemptylseg e1 e2 sigma =
| Sil.Hpointsto _ as hpred :: sigma' ->
f (hpred :: sigma_passed) sigma'
| Sil.Hlseg (Sil.Lseg_PE, para, f1, f2, shared) :: sigma'
when (Sil.exp_equal e1 f1 && Sil.exp_equal e2 f2)
|| (Sil.exp_equal e2 f1 && Sil.exp_equal e1 f2) ->
when (Exp.equal e1 f1 && Exp.equal e2 f2)
|| (Exp.equal e2 f1 && Exp.equal e1 f2) ->
f (Sil.Hlseg (Sil.Lseg_NE, para, f1, f2, shared) :: sigma_passed) sigma'
| Sil.Hlseg _ as hpred :: sigma' ->
f (hpred :: sigma_passed) sigma'
| Sil.Hdllseg (Sil.Lseg_PE, para, iF, oB, oF, iB, shared) :: sigma'
when (Sil.exp_equal e1 iF && Sil.exp_equal e2 oF)
|| (Sil.exp_equal e2 iF && Sil.exp_equal e1 oF)
|| (Sil.exp_equal e1 iB && Sil.exp_equal e2 oB)
|| (Sil.exp_equal e2 iB && Sil.exp_equal e1 oB) ->
when (Exp.equal e1 iF && Exp.equal e2 oF)
|| (Exp.equal e2 iF && Exp.equal e1 oF)
|| (Exp.equal e1 iB && Exp.equal e2 oB)
|| (Exp.equal e2 iB && Exp.equal e1 oB) ->
f (Sil.Hdllseg (Sil.Lseg_NE, para, iF, oB, oF, iB, shared) :: sigma_passed) sigma'
| Sil.Hdllseg _ as hpred :: sigma' ->
f (hpred :: sigma_passed) sigma'
@ -1716,7 +1716,7 @@ let rec prop_atom_and ?(footprint=false) (p : normal t) a : normal t =
let (eqs_zero, nsigma'') = sigma_remove_emptylseg nsigma' in
let p' = { p with sub = nsub'; pi = npi'; sigma = nsigma''} in
IList.fold_left (prop_atom_and ~footprint) p' eqs_zero
| Sil.Aeq (e1, e2) when (Sil.exp_compare e1 e2 = 0) ->
| Sil.Aeq (e1, e2) when (Exp.compare e1 e2 = 0) ->
p
| Sil.Aneq (e1, e2) ->
let sigma' = sigma_intro_nonemptylseg e1 e2 p.sigma in
@ -1790,7 +1790,7 @@ let get_attributes prop exp =
let nexp = exp_normalize_prop prop exp in
let atom_get_attr attributes atom =
match atom with
| Sil.Apred (_, es) | Anpred (_, es) when IList.mem Sil.exp_equal nexp es -> atom :: attributes
| Sil.Apred (_, es) | Anpred (_, es) when IList.mem Exp.equal nexp es -> atom :: attributes
| _ -> attributes in
IList.fold_left atom_get_attr [] prop.pi
@ -1864,7 +1864,7 @@ let add_or_replace_attribute_check_changed check_attribute_change prop atom0 =
let natom = Sil.atom_replace_exp (IList.combine exps0 nexps) atom0 in
let atom_map = function
| Sil.Apred (att, exp :: _) | Anpred (att, exp :: _)
when Sil.exp_equal nexp exp && attributes_in_same_category att att0 ->
when Exp.equal nexp exp && attributes_in_same_category att att0 ->
check_attribute_change att att0;
natom
| atom ->
@ -2089,7 +2089,7 @@ end = struct
end
let sigma_get_start_lexps_sort sigma =
let exp_compare_neg e1 e2 = - (Sil.exp_compare e1 e2) in
let exp_compare_neg e1 e2 = - (Exp.compare e1 e2) in
let filter e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
let lexps = Sil.hpred_list_get_lexps filter sigma in
IList.sort exp_compare_neg lexps
@ -2114,14 +2114,14 @@ let sigma_dfs_sort sigma =
| hpred :: cur ->
begin
match hpred with
| Sil.Hpointsto (e', se, _) when Sil.exp_equal e e' ->
| Sil.Hpointsto (e', se, _) when Exp.equal e e' ->
handle_strexp se;
(hpred:: visited, IList.rev_append cur seen)
| Sil.Hlseg (_, _, root, next, shared) when Sil.exp_equal e root ->
| Sil.Hlseg (_, _, root, next, shared) when Exp.equal e root ->
IList.iter ExpStack.push (next:: shared);
(hpred:: visited, IList.rev_append cur seen)
| Sil.Hdllseg (_, _, iF, oB, oF, iB, shared)
when Sil.exp_equal e iF || Sil.exp_equal e iB ->
when Exp.equal e iF || Exp.equal e iB ->
IList.iter ExpStack.push (oB:: oF:: shared);
(hpred:: visited, IList.rev_append cur seen)
| _ ->
@ -2231,7 +2231,7 @@ let prop_rename_array_indices prop =
match e1, e2 with
| Exp.BinOp(Binop.PlusA, e1', Exp.Const (Const.Cint n1')),
Exp.BinOp(Binop.PlusA, e2', Exp.Const (Const.Cint n2')) ->
not (Sil.exp_equal e1' e2' && IntLit.lt n1' n2')
not (Exp.equal e1' e2' && IntLit.lt n1' n2')
| _ -> true in
let rec select_minimal_indices indices_seen = function
| [] -> IList.rev indices_seen
@ -2819,7 +2819,7 @@ let find_equal_formal_path e prop =
| None ->
match hpred with
| Sil.Hpointsto (Exp.Lvar pvar1, Sil.Eexp (exp2, Sil.Iformal(_, _) ), _)
when Sil.exp_equal exp2 e &&
when Exp.equal exp2 e &&
(Pvar.is_local pvar1 || Pvar.is_seed pvar1) ->
Some (Exp.Lvar pvar1)
| Sil.Hpointsto (exp1, Sil.Estruct (fields, _), _) ->
@ -2828,7 +2828,7 @@ let find_equal_formal_path e prop =
| Some _ -> res
| None ->
match strexp with
| Sil.Eexp (exp2, _) when Sil.exp_equal exp2 e ->
| Sil.Eexp (exp2, _) when Exp.equal exp2 e ->
(match find_in_sigma exp1 seen_hpreds with
| Some vfs -> Some (Exp.Lfield (vfs, field, Typ.Tvoid))
| None -> None)
@ -3027,7 +3027,7 @@ let rec pp_ren pe f = function
| (i, x):: ren -> F.fprintf f "%a->%a, %a" (Ident.pp pe) i (Ident.pp pe) x (pp_ren pe) ren
let id_exp_compare (id1, e1) (id2, e2) =
let n = Sil.exp_compare e1 e2 in
let n = Exp.compare e1 e2 in
if n <> 0 then n
else Ident.compare id1 id2

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

@ -34,7 +34,7 @@ let rec is_root = function
(** Return [true] if the nodes are connected. Used to compute reachability. *)
let nodes_connected n1 n2 =
Sil.exp_equal n1 n2 (* Implemented as equality for now, later it might contain offset by a constant *)
Exp.equal n1 n2 (* Implemented as equality for now, later it might contain offset by a constant *)
(** Return [true] if the edge is an hpred, and [false] if it is an atom *)
let edge_is_hpred = function
@ -77,7 +77,7 @@ let edge_from_source g n footprint_part is_hpred =
else IList.map (fun a -> Eatom a) (get_pi footprint_part g) @ IList.map (fun entry -> Esub_entry entry) (get_subl footprint_part g) in
let starts_from hpred =
match edge_get_source hpred with
| Some e -> Sil.exp_equal n e
| Some e -> Exp.equal n e
| None -> false in
match IList.filter starts_from edges with
| [] -> None
@ -100,7 +100,7 @@ let get_edges footprint_part g =
let edge_equal e1 e2 = match e1, e2 with
| Ehpred hp1, Ehpred hp2 -> Sil.hpred_equal hp1 hp2
| Eatom a1, Eatom a2 -> Sil.atom_equal a1 a2
| Esub_entry (x1, e1), Esub_entry (x2, e2) -> Ident.equal x1 x2 && Sil.exp_equal e1 e2
| Esub_entry (x1, e1), Esub_entry (x2, e2) -> Ident.equal x1 x2 && Exp.equal e1 e2
| _ -> false
(** [contains_edge footprint_part g e] returns true if the graph [g] contains edge [e],
@ -124,12 +124,12 @@ type diff =
(** Compute the subobjects in [e2] which are different from those in [e1] *)
let compute_exp_diff (e1: Exp.t) (e2: Exp.t) : Obj.t list =
if Sil.exp_equal e1 e2 then [] else [Obj.repr e2]
if Exp.equal e1 e2 then [] else [Obj.repr e2]
(** Compute the subobjects in [se2] which are different from those in [se1] *)
let rec compute_sexp_diff (se1: Sil.strexp) (se2: Sil.strexp) : Obj.t list = match se1, se2 with
| Sil.Eexp (e1, _), Sil.Eexp (e2, _) -> if Sil.exp_equal e1 e2 then [] else [Obj.repr se2]
| Sil.Eexp (e1, _), Sil.Eexp (e2, _) -> if Exp.equal e1 e2 then [] else [Obj.repr se2]
| Sil.Estruct (fsel1, _), Sil.Estruct (fsel2, _) ->
compute_fsel_diff fsel1 fsel2
| Sil.Earray (e1, esel1, _), Sil.Earray (e2, esel2, _) ->
@ -148,7 +148,7 @@ and compute_fsel_diff fsel1 fsel2 : Obj.t list = match fsel1, fsel2 with
and compute_esel_diff esel1 esel2 : Obj.t list = match esel1, esel2 with
| ((e1, se1):: esel1'), (((e2, se2) as x):: esel2') ->
(match Sil.exp_compare e1 e2 with
(match Exp.compare e1 e2 with
| n when n < 0 -> compute_esel_diff esel1' esel2
| 0 -> compute_sexp_diff se1 se2 @ compute_esel_diff esel1' esel2'
| _ -> (Obj.repr x) :: compute_esel_diff esel1 esel2')

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

@ -26,8 +26,8 @@ let compute_min_from_nonempty_int_list l =
IList.hd (IList.sort IntLit.compare_value l)
let exp_pair_compare (e1, e2) (f1, f2) =
let c1 = Sil.exp_compare e1 f1 in
if c1 <> 0 then c1 else Sil.exp_compare e2 f2
let c1 = Exp.compare e1 f1 in
if c1 <> 0 then c1 else Exp.compare e2 f2
let rec list_rev_acc acc = function
| [] -> acc
@ -102,8 +102,8 @@ end = struct
let rec generate ((e1, e2, n) as constr) acc = function
| [] -> false, acc
| (f1, f2, m):: rest ->
let equal_e2_f1 = Sil.exp_equal e2 f1 in
let equal_e1_f2 = Sil.exp_equal e1 f2 in
let equal_e2_f1 = Exp.equal e2 f1 in
let equal_e1_f2 = Exp.equal e1 f2 in
if equal_e2_f1 && equal_e1_f2 && IntLit.lt (n ++ m) IntLit.zero then
true, [] (* constraints are inconsistent *)
else if equal_e2_f1 && equal_e1_f2 then
@ -256,18 +256,18 @@ end = struct
let inconsistent_ineq = { leqs = [(Sil.exp_one, Sil.exp_zero)]; lts = []; neqs = [] }
let leq_compare (e1, e2) (f1, f2) =
let c1 = Sil.exp_compare e1 f1 in
if c1 <> 0 then c1 else Sil.exp_compare e2 f2
let c1 = Exp.compare e1 f1 in
if c1 <> 0 then c1 else Exp.compare e2 f2
let lt_compare (e1, e2) (f1, f2) =
let c2 = Sil.exp_compare e2 f2 in
if c2 <> 0 then c2 else - (Sil.exp_compare e1 f1)
let c2 = Exp.compare e2 f2 in
if c2 <> 0 then c2 else - (Exp.compare e1 f1)
let leqs_sort_then_remove_redundancy leqs =
let leqs_sorted = IList.sort leq_compare leqs in
let have_same_key leq1 leq2 =
match leq1, leq2 with
| (e1, Exp.Const (Const.Cint n1)), (e2, Exp.Const (Const.Cint n2)) ->
Sil.exp_equal e1 e2 && IntLit.leq n1 n2
Exp.equal e1 e2 && IntLit.leq n1 n2
| _, _ -> false in
remove_redundancy have_same_key [] leqs_sorted
let lts_sort_then_remove_redundancy lts =
@ -275,7 +275,7 @@ end = struct
let have_same_key lt1 lt2 =
match lt1, lt2 with
| (Exp.Const (Const.Cint n1), e1), (Exp.Const (Const.Cint n2), e2) ->
Sil.exp_equal e1 e2 && IntLit.geq n1 n2
Exp.equal e1 e2 && IntLit.geq n1 n2
| _, _ -> false in
remove_redundancy have_same_key [] lts_sorted
@ -411,7 +411,7 @@ end = struct
(** Return true if the two pairs of expressions are equal *)
let exp_pair_eq (e1, e2) (f1, f2) =
Sil.exp_equal e1 f1 && Sil.exp_equal e2 f2
Exp.equal e1 f1 && Exp.equal e2 f2
(** Check [t |- e1<=e2]. Result [false] means "don't know". *)
let check_le { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
@ -425,13 +425,13 @@ end = struct
check_type_size_lt t1 t2
| e, Exp.Const (Const.Cint n) -> (* [e <= n' <= n |- e <= n] *)
IList.exists (function
| e', Exp.Const (Const.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' n
| e', Exp.Const (Const.Cint n') -> Exp.equal e e' && IntLit.leq n' n
| _, _ -> false) leqs
| Exp.Const (Const.Cint n), e -> (* [ n-1 <= n' < e |- n <= e] *)
IList.exists (function
| Exp.Const (Const.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq (n -- IntLit.one) n'
| Exp.Const (Const.Cint n'), e' -> Exp.equal e e' && IntLit.leq (n -- IntLit.one) n'
| _, _ -> false) lts
| _ -> Sil.exp_equal e1 e2
| _ -> Exp.equal e1 e2
(** Check [prop |- e1<e2]. Result [false] means "don't know". *)
let check_lt { leqs = leqs; lts = lts; neqs = _ } e1 e2 =
@ -440,17 +440,17 @@ end = struct
| Exp.Const (Const.Cint n1), Exp.Const (Const.Cint n2) -> IntLit.lt n1 n2
| Exp.Const (Const.Cint n), e -> (* [n <= n' < e |- n < e] *)
IList.exists (function
| Exp.Const (Const.Cint n'), e' -> Sil.exp_equal e e' && IntLit.leq n n'
| Exp.Const (Const.Cint n'), e' -> Exp.equal e e' && IntLit.leq n n'
| _, _ -> false) lts
| e, Exp.Const (Const.Cint n) -> (* [e <= n' <= n-1 |- e < n] *)
IList.exists (function
| e', Exp.Const (Const.Cint n') -> Sil.exp_equal e e' && IntLit.leq n' (n -- IntLit.one)
| e', Exp.Const (Const.Cint n') -> Exp.equal e e' && IntLit.leq n' (n -- IntLit.one)
| _, _ -> false) leqs
| _ -> false
(** Check [prop |- e1!=e2]. Result [false] means "don't know". *)
let check_ne ineq _e1 _e2 =
let e1, e2 = if Sil.exp_compare _e1 _e2 <= 0 then _e1, _e2 else _e2, _e1 in
let e1, e2 = if Exp.compare _e1 _e2 <= 0 then _e1, _e2 else _e2, _e1 in
IList.exists (exp_pair_eq (e1, e2)) ineq.neqs || check_lt ineq e1 e2 || check_lt ineq e2 e1
(** Find a IntLit.t n such that [t |- e<=n] if possible. *)
@ -460,7 +460,7 @@ end = struct
| _ ->
let e_upper_list =
IList.filter (function
| e', Exp.Const (Const.Cint _) -> Sil.exp_equal e1 e'
| e', Exp.Const (Const.Cint _) -> Exp.equal e1 e'
| _, _ -> false) leqs in
let upper_list =
IList.map (function
@ -477,7 +477,7 @@ end = struct
| _ ->
let e_lower_list =
IList.filter (function
| Exp.Const (Const.Cint _), e' -> Sil.exp_equal e1 e'
| Exp.Const (Const.Cint _), e' -> Exp.equal e1 e'
| _, _ -> false) lts in
let lower_list =
IList.map (function
@ -524,12 +524,12 @@ let check_equal prop e1 e2 =
let n_e1 = Prop.exp_normalize_prop prop e1 in
let n_e2 = Prop.exp_normalize_prop prop e2 in
let check_equal () =
Sil.exp_equal n_e1 n_e2 in
Exp.equal n_e1 n_e2 in
let check_equal_const () =
match n_e1, n_e2 with
| Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2
| e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) ->
if Sil.exp_equal e1 e2 then IntLit.iszero d
if Exp.equal e1 e2 then IntLit.iszero d
else false
| Exp.Const c1, Exp.Lindex(Exp.Const c2, Exp.Const (Const.Cint i)) when IntLit.iszero i ->
Const.equal c1 c2
@ -597,11 +597,11 @@ let check_disequal prop e1 e2 =
else Const.equal c1 c2 (* same base, different offsets *)
| Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d1)),
Exp.BinOp (Binop.PlusA, e2, Exp.Const (Const.Cint d2)) ->
if Sil.exp_equal e1 e2 then IntLit.neq d1 d2
if Exp.equal e1 e2 then IntLit.neq d1 d2
else false
| Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)), e2
| e2, Exp.BinOp (Binop.PlusA, e1, Exp.Const (Const.Cint d)) ->
if Sil.exp_equal e1 e2 then not (IntLit.iszero d)
if Exp.equal e1 e2 then not (IntLit.iszero d)
else false
| Exp.Lindex(Exp.Const c1, Exp.Const (Const.Cint d)), Exp.Const c2 ->
if IntLit.iszero d then not (Const.equal c1 c2) else Const.equal c1 c2
@ -631,7 +631,7 @@ let check_disequal prop e1 e2 =
if (k == Sil.Lseg_NE || check_pi_implies_disequal e1 e2) then
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (true, sigma_irrelevant')
else if (Sil.exp_equal e2 Sil.exp_zero) then
else if (Exp.equal e2 Sil.exp_zero) then
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (false, sigma_irrelevant')
else
@ -653,14 +653,14 @@ let check_disequal prop e1 e2 =
if (check_pi_implies_disequal iF oF) then
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (true, sigma_irrelevant')
else if (Sil.exp_equal oF Sil.exp_zero) then
else if (Exp.equal oF Sil.exp_zero) then
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (false, sigma_irrelevant')
else
let sigma_rest' = (IList.rev sigma_irrelevant) @ sigma_rest
in f [] oF sigma_rest') in
let f_null_check sigma_irrelevant e sigma_rest =
if not (Sil.exp_equal e Sil.exp_zero) then f sigma_irrelevant e sigma_rest
if not (Exp.equal e Sil.exp_zero) then f sigma_irrelevant e sigma_rest
else
let sigma_irrelevant' = (IList.rev sigma_irrelevant) @ sigma_rest
in Some (false, sigma_irrelevant')
@ -679,7 +679,7 @@ let check_le_normalized prop e1 e2 =
(* L.d_str "check_le_normalized "; Sil.d_exp e1; L.d_str " "; Sil.d_exp e2; L.d_ln (); *)
let eL, eR, off = match e1, e2 with
| Exp.BinOp(Binop.MinusA, f1, f2), Exp.Const (Const.Cint n) ->
if Sil.exp_equal f1 f2
if Exp.equal f1 f2
then Sil.exp_zero, Sil.exp_zero, n
else f1, f2, n
| _ ->
@ -777,17 +777,17 @@ let check_inconsistency_two_hpreds prop =
| [] -> false
| (Sil.Hpointsto (e1, _, _) as hpred) :: sigma_rest
| (Sil.Hlseg (Sil.Lseg_NE, _, e1, _, _) as hpred) :: sigma_rest ->
if Sil.exp_equal e1 e then true
if Exp.equal e1 e then true
else f e (hpred:: sigma_seen) sigma_rest
| (Sil.Hdllseg (Sil.Lseg_NE, _, iF, _, _, iB, _) as hpred) :: sigma_rest ->
if Sil.exp_equal iF e || Sil.exp_equal iB e then true
if Exp.equal iF e || Exp.equal iB e then true
else f e (hpred:: sigma_seen) sigma_rest
| Sil.Hlseg (Sil.Lseg_PE, _, e1, Exp.Const (Const.Cint i), _) as hpred :: sigma_rest
when IntLit.iszero i ->
if Sil.exp_equal e1 e then true
if Exp.equal e1 e then true
else f e (hpred:: sigma_seen) sigma_rest
| Sil.Hlseg (Sil.Lseg_PE, _, e1, e2, _) as hpred :: sigma_rest ->
if Sil.exp_equal e1 e
if Exp.equal e1 e
then
let prop' = Prop.normalize (Prop.from_sigma (sigma_seen@sigma_rest)) in
let prop_new = Prop.conjoin_eq e1 e2 prop' in
@ -797,10 +797,10 @@ let check_inconsistency_two_hpreds prop =
else f e (hpred:: sigma_seen) sigma_rest
| Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, Exp.Const (Const.Cint i), _, _) as hpred :: sigma_rest
when IntLit.iszero i ->
if Sil.exp_equal e1 e then true
if Exp.equal e1 e then true
else f e (hpred:: sigma_seen) sigma_rest
| Sil.Hdllseg (Sil.Lseg_PE, _, e1, _, e3, _, _) as hpred :: sigma_rest ->
if Sil.exp_equal e1 e
if Exp.equal e1 e
then
let prop' = Prop.normalize (Prop.from_sigma (sigma_seen@sigma_rest)) in
let prop_new = Prop.conjoin_eq e1 e3 prop' in
@ -845,7 +845,7 @@ let check_inconsistency_base prop =
procedure_attr.ProcAttributes.is_cpp_instance_method in
let do_hpred = function
| Sil.Hpointsto (Exp.Lvar pv, Sil.Eexp (e, _), _) ->
Sil.exp_equal e Sil.exp_zero &&
Exp.equal e Sil.exp_zero &&
Pvar.is_seed pv &&
(is_java_this pv || is_cpp_this pv || is_objc_instance_self pv)
| _ -> false in
@ -858,7 +858,7 @@ let check_inconsistency_base prop =
| Sil.Aneq (e1, e2) ->
(match e1, e2 with
| Exp.Const c1, Exp.Const c2 -> Const.equal c1 c2
| _ -> (Sil.exp_compare e1 e2 = 0))
| _ -> (Exp.compare e1 e2 = 0))
| Sil.Apred _ | Anpred _ -> false in
let inconsistent_inequalities () =
let ineq = Inequalities.from_prop prop in
@ -1344,7 +1344,7 @@ and array_imply source calc_index_frame calc_missing subs esel1 esel2 typ2
| (e1, se1) :: esel1', (e2, se2) :: esel2' ->
let e1n = Prop.exp_normalize_noabs (fst subs) e1 in
let e2n = Prop.exp_normalize_noabs (snd subs) e2 in
let n = Sil.exp_compare e1n e2n in
let n = Exp.compare e1n e2n in
if n < 0 then array_imply source calc_index_frame calc_missing subs esel1' esel2 typ2
else if n > 0 then array_imply source calc_index_frame calc_missing subs esel1 esel2' typ2
else (* n=0 *)
@ -1391,10 +1391,11 @@ let rec exp_list_imply calc_missing subs l1 l2 = match l1, l2 with
| _ -> assert false
let filter_ne_lhs sub e0 = function
| Sil.Hpointsto (e, _, _) -> if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None
| Sil.Hlseg (Sil.Lseg_NE, _, e, _, _) -> if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None
| Sil.Hpointsto (e, _, _) -> if Exp.equal e0 (Sil.exp_sub sub e) then Some () else None
| Sil.Hlseg (Sil.Lseg_NE, _, e, _, _) ->
if Exp.equal e0 (Sil.exp_sub sub e) then Some () else None
| Sil.Hdllseg (Sil.Lseg_NE, _, e, _, _, e', _) ->
if Sil.exp_equal e0 (Sil.exp_sub sub e) || Sil.exp_equal e0 (Sil.exp_sub sub e')
if Exp.equal e0 (Sil.exp_sub sub e) || Exp.equal e0 (Sil.exp_sub sub e')
then Some ()
else None
| _ -> None
@ -1405,7 +1406,7 @@ let filter_hpred sub hpred2 hpred1 = match (Sil.hpred_sub sub hpred1), hpred2 wi
| Sil.Hlseg(Sil.Lseg_PE, hpara1, e1, f1, el1), Sil.Hlseg(Sil.Lseg_NE, _, _, _, _) ->
if Sil.hpred_equal (Sil.Hlseg(Sil.Lseg_NE, hpara1, e1, f1, el1)) hpred2 then Some true else None (* return missing disequality *)
| Sil.Hpointsto(e1, _, _), Sil.Hlseg(_, _, e2, _, _) ->
if Sil.exp_equal e1 e2 then Some false else None
if Exp.equal e1 e2 then Some false else None
| hpred1, hpred2 -> if Sil.hpred_equal hpred1 hpred2 then Some false else None
let hpred_has_primed_lhs sub hpred =
@ -1661,9 +1662,9 @@ let get_overrides_of tenv supertype pname =
let texp_equal_modulo_subtype_flag texp1 texp2 = match texp1, texp2 with
| Exp.Sizeof (t1, len1, st1), Exp.Sizeof (t2, len2, st2) ->
Typ.equal t1 t2
&& (opt_equal Sil.exp_equal len1 len2)
&& (opt_equal Exp.equal len1 len2)
&& Subtype.equal_modulo_flag st1 st2
| _ -> Sil.exp_equal texp1 texp2
| _ -> Exp.equal texp1 texp2
(** check implication between type expressions *)
let texp_imply tenv subs texp1 texp2 e1 calc_missing =
@ -1725,13 +1726,13 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2
| _ -> false in
let is_allocated_lhs e =
let filter = function
| Sil.Hpointsto(e', _, _) -> Sil.exp_equal e' e
| Sil.Hpointsto(e', _, _) -> Exp.equal e' e
| _ -> false in
IList.exists filter (Prop.get_sigma prop1) in
let type_rhs e =
let sub_opt = ref None in
let filter = function
| Sil.Hpointsto(e', _, Exp.Sizeof(t, len, sub)) when Sil.exp_equal e' e ->
| Sil.Hpointsto(e', _, Exp.Sizeof(t, len, sub)) when Exp.equal e' e ->
sub_opt := Some (t, len, sub);
true
| _ -> false in
@ -1820,7 +1821,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
L.d_decrease_indent 1;
res
| Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Sil.exp_equal (Sil.exp_sub (fst subs) iF1) e2 -> (* Unroll dllseg forward *)
when Exp.equal (Sil.exp_sub (fst subs) iF1) e2 -> (* Unroll dllseg forward *)
let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
let (_, para_inst1) = Sil.hpara_dll_instantiate para1 iF1 oB1 n' elist1 in
let hpred_list1 = para_inst1@[Prop.mk_dllseg Sil.Lseg_PE para1 n' iF1 oF1 iB1 elist1] in
@ -1832,8 +1833,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
L.d_decrease_indent 1;
res
| Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Sil.exp_equal (Sil.exp_sub (fst subs) iB1) e2 ->
(* Unroll dllseg backward *)
when Exp.equal (Sil.exp_sub (fst subs) iB1) e2 -> (* Unroll dllseg backward *)
let n' = Exp.Var (Ident.create_fresh Ident.kprimed) in
let (_, para_inst1) = Sil.hpara_dll_instantiate para1 iB1 n' oF1 elist1 in
let hpred_list1 = para_inst1@[Prop.mk_dllseg Sil.Lseg_PE para1 iF1 oB1 iB1 n' elist1] in
@ -1857,7 +1857,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
raise (Exceptions.Abduction_case_not_implemented __POS__))
| _ -> ()
in
if Sil.exp_equal e2 f2 && k == Sil.Lseg_PE then (subs, prop1)
if Exp.equal e2 f2 && k == Sil.Lseg_PE then (subs, prop1)
else
(match Prop.prop_iter_create prop1 with
| None -> raise (IMPL_EXC ("lhs is empty", subs, EXC_FALSE))
@ -1932,7 +1932,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
| None ->
let elist2 = IList.map (fun e -> Sil.exp_sub (snd subs) e) elist2 in
let _, para_inst2 =
if Sil.exp_equal iF2 iB2 then
if Exp.equal iF2 iB2 then
Sil.hpara_dll_instantiate para2 iF2 oB2 oF2 elist2
else assert false (* Only base case of rhs list considered for now *) in
L.d_increase_indent 1;
@ -2094,7 +2094,7 @@ let rec pre_check_pure_implication calc_missing subs pi1 pi2 =
| [] -> subs
| (Sil.Aeq (e2_in, f2_in) as a) :: pi2' when not (Prop.atom_is_inequality a) ->
let e2, f2 = Sil.exp_sub (snd subs) e2_in, Sil.exp_sub (snd subs) f2_in in
if Sil.exp_equal e2 f2 then pre_check_pure_implication calc_missing subs pi1 pi2'
if Exp.equal e2 f2 then pre_check_pure_implication calc_missing subs pi1 pi2'
else
(match e2, f2 with
| Exp.Var v2, f2
@ -2275,6 +2275,6 @@ let check_lt prop e1 e2 =
check_atom prop (Prop.mk_inequality e1_lt_e2)
let filter_ptsto_lhs sub e0 = function
| Sil.Hpointsto (e, _, _) -> if Sil.exp_equal e0 (Sil.exp_sub sub e) then Some () else None
| Sil.Hpointsto (e, _, _) -> if Exp.equal e0 (Sil.exp_sub sub e) then Some () else None
| _ -> None
*)

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

@ -265,12 +265,12 @@ let rec _strexp_extend_values
bounds_check pname orig_prop len e (State.get_loc ());
begin
try
let _, se' = IList.find (fun (e', _) -> Sil.exp_equal e e') esel in
let _, se' = IList.find (fun (e', _) -> Exp.equal e e') esel in
let atoms_se_typ_list' =
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se' typ' off' inst in
let replace acc (res_atoms', res_se', res_typ') =
let replace_ise ise = if Sil.exp_equal e (fst ise) then (e, res_se') else ise in
let replace_ise ise = if Exp.equal e (fst ise) then (e, res_se') else ise in
let res_esel' = IList.map replace_ise esel in
if (Typ.equal res_typ' typ') || (IList.length res_esel' = 1) then
( res_atoms'
@ -544,10 +544,10 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
let footprint_sigma = Prop.prop_iter_get_footprint_sigma iter in
let sigma_pto, sigma_rest =
IList.partition (function
| Sil.Hpointsto(e', _, _) -> Sil.exp_equal e e'
| Sil.Hlseg (_, _, e1, _, _) -> Sil.exp_equal e e1
| Sil.Hpointsto(e', _, _) -> Exp.equal e e'
| Sil.Hlseg (_, _, e1, _, _) -> Exp.equal e e1
| Sil.Hdllseg (_, _, e_iF, _, _, e_iB, _) ->
Sil.exp_equal e e_iF || Sil.exp_equal e e_iB
Exp.equal e e_iF || Exp.equal e e_iB
) footprint_sigma in
let atoms_sigma_list =
match sigma_pto with
@ -756,12 +756,12 @@ let add_guarded_by_constraints prop lexp pdesc =
IList.exists
(function
| Sil.Hpointsto (Lvar _, Eexp (rhs_exp, _), _) ->
Sil.exp_equal exp rhs_exp
Exp.equal exp rhs_exp
| Sil.Hpointsto (_, Estruct (flds, _), _) ->
IList.exists
(fun (fld, strexp) -> match strexp with
| Sil.Eexp (rhs_exp, _) ->
Sil.exp_equal exp rhs_exp && not (Ident.fieldname_equal fld accessed_fld)
Exp.equal exp rhs_exp && not (Ident.fieldname_equal fld accessed_fld)
| _ ->
false)
flds
@ -811,7 +811,7 @@ let add_guarded_by_constraints prop lexp pdesc =
| Some guarded_by_fld_str -> enforce_guarded_access_ fld guarded_by_fld_str prop
| None -> prop in
let check_fld_locks typ prop_acc (fld, strexp) = match strexp with
| Sil.Eexp (exp, _) when Sil.exp_equal exp lexp -> enforce_guarded_access fld typ prop_acc
| Sil.Eexp (exp, _) when Exp.equal exp lexp -> enforce_guarded_access fld typ prop_acc
| _ -> prop_acc in
let hpred_check_flds prop_acc = function
| Sil.Hpointsto (_, Estruct (flds, _), Sizeof (typ, _, _)) ->
@ -1188,7 +1188,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
(fun hpred ->
match hpred with
| Sil.Hpointsto (Exp.Lvar pvar, Sil.Eexp (Exp.Var _ as exp, _), _)
when Sil.exp_equal exp deref_exp ->
when Exp.equal exp deref_exp ->
let is_weak_captured_var = is_weak_captured_var pdesc pvar in
let is_nullable =
if Annotations.param_is_nullable pvar ann_sig || is_weak_captured_var
@ -1215,7 +1215,7 @@ let check_dereference_error pdesc (prop : Prop.normal Prop.t) lexp loc =
| _ -> false in
let is_strexp_pt_by_nullable_fld (fld, strexp) =
match strexp with
| Sil.Eexp (Exp.Var _ as exp, _) when Sil.exp_equal exp deref_exp ->
| Sil.Eexp (Exp.Var _ as exp, _) when Exp.equal exp deref_exp ->
let is_nullable = fld_is_nullable fld in
if is_nullable then
nullable_obj_str := Some (Ident.fieldname_to_simplified_string fld);

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

@ -184,7 +184,7 @@ let rec apply_offlist
pdesc tenv p fp_root nullify_struct
(root_lexp, se', t') offlist' f inst lookup_inst in
let replace_ese ese =
if Sil.exp_equal idx_ese' (fst ese)
if Exp.equal idx_ese' (fst ese)
then (idx_ese', res_se')
else ese in
let res_se = Sil.Earray (len, IList.map replace_ese esel, inst1) in
@ -288,7 +288,7 @@ let prune_ne ~positive e1 e2 prop =
is "<" if [is_strict] is true and "<=" if [is_strict] is false.
*)
let prune_ineq ~is_strict ~positive prop e1 e2 =
if Sil.exp_equal e1 e2 then
if Exp.equal e1 e2 then
if (positive && not is_strict) || (not positive && is_strict) then
Propset.singleton prop
else Propset.empty
@ -439,7 +439,7 @@ let check_arith_norm_exp pname exp prop =
let check_already_dereferenced pname cond prop =
let find_hpred lhs =
try Some (IList.find (function
| Sil.Hpointsto (e, _, _) -> Sil.exp_equal e lhs
| Sil.Hpointsto (e, _, _) -> Exp.equal e lhs
| _ -> false) (Prop.get_sigma prop))
with Not_found -> None in
let rec is_check_zero = function
@ -530,7 +530,7 @@ let resolve_typename prop receiver_exp =
let typexp_opt =
let rec loop = function
| [] -> None
| Sil.Hpointsto(e, _, typexp) :: _ when Sil.exp_equal e receiver_exp -> Some typexp
| Sil.Hpointsto(e, _, typexp) :: _ when Exp.equal e receiver_exp -> Some typexp
| _ :: hpreds -> loop hpreds in
loop (Prop.get_sigma prop) in
match typexp_opt with
@ -730,7 +730,7 @@ let handle_objc_instance_method_call_or_skip actual_pars path callee_pname pre r
let is_receiver_null =
match actual_pars with
| (e, _) :: _
when Sil.exp_equal e Sil.exp_zero ||
when Exp.equal e Sil.exp_zero ||
Option.is_some (Prop.get_objc_null_attribute pre e) -> true
| _ -> false in
let add_objc_null_attribute_or_nullify_result prop =
@ -1285,7 +1285,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
let sigma' =
IList.map
(function
| Sil.Hpointsto (lhs, _, _) when Sil.exp_equal lhs actual_var -> new_hpred
| Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual_var -> new_hpred
| hpred -> hpred)
(Prop.get_sigma prop) in
Prop.normalize (Prop.replace_sigma sigma' prop) in
@ -1324,7 +1324,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
let filtered_sigma =
IList.map
(function
| Sil.Hpointsto (lhs, _, typ_exp) when Sil.exp_equal lhs actual ->
| Sil.Hpointsto (lhs, _, typ_exp) when Exp.equal lhs actual ->
Sil.Hpointsto (lhs, abduced_strexp, typ_exp)
| hpred -> hpred)
(Prop.get_sigma prop') in
@ -1335,7 +1335,7 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
let filtered_sigma =
IList.filter
(function
| Sil.Hpointsto (lhs, _, _) when Sil.exp_equal lhs actual ->
| Sil.Hpointsto (lhs, _, _) when Exp.equal lhs actual ->
false
| _ -> true)
(Prop.get_sigma prop) in

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

@ -298,7 +298,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
L.d_strln (" desc: " ^ (pp_to_string Localise.pp_error_desc error_desc));
error_desc in
let deref_no_null_check_pos =
if Sil.exp_equal e_sub Sil.exp_zero then
if Exp.equal e_sub Sil.exp_zero then
match find_dereference_without_null_check_in_sexp sexp with
| Some (_, pos) -> Some pos
| None -> None
@ -315,7 +315,7 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params =
(* In that case it raise a dangling pointer dereferece *)
if Prop.has_dangling_uninit_attribute spec_pre e then
Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some Sil.DAuninit)) )
else if Sil.exp_equal e_sub Sil.exp_minus_one
else if Exp.equal e_sub Sil.exp_minus_one
then Some (Deref_minusone, desc true (Localise.deref_str_dangling None))
else match Prop.get_resource_attribute actual_pre e_sub with
| Some (Apred (Aresource ({ ra_kind = Rrelease } as ra), _)) ->
@ -401,7 +401,7 @@ let post_process_post
post', post_path
let hpred_lhs_compare hpred1 hpred2 = match hpred1, hpred2 with
| Sil.Hpointsto(e1, _, _), Sil.Hpointsto(e2, _, _) -> Sil.exp_compare e1 e2
| Sil.Hpointsto(e1, _, _), Sil.Hpointsto(e2, _, _) -> Exp.compare e1 e2
| Sil.Hpointsto _, _ -> - 1
| _, Sil.Hpointsto _ -> 1
| hpred1, hpred2 -> Sil.hpred_compare hpred1 hpred2
@ -433,7 +433,7 @@ and esel_star_fld esel1 esel2 = match esel1, esel2 with
IList.map (fun (e, se) -> (e, sexp_set_inst Sil.Inone se)) esel2
| esel1,[] -> esel1
| (e1, se1):: esel1', (e2, se2):: esel2' ->
(match Sil.exp_compare e1 e2 with
(match Exp.compare e1 e2 with
| 0 -> (e1, array_content_star se1 se2) :: esel_star_fld esel1' esel2'
| n when n < 0 -> (e1, se1) :: esel_star_fld esel1' esel2
| _ ->
@ -510,7 +510,7 @@ let sigma_star_fld (sigma1 : Sil.hpred list) (sigma2 : Sil.hpred list) : Sil.hpr
raise (Prop.Cannot_star __POS__)
let hpred_typing_lhs_compare hpred1 (e2, _) = match hpred1 with
| Sil.Hpointsto(e1, _, _) -> Sil.exp_compare e1 e2
| Sil.Hpointsto(e1, _, _) -> Exp.compare e1 e2
| _ -> - 1
let hpred_star_typing (hpred1 : Sil.hpred) (_, te2) : Sil.hpred =
@ -521,7 +521,7 @@ let hpred_star_typing (hpred1 : Sil.hpred) (_, te2) : Sil.hpred =
(** Implementation of [*] between predicates and typings *)
let sigma_star_typ
(sigma1 : Sil.hpred list) (typings2 : (Exp.t * Exp.t) list) : Sil.hpred list =
let typing_lhs_compare (e1, _) (e2, _) = Sil.exp_compare e1 e2 in
let typing_lhs_compare (e1, _) (e2, _) = Exp.compare e1 e2 in
let sigma1 = IList.stable_sort hpred_lhs_compare sigma1 in
let typings2 = IList.stable_sort typing_lhs_compare typings2 in
let rec star sg1 typ2 : Sil.hpred list =
@ -618,7 +618,7 @@ let exp_is_exn = function
let prop_is_exn pname prop =
let ret_pvar = Exp.Lvar (Pvar.get_ret_pvar pname) in
let is_exn = function
| Sil.Hpointsto (e1, Sil.Eexp(e2, _), _) when Sil.exp_equal e1 ret_pvar ->
| Sil.Hpointsto (e1, Sil.Eexp(e2, _), _) when Exp.equal e1 ret_pvar ->
exp_is_exn e2
| _ -> false in
IList.exists is_exn (Prop.get_sigma prop)
@ -629,13 +629,13 @@ let prop_get_exn_name pname prop =
let rec search_exn e = function
| [] -> None
| Sil.Hpointsto (e1, _, Exp.Sizeof (Typ.Tstruct { Typ.struct_name = Some name }, _, _)) :: _
when Sil.exp_equal e1 e ->
when Exp.equal e1 e ->
Some (Typename.TN_csu (Csu.Class Csu.Java, name))
| _ :: tl -> search_exn e tl in
let rec find_exn_name hpreds = function
| [] -> None
| Sil.Hpointsto (e1, Sil.Eexp (Exp.Exn e2, _), _) :: _
when Sil.exp_equal e1 ret_pvar ->
when Exp.equal e1 ret_pvar ->
search_exn e2 hpreds
| _ :: tl -> find_exn_name hpreds tl in
let hpreds = Prop.get_sigma prop in
@ -655,7 +655,7 @@ let lookup_custom_errors prop =
let prop_set_exn pname prop se_exn =
let ret_pvar = Exp.Lvar (Pvar.get_ret_pvar pname) in
let map_hpred = function
| Sil.Hpointsto (e, _, t) when Sil.exp_equal e ret_pvar ->
| Sil.Hpointsto (e, _, t) when Exp.equal e ret_pvar ->
Sil.Hpointsto(e, se_exn, t)
| hpred -> hpred in
let sigma' = IList.map map_hpred (Prop.get_sigma prop) in
@ -744,7 +744,7 @@ let combine
| None -> post_p2
| Some iter ->
let filter = function
| Sil.Hpointsto (e, _, _) when Sil.exp_equal e callee_ret_pvar -> Some ()
| Sil.Hpointsto (e, _, _) when Exp.equal e callee_ret_pvar -> Some ()
| _ -> None in
match Prop.prop_iter_find iter filter with
| None -> post_p2
@ -1321,7 +1321,7 @@ let check_splitting_precondition sub1 sub2 =
let sigma_has_null_pointer sigma =
let hpred_null_pointer = function
| Sil.Hpointsto (e, _, _) ->
Sil.exp_equal e Sil.exp_zero
Exp.equal e Sil.exp_zero
| _ -> false in
IList.exists hpred_null_pointer sigma
*)

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

@ -294,10 +294,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let prunes_tracking_var astate = function
| Exp.BinOp (Binop.Eq, lhs, rhs)
when is_tracking_exp astate lhs ->
Sil.exp_equal rhs Sil.exp_one
Exp.equal rhs Sil.exp_one
| Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, lhs, rhs), _)
when is_tracking_exp astate lhs ->
Sil.exp_equal rhs Sil.exp_zero
Exp.equal rhs Sil.exp_zero
| _ ->
false

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

@ -448,7 +448,7 @@ let callback_find_deserialization { Callbacks.proc_desc; get_proc_desc; idenv; p
when Ident.equal i1 i2 -> true
| _ -> false in
let is_set_instr = function
| Sil.Set (e1, _, _, _) when Sil.exp_equal expanded e1 -> true
| Sil.Set (e1, _, _, _) when Exp.equal expanded e1 -> true
| _ -> false in
match reverse_find_instr is_set_instr node with
(* Look for ivar := tmp *)

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

@ -76,7 +76,7 @@ module Match = struct
| Vfun pn -> F.fprintf fmt "%s" (Procname.to_string pn)
let value_equal v1 v2 = match v1, v2 with
| Vval e1, Vval e2 -> Sil.exp_equal e1 e2
| Vval e1, Vval e2 -> Exp.equal e1 e2
| Vval _, _ -> false
| _, Vval _ -> false
| Vfun pn1, Vfun pn2 -> Procname.equal pn1 pn2
@ -98,7 +98,7 @@ module Match = struct
Hashtbl.iter pp_item env
let exp_match env ae value = match ae, value with
| CodeQueryAst.Null, Vval e -> Sil.exp_equal e Sil.exp_zero
| CodeQueryAst.Null, Vval e -> Exp.equal e Sil.exp_zero
| CodeQueryAst.Null, _ -> false
| CodeQueryAst.ConstString s, (Vfun pn) -> string_contains s (Procname.to_string pn)
| CodeQueryAst.ConstString _, _ -> false

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

@ -318,7 +318,7 @@ let java_get_vararg_values node pvar idenv =
let values = ref [] in
let do_instr = function
| Sil.Set (Exp.Lindex (array_exp, _), _, content_exp, _)
when Sil.exp_equal (Exp.Lvar pvar) (Idenv.expand_expr idenv array_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
| _ -> () in

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

@ -27,7 +27,7 @@ struct
let compare i1 i2 = match i1, i2 with
| Sil.Call (_, e1, etl1, _, cf1), Sil.Call (_, e2, etl2, _, cf2) ->
(* ignore return ids and call flags *)
let n = Sil.exp_compare e1 e2 in
let n = Exp.compare e1 e2 in
if n <> 0 then n else let n = IList.compare Sil.exp_typ_compare etl1 etl2 in
if n <> 0 then n else CallFlags.compare cf1 cf2
| _ -> Sil.instr_compare i1 i2

2
infer/src/clang/cFrontend_utils.ml
Unescape View File

@ -533,7 +533,7 @@ struct
append_no_duplicates eq list1 list2
let append_no_duplicateds list1 list2 =
let eq (e1, t1) (e2, t2) = (Sil.exp_equal e1 e2) && (Typ.equal t1 t2) in
let eq (e1, t1) (e2, t2) = (Exp.equal e1 e2) && (Typ.equal t1 t2) in
append_no_duplicates eq list1 list2

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

@ -766,7 +766,7 @@ struct
let (sil_e2, _) = extract_exp_from_list res_trans_e2.exps
"\nWARNING: Missing RHS operand in BinOp. Returning -1. Fix needed...\n" in
let binop_res_trans, exp_to_parent =
if IList.exists (Sil.exp_equal var_exp) res_trans_e2.initd_exps then [], []
if IList.exists (Exp.equal var_exp) res_trans_e2.initd_exps then [], []
else
let exp_op, instr_bin =
CArithmetic_trans.binary_operation_instruction
@ -1653,7 +1653,7 @@ struct
let rhs_owning_method = CTrans_utils.is_owning_method ie in
let _, instrs_assign =
(* variable might be initialized already - do nothing in that case*)
if IList.exists (Sil.exp_equal var_exp) res_trans_ie.initd_exps then ([], [])
if IList.exists (Exp.equal var_exp) res_trans_ie.initd_exps then ([], [])
else if !Config.arc_mode &&
(CTrans_utils.is_method_call ie ||
ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv ie_typ)
@ -1873,7 +1873,7 @@ struct
let (sil_expr, _) = extract_exp_from_list res_trans_stmt.exps
"WARNING: There should be only one return expression.\n" in
let ret_instrs = if IList.exists (Sil.exp_equal ret_exp) res_trans_stmt.initd_exps
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
let autorelease_instrs =

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

@ -1037,7 +1037,7 @@ let typecheck_instr
let found = ref None in
let do_instr i = match i with
| Sil.Set (e, _, e', _)
when Sil.exp_equal (Exp.Lvar pvar) (Idenv.expand_expr idenv e') ->
when Exp.equal (Exp.Lvar pvar) (Idenv.expand_expr idenv e') ->
found := Some e
| _ -> () in
IList.iter do_instr (Cfg.Node.get_instrs prev_node);
@ -1055,7 +1055,7 @@ let typecheck_instr
node'', Exp.BinOp (bop, c1', c2')
| Exp.Var _ ->
let c' = Idenv.expand_expr idenv _cond in
if not (Sil.exp_equal c' _cond) then normalize_cond _node c'
if not (Exp.equal c' _cond) then normalize_cond _node c'
else _node, c'
| Exp.Lvar pvar when Pvar.is_frontend_tmp pvar ->
(match handle_assignment_in_condition pvar with

2
infer/src/eradicate/typeState.ml
Unescape View File

@ -35,7 +35,7 @@ type 'a ext =
module M = Map.Make (struct
type t = Exp.t
let compare = Sil.exp_compare end)
let compare = Exp.compare end)
type range = Typ.t * TypeAnnotation.t * (Location.t list)

Write Preview
Loading…
Cancel
Save