May 7-10, 2017 Asilomar, California
Lightweight formal methods for LLVM verification
Santosh Nagarakatte
Peephole optimizations perform local algebraic simplifications to improve the efficiency of the code input to the compiler. These optimizations are a persistent source of bugs. The talk will present domain specific languages (DSL) in the Alive-NJ tool kit to verify both integer and floating point based peephole optimizations in LLVM. The talk will briefly highlight the challenges in handling the ambiguities in the LLVM's semantics. A transformation expressed in these DSLs is shown to be correct by automatically encoding it as constraints whose validity is checked using a satisfiability modulo theory (SMT) solver. Furthermore, an optimization expressed in the DSL can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. The talk will also highlight our recent results and future directions on data driven precondition inference for these optimizations, which will be useful while debugging an incorrect optimization.