From aa5998a9d19fa1c3860e58c8f3536ae82e4d383b Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 29 Nov 2016 16:37:54 -0800 Subject: [PATCH] ppx_compare Sil Reviewed By: cristianoc Differential Revision: D4232394 fbshipit-source-id: 3296d74 --- infer/src/IR/Cfg.re | 2 +- infer/src/IR/Sil.re | 654 ++++----------------- infer/src/IR/Sil.rei | 178 +++--- infer/src/backend/Attribute.ml | 4 +- infer/src/backend/abs.ml | 10 +- infer/src/backend/absarray.ml | 2 +- infer/src/backend/dom.ml | 14 +- infer/src/backend/dotty.ml | 2 +- infer/src/backend/match.ml | 4 +- infer/src/backend/preanal.ml | 2 +- infer/src/backend/prop.ml | 36 +- infer/src/backend/propgraph.ml | 4 +- infer/src/backend/prover.ml | 10 +- infer/src/backend/rearrange.ml | 10 +- infer/src/backend/state.ml | 2 +- infer/src/backend/tabulation.ml | 4 +- infer/src/checkers/repeatedCallsChecker.ml | 4 +- 17 files changed, 254 insertions(+), 688 deletions(-) diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 66ca3b0db..81544e7a5 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -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 } diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index ae1995fb1..e95552811 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -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; }; diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index afba88c53..853cdcc83 100644 --- a/infer/src/IR/Sil.rei +++ b/infer/src/IR/Sil.rei @@ -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] diff --git a/infer/src/backend/Attribute.ml b/infer/src/backend/Attribute.ml index c68fab377..a4701a8ac 100644 --- a/infer/src/backend/Attribute.ml +++ b/infer/src/backend/Attribute.ml @@ -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 diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index 982e8f7bf..547e8efe5 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -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 diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index a22afd4c8..8727b6264 100644 --- a/infer/src/backend/absarray.ml +++ b/infer/src/backend/absarray.ml @@ -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 diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index 8a9158821..7d7c39b18 100644 --- a/infer/src/backend/dom.ml +++ b/infer/src/backend/dom.ml @@ -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) diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 32bd6d1bf..31bd1fe58 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -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 = diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index f0bca1a23..cc34f174d 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -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] diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index f2f304917..045ccb0a8 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -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) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index da214226b..660ee8cc2 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -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 diff --git a/infer/src/backend/propgraph.ml b/infer/src/backend/propgraph.ml index 7e83a6e7e..8a2e4bc4c 100644 --- a/infer/src/backend/propgraph.ml +++ b/infer/src/backend/propgraph.ml @@ -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 diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 1a5809005..c10d2550c 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -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 diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 8d411911b..d1a2df363 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -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)) -> diff --git a/infer/src/backend/state.ml b/infer/src/backend/state.ml index d15efed6e..1eab0a550 100644 --- a/infer/src/backend/state.ml +++ b/infer/src/backend/state.ml @@ -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) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 881987fb5..9804c5be1 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -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; diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml index 4c95f3c90..2efe30490 100644 --- a/infer/src/checkers/repeatedCallsChecker.ml +++ b/infer/src/checkers/repeatedCallsChecker.ml @@ -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