The CompCert verified compiler

Commented Coq development

Version 3.13, 2023-07-04

Chamois fork for the KVX backend: version 2024-04-29

The Chamois CompCert fork for the KVX backend

This web page is a patched version of the table of contents of the official CompCert sources documentation, as given on the CompCert Web site. The unmodified parts of this table appear in gray.

A high-level view of this CompCert backend is provided by the following documents:

Formally Verifying Optimizations with Block Simulations an OOPSLA'23 paper, by Gourdin, Bonneau, Boulmé, Monniaux and Bérard.
Certified and Efficient Instruction Scheduling, an OOPSLA'20 paper, by Six, Boulmé and Monniaux.
Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion, a LCTES'21 paper, by Monniaux and Six.
More papers and details are given in the The Git repo README.md.

The people responsible for this version are

Sylvain Boulmé (Grenoble-INP, Verimag)
David Monniaux (CNRS, Verimag)
Léo Gourdin (UGA, Verimag)
Benjamin Bonneau (ENS-PSL, UGA, Verimag)
Alexandre Bérard (Framatome, UGA, Verimag).

and formerly

Cyril Six (Kalray)

with contributions of:

Justus Fasse (M2R UGA, now at KU Leuven).
Pierre Goutagny and Nicolas Nardino (L3 ENS-Lyon 2021).

Introduction

CompCert is a compiler that generates ARM, PowerPC, RISC-V and x86 assembly code from CompCert C, 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.

High-level descriptions of the CompCert compiler and its proof of correctness can be found in the following papers (in increasing order of technical details):

Xavier Leroy, Formal verification of a realistic compiler. Communications of the ACM 52(7), July 2009.
Xavier Leroy, A formally verified compiler back-end. Journal of Automated Reasoning 43(4):363-446, 2009.

This Web site gives a commented listing of the underlying Coq specifications and proofs. Proof scripts are folded by default, but can be viewed by clicking on "Proof". Some modules (written in italics below) differ between the five target architectures. The PowerPC versions of these modules are shown below; the AArch64, ARM, x86 and RISC-V versions can be found in the source distribution.

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 Git repository or the CompCert Web site.

This document and the CompCert sources are copyright Institut National de Recherche en Informatique et en Automatique (INRIA) and AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the following license.

Compiler options specific to the Chamois fork

See this page.

Oracles' documentation

The various oracles validated by translation in our CompCert version are documented here. Most of them rely on the symbolic execution validator provided with the BTL IR, but there are also some specialized oracles helping in specific passes. Note that this documentation only covers oracles from the Chamois fork, not those of the mainline CompCert.

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.
UnionFind: a persistent union-find data structure.
Postorder: postorder numbering of a directed graph.

The Impure library (of Boulmé)

ImpConfig: declares the Impure monad and defines its extraction.
ImpCore: defines notations for the Impure monad and a wlp_simplify tactic (to reason about Impure functions in a Hoare-logic style).
ImpLoops, ImpIO, ImpHCons: declare Impure oracles and define operators from these oracles. ImpExtern exports all these impure operators.
ImpMonads: axioms of "impure computations" and some Coq models of these axioms.
ImpPrelude: declares the data types exchanged with Impure oracles.

The `abstractbb` library, introduced for Aarch64 and KVX cores

This library introduces a block intermediate representation used for postpass scheduling verification. It might be extended to others backends.

AbstractBasicBlocksDef: an IR for verifying some semantic properties on basic-blocks.
Parallelizability: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block.
ImpSimuTest: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines SeqSimuTheory with hash-consing and uses The Impure library to reason on physical equality and handling of imperative code in Coq.

Definitions and theorems used in many parts of the development

Errors: the Error monad.
AST: identifiers, whole programs and other common elements of abstract syntaxes.
Linking: generic framework to define syntactic linking over the CompCert languages.
Values: run-time values.
Events: observable events and traces.
Memory: memory model.
See also: Memdata (in-memory representation of data).
Globalenvs: global execution environments.
Smallstep: tools for small-step semantics.
Behaviors: from small-step semantics to observable behaviors of programs.
Determinism: determinism properties of small-step semantics.
Op: operators, addressing modes and their semantics.
Builtins: semantics of built-in functions.
See also: Builtins0 (target-independent part), Builtins1 (target-dependent part).
Unityping: a solver for atomic unification constraints.

Source, intermediate and target languages: syntax and semantics

The CompCert C source language: syntax and semantics and determinized semantics and type system.
See also: type expressions and operators (syntax and semantics).
See also: reference interpreter.
Clight: a simpler version of CompCert C where expressions contain no side-effects.
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 of basic blocks, finitely many physical registers, infinitely many stack slots).
See also: Locations (representation of locations) and Machregs (description of processor registers).
Linear: like LTL, but the CFG is replaced by a linear list of instructions with explicit branches and labels.
Mach: like Linear, with a more concrete view of the activation record.
Asm: abstract syntax for PowerPC assembly code.

Languages introduced in the Chamois version

Generic (or possibly adaptable) Intermediate Representations (IR):

BTL: an IR dedicated to defensive certification of middle-end optimizations (before register allocation). BTL stands for "Block Transfer Language".
Machblock: a variant of Mach, with a syntax for basic-blocks, and a block-step semantics (execute one basic-block in one step). This IR is generic over the processor and used for KVX and Aarch64.
Asmblock: a variant of Asm, with a big-step semantics of basic-blocks. This IR is an intermediate step between Machblock and Asm on backends featuring postpass scheduling (KVX and Aarch64).
AbstractBasicBlocks: the AbstractBasicBlocks Domain Specific Language (DSL) used in the postpass scheduling verification. This DSL is only used as a library on KVX and Aarch64.

Specific to KVX:

Asmvliw: abstract syntax and semantics for KVX VLIW assembly: atomic instructions are grouped by "bundles". These bundles are executed sequentially, but execution is parallel within bundles.
kvx/Asm: a variant of Asmvliw with a flat syntax for bundles, instead of a structured one (bundle termination is encoded as a pseudo-instruction). This IR is mainly a wrapper of Asmvliw for a smooth integration in CompCert (and an easier pretty-printing of the abstract syntax).

Compiler passes

Pass	Source & target	Compiler code	Correctness proof
Pulling side-effects out of expressions; fixing an evaluation order	CompCert C to Clight	SimplExpr	SimplExprspec SimplExprproof
Pulling non-adressable scalar local variables out of memory	Clight to Clight	SimplLocals	SimplLocalsproof
Simplification of control structures; explication of type-dependent computations	Clight to Csharpminor	Cshmgen	Cshmgenproof
Stack allocation of local variables whose address is taken; simplification of switch statements	Csharpminor to Cminor	Cminorgen	Cminorgenproof
Recognition of operators and addressing modes; if-conversion	Cminor to CminorSel	Selection SelectOp SelectLong SelectDiv SplitLong	Selectionproof SelectOpproof SelectLongproof SelectDivproof SplitLongproof
Construction of the CFG, 3-address code generation	CminorSel to RTL	RTLgen	RTLgenspec RTLgenproof
Recognition of tail calls	RTL to RTL	Tailcall	Tailcallproof
Recognition of tail recursion calls	RTL to RTL	Tailrec	Tailrecproof
Function inlining	RTL to RTL	Inlining	Inliningspec Inliningproof
Passes introduced for profiling (for later use in trace selection)
Insert profiling annotations (for recording experiments -- see PROFILE.md).	RTL to RTL	Profiling	Profilingproof
Update ICond nodes (from recorded experiments -- see PROFILE.md).	RTL to RTL	ProfilingExploit	ProfilingExploitproof
Postorder renumbering of the CFG (1)	RTL to RTL	Renumber	Renumberproof
[CSE1] Common subexpression elimination (1)	RTL to RTL	CSE CombineOp	CSEproof CombineOpproof
[Duplicate pass] Static Prediction + Unroll single
Add static prediction information to Icond nodes Unrolls a single iteration of innermost loops	RTL to RTL	Duplicate (generic checker)	Duplicateproof (generic proof) Duplicatepasses (several passes from several oracles)
Postorder renumbering of the CFG (2)	RTL to RTL	Renumber	Renumberproof
[Duplicate pass] Tail Duplication
Performs tail duplication on interesting traces to form superblocks	RTL to RTL	Duplicate (generic checker)	Duplicateproof (generic proof) Duplicatepasses (several passes from several oracles)
Postorder renumbering of the CFG (3)	RTL to RTL	Renumber	Renumberproof
[Duplicate pass] Unroll Body
Unrolling the body of innermost loops	RTL to RTL	Duplicate (generic checker)	Duplicateproof (generic proof) Duplicatepasses (several passes from several oracles)
Postorder renumbering of the CFG (4)	RTL to RTL	Renumber	Renumberproof
[Duplicate pass] Loop Rotate
Loop rotation	RTL to RTL	Duplicate (generic checker)	Duplicateproof (generic proof) Duplicatepasses (several passes from several oracles)
Postorder renumbering of the CFG (5)	RTL to RTL	Renumber	Renumberproof
Constant propagation	RTL to RTL	Constprop ConstpropOp	Constpropproof ConstproppOproof
Integer Promotion Pass (RISC-V only)	RTL to RTL	IntPromotionCommon	IntPromotion
Postorder renumbering of the CFG (6)	RTL to RTL	Renumber	Renumberproof
[CSE1] Common subexpression elimination (2)	RTL to RTL	CSE CombineOp	CSEproof CombineOpproof
[CSE2] Common subexpression elimination	RTL to RTL	CSE2	CSE2proof
[CSE3] Common subexpression elimination (1)	RTL to RTL	CSE3	CSE3proof
KillUselessMoves: removing useless moves instructions after CSE3	RTL to RTL	KillUselessMoves	KillUselessMovesproof
Forwarding Moves	RTL to RTL	ForwardMoves	ForwardMovesproof
Redundancy elimination (1)	RTL to RTL	Deadcode	Deadcodeproof
RTL Tunneling	RTL to RTL	RTLTunneling	RTLTunnelingproof
Allnontrap: transforming loads to non-trapping ones	RTL to RTL	Allnontrap	Allnontrapproof
Removal of unused static globals	RTL to RTL	Unusedglob	Unusedglobproof
Passes introduced for BTL
Block selection (with Liveness information)	RTL to BTL	RTLtoBTL	RTLtoBTLproof BTLmatchRTL
Block Optimizations	BTL to BTL	BTL_BlockSimulation	BTL_BlockSimulationproof with BTL_Invariants (syntax of symbolic expressions and invariants); BTL_SEtheory (the theory of symbolic execution on BTL_); BTL_SEsimuref (the low-level specifications of the simulation checker); BTL_SEimpl_prelude (the implementation's common definitions); BTL_SEimpl_SE (the Symbolic Execution implementation); BTL_SEimpl_SI (the Symbolic Invariants implementation); and BTL_SEimpl_check (the simulation checker with hash-consing).
Forgeting blocks	BTL to RTL	BTLtoRTL	BTLtoRTLproof BTLmatchRTL
Postorder renumbering of the CFG (7)	RTL to RTL	Renumber	Renumberproof
Passes from register allocation
Register allocation (validation a posteriori)	RTL to LTL	Allocation	Allocationproof
Branch tunneling	LTL to LTL	LTLTunneling	LTLTunnelingproof
Linearization of the CFG	LTL to Linear	Linearize	Linearizeproof
Removal of unreferenced labels	Linear to Linear	CleanupLabels	CleanupLabelsproof
Synthesis of debugging information	Linear to Linear	Debugvar	Debugvarproof
Laying out the activation records	Linear to Mach	Stacking Bounds Stacklayout	Stackingproof Separation
Passes introduced for backends with postpass scheduling
Reconstruction of basic-blocks at Mach level	Mach to Machblock	Machblockgen	ForwardSimulationBlock Machblockgenproof
Emission of purely sequential assembly code	Machblock to Asmblock	Asmblockgen	Asmblockgenproof0 Asmblockgenproof1 Asmblockgenproof
Bundling (and basic-block scheduling)	Asmblock to Asmvliw	PostpassScheduling using Asmblockdeps and the `abstractbb` library	PostpassSchedulingproof Asmblockprops
Flattening bundles (only a bureaucratic operation)	Asmvliw to Asm	Asmgen	Asmgenproof (whole simulation proof from `Mach` to `Asm`)

All together (there are many more passes than on vanilla CompCert: their order is specified in Compiler)

Compiler: composing the passes together; whole-compiler semantic preservation theorems.
Complements: interesting consequences of the semantic preservation theorems.

Static analyses

The following static analyses are performed over the RTL intermediate representation to support optimizations such as constant propagation, CSE, and dead code elimination.

Liveness: liveness analysis.
ValueAnalysis: value and alias analysis.
See also: ValueDomain: the abstract domain for value analysis.
See also: ValueAOp: processor-dependent parts of value analysis.
Deadcode: neededness analysis.
See also: NeedDomain: the abstract domain for neededness analysis.
See also: NeedOp: processor-dependent parts of neededness analysis.

Type systems

The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.

Ctyping: typing for CompCert C + type-checking functions.
RTLtyping: typing for RTL + type reconstruction.
Lineartyping: typing for Linear.