Found side effects: incomplete pattern match; but it is complete?

[Timmmm]

Consider the following code:

default Order dec

$include <prelude.sail>

enum ExecutionMode = {
  Legacy,
  PureCap,
}

mapping execution_mode_encdec : ExecutionMode <-> bits(1) = {
  Legacy <-> 0b0,
  PureCap <-> 0b1,
}

struct Capability = {
  mode : ExecutionMode,
}

function bitsToCap(cap_bits : bits(1)) -> Capability = {
  struct {
    mode = execution_mode_encdec(cap_bits),
  }
}

let null_cap : Capability = bitsToCap(0b0)

It gives this error:

25 |let null_cap : Capability = bitsToCap(0b0)
   |    ^------^
   | Top-level let statement must not have any side effects. Found side effects: incomplete pattern match

But execution_mode_encdec is complete, unless I'm missing something.

[Timmmm]

Much simpler example:

default Order dec

$include <prelude.sail>

mapping bool_bit : bool <-> bit = {
  true <-> bitone,
  false <-> bitzero,
}

let x : bool = bool_bit(bitzero)

I believe the error originates with this line in src/lib/effects.ml:221:

    | DEF_aux (DEF_mapdef _, _) -> effects := EffectSet.add IncompleteMatch !effects

If I comment it out then it compiles without any issues, though presumably this isn't sound. It looks like although match is checked for completeness, mapping isn't, so the code just assumes it might be incomplete. This probably also explains why this doesn't produce a The following expression is unmatched warning:

mapping bool_bit : bool <-> bit = {
  true <-> bitone,
}

[trdthg]

Hi, I have some idea about this:

• reuse match's complete check on mapping's both sides

  • there would be something like this:

    mapping Foo : bits(2) <-> int = {
    0b00 <-> 10,
    0b01 <-> 1,
    forwards _ => 5,
    backwards _ => 0b11
    }

    commit

  • and type_check ignore guard now， but this is acceptable? rustc can't do it either

• add $[complete] addribute for mapping

  • which can be very easy here

• add something like $[allow(incomplete)] for let exp, like #[allow(xxx)] in rust

I personally like the first

---

Update: trying to implement the first method. add something like PC.is_complete_mapcls_wildcarded.