Alive: Automatic LLVM's Instcombine Verifier
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
llvm-pass replace InstructionCombining.cpp and InstCombineInternal.h, for using… May 19, 2017
pyparsing initial commit Jun 11, 2014
tests add 2 regression tests for bugs found with Alive May 30, 2015
.gitignore minor cleanups Jun 12, 2014
AUTHORS Add a script that can run multiple copies of alive in parallel Mar 3, 2018
LICENSE Initial commit Jun 11, 2014
README.md Add link to rise4fun.com Jan 5, 2017
TODO bug fixes to new --use-array-th option. still not ready. Mar 31, 2015
alive.py
codegen.py add copyright header Apr 2, 2015
common.py add a --new-sema cmd argument May 23, 2015
constants.py make codegenerator work with latest llvm version (svn rev 303414 tested) May 19, 2017
gen.py make codegenerator work with latest llvm version (svn rev 303414 tested) May 19, 2017
language.py add a --new-sema cmd argument May 23, 2015
parallel-alive.py
parser.py Add a script that can run multiple copies of alive in parallel Mar 3, 2018
precondition.py make codegenerator work with latest llvm version (svn rev 303414 tested) May 19, 2017
pretty.py
run-tests.sh
value.py reimplement the default memory vcgen around the same API as the one u… Apr 6, 2015

README.md

Alive: Automatic LLVM's Instcombine Verifier

Alive is a tool that can prove the correctness of InstCombine optimizations specified in a high-level language.

Requirements

Alive requires Python 2.7.x and Z3 4.3.2 (or later), which can be obtained from https://github.com/Z3Prover/z3 (use the unstable branch)

Usage

./alive.py file.opt

The 'tests' directory has multiple examples of optimizations.

More Information

Please see this paper for more details about Alive:

http://www.cs.utah.edu/~regehr/papers/pldi15.pdf

Online Version

Alive is also available online at: http://rise4fun.com/Alive

Generating Benchmarks

Alive will automatically generate benchmarks in SMT-LIB 2 format when the 'bench' directory exists and when python is run in non-optimized mode (the default). These benchmarks are over the bit-vector theory and may or may not have quantifiers.