fix a number of issues related to the treatment of global state in ondemand analysis

Reviewed By: jvillard

Differential Revision: D2549699

fb-gh-sync-id: 40e174d

infer/src/backend/ident.ml

@@ -189,8 +189,45 @@ let set_stamp i stamp =
 let get_stamp i =
   i.stamp
 
-(** Map from names to stamps. *)
-let name_map = NameHash.create 1000
+module NameGenerator = struct
+  type t = int NameHash.t
+
+  let create () : t = NameHash.create 17
+
+  (** Map from names to stamps. *)
+  let name_map = ref (create ())
+
+  let get_current () =
+    !name_map
+
+  let set_current map =
+    name_map := map
+
+  (** Reset the name generator *)
+  let reset () =
+    name_map := create ()
+
+  (** Create a fresh identifier with the given kind and name. *)
+  let create_fresh_ident kind name =
+    let stamp =
+      try
+        let stamp = NameHash.find !name_map name in
+        NameHash.replace !name_map name (stamp + 1);
+        stamp + 1
+      with Not_found ->
+        NameHash.add !name_map name 0;
+        0 in
+    { kind = kind; name = name; stamp = stamp }
+
+  (** Make sure that fresh ids after whis one will be with different stamps *)
+  let update_name_hash name stamp =
+    try
+      let curr_stamp = NameHash.find !name_map name in
+      let new_stamp = max curr_stamp stamp in
+      NameHash.replace !name_map name new_stamp
+    with Not_found ->
+      NameHash.add !name_map name stamp
+end
 
 (** Name used for primed tmp variables *)
 let name_primed = string_to_name "t"
@@ -215,15 +252,8 @@ let standard_name kind =
 
 (** Every identifier with a given stamp should unltimately be created using this function *)
 let create_with_stamp kind name stamp =
-  let update_name_hash () = (* make sure that fresh ids after whis one will be with different stamps *)
-    try
-      let curr_stamp = NameHash.find name_map name in
-      let new_stamp = max curr_stamp stamp in
-      NameHash.replace name_map name new_stamp
-    with Not_found ->
-      NameHash.add name_map name stamp in
-  update_name_hash ();
-  { kind = kind; name = name; stamp = stamp }
+  NameGenerator.update_name_hash name stamp;
+  { kind = kind; name = name; stamp = stamp; }
 
 (** Create an identifier with default name for the given kind *)
 let create kind stamp =
@@ -273,30 +303,14 @@ let make_unprimed id =
   if id.kind <> kprimed then assert false
   else { id with kind = knormal }
 
-(** Reset the name generator *)
-let reset_name_generator () =
-  NameHash.clear name_map
-
 (** Update the name generator so that the given id's are not generated again *)
 let update_name_generator ids =
   let upd id = ignore (create_with_stamp id.kind id.name id.stamp) in
   IList.iter upd ids
 
-(** Create a fresh identifier with the given kind and name. *)
-let create_fresh_ident kind name =
-  let stamp =
-    try
-      let stamp = NameHash.find name_map name in
-      NameHash.replace name_map name (stamp + 1);
-      stamp + 1
-    with Not_found ->
-      NameHash.add name_map name 0;
-      0 in
-  { kind = kind; name = name; stamp = stamp }
-
 (** Create a fresh identifier with default name for the given kind. *)
 let create_fresh kind =
-  create_fresh_ident kind (standard_name kind)
+  NameGenerator.create_fresh_ident kind (standard_name kind)
 
 (** Generate a normal identifier whose name encodes a path given as a string. *)
 let create_path pathstring =

infer/src/backend/ident.mli

@@ -36,6 +36,19 @@ module FieldSet : Set.S with type elt = fieldname
 (** Map for fieldnames *)
 module FieldMap : Map.S with type key = fieldname
 
+module NameGenerator : sig
+  type t
+
+  (** Get the current name generator. *)
+  val get_current : unit -> t
+
+  (** Reset the name generator. *)
+  val reset : unit -> unit
+
+  (** Set the current name generator. *)
+  val set_current : t -> unit
+end
+
 (** Convert an identfier list to an identifier set *)
 val idlist_to_idset : t list -> IdentSet.t
 
@@ -109,9 +122,6 @@ val create_primed : name -> int -> t
 (** Generate a footprint identifier with the given name and stamp. *)
 val create_footprint : name -> int -> t
 
-(** Reset the name generator *)
-val reset_name_generator : unit -> unit
-
 (** Update the name generator so that the given id's are not generated again *)
 val update_name_generator : t list -> unit
 

infer/src/backend/interproc.ml

@@ -989,7 +989,7 @@ let set_current_language cfg proc_desc =
 
 (** reset counters before analysing a procedure *)
 let reset_global_counters cfg proc_name proc_desc =
-  Ident.reset_name_generator ();
+  Ident.NameGenerator.reset ();
   SymOp.reset_total ();
   reset_prop_metrics ();
   Abs.abs_rules_reset ();
@@ -1154,7 +1154,7 @@ let perform_transition exe_env cg proc_name =
     parent process as soon as a child process returns a result. *)
 let process_result (exe_env: Exe_env.t) (proc_name, calls) (_summ: Specs.summary) : unit =
   if !Config.trace_anal then L.err "===process_result@.";
-  Ident.reset_name_generator (); (* for consistency with multi-core mode *)
+  Ident.NameGenerator.reset (); (* for consistency with multi-core mode *)
   let summ =
     { _summ with
       Specs.stats = { _summ.Specs.stats with Specs.stats_calls = calls }} in
@@ -1263,11 +1263,13 @@ let do_analysis exe_env =
       Cfg.Procdesc.find_from_name callee_cfg proc_name in
     let analyze_ondemand proc_name =
       let saved_footprint = !Config.footprint in
+      Config.footprint := true;
       let summaryfp = analyze_proc exe_env proc_name in
       Specs.add_summary proc_name summaryfp;
       let cg = Cg.create () in
       Cg.add_defined_node cg proc_name;
       perform_transition exe_env cg proc_name;
+      Config.footprint := false;
       let summaryre = analyze_proc exe_env proc_name in
       Specs.add_summary proc_name summaryre;
       Config.footprint := saved_footprint;

infer/src/backend/ondemand.ml

@@ -72,6 +72,11 @@ let procedure_should_be_analyzed curr_pdesc proc_name =
   | None ->
       false
 
+type global_state =
+  {
+    name_generator : Ident.NameGenerator.t;
+  }
+
 let do_analysis curr_pdesc proc_name =
   let curr_pname = Cfg.Procdesc.get_proc_name curr_pdesc in
 
@@ -90,7 +95,15 @@ let do_analysis curr_pdesc proc_name =
         Cg.add_defined_node cg proc_name;
         cg in
       Specs.reset_summary call_graph proc_name attributes_opt;
-      Specs.set_status proc_name Specs.ACTIVE in
+      Specs.set_status proc_name Specs.ACTIVE;
+      let old_state =
+        {
+          name_generator = Ident.NameGenerator.get_current ();
+        } in
+      old_state in
+
+    let restore old_state =
+      Ident.NameGenerator.set_current old_state.name_generator in
 
     let postprocess () =
       decr nesting;
@@ -102,15 +115,17 @@ let do_analysis curr_pdesc proc_name =
       Specs.add_summary proc_name summary';
       Checkers.ST.store_summary proc_name in
 
+    let old_state = preprocess () in
     try
-      preprocess ();
       analyze_proc proc_name;
-      postprocess ()
+      postprocess ();
+      restore old_state;
     with e ->
       L.stderr "ONDEMAND EXCEPTION %a %s %s@."
         Procname.pp proc_name
         (Printexc.to_string e)
         (Printexc.get_backtrace ());
+      restore old_state;
       raise e in
 
   match !callbacks_ref with

infer/src/clang/cFrontend.ml

@@ -22,7 +22,7 @@ open CGen_trans
 (* Translate one global declaration *)
 let rec translate_one_declaration tenv cg cfg namespace parent_dec dec =
   (* each procedure has different scope: start names from id 0 *)
-  Ident.reset_name_generator ();
+  Ident.NameGenerator.reset ();
 
   let ns_suffix = Ast_utils.namespace_to_string namespace in
   let info = Clang_ast_proj.get_decl_tuple dec in
@@ -124,7 +124,7 @@ let init_global_state source_file =
   Config.curr_language := Config.C_CPP;
   DB.current_source := source_file;
   DB.Results_dir.init ();
-  Ident.reset_name_generator ();
+  Ident.NameGenerator.reset ();
   CFrontend_config.global_translation_unit_decls := [];
   ObjcProperty_decl.reset_property_table ();
   CFrontend_utils.General_utils.reset_block_counter ()

infer/src/harness/inhabit.ml

@@ -304,7 +304,7 @@ let add_harness_to_cg harness_name harness_cfg harness_node loc cg tenv =
  * proc to the cg *)
 let setup_harness_cfg harness_name harness_cfg env source_dir cg tenv =
   (* each procedure has different scope: start names from id 0 *)
-  Ident.reset_name_generator ();
+  Ident.NameGenerator.reset ();
 
   let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
   let harness_cfg = match Cfg.load_cfg_from_file cfg_file with

infer/src/java/jFrontend.ml

@@ -161,7 +161,7 @@ let create_icfg never_null_matcher linereader program icfg source_file cn node =
     Javalib.m_iter (JTrans.create_local_procdesc program linereader cfg tenv node) node;
     Javalib.m_iter (fun m ->
         (* each procedure has different scope: start names from id 0 *)
-        Ident.reset_name_generator ();
+        Ident.NameGenerator.reset ();
 
         let method_kind = JTransType.get_method_kind m in
         match m with

infer/src/java/jMain.ml

@@ -48,7 +48,7 @@ let init_global_state source_file =
   Config.curr_language := Config.Java;
   DB.current_source := source_file;
   DB.Results_dir.init ();
-  Ident.reset_name_generator ();
+  Ident.NameGenerator.reset ();
   SymOp.reset_total ();
   JContext.reset_exn_node_table ();
   let nLOC = FileLOC.file_get_loc (DB.source_file_to_string source_file) in

infer/src/llvm/lMain.ml

@@ -40,7 +40,7 @@ let init_global_state source_filename =
             (filename_to_absolute source_filename)
   end;
   DB.Results_dir.init ();
-  Ident.reset_name_generator ();
+  Ident.NameGenerator.reset ();
   SymOp.reset_total ();
   Config.nLOC := FileLOC.file_get_loc source_filename
 

infer/src/llvm/lTrans.ml

@@ -116,7 +116,7 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
     (func_def : LAst.function_def) : unit =
 
   (* each procedure has different scope: start names from id 0 *)
-  Ident.reset_name_generator ();
+  Ident.NameGenerator.reset ();
 
   match func_def with
     FunctionDef (func_name, ret_tp_opt, params, annotated_instrs) ->