Sail dislikes the arm-v9.4-a spec ("Fatal error: exception Stack overflow")

[Trolldemorted]

I tried to use the armv8 spec, but unfortunately sail complains:

root@637ad2b838a9:/input/arm-v9.4-a# make   
[WARNING] Running as root is not recommended
[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 isabelle
sail -dprofile -verbose 1 -memo_z3 -grouped_regstate \
        -lem -lem_output_dir lem -isa_output_dir isabelle -o armv9 -lem_lib Prelude \
        -lem_mwords -mono_rewrites -auto_mono -undefined_gen \
        -splice src/lem-patches/AddPAC.sail -splice src/lem-patches/Auth.sail -splice src/lem-patches/CountLeadingSignBits.sail -splice src/lem-patches/DecodeBitMasks.sail -splice src/lem-patches/FPRecpX.sail -splice src/lem-patches/FPRoundIntN.sail -splice src/lem-patches/Poly32Mod2.sail -splice src/lem-patches/Reduce.sail -splice src/lem-patches/SPEConstructRecord.sail -splice src/lem-patches/memcpy.sail -splice src/lem-patches/merging_float_conversions.sail \
        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  -mono_split src/instrs64_sve.sail:11315:esize \
 -mono_split src/instrs64_sve.sail:11394:esize \
 -mono_split src/instrs64_sve.sail:11473:esize \
 -mono_split src/instrs64_sve.sail:11552:esize \
 -mono_split src/instrs64_sve.sail:11631:esize
Warning: Deprecated src/v8_base.sail:2141.61-74:
2141 |val read_gpr : forall 'n, 0 <= 'n <= 30. int('n) -> bits(64) effect {rreg}
     |                                                             ^-----------^
     |
Explicit effect annotations are deprecated. They are no longer used and can be removed.

Fatal error: exception Stack overflow
make: *** [Makefile:38: lem.stamp] Error 2

Steps to reproduce:

• clone https://github.com/rems-project/sail-arm
• clone this repo, build the latest nightly image
• docker run --rm -it -v "/path/to/sail-arm\:/input" --entrypoint bash sail
• eval `opam env`
• cd /input/arm-v9.4-a/
• make

Am I doing something wrong?

[bacam]

Perhaps the environment has a stack limit that's too low? On my Ubuntu 22.04 machine the default is 8MB (from ulimit -a) and having just set it running it's already much further on. That said, from memory you'll need to increase the stack limit for lem anyway, because there's some inefficiency that's not been important enough for us to track down. Note that the C output is generally much more efficient.

[Trolldemorted]

My ulimit -a says the stack size is 8 MB as well:

root@b056f82bd82a:/input/arm-v9.4-a# ulimit -a
real-time non-blocking time  (microseconds, -R) unlimited
core file size              (blocks, -c) 0
data seg size               (kbytes, -d) unlimited
scheduling priority                 (-e) 0
file size                   (blocks, -f) unlimited
pending signals                     (-i) 102326
max locked memory           (kbytes, -l) 82000
max memory size             (kbytes, -m) unlimited
open files                          (-n) 1048576
pipe size                (512 bytes, -p) 8
POSIX message queues         (bytes, -q) 819200
real-time priority                  (-r) 0
stack size                  (kbytes, -s) 8192
cpu time                   (seconds, -t) unlimited
max user processes                  (-u) unlimited
virtual memory              (kbytes, -v) unlimited
file locks                          (-x) unlimited

[Alasdair]

The nightly docker container is using an older version of OCaml that doesn't have the TRMC (tail recursion modolo cons) optimisation. Maybe that's the issue? You could try switching it to OCaml 5.2.0

[bacam]

I finally got a setup where I could use docker, and increasing the stack to 64kB (a number I just tried at random) works. Looking at the stack trace when it fails with the default stack size, it's in the menhir generated parser during expression parsing. It appears to be a plain tail-call optimisation failure, which is a little bizarre.

[Alasdair]

I'm sure I've run into this before, and I think it's that recent menhir versions are relying on recent OCaml versions for optimizations.

[Alasdair]

#751 I increased the version because there's no reason for it to be on 4.10.0

[bacam]

That gets past parsing without any problems (I'll leave it running to check it actually produces a C model). It's a little unfortunate that we don't know suitable version combinations in general, although from the changelog any OCaml version from 4.14.0 onwards should be OK.