Wiki
Clone wikiDIG2 / Home
DIG2 (or NumInv) is a tool for generating numerical invariants using the KLEE symbolic execution tool. Currently DIG3 supports C programs.
Setup
DIG2 is written in Python using the SAGE mathematics system. Candidate invariants are checked using KLEE. Other verification tasks are done using the Z3 SMT solver. The tool has been tested using the following setup:
- Debian Linux 8 (64 bit)
- SageMath 7.5.1
- Microsoft Z3 SMT solver 4.5.x
- KLEE 1.3.0.0
Obtain DIG2
git clone https://nguyenthanhvuh@bitbucket.org/nguyenthanhvuh/dig2/
Installing SAGE and Z3
- Setup SAGE: download a precompiled SageMath binary
- Setup Z3: download and build Z3 by following the instructions in the README file
Installing KLEE
- Build KLEE using these instructions
- Important: build KLEE with Z3 support !
#!shell #command to build klee cmake -DENABLE_SOLVER_Z3=ON -DENABLE_SOLVER_STP=OFF -DENABLE_POSIX_RUNTIME=ON -DENABLE_KLEE_UCLIBC=ON -DENABLE_UNIT_TESTS=OFF -DENABLE_SYSTEM_TESTS=OFF -DKLEE_UCLIBC_PATH=/home/tnguyen/Src/Devel/KLEE/klee-uclibc /home/tnguyen/Src/Devel/KLEE/klee
Setup Paths
- Put the following in your
~/.bash_profile
. Adjust the directory paths to the ones you used.#!shell # ~/.bash_profile export Z3=PATH/TO/z3 #Z3 dir export SAGE=PATH/TO/sage #where your SAGE dir is export SAGE_PATH=$Z3/src/api/python export KLEE=$DEVEL/KLEE/ export PATH=$KLEE/klee_build_dir/bin:$SAGE:$PATH
- Make sure SAGE works, e.g., use
sage
to run the SAGE interpreter orsage --help
- Make sure Z3 is installed correctly so that you can do
sage -c "import z3"
without error. - Make sure KLEE works, e.g., `klee --help | grep z3' should say something that Z3 is the default solver
Other miscs installations
- astyle: do a
apt-get install astyle
Usage
Here are some usage examples of DIG2. The following assumes we are currently in the dig2
directory.
Generating invariants
#!shell $ sage -python -O dig2.py programs/nla/cohendiv.c 15:47:38:alg:Info:analyze programs/nla/cohendiv.c 15:47:38:alg:Info:set seed to: 1495658857.7 (test 12) 15:47:38:miscs:Info:autodeg 3 15:47:38:alg:Info:check reachability 15:47:38:alg:Info:gen eqts at 2 locs: l37 (int x, int y, int r, int q, int a, int b); l25 (int x, int y, int q, int a, int b, int r) 15:48:4:alg:Info:gen eqts: (25.3289949894s) 15:48:4:alg:Info:4 invs: l37: a*y - b == 0, q*y + r - x == 0 l25: a*y - b == 0, q*y + r - x == 0 15:48:4:alg:Info:gen ieqs at 2 locs: l37 (int x, int y, int r, int q, int a, int b); l25 (int x, int y, int q, int a, int b, int r) 15:48:4:alg:Info:2 locs: check upperbounds for 144 terms (range 10) 15:48:25:alg:Info:gen ieqs: (21.7538409233s) 15:48:25:alg:Info:63 invs: l37: -r - y <= -1, b - x <= 0, -b - r <= -1, -q - r <= -1, -r - x <= -1, -a - x <= -1, q - x <= 0, -r <= 0, a - x <= 0, -q - x <= -1, -a - y <= -2, a - b <= 0, r - x <= 0, r - y <= -1, -b <= 0, a - q <= 0, -q <= 0, -a - q <= 0, -y <= -1, -x <= -1, -a - b <= 0, -a - r <= -1, -b - q <= 0, -b - y <= -2, -a <= 0, -x - y <= -2, -b - x <= -1, -q - y <= -2, a*y - b == 0, q*y + r - x == 0 l25: a - x <= 0, -b + y <= 0, -r <= -1, -r - x <= -2, q - x <= -1, -a - y <= -2, -b - x <= -2, -q - y <= -1, -b - q <= -1, b - r <= 0, -x - y <= -2, a - r <= 0, a - b <= 0, -a <= -1, -b <= -1, -a - b <= -2, -b - y <= -2, -r + y <= 0, -q <= 0, -x <= -1, -q - x <= -1, r - x <= 0, -x + y <= 0, -a - x <= -2, -b - r <= -2, -q - r <= -1, -r - y <= -2, b - x <= 0, -a - q <= -1, -a - r <= -2, -y <= -1, a*y - b == 0, q*y + r - x == 0 15:48:25:alg:Info:test 63 invs on all 1622 traces 15:48:29:alg:Info:find uniq invs 15:48:29:alg:Info:63 invs: l37: -r - y <= -1, b - x <= 0, -b - r <= -1, -q - r <= -1, -r - x <= -1, -a - x <= -1, q - x <= 0, -r <= 0, a - x <= 0, -q - x <= -1, -a - y <= -2, a - b <= 0, r - x <= 0, r - y <= -1, -b <= 0, a - q <= 0, -q <= 0, -a - q <= 0, -y <= -1, -x <= -1, -a - b <= 0, -a - r <= -1, -b - q <= 0, -b - y <= -2, -a <= 0, -x - y <= -2, -b - x <= -1, -q - y <= -2, a*y - b == 0, q*y + r - x == 0 l25: a - x <= 0, -b + y <= 0, -r <= -1, -r - x <= -2, q - x <= -1, -a - y <= -2, -b - x <= -2, -q - y <= -1, -b - q <= -1, b - r <= 0, -x - y <= -2, a - r <= 0, a - b <= 0, -a <= -1, -b <= -1, -a - b <= -2, -b - y <= -2, -r + y <= 0, -q <= 0, -x <= -1, -q - x <= -1, r - x <= 0, -x + y <= 0, -a - x <= -2, -b - r <= -2, -q - r <= -1, -r - y <= -2, b - x <= 0, -a - q <= -1, -a - r <= -2, -y <= -1, a*y - b == 0, q*y + r - x == 0 15:48:30:alg:Info:*** programs/nla/cohendiv.c, 2 locs, invs 14, inps 234, time 52.1688649654 s, rand 16: l37: a - q <= 0, q*y + r - x == 0, -b <= 0, r - y <= -1, -r <= 0, -a - r <= -1, a*y - b == 0 l25: -b + y <= 0, q*y + r - x == 0, a - b <= 0, b - r <= 0, -a - y <= -2, r - x <= 0, a*y - b == 0
Here DIG3 discovers the equality invariants a*y = b, q*y + r = x
and other inequalities at the locations marked with //%%%traces
from the program programs/nla/cohenDiv.c
below:
#!C int cohendiv(int x, int y){ //Cohen's integer division that returns x % y assert(x>0 && y>0); int q=0; int r=x; while(1){ if (!(r>=y)) break; int a=1; int b=y; while(1){ //traces: int q, int r, int a, int b, int x, int y if (!(r >= 2*b)) break; a = 2*a; b = 2*b; } r=r-b; q=q+a; } //%%%traces: int q, int r, int a, int b, int x, int y return q; }
Other programs
The directory ../programs/nla/
contains many programs having such nonlinear invariants.
Publications
Additional information on DIG can be found from these papers: * ThanhVu Nguyen, Timos Antopoulos, Andrew Ruef, and Michael Hicks. A Counterexample-guided Approach to Finding Numerical Invariants. In Foundations of Software Engineering (FSE), page (to appear). ACM, 2017
Others
- Benchmarks are in subdirectory "programs" (nla, complexity, and hola)
- Results are in "fse17_results". These are logs, which we use collect_results.py to extract stats such as mean #'s of invs, time, etc
Updated