The whole compiler and its proof of semantic preservation
Libraries.
Require Import String.
Require Import Coqlib Errors.
Require Import AST Linking Smallstep.
Languages (syntax and semantics).
Require Ctypes Csyntax Csem Cstrategy Cexec.
Require Clight.
Require Csharpminor.
Require Cminor.
Require CminorSel.
Require RTL.
Require LTL.
Require Linear.
Require Mach.
Require Asm.
Translation passes.
Require Initializers.
Require SimplExpr.
Require SimplLocals.
Require Cshmgen.
Require Cminorgen.
Require Selection.
Require RTLgen.
Require Import Duplicatepasses.
Require Tailcall.
Require Inlining.
Require Profiling.
Require ProfilingExploit.
Require FirstNop.
Require Renumber.
Require CSE.
Require Constprop.
Require CSE.
Require CSE2.
Require CSE3.
Require KillUselessMoves.
Require ForwardMoves.
Require Deadcode.
Require RTLTunneling.
Require LICM.
Require Allnontrap.
Require Unusedglob.
Require Allocation.
Require LTLTunneling.
Require Linearize.
Require CleanupLabels.
Require Debugvar.
Require Stacking.
Require Asmgen.
Proofs of semantic preservation.
Require SimplExprproof.
Require SimplLocalsproof.
Require Cshmgenproof.
Require Cminorgenproof.
Require Selectionproof.
Require RTLgenproof.
Require Tailcallproof.
Require Inliningproof.
Require Profilingproof.
Require ProfilingExploitproof.
Require FirstNopproof.
Require Renumberproof.
Require CSEproof.
Require Constpropproof.
Require CSEproof.
Require CSE2proof.
Require CSE3proof.
Require KillUselessMovesproof.
Require ForwardMovesproof.
Require Deadcodeproof.
Require RTLTunnelingproof.
Require LICMproof.
Require Allnontrapproof.
Require Unusedglobproof.
Require Allocationproof.
Require LTLTunnelingproof.
Require Linearizeproof.
Require CleanupLabelsproof.
Require Debugvarproof.
Require Stackingproof.
Require Import Asmgenproof.
Command-line flags.
Require Import Compopts.
Require Import BTLpasses.
Pretty-printers (defined in Caml).
Parameter print_Clight:
Clight.program ->
unit.
Parameter print_Cminor:
Cminor.program ->
unit.
Parameter print_RTL:
Z ->
RTL.program ->
unit.
Parameter print_LTL:
Z ->
LTL.program ->
unit.
Parameter print_Mach:
Mach.program ->
unit.
Local Open 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.
Definition total_if {
A:
Type}
(
flag:
unit ->
bool) (
f:
A ->
A) (
prog:
A) :
A :=
if flag tt then f prog else prog.
Definition partial_if {
A:
Type}
(
flag:
unit ->
bool) (
f:
A ->
res A) (
prog:
A) :
res A :=
if flag tt then f prog else OK prog.
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_rtl_program (
f:
RTL.program) :
res Asm.program :=
OK f
@@
print (
print_RTL 0)
@@
total_if Compopts.optim_tailcalls (
time "
Tail calls"
Tailcall.transf_program)
@@
print (
print_RTL 1)
@@@ (
time "
Inlining"
Inlining.transf_program)
@@
print (
print_RTL 2)
@@
total_if Compopts.profile_arcs (
time "
Profiling insertion"
Profiling.transf_program)
@@
print (
print_RTL 3)
@@
total_if Compopts.branch_probabilities (
time "
Profiling use"
ProfilingExploit.transf_program)
@@
print (
print_RTL 4)
@@
total_if Compopts.optim_move_loop_invariants (
time "
Inserting initial nop"
FirstNop.transf_program)
@@
print (
print_RTL 5)
@@ (
time "
Renumbering"
Renumber.transf_program)
@@
print (
print_RTL 6)
@@@
partial_if Compopts.optim_CSE (
time "
CSE"
CSE.transf_program)
@@
print (
print_RTL 7)
@@@ (
time "
Static Prediction +
inverting conditions"
Staticpredict.transf_program)
@@
print (
print_RTL 8)
@@@ (
time "
Unrolling one iteration out of innermost loops"
Unrollsingle.transf_program)
@@
print (
print_RTL 9)
@@ (
time "
Renumbering pre tail duplication"
Renumber.transf_program)
@@
print (
print_RTL 10)
@@@ (
time "
Performing tail duplication"
Tailduplicate.transf_program)
@@
print (
print_RTL 11)
@@ (
time "
Renumbering pre unrolling"
Renumber.transf_program)
@@
print (
print_RTL 12)
@@@ (
time "
Unrolling the body of innermost loops"
Unrollbody.transf_program)
@@
print (
print_RTL 13)
@@ (
time "
Renumbering pre constprop"
Renumber.transf_program)
@@
print (
print_RTL 14)
@@
total_if Compopts.optim_constprop (
time "
Constant propagation"
Constprop.transf_program)
@@
print (
print_RTL 15)
@@ (
time "
Renumbering pre CSE"
Renumber.transf_program)
@@
print (
print_RTL 16)
@@@
partial_if Compopts.optim_CSE (
time "
CSE"
CSE.transf_program)
@@
print (
print_RTL 17)
@@
total_if Compopts.optim_CSE2 (
time "
CSE2"
CSE2.transf_program)
@@
print (
print_RTL 18)
@@@
partial_if Compopts.optim_CSE3 (
time "
CSE3"
CSE3.transf_program)
@@
print (
print_RTL 19)
@@
total_if Compopts.optim_CSE3 (
time "
Kill useless moves after CSE3"
KillUselessMoves.transf_program)
@@
print (
print_RTL 20)
@@
total_if Compopts.optim_forward_moves (
time "
Forwarding moves"
ForwardMoves.transf_program)
@@
print (
print_RTL 21)
@@@
partial_if Compopts.optim_redundancy (
time "
Redundancy elimination"
Deadcode.transf_program)
@@
print (
print_RTL 22)
@@@ (
time "
RTL Branch Tunneling"
RTLTunneling.transf_program)
@@
print (
print_RTL 23)
@@ (
time "
Renumbering pre rotate"
Renumber.transf_program)
@@
print (
print_RTL 24)
@@@ (
time "
Loop Rotate"
Looprotate.transf_program)
@@
print (
print_RTL 25)
@@
total_if Compopts.optim_move_loop_invariants (
time "
Renumbering for LICM"
Renumber.transf_program)
@@
print (
print_RTL 26)
@@@
partial_if Compopts.optim_move_loop_invariants (
time "
LICM"
LICM.transf_program)
@@
print (
print_RTL 27)
@@
total_if Compopts.optim_move_loop_invariants (
time "
Renumbering for LICM"
Renumber.transf_program)
@@
print (
print_RTL 28)
@@@
partial_if Compopts.optim_move_loop_invariants (
time "
CSE3 for LICM"
CSE3.transf_program)
@@
print (
print_RTL 29)
@@@
partial_if Compopts.optim_move_loop_invariants (
time "
Redundancy elimination for LICM"
Deadcode.transf_program)
@@
print (
print_RTL 30)
@@
total_if Compopts.all_loads_nontrap (
Allnontrap.transf_program)
@@
print (
print_RTL 31)
@@@ (
time "
Unused globals"
Unusedglob.transf_program)
@@
print (
print_RTL 32)
@@
total_if Compopts.btl_bb (
time "
Renumbering pre BTL (
BB)"
Renumber.transf_program)
@@
print (
print_RTL 33)
@@@
partial_if Compopts.btl_bb (
time "
BTL BBpasses"
BTL_BBpasses.transf_program)
@@
print (
print_RTL 34)
@@@
partial_if Compopts.lct_tun (
time "
RTL Tunneling post LCT"
RTLTunneling.transf_program)
@@
print (
print_RTL 35)
@@
total_if Compopts.btl_sb (
time "
Renumbering pre BTL (
SB)"
Renumber.transf_program)
@@
print (
print_RTL 36)
@@@
partial_if Compopts.btl_sb (
time "
BTL SBpasses"
BTL_SBpasses.transf_program)
@@
print (
print_RTL 37)
@@@ (
time "
Register allocation"
Allocation.transf_program)
@@
print (
print_LTL 1)
@@@ (
time "
LTL Branch tunneling"
LTLTunneling.transf_program)
@@
print (
print_LTL 2)
@@@ (
time "
CFG linearization"
Linearize.transf_program)
@@ (
time "
Label cleanup"
CleanupLabels.transf_program)
@@@
partial_if Compopts.debug (
time "
Debugging info for local variables"
Debugvar.transf_program)
@@@ (
time "
Mach generation"
Stacking.transf_program)
@@
print (
print_Mach)
@@@
time "
Total Mach->
Asm generation"
Asmgen.transf_program.
Definition transf_cminor_program (
p:
Cminor.program) :
res Asm.program :=
OK p
@@
print print_Cminor
@@@
time "
Instruction selection"
Selection.sel_program
@@@
time "
RTL generation"
RTLgen.transl_program
@@@
transf_rtl_program.
Definition transf_clight_program (
p:
Clight.program) :
res Asm.program :=
OK p
@@
print print_Clight
@@@
time "
Simplification of locals"
SimplLocals.transf_program
@@@
time "
C#
minor generation"
Cshmgen.transl_program
@@@
time "
Cminor generation"
Cminorgen.transl_program
@@@
transf_cminor_program.
Definition transf_c_program (
p:
Csyntax.program) :
res Asm.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.
Relational specification of compilation
Definition match_if {
A:
Type} (
flag:
unit ->
bool) (
R:
A ->
A ->
Prop):
A ->
A ->
Prop :=
if flag tt then R else eq.
Lemma total_if_match:
forall (
A:
Type) (
flag:
unit ->
bool) (
f:
A ->
A) (
rel:
A ->
A ->
Prop) (
prog:
A),
(
forall p,
rel p (
f p)) ->
match_if flag rel prog (
total_if flag f prog).
Proof.
Lemma partial_if_match:
forall (
A:
Type) (
flag:
unit ->
bool) (
f:
A ->
res A) (
rel:
A ->
A ->
Prop) (
prog tprog:
A),
(
forall p tp,
f p =
OK tp ->
rel p tp) ->
partial_if flag f prog =
OK tprog ->
match_if flag rel prog tprog.
Proof.
Global Instance TransfIfLink {
A:
Type} {
LA:
Linker A}
(
flag:
unit ->
bool) (
transf:
A ->
A ->
Prop) (
TL:
TransfLink transf)
:
TransfLink (
match_if flag transf).
Proof.
unfold match_if.
destruct (
flag tt).
-
auto.
-
red;
intros.
subst tp1 tp2.
exists p;
auto.
Qed.
This is the list of compilation passes of CompCert in relational style.
Each pass is characterized by a match_prog relation between its
input code and its output code. The mkpass and ::: combinators,
defined in module Linking, ensure that the passes are composable
(the output language of a pass is the input language of the next pass)
and that they commute with linking (property TransfLink, inferred
by the type class mechanism of Coq).
Local Open Scope linking_scope.
Definition CompCert'
s_passes :=
mkpass SimplExprproof.match_prog
:::
mkpass SimplLocalsproof.match_prog
:::
mkpass Cshmgenproof.match_prog
:::
mkpass Cminorgenproof.match_prog
:::
mkpass Selectionproof.match_prog
:::
mkpass RTLgenproof.match_prog
:::
mkpass (
match_if Compopts.optim_tailcalls Tailcallproof.match_prog)
:::
mkpass (
Inliningproof.match_prog)
:::
mkpass (
match_if Compopts.profile_arcs Profilingproof.match_prog)
:::
mkpass (
match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog)
:::
mkpass (
match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog)
:::
mkpass (
Renumberproof.match_prog)
:::
mkpass (
match_if Compopts.optim_CSE CSEproof.match_prog)
:::
mkpass (
Staticpredictproof.match_prog)
:::
mkpass (
Unrollsingleproof.match_prog)
:::
mkpass (
Renumberproof.match_prog)
:::
mkpass (
Tailduplicateproof.match_prog)
:::
mkpass (
Renumberproof.match_prog)
:::
mkpass (
Unrollbodyproof.match_prog)
:::
mkpass (
Renumberproof.match_prog)
:::
mkpass (
match_if Compopts.optim_constprop Constpropproof.match_prog)
:::
mkpass (
Renumberproof.match_prog)
:::
mkpass (
match_if Compopts.optim_CSE CSEproof.match_prog)
:::
mkpass (
match_if Compopts.optim_CSE2 CSE2proof.match_prog)
:::
mkpass (
match_if Compopts.optim_CSE3 CSE3proof.match_prog)
:::
mkpass (
match_if Compopts.optim_CSE3 KillUselessMovesproof.match_prog)
:::
mkpass (
match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog)
:::
mkpass (
match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
:::
mkpass (
RTLTunnelingproof.match_prog)
:::
mkpass (
Renumberproof.match_prog)
:::
mkpass (
Looprotateproof.match_prog)
:::
mkpass (
match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog)
:::
mkpass (
match_if Compopts.optim_move_loop_invariants LICMproof.match_prog)
:::
mkpass (
match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog)
:::
mkpass (
match_if Compopts.optim_move_loop_invariants CSE3proof.match_prog)
:::
mkpass (
match_if Compopts.optim_move_loop_invariants Deadcodeproof.match_prog)
:::
mkpass (
match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog)
:::
mkpass (
Unusedglobproof.match_prog)
:::
mkpass (
match_if Compopts.btl_bb Renumberproof.match_prog)
:::
mkpass (
match_if Compopts.btl_bb BTL_BBpassesproof.match_prog)
:::
mkpass (
match_if Compopts.lct_tun RTLTunnelingproof.match_prog)
:::
mkpass (
match_if Compopts.btl_sb Renumberproof.match_prog)
:::
mkpass (
match_if Compopts.btl_sb BTL_SBpassesproof.match_prog)
:::
mkpass (
Allocationproof.match_prog)
:::
mkpass (
LTLTunnelingproof.match_prog)
:::
mkpass (
Linearizeproof.match_prog)
:::
mkpass (
CleanupLabelsproof.match_prog)
:::
mkpass (
match_if Compopts.debug Debugvarproof.match_prog)
:::
mkpass (
Stackingproof.match_prog)
:::
mkpass Asmgenproof.match_prog
:::
pass_nil _.
Composing the match_prog relations above, we obtain the relation
between CompCert C sources and Asm code that characterize CompCert's
compilation.
Definition match_prog:
Csyntax.program ->
Asm.program ->
Prop :=
pass_match (
compose_passes CompCert'
s_passes).
The transf_c_program function, when successful, produces
assembly code that is in the match_prog relation with the source C program.
Theorem transf_c_program_match:
forall p tp,
transf_c_program p =
OK tp ->
match_prog p tp.
Proof.
Semantic preservation
We now prove that the whole CompCert compiler (as characterized by the
match_prog relation) preserves semantics by constructing
the following simulations:
-
Forward simulations from Cstrategy 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).
:
forall sem,
forward_simulation sem sem.
Proof.
intros.
apply forward_simulation_step with (
fun s1 s2 =>
s2 =
s1);
intros.
-
auto.
-
exists s1;
auto.
-
subst s2;
auto.
-
subst s2.
exists s1';
auto.
Qed.
Lemma match_if_simulation:
forall (
A:
Type) (
sem:
A ->
semantics) (
flag:
unit ->
bool) (
transf:
A ->
A ->
Prop) (
prog tprog:
A),
match_if flag transf prog tprog ->
(
forall p tp,
transf p tp ->
forward_simulation (
sem p) (
sem tp)) ->
forward_simulation (
sem prog) (
sem tprog).
Proof.
Theorem cstrategy_semantic_preservation:
forall p tp,
match_prog p tp ->
forward_simulation (
Cstrategy.semantics p) (
Asm.semantics tp)
/\
backward_simulation (
atomic (
Cstrategy.semantics p)) (
Asm.semantics tp).
Proof.
Theorem c_semantic_preservation:
forall p tp,
match_prog p tp ->
backward_simulation (
Csem.semantics p) (
Asm.semantics tp).
Proof.
Correctness of the CompCert compiler
Combining the results above, we obtain semantic preservation for two
usage scenarios of CompCert: compilation of a single monolithic program,
and separate compilation of multiple source files followed by linking.
In the monolithic case, we have a whole C program p that is
compiled in one run of CompCert to a whole Asm program tp.
Then, tp preserves the semantics of p, in the sense that there
exists a backward simulation of the dynamic semantics of p
by the dynamic semantics of tp.
Theorem transf_c_program_correct:
forall p tp,
transf_c_program p =
OK tp ->
backward_simulation (
Csem.semantics p) (
Asm.semantics tp).
Proof.
Here is the separate compilation case. Consider a nonempty list c_units
of C source files (compilation units), C1 ,,, Cn. Assume that every
C compilation unit Ci is successfully compiled by CompCert, obtaining
an Asm compilation unit Ai. Let asm_unit be the nonempty list
A1 ... An. Further assume that the C units C1 ... Cn can be linked
together to produce a whole C program c_program. Then, the generated
Asm units can be linked together, producing a whole Asm program
asm_program. Moreover, asm_program preserves the semantics of
c_program, in the sense that there exists a backward simulation of
the dynamic semantics of asm_program by the dynamic semantics of c_program.
Theorem separate_transf_c_program_correct:
forall c_units asm_units c_program,
nlist_forall2 (
fun cu tcu =>
transf_c_program cu =
OK tcu)
c_units asm_units ->
link_list c_units =
Some c_program ->
exists asm_program,
link_list asm_units =
Some asm_program
/\
backward_simulation (
Csem.semantics c_program) (
Asm.semantics asm_program).
Proof.