Correctness proof for the branch tunneling optimization.
The proof of semantic preservation is a simulation argument
based on diagrams of the following form:
st1 --------------- st2
| |
t| ?|t
| |
v v
st1'--------------- st2'
The
match_states predicate, defined below, captures the precondition
between states
st1 and
st2, as well as the postcondition between
st1' and
st2'. One transition in the source code (left) can correspond
to zero or one transition in the transformed code (right). The
"zero transition" case occurs when executing a
Lnop instruction
in the source code that has been removed by tunneling.
In the definition of
match_states, what changes between the original and
transformed codes is mainly the control-flow
(in particular, the current program point
pc), but also some values
and memory states, since some
Vundef values can become more defined
as a consequence of eliminating useless
Lcond instructions.
To preserve non-terminating behaviours, we show that the transformed
code cannot take an infinity of "zero transition" cases.
We use the following measure function over source states,
which decreases strictly in the "zero transition" case.