Clone wiki

symtraces / Home

DIG3 (or SymInfer) is a tool for generating numerical invariants using symbolic states extracted from a symbolic execution tool. By default DIG3 works with Java program. DIG3 also supports C programs but it directly uses a symbolic execution tool instead of symbolic traces.

Setup

DIG3 is written in Python using the SAGE mathematics system. Symbolic states are obtained using Symbolic PathFinder. All 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 For Java programs
  • JPF/SPF
  • Oracle Java JDK 1.8.0_121

Obtain DIG3 (SymInfer)

git clone https://nguyenthanhvuh@bitbucket.org/nguyenthanhvuh/symtraces.git

Installing SAGE and Z3

  • Setup SAGE: download a precompiled SageMath binary
  • Setup Z3: download and build Z3 by following the instructions in its README file
  • To check that you have all needed stuff: run
$ sage check_requirements.py
...
...
Everything seems OK. Have fun with DIG!

For JAVA programs: Installing JPF (and Java)

  • Install Oracle Java JDK
  • Install JPF
mkdir /PATH/TO/JPF; cd /PATH/TO/JPF
hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-core  #JPF
hg clone http://babelfish.arc.nasa.gov/hg/jpf/jpf-symbc #Symbolic extension

#then add the following to `~/.jpf/site.properties` (create ~/.jpf if it doesn't exist)
jpf-core = /PATH/TO/JPF/jpf-core
jpf-symbc = /PATH/TO/JPF/jpf-symbc
extensions=${jpf-core},${jpf-symbc}


#copy patched file
cp /PATH/TO/symtraces/InvariantListenerVu.java jpf-symbc/src/main/gov/nasa/jpf/symbc

#build jpf
cd jpf-core
ant  
#build spf
cd ..
cd jpf-symbc
ant

Setup Paths

  • Put the following in your ~/.bash_profile
# ~/.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 JAVA_HOME=/PATH/TO/JAVA
export PATH=$SAGE:$JAVA_HOME/bin:$PATH
export JPF_HOME=/PATH/TO/JPF

#for C programs
export KLEE=$DEVEL/KLEE/
export PATH=$KLEE/klee_build_dir/bin:$SAGE:$PATH
  • Make sure SAGE works, e.g., sage to run the SAGE interpreter or sage --help
  • Make sure Z3 is installed correctly so that you can do sage -c "import z3; z3.get_version()" without error.

Other installations

  • astyle: do a apt-get install astyle

Usage

Here are some usage examples of DIG3. The following assumes we are currently in the symtraces directory.

Generating invariants

$ sage -python -O dig.py programs/nla/CohenDiv.java 
22:15:39:alg:Info:analyze programs/nla/CohenDiv.java
22:15:39:alg:Info:seed to: 1495077335.48 (test 85)
22:15:39:miscs:Info:autodeg 3
...
22:15:45:alg:Info:check reachability
22:15:45:alg:Info:gen eqts at 2 locs: 21 (int q, int r, int a, int b, int x, int y); 30 (int x, int y, int q, int r)
22:16:0:alg:Info:gen eqts: (14.8545670509s)
22:16:0:alg:Info:3 invs:
21: q*y + r - x == 0, a*y - b == 0
30: q*y + r - x == 0
22:16:0:alg:Info:gen ieqs at 2 locs: 21 (int q, int r, int a, int b, int x, int y); 30 (int x, int y, int q, int r)
...
22:16:11:alg:Info:47 invs:
21: a*y - b == 0, q*y + r - x == 0, -q - x <= -1, -r + y <= 0, -r - y <= -2, -a <= -1, a - x <= 0, -a - q <= -1, -r - x <= -2, r - x <= 0, -x <= -1, -y <= -1, -r <= -1, -a - y <= -2, -q <= 0, -b - r <= -2, -q - r <= -1, -x - y <= -2, -x + y <= 0, a - r <= 0, -a - r <= -2, b - r <= 0, -b + y <= 0, -b - y <= -2, -b - x <= -2, b - x <= 0, -q - y <= -1, -b <= -1, -b - q <= -1, -a - x <= -2, a - b <= 0, q - x <= -1, -a - b <= -2
30: q*y + r - x == 0, -q - r <= -1, -q - x <= -1, q - x <= 0, -q - y <= -2, -r - y <= -1, -r <= 0, r - y <= -1, -r - x <= -1, r - x <= 0, -x <= -1, -q <= 0, -y <= -1, -x - y <= -2
22:16:13:alg:Info:*** programs/nla/CohenDiv.java, 2 locs, invs 11, inps 82, time 34.1111209393 s, rand 67: 
21: q*y + r - x == 0, a*y - b == 0, -a - y <= -2, -q <= 0, b - r <= 0, a - b <= 0, -a - b <= -2
30: q*y + r - x == 0, -x <= -1, r - y <= -1, -r <= 0

Here DIG3 discovers the equality invariants a*y = b, q*y + r = x and other inequalities at at locations marked with //%%%traces from the program programs/nla/CohenDiv.java below:

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(true){
    if (!(r>=y)) break;
    int a=1; 
    int b=y;
    while(true){
      //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.

Additional Info

To run doctests, use sage -t

$ export SAGE_PATH=$Z3/src/api/python:.
$ sage -t miscs.py

Publications

Additional information on DIG3 can be found from these papers:

  • ThanhVu Nguyen, Matthew Dwyer, and William Visser. SymInfer: Inferring Program Invariants using Symbolic States. In Automated Software Engineering (ASE). IEEE, 2017.

For C programs

DIG3 also supports C programs, but has a differently underlying algorithm. More specifically, the tool doesn't compute symbolic states and instead directly calls a symbolic execution tool to check candidate invariants.

Install KLEE

To setup DIG3 to work with C, do all the above steps for Java and then install KLEE. DIG3 has been tested with

  • KLEE 1.3.0.0

Then build KLEE using these instructions. Important: build KLEE with Z3 support !

#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

  • Append the following in your ~/.bash_profile
# ~/.bash_profile
...
export KLEE=$DEVEL/KLEE/
export PATH=$KLEE/klee_build_dir/bin:$SAGE:$PATH
  • Make sure KLEE works, e.g., `klee --help | grep z3' should say something that Z3 is the default solver

Usage

Here's the equivalent C program of the above CohenDiv.java. Again the following assumes we are currently in the symtraces directory.

Generating invariants

mu1k4sfag@debian:~/symtraces$ sage -python -O dig.py programs/nla/cohendiv.c -log 3
alg:INFO:analyze 'programs/nla/cohendiv.c'
...

Updated