From 3ee953ebefdedef1a79c7cc0d980b311b296ed94 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 15 Sep 2020 01:48:54 -0700
Subject: [PATCH] [sledge] Test: Include steps stats in reports

Summary:
Increase the fidelity of the status in the analysis report slightly by
including the number of analysis steps taken.

Reviewed By: jvillard

Differential Revision: D23648493

fbshipit-source-id: 8050b7829
---
 sledge/report/sledge_report.ml |  2 +-
 sledge/src/control.ml          |  2 ++
 sledge/src/report.ml           | 18 +++++++++++++-----
 sledge/src/report.mli          |  5 +++--
 4 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/sledge/report/sledge_report.ml b/sledge/report/sledge_report.ml
index 029f0389c..74e3ea378 100644
--- a/sledge/report/sledge_report.ml
+++ b/sledge/report/sledge_report.ml
@@ -343,7 +343,7 @@ let write_html ranges rows chan =
         | ss ->
             List.iter ss ~f:(fun s ->
                 match (s : Report.status) with
-                | Safe | Unsafe _ | Ok ->
+                | Safe _ | Unsafe _ | Ok ->
                     Printf.fprintf ppf
                       "<td style=\"border-left: 2px solid #eee8d5\";>%a</td>\n"
                       pf_status s
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 05f92828c..f2491bddd 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -400,6 +400,7 @@ module Make (Dom : Domain_intf.Dom) = struct
    fun opts pgm stk state block ->
     [%Trace.info
       "@[<2>exec term@\n@[%a@]@\n%a@]" Dom.pp state Llair.Term.pp block.term] ;
+    Report.step () ;
     match block.term with
     | Switch {key; tbl; els} ->
         IArray.fold tbl
@@ -465,6 +466,7 @@ module Make (Dom : Domain_intf.Dom) = struct
    fun state inst ->
     [%Trace.info
       "@[<2>exec inst@\n@[%a@]@\n%a@]" Dom.pp state Llair.Inst.pp inst] ;
+    Report.step () ;
     Dom.exec_inst state inst |> Result.of_option ~error:(state, inst)
 
   let exec_block :
diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index e9a118640..ecaefdc2b 100644
--- a/sledge/src/report.ml
+++ b/sledge/src/report.ml
@@ -40,9 +40,16 @@ let invalid_access_inst fmt_thunk inst =
 let invalid_access_term fmt_thunk term =
   invalid_access fmt_thunk Llair.Term.pp term Llair.Term.loc
 
+(** Functional statistics *)
+
+let steps = ref 0
+let step () = Int.incr steps
+
+(** Status reporting *)
+
 type status =
-  | Safe
-  | Unsafe of int
+  | Safe of {steps: int}
+  | Unsafe of {alarms: int; steps: int}
   | Ok
   | Unsound
   | Incomplete
@@ -58,8 +65,8 @@ type status =
 let pp_status ppf stat =
   let pf fmt = Format.fprintf ppf fmt in
   match stat with
-  | Safe -> pf "Safe"
-  | Unsafe i -> pf "Unsafe: %i" i
+  | Safe {steps} -> pf "Safe (%i)" steps
+  | Unsafe {alarms; steps} -> pf "Unsafe: %i (%i)" alarms steps
   | Ok -> pf "Ok"
   | Unsound -> pf "Unsound"
   | Incomplete -> pf "Incomplete"
@@ -72,7 +79,8 @@ let pp_status ppf stat =
   | UnknownError msg -> pf "Unknown error: %s" msg
 
 let safe_or_unsafe () =
-  if !invalid_access_count = 0 then Safe else Unsafe !invalid_access_count
+  if !invalid_access_count = 0 then Safe {steps= !steps}
+  else Unsafe {alarms= !invalid_access_count; steps= !steps}
 
 type gc_stats = {allocated: float; promoted: float; peak_size: float}
 [@@deriving sexp]
diff --git a/sledge/src/report.mli b/sledge/src/report.mli
index 8d2b50f31..703771982 100644
--- a/sledge/src/report.mli
+++ b/sledge/src/report.mli
@@ -8,13 +8,14 @@
 (** Issue reporting *)
 
 val init : ?append:bool -> string -> unit
+val step : unit -> unit
 val unknown_call : Llair.term -> unit
 val invalid_access_inst : (Formatter.t -> unit) -> Llair.inst -> unit
 val invalid_access_term : (Formatter.t -> unit) -> Llair.term -> unit
 
 type status =
-  | Safe
-  | Unsafe of int
+  | Safe of {steps: int}
+  | Unsafe of {alarms: int; steps: int}
   | Ok
   | Unsound
   | Incomplete