From 13e199a4ca5f400f367f94ad225106d3557a4e57 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Sun, 5 Mar 2017 11:19:42 -0800 Subject: [PATCH] [infer][ondemand] no need to pass the procedure name to save a summary Summary: I accidentally save a summary with the wrong procedure name, which was affecting the analysis in some weird way. This makes this case no longer possible Reviewed By: cristianoc Differential Revision: D4654002 fbshipit-source-id: 9fcbe4e --- infer/src/backend/callbacks.ml | 2 +- infer/src/backend/ondemand.ml | 4 ++-- infer/src/backend/specs.ml | 34 +++++++++++++++++++--------------- infer/src/backend/specs.mli | 2 +- infer/src/checkers/summary.ml | 2 +- 5 files changed, 24 insertions(+), 20 deletions(-) diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index cab98f8a1..f88670142 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -181,7 +181,7 @@ let iterate_callbacks call_graph exe_env = (* Store all the summaries to disk *) List.iter ~f:(fun pname -> - Specs.store_summary pname (Specs.get_summary_unsafe "Checkers: store summaries" pname)) + Specs.store_summary (Specs.get_summary_unsafe "Checkers: store summaries" pname)) procs_to_analyze; Config.curr_language := saved_language diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 334cf62dc..774d3e4b2 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -143,7 +143,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc let postprocess source summary = decr nesting; - Specs.store_summary callee_pname summary; + Specs.store_summary summary; Printer.write_proc_html source false callee_pdesc; summary in @@ -154,7 +154,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc let payload = { prev_summary.Specs.payload with Specs.preposts = Some []; } in let new_summary = { prev_summary with Specs.stats; payload } in - Specs.store_summary callee_pname new_summary; + Specs.store_summary new_summary; new_summary in let old_state = save_global_state () in diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 3845d49f8..578d1ec5d 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -545,25 +545,10 @@ let summary_exists_in_models pname = let summary_serializer : summary Serialization.serializer = Serialization.create_serializer Serialization.Key.summary -(** Save summary for the procedure into the spec database *) -let store_summary pname (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 - add_summary pname summ3 (* Make sure the summary in memory is identical to the saved one *); - Serialization.write_to_file summary_serializer (res_dir_specs_filename pname) ~data:final_summary - (** Load procedure summary from the given file *) let load_summary specs_file = Serialization.read_from_file summary_serializer specs_file - (** Load procedure summary for the given procedure name and update spec table *) let load_summary_to_spec_table proc_name = let add summ = @@ -702,6 +687,25 @@ let get_specs proc_name = let get_phase summary = summary.phase +(** Save summary for the procedure into the spec database *) +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 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; + Serialization.write_to_file + summary_serializer + (res_dir_specs_filename proc_name) + ~data:final_summary + (** Set the current status for the proc *) let set_status proc_name status = match get_summary proc_name with diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index f67aecf99..34a9170a5 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -274,7 +274,7 @@ val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t val res_dir_specs_filename : Procname.t -> DB.filename (** Save summary for the procedure into the spec database *) -val store_summary : Procname.t -> summary -> unit +val store_summary : summary -> unit (** Return a compact representation of the summary *) val summary_compact : Sil.sharing_env -> summary -> summary diff --git a/infer/src/checkers/summary.ml b/infer/src/checkers/summary.ml index 32706c9bc..304769a7e 100644 --- a/infer/src/checkers/summary.ml +++ b/infer/src/checkers/summary.ml @@ -39,7 +39,7 @@ module Make (H : Helper) = struct match Specs.get_summary pname with | Some global_summary -> let payload = H.update_payload summary global_summary.Specs.payload in - Specs.store_summary pname { global_summary with payload; } + Specs.store_summary { global_summary with payload; } | None -> failwithf "Summary for %a should exist, but does not!@." Procname.pp pname