CakeML / cakeml

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

Remove Failure CompileError #520

Open myreen opened 6 years ago

myreen commented 6 years ago

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:

  1. 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

  2. adjust the lab_to_target compiler so that it makes use of these temporaries

  3. adjust the semantics of LabLang and StackLang 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.

myreen commented 6 years ago

Note that this issue goes against #186.

myreen commented 6 years ago

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.

sorear commented 4 years ago

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.