Library Compiler
The whole compiler and its proof of semantic preservation
Libraries.
Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import AST.
Require Import Values.
Require Import Smallstep.
Languages (syntax and semantics).
Require Csyntax.
Require Csem.
Require Csharpminor.
Require Cminor.
Require CminorSel.
Require RTL.
Require LTL.
Require LTLin.
Require Linear.
Require Mach.
Require Asm.
Translation passes.
Require Cshmgen.
Require Cminorgen.
Require Selection.
Require RTLgen.
Require Tailcall.
Require Constprop.
Require CSE.
Require Allocation.
Require Tunneling.
Require Linearize.
Require Reload.
Require Stacking.
Require Asmgen.
Type systems.
Require Ctyping.
Require RTLtyping.
Require LTLtyping.
Require LTLintyping.
Require Lineartyping.
Require Machtyping.
Proofs of semantic preservation and typing preservation.
Require Cshmgenproof3.
Require Cminorgenproof.
Require Selectionproof.
Require RTLgenproof.
Require Tailcallproof.
Require Constpropproof.
Require CSEproof.
Require Allocproof.
Require Alloctyping.
Require Tunnelingproof.
Require Tunnelingtyping.
Require Linearizeproof.
Require Linearizetyping.
Require Reloadproof.
Require Reloadtyping.
Require Stackingproof.
Require Stackingtyping.
Require Machabstr2concr.
Require Asmgenproof.
Open Local Scope string_scope.
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).
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.
There are two ways to compose the compiler passes. The first translates every function from the Cminor program from Cminor to RTL, then to LTL, etc, all the way to Asm, and iterates this transformation for every function. The second translates the whole Cminor program to a RTL program, then to an LTL program, etc. Between Cminor and Asm, we follow the first approach because it has lower memory requirements. The translation from Clight to Asm follows the second approach.
The translation of an RTL function to an Asm function is as follows.
There are two ways to compose the compiler passes. The first translates every function from the Cminor program from Cminor to RTL, then to LTL, etc, all the way to Asm, and iterates this transformation for every function. The second translates the whole Cminor program to a RTL program, then to an LTL program, etc. Between Cminor and Asm, we follow the first approach because it has lower memory requirements. The translation from Clight to Asm follows the second approach.
The translation of an RTL function to an Asm function is as follows.
Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef :=
OK f
@@ Tailcall.transf_fundef
@@ Constprop.transf_fundef
@@ CSE.transf_fundef
@@@ Allocation.transf_fundef
@@ Tunneling.tunnel_fundef
@@@ Linearize.transf_fundef
@@ Reload.transf_fundef
@@@ Stacking.transf_fundef
@@@ Asmgen.transf_fundef.
Definition transf_cminor_fundef (f: Cminor.fundef) : res Asm.fundef :=
OK f
@@ Selection.sel_fundef
@@@ RTLgen.transl_fundef
@@@ transf_rtl_fundef.
The corresponding translations for whole program follow.
Definition transf_rtl_program (p: RTL.program) : res Asm.program :=
transform_partial_program transf_rtl_fundef p.
Definition transf_cminor_program (p: Cminor.program) : res Asm.program :=
transform_partial_program transf_cminor_fundef p.
Definition transf_c_program (p: Csyntax.program) : res Asm.program :=
match Ctyping.typecheck_program p with
| false =>
Error (msg "Ctyping: type error")
| true =>
OK p
@@@ Cshmgen.transl_program
@@@ Cminorgen.transl_program
@@@ transf_cminor_program
end.
The following lemmas help reason over compositions of passes.
Lemma map_partial_compose:
forall (X A B C: Type)
(ctx: X -> errmsg)
(f1: A -> res B) (f2: B -> res C)
(pa: list (X * A)) (pc: list (X * C)),
map_partial ctx (fun f => f1 f @@@ f2) pa = OK pc ->
exists pb, map_partial ctx f1 pa = OK pb /\ map_partial ctx f2 pb = OK pc.
Lemma transform_partial_program_compose:
forall (A B C V: Type)
(f1: A -> res B) (f2: B -> res C)
(pa: program A V) (pc: program C V),
transform_partial_program (fun f => f1 f @@@ f2) pa = OK pc ->
exists pb, transform_partial_program f1 pa = OK pb /\
transform_partial_program f2 pb = OK pc.
Lemma transform_program_partial_program:
forall (A B V: Type) (f: A -> B) (p: program A V) (tp: program B V),
transform_partial_program (fun x => OK (f x)) p = OK tp ->
transform_program f p = tp.
Lemma transform_program_compose:
forall (A B C V: Type)
(f1: A -> res B) (f2: B -> C)
(pa: program A V) (pc: program C V),
transform_partial_program (fun f => f1 f @@ f2) pa = OK pc ->
exists pb, transform_partial_program f1 pa = OK pb /\
transform_program f2 pb = pc.
Lemma transform_partial_program_identity:
forall (A V: Type) (pa pb: program A V),
transform_partial_program (@OK A) pa = OK pb ->
pa = pb.
We prove that the
transf_program translations preserve semantics.
The proof composes the semantic preservation results for each pass.
This establishes the correctness of the whole compiler!
Theorem transf_rtl_program_correct:
forall p tp beh,
transf_rtl_program p = OK tp ->
not_wrong beh ->
RTL.exec_program p beh ->
Asm.exec_program tp beh.
Theorem transf_cminor_program_correct:
forall p tp beh,
transf_cminor_program p = OK tp ->
not_wrong beh ->
Cminor.exec_program p beh ->
Asm.exec_program tp beh.
Theorem transf_c_program_correct:
forall p tp beh,
transf_c_program p = OK tp ->
not_wrong beh ->
Csem.exec_program p beh ->
Asm.exec_program tp beh.