sailcov warnings with mapping

[rmn30]

I added this as a comment on #502 but think it might have gone unnoticed. Here is another example from the RISC-V spec. where sailcov gives warnings and produces confusing output:

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

It looks like sail is producing a coverage point that covers the entire (backwards) pattern for DIVW including the condition but it doesn't get hit in the c. It also produces coverage points for the pattern without the condition which do get hit so sailcov sees a covered region within an (apparently) uncovered region.

[Alasdair]

I think the issue is with tracking locations for scattered definitions more generally, but I haven't had the time to look in detail yet.

[rmn30]

Fair enough. It is not too critical but I wanted to make a note of it. For the benefit of search engines the error reported is :

Warning: assertion failed at File "sailcov/main.ml", line 561, characters 30-37
Warning: assertion failed at File "sailcov/main.ml", line 584, characters 28-35
<second line above repeated many times>

[trdthg]

I forgot to mention that I modified the test case a bit. It's in the last picture.

After two days of searching, it seems that I have found the reason.

I added lots of print statements for each match, pat, body for rewriter, ANF and jib_compile. And after reviewing thousands of lines of logs, I've identified some anomalies

the logs are quite messy, I highlight a few lines of logs with markdown diff:

##### E_match exp=match head_exp# { b__0 if eq_bits(b__0, [bitzero, bitzero]) => Some(Z()), b__1 if eq_bits(b__1, [bitzero, bitone]) => Some(Z()), mapping0# : bitvector(2) if bool_not_bits2_backwards_matches(mapping0#) => match bool_not_bits2_backwards(mapping0#) { s => Some(B(s)), _ => None() }, _ => None() } loc=Generated(Unknown)
anf::E_match::and exp=match head_exp# { b__0 if eq_bits(b__0, [bitzero, bitzero]) => Some(Z()), b__1 if eq_bits(b__1, [bitzero, bitone]) => Some(Z()), mapping0# : bitvector(2) if bool_not_bits2_backwards_matches(mapping0#) => match bool_not_bits2_backwards(mapping0#) { s => Some(B(s)), _ => None() }, _ => None() } loc=Unknown

##### E_match exp=head_exp# loc=Unknown
anf::E_match::and exp=head_exp# loc=Unknown
#### anf::E_match::anf_pexp::Pat_when pat=b__0 loc=Range(nested_mapping.sail,14,209,211->nested_mapping.sail,14,209,215) guard_exp=eq_bits(b__0, [bitzero, bitzero])
### pat 
anf::E_match::anf_pexp->anf_pat pat=b__0 loc=Range(nested_mapping.sail,14,209,211->nested_mapping.sail,14,209,215)
P_id id
### body 

+anf::E_match::and exp=Some(Z()) loc=Generated(Unknown)
anf::E_match::and exp=Z() loc=Range(nested_mapping.sail,14,209,220->nested_mapping.sail,14,209,223)
anf::E_match::and exp=() loc=Range(nested_mapping.sail,14,209,221->nested_mapping.sail,14,209,223)
anf::E_match::and exp=eq_bits(b__0, [bitzero, bitzero]) loc=Range(nested_mapping.sail,14,209,211->nested_mapping.sail,14,209,215)
anf::E_match::and exp=b__0 loc=Range(nested_mapping.sail,14,209,211->nested_mapping.sail,14,209,215)
anf::E_match::and exp=[bitzero, bitzero] loc=Range(nested_mapping.sail,14,209,211->nested_mapping.sail,14,209,215)
anf::E_match::and exp=bitzero loc=Range(nested_mapping.sail,14,209,211->nested_mapping.sail,14,209,215)
anf::E_match::and exp=bitzero loc=Range(nested_mapping.sail,14,209,211->nested_mapping.sail,14,209,215)
#### anf::E_match::anf_pexp::Pat_when pat=b__1 loc=Range(nested_mapping.sail,15,225,227->nested_mapping.sail,15,225,231) guard_exp=eq_bits(b__1, [bitzero, bitone])
### pat 
anf::E_match::anf_pexp->anf_pat pat=b__1 loc=Range(nested_mapping.sail,15,225,227->nested_mapping.sail,15,225,231)
P_id id
### body 

+anf::E_match::and exp=Some(Z()) loc=Generated(Unknown)
anf::E_match::and exp=Z() loc=Range(nested_mapping.sail,15,225,236->nested_mapping.sail,15,225,239)
anf::E_match::and exp=() loc=Range(nested_mapping.sail,15,225,237->nested_mapping.sail,15,225,239)
anf::E_match::and exp=Z() loc=Range(nested_mapping.sail,15,225,236->nested_mapping.sail,15,225,239)
anf::E_match::and exp=() loc=Range(nested_mapping.sail,15,225,237->nested_mapping.sail,15,225,239)
anf::E_match::and exp=eq_bits(b__1, [bitzero, bitone]) loc=Range(nested_mapping.sail,15,225,227->nested_mapping.sail,15,225,231)
anf::E_match::and exp=b__1 loc=Range(nested_mapping.sail,15,225,227->nested_mapping.sail,15,225,231)
anf::E_match::and exp=[bitzero, bitone] loc=Range(nested_mapping.sail,15,225,227->nested_mapping.sail,15,225,231)
anf::E_match::and exp=bitzero loc=Range(nested_mapping.sail,15,225,227->nested_mapping.sail,15,225,231)
anf::E_match::and exp=bitone loc=Range(nested_mapping.sail,15,225,227->nested_mapping.sail,15,225,231)
#### anf::E_match::anf_pexp::Pat_when pat=mapping0# : bitvector(2) loc=Generated(Range(nested_mapping.sail,16,241,243->nested_mapping.sail,16,241,260)) guard_exp=bool_not_bits2_backwards_matches(mapping0#)
### pat 
anf::E_match::anf_pexp->anf_pat pat=mapping0# : bitvector(2) loc=Range(nested_mapping.sail,16,241,243->nested_mapping.sail,16,241,260)
anf::E_match::anf_pexp->anf_pat pat=mapping0# loc=Range(nested_mapping.sail,16,241,243->nested_mapping.sail,16,241,260)
P_id id
### body 

+anf::E_match::and exp=match bool_not_bits2_backwards(mapping0#) { s => Some(B(s)), _ => None() } loc=Generated(Range(nested_mapping.sail,16,241,243->nested_mapping.sail,16,241,260))

You can see here that the loc for Some(Z()) is empty, I guess this is why sail_branch_target_taken couldn't find the loc, and finally use the default value 0, 0, 0, 0.

Here is the rewrited code (I did a little format)

$[complete]
function encdec_forwards_matches arg# = let head_exp# = arg# in
        $[complete] $[mapping_match] 
        match 
        $[complete] 
        match head_exp# {
            b__0 if $[overloaded { "name" = "==", "is_infix" = true }] 
                eq_bits(b__0, [bitzero, bitzero]) => Some(true),
            b__1 if $[overloaded { "name" = "==", "is_infix" = true }]
                eq_bits(b__1, [bitzero, bitone]) => Some(true),
            ($[backwards] mapping0# : bitvector(2)) 
                if bool_not_bits2_backwards_matches(mapping0#) => 
                    $[complete] match bool_not_bits2_backwards(mapping0#) {
                        s => Some(true),
                        _ => None()
                    },
            _ => None()
        } {
        Some(result) => result,
        None(_) => $[incomplete] match head_exp# {_ => false}
    }

Related function should be the following, this is where exp is wrapped by Option:

let some_arm = function
  | Pat_aux (Pat_exp (pat, exp), annot) -> Pat_aux (Pat_exp (pat, mk_exp (E_app (mk_id "Some", [exp]))), annot)
  | Pat_aux (Pat_when (pat, guard, exp), annot) ->
      Pat_aux (Pat_when (pat, guard, mk_exp (E_app (mk_id "Some", [exp]))), annot)

After I add the loc to Some, log shows correct, and html result looks very good

Result before modification

I'll add and test more cases

[Alasdair]

Thanks, I'm on vacation this week but I can take a look at any PR when I get back on monday!