From 03bca6734c871d92082f12d731c2bf0e3f5e8711 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Tue, 20 Oct 2015 08:32:11 -0700 Subject: [PATCH] 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 | 70 ++++++++++++++++++++-------------- infer/src/backend/ident.mli | 16 ++++++-- infer/src/backend/interproc.ml | 6 ++- infer/src/backend/ondemand.ml | 21 ++++++++-- infer/src/clang/cFrontend.ml | 4 +- infer/src/harness/inhabit.ml | 2 +- infer/src/java/jFrontend.ml | 2 +- infer/src/java/jMain.ml | 2 +- infer/src/llvm/lMain.ml | 2 +- infer/src/llvm/lTrans.ml | 2 +- 10 files changed, 84 insertions(+), 43 deletions(-) diff --git a/infer/src/backend/ident.ml b/infer/src/backend/ident.ml index 8c7a2bfba..419beac07 100644 --- a/infer/src/backend/ident.ml +++ b/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 = diff --git a/infer/src/backend/ident.mli b/infer/src/backend/ident.mli index 3b0e287e3..63e10e202 100644 --- a/infer/src/backend/ident.mli +++ b/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 diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index f5b2bc598..8d678e6c8 100644 --- a/infer/src/backend/interproc.ml +++ b/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; diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 7c0227c1d..2c56011f2 100644 --- a/infer/src/backend/ondemand.ml +++ b/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 diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index 4f1ce10c0..097353968 100644 --- a/infer/src/clang/cFrontend.ml +++ b/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 () diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index c0c3c035c..666222adb 100644 --- a/infer/src/harness/inhabit.ml +++ b/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 diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index 4afc71e57..029edcf5b 100644 --- a/infer/src/java/jFrontend.ml +++ b/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 diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index b13b87e1a..49ea08c39 100644 --- a/infer/src/java/jMain.ml +++ b/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 diff --git a/infer/src/llvm/lMain.ml b/infer/src/llvm/lMain.ml index 8a5e1e224..2206c83b5 100644 --- a/infer/src/llvm/lMain.ml +++ b/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 diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 26499df0a..78365dcb6 100644 --- a/infer/src/llvm/lTrans.ml +++ b/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) ->