From 16cae31f200549eb39f58c6eff796511214f196b Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Wed, 14 Dec 2016 09:57:17 -0800
Subject: [PATCH] [absint] add inverted set domain

Reviewed By: jberdine

Differential Revision: D4320020

fbshipit-source-id: f2810ae
---
 infer/src/checkers/AbstractDomain.mli | 10 ++++++++--
 infer/src/checkers/abstractDomain.ml  | 20 ++++++++++++++++++++
 2 files changed, 28 insertions(+), 2 deletions(-)

diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli
index 7ee60f089..c26f5b754 100644
--- a/infer/src/checkers/AbstractDomain.mli
+++ b/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
-    possible values, since the widening operator here is just union. *)
+(** Lift a set to a powerset domain ordered by subset. The elements of the set should be drawn from
+    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
diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml
index bbc1bb043..50733b6a6 100644
--- a/infer/src/checkers/abstractDomain.ml
+++ b/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