Correctness proof for PPC generation: main proof.
Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Mach Conventions Asm.
Require Import Asmgen Asmgenproof0 Asmgenproof1.
Local Transparent Archi.ptr64.
Definition match_prog (
p:
Mach.program) (
tp:
Asm.program) :=
match_program (
fun _ f tf =>
transf_fundef f =
OK tf)
eq p tp.
Lemma transf_program_match:
forall p tp,
transf_program p =
OK tp ->
match_prog p tp.
Proof.
Section PRESERVATION.
Variable prog:
Mach.program.
Variable tprog:
Asm.program.
Hypothesis TRANSF:
match_prog prog tprog.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_match TRANSF).
Lemma senv_preserved:
Senv.equiv ge tge.
Proof (
Genv.senv_match TRANSF).
Lemma functions_translated:
forall b f,
Genv.find_funct_ptr ge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf /\
transf_fundef f =
OK tf.
Proof (
Genv.find_funct_ptr_transf_partial TRANSF).
Lemma functions_transl:
forall fb f tf,
Genv.find_funct_ptr ge fb =
Some (
Internal f) ->
transf_function f =
OK tf ->
Genv.find_funct_ptr tge fb =
Some (
Internal tf).
Proof.
intros.
exploit functions_translated;
eauto.
intros [
tf' [
A B]].
monadInv B.
rewrite H0 in EQ;
inv EQ;
auto.
Qed.
Properties of control flow
Lemma transf_function_no_overflow:
forall f tf,
transf_function f =
OK tf ->
list_length_z tf.(
fn_code) <=
Ptrofs.max_unsigned.
Proof.
Lemma exec_straight_exec:
forall fb f c ep tf tc c'
rs m rs'
m',
transl_code_at_pc ge (
rs PC)
fb f c ep tf tc ->
exec_straight tge tf tc rs m c'
rs'
m' ->
plus step tge (
State rs m)
E0 (
State rs'
m').
Proof.
Lemma exec_straight_at:
forall fb f c ep tf tc c'
ep'
tc'
rs m rs'
m',
transl_code_at_pc ge (
rs PC)
fb f c ep tf tc ->
transl_code f c'
ep' =
OK tc' ->
exec_straight tge tf tc rs m tc'
rs'
m' ->
transl_code_at_pc ge (
rs'
PC)
fb f c'
ep'
tf tc'.
Proof.
The following lemmas show that the translation from Mach to PPC
preserves labels, in the sense that the following diagram commutes:
translation
Mach code ------------------------ PPC instr sequence
| |
| Mach.find_label lbl find_label lbl |
| |
v v
Mach code tail ------------------- PPC instr seq tail
translation
The proof demands many boring lemmas showing that PPC constructor
functions do not introduce new labels.
.
Remark loadimm_label:
forall r n k,
tail_nolabel k (
loadimm r n k).
Proof.
Hint Resolve loadimm_label:
labels.
Remark addimm_label:
forall r1 r2 n k,
tail_nolabel k (
addimm r1 r2 n k).
Proof.
Hint Resolve addimm_label:
labels.
Remark andimm_base_label:
forall r1 r2 n k,
tail_nolabel k (
andimm_base r1 r2 n k).
Proof.
Hint Resolve andimm_base_label:
labels.
Remark andimm_label:
forall r1 r2 n k,
tail_nolabel k (
andimm r1 r2 n k).
Proof.
Hint Resolve andimm_label:
labels.
Remark orimm_label:
forall r1 r2 n k,
tail_nolabel k (
orimm r1 r2 n k).
Proof.
Hint Resolve orimm_label:
labels.
Remark xorimm_label:
forall r1 r2 n k,
tail_nolabel k (
xorimm r1 r2 n k).
Proof.
Hint Resolve xorimm_label:
labels.
Remark rolm_label:
forall r1 r2 amount mask k,
tail_nolabel k (
rolm r1 r2 amount mask k).
Proof.
Hint Resolve rolm_label:
labels.
Remark loadimm64_32s_label:
forall r n k,
tail_nolabel k (
loadimm64_32s r n k).
Proof.
Hint Resolve loadimm64_32s_label:
labels.
Remark loadimm64_label:
forall r n k,
tail_nolabel k (
loadimm64 r n k).
Proof.
Hint Resolve loadimm64_label:
labels.
Remark loadimm64_notemp_label:
forall r n k,
tail_nolabel k (
loadimm64_notemp r n k).
Proof.
Hint Resolve loadimm64_notemp_label:
labels.
Remark loadind_label:
forall base ofs ty dst k c,
loadind base ofs ty dst k =
OK c ->
tail_nolabel k c.
Proof.
Remark storeind_label:
forall base ofs ty src k c,
storeind src base ofs ty k =
OK c ->
tail_nolabel k c.
Proof.
Remark floatcomp_label:
forall cmp r1 r2 k,
tail_nolabel k (
floatcomp cmp r1 r2 k).
Proof.
intros;
unfold floatcomp.
destruct cmp;
TailNoLabel.
Qed.
Hint Resolve floatcomp_label:
labels.
Remark transl_cond_label:
forall cond args k c,
transl_cond cond args k =
OK c ->
tail_nolabel k c.
Proof.
Remark transl_cond_op_label:
forall cond args r k c,
transl_cond_op cond args r k =
OK c ->
tail_nolabel k c.
Proof.
Remark transl_select_op_label:
forall cond args r1 r2 rd k c,
transl_select_op cond args r1 r2 rd k =
OK c ->
tail_nolabel k c.
Proof.
Remark transl_fselect_op_label:
forall cond args r1 r2 rd k c,
transl_fselect_op cond args r1 r2 rd k =
OK c ->
tail_nolabel k c.
Proof.
Remark transl_op_label:
forall op args r k c,
transl_op op args r k =
OK c ->
tail_nolabel k c.
Proof.
Remark transl_memory_access_label:
forall (
mk1:
constant ->
ireg ->
instruction) (
mk2:
ireg ->
ireg ->
instruction)
unaligned addr args temp k c,
transl_memory_access mk1 mk2 unaligned addr args temp k =
OK c ->
(
forall c r,
nolabel (
mk1 c r)) ->
(
forall r1 r2,
nolabel (
mk2 r1 r2)) ->
tail_nolabel k c.
Proof.
Remark transl_epilogue_label:
forall f k,
tail_nolabel k (
transl_epilogue f k).
Proof.
Lemma transl_instr_label:
forall f i ep k c,
transl_instr f i ep k =
OK c ->
match i with Mlabel lbl =>
c =
Plabel lbl ::
k |
_ =>
tail_nolabel k c end.
Proof.
Lemma transl_instr_label':
forall lbl f i ep k c,
transl_instr f i ep k =
OK c ->
find_label lbl c =
if Mach.is_label lbl i then Some k else find_label lbl k.
Proof.
intros.
exploit transl_instr_label;
eauto.
destruct i;
try (
intros [
A B];
apply B).
intros.
subst c.
simpl.
auto.
Qed.
Lemma transl_code_label:
forall lbl f c ep tc,
transl_code f c ep =
OK tc ->
match Mach.find_label lbl c with
|
None =>
find_label lbl tc =
None
|
Some c' =>
exists tc',
find_label lbl tc =
Some tc' /\
transl_code f c'
false =
OK tc'
end.
Proof.
induction c;
simpl;
intros.
inv H.
auto.
monadInv H.
rewrite (
transl_instr_label'
lbl _ _ _ _ _ EQ0).
generalize (
Mach.is_label_correct lbl a).
destruct (
Mach.is_label lbl a);
intros.
subst a.
simpl in EQ.
exists x;
auto.
eapply IHc;
eauto.
Qed.
Lemma transl_find_label:
forall lbl f tf,
transf_function f =
OK tf ->
match Mach.find_label lbl f.(
Mach.fn_code)
with
|
None =>
find_label lbl tf.(
fn_code) =
None
|
Some c =>
exists tc,
find_label lbl tf.(
fn_code) =
Some tc /\
transl_code f c false =
OK tc
end.
Proof.
End TRANSL_LABEL.
A valid branch in a piece of Mach code translates to a valid ``go to''
transition in the generated PPC code.
Lemma find_label_goto_label:
forall f tf lbl rs m c'
b ofs,
Genv.find_funct_ptr ge b =
Some (
Internal f) ->
transf_function f =
OK tf ->
rs PC =
Vptr b ofs ->
Mach.find_label lbl f.(
Mach.fn_code) =
Some c' ->
exists tc',
exists rs',
goto_label tf lbl rs m =
Next rs'
m
/\
transl_code_at_pc ge (
rs'
PC)
b f c'
false tf tc'
/\
forall r,
r <>
PC ->
rs'#
r =
rs#
r.
Proof.
Existence of return addresses
Lemma return_address_exists:
forall f sg ros c,
is_tail (
Mcall sg ros ::
c)
f.(
Mach.fn_code) ->
exists ra,
return_address_offset f c ra.
Proof.
Proof of semantic preservation
Semantic preservation is proved using simulation diagrams
of the following form.
st1 --------------- st2
| |
t| *|t
| |
v v
st1'--------------- st2'
The invariant is the
match_states predicate below, which includes:
-
The PPC code pointed by the PC register is the translation of
the current Mach code sequence.
-
Mach register values and PPC register values agree.
:
Mach.state ->
Asm.state ->
Prop :=
|
match_states_intro:
forall s fb sp c ep ms m m'
rs f tf tc
(
STACKS:
match_stack ge s)
(
FIND:
Genv.find_funct_ptr ge fb =
Some (
Internal f))
(
MEXT:
Mem.extends m m')
(
AT:
transl_code_at_pc ge (
rs PC)
fb f c ep tf tc)
(
AG:
agree ms sp rs)
(
DXP:
ep =
true ->
rs#
GPR11 =
parent_sp s)
(
LEAF:
is_leaf_function f =
true ->
rs#
LR =
parent_ra s),
match_states (
Mach.State s fb sp c ms m)
(
Asm.State rs m')
|
match_states_call:
forall s fb ms m m'
rs
(
STACKS:
match_stack ge s)
(
MEXT:
Mem.extends m m')
(
AG:
agree ms (
parent_sp s)
rs)
(
ATPC:
rs PC =
Vptr fb Ptrofs.zero)
(
ATLR:
rs RA =
parent_ra s),
match_states (
Mach.Callstate s fb ms m)
(
Asm.State rs m')
|
match_states_return:
forall s ms m m'
rs
(
STACKS:
match_stack ge s)
(
MEXT:
Mem.extends m m')
(
AG:
agree ms (
parent_sp s)
rs)
(
ATPC:
rs PC =
parent_ra s),
match_states (
Mach.Returnstate s ms m)
(
Asm.State rs m').
Lemma exec_straight_steps:
forall s fb f rs1 i c ep tf tc m1'
m2 m2'
sp ms2,
match_stack ge s ->
Mem.extends m2 m2' ->
Genv.find_funct_ptr ge fb =
Some (
Internal f) ->
transl_code_at_pc ge (
rs1 PC)
fb f (
i ::
c)
ep tf tc ->
(
is_leaf_function f =
true ->
rs1#
LR =
parent_ra s) ->
(
forall k c (
TR:
transl_instr f i ep k =
OK c),
exists rs2,
exec_straight tge tf c rs1 m1'
k rs2 m2'
/\
agree ms2 sp rs2
/\ (
it1_is_parent ep i =
true ->
rs2#
GPR11 =
parent_sp s)
/\
rs2#
LR =
rs1#
LR) ->
exists st',
plus step tge (
State rs1 m1')
E0 st' /\
match_states (
Mach.State s fb sp c ms2 m2)
st'.
Proof.
intros.
inversion H2.
subst.
monadInv H8.
exploit H4;
eauto.
intros (
rs2 &
A &
B &
C &
D).
exists (
State rs2 m2');
split.
eapply exec_straight_exec;
eauto.
econstructor;
eauto.
eapply exec_straight_at;
eauto.
rewrite D;
auto.
Qed.
Lemma exec_straight_steps_goto:
forall s fb f rs1 i c ep tf tc m1'
m2 m2'
sp ms2 lbl c',
match_stack ge s ->
Mem.extends m2 m2' ->
Genv.find_funct_ptr ge fb =
Some (
Internal f) ->
Mach.find_label lbl f.(
Mach.fn_code) =
Some c' ->
transl_code_at_pc ge (
rs1 PC)
fb f (
i ::
c)
ep tf tc ->
it1_is_parent ep i =
false ->
(
is_leaf_function f =
true ->
rs1#
LR =
parent_ra s) ->
(
forall k c (
TR:
transl_instr f i ep k =
OK c),
exists jmp,
exists k',
exists rs2,
exec_straight tge tf c rs1 m1' (
jmp ::
k')
rs2 m2'
/\
agree ms2 sp rs2
/\
exec_instr tge tf jmp rs2 m2' =
goto_label tf lbl rs2 m2'
/\
rs2#
LR =
rs1#
LR) ->
exists st',
plus step tge (
State rs1 m1')
E0 st' /\
match_states (
Mach.State s fb sp c'
ms2 m2)
st'.
Proof.
We need to show that, in the simulation diagram, we cannot
take infinitely many Mach transitions that correspond to zero
transitions on the PPC side. Actually, all Mach transitions
correspond to at least one PPC transition, except the
transition from Machsem.Returnstate to Machsem.State.
So, the following integer measure will suffice to rule out
the unwanted behaviour.
Definition measure (
s:
Mach.state) :
nat :=
match s with
|
Mach.State _ _ _ _ _ _ => 0%
nat
|
Mach.Callstate _ _ _ _ => 0%
nat
|
Mach.Returnstate _ _ _ => 1%
nat
end.
Remark preg_of_not_GPR11:
forall r,
negb (
mreg_eq r R11) =
true ->
IR GPR11 <>
preg_of r.
Proof.
This is the simulation diagram. We prove it by case analysis on the Mach transition.
Theorem step_simulation:
forall S1 t S2,
Mach.step return_address_offset ge S1 t S2 ->
forall S1' (
MS:
match_states S1 S1') (
WF:
wf_state ge S1),
(
exists S2',
plus step tge S1'
t S2' /\
match_states S2 S2')
\/ (
measure S2 <
measure S1 /\
t =
E0 /\
match_states S2 S1')%
nat.
Proof.
Lemma transf_initial_states:
forall st1,
Mach.initial_state prog st1 ->
exists st2,
Asm.initial_state tprog st2 /\
match_states st1 st2.
Proof.
Lemma transf_final_states:
forall st1 st2 r,
match_states st1 st2 ->
Mach.final_state st1 r ->
Asm.final_state st2 r.
Proof.
intros.
inv H0.
inv H.
constructor.
auto.
compute in H1.
inv H1.
generalize (
preg_val _ _ _ R3 AG).
rewrite H2.
intros LD;
inv LD.
auto.
Qed.
Theorem transf_program_correct:
forward_simulation (
Mach.semantics return_address_offset prog) (
Asm.semantics tprog).
Proof.
End PRESERVATION.