From c5b30b4c050e0a0ce13a40ff55e912bb53ab602d Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Wed, 15 Mar 2017 23:08:02 -0700 Subject: [PATCH] [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 | 14 ++------------ infer/src/backend/callbacks.ml | 10 ---------- infer/src/backend/interproc.ml | 8 ++------ infer/src/backend/ondemand.ml | 12 +++++++++++- infer/src/backend/printer.ml | 4 ++-- infer/src/backend/printer.mli | 5 ++--- infer/src/backend/specs.ml | 32 ++++++++++++-------------------- infer/src/backend/specs.mli | 10 ++++------ infer/src/base/Config.ml | 4 ---- infer/src/base/Config.mli | 1 - 10 files changed, 35 insertions(+), 65 deletions(-) diff --git a/infer/src/backend/InferPrint.re b/infer/src/backend/InferPrint.re index 30a79c74d..874c3a5cb 100644 --- a/infer/src/backend/InferPrint.re +++ b/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 "@[%a@]" (Specs.pp_summary_latex Black whole_seconds::Config.whole_seconds) summary + F.fprintf fmt "@[%a@]" (Specs.pp_summary_latex Black) summary }; let pp_summary_xml summary fname => if Config.xml_specs { diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index 7e18da855..771fc6ec7 100644 --- a/infer/src/backend/callbacks.ml +++ b/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 diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index f2b5265e3..9e18756dc 100644 --- a/infer/src/backend/interproc.ml +++ b/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 diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 915488b7e..1d2fceb89 100644 --- a/infer/src/backend/ondemand.ml +++ b/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 diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index d04fccc4d..e29ecb12f 100644 --- a/infer/src/backend/printer.ml +++ b/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 diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index ee915ede1..0b34f8370 100644 --- a/infer/src/backend/printer.mli +++ b/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 diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 793cc78b7..4b4b3fa27 100644 --- a/infer/src/backend/specs.ml +++ b/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: @[%a@]@." Errlog.pp_errors err_log; F.fprintf fmt "WARNINGS: @[%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 "
%a
@\n" (pp_stats whole_seconds) summary.stats; + F.fprintf fmt "
%a
@\n" pp_stats summary.stats; Errlog.pp_html source [] fmt err_log; Io_infer.Html.pp_hline fmt (); F.fprintf fmt "@\n"; @@ -493,8 +491,7 @@ let pp_summary_html ~whole_seconds source color fmt summary = F.fprintf fmt "@\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@[ %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; diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 79bb059e7..737cb9738 100644 --- a/infer/src/backend/specs.mli +++ b/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 diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index c2ce8e97f..f9b7360a6 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 99aa43070..2d858a02d 100644 --- a/infer/src/base/Config.mli +++ b/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