Move get_phase from Tabulation to BiabductionSummary

Reviewed By: jvillard

Differential Revision: D7987204

fbshipit-source-id: be6b44e

infer/src/backend/ondemand.ml

@@ -138,9 +138,9 @@ let run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc =
     let stats = Summary.Stats.update summary.stats ~failure_kind:kind in
     let payload =
       let biabduction =
-        Some BiabductionSummary.{preposts= []; phase= Tabulation.get_phase summary}
+        Some BiabductionSummary.{preposts= []; phase= summary.payload.biabduction |> opt_get_phase}
       in
-      {summary.payload with Summary.biabduction}
+      {summary.payload with biabduction}
     in
     let new_summary = {summary with stats; payload} in
     Summary.store new_summary ; remove_active callee_pname ; log_elapsed_time () ; new_summary

infer/src/biabduction/BiabductionSummary.ml

@@ -233,6 +233,10 @@ type phase = FOOTPRINT | RE_EXECUTION [@@deriving compare]
 
 let equal_phase = [%compare.equal : phase]
 
+let string_of_phase = function FOOTPRINT -> "FOOTPRINT" | RE_EXECUTION -> "RE_EXECUTION"
+
+let string_of_phase_short = function FOOTPRINT -> "FP" | RE_EXECUTION -> "RE"
+
 (** Print the spec *)
 let pp_spec pe num_opt fmt spec =
   let pp_num_opt fmt = function
@@ -274,11 +278,11 @@ let pp_specs pe fmt specs =
           F.fprintf fmt "%a<br>@\n" (pp_spec pe (Some (cnt + 1, total))) spec )
 
 
-let string_of_phase = function FOOTPRINT -> "FOOTPRINT" | RE_EXECUTION -> "RE_EXECUTION"
-
 let get_specs_from_preposts preposts = Option.value_map ~f:NormSpec.tospecs ~default:[] preposts
 
 type t = {preposts: NormSpec.t list; phase: phase}
 
+let opt_get_phase = function None -> FOOTPRINT | Some {phase} -> phase
+
 let pp pe fmt {preposts; phase} =
   F.fprintf fmt "phase= %s@\n%a" (string_of_phase phase) (pp_specs pe) (NormSpec.tospecs preposts)

infer/src/biabduction/BiabductionSummary.mli

@@ -85,8 +85,12 @@ type phase = FOOTPRINT | RE_EXECUTION
 
 val equal_phase : phase -> phase -> bool
 
+val string_of_phase_short : phase -> string
+
 val get_specs_from_preposts : NormSpec.t list option -> Prop.normal spec list
 
 type t = {preposts: NormSpec.t list; phase: phase}
 
+val opt_get_phase : t option -> phase
+
 val pp : Pp.env -> Format.formatter -> t -> unit

infer/src/biabduction/Tabulation.ml

@@ -123,12 +123,6 @@ let get_specs_from_payload summary =
   |> BiabductionSummary.get_specs_from_preposts
 
 
-(** Return the current phase for the proc *)
-let get_phase summary =
-  Option.value_map summary.Summary.payload.biabduction ~default:BiabductionSummary.FOOTPRINT ~f:
-    (fun BiabductionSummary.({phase}) -> phase )
-
-
 (** Rename the variables in the spec. *)
 let spec_rename_vars pname spec =
   let prop_add_callee_suffix p =

infer/src/biabduction/Tabulation.mli

@@ -53,8 +53,5 @@ val exe_function_call :
   -> (Prop.normal Prop.t * Paths.Path.t) list
 (** Execute the function call and return the list of results with return value *)
 
-val get_phase : Summary.t -> BiabductionSummary.phase
-(** Return the current phase for the proc *)
-
 val get_specs_from_payload : Summary.t -> Prop.normal BiabductionSummary.spec list
 (** Get the specs from the payload of the summary. *)

infer/src/biabduction/interproc.ml

@@ -435,7 +435,7 @@ let forward_tabulate exe_env tenv proc_cfg wl =
     let log_string proc_name =
       let summary = Summary.get_unsafe proc_name in
       let phase_string =
-        match Tabulation.get_phase summary with FOOTPRINT -> "FP" | RE_EXECUTION -> "RE"
+        BiabductionSummary.(summary.payload.biabduction |> opt_get_phase |> string_of_phase_short)
       in
       let status = Summary.get_status summary in
       F.sprintf "[%s:%s] %s" phase_string (Summary.Status.to_string status)
@@ -904,7 +904,7 @@ let perform_analysis_phase exe_env tenv (summary: Summary.t) (proc_cfg: ProcCfg.
     in
     (go, get_results)
   in
-  match Tabulation.get_phase summary with
+  match BiabductionSummary.opt_get_phase summary.payload.biabduction with
   | FOOTPRINT ->
       compute_footprint ()
   | RE_EXECUTION ->
@@ -1219,7 +1219,8 @@ let perform_transition proc_cfg tenv proc_name =
     transition_footprint_re_exe tenv proc_name joined_pres
   in
   match Summary.get proc_name with
-  | Some summary when BiabductionSummary.equal_phase (Tabulation.get_phase summary) FOOTPRINT ->
+  | Some summary
+    when BiabductionSummary.(summary.payload.biabduction |> opt_get_phase |> equal_phase FOOTPRINT) ->
       transition summary
   | _ ->
       ()