Two more mapping bugs

[nwf-msr]

These might really stem from partiality of mappings, but at a glance it looks like the generated code is confused.

Sometimes sail is deeply confused about whether a mapping applies:

default Order dec
$include <prelude.sail>

enum E = { EA, EB }
mapping inner : bits(1) <-> E = { 0b0 <-> EA }
mapping outer : bits(2) <-> (E, bits(1)) =  { x @ y <-> (inner(x), y) }

val main : unit -> unit
function main() =
{
  /* These check out */
  assert(outer_forwards_matches(0b00) == true);
  assert(match outer(0b00) { (EA, 0b0) => true, _ => false });
  assert(outer_forwards_matches(0b01) == true);
  assert(match outer(0b01) { (EA, 0b1) => true, _ => false });

  /* This assertion fails; that is, outer_forwards_matches(0b10) returns true. */
  assert(outer_forwards_matches(0b10) == false);

  /* This throws a pattern match failure in inner_forwards, despite the true return above. */
  assert(match outer(0b10) { _ => true });

  ()
}

Moreover, sometimes sail generates code that blows up when the question is even asked:

default Order dec
$include <prelude.sail>

union E = { EA : unit, EB : unit }
mapping inner : E <-> bits(2) = { EA() <-> 0b00, EB() <-> 0b10 }
mapping outer : bits(4) <-> unit = { inner(EA()) @ 0b00 <-> () }

val main : unit -> unit
function main() = assert(outer_forwards_matches(0b1000) == false)

When compiled (without error) into C and then compiled and run, the resulting program dies with

Pattern match failure in outer_forwards_matches

[Alasdair]

I think this is intentional as x @ y matches all bitvectors of length 2.

  /* This assertion fails; that is, outer_forwards_matches(0b10) returns true. */
  assert(outer_forwards_matches(0b10) == false);

This is also what I would expect as there is no case for 0b1 in inner, so it will fail at runtime - pattern match failure is always instantly fatal and cannot be recovered from, there is no backtracking.

  /* This throws a pattern match failure in inner_forwards, despite the true return above. */
  assert(match outer(0b10) { _ => true });

The second example is just broken, but I don't see a good way of fixing it without rewriting all the mapping elaboration code sigh, the current code doesn't handle the nested matching within the inner match, so when it gets EB() from 0b10 that fails to match with EA(). I can probably easily fix it in the C backend, because there I can handle the mapping patterns in a custom way without relying on a Sail -> Sail rewrite.

The actually correct elaboration should be:

match x {
  mapping(A) => <expr>,
  <rest>
}

into

let y = x;
match (match y {
  z => {
    match mapping(z) {
      A => Some(<expr>),
      _ => None(),
    }
  },
  _ => None()
}) {
  Some(w) => w,
  None() => match y {
    <rest>
  }
}

[nwf]

I think this is intentional as x @ y matches all bitvectors of length 2.

  /* This assertion fails; that is, outer_forwards_matches(0b10) returns true. */
  assert(outer_forwards_matches(0b10) == false);

I was, perhaps naively, expecting the partiality of inner to impact the totality of the outer match. Is there a concise way of doing what I want, there? (I guess x @ y if inner_forwards_matches(x) <-> (inner(x), y)?)

[Alasdair]

It's possible we could generate code in such a way that it would do that, I'm not sure if it makes sense though.

[Alasdair]

Currently I have:

default Order dec
$include <prelude.sail>

enum E = { EA, EB }
mapping inner : bits(1) <-> E = { 0b0 <-> EA }
mapping outer : bits(2) <-> (E, bits(1)) =  { x @ y <-> (inner(x), y) }

val main : unit -> unit
function main() =
{
  /* All inner cases */
  assert(inner_forwards_matches(0b0));
  assert(not_bool(inner_forwards_matches(0b1)));
  assert(inner_backwards_matches(EA));
  assert(not_bool(inner_backwards_matches(EB)));

  /* x @ y matches anything */
  assert(outer_forwards_matches(0b00));
  assert(outer_forwards_matches(0b01));
  assert(outer_forwards_matches(0b10));
  assert(outer_forwards_matches(0b11));

  /* inner(x) only matches for EA */
  assert(outer_backwards_matches((EA, 0b0)));
  assert(outer_backwards_matches((EA, 0b1)));
  assert(not_bool(outer_backwards_matches((EB, 0b0))));
  assert(not_bool(outer_backwards_matches((EB, 0b0))));
}

In this case it's not hard to see how we could take inner(x) into account for outer_forwards_matches, but the cases I'm wondering about are if we replaced inner(x) with nested mappings like f(g(x)), then we have to apply g(x) first so the rewriting step becomes more complex (but it's in theory doable, as mappings are technically supposed to be pure anyway).

[nwf-msr]

In re x @ y matches anything, I guess my only argument is one of aesthetics: it seems rude for _matches to return true on an input that will irrecoverably crash Sail if passed to the mapping function. But I think this case could be addressed by model authors by using x @ y if inner_backwards_matches(x) <-> (inner(x), y), which will cause the LHS pattern to become partial and so outer_forwards_matches no longer constantly true, right?

But it looks like the other issues I've tripped over are fixed in HEAD. Thank you very much for looking at this all so quickly. <3

[Alasdair]

It's the same behaviour as if you wrote match <bitvector> { x @ y => (inner(x), y) }. There the inner mapping as part of an arbitrary expression on the right hand side of the match, so it can't really affect whether x @ y matches. I'm wary of changing the semantics of x @ y <-> (inner(x), y) to something that isn't just x @ y => (inner(x), y) and (inner(x), y) => x @ y.

Using the guard like you suggest works. I could add an overload for inner_forwards_matches and inner_backwards_matches to allow:

x @ y if inner_matches(x) <-> (inner(x), y)

[Alasdair]

Now I'm thinking about a case like:

UTYPE(hex_bits(20, imm), rd, op) <-> utype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ imm

where it probably does make sense to use the hex_bits constraint on imm in the parsing direction.

[nwf-msr]

Ah, yes, that (the desugaring into match) is quite fair!

OK, I think I am happy in a world where:

• mapping partiality is recursive through patterns, so that if inner is partial, (inner(x), y) and inner(x) @ y are also partial patterns.
  • This addresses the special cases of inner(EnumArm) and the "unit mapping to get a constant" trick.
• the other-hand side of a mapping or match clause should not influence totality of a pattern.

Injective-but-not-bijective mappings need guards only in the backwards direction (resp. surjective the forwards direction); arbitrary mappings will want guards on both sides. That seems manageable to me.