[absint] add inverted set domain

Reviewed By: jberdine

Differential Revision: D4320020

fbshipit-source-id: f2810ae

infer/src/checkers/AbstractDomain.mli

@@ -35,13 +35,19 @@ end
 (** Cartesian product of two domains. *)
 module Pair (Domain1 : S) (Domain2 : S) : S with type astate = Domain1.astate * Domain2.astate
 
-(** Lift a set to a domain. The elements of the set should be drawn from a *finite* collection of
+(** Lift a set to a powerset domain ordered by subset. The elements of the set should be drawn from
-    possible values, since the widening operator here is just union. *)
+    a *finite* collection of possible values, since the widening operator here is just union. *)
 module FiniteSet (Set : PrettyPrintable.PPSet) : sig
   include PrettyPrintable.PPSet with type t = Set.t and type elt = Set.elt
   include S with type astate = t
 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
+  include S with type astate = t
+end
+
 (** Lift a map whose value type is an abstract domain to a domain. *)
 module Map (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig
   include PrettyPrintable.PPMap with type 'a t = 'a Map.t and type key = Map.key

infer/src/checkers/abstractDomain.ml

@@ -107,6 +107,26 @@ module FiniteSet (S : PrettyPrintable.PPSet) = struct
     join prev next
 end
 
+module InvertedSet (S : PrettyPrintable.PPSet) = struct
+  include S
+  type astate = t
+
+  let initial = 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
+
+  let widen ~prev ~next ~num_iters:_ =
+    join prev next
+end
+
 module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
   include M
   type astate = ValueDomain.astate M.t