The CompCert verified compiler

Commented Coq development

Version 3.11, 2022-06-27

VERIMAG fork version 2022-11-16

The CompCert Verimag's fork

Warning: our fork migrated to Chamois CompCert repository. This web page may no more be up-to-date.

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:

The people responsible for this version are

with contributions of:

Introduction

CompCert is a compiler that generates PowerPC, ARM, 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):

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.

Table of contents

General-purpose libraries, data structures and algorithms

The Impure library (of Boulmé)

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.

Definitions and theorems used in many parts of the development

Source, intermediate and target languages: syntax and semantics