Lexical Error?

[selig]

Hi,

I want to explore the SMT translations produced by Sail for the CHERI Sail definitions. My starting point has been to try and get something running but I hit against the below error. I assume I'm doing something wrong (probably due to skipping some README somewhere) but would welcome a hint.

Thanks, Giles

Giless-Laptop:mips giles$ sail mips_prelude.sail mips_wrappers.sail mips_insts.sail mips_epilogue.sail
Lexical error:
[mips_prelude.sail]:339:14-14
339 | (word[31] ^^ 32) != word[63..32]
| ^
| Operator fixity undeclared ^^

[selig]

I am using "Sail 0.13 (sail2 @ opam)" installed from opam

[bauereiss]

That operator is declared in mips/prelude.sail. It might be useful to look at the Makefiles, which contain commands with the right files in the right order to generate different artifacts. In particular, there is the cheri128_smt target in the Makefile in the cheri directory, which generates SMT problems for the properties defined in the properties_128.sail file. It doesn't seem to work as is at the moment; I think that's because a recent change in the TLB code is not reflected in the mips_tlb_stubs.sail file. It works for me when changing the dependency of the Makefile target from $(CHERI128_NO_TLB_SAILS) to $(CHERI128_SAILS).