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

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 and code generation framework for floating point based peephole optimizations in LLVM. Alive-FP handles bit precise floating point optimizations and a class of fast-math optimizations involving signed zeros, not-a-number, and infinities. 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.Technical report DCS-TR-72