cakeml
cakeml copied to clipboard
Remove Failure CompileError
Currently, the compiler is allowed to return Failure CompileError
for any input program. At present, these compiler errors can only
occur when a code label is too far from the current program location,
i.e. the jump offset that needs to be encoded in the instruction just
does not fit the instruction encoding.
This issue is about removing such compiler errors completely by:
-
annotating each instruction that might cause such an encoding error with two registers that can safely be used as temporaries when computing the target address
-
adjust the
lab_to_target
compiler so that it makes use of these temporaries -
adjust the semantics of
LabLang
andStackLang
so that these instructions delete the registers mentioned in temporary register annotations
I suspect the word_to_stack
compiler knows which two registers are
available to be used as temporaries on the StackLang
side.
Note that this issue goes against #186.
A potentially less intrusive approach could be to leave the compiler implementation as is, but instead construct a compiler configuration transformer that given a normal compiler configuration produces a new configuration where two registers are reserved (unusable by CakeML's register allocator). These reserved registers can then be used to implement "smart" encoders for instructions that require unusually large code offsets.
One could prove that, given such a tweaked compiler configuration,
the compiler can never return Failure CompileError
.
Use of such defensively written compiler configurations might not have a performance impact on architectures that provide more than 16 registers, since CakeML is unlikely to be able to make effective use of that many registers anyway.
What's going to happen if I feed code that would be >4GB compiled to a 32-bit backend? Also, this seems to be in contradiction with #544.