From abc36fe97f4b27c75ce880a90e89e8f3810bff2f Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 28 Jan 2021 06:47:47 -0800 Subject: [PATCH] [pulse] add a bunch of equal and compare functions Summary: This is all dead code but I had to do this to try something else and I don't want to have to do that again :) Reviewed By: skcho Differential Revision: D26022111 fbshipit-source-id: 622ca10b9 --- infer/src/absint/HilExp.ml | 4 +++- infer/src/absint/HilExp.mli | 2 +- infer/src/bufferoverrun/itv.ml | 2 +- infer/src/bufferoverrun/itv.mli | 2 +- infer/src/istd/PrettyPrintable.ml | 6 +++--- infer/src/istd/PrettyPrintable.mli | 4 +--- infer/src/istd/RecencyMap.ml | 15 +++++++++++---- infer/src/istd/RecencyMap.mli | 6 +++--- infer/src/istd/UnionFind.ml | 6 +++--- infer/src/istd/UnionFind.mli | 2 +- infer/src/pulse/PulseAbductiveDomain.ml | 8 ++++---- infer/src/pulse/PulseAbductiveDomain.mli | 5 +++-- infer/src/pulse/PulseBaseAddressAttributes.ml | 4 ++++ .../src/pulse/PulseBaseAddressAttributes.mli | 2 +- infer/src/pulse/PulseBaseDomain.ml | 3 ++- infer/src/pulse/PulseBaseDomain.mli | 2 +- infer/src/pulse/PulseBaseMemory.ml | 4 ++++ infer/src/pulse/PulseBaseMemory.mli | 4 ++++ infer/src/pulse/PulseBaseStack.ml | 4 +++- infer/src/pulse/PulseBaseStack.mli | 2 ++ infer/src/pulse/PulseCItv.ml | 7 ++++--- infer/src/pulse/PulseCItv.mli | 2 +- infer/src/pulse/PulseDiagnostic.ml | 4 ++-- infer/src/pulse/PulseDiagnostic.mli | 4 ++-- infer/src/pulse/PulseExecutionDomain.ml | 4 ++-- infer/src/pulse/PulseExecutionDomain.mli | 2 +- infer/src/pulse/PulseFormula.ml | 19 +++++++++++++------ infer/src/pulse/PulseFormula.mli | 2 +- infer/src/pulse/PulseLatentIssue.ml | 2 +- infer/src/pulse/PulseLatentIssue.mli | 2 +- infer/src/pulse/PulsePathCondition.ml | 7 +++++++ infer/src/pulse/PulsePathCondition.mli | 2 +- infer/src/pulse/PulseSkippedCalls.ml | 6 +++++- infer/src/pulse/PulseSkippedCalls.mli | 4 ++++ infer/src/pulse/PulseTopl.ml | 4 +++- infer/src/pulse/PulseTopl.mli | 2 +- 36 files changed, 105 insertions(+), 55 deletions(-) diff --git a/infer/src/absint/HilExp.ml b/infer/src/absint/HilExp.ml index 816b300e0..e70e41f32 100644 --- a/infer/src/absint/HilExp.ml +++ b/infer/src/absint/HilExp.ml @@ -15,13 +15,15 @@ let yojson_of_typ_ = [%yojson_of: _] let compare_typ_ _ _ = 0 +let equal_typ_ = [%compare.equal: typ_] + module Access = struct type ('fieldname, 'array_index) t_ = | FieldAccess of 'fieldname | ArrayAccess of typ_ * 'array_index | TakeAddress | Dereference - [@@deriving compare, yojson_of] + [@@deriving compare, equal, yojson_of] type 'array_index t = (Fieldname.t, 'array_index) t_ [@@deriving compare, yojson_of] diff --git a/infer/src/absint/HilExp.mli b/infer/src/absint/HilExp.mli index 257d3e5e0..f0eb55bad 100644 --- a/infer/src/absint/HilExp.mli +++ b/infer/src/absint/HilExp.mli @@ -14,7 +14,7 @@ module Access : sig | ArrayAccess of Typ.t * 'array_index | TakeAddress | Dereference - [@@deriving compare, yojson_of] + [@@deriving compare, equal, yojson_of] type 'array_index t = (Fieldname.t, 'array_index) t_ [@@deriving compare, yojson_of] diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 76234609c..bf65830b6 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -43,7 +43,7 @@ end module ItvPure = struct (** (l, u) represents the closed interval [l; u] (of course infinite bounds are open) *) - type t = Bound.t * Bound.t [@@deriving compare] + type t = Bound.t * Bound.t [@@deriving compare, equal] let lb : t -> Bound.t = fst diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli index 0b4d241ce..7805890fb 100644 --- a/infer/src/bufferoverrun/itv.mli +++ b/infer/src/bufferoverrun/itv.mli @@ -19,7 +19,7 @@ module ItvRange : sig end module ItvPure : sig - type t [@@deriving compare] + type t [@@deriving compare, equal] val pp : F.formatter -> t -> unit diff --git a/infer/src/istd/PrettyPrintable.ml b/infer/src/istd/PrettyPrintable.ml index 1091b045b..ccbb7e7b1 100644 --- a/infer/src/istd/PrettyPrintable.ml +++ b/infer/src/istd/PrettyPrintable.ml @@ -221,7 +221,7 @@ module type PrintableRankedType = sig end module type PPUniqRankSet = sig - type t + type t [@@deriving compare, equal] type rank @@ -231,8 +231,6 @@ module type PPUniqRankSet = sig val empty : t - val equal : t -> t -> bool - val find_rank : t -> rank -> elt option val fold : t -> init:'accum -> f:('accum -> elt -> 'accum) -> 'accum @@ -278,6 +276,8 @@ module MakePPUniqRankSet let empty = Map.empty + let compare = Map.compare Val.compare + let equal = Map.equal Val.equal let find_rank m rank = Map.find_opt rank m diff --git a/infer/src/istd/PrettyPrintable.mli b/infer/src/istd/PrettyPrintable.mli index 7f82ba9bd..5c0bd0ef8 100644 --- a/infer/src/istd/PrettyPrintable.mli +++ b/infer/src/istd/PrettyPrintable.mli @@ -172,7 +172,7 @@ end (** set where at most one element of a given rank can be present *) module type PPUniqRankSet = sig - type t + type t [@@deriving compare, equal] type rank @@ -182,8 +182,6 @@ module type PPUniqRankSet = sig val empty : t - val equal : t -> t -> bool - val find_rank : t -> rank -> elt option val fold : t -> init:'accum -> f:('accum -> elt -> 'accum) -> 'accum diff --git a/infer/src/istd/RecencyMap.ml b/infer/src/istd/RecencyMap.ml index 00595b676..828ae194f 100644 --- a/infer/src/istd/RecencyMap.ml +++ b/infer/src/istd/RecencyMap.ml @@ -13,7 +13,7 @@ module type Config = sig end module type S = sig - type t + type t [@@deriving compare, equal] type key @@ -48,10 +48,14 @@ module Make (Key : PrettyPrintable.PrintableEquatableOrderedType) (Value : PrettyPrintable.PrintableOrderedType) (Config : Config) : S with type key = Key.t and type value = Value.t = struct - type key = Key.t + type key = Key.t [@@deriving compare] type value = Value.t [@@deriving compare] + (* suppress warnings about using {!List.Assoc.compare} since our own compare function also ignores + that different representations of a [t] can have the same meaning *) + [@@@warning "-3"] + (** [new_] and [old] together represent the map. Keys may be present in both [old] and [new_], in which case bindings in [new_] take precendence. @@ -68,6 +72,11 @@ module Make ; old: (key, value) List.Assoc.t (** invariant: [List.length old ≤ Config.limit]. Actually, the length of [old] is always either [0] or [N], except possibly after a call to [merge]. *) } + [@@deriving compare] + + [@@@warning "+3"] + + let equal = [%compare.equal: t] let empty = {count_new= 0; old= []; new_= []} @@ -126,8 +135,6 @@ module Make else {count_new= next_count_new; new_= (key, value) :: new_without_key; old= map.old} - let equal map1 map2 = phys_equal map1 map2 - let fold map ~init ~f = let acc = List.fold map.new_ ~init ~f in (* this is quadratic time but the lists are at most [Config.limit] long, assumed small *) diff --git a/infer/src/istd/RecencyMap.mli b/infer/src/istd/RecencyMap.mli index 400457485..789b5bfb5 100644 --- a/infer/src/istd/RecencyMap.mli +++ b/infer/src/istd/RecencyMap.mli @@ -16,14 +16,14 @@ end (** A functional map interface where only the [N] most recently-accessed elements are guaranteed to be persisted, similarly to an LRU cache. The map stores at most [2*N] elements. *) module type S = sig - type t + (** Note that the derived [compare] and [equal] functions are sensitive to the underlying + implementation and in particular won't equate some objects that denote the same map. *) + type t [@@deriving compare, equal] type key type value - val equal : t -> t -> bool - val pp : F.formatter -> t -> unit val empty : t diff --git a/infer/src/istd/UnionFind.ml b/infer/src/istd/UnionFind.ml index 7369ecb88..9f59e51b7 100644 --- a/infer/src/istd/UnionFind.ml +++ b/infer/src/istd/UnionFind.ml @@ -26,7 +26,7 @@ struct (** to get a little bit of type safety *) type repr = private X.t - type t + type t [@@deriving compare, equal] val empty : t @@ -43,7 +43,7 @@ struct end = struct type repr = X.t - type t = X.t XMap.t + type t = X.t XMap.t [@@deriving compare, equal] let empty = XMap.empty @@ -82,7 +82,7 @@ struct UF.Map.remove x1 classes |> UF.Map.add x2 new_class end - type t = {reprs: UF.t; classes: XSet.t UF.Map.t} + type t = {reprs: UF.t; classes: XSet.t UF.Map.t} [@@deriving compare, equal] let empty = {reprs= UF.empty; classes= UF.Map.empty} diff --git a/infer/src/istd/UnionFind.mli b/infer/src/istd/UnionFind.mli index c454a8cae..6e2f65bac 100644 --- a/infer/src/istd/UnionFind.mli +++ b/infer/src/istd/UnionFind.mli @@ -21,7 +21,7 @@ module Make (X : Element) (XSet : Caml.Set.S with type elt = X.t) (XMap : Caml.Map.S with type key = X.t) : sig - type t + type t [@@deriving compare, equal] val pp : pp_empty:(F.formatter -> unit) -> (F.formatter -> X.t -> unit) -> F.formatter -> t -> unit diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 60689067f..773260d84 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -19,7 +19,7 @@ module BaseAddressAttributes = PulseBaseAddressAttributes module type BaseDomainSig = sig (* private because the lattice is not the same for preconditions and postconditions so we don't want to confuse them *) - type t = private BaseDomain.t [@@deriving yojson_of] + type t = private BaseDomain.t [@@deriving compare, equal, yojson_of] val empty : t @@ -86,7 +86,7 @@ end (** represents the inferred pre-condition at each program point, biabduction style *) module PreDomain : BaseDomainSig = PostDomain -type isl_status = ISLOk | ISLError [@@deriving equal, yojson_of] +type isl_status = ISLOk | ISLError [@@deriving compare, equal, yojson_of] let pp_isl_status f s = if Config.pulse_isl then @@ -106,7 +106,7 @@ type t = ; topl: (PulseTopl.state[@yojson.opaque]) ; skipped_calls: SkippedCalls.t ; isl_status: isl_status } -[@@deriving yojson_of] +[@@deriving compare, equal, yojson_of] let pp f {post; pre; topl; path_condition; skipped_calls; isl_status} = F.fprintf f "@[%a@;%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp @@ -628,7 +628,7 @@ let invalidate_locals pdesc astate : t = else {astate with post= PostDomain.update astate.post ~attrs:attrs'} -type summary = t [@@deriving yojson_of] +type summary = t [@@deriving compare, equal, yojson_of] let is_allocated {post; pre} v = let is_pvar = function Var.ProgramVar _ -> true | Var.LogicalVar _ -> false in diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index fbb979b99..7930b8c4b 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/infer/src/pulse/PulseAbductiveDomain.mli @@ -23,7 +23,7 @@ module BaseStack = PulseBaseStack module type BaseDomainSig = sig (* private because the lattice is not the same for preconditions and postconditions so we don't want to confuse them *) - type t = private BaseDomain.t [@@deriving yojson_of] + type t = private BaseDomain.t [@@deriving compare, equal, yojson_of] val yojson_of_t : t -> Yojson.Safe.t @@ -73,6 +73,7 @@ type t = private (** state at of the Topl monitor at the current program point, when Topl is enabled *) ; skipped_calls: SkippedCalls.t (** metadata: procedure calls for which no summary was found *) ; isl_status: isl_status } +[@@deriving equal] val leq : lhs:t -> rhs:t -> bool @@ -189,7 +190,7 @@ val add_skipped_calls : SkippedCalls.t -> t -> t val set_path_condition : PathCondition.t -> t -> t (** private type to make sure {!summary_of_post} is always called when creating summaries *) -type summary = private t [@@deriving yojson_of] +type summary = private t [@@deriving compare, equal, yojson_of] val summary_of_post : Procdesc.t -> t -> summary SatUnsat.t (** trim the state down to just the procedure's interface (formals and globals), and simplify and diff --git a/infer/src/pulse/PulseBaseAddressAttributes.ml b/infer/src/pulse/PulseBaseAddressAttributes.ml index 1ac49170f..813af70c3 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.ml +++ b/infer/src/pulse/PulseBaseAddressAttributes.ml @@ -19,6 +19,10 @@ module Graph = PrettyPrintable.MakePPMonoMap (AbstractValue) (AttributesNoRank) type t = Graph.t +let compare = Graph.compare AttributesNoRank.compare + +let equal = Graph.equal AttributesNoRank.equal + let yojson_of_t = [%yojson_of: _] let add_one addr attribute attrs = diff --git a/infer/src/pulse/PulseBaseAddressAttributes.mli b/infer/src/pulse/PulseBaseAddressAttributes.mli index c09cfa5d6..cb042f08f 100644 --- a/infer/src/pulse/PulseBaseAddressAttributes.mli +++ b/infer/src/pulse/PulseBaseAddressAttributes.mli @@ -8,7 +8,7 @@ open! IStd module F = Format open PulseBasicInterface -type t [@@deriving yojson_of] +type t [@@deriving compare, equal, yojson_of] val empty : t diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml index 7a128620e..8e1ab533e 100644 --- a/infer/src/pulse/PulseBaseDomain.ml +++ b/infer/src/pulse/PulseBaseDomain.ml @@ -14,7 +14,8 @@ module AddressAttributes = PulseBaseAddressAttributes (* {2 Abstract domain description } *) -type t = {heap: Memory.t; stack: Stack.t; attrs: AddressAttributes.t} [@@deriving yojson_of] +type t = {heap: Memory.t; stack: Stack.t; attrs: AddressAttributes.t} +[@@deriving compare, equal, yojson_of] let empty = { heap= diff --git a/infer/src/pulse/PulseBaseDomain.mli b/infer/src/pulse/PulseBaseDomain.mli index 7c756ecbc..9a1585e80 100644 --- a/infer/src/pulse/PulseBaseDomain.mli +++ b/infer/src/pulse/PulseBaseDomain.mli @@ -10,7 +10,7 @@ open PulseBasicInterface module F = Format type t = {heap: PulseBaseMemory.t; stack: PulseBaseStack.t; attrs: PulseBaseAddressAttributes.t} -[@@deriving yojson_of] +[@@deriving compare, equal, yojson_of] type cell = PulseBaseMemory.Edges.t * Attributes.t diff --git a/infer/src/pulse/PulseBaseMemory.ml b/infer/src/pulse/PulseBaseMemory.ml index 13b82309b..a98a9a5a4 100644 --- a/infer/src/pulse/PulseBaseMemory.ml +++ b/infer/src/pulse/PulseBaseMemory.ml @@ -104,3 +104,7 @@ let canonicalize ~get_var_repr memory = include Graph + +let compare = Graph.compare Edges.compare + +let equal = Graph.equal Edges.equal diff --git a/infer/src/pulse/PulseBaseMemory.mli b/infer/src/pulse/PulseBaseMemory.mli index 9815b9b45..b6a95c602 100644 --- a/infer/src/pulse/PulseBaseMemory.mli +++ b/infer/src/pulse/PulseBaseMemory.mli @@ -24,6 +24,10 @@ module Edges : RecencyMap.S with type key = Access.t and type value = AddrTrace. include PrettyPrintable.PPMonoMap with type key = AbstractValue.t and type value = Edges.t +val compare : t -> t -> int + +val equal : t -> t -> bool + val register_address : AbstractValue.t -> t -> t val add_edge : AbstractValue.t -> Access.t -> AddrTrace.t -> t -> t diff --git a/infer/src/pulse/PulseBaseStack.ml b/infer/src/pulse/PulseBaseStack.ml index ac2215607..1067f67c6 100644 --- a/infer/src/pulse/PulseBaseStack.ml +++ b/infer/src/pulse/PulseBaseStack.ml @@ -19,7 +19,7 @@ module VarAddress = struct end module AddrHistPair = struct - type t = AbstractValue.t * ValueHistory.t [@@deriving compare, yojson_of] + type t = AbstractValue.t * ValueHistory.t [@@deriving compare, equal, yojson_of] let pp f addr_trace = if Config.debug_level_analysis >= 3 then @@ -50,6 +50,8 @@ include M let compare = M.compare AddrHistPair.compare +let equal = M.equal AddrHistPair.equal + let pp fmt m = let pp_item fmt (var_address, v) = F.fprintf fmt "%a=%a" VarAddress.pp var_address AddrHistPair.pp v diff --git a/infer/src/pulse/PulseBaseStack.mli b/infer/src/pulse/PulseBaseStack.mli index 58a0bfa2d..35f053249 100644 --- a/infer/src/pulse/PulseBaseStack.mli +++ b/infer/src/pulse/PulseBaseStack.mli @@ -15,6 +15,8 @@ include different type *) val compare : t -> t -> int [@@warning "-32"] +val equal : t -> t -> bool + val pp : F.formatter -> t -> unit val yojson_of_t : t -> Yojson.Safe.t diff --git a/infer/src/pulse/PulseCItv.ml b/infer/src/pulse/PulseCItv.ml index a61db360b..40b97da17 100644 --- a/infer/src/pulse/PulseCItv.ml +++ b/infer/src/pulse/PulseCItv.ml @@ -10,7 +10,7 @@ module F = Format module L = Logging module Bound = struct - type t = Int of IntLit.t | MinusInfinity | PlusInfinity [@@deriving compare] + type t = Int of IntLit.t | MinusInfinity | PlusInfinity [@@deriving compare, equal] let pp fmt = function | Int i -> @@ -112,7 +112,7 @@ module Unsafe : sig type t = private | Between of Bound.t * Bound.t (** we write \[b1,b2\] for these *) | Outside of IntLit.t * IntLit.t (** we write i1\]\[i2 for these *) - [@@deriving compare] + [@@deriving compare, equal] val between : Bound.t -> Bound.t -> t @@ -124,7 +124,8 @@ module Unsafe : sig val ge_to : IntLit.t -> t end = struct - type t = Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t [@@deriving compare] + type t = Between of Bound.t * Bound.t | Outside of IntLit.t * IntLit.t + [@@deriving compare, equal] let between b1 b2 = assert (Bound.is_interval b1 b2) ; diff --git a/infer/src/pulse/PulseCItv.mli b/infer/src/pulse/PulseCItv.mli index e74401aa1..a3452749b 100644 --- a/infer/src/pulse/PulseCItv.mli +++ b/infer/src/pulse/PulseCItv.mli @@ -9,7 +9,7 @@ module F = Format (** Concrete interval domain (CItv) *) -type t [@@deriving compare] +type t [@@deriving compare, equal] val equal_to : IntLit.t -> t diff --git a/infer/src/pulse/PulseDiagnostic.ml b/infer/src/pulse/PulseDiagnostic.ml index 4938ef5ca..e6467e2c4 100644 --- a/infer/src/pulse/PulseDiagnostic.ml +++ b/infer/src/pulse/PulseDiagnostic.ml @@ -17,10 +17,10 @@ type access_to_invalid_address = ; invalidation: Invalidation.t ; invalidation_trace: Trace.t ; access_trace: Trace.t } -[@@deriving equal] +[@@deriving compare, equal] type read_uninitialized_value = {calling_context: (CallEvent.t * Location.t) list; trace: Trace.t} -[@@deriving equal] +[@@deriving compare, equal] let yojson_of_access_to_invalid_address = [%yojson_of: _] diff --git a/infer/src/pulse/PulseDiagnostic.mli b/infer/src/pulse/PulseDiagnostic.mli index 710a8f652..98d5df530 100644 --- a/infer/src/pulse/PulseDiagnostic.mli +++ b/infer/src/pulse/PulseDiagnostic.mli @@ -22,7 +22,7 @@ type access_to_invalid_address = ; access_trace: Trace.t (** assuming we are in the calling context, the trace leads to an access to the value invalidated in [invalidation_trace] without further assumptions *) } -[@@deriving equal, yojson_of] +[@@deriving compare, equal, yojson_of] type read_uninitialized_value = { calling_context: (CallEvent.t * Location.t) list @@ -31,7 +31,7 @@ type read_uninitialized_value = ; trace: Trace.t (** assuming we are in the calling context, the trace leads to read of the uninitialized value *) } -[@@deriving equal, yojson_of] +[@@deriving compare, equal, yojson_of] (** an error to report to the user *) type t = diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 579da13ad..48cdb076c 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -22,7 +22,7 @@ type 'abductive_domain_t base_t = | AbortProgram of AbductiveDomain.summary | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t} | ISLLatentMemoryError of 'abductive_domain_t -[@@deriving yojson_of] +[@@deriving equal, compare, yojson_of] type t = AbductiveDomain.t base_t @@ -76,7 +76,7 @@ let get_astate : t -> AbductiveDomain.t = function let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_state).path_condition -type summary = AbductiveDomain.summary base_t [@@deriving yojson_of] +type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of] let summary_of_posts_common ~continue_program pdesc posts = List.filter_mapi posts ~f:(fun i exec_state -> diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli index 33ba700dc..a1080e536 100644 --- a/infer/src/pulse/PulseExecutionDomain.mli +++ b/infer/src/pulse/PulseExecutionDomain.mli @@ -32,7 +32,7 @@ val mk_initial : Procdesc.t -> t val is_unsat_cheap : t -> bool (** see {!PulsePathCondition.is_unsat_cheap} *) -type summary = AbductiveDomain.summary base_t [@@deriving yojson_of] +type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of] val summary_of_posts : Procdesc.t -> t list -> summary list diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 1d0b1d687..b32314118 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -48,7 +48,7 @@ end (** Linear Arithmetic *) module LinArith : sig (** linear combination of variables, eg [2·x + 3/4·y + 12] *) - type t [@@deriving compare, yojson_of] + type t [@@deriving compare, yojson_of, equal] type subst_target = QSubst of Q.t | VarSubst of Var.t | LinSubst of t @@ -239,7 +239,7 @@ module Term = struct | BitShiftLeft of t * t | BitShiftRight of t * t | BitXor of t * t - [@@deriving compare, yojson_of] + [@@deriving compare, equal, yojson_of] let equal_syntax = [%compare.equal: t] @@ -703,7 +703,7 @@ module Atom = struct | LessThan of Term.t * Term.t | Equal of Term.t * Term.t | NotEqual of Term.t * Term.t - [@@deriving compare, yojson_of] + [@@deriving compare, equal, yojson_of] let pp_with_pp_var pp_var fmt atom = (* add parens around terms that look like atoms to disambiguate *) @@ -973,7 +973,7 @@ type new_eqs = new_eq list module Formula = struct (* redefined for yojson output *) - type var_eqs = VarUF.t + type var_eqs = VarUF.t [@@deriving compare, equal] let yojson_of_var_eqs var_eqs = `List @@ -983,7 +983,7 @@ module Formula = struct :: jsons )) - type linear_eqs = LinArith.t Var.Map.t + type linear_eqs = LinArith.t Var.Map.t [@@deriving compare, equal] let yojson_of_linear_eqs linear_eqs = Var.Map.yojson_of_t LinArith.yojson_of_t linear_eqs @@ -992,7 +992,7 @@ module Formula = struct ; linear_eqs: linear_eqs (** equalities of the form [x = l] where [l] is from linear arithmetic *) ; atoms: Atom.Set.t (** not always normalized w.r.t. [var_eqs] and [linear_eqs] *) } - [@@deriving yojson_of] + [@@deriving compare, equal, yojson_of] let ttrue = {var_eqs= VarUF.empty; linear_eqs= Var.Map.empty; atoms= Atom.Set.empty} @@ -1275,6 +1275,13 @@ type t = ; both: Formula.t (** [both = known ∧ pruned], allows us to detect contradictions *) } [@@deriving yojson_of] +let compare phi1 phi2 = + if phys_equal phi1 phi2 then 0 + else [%compare: Atom.Set.t * Formula.t] (phi1.pruned, phi1.known) (phi2.pruned, phi2.known) + + +let equal = [%compare.equal: t] + let ttrue = {known= Formula.ttrue; pruned= Atom.Set.empty; both= Formula.ttrue} let pp_with_pp_var pp_var fmt {known; pruned; both} = diff --git a/infer/src/pulse/PulseFormula.mli b/infer/src/pulse/PulseFormula.mli index 46ac49503..f6d41a9b8 100644 --- a/infer/src/pulse/PulseFormula.mli +++ b/infer/src/pulse/PulseFormula.mli @@ -17,7 +17,7 @@ module Var = PulseAbstractValue Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable. *) -type t [@@deriving yojson_of] +type t [@@deriving compare, equal, yojson_of] val pp : F.formatter -> t -> unit diff --git a/infer/src/pulse/PulseLatentIssue.ml b/infer/src/pulse/PulseLatentIssue.ml index 1aa066228..1387a47c6 100644 --- a/infer/src/pulse/PulseLatentIssue.ml +++ b/infer/src/pulse/PulseLatentIssue.ml @@ -13,7 +13,7 @@ module Arithmetic = PulseArithmetic type t = | AccessToInvalidAddress of Diagnostic.access_to_invalid_address | ReadUninitializedValue of Diagnostic.read_uninitialized_value -[@@deriving equal, yojson_of] +[@@deriving compare, equal, yojson_of] let to_diagnostic = function | AccessToInvalidAddress access_to_invalid_address -> diff --git a/infer/src/pulse/PulseLatentIssue.mli b/infer/src/pulse/PulseLatentIssue.mli index 09469d118..c150a18e7 100644 --- a/infer/src/pulse/PulseLatentIssue.mli +++ b/infer/src/pulse/PulseLatentIssue.mli @@ -16,7 +16,7 @@ module AbductiveDomain = PulseAbductiveDomain type t = | AccessToInvalidAddress of Diagnostic.access_to_invalid_address | ReadUninitializedValue of Diagnostic.read_uninitialized_value -[@@deriving equal, yojson_of] +[@@deriving compare, equal, yojson_of] val to_diagnostic : t -> Diagnostic.t diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index a84c78d46..0f7052d68 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -36,6 +36,13 @@ type t = ; citvs: CItvs.t ; formula: Formula.t } +let compare phi1 phi2 = + if phys_equal phi1 phi2 || (phi1.is_unsat && phi2.is_unsat) then 0 + else [%compare: bool * Formula.t] (phi1.is_unsat, phi1.formula) (phi2.is_unsat, phi2.formula) + + +let equal = [%compare.equal: t] + let yojson_of_t {formula} = [%yojson_of: Formula.t] formula let pp fmt {is_unsat; bo_itvs; citvs; formula} = diff --git a/infer/src/pulse/PulsePathCondition.mli b/infer/src/pulse/PulsePathCondition.mli index f9b7a3d2f..1df80cf92 100644 --- a/infer/src/pulse/PulsePathCondition.mli +++ b/infer/src/pulse/PulsePathCondition.mli @@ -11,7 +11,7 @@ module AbstractValue = PulseAbstractValue module SatUnsat = PulseSatUnsat module ValueHistory = PulseValueHistory -type t [@@deriving yojson_of] +type t [@@deriving compare, equal, yojson_of] val true_ : t diff --git a/infer/src/pulse/PulseSkippedCalls.ml b/infer/src/pulse/PulseSkippedCalls.ml index 8c2d9c478..b581ce9ab 100644 --- a/infer/src/pulse/PulseSkippedCalls.ml +++ b/infer/src/pulse/PulseSkippedCalls.ml @@ -9,7 +9,7 @@ open! IStd module F = Format module SkippedTrace = struct - type t = PulseTrace.t [@@deriving compare] + type t = PulseTrace.t [@@deriving compare, equal] let pp fmt = PulseTrace.pp fmt ~pp_immediate:(fun fmt -> @@ -26,6 +26,10 @@ end module M = AbstractDomain.Map (Procname) (SkippedTrace) include M +let compare = M.compare SkippedTrace.compare + +let equal = M.equal SkippedTrace.equal + let yojson_of_t = [%yojson_of: _] (* ignore traces, just compare if the set of skipped procedures is the same *) diff --git a/infer/src/pulse/PulseSkippedCalls.mli b/infer/src/pulse/PulseSkippedCalls.mli index 6965cb80d..be257f67a 100644 --- a/infer/src/pulse/PulseSkippedCalls.mli +++ b/infer/src/pulse/PulseSkippedCalls.mli @@ -9,4 +9,8 @@ open! IStd include AbstractDomain.MapS with type key = Procname.t and type value = PulseTrace.t +val compare : t -> t -> int + +val equal : t -> t -> bool + val yojson_of_t : t -> Yojson.Safe.t diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 0878c3552..f4d9815f7 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -202,9 +202,11 @@ and simple_state = ; last_step: step option [@compare.ignore] (** for trace error reporting *) } [@@deriving compare] +let equal_simple_state = [%compare.equal: simple_state] + (* TODO: include a hash of the automaton in a summary to avoid caching problems. *) (* TODO: limit the number of simple_states to some configurable number (default ~5) *) -type state = simple_state list +type state = simple_state list [@@deriving compare, equal] let pp_mapping f (x, value) = Format.fprintf f "@[%s↦%a@]@," x AbstractValue.pp value diff --git a/infer/src/pulse/PulseTopl.mli b/infer/src/pulse/PulseTopl.mli index 13efd77c6..755563690 100644 --- a/infer/src/pulse/PulseTopl.mli +++ b/infer/src/pulse/PulseTopl.mli @@ -13,7 +13,7 @@ type event = | ArrayWrite of {aw_array: value; aw_index: value} | Call of {return: value option; arguments: value list; procname: Procname.t} -type state +type state [@@deriving compare, equal] val start : unit -> state (** Return the initial state of [Topl.automaton ()]. *)