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

Formalization in Coq

• Gforge web page of the project: click here.

• Download the last stable version of the Coq development [.tgz] (tested with OCaml 4.01.0 and Coq 8.4pl2).

1. Extract the archive using tar xvzf
2. Compile compcertSSA (the project focuses on the x86 backend)

	cd compcertSSA
	./configure ia32-{your OS}
	make depend
	make all
      

3. Usage of compcertSSA

	cd compcertSSA
	./ccomp -ssa on [target]
      

Recent versions of Xcode (> 5.1.1) might require to invoke the compiler command with -D_VA_LIST flag.
4. Help on compcertSSA

	cd compcertSSA
	./ccomp --help
      

• Browsable version of the files specific to the SSA-based 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
  • RTL transformations, previous to SSA generation
    • CFG Normalisation (only a nop can lead to a junction point): RTLnorm RTLnormspec RTLnormproof
    • Unreachable code removal : RTLdfs RTLdfsproof
  • SSA form: definition and validation
    • Syntax and semantics (3-address code, CFGs, infinitely many indexed pseudo-registers): SSA
    • Generation algorithm: SSAgen SSAgenproof
    • SSA generation validation : SSAvalid SSAvalidspec SSAvalidproof
  • SSA properties and libraries:
    • Equational lemma: SSAtoolinv
    • 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
  • Destruction of the SSA form back to RTL : DeSSA DeSSAspec DeSSAproof
    • The enhanced destruction via CSSA will be integrated in the next release. In the meantime, see here.