From a3cffa7116fa7861e08e760fca688f1516c3381b Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Wed, 8 Feb 2017 08:31:35 -0800
Subject: [PATCH] [absint] add inverted map domain

Reviewed By: jberdine

Differential Revision: D4523126

fbshipit-source-id: dee2894
---
 infer/src/checkers/AbstractDomain.ml  | 44 +++++++++++++++++++++++++--
 infer/src/checkers/AbstractDomain.mli | 12 +++++++-
 2 files changed, 53 insertions(+), 3 deletions(-)

diff --git a/infer/src/checkers/AbstractDomain.ml b/infer/src/checkers/AbstractDomain.ml
index e46f429cc..6e6ee40ec 100644
--- a/infer/src/checkers/AbstractDomain.ml
+++ b/infer/src/checkers/AbstractDomain.ml
@@ -162,13 +162,53 @@ module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
            | Some v1, Some v2 -> Some (ValueDomain.widen ~prev:v1 ~next:v2 ~num_iters)
            | Some v, _ | _, Some v -> Some v
            | None, None -> None)
-      prev
-      next
+        prev
+        next
 
   let pp fmt astate =
     M.pp ~pp_value:ValueDomain.pp fmt astate
 end
 
+module InvertedMap (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
+  include M
+  type astate = ValueDomain.astate M.t
+
+  let (<=) ~lhs ~rhs =
+    if phys_equal lhs rhs
+    then true
+    else
+      try M.for_all (fun k rhs_v -> ValueDomain.(<=) ~lhs:(M.find k lhs) ~rhs:rhs_v) rhs
+      with Not_found -> false
+
+  let join astate1 astate2 =
+    if phys_equal astate1 astate2
+    then astate1
+    else
+      M.merge
+        (fun _ v1_opt v2_opt -> match v1_opt, v2_opt with
+           | Some v1, Some v2 -> Some (ValueDomain.join v1 v2)
+           | _ -> None)
+        astate1
+        astate2
+
+  let widen ~prev ~next ~num_iters =
+    if phys_equal prev next
+    then prev
+    else
+      M.merge
+        (fun _ v1_opt v2_opt -> match v1_opt, v2_opt with
+           | Some v1, Some v2 -> Some (ValueDomain.widen ~prev:v1 ~next:v2 ~num_iters)
+           | _ -> None)
+        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
   type astate = bool
 
diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli
index 281368a99..77113b3e8 100644
--- a/infer/src/checkers/AbstractDomain.mli
+++ b/infer/src/checkers/AbstractDomain.mli
@@ -59,12 +59,22 @@ module InvertedSet (Set : PrettyPrintable.PPSet) : sig
   include S with type astate = t
 end
 
-(** Lift a map whose value type is an abstract domain to a domain. *)
+(** Map domain ordered by union over the set of bindings, so the bottom element is the empty map.
+    Every element implicitly maps to bottom unless it is explicitly bound to something else *)
 module Map (Map : PrettyPrintable.PPMap) (ValueDomain : S) : sig
   include PrettyPrintable.PPMap with type 'a t = 'a Map.t and type key = Map.key
   include WithBottom with type astate = ValueDomain.astate Map.t
 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
+
+  val empty : [`This_domain_is_not_pointed] (** this domain doesn't have a natural bottom element *)
+end
+
 (** Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's
     true in both branches. *)
 module BooleanAnd : S with type astate = bool