[pulse] refactor of PrePost.t vs AbductiveDomain.t

Summary:
Be a bit more careful about the difference between PrePost.t and
AbductiveDomain.t. It's needed in another diff where the types will be
different.

Reviewed By: ezgicicek

Differential Revision: D20393927

fbshipit-source-id: beaf80c90

infer/src/checkers/impurity.ml

@@ -139,8 +139,8 @@ let is_modeled_pure tenv pname =
 (** Given Pulse summary, extract impurity info, i.e. parameters and global variables that are
     modified by the function and skipped functions. *)
 let extract_impurity tenv pdesc pre_post : ImpurityDomain.t =
-  let pre_heap = (AbductiveDomain.extract_pre pre_post).BaseDomain.heap in
-  let post = AbductiveDomain.extract_post pre_post in
+  let pre_heap = (AbductiveDomain.PrePost.get_pre pre_post).BaseDomain.heap in
+  let post = AbductiveDomain.PrePost.get_post pre_post in
   let post_stack = post.BaseDomain.stack in
   let pname = Procdesc.get_proc_name pdesc in
   let modified_params =
@@ -148,7 +148,7 @@ let extract_impurity tenv pdesc pre_post : ImpurityDomain.t =
   in
   let modified_globals = get_modified_globals pre_heap post post_stack in
   let skipped_calls =
-    AbductiveDomain.extract_skipped_calls pre_post
+    AbductiveDomain.PrePost.get_skipped_calls pre_post
     |> PulseAbductiveDomain.SkippedCalls.filter (fun proc_name _ ->
            Purity.should_report proc_name && not (is_modeled_pure tenv proc_name) )
   in

infer/src/pulse/PulseAbductiveDomain.ml

@@ -96,6 +96,12 @@ type t =
   ; pre: InvertedDomain.t  (** inferred pre at the current program point *)
   ; skipped_calls: SkippedCalls.t  (** set of skipped calls *) }
 
+let get_pre {pre} = (pre :> BaseDomain.t)
+
+let get_post {post} = (post :> BaseDomain.t)
+
+let get_skipped_calls {skipped_calls} = skipped_calls
+
 let pp f {post; pre} = F.fprintf f "@[<v>%a@;PRE=[%a]@]" Domain.pp post InvertedDomain.pp pre
 
 let leq ~lhs ~rhs =
@@ -414,7 +420,7 @@ module PrePost = struct
 
   (** stuff we carry around when computing the result of applying one pre/post pair *)
   type call_state =
-    { astate: t  (** caller's abstract state computed so far *)
+    { astate: domain_t  (** caller's abstract state computed so far *)
     ; subst: (AbstractValue.t * ValueHistory.t) AddressMap.t
           (** translation from callee addresses to caller addresses and their caller histories *)
     ; rev_subst: AbstractValue.t AddressMap.t
@@ -1077,10 +1083,11 @@ module PrePost = struct
             Ok None
         | Error _ as error ->
             error )
-end
 
-let extract_pre {pre} = (pre :> BaseDomain.t)
 
-let extract_post {post} = (post :> BaseDomain.t)
+  let get_pre {pre} = (pre :> BaseDomain.t)
+
+  let get_post {post} = (post :> BaseDomain.t)
 
-let extract_skipped_calls {skipped_calls} = skipped_calls
+  let get_skipped_calls {skipped_calls} = skipped_calls
+end

infer/src/pulse/PulseAbductiveDomain.mli

@@ -103,6 +103,18 @@ end
 
 module SkippedCalls : AbstractDomain.MapS with type key = Procname.t and type value = SkippedTrace.t
 
+val discard_unreachable : t -> t
+(** garbage collect unreachable addresses in the state to make it smaller, just for convenience and
+    keep its size down *)
+
+val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t
+
+val get_pre : t -> BaseDomain.t
+
+val get_post : t -> BaseDomain.t
+
+val get_skipped_calls : t -> SkippedCalls.t
+
 module PrePost : sig
   type domain_t = t
 
@@ -122,16 +134,10 @@ module PrePost : sig
     -> ((domain_t * (AbstractValue.t * ValueHistory.t) option) option, Diagnostic.t) result
   (** return the abstract state after the call along with an optional return value, or [None] if the
       precondition could not be satisfied (e.g. some aliasing constraints were not satisfied) *)
-end
-
-val discard_unreachable : t -> t
-(** garbage collect unreachable addresses in the state to make it smaller, just for convenience and
-    keep its size down *)
-
-val add_skipped_calls : Procname.t -> PulseTrace.t -> t -> t
 
-val extract_pre : PrePost.t -> BaseDomain.t
+  val get_pre : t -> BaseDomain.t
 
-val extract_post : PrePost.t -> BaseDomain.t
+  val get_post : t -> BaseDomain.t
 
-val extract_skipped_calls : PrePost.t -> SkippedCalls.t
+  val get_skipped_calls : t -> SkippedCalls.t
+end

infer/src/pulse/PulseSummary.ml

@@ -6,8 +6,9 @@
  *)
 open! IStd
 module F = Format
+open PulseDomainInterface
 
-type t = PulseAbductiveDomain.PrePost.t list
+type t = AbductiveDomain.PrePost.t list
 
 let of_posts pdesc posts = List.map posts ~f:(PulseAbductiveDomain.PrePost.of_post pdesc)