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
- Compiling CompCertSSA follows the same process as for
CompCert (see
manual).
- Usage of CompCertSSA: same as CompCert, but with
the
-ssa
option, e.g.
./ccomp -ssa on [target]
- 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
- 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:
RTLdpar
RTLdparspec
RTLdparproof