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

@@ -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

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
 

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
 

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;

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 *)
+    Unix.close fd;
-    then Unix.close fd;
     html_formatter := F.std_formatter
 end
 (* =============== END of module Log_nodes =============== *)

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