Control-flow cut based Learning framework
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
benchmark
cfg
cmake
include
parser
patch
pc
scripts
src
.gitignore
.travis.yml
Dockerfile
LICENSE
README.md
cmake.in
config.h.in
run

README.md

zimu is an open source learning framework for inferring complex invariant

zimu is an invariant inference framework which integrates program cfg information with loop invariant procedure. The talented author came up with the idea and this implementation during his desperate year for his PhD. This will enlighten many other researchers to adapt the idea to get some other invariant forms, array, string for example.

WindowsUbuntuOS X
TBD TBD

Installation

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 zimu

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

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
  • patch KLEE.
    • git apply ${zimu-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 zimu

./run.sh add

Try zimu from docker hub

docker pull lijiaying/zimu

Enjoy your tour with our Invariant Inference Framework: zimu