From 5b495c6a386186f4da202cfa9d8f38c63e63e14b Mon Sep 17 00:00:00 2001
From: Jeremy Dubreil <jrm@fb.com>
Date: Wed, 17 May 2017 15:28:46 -0700
Subject: [PATCH] [infer][absint] Functor to create a domain with Top

Reviewed By: sblackshear

Differential Revision: D5081605

fbshipit-source-id: 07d19ed
---
 infer/src/checkers/AbstractDomain.ml  | 46 +++++++++++++++++++++++++++
 infer/src/checkers/AbstractDomain.mli | 21 +++++++++++-
 2 files changed, 66 insertions(+), 1 deletion(-)

diff --git a/infer/src/checkers/AbstractDomain.ml b/infer/src/checkers/AbstractDomain.ml
index 077867c76..044203bb4 100644
--- a/infer/src/checkers/AbstractDomain.ml
+++ b/infer/src/checkers/AbstractDomain.ml
@@ -26,6 +26,12 @@ module type WithBottom = sig
   val empty : astate
 end
 
+module type WithTop = sig
+  include S
+
+  val top : astate
+end
+
 module BottomLifted (Domain : S) = struct
   type astate =
     | Bottom
@@ -65,6 +71,46 @@ module BottomLifted (Domain : S) = struct
     | NonBottom astate -> Domain.pp fmt astate
 end
 
+module TopLifted (Domain: S) = struct
+  type astate =
+    | Top
+    | NonTop of Domain.astate
+
+  let top = Top
+
+  let (<=) ~lhs ~rhs =
+    if phys_equal lhs rhs
+    then true
+    else
+      match lhs, rhs with
+      | _, Top -> true
+      | Top, _ -> false
+      | NonTop lhs, NonTop rhs -> Domain.(<=) ~lhs ~rhs
+
+  let join astate1 astate2 =
+    if phys_equal astate1 astate2
+    then astate1
+    else
+      match astate1, astate2 with
+      | Top, _
+      | _, Top -> Top
+      | NonTop a1, NonTop a2 -> NonTop (Domain.join a1 a2)
+
+  let widen ~prev ~next ~num_iters =
+    if phys_equal prev next
+    then prev
+    else
+      match prev, next with
+      | Top, _
+      | _, Top -> Top
+      | NonTop prev, NonTop next -> NonTop (Domain.widen ~prev ~next ~num_iters)
+
+  let pp fmt = function
+    | Top -> F.fprintf fmt "T"
+    | NonTop astate -> Domain.pp fmt astate
+
+end
+
 module Pair (Domain1 : S) (Domain2 : S) = struct
   type astate = Domain1.astate * Domain2.astate
 
diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli
index 9c5dbbb50..041b9755d 100644
--- a/infer/src/checkers/AbstractDomain.mli
+++ b/infer/src/checkers/AbstractDomain.mli
@@ -30,10 +30,19 @@ end
 module type WithBottom = sig
   include S
 
-  (** The bottom value of the domain. *)
+  (** The bottom value of the domain.
+      Naming it empty instead of bottom helps to bind the empty
+      value for sets and maps to the natural definition for bottom *)
   val empty : astate
 end
 
+(** A domain with an explicit top value *)
+module type WithTop = sig
+  include S
+
+  val top : astate
+end
+
 (** Lift a pre-domain to a domain *)
 module BottomLifted (Domain : S) : sig
   type astate =
@@ -43,6 +52,16 @@ module BottomLifted (Domain : S) : sig
   include WithBottom with type astate := astate
 end
 
+(** Create a domain with Top element from a pre-domain *)
+module TopLifted (Domain : S) : sig
+  type astate =
+    | Top
+    | NonTop of Domain.astate
+
+  include WithTop with type astate := astate
+end
+
+
 (** Cartesian product of two domains. *)
 module Pair (Domain1 : S) (Domain2 : S) : S with type astate = Domain1.astate * Domain2.astate