[pulse] expose fewer details of internal modules of AbductiveDomain

Summary: Cleaner + makes it easier to change details of the implementation.

Reviewed By: da319

Differential Revision: D28125725

fbshipit-source-id: ac9258908

infer/src/pulse/PulseAbductiveDomain.ml

@@ -21,6 +21,11 @@ module type BaseDomainSig = sig
   (* private because the lattice is not the same for preconditions and postconditions so we don't
      want to confuse them *)
   type t = private BaseDomain.t [@@deriving compare, equal, yojson_of]
+end
+
+(* defined in two parts to avoid exporting internal APIs to the .mli *)
+module type BaseDomainSig_ = sig
+  include BaseDomainSig
 
   val empty : t
 
@@ -46,7 +51,7 @@ type base_domain = BaseDomain.t =
 
 (** represents the post abstract state at each program point *)
 module PostDomain : sig
-  include BaseDomainSig
+  include BaseDomainSig_
 
   val initialize : AbstractValue.t -> t -> t
 end = struct
@@ -87,7 +92,7 @@ end
 (* NOTE: [PreDomain] and [Domain] theoretically differ in that [PreDomain] should be the inverted lattice of [Domain], but since we never actually join states or check implication the two collapse into one. *)
 
 (** represents the inferred pre-condition at each program point, biabduction style *)
-module PreDomain : BaseDomainSig = PostDomain
+module PreDomain : BaseDomainSig_ = PostDomain
 
 (* see documentation in this file's .mli *)
 type t =

infer/src/pulse/PulseAbductiveDomain.mli

@@ -6,9 +6,7 @@
  *)
 
 open! IStd
-module F = Format
 open PulseBasicInterface
-module BaseAddressAttributes = PulseBaseAddressAttributes
 module BaseDomain = PulseBaseDomain
 module BaseMemory = PulseBaseMemory
 module BaseStack = PulseBaseStack
@@ -24,24 +22,6 @@ module type BaseDomainSig = sig
   (* private because the lattice is not the same for preconditions and postconditions so we don't
      want to confuse them *)
   type t = private BaseDomain.t [@@deriving compare, equal, yojson_of]
-
-  val yojson_of_t : t -> Yojson.Safe.t
-
-  val empty : t
-
-  val update : ?stack:BaseStack.t -> ?heap:BaseMemory.t -> ?attrs:BaseAddressAttributes.t -> t -> t
-
-  val filter_addr : f:(AbstractValue.t -> bool) -> t -> t
-  (** filter both heap and attrs *)
-
-  val filter_addr_with_discarded_addrs :
-    f:(AbstractValue.t -> bool) -> t -> t * AbstractValue.t list
-  (** compute new state containing only reachable addresses in its heap and attributes, as well as
-      the list of discarded unreachable addresses *)
-
-  val subst_var : AbstractValue.t * AbstractValue.t -> t -> t SatUnsat.t
-
-  val pp : F.formatter -> t -> unit
 end
 
 (** The post abstract state at each program point, or current state. *)