Error during Lem generates definitions for Isabelle

[haitianzhishang]

Source sail code: Translated Lem code: The error during generating Isabelle definition using 'make riscv_isa_build' : The error description is rough and I don't know how to solve it. Hope for some directions.

[bacam]

Isabelle and Lem both require bitvectors to have statically known sizes - that is, they should either be a constant, or a parameter of the function (like 'n here). Unfortunately the size of shift_bits is only known at execution time.

We've encountered this before in the Arm models, and have a little support for rewriting this kind of thing into operations that don't need the execution-time sized bitvectors. For example, if we include mono_rewrites.sail from the libarary, use the -mono_rewrites option, and inline shift_bits,

let result : int = unsigned(slice(data, 0, lg2_sew));

then the resulting Lem uses unsigned_slice from the mono_rewrites library. I'm not sure what the best solution here is; some options are:

• Use unsigned_slice from mono_rewrites directly in the specification
• Do the inlining above so that it's rewritten for you
• If sew can only take a small set of values (e.g., {8,16,32,64}) then put that in the function signature and let Sail's monomorphisation introduce a case split

None of these is ideal, but I suspect the last one is probably the best option.

[haitianzhishang]

Thanks for your reply. If in this case that Isabelle and Lem both require bitvectors to have statically known sizes, it maybe inflexible for RISC-V vector extension and matrix extension.

[bacam]

It can be a problem, but we have successfully built several Arm models with vector instructions. This uses the monomorphisation support I mentioned above, which tries to introduce enough case splits that the resulting bitvectors have suitable sizes, along with some built-in rewrites to handle common patterns like unsigned(slice(...)).