Correctness proof for common subexpression elimination.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Errors.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import Kildall.
Require Import ValueDomain.
Require Import ValueAOp.
Require Import ValueAnalysis.
Require Import CSEdomain.
Require Import CombineOp.
Require Import CombineOpproof.
Require Import CSE2.
Soundness of operations over value numberings
Remark wf_equation_incr:
forall next1 next2 e,
wf_equation next1 e ->
Ple next1 next2 ->
wf_equation next2 e.
Proof.
Extensionality with respect to valuations.
Definition valu_agree (
valu1 valu2:
valuation) (
upto:
valnum) :=
forall v,
Plt v upto ->
valu2 v =
valu1 v.
Section EXTEN.
Variable valu1:
valuation.
Variable upto:
valnum.
Variable valu2:
valuation.
Hypothesis AGREE:
valu_agree valu1 valu2 upto.
Variable ge:
genv.
Variable sp:
val.
Variable rs:
regset.
Variable m:
mem.
Lemma valnums_val_exten:
forall vl,
(
forall v,
In v vl ->
Plt v upto) ->
map valu2 vl =
map valu1 vl.
Proof.
Lemma rhs_eval_to_exten:
forall r v,
rhs_eval_to valu1 ge sp m r v ->
(
forall v,
In v (
valnums_rhs r) ->
Plt v upto) ->
rhs_eval_to valu2 ge sp m r v.
Proof.
Lemma equation_holds_exten:
forall e,
equation_holds valu1 ge sp m e ->
wf_equation upto e ->
equation_holds valu2 ge sp m e.
Proof.
Lemma numbering_holds_exten:
forall n,
numbering_holds valu1 ge sp rs m n ->
Ple n.(
num_next)
upto ->
numbering_holds valu2 ge sp rs m n.
Proof.
End EXTEN.
Ltac splitall :=
repeat (
match goal with |-
_ /\
_ =>
split end).
Lemma valnum_reg_holds:
forall valu1 ge sp rs m n r n'
v,
numbering_holds valu1 ge sp rs m n ->
valnum_reg n r = (
n',
v) ->
exists valu2,
numbering_holds valu2 ge sp rs m n'
/\
rs#
r =
valu2 v
/\
valu_agree valu1 valu2 n.(
num_next)
/\
Plt v n'.(
num_next)
/\
Ple n.(
num_next)
n'.(
num_next).
Proof.
Lemma valnum_regs_holds:
forall rl valu1 ge sp rs m n n'
vl,
numbering_holds valu1 ge sp rs m n ->
valnum_regs n rl = (
n',
vl) ->
exists valu2,
numbering_holds valu2 ge sp rs m n'
/\
rs##
rl =
map valu2 vl
/\
valu_agree valu1 valu2 n.(
num_next)
/\ (
forall v,
In v vl ->
Plt v n'.(
num_next))
/\
Ple n.(
num_next)
n'.(
num_next).
Proof.
induction rl;
simpl;
intros.
-
inv H0.
exists valu1;
splitall;
auto.
red;
auto.
simpl;
tauto.
xomega.
-
destruct (
valnum_reg n a)
as [
n1 v1]
eqn:
V1.
destruct (
valnum_regs n1 rl)
as [
n2 vs]
eqn:
V2.
inv H0.
exploit valnum_reg_holds;
eauto.
intros (
valu2 &
A &
B &
C &
D &
E).
exploit (
IHrl valu2);
eauto.
intros (
valu3 &
P &
Q &
R &
S &
T).
exists valu3;
splitall.
+
auto.
+
simpl;
f_equal;
auto.
rewrite R;
auto.
+
red;
intros.
transitivity (
valu2 v);
auto.
apply R.
xomega.
+
simpl;
intros.
destruct H0;
auto.
subst v1;
xomega.
+
xomega.
Qed.
Lemma find_valnum_rhs_charact:
forall rh v eqs,
find_valnum_rhs rh eqs =
Some v ->
In (
Eq v true rh)
eqs.
Proof.
induction eqs;
simpl;
intros.
-
inv H.
-
destruct a.
destruct (
strict &&
eq_rhs rh r)
eqn:
T.
+
InvBooleans.
inv H.
left;
auto.
+
right;
eauto.
Qed.
Lemma find_valnum_rhs'
_charact:
forall rh v eqs,
find_valnum_rhs'
rh eqs =
Some v ->
exists strict,
In (
Eq v strict rh)
eqs.
Proof.
induction eqs;
simpl;
intros.
-
inv H.
-
destruct a.
destruct (
eq_rhs rh r)
eqn:
T.
+
inv H.
exists strict;
auto.
+
exploit IHeqs;
eauto.
intros [
s IN].
exists s;
auto.
Qed.
Lemma find_valnum_num_charact:
forall v r eqs,
find_valnum_num v eqs =
Some r ->
In (
Eq v true r)
eqs.
Proof.
induction eqs;
simpl;
intros.
-
inv H.
-
destruct a.
destruct (
strict &&
peq v v0)
eqn:
T.
+
InvBooleans.
inv H.
auto.
+
eauto.
Qed.
Lemma reg_valnum_sound:
forall n v r valu ge sp rs m,
reg_valnum n v =
Some r ->
numbering_holds valu ge sp rs m n ->
rs#
r =
valu v.
Proof.
Lemma regs_valnums_sound:
forall n valu ge sp rs m,
numbering_holds valu ge sp rs m n ->
forall vl rl,
regs_valnums n vl =
Some rl ->
rs##
rl =
map valu vl.
Proof.
induction vl;
simpl;
intros.
-
inv H0;
auto.
-
destruct (
reg_valnum n a)
as [
r1|]
eqn:
RV1;
try discriminate.
destruct (
regs_valnums n vl)
as [
rl1|]
eqn:
RVL;
inv H0.
simpl;
f_equal.
eapply reg_valnum_sound;
eauto.
eauto.
Qed.
Lemma find_rhs_sound:
forall n rh r valu ge sp rs m,
find_rhs n rh =
Some r ->
numbering_holds valu ge sp rs m n ->
exists v,
rhs_eval_to valu ge sp m rh v /\
Val.lessdef v rs#
r.
Proof.
unfold find_rhs;
intros.
destruct (
find_valnum_rhs'
rh (
num_eqs n))
as [
vres|]
eqn:
E;
try discriminate.
exploit find_valnum_rhs'
_charact;
eauto.
intros [
strict IN].
erewrite reg_valnum_sound by eauto.
exploit num_holds_eq;
eauto.
intros EH.
inv EH.
-
exists (
valu vres);
auto.
-
exists v;
auto.
Qed.
Remark in_remove:
forall (
A:
Type) (
eq:
forall (
x y:
A), {
x=
y}+{
x<>
y})
x y l,
In y (
List.remove eq x l) <->
x <>
y /\
In y l.
Proof.
induction l; simpl.
tauto.
destruct (eq x a).
subst a. rewrite IHl. tauto.
simpl. rewrite IHl. intuition congruence.
Qed.
Lemma forget_reg_charact:
forall n rd r v,
wf_numbering n ->
In r (
PMap.get v (
forget_reg n rd)) ->
r <>
rd /\
In r (
PMap.get v n.(
num_val)).
Proof.
Lemma update_reg_charact:
forall n rd vd r v,
wf_numbering n ->
In r (
PMap.get v (
update_reg n rd vd)) ->
PTree.get r (
PTree.set rd vd n.(
num_reg)) =
Some v.
Proof.
Lemma rhs_eval_to_inj:
forall valu ge sp m rh v1 v2,
rhs_eval_to valu ge sp m rh v1 ->
rhs_eval_to valu ge sp m rh v2 ->
v1 =
v2.
Proof.
intros. inv H; inv H0; congruence.
Qed.
Lemma add_rhs_holds:
forall valu1 ge sp rs m n rd rh rs',
numbering_holds valu1 ge sp rs m n ->
rhs_eval_to valu1 ge sp m rh (
rs'#
rd) ->
wf_rhs n.(
num_next)
rh ->
(
forall r,
r <>
rd ->
rs'#
r =
rs#
r) ->
exists valu2,
numbering_holds valu2 ge sp rs'
m (
add_rhs n rd rh).
Proof.
Lemma add_op_holds:
forall valu1 ge sp rs m n op (
args:
list reg)
v dst,
numbering_holds valu1 ge sp rs m n ->
eval_operation ge sp op rs##
args m =
Some v ->
exists valu2,
numbering_holds valu2 ge sp (
rs#
dst <-
v)
m (
add_op n dst op args).
Proof.
Lemma add_load_holds:
forall valu1 ge sp rs m n addr (
args:
list reg)
a chunk v dst,
numbering_holds valu1 ge sp rs m n ->
eval_addressing ge sp addr rs##
args =
Some a ->
Mem.loadv chunk m a =
Some v ->
exists valu2,
numbering_holds valu2 ge sp (
rs#
dst <-
v)
m (
add_load n dst chunk addr args).
Proof.
Lemma set_unknown_holds:
forall valu ge sp rs m n r v,
numbering_holds valu ge sp rs m n ->
numbering_holds valu ge sp (
rs#
r <-
v)
m (
set_unknown n r).
Proof.
Lemma set_res_unknown_holds:
forall valu ge sp rs m n r v,
numbering_holds valu ge sp rs m n ->
numbering_holds valu ge sp (
regmap_setres r v rs)
m (
set_res_unknown n r).
Proof.
Lemma kill_eqs_charact:
forall pred l strict r eqs,
In (
Eq l strict r) (
kill_eqs pred eqs) ->
pred r =
false /\
In (
Eq l strict r)
eqs.
Proof.
induction eqs; simpl; intros.
- tauto.
- destruct a. destruct (pred r0) eqn:PRED.
tauto.
inv H. inv H0. auto. tauto.
Qed.
Lemma kill_equations_hold:
forall valu ge sp rs m n pred m',
numbering_holds valu ge sp rs m n ->
(
forall r v,
pred r =
false ->
rhs_eval_to valu ge sp m r v ->
rhs_eval_to valu ge sp m'
r v) ->
numbering_holds valu ge sp rs m' (
kill_equations pred n).
Proof.
intros;
constructor;
simpl;
intros.
-
constructor;
simpl;
intros;
eauto with cse.
destruct e.
exploit kill_eqs_charact;
eauto.
intros [
A B].
eauto with cse.
-
destruct eq.
exploit kill_eqs_charact;
eauto.
intros [
A B].
exploit num_holds_eq;
eauto.
intro EH;
inv EH;
econstructor;
eauto.
-
eauto with cse.
Qed.
Lemma kill_all_loads_hold:
forall valu ge sp rs m n m',
numbering_holds valu ge sp rs m n ->
numbering_holds valu ge sp rs m' (
kill_all_loads n).
Proof.
Lemma kill_loads_after_store_holds:
forall valu ge sp rs m n addr args a chunk v m'
bc approx ae am,
numbering_holds valu ge (
Vptr sp Int.zero)
rs m n ->
eval_addressing ge (
Vptr sp Int.zero)
addr rs##
args =
Some a ->
Mem.storev chunk m a v =
Some m' ->
genv_match bc ge ->
bc sp =
BCstack ->
ematch bc rs ae ->
approx =
VA.State ae am ->
numbering_holds valu ge (
Vptr sp Int.zero)
rs m'
(
kill_loads_after_store approx n chunk addr args).
Proof.
Lemma store_normalized_range_sound:
forall bc chunk v,
vmatch bc v (
store_normalized_range chunk) ->
Val.lessdef (
Val.load_result chunk v)
v.
Proof.
intros.
destruct chunk;
simpl in *;
destruct v;
auto.
-
inv H.
rewrite is_sgn_sign_ext in H4 by omega.
rewrite H4;
auto.
-
inv H.
rewrite is_uns_zero_ext in H4 by omega.
rewrite H4;
auto.
-
inv H.
rewrite is_sgn_sign_ext in H4 by omega.
rewrite H4;
auto.
-
inv H.
rewrite is_uns_zero_ext in H4 by omega.
rewrite H4;
auto.
Qed.
Lemma add_store_result_hold:
forall valu1 ge sp rs m'
n addr args a chunk m src bc ae approx am,
numbering_holds valu1 ge sp rs m'
n ->
eval_addressing ge sp addr rs##
args =
Some a ->
Mem.storev chunk m a rs#
src =
Some m' ->
ematch bc rs ae ->
approx =
VA.State ae am ->
exists valu2,
numbering_holds valu2 ge sp rs m' (
add_store_result approx n chunk addr args src).
Proof.
Lemma kill_loads_after_storebytes_holds:
forall valu ge sp rs m n dst b ofs bytes m'
bc approx ae am sz,
numbering_holds valu ge (
Vptr sp Int.zero)
rs m n ->
pmatch bc b ofs dst ->
Mem.storebytes m b (
Int.unsigned ofs)
bytes =
Some m' ->
genv_match bc ge ->
bc sp =
BCstack ->
ematch bc rs ae ->
approx =
VA.State ae am ->
length bytes =
nat_of_Z sz ->
sz >= 0 ->
numbering_holds valu ge (
Vptr sp Int.zero)
rs m'
(
kill_loads_after_storebytes approx n dst sz).
Proof.
Lemma load_memcpy:
forall m b1 ofs1 sz bytes b2 ofs2 m'
chunk i v,
Mem.loadbytes m b1 ofs1 sz =
Some bytes ->
Mem.storebytes m b2 ofs2 bytes =
Some m' ->
Mem.load chunk m b1 i =
Some v ->
ofs1 <=
i ->
i +
size_chunk chunk <=
ofs1 +
sz ->
(
align_chunk chunk |
ofs2 -
ofs1) ->
Mem.load chunk m'
b2 (
i + (
ofs2 -
ofs1)) =
Some v.
Proof.
Lemma shift_memcpy_eq_wf:
forall src sz delta e e'
next,
shift_memcpy_eq src sz delta e =
Some e' ->
wf_equation next e ->
wf_equation next e'.
Proof with
Lemma shift_memcpy_eq_holds:
forall src dst sz e e'
m sp bytes m'
valu ge,
shift_memcpy_eq src sz (
dst -
src)
e =
Some e' ->
Mem.loadbytes m sp src sz =
Some bytes ->
Mem.storebytes m sp dst bytes =
Some m' ->
equation_holds valu ge (
Vptr sp Int.zero)
m e ->
equation_holds valu ge (
Vptr sp Int.zero)
m'
e'.
Proof with
Lemma add_memcpy_eqs_charact:
forall e'
src sz delta eqs2 eqs1,
In e' (
add_memcpy_eqs src sz delta eqs1 eqs2) ->
In e'
eqs2 \/
exists e,
In e eqs1 /\
shift_memcpy_eq src sz delta e =
Some e'.
Proof.
induction eqs1;
simpl;
intros.
-
auto.
-
destruct (
shift_memcpy_eq src sz delta a)
as [
e''|]
eqn:
SHIFT.
+
destruct H.
subst e''.
right;
exists a;
auto.
destruct IHeqs1 as [
A | [
e [
A B]]];
auto.
right;
exists e;
auto.
+
destruct IHeqs1 as [
A | [
e [
A B]]];
auto.
right;
exists e;
auto.
Qed.
Lemma add_memcpy_holds:
forall m bsrc osrc sz bytes bdst odst m'
valu ge sp rs n1 n2 bc asrc adst,
Mem.loadbytes m bsrc (
Int.unsigned osrc)
sz =
Some bytes ->
Mem.storebytes m bdst (
Int.unsigned odst)
bytes =
Some m' ->
numbering_holds valu ge (
Vptr sp Int.zero)
rs m n1 ->
numbering_holds valu ge (
Vptr sp Int.zero)
rs m'
n2 ->
pmatch bc bsrc osrc asrc ->
pmatch bc bdst odst adst ->
bc sp =
BCstack ->
Ple (
num_next n1) (
num_next n2) ->
numbering_holds valu ge (
Vptr sp Int.zero)
rs m' (
add_memcpy n1 n2 asrc adst sz).
Proof.
Correctness of operator reduction
Section REDUCE.
Variable A:
Type.
Variable f: (
valnum ->
option rhs) ->
A ->
list valnum ->
option (
A *
list valnum).
Variable V:
Type.
Variable ge:
genv.
Variable sp:
val.
Variable rs:
regset.
Variable m:
mem.
Variable sem:
A ->
list val ->
option V.
Hypothesis f_sound:
forall eqs valu op args op'
args',
(
forall v rhs,
eqs v =
Some rhs ->
rhs_eval_to valu ge sp m rhs (
valu v)) ->
f eqs op args =
Some(
op',
args') ->
sem op' (
map valu args') =
sem op (
map valu args).
Variable n:
numbering.
Variable valu:
valnum ->
val.
Hypothesis n_holds:
numbering_holds valu ge sp rs m n.
Lemma reduce_rec_sound:
forall niter op args op'
rl'
res,
reduce_rec A f n niter op args =
Some(
op',
rl') ->
sem op (
map valu args) =
Some res ->
sem op' (
rs##
rl') =
Some res.
Proof.
Lemma reduce_sound:
forall op rl vl op'
rl'
res,
reduce A f n op rl vl = (
op',
rl') ->
map valu vl =
rs##
rl ->
sem op rs##
rl =
Some res ->
sem op'
rs##
rl' =
Some res.
Proof.
End REDUCE.
The numberings associated to each instruction by the static analysis
are inductively satisfiable, in the following sense: the numbering
at the function entry point is satisfiable, and for any RTL execution
from pc to pc', satisfiability at pc implies
satisfiability at pc'.
Theorem analysis_correct_1:
forall ge sp rs m STK SIZE f vapprox approx pc pc'
i,
analyze STK SIZE f vapprox =
Some approx ->
f.(
fn_code)!
pc =
Some i ->
In pc' (
successors_instr i) ->
(
exists valu,
numbering_holds valu ge sp rs m (
transfer STK SIZE f vapprox pc approx!!
pc)) ->
(
exists valu,
numbering_holds valu ge sp rs m approx!!
pc').
Proof.
Theorem analysis_correct_entry:
forall ge sp rs m STK SIZE f vapprox approx,
analyze STK SIZE f vapprox =
Some approx ->
exists valu,
numbering_holds valu ge sp rs m approx!!(
f.(
fn_entrypoint)).
Proof.
Semantic preservation
Section PRESERVATION.
Variable prog:
program.
Variable tprog :
program.
Hypothesis TRANSF:
transf_program prog =
OK tprog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Let rm :=
romem_for_program prog.
Let STK :=
match List.rev prog.(
prog_defs)
with
| (
SIZE,
Gvar SIZE_globvar)::(
STK,
Gvar STK_globvar)::
_ =>
STK
|
_ =>
xH
end.
Let SIZE :=
match List.rev prog.(
prog_defs)
with
| (
SIZE,
Gvar SIZE_globvar)::(
STK,
Gvar STK_globvar)::
_ =>
SIZE
|
_ =>
xH
end.
Lemma TRANSF':
transform_partial_program (
transf_fundef STK SIZE rm)
prog =
OK tprog.
Proof.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_transf_partial (
transf_fundef _ _ rm)
prog TRANSF').
Lemma public_preserved:
forall (
s:
ident),
Genv.public_symbol tge s =
Genv.public_symbol ge s.
Proof (
Genv.public_symbol_transf_partial (
transf_fundef _ _ rm)
prog TRANSF').
Lemma varinfo_preserved:
forall b,
Genv.find_var_info tge b =
Genv.find_var_info ge b.
Proof (
Genv.find_var_info_transf_partial (
transf_fundef _ _ rm)
prog TRANSF').
Lemma functions_translated:
forall (
v:
val) (
f:
RTL.fundef),
Genv.find_funct ge v =
Some f ->
exists tf,
Genv.find_funct tge v =
Some tf /\
transf_fundef STK SIZE rm f =
OK tf.
Proof (
Genv.find_funct_transf_partial (
transf_fundef _ _ rm)
prog TRANSF').
Lemma funct_ptr_translated:
forall (
b:
block) (
f:
RTL.fundef),
Genv.find_funct_ptr ge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf /\
transf_fundef STK SIZE rm f =
OK tf.
Proof (
Genv.find_funct_ptr_transf_partial (
transf_fundef _ _ rm)
prog TRANSF').
Lemma sig_preserved:
forall f tf,
transf_fundef STK SIZE rm f =
OK tf ->
funsig tf =
funsig f.
Proof.
Definition transf_function' (
f:
function) (
approxs:
PMap.t numbering) :
function :=
mkfunction
f.(
fn_sig)
f.(
fn_params)
f.(
fn_stacksize)
(
transf_code STK SIZE approxs f.(
fn_code))
f.(
fn_entrypoint).
Definition regs_lessdef (
rs1 rs2:
regset) :
Prop :=
forall r,
Val.lessdef (
rs1#
r) (
rs2#
r).
Lemma regs_lessdef_regs:
forall rs1 rs2,
regs_lessdef rs1 rs2 ->
forall rl,
Val.lessdef_list rs1##
rl rs2##
rl.
Proof.
induction rl; constructor; auto.
Qed.
Lemma set_reg_lessdef:
forall r v1 v2 rs1 rs2,
Val.lessdef v1 v2 ->
regs_lessdef rs1 rs2 ->
regs_lessdef (
rs1#
r <-
v1) (
rs2#
r <-
v2).
Proof.
intros;
red;
intros.
repeat rewrite Regmap.gsspec.
destruct (
peq r0 r);
auto.
Qed.
Lemma init_regs_lessdef:
forall rl vl1 vl2,
Val.lessdef_list vl1 vl2 ->
regs_lessdef (
init_regs vl1 rl) (
init_regs vl2 rl).
Proof.
Lemma find_function_translated:
forall ros rs fd rs',
find_function ge ros rs =
Some fd ->
regs_lessdef rs rs' ->
exists tfd,
find_function tge ros rs' =
Some tfd /\
transf_fundef STK SIZE rm fd =
OK tfd.
Proof.
The proof of semantic preservation is a simulation argument using
diagrams of the following form:
st1 --------------- st2
| |
t| |t
| |
v v
st1'--------------- st2'
Left: RTL execution in the original program. Right: RTL execution in
the optimized program. Precondition (top) and postcondition (bottom):
agreement between the states, including the fact that
the numbering at
pc (returned by the static analysis) is satisfiable.
:
list stackframe ->
list stackframe ->
Prop :=
|
match_stackframes_nil:
match_stackframes nil nil
|
match_stackframes_cons:
forall res sp pc rs f approx s rs'
s'
(
ANALYZE:
analyze STK SIZE f (
vanalyze rm f) =
Some approx)
(
SAT:
forall v m,
exists valu,
numbering_holds valu ge sp (
rs#
res <-
v)
m approx!!
pc)
(
RLD:
regs_lessdef rs rs')
(
STACKS:
match_stackframes s s'),
match_stackframes
(
Stackframe res f sp pc rs ::
s)
(
Stackframe res (
transf_function'
f approx)
sp pc rs' ::
s').
Inductive match_states:
state ->
state ->
Prop :=
|
match_states_intro:
forall s sp pc rs m s'
rs'
m'
f approx
(
ANALYZE:
analyze STK SIZE f (
vanalyze rm f) =
Some approx)
(
SAT:
exists valu,
numbering_holds valu ge sp rs m approx!!
pc)
(
RLD:
regs_lessdef rs rs')
(
MEXT:
Mem.extends m m')
(
STACKS:
match_stackframes s s'),
match_states (
State s f sp pc rs m)
(
State s' (
transf_function'
f approx)
sp pc rs'
m')
|
match_states_call:
forall s f tf args m s'
args'
m',
match_stackframes s s' ->
transf_fundef STK SIZE rm f =
OK tf ->
Val.lessdef_list args args' ->
Mem.extends m m' ->
match_states (
Callstate s f args m)
(
Callstate s'
tf args'
m')
|
match_states_return:
forall s s'
v v'
m m',
match_stackframes s s' ->
Val.lessdef v v' ->
Mem.extends m m' ->
match_states (
Returnstate s v m)
(
Returnstate s'
v'
m').
Ltac TransfInstr :=
match goal with
|
H1: (
PTree.get ?
pc ?
c =
Some ?
instr),
f:
function,
approx:
PMap.t numbering |-
_ =>
cut ((
transf_function'
f approx).(
fn_code)!
pc =
Some(
transf_instr STK SIZE approx!!
pc instr));
[
simpl transf_instr
|
unfold transf_function',
transf_code;
simpl;
rewrite PTree.gmap;
unfold option_map;
rewrite H1;
reflexivity ]
end.
The proof of simulation is a case analysis over the transition
in the source code.
Lemma transf_step_correct:
forall s1 t s2,
step ge s1 t s2 ->
forall s1' (
MS:
match_states s1 s1') (
SOUND:
sound_state prog s1),
exists s2',
step tge s1'
t s2' /\
match_states s2 s2'.
Proof.
Lemma transf_initial_states:
forall st1,
initial_state prog st1 ->
exists st2,
initial_state tprog st2 /\
match_states st1 st2.
Proof.
Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 ->
final_state st1 r ->
final_state st2 r.
Proof.
intros. inv H0. inv H. inv H5. inv H3. constructor.
Qed.
Theorem transf_program_correct:
forward_simulation (
RTL.semantics prog) (
RTL.semantics tprog).
Proof.
End PRESERVATION.