Error on ARM v9.4: exception File "jib_ir.ml", line 84, characters 2-7: Pattern matching failed

[mmcloughlin]

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 run make gen_ir in the arm-v9.4-a directory of sail-arm:

...
Type check [==================================================] 100% (2/2)
Type check [==================================================] 100% (2/2)
Type check [==================================================] 100% (2/2)
Type check [==================================================] 100% (137593/137593)
Type check [==================================================] 100% (137593/137593)
Rewrite [==================================================] 100% (constant_fold)
Type check [==================================================] 100% (3/3)
Compiling [==================================================] 100% (initialize_registers)
Fatal error: exception File "jib_ir.ml", line 84, characters 2-7: Pattern matching failed
make: *** [Makefile:75: gen_ir] Error 2

These projects appear to be very sensitive to version combinations. I am testing with:

isla: b1d9314
sail: https://github.com/rems-project/sail/tree/0.17.1
sail-arm: rems-project/sail-arm@c3ea123

Thank you!

[mmcloughlin]

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.

[Alasdair]

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).

[mmcloughlin]

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

[mmcloughlin]

On the other hand, make x86.ir in sail-x86-from-acl2 does now work!

[bauereiss]

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.

[Alasdair]

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.

rems-project/sail-arm@f7dedcf

[mmcloughlin]

Thanks! I am able to produce armv9.ir now.