[pulse][8/9] Domain interface

Summary:
Another poorman's library, this time about Pulse Domains. Also renames
`PulseDomain` to `PulseBaseDomain`.

Reviewed By: ezgicicek

Differential Revision: D17955287

fbshipit-source-id: 9c947cf98

infer/src/checkers/impurity.ml

@@ -7,8 +7,8 @@
 open! IStd
 module F = Format
 module L = Logging
-module BaseStack = PulseDomain.Stack
 open PulseBasicInterface
+open PulseDomainInterface
 
 let debug fmt = L.(debug Analysis Verbose fmt)
 
@@ -22,8 +22,8 @@ let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractValue.t list opt
         if AbstractValue.equal addr_dest_pre addr_dest_post then
           Option.map acc ~f:(fun acc -> addr_dest_pre :: acc)
         else None )
-      (PulseDomain.Memory.Edges.bindings edges_pre)
-      (PulseDomain.Memory.Edges.bindings edges_post)
+      (BaseMemory.Edges.bindings edges_pre)
+      (BaseMemory.Edges.bindings edges_post)
   with
   | Unequal_lengths ->
       debug "Mismatch in pre and post.\n" ;
@@ -52,9 +52,9 @@ let add_invalid_and_modified ~check_empty attrs acc =
 
   TODO: keep track of impure library calls *)
 let extract_impurity pdesc pre_post : ImpurityDomain.t =
-  let pre_heap = (PulseAbductiveDomain.extract_pre pre_post).PulseDomain.heap in
-  let post_heap = (PulseAbductiveDomain.extract_post pre_post).PulseDomain.heap in
-  let post_stack = (PulseAbductiveDomain.extract_post pre_post).PulseDomain.stack in
+  let pre_heap = (AbductiveDomain.extract_pre pre_post).BaseDomain.heap in
+  let post_heap = (AbductiveDomain.extract_post pre_post).BaseDomain.heap in
+  let post_stack = (AbductiveDomain.extract_post pre_post).BaseDomain.stack in
   let add_to_modified var addr acc =
     let rec aux acc ~addr_to_explore ~visited : ImpurityDomain.trace list =
       match addr_to_explore with
@@ -63,8 +63,8 @@ let extract_impurity pdesc pre_post : ImpurityDomain.t =
       | addr :: addr_to_explore -> (
           if AbstractValue.Set.mem addr visited then aux acc ~addr_to_explore ~visited
           else
-            let cell_pre_opt = PulseDomain.Memory.find_opt addr pre_heap in
-            let cell_post_opt = PulseDomain.Memory.find_opt addr post_heap in
+            let cell_pre_opt = BaseMemory.find_opt addr pre_heap in
+            let cell_post_opt = BaseMemory.find_opt addr post_heap in
             let visited = AbstractValue.Set.add addr visited in
             match (cell_pre_opt, cell_post_opt) with
             | None, None ->

infer/src/pulse/Pulse.ml

@@ -10,17 +10,6 @@ module L = Logging
 open Result.Monad_infix
 open PulseBasicInterface
 
-include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
-  struct
-  [@@@warning "-60"]
-
-  (** Do not use {!PulseDomain} directly as it could result in bypassing abduction mechanisms in
-     {!PulseOperations} and {!PulseAbductiveDomain} that take care of propagating facts to the
-     precondition. *)
-  module PulseDomain = struct end
-  [@@deprecated "Use PulseAbductiveDomain or PulseOperations instead."]
-end
-
 let report summary diagnostic =
   let open PulseDiagnostic in
   Reporting.log_error summary ~loc:(get_location diagnostic) ~ltr:(get_trace diagnostic)

infer/src/pulse/PulseAbductiveDomain.ml

@@ -7,8 +7,9 @@
 open! IStd
 module F = Format
 module L = Logging
-module BaseStack = PulseDomain.Stack
-module BaseMemory = PulseDomain.Memory
+module BaseDomain = PulseBaseDomain
+module BaseStack = BaseDomain.Stack
+module BaseMemory = BaseDomain.Memory
 open PulseBasicInterface
 
 (** signature common to the "normal" [Domain], representing the post at the current program point,
@@ -16,7 +17,7 @@ open PulseBasicInterface
 module type BaseDomain = sig
   (* private because the lattice is not the same for preconditions and postconditions so we don't
      want to confuse them *)
-  type t = private PulseDomain.t
+  type t = private BaseDomain.t
 
   val empty : t
 
@@ -28,8 +29,8 @@ module type BaseDomain = sig
 end
 
 (* just to expose the [heap] and [stack] record field names without having to type
-   [PulseDomain.heap] *)
-type base_domain = PulseDomain.t = {heap: BaseMemory.t; stack: BaseStack.t}
+   [BaseDomain.heap] *)
+type base_domain = BaseDomain.t = {heap: BaseMemory.t; stack: BaseStack.t}
 
 (** operations common to [Domain] and [InvertedDomain], see also the [BaseDomain] signature *)
 module BaseDomainCommon = struct
@@ -46,21 +47,21 @@ end
 (** represents the post abstract state at each program point *)
 module Domain : BaseDomain = struct
   include BaseDomainCommon
-  include PulseDomain
+  include BaseDomain
 end
 
 (** represents the inferred pre-condition at each program point, biabduction style *)
 module InvertedDomain : BaseDomain = struct
   include BaseDomainCommon
 
-  type t = PulseDomain.t
+  type t = BaseDomain.t
 
-  let empty = PulseDomain.empty
+  let empty = BaseDomain.empty
 
-  let pp = PulseDomain.pp
+  let pp = BaseDomain.pp
 
   (** inverted lattice *)
-  let ( <= ) ~lhs ~rhs = PulseDomain.( <= ) ~rhs:lhs ~lhs:rhs
+  let ( <= ) ~lhs ~rhs = BaseDomain.( <= ) ~rhs:lhs ~lhs:rhs
 end
 
 (** biabduction-style pre/post state *)
@@ -72,16 +73,16 @@ let pp f {post; pre} = F.fprintf f "@[<v>%a@;PRE=[%a]@]" Domain.pp post Inverted
 
 let ( <= ) ~lhs ~rhs =
   match
-    PulseDomain.isograph_map PulseDomain.empty_mapping
-      ~lhs:(rhs.pre :> PulseDomain.t)
-      ~rhs:(lhs.pre :> PulseDomain.t)
+    BaseDomain.isograph_map BaseDomain.empty_mapping
+      ~lhs:(rhs.pre :> BaseDomain.t)
+      ~rhs:(lhs.pre :> BaseDomain.t)
   with
   | NotIsomorphic ->
       false
   | IsomorphicUpTo foot_mapping ->
-      PulseDomain.is_isograph foot_mapping
-        ~lhs:(lhs.post :> PulseDomain.t)
-        ~rhs:(rhs.post :> PulseDomain.t)
+      BaseDomain.is_isograph foot_mapping
+        ~lhs:(lhs.post :> BaseDomain.t)
+        ~rhs:(rhs.post :> BaseDomain.t)
 
 
 module Stack = struct
@@ -245,7 +246,7 @@ let mk_initial proc_desc =
            , (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) )
   in
   let initial_stack =
-    List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack
+    List.fold formals ~init:(InvertedDomain.empty :> BaseDomain.t).stack
       ~f:(fun stack (formal, addr_loc) -> BaseStack.add formal addr_loc stack)
   in
   let pre =
@@ -260,21 +261,21 @@ let mk_initial proc_desc =
 
 
 let discard_unreachable ({pre; post} as astate) =
-  let pre_addresses = PulseDomain.reachable_addresses (pre :> PulseDomain.t) in
-  let pre_old_heap = (pre :> PulseDomain.t).heap in
+  let pre_addresses = BaseDomain.reachable_addresses (pre :> BaseDomain.t) in
+  let pre_old_heap = (pre :> BaseDomain.t).heap in
   let pre_new_heap =
     BaseMemory.filter (fun address -> AbstractValue.Set.mem address pre_addresses) pre_old_heap
   in
-  let post_addresses = PulseDomain.reachable_addresses (post :> PulseDomain.t) in
+  let post_addresses = BaseDomain.reachable_addresses (post :> BaseDomain.t) in
   let all_addresses = AbstractValue.Set.union pre_addresses post_addresses in
-  let post_old_heap = (post :> PulseDomain.t).heap in
+  let post_old_heap = (post :> BaseDomain.t).heap in
   let post_new_heap =
     BaseMemory.filter (fun address -> AbstractValue.Set.mem address all_addresses) post_old_heap
   in
   if phys_equal pre_new_heap pre_old_heap && phys_equal post_new_heap post_old_heap then astate
   else
-    { pre= InvertedDomain.make (pre :> PulseDomain.t).stack pre_new_heap
-    ; post= Domain.make (post :> PulseDomain.t).stack post_new_heap }
+    { pre= InvertedDomain.make (pre :> BaseDomain.t).stack pre_new_heap
+    ; post= Domain.make (post :> BaseDomain.t).stack post_new_heap }
 
 
 let is_local var astate = not (Var.is_return var || Stack.is_abducible astate var)
@@ -288,7 +289,7 @@ module PrePost = struct
     let post_stack =
       BaseStack.filter
         (fun var _ -> Var.appears_in_source_code var && not (is_local var astate))
-        (astate.post :> PulseDomain.t).stack
+        (astate.post :> BaseDomain.t).stack
     in
     (* deregister empty edges *)
     let deregister_empty heap =
@@ -309,7 +310,7 @@ module PrePost = struct
 
   (** invalidate local variables going out of scope *)
   let invalidate_locals pdesc astate : t =
-    let heap : BaseMemory.t = (astate.post :> PulseDomain.t).heap in
+    let heap : BaseMemory.t = (astate.post :> BaseDomain.t).heap in
     let heap' =
       BaseMemory.fold_attrs
         (fun addr attrs heap ->
@@ -411,8 +412,8 @@ module PrePost = struct
 
 
   let pp f {pre; post} =
-    F.fprintf f "PRE:@\n  @[%a@]@\n" PulseDomain.pp (pre :> PulseDomain.t) ;
-    F.fprintf f "POST:@\n  @[%a@]@\n" PulseDomain.pp (post :> PulseDomain.t)
+    F.fprintf f "PRE:@\n  @[%a@]@\n" BaseDomain.pp (pre :> BaseDomain.t) ;
+    F.fprintf f "POST:@\n  @[%a@]@\n" BaseDomain.pp (post :> BaseDomain.t)
 
 
   (* {3 reading the pre from the current state} *)
@@ -434,7 +435,7 @@ module PrePost = struct
         Ok call_state
     | `NotAlreadyVisited, call_state -> (
         (let open Option.Monad_infix in
-        BaseMemory.find_opt addr_pre pre.PulseDomain.heap
+        BaseMemory.find_opt addr_pre pre.BaseDomain.heap
         >>= fun (edges_pre, attrs_pre) ->
         Attributes.get_must_be_valid attrs_pre
         >>| fun callee_access_trace ->
@@ -463,9 +464,9 @@ module PrePost = struct
   let materialize_pre_from_actual callee_proc_name call_location ~pre ~formal ~actual call_state =
     L.d_printfln "Materializing PRE from [%a <- %a]" Var.pp formal AbstractValue.pp (fst actual) ;
     (let open Option.Monad_infix in
-    BaseStack.find_opt formal pre.PulseDomain.stack
+    BaseStack.find_opt formal pre.BaseDomain.stack
     >>= fun (addr_formal_pre, _) ->
-    BaseMemory.find_edge_opt addr_formal_pre Dereference pre.PulseDomain.heap
+    BaseMemory.find_edge_opt addr_formal_pre Dereference pre.BaseDomain.heap
     >>| fun (formal_pre, _) ->
     materialize_pre_from_address callee_proc_name call_location ~pre ~addr_pre:formal_pre
       ~addr_hist_caller:actual call_state)
@@ -501,7 +502,7 @@ module PrePost = struct
     match
       IList.fold2_result formals actuals ~init:call_state ~f:(fun call_state formal (actual, _) ->
           materialize_pre_from_actual callee_proc_name call_location
-            ~pre:(pre_post.pre :> PulseDomain.t)
+            ~pre:(pre_post.pre :> BaseDomain.t)
             ~formal ~actual call_state )
     with
     | Unequal_lengths ->
@@ -513,10 +514,10 @@ module PrePost = struct
 
 
   let materialize_pre_for_globals callee_proc_name call_location pre_post call_state =
-    fold_globals_of_stack call_location (pre_post.pre :> PulseDomain.t).stack call_state
+    fold_globals_of_stack call_location (pre_post.pre :> BaseDomain.t).stack call_state
       ~f:(fun _var ~stack_value:(addr_pre, _) ~addr_hist_caller call_state ->
         materialize_pre_from_address callee_proc_name call_location
-          ~pre:(pre_post.pre :> PulseDomain.t)
+          ~pre:(pre_post.pre :> BaseDomain.t)
           ~addr_pre ~addr_hist_caller call_state )
 
 
@@ -655,12 +656,12 @@ module PrePost = struct
     | `AlreadyVisited, call_state ->
         call_state
     | `NotAlreadyVisited, call_state -> (
-      match BaseMemory.find_opt addr_callee (post :> PulseDomain.t).PulseDomain.heap with
+      match BaseMemory.find_opt addr_callee (post :> BaseDomain.t).BaseDomain.heap with
       | None ->
           call_state
       | Some ((edges_post, _attrs_post) as cell_post) ->
           let cell_pre_opt =
-            BaseMemory.find_opt addr_callee (pre :> PulseDomain.t).PulseDomain.heap
+            BaseMemory.find_opt addr_callee (pre :> BaseDomain.t).BaseDomain.heap
           in
           let call_state_after_post =
             if is_cell_read_only ~cell_pre_opt ~cell_post then call_state
@@ -684,10 +685,10 @@ module PrePost = struct
       (fst actual) ;
     match
       let open Option.Monad_infix in
-      BaseStack.find_opt formal (pre_post.pre :> PulseDomain.t).PulseDomain.stack
+      BaseStack.find_opt formal (pre_post.pre :> BaseDomain.t).BaseDomain.stack
       >>= fun (addr_formal_pre, _) ->
       BaseMemory.find_edge_opt addr_formal_pre Dereference
-        (pre_post.pre :> PulseDomain.t).PulseDomain.heap
+        (pre_post.pre :> BaseDomain.t).BaseDomain.heap
       >>| fun (formal_pre, _) ->
       record_post_for_address callee_proc_name call_loc pre_post ~addr_callee:formal_pre
         ~addr_hist_caller:actual call_state
@@ -700,13 +701,13 @@ module PrePost = struct
 
   let record_post_for_return callee_proc_name call_loc pre_post call_state =
     let return_var = Var.of_pvar (Pvar.get_ret_pvar callee_proc_name) in
-    match BaseStack.find_opt return_var (pre_post.post :> PulseDomain.t).stack with
+    match BaseStack.find_opt return_var (pre_post.post :> BaseDomain.t).stack with
     | None ->
         (call_state, None)
     | Some (addr_return, _) -> (
       match
         BaseMemory.find_edge_opt addr_return Dereference
-          (pre_post.post :> PulseDomain.t).PulseDomain.heap
+          (pre_post.post :> BaseDomain.t).BaseDomain.heap
       with
       | None ->
           (call_state, None)
@@ -747,7 +748,7 @@ module PrePost = struct
 
   let apply_post_for_globals callee_proc_name call_location pre_post call_state =
     match
-      fold_globals_of_stack call_location (pre_post.pre :> PulseDomain.t).stack call_state
+      fold_globals_of_stack call_location (pre_post.pre :> BaseDomain.t).stack call_state
         ~f:(fun _var ~stack_value:(addr_callee, _) ~addr_hist_caller call_state ->
           Ok
             (record_post_for_address callee_proc_name call_location pre_post ~addr_callee
@@ -777,11 +778,11 @@ module PrePost = struct
                     attrs
                 in
                 BaseMemory.set_attrs addr_caller attrs' heap )
-        (pre_post.post :> PulseDomain.t).heap heap0
+        (pre_post.post :> BaseDomain.t).heap heap0
     in
     if phys_equal heap heap0 then call_state
     else
-      let post = Domain.make (call_state.astate.post :> PulseDomain.t).stack heap in
+      let post = Domain.make (call_state.astate.post :> BaseDomain.t).stack heap in
       {call_state with astate= {call_state.astate with post}}
 
 
@@ -843,6 +844,6 @@ module PrePost = struct
         Ok (apply_post callee_proc_name call_location pre_post ~formals ~actuals call_state)
 end
 
-let extract_pre {pre} = (pre :> PulseDomain.t)
+let extract_pre {pre} = (pre :> BaseDomain.t)
 
-let extract_post {post} = (post :> PulseDomain.t)
+let extract_post {post} = (post :> BaseDomain.t)

infer/src/pulse/PulseAbductiveDomain.mli

@@ -6,8 +6,9 @@
  *)
 open! IStd
 open PulseBasicInterface
+module BaseDomain = PulseBaseDomain
 
-(* layer on top of {!PulseDomain} to propagate operations on the current state to the pre-condition
+(* layer on top of {!BaseDomain} to propagate operations on the current state to the pre-condition
    when necessary
 
    The abstract type [t] is a pre/post pair in the style of biabduction.
@@ -17,30 +18,30 @@ include AbstractDomain.NoJoin
 
 val mk_initial : Procdesc.t -> t
 
-(** stack operations like {!PulseDomain.Stack} but that also take care of propagating facts to the
+(** stack operations like {!BaseDomain.Stack} but that also take care of propagating facts to the
     precondition *)
 module Stack : sig
-  val add : Var.t -> PulseDomain.Stack.value -> t -> t
+  val add : Var.t -> BaseDomain.Stack.value -> t -> t
 
   val remove_vars : Var.t list -> t -> t
 
-  val fold : (Var.t -> PulseDomain.Stack.value -> 'a -> 'a) -> t -> 'a -> 'a
+  val fold : (Var.t -> BaseDomain.Stack.value -> 'a -> 'a) -> t -> 'a -> 'a
 
-  val find_opt : Var.t -> t -> PulseDomain.Stack.value option
+  val find_opt : Var.t -> t -> BaseDomain.Stack.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 -> PulseDomain.Stack.value -> bool) -> t -> bool
+  val exists : (Var.t -> BaseDomain.Stack.value -> bool) -> t -> bool
 end
 
-(** stack operations like {!PulseDomain.Heap} but that also take care of propagating facts to the
+(** memory operations like {!BaseDomain.Memory} but that also take care of propagating facts to the
     precondition *)
 module Memory : sig
-  module Access = PulseDomain.Memory.Access
-  module Edges = PulseDomain.Memory.Edges
+  module Access = BaseDomain.Memory.Access
+  module Edges = BaseDomain.Memory.Edges
 
   val add_attribute : AbstractValue.t -> Attribute.t -> t -> t
 
@@ -54,12 +55,11 @@ module Memory : sig
 
   val check_valid : unit Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t Trace.t) result
 
-  val find_opt : AbstractValue.t -> t -> PulseDomain.Memory.cell option
+  val find_opt : AbstractValue.t -> t -> BaseDomain.Memory.cell option
 
   val find_edge_opt : AbstractValue.t -> Access.t -> t -> (AbstractValue.t * ValueHistory.t) option
 
-  val set_cell :
-    AbstractValue.t * ValueHistory.t -> PulseDomain.Memory.cell -> Location.t -> t -> t
+  val set_cell : AbstractValue.t * ValueHistory.t -> BaseDomain.Memory.cell -> Location.t -> t -> t
 
   val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
@@ -103,6 +103,6 @@ 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 extract_pre : PrePost.t -> PulseDomain.t
+val extract_pre : PrePost.t -> BaseDomain.t
 
-val extract_post : PrePost.t -> PulseDomain.t
+val extract_post : PrePost.t -> BaseDomain.t

infer/src/pulse/PulseDomainInterface.ml

@@ -0,0 +1,19 @@
+(*
+ * 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
+
+(** if you do any mutations of the state in pulse you probably want this module *)
+module AbductiveDomain = PulseAbductiveDomain
+
+module Stack = AbductiveDomain.Stack
+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 BaseMemory = BaseDomain.Memory

infer/src/pulse/PulseOperations.ml

@@ -6,20 +6,11 @@
  *)
 open! IStd
 module L = Logging
-module Memory = PulseAbductiveDomain.Memory
-module Stack = PulseAbductiveDomain.Stack
 open Result.Monad_infix
 open PulseBasicInterface
+open PulseDomainInterface
 
-include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
-  struct
-  [@@@warning "-60"]
-
-  (** Do not use {!PulseDomain} directly, go through {!PulseAbductiveDomain} instead *)
-  module PulseDomain = struct end [@@deprecated "Use PulseAbductiveDomain instead."]
-end
-
-type t = PulseAbductiveDomain.t
+type t = AbductiveDomain.t
 
 type 'a access_result = ('a, PulseDiagnostic.t) result
 
@@ -33,7 +24,7 @@ let check_addr_access location (address, history) astate =
 
 module Closures = struct
   open Result.Monad_infix
-  module Memory = PulseAbductiveDomain.Memory
+  module Memory = AbductiveDomain.Memory
 
   let fake_capture_field_prefix = "__capture_"
 
@@ -352,7 +343,7 @@ let remove_vars vars location astate =
         match Stack.find_opt var astate with
         | Some (address, history) ->
             let astate =
-              if Var.appears_in_source_code var && PulseAbductiveDomain.is_local var astate then
+              if Var.appears_in_source_code var && AbductiveDomain.is_local var astate then
                 mark_address_of_stack_variable history var location address astate
               else astate
             in
@@ -363,7 +354,7 @@ let remove_vars vars location astate =
             astate )
   in
   let astate' = Stack.remove_vars vars astate in
-  if phys_equal astate' astate then astate else PulseAbductiveDomain.discard_unreachable astate'
+  if phys_equal astate' astate then astate else AbductiveDomain.discard_unreachable astate'
 
 
 let call ~caller_summary call_loc callee_pname ~ret ~actuals astate =
@@ -373,11 +364,10 @@ let call ~caller_summary call_loc callee_pname ~ret ~actuals astate =
         Procdesc.get_formals callee_proc_desc
         |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar)
       in
-      (* call {!PulseAbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *)
+      (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *)
       List.fold_result preposts ~init:[] ~f:(fun posts pre_post ->
           (* apply all pre/post specs *)
-          PulseAbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals
-            astate
+          AbductiveDomain.PrePost.apply callee_pname call_loc pre_post ~formals ~actuals astate
           >>| fun (post, return_val_opt) ->
           let event = ValueHistory.Call {f= Call callee_pname; location= call_loc; in_call= []} in
           let post =

infer/src/pulse/PulseOperations.mli

@@ -7,6 +7,7 @@
 
 open! IStd
 open PulseBasicInterface
+open PulseDomainInterface
 
 type t = PulseAbductiveDomain.t
 
@@ -38,7 +39,7 @@ val eval_deref : Location.t -> Exp.t -> t -> (t * (AbstractValue.t * ValueHistor
 val eval_access :
      Location.t
   -> AbstractValue.t * ValueHistory.t
-  -> PulseDomain.Memory.Access.t
+  -> BaseMemory.Access.t
   -> t
   -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** Like [eval] but starts from an address instead of an expression, checks that it is valid, and if
@@ -59,7 +60,7 @@ val havoc_field :
 
 val realloc_pvar : Pvar.t -> Location.t -> t -> t
 
-val write_id : Ident.t -> PulseDomain.Stack.value -> t -> t
+val write_id : Ident.t -> AbstractValue.t * ValueHistory.t -> t -> t
 
 val write_deref :
      Location.t