The Compcert verified compiler

Commented Coq development

Version 1.2, 2008-02-13

Introduction

Compcert is a compiler that generates PowerPC assembly code from Clight, a large subset of the C programming language. The particularity of this compiler is that it is written mostly within the specification language of the Coq proof assistant, and its correctness --- the fact that the generated assembly code is semantically equivalent to its source program --- was entirely proved within the Coq proof assistant.

A high-level overview of the Compcert compiler and its proof of correctness can be found in the following papers:

Xavier Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. Proceedings of the POPL 2006 symposium.
Sandrine Blazy, Zaynah Dargaye and Xavier Leroy, Formal verification of a C compiler front-end. Proceedings of Formal Methods 2006, LNCS 4085.

This Web site gives a commented listing of the underlying Coq specifications and proofs. Proof scripts and the parts of the compiler written directly in Caml are omitted. This development is a work in progress; some parts have substantially changed since the overview papers above were written.

The complete sources for Compcert can be downloaded from the Compcert Web site.

This document and the Compcert sources are copyright 2005, 2006, 2007, 2008 Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the following license.

General-purpose libraries, data structures and algorithms

Coqlib: addendum to the Coq standard library.
Maps: finite maps.
Integers: machine integers.
Floats: machine floating-point numbers.
Iteration: various forms of "while" loops.
Ordered: construction of ordered types.
Lattice: construction of semi-lattices.
Kildall: resolution of dataflow inequations by fixpoint iteration.
Parmov: compilation of parallel assignments.

Definitions and properties used in many parts of the development

Errors: the Error monad.
AST: identifiers, whole programs and other common elements of abstract syntaxes.
Values: run-time values.
Events: observable events and traces.
Mem: the memory model.
Globalenvs: global execution environments.
Smallstep: tools for small-step semantics.
Op: operators, addressing modes and their semantics.

Source, intermediate and target languages: syntax and semantics

Clight syntax and its semantics: the source language.
Csharpminor: low-level structured language.
Cminor: low-level structured language, with explicit stack allocation of certain local variables.
CminorSel: like Cminor, with machine-specific operators and addressing modes.
RTL: register transfer language (3-address code, control-flow graph, infinitely many pseudo-registers).
See also: Registers (representation of pseudo-registers).
LTL: location transfer language (3-address code, control-flow graph, finitely many physical registers, infinitely many stack slots).
See also: Locations (representation of locations).
LTLin: like LTL, but the CFG is replaced by a linear list of instructions with explicit branches and labels.
Linear: like LTLin, with explicit spilling, reloading and enforcement of calling conventions.
Mach: like Linear, with a more concrete view of the activation record.
See also: Machabstr abstract semantics for Mach.
See also: Machconcr concrete semantics for Mach.
PPC: abstract syntax for PowerPC assembly code.

Compiler passes

Pass	Source & target	Compiler code	Correctness proof
Simplification of control structures; explication of type-dependent computations	Clight to Csharpminor	Cshmgen	Cshmgenproof1 Cshmgenproof2 Cshmgenproof3
Stack allocation of local variables whose address is taken	Csharpminor to Cminor	Cminorgen	Cminorgenproof
Recognition of operators and addressing modes	Cminor to CminorSel	Selection	Selectionproof
Construction of the CFG, 3-address code generation	Cminor to RTL	RTLgen	RTLgenspec RTLgenproof
Constant propagation	RTL to RTL	Constprop	Constpropproof
Common subexpression elimination	RTL to RTL	CSE	CSEproof
Register allocation by coloring of an interference graph	RTL to LTL	InterfGraph Coloring Allocation	Coloringproof Allocproof
Branch tunneling	LTL to LTL	Tunneling	Tunnelingproof
Linearization of the CFG	LTL to LTLin	Linearize	Linearizeproof
Spilling, reloading, calling conventions	LTLin to Linear	Conventions Reload	Parallelmove Reloadproof
Laying out the activation records	Linear to Mach	Bounds Stacking	Stackingproof
Storing the activation records in memory	Mach to Mach	(none)	PPCgenretaddr Machabstr2concr
Emission of PowerPC assembly	Mach to PPC	PPCgen	PPCgenproof1 PPCgenproof

Type systems

Trivial type systems are used to statically capture well-formedness conditions on the source and intermediate languages.

Ctyping: partial typing for Clight + type-checking
RTLtyping: typing for RTL + type reconstruction.
LTLtyping: typing for LTL.
LTLintyping: typing for LTLin.
Lineartyping: typing for Linear.
Machtyping: typing for Mach.

Proofs that compiler passes are type-preserving:

Alloctyping (register allocation).
Tunnelingtyping (branch tunneling).
Linearizetyping (code linearization).
Reloadtyping (spilling and reloading).
Stackingtyping (layout of activation records).

All together

Main: composing the passes together; the final semantic preservation theorems.
Complements: interesting consequences of the semantic preservation theorems.

Xavier.Leroy@inria.fr