sailcov fails upon goodness within badness

[elliotb-lowrisc]

It appears that sailcov fatally crashes when it encounters a region of "goodness" within a region of "badness" when writing out HTML files.

Here is a minimal test case I have put together.

all_branches_edit:

B 1121, "cheri_insts.sail", 295, 32, 295, 80
T 1016, 2616, "cheri_insts.sail", 292, 45, 297, 1

sail_coverage_edit:

B "cheri_insts.sail", 295, 32, 295, 80

cheri_insts.sail (relevant section lines 292-297):
https://github.com/microsoft/cheriot-sail/blob/d641fb1e65378596b79306938ad70a2b58b91cb7/src/cheri_insts.sail#L292-L297

Command:

$SAILCOV -a all_branches_edit -t sail_coverage_edit cheri_insts.sail

...where $SAILCOV is a path to a sailcov binary.

Terminal output:

cheri_insts.sail (1/2) 50%
Fatal error: exception Assert_failure("sailcov/main.ml", 541, 18)

Tail of the output "cheri_insts.html" file:

...
function&nbsp;clause&nbsp;execute&nbsp;(CGetLen(rd,&nbsp;cs1))&nbsp;=&nbsp;<span style="background-color: hsl(0, 85%, 80%)">{<br>
&nbsp;&nbsp;let&nbsp;capVal&nbsp;=&nbsp;C(cs1);<br>
&nbsp;&nbsp;let&nbsp;len&nbsp;=&nbsp;getCapLength(capVal);<br>
&nbsp;&nbsp;X(rd)&nbsp;=&nbsp;to_bits(sizeof(xlen),&nbsp;

---

I have an idea for a fix, but am uncertain whether it would be correct or not due to my limited understanding of sailcov.

Here is the assert that is triggered:

sail/sailcov/main.ml

Lines 540 to 542 in a3f4047

	else if loc.goodness > 0 then (
	assert (!current_badness == 0);
	current_goodness := !current_goodness + loc.goodness;

Purely going on the pattern of the surrounding code, it looks like it should instead be:

assert (loc.badness <= 0);

If written this way, it would match the pattern set by the if-else case above it:

sail/sailcov/main.ml

Lines 532 to 534 in a3f4047

	else if loc.badness > 0 then (
	assert (loc.goodness <= 0);
	current_badness := !current_badness + loc.badness;

I'm happy to create a PR for this fix if requested.

[Alasdair]

Do you have this commit: 28ef9e9?

[elliotb-lowrisc]

Yes, I tested this with a sailcov binary I built from source as of cb0a396

[Alasdair]

And the sail binary used was also from that commit? Just making sure I have the same environment before I try to reproduce it myself.

I think the asserts may be trying to check slightly different invariants, so even if changing the asserts produces outputs it might be worth thinking a bit harder about the invariants to ensure there isn't a deeper underlying problem.

[elliotb-lowrisc]

I have just now been able to reproduce this issue with both sail and sailcov binaries generated from cb0a396. I had to do some hackery to work around the coverage filename override issue, but I managed to do it outside of the sail repository this time.

For the avoidance of doubt, here are the commands I used to generate the binaries:

git checkout cb0a396
make clean
make install
rm -f sailcov/sailcov
make -C sailcov

[Alasdair]

I had a look at the output after just commenting out the assert, and it looks like it is hitting the case the assert is trying to guard against where we have covered code within uncovered code. Obviously we can't execute the if without calling the function, so there must be some underlying issue.

[Alasdair]

Ok, after looking at the generated C from the CHERIoT model, I think the problem is how the separate function clauses interact with the coverage points.

[Alasdair]

With some more investigation, that is not the case...

Could you send me the complete set of coverage points and all the complete output from running the test?

The generated code looks like:

    sail_branch_target_taken(1017, 2612, "src/cheri_insts.sail", 292, 45, 297, 1);
    struct zCapability zuz3691;
    {
      zuz3691 = zrC_bits(zuz3690);
      if (have_exception) {
        goto end_block_exception_3672;
      }
    }
    int64_t zlen;
    zlen = zgetCapLength(zuz3691);
    {
      uint64_t zgaz33584;
      {
        int64_t zgaz33583;
        {
          bool zgaz33582;
          zgaz33582 = (zlen > zcap_max_addr);
          {
            sail_branch_reached(1122, "src/cheri_insts.sail", 295, 32, 295, 80);
            if (zgaz33582) {
              sail_branch_target_taken(1122, 2611, "src/cheri_insts.sail", 295, 59, 295, 71);
              zgaz33583 = zcap_max_addr;
            } else {
              sail_branch_target_taken(1122, 2610, "src/cheri_insts.sail", 295, 77, 295, 80);
              zgaz33583 = zlen;
            }
          }

the first call to sail_branch_target_taken should prevent the error, but somehow we only see the sail_branch_reached output in your generated coverage file. Neither of the inner sail_branch_target_taken outputs are there either which is strange.

Maybe I should change these asserts to warnings though, as they are reliant on location information for the coverage points being fully accurate.

[elliotb-lowrisc]

2024_04_26-cheriot-sailcov.zip

Are these the files you're after?

[elliotb-lowrisc]

I found today that I'd forgotten to rebuild libsail_coverage.a as part of my cb0a396 rebuild. Here are similar files again after another go with the rebuilt lib, just in case it matters for you. I've also tried adding a .txt suffix this time so I could upload them without zipping.

sail_coverage_40261.txt
all_branches.txt

[rmn30]

Hmmm. I notice there are odd lines in the sail_coverage file like:

B "", 0, 0, 0, 0
...
F "", 1, 70, 4, 1
...
F "", 1, 54, 1, 73

[marnovandermaas]

What do you think we should do next on this @Alasdair?

[Alasdair]

I haven't been able to reproduce the issue, so I'm still not sure what exactly is going wrong.

[rmn30]

I followed these instructions: https://github.com/lowRISC/TestRIG/tree/cheriot?tab=readme-ov-file#getting-started

When I ran sailcov from HEAD I got a lot of assertions like:

Warning: assertion failed at File "sailcov/main.ml", line 576, characters 28-35
Warning: assertion failed at File "sailcov/main.ml", line 577, characters 28-35

Tip: I limited the run to just the arithmetic tests using the suggested arguments so that it would finish quickly.

[elliotb-lowrisc]

When I ran sailcov from HEAD I got a lot of assertions like:

Warning: assertion failed at File "sailcov/main.ml", line 576, characters 28-35
Warning: assertion failed at File "sailcov/main.ml", line 577, characters 28-35

I've rebuilt with 1edb36b and am also now getting these warnings instead of a crash when I run sailcov. HTML generation now seems to work for all files, except for the warnings.

[marnovandermaas]

Please feel free to close this issue since it the warning now no longer causes a failure.

[rmn30]

I have reproduced the "goodness within badness" in a small example:

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") 
    }
}

The problem is an apparently spurious entry in the all_branches file for the let with tuple deconstruction. sailcov gives a warning and produces the following output:

.

[Alasdair]

Should be fixed by #625

[rmn30]

This is a big improvement but we still get some warnings from sailcov that appear to be caused by this line in the sail-riscv model.

The assertion at sailcov/main.ml:561 is triggered once followed by many of the assertion at sailcov/main.ml:584.

Here are the relevant lines from all_branches:

B 807, "", 0, 0, 0, 0
B 808, "sail-riscv/model/riscv_insts_mext.sail", 146, 6, 146, 70
B 809, "sail-riscv/model/riscv_insts_mext.sail", 146, 6, 146, 70
T 809, 2050, "sail-riscv/model/riscv_insts_mext.sail", 146, 6, 146, 70
T 808, 2051, "sail-riscv/model/riscv_insts_mext.sail", 146, 6, 146, 70
T 807, 2052, "sail-riscv/model/riscv_insts_mext.sail", 146, 6, 146, 70
B 810, "sail-riscv/model/riscv_insts_mext.sail", 146, 6, 147, 27
T 806, 2054, "sail-riscv/model/riscv_insts_mext.sail", 146, 6, 147, 27

and sail_coverage:

B "sail-riscv/model/riscv_insts_mext.sail", 146, 6, 146, 70
T "sail-riscv/model/riscv_insts_mext.sail", 146, 6, 146, 70

Looks like multiple branches are emitted for the same span in all_branches.

[rmn30]

Here is a reduced example:

default Order dec

$include <prelude.sail>

type xlen : Int = 32
type regidx = bits(5)
scattered union ast
val encdec : ast <-> bits(32)
scattered mapping encdec

mapping bool_not_bits : bool <-> bits(1) = {
  true   <-> 0b0,
  false  <-> 0b1
}

union clause ast = DIVW : (regidx, regidx, regidx, bool)

mapping clause encdec = DIVW(rs2, rs1, rd, s)
      if sizeof(xlen) == 64
  <-> 0b0000001 @ rs2 @ rs1 @ 0b10 @ bool_not_bits(s) @ rd @ 0b0111011
      if sizeof(xlen) == 64

union clause ast = Z : unit
mapping clause encdec = Z() <-> 0x00000000

val main : unit -> unit
function main() = {
    let _ = encdec(0x00000000)
}