search

CHERIoT-Platform / cheriot-sail

Sail code model of the CHERIoT ISA
Other
34 stars 9 forks source link

Type error while building with upstream Sail #56

Closed marnovandermaas closed 4 months ago

marnovandermaas commented 5 months ago

I am building with upstream Sail, commit: b81e2823f8b4ffcf14cb0b11c260d79d3a19b0dc

I'm getting the following type error:

Type error:
src/cheri_riscv_types.sail:143.31-33:
143 |    EXC_LOAD_CAP_PAGE_FAULT => 26,
    |                               ^^
    | int(26) is not a subtype of {('e : Int), (0 <= 'e & 'e <= 2). int('e)}
    | as (0 <= 'ex2448167 & 'ex2448167 <= 2) could not be proven
    | 
    | type variable 'ex2448167:
    | src/cheri_riscv_types.sail:143.31-33:
    | 143 |    EXC_LOAD_CAP_PAGE_FAULT => 26,
    |     |                               ^^ bound here
    |     | has constraint: 26 == 'ex2448167

In the code the type definition says the execution code must be less than xlen: https://github.com/microsoft/cheriot-sail/blob/ef8cfbccdbaf760798449827b5d82ffa2ba9a582/src/cheri_riscv_types.sail#L140

I'm not exactly sure why the Sail compiler thinks xlen is equal to 2.

rmn30 commented 5 months ago

Looks like it might be a recently introduced bug in the Sail compiler. I'll investigate a bit. That type looks a bit odd anyway as I'd expect the result to be in the range 0..2**xlen-1 . That doesn't appear to be the problem, though.

marnovandermaas commented 5 months ago

Ok, thanks. May be worth opening up an issue on the Sail repo in that case.

Alasdair commented 5 months ago

Should now be fixed in Sail if you pull the latest commit.

marnovandermaas commented 4 months ago

Ok, I'm going to close this issue now.