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):
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) |