zilu is an open source invariant inference Framework

zilu is named after a disciple of Confucius. zilu has been tested on Ubuntu 14.04 x64. It should work on other Linux platfroms, but we have not tested yet.

Windows	Ubuntu	OS X
TBD		TBD

zilu Installation on local computer

pre-requirement (most of the package can be installed with apt-get on Ubuntu)

• apt-get install git cmake flex bison clang z3 libz3-dev libgsl0-dev
  • git
  • cmake version 2.8 or later
  • flex version 2.6.1 or later
  • bison version 2.6.0 or later
  • clang
  • z3 is applied to check the smt-constraints generated by KLEE.
  • GSL This library is used to solve equations in our project.

• "make" and otherLLVM essential building tools, you can add if needed
• KLEE only test llvm2.9 yet, so try to build KLEE by build-llvm29.
  • If you can not build KLEE with the above instruction, maybe you can refer to
    • link1
    • link2.

Get the latest zilu

git clone https://github.com/lijiaying/zilu.git
cd zilu

Patch KLEE source code

This modification aims at generating smt2 file for each path condition. We mainly add new method calls ``klee_fail && klee_pass'', as we would like to output the path condition to files in these method calls.

• patch/klee.6609a03.patch is the patch file. It should be applied to KLEE with commit signature 6609a03e68bf551f433ddd0fd8cf64a8683ee2ee, the short SHA: 6609a03.
• Change to Klee with commit 6609a03.
  • git checkout 6609a03
• Apply the patch
  • git apply ${zilu-home}/patch/klee.6609a03.patch
• Rebuild and install the patched KLEE.
  • make ENABLE_OPTIMIZED=1
  • sudo make install
• After patching KLEE, it is OK that several tests of KLEE might be failed. Just ignore them as long as the make return 0.

build parser

mkdir -p build/parser
cd build/parser
cmake ../../parser
make
cd ../..

Test zilu

./run benchmark/35.cfg

Try zilu from docker hub

docker pull lijiaying/zilu

Enjoy your tour with our Invariant Inference Framework: zilu