Alive2 ======
Alive2 consists of several libraries and tools for analysis and verification of LLVM code and transformations. Alive2 includes the following libraries:
- Alive2 IR
- Symbolic executor
- LLVM → Alive2 IR converter
- Refinement check (aka optimization verifier)
- SMT abstraction layer
Included tools:
- Alive drop-in replacement
- Translation validation plugins for clang and LLVM's opt
- Standalone translation validation tool: alive-tv (online)
- Clang drop-in replacement with translation validation (alivecc and
alive++)
- An LLVM IR interpreter that is UB precise (alive-exec)
For a technical introduction to Alive2, please see our paper from PLDI 2021.
WARNING ------- Alive2 does not support inter-procedural transformations. Alive2 may produce spurious counterexamples if run with such passes.
Sponsors -------- We thank the continuous support of all of our sponsors! Alive2 wouldn't be possible without their support.
[](https://nlnet.nl) [](https://woven.toyota) [](https://matter-labs.io)
If your company has benefitted from Alive2 (including having a less buggy LLVM), please consider sponsoring our research lab.
Prerequisites ------------- To build Alive2 you need recent versions of:
- cmake
- gcc/clang
- re2c
- Z3
- LLVM (optional)
- hiredis (optional, needed for caching)
Building --------
git clone git@github.com:AliveToolkit/alive2.git
cd alive2
mkdir build
cd build
cmake -GNinja -DCMAKE_BUILD_TYPE=Release ..
ninjaIf CMake cannot find the Z3 include directory (or finds the wrong one) pass the -DZ3INCLUDEDIR=/path/to/z3/include and -DZ3LIBRARIES=/path/to/z3/lib/libz3.so arguments to CMake.
Building and Running Translation Validation --------