Closed mmcloughlin closed 9 months ago
I also get the same error when running on the ACL2 x86 model. Running make x86.ir
in sail-x86-from-acl2/model
:
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
../../isla/isla-sail/isla-sail -splice ../test-generation-patches/bang_memi.sail -splice ../test-generation-patches/lahf.sail -splice ../test-generation-patches/logcount_alt.sail -splice ../test-generation-patches/slices.sail -verbose 1 -o x86 prelude.sail register_types.sail registers.sail register_accessors.sail opcode_ext.sail memory_accessors.sail init.sail config.sail logging.sail step.sail main.sail
Type check [==================================================] 100% (71/71)
Type check [==================================================] 100% (87/87)
Type check [==================================================] 100% (87/87)
Type check [==================================================] 100% (87/87)
Type check [==================================================] 100% (87/87)
Type check [==================================================] 100% (119/119)
...
Type check [==================================================] 100% (7850/7850)
Effects (direct) [==================================================] 100% (7850/7850)
Effects (transitive) [==================================================] 100% (2073/2073)
Type check [==================================================] 100% (7850/7850)
Rewrite [==================================================] 100% (constant_fold)
Type check [==================================================] 100% (3/3)
Fatal error: exception File "jib_ir.ml", line 84, characters 2-7: Pattern matching failed
As an aside, would you be able to advise whether you expect ISLA to work on the x86 model?
Thanks again.
Currently the isla-sail plugin only works with the very latest development commit of Sail (when I remember to update it...) and not any released version.
When I started developing Isla I didn't want commit to the IR format being stable, so I made the translator as an external plugin to avoid it being part of the released version of Sail. I then made the isla-snapshots repository as a workaround for others when having a bleeding-edge version of everything wasn't practical. Now I could probably upstream the IR translator and have it be built into Sail, as things are more stable. Might be worth considering now.
I think we have had some success with translating the x86 model, but I don't think it's been fully integrated with the concurrency tooling yet (I also have some personal RISC-V patches I haven't upstreamed yet).
Thanks for getting back to me. I think I have run this with the latest commit of Sail now, and I'm getting a different error. (My hesitancy is because I have never used OCaml before and I am getting confusing results from opam pin
.)
arm-v9.4-a$ make gen_ir
[WARNING] var was deprecated in version 2.1 of the opam CLI. Use opam var instead or set OPAMCLI environment variable to 2.0.
mkdir -p ir
../../isla/isla-sail/isla-sail -v 1 -mono_rewrites src/prelude.sail src/decode_start.sail src/builtins.sail src/v8_base.sail src/sysregs_autogen.sail src/sysregs.sail src/instrs64.sail src/instrs64_sve.sail src/instrs64_sme.sail src/instrs32.sail src/interrupts.sail src/reset.sail src/fetch.sail src/interface.sail src/devices.sail src/impdefs.sail src/mem.sail src/decode_end.sail src/map_clauses.sail src/event_clauses.sail src/stubs.sail src/elfmain.sail src/isla_main.sail -o ir/armv9
Type check [==================================================] 100% (2/2)
Type check [==================================================] 100% (2/2)
Type check [==================================================] 100% (2/2)
Type check [==================================================] 100% (6/6)
Type check [==================================================] 100% (6/6)
Type check [==================================================] 100% (4/4)
Type check [==================================================] 100% (2/2)
Type error:[ ] 1% (505/31593)
/home/mbmcloug/.opam/4.10.0/share/sail/lib/string.sail:99.4-9:
99 |val print = pure "print" : string -> unit
| ^---^ Previous binding
src/prelude.sail:314.0-58:
314 |overload print = {print_endline, print_int, print_integer}
|^--------------------------------------------------------^
| print cannot be defined as an overload, as it is already bound
make: *** [Makefile:75: gen_ir] Error 1
On the other hand, make x86.ir
in sail-x86-from-acl2
does now work!
I've seen that error (with other backends), and a workaround seems to be to remove the line
overload print = {print_endline, print_int, print_integer}
in src/prelude.sail
. We should double-check the impact on other Sail versions, though.
I think I pushed a fix to sail-arm. In the library print
is without a newline like in OCaml and the uses in elfmain were expecting that as they had an explicit '\n' at the end of the string literal. I think the __ListConfigs bits were the only other usage, so I changed them to print_endline
directly but they look odd as they seem to have \\n
which I'm not sure is intended.
https://github.com/rems-project/sail-arm/commit/f7dedcf3564df71ef065e56b28ff8c9689272596
Thanks! I am able to produce armv9.ir
now.
I am trying to use
isle-isla
to derive the input IR files, rather than relying on the snapshots.I'm currently getting an error from
isle-isla
on the ARM v9.4 SAIL. Specifically, when I runmake gen_ir
in thearm-v9.4-a
directory ofsail-arm
:These projects appear to be very sensitive to version combinations. I am testing with:
isla
: https://github.com/rems-project/isla/commit/b1d9314c938407dc08bb494b6cabb2bb32332ae3sail
: https://github.com/rems-project/sail/tree/0.17.1sail-arm
: https://github.com/rems-project/sail-arm/commit/c3ea1230c8401d45b29324829cc00ecc9fb726d3Thank you!