From 9c52e8ee682fd174166117ccfa403dac25b1fcff Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Tue, 28 Feb 2017 21:04:49 -0800 Subject: [PATCH] [infer][backend] remove the concept of timestamp in summaries and use the summary status instead Summary: With the ondemand analysis framework, the concept of timestamp was only being use to check if a procedure has already been analyzed. There was already a concept of "active" procedure for the procedure that were already being analyzed. This revision removes the concept of timestamp and merge it with the concept of analysis status. This can be simplified further once the analysis always goes through `Ondemand.analyze`. Reviewed By: cristianoc Differential Revision: D4610371 fbshipit-source-id: 0fc516b --- infer/src/backend/callbacks.ml | 4 +--- infer/src/backend/interproc.ml | 24 ++++++---------------- infer/src/backend/ondemand.ml | 16 +++++---------- infer/src/backend/specs.ml | 36 ++++++++++++++------------------- infer/src/backend/specs.mli | 21 ++++++++++--------- infer/src/base/Serialization.ml | 2 +- infer/src/checkers/summary.ml | 6 ++---- 7 files changed, 42 insertions(+), 67 deletions(-) diff --git a/infer/src/backend/callbacks.ml b/infer/src/backend/callbacks.ml index db00d649f..8f8896816 100644 --- a/infer/src/backend/callbacks.ml +++ b/infer/src/backend/callbacks.ml @@ -181,9 +181,7 @@ let iterate_callbacks call_graph exe_env = (* Store all the summaries to disk *) List.iter ~f:(fun pname -> - let updated_summary_opt = - Option.map (Specs.get_summary pname) ~f:Specs.increment_timestamp in - Option.iter ~f:(Specs.store_summary pname) updated_summary_opt) + Specs.store_summary pname (Specs.get_summary_unsafe "Checkers: store summaries" pname)) procs_to_analyze; Config.curr_language := saved_language diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index db9ee3a66..54ace86ed 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -533,8 +533,9 @@ let forward_tabulate tenv pdesc wl source = let summary = Specs.get_summary_unsafe "forward_tabulate" proc_name in let phase_string = if Specs.equal_phase (Specs.get_phase summary) Specs.FOOTPRINT then "FP" else "RE" in - let timestamp = Specs.get_timestamp summary in - F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) in + let status = Specs.get_status summary in + F.sprintf + "[%s:%s] %s" phase_string (Specs.string_of_status status) (Procname.to_string proc_name) in L.d_strln ("**** " ^ (log_string pname) ^ " " ^ "Node: " ^ string_of_int (Procdesc.Node.get_id curr_node :> int) ^ ", " ^ "Procedure: " ^ Procname.to_string pname ^ ", " ^ @@ -989,17 +990,9 @@ type exe_phase = (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.p [go ()] was interrupted by and exception. *) let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source : exe_phase = - let summary = Specs.get_summary_unsafe "check_recursion_level" pname in + let summary = Specs.get_summary_unsafe "perform_analysis_phase" pname in let start_node = Procdesc.get_start_node pdesc in - let check_recursion_level () = - let recursion_level = Specs.get_timestamp summary in - if recursion_level > Config.max_recursion then - begin - L.err "Reached maximum level of recursion, raising a Timeout@."; - raise (SymOp.Analysis_failure_exe (FKrecursion_timeout recursion_level)) - end in - let compute_footprint () : exe_phase = let go (wl : Worklist.t) () = let init_prop = initial_prop_from_emp tenv pdesc in @@ -1020,7 +1013,6 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source L.d_strln "initial props ="; Propset.d Prop.prop_emp init_props; L.d_ln (); L.d_ln(); L.d_decrease_indent 1; - check_recursion_level (); Worklist.add wl start_node; Config.arc_mode := Hashtbl.mem @@ -1057,7 +1049,6 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source let valid_specs = ref [] in let go () = L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp pname; - check_recursion_level (); let filter p = let wl = path_set_create_worklist pdesc in let speco = execute_filter_prop wl tenv pdesc start_node p source in @@ -1286,8 +1277,7 @@ let update_specs tenv proc_name phase (new_specs : Specs.NormSpec.t list) (** update a summary after analysing a procedure *) let update_summary tenv prev_summary specs phase proc_name elapsed res = let normal_specs = List.map ~f:(Specs.spec_normalize tenv) specs in - let new_specs, changed = update_specs tenv proc_name phase normal_specs in - let timestamp = max 1 (prev_summary.Specs.timestamp + if changed then 1 else 0) 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 @@ -1310,7 +1300,6 @@ let update_summary tenv prev_summary specs phase proc_name elapsed res = Specs.phase; stats; payload; - timestamp; } @@ -1355,8 +1344,7 @@ let transition_footprint_re_exe tenv proc_name joined_pres = { summary.Specs.payload with Specs.preposts = Some specs; } in { summary with - Specs.timestamp = 0; - phase = Specs.RE_EXECUTION; + Specs.phase = Specs.RE_EXECUTION; payload; } in Specs.add_summary proc_name summary' diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index b87dbc804..e75b1a744 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -55,7 +55,7 @@ let should_be_analyzed proc_name proc_attributes = let already_analyzed () = match Specs.get_summary proc_name with | Some summary -> - Specs.get_timestamp summary > 0 + Specs.equal_status (Specs.get_status summary) Specs.Analyzed | None -> false in proc_attributes.ProcAttributes.is_defined && (* we have the implementation *) @@ -142,29 +142,23 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc then Some callee_pdesc else None in Specs.reset_summary call_graph callee_pname attributes_opt callee_pdesc_option; - Specs.set_status callee_pname Specs.ACTIVE; + Specs.set_status callee_pname Specs.Active; source in let postprocess source = decr nesting; let summary = Specs.get_summary_unsafe "ondemand" callee_pname in - let summary' = - { summary with - Specs.status = Specs.INACTIVE; - timestamp = summary.Specs.timestamp + 1 } in - Specs.store_summary callee_pname summary'; + Specs.store_summary callee_pname summary; Printer.write_proc_html source false callee_pdesc; - summary' in + summary in let log_error_and_continue exn kind = Reporting.log_error callee_pname exn; let prev_summary = Specs.get_summary_unsafe "Ondemand.do_analysis" callee_pname in - let timestamp = max 1 (prev_summary.Specs.timestamp) in let stats = { prev_summary.Specs.stats with Specs.stats_failure = Some kind } in let payload = { prev_summary.Specs.payload with Specs.preposts = Some []; } in - let new_summary = - { prev_summary with Specs.stats; payload; timestamp; } in + let new_summary = { prev_summary with Specs.stats; payload } in Specs.store_summary callee_pname new_summary; new_summary in diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 306af6bdf..a1f34ba35 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -305,7 +305,15 @@ type stats = call_stats : call_stats; } -type status = ACTIVE | INACTIVE | STALE [@@deriving compare] +type status = Initialized | Active | Analyzed [@@deriving compare] + +let string_of_status = function + | Initialized -> "Initialized" + | Active -> "Active" + | Analyzed -> "Analyzed" + +let pp_status fmt status = + F.fprintf fmt "%s" (string_of_status status) let equal_status = [%compare.equal : status] @@ -335,8 +343,7 @@ type summary = { payload: payload; (** payload containing the result of some analysis *) sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) stats: stats; (** statistics: execution time and list of errors *) - status: status; (** ACTIVE when the proc is being analyzed *) - timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) + status: status; (** Analysis status of the procedure *) attributes : ProcAttributes.t; (** Attributes of the procedure *) proc_desc_option : Procdesc.t option; } @@ -407,12 +414,6 @@ let pp_specs pe fmt specs = F.fprintf fmt "\\subsection*{Spec %d of %d}@\n\\(%a\\)@\n" !cnt total (pp_spec pe None) spec) specs -let describe_timestamp summary = - ("Timestamp", Printf.sprintf "%d" summary.timestamp) - -let describe_status summary = - ("Status", if equal_status summary.status ACTIVE then "ACTIVE" else "INACTIVE") - let describe_phase summary = ("Phase", if equal_phase summary.phase FOOTPRINT then "FOOTPRINT" else "RE_EXECUTION") @@ -444,8 +445,7 @@ let get_specs_from_payload summary = let pp_summary_no_stats_specs fmt summary = let pp_pair fmt (x, y) = F.fprintf fmt "%s: %s" x y in F.fprintf fmt "%s@\n" (get_signature summary); - F.fprintf fmt "%a@\n" pp_pair (describe_timestamp summary); - F.fprintf fmt "%a@\n" pp_pair (describe_status summary); + F.fprintf fmt "%a@\n" pp_status summary.status; F.fprintf fmt "%a@\n" pp_pair (describe_phase summary) let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety; buffer_overrun } = @@ -561,8 +561,9 @@ let store_summary pname (summ1: summary) = 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) summ3 + Serialization.write_to_file summary_serializer (res_dir_specs_filename pname) final_summary (** Load procedure summary from the given file *) let load_summary specs_file = @@ -668,13 +669,7 @@ let get_status summary = summary.status let is_active summary = - equal_status (get_status summary) ACTIVE - -let get_timestamp summary = - summary.timestamp - -let increment_timestamp summary = - { summary with timestamp = summary.timestamp + 1 } + equal_status (get_status summary) Active let get_proc_name summary = summary.attributes.ProcAttributes.proc_name @@ -746,8 +741,7 @@ let init_summary sessions = ref 0; payload = empty_payload; stats = empty_stats calls in_out_calls_opt; - status = INACTIVE; - timestamp = 0; + status = Initialized; attributes = { proc_attributes with ProcAttributes.proc_flags = proc_flags; }; diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 0e4c9a838..02768f6ad 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -115,7 +115,17 @@ type stats = call_stats : CallStats.t; } -type status = ACTIVE | INACTIVE | STALE +(** Analysis status of the procedure: + - Initialized means that the summary has been created by the procedure has not been analyzed yet + - Active meas that the procedure is being analyzed + - Analyzed means that the analysis of the procedure is finished *) +type status = Initialized | Active | Analyzed + +val equal_status : status -> status -> bool + +val string_of_status : status -> string + +val pp_status : Format.formatter -> status -> unit type phase = FOOTPRINT | RE_EXECUTION @@ -144,8 +154,7 @@ type summary = { payload: payload; (** payload containing the result of some analysis *) sessions: int ref; (** Session number: how many nodes went trough symbolic execution *) stats: stats; (** statistics: execution time and list of errors *) - status: status; (** ACTIVE when the proc is being analyzed *) - timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *) + status: status; (** Analysis status of the procedure *) attributes : ProcAttributes.t; (** Attributes of the procedure *) proc_desc_option : Procdesc.t option; } @@ -198,12 +207,6 @@ val get_specs_from_payload : summary -> Prop.normal spec list (** @deprecated Return the summary for the procedure name. Raises an exception when not found. *) val get_summary_unsafe : string -> Procname.t -> summary -(** Return the current timestamp for the summary *) -val get_timestamp : summary -> int - -(** Increment the number of times a summary has been updated *) -val increment_timestamp : summary -> summary - (** Return the status (active v.s. inactive) of a procedure summary *) val get_status : summary -> status diff --git a/infer/src/base/Serialization.ml b/infer/src/base/Serialization.ml index 33b6e63cb..07b5c5bf5 100644 --- a/infer/src/base/Serialization.ml +++ b/infer/src/base/Serialization.ml @@ -34,7 +34,7 @@ module Key = struct end (** version of the binary files, to be incremented for each change *) -let version = 26 +let version = 27 (** Retry the function while an exception filtered is thrown, diff --git a/infer/src/checkers/summary.ml b/infer/src/checkers/summary.ml index cf7b2ed39..32706c9bc 100644 --- a/infer/src/checkers/summary.ml +++ b/infer/src/checkers/summary.ml @@ -24,8 +24,7 @@ module type S = sig type summary (* type astate*) - (** Write the [summary] for the procname to persistent storage. Returns the summary actually - written. *) + (** Write the [summary] for the procname to persistent storage. *) val write_summary : Procname.t -> summary -> unit (** read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis @@ -40,8 +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 - let timestamp = global_summary.timestamp + 1 in - Specs.store_summary pname { global_summary with payload; timestamp; } + Specs.store_summary pname { global_summary with payload; } | None -> failwithf "Summary for %a should exist, but does not!@." Procname.pp pname