[absint] make InvertedSet/InvertedMap functors consistent non-inverted versions

Reviewed By: mbouaziz

Differential Revision: D5879318

fbshipit-source-id: 278e5ad

infer/src/absint/AbstractDomain.ml

@@ -151,8 +151,8 @@ module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) = struct
   let widen ~prev ~next ~num_iters:_ = join prev next
 end
 
-module InvertedSet (S : PrettyPrintable.PPSet) = struct
-  include S
+module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) = struct
+  include PrettyPrintable.MakePPSet (Element)
 
   type astate = t
 
@@ -210,7 +210,8 @@ module Map (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = stru
   let pp fmt astate = M.pp ~pp_value:ValueDomain.pp fmt astate
 end
 
-module InvertedMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
+module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) = struct
+  module M = PrettyPrintable.MakePPMap (Key)
   include M
 
   type astate = ValueDomain.astate M.t
@@ -246,9 +247,6 @@ module InvertedMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
         prev next
 
   let pp fmt astate = M.pp ~pp_value:ValueDomain.pp fmt astate
-
-  (* hide empty so we don't accidentally satisfy the WithBottom signature *)
-  let empty = `This_domain_is_not_pointed
 end
 
 module BooleanAnd = struct

infer/src/absint/AbstractDomain.mli

@@ -71,8 +71,8 @@ module FiniteSet (Element : PrettyPrintable.PrintableOrderedType) : sig
 end
 
 (** Lift a set to a powerset domain ordered by superset, so the join operator is intersection *)
-module InvertedSet (Set : PrettyPrintable.PPSet) : sig
-  include PrettyPrintable.PPSet with type t = Set.t and type elt = Set.elt
+module InvertedSet (Element : PrettyPrintable.PrintableOrderedType) : sig
+  include module type of PrettyPrintable.MakePPSet (Element)
 
   include S with type astate = t
 end
@@ -87,13 +87,10 @@ end
 
 (** Map domain ordered by intersection over the set of bindings, so the top element is the empty
     map. Every element implictly maps to top unless it is explicitly bound to something else *)
-module InvertedMap (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig
-  include PrettyPrintable.PPMap with type 'a t = 'a Map.t and type key = Map.key
-
-  include S with type astate = ValueDomain.astate Map.t
+module InvertedMap (Key : PrettyPrintable.PrintableOrderedType) (ValueDomain : S) : sig
+  include module type of PrettyPrintable.MakePPMap (Key)
 
-  val empty : [`This_domain_is_not_pointed]
-  (** this domain doesn't have a natural bottom element *)
+  include S with type astate = ValueDomain.astate t
 end
 
 (** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's

infer/src/checkers/ThreadSafetyDomain.ml

@@ -194,7 +194,7 @@ module Attribute = struct
   end)
 end
 
-module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute.Set)
+module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute)
 
 module OwnershipAbstractValue = struct
   type astate = Owned | OwnedIf of IntSet.t | Unowned [@@deriving compare]
@@ -257,7 +257,7 @@ module OwnershipDomain = struct
 end
 
 module AttributeMapDomain = struct
-  include AbstractDomain.InvertedMap (AccessPath.Map) (AttributeSetDomain)
+  include AbstractDomain.InvertedMap (AccessPath) (AttributeSetDomain)
 
   let add access_path attribute_set t =
     if AttributeSetDomain.is_empty attribute_set then t else add access_path attribute_set t
@@ -377,7 +377,7 @@ let empty =
   let locks = false in
   let accesses = AccessDomain.empty in
   let ownership = OwnershipDomain.empty in
-  let attribute_map = AccessPath.Map.empty in
+  let attribute_map = AttributeMapDomain.empty in
   let escapees = EscapeeDomain.empty in
   {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees}
 

infer/src/checkers/ThreadSafetyDomain.mli

@@ -108,10 +108,10 @@ module Attribute : sig
   module Set : PrettyPrintable.PPSet with type elt = t
 end
 
-module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute.Set)
+module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute)
 
 module AttributeMapDomain : sig
-  include module type of AbstractDomain.InvertedMap (AccessPath.Map) (AttributeSetDomain)
+  include module type of AbstractDomain.InvertedMap (AccessPath) (AttributeSetDomain)
 
   val add : AccessPath.t -> AttributeSetDomain.astate -> astate -> astate