From 7bc2d6de124d435cef18d7fe686e42cbdf7b2184 Mon Sep 17 00:00:00 2001 From: Jeremy Dubreil Date: Mon, 8 May 2017 22:40:54 -0700 Subject: [PATCH] [infer][ondemand] confine the concept of currently analyzed method to the Ondemand module Summary: This actually fixes issues of infinite loop as the function `Specs.set_status` was saving the `Active` status in the summary from the specs table which could differ from the summary passed as argument to the checkers Reviewed By: sblackshear Differential Revision: D5025923 fbshipit-source-id: c23a6f9 --- infer/src/backend/ondemand.ml | 20 ++++++++++++++------ infer/src/backend/specs.ml | 16 +++------------- infer/src/backend/specs.mli | 11 ++--------- 3 files changed, 19 insertions(+), 28 deletions(-) diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 9b7d59d8a..a1857d9bb 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -47,11 +47,17 @@ let unset_callbacks () = let nesting = ref 0 +let is_active, add_active, remove_active = + let currently_analyzed = ref Typ.Procname.Set.empty in + let is_active proc_name = + Typ.Procname.Set.mem proc_name !currently_analyzed + and add_active proc_name = + currently_analyzed := Typ.Procname.Set.add proc_name !currently_analyzed + and remove_active proc_name = + currently_analyzed := Typ.Procname.Set.remove proc_name !currently_analyzed in + (is_active, add_active, remove_active) + let should_be_analyzed proc_name proc_attributes = - let currently_analyzed () = - match Specs.get_summary proc_name with - | None -> false - | Some summary -> Specs.is_active summary in let already_analyzed () = match Specs.get_summary proc_name with | Some summary -> @@ -59,7 +65,7 @@ let should_be_analyzed proc_name proc_attributes = | None -> false in proc_attributes.ProcAttributes.is_defined && (* we have the implementation *) - not (currently_analyzed ()) && (* avoid infinite loops *) + not (is_active proc_name) && (* avoid infinite loops *) not (already_analyzed ()) (* avoid re-analysis of the same procedure *) let procedure_should_be_analyzed proc_name = @@ -136,12 +142,13 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc then Some callee_pdesc else None in let initial_summary = Specs.reset_summary callee_pname attributes_opt callee_pdesc_option in - Specs.set_status callee_pname Specs.Active; + add_active callee_pname; initial_summary in let postprocess summary = decr nesting; Specs.store_summary summary; + remove_active callee_pname; Printer.write_proc_html callee_pdesc; log_elapsed_time (); summary in @@ -153,6 +160,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc { summary.Specs.payload with Specs.preposts = Some []; } in let new_summary = { summary with Specs.stats; payload } in Specs.store_summary new_summary; + remove_active callee_pname; log_elapsed_time (); new_summary in diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 671f3c9fc..0050b61a3 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -303,11 +303,10 @@ type stats = call_stats : call_stats; } -type status = Initialized | Active | Analyzed [@@deriving compare] +type status = Pending | Analyzed [@@deriving compare] let string_of_status = function - | Initialized -> "Initialized" - | Active -> "Active" + | Pending -> "Pending" | Analyzed -> "Analyzed" let pp_status fmt status = @@ -640,9 +639,6 @@ let summary_exists proc_name = let get_status summary = summary.status -let is_active summary = - equal_status (get_status summary) Active - let get_proc_name summary = summary.attributes.ProcAttributes.proc_name @@ -680,12 +676,6 @@ let store_summary (summ1: summary) = (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 - | None -> raise (Failure ("Specs.set_status: " ^ (Typ.Procname.to_string proc_name) ^ " Not_found")) - | Some summary -> add_summary proc_name { summary with status = status } - let empty_payload = { preposts = None; @@ -713,7 +703,7 @@ let init_summary sessions = ref 0; payload = empty_payload; stats = empty_stats calls; - status = Initialized; + status = Pending; attributes = { proc_attributes with ProcAttributes.proc_flags = proc_flags; }; diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index fc8af6bdd..45a4edbed 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -114,10 +114,9 @@ type stats = } (** 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 + - Pending means that the summary has been created by the procedure has not been analyzed yet - Analyzed means that the analysis of the procedure is finished *) -type status = Initialized | Active | Analyzed +type status = Pending | Analyzed val equal_status : status -> status -> bool @@ -200,9 +199,6 @@ val get_summary_unsafe : string -> Typ.Procname.t -> summary (** Return the status (active v.s. inactive) of a procedure summary *) val get_status : summary -> status -(** Check if the procedure is active *) -val is_active : summary -> bool - (** Initialize the summary for [proc_name] given dependent procs in list [depend_list]. This also stores the new summary in the spec table. *) val init_summary : @@ -254,9 +250,6 @@ val proc_resolve_attributes : Typ.Procname.t -> ProcAttributes.t option It's not defined, and there is no spec file for it. *) val proc_is_library : ProcAttributes.t -> bool -(** Set the current status for the proc *) -val set_status : Typ.Procname.t -> status -> unit - (** Convert spec into normal form w.r.t. variable renaming *) val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t