[AI] fix top interface

Reviewed By: jeremydubreil

Differential Revision: D13342552

fbshipit-source-id: 2839d62f9

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
 

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"]
+  (** top is maximum value *)
-  (** maximum value *)
+  include WithTop with type t := t
-
-  val is_top : t -> bool [@@warning "-32"]
-  (** return true if this is the maximum value *)
 
   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 *)
+  (** throws exception on empty/top *)
-
-  val empty : t
-
-  val is_empty : t -> bool
 end

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.
+          (** Conjunction of "formal index must be owned" predicates. true if empty *)
-                                         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
 

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
+    let current_value = try find lock_id map with Caml.Not_found -> LockStack.top in
-    if LockStack.is_empty current_value then map
+    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 =