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.
- 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
- Verifying Fast and Sparse SSA-based Optimizations in
Coq. D. Demange, D. Pichardie and L. Stefanesco. CC 2015.
- Validating Dominator Trees for a Fast, Verified Dominance Test.
S. Blazy, D. Demange and D. Pichardie. ITP 2015.
- Mechanizing Conventional SSA for a Verified Destruction with
Coalescing. D. Demange and Y. Fernandez de Retana. CC 2016.
Project, and releases
Access the Gitlab project here, or
get the latest release.
CompCertSSA quick start
- Compiling CompCertSSA follows the same process as for
- Usage of CompCertSSA: same as CompCert, but with
-ssa option, e.g.
./ccomp -ssa on [target]
- Help on CompCertSSA: same as CompCert, with
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
- RTL transformations, previous to SSA generation
- SSA form: definition and validation
- SSA properties and libraries:
- Optimizations :
- CSSA form (Conventional SSA) :
- RTLpar, RTL with parallel-copy blocks:
- Deparallelization of copy-blocks, from RTLpar to RTL: