[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

@@ -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 =
+        Specs.store_summary pname (Specs.get_summary_unsafe "Checkers: store summaries" pname))
-          Option.map (Specs.get_summary pname) ~f:Specs.increment_timestamp in
-        Option.iter ~f:(Specs.store_summary pname) updated_summary_opt)
     procs_to_analyze;
 
   Config.curr_language := saved_language

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
+      let status = Specs.get_status summary in
-      F.sprintf "[%s:%d] %s" phase_string timestamp (Procname.to_string proc_name) 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 new_specs, _ = 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 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;
+        Specs.phase = Specs.RE_EXECUTION;
-        phase = Specs.RE_EXECUTION;
         payload;
       } in
   Specs.add_summary proc_name summary'

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' =
+    Specs.store_summary callee_pname summary;
-      { summary with
-        Specs.status = Specs.INACTIVE;
-        timestamp = summary.Specs.timestamp + 1 } in
-    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 =
+    let new_summary = { prev_summary with Specs.stats; payload } in
-      { prev_summary with Specs.stats; payload; timestamp; } in
     Specs.store_summary callee_pname new_summary;
     new_summary in
 

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 *)
+  status: status; (** Analysis status of the procedure *)
-  timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *)
   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_status summary.status;
-  F.fprintf fmt "%a@\n" pp_pair (describe_status summary);
   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
+  equal_status (get_status summary) Active
-
-let get_timestamp summary =
-  summary.timestamp
-
-let increment_timestamp summary =
-  { summary with timestamp = summary.timestamp + 1 }
 
 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;
+      status = Initialized;
-      timestamp = 0;
       attributes =
         { proc_attributes with
           ProcAttributes.proc_flags = proc_flags; };

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 *)
+  status: status; (** Analysis status of the procedure *)
-  timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *)
   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
 

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,

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
+  (** Write the [summary] for the procname to persistent storage. *)
-      written. *)
   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; }
-        Specs.store_summary pname { global_summary with payload; timestamp; }
     | None ->
         failwithf "Summary for %a should exist, but does not!@." Procname.pp pname