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 |
Cminor to CminorSel | Selection SelectOp SelectDiv SelectLong |
Selectionproof SelectOpproof SelectDiv SelectLongproof |
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 |
Constant propagation | RTL to RTL | Constprop ConstpropOp |
Constpropproof ConstproppOproof |
Common subexpression elimination | RTL to RTL | CSE CombineOp |
CSEproof CombineOpproof |
Redundancy elimination | RTL to RTL | Deadcode | Deadcodeproof |
Removal of unused static globals | RTL to RTL | Unusedglob | Unusedglobproof |
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 |
Laying out the activation records | Linear to Mach | Stacking Bounds Stacklayout |
Stackingproof |
Emission of assembly code | Mach to Asm | Asmgen | Asmgenproof0 Asmgenproof1 Asmgenproof |