The Compcert certified compiler back-end

Commented Coq development

Version 0.2, 2006-01-07

Introduction

The Compcert back-end is a compiler that generates PowerPC assembly code from a low-level intermediate language called Cminor and a slightly more expressive intermediate language called Csharpminor. 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 back-end and its proof of correctness can be found in the following paper:

Xavier Leroy, Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. Proceedings of the POPL 2006 symposium.

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 may have changed since the overview paper above was written.

This document and all Coq source files referenced from it are copyright 2005, 2006 Institut National de Recherche en Informatique et en Automatique (INRIA) and distributed under the terms of the GNU General Public License version 2.

Table of contents

General-purpose libraries, data structures and algorithms

Definitions and properties used in many parts of the development

Source, intermediate and target languages: syntax and semantics

Compiler passes

Pass Source & target Compiler code Correctness proof
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
Machabstr2mach
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 intermediate languages. Proofs that compiler passes are type-preserving:

All together


Xavier.Leroy@inria.fr