search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
947 stars 83 forks source link

Trouble building arm8 compiler #780

Open sorear opened 4 years ago

sorear commented 4 years ago

Even with CML_HEAP_SIZE=60000 it fails with an out of heap error.

tanyongkiam commented 4 years ago

Just to clarify: Do you mean compiling the 64-bit CakeML compiler sexpr using the x64 compiler with --target=arm8?

If so that seems extremely weird.

sorear commented 4 years ago

Yes. I get a working compiler for x64 and riscv, a compiler (untested) for mips, and no compiler for arm8.

tanyongkiam commented 4 years ago

I suspect it's not actually running out of heap -- that's a misleading error message.

Instead, I think the ARM8 encoder is actually failing to compute a jump that is large enough.

Could you try compiling with --jump=false please?

tanyongkiam commented 4 years ago

Specifically, see https://github.com/CakeML/cakeml/pull/721 and the issues inside.

sorear commented 4 years ago

Ah, I see what happened here. I got "AssembleError" then "out of heap", which I misinterpreted as the heap error being caught (makes no sense in retrospect, but yet). --jump=false resolved it; I think the arm8 encoder just needs to fall back to jump-over-jump.

tanyongkiam commented 4 years ago

Yes we've run into this issue before: arm8 used to be just under the jump offset limit, but I guess we've grown the basis a lot since I last tried.

I'm not sure what you meant by jump-over-jump but the --jump=false flag toggles between either jumping to a call or halting on a branch: https://github.com/CakeML/cakeml/blob/master/compiler/backend/stack_removeScript.sml#L59

If I remember right (@myreen can confirm), the reason for the jump is because it is more space efficient.

However JumpLower has a short range (when encoded) on some platforms. We should consider just setting the default configuration for arm8 to F.

sorear commented 4 years ago

arm8 conditional branches have a range limit of 1 MiB; I'm trying to build the compiler itself from the sexpr, which results in 13 MiB of text. It's not close.

By jump-over-jump I mean that overlong conditional branches should be rewritten into a conditional jump of the opposite sense around an unconditional jump, e.g. https://github.com/CakeML/cakeml/blob/master/compiler/encoders/riscv/riscv_targetScript.sml#L164 . (This example is not ideal because it needs to allow for >1MiB jumps using auipc/jalr, ideally we would have fall backs for >2GiB so that the only way to get an AssembleError is if the address space is exhausted)