Formal verification of ssa-based optimizations for llvm

Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, Steve Zdancewic

Research output: Contribution to journalArticlepeer-review

19 Scopus citations

Abstract

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.

Original languageEnglish (US)
Pages (from-to)175-186
Number of pages12
JournalACM SIGPLAN Notices
Volume48
Issue number6
DOIs
StatePublished - Jun 2013

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Keywords

  • Coq
  • LLVM
  • Single static assignment

Fingerprint Dive into the research topics of 'Formal verification of ssa-based optimizations for llvm'. Together they form a unique fingerprint.

Cite this