Type check error with recent dev Sail

[rmn30]

As per CHERIoT-Platform/cheriot-sail#56 recent dev versions of Sail have started to give an odd type check failure compiling the CHERIoT sail model. It looks like this might be common to sail-riscv although I haven't tried. The following extract is sufficient to reproduce:

$include <generic_equality.sail>

type xlen : Int = 32

enum ext_exc_type = {
  EXC_LOAD_CAP_PAGE_FAULT,
  EXC_SAMO_CAP_PAGE_FAULT,
  EXC_CHERI
}

/* CHERI conversion of extension exceptions to integers */
val num_of_ext_exc_type : ext_exc_type -> {'n, (0 <= 'n < xlen). int('n)}
function num_of_ext_exc_type(e) =
  match (e) {
    EXC_LOAD_CAP_PAGE_FAULT => 26,
    EXC_SAMO_CAP_PAGE_FAULT => 27,
    EXC_CHERI               => 28
  }

sail -c then says:

15 |    EXC_LOAD_CAP_PAGE_FAULT => 26,
   |                               ^^
   | int(26) is not a subtype of {('e : Int), (0 <= 'e & 'e <= 2). int('e)}
   | as (0 <= 'ex18 & 'ex18 <= 2) could not be proven
   | 
   | type variable 'ex18:
   | /home/rmn30/cheriot-sail/sail-riscv/test.sail:15.31-33:
   | 15 |    EXC_LOAD_CAP_PAGE_FAULT => 26,
   |    |                               ^^ bound here
   |    | has constraint: 26 == 'ex18

Not sure why xlen has become 2 rather than 32.

Git bisect points the finger at ce27f52 .

[Alasdair]

It isn't that xlen has become 2, it's because for an enum e, Sail will automatically generate num_of_e and e_of_num functions that provide default conversions to and from integers. What's happening is Sail is checking your num_of_ext_exc_type using the type signature it generates for the default conversion.

Prior to that commit, Sail would look at all the definitions and if any had the same name as one of the default enum conversion functions it would just silently skip generating these functions. I wanted to move away from that as it's a very global check that makes it hard to check things incrementally per-file (which is where I want to be for future LSP support).

I think because your function is defined in the same file I can make it work. I want to make it so you can do something like

$[no_num_conversions]
enum E = ...

or

$[num_conversions { to_enum: <function_id>, from_enum: <function_id> }]
enum E = ...

and be more explicit in the future.

[rmn30]

OK, thanks for the explanation. I guess we could also rename the function so it doesn't conflict with the automatic generation. Maybe the generated ones should have a prefix like _ to reduce the chance of collisions?

[Alasdair]

Should be fixed by c057bfb which restores the previous behaviour, but with a warning.

The number conversion functions are intended to be used as a convenience, so I don't think they should be prefixed with an underscore. I think we just need to have more documentation and be a bit more explicit about what is going on.

[Alasdair]

I've been writing the manual section on enumerations recently, so it should be better documented soon.

[Timmmm]

It would be good to have a single list of all the functions that Sail automatically generates somewhere in the manual. I.e.

• Mk<Type>
• <mapping>_forward, <mapping>_backward
• num_of_<type>
• <type>_of_num

Are there any more?