Branch tunneling (optimization of branches to branches).
Branch tunneling shortens sequences of branches (with no intervening
computations) by rewriting the branch and conditional branch instructions
so that they jump directly to the end of the branch sequence.
L1: nop L2; L1: nop L3;
L2; nop L3; becomes L2: nop L3;
L3: instr; L3: instr;
L4: if (cond) goto L1; L4: if (cond) goto L3;
This optimization can be applied to several of our intermediate
languages. We choose to perform it on the LTL
after register allocation but before code linearization.
Register allocation can delete instructions (such as dead
computations or useless moves), therefore there are more
opportunities for tunneling after allocation than before.
Symmetrically, prior tunneling helps linearization to produce
better code, e.g. by revealing that some nop
dead code (as the "nop L3" in the example above).
The naive implementation of branch tunneling would replace
any branch to a node pc
by a branch to the node
branch_target f pc
, defined as follows:
branch_target f pc = branch_target f pc' if f(pc) = nop pc'
= pc otherwise
However, this definition can fail to terminate if
the program can contain loops consisting only of branches, as in
L1: nop L1;
<< L1: nop L2;
L2: nop L1;
Coq warns us of this fact by not accepting the definition
To handle this problem, we proceed in two passes. The first pass
populates a union-find data structure, adding equalities pc = pc'
for every instruction pc: nop pc'
in the function.