[pulse][6/9] add PulseAbstractValue to PulseBasicInterface

Summary:
See explanations in D17955104.

This renames `AbstractAddress` to `AbstractValue` since they are not
necessarily addresses.

Reviewed By: ezgicicek

Differential Revision: D17955290

fbshipit-source-id: 8bb4c61f2

infer/src/backend/ondemand.ml

@@ -97,7 +97,7 @@ type global_state =
   ; name_generator: Ident.NameGenerator.t
   ; proc_analysis_time: (Mtime.Span.t * string) option
         (** the time elapsed doing [status] so far *)
-  ; pulse_address_generator: PulseDomain.AbstractAddress.state
+  ; pulse_address_generator: PulseAbstractValue.state
   ; symexec_state: State.t }
 
 let save_global_state () =
@@ -112,7 +112,7 @@ let save_global_state () =
   ; proc_analysis_time=
       Option.map !current_taskbar_status ~f:(fun (t0, status) ->
           (Mtime.span t0 (Mtime_clock.now ()), status) )
-  ; pulse_address_generator= PulseDomain.AbstractAddress.get_state ()
+  ; pulse_address_generator= PulseAbstractValue.get_state ()
   ; symexec_state= State.save_state () }
 
 
@@ -123,7 +123,7 @@ let restore_global_state st =
   BiabductionConfig.footprint := st.footprint_mode ;
   Printer.curr_html_formatter := st.html_formatter ;
   Ident.NameGenerator.set_current st.name_generator ;
-  PulseDomain.AbstractAddress.set_state st.pulse_address_generator ;
+  PulseAbstractValue.set_state st.pulse_address_generator ;
   State.restore_state st.symexec_state ;
   current_taskbar_status :=
     Option.map st.proc_analysis_time ~f:(fun (suspended_span, status) ->

infer/src/checkers/impurity.ml

@@ -7,7 +7,6 @@
 open! IStd
 module F = Format
 module L = Logging
-module AbstractAddress = PulseDomain.AbstractAddress
 module BaseStack = PulseDomain.Stack
 open PulseBasicInterface
 
@@ -16,11 +15,11 @@ let debug fmt = L.(debug Analysis Verbose fmt)
 (* An impurity analysis that relies on pulse to determine how the state
    changes *)
 
-let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractAddress.t list option =
+let get_matching_dest_addr_opt ~edges_pre ~edges_post : AbstractValue.t list option =
   match
     List.fold2 ~init:(Some [])
       ~f:(fun acc (_, (addr_dest_pre, _)) (_, (addr_dest_post, _)) ->
-        if AbstractAddress.equal addr_dest_pre addr_dest_post then
+        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)
@@ -62,11 +61,11 @@ let extract_impurity pdesc pre_post : ImpurityDomain.t =
       | [] ->
           acc
       | addr :: addr_to_explore -> (
-          if PulseDomain.AbstractAddressSet.mem addr visited then aux acc ~addr_to_explore ~visited
+          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 visited = PulseDomain.AbstractAddressSet.add addr visited in
+            let visited = AbstractValue.Set.add addr visited in
             match (cell_pre_opt, cell_post_opt) with
             | None, None ->
                 aux acc ~addr_to_explore ~visited
@@ -88,7 +87,7 @@ let extract_impurity pdesc pre_post : ImpurityDomain.t =
                     (add_invalid_and_modified ~check_empty:true attrs_post acc)
                     ~addr_to_explore ~visited ) )
     in
-    match aux [] ~addr_to_explore:[addr] ~visited:PulseDomain.AbstractAddressSet.empty with
+    match aux [] ~addr_to_explore:[addr] ~visited:AbstractValue.Set.empty with
     | [] ->
         acc
     | hd :: tl ->

infer/src/pulse/Pulse.ml

@@ -8,7 +8,6 @@ open! IStd
 module F = Format
 module L = Logging
 open Result.Monad_infix
-module AbstractAddress = PulseDomain.AbstractAddress
 open PulseBasicInterface
 
 include (* ocaml ignores the warning suppression at toplevel, hence the [include struct ... end] trick *)
@@ -218,7 +217,7 @@ module DisjunctiveAnalyzer = AbstractInterpreter.MakeWTO (DisjunctiveTransferFun
 let checker {Callbacks.exe_env; summary} =
   let tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary) in
   let proc_data = ProcData.make summary tenv () in
-  AbstractAddress.init () ;
+  AbstractValue.init () ;
   let pdesc = Summary.get_proc_desc summary in
   let initial =
     DisjunctiveTransferFunctions.Disjuncts.singleton (PulseAbductiveDomain.mk_initial pdesc)

infer/src/pulse/PulseAbductiveDomain.ml

@@ -7,7 +7,6 @@
 open! IStd
 module F = Format
 module L = Logging
-module AbstractAddress = PulseDomain.AbstractAddress
 module BaseStack = PulseDomain.Stack
 module BaseMemory = PulseDomain.Memory
 open PulseBasicInterface
@@ -102,7 +101,7 @@ module Stack = struct
     | Some addr_hist ->
         (astate, addr_hist)
     | None ->
-        let addr = AbstractAddress.mk_fresh () in
+        let addr = AbstractValue.mk_fresh () in
         let addr_hist = (addr, origin) in
         let post_stack = BaseStack.add var addr_hist (astate.post :> base_domain).stack in
         let pre =
@@ -182,7 +181,7 @@ module Memory = struct
     | Some addr_hist_dst ->
         (astate, addr_hist_dst)
     | None ->
-        let addr_dst = AbstractAddress.mk_fresh () in
+        let addr_dst = AbstractValue.mk_fresh () in
         let addr_hist_dst = (addr_dst, hist_src) in
         let post_heap =
           BaseMemory.add_edge addr_src access addr_hist_dst (astate.post :> base_domain).heap
@@ -243,7 +242,7 @@ let mk_initial proc_desc =
     |> List.map ~f:(fun (mangled, _) ->
            let pvar = Pvar.mk mangled proc_name in
            ( Var.of_pvar pvar
-           , (AbstractAddress.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) )
+           , (AbstractValue.mk_fresh (), [ValueHistory.FormalDeclared (pvar, location)]) ) )
   in
   let initial_stack =
     List.fold formals ~init:(InvertedDomain.empty :> PulseDomain.t).stack
@@ -264,17 +263,13 @@ 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_new_heap =
-    BaseMemory.filter
+    BaseMemory.filter (fun address -> AbstractValue.Set.mem address pre_addresses) pre_old_heap
-      (fun address -> PulseDomain.AbstractAddressSet.mem address pre_addresses)
-      pre_old_heap
   in
   let post_addresses = PulseDomain.reachable_addresses (post :> PulseDomain.t) in
-  let all_addresses = PulseDomain.AbstractAddressSet.union pre_addresses post_addresses in
+  let all_addresses = AbstractValue.Set.union pre_addresses post_addresses in
   let post_old_heap = (post :> PulseDomain.t).heap in
   let post_new_heap =
-    BaseMemory.filter
+    BaseMemory.filter (fun address -> AbstractValue.Set.mem address all_addresses) post_old_heap
-      (fun address -> PulseDomain.AbstractAddressSet.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
@@ -345,8 +340,8 @@ module PrePost = struct
   (* {2 machinery to apply a pre/post pair corresponding to a function's summary in a function call
      to the current state} *)
 
-  module AddressSet = PulseDomain.AbstractAddressSet
+  module AddressSet = AbstractValue.Set
-  module AddressMap = PulseDomain.AbstractAddressMap
+  module AddressMap = AbstractValue.Map
 
   (** raised when the pre/post pair and the current state disagree on the aliasing, i.e. some
      addresses that are distinct in the pre/post are aliased in the current state. Typically raised
@@ -356,9 +351,9 @@ 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 *)
-    ; subst: (AbstractAddress.t * ValueHistory.t) AddressMap.t
+    ; subst: (AbstractValue.t * ValueHistory.t) AddressMap.t
           (** translation from callee addresses to caller addresses and their caller histories *)
-    ; rev_subst: AbstractAddress.t AddressMap.t
+    ; rev_subst: AbstractValue.t AddressMap.t
           (** the inverse translation from [subst] from caller addresses to callee addresses *)
     ; visited: AddressSet.t
           (** set of callee addresses that have been visited already
@@ -373,9 +368,9 @@ module PrePost = struct
       "@[<v>{ astate=@[<hv2>%a@];@, subst=@[<hv2>%a@];@, rev_subst=@[<hv2>%a@];@, \
        visited=@[<hv2>%a@]@, }@]"
       pp astate
-      (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractAddress.pp fmt addr))
+      (AddressMap.pp ~pp_value:(fun fmt (addr, _) -> AbstractValue.pp fmt addr))
       subst
-      (AddressMap.pp ~pp_value:AbstractAddress.pp)
+      (AddressMap.pp ~pp_value:AbstractValue.pp)
       rev_subst AddressSet.pp visited
 
 
@@ -399,10 +394,10 @@ module PrePost = struct
   let visit call_state ~addr_callee ~addr_hist_caller =
     let addr_caller = fst addr_hist_caller in
     ( match AddressMap.find_opt addr_caller call_state.rev_subst with
-    | Some addr_callee' when not (AbstractAddress.equal addr_callee addr_callee') ->
+    | Some addr_callee' when not (AbstractValue.equal addr_callee addr_callee') ->
         L.d_printfln "Huho, address %a in post already bound to %a, not %a@\nState=%a"
-          AbstractAddress.pp addr_caller AbstractAddress.pp addr_callee' AbstractAddress.pp
+          AbstractValue.pp addr_caller AbstractValue.pp addr_callee' AbstractValue.pp addr_callee
-          addr_callee pp_call_state call_state ;
+          pp_call_state call_state ;
         raise Aliasing
     | _ ->
         () ) ;
@@ -466,7 +461,7 @@ module PrePost = struct
       has been instantiated with the corresponding [actual] into the current state
       [call_state.astate] *)
   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 AbstractAddress.pp (fst actual) ;
+    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
     >>= fun (addr_formal_pre, _) ->
@@ -489,7 +484,7 @@ module PrePost = struct
 
                   TODO: can the traces be leveraged here? maybe easy to detect writes by looking at
                   the post trace *)
-              AbstractAddress.equal addr_dest_pre addr_dest_post )
+              AbstractValue.equal addr_dest_pre addr_dest_post )
             edges_pre edges_post
         in
         if CommandLineOption.strict_mode then assert are_edges_equal ;
@@ -544,7 +539,7 @@ module PrePost = struct
   let subst_find_or_new subst addr_callee ~default_hist_caller =
     match AddressMap.find_opt addr_callee subst with
     | None ->
-        let addr_hist_fresh = (AbstractAddress.mk_fresh (), default_hist_caller) in
+        let addr_hist_fresh = (AbstractValue.mk_fresh (), default_hist_caller) in
         (AddressMap.add addr_callee addr_hist_fresh subst, addr_hist_fresh)
     | Some addr_hist_caller ->
         (subst, addr_hist_caller)
@@ -655,7 +650,7 @@ module PrePost = struct
 
   let rec record_post_for_address callee_proc_name call_loc ({pre; post} as pre_post) ~addr_callee
       ~addr_hist_caller call_state =
-    L.d_printfln "%a<->%a" AbstractAddress.pp addr_callee AbstractAddress.pp (fst addr_hist_caller) ;
+    L.d_printfln "%a<->%a" AbstractValue.pp addr_callee AbstractValue.pp (fst addr_hist_caller) ;
     match visit call_state ~addr_callee ~addr_hist_caller with
     | `AlreadyVisited, call_state ->
         call_state
@@ -685,7 +680,7 @@ module PrePost = struct
 
 
   let record_post_for_actual callee_proc_name call_loc pre_post ~formal ~actual call_state =
-    L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractAddress.pp
+    L.d_printfln_escaped "Recording POST from [%a] <-> %a" Var.pp formal AbstractValue.pp
       (fst actual) ;
     match
       let open Option.Monad_infix in
@@ -721,7 +716,7 @@ module PrePost = struct
             | Some return_caller_hist ->
                 return_caller_hist
             | None ->
-                ( AbstractAddress.mk_fresh ()
+                ( AbstractValue.mk_fresh ()
                 , [ (* this could maybe include an event like "returned here" *) ] )
           in
           let call_state =

infer/src/pulse/PulseAbductiveDomain.mli

@@ -5,7 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 open! IStd
-module AbstractAddress = PulseDomain.AbstractAddress
 open PulseBasicInterface
 
 (* layer on top of {!PulseDomain} to propagate operations on the current state to the pre-condition
@@ -43,39 +42,39 @@ module Memory : sig
   module Access = PulseDomain.Memory.Access
   module Edges = PulseDomain.Memory.Edges
 
-  val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t
+  val add_attribute : AbstractValue.t -> Attribute.t -> t -> t
 
   val add_edge :
-       AbstractAddress.t * ValueHistory.t
+       AbstractValue.t * ValueHistory.t
     -> Access.t
     -> PulseDomain.AddrTracePair.t
     -> Location.t
     -> t
     -> t
 
-  val check_valid : unit Trace.t -> AbstractAddress.t -> t -> (t, Invalidation.t Trace.t) result
+  val check_valid : unit Trace.t -> AbstractValue.t -> t -> (t, Invalidation.t Trace.t) result
 
-  val find_opt : AbstractAddress.t -> t -> PulseDomain.Memory.cell option
+  val find_opt : AbstractValue.t -> t -> PulseDomain.Memory.cell option
 
-  val find_edge_opt : AbstractAddress.t -> Access.t -> t -> PulseDomain.AddrTracePair.t option
+  val find_edge_opt : AbstractValue.t -> Access.t -> t -> PulseDomain.AddrTracePair.t option
 
   val set_cell :
-    AbstractAddress.t * ValueHistory.t -> PulseDomain.Memory.cell -> Location.t -> t -> t
+    AbstractValue.t * ValueHistory.t -> PulseDomain.Memory.cell -> Location.t -> t -> t
 
-  val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
+  val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
-  val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option
+  val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option
 
-  val is_std_vector_reserved : AbstractAddress.t -> t -> bool
+  val is_std_vector_reserved : AbstractValue.t -> t -> bool
 
-  val std_vector_reserve : AbstractAddress.t -> t -> t
+  val std_vector_reserve : AbstractValue.t -> t -> t
 
   val eval_edge :
-    AbstractAddress.t * ValueHistory.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t
+    AbstractValue.t * ValueHistory.t -> Access.t -> t -> t * PulseDomain.AddrTracePair.t
   (** [eval_edge (addr,hist) access astate] follows the edge [addr --access--> .] in memory and
       returns what it points to or creates a fresh value if that edge didn't exist.  *)
 
-  val get_constant : AbstractAddress.t -> t -> Const.t option
+  val get_constant : AbstractValue.t -> t -> Const.t option
 end
 
 val is_local : Var.t -> t -> bool
@@ -94,9 +93,9 @@ module PrePost : sig
     -> Location.t
     -> t
     -> formals:Var.t list
-    -> actuals:((AbstractAddress.t * ValueHistory.t) * Typ.t) list
+    -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
     -> domain_t
-    -> (domain_t * (AbstractAddress.t * ValueHistory.t) option, PulseDiagnostic.t) result
+    -> (domain_t * (AbstractValue.t * ValueHistory.t) option, PulseDiagnostic.t) result
   (** return the abstract state after the call along with an optional return value *)
 end
 

infer/src/pulse/PulseAbstractValue.ml

@@ -0,0 +1,40 @@
+(*
+ * 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
+
+type t = int [@@deriving compare]
+
+let equal = [%compare.equal: t]
+
+let next_fresh = ref 1
+
+let mk_fresh () =
+  let l = !next_fresh in
+  incr next_fresh ; l
+
+
+let pp f l = F.fprintf f "v%d" l
+
+let init () = next_fresh := 1
+
+type state = int
+
+let get_state () = !next_fresh
+
+let set_state counter = next_fresh := counter
+
+module PPKey = struct
+  type nonrec t = t
+
+  let compare = compare
+
+  let pp = pp
+end
+
+module Set = PrettyPrintable.MakePPSet (PPKey)
+module Map = PrettyPrintable.MakePPMap (PPKey)

infer/src/pulse/PulseAbstractValue.mli

@@ -0,0 +1,30 @@
+(*
+ * 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
+
+(** An abstract value, eg an address in memory. *)
+
+type t = private int [@@deriving compare]
+
+val equal : t -> t -> bool
+
+val mk_fresh : unit -> t
+
+val pp : F.formatter -> t -> unit
+
+val init : unit -> unit
+
+type state
+
+val get_state : unit -> state
+
+val set_state : state -> unit
+
+module Set : PrettyPrintable.PPSet with type elt = t
+
+module Map : PrettyPrintable.PPMap with type key = t

infer/src/pulse/PulseAttribute.ml

@@ -10,18 +10,18 @@ module Invalidation = PulseInvalidation
 module Trace = PulseTrace
 module ValueHistory = PulseValueHistory
 
-(** Make sure we don't depend on {!AbstractAddress} to avoid attributes depending on
+(** Make sure we don't depend on {!AbstractValue} to avoid attributes depending on
-   addresses. Otherwise they become a pain to handle when comparing memory states.
+    values. Otherwise they become a pain to handle when comparing memory states.
 
-    If you find you need to make attributes depend on {!AbstractAddress} then remember to modify
+    If you find you need to make attributes depend on {!AbstractValue} then remember to modify
     graph operations of {!PulseDomain} and the interprocedural operations in {!PulseAbductiveDomain}
 *)
 include struct
   [@@@warning "-60"]
 
-  module AbstractAddress = struct end
+  module AbstractValue = struct end
 
-  module PulseAbstractAddress = struct end
+  module PulseAbstractValue = struct end
 end
 
 module Attribute = struct

infer/src/pulse/PulseBasicInterface.ml

@@ -8,6 +8,7 @@ open! IStd
 
 (** Basic Pulse modules that are safe to use in any module *)
 
+module AbstractValue = PulseAbstractValue
 module Attribute = PulseAttribute
 module Attributes = PulseAttribute.Attributes
 module CallEvent = PulseCallEvent

infer/src/pulse/PulseDomain.ml

@@ -11,63 +11,20 @@ open PulseBasicInterface
 
 (* {2 Abstract domain description } *)
 
-(** An abstract address in memory. *)
-module AbstractAddress : sig
-  type t = private int [@@deriving compare]
-
-  val equal : t -> t -> bool
-
-  val mk_fresh : unit -> t
-
-  val pp : F.formatter -> t -> unit
-
-  val init : unit -> unit
-
-  type state
-
-  val get_state : unit -> state
-
-  val set_state : state -> unit
-end = struct
-  type t = int [@@deriving compare]
-
-  let equal = [%compare.equal: t]
-
-  let next_fresh = ref 1
-
-  let mk_fresh () =
-    let l = !next_fresh in
-    incr next_fresh ; l
-
-
-  let pp f l = F.fprintf f "v%d" l
-
-  let init () = next_fresh := 1
-
-  type state = int
-
-  let get_state () = !next_fresh
-
-  let set_state counter = next_fresh := counter
-end
-
-module AbstractAddressSet = PrettyPrintable.MakePPSet (AbstractAddress)
-module AbstractAddressMap = PrettyPrintable.MakePPMap (AbstractAddress)
-
 (* {3 Heap domain } *)
 
 module AddrTracePair = struct
-  type t = AbstractAddress.t * ValueHistory.t [@@deriving compare]
+  type t = AbstractValue.t * ValueHistory.t [@@deriving compare]
 
   let pp f addr_trace =
     if Config.debug_level_analysis >= 3 then
-      Pp.pair ~fst:AbstractAddress.pp ~snd:ValueHistory.pp f addr_trace
+      Pp.pair ~fst:AbstractValue.pp ~snd:ValueHistory.pp f addr_trace
-    else AbstractAddress.pp f (fst addr_trace)
+    else AbstractValue.pp f (fst addr_trace)
 end
 
 module Memory : sig
   module Access : sig
-    include PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t
+    include PrettyPrintable.PrintableOrderedType with type t = AbstractValue.t HilExp.Access.t
 
     val equal : t -> t -> bool
   end
@@ -84,54 +41,54 @@ module Memory : sig
 
   val empty : t
 
-  val filter : (AbstractAddress.t -> bool) -> t -> t
+  val filter : (AbstractValue.t -> bool) -> t -> t
 
-  val filter_heap : (AbstractAddress.t -> edges -> bool) -> t -> t
+  val filter_heap : (AbstractValue.t -> edges -> bool) -> t -> t
 
-  val find_opt : AbstractAddress.t -> t -> cell option
+  val find_opt : AbstractValue.t -> t -> cell option
 
-  val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc
+  val fold_attrs : (AbstractValue.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc
 
-  val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t
+  val set_attrs : AbstractValue.t -> Attributes.t -> t -> t
 
-  val set_edges : AbstractAddress.t -> edges -> t -> t
+  val set_edges : AbstractValue.t -> edges -> t -> t
 
-  val set_cell : AbstractAddress.t -> cell -> t -> t
+  val set_cell : AbstractValue.t -> cell -> t -> t
 
-  val find_edges_opt : AbstractAddress.t -> t -> edges option
+  val find_edges_opt : AbstractValue.t -> t -> edges option
 
-  val mem_edges : AbstractAddress.t -> t -> bool
+  val mem_edges : AbstractValue.t -> t -> bool
 
   val pp_heap : F.formatter -> t -> unit
 
   val pp_attributes : F.formatter -> t -> unit
 
-  val register_address : AbstractAddress.t -> t -> t
+  val register_address : AbstractValue.t -> t -> t
 
-  val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
+  val add_edge : AbstractValue.t -> Access.t -> AddrTracePair.t -> t -> t
 
-  val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option
+  val find_edge_opt : AbstractValue.t -> Access.t -> t -> AddrTracePair.t option
 
-  val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t
+  val add_attribute : AbstractValue.t -> Attribute.t -> t -> t
 
-  val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
+  val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
-  val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result
+  val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t Trace.t) result
 
-  val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option
+  val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option
 
-  val get_constant : AbstractAddress.t -> t -> Const.t option
+  val get_constant : AbstractValue.t -> t -> Const.t option
 
-  val std_vector_reserve : AbstractAddress.t -> t -> t
+  val std_vector_reserve : AbstractValue.t -> t -> t
 
-  val is_std_vector_reserved : AbstractAddress.t -> t -> bool
+  val is_std_vector_reserved : AbstractValue.t -> t -> bool
 end = struct
   module Access = struct
-    type t = AbstractAddress.t HilExp.Access.t [@@deriving compare]
+    type t = AbstractValue.t HilExp.Access.t [@@deriving compare]
 
     let equal = [%compare.equal: t]
 
-    let pp = HilExp.Access.pp AbstractAddress.pp
+    let pp = HilExp.Access.pp AbstractValue.pp
   end
 
   module Edges = PrettyPrintable.MakePPMap (Access)
@@ -142,7 +99,7 @@ end = struct
 
   type cell = edges * Attributes.t
 
-  module Graph = PrettyPrintable.MakePPMap (AbstractAddress)
+  module Graph = PrettyPrintable.MakePPMap (AbstractValue)
 
   type t = edges Graph.t * Attributes.t Graph.t
 
@@ -184,7 +141,7 @@ end = struct
 
 
   let check_valid address memory =
-    L.d_printfln "Checking validity of %a" AbstractAddress.pp address ;
+    L.d_printfln "Checking validity of %a" AbstractValue.pp address ;
     match Graph.find_opt address (snd memory) |> Option.bind ~f:Attributes.get_invalid with
     | Some invalidation ->
         Error invalidation
@@ -295,20 +252,20 @@ let empty =
     [rhs_to_lhs]) between the addresses of [lhs] and [rhs] such that [lhs_to_rhs(reachable(lhs)) =
     reachable(rhs)] (where addresses are reachable if they are reachable from stack variables).  *)
 module GraphComparison = struct
-  module AddressMap = PrettyPrintable.MakePPMap (AbstractAddress)
+  module AddressMap = PrettyPrintable.MakePPMap (AbstractValue)
 
   (** translation between the abstract values on the LHS and the ones on the RHS *)
   type mapping =
-    { rhs_to_lhs: AbstractAddress.t AddressMap.t  (** map from RHS values to LHS *)
+    { rhs_to_lhs: AbstractValue.t AddressMap.t  (** map from RHS values to LHS *)
-    ; lhs_to_rhs: AbstractAddress.t AddressMap.t  (** inverse map from [rhs_to_lhs] *) }
+    ; lhs_to_rhs: AbstractValue.t AddressMap.t  (** inverse map from [rhs_to_lhs] *) }
 
   let empty_mapping = {rhs_to_lhs= AddressMap.empty; lhs_to_rhs= AddressMap.empty}
 
   let pp_mapping fmt {rhs_to_lhs; lhs_to_rhs} =
     F.fprintf fmt "@[<v>{ rhs_to_lhs=@[<hv2>%a@];@,lhs_to_rhs=@[<hv2>%a@];@,}@]"
-      (AddressMap.pp ~pp_value:AbstractAddress.pp)
+      (AddressMap.pp ~pp_value:AbstractValue.pp)
       rhs_to_lhs
-      (AddressMap.pp ~pp_value:AbstractAddress.pp)
+      (AddressMap.pp ~pp_value:AbstractValue.pp)
       lhs_to_rhs
 
 
@@ -316,13 +273,13 @@ module GraphComparison = struct
   let record_equal ~addr_lhs ~addr_rhs mapping =
     (* have we seen [addr_lhs] before?.. *)
     match AddressMap.find_opt addr_lhs mapping.lhs_to_rhs with
-    | Some addr_rhs' when not (AbstractAddress.equal addr_rhs addr_rhs') ->
+    | Some addr_rhs' when not (AbstractValue.equal addr_rhs addr_rhs') ->
         (* ...yes, but it was bound to another address *)
         L.d_printfln
           "Aliasing in LHS not in RHS: LHS address %a in current already bound to %a, not %a@\n\
            State=%a"
-          AbstractAddress.pp addr_lhs AbstractAddress.pp addr_rhs' AbstractAddress.pp addr_rhs
+          AbstractValue.pp addr_lhs AbstractValue.pp addr_rhs' AbstractValue.pp addr_rhs pp_mapping
-          pp_mapping mapping ;
+          mapping ;
         `AliasingLHS
     | Some _addr_rhs (* [_addr_rhs = addr_rhs] *) ->
         `AlreadyVisited
@@ -335,7 +292,7 @@ module GraphComparison = struct
           L.d_printfln
             "Aliasing in RHS not in LHS: RHS address %a in current already bound to %a, not %a@\n\
              State=%a"
-            AbstractAddress.pp addr_rhs AbstractAddress.pp addr_lhs' AbstractAddress.pp addr_lhs
+            AbstractValue.pp addr_rhs AbstractValue.pp addr_lhs' AbstractValue.pp addr_lhs
             pp_mapping mapping ;
           `AliasingRHS
       | None ->
@@ -354,7 +311,7 @@ module GraphComparison = struct
   (** can we extend [mapping] so that the subgraph of [lhs] rooted at [addr_lhs] is isomorphic to
       the subgraph of [rhs] rooted at [addr_rhs]? *)
   let rec isograph_map_from_address ~lhs ~addr_lhs ~rhs ~addr_rhs mapping =
-    L.d_printfln "%a<->%a@\n" AbstractAddress.pp addr_lhs AbstractAddress.pp addr_rhs ;
+    L.d_printfln "%a<->%a@\n" AbstractValue.pp addr_lhs AbstractValue.pp addr_rhs ;
     match record_equal mapping ~addr_lhs ~addr_rhs with
     | `AlreadyVisited ->
         IsomorphicUpTo mapping
@@ -449,12 +406,12 @@ module GraphVisit : sig
     -> t
     -> init:'accum
     -> f:(   'accum
-          -> AbstractAddress.t
+          -> AbstractValue.t
           -> Var.t
           -> Memory.Access.t list
           -> ('accum, 'final) Base.Continue_or_stop.t)
     -> finish:('accum -> 'final)
-    -> AbstractAddressSet.t * 'final
+    -> AbstractValue.Set.t * 'final
   (** Generic graph traversal of the memory starting from each variable in the stack that pass
       [var_filter], in order. Returns the result of folding over every address in the graph and the
       set of addresses that have been visited before [f] returned [Stop] or all reachable addresses
@@ -464,9 +421,9 @@ end = struct
   open Base.Continue_or_stop
 
   let visit address visited =
-    if AbstractAddressSet.mem address visited then `AlreadyVisited
+    if AbstractValue.Set.mem address visited then `AlreadyVisited
     else
-      let visited = AbstractAddressSet.add address visited in
+      let visited = AbstractValue.Set.add address visited in
       `NotAlreadyVisited visited
 
 
@@ -501,7 +458,7 @@ end = struct
 
   let fold ~var_filter astate ~init ~f ~finish =
     let finish (visited, accum) = (visited, finish accum) in
-    let init = (AbstractAddressSet.empty, init) in
+    let init = (AbstractValue.Set.empty, init) in
     Container.fold_until astate.stack
       ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Stack.fold) ~init ~finish
       ~f:(fun visited_accum (var, (address, _loc)) ->

infer/src/pulse/PulseDomain.mli

@@ -9,30 +9,8 @@ open! IStd
 module F = Format
 open PulseBasicInterface
 
-module AbstractAddress : sig
-  type t = private int [@@deriving compare]
-
-  val equal : t -> t -> bool
-
-  val init : unit -> unit
-
-  val pp : F.formatter -> t -> unit [@@warning "-32"]
-
-  val mk_fresh : unit -> t
-
-  type state
-
-  val get_state : unit -> state
-
-  val set_state : state -> unit
-end
-
-module AbstractAddressSet : PrettyPrintable.PPSet with type elt = AbstractAddress.t
-
-module AbstractAddressMap : PrettyPrintable.PPMap with type key = AbstractAddress.t
-
 module AddrTracePair : sig
-  type t = AbstractAddress.t * ValueHistory.t [@@deriving compare]
+  type t = AbstractValue.t * ValueHistory.t [@@deriving compare]
 end
 
 module Stack : sig
@@ -45,7 +23,7 @@ end
 
 module Memory : sig
   module Access :
-    PrettyPrintable.PrintableOrderedType with type t = AbstractAddress.t HilExp.Access.t
+    PrettyPrintable.PrintableOrderedType with type t = AbstractValue.t HilExp.Access.t
 
   module Edges : PrettyPrintable.PPMap with type key = Access.t
 
@@ -57,43 +35,43 @@ module Memory : sig
 
   type t
 
-  val filter : (AbstractAddress.t -> bool) -> t -> t
+  val filter : (AbstractValue.t -> bool) -> t -> t
 
-  val filter_heap : (AbstractAddress.t -> edges -> bool) -> t -> t
+  val filter_heap : (AbstractValue.t -> edges -> bool) -> t -> t
 
-  val find_opt : AbstractAddress.t -> t -> cell option
+  val find_opt : AbstractValue.t -> t -> cell option
 
-  val fold_attrs : (AbstractAddress.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc
+  val fold_attrs : (AbstractValue.t -> Attributes.t -> 'acc -> 'acc) -> t -> 'acc -> 'acc
 
-  val set_attrs : AbstractAddress.t -> Attributes.t -> t -> t
+  val set_attrs : AbstractValue.t -> Attributes.t -> t -> t
 
-  val set_edges : AbstractAddress.t -> edges -> t -> t
+  val set_edges : AbstractValue.t -> edges -> t -> t
 
-  val set_cell : AbstractAddress.t -> cell -> t -> t
+  val set_cell : AbstractValue.t -> cell -> t -> t
 
-  val find_edges_opt : AbstractAddress.t -> t -> edges option
+  val find_edges_opt : AbstractValue.t -> t -> edges option
 
-  val mem_edges : AbstractAddress.t -> t -> bool
+  val mem_edges : AbstractValue.t -> t -> bool
 
-  val register_address : AbstractAddress.t -> t -> t
+  val register_address : AbstractValue.t -> t -> t
 
-  val add_edge : AbstractAddress.t -> Access.t -> AddrTracePair.t -> t -> t
+  val add_edge : AbstractValue.t -> Access.t -> AddrTracePair.t -> t -> t
 
-  val find_edge_opt : AbstractAddress.t -> Access.t -> t -> AddrTracePair.t option
+  val find_edge_opt : AbstractValue.t -> Access.t -> t -> AddrTracePair.t option
 
-  val add_attribute : AbstractAddress.t -> Attribute.t -> t -> t
+  val add_attribute : AbstractValue.t -> Attribute.t -> t -> t
 
-  val invalidate : AbstractAddress.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
+  val invalidate : AbstractValue.t * ValueHistory.t -> Invalidation.t -> Location.t -> t -> t
 
-  val check_valid : AbstractAddress.t -> t -> (unit, Invalidation.t Trace.t) result
+  val check_valid : AbstractValue.t -> t -> (unit, Invalidation.t Trace.t) result
 
-  val get_closure_proc_name : AbstractAddress.t -> t -> Typ.Procname.t option
+  val get_closure_proc_name : AbstractValue.t -> t -> Typ.Procname.t option
 
-  val get_constant : AbstractAddress.t -> t -> Const.t option
+  val get_constant : AbstractValue.t -> t -> Const.t option
 
-  val std_vector_reserve : AbstractAddress.t -> t -> t
+  val std_vector_reserve : AbstractValue.t -> t -> t
 
-  val is_std_vector_reserved : AbstractAddress.t -> t -> bool
+  val is_std_vector_reserved : AbstractValue.t -> t -> bool
 end
 
 type t = {heap: Memory.t; stack: Stack.t}
@@ -102,7 +80,7 @@ val empty : t
 
 include AbstractDomain.NoJoin with type t := t
 
-val reachable_addresses : t -> AbstractAddressSet.t
+val reachable_addresses : t -> AbstractValue.Set.t
 (** compute the set of abstract addresses that are "used" in the abstract state, i.e. reachable
     from the stack variables *)
 

infer/src/pulse/PulseOperations.ml

@@ -6,7 +6,6 @@
  *)
 open! IStd
 module L = Logging
-module AbstractAddress = PulseDomain.AbstractAddress
 module Memory = PulseAbductiveDomain.Memory
 module Stack = PulseAbductiveDomain.Stack
 open Result.Monad_infix
@@ -91,7 +90,7 @@ module Closures = struct
               let new_trace = ValueHistory.Capture {captured_as; location} :: trace_captured in
               Some (address_captured, new_trace) )
     in
-    let closure_addr_hist = (AbstractAddress.mk_fresh (), [ValueHistory.Assignment location]) in
+    let closure_addr_hist = (AbstractValue.mk_fresh (), [ValueHistory.Assignment location]) in
     let fake_capture_edges = mk_capture_edges captured_addresses in
     let astate =
       Memory.set_cell closure_addr_hist
@@ -144,16 +143,16 @@ let eval location exp0 astate =
         eval exp' astate
     | Const c ->
         (* TODO: make identical const the same address *)
-        let addr = AbstractAddress.mk_fresh () in
+        let addr = AbstractValue.mk_fresh () in
         let astate = Memory.add_attribute addr (Constant c) astate in
         Ok (astate, (addr, []))
     | Sizeof _ | UnOp _ | BinOp _ | Exn _ ->
-        Ok (astate, (AbstractAddress.mk_fresh (), (* TODO history *) []))
+        Ok (astate, (AbstractValue.mk_fresh (), (* TODO history *) []))
   in
   eval exp0 astate
 
 
-type eval_result = EvalConst of Const.t | EvalAddr of AbstractAddress.t
+type eval_result = EvalConst of Const.t | EvalAddr of AbstractValue.t
 
 let eval_to_const location exp astate =
   match (exp : Exp.t) with
@@ -222,14 +221,14 @@ let eval_deref location exp astate =
 
 let realloc_pvar pvar location astate =
   Stack.add (Var.of_pvar pvar)
-    (AbstractAddress.mk_fresh (), [ValueHistory.VariableDeclared (pvar, location)])
+    (AbstractValue.mk_fresh (), [ValueHistory.VariableDeclared (pvar, location)])
     astate
 
 
 let write_id id new_addr_loc astate = Stack.add (Var.of_id id) new_addr_loc astate
 
 let havoc_id id loc_opt astate =
-  if Stack.mem (Var.of_id id) astate then write_id id (AbstractAddress.mk_fresh (), loc_opt) astate
+  if Stack.mem (Var.of_id id) astate then write_id id (AbstractValue.mk_fresh (), loc_opt) astate
   else astate
 
 
@@ -247,11 +246,11 @@ let write_field location addr_trace_ref field addr_trace_obj astate =
 
 
 let havoc_deref location addr_trace trace_obj astate =
-  write_deref location ~ref:addr_trace ~obj:(AbstractAddress.mk_fresh (), trace_obj) astate
+  write_deref location ~ref:addr_trace ~obj:(AbstractValue.mk_fresh (), trace_obj) astate
 
 
 let havoc_field location addr_trace field trace_obj astate =
-  write_field location addr_trace field (AbstractAddress.mk_fresh (), trace_obj) astate
+  write_field location addr_trace field (AbstractValue.mk_fresh (), trace_obj) astate
 
 
 let invalidate location cause addr_trace astate =
@@ -290,7 +289,7 @@ let shallow_copy location addr_hist astate =
     | Some cell ->
         cell
   in
-  let copy = (AbstractAddress.mk_fresh (), [ValueHistory.Assignment location]) in
+  let copy = (AbstractValue.mk_fresh (), [ValueHistory.Assignment location]) in
   (Memory.set_cell copy cell location astate, copy)
 
 
@@ -298,7 +297,7 @@ let check_address_escape escape_location proc_desc address history astate =
   let is_assigned_to_global address astate =
     let points_to_address pointer address astate =
       Memory.find_edge_opt pointer Dereference astate
-      |> Option.exists ~f:(fun (pointee, _) -> AbstractAddress.equal pointee address)
+      |> Option.exists ~f:(fun (pointee, _) -> AbstractValue.equal pointee address)
     in
     Stack.exists
       (fun var (pointer, _) -> Var.is_global var && points_to_address pointer address astate)
@@ -324,13 +323,13 @@ let check_address_escape escape_location proc_desc address history astate =
     IContainer.iter_result ~fold:(IContainer.fold_of_pervasives_map_fold ~fold:Stack.fold) astate
       ~f:(fun (variable, (var_address, _)) ->
         if
-          AbstractAddress.equal var_address address
+          AbstractValue.equal var_address address
           && ( Var.is_cpp_temporary variable
              || Var.is_local_to_procedure proc_name variable
                 && not (Procdesc.is_captured_var proc_desc variable) )
         then (
           L.d_printfln_escaped "Stack variable address &%a detected at address %a" Var.pp variable
-            AbstractAddress.pp address ;
+            AbstractValue.pp address ;
           Error
             (PulseDiagnostic.StackVariableAddressEscape
                {variable; location= escape_location; history}) )

infer/src/pulse/PulseOperations.mli

@@ -6,7 +6,6 @@
  *)
 
 open! IStd
-module AbstractAddress = PulseDomain.AbstractAddress
 open PulseBasicInterface
 
 type t = PulseAbductiveDomain.t
@@ -15,7 +14,7 @@ type 'a access_result = ('a, PulseDiagnostic.t) result
 
 module Closures : sig
   val check_captured_addresses :
-    Location.t -> AbstractAddress.t -> t -> (t, PulseDiagnostic.t) result
+    Location.t -> AbstractValue.t -> t -> (t, PulseDiagnostic.t) result
   (** assert the validity of the addresses captured by the lambda *)
 end
 
@@ -86,20 +85,20 @@ val shallow_copy :
      Location.t
   -> PulseDomain.AddrTracePair.t
   -> t
-  -> (t * (AbstractAddress.t * ValueHistory.t)) access_result
+  -> (t * (AbstractValue.t * ValueHistory.t)) access_result
 (** returns the address of a new cell with the same edges as the original *)
 
 val remove_vars : Var.t list -> Location.t -> t -> t
 
 val check_address_escape :
-  Location.t -> Procdesc.t -> AbstractAddress.t -> ValueHistory.t -> t -> t access_result
+  Location.t -> Procdesc.t -> AbstractValue.t -> ValueHistory.t -> t -> t access_result
 
 val call :
      caller_summary:Summary.t
   -> Location.t
   -> Typ.Procname.t
   -> ret:Ident.t * Typ.t
-  -> actuals:((AbstractAddress.t * ValueHistory.t) * Typ.t) list
+  -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
   -> t
   -> t list access_result
 (** perform an interprocedural call: apply the summary for the call proc name passed as argument if