From 74dbfd72b56505e0aff69d48a9ca43d71cf2a12f Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Thu, 28 Jan 2016 16:45:09 -0800 Subject: [PATCH] Fix issues with html output for debug in on-demand mode. Reviewed By: sblackshear Differential Revision: D2873791 fb-gh-sync-id: c1b1543 --- infer/src/backend/exe_env.ml | 7 ++++++- infer/src/backend/logging.ml | 4 ++++ infer/src/backend/logging.mli | 3 +++ infer/src/backend/ondemand.ml | 21 ++++++++++++++++----- infer/src/backend/printer.ml | 3 +-- infer/src/backend/printer.mli | 3 +++ 6 files changed, 33 insertions(+), 8 deletions(-) diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index 0753ac728..09a045a2d 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -52,6 +52,7 @@ type t = proc_map: file_data Procname.Hash.t; (** map from procedure name to file data *) mutable active_opt : Procname.Set.t option; (** if not None, restrict the active procedures to the given set *) mutable procs_defined_in_several_files : Procname.Set.t; (** Procedures defined in more than one file *) + mutable source_files : DB.SourceFileSet.t; (** Source files in the execution environment *) } (** initial state, used to add cg's *) @@ -66,6 +67,7 @@ let create procset_opt = proc_map = Procname.Hash.create 17; active_opt = procset_opt; procs_defined_in_several_files = Procname.Set.empty; + source_files = DB.SourceFileSet.empty; } (** check if a procedure is marked as active *) @@ -92,6 +94,7 @@ let add_cg_exclude_fun (exe_env: t) (source_dir : DB.source_dir) exclude_fun = | None -> None | Some cg -> let source = Cg.get_source cg in + exe_env.source_files <- DB.SourceFileSet.add source exe_env.source_files; if exclude_fun source then None else let nLOC = Cg.get_nLOC cg in @@ -195,7 +198,9 @@ let get_cfg exe_env pname = let iter_files f exe_env = let do_file _ file_data seen_files_acc = let fname = file_data.source in - if DB.SourceFileSet.mem fname seen_files_acc + if DB.SourceFileSet.mem fname seen_files_acc || + (* only files added with add_cg* functions *) + not (DB.SourceFileSet.mem fname exe_env.source_files) then seen_files_acc else begin diff --git a/infer/src/backend/logging.ml b/infer/src/backend/logging.ml index 88b7b26d2..605f3e79e 100644 --- a/infer/src/backend/logging.ml +++ b/infer/src/backend/logging.ml @@ -102,6 +102,10 @@ let reset_delayed_prints () = let get_delayed_prints () = !delayed_actions +(** set the delayed print actions *) +let set_delayed_prints new_delayed_actions = + delayed_actions := new_delayed_actions + let do_print fmt fmt_string = F.fprintf fmt fmt_string diff --git a/infer/src/backend/logging.mli b/infer/src/backend/logging.mli index 74d036b7e..5dc13bb31 100644 --- a/infer/src/backend/logging.mli +++ b/infer/src/backend/logging.mli @@ -65,6 +65,9 @@ val add_print_action : print_action -> unit (** return the delayed print actions *) val get_delayed_prints : unit -> print_action list +(** set the delayed print actions *) +val set_delayed_prints : print_action list -> unit + (** reset the delayed print actions *) val reset_delayed_prints : unit -> unit diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index d29c08472..6d739919f 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -90,6 +90,9 @@ let procedure_should_be_analyzed curr_pdesc proc_name = type global_state = { name_generator : Ident.NameGenerator.t; + current_source : DB.source_file; + html_formatter : F.formatter; + delayed_prints : L.print_action list; } let do_analysis curr_pdesc callee_pname = @@ -102,11 +105,19 @@ let do_analysis curr_pdesc callee_pname = Procname.pp callee_pname; let preprocess () = + let old_state = + { + name_generator = Ident.NameGenerator.get_current (); + current_source = !DB.current_source; + html_formatter = !Printer.html_formatter; + delayed_prints = L.get_delayed_prints (); + } in incr nesting; let attributes_opt = Specs.proc_resolve_attributes callee_pname in Option.may (fun attribute -> + DB.current_source := attribute.ProcAttributes.loc.Location.file; let attribute_pname = attribute.ProcAttributes.proc_name in if not (Procname.equal callee_pname attribute_pname) then failwith ("ERROR: "^(Procname.to_string callee_pname) @@ -118,14 +129,14 @@ let do_analysis curr_pdesc callee_pname = cg in Specs.reset_summary call_graph callee_pname attributes_opt; Specs.set_status callee_pname 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 + Ident.NameGenerator.set_current old_state.name_generator; + DB.current_source := old_state.current_source; + Printer.html_formatter := old_state.html_formatter; + L.set_delayed_prints old_state.delayed_prints in let postprocess () = decr nesting; diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index b69acac5f..8ca494405 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -92,8 +92,7 @@ end = struct let finish_node nodeid = let fname = id_to_fname nodeid in let fd = Hashtbl.find log_files (fname, !DB.current_source) in - if not !Config.ondemand_enabled (* TODO: close all file descriptors at the end in on-demand *) - then Unix.close fd; + Unix.close fd; html_formatter := F.std_formatter end (* =============== END of module Log_nodes =============== *) diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index 25b727b2f..9309b9cc5 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -10,6 +10,9 @@ (** Printers for the analysis results *) +(** Current html formatter *) +val html_formatter : Format.formatter ref + (** return true if the node was visited during footprint and during re-execution*) val is_visited_phase : Cfg.Node.t -> bool * bool