Library compcert.driver.Compiler

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.
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 Tailcall.
Require Inlining.
Require Renumber.
Require Constprop.
Require CSE.
Require Deadcode.
Require Allocation.
Require Tunneling.
Require Linearize.
Require CleanupLabels.
Require Stacking.
Require Asmgen.

Proofs of semantic preservation.

Require SimplExprproof.
Require SimplLocalsproof.
Require Cshmgenproof.
Require Cminorgenproof.
Require Import SelectLongproofImpl.
Require Selectionproof.
Require RTLgenproof.
Require Tailcallproof.
Require Inliningproof.
Require Renumberproof.
Require Import ValueAnalysisImpl.
Require Constpropproof.
Require CSEproof.
Require Deadcodeproof.
Require Import DeadcodeproofImpl.
Require Allocproof.
Require Tunnelingproof.
Require Linearizeproof.
Require CleanupLabelsproof.
Require Stackingproof.
Require Asmgenproof.

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: LTL.program -> unit.
Parameter print_Mach: Mach.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.

Force Initializers and Cexec to be extracted as well.

CompCertX:test-compcert-param-memory In fact, we have to list all extracted symbols that are actually used in OCaml code, and instantiate them with the concrete Memimpl memory model. They have nothing to do with compilation, they are relevant only for initializer and interpreter. See InitializersImpl and CexecImpl.

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.
  intros. destruct x; simpl. rewrite print_identity. auto. auto.
Qed.

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!

CompCertX:test-compcert-param-memory We create section WITHMEM and associated contexts to parameterize the proof over the memory model. We also parameterize over mmatch_inj, the proof that matching a concrete memory state with an abstract representation yields a memory that injects into itself. We also parameterize over magree_spec, the specification of memory matching for dead code elimination (a weaker form of memory extension.) CompCertX:test-compcert-param-extcall Actually, we also need to parameterize over external functions. To this end, we created a CompilerConfiguration class (cf. Events) which is designed to be the single class on which the whole CompCert is to be parameterized. It includes all operations and properties on which CompCert depends: memory model, semantics of external functions and their preservation through compilation. But it does not include mmatch_inj nor magree_spec (because their specification are too specific to the optimizations)

CompCertX:test-compcert-param-i64-helpers Because of the axiom get_helpers_correct, we need to instantiate those classes now. It does not matter for whole programs.