Skip to main content

Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM

Author(s): Menendez, David; Nagarakatte, Santosh; Gupta, Aarti

To refer to this page use:
Abstract: Peephole optimizations optimize and canonicalize code to enable other optimizations but are error-prone. Our prior research on Alive, a domain-specific language for specifying LLVM’s peephole optimizations, automatically verifies the correctness of integer-based peephole optimizations and generates C++ code for use within LLVM. This paper proposes Alive-FP, an automated verification framework for floating point based peephole optimizations in LLVM. Alive-FP handles a class of floating point optimizations and fast-math optimizations involving signed zeros, not-a-number, and infinities, which do not result in loss of accuracy. This paper provides multiple encodings for various floating point operations to account for the various kinds of undefined behavior and under-specification in the LLVM’s language reference manual. We have translated all optimizations that belong to this category into Alive-FP. In this process, we have discovered seven wrong optimizations in LLVM.
Publication Date: 2016
Citation: Menendez, David, Santosh Nagarakatte, and Aarti Gupta. "Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM." In International Static Analysis Symposium (2016): pp. 317-337. doi:10.1007/978-3-662-53413-7_16
DOI: 10.1007/978-3-662-53413-7_16
ISSN: 0302-9743
EISSN: 1611-3349
Pages: 317 - 337
Type of Material: Conference Article
Journal/Proceeding Title: International Static Analysis Symposium
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.