Add coverage tracking tool

See sailcov/README.md for a short description

Fix many location info bugs discovered by eyeballing output

4 files changed, 197 insertions, 0 deletions

diff --git a/sailcov/Makefile b/sailcov/Makefile
new file mode 100644
index 00000000..bc9e39d8
--- /dev/null
+++ b/sailcov/Makefile
@@ -0,0 +1,4 @@
+
+sailcov: *.ml dune
+	dune build main.exe
+	cp -f _build/default/main.exe sailcov
diff --git a/sailcov/dune b/sailcov/dune
new file mode 100644
index 00000000..c69fec07
--- /dev/null
+++ b/sailcov/dune
@@ -0,0 +1,2 @@
+(executable
+  (name main))
diff --git a/sailcov/dune-project b/sailcov/dune-project
new file mode 100644
index 00000000..4c6dd5ae
--- /dev/null
+++ b/sailcov/dune-project
@@ -0,0 +1 @@
+(lang dune 2.4)
diff --git a/sailcov/main.ml b/sailcov/main.ml
new file mode 100644
index 00000000..84fbd595
--- /dev/null
+++ b/sailcov/main.ml
@@ -0,0 +1,190 @@
+
+let opt_files = ref ([] : string list)
+
+let opt_taken = ref "sail_coverage"
+
+let opt_all = ref "all_branches"
+              
+let options =
+  Arg.align [
+      ( "-t",
+        Arg.String (fun str -> opt_taken := str),
+        "<file> coverage information for branches taken while executing the model (default: sail_coverage)");
+      ( "-a",
+        Arg.String (fun str -> opt_all := str),
+        "<file> information about all possible branches (default: all_branches)")
+    ]
+
+type span = {
+    file : string;
+    l1 : int;
+    c1 : int;
+    l2 : int;
+    c2 : int;
+  }
+
+module Span = struct
+  type t = span
+  let compare s1 s2 = compare s1 s2
+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
+  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;
+      loop ()
+    in
+    loop ()
+  with End_of_file ->
+    close_in chan;
+    !spans
+
+(** 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
+   increasingly good. *) 
+type source_char = {
+    mutable badness : int;
+    mutable goodness : int;
+    char : char;
+  }
+
+let mark_bad_region source span =
+  source.(span.l1 - 1).(span.c1).badness <- source.(span.l1 - 1).(span.c1).badness + 1;
+  source.(span.l2 - 1).(span.c2 - 1).badness <- source.(span.l2 - 1).(span.c2 - 1).badness - 1
+
+let mark_good_region source span =
+  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
+  
+let process_line l = Array.init (String.length l) (fun n -> { badness = 0; goodness = 0; char = l.[n] })
+
+let read_source filename =
+  let lines = ref [] in
+  let chan = open_in filename in
+  try
+    let rec loop () =
+      lines := process_line (input_line chan) :: !lines;
+      loop ()
+    in
+    loop ()
+  with End_of_file ->
+    close_in chan;
+    Array.of_list (List.rev !lines)
+
+let output_html_char chan c =
+  if c == ' ' then
+    output_string chan "&nbsp;"
+  else if c == '<' then
+    output_string chan "&lt;"
+  else if c == '>' then
+    output_string chan "&gt;"
+  else if c == '"' then
+    output_string chan "&quot;"
+  else
+    output_char chan c
+    
+let main () =
+  let all = read_coverage !opt_all in
+  let taken = read_coverage !opt_taken in
+  List.iter (fun file ->
+      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 source = read_source file in
+      SpanSet.iter (mark_good_region source) taken;
+      SpanSet.iter (mark_bad_region source) not_taken;
+
+      let output_file = Filename.remove_extension (Filename.basename file) ^ ".html" in
+      let chan = open_out output_file in
+
+      let current_goodness = ref 0 in
+      let current_badness = ref 0 in
+
+      let good_color () =
+        let darken = 0xE0 - (!current_goodness * 0x20) in
+        Printf.sprintf "#%xFF%x" darken darken
+      in
+      let bad_color () =
+        let darken = 0xE0 - (!current_badness * 0x20) in
+        Printf.sprintf "#FF%x%x" darken darken
+      in
+      output_string chan "<!DOCTYPE html>\n";
+      output_string chan "<html lang=\"en\">\n<head>\n<meta charset=\"utf-8\">\n";
+      output_string chan (Printf.sprintf "<title>%s</title>" (Filename.remove_extension (Filename.basename file)));
+      output_string chan "</head>\n";
+      output_string chan "<body>\n";
+      output_string chan "<code style=\"display: block\">\n";
+
+      Array.iter (fun line ->
+          Array.iter (fun loc ->
+              if loc.goodness < 0 && loc.badness < 0 then (
+                output_html_char chan loc.char;
+                current_goodness := !current_goodness + loc.goodness;
+                current_badness := !current_badness + loc.badness;
+                for _ = 1 to abs loc.goodness + abs loc.badness do
+                  output_string chan (Printf.sprintf "</span>")
+                done
+              ) else if loc.goodness < 0 then (
+                assert (loc.badness >= 0);
+                output_html_char chan loc.char;
+                current_goodness := !current_goodness + loc.goodness;
+                for _ = 1 to abs loc.goodness do
+                  output_string chan (Printf.sprintf "</span>")
+                done
+              ) else if loc.badness < 0 then (
+                assert (loc.goodness >= 0);
+                output_html_char chan loc.char;
+                current_badness := !current_badness + loc.badness;
+                for _ = 1 to abs loc.badness do
+                  output_string chan (Printf.sprintf "</span>")
+                done
+              ) else if loc.badness > 0 then (
+                assert (loc.goodness <= 0);
+                current_badness := !current_badness + loc.badness;
+                for _ = 1 to loc.badness do
+                  output_string chan (Printf.sprintf "<span style=\"background-color: %s\">" (bad_color ()));
+                done;
+                output_html_char chan loc.char
+              ) else if loc.goodness > 0 then (
+                assert (!current_badness == 0);
+                current_goodness := !current_goodness + loc.goodness;
+                for _ = 1 to loc.goodness do
+                  output_string chan (Printf.sprintf "<span style=\"background-color: %s\">" (good_color ()));
+                done;
+                output_html_char chan loc.char
+              ) else (
+                output_html_char chan loc.char
+              );
+              assert (!current_goodness >= 0);
+              assert (!current_badness >= 0)
+                      
+            ) line;
+          output_string chan "<br>\n"
+        ) source;
+
+      output_string chan "</code>\n";
+      output_string chan "</body>\n";
+      output_string chan "</html>";
+      
+      close_out chan;
+      Printf.printf "%s (%d/%d)\n" file (SpanSet.cardinal taken) (SpanSet.cardinal all)
+    ) !opt_files
+
+let usage_msg = "usage: sail-coverage-viz -c <file> -a <file> <.sail files>\n"
+
+let _ =
+  Arg.parse options
+    (fun s -> opt_files := !opt_files @ [s])
+    usage_msg;
+  try main () with
+  | Sys_error msg -> prerr_endline msg; exit 1