Type-checker confused about what constitutes a binding or a reference in mapping patterns

[nwf-msr]

Whether a variable in a pattern is in reference to a value in scope or is, instead, a binder introduced by the pattern is inconsistently handled. This results in confusion when one attempts to use a value (that is, a variable in the former case) twice in a pattern.

Here's a reasonably minimal test program. Compile with -D BAD1 through -D BAD4 to elicit different cases. It is not necessary to do more than type-check to tickle this behavior (that is, -just_check suffices, without need of -c or -ocaml or any such).

default Order dec
$include <prelude.sail>

let zeros_2 : bits(2) = sail_zeros(2)
let zeros_3 : bits(3) = sail_zeros(3)

val test : (bits(3), bits(3)) <-> bits(6)
scattered mapping test

mapping clause test = (0b111, zeros_3) <-> 0b111000

$ifdef BAD1
    /*
     * This raises a type error if included:
     *   Tried performing type coercion from bitvector(2, dec) to bitvector(3, dec) on zeros_2
     *   Coercion failed because:
     *   Failed to prove constraint: 2 == 3
     * so clearly the pattern matching system understands that this is in reference to the value
     * zeros_2 in scope and defined above.  Given that, I expect this to fail as it does.
     */
  mapping clause test = (0b000, zeros_2) <-> 0b000001
$endif

$ifdef BAD2
    /*
     * This raises a compiler failure if included:
     *   Duplicate binding for zeros_3 in pattern
     * but this isn't (meant to be) a binding!  It wasn't a binding in either case above, so it's
     * rather odd that this is rejected.
     */
  mapping clause test = (zeros_3, zeros_3) <-> 0b000010
$endif

/* Of course, there's nothing special about doing this in tuples.  This is OK... */
mapping clause test = (0b000, 0b001) <-> zeros_3 @ 0b001

$ifdef BAD3
    /* This isn't: Failed to prove constraint 6 == 5.  I expect this */
  mapping clause test = (0b000, 0b010) <-> zeros_3 @ zeros_2
$endif

$ifdef BAD4
    /* This isn't either: Duplicate binding for zeros_3.  As with BAD2, I don't expect this either. */
  mapping clause test = (0b000, 0b011) <-> zeros_3 @ zeros_3
$endif

[Alasdair]

All these mappings should be rejected I think. The left and right hand sides of a mapping should bind the same set of identifiers, and none should be duplicated. Referring to external let-bound variables should not be allowed.

Here the forwards case binds (shadows) zeros_3 but it doesn't appear on the rhs:

(0b111, zeros_3) <-> 0b111000

The second case (BAD1) should fail for the same reason.

For BAD2 this should fail because the forwards case becomes

function test_forwards(zeros_3, zeros_3) = 0b000010

which binds zeros_3 twice. BAD4 has the same problem.

BAD3 and the case between BAD2 and BAD3 should fail because they have the same problem as BAD1 in reverse.

I think in these cases what you really want are functions, not mappings. In general mappings should be total in both directions. The semantics for partial mappings were not adequately considered when they were implemented, and I don't see any real way to fix them in a backwards compatible way. Realistically the mapping code needs a full re-write, when I do go in to patch issues I just find more wrong with it - like the fix the other day was replacing OCaml's polymorphic equality with an alpha_equivalent check, but was very clear to me that the code in question relying on some notion of syntactic type-equality is likely just incorrect.

[nwf-msr]

Hm. Partiality of mappings is very convenient as a sail user, but I am willing to believe that it's painful for sail's authors. I'm not quite sure that this particular issue comes from partiality, though, but I could be convinced.

Concretely, this case comes about in my model because I am using a mapping to decode instructions, and some of the instructions I'm trying to decode do not pay attention to all of their bits, so I'd like the "ADT" side to not need to capture those fields and for the "bitvector" side to just have zeros in their place. I can do that in Sail as it stands, but IMHO it's much nicer to see

... @ register_selector_bits(rd) @ register_selector_zero @ register_selector_zero  @ ...

than

...  @ register_selector_bits(rd) @ 0b000000 @ 0b000000 @ ...

and that means referring to values in the environment. I can try using function clauses instead of mapping clauses in my model, but that sounds like it's going to be a bit of pain.

[nwf-msr]

Oh, hah, I just thought up the following terrible hack.

mapping register_selector_bits_zero : unit <-> bits(RegisterSelectorBits) = { () <-> 0b000000 }
mapping clause insn_code = ... <-> ... @ register_selector_bits_zero() @ register_selector_bits_zero() @ ...

works just fine.

[Alasdair]

Yes, there's no way with mapping patterns to distinguish between a new variable in the mapping and a reference to a constant. In a regular pattern you would have to introduce a new variable and do:

match bitvector {
    0b1 @ 0x0 @ field : bits(3) if field == register_selector_zero => ...
}

but you can't do that for all guards expressions in a bi-directional way. To support that we would need either need new syntax for a pattern that means "check the matched value is equal to this expression", or a special toplevel constant definition that always binds to a literal so you could do:

constant register_selector_bits_zero = 0b000000

and use it in patterns. It might be good to enforce some style like ALL_CAPS to distinguish from regular variables there though.

[Alasdair]

Your hack also really isn't that terrible imho

[Alasdair]

Another thing is having a way to name the bitvectors in patterns is something I want for documentation generation, so worth thinking about the right way to go about this.

[nwf-msr]

Your hack also really isn't that terrible imho

Unfortunately, it doesn't actually work due to #245. The code generated for the outer pattern's matches logic makes an unconditional call to zregister_selector_bits_zzero_backwards rather than conditioning on zregister_selector_bits_zzero_backwards_matches:

bool zinsn_code_backwards_matches(uint64_t zargz3)
{
    // ... much code elided ...
    uint64_t z_mappingpatterns_49z3shadowz3167;
    z_mappingpatterns_49z3shadowz3167 = (safe_rshift(UINT64_MAX, 64 - 6) & (zv__77 >> INT64_C(54)));
    // ... some other bit slicing elided ...
    unit zgaz3319;
    zgaz3319 = zregister_selector_bits_zzero_backwards(z_mappingpatterns_49z3shadowz3167);

[Alasdair]

Original issue should be addressed by #253 I'll look into the thing with the register_selector_bits_zero

[Alasdair]

I added a test for unit <-> bits(N) mappings and it seems to work fine now