Termination-checking for LLVM peephole optimizations

Abstract

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.

BibTeX

@inproceedings{Menendez-Nagarakatte:ICSE16,
  author    = {David Menendez and
               Santosh Nagarakatte},
  title     = {Termination-checking for {LLVM} peephole optimizations},
  booktitle = {ICSE},
  pages     = {191--202},
  publisher = {{ACM}},
  year      = {2016},
}

Termination-checking for LLVM peephole optimizations

Abstract

Related papers