ALIVe: Automatic LLVM's Instcombine Verifier
Python Shell C++ Makefile Other
Switch branches/tags
Nothing to show
Clone or download
Pull request Compare This branch is 235 commits ahead of davemenendez:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
llvm-pass
logutils
looptests
pyparsing
tests
.gitignore
AUTHORS
LICENSE
README.md
TODO
TODO_LOOPS
alive.py
codegen.py
common.py
constants.py
debug_count.py
debug_count3.py
debug_loops.py
debug_sequence.py
find-loops.py
find-simple-loops.py
find_random_loops.py
fsl.py
gen.py
language.py
loops.py
master.opt
parser.py
precondition.py
pretty.py
problems.opt
run-tests.sh
safemaster.opt
sample_prefixes.py
subsets.py
test_loops.py
value.py

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.

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.