From cf6f107b88a0d723747314c5eedec49397d1839b Mon Sep 17 00:00:00 2001
From: Jules Villard <jul@fb.com>
Date: Mon, 21 Oct 2019 03:30:21 -0700
Subject: [PATCH] [pulse][11/9] carve out PulseBaseStack

Summary: To be consistent with PulseBaseMemomy, mostly.

Reviewed By: ezgicicek

Differential Revision: D17977208

fbshipit-source-id: 6a75c5b0e
---
 infer/src/pulse/PulseAbductiveDomain.ml  |  2 +-
 infer/src/pulse/PulseAbductiveDomain.mli | 11 ++++---
 infer/src/pulse/PulseBaseDomain.ml       | 37 +---------------------
 infer/src/pulse/PulseBaseDomain.mli      | 11 +------
 infer/src/pulse/PulseBaseStack.ml        | 39 ++++++++++++++++++++++++
 infer/src/pulse/PulseBaseStack.mli       | 18 +++++++++++
 infer/src/pulse/PulseDomainInterface.ml  |  2 +-
 7 files changed, 67 insertions(+), 53 deletions(-)
 create mode 100644 infer/src/pulse/PulseBaseStack.ml
 create mode 100644 infer/src/pulse/PulseBaseStack.mli

diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml
index d68781dec..2a0996ef5 100644
--- a/infer/src/pulse/PulseAbductiveDomain.ml
+++ b/infer/src/pulse/PulseAbductiveDomain.ml
@@ -9,7 +9,7 @@ module F = Format
 module L = Logging
 open PulseBasicInterface
 module BaseDomain = PulseBaseDomain
-module BaseStack = BaseDomain.Stack
+module BaseStack = PulseBaseStack
 module BaseMemory = PulseBaseMemory
 
 (** signature common to the "normal" [Domain], representing the post at the current program point,
diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli
index 2f6427849..ec74f9264 100644
--- a/infer/src/pulse/PulseAbductiveDomain.mli
+++ b/infer/src/pulse/PulseAbductiveDomain.mli
@@ -8,6 +8,7 @@ open! IStd
 open PulseBasicInterface
 module BaseDomain = PulseBaseDomain
 module BaseMemory = PulseBaseMemory
+module BaseStack = PulseBaseStack
 
 (* layer on top of {!BaseDomain} to propagate operations on the current state to the pre-condition
    when necessary
@@ -19,23 +20,23 @@ include AbstractDomain.NoJoin
 
 val mk_initial : Procdesc.t -> t
 
-(** stack operations like {!BaseDomain.Stack} but that also take care of propagating facts to the
+(** stack operations like {!BaseStack} but that also take care of propagating facts to the
     precondition *)
 module Stack : sig
-  val add : Var.t -> BaseDomain.Stack.value -> t -> t
+  val add : Var.t -> BaseStack.value -> t -> t
 
   val remove_vars : Var.t list -> t -> t
 
-  val fold : (Var.t -> BaseDomain.Stack.value -> 'a -> 'a) -> t -> 'a -> 'a
+  val fold : (Var.t -> BaseStack.value -> 'a -> 'a) -> t -> 'a -> 'a
 
-  val find_opt : Var.t -> t -> BaseDomain.Stack.value option
+  val find_opt : Var.t -> t -> BaseStack.value option
 
   val eval : ValueHistory.t -> Var.t -> t -> t * (AbstractValue.t * ValueHistory.t)
   (** return the value of the variable in the stack or create a fresh one if needed *)
 
   val mem : Var.t -> t -> bool
 
-  val exists : (Var.t -> BaseDomain.Stack.value -> bool) -> t -> bool
+  val exists : (Var.t -> BaseStack.value -> bool) -> t -> bool
 end
 
 (** memory operations like {!BaseMemory} but that also take care of propagating facts to the
diff --git a/infer/src/pulse/PulseBaseDomain.ml b/infer/src/pulse/PulseBaseDomain.ml
index 677d6cae7..92ae35dd2 100644
--- a/infer/src/pulse/PulseBaseDomain.ml
+++ b/infer/src/pulse/PulseBaseDomain.ml
@@ -9,45 +9,10 @@ module F = Format
 module L = Logging
 open PulseBasicInterface
 module Memory = PulseBaseMemory
+module Stack = PulseBaseStack
 
 (* {2 Abstract domain description } *)
 
-module AddrHistPair = struct
-  type t = AbstractValue.t * ValueHistory.t [@@deriving compare]
-
-  let pp f addr_trace =
-    if Config.debug_level_analysis >= 3 then
-      Pp.pair ~fst:AbstractValue.pp ~snd:ValueHistory.pp f addr_trace
-    else AbstractValue.pp f (fst addr_trace)
-end
-
-(** Stacks: map addresses of variables to values and initialisation location. *)
-module Stack = struct
-  module VarAddress = struct
-    include Var
-
-    let pp f var =
-      let pp_ampersand f = function
-        | ProgramVar _ ->
-            F.pp_print_string f "&"
-        | LogicalVar _ ->
-            ()
-      in
-      F.fprintf f "%a%a" pp_ampersand var Var.pp var
-  end
-
-  include PrettyPrintable.MakePPMonoMap (VarAddress) (AddrHistPair)
-
-  let pp fmt m =
-    let pp_item fmt (var_address, v) =
-      F.fprintf fmt "%a=%a" VarAddress.pp var_address AddrHistPair.pp v
-    in
-    PrettyPrintable.pp_collection ~pp_item fmt (bindings m)
-
-
-  let compare = compare AddrHistPair.compare
-end
-
 type t = {heap: Memory.t; stack: Stack.t}
 
 let empty =
diff --git a/infer/src/pulse/PulseBaseDomain.mli b/infer/src/pulse/PulseBaseDomain.mli
index 1a0d22982..0e5a19954 100644
--- a/infer/src/pulse/PulseBaseDomain.mli
+++ b/infer/src/pulse/PulseBaseDomain.mli
@@ -8,16 +8,7 @@
 open! IStd
 open PulseBasicInterface
 
-module Stack : sig
-  include
-    PrettyPrintable.MonoMap with type key = Var.t and type value = AbstractValue.t * ValueHistory.t
-
-  (* need to shadow the declaration in [MonoMap] even though it is unused since [MapS.compare] has a
-     different type *)
-  val compare : t -> t -> int [@@warning "-32"]
-end
-
-type t = {heap: PulseBaseMemory.t; stack: Stack.t}
+type t = {heap: PulseBaseMemory.t; stack: PulseBaseStack.t}
 
 val empty : t
 
diff --git a/infer/src/pulse/PulseBaseStack.ml b/infer/src/pulse/PulseBaseStack.ml
new file mode 100644
index 000000000..3148af67d
--- /dev/null
+++ b/infer/src/pulse/PulseBaseStack.ml
@@ -0,0 +1,39 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+open PulseBasicInterface
+
+(** Stacks: map addresses of variables to values and histoy. *)
+
+module VarAddress = struct
+  include Var
+
+  let pp f var =
+    let pp_ampersand f = function ProgramVar _ -> F.pp_print_string f "&" | LogicalVar _ -> () in
+    F.fprintf f "%a%a" pp_ampersand var Var.pp var
+end
+
+module AddrHistPair = struct
+  type t = AbstractValue.t * ValueHistory.t [@@deriving compare]
+
+  let pp f addr_trace =
+    if Config.debug_level_analysis >= 3 then
+      Pp.pair ~fst:AbstractValue.pp ~snd:ValueHistory.pp f addr_trace
+    else AbstractValue.pp f (fst addr_trace)
+end
+
+include PrettyPrintable.MakePPMonoMap (VarAddress) (AddrHistPair)
+
+let pp fmt m =
+  let pp_item fmt (var_address, v) =
+    F.fprintf fmt "%a=%a" VarAddress.pp var_address AddrHistPair.pp v
+  in
+  PrettyPrintable.pp_collection ~pp_item fmt (bindings m)
+
+
+let compare = compare AddrHistPair.compare
diff --git a/infer/src/pulse/PulseBaseStack.mli b/infer/src/pulse/PulseBaseStack.mli
new file mode 100644
index 000000000..46fb36dd6
--- /dev/null
+++ b/infer/src/pulse/PulseBaseStack.mli
@@ -0,0 +1,18 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+open! IStd
+module F = Format
+open PulseBasicInterface
+
+include
+  PrettyPrintable.MonoMap with type key = Var.t and type value = AbstractValue.t * ValueHistory.t
+
+(* need to shadow the declaration in [MonoMap] even though it is unused since [MapS.compare] has a
+     different type *)
+val compare : t -> t -> int [@@warning "-32"]
+
+val pp : F.formatter -> t -> unit
diff --git a/infer/src/pulse/PulseDomainInterface.ml b/infer/src/pulse/PulseDomainInterface.ml
index df7ce774a..faca03e80 100644
--- a/infer/src/pulse/PulseDomainInterface.ml
+++ b/infer/src/pulse/PulseDomainInterface.ml
@@ -15,5 +15,5 @@ module Memory = AbductiveDomain.Memory
 (** use only if you know what you are doing or you risk break bi-abduction *)
 module BaseDomain = PulseBaseDomain
 
-module BaseStack = BaseDomain.Stack
+module BaseStack = PulseBaseStack
 module BaseMemory = PulseBaseMemory