split off parts of State unrelated to biabduction

Summary:
`State` is used by the AI framework, which isn't supposed to know about
biabduction/. Split the biabduction-specific parts into
biabduction/State.ml and keep the rest in absint/AnalysisState.ml.

Reviewed By: ngorogiannis

Differential Revision: D21257470

fbshipit-source-id: e01d1fed3

infer/src/absint/AbstractInterpreter.ml

@@ -8,7 +8,6 @@
 open! IStd
 module F = Format
 module L = Logging
-module AnalysisState = State
 
 type exec_node_schedule_result = ReachedFixPoint | DidNotReachFixPoint
 

infer/src/absint/AnalysisState.ml

@@ -0,0 +1,60 @@
+(*
+ * Copyright (c) 2009-2013, Monoidics ltd.
+ * 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
+
+(** State of symbolic execution *)
+
+type t =
+  { mutable last_instr: Sil.instr option  (** Last instruction seen *)
+  ; mutable last_node: Procdesc.Node.t option  (** Last node seen *)
+  ; mutable last_session: int  (** Last session seen *) }
+
+let initial () = {last_instr= None; last_node= None; last_session= 0}
+
+(** Global state *)
+let gs = ref (initial ())
+
+let get_instr () = !gs.last_instr
+
+let set_instr instr = !gs.last_instr <- Some instr
+
+let get_node_exn () = Option.value_exn !gs.last_node
+
+let get_node () = !gs.last_node
+
+let set_node (node : Procdesc.Node.t) =
+  !gs.last_instr <- None ;
+  !gs.last_node <- Some node
+
+
+let get_session () = !gs.last_session
+
+let set_session (session : int) = !gs.last_session <- session
+
+let get_loc_exn () =
+  match !gs.last_instr with
+  | Some instr ->
+      Sil.location_of_instr instr
+  | None ->
+      get_node_exn () |> Procdesc.Node.get_loc
+
+
+let get_loc () =
+  match !gs.last_instr with Some instr -> Some (Sil.location_of_instr instr) | None -> None
+
+
+(** Return the old state, and revert the current state to the initial one. *)
+let save () =
+  let old = !gs in
+  gs := initial () ;
+  old
+
+
+(** Restore the old state. *)
+let restore st = gs := st

infer/src/absint/AnalysisState.mli

@@ -0,0 +1,48 @@
+(*
+ * Copyright (c) 2009-2013, Monoidics ltd.
+ * 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
+
+(** State of symbolic execution *)
+
+type t
+
+val get_instr : unit -> Sil.instr option
+(** Get last instruction seen in symbolic execution *)
+
+val get_loc_exn : unit -> Location.t
+(** Get last location seen in symbolic execution *)
+
+val get_loc : unit -> Location.t option
+(** Get last location seen in symbolic execution *)
+
+val get_node_exn : unit -> Procdesc.Node.t
+(** Get last node seen in symbolic execution *)
+
+val get_node : unit -> Procdesc.Node.t option
+(** Get last node seen in symbolic execution *)
+
+val get_session : unit -> int
+(** Get last session seen in symbolic execution *)
+
+val set_instr : Sil.instr -> unit
+(** Set last instruction seen in symbolic execution *)
+
+val set_node : Procdesc.Node.t -> unit
+(** Set last node seen in symbolic execution *)
+
+val set_session : int -> unit
+(** Set last session seen in symbolic execution *)
+
+(** {2 State management} *)
+
+val restore : t -> unit
+(** Restore the old state. *)
+
+val save : unit -> t
+(** Return the old state, and revert the current state to the initial one. *)

infer/src/absint/exe_env.ml

@@ -107,11 +107,11 @@ let get_column_value ~value_on_java ~file_data_to_value ~column_name exe_env pro
       | Some v ->
           v
       | None ->
-          let loc_opt = State.get_loc () in
+          let loc_opt = AnalysisState.get_loc () in
           L.die InternalError "get_column_value: %s not found for %a%a" column_name Procname.pp
             proc_name pp_loc_opt loc_opt )
     | None ->
-        let loc_opt = State.get_loc () in
+        let loc_opt = AnalysisState.get_loc () in
         L.die InternalError "get_column_value: file_data not found for %a%a" Procname.pp proc_name
           pp_loc_opt loc_opt )
 

infer/src/backend/errdesc.ml

@@ -453,9 +453,9 @@ let find_typ_without_ptr prop pvar =
     variable nullify, blame the variable. If it is an abstraction, blame any variable nullify at the
     current node. If there is an alloc attribute, print the function call and line number. *)
 let explain_leak tenv hpred prop alloc_att_opt bucket =
-  let instro = State.get_instr () in
-  let loc = State.get_loc_exn () in
-  let node = State.get_node_exn () in
+  let instro = AnalysisState.get_instr () in
+  let loc = AnalysisState.get_loc_exn () in
+  let node = AnalysisState.get_node_exn () in
   let node_instrs = Procdesc.Node.get_instrs node in
   let hpred_typ_opt = find_hpred_typ hpred in
   let value_str_from_pvars_vpath pvars vpath =
@@ -503,7 +503,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
           L.d_str "explain_leak: current instruction is Nullify for pvar " ;
           Pvar.d pvar ;
           L.d_ln () ) ;
-        match exp_lv_dexp tenv (State.get_node_exn ()) (Exp.Lvar pvar) with
+        match exp_lv_dexp tenv (AnalysisState.get_node_exn ()) (Exp.Lvar pvar) with
         | Some de when not (DExp.has_tmp_var de) ->
             Some (DExp.to_string de)
         | _ ->
@@ -944,7 +944,7 @@ let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = fa
     ?(outermost_dereference = false) ?(is_nullable = false) ?(is_premature_nil = false) deref_str
     prop loc =
   let find_exp_dereferenced () =
-    match State.get_instr () with
+    match AnalysisState.get_instr () with
     | Some (Sil.Store {e1= e}) ->
         if verbose then (
           L.d_str "explain_dereference Sil.Store " ;
@@ -974,7 +974,7 @@ let explain_access_ proc_name tenv ?(use_buckets = false) ?(outermost_array = fa
     | _ ->
         None
   in
-  let node = State.get_node_exn () in
+  let node = AnalysisState.get_node_exn () in
   match find_exp_dereferenced () with
   | None ->
       if verbose then L.d_strln "_explain_access: find_exp_dereferenced returned None" ;
@@ -1026,9 +1026,9 @@ let dexp_apply_pvar_off dexp pvar_off =
 (** Produce a description of the nth parameter of the function call, if the current instruction is a
     function call with that parameter *)
 let explain_nth_function_parameter proc_name tenv use_buckets deref_str prop n pvar_off =
-  let node = State.get_node_exn () in
-  let loc = State.get_loc_exn () in
-  match State.get_instr () with
+  let node = AnalysisState.get_node_exn () in
+  let loc = AnalysisState.get_loc_exn () in
+  match AnalysisState.get_instr () with
   | Some (Sil.Call (_, _, args, _, _)) -> (
     try
       let arg = fst (List.nth_exn args (n - 1)) in

infer/src/backend/ondemand.ml

@@ -97,7 +97,8 @@ type global_state =
   ; proc_analysis_time: (Mtime.Span.t * string) option
         (** the time elapsed doing [status] so far *)
   ; pulse_address_generator: PulseAbstractValue.State.t
-  ; symexec_state: State.t }
+  ; absint_state: AnalysisState.t
+  ; biabduction_state: State.t }
 
 let save_global_state () =
   Timeout.suspend_existing_timeout ~keep_symop_total:false ;
@@ -112,7 +113,8 @@ let save_global_state () =
       Option.map !current_taskbar_status ~f:(fun (t0, status) ->
           (Mtime.span t0 (Mtime_clock.now ()), status) )
   ; pulse_address_generator= PulseAbstractValue.State.get ()
-  ; symexec_state= State.save_state () }
+  ; absint_state= AnalysisState.save ()
+  ; biabduction_state= State.save_state () }
 
 
 let restore_global_state st =
@@ -123,7 +125,8 @@ let restore_global_state st =
   Printer.curr_html_formatter := st.html_formatter ;
   Ident.NameGenerator.set_current st.name_generator ;
   PulseAbstractValue.State.set st.pulse_address_generator ;
-  State.restore_state st.symexec_state ;
+  AnalysisState.restore st.absint_state ;
+  State.restore_state st.biabduction_state ;
   current_taskbar_status :=
     Option.map st.proc_analysis_time ~f:(fun (suspended_span, status) ->
         (* forget about the time spent doing a nested analysis and resend the status of the outer

infer/src/biabduction/Abs.ml

@@ -990,7 +990,7 @@ let check_observer_is_unsubscribed_deallocation tenv prop e =
     | _ ->
         None
   in
-  let loc = State.get_loc_exn () in
+  let loc = AnalysisState.get_loc_exn () in
   match Attribute.get_observer tenv prop e with
   | Some (Apred (Aobserver, _)) -> (
     match pvar_opt with

infer/src/biabduction/BiabductionReporting.ml

@@ -13,11 +13,11 @@ let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn =
     match Summary.OnDisk.get proc_name with
     | Some summary ->
         let node =
-          let node = match node with None -> State.get_node_exn () | Some node -> node in
+          let node = match node with None -> AnalysisState.get_node_exn () | Some node -> node in
           Errlog.BackendNode {node}
         in
-        let session = State.get_session () in
-        let loc = match loc with None -> State.get_loc_exn () | Some loc -> loc in
+        let session = AnalysisState.get_session () in
+        let loc = match loc with None -> AnalysisState.get_loc_exn () | Some loc -> loc in
         let ltr = match ltr with None -> State.get_loc_trace () | Some ltr -> ltr in
         Reporting.log_issue_from_summary severity (Summary.get_attributes summary)
           summary.Summary.err_log ~node ~session ~loc ~ltr exn
@@ -31,11 +31,13 @@ let log_issue_deprecated_using_state severity proc_name ?node ?loc ?ltr exn =
 let log_error_using_state proc_desc err_log exn =
   if !BiabductionConfig.footprint then
     let node' =
-      match State.get_node () with Some n -> n | None -> Procdesc.get_start_node proc_desc
+      match AnalysisState.get_node () with Some n -> n | None -> Procdesc.get_start_node proc_desc
     in
     let node = Errlog.BackendNode {node= node'} in
-    let session = State.get_session () in
-    let loc = match State.get_loc () with Some l -> l | None -> Procdesc.Node.get_loc node' in
+    let session = AnalysisState.get_session () in
+    let loc =
+      match AnalysisState.get_loc () with Some l -> l | None -> Procdesc.Node.get_loc node'
+    in
     let ltr = State.get_loc_trace () in
     let attrs = Procdesc.get_attributes proc_desc in
     Reporting.log_issue_from_summary Exceptions.Error attrs err_log ~node ~session ~loc ~ltr exn

infer/src/biabduction/BuiltinDefn.ml

@@ -32,7 +32,7 @@ let mk_empty_array len = Predicates.Earray (len, [], Predicates.inst_none)
    return a null pointer deref *)
 let mk_empty_array_rearranged len =
   Predicates.Earray
-    (len, [], Predicates.inst_rearrange true (State.get_loc_exn ()) (State.get_path_pos ()))
+    (len, [], Predicates.inst_rearrange true (AnalysisState.get_loc_exn ()) (State.get_path_pos ()))
 
 
 let extract_array_type typ =

infer/src/biabduction/Prover.ml

@@ -835,7 +835,7 @@ let check_atom tenv prop a0 =
   if Config.smt_output then (
     let key = get_smt_key a prop_no_fp in
     let key_filename =
-      let source = (State.get_loc_exn ()).file in
+      let source = (AnalysisState.get_loc_exn ()).file in
       DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source) [key ^ ".cns"]
     in
     let outc = Out_channel.create (DB.filename_to_string key_filename) in

infer/src/biabduction/Rearrange.ml

@@ -136,7 +136,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
         | [] ->
             ([], Predicates.Earray (len, [], inst), t)
         | Predicates.Off_index e :: off' ->
-            bounds_check tenv pname orig_prop len e (State.get_loc_exn ()) ;
+            bounds_check tenv pname orig_prop len e (AnalysisState.get_loc_exn ()) ;
             let atoms', se', res_t' =
               create_struct_values pname tenv orig_prop footprint_part kind max_stamp t' off' inst
             in
@@ -263,7 +263,7 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp
   | ( Off_index e :: off'
     , Predicates.Earray (len, esel, inst_arr)
     , Tarray {elt= typ'; length= len_for_typ'; stride} ) -> (
-      bounds_check tenv pname orig_prop len e (State.get_loc_exn ()) ;
+      bounds_check tenv pname orig_prop len e (AnalysisState.get_loc_exn ()) ;
       match List.find ~f:(fun (e', _) -> Exp.equal e e') esel with
       | Some (_, se') ->
           let atoms_se_typ_list' =
@@ -444,7 +444,7 @@ let mk_ptsto_exp_footprint pname tenv orig_prop (lexp, typ) max_stamp inst :
       L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp ;
       let deref_str = Localise.deref_str_dangling None in
       let err_desc =
-        Errdesc.explain_dereference pname tenv deref_str orig_prop (State.get_loc_exn ())
+        Errdesc.explain_dereference pname tenv deref_str orig_prop (AnalysisState.get_loc_exn ())
       in
       raise (Exceptions.Dangling_pointer_dereference (false, err_desc, __POS__)) ) ;
   let off_foot, eqs = laundry_offset_for_footprint max_stamp off in
@@ -986,7 +986,7 @@ let check_type_size tenv pname prop texp off typ_from_instr =
         && not (Prover.check_type_size_leq typ_from_instr typ_of_object)
       then
         let deref_str = Localise.deref_str_pointer_size_mismatch typ_from_instr typ_of_object in
-        let loc = State.get_loc_exn () in
+        let loc = AnalysisState.get_loc_exn () in
         let exn =
           Exceptions.Pointer_size_mismatch
             (Errdesc.explain_dereference pname tenv deref_str prop loc, __POS__)
@@ -1254,7 +1254,9 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc =
   match attribute_opt with
   | Some (Apred (Adangling dk, _)) ->
       let deref_str = Localise.deref_str_dangling (Some dk) in
-      let err_desc = Errdesc.explain_dereference pname tenv deref_str prop (State.get_loc_exn ()) in
+      let err_desc =
+        Errdesc.explain_dereference pname tenv deref_str prop (AnalysisState.get_loc_exn ())
+      in
       raise (Exceptions.Dangling_pointer_dereference (true, err_desc, __POS__))
   | Some (Apred (Aundef _, _)) ->
       ()
@@ -1294,7 +1296,7 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc =
     (* when e is a temp var, try to find the pvar defining e*)
     match e with
     | Exp.Var id -> (
-      match Errdesc.find_ident_assignment (State.get_node_exn ()) id with
+      match Errdesc.find_ident_assignment (AnalysisState.get_node_exn ()) id with
       | Some (_, e') ->
           e'
       | None ->
@@ -1304,9 +1306,9 @@ let check_call_to_objc_block_error tenv pdesc prop fun_exp loc =
   in
   let get_exp_called () =
     (* Exp called in the block's function call*)
-    match State.get_instr () with
+    match AnalysisState.get_instr () with
     | Some (Sil.Call (_, Var id, _, _, _)) ->
-        Errdesc.find_ident_assignment (State.get_node_exn ()) id
+        Errdesc.find_ident_assignment (AnalysisState.get_node_exn ()) id
     | _ ->
         None
   in
@@ -1384,7 +1386,8 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc :
   Prop.d_prop prop ;
   L.d_ln () ;
   L.d_ln () ;
-  if report_deref_errors then check_dereference_error tenv pdesc prop nlexp (State.get_loc_exn ()) ;
+  if report_deref_errors then
+    check_dereference_error tenv pdesc prop nlexp (AnalysisState.get_loc_exn ()) ;
   let pname = Procdesc.get_proc_name pdesc in
   match Prop.prop_iter_create prop with
   | None ->

infer/src/biabduction/RetainCycles.ml

@@ -12,7 +12,7 @@ let desc_retain_cycle tenv (cycle : RetainCyclesType.t) =
   Logging.d_strln "Proposition with retain cycle:" ;
   let do_edge index_ edge =
     let index = index_ + 1 in
-    let node = State.get_node_exn () in
+    let node = AnalysisState.get_node_exn () in
     let from_exp_str edge_obj =
       let type_str =
         let typ_str = Typ.to_string edge_obj.rc_from.rc_node_typ in
@@ -230,7 +230,9 @@ let exn_retain_cycle tenv cycle =
     Utils.create_dir rc_dotty_dir ;
     let rc_dotty_file = Filename.temp_file ~in_dir:rc_dotty_dir "rc" ".dot" in
     RetainCyclesType.write_dotty_to_file rc_dotty_file cycle ) ;
-  let desc = Localise.desc_retain_cycle retain_cycle (State.get_loc_exn ()) (Some cycle_dotty) in
+  let desc =
+    Localise.desc_retain_cycle retain_cycle (AnalysisState.get_loc_exn ()) (Some cycle_dotty)
+  in
   Exceptions.Retain_cycle (desc, __POS__)
 
 

infer/src/biabduction/State.ml

@@ -30,22 +30,16 @@ type t =
         (** Diverging states since the last reset for the node *)
   ; mutable diverging_states_proc: Paths.PathSet.t
         (** Diverging states since the last reset for the procedure *)
-  ; mutable last_instr: Sil.instr option  (** Last instruction seen *)
-  ; mutable last_node: Procdesc.Node.t option  (** Last node seen *)
   ; mutable last_path: (Paths.Path.t * PredSymb.path_pos option) option  (** Last path seen *)
   ; mutable last_prop_tenv_pdesc: (Prop.normal Prop.t * Tenv.t * Procdesc.t) option
         (** Last prop,tenv,pdesc seen *)
-  ; mutable last_session: int  (** Last session seen *)
   ; failure_map: failure_stats NodeHash.t  (** Map visited nodes to failure statistics *) }
 
 let initial () =
   { diverging_states_node= Paths.PathSet.empty
   ; diverging_states_proc= Paths.PathSet.empty
-  ; last_instr= None
-  ; last_node= None
   ; last_path= None
   ; last_prop_tenv_pdesc= None
-  ; last_session= 0
   ; failure_map= NodeHash.create 1 }
 
 
@@ -83,24 +77,6 @@ let get_diverging_states_node () = !gs.diverging_states_node
 
 let get_diverging_states_proc () = !gs.diverging_states_proc
 
-let get_instr () = !gs.last_instr
-
-let get_node_exn () = Option.value_exn !gs.last_node
-
-let get_node () = !gs.last_node
-
-let get_loc_exn () =
-  match !gs.last_instr with
-  | Some instr ->
-      Sil.location_of_instr instr
-  | None ->
-      get_node_exn () |> Procdesc.Node.get_loc
-
-
-let get_loc () =
-  match !gs.last_instr with Some instr -> Some (Sil.location_of_instr instr) | None -> None
-
-
 (** normalize the list of instructions by renaming let-bound ids *)
 let instrs_normalize instrs =
   let bound_ids =
@@ -166,14 +142,14 @@ let mk_find_duplicate_nodes : Procdesc.t -> Procdesc.Node.t -> Procdesc.NodeSet.
 
 
 let get_inst_update pos =
-  let loc = get_loc_exn () in
+  let loc = AnalysisState.get_loc_exn () in
   Predicates.inst_update loc pos
 
 
 let get_path () =
   match !gs.last_path with
   | None ->
-      (Paths.Path.start (get_node_exn ()), None)
+      (Paths.Path.start (AnalysisState.get_node_exn ()), None)
   | Some (path, pos_opt) ->
       (path, pos_opt)
 
@@ -215,8 +191,6 @@ let get_normalized_pre (abstract_fun : Tenv.t -> Prop.normal Prop.t -> Prop.norm
       Some (extract_pre prop tenv pdesc abstract_fun)
 
 
-let get_session () = !gs.last_session
-
 let get_path_pos () =
   let pname =
     match get_prop_tenv_pdesc () with
@@ -225,7 +199,7 @@ let get_path_pos () =
     | None ->
         Procname.from_string_c_fun "unknown_procedure"
   in
-  let nid = Procdesc.Node.get_id (get_node_exn ()) in
+  let nid = Procdesc.Node.get_id (AnalysisState.get_node_exn ()) in
   (pname, (nid :> int))
 
 
@@ -244,14 +218,14 @@ let mark_execution_end node =
 
 
 let mark_instr_ok () =
-  let fs = get_failure_stats (get_node_exn ()) in
+  let fs = get_failure_stats (AnalysisState.get_node_exn ()) in
   fs.instr_ok <- fs.instr_ok + 1
 
 
 let mark_instr_fail exn =
-  let loc = get_loc_exn () in
-  let node = get_node_exn () in
-  let session = get_session () in
+  let loc = AnalysisState.get_loc_exn () in
+  let node = AnalysisState.get_node_exn () in
+  let session = AnalysisState.get_session () in
   let loc_trace = get_loc_trace () in
   let fs = get_failure_stats node in
   if is_none fs.first_failure then
@@ -277,15 +251,6 @@ let process_execution_failures (log_issue : log_issue) pname =
   NodeHash.iter do_failure !gs.failure_map
 
 
-let set_instr (instr : Sil.instr) = !gs.last_instr <- Some instr
-
 let set_path path pos_opt = !gs.last_path <- Some (path, pos_opt)
 
 let set_prop_tenv_pdesc prop tenv pdesc = !gs.last_prop_tenv_pdesc <- Some (prop, tenv, pdesc)
-
-let set_node (node : Procdesc.Node.t) =
-  !gs.last_instr <- None ;
-  !gs.last_node <- Some node
-
-
-let set_session (session : int) = !gs.last_session <- session

infer/src/biabduction/State.mli

@@ -25,24 +25,9 @@ val get_diverging_states_proc : unit -> Paths.PathSet.t
 val get_inst_update : PredSymb.path_pos -> Predicates.inst
 (** Get update instrumentation for the current loc *)
 
-val get_instr : unit -> Sil.instr option
-(** Get last instruction seen in symbolic execution *)
-
-val get_loc_exn : unit -> Location.t
-(** Get last location seen in symbolic execution *)
-
-val get_loc : unit -> Location.t option
-(** Get last location seen in symbolic execution *)
-
 val get_loc_trace : unit -> Errlog.loc_trace
 (** Get the location trace of the last path seen in symbolic execution *)
 
-val get_node_exn : unit -> Procdesc.Node.t
-(** Get last node seen in symbolic execution *)
-
-val get_node : unit -> Procdesc.Node.t option
-(** Get last node seen in symbolic execution *)
-
 val get_normalized_pre :
   (Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t) -> Prop.normal Prop.t option
 (** return the normalized precondition extracted form the last prop seen, if any the abstraction
@@ -57,9 +42,6 @@ val get_path_pos : unit -> PredSymb.path_pos
 val get_prop_tenv_pdesc : unit -> (Prop.normal Prop.t * Tenv.t * Procdesc.t) option
 (** Get last last prop,tenv,pdesc seen in symbolic execution *)
 
-val get_session : unit -> int
-(** Get last session seen in symbolic execution *)
-
 val mark_execution_end : Procdesc.Node.t -> unit
 (** Mark the end of symbolic execution of a node *)
 
@@ -94,17 +76,8 @@ val restore_state : t -> unit
 val save_state : unit -> t
 (** Return the old state, and revert the current state to the initial one. *)
 
-val set_instr : Sil.instr -> unit
-(** Set last instruction seen in symbolic execution *)
-
-val set_node : Procdesc.Node.t -> unit
-(** Set last node seen in symbolic execution *)
-
 val set_path : Paths.Path.t -> PredSymb.path_pos option -> unit
 (** Get last path seen in symbolic execution *)
 
 val set_prop_tenv_pdesc : Prop.normal Prop.t -> Tenv.t -> Procdesc.t -> unit
 (** Set last prop,tenv,pdesc seen in symbolic execution *)
-
-val set_session : int -> unit
-(** Set last session seen in symbolic execution *)

infer/src/biabduction/SymExec.ml

@@ -405,7 +405,8 @@ let check_arith_norm_exp tenv pname exp prop =
   match Attribute.find_arithmetic_problem tenv (State.get_path_pos ()) prop exp with
   | Some (Attribute.Div0 div), prop' ->
       let desc =
-        Errdesc.explain_divide_by_zero tenv div (State.get_node_exn ()) (State.get_loc_exn ())
+        Errdesc.explain_divide_by_zero tenv div (AnalysisState.get_node_exn ())
+          (AnalysisState.get_loc_exn ())
       in
       let exn = Exceptions.Divide_by_zero (desc, __POS__) in
       BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ;
@@ -413,7 +414,7 @@ let check_arith_norm_exp tenv pname exp prop =
   | Some (Attribute.UminusUnsigned (e, typ)), prop' ->
       let desc =
         Errdesc.explain_unary_minus_applied_to_unsigned_expression tenv e typ
-          (State.get_node_exn ()) (State.get_loc_exn ())
+          (AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ())
       in
       let exn = Exceptions.Unary_minus_applied_to_unsigned_expression (desc, __POS__) in
       BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn ;
@@ -470,8 +471,8 @@ let check_already_dereferenced tenv pname cond prop =
   match dereferenced_line with
   | Some (id, (n, _)) ->
       let desc =
-        Errdesc.explain_null_test_after_dereference tenv (Exp.Var id) (State.get_node_exn ()) n
-          (State.get_loc_exn ())
+        Errdesc.explain_null_test_after_dereference tenv (Exp.Var id)
+          (AnalysisState.get_node_exn ()) n (AnalysisState.get_loc_exn ())
       in
       let exn = Exceptions.Null_test_after_dereference (desc, __POS__) in
       BiabductionReporting.log_issue_deprecated_using_state Exceptions.Warning pname exn
@@ -1174,7 +1175,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
     (Prop.normal Prop.t * Paths.Path.t) list =
   let current_pdesc = Summary.get_proc_desc current_summary in
   let current_pname = Procdesc.get_proc_name current_pdesc in
-  State.set_instr instr_ ;
+  AnalysisState.set_instr instr_ ;
   (* mark instruction last seen *)
   State.set_prop_tenv_pdesc prop_ tenv current_pdesc ;
   (* mark prop,tenv,pdesc last seen *)
@@ -1264,7 +1265,7 @@ let rec sym_exec exe_env tenv current_summary instr_ (prop_ : Prop.normal Prop.t
           in
           match Prop.exp_normalize_prop tenv Prop.prop_emp cond with
           | Exp.Const (Const.Cint i) when report_condition_always_true_false i ->
-              let node = State.get_node_exn () in
+              let node = AnalysisState.get_node_exn () in
               let desc = Errdesc.explain_condition_always_true_false tenv i cond node loc in
               let exn =
                 Exceptions.Condition_always_true_false (desc, not (IntLit.iszero i), __POS__)
@@ -1824,7 +1825,7 @@ and proc_call exe_env callee_summary
     | (e, t_e) :: etl', _ :: tl' ->
         (e, t_e) :: comb etl' tl'
     | _, [] ->
-        Errdesc.warning_err (State.get_loc_exn ())
+        Errdesc.warning_err (AnalysisState.get_loc_exn ())
           "likely use of variable-arguments function, or function prototype missing@." ;
         L.d_warning "likely use of variable-arguments function, or function prototype missing" ;
         L.d_ln () ;
@@ -1917,7 +1918,7 @@ and sym_exec_wrapper exe_env handle_exn tenv summary proc_cfg instr
         let instr_is_abstraction = function Sil.Metadata (Abstract _) -> true | _ -> false in
         Instrs.exists ~f:instr_is_abstraction (ProcCfg.Exceptional.instrs node)
       in
-      let curr_node = State.get_node_exn () in
+      let curr_node = AnalysisState.get_node_exn () in
       match ProcCfg.Exceptional.Node.kind curr_node with
       | Procdesc.Node.Prune_node _ when not (node_has_abstraction curr_node) ->
           (* don't check for leaks in prune nodes, unless there is abstraction anyway,*)

infer/src/biabduction/Tabulation.ml

@@ -302,7 +302,8 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo
     let desc use_buckets deref_str =
       let error_desc =
         Errdesc.explain_dereference_as_caller_expression caller_pname tenv ~use_buckets deref_str
-          actual_pre spec_pre e (State.get_node_exn ()) (State.get_loc_exn ()) formal_params
+          actual_pre spec_pre e (AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ())
+          formal_params
       in
       L.d_strln ~color:Red "found error in dereference" ;
       L.d_strln "spec_pre:" ;
@@ -392,7 +393,8 @@ let check_path_errors_in_post tenv caller_pname post post_path =
     | Predicates.Apred (Adiv0 path_pos, [e]) ->
         if Prover.check_zero tenv e then (
           let desc =
-            Errdesc.explain_divide_by_zero tenv e (State.get_node_exn ()) (State.get_loc_exn ())
+            Errdesc.explain_divide_by_zero tenv e (AnalysisState.get_node_exn ())
+              (AnalysisState.get_loc_exn ())
           in
           let new_path, path_pos_opt =
             let current_path, _ = State.get_path () in
@@ -989,8 +991,8 @@ let inconsistent_actualpre_missing tenv actual_pre split_opt =
 
 let class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc =
   let desc =
-    Errdesc.explain_class_cast_exception tenv pname_opt texp1 texp2 exp (State.get_node_exn ())
-      (State.get_loc_exn ())
+    Errdesc.explain_class_cast_exception tenv pname_opt texp1 texp2 exp
+      (AnalysisState.get_node_exn ()) (AnalysisState.get_loc_exn ())
   in
   Exceptions.Class_cast_exception (desc, ml_loc)
 

infer/src/biabduction/Timeout.ml

@@ -117,6 +117,6 @@ let exe_timeout f x =
         None )
       ~finally:resume_previous_timeout
   with SymOp.Analysis_failure_exe kind ->
-    let loc = State.get_loc () |> Option.value ~default:Location.dummy in
+    let loc = AnalysisState.get_loc () |> Option.value ~default:Location.dummy in
     Errdesc.warning_err loc "TIMEOUT: %a@." SymOp.pp_failure_kind kind ;
     Some kind

infer/src/biabduction/interproc.ml

@@ -265,7 +265,7 @@ let propagate (wl : Worklist.t) pname ~is_exception (pset : Paths.PathSet.t)
     let f prop path edgeset_curr =
       let exn_opt = if is_exception then Tabulation.prop_get_exn_name pname prop else None in
       Paths.PathSet.add_renamed_prop prop
-        (Paths.Path.extend curr_node exn_opt (State.get_session ()) path)
+        (Paths.Path.extend curr_node exn_opt (AnalysisState.get_session ()) path)
         edgeset_curr
     in
     Paths.PathSet.fold f pset Paths.PathSet.empty
@@ -283,7 +283,7 @@ let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : P
     !BiabductionConfig.footprint
     && not (Paths.PathSet.is_empty (State.get_diverging_states_node ()))
   then (
-    Errdesc.warning_err (State.get_loc_exn ()) "Propagating Divergence@." ;
+    Errdesc.warning_err (AnalysisState.get_loc_exn ()) "Propagating Divergence@." ;
     let exit_node = ProcCfg.Exceptional.exit_node proc_cfg in
     let diverging_states = State.get_diverging_states_node () in
     let prop_incons =
@@ -356,8 +356,8 @@ exception RE_EXE_ERROR
 let pp_name fmt = F.pp_print_string fmt "interproc"
 
 let do_before_node session node =
-  State.set_node node ;
-  State.set_session session ;
+  AnalysisState.set_node node ;
+  AnalysisState.set_session session ;
   L.reset_delayed_prints () ;
   Printer.node_start_session ~pp_name node (session :> int)
 
@@ -416,7 +416,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
     | None ->
         () ) ;
     L.d_strln "SIL INSTR:" ;
-    Procdesc.Node.d_instrs ~highlight:(State.get_instr ()) curr_node ;
+    Procdesc.Node.d_instrs ~highlight:(AnalysisState.get_instr ()) curr_node ;
     L.d_ln () ;
     BiabductionReporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;
     State.mark_instr_fail exn
@@ -442,7 +442,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
     L.d_increase_indent () ;
     Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv pathset_todo) ;
     L.d_strln ".... Instructions: ...." ;
-    Procdesc.Node.d_instrs ~highlight:(State.get_instr ()) curr_node ;
+    Procdesc.Node.d_instrs ~highlight:(AnalysisState.get_instr ()) curr_node ;
     L.d_ln () ;
     L.d_ln ()
   in

infer/src/nullsafe/eradicate.ml

@@ -53,7 +53,7 @@ let callback1 tenv find_canonical_duplicate calls_this checks idenv curr_pname c
     let ret_implicitly_nullable =
       String.equal (PatternMatch.get_type_name ret_annotated_type.typ) "java.lang.Void"
     in
-    State.set_node exit_node ;
+    AnalysisState.set_node exit_node ;
     if not (List.is_empty checks.TypeCheck.check_ret_type) then
       List.iter
         ~f:(fun f -> f curr_pname curr_pdesc ret_annotated_type.typ typ_found_opt loc)
@@ -81,7 +81,7 @@ let callback1 tenv find_canonical_duplicate calls_this checks idenv curr_pname c
 
     let do_node tenv node typestate =
       NodePrinter.with_session ~pp_name node ~f:(fun () ->
-          State.set_node node ;
+          AnalysisState.set_node node ;
           if Config.write_html then L.d_printfln "before:@\n%a@\n" TypeState.pp typestate ;
           let TypeCheck.{normal_flow_typestate; exception_flow_typestates} =
             TypeCheck.typecheck_node tenv calls_this checks idenv curr_pname curr_pdesc

infer/src/nullsafe/eradicateChecks.ml

@@ -232,7 +232,7 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc
     curr_constructor_pdesc start_node ~nullsafe_mode
     ~typestates_for_curr_constructor_and_all_initializer_methods
     ~typestates_for_all_constructors_incl_current loc : unit =
-  State.set_node start_node ;
+  AnalysisState.set_node start_node ;
   if Procname.is_constructor curr_constructor_pname then
     match
       PatternMatch.get_this_type_nonstatic_methods_only

infer/src/nullsafe/typeErr.ml

@@ -365,7 +365,7 @@ let report_forall_issues_and_reset st_report_error ~nullsafe_mode proc_desc =
     match (instr_ref_opt, get_forall err_instance) with
     | Some instr_ref, is_forall ->
         let node = InstrRef.get_node instr_ref in
-        State.set_node node ;
+        AnalysisState.set_node node ;
         if is_forall && err_state.always then
           report_now_if_reportable st_report_error err_instance err_state.loc ~nullsafe_mode
             proc_desc