Mechanizing Conventional SSA for
a Verified Destruction with Coalescing

Paper

Mechanizing Conventional SSA for a Verified Destruction with Coalescing. D. Demange and Y. Fernandez de Retana. CC'16. preprint pdf

Source code

Download the corresponding Coq development snapshot.

CompCertSSA main web page.

Main files

• midend/CSSApar.v: CSSA syntax and semantics
• midend/CSSApargen.v: CSSA generation
• midend/CSSApargenspec.v: CSSA generation specification
• midend/CSSApargenproof.v: CSSA generation semantics preservation
• midend/CSSApargenwf.v: CSSA generation well-formedness propreties
• midend/CSSAlive.v: CSSA live-range properties
• midend/RTLpar.v: RTLpar syntax and semantics
• midend/RTLpargensimpl.v: Simple destruction: just elimination of phi-functions (implementation)
• midend/CSSAliverange.v: for simple destruction: live-range splitting property
• midend/CSSAsimpldestruction.v: Simple destruction: semantics preservation proof
• midend/RTLpargen.v: Destruction with coalescing (implementation)
• midend/CSSAval.v: CSSA-value properties and checker
• midend/CSSAninterf.v: Non-interference properties
• midend/CSSAcoalescing.v: Destruction with coalescing: semantics preservation proof

Experiments

The version of Coq used in this work is version 8.4pl6 (April 2015) compiled with OCaml 4.02.2.

1. Unzip the archive
2. Compile compcertSSA

             cd coalescing
             ./configure ia32-linux  # or ia32-macosx, etc...
             make depend
             make all

3. Run experiments (after having compiled compcertSSA)

             cd test (if necessary)
             make coalescing
             make spilling

   Then each subfolder of "test" will contain files with results named results_coalescing.out and results_spilling.out for each test.