Modern compilers, such as LLVM and GCC, use a static single assignment (SSA) intermediate representation (IR) to simplify and enable many advanced optimizations. However, formally verifying the correctness of SSA-based optimizations is challenging because SSA properties depend on a function's entire control-flow graph. This paper addresses this challenge by developing a proof tech- nique for proving SSA-based program invariants and compiler op- timizations.We use this technique in the Coq proof assistant to cre- ate mechanized correctness proofs of several "micro" transforma- tions that form the building blocks for larger SSA optimizations. To demonstrate the utility of this approach, we formally verify a vari- ant of LLVM's mem2reg transformation in Vellvm, a Coq-based formal semantics of the LLVM IR. The extracted implementation generates code with performance comparable to that of LLVM's unverified implementation.
All Science Journal Classification (ASJC) codes
- Computer Science(all)
- Single static assignment