[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

@@ -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
 

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"
+  | Pending -> "Pending"
-  | Active -> "Active"
   | 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; };

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
+    - Pending 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
+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