The whole compiler and its proof of semantic preservation
Libraries.
Require Import String.
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Smallstep.
Languages (syntax and semantics).
Require Csyntax.
Require Csem.
Require Cstrategy.
Require Cexec.
Require Clight.
Require Csharpminor.
Require Cminor.
Translation passes.
Require Initializers.
Require SimplExpr.
Require SimplLocalsDummy.
Require Cshmgen.
Require Cminorgen.
Proofs of semantic preservation.
Require SimplExprproof.
Require SimplLocalsDummyproof.
Require Cshmgenproof.
Require Cminorgenproof.
Pretty-printers (defined in Caml).
Parameter print_Clight:
Clight.program ->
unit.
Parameter print_Cminor:
Cminor.program ->
unit.
Open Local Scope string_scope.
Composing the translation passes
We first define useful monadic composition operators,
along with funny (but convenient) notations.
Definition apply_total (
A B:
Type) (
x:
res A) (
f:
A ->
B) :
res B :=
match x with Error msg =>
Error msg |
OK x1 =>
OK (
f x1)
end.
Definition apply_partial (
A B:
Type)
(
x:
res A) (
f:
A ->
res B) :
res B :=
match x with Error msg =>
Error msg |
OK x1 =>
f x1 end.
Notation "
a @@@
b" :=
(
apply_partial _ _ a b) (
at level 50,
left associativity).
Notation "
a @@
b" :=
(
apply_total _ _ a b) (
at level 50,
left associativity).
Definition print {
A:
Type} (
printer:
A ->
unit) (
prog:
A) :
A :=
let unused :=
printer prog in prog.
Definition time {
A B:
Type} (
name:
string) (
f:
A ->
B) :
A ->
B :=
f.
We define three translation functions for whole programs: one
starting with a C program, one with a Cminor program, one with an
RTL program. The three translations produce Asm programs ready for
pretty-printing and assembling.
Definition transf_clight_program (
p:
Clight.program) :
res Cminor.program :=
OK p
@@
print print_Clight
@@@
time "
Simplification of locals"
SimplLocalsDummy.transf_program
@@@
time "
C#
minor generation"
Cshmgen.transl_program
@@@
time "
Cminor generation"
Cminorgen.transl_program.
Definition transf_c_program (
p:
Csyntax.program) :
res Cminor.program :=
OK p
@@@
time "
Clight generation"
SimplExpr.transl_program
@@@
transf_clight_program.
Force Initializers and Cexec to be extracted as well.
Definition transl_init :=
Initializers.transl_init.
Definition cexec_do_step :=
Cexec.do_step.
The following lemmas help reason over compositions of passes.
Lemma print_identity:
forall (
A:
Type) (
printer:
A ->
unit) (
prog:
A),
print printer prog =
prog.
Proof.
intros;
unfold print.
destruct (
printer prog);
auto.
Qed.
Lemma compose_print_identity:
forall (
A:
Type) (
x:
res A) (
f:
A ->
unit),
x @@
print f =
x.
Proof.
Semantic preservation
We prove that the
transf_program translations preserve semantics
by constructing the following simulations:
-
Forward simulations from Cstrategy / Cminor / RTL to Asm
(composition of the forward simulations for each pass).
-
Backward simulations for the same languages
(derived from the forward simulation, using receptiveness of the source
language and determinacy of Asm).
-
Backward simulation from Csem to Asm
(composition of two backward simulations).
These results establish the correctness of the whole compiler!
We prove here determinism of Cminor evaluation, since it is needed to obtain
the backward simulation from the forward simulation.
Lemma Cminor_eval_expr_determ:
forall ge sp e m a v1,
Cminor.eval_expr ge sp e m a v1 ->
forall v2,
Cminor.eval_expr ge sp e m a v2 ->
v1 =
v2.
Proof.
induction 1; simpl; intros; eauto;
try solve [inv H0; congruence].
inv H1.
apply IHeval_expr in H4. congruence.
inv H2.
apply IHeval_expr1 in H6.
apply IHeval_expr2 in H8. congruence.
inv H1.
apply IHeval_expr in H4. congruence.
Qed.
Lemma Cminor_eval_exprlist_determ:
forall ge sp e m a v1,
Cminor.eval_exprlist ge sp e m a v1 ->
forall v2,
Cminor.eval_exprlist ge sp e m a v2 ->
v1 =
v2.
Proof.
induction 1;
simpl;
intros;
auto.
inv H;
auto.
inv H1;
auto.
f_equal.
eapply Cminor_eval_expr_determ;
eauto.
eapply IHeval_exprlist;
eauto.
Qed.
Ltac detcm :=
match goal with
A : ?
a = ?
b,
B : ?
a = ?
c |-
_ =>
rewrite A in B;
inv B
|
A:
Cminor.eval_expr ?
ge ?
sp ?
e ?
m ?
a ?
v1,
B:
Cminor.eval_expr ?
ge ?
sp ?
e ?
m ?
a ?
v2 |-
_ =>
rewrite (
Cminor_eval_expr_determ ge sp e m a _ A _ B)
in *;
clear A B
|
A:
Cminor.eval_exprlist ?
ge ?
sp ?
e ?
m ?
a ?
v1,
B:
Cminor.eval_exprlist ?
ge ?
sp ?
e ?
m ?
a ?
v2 |-
_ =>
rewrite (
Cminor_eval_exprlist_determ ge sp e m a _ A _ B)
in *;
clear A B
end.
Lemma cminor_determinate:
forall tp,
determinate (
Cminor.semantics tp).
Proof.
intros;
constructor;
simpl;
intros.
-
inv H;
inv H0;
split;
auto;
try constructor;
simpl in *;
try solve [
exfalso;
auto];
repeat detcm;
try congruence.
eapply Events.external_call_determ;
eauto.
generalize (
Events.external_call_determ _ _ _ _ _ _ _ _ _ _ H2 H13).
intros [
A B]
C.
apply B in C.
destruct C;
congruence.
inv H2;
inv H14.
congruence.
congruence.
generalize (
Events.external_call_determ _ _ _ _ _ _ _ _ _ _ H1 H7).
tauto.
intro.
generalize (
Events.external_call_determ _ _ _ _ _ _ _ _ _ _ H1 H7).
intros [
A B].
apply B in H.
destruct H;
congruence.
-
red;
intros.
inv H;
simpl;
auto;
eapply Events.external_call_trace_length;
eauto.
-
inv H;
inv H0.
repeat detcm.
unfold ge,
ge0 in *.
congruence.
-
red;
intros.
inv H.
intro A;
inv A.
-
inv H;
inv H0.
congruence.
Qed.
Theorem transf_clight_program_correct:
forall p tp,
transf_clight_program p =
OK tp ->
forward_simulation (
Clight.semantics1 p) (
Cminor.semantics tp)
*
backward_simulation (
Clight.semantics1 p) (
Cminor.semantics tp).
Proof.
Theorem transf_cstrategy_program_correct:
forall p tp,
transf_c_program p =
OK tp ->
forward_simulation (
Cstrategy.semantics p) (
Cminor.semantics tp)
*
backward_simulation (
atomic (
Cstrategy.semantics p)) (
Cminor.semantics tp).
Proof.
Theorem transf_c_program_correct:
forall p tp,
transf_c_program p =
OK tp ->
backward_simulation (
Csem.semantics p) (
Cminor.semantics tp).
Proof.