Alive-FP: Automated verification of floating point based peephole optimizations in LLVM

David Menendez, Santosh Nagarakatte, Aarti Gupta

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

16 Scopus citations


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 opti- mizations, automatically verifies the correctness of integer-based peep- hole optimizations and generates C++ code for use within LLVM. This paper proposes Alive-FP, an automated verification framework for float- ing point based peephole optimizations in LLVM. Alive-FP handles a class of floating point optimizations and fast-math optimizations involv- ing 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.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 23rd International Symposium, SAS 2016, Proceedings
EditorsXavier Rival
PublisherSpringer Verlag
Number of pages21
ISBN (Print)9783662534120
StatePublished - 2016
Event23rd International Symposium on Static Analysis, SAS 2016 - Edinburgh, United Kingdom
Duration: Sep 8 2016Sep 10 2016

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9837 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other23rd International Symposium on Static Analysis, SAS 2016
Country/TerritoryUnited Kingdom

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Alive-FP: Automated verification of floating point based peephole optimizations in LLVM'. Together they form a unique fingerprint.

Cite this