Fix an issue with sailcov on 1-case matches

A match with a single case (or a let statement) would generate a coverage point that would never be reached.
rems-project · Jul 8, 2024 · 09ac4b2 · 09ac4b2
1 parent 155d567
commit 09ac4b2
Show file tree

Hide file tree

Showing 3 changed files with 41 additions and 2 deletions.
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) =
@@ -807,7 +807,7 @@ module Make (C : CONFIG) = struct
         in
         ( aval_setup
           @ [icomment ("Case with num_cases: " ^ string_of_int num_cases)]
-          @ (if num_cases > 1 then on_reached else [])
+          @ on_reached
           @ [idecl l ctyp case_return_id]
           @ List.concat (List.map compile_case cases)
           @ [imatch_failure l]

diff --git a/test/sailcov/let_single_branch.expect b/test/sailcov/let_single_branch.expect
@@ -0,0 +1,25 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+<meta charset="utf-8">
+<title>let_single_branch</title></head>
+<body>
+<h1>let_single_branch.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_single_branch.sail b/test/sailcov/let_single_branch.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")
+    }
+}