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