diff options
| -rw-r--r-- | lib/rts.c | 3 | ||||
| -rw-r--r-- | sailcov/README.md | 9 | ||||
| -rw-r--r-- | sailcov/main.ml | 231 | ||||
| -rw-r--r-- | src/jib/c_backend.ml | 32 |
4 files changed, 238 insertions, 37 deletions
@@ -10,9 +10,12 @@ static uint64_t g_elf_entry; uint64_t g_cycle_count = 0; static uint64_t g_cycle_limit; +extern void model_pre_exit(); + unit sail_exit(unit u) { fprintf(stderr, "[Sail] Exiting after %" PRIu64 " cycles\n", g_cycle_count); + model_pre_exit(); exit(EXIT_SUCCESS); return UNIT; } diff --git a/sailcov/README.md b/sailcov/README.md index 31c775c1..0a49f51c 100644 --- a/sailcov/README.md +++ b/sailcov/README.md @@ -55,3 +55,12 @@ yellow/blue theme using `--alt-colors` or `--alt-colours`. See the alternate [riscv_vmem_sv39.html](https://alasdair.github.io/alt_riscv_vmem_sv39.html) for an example. + +### Combining multiple coverage files + +The `-t` option can be given multiple times to merge the coverage from +multiple executions. The `--taken-list` option acts as if each line +of the given file is a `-t` argument, allowing the coverage of large +number of tests to be assessed. Adding the `--cumulative-table` +option will output an additional file in CSV format showing how the +coverage increases across all the files. diff --git a/sailcov/main.ml b/sailcov/main.ml index 4f1e054c..35d6e7c8 100644 --- a/sailcov/main.ml +++ b/sailcov/main.ml @@ -1,7 +1,8 @@ let opt_files = ref ([] : string list) -let opt_taken = ref "sail_coverage" +let opt_taken = ref ([] : string list) +let opt_taken_list = ref ([] : string list) let opt_all = ref "all_branches" let opt_tab_width = ref 4 @@ -10,6 +11,10 @@ let opt_index = ref None let opt_index_default = ref None let opt_prefix = ref "" +let opt_cumulative_table = ref None +let opt_histogram = ref false +let opt_colour_count = ref false + type color = { hue: int; saturation: int; @@ -29,11 +34,14 @@ let use_alt_colors () = let options = Arg.align [ ( "-t", - Arg.String (fun str -> opt_taken := str), + Arg.String (fun str -> opt_taken := str::!opt_taken), "<file> coverage information for branches taken while executing the model (default: sail_coverage)"); ( "--taken", - Arg.String (fun str -> opt_taken := str), + Arg.String (fun str -> opt_taken := str::!opt_taken), " long form of -t"); + ( "--taken-list", + Arg.String (fun str -> opt_taken_list := str::!opt_taken_list), + "<file> file containing a list of filenames of branches taken"); ( "-a", Arg.String (fun str -> opt_all := str), "<file> information about all possible branches (default: all_branches)"); @@ -72,37 +80,62 @@ let options = " swap default colors from red/green into alternate yellow/blue theme"); ( "--alt-colours", Arg.Unit use_alt_colors, - "") + ""); + ( "--cumulative-table", + Arg.String (fun str -> opt_cumulative_table := Some str), + "<file> write a table of cumulative coverage to file"); + ( "--histogram", + Arg.Set opt_histogram, + "display a histogram of the coverage level"); + ( "--color-by-count", + Arg.Set opt_colour_count, + "color by number of files a span appears in (instead of nesting depth)"); + ( "--colour-by-count", + Arg.Set opt_colour_count, + "colour by number of files a span appears in (instead of nesting depth)"); ] type span = { - file : string; l1 : int; c1 : int; l2 : int; c2 : int; } -let string_of_span span = - Printf.sprintf "\"%s\" %d:%d - %d:%d" span.file span.l1 span.c1 span.l2 span.c2 +let string_of_span file span = + Printf.sprintf "\"%s\" %d:%d - %d:%d" file span.l1 span.c1 span.l2 span.c2 module Span = struct type t = span - let compare s1 s2 = compare s1 s2 + let compare s1 s2 = + if s1.l1 < s2.l1 then -1 else if s1.l1 > s2.l1 then 1 + else if s1.c1 < s2.c1 then -1 else if s1.c1 > s2.c1 then 1 + else if s1.l2 < s2.l2 then -1 else if s1.l2 > s2.l2 then 1 + else if s1.c2 < s2.c2 then -1 else if s1.c2 > s2.c2 then 1 + else 0 end module SpanSet = Set.Make(Span) module SpanMap = Map.Make(Span) -let mk_span _ file l1 c1 l2 c2 = { file = Filename.basename file; l1 = l1; c1 = c1; l2 = l2; c2 = c2 } - -let read_coverage filename = - let spans = ref SpanSet.empty in +module StringMap = Map.Make(String) +module IntMap = Map.Make(Int) + +let add_span spans _ file l1 c1 l2 c2 = + StringMap.update (Filename.basename file) + (fun x -> + let file_spans = Option.value x ~default:SpanMap.empty in + Some (SpanMap.update { l1 = l1; c1 = c1; l2 = l2; c2 = c2 } + (function None -> Some 1 | Some i -> Some (i+1)) file_spans)) + spans + +let read_more_coverage filename spans = + let spans = ref spans in let chan = open_in filename in try let rec loop () = let line = input_line chan in - spans := SpanSet.add (Scanf.sscanf line "%c %S, %d, %d, %d, %d" mk_span) !spans; + spans := Scanf.sscanf line "%c %S, %d, %d, %d, %d" (add_span !spans); loop () in loop () @@ -110,6 +143,8 @@ let read_coverage filename = close_in chan; !spans +let read_coverage filename = read_more_coverage filename StringMap.empty + (** We color the source either red (bad) or green (good) if it's covered vs uncovered. If we have nested uncovered branches, they will be increasingly bad, whereas nested covered branches will be @@ -123,7 +158,7 @@ type source_char = { let zero_width span = span.l1 = span.l2 && span.c1 = span.c2 -let mark_bad_region source span = +let mark_bad_region source span _ = if zero_width span then ( source.(span.l2 - 1).(span.c2 - 1).bad_zero_width <- true ) else ( @@ -131,7 +166,7 @@ let mark_bad_region source span = source.(span.l2 - 1).(span.c2 - 1).badness <- source.(span.l2 - 1).(span.c2 - 1).badness - 1 ) -let mark_good_region source span = +let mark_good_region source span _ = if not (zero_width span) then ( source.(span.l1 - 1).(span.c1).goodness <- source.(span.l1 - 1).(span.c1).goodness + 1; source.(span.l2 - 1).(span.c2 - 1).goodness <- source.(span.l2 - 1).(span.c2 - 1).goodness - 1 @@ -167,13 +202,21 @@ let output_html_char chan c = output_char chan c let file_info file all taken = - let all = SpanSet.filter (fun s -> s.file = Filename.basename file) all in - let taken = SpanSet.filter (fun s -> s.file = Filename.basename file) taken in - let not_taken = SpanSet.diff all taken in + let diff span all_count taken_count = + match all_count, taken_count with + | Some _, Some _ -> None + | Some n, None -> Some n + | None, Some _ -> begin + Printf.eprintf "Warning: span not in all branches file: %s\n" (string_of_span file span); + None + end + | None, None -> None + in + let not_taken = SpanMap.merge diff all taken in let percent = - if SpanSet.cardinal all != 0 then - let p = 100. *. (Float.of_int (SpanSet.cardinal taken) /. Float.of_int (SpanSet.cardinal all)) in + if SpanMap.cardinal all != 0 then + let p = 100. *. (Float.of_int (SpanMap.cardinal taken) /. Float.of_int (SpanMap.cardinal all)) in Printf.sprintf "%.0f%%" p else "-" @@ -181,7 +224,7 @@ let file_info file all taken = taken, not_taken, - Printf.sprintf "%s (%d/%d) %s" (Filename.basename file) (SpanSet.cardinal taken) (SpanSet.cardinal all) percent + Printf.sprintf "%s (%d/%d) %s" (Filename.basename file) (SpanMap.cardinal taken) (SpanMap.cardinal all) percent let index_css = " body, html { @@ -239,16 +282,57 @@ iframe { let html_file_for file = !opt_prefix ^ Filename.remove_extension (Filename.basename file) ^ ".html" +let read_taken_files () = + match !opt_cumulative_table with + | Some table_name -> + let table_chan = open_out table_name in + List.iter (fun src_file -> Printf.fprintf table_chan "%s, " (Filename.basename src_file)) !opt_files; + Printf.fprintf table_chan ",, Total\n"; + let read_more filename spans = + let new_spans = read_more_coverage filename spans in + let counts = List.map (fun src_name -> + let taken = Option.value ~default:SpanMap.empty (StringMap.find_opt (Filename.basename src_name) new_spans) in + SpanMap.cardinal taken + ) !opt_files + in + List.iter (fun i -> Printf.fprintf table_chan "%d, " i) counts; + Printf.fprintf table_chan ",, %d\n" (List.fold_left (+) 0 counts); + new_spans + in + let spans = List.fold_right read_more !opt_taken StringMap.empty in + close_out table_chan; + spans + | None -> + List.fold_right read_more_coverage !opt_taken StringMap.empty + +let get_file_spans filename all taken = + let file = Filename.basename filename in + let all = match StringMap.find_opt file all with + | None -> Printf.eprintf "Warning: %s not found in coverage files\n" file; SpanMap.empty + | Some s -> s + in + let taken = Option.value ~default:SpanMap.empty (StringMap.find_opt file taken) in + all, taken + let main () = let all = read_coverage !opt_all in - let taken = read_coverage !opt_taken in + let taken = read_taken_files () in List.iter (fun file -> + let all, taken = get_file_spans file all taken in let taken, not_taken, desc = file_info file all taken in print_endline desc; + + if !opt_histogram && not (SpanMap.is_empty taken) then begin + let histogram = SpanMap.fold (fun _ count m -> IntMap.update count (function None -> Some 1 | Some i -> Some (i+1)) m) taken IntMap.empty in + Printf.printf "Files | Number of spans\n"; + IntMap.iter (fun count spans -> + Printf.printf "%5d | %7d\n" count spans + ) histogram + end; let source = read_source file in - SpanSet.iter (mark_good_region source) taken; - SpanSet.iter (mark_bad_region source) not_taken; + SpanMap.iter (mark_good_region source) taken; + SpanMap.iter (mark_bad_region source) not_taken; let output_file = html_file_for file in let chan = open_out output_file in @@ -273,6 +357,84 @@ let main () = output_string chan (Printf.sprintf "<h1>%s</h1>\n" desc); output_string chan "<code style=\"display: block\">\n"; + if !opt_colour_count then + let combined = SpanMap.merge (fun span present count -> + match present, count with + | None, _ -> Printf.eprintf "Span %s missing in all branches file %s" (string_of_span file span) !opt_all; None + | Some _, None -> Some 0 + | Some _, Some n -> Some n) all taken + in + (* The spans are ordered, so print forwards until we find the next span start or end (the + ends of spans are held in the stack). TODO: check for lingering off-by-one errors. *) + let rec process span count (stack, line, char) = + (*Printf.eprintf "span %s line %d char %d\n" (string_of_span file span) line char;*) + if span.l1 > line then + match stack with + | h::t when h.l2 = line -> + for i = char to h.c2 - 1 do + output_html_char chan source.(line - 1).(i).char + done; + output_string chan (Printf.sprintf "</span>"); + process span count (t, line, h.c2) + | _ -> + for i = char to Array.length (source.(line - 1)) - 1 do + output_html_char chan source.(line - 1).(i).char + done; + output_string chan "<br>\n"; + process span count (stack, line + 1, 0) + else if span.l1 = line && span.c1 > char then + match stack with + | h::t when h.l2 = line && h.c2 < span.c1 -> + for i = char to h.c2 - 1 do + output_html_char chan source.(line - 1).(i).char + done; + output_string chan (Printf.sprintf "</span>"); + process span count (t, line, h.c2) + | _ -> + for i = char to span.c1 - 1 do + output_html_char chan source.(line - 1).(i).char + done; + if span.c1 - 1 = Array.length source.(line - 1) + then process span count (stack, line + 1, 0) + else process span count (stack, line, span.c1) + else + let () = assert (span.l1 = line && span.c1 = char) in + if zero_width span then begin + output_string chan (Printf.sprintf "<span style=\"background-color: %s\">" (bad_color ())); + output_string chan "«Invisible branch not taken here»"; + output_string chan "</span>"; + (stack, line, char) + end else begin + let colour = + if count = 0 then html_color !opt_bad_color 0 else + html_color !opt_good_color count + in + output_string chan (Printf.sprintf "<span title=\"%d\" style=\"background-color: %s\">" count colour); + (span::stack, line, char) + end + in + let rec finish (stack, line, char) = + (*Printf.eprintf "line %d char %d\n" line char;*) + match stack with + | h::t when h.l2 = line -> + for i = char to h.c2 - 1 do + output_html_char chan source.(line - 1).(i).char + done; + output_string chan (Printf.sprintf "</span>"); + finish (t, line, h.c2) + | _ -> + if line >= Array.length source then () else + for i = char to Array.length (source.(line - 1)) - 1 do + output_html_char chan source.(line - 1).(i).char + done; + output_string chan "<br>\n"; + if line + 1 < Array.length source + then finish (stack, line + 1, 0) + else () + in + let (stack, line, char) = SpanMap.fold process combined ([], 1, 0) in + finish (stack, line, char) + else Array.iter (fun line -> Array.iter (fun loc -> if loc.goodness < 0 && loc.badness < 0 then ( @@ -322,7 +484,7 @@ let main () = assert (!current_goodness >= 0); assert (!current_badness >= 0) - + ) line; output_string chan "<br>\n" ) source; @@ -337,7 +499,7 @@ let main () = begin match !opt_index with | Some name -> let chan = open_out (name ^ ".html") in - + output_string chan "<!DOCTYPE html>\n"; output_string chan "<html lang=\"en\">\n"; Printf.ksprintf (output_string chan) @@ -347,6 +509,7 @@ let main () = output_string chan "<table><tr><td class=\"left\"><div class=\"scroll\">"; List.iter (fun file -> + let all, taken = get_file_spans file all taken in let _, _, desc = file_info file all taken in Printf.ksprintf (output_string chan) "<a href=\"%s\" target=\"source\">%s</a><br>\n" (html_file_for file) desc @@ -370,9 +533,25 @@ let main () = let usage_msg = "usage: sailcov -t <file> -a <file> <.sail files>\n" +let read_taken_lists () = + List.iter (fun filename -> + let chan = open_in filename in + try + let rec loop () = + opt_taken := (input_line chan)::!opt_taken; + loop () + in loop () + with End_of_file -> + ()) !opt_taken_list + let _ = Arg.parse options (fun s -> opt_files := !opt_files @ [s]) usage_msg; + read_taken_lists (); + begin opt_taken := match !opt_taken with + | [] -> ["sail_coverage"] + | l -> List.rev l + end; try main () with | Sys_error msg -> prerr_endline msg; exit 1 diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml index 2fe21d93..88b01d87 100644 --- a/src/jib/c_backend.ml +++ b/src/jib/c_backend.ml @@ -2310,23 +2310,32 @@ let compile_ast env output_chan c_includes ast = @ [ "}" ] )) in + let model_pre_exit = + [ "void model_pre_exit()"; + "{" ] + @ (if Util.is_some !opt_branch_coverage then + [ " if (sail_coverage_exit() != 0) {"; + " fprintf(stderr, \"Could not write coverage information\\n\");"; + " exit(EXIT_FAILURE);"; + " }"; + "}" ] + else + ["}"] + ) + |> List.map string + |> separate hardline + in + let model_default_main = ([ Printf.sprintf "%sint model_main(int argc, char *argv[])" (static ()); "{"; " model_init();"; " if (process_arguments(argc, argv)) exit(EXIT_FAILURE);"; Printf.sprintf " %s(UNIT);" (sgen_function_id (mk_id "main")); - " model_fini();" ] - @ (if Util.is_some !opt_branch_coverage then - [ " if (sail_coverage_exit() != 0) {"; - " fprintf(stderr, \"Could not write coverage information\\n\");"; - " exit(EXIT_FAILURE);"; - " }" ] - else - [] - ) - @ [ " return EXIT_SUCCESS;"; - "}" ]) + " model_fini();"; + " model_pre_exit();"; + " return EXIT_SUCCESS;"; + "}" ]) |> List.map string |> separate hardline in @@ -2344,6 +2353,7 @@ let compile_ast env output_chan c_includes ast = ^^ (if not !opt_no_rts then model_init ^^ hlhl ^^ model_fini ^^ hlhl + ^^ model_pre_exit ^^ hlhl ^^ model_default_main ^^ hlhl else empty) |