CompCertSSA
A companion web page

CompCertSSA is built on top of the C CompCert verified compiler, by adding a SSA-based middle-end (conversion to SSA, SSA-based optimizations, destruction of SSA). This web page reports only on the parts of the development specific to this SSA middle-end. The complete development is available below.

Papers

• A formally verified SSA-based middle-end. G. Barthe, D. Demange, and D. Pichardie. ESOP 2012.
• Formal Verification of an SSA-based Middle-end for CompCert. G. Barthe, D. Demange, and D. Pichardie. ACM TOPLAS 2014.
• Verifying Fast and Sparse SSA-based Optimizations in Coq. D. Demange, D. Pichardie and L. Stefanesco. CC 2015. more
• Validating Dominator Trees for a Fast, Verified Dominance Test. S. Blazy, D. Demange and D. Pichardie. ITP 2015. more
• Mechanizing Conventional SSA for a Verified Destruction with Coalescing. D. Demange and Y. Fernandez de Retana. CC 2016. more
• A Fast Verified Liveness Analysis in SSA Form. JC. Léchenet, S. Blazy, D. Pichardie. IJCAR 2020. more

Coq Formalization

• Project, and releases

  Access the Gitlab project here, or get the latest release.

• CompCertSSA quick start

  1. Compiling CompCertSSA follows the same process as for CompCert (see manual).
  2. Usage of CompCertSSA: same as CompCert, but with the -ssa option, e.g. ./ccomp -ssa on [target]
  3. Help on CompCertSSA: same as CompCert, with ./ccomp --help

• Browsable version of files specific to the SSA middle-end.

  Below is a commented listing of the underlying Coq specifications and proofs. Proof scripts folded by default, to unfold, click on "Proof".

  • The whole compilation chain, with middle-end plugged in: Compiler Complements
  • RTL transformations, previous to SSA generation
    • CFG Normalisation (only a nop can lead to a junction point): RTLnorm RTLnormspec RTLnormproof
    • Unreachable code removal, and computation of a DFS traversal: RTLdfs RTLdfs RTLdfsproof
  • SSA form: definition and validation
    • Syntax and semantics (3-address code, CFGs, infinitely many pseudo-registers): SSA
    • Generation algorithm, using a posteriori validation: SSAvalid SSAvalidspec SSAvalidproof
  • SSA properties and libraries:
    • Equational lemma: SSAinv
    • Dominance libraries: Dom Dsd
  • Optimizations :
    • Common framework for dominance based optimizations: Opt OptInv
    • Sparse Conditional Constant Propagation SCCPopt SCCPoptProp SCCPoptProof
    • SSA-based Global Value Numbering GVNopt GVNoptProp GVNoptProof
  • CSSA form (Conventional SSA) :
    • Syntax and semantics: CSSA
    • Property of split live ranges: CSSAliverange
    • Generating CSSA, using a posteriori validation: CSSAgen CSSAgenspec CSSAproof
  • RTLpar, RTL with parallel-copy blocks:
    • Syntax and semantics: RTLpar
    • Generation from CSSA of RTLpar: RTLpargen RTLparproof
  • Deparallelization of copy-blocks, from RTLpar to RTL: RTLdpar RTLdparspec RTLdparproof