Fix coverage for matches containing a single case.

The C backend tries not to emit branch coverage points for matches containing a single case but was still emitting a line in all_branches. This confused sailcov and resulting in warnings and weird output. Hopefully fixes #502. Also adds a test case containing a tuple deconstruction (which apparently gets compiled to a single case match).
rems-project · Jul 8, 2024 · 90e6358 · 90e6358
1 parent 155d567
commit 90e6358
Show file tree

Hide file tree

Showing 3 changed files with 40 additions and 1 deletion.
diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml
@@ -767,7 +767,7 @@ module Make (C : CONFIG) = struct
         (* Get the number of cases, because we don't want to check branch
            coverage for matches with only a single case. *)
         let num_cases = List.length cases in
-        let branch_id, on_reached = coverage_branch_reached ctx l in
+        let branch_id, on_reached = if num_cases > 1 then coverage_branch_reached ctx l else (0, []) in
         let case_return_id = ngensym () in
         let finish_match_label = label "finish_match_" in
         let compile_case (apat, guard, body) =

diff --git a/test/sailcov/let.expect b/test/sailcov/let.expect
@@ -0,0 +1,25 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+<meta charset="utf-8">
+<title>let</title></head>
+<body>
+<h1>let.sail (3/4) 75%</h1>
+<code style="display: block">
+default&nbsp;Order&nbsp;dec<br>
+$include&nbsp;&lt;prelude.sail&gt;<br>
+<br>
+register&nbsp;R&nbsp;:&nbsp;bool&nbsp;=&nbsp;true<br>
+val&nbsp;main&nbsp;:&nbsp;unit&nbsp;-&gt;&nbsp;unit<br>
+<br>
+function&nbsp;main()&nbsp;=&nbsp;<span style="background-color: hsl(120, 85%, 80%)">{<br>
+&nbsp;&nbsp;&nbsp;&nbsp;let&nbsp;(x,&nbsp;y)&nbsp;=&nbsp;(R,&nbsp;R);<br>
+&nbsp;&nbsp;&nbsp;&nbsp;<span style="background-color: hsl(120, 85%, 75%)">if&nbsp;x&nbsp;then&nbsp;<span style="background-color: hsl(120, 85%, 70%)">{<br>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;print_endline(&quot;A&quot;)<br>
+&nbsp;&nbsp;&nbsp;&nbsp;}</span>&nbsp;else&nbsp;<span style="background-color: hsl(0, 85%, 80%)">{<br>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;print_endline(&quot;B&quot;)<br>
+&nbsp;&nbsp;&nbsp;&nbsp;}</span></span><br>
+}</span><br>
+</code>
+</body>
+</html>
diff --git a/test/sailcov/let.sail b/test/sailcov/let.sail
@@ -0,0 +1,14 @@
+default Order dec
+$include <prelude.sail>
+
+register R : bool = true
+val main : unit -> unit
+
+function main() = {
+    let (x, y) = (R, R);
+    if x then {
+        print_endline("A")
+    } else {
+        print_endline("B")
+    }
+}