[pulse][interproc 1/3] save/restore fresh abstract address generator across ondemand calls

Summary:
This is in preparation of interprocedural pulse. The abstract addresses
generator keeps a reference to create fresh addresses, but that's a
piece of global state that needs to persist across ondemand analyses.

Reviewed By: jberdine

Differential Revision: D14324760

fbshipit-source-id: 5cdb1d3f5

infer/src/backend/ondemand.ml

@@ -80,6 +80,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
   ; symexec_state: State.t }
 
 let save_global_state () =
@@ -94,6 +95,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 ()
   ; symexec_state= State.save_state () }
 
 
@@ -104,6 +106,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 ;
   State.restore_state st.symexec_state ;
   current_taskbar_status :=
     Option.map st.proc_analysis_time ~f:(fun (suspended_span, status) ->

infer/src/pulse/PulseDomain.ml

@@ -57,6 +57,12 @@ module AbstractAddress : sig
   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]
 
@@ -72,6 +78,12 @@ end = struct
   let pp = F.pp_print_int
 
   let init () = next_fresh := 1
+
+  type state = int
+
+  let get_state () = !next_fresh
+
+  let set_state counter = next_fresh := counter
 end
 
 (* {3 Heap domain } *)

infer/src/pulse/PulseDomain.mli

@@ -27,6 +27,12 @@ module AbstractAddress : sig
   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 Stack : sig