Module MIRcompiler
Require Import Coqlib.
Require Import Errors Traces.
Require Import Common.
Require MIR Asm.
Require RTLinjectgen RTLofRTLinject RTLsort.
Require RTLofRTLinjectproof.
Require Constprop CSE.
Require Fenceelim Fenceintro2 Fenceelim2.
Require Allocation Tunneling Linearize Reload Stacking Asmgen.
Require Alloctyping Tunnelingtyping Linearizetyping Reloadtyping Stackingtyping.
Require Constpropproof CSEproof Tunnelingproof Linearizeproof Reloadproof Stackingproof.
Require RTLsortproof Fenceelimproof Fenceintro2proof Fenceelim2proof.
Require MMproof Asmgenproof.
Parameter print_RTL :
RTL.program ->
unit.
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.
Program compilation
Definition transf_rtlinject_program (
sort fe1 fi2 fe2:
bool)
bi (
p:
RTLinject.program) :
res Asm.program :=
OK p
@@@ (
RTLofRTLinject.transf_program bi)
@@@ (
if sort then RTLsort.transf_program else (
fun x =>
OK x))
@@
print print_RTL
@@
Constprop.transf_program
@@
CSE.transf_program
@@ (
if fe1 then Fenceelim.transf_program else (
fun x =>
x))
@@ (
if fi2 then Fenceintro2.transf_program else (
fun x =>
x))
@@ (
if fe2 then Fenceelim2.transf_program else (
fun x =>
x))
@@@
Allocation.transf_program
@@
Tunneling.tunnel_program
@@@
Linearize.transf_program
@@
Reload.transf_program
@@@
Stacking.transf_program
@@@
Asmgen.transf_program
.
Definition transf_mir_program (
sort fe1 fi2 fe2:
bool)
bi om (
p:
MIR.program) :
res Asm.program :=
OK p
@@@ (
RTLinjectgen.transf_program bi om)
@@@ (
transf_rtlinject_program sort fe1 fi2 fe2 bi)
.
Theorem compiler_correctness :
forall sort fe1 fi2 fe2 bi p p' (
HBI:
ok_bi bi),
transf_rtlinject_program sort fe1 fi2 fe2 bi p =
OK p' ->
forall args trace,
valid_args args ->
prog_traces Asm.x86_sem p'
args trace ->
RTLinjectlow.rtli_traces p args trace.
Proof.
unfold transf_rtlinject_program,
apply_partial,
apply_total;
intros.
repeat (
match goal with
|
H :
context[
match ?
x with OK _ =>
_ |
Error _ =>
_ end] |-
_ =>
destruct x as []
_eqn: ?;
clarify
end).
Ltac typtac2 PL N :=
refine (
modusponens _ _ (
PL _ _)
_);
try edone; [];
intro N.
Ltac typtac3 PL N :=
refine (
modusponens _ _ (
PL _ _ _)
_);
try edone; [];
intro N.
Ltac typtac4 PL N :=
refine (
modusponens _ _ (
PL _ _ _ _)
_);
try edone; [];
intro N.
Ltac phase X :=
eapply (
Sim.traces_incl X);
try edone;
vauto.
Ltac phase2 X :=
eapply (
WTsim.traces_incl X);
try edone;
vauto.
typtac3 Alloctyping.program_typing_preserved ALLOCt.
typtac2 Tunnelingtyping.program_typing_preserved TUNNELt.
typtac4 Linearizetyping.program_typing_preserved LINt.
typtac2 Reloadtyping.program_typing_preserved RLt.
typtac4 Stackingtyping.program_typing_preserved MACHt.
phase (
RTLofRTLinjectproof.rtlgen_sim bi HBI).
assert (
prog_traces RTL.rtl_sem p1 args trace).
phase Constpropproof.constprop_sim.
phase CSEproof.cse_sim.
assert (
prog_traces LTL.ltl_sem p3 args trace)
by (
phase Tunnelingproof.tunnel_sim;
phase Linearizeproof.linearize_sim;
phase Reloadproof.reload_sim;
phase Stackingproof.stacking_sim;
phase MMproof.mm_sim;
phase Asmgenproof.asmgen_sim).
destruct fe1; [
phase Fenceelimproof.fenceelim_sim|];
(
destruct fi2; [
phase Fenceintro2proof.fenceintro2_sim|]);
(
destruct fe2; [
phase2 Fenceelim2proof.fenceelim2sim|]);
phase Allocproof.alloc_sim.
destruct sort;[
phase RTLsortproof.sim|].
clarify.
Qed.
Theorem rtlinject_compiler_correctness :
forall sort fe1 fi2 fe2 bi p p' (
HBI:
ok_bi bi),
transf_rtlinject_program sort fe1 fi2 fe2 bi p =
OK p' ->
forall trace,
RTLinjectlow.safe_program p ->
RTLinjectlow.tfin trace ->
prog_traces Asm.x86_sem p'
nil trace ->
RTLinjectlow.low_traces p trace.
Proof.