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

ppx_compare Sil

Browse Source 
Reviewed By: cristianoc

Differential Revision: D4232394

fbshipit-source-id: 3296d74
master
Josh Berdine 8 years ago committed by Facebook Github Bot
parent 6298d043e6
commit aa5998a9d1
17 changed files with 254 additions and 688 deletions
Show Stats Download Patch File Download Diff File

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

@ -279,7 +279,7 @@ let mark_unchanged_pdescs cfg_new cfg_old => {
IList.equal
(
fun i1 i2 => {
let (n, exp_map') = Sil.instr_compare_structural i1 i2 !exp_map;
let (n, exp_map') = Sil.compare_structural_instr i1 i2 !exp_map;
exp_map := exp_map';
n
}

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

@ -29,7 +29,8 @@ type if_kind =
| Ik_if
| Ik_land_lor /* obtained from translation of && or || */
| Ik_while
| Ik_switch;
| Ik_switch
[@@deriving compare];
/** An instruction. */
@ -57,7 +58,8 @@ type instr =
| Nullify Pvar.t Location.t
| Abstract Location.t /** apply abstraction */
| Remove_temps (list Ident.t) Location.t /** remove temporaries */
| Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */;
| Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */
[@@deriving compare];
let skip_instr = Remove_temps [] Location.dummy;
@ -88,21 +90,27 @@ type atom =
| Aeq Exp.t Exp.t /** equality */
| Aneq Exp.t Exp.t /** disequality */
| Apred PredSymb.t (list Exp.t) /** predicate symbol applied to exps */
| Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */;
| Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */
[@@deriving compare];
let equal_atom x y => compare_atom x y == 0;
/** kind of lseg or dllseg predicates */
type lseg_kind =
| Lseg_NE /** nonempty (possibly circular) listseg */
| Lseg_PE /** possibly empty (possibly circular) listseg */;
| Lseg_PE /** possibly empty (possibly circular) listseg */
[@@deriving compare];
let equal_lseg_kind k1 k2 => compare_lseg_kind k1 k2 == 0;
/** The boolean is true when the pointer was dereferenced without testing for zero. */
type zero_flag = option bool;
type zero_flag = option bool [@@deriving compare];
/** True when the value was obtained by doing case analysis on null in a procedure call. */
type null_case_flag = bool;
type null_case_flag = bool [@@deriving compare];
/** instrumentation of heap values */
@ -118,13 +126,19 @@ type inst =
| Irearrange zero_flag null_case_flag int PredSymb.path_pos
| Itaint
| Iupdate zero_flag null_case_flag int PredSymb.path_pos
| Ireturn_from_call int;
| Ireturn_from_call int
[@@deriving compare];
/* some occurrences of inst are always ignored by compare */
type _inst = inst;
let compare__inst _ _ => 0;
/** structured expressions represent a value of structured type, such as an array or a struct. */
type strexp =
| Eexp Exp.t inst /** Base case: expression with instrumentation */
| Estruct (list (Ident.fieldname, strexp)) inst /** C structure */
type strexp0 'inst =
| Eexp Exp.t 'inst /** Base case: expression with instrumentation */
| Estruct (list (Ident.fieldname, strexp0 _inst)) 'inst /** C structure */
/** Array of given length
There are two conditions imposed / used in the array case.
First, if some index and value pair appears inside an array
@ -132,45 +146,102 @@ type strexp =
For instance, x |->[10 | e1: v1] implies that e1 <= 9.
Second, if two indices appear in an array, they should be different.
For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. */
| Earray Exp.t (list (Exp.t, strexp)) inst;
| Earray Exp.t (list (Exp.t, strexp0 _inst)) 'inst
[@@deriving compare];
type strexp = strexp0 inst;
let compare_strexp inst::inst=false se1 se2 =>
compare_strexp0 (inst ? compare_inst : compare__inst) se1 se2;
let equal_strexp inst::inst=false se1 se2 => compare_strexp inst::inst se1 se2 == 0;
/** an atomic heap predicate */
type hpred =
| Hpointsto Exp.t strexp Exp.t
type hpred0 'inst =
| Hpointsto Exp.t (strexp0 'inst) Exp.t
/** represents [exp|->strexp:typexp] where [typexp]
is an expression representing a type, e.h. [sizeof(t)]. */
| Hlseg lseg_kind hpara Exp.t Exp.t (list Exp.t)
| Hlseg lseg_kind (hpara0 'inst) Exp.t Exp.t (list Exp.t)
/** higher - order predicate for singly - linked lists.
Should ensure that exp1!= exp2 implies that exp1 is allocated.
This assumption is used in the rearrangement. The last [exp list] parameter
is used to denote the shared links by all the nodes in the list. */
| Hdllseg lseg_kind hpara_dll Exp.t Exp.t Exp.t Exp.t (list Exp.t)
/** higher-order predicate for doubly-linked lists. */
/** parameter for the higher-order singly-linked list predicate.
Means "lambda (root,next,svars). Exists evars. body".
Assume that root, next, svars, evars are disjoint sets of
primed identifiers, and include all the free primed identifiers in body.
body should not contain any non - primed identifiers or program
variables (i.e. pvars). */
and hpara = {
| Hdllseg lseg_kind (hpara_dll0 'inst) Exp.t Exp.t Exp.t Exp.t (list Exp.t)
/** higher-order predicate for doubly-linked lists.
Parameter for the higher-order singly-linked list predicate.
Means "lambda (root,next,svars). Exists evars. body".
Assume that root, next, svars, evars are disjoint sets of
primed identifiers, and include all the free primed identifiers in body.
body should not contain any non - primed identifiers or program
variables (i.e. pvars). */
[@@deriving compare]
and hpara0 'inst = {
root: Ident.t,
next: Ident.t,
svars: list Ident.t,
evars: list Ident.t,
body: list hpred
body: list (hpred0 'inst)
}
[@@deriving compare]
/** parameter for the higher-order doubly-linked list predicates.
Assume that all the free identifiers in body_dll should belong to
cell, blink, flink, svars_dll, evars_dll. */
and hpara_dll = {
and hpara_dll0 'inst = {
cell: Ident.t, /** address cell */
blink: Ident.t, /** backward link */
flink: Ident.t, /** forward link */
svars_dll: list Ident.t,
evars_dll: list Ident.t,
body_dll: list hpred
};
body_dll: list (hpred0 'inst)
}
[@@deriving compare];
type hpred = hpred0 inst;
/** Comparsion between heap predicates. Reverse natural order, and order first by anchor exp. */
let compare_hpred inst::inst=false hpred1 hpred2 =>
if (hpred1 === hpred2) {
0
} else {
switch (hpred1, hpred2) {
| (
Hpointsto e1 _ _ | Hlseg _ _ e1 _ _ | Hdllseg _ _ e1 _ _ _ _,
Hpointsto e2 _ _ | Hlseg _ _ e2 _ _ | Hdllseg _ _ e2 _ _ _ _
)
when Exp.compare e2 e1 != 0 =>
Exp.compare e2 e1
| (Hpointsto _, Hpointsto _)
| (Hlseg _, Hlseg _)
| (Hdllseg _, Hdllseg _) =>
if inst {
compare_hpred0 compare_inst hpred2 hpred1
} else {
compare_hpred0 (fun _ _ => 0) hpred2 hpred1
}
| _ =>
if inst {
compare_hpred0 compare_inst hpred1 hpred2
} else {
compare_hpred0 (fun _ _ => 0) hpred1 hpred2
}
}
};
let equal_hpred inst::inst=false hpred1 hpred2 => compare_hpred inst::inst hpred1 hpred2 == 0;
type hpara = hpara0 inst;
let compare_hpara = compare_hpara0 (fun _ _ => 0);
let equal_hpara hpara1 hpara2 => compare_hpara hpara1 hpara2 == 0;
type hpara_dll = hpara_dll0 inst;
let compare_hpara_dll = compare_hpara_dll0 (fun _ _ => 0);
let equal_hpara_dll hpara1 hpara2 => compare_hpara_dll hpara1 hpara2 == 0;
/** Return the lhs expression of a hpred */
@ -222,343 +293,6 @@ let is_static_local_name pname pvar => {
}
};
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;
/** Compare atoms. Equalities come before disequalities */
let atom_compare a b =>
if (a === b) {
0
} else {
switch (a, b) {
| (Aeq e1 e2, Aeq f1 f2) =>
let n = Exp.compare e1 f1;
if (n != 0) {
n
} else {
Exp.compare e2 f2
}
| (Aeq _, _) => (-1)
| (_, Aeq _) => 1
| (Aneq e1 e2, Aneq f1 f2) =>
let n = Exp.compare e1 f1;
if (n != 0) {
n
} else {
Exp.compare e2 f2
}
| (Aneq _, _) => (-1)
| (_, Aneq _) => 1
| (Apred a1 es1, Apred a2 es2) =>
let n = PredSymb.compare a1 a2;
if (n != 0) {
n
} else {
IList.compare Exp.compare es1 es2
}
| (Apred _, _) => (-1)
| (_, Apred _) => 1
| (Anpred a1 es1, Anpred a2 es2) =>
let n = PredSymb.compare a1 a2;
if (n != 0) {
n
} else {
IList.compare Exp.compare es1 es2
}
}
};
let atom_equal x y => atom_compare x y == 0;
let lseg_kind_compare k1 k2 =>
switch (k1, k2) {
| (Lseg_NE, Lseg_NE) => 0
| (Lseg_NE, Lseg_PE) => (-1)
| (Lseg_PE, Lseg_NE) => 1
| (Lseg_PE, Lseg_PE) => 0
};
let lseg_kind_equal k1 k2 => lseg_kind_compare k1 k2 == 0;
let zero_flag_compare = opt_compare bool_compare;
let inst_compare_base inst1 inst2 =>
switch (inst1, inst2) {
| (Iabstraction, Iabstraction) => 0
| (Iabstraction, _) => (-1)
| (_, Iabstraction) => 1
| (Iactual_precondition, Iactual_precondition) => 0
| (Iactual_precondition, _) => (-1)
| (_, Iactual_precondition) => 1
| (Ialloc, Ialloc) => 0
| (Ialloc, _) => (-1)
| (_, Ialloc) => 1
| (Iformal zero_flag1 null_case_flag1, Iformal zero_flag2 null_case_flag2) =>
let n = zero_flag_compare zero_flag1 zero_flag2;
if (n != 0) {
n
} else {
bool_compare null_case_flag1 null_case_flag2
}
| (Iformal _, _) => (-1)
| (_, Iformal _) => 1
| (Iinitial, Iinitial) => 0
| (Iinitial, _) => (-1)
| (_, Iinitial) => 1
| (Ilookup, Ilookup) => 0
| (Ilookup, _) => (-1)
| (_, Ilookup) => 1
| (Inone, Inone) => 0
| (Inone, _) => (-1)
| (_, Inone) => 1
| (Inullify, Inullify) => 0
| (Inullify, _) => (-1)
| (_, Inullify) => 1
| (
Irearrange zero_flag1 null_case_flag1 i1 path_pos1,
Irearrange zero_flag2 null_case_flag2 i2 path_pos2
) =>
let n = zero_flag_compare zero_flag1 zero_flag2;
if (n != 0) {
n
} else {
let n = bool_compare null_case_flag1 null_case_flag2;
if (n != 0) {
n
} else {
let n = int_compare i1 i2;
if (n != 0) {
n
} else {
PredSymb.compare_path_pos path_pos1 path_pos2
}
}
}
| (Irearrange _, _) => (-1)
| (_, Irearrange _) => 1
| (Itaint, Itaint) => 0
| (Itaint, _) => (-1)
| (_, Itaint) => 1
| (
Iupdate zero_flag1 null_case_flag1 i1 path_pos1,
Iupdate zero_flag2 null_case_flag2 i2 path_pos2
) =>
let n = zero_flag_compare zero_flag1 zero_flag2;
if (n != 0) {
n
} else {
let n = bool_compare null_case_flag1 null_case_flag2;
if (n != 0) {
n
} else {
let n = int_compare i1 i2;
if (n != 0) {
n
} else {
PredSymb.compare_path_pos path_pos1 path_pos2
}
}
}
| (Iupdate _, _) => (-1)
| (_, Iupdate _) => 1
| (Ireturn_from_call i1, Ireturn_from_call i2) => int_compare i1 i2
};
let inst_compare inst::inst inst1 inst2 => inst ? inst_compare_base inst1 inst2 : 0;
/* Comparison for strexps */
let rec strexp_compare inst::inst=false se1 se2 =>
if (se1 === se2) {
0
} else {
switch (se1, se2) {
| (Eexp e1 i1, Eexp e2 i2) =>
let n = Exp.compare e1 e2;
if (n != 0) {
n
} else {
inst_compare inst::inst i1 i2
}
| (Eexp _, _) => (-1)
| (_, Eexp _) => 1
| (Estruct fel1 i1, Estruct fel2 i2) =>
let n = fld_strexp_list_compare fel1 fel2;
if (n != 0) {
n
} else {
inst_compare inst::inst i1 i2
}
| (Estruct _, _) => (-1)
| (_, Estruct _) => 1
| (Earray e1 esel1 i1, Earray e2 esel2 i2) =>
let n = Exp.compare e1 e2;
if (n != 0) {
n
} else {
let n = exp_strexp_list_compare esel1 esel2;
if (n != 0) {
n
} else {
inst_compare inst::inst i1 i2
}
}
}
}
and fld_strexp_compare fse1 fse2 => pair_compare Ident.compare_fieldname 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_list_compare esel1 esel2 => IList.compare exp_strexp_compare esel1 esel2;
/** Comparsion between heap predicates. Hpointsto comes before others. */
let rec hpred_compare inst::inst=false hpred1 hpred2 =>
if (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 se1 te1, Hpointsto e2 se2 te2) =>
let n = Exp.compare e2 e1;
if (n != 0) {
n
} else {
let n = strexp_compare inst::inst se2 se1;
if (n != 0) {
n
} else {
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;
if (n != 0) {
n
} else {
let n = lseg_kind_compare k2 k1;
if (n != 0) {
n
} else {
let n = hpara_compare hpar2 hpar1;
if (n != 0) {
n
} else {
let n = Exp.compare f2 f1;
if (n != 0) {
n
} else {
exp_list_compare el2 el1
}
}
}
}
| (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;
if (n != 0) {
n
} else {
let n = lseg_kind_compare k2 k1;
if (n != 0) {
n
} else {
let n = hpara_dll_compare hpar2 hpar1;
if (n != 0) {
n
} else {
let n = Exp.compare f2 f1;
if (n != 0) {
n
} else {
let n = Exp.compare g2 g1;
if (n != 0) {
n
} else {
let n = Exp.compare h2 h1;
if (n != 0) {
n
} else {
exp_list_compare el2 el1
}
}
}
}
}
}
}
}
and hpred_list_compare l1 l2 => IList.compare hpred_compare l1 l2
and hpara_compare hp1 hp2 => {
let n = Ident.compare hp1.root hp2.root;
if (n != 0) {
n
} else {
let n = Ident.compare hp1.next hp2.next;
if (n != 0) {
n
} else {
let n = IList.compare Ident.compare hp1.svars hp2.svars;
if (n != 0) {
n
} else {
let n = IList.compare Ident.compare hp1.evars hp2.evars;
if (n != 0) {
n
} else {
hpred_list_compare hp1.body hp2.body
}
}
}
}
}
and hpara_dll_compare hp1 hp2 => {
let n = Ident.compare hp1.cell hp2.cell;
if (n != 0) {
n
} else {
let n = Ident.compare hp1.blink hp2.blink;
if (n != 0) {
n
} else {
let n = Ident.compare hp1.flink hp2.flink;
if (n != 0) {
n
} else {
let n = IList.compare Ident.compare hp1.svars_dll hp2.svars_dll;
if (n != 0) {
n
} else {
let n = IList.compare Ident.compare hp1.evars_dll hp2.evars_dll;
if (n != 0) {
n
} else {
hpred_list_compare hp1.body_dll hp2.body_dll
}
}
}
}
}
};
let strexp_equal inst::inst=false se1 se2 => strexp_compare inst::inst se1 se2 == 0;
let hpred_equal inst::inst=false hpred1 hpred2 => hpred_compare inst::inst hpred1 hpred2 == 0;
let hpara_equal hpara1 hpara2 => hpara_compare hpara1 hpara2 == 0;
let hpara_dll_equal hpara1 hpara2 => hpara_dll_compare hpara1 hpara2 == 0;
/** {2 Sets of expressions} */
let elist_to_eset es => IList.fold_left (fun set e => Exp.Set.add e set) Exp.Set.empty es;
@ -567,7 +301,7 @@ let elist_to_eset es => IList.fold_left (fun set e => Exp.Set.add e set) Exp.Set
/** {2 Sets of heap predicates} */
let module HpredSet = Set.Make {
type t = hpred;
let compare = hpred_compare inst::false;
let compare = compare_hpred inst::false;
};
@ -891,14 +625,14 @@ let module Predicates: {
/** hash tables for hpara */
let module HparaHash = Hashtbl.Make {
type t = hpara;
let equal = hpara_equal;
let equal = equal_hpara;
let hash = Hashtbl.hash;
};
/** hash tables for hpara_dll */
let module HparaDllHash = Hashtbl.Make {
type t = hpara_dll;
let equal = hpara_dll_equal;
let equal = equal_hpara_dll;
let hash = Hashtbl.hash;
};
@ -1915,36 +1649,15 @@ let rec sorted_list_check_consecutives f =>
/** substitution */
type subst = list (Ident.t, Exp.t);
type ident_exp = (Ident.t, Exp.t) [@@deriving compare];
let equal_ident_exp ide1 ide2 => compare_ident_exp ide1 ide2 == 0;
/** Comparison between substitutions. */
let rec sub_compare (sub1: subst) (sub2: subst) =>
if (sub1 === sub2) {
0
} else {
switch (sub1, sub2) {
| ([], []) => 0
| ([], [_, ..._]) => (-1)
| ([(i1, e1), ...sub1'], [(i2, e2), ...sub2']) =>
let n = Ident.compare i1 i2;
if (n != 0) {
n
} else {
let n = Exp.compare e1 e2;
if (n != 0) {
n
} else {
sub_compare sub1' sub2'
}
}
| ([_, ..._], []) => 1
}
};
type subst = list ident_exp [@@deriving compare];
/** Equality for substitutions. */
let sub_equal sub1 sub2 => sub_compare sub1 sub2 == 0;
let equal_subst sub1 sub2 => compare_subst sub1 sub2 == 0;
let sub_check_duplicated_ids sub => {
let f (id1, _) (id2, _) => Ident.equal id1 id2;
@ -1956,8 +1669,8 @@ let sub_check_duplicated_ids sub => {
For all (id1, e1), (id2, e2) in the input list,
if id1 = id2, then e1 = e2. */
let sub_of_list sub => {
let sub' = IList.sort ident_exp_compare sub;
let sub'' = remove_duplicates_from_sorted ident_exp_equal sub';
let sub' = IList.sort compare_ident_exp sub;
let sub'' = remove_duplicates_from_sorted equal_ident_exp sub';
if (sub_check_duplicated_ids sub'') {
assert false
};
@ -1967,7 +1680,7 @@ let sub_of_list sub => {
/** like sub_of_list, but allow duplicate ids and only keep the first occurrence */
let sub_of_list_duplicates sub => {
let sub' = IList.sort ident_exp_compare sub;
let sub' = IList.sort compare_ident_exp sub;
let rec remove_duplicate_ids =
fun
| [(id1, e1), (id2, e2), ...l] =>
@ -1992,8 +1705,8 @@ let sub_empty = sub_of_list [];
/** Join two substitutions into one.
For all id in dom(sub1) cap dom(sub2), sub1(id) = sub2(id). */
let sub_join sub1 sub2 => {
let sub = sorted_list_merge ident_exp_compare sub1 sub2;
let sub' = remove_duplicates_from_sorted ident_exp_equal sub;
let sub = sorted_list_merge compare_ident_exp sub1 sub2;
let sub' = remove_duplicates_from_sorted equal_ident_exp sub;
if (sub_check_duplicated_ids sub') {
assert false
};
@ -2015,7 +1728,7 @@ let sub_symmetric_difference sub1_in sub2_in => {
let sub_common = reverse_with_base [] sub_common;
(sub_common, sub1_only', sub2_only')
| ([id_e1, ...sub1'], [id_e2, ...sub2']) =>
let n = ident_exp_compare id_e1 id_e2;
let n = compare_ident_exp id_e1 id_e2;
if (n == 0) {
diff [id_e1, ...sub_common] sub1_only sub2_only sub1' sub2'
} else if (n < 0) {
@ -2280,145 +1993,6 @@ let instr_sub_ids sub_id_binders::sub_id_binders (f: Ident.t => Exp.t) instr =>
/** apply [subst] to all id's in [instr], including binder id's */
let instr_sub (subst: subst) instr => instr_sub_ids sub_id_binders::true (apply_sub subst) instr;
let id_typ_compare (id1, typ1) (id2, typ2) => {
let n = Ident.compare id1 id2;
if (n != 0) {
n
} else {
Typ.compare typ1 typ2
}
};
let exp_typ_compare (exp1, typ1) (exp2, typ2) => {
let n = Exp.compare exp1 exp2;
if (n != 0) {
n
} else {
Typ.compare typ1 typ2
}
};
let instr_compare instr1 instr2 =>
switch (instr1, instr2) {
| (Load id1 e1 t1 loc1, Load id2 e2 t2 loc2) =>
let n = Ident.compare id1 id2;
if (n != 0) {
n
} else {
let n = Exp.compare e1 e2;
if (n != 0) {
n
} else {
let n = Typ.compare t1 t2;
if (n != 0) {
n
} else {
Location.compare loc1 loc2
}
}
}
| (Load _, _) => (-1)
| (_, Load _) => 1
| (Store e11 t1 e21 loc1, Store e12 t2 e22 loc2) =>
let n = Exp.compare e11 e12;
if (n != 0) {
n
} else {
let n = Typ.compare t1 t2;
if (n != 0) {
n
} else {
let n = Exp.compare e21 e22;
if (n != 0) {
n
} else {
Location.compare loc1 loc2
}
}
}
| (Store _, _) => (-1)
| (_, Store _) => 1
| (Prune cond1 loc1 true_branch1 ik1, Prune cond2 loc2 true_branch2 ik2) =>
let n = Exp.compare cond1 cond2;
if (n != 0) {
n
} else {
let n = Location.compare loc1 loc2;
if (n != 0) {
n
} else {
let n = bool_compare true_branch1 true_branch2;
if (n != 0) {
n
} else {
Pervasives.compare ik1 ik2
}
}
}
| (Prune _, _) => (-1)
| (_, Prune _) => 1
| (Call ret_id1 e1 arg_ts1 loc1 cf1, Call ret_id2 e2 arg_ts2 loc2 cf2) =>
let n = opt_compare id_typ_compare ret_id1 ret_id2;
if (n != 0) {
n
} else {
let n = Exp.compare e1 e2;
if (n != 0) {
n
} else {
let n = IList.compare exp_typ_compare arg_ts1 arg_ts2;
if (n != 0) {
n
} else {
let n = Location.compare loc1 loc2;
if (n != 0) {
n
} else {
CallFlags.compare cf1 cf2
}
}
}
}
| (Call _, _) => (-1)
| (_, Call _) => 1
| (Nullify pvar1 loc1, Nullify pvar2 loc2) =>
let n = Pvar.compare pvar1 pvar2;
if (n != 0) {
n
} else {
Location.compare loc1 loc2
}
| (Nullify _, _) => (-1)
| (_, Nullify _) => 1
| (Abstract loc1, Abstract loc2) => Location.compare loc1 loc2
| (Abstract _, _) => (-1)
| (_, Abstract _) => 1
| (Remove_temps temps1 loc1, Remove_temps temps2 loc2) =>
let n = IList.compare Ident.compare temps1 temps2;
if (n != 0) {
n
} else {
Location.compare loc1 loc2
}
| (Remove_temps _, _) => (-1)
| (_, Remove_temps _) => 1
| (Declare_locals ptl1 loc1, Declare_locals ptl2 loc2) =>
let pt_compare (pv1, t1) (pv2, t2) => {
let n = Pvar.compare pv1 pv2;
if (n != 0) {
n
} else {
Typ.compare t1 t2
}
};
let n = IList.compare pt_compare ptl1 ptl2;
if (n != 0) {
n
} else {
Location.compare loc1 loc2
}
};
/** compare expressions from different procedures without considering loc's, ident's, and pvar's.
the [exp_map] param gives a mapping of names used in the procedure of [e1] to names used in the
@ -2515,7 +2089,7 @@ let exp_typ_compare_structural (e1, t1) (e2, t2) exp_map => {
/** compare instructions from different procedures without considering loc's, ident's, and pvar's.
the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
used in the procedure of [instr2] */
let instr_compare_structural instr1 instr2 exp_map => {
let compare_structural_instr instr1 instr2 exp_map => {
let id_typ_opt_compare_structural id_typ1 id_typ2 exp_map => {
let id_typ_compare_structural (id1, typ1) (id2, typ2) => {
let (n, exp_map) = exp_compare_structural (Var id1) (Var id2) exp_map;
@ -2660,7 +2234,7 @@ let instr_compare_structural instr1 instr2 exp_map => {
ptl1
ptl2
}
| _ => (instr_compare instr1 instr2, exp_map)
| _ => (compare_instr instr1 instr2, exp_map)
}
};
@ -2726,7 +2300,7 @@ let hpred_replace_exp epairs =>
/** {2 Compaction} */
let module HpredInstHash = Hashtbl.Make {
type t = hpred;
let equal = hpred_equal inst::true;
let equal = equal_hpred inst::true;
let hash = Hashtbl.hash;
};

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

@ -31,7 +31,8 @@ type if_kind =
| Ik_if
| Ik_land_lor /* obtained from translation of && or || */
| Ik_while
| Ik_switch;
| Ik_switch
[@@deriving compare];
/** An instruction. */
@ -59,7 +60,14 @@ type instr =
| Nullify Pvar.t Location.t
| Abstract Location.t /** apply abstraction */
| Remove_temps (list Ident.t) Location.t /** remove temporaries */
| Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */;
| Declare_locals (list (Pvar.t, Typ.t)) Location.t /** declare local variables */
[@@deriving compare];
/** compare instructions from different procedures without considering loc's, ident's, and pvar's.
the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
used in the procedure of [instr2] */
let compare_structural_instr: instr => instr => Exp.Map.t Exp.t => (int, Exp.Map.t Exp.t);
let skip_instr: instr;
@ -81,13 +89,19 @@ type atom =
| Aeq Exp.t Exp.t /** equality */
| Aneq Exp.t Exp.t /** disequality */
| Apred PredSymb.t (list Exp.t) /** predicate symbol applied to exps */
| Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */;
| Anpred PredSymb.t (list Exp.t) /** negated predicate symbol applied to exps */
[@@deriving compare];
let equal_atom: atom => atom => bool;
/** kind of lseg or dllseg predicates */
type lseg_kind =
| Lseg_NE /** nonempty (possibly circular) listseg */
| Lseg_PE /** possibly empty (possibly circular) listseg */;
| Lseg_PE /** possibly empty (possibly circular) listseg */
[@@deriving compare];
let equal_lseg_kind: lseg_kind => lseg_kind => bool;
/** The boolean is true when the pointer was dereferenced without testing for zero. */
@ -111,7 +125,8 @@ type inst =
| Irearrange zero_flag null_case_flag int PredSymb.path_pos
| Itaint
| Iupdate zero_flag null_case_flag int PredSymb.path_pos
| Ireturn_from_call int;
| Ireturn_from_call int
[@@deriving compare];
let inst_abstraction: inst;
@ -161,11 +176,13 @@ let inst_partial_join: inst => inst => inst;
/** meet of instrumentations */
let inst_partial_meet: inst => inst => inst;
type _inst = inst;
/** structured expressions represent a value of structured type, such as an array or a struct. */
type strexp =
| Eexp Exp.t inst /** Base case: expression with instrumentation */
| Estruct (list (Ident.fieldname, strexp)) inst /** C structure */
type strexp0 'inst =
| Eexp Exp.t 'inst /** Base case: expression with instrumentation */
| Estruct (list (Ident.fieldname, strexp0 _inst)) 'inst /** C structure */
/** Array of given length
There are two conditions imposed / used in the array case.
First, if some index and value pair appears inside an array
@ -173,45 +190,81 @@ type strexp =
For instance, x |->[10 | e1: v1] implies that e1 <= 9.
Second, if two indices appear in an array, they should be different.
For instance, x |->[10 | e1: v1, e2: v2] implies that e1 != e2. */
| Earray Exp.t (list (Exp.t, strexp)) inst;
| Earray Exp.t (list (Exp.t, strexp0 _inst)) 'inst
[@@deriving compare];
type strexp = strexp0 inst;
/** Comparison function for strexp.
The inst:: parameter specifies whether instumentations should also
be considered (false by default). */
let compare_strexp: inst::bool? => strexp => strexp => int;
/** Equality function for strexp.
The inst:: parameter specifies whether instumentations should also
be considered (false by default). */
let equal_strexp: inst::bool? => strexp => strexp => bool;
/** an atomic heap predicate */
type hpred =
| Hpointsto Exp.t strexp Exp.t
type hpred0 'inst =
| Hpointsto Exp.t (strexp0 'inst) Exp.t
/** represents [exp|->strexp:typexp] where [typexp]
is an expression representing a type, e.g. [sizeof(t)]. */
| Hlseg lseg_kind hpara Exp.t Exp.t (list Exp.t)
is an expression representing a type, e.h. [sizeof(t)]. */
| Hlseg lseg_kind (hpara0 'inst) Exp.t Exp.t (list Exp.t)
/** higher - order predicate for singly - linked lists.
Should ensure that exp1!= exp2 implies that exp1 is allocated.
This assumption is used in the rearrangement. The last [exp list] parameter
is used to denote the shared links by all the nodes in the list.*/
| Hdllseg lseg_kind hpara_dll Exp.t Exp.t Exp.t Exp.t (list Exp.t)
/** higher-order predicate for doubly-linked lists. */
/** parameter for the higher-order singly-linked list predicate.
Means "lambda (root,next,svars). Exists evars. body".
Assume that root, next, svars, evars are disjoint sets of
primed identifiers, and include all the free primed identifiers in body.
body should not contain any non - primed identifiers or program
variables (i.e. pvars). */
and hpara = {
is used to denote the shared links by all the nodes in the list. */
| Hdllseg lseg_kind (hpara_dll0 'inst) Exp.t Exp.t Exp.t Exp.t (list Exp.t)
/** higher-order predicate for doubly-linked lists.
Parameter for the higher-order singly-linked list predicate.
Means "lambda (root,next,svars). Exists evars. body".
Assume that root, next, svars, evars are disjoint sets of
primed identifiers, and include all the free primed identifiers in body.
body should not contain any non - primed identifiers or program
variables (i.e. pvars). */
[@@deriving compare]
and hpara0 'inst = {
root: Ident.t,
next: Ident.t,
svars: list Ident.t,
evars: list Ident.t,
body: list hpred
body: list (hpred0 'inst)
}
[@@deriving compare]
/** parameter for the higher-order doubly-linked list predicates.
Assume that all the free identifiers in body_dll should belong to
cell, blink, flink, svars_dll, evars_dll. */
and hpara_dll = {
and hpara_dll0 'inst = {
cell: Ident.t, /** address cell */
blink: Ident.t, /** backward link */
flink: Ident.t, /** forward link */
svars_dll: list Ident.t,
evars_dll: list Ident.t,
body_dll: list hpred
};
body_dll: list (hpred0 'inst)
}
[@@deriving compare];
type hpred = hpred0 inst;
type hpara = hpara0 inst;
type hpara_dll = hpara_dll0 inst;
/** Comparison function for hpred.
The inst:: parameter specifies whether instumentations should also
be considered (false by default). */
let compare_hpred: inst::bool? => hpred => hpred => int;
/** Equality function for hpred.
The inst:: parameter specifies whether instumentations should also
be considered (false by default). */
let equal_hpred: inst::bool? => hpred => hpred => bool;
/** Sets of heap predicates */
@ -260,63 +313,6 @@ let block_pvar: Pvar.t;
/** Check if a pvar is a local pointing to a block in objc */
let is_block_pvar: Pvar.t => bool;
let exp_typ_compare: (Exp.t, Typ.t) => (Exp.t, Typ.t) => int;
let instr_compare: instr => instr => int;
/** compare instructions from different procedures without considering loc's, ident's, and pvar's.
the [exp_map] param gives a mapping of names used in the procedure of [instr1] to identifiers
used in the procedure of [instr2] */
let instr_compare_structural: instr => instr => Exp.Map.t Exp.t => (int, Exp.Map.t Exp.t);
let atom_compare: atom => atom => int;
let atom_equal: atom => atom => bool;
/** Comparison function for strexp.
The inst:: parameter specifies whether instumentations should also
be considered (false by default). */
let strexp_compare: inst::bool? => strexp => strexp => int;
/** Equality function for strexp.
The inst:: parameter specifies whether instumentations should also
be considered (false by default). */
let strexp_equal: inst::bool? => strexp => strexp => bool;
let hpara_compare: hpara => hpara => int;
let hpara_equal: hpara => hpara => bool;
let hpara_dll_compare: hpara_dll => hpara_dll => int;
let hpara_dll_equal: hpara_dll => hpara_dll => bool;
let lseg_kind_compare: lseg_kind => lseg_kind => int;
let lseg_kind_equal: lseg_kind => lseg_kind => bool;
/** Comparison function for hpred.
The inst:: parameter specifies whether instumentations should also
be considered (false by default). */
let hpred_compare: inst::bool? => hpred => hpred => int;
/** Equality function for hpred.
The inst:: parameter specifies whether instumentations should also
be considered (false by default). */
let hpred_equal: inst::bool? => hpred => hpred => bool;
let fld_strexp_compare: (Ident.fieldname, strexp) => (Ident.fieldname, strexp) => int;
let fld_strexp_list_compare:
list (Ident.fieldname, strexp) => list (Ident.fieldname, strexp) => int;
let exp_strexp_compare: (Exp.t, strexp) => (Exp.t, strexp) => int;
/** Return the lhs expression of a hpred */
let hpred_get_lhs: hpred => Exp.t;
@ -669,7 +665,11 @@ let hpara_av_add: fav => hpara => unit;
/** {2 Substitution} */
type subst;
type subst [@@deriving compare];
/** Equality for substitutions. */
let equal_subst: subst => subst => bool;
/** Create a substitution from a list of pairs.
@ -690,14 +690,6 @@ let sub_to_list: subst => list (Ident.t, Exp.t);
let sub_empty: subst;
/** Comparison for substitutions. */
let sub_compare: subst => subst => int;
/** Equality for substitutions. */
let sub_equal: subst => subst => bool;
/** Compute the common id-exp part of two inputs [subst1] and [subst2].
The first component of the output is this common part.
The second and third components are the remainder of [subst1]

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

@ -135,7 +135,7 @@ let filter_atoms tenv ~f prop =
let remove tenv prop atom =
if is_pred atom then
let natom = Prop.atom_normalize_prop tenv prop atom in
let f a = not (Sil.atom_equal natom a) in
let f a = not (Sil.equal_atom natom a) in
filter_atoms tenv ~f prop
else
prop
@ -295,7 +295,7 @@ let find_equal_formal_path tenv e prop =
let rec find_in_sigma e seen_hpreds =
IList.fold_right (
fun hpred res ->
if IList.mem Sil.hpred_equal hpred seen_hpreds then None
if IList.mem Sil.equal_hpred hpred seen_hpreds then None
else
let seen_hpreds = hpred :: seen_hpreds in
match res with

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

@ -189,7 +189,7 @@ let mk_rule_lsls_ls tenv k1 k2 impl_ok1 impl_ok2 para =
(find id_base, find id_next, find id_end)
with Not_found -> assert false in
let spooky_case _ =
(lseg_kind_equal Sil.Lseg_PE k_res)
(equal_lseg_kind Sil.Lseg_PE k_res)
&& (check_allocatedness p_leftover inst_end)
&& ((check_disequal p_start inst_base inst_next)
|| (check_disequal p_start inst_next inst_end)) in
@ -836,7 +836,7 @@ module IdMap = Map.Make (Ident) (** maps from identifiers *)
module HpredSet =
Set.Make(struct
type t = Sil.hpred
let compare = Sil.hpred_compare ~inst:false
let compare = Sil.compare_hpred ~inst:false
end)
let hpred_entries hpred = match hpred with
@ -904,9 +904,9 @@ let get_cycle root prop =
match el with
| [] -> path, false
| (f, e):: el' ->
if Sil.strexp_equal e e_root then
if Sil.equal_strexp e e_root then
(et_src, f, e):: path, true
else if IList.mem Sil.strexp_equal e visited then
else if IList.mem Sil.equal_strexp e visited then
path, false
else (
let visited' = (fst et_src):: visited in
@ -954,7 +954,7 @@ let get_var_retain_cycle prop_ =
let sigma = prop_.Prop.sigma in
let is_pvar v h =
match h with
| Sil.Hpointsto (Exp.Lvar _, v', _) when Sil.strexp_equal v v' -> true
| Sil.Hpointsto (Exp.Lvar _, v', _) when Sil.equal_strexp v v' -> true
| _ -> false in
let is_hpred_block v h =
match h, v with

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

@ -271,7 +271,7 @@ end = struct
let replace_strexp_sigma footprint_part ((_, hpred, syn_offs) : t) se_in sigma_in =
let new_sigma = hpred :: sigma_in in
let sigma' = replace_strexp tenv footprint_part (new_sigma, hpred, syn_offs) se_in in
IList.sort Sil.hpred_compare sigma'
IList.sort Sil.compare_hpred sigma'
*)
end

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

@ -32,10 +32,10 @@ let sigma_equal sigma1 sigma2 =
| [], _:: _ | _:: _, [] ->
(L.d_strln "failure reason 1"; raise IList.Fail)
| hpred1:: sigma1_rest', hpred2:: sigma2_rest' ->
if Sil.hpred_equal hpred1 hpred2 then f sigma1_rest' sigma2_rest'
if Sil.equal_hpred hpred1 hpred2 then f sigma1_rest' sigma2_rest'
else (L.d_strln "failure reason 2"; raise IList.Fail) in
let sigma1_sorted = IList.sort Sil.hpred_compare sigma1 in
let sigma2_sorted = IList.sort Sil.hpred_compare sigma2 in
let sigma1_sorted = IList.sort Sil.compare_hpred sigma1 in
let sigma2_sorted = IList.sort Sil.compare_hpred sigma2 in
f sigma1_sorted sigma2_sorted
let sigma_get_start_lexps_sort sigma =
@ -1436,7 +1436,7 @@ let rec sigma_partial_join' tenv mode (sigma_acc: Prop.sigma)
| Some (Sil.Hlseg (k, _, _, _, _) as lseg), None
| Some (Sil.Hdllseg (k, _, _, _, _, _, _) as lseg), None ->
if (not Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then
if (not Config.nelseg) || (Sil.equal_lseg_kind k Sil.Lseg_PE) then
let sigma_acc' = join_list_and_non Lhs e lseg e1 e2 :: sigma_acc in
sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2
else
@ -1444,7 +1444,7 @@ let rec sigma_partial_join' tenv mode (sigma_acc: Prop.sigma)
| None, Some (Sil.Hlseg (k, _, _, _, _) as lseg)
| None, Some (Sil.Hdllseg (k, _, _, _, _, _, _) as lseg) ->
if (not Config.nelseg) || (Sil.lseg_kind_equal k Sil.Lseg_PE) then
if (not Config.nelseg) || (Sil.equal_lseg_kind k Sil.Lseg_PE) then
let sigma_acc' = join_list_and_non Rhs e lseg e2 e1 :: sigma_acc in
sigma_partial_join' tenv mode sigma_acc' sigma1 sigma2
else
@ -1675,7 +1675,7 @@ let pi_partial_join tenv mode
IList.fold_left (handle_atom_with_widening Rhs p1 pi1) [] pi2 in
if Config.trace_join then
(L.d_str "atom_list2: "; Prop.d_pi atom_list2; L.d_ln ());
let atom_list_combined = IList.inter Sil.atom_compare atom_list1 atom_list2 in
let atom_list_combined = IList.inter Sil.compare_atom atom_list1 atom_list2 in
if Config.trace_join then
(L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ());
atom_list_combined
@ -1722,7 +1722,7 @@ let eprop_partial_meet tenv (ep1: 'a Prop.t) (ep2: 'b Prop.t) : 'c Prop.t =
let sub2 = ep2.Prop.sub in
let range1 = Sil.sub_range sub1 in
let f e = Sil.fav_for_all (Sil.exp_fav e) Ident.is_normal in
Sil.sub_equal sub1 sub2 && IList.for_all f range1 in
Sil.equal_subst sub1 sub2 && IList.for_all f range1 in
if not (sub_check ()) then
(L.d_strln "sub_check() failed"; raise IList.Fail)

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

@ -384,7 +384,7 @@ let in_cycle cycle edge =
match cycle with
| Some cycle' ->
IList.mem (fun (fn, se) (_,fn',se') ->
Ident.equal_fieldname fn fn' && Sil.strexp_equal se se') edge cycle'
Ident.equal_fieldname fn fn' && Sil.equal_strexp se se') edge cycle'
| _ -> false
let node_in_cycle cycle node =

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

@ -335,7 +335,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
| (None, _) when not hpat.flag ->
(* L.out "@[.... iter_match_with_impl (lseg not-matched) ....@\n@."; *)
None
| (None, _) when Sil.lseg_kind_equal k2 Sil.Lseg_NE ->
| (None, _) when Sil.equal_lseg_kind k2 Sil.Lseg_NE ->
(* L.out "@[.... iter_match_with_impl (lseg not-matched) ....@\n@."; *)
do_para_lseg ()
| (None, _) ->
@ -390,7 +390,7 @@ let rec iter_match_with_impl tenv iter condition sub vars hpat hpats =
| Some _ -> None
in begin match ((Prop.prop_iter_find iter filter), hpats) with
| (None, _) when not hpat.flag -> None
| (None, _) when Sil.lseg_kind_equal k2 Sil.Lseg_NE -> do_para_dllseg ()
| (None, _) when Sil.equal_lseg_kind k2 Sil.Lseg_NE -> do_para_dllseg ()
| (None, _) -> execute_with_backtracking [do_emp_dllseg; do_para_dllseg]
| (Some iter_cur, []) -> do_empty_hpats iter_cur ()
| (Some iter_cur, _) -> execute_with_backtracking [do_nonempty_hpats iter_cur; do_next iter_cur]

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

@ -127,7 +127,7 @@ module NullifyTransferFunctions = struct
let is_last_instr_in_node instr node =
let rec is_last_instr instr = function
| [] -> true
| last_instr :: [] -> Sil.instr_compare instr last_instr = 0
| last_instr :: [] -> Sil.compare_instr instr last_instr = 0
| _ :: instrs -> is_last_instr instr instrs in
is_last_instr instr (CFG.instrs node)

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

@ -112,7 +112,7 @@ let rec pi_compare pi1 pi2 =
| ([], _:: _) -> - 1
| (_:: _,[]) -> 1
| (a1:: pi1', a2:: pi2') ->
let n = Sil.atom_compare a1 a2 in
let n = Sil.compare_atom a1 a2 in
if n <> 0 then n
else pi_compare pi1' pi2'
@ -127,7 +127,7 @@ let rec sigma_compare sigma1 sigma2 =
| ([], _:: _) -> - 1
| (_:: _,[]) -> 1
| (h1:: sigma1', h2:: sigma2') ->
let n = Sil.hpred_compare h1 h2 in
let n = Sil.compare_hpred h1 h2 in
if n <> 0 then n
else sigma_compare sigma1' sigma2'
@ -137,7 +137,7 @@ let sigma_equal sigma1 sigma2 =
(** Comparison between propositions. Lexicographical order. *)
let prop_compare p1 p2 =
sigma_compare p1.sigma p2.sigma
|> next Sil.sub_compare p1.sub p2.sub
|> next Sil.compare_subst p1.sub p2.sub
|> next pi_compare p1.pi p2.pi
|> next sigma_compare p1.sigma_fp p2.sigma_fp
|> next pi_compare p1.pi_fp p2.pi_fp
@ -230,7 +230,7 @@ let sigma_get_stack_nonstack only_local_vars sigma =
let pp_sigma_simple pe env fmt sigma =
let sigma_stack, sigma_nonstack = sigma_get_stack_nonstack false sigma in
let pp_stack fmt _sg =
let sg = IList.sort Sil.hpred_compare _sg in
let sg = IList.sort Sil.compare_hpred _sg in
if sg != [] then Format.fprintf fmt "%a" (pp_semicolon_seq pe (pp_hpred_stackvar pe)) sg in
let pp_nl fmt doit = if doit then
(match pe.pe_kind with
@ -549,7 +549,7 @@ let rec pi_sorted_remove_redundant (pi : pi) = match pi with
(* first inequality redundant *)
pi_sorted_remove_redundant (a2 :: rest)
| a1:: a2:: rest ->
if Sil.atom_equal a1 a2 then pi_sorted_remove_redundant (a2 :: rest)
if Sil.equal_atom a1 a2 then pi_sorted_remove_redundant (a2 :: rest)
else a1 :: pi_sorted_remove_redundant (a2 :: rest)
| [a] -> [a]
| [] -> []
@ -1314,13 +1314,13 @@ module Normalize = struct
when IntLit.isone i ->
let lower = Exp.int (n -- IntLit.one) in
let a_lower : Sil.atom = Aeq (BinOp (Lt, lower, Var id), Exp.one) in
if not (IList.mem Sil.atom_equal a_lower p.pi) then a'
if not (IList.mem Sil.equal_atom a_lower p.pi) then a'
else Aeq (Var id, Exp.int n)
| Aeq (BinOp (Lt, Const (Cint n), Var id), Const (Cint i))
when IntLit.isone i ->
let upper = Exp.int (n ++ IntLit.one) in
let a_upper : Sil.atom = Aeq (BinOp (Le, Var id, upper), Exp.one) in
if not (IList.mem Sil.atom_equal a_upper p.pi) then a'
if not (IList.mem Sil.equal_atom a_upper p.pi) then a'
else Aeq (Var id, upper)
| Aeq (BinOp (Ne, e1, e2), Const (Cint i)) when IntLit.isone i ->
Aneq (e1, e2)
@ -1338,7 +1338,7 @@ module Normalize = struct
let fld_cnts' =
IList.map (fun (fld, cnt) ->
fld, strexp_normalize tenv sub cnt) fld_cnts in
let fld_cnts'' = IList.sort Sil.fld_strexp_compare fld_cnts' in
let fld_cnts'' = IList.sort [%compare: Ident.fieldname * Sil.strexp] fld_cnts' in
Estruct (fld_cnts'', inst)
end
| Earray (len, idx_cnts, inst) ->
@ -1353,7 +1353,7 @@ module Normalize = struct
let idx' = exp_normalize tenv sub idx in
idx', strexp_normalize tenv sub cnt) idx_cnts in
let idx_cnts'' =
IList.sort Sil.exp_strexp_compare idx_cnts' in
IList.sort [%compare: Exp.t * Sil.strexp] idx_cnts' in
Earray (len', idx_cnts'', inst)
end
@ -1433,18 +1433,18 @@ module Normalize = struct
and hpara_normalize tenv (para : Sil.hpara) =
let normalized_body = IList.map (hpred_normalize tenv Sil.sub_empty) (para.body) in
let sorted_body = IList.sort Sil.hpred_compare normalized_body in
let sorted_body = IList.sort Sil.compare_hpred normalized_body in
{ para with body = sorted_body }
and hpara_dll_normalize tenv (para : Sil.hpara_dll) =
let normalized_body = IList.map (hpred_normalize tenv Sil.sub_empty) (para.body_dll) in
let sorted_body = IList.sort Sil.hpred_compare normalized_body in
let sorted_body = IList.sort Sil.compare_hpred normalized_body in
{ para with body_dll = sorted_body }
let sigma_normalize tenv sub sigma =
let sigma' =
IList.stable_sort Sil.hpred_compare (IList.map (hpred_normalize tenv sub) sigma) in
IList.stable_sort Sil.compare_hpred (IList.map (hpred_normalize tenv sub) sigma) in
if sigma_equal sigma sigma' then sigma else sigma'
let pi_tighten_ineq tenv pi =
@ -1540,7 +1540,7 @@ module Normalize = struct
| _ -> true in
let pi' =
IList.stable_sort
Sil.atom_compare
Sil.compare_atom
((IList.filter filter_useful_atom nonineq_list) @ ineq_list) in
let pi'' = pi_sorted_remove_redundant pi' in
if pi_equal pi0 pi'' then pi0 else pi''
@ -1580,12 +1580,12 @@ module Normalize = struct
let sub_normalize sub =
let f (id, e) = (not (Ident.is_primed id)) && (not (Sil.ident_in_exp id e)) in
let sub' = Sil.sub_filter_pair f sub in
if Sil.sub_equal sub sub' then sub else sub'
if Sil.equal_subst sub sub' then sub else sub'
(** Conjoin a pure atomic predicate by normal conjunction. *)
let rec prop_atom_and tenv ?(footprint=false) (p : normal t) a : normal t =
let a' = normalize_and_strengthen_atom tenv p a in
if IList.mem Sil.atom_equal a' p.pi then p
if IList.mem Sil.equal_atom a' p.pi then p
else begin
let p' =
match a' with
@ -2152,7 +2152,7 @@ let exist_quantify tenv fav (prop : normal t) : normal t =
(* throw away x=E if x becomes _x *)
let mem_idlist i = IList.exists (fun id -> Ident.equal i id) in
let sub = Sil.sub_filter (fun i -> not (mem_idlist i ids)) prop.sub in
if Sil.sub_equal sub prop.sub then prop
if Sil.equal_subst sub prop.sub then prop
else unsafe_cast_to_normal (set prop ~sub) in
(*
L.out "@[<2>.... Existential Quantification ....\n";
@ -2457,7 +2457,7 @@ let rec strexp_gc_fields (fav: Sil.fav) (se : Sil.strexp) =
let fsel' =
let fselo' = IList.filter (function | (_, Some _) -> true | _ -> false) fselo in
IList.map (function (f, seo) -> (f, unSome seo)) fselo' in
if Sil.fld_strexp_list_compare fsel fsel' = 0 then Some se
if [%compare.equal: (Ident.fieldname * Sil.strexp) list] fsel fsel' then Some se
else Some (Sil.Estruct (fsel', inst))
| Earray _ ->
Some se
@ -2469,7 +2469,7 @@ let hpred_gc_fields (fav: Sil.fav) (hpred : Sil.hpred) : Sil.hpred = match hpred
(match strexp_gc_fields fav se with
| None -> hpred
| Some se' ->
if Sil.strexp_compare se se' = 0 then hpred
if Sil.compare_strexp se se' = 0 then hpred
else Hpointsto (e, se', te))
| Hlseg _ | Hdllseg _ ->
hpred

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

@ -98,8 +98,8 @@ let get_edges footprint_part g =
IList.map (fun hpred -> Ehpred hpred) hpreds @ IList.map (fun a -> Eatom a) atoms @ IList.map (fun entry -> Esub_entry entry) subst_entries
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
| Ehpred hp1, Ehpred hp2 -> Sil.equal_hpred hp1 hp2
| Eatom a1, Eatom a2 -> Sil.equal_atom a1 a2
| Esub_entry (x1, e1), Esub_entry (x2, e2) -> Ident.equal x1 x2 && Exp.equal e1 e2
| _ -> false

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

@ -565,7 +565,7 @@ let check_equal tenv prop e1 e2 =
let eq = Sil.Aeq(n_e1, n_e2) in
let n_eq = Prop.atom_normalize_prop tenv prop eq in
let pi = prop.Prop.pi in
IList.exists (Sil.atom_equal n_eq) pi in
IList.exists (Sil.equal_atom n_eq) pi in
check_equal () || check_equal_const () || check_equal_pi ()
(** Check [ |- e=0]. Result [false] means "don't know". *)
@ -769,7 +769,7 @@ let check_atom tenv prop a0 =
when IntLit.isone i -> check_lt_normalized tenv prop e1 e2
| Sil.Aeq (e1, e2) -> check_equal tenv prop e1 e2
| Sil.Aneq (e1, e2) -> check_disequal tenv prop e1 e2
| Sil.Apred _ | Anpred _ -> IList.exists (Sil.atom_equal a) prop.Prop.pi
| Sil.Apred _ | Anpred _ -> IList.exists (Sil.equal_atom a) prop.Prop.pi
(** Check [prop |- e1<=e2]. Result [false] means "don't know". *)
let check_le tenv prop e1 e2 =
@ -1432,12 +1432,12 @@ let filter_ne_lhs sub e0 = function
let filter_hpred sub hpred2 hpred1 = match (Sil.hpred_sub sub hpred1), hpred2 with
| Sil.Hlseg(Sil.Lseg_NE, hpara1, e1, f1, el1), Sil.Hlseg(Sil.Lseg_PE, _, _, _, _) ->
if Sil.hpred_equal (Sil.Hlseg(Sil.Lseg_PE, hpara1, e1, f1, el1)) hpred2 then Some false else None
if Sil.equal_hpred (Sil.Hlseg(Sil.Lseg_PE, hpara1, e1, f1, el1)) hpred2 then Some false else None
| 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 *)
if Sil.equal_hpred (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 Exp.equal e1 e2 then Some false else None
| hpred1, hpred2 -> if Sil.hpred_equal hpred1 hpred2 then Some false else None
| hpred1, hpred2 -> if Sil.equal_hpred hpred1 hpred2 then Some false else None
let hpred_has_primed_lhs sub hpred =
let rec find_primed e = match e with

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

@ -217,7 +217,7 @@ let rec _strexp_extend_values
let replace acc (res_atoms', res_se', res_typ') =
let replace_fse = replace_fv res_se' in
let res_fsel' =
IList.sort Sil.fld_strexp_compare (IList.map replace_fse fsel) in
IList.sort [%compare: Ident.fieldname * Sil.strexp] (IList.map replace_fse fsel) in
let replace_fta (f, t, a) =
let f', t' = replace_fv res_typ' (f, t) in
(f', t', a) in
@ -230,7 +230,7 @@ let rec _strexp_extend_values
let atoms', se', res_typ' =
create_struct_values
pname tenv orig_prop footprint_part kind max_stamp typ' off' inst in
let res_fsel' = IList.sort Sil.fld_strexp_compare ((f, se'):: fsel) in
let res_fsel' = IList.sort [%compare: Ident.fieldname * Sil.strexp] ((f, se'):: fsel) in
let replace_fta (f', t', a') =
if Ident.equal_fieldname f' f then (f, res_typ', a') else (f', t', a') in
let fields' =
@ -312,7 +312,7 @@ and array_case_analysis_index pname tenv orig_prop
create_struct_values
pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst in
check_sound elem_typ;
let cont_new = IList.sort Sil.exp_strexp_compare ((index, elem_se):: array_cont) in
let cont_new = IList.sort [%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) in
let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
let typ_new = Typ.Tarray (elem_typ, typ_array_len) in
[(atoms, array_new, typ_new)]
@ -325,7 +325,7 @@ and array_case_analysis_index pname tenv orig_prop
create_struct_values
pname tenv orig_prop footprint_part kind max_stamp typ_cont off inst in
check_sound elem_typ;
let cont_new = IList.sort Sil.exp_strexp_compare ((index, elem_se):: array_cont) in
let cont_new = IList.sort [%compare: Exp.t * Sil.strexp] ((index, elem_se):: array_cont) in
let array_new = Sil.Earray (array_len, cont_new, inst_arr) in
let typ_new = Typ.Tarray (elem_typ, typ_array_len) in
[(atoms, array_new, typ_new)]
@ -554,7 +554,7 @@ let prop_iter_extend_ptsto pname tenv orig_prop iter lexp inst =
| _ ->
L.d_warning "Cannot extend "; Sil.d_exp lexp; L.d_strln " in"; Prop.d_prop (Prop.prop_iter_to_prop tenv iter); L.d_ln();
[([], footprint_sigma)] in
IList.map (fun (atoms, sigma') -> (atoms, IList.stable_sort Sil.hpred_compare sigma')) atoms_sigma_list in
IList.map (fun (atoms, sigma') -> (atoms, IList.stable_sort Sil.compare_hpred sigma')) atoms_sigma_list in
let iter_atoms_fp_sigma_list =
list_product iter_list atoms_fp_sigma_list in
IList.map (fun (iter, (atoms, fp_sigma)) ->

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

@ -217,7 +217,7 @@ let mk_find_duplicate_nodes proc_desc : (Procdesc.Node.t -> Procdesc.NodeSet.t)
| _ -> raise Not_found in
let duplicates =
let equal_normalized_instrs (_, normalized_instrs') =
IList.compare Sil.instr_compare node_normalized_instrs normalized_instrs' = 0 in
IList.compare Sil.compare_instr node_normalized_instrs normalized_instrs' = 0 in
IList.filter equal_normalized_instrs elements in
IList.fold_left
(fun nset (node', _) -> Procdesc.NodeSet.add node' nset)

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

@ -403,7 +403,7 @@ let hpred_lhs_compare hpred1 hpred2 = match hpred1, hpred2 with
| Sil.Hpointsto(e1, _, _), Sil.Hpointsto(e2, _, _) -> Exp.compare e1 e2
| Sil.Hpointsto _, _ -> - 1
| _, Sil.Hpointsto _ -> 1
| hpred1, hpred2 -> Sil.hpred_compare hpred1 hpred2
| hpred1, hpred2 -> Sil.compare_hpred hpred1 hpred2
(** set the inst everywhere in a sexp *)
let rec sexp_set_inst inst = function
@ -974,7 +974,7 @@ let do_taint_check tenv caller_pname callee_pname calling_prop missing_pi sub ac
(Exp.Map.exists
(fun _ (_, untaint_atoms) ->
IList.exists
(fun a -> Sil.atom_equal atom a)
(fun a -> Sil.equal_atom atom a)
untaint_atoms)
taint_untaint_exp_map) in
check_taint_on_variadic_function tenv callee_pname caller_pname actual_params calling_prop;

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

@ -25,9 +25,9 @@ struct
| Sil.Call (_, e1, etl1, _, cf1), Sil.Call (_, e2, etl2, _, cf2) ->
(* ignore return ids and call flags *)
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 let n = IList.compare [%compare: Exp.t * Typ.t] etl1 etl2 in
if n <> 0 then n else CallFlags.compare cf1 cf2
| _ -> Sil.instr_compare i1 i2
| _ -> Sil.compare_instr i1 i2
end)
type extension = InstrSet.t

Write Preview
Loading…
Cancel
Save