From 02625ac1ce1effb5b984627d547ffc591a211fc9 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 16 Nov 2020 12:53:37 -0800 Subject: [PATCH] [sledge] Add coverage statistics to test report Reviewed By: jvillard Differential Revision: D24989065 fbshipit-source-id: e0385df79 --- sledge/cli/sledge_cli.ml | 1 + sledge/report/sledge_report.ml | 125 ++++++++++++++++++++++++++++----- sledge/src/control.ml | 9 ++- sledge/src/llair/llair.ml | 16 ++++- sledge/src/llair/llair.mli | 9 ++- sledge/src/report.ml | 44 ++++++++++-- sledge/src/report.mli | 14 +++- 7 files changed, 183 insertions(+), 35 deletions(-) diff --git a/sledge/cli/sledge_cli.ml b/sledge/cli/sledge_cli.ml index fb1271329..a18a220cc 100644 --- a/sledge/cli/sledge_cli.ml +++ b/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 = diff --git a/sledge/report/sledge_report.ml b/sledge/report/sledge_report.ml index 1e2ba542c..36cb28fce 100644 --- a/sledge/report/sledge_report.ml +++ b/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, GcStats gc -> Tbl.replace tbl name ([], [gc], []) - | None, Status status -> Tbl.replace tbl name ([], [], [status]) - | Some (times, gcs, statuses), ProcessTimes ptimes -> - Tbl.replace tbl name (ptimes :: times, gcs, statuses) - | Some (times, gcs, statuses), GcStats gc -> - Tbl.replace tbl name (times, gc :: gcs, statuses) - | Some (times, gc, statuses), Status status -> - Tbl.replace tbl name (times, gc, status :: statuses) ) ; + | None, ProcessTimes t -> Tbl.replace tbl name ([t], [], [], []) + | None, GcStats g -> Tbl.replace tbl name ([], [g], [], []) + | None, Coverage c -> Tbl.replace tbl name ([], [], [c], []) + | None, Status s -> Tbl.replace tbl name ([], [], [], [s]) + | Some (times, gcs, coverages, statuses), ProcessTimes ptimes -> + Tbl.replace tbl name (ptimes :: times, gcs, coverages, statuses) + | Some (times, gcs, coverages, statuses), GcStats gc -> + Tbl.replace tbl name (times, gc :: gcs, coverages, 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) - | None -> (None, None, None) + (times, gcs, covs, status) + | 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} - | Some (c_times, c_gcs, c_statuses) -> + {row with times_deltas; gcs_deltas; cov_deltas; status_deltas} + | 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 = Δ%%
Status Δ
+ Steps + Δ
+ Cover + %% + Δ
+ Δ%%
|} ; 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 "\n" attr + | cs -> + List.iter cs ~f:(fun {Report.steps} -> + if steps = 0 then Printf.fprintf ppf "\n" + else + Printf.fprintf ppf "%i\n" attr + steps ) + in + let hit attr ppf = function + | [] -> Printf.fprintf ppf "\n" attr + | cs -> + List.iter cs ~f:(fun {Report.hit} -> + if hit = 0 then Printf.fprintf ppf "\n" + else + Printf.fprintf ppf "%i\n" attr + hit ) + in + let coverage attr ppf = function + | [] -> Printf.fprintf ppf "\n" + | cs -> + List.iter cs ~f:(fun {Report.fraction} -> + if Float.(abs fraction < 0.000001) then + Printf.fprintf ppf "\n" + else + Printf.fprintf ppf + "%12.0f%%\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 = \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 "\n" ) ; pf "\n" ; pf "\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 diff --git a/sledge/src/control.ml b/sledge/src/control.ml index 1a1af2d76..596c63ed7 100644 --- a/sledge/src/control.ml +++ b/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) diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index cd0d7454f..bb8504c37 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -335,7 +335,12 @@ and dummy_func = (** Instructions *) module Inst = struct - type t = inst [@@deriving compare, equal, hash, sexp] + 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 - type t = term [@@deriving compare, equal, hash, sexp_of] + 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 diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index ac650ad53..479bbcbeb 100644 --- a/sledge/src/llair/llair.mli +++ b/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 diff --git a/sledge/src/report.ml b/sledge/src/report.ml index b0760aa0e..fef446e4f 100644 --- a/sledge/src/report.ml +++ b/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} - | Unsafe of {alarms: int; steps: int} + | Safe of {bound: 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 - | Unsafe {alarms; steps} -> pf "Unsafe: %i (%i)" alarms steps + | Safe {bound= -1} -> pf "Safe" + | 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} - else Unsafe {alarms= !invalid_access_count; steps= !steps} + if !invalid_access_count = 0 then Safe {bound= !bound} + 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) diff --git a/sledge/src/report.mli b/sledge/src/report.mli index 06af41c1f..984618ecd 100644 --- a/sledge/src/report.mli +++ b/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} - | Unsafe of {alarms: int; steps: int} + | Safe of {bound: 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]