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.
For example:
L1: if (cond) nop L2; L1: nop L3;
L2: nop L3; becomes L2: nop L3;
L3: instr; L3: instr;
L4: if (cond) goto L1; L4: if (cond) nop L1;
This optimization can be applied to several of our intermediate
languages. We choose to perform it on the
LTL language,
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
branch instructions are
dead code (as the "branch L3" in the example above).
The implementation consists in two passes: the first pass
records the branch t of each "nop"
and the second pass replace any "nop" node to
pc
by a branch to a "nop" at
branch_t f pc
Naively, we may define
branch_t f pc as follows:
branch_t f pc = branch_t 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: branch L1;
or
L1: nop L2;
L2: nop L1;
Coq warns us of this fact by not accepting the definition
of
branch_t above.
To handle this problem, we use a union-find data structure, adding equalities
pc = pc'
for every instruction
pc: nop pc' in the function.
Moreover, because the elimination of "useless"
Lcond depends on the current
uf datastructure,
we need to iterate until we reach a fixpoint.
Actually, it is simpler and more efficient to perform this in an external oracle, that also returns a measure
in order to help the proof.
A verifier checks that this data-structure is correct.
.
).