Formalizing the LLVM intermediate representation for verified program transformations. This paper presents Vellvm (verified LLVM), a framework for reasoning about programs expressed in LLVM’s intermediate representation and transformations that operate on it. Vellvm provides a mechanized formal semantics of LLVM’s intermediate representation, its type system, and properties of its SSA form. The framework is built using the Coq interactive theorem prover. It includes multiple operational semantics and proves relations among them to facilitate different reasoning styles and proof techniques.par To validate Vellvm’s design, we extract an interpreter from the Coq formal semantics that can execute programs from LLVM test suite and thus be compared against LLVM reference implementations. To demonstrate Vellvm’s practicality, we formalize and verify a previously proposed transformation that hardens C programs against spatial memory safety violations. Vellvm’s tools allow us to extract a new, verified implementation of the transformation pass that plugs into the real LLVM infrastructure; its performance is competitive with the non-verified, ad-hoc original.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
- Felty, Amy P.; Momigliano, Alberto; Pientka, Brigitte: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey (2015)
- Schneider, Sigurd; Smolka, Gert; Hack, Sebastian: A linear first-order functional intermediate language for verified compilers (2015)
- Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter: Proving termination and memory safety for programs with pointer arithmetic (2014)
- Zhao, Jianzhou; Nagarakatte, Santosh; Martin, Milo M.K.; Zdancewic, Steve: Formalizing the LLVM intermediate representation for verified program transformations (2012)
- Zhao, Jianzhou; Zdancewic, Steve: Mechanized verification of computing dominators for formalizing compilers (2012)