From abee2a5cb05f3b6f6b66cf3e6647b6363283bd2f Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Wed, 5 Dec 2018 23:42:36 -0800 Subject: [PATCH] [AI] fix top interface Reviewed By: jeremydubreil Differential Revision: D13342552 fbshipit-source-id: 2839d62f9 --- infer/src/absint/AbstractDomain.ml | 22 ++++++++++++++++++---- infer/src/absint/AbstractDomain.mli | 21 ++++++++------------- infer/src/concurrency/RacerDDomain.mli | 13 +++++++------ infer/src/concurrency/starvationDomain.ml | 10 +++++----- 4 files changed, 38 insertions(+), 28 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index f040995e9..8e54603ed 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -52,6 +52,8 @@ module type WithTop = sig include S val top : t + + val is_top : t -> bool end module BottomLifted (Domain : S) = struct @@ -109,6 +111,8 @@ module TopLifted (Domain : S) = struct let top = Top + let is_top = function Top -> true | _ -> false + let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else @@ -181,6 +185,8 @@ module Flat (V : PrettyPrintable.PrintableEquatableType) = struct let top = Top + let is_top = function Top -> true | _ -> false + let ( <= ) ~lhs ~rhs = phys_equal lhs rhs || @@ -241,12 +247,16 @@ module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) = module type InvertedSetS = sig include PrettyPrintable.PPSet - include S with type t := t + include WithTop with type t := t end module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) = struct include PrettyPrintable.MakePPSet (Element) + let top = empty + + let is_top = is_empty + let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else subset rhs lhs let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else inter astate1 astate2 @@ -318,12 +328,16 @@ end module type InvertedMapS = sig include PrettyPrintable.PPMonoMap - include S with type t := t + include WithTop with type t := t end module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = struct include PrettyPrintable.MakePPMonoMap (Key) (ValueDomain) + let top = empty + + let is_top = is_empty + let ( <= ) ~lhs ~rhs = if phys_equal lhs rhs then true else @@ -425,9 +439,9 @@ module StackDomain (Element : PrettyPrintable.PrintableOrderedType) = struct let pop = List.tl_exn - let is_empty = List.is_empty + let is_top = List.is_empty - let empty = [] + let top = [] let pp fmt x = Pp.semicolon_seq Element.pp fmt x diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index c68d58e62..4409282d2 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -59,6 +59,8 @@ module type WithTop = sig include S val top : t + + val is_top : t -> bool end (** Lift a pre-domain to a domain *) @@ -106,7 +108,7 @@ module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) : module type InvertedSetS = sig include PrettyPrintable.PPSet - include S with type t := t + include WithTop with type t := t end (** Lift a set to a powerset domain ordered by superset, so the join operator is intersection *) @@ -133,7 +135,7 @@ module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) : module type InvertedMapS = sig include PrettyPrintable.PPMonoMap - include S with type t := t + include WithTop with type t := t end (** Map domain ordered by intersection over the set of bindings, so the top element is the empty @@ -166,11 +168,8 @@ end module CountDomain (MaxCount : MaxCount) : sig include WithBottom with type t = private int - val top : t [@@warning "-32"] - (** maximum value *) - - val is_top : t -> bool [@@warning "-32"] - (** return true if this is the maximum value *) + (** top is maximum value *) + include WithTop with type t := t val increment : t -> t (** bump the count by one if it is less than the max *) @@ -187,14 +186,10 @@ end longest common prefix (so [c;b;a] join [f;g;b;c;a] = [a]), so the top element is the empty stack. *) module StackDomain (Element : PrettyPrintable.PrintableOrderedType) : sig - include S with type t = Element.t list + include WithTop with type t = Element.t list val push : Element.t -> t -> t val pop : t -> t - (** throws exception on empty *) - - val empty : t - - val is_empty : t -> bool + (** throws exception on empty/top *) end diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index cc4c9f48b..a8c5a3389 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -101,8 +101,7 @@ module AccessSnapshot : sig module OwnershipPrecondition : sig type t = | Conjunction of IntSet.t - (** Conjunction of "formal index must be owned" predicates. - true if empty *) + (** Conjunction of "formal index must be owned" predicates. true if empty *) | False include PrettyPrintable.PrintableOrderedType with type t := t @@ -135,7 +134,7 @@ end (** map of access metadata |-> set of accesses. the map should hold all accesses to a possibly-unowned access path *) -module AccessDomain : module type of AbstractDomain.FiniteSet (AccessSnapshot) +module AccessDomain : AbstractDomain.FiniteSetS with type elt = AccessSnapshot.t (** Powerset domain on the formal indexes in OwnedIf with a distinguished bottom element (Owned) and top element (Unowned) *) @@ -156,7 +155,8 @@ module OwnershipAbstractValue : sig end module OwnershipDomain : sig - include module type of AbstractDomain.Map (AccessPath) (OwnershipAbstractValue) + include + AbstractDomain.MapS with type key = AccessPath.t with type value = OwnershipAbstractValue.t val get_owned : AccessPath.t -> t -> OwnershipAbstractValue.t @@ -186,10 +186,11 @@ module Attribute : sig include PrettyPrintable.PrintableOrderedType with type t := t end -module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute) +module AttributeSetDomain : AbstractDomain.InvertedSetS with type elt = Attribute.t module AttributeMapDomain : sig - include module type of AbstractDomain.InvertedMap (AccessPath) (AttributeSetDomain) + include + AbstractDomain.InvertedMapS with type key = AccessPath.t with type value = AttributeSetDomain.t val add : AccessPath.t -> AttributeSetDomain.t -> t -> t diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index a0d771c4e..74e31336e 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -141,23 +141,23 @@ module LockState = struct let is_taken lock_event map = match lock_event.Event.elem with | Event.LockAcquire lock -> ( - try not (find lock map |> LockStack.is_empty) with Caml.Not_found -> false ) + try not (find lock map |> LockStack.is_top) with Caml.Not_found -> false ) | _ -> false let acquire lock_id lock_event map = - let current_value = try find lock_id map with Caml.Not_found -> LockStack.empty in + let current_value = try find lock_id map with Caml.Not_found -> LockStack.top in let new_value = LockStack.push lock_event current_value in add lock_id new_value map let release lock_id map = - let current_value = try find lock_id map with Caml.Not_found -> LockStack.empty in - if LockStack.is_empty current_value then map + let current_value = try find lock_id map with Caml.Not_found -> LockStack.top in + if LockStack.is_top current_value then map else let new_value = LockStack.pop current_value in - if LockStack.is_empty new_value then remove lock_id map else add lock_id new_value map + if LockStack.is_top new_value then remove lock_id map else add lock_id new_value map let fold_over_events f map init =