The CompCert verified compiler

Commented Coq development

Version 3.8, 2020-11-16

PATCHED for the Kalray MPPA-KVX VLIW CORE (2021-04-16)

Introduction

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 this OOPSLA'20 paper (of Six, Boulmé and Monniaux):

Certified and Efficient Instruction Scheduling. Application to Interlocked VLIW Processors.

See also the README.md of our GitLab public repository.

Table of contents

General-purpose libraries, data structures and algorithms

The abstractbb library, introduced for KVX core

Definitions and theorems used in many parts of the development

Source, intermediate and target languages: syntax and semantics

Languages introduced for KVX core

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
Function inlining RTL to RTL Inlining Inliningspec
Inliningproof
Postorder renumbering of the CFG RTL to RTL Renumber Renumberproof
Common subexpression elimination RTL to RTL CSE
CombineOp
CSEproof
CombineOpproof
Constant propagation RTL to RTL Constprop
ConstpropOp
Constpropproof
ConstproppOproof
Redundancy elimination RTL to RTL Deadcode Deadcodeproof
Removal of unused static globals RTL to RTL Unusedglob Unusedglobproof
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
Passes introduced for superblock prepass scheduling
Code duplications (trace selection, loop unrollings, etc) RTL to RTL Duplicate (generic checker) Duplicateproof (generic proof)
Duplicatepasses (several passes from several oracles)
Superblock selection (with Liveness information) RTL to RTLPath RTLpathLivegen RTLpathLivegenproof
Superblock prepass scheduling RTLPath to RTLPath RTLpathScheduler RTLpathSchedulerproof
with RTLpathSE_theory (the theory of symbolic execution on RTLpath)
and RTLpathSE_simu_specs (the low-level specifications of the simulation checker)
and RTLpathSE_impl (the simulation checker with hash-consing)
Forgeting superblocks RTLPath to RTL RTLpath.transf_program RTLpathproof
Passes from register allocation
Register allocation (validation a posteriori) RTL to LTL Allocation Allocproof
Branch tunneling LTL to LTL Tunneling Tunnelingproof
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 KVX VLIW
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
Flattening bundles (only a bureaucratic operation) Asmvliw to Asm Asmgen Asmgenproof (whole simulation proof from Mach to Asm)

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

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.

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.