Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM
Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM
复制标题
Alive-FP：LLVM 中基于浮点的窥孔优化的自动验证
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Aarti Gupta
中科院分区：
文献类型：
--
作者：
David Menendez;Santosh Nagarakatte;Aarti Gupta
窥视孔优化优化和规范化代码以启用其他优化，但容易出错。我们之前对Alive（一种用于指定LLVM窥视孔优化的特定于域的语言）的研究，自动验证基于整数的窥视孔优化的正确性，并生成用于LLVM的C++代码。本文提出了Alive-FP，一个自动验证框架，用于LLVM中基于浮点的窥视孔优化。Alive-FP处理一类浮点优化和快速数学优化，涉及有符号零、非数字和无穷大，不会导致精度损失。本文为各种浮点运算提供了多种编码，以解决LLVM语言参考手册中各种未定义行为和未规范的问题。我们已经将属于这一类别的所有优化转换为Alive-FP。在这个过程中，我们发现了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 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.