Correctness proof for RISC-V 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.
Require Compopts.
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:
qualident),
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 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.
.
Remark loadimm32_label:
forall r n k,
tail_nolabel k (
loadimm32 r n k).
Proof.
Hint Resolve loadimm32_label:
labels.
Remark opimm32_label:
forall op opimm r1 r2 n k,
(
forall r1 r2 r3,
nolabel (
op r1 r2 r3)) ->
(
forall r1 r2 n,
nolabel (
opimm r1 r2 n)) ->
tail_nolabel k (
opimm32 op opimm r1 r2 n k).
Proof.
Hint Resolve opimm32_label:
labels.
Remark loadimm64_label:
forall r n k,
tail_nolabel k (
loadimm64 r n k).
Proof.
Hint Resolve loadimm64_label:
labels.
Remark opimm64_label:
forall op opimm r1 r2 n k,
(
forall r1 r2 r3,
nolabel (
op r1 r2 r3)) ->
(
forall r1 r2 n,
nolabel (
opimm r1 r2 n)) ->
tail_nolabel k (
opimm64 op opimm r1 r2 n k).
Proof.
Hint Resolve opimm64_label:
labels.
Remark addptrofs_label:
forall r1 r2 n k,
tail_nolabel k (
addptrofs r1 r2 n k).
Proof.
Hint Resolve addptrofs_label:
labels.
Remark transl_cond_float_nolabel:
forall c r1 r2 r3 insn normal,
transl_cond_float c r1 r2 r3 = (
insn,
normal) ->
nolabel insn.
Proof.
Remark transl_cond_single_nolabel:
forall c r1 r2 r3 insn normal,
transl_cond_single c r1 r2 r3 = (
insn,
normal) ->
nolabel insn.
Proof.
Remark transl_cbranch_label:
forall cond args lbl k c,
transl_cbranch cond args lbl k =
OK c ->
tail_nolabel k c.
Proof.
Remark transl_cond_op_label:
forall cond args r k c,
transl_cond_op cond r args 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 indexed_memory_access_label:
forall (
mk_instr:
ireg ->
offset ->
instruction)
base ofs k,
(
forall r o,
nolabel (
mk_instr r o)) ->
tail_nolabel k (
indexed_memory_access mk_instr base ofs k).
Proof.
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 src base ofs ty k c,
storeind src base ofs ty k =
OK c ->
tail_nolabel k c.
Proof.
Remark loadind_ptr_label:
forall base ofs dst k,
tail_nolabel k (
loadind_ptr base ofs dst k).
Proof.
Remark storeind_ptr_label:
forall src base ofs k,
tail_nolabel k (
storeind_ptr src base ofs k).
Proof.
Remark transl_memory_access_label:
forall (
mk_instr:
ireg ->
offset ->
instruction)
addr args k c,
(
forall r o,
nolabel (
mk_instr r o)) ->
transl_memory_access mk_instr addr args k =
OK c ->
tail_nolabel k c.
Proof.
Remark make_epilogue_label:
forall f k,
tail_nolabel k (
make_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 Asm 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 Asm code pointed by the PC register is the translation of
the current Mach code sequence.
-
Mach register values and Asm 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#
X30 =
parent_sp s)
(
LEAF:
Compopts.optim_leaf tt &&
is_leaf_function f =
true ->
rs#
RA =
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 ->
forall (
LEAF :
Compopts.optim_leaf tt &&
is_leaf_function f =
true ->
rs1#
RA =
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#
X30 =
parent_sp s)
/\
rs2#
RA =
rs1#
RA) ->
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 D]]]].
exists (
State rs2 m2');
split.
{
eapply exec_straight_exec;
eauto. }
econstructor;
eauto.
{
eapply exec_straight_at;
eauto. }
rewrite D;
exact LEAF.
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 (
LEAF : (
Compopts.optim_leaf tt &&
is_leaf_function f =
true ->
rs1#
RA =
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#
RA =
rs1#
RA) ->
exists st',
plus step tge (
State rs1 m1')
E0 st' /\
match_states (
Mach.State s fb sp c' ms2 m2)
st'.
Proof.
Lemma exec_straight_opt_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 (
LEAF : (
Compopts.optim_leaf tt &&
is_leaf_function f =
true ->
rs1#
RA =
parent_ra s)),
(
forall k c (
TR:
transl_instr f i ep k =
OK c),
exists jmp,
exists k',
exists rs2,
exec_straight_opt 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#
RA =
rs1#
RA) ->
exists st',
plus step tge (
State rs1 m1')
E0 st' /\
match_states (
Mach.State s fb sp c' ms2 m2)
st'.
Proof.
intros.
inversion H3.
subst.
monadInv H9.
exploit H5;
eauto.
intros [
jmp [
k' [
rs2 [
A [
B [
C D]]]]]].
generalize (
functions_transl _ _ _
H7 H8);
intro FN.
generalize (
transf_function_no_overflow _ _
H8);
intro NOOV.
inv A.
-
exploit find_label_goto_label;
eauto.
intros [
tc' [
rs3 [
GOTO [
AT' OTH]]]].
exists (
State rs3 m2');
split.
apply plus_one.
econstructor;
eauto.
eapply find_instr_tail.
eauto.
rewrite C.
eexact GOTO.
econstructor;
eauto.
apply agree_exten with rs2;
auto with asmgen.
congruence.
{
rewrite OTH by congruence.
exact LEAF. }
-
exploit exec_straight_steps_2;
eauto.
intros [
ofs' [
PC2 CT2]].
exploit find_label_goto_label;
eauto.
intros [
tc' [
rs3 [
GOTO [
AT' OTH]]]].
exists (
State rs3 m2');
split.
eapply plus_right'.
eapply exec_straight_steps_1;
eauto.
econstructor;
eauto.
eapply find_instr_tail.
eauto.
rewrite C.
eexact GOTO.
traceEq.
econstructor;
eauto.
apply agree_exten with rs2;
auto with asmgen.
congruence.
{
rewrite OTH by congruence.
rewrite D.
exact LEAF. }
Qed.
We need to show that, in the simulation diagram, we cannot
take infinitely many Mach transitions that correspond to zero
transitions on the Asm side. Actually, all Mach transitions
correspond to at least one Asm 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.
Hint Resolve preg_of_not_X1 :
asmgen.
Remark preg_of_not_X30:
forall r,
negb (
mreg_eq r R30) =
true ->
IR X30 <>
preg_of r.
Proof.
Lemma preg_notin_X1_cons:
forall (
r :
mreg) (
l :
list mreg),
preg_notin X1 l ->
preg_notin X1 (
r ::
l).
Proof.
Lemma preg_notin_X1_destroyed_by_clobber:
forall clobbers,
preg_notin X1 (
destroyed_by_clobber clobbers).
Proof.
Lemma preg_notin_X1_destroyed_by_builtin:
forall ef,
preg_notin X1 (
destroyed_by_builtin ef).
Proof.
This is the simulation diagram. We prove it by case analysis on the Mach transition.
Lemma if_in_is_tail_remains:
forall {
A :
Type } (
l1 :
list A)
l2 x
(
IN :
In x l1)
(
TAIL:
is_tail l1 l2),
(
In x l2).
Proof.
intros.
induction TAIL.
assumption.
cbn.
auto.
Qed.
Lemma is_tail_builtin_not_leaf:
forall b ef args res f0
(
TAIL :
is_tail (
Mbuiltin ef args res ::
b) (
Mach.fn_code f0)),
is_leaf_function f0 =
false.
Proof.
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.
assumption.
compute in H1.
inv H1.
generalize (
preg_val _ _ _
R10 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.