CakeML
Using the ABI stack pointer
Most of our targets have some degree of ISA support for a stack using a single register, which by necessity is shared with C:
- x64: %rsp is the only register which can be used for the push/pop/call/ret family of instructions, which allows for much smaller save and restore code and potentially avoids branch mispredicts for functions called from several places.
- riscv: sp supports a 16-bit encoding for saving and restoring any register, so save and restore sequences will be moderately shorter in proportion to the number of registers used.
- arm7: Supports load-multiple and store-multiple on any register, so save and restore code should only be 32 bits normally, but using sp can reduce that to 16.
- mips: I do not believe the ABI stack pointer is special in the 32-bit mode. There are several 16-bit modes, I believe much of the above for riscv is applicable but have not checked details.
- arm8: The ABI stack pointer x31 has less features than a general register since it is overloaded as zero for some instructions. In particular this includes
cmp; checking the stack against a limit stored in another register requires 3 instructions on arm8.
On x64 and arm7, another advantage is that using sp for the stack frees up another register for general use.
On all architectures, including arm8, there may be tooling advantages to using the architectural stack. I believe that DWARF is general enough that a full-featured debugger can be taught to walk stack traces on %r12; however the perf tool's DWARF mode can only record within a fixed window around the ABI stack pointer, so using that would make perf record more useful.
In any case this should probably be an option.
The difficulty of this depends greatly on environmental assumptions. If there is no C FFI, changing the register used is trivial; otherwise the proofs would need to model the possibility of FFI calls and in particular signal handlers modifying a configuration-dependent amount of memory below the stack pointer. (On x64 and SPARC, signal handlers can only modify below sp - N for an architecture-defined N, so small negative offsets can be used.)
