[sledge] Add coverage statistics to test report

Reviewed By: jvillard

Differential Revision: D24989065

fbshipit-source-id: e0385df79

sledge/cli/sledge_cli.ml

@@ -141,6 +141,7 @@ let analyze =
     Domain_sh.simplify_states := not no_simplify_states ;
     Timer.enabled := stats ;
     exec {bound; skip_throw; function_summaries; entry_points; globals} pgm ;
+    Report.coverage pgm ;
     Report.safe_or_unsafe ()
 
 let analyze_cmd =

sledge/report/sledge_report.ml

@@ -14,15 +14,18 @@ let read filename =
   List.iter sexps ~f:(fun sexp ->
       let {Report.name; entry} = Report.t_of_sexp sexp in
       match (Tbl.find_opt tbl name, entry) with
-      | None, ProcessTimes ptimes -> Tbl.replace tbl name ([ptimes], [], [])
+      | None, ProcessTimes t -> Tbl.replace tbl name ([t], [], [], [])
-      | None, GcStats gc -> Tbl.replace tbl name ([], [gc], [])
+      | None, GcStats g -> Tbl.replace tbl name ([], [g], [], [])
-      | None, Status status -> Tbl.replace tbl name ([], [], [status])
+      | None, Coverage c -> Tbl.replace tbl name ([], [], [c], [])
-      | Some (times, gcs, statuses), ProcessTimes ptimes ->
+      | None, Status s -> Tbl.replace tbl name ([], [], [], [s])
-          Tbl.replace tbl name (ptimes :: times, gcs, statuses)
+      | Some (times, gcs, coverages, statuses), ProcessTimes ptimes ->
-      | Some (times, gcs, statuses), GcStats gc ->
+          Tbl.replace tbl name (ptimes :: times, gcs, coverages, statuses)
-          Tbl.replace tbl name (times, gc :: gcs, statuses)
+      | Some (times, gcs, coverages, statuses), GcStats gc ->
-      | Some (times, gc, statuses), Status status ->
+          Tbl.replace tbl name (times, gc :: gcs, coverages, statuses)
-          Tbl.replace tbl name (times, gc, status :: statuses) ) ;
+      | Some (times, gcs, coverages, statuses), Coverage c ->
+          Tbl.replace tbl name (times, gcs, c :: coverages, statuses)
+      | Some (times, gc, coverages, statuses), Status status ->
+          Tbl.replace tbl name (times, gc, coverages, status :: statuses) ) ;
   tbl
 
 type times = {etime: float; utime: float; stime: float}
@@ -33,6 +36,8 @@ type ('t, 'g) row =
   ; times_deltas: 't
   ; gcs: 'g
   ; gcs_deltas: 'g
+  ; cov: Report.coverage list
+  ; cov_deltas: Report.coverage list option
   ; status: Report.status list
   ; status_deltas: Report.status list option }
 
@@ -75,6 +80,27 @@ let add_gcs base_gcs gcs row =
   if List.is_empty gcs then {row with gcs_deltas= Option.to_list base_gcs}
   else List.fold ~f:(add_gc base_gcs) gcs row
 
+let add_cov base_cov cov row =
+  if List.mem ~eq:Report.equal_coverage cov row.cov then row
+  else
+    let cov_deltas =
+      match base_cov with
+      | Some (base_cov :: _) ->
+          let covd =
+            Report.
+              { steps= cov.steps - base_cov.steps
+              ; hit= cov.hit - base_cov.hit
+              ; fraction= cov.fraction -. base_cov.fraction }
+          in
+          Some (covd :: Option.value row.cov_deltas ~default:[])
+      | _ -> None
+    in
+    {row with cov= cov :: row.cov; cov_deltas}
+
+let add_covs base_cov covs row =
+  let row = List.fold ~f:(add_cov base_cov) covs row in
+  {row with cov= List.sort ~cmp:(Ord.opp Report.compare_coverage) row.cov}
+
 let add_status base_status status row =
   if List.mem ~eq:Report.equal_status status row.status then row
   else
@@ -103,9 +129,9 @@ let ave_floats flts =
   else sum /. Float.of_int num
 
 let combine name b_result c_result =
-  let base_times, base_gcs, base_status =
+  let base_times, base_gcs, base_cov, base_status =
     match b_result with
-    | Some (times, gcs, statuses) ->
+    | Some (times, gcs, covs, statuses) ->
         let times =
           if List.is_empty times then None
           else
@@ -149,11 +175,12 @@ let combine name b_result c_result =
                 ; promoted= ave_floats promos
                 ; peak_size= ave_floats peaks }
         in
+        let covs = if List.is_empty covs then None else Some covs in
         let status =
           Some (List.sort_uniq ~cmp:Report.compare_status statuses)
         in
-        (times, gcs, status)
+        (times, gcs, covs, status)
-    | None -> (None, None, None)
+    | None -> (None, None, None, None)
   in
   let row =
     { name
@@ -161,6 +188,8 @@ let combine name b_result c_result =
     ; times_deltas= []
     ; gcs= []
     ; gcs_deltas= []
+    ; cov= []
+    ; cov_deltas= None
     ; status= []
     ; status_deltas= None }
   in
@@ -168,12 +197,14 @@ let combine name b_result c_result =
   | None ->
       let times_deltas = Option.to_list base_times in
       let gcs_deltas = Option.to_list base_gcs in
+      let cov_deltas = base_cov in
       let status_deltas = base_status in
-      {row with times_deltas; gcs_deltas; status_deltas}
+      {row with times_deltas; gcs_deltas; cov_deltas; status_deltas}
-  | Some (c_times, c_gcs, c_statuses) ->
+  | Some (c_times, c_gcs, c_cov, c_statuses) ->
       row
       |> add_times base_times c_times
       |> add_gcs base_gcs c_gcs
+      |> add_covs base_cov c_cov
       |> add_statuses base_status c_statuses
 
 type ranges =
@@ -258,7 +289,8 @@ let color max dat =
     Printf.sprintf "#%2x%2x%2x" (to_int r) (to_int g) (to_int b)
   in
   let rat = dat /. max in
-  if Float.is_nan rat then rgb_to_hex lace else rgb_to_hex (gradient rat)
+  if Float.(abs dat < 0.000001 || is_nan rat) then rgb_to_hex lace
+  else rgb_to_hex (gradient rat)
 
 let write_html ranges rows chan =
   let pf fmt = Printf.fprintf chan fmt in
@@ -295,11 +327,24 @@ let write_html ranges rows chan =
           <th>&Delta;%%<br></th>
           <th>Status</th>
           <th>&Delta;<br></th>
+          <th>Steps</th>
+          <th>&Delta;<br></th>
+          <th>Cover</th>
+          <th>%%</th>
+          <th>&Delta;<br></th>
+          <th>&Delta;%%<br></th>
         </tr>|} ;
   pf "\n" ;
   Iter.iter rows ~f:(fun row ->
-      let {name; times; times_deltas; gcs; gcs_deltas; status; status_deltas}
+      let { name
-          =
+          ; times
+          ; times_deltas
+          ; gcs
+          ; gcs_deltas
+          ; cov
+          ; cov_deltas
+          ; status
+          ; status_deltas } =
         row
       in
       let max_name_length = 50 in
@@ -354,6 +399,41 @@ let write_html ranges rows chan =
         let status_to_string = Format.asprintf "%a" Report.pp_status in
         Printf.fprintf ppf "%s" (String.take 50 (status_to_string s))
       in
+      let steps attr ppf = function
+        | [] -> Printf.fprintf ppf "<td %s></td>\n" attr
+        | cs ->
+            List.iter cs ~f:(fun {Report.steps} ->
+                if steps = 0 then Printf.fprintf ppf "<td></td>\n"
+                else
+                  Printf.fprintf ppf "<td %s align=\"right\">%i</td>\n" attr
+                    steps )
+      in
+      let hit attr ppf = function
+        | [] -> Printf.fprintf ppf "<td %s></td>\n" attr
+        | cs ->
+            List.iter cs ~f:(fun {Report.hit} ->
+                if hit = 0 then Printf.fprintf ppf "<td></td>\n"
+                else
+                  Printf.fprintf ppf "<td %s align=\"right\">%i</td>\n" attr
+                    hit )
+      in
+      let coverage attr ppf = function
+        | [] -> Printf.fprintf ppf "<td align=\"right\"></td>\n"
+        | cs ->
+            List.iter cs ~f:(fun {Report.fraction} ->
+                if Float.(abs fraction < 0.000001) then
+                  Printf.fprintf ppf "<td></td>\n"
+                else
+                  Printf.fprintf ppf
+                    "<td %s align=\"right\">%12.0f%%</td>\n" attr
+                    (Base.Float.round_decimal ~decimal_digits:2
+                       (100. *. fraction)) )
+      in
+      let coveraged coverage ppf cs =
+        let cs = Option.value cs ~default:[] in
+        let attr = if List.is_empty cs then "" else " class=\"neutral\"" in
+        Printf.fprintf ppf "%a" (coverage attr) cs
+      in
       let stat ppf = function
         | [] ->
             Printf.fprintf ppf
@@ -437,6 +517,13 @@ let write_html ranges rows chan =
              <td style=\"border-left: 2px solid \
              #eee8d5\";></td><td></td><td></td>\n" ) ;
       pf "%a%a" stat status statd status_deltas ;
+      pf "%a%a"
+        (steps " style=\"border-left: 2px solid #eee8d5\";")
+        cov (coveraged steps) cov_deltas ;
+      pf "%a%a"
+        (hit " style=\"border-left: 2px solid #eee8d5\";")
+        cov (coverage "") cov ;
+      pf "%a%a" (coveraged hit) cov_deltas (coveraged coverage) cov_deltas ;
       pf "</tr>\n" ) ;
   pf "<table>\n" ;
   pf "</body></html>\n"
@@ -488,6 +575,8 @@ let add_total rows =
     ; times_deltas= Some {etime= 0.; utime= 0.; stime= 0.}
     ; gcs= Some {Report.allocated= 0.; promoted= 0.; peak_size= 0.}
     ; gcs_deltas= Some {Report.allocated= 0.; promoted= 0.; peak_size= 0.}
+    ; cov= []
+    ; cov_deltas= None
     ; status= []
     ; status_deltas= None }
   in

sledge/src/control.ml

@@ -119,7 +119,9 @@ module Make (Dom : Domain_intf.Dom) = struct
         | _ -> acc
       in
       let n = count_f_in_stack 0 return stk in
-      ( if n > bound then None
+      ( if n > bound then (
+        Report.hit_bound n ;
+        None )
       else Some (push_throw throw (push_return call from_call stk)) )
       |>
       [%Trace.retn fun {pf} _ ->
@@ -219,6 +221,7 @@ module Make (Dom : Domain_intf.Dom) = struct
       let depth = if retreating then depth + 1 else depth in
       if depth > bound then (
         [%Trace.info "prune: %i: %a" depth Edge.pp edge] ;
+        Report.hit_bound bound ;
         work )
       else
         let pq = FHeap.add pq (depth, edge) in
@@ -395,7 +398,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 () ;
+    Report.step_term block.term ;
     match block.term with
     | Switch {key; tbl; els} ->
         IArray.fold
@@ -460,7 +463,7 @@ module Make (Dom : Domain_intf.Dom) = struct
    fun inst state ->
     [%Trace.info
       "@[<2>exec inst@\n@[%a@]@\n%a@]" Dom.pp state Llair.Inst.pp inst] ;
-    Report.step () ;
+    Report.step_inst inst ;
     Dom.exec_inst inst state
     |> function
     | Some state -> Result.Ok state | None -> Result.Error (state, inst)

sledge/src/llair/llair.ml

@@ -335,7 +335,12 @@ and dummy_func =
 (** Instructions *)
 
 module Inst = struct
+  module T = struct
     type t = inst [@@deriving compare, equal, hash, sexp]
+  end
+
+  include T
+  module Tbl = HashTable.Make (T)
 
   let pp = pp_inst
   let move ~reg_exps ~loc = Move {reg_exps; loc}
@@ -404,7 +409,12 @@ end
 (** Basic-Block Terminators *)
 
 module Term = struct
+  module T = struct
     type t = term [@@deriving compare, equal, hash, sexp_of]
+  end
+
+  include T
+  module Tbl = HashTable.Make (T)
 
   let pp = pp_term
 
@@ -519,7 +529,7 @@ module Func = struct
     | {entry= {cmnd; term= Unreachable; _}; _} -> IArray.is_empty cmnd
     | _ -> false
 
-  let fold_cfg ~f func s =
+  let fold_cfg func s ~f =
     let seen = BlockS.create 0 in
     let rec fold_cfg_ blk s =
       if not (BlockS.add seen blk) then s

sledge/src/llair/llair.mli

@@ -102,7 +102,7 @@ and func = private
   ; entry: block
   ; loc: Loc.t }
 
-type functions
+type functions = func Function.Map.t
 
 type program = private
   { globals: GlobalDefn.t iarray  (** Global definitions. *)
@@ -125,6 +125,8 @@ module Inst : sig
   val loc : inst -> Loc.t
   val locals : inst -> Reg.Set.t
   val fold_exps : inst -> 's -> f:(Exp.t -> 's -> 's) -> 's
+
+  module Tbl : HashTable.S with type key := t
 end
 
 module Jump : sig
@@ -164,6 +166,8 @@ module Term : sig
   val throw : exc:Exp.t -> loc:Loc.t -> term
   val unreachable : term
   val loc : term -> Loc.t
+
+  module Tbl : HashTable.S with type key := t
 end
 
 module Block : sig
@@ -203,6 +207,9 @@ module Func : sig
   val find : Function.t -> functions -> t option
   (** Look up a function of the given name in the given functions. *)
 
+  val fold_cfg : func -> 'a -> f:(block -> 'a -> 'a) -> 'a
+  (** Fold over the blocks of the control-flow graph of a function. *)
+
   val is_undefined : t -> bool
   (** Holds of functions that are declared but not defined. *)
 end

sledge/src/report.ml

@@ -38,13 +38,25 @@ let invalid_access_term fmt_thunk term =
 (** Functional statistics *)
 
 let steps = ref 0
-let step () = Int.incr steps
+let hit_insts = Llair.Inst.Tbl.create ()
+let hit_terms = Llair.Term.Tbl.create ()
+
+let step_inst i =
+  Llair.Inst.Tbl.incr hit_insts i ;
+  Int.incr steps
+
+let step_term t =
+  Llair.Term.Tbl.incr hit_terms t ;
+  Int.incr steps
+
+let bound = ref (-1)
+let hit_bound n = bound := n
 
 (** Status reporting *)
 
 type status =
-  | Safe of {steps: int}
+  | Safe of {bound: int}
-  | Unsafe of {alarms: int; steps: int}
+  | Unsafe of {alarms: int; bound: int}
   | Ok
   | Unsound
   | Incomplete
@@ -60,8 +72,10 @@ type status =
 let pp_status ppf stat =
   let pf fmt = Format.fprintf ppf fmt in
   match stat with
-  | Safe {steps} -> pf "Safe (%i)" steps
+  | Safe {bound= -1} -> pf "Safe"
-  | Unsafe {alarms; steps} -> pf "Unsafe: %i (%i)" alarms steps
+  | Safe {bound} -> pf "Safe (%i)" bound
+  | Unsafe {alarms; bound= -1} -> pf "Unsafe: %i" alarms
+  | Unsafe {alarms; bound} -> pf "Unsafe: %i (%i)" alarms bound
   | Ok -> pf "Ok"
   | Unsound -> pf "Unsound"
   | Incomplete -> pf "Incomplete"
@@ -74,8 +88,8 @@ let pp_status ppf stat =
   | UnknownError msg -> pf "Unknown error: %s" msg
 
 let safe_or_unsafe () =
-  if !invalid_access_count = 0 then Safe {steps= !steps}
+  if !invalid_access_count = 0 then Safe {bound= !bound}
-  else Unsafe {alarms= !invalid_access_count; steps= !steps}
+  else Unsafe {alarms= !invalid_access_count; bound= !bound}
 
 type gc_stats = {allocated: float; promoted: float; peak_size: float}
 [@@deriving sexp]
@@ -84,10 +98,14 @@ type times =
   {etime: float; utime: float; stime: float; cutime: float; cstime: float}
 [@@deriving sexp]
 
+type coverage = {steps: int; hit: int; fraction: float}
+[@@deriving compare, equal, sexp]
+
 type entry =
   | ProcessTimes of times
   | GcStats of gc_stats
   | Status of status
+  | Coverage of coverage
 [@@deriving sexp]
 
 let process_times () =
@@ -140,4 +158,16 @@ let init ?append filename =
       output (gc_stats ()) ;
       Option.iter ~f:Out_channel.close_no_err !chan )
 
+let coverage (pgm : Llair.program) =
+  let size =
+    Llair.Function.Map.fold pgm.functions 0 ~f:(fun ~key:_ ~data:func n ->
+        Llair.Func.fold_cfg func n ~f:(fun blk n ->
+            n + IArray.length blk.cmnd + 1 ) )
+  in
+  let hit =
+    Llair.Inst.Tbl.length hit_insts + Llair.Term.Tbl.length hit_terms
+  in
+  let fraction = Float.(of_int hit /. of_int size) in
+  output (Coverage {steps= !steps; hit; fraction})
+
 let status s = output (Status s)

sledge/src/report.mli

@@ -8,14 +8,16 @@
 (** Issue reporting *)
 
 val init : ?append:bool -> string -> unit
-val step : unit -> unit
+val step_inst : Llair.inst -> unit
+val step_term : Llair.term -> unit
+val hit_bound : int -> unit
 val unknown_call : Llair.term -> unit
 val invalid_access_inst : (Format.formatter -> unit) -> Llair.inst -> unit
 val invalid_access_term : (Format.formatter -> unit) -> Llair.term -> unit
 
 type status =
-  | Safe of {steps: int}
+  | Safe of {bound: int}
-  | Unsafe of {alarms: int; steps: int}
+  | Unsafe of {alarms: int; bound: int}
   | Ok
   | Unsound
   | Incomplete
@@ -31,17 +33,23 @@ type status =
 val pp_status : status pp
 val safe_or_unsafe : unit -> status
 val status : status -> unit
+val coverage : Llair.program -> unit
 
 type gc_stats = {allocated: float; promoted: float; peak_size: float}
 [@@deriving sexp]
 
 type times =
   {etime: float; utime: float; stime: float; cutime: float; cstime: float}
+[@@deriving sexp]
+
+type coverage = {steps: int; hit: int; fraction: float}
+[@@deriving compare, equal, sexp]
 
 type entry =
   | ProcessTimes of times
   | GcStats of gc_stats
   | Status of status
+  | Coverage of coverage
 [@@deriving sexp]
 
 type t = {name: string; entry: entry} [@@deriving sexp]