Correctness proof for the branch tunneling optimization.
Proof.
Proof.
Proof.
Proof.
Proof.
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
Lgoto instruction
in the source code that has been removed by tunneling.
In the definition of
match_states, note that only the control-flow
(in particular, the current program point
pc) is changed:
the values of locations and the memory states are identical in the
original and transformed codes.
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.
Proof.
Proof.
Proof.
Proof.
Proof.