From 9bf318fd4dbcc52215af0992af0abaf2650f895b Mon Sep 17 00:00:00 2001
From: Sam Blackshear <shb@fb.com>
Date: Wed, 26 Oct 2016 07:15:48 -0700
Subject: [PATCH] [checkers] mlis for abstract domains

Reviewed By: jvillard, jberdine

Differential Revision: D4078302

fbshipit-source-id: 3b5f961
---
 infer/src/checkers/AbstractDomain.mli | 49 +++++++++++++++++++++++++++
 infer/src/checkers/abstractDomain.ml  |  5 ---
 2 files changed, 49 insertions(+), 5 deletions(-)
 create mode 100644 infer/src/checkers/AbstractDomain.mli

diff --git a/infer/src/checkers/AbstractDomain.mli b/infer/src/checkers/AbstractDomain.mli
new file mode 100644
index 000000000..b7e8bc2a8
--- /dev/null
+++ b/infer/src/checkers/AbstractDomain.mli
@@ -0,0 +1,49 @@
+(*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! Utils
+
+module F = Format
+
+(** Abstract domains and domain combinators *)
+
+module type S = sig
+  type astate
+
+  val initial : astate
+  val (<=) : lhs:astate -> rhs:astate -> bool (* fst \sqsubseteq snd? *)
+  val join : astate -> astate -> astate
+  val widen : prev:astate -> next:astate -> num_iters:int -> astate
+  val pp : F.formatter -> astate -> unit
+end
+
+(** Lift a pre-domain to a domain *)
+module BottomLifted (Domain : S) : sig
+  type astate =
+    | Bottom
+    | NonBottom of Domain.astate
+
+  include S with type astate := astate
+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. *)
+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 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
+  include S with type astate = ValueDomain.astate Map.t
+end
diff --git a/infer/src/checkers/abstractDomain.ml b/infer/src/checkers/abstractDomain.ml
index 39c0db90c..f20412420 100644
--- a/infer/src/checkers/abstractDomain.ml
+++ b/infer/src/checkers/abstractDomain.ml
@@ -21,7 +21,6 @@ module type S = sig
   val pp : F.formatter -> astate -> unit
 end
 
-(** Lift a domain without bottom to a domain with bottom. *)
 module BottomLifted (Domain : S) = struct
   type astate =
     | Bottom
@@ -61,7 +60,6 @@ module BottomLifted (Domain : S) = struct
     | NonBottom astate -> Domain.pp fmt astate
 end
 
-(** Cartestian product of two domains. *)
 module Pair (Domain1 : S) (Domain2 : S) = struct
   type astate = Domain1.astate * Domain2.astate
 
@@ -89,8 +87,6 @@ module Pair (Domain1 : S) (Domain2 : S) = struct
     F.fprintf fmt "(%a, %a)" Domain1.pp astate1 Domain2.pp astate2
 end
 
-(** 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. *)
 module FiniteSet (S : PrettyPrintable.PPSet) = struct
   include S
   type astate = t
@@ -111,7 +107,6 @@ module FiniteSet (S : PrettyPrintable.PPSet) = struct
     join prev next
 end
 
-(** Lift a map whose value type is an abstract domain to a domain. *)
 module Map (M : PrettyPrintable.PPMap) (ValueDomain : S) = struct
   include M
   type astate = ValueDomain.astate M.t