cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Variable length instructions on arm7 and riscv

Open sorear opened this issue 5 years ago • 0 comments

On riscv, this might be as simple as changing Encode to EncodeRVC in compiler/encoders/riscv/riscv_targetScript.sml and fixing the type error. This should be optional since riscv implementations are allowed to omit RVC (mostly as a concession to academic and hobbyist implementors; I have not seen a product lacking RVC) which requires plumbing target flags from the toplevel. Ideally the compiler should also generate addi instructions for loading small immediates and copying registers; the current code using ori and or is a MIPSism. A preliminary estimate by reassembling instructions in a current binary is that this could save 3.5 MB (about 20%); it would be higher if register allocation were also optimized.

The T32 instruction set is mandatory on arm7 and, since we're not using predicates, there is little reason not to use it. Little reason except for T32 function pointers being architecturally required to be odd (there are no non-interworking calls AFAIK) and the CakeML GC expecting all odd values in the heap to be pointers. You will likely need to store code pointers with their bit 0 cleared and add 1 to them prior to calls. It should be possible to avoid this overhead for return addresses since the GC has precise stack maps.

sorear avatar Sep 17 '20 00:09 sorear