search

riscv / sail-riscv

Sail RISC-V model
https://lists.riscv.org/g/tech-golden-model
Other
409 stars 150 forks source link

sail compile temp broken. #292

Open dansmathers opened 11 months ago

dansmathers commented 11 months ago

When I ran: make ARCH=RV32

echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/RV32/riscv_types.lem lem -isa -outdir generated_definitions/isabelle/RV32 -lib Sail=/home/504984/.opam/default/share/sail/src/lem_interp -lib Sail=/home/504984/.opam/default/share/sail/src/gen_lib \       handwritten_support/0.11/riscv_extras.lem handwritten_support/0.11/mem_metadata.lem handwritten_support/0.11/riscv_extras_fdext.lem \       generated_definitions/lem/RV32/riscv_types.lem \       generated_definitions/lem/RV32/riscv.lem File "generated_definitions/lem/RV32/riscv.lem", line 282, character 24 to line 282, character 34 Type error: unbound variable for targets {isabelle}: sign_extend make: *** [Makefile:318: generated_definitions/isabelle/RV32/Riscv.thy] Error 1

Bill is investigating. The current workaround is to only build the C simulator: make [options] csim

I verified make ARCH=RV32 csim worked for me. creating an issue for tracking

bacam commented 11 months ago

Sounds like the name shadowing bug I fixed in Sail the other day: https://github.com/rems-project/sail/commit/1b7964d85ac179623d6d2e497b38407ad77fd425

billmcspadden-riscv commented 11 months ago

I was able to recreate this after some difficulty.

I see the problem with Sail version 0.15, not 0.14. (<--- This statement is probably incorrect. I'm having problems with opam. Once I got sail v0.14 properly installed, I ran into compile errors, just not the one that @dansmathers reports)

Questions:

  1. To fix this problem, we will need to update the version of Sail, yes? Or we might back out PR #279 (not preferred).

  2. Why wasn't this caught during CI? I'm assuming that the CI flow did not use Sail version 0.15, else this would have been caught.

  3. @bacam, did you check to see if your change to Sail fixed this problem? (I'm attempting to check, but am having serious problems getting opam to do what I want.)

bacam commented 11 months ago

It does (I was looking at sail-cheri-riscv at the time, but it works with the main sail-riscv repo too). A workaround would be to rename sign_extend and zero_extend to avoid the name clash with Lem's library, although it might be simpler to remove the theorem prover models from the default target, and only build them with the latest version of Sail in the CI.

jrtc27 commented 11 months ago

CI only builds the emulators; see test/run_tests.sh

Timmmm commented 2 months ago

Sounds like this is fixed?