From 8cd68cd890933a5f3a19705b1c164fe694aa78a5 Mon Sep 17 00:00:00 2001 From: Cristiano Calcagno Date: Wed, 25 Nov 2015 06:08:21 -0800 Subject: [PATCH] Separate payloads from different analyses in specs. Summary: public Currently payloads for different analyses are stored in a disjoint union. After this diff, a record is used to enable running different analyses using the same spec files. Reviewed By: jvillard Differential Revision: D2695566 fb-gh-sync-id: 3d2886d --- infer/src/backend/fork.ml | 37 ++++++++++------- infer/src/backend/interproc.ml | 12 ++++-- infer/src/backend/specs.ml | 46 +++++++++++++++------- infer/src/backend/specs.mli | 8 ++-- infer/src/checkers/codeQuery.ml | 11 ++++-- infer/src/checkers/eradicate.ml | 9 +++-- infer/src/checkers/eradicate.mli | 2 +- infer/src/checkers/performanceCritical.ml | 14 ++++--- infer/src/checkers/repeatedCallsChecker.ml | 2 +- 9 files changed, 90 insertions(+), 51 deletions(-) diff --git a/infer/src/backend/fork.ml b/infer/src/backend/fork.ml index 1fc083bad..d2dcbd8f5 100644 --- a/infer/src/backend/fork.ml +++ b/infer/src/backend/fork.ml @@ -65,20 +65,24 @@ let transition_footprint_re_exe proc_name joined_pres = Specs.phase = Specs.RE_EXECUTION; } else + let specs = + IList.map + (fun jp -> + Specs.spec_normalize + { Specs.pre = jp; + posts = []; + visited = Specs.Visitedset.empty }) + joined_pres in + let payload = + { summary.Specs.payload with + Specs.preposts = Some specs; } in + let dependency_map = + Specs.re_initialize_dependency_map summary.Specs.dependency_map in { summary with Specs.timestamp = 0; - Specs.phase = Specs.RE_EXECUTION; - Specs.dependency_map = Specs.re_initialize_dependency_map summary.Specs.dependency_map; - Specs.payload = - let specs = - IList.map - (fun jp -> - Specs.spec_normalize - { Specs.pre = jp; - Specs.posts = []; - Specs.visited = Specs.Visitedset.empty }) - joined_pres in - Specs.PrePosts specs + phase = Specs.RE_EXECUTION; + dependency_map; + payload; } in Specs.add_summary proc_name summary' @@ -414,11 +418,14 @@ let interprocedural_algorithm let prev_summary = Specs.get_summary_unsafe "interprocedural_algorithm" pname in let timestamp = max 1 (prev_summary.Specs.timestamp) in let stats = { prev_summary.Specs.stats with Specs.stats_timeout = true } in + let payload = + { prev_summary.Specs.payload with + Specs.preposts = Some []; } in let summ = { prev_summary with - Specs.stats = stats; - Specs.payload = Specs.PrePosts []; - Specs.timestamp = timestamp } in + Specs.stats; + payload; + timestamp; } in summ in let process_result exe_env (pname, calls) summary = (* wrap _process_result and handle exceptions *) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index c2779df7c..3008f06ff 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -1093,10 +1093,14 @@ let update_summary prev_summary specs proc_name elapsed res = Specs.stats_time = stats_time; Specs.symops = symops; Specs.stats_timeout = timeout } in + let payload = + { prev_summary.Specs.payload with + Specs.preposts = Some new_specs; } in { prev_summary with - Specs.stats = stats; - Specs.payload = Specs.PrePosts new_specs; - Specs.timestamp = timestamp } + Specs.stats; + payload; + timestamp; + } (** Analyze [proc_name] and return the updated summary. Use module @@ -1119,7 +1123,7 @@ let analyze_proc exe_env (proc_name: Procname.t) : Specs.summary = let updated_summary = update_summary prev_summary specs proc_name elapsed res in if (!Config.curr_language <> Config.Java && Config.report_assertion_failure) - || !Config.report_runtime_exceptions then + || !Config.report_runtime_exceptions then report_runtime_exceptions tenv cfg proc_desc updated_summary; updated_summary diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 5ded8535e..32c89b65a 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -307,9 +307,11 @@ type is_library = Source | Library (** Payload: results of some analysis *) type payload = - | PrePosts of NormSpec.t list (** list of specs *) - | TypeState of unit TypeState.t option (** final typestate *) - | Calls of CallTree.t list + { + preposts : NormSpec.t list option; (** list of specs *) + typestate : unit TypeState.t option; (** final typestate *) + calls: CallTree.t list option; + } type summary = { dependency_map: dependency_map_t; (** maps children procs to timestamp as last seen at the start of an analysys phase for this proc *) @@ -426,9 +428,10 @@ let pp_summary_no_stats_specs fmt summary = let pp_stats_html err_log fmt stats = Errlog.pp_html [] fmt err_log -let get_specs_from_payload summary = match summary.payload with - | PrePosts specs -> NormSpec.tospecs specs - | TypeState _ | Calls _ -> [] +let get_specs_from_payload summary = + match summary.payload.preposts with + | Some specs -> NormSpec.tospecs specs + | None -> [] (** Print the summary *) let pp_summary pe whole_seconds fmt summary = @@ -480,10 +483,14 @@ let rec post_equal pl1 pl2 = match pl1, pl2 with if Prop.prop_equal p1 p2 then post_equal pl1' pl2' else false -let payload_compact sh payload = match payload with - | PrePosts specs -> PrePosts (IList.map (NormSpec.compact sh) specs) - | TypeState _ as p -> p - | Calls _ as p -> p +let payload_compact sh payload = + match payload.preposts with + | Some specs -> + { payload with + preposts = Some (IList.map (NormSpec.compact sh) specs); + } + | None -> + payload (** Return a compact representation of the summary *) let summary_compact sh summary = @@ -529,10 +536,12 @@ let summary_serializer : summary Serialization.serializer = (** Save summary for the procedure into the spec database *) let store_summary pname (summ: summary) = - let process_payload = function - | PrePosts specs -> PrePosts (IList.map NormSpec.erase_join_info_pre specs) - | TypeState _ as p -> p - | Calls _ as p -> p in + let process_payload payload = match payload.preposts with + | Some specs -> + { payload with + preposts = Some (IList.map NormSpec.erase_join_info_pre specs); + } + | None -> payload in let summ1 = { summ with payload = process_payload summ.payload } in let summ2 = if !Config.save_compact_summaries then summary_compact (Sil.create_sharing_env ()) summ1 @@ -778,6 +787,13 @@ let update_dependency_map proc_name = summary.dependency_map in set_summary_origin proc_name { summary with dependency_map = current_dependency_map } origin +let empty_payload = + { + preposts = None; + typestate = None; + calls = None; + } + (** [init_summary (depend_list, nodes, proc_flags, calls, cyclomatic, in_out_calls_opt, proc_attributes)] initializes the summary for [proc_name] given dependent procs in list [depend_list]. *) @@ -792,7 +808,7 @@ let init_summary nodes = nodes; phase = FOOTPRINT; sessions = ref 0; - payload = PrePosts []; + payload = empty_payload; stats = empty_stats calls cyclomatic in_out_calls_opt; status = INACTIVE; timestamp = 0; diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 8d7eb6178..7532a0088 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -119,9 +119,11 @@ type dependency_map_t = int Procname.Map.t (** Payload: results of some analysis *) type payload = - | PrePosts of NormSpec.t list (** list of specs *) - | TypeState of unit TypeState.t option (** final typestate *) - | Calls of CallTree.t list (** list of call tree *) + { + preposts : NormSpec.t list option; (** list of specs *) + typestate : unit TypeState.t option; (** final typestate *) + calls: CallTree.t list option; (** list of call tree *) + } (** Procedure summary *) type summary = diff --git a/infer/src/checkers/codeQuery.ml b/infer/src/checkers/codeQuery.ml index dba43e131..4a1a1bb7a 100644 --- a/infer/src/checkers/codeQuery.ml +++ b/infer/src/checkers/codeQuery.ml @@ -42,16 +42,19 @@ module Err = struct let specs = let spec = { Specs.pre = Specs.Jprop.Prop (1, Prop.prop_emp); - Specs.posts = []; - Specs.visited = Specs.Visitedset.empty + posts = []; + visited = Specs.Visitedset.empty } in [(Specs.spec_normalize spec)] in let new_summ = { old_summ with Specs.attributes = { old_summ.Specs.attributes with ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc }; - Specs.nodes = nodes; - Specs.payload = Specs.PrePosts specs } in + nodes = nodes; + payload = + { old_summ.Specs.payload with + Specs.preposts = Some specs; } + } in Specs.add_summary proc_name new_summ let add_error_to_spec proc_name s node loc = diff --git a/infer/src/checkers/eradicate.ml b/infer/src/checkers/eradicate.ml index 50c9b29d8..d130193a2 100644 --- a/infer/src/checkers/eradicate.ml +++ b/infer/src/checkers/eradicate.ml @@ -41,7 +41,7 @@ end (* CallBackT *) module type ExtensionT = sig type extension val ext : extension TypeState.ext - val mkpayload : extension TypeState.t option -> Specs.payload + val update_payload : extension TypeState.t option -> Specs.payload -> Specs.payload end (** Create a module with the toplevel callback. *) @@ -60,7 +60,8 @@ struct { old_summ with Specs.nodes = nodes; - Specs.payload = Extension.mkpayload final_typestate_opt; + Specs.payload = + Extension.update_payload final_typestate_opt old_summ.Specs.payload; Specs.attributes = { old_summ.Specs.attributes with @@ -373,7 +374,9 @@ struct join = join; pp = pp; } - let mkpayload typestate_opt = Specs.TypeState typestate_opt + let update_payload typestate_opt payload = + { payload with + Specs.typestate = typestate_opt; } end module Main = diff --git a/infer/src/checkers/eradicate.mli b/infer/src/checkers/eradicate.mli index fe7f37cad..3d9738c66 100644 --- a/infer/src/checkers/eradicate.mli +++ b/infer/src/checkers/eradicate.mli @@ -32,7 +32,7 @@ end (* CallBackT *) module type ExtensionT = sig type extension val ext : extension TypeState.ext - val mkpayload : extension TypeState.t option -> Specs.payload + val update_payload : extension TypeState.t option -> Specs.payload -> Specs.payload end (** Given an extension to the typestate with a check, call the check on each instruction. *) diff --git a/infer/src/checkers/performanceCritical.ml b/infer/src/checkers/performanceCritical.ml index 93c39fc6a..e4aaeec74 100644 --- a/infer/src/checkers/performanceCritical.ml +++ b/infer/src/checkers/performanceCritical.ml @@ -54,9 +54,9 @@ let lookup_call_trees pname = | None -> [] | Some summary -> begin - match summary.Specs.payload with - | Specs.Calls tree -> tree - | _ -> [] + match summary.Specs.payload.Specs.calls with + | Some tree -> tree + | None -> [] end @@ -80,7 +80,11 @@ let update_summary call_trees pname = | None -> () | Some summary -> let updated_summary = - { summary with Specs.payload = Specs.Calls call_trees } in + { summary with + Specs.payload = + { summary.Specs.payload with + Specs.calls = Some call_trees; } + } in Specs.add_summary pname updated_summary @@ -164,7 +168,7 @@ let callback_performance_checker _ get_proc_desc _ tenv pname proc_desc = | Some pd -> check_one_procedure tenv pn pd in { Ondemand.analyze_ondemand; get_proc_desc; } in if !Config.ondemand_enabled - || Ondemand.procedure_should_be_analyzed proc_desc pname + || Ondemand.procedure_should_be_analyzed proc_desc pname then begin Ondemand.set_callbacks callbacks; diff --git a/infer/src/checkers/repeatedCallsChecker.ml b/infer/src/checkers/repeatedCallsChecker.ml index c3356d75f..d2784eccb 100644 --- a/infer/src/checkers/repeatedCallsChecker.ml +++ b/infer/src/checkers/repeatedCallsChecker.ml @@ -159,7 +159,7 @@ struct pp = pp; } - let mkpayload typestate = Specs.TypeState None + let update_payload typestate payload = payload end (* CheckRepeatedCalls *) module MainRepeatedCalls =