Correctness proof for constant propagation.
).
We now show that the transformed code after constant propagation
has the same semantics as the original code.
The proof of semantic preservation is a simulation argument
based on "option" diagrams of the following form:
n
st1 --------------- st2
| |
t| |t or (? and n' < n)
| |
v v
st1'--------------- st2'
n'
The left vertical arrow represents a transition in the
original RTL code. The top horizontal bar is the
match_states
invariant between the initial state
st1 in the original RTL code
and an initial state
st2 in the transformed code.
This invariant expresses that all code fragments appearing in
st2
are obtained by
transf_code transformation of the corresponding
fragments in
st1. Moreover, the state
st1 must match its compile-time
approximations at the current program point.
These two parts of the diagram are the hypotheses. In conclusions,
we want to prove the other two parts: the right vertical arrow,
which is a transition in the transformed RTL code, and the bottom
horizontal bar, which means that the
match_state predicate holds
between the final states
st1' and
st2'.
The proof of simulation proceeds by case analysis on the transition
taken in the source code.
The preservation of the observable behavior of the program then
follows.