Correctness proof for x86-64 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.
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 (
fn_code tf) <=
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 Asm
preserves labels, in the sense that the following diagram commutes:
translation
Mach code ------------------------ Asm instr sequence
| |
| Mach.find_label lbl find_label lbl |
| |
v v
Mach code tail ------------------- Asm instr seq tail
translation
The proof demands many boring lemmas showing that Asm constructor
functions do not introduce new labels.
In passing, we also prove a "is tail" property of the generated Asm code.
.
Remark mk_mov_label:
forall rd rs k c,
mk_mov rd rs k =
OK c ->
tail_nolabel k c.
Proof.
unfold mk_mov;
intros.
destruct rd;
try discriminate;
destruct rs;
TailNoLabel.
Qed.
Hint Resolve mk_mov_label:
labels.
Remark mk_shrximm_label:
forall n k c,
mk_shrximm n k =
OK c ->
tail_nolabel k c.
Proof.
intros. monadInv H; TailNoLabel.
Qed.
Hint Resolve mk_shrximm_label:
labels.
Remark mk_shrxlimm_label:
forall n k c,
mk_shrxlimm n k =
OK c ->
tail_nolabel k c.
Proof.
Hint Resolve mk_shrxlimm_label:
labels.
Remark mk_intconv_label:
forall f r1 r2 k c,
mk_intconv f r1 r2 k =
OK c ->
(
forall r r',
nolabel (
f r r')) ->
tail_nolabel k c.
Proof.
Hint Resolve mk_intconv_label:
labels.
Remark mk_storebyte_label:
forall addr r k c,
mk_storebyte addr r k =
OK c ->
tail_nolabel k c.
Proof.
Hint Resolve mk_storebyte_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.
unfold loadind;
intros.
destruct ty;
try discriminate;
destruct (
preg_of dst);
TailNoLabel.
Qed.
Remark storeind_label:
forall base ofs ty src k c,
storeind src base ofs ty k =
OK c ->
tail_nolabel k c.
Proof.
unfold storeind;
intros.
destruct ty;
try discriminate;
destruct (
preg_of src);
TailNoLabel.
Qed.
Remark mk_setcc_base_label:
forall xc rd k,
tail_nolabel k (
mk_setcc_base xc rd k).
Proof.
intros.
destruct xc;
simpl;
destruct (
ireg_eq rd RAX);
TailNoLabel.
Qed.
Remark mk_setcc_label:
forall xc rd k,
tail_nolabel k (
mk_setcc xc rd k).
Proof.
Remark mk_jcc_label:
forall xc lbl'
k,
tail_nolabel k (
mk_jcc xc lbl'
k).
Proof.
intros. destruct xc; simpl; TailNoLabel.
Qed.
Remark mk_sel_label:
forall xc rd r2 k c,
mk_sel xc rd r2 k =
OK c ->
tail_nolabel k c.
Proof.
unfold mk_sel;
intros;
destruct xc;
inv H;
TailNoLabel.
Qed.
Remark transl_cond_label:
forall cond args k c,
transl_cond cond args k =
OK c ->
tail_nolabel k c.
Proof.
unfold transl_cond;
intros.
destruct cond;
TailNoLabel.
destruct (
Int.eq_dec n Int.zero);
TailNoLabel.
destruct (
Int64.eq_dec n Int64.zero);
TailNoLabel.
destruct c0;
simpl;
TailNoLabel.
destruct c0;
simpl;
TailNoLabel.
destruct c0;
simpl;
TailNoLabel.
destruct c0;
simpl;
TailNoLabel.
Qed.
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_load_label:
forall chunk addr args dest k c,
transl_load chunk addr args dest k =
OK c ->
tail_nolabel k c.
Proof.
intros. monadInv H. destruct chunk; TailNoLabel.
Qed.
Remark transl_store_label:
forall chunk addr args src k c,
transl_store chunk addr args src k =
OK c ->
tail_nolabel k c.
Proof.
intros. monadInv H. destruct chunk; TailNoLabel.
Qed.
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)
(
AXP:
ep =
true ->
rs#
RAX =
parent_sp 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 ->
(
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#
RAX =
parent_sp s)) ->
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 H7.
exploit H3;
eauto.
intros [
rs2 [
A [
B C]]].
exists (
State rs2 m2');
split.
eapply exec_straight_exec;
eauto.
econstructor;
eauto.
eapply exec_straight_at;
eauto.
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 ->
(
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') ->
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 Asm transition, except the
transition from Mach.Returnstate to Mach.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.
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'),
(
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.
assert (
r0 =
AX).
{
unfold loc_result in H1;
destruct Archi.ptr64;
compute in H1;
congruence. }
subst r0.
generalize (
preg_val _ _ _ AX 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.