Termination-Checking for LLVM Peephole Optimizations
Termination-Checking for LLVM Peephole Optimizations
复制标题
LLVM 窥孔优化的终止检查
DOI:
--
复制
发表时间:
2016
期刊:
影响因子:
--
通讯作者:
Santosh Nagarakatte
中科院分区:
文献类型:
--
作者:
David Menendez;Santosh Nagarakatte
Mainstream compilers contain a large number of peephole optimizations, which perform algebraic simplification of the input program with local rewriting of the code. These optimizations are a persistent source of bugs. Our recent research on Alive, a domain-specific language for expressing peephole optimizations in LLVM, addresses a part of the problem by automatically verifying the correctness of these optimizations and generating C++ code for use with LLVM. This paper identifies a class of non-termination bugs that arise when a suite of peephole optimizations is executed until a fixed point. An optimization can undo the effect of another optimization in the suite, which results in non-terminating compilation. This paper (1) proposes a methodology to detect non-termination bugs with a suite of peephole optimizations, (2) identifies the necessary condition to ensure termination while composing peephole optimizations, and (3) provides debugging support by generating concrete input programs that cause non-terminating compilation. We have discovered 184 optimization sequences, involving 38 optimizations, that cause non-terminating compilation in LLVM with Alive-generated C++ code.