TY - GEN
T1 - Alive-FP
T2 - 23rd International Symposium on Static Analysis, SAS 2016
AU - Menendez, David
AU - Nagarakatte, Santosh
AU - Gupta, Aarti
N1 - Publisher Copyright:
© Springer-Verlag GmbH Germany 2016.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84988369706&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84988369706&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-53413-7_16
DO - 10.1007/978-3-662-53413-7_16
M3 - Conference contribution
AN - SCOPUS:84988369706
SN - 9783662534120
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 317
EP - 337
BT - Static Analysis - 23rd International Symposium, SAS 2016, Proceedings
A2 - Rival, Xavier
PB - Springer Verlag
Y2 - 8 September 2016 through 10 September 2016
ER -