[infer][backend] remove the perf stats from the summaries

Summary:
It is definitely useful to collect information about how long the analysis of every procedure takes. It allows to detect and focus on outliers when trying to improve performance.  However, this kind of information could be collected using a standard logging mechanism and does not need to be stored within the analysis artifacts.

I intend to add some form of similar logging in the context of #16348004 once we can get every analysis procedure analyzed through the `Ondemand` module. In this case, it would be easy to have a single place to log how does the analysis of a procedure take.

Reviewed By: jberdine

Differential Revision: D4636755

fbshipit-source-id: 01f3bca

infer/src/backend/InferPrint.re

@@ -124,7 +124,6 @@ type summary_val = {
   vname: string,
   vname_id: string,
   vspecs: int,
-  vtime: string,
   vto: string,
   vsymop: int,
   verr: int,
@@ -173,7 +172,6 @@ let summary_values summary => {
     vname: Typ.Procname.to_string proc_name,
     vname_id: Typ.Procname.to_filename proc_name,
     vspecs: List.length specs,
-    vtime: Printf.sprintf "%.0f" stats.Specs.stats_time,
     vto: Option.value_map f::pp_failure default::"NONE" stats.Specs.stats_failure,
     vsymop: stats.Specs.symops,
     verr:
@@ -226,7 +224,6 @@ let module ProcsCsv = {
     pp "\"%s\"," (Escape.escape_csv sv.vname);
     pp "\"%s\"," (Escape.escape_csv sv.vname_id);
     pp "%d," sv.vspecs;
-    pp "%s," sv.vtime;
     pp "%s," sv.vto;
     pp "%d," sv.vsymop;
     pp "%d," sv.verr;
@@ -253,7 +250,6 @@ let module ProcsXml = {
         subtree Io_infer.Xml.tag_name (Escape.escape_xml sv.vname),
         subtree Io_infer.Xml.tag_name_id (Escape.escape_xml sv.vname_id),
         subtree Io_infer.Xml.tag_specs (string_of_int sv.vspecs),
-        subtree Io_infer.Xml.tag_time sv.vtime,
         subtree Io_infer.Xml.tag_to sv.vto,
         subtree Io_infer.Xml.tag_symop (string_of_int sv.vsymop),
         subtree Io_infer.Xml.tag_err (string_of_int sv.verr),
@@ -876,12 +872,7 @@ let module Summary = {
     if Config.quiet {
       ()
     } else {
-      L.stdout
-        "Procedure: %a@\n%a@."
-        Typ.Procname.pp
-        proc_name
-        (Specs.pp_summary_text whole_seconds::Config.whole_seconds)
-        summary
+      L.stdout "Procedure: %a@\n%a@." Typ.Procname.pp proc_name Specs.pp_summary_text summary
     }
   };
 
@@ -890,8 +881,7 @@ let module Summary = {
     let proc_name = Specs.get_proc_name summary;
     Latex.pp_section
       fmt ("Analysis of function " ^ Latex.convert_string (Typ.Procname.to_string proc_name));
-    F.fprintf
-      fmt "@[<v>%a@]" (Specs.pp_summary_latex Black whole_seconds::Config.whole_seconds) summary
+    F.fprintf fmt "@[<v>%a@]" (Specs.pp_summary_latex Black) summary
   };
   let pp_summary_xml summary fname =>
     if Config.xml_specs {

infer/src/backend/callbacks.ml

@@ -81,14 +81,6 @@ let iterate_procedure_callbacks exe_env caller_pname =
     | None ->
         [] in
 
-  let update_time elapsed prev_summary =
-    let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
-    let stats = { prev_summary.Specs.stats with Specs.stats_time = stats_time } in
-    let summary = { prev_summary with Specs.stats = stats } in
-    let proc_name = Specs.get_proc_name summary in
-    Specs.add_summary proc_name summary;
-    summary in
-
   let initial_summary = reset_summary caller_pname in
   match get_procedure_definition exe_env caller_pname with
   | None -> initial_summary
@@ -100,7 +92,6 @@ let iterate_procedure_callbacks exe_env caller_pname =
               | Some language -> Config.equal_language language procedure_language
               | None -> true in
             if language_matches then
-              let init_time = Unix.gettimeofday () in
               proc_callback
                 {
                   get_proc_desc;
@@ -110,7 +101,6 @@ let iterate_procedure_callbacks exe_env caller_pname =
                   summary;
                   proc_desc;
                 }
-              |> update_time (Unix.gettimeofday () -. init_time)
             else
               summary)
         !procedure_callbacks

infer/src/backend/interproc.ml

@@ -1268,17 +1268,15 @@ let update_specs tenv proc_name phase (new_specs : Specs.NormSpec.t list)
   !res,!changed
 
 (** update a summary after analysing a procedure *)
-let update_summary tenv prev_summary specs phase proc_name elapsed res =
+let update_summary tenv prev_summary specs phase proc_name res =
   let normal_specs = List.map ~f:(Specs.spec_normalize tenv) specs in
   let new_specs, _ = update_specs tenv proc_name phase normal_specs in
-  let stats_time = prev_summary.Specs.stats.Specs.stats_time +. elapsed in
   let symops = prev_summary.Specs.stats.Specs.symops + SymOp.get_total () in
   let stats_failure = match res with
     | None -> prev_summary.Specs.stats.Specs.stats_failure
     | Some _ -> res in
   let stats =
     { prev_summary.Specs.stats with
-      Specs.stats_time;
       symops;
       stats_failure;
     } in
@@ -1299,16 +1297,14 @@ let update_summary tenv prev_summary specs phase proc_name elapsed res =
 (** Analyze the procedure and return the resulting summary. *)
 let analyze_proc source exe_env proc_desc : Specs.summary =
   let proc_name = Procdesc.get_proc_name proc_desc in
-  let init_time = Unix.gettimeofday () in
   let tenv = Exe_env.get_tenv exe_env proc_name in
   reset_global_values proc_desc;
   let go, get_results = perform_analysis_phase tenv proc_name proc_desc source in
   let res = Timeout.exe_timeout go () in
   let specs, phase = get_results () in
-  let elapsed = Unix.gettimeofday () -. init_time in
   let prev_summary = Specs.get_summary_unsafe "analyze_proc" proc_name in
   let updated_summary =
-    update_summary tenv prev_summary specs phase proc_name elapsed res in
+    update_summary tenv prev_summary specs phase proc_name res in
   if Config.curr_language_is Config.Clang && Config.report_custom_error then
     report_custom_errors tenv updated_summary;
   if Config.curr_language_is Config.Java && Config.report_runtime_exceptions then

infer/src/backend/ondemand.ml

@@ -112,6 +112,14 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
   let curr_pname = Procdesc.get_proc_name curr_pdesc in
   let callee_pname = Procdesc.get_proc_name callee_pdesc in
 
+  let log_elapsed_time =
+    let start_time = Unix.gettimeofday () in
+    fun () ->
+      let elapsed_time = Unix.gettimeofday () -. start_time in
+      L.out "Elapsed analysis time: %a: %f\n"
+        Typ.Procname.pp callee_pname
+        elapsed_time in
+
   (* Dot means start of a procedure *)
   L.log_progress_procedure ();
   if Config.trace_ondemand then L.stderr "[%d] run_proc_analysis %a -> %a@."
@@ -144,7 +152,8 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
   let postprocess source summary =
     decr nesting;
     Specs.store_summary summary;
-    Printer.write_proc_html source false callee_pdesc;
+    Printer.write_proc_html source callee_pdesc;
+    log_elapsed_time ();
     summary in
 
   let log_error_and_continue exn kind =
@@ -155,6 +164,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
       { prev_summary.Specs.payload with Specs.preposts = Some []; } in
     let new_summary = { prev_summary with Specs.stats; payload } in
     Specs.store_summary new_summary;
+    log_elapsed_time ();
     new_summary in
 
   let old_state = save_global_state () in

infer/src/backend/printer.ml

@@ -414,7 +414,7 @@ let node_finish_session node source =
 
 (** Write html file for the procedure.
     The boolean indicates whether to print whole seconds only *)
-let write_proc_html source whole_seconds pdesc =
+let write_proc_html source pdesc =
   if Config.write_html then
     begin
       let pname = Procdesc.get_proc_name pdesc in
@@ -446,7 +446,7 @@ let write_proc_html source whole_seconds pdesc =
        | None ->
            ()
        | Some summary ->
-           Specs.pp_summary_html source Black ~whole_seconds fmt summary;
+           Specs.pp_summary_html source Black fmt summary;
            Io_infer.Html.close (fd, fmt))
     end
 

infer/src/backend/printer.mli

@@ -45,9 +45,8 @@ val node_is_visited : Procdesc.Node.t -> bool * bool
 (** Start a session, and create a new html fine for the node if it does not exist yet *)
 val node_start_session : Procdesc.Node.t -> int -> SourceFile.t -> unit
 
-(** Write html file for the procedure.
-    The boolean indicates whether to print whole seconds only. *)
-val write_proc_html : SourceFile.t -> bool -> Procdesc.t -> unit
+(** Write html file for the procedure. *)
+val write_proc_html : SourceFile.t -> Procdesc.t -> unit
 
 (** Create filename.ext.html for each file in the cluster. *)
 val write_all_html_files : Cluster.t -> unit

infer/src/backend/specs.ml

@@ -295,8 +295,7 @@ type call_stats = CallStats.t
 
 (** Execution statistics *)
 type stats =
-  { stats_time: float; (** Analysis time for the procedure *)
-    stats_failure:
+  { stats_failure:
       SymOp.failure_kind option; (** what type of failure stopped the analysis (if any) *)
     symops: int; (** Number of SymOp's throughout the whole analysis of the function *)
     mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *)
@@ -366,9 +365,8 @@ let pp_errlog fmt err_log =
   F.fprintf fmt "ERRORS: @[<h>%a@]@." Errlog.pp_errors err_log;
   F.fprintf fmt "WARNINGS: @[<h>%a@]" Errlog.pp_warnings err_log
 
-let pp_stats whole_seconds fmt stats =
-  F.fprintf fmt "TIME:%a FAILURE:%a SYMOPS:%d@\n" (pp_time whole_seconds)
-    stats.stats_time pp_failure_kind_opt stats.stats_failure stats.symops
+let pp_stats fmt stats =
+  F.fprintf fmt "FAILURE:%a SYMOPS:%d@\n" pp_failure_kind_opt stats.stats_failure stats.symops
 
 
 (** Print the spec *)
@@ -460,32 +458,32 @@ let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof;
     (pp_opt BufferOverrunDomain.Summary.pp) buffer_overrun
 
 
-let pp_summary_text ~whole_seconds fmt summary =
+let pp_summary_text fmt summary =
   let err_log = summary.attributes.ProcAttributes.err_log in
   let pe = Pp.text in
   pp_summary_no_stats_specs fmt summary;
   F.fprintf fmt "%a@\n%a%a"
     pp_errlog err_log
-    (pp_stats whole_seconds) summary.stats
+    pp_stats summary.stats
     (pp_payload pe) summary.payload
 
-let pp_summary_latex ~whole_seconds color fmt summary =
+let pp_summary_latex color fmt summary =
   let err_log = summary.attributes.ProcAttributes.err_log in
   let pe = Pp.latex color in
   F.fprintf fmt "\\begin{verbatim}@\n";
   pp_summary_no_stats_specs fmt summary;
   F.fprintf fmt "%a@\n" pp_errlog err_log;
-  F.fprintf fmt "%a@\n" (pp_stats whole_seconds) summary.stats;
+  F.fprintf fmt "%a@\n" pp_stats summary.stats;
   F.fprintf fmt "\\end{verbatim}@\n";
   F.fprintf fmt "%a@\n" (pp_specs pe) (get_specs_from_payload summary)
 
-let pp_summary_html ~whole_seconds source color fmt summary =
+let pp_summary_html source color fmt summary =
   let err_log = summary.attributes.ProcAttributes.err_log in
   let pe = Pp.html color in
   Io_infer.Html.pp_start_color fmt Black;
   F.fprintf fmt "@\n%a" pp_summary_no_stats_specs summary;
   Io_infer.Html.pp_end_color fmt ();
-  F.fprintf fmt "<br />%a<br />@\n" (pp_stats whole_seconds) summary.stats;
+  F.fprintf fmt "<br />%a<br />@\n" pp_stats summary.stats;
   Errlog.pp_html source [] fmt err_log;
   Io_infer.Html.pp_hline fmt ();
   F.fprintf fmt "<LISTING>@\n";
@@ -493,8 +491,7 @@ let pp_summary_html ~whole_seconds source color fmt summary =
   F.fprintf fmt "</LISTING>@\n"
 
 let empty_stats calls =
-  { stats_time = 0.0;
-    stats_failure = None;
+  { stats_failure = None;
     symops = 0;
     nodes_visited_fp = IntSet.empty;
     nodes_visited_re = IntSet.empty;
@@ -518,7 +515,7 @@ let summary_compact sh summary =
 let add_summary (proc_name : Typ.Procname.t) (summary: summary) : unit =
   L.out "Adding summary for %a@\n@[<v 2>  %a@]@."
     Typ.Procname.pp proc_name
-    (pp_summary_text ~whole_seconds:false) summary;
+    pp_summary_text summary;
   Typ.Procname.Hash.replace spec_tbl proc_name summary
 
 let specs_filename pname =
@@ -692,12 +689,7 @@ let store_summary (summ1: summary) =
   let summ2 = if Config.save_compact_summaries
     then summary_compact (Sil.create_sharing_env ()) summ1
     else summ1 in
-  let summ3 = if Config.save_time_in_summaries
-    then summ2
-    else
-      { summ2 with
-        stats = { summ1.stats with stats_time = 0.0} } in
-  let final_summary = { summ3 with status = Analyzed } in
+  let final_summary = { summ2 with status = Analyzed } in
   let proc_name = get_proc_name final_summary in
   (* Make sure the summary in memory is identical to the saved one *)
   add_summary proc_name final_summary;

infer/src/backend/specs.mli

@@ -105,8 +105,7 @@ end
 
 (** Execution statistics *)
 type stats =
-  { stats_time: float; (** Analysis time for the procedure *)
-    stats_failure:
+  { stats_failure:
       SymOp.failure_kind option; (** what type of failure stopped the analysis (if any) *)
     symops: int; (** Number of SymOp's throughout the whole analysis of the function *)
     mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *)
@@ -241,14 +240,13 @@ val pp_spec : Pp.env -> (int * int) option -> Format.formatter -> Prop.normal sp
 val pp_specs : Pp.env -> Format.formatter -> Prop.normal spec list -> unit
 
 (** Print the summary in html format *)
-val pp_summary_html :
-  whole_seconds:bool -> SourceFile.t -> Pp.color -> Format.formatter -> summary -> unit
+val pp_summary_html : SourceFile.t -> Pp.color -> Format.formatter -> summary -> unit
 
 (** Print the summary in latext format *)
-val pp_summary_latex : whole_seconds:bool -> Pp.color -> Format.formatter -> summary -> unit
+val pp_summary_latex : Pp.color -> Format.formatter -> summary -> unit
 
 (** Print the summary in text format *)
-val pp_summary_text : whole_seconds:bool -> Format.formatter -> summary -> unit
+val pp_summary_text : Format.formatter -> summary -> unit
 
 (** Like proc_resolve_attributes but start from a proc_desc. *)
 val pdesc_resolve_attributes : Procdesc.t -> ProcAttributes.t

infer/src/base/Config.ml

@@ -210,10 +210,6 @@ let reporting_stats_dir_name = "reporting_stats"
 (** If true, compact summaries before saving *)
 let save_compact_summaries = true
 
-(** If true, save the execution time in summaries.  This makes the analysis
-    nondeterministic. *)
-let save_time_in_summaries = false
-
 (** If true enables printing proposition compatible for the SMT project *)
 let smt_output = false
 

infer/src/base/Config.mli

@@ -135,7 +135,6 @@ val report_custom_error : bool
 val report_nullable_inconsistency : bool
 val reporting_stats_dir_name : string
 val save_compact_summaries : bool
-val save_time_in_summaries : bool
 val smt_output : bool
 val source_file_extentions : string list
 val sources : string list