Formal verification of SSA-based optimizations for LLVM

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

35 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 technique for proving SSA-based program invariants and compiler optimizations. We use this technique in the Coq proof assistant to create mechanized correctness proofs of several "micro" transformations that form the building blocks for larger SSA optimizations. To demonstrate the utility of this approach, we formally verify a variant 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)
Title of host publicationPLDI 2013 - Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation
Pages175-186
Number of pages12
DOIs
StatePublished - 2013
Event34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013 - Seattle, WA, United States
Duration: Jun 16 2013Jun 19 2013

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Other

Other34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013
CountryUnited States
CitySeattle, WA
Period6/16/136/19/13

All Science Journal Classification (ASJC) codes

  • Software

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