Branch relaxation

[xavierleroy]

Sometimes, the target of a conditional branch instruction is so far away that the displacement overflows the range of the instruction. As a workaround, the instruction can be rewritten as a negated conditional branch followed by an unconditional jump to the target. This rewriting is called branch relaxation.

Currently, branch relaxation is implemented for PowerPC only, in the powerpc/TargetPrinter.ml pass. The implementation is suboptimal in that code size computation assumes all branch instructions to be expanded.

This PR adds a generic implementation of branch relaxation in backend/Asmexpandaux.ml, with a more clever algorithm that assumes all branch instructions not expanded initially, and recomputes code size info when some branches are expanded, until reaching a fixed point.

This PR then instantiates the generic implementation

• for AArch64, which should fix issue aarch64 assembler error: conditional branch out of range #564 ;
• for PowerPC, replacing the previous powerpc/TargetPrinter.ml implementation.

Branch relaxation is not currently implemented for the other CompCert targets:

• RISC-V: the assembler does it automatically for us;
• x86: conditional branches can have offsets of 8, 16 or 32 bits, just like unconditional jumps, and the assembler chooses which one to use. With such large offsets, overflow should never occur.
• ARM: all jumps (conditional or not) have offsets up to 24 bits, which is pretty big. Plus, relaxation is not obvious to implement, since unconditional jumps do not have larger displacements than conditional branches.

[jhjourdan]

Should we make an internship offer to make a formal proof of the fixpoint algorithm? This does not look so difficult but still interesting.

[xavierleroy]

There might be a verified branch relaxation pass in CakeML. See also https://arxiv.org/abs/1209.5920 .