Termination-Checking for LLVM Peephole Optimizations

Termination-Checking for LLVM Peephole Optimizations
复制标题

LLVM 窥孔优化的终止检查

DOI:
--
复制
发表时间:
2016
期刊:
International Conference on Software Engineering
影响因子:
--
通讯作者:
Santosh Nagarakatte
Santosh Nagarakatte
中科院分区:
--
文献类型:
--
作者:
David Menendez;Santosh Nagarakatte

文献摘要

被引文献

相似文献

主流编译器包含大量的窥视孔优化,通过本地重写代码对输入程序进行代数简化。这些优化是错误的持续来源。我们对Alive的最新研究是一种针对LLVM中窥视孔优化的特定领域的语言,它通过自动验证这些优化的正确性并生成用于LLVM的C ++代码来解决问题的一部分。本文确定当执行一套窥视孔优化直到固定点时会出现的一类非终止错误。优化可以消除套件中另一种优化的效果,从而导致不终止汇编。本文(1)提出了一种方法来检测具有窥视孔优化套件的非终止错误,(2)确定了必要条件,以确保终止时终止窥视孔时,并且(3)通过生成混凝土输入程序来提供调试支持非终止汇编。我们发现了184个优化序列,涉及38个优化,这些序列在LLVM中引起了活着生成的C ++代码的非终止汇编。
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.