No description or website provided.
Clone or download
Latest commit 2602689 Oct 27, 2017
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
benchmark fix for most cases Oct 25, 2017
cfg fix parser error, add parser module test Oct 24, 2017
cmake add dockerfile and travis.ci file Jul 17, 2017
disj remove autotest script Oct 26, 2017
include fix for most cases Oct 25, 2017
parser fix parser error, add parser module test Oct 24, 2017
patch move patches Sep 4, 2017
scripts fix docker build, NOW OK Sep 4, 2017
src update @Linux May 6, 2017
test fix for most cases Oct 25, 2017
.gitignore update build system May 23, 2017
.travis.yml add dockerfile and travis.ci file Jul 17, 2017
CMakeLists.txt update @Linux Oct 27, 2017
Dockerfile remove autotest script Oct 26, 2017
LICENSE update latest zilu May 25, 2016
README.md update @Linux Sep 4, 2017
cmake.in fix docker build, NOW OK Sep 4, 2017
config.h.in update @Linux Oct 27, 2017
run update Sep 4, 2017

README.md

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.

WindowsUbuntuOS 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

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