# Wiki

# dig / Home

# README

DIG (Dynamic Invariant Generator) is a dynamic analysis tool that discovers polynomial and array invariants from program traces. For polynomial invariants, DIG supports conjunction of (potentially nonlinear) polynomial relations over numerical variables. DIG also supports the max and min-plus forms of disjunction polynomial invariants. For array invariants, DIG supports flat and nested form of relations among multidimentional array variables.

## Setup

The source code of DIG is released under the **BSD** license and can be obtained using the commands

hg clone https://nguyenthanhvuh@bitbucket.org/nguyenthanhvuh/dig/ hg clone https://nguyenthanhvuh@bitbucket.org/nguyenthanhvuh/common_python/

DIG uses Python/SAGE. Some tasks such as verifying candidate invariants require a recent SMT solver. The tool has been tested using the following setup:

- Debian Linux 7 or 8
- Sage 7.5.1 (older versions might work, but if you see some errors about sage, then update to this version)
- Microsoft Z3 SMT solver 4.x

### Installing Z3 and SAGE

First, setup Z3 using its own build instruction. Make sure Z3 is installed correctly so that you can do `import z3`

in a Python interpreter. Next, setup SAGE (you can simply download the tarball consisting of precompiled SAGE, or build SAGE directly from source). Finally, setup the SAGE environment and add Z3's lib to its path as follows.

# ~/.bash_profile export Z3=PATH/TO/z3 #Z3 dir export SAGE=PATH/TO/sage #where your SAGE dir is export $DIG=/PATH/TO/dig #DIG main dir export SAGE_PATH=/PATH/TO/common_python:$DIG:$Z3/src/api/python:$DIG/dig:$DIG/miscs export PATH=$SAGE:$PATH

Now we should be able to do `import z3`

in SAGE. For additional testings, execute the `run_doctests.sh`

script to tests all doctests in DIG's files.

### Installing compute_ext_rays_polar

For `max/min`

inequalities, compile the program `tplib`

package. Then put the compiled program `compute_ext_rays_polar`

in your PATH (e.g., in `/usr/local/bin`

).

Note that this installation can be discarded if we don't need max/min inequalities.

## Usage

Here are some usage examples of DIG. The following assumes we are currently in the `$DIG/dig`

directory.

### (Nonlinear) Polynomial Invariants

sage: %attach dig.py sage: dig = DIG('../traces/NLA/tcs/cohendiv.l1a.tcs') ... sage: dig.get_invs() dig:Debug:*** Generate Polynomial Invs over [a, b, q, r, x, y] *** ... dig:Info:Detected 2 invs for Eqt: 0: a*y - b == 0 1: q*y + r - x == 0

Here DIG discovers the invariants `a*y = b, q*y + r = x`

from the traces in `../traces/NLA/tcs/cohendiv.l1a.tcs`

x y q a b r 102031 19229 0 1 19229 102031 102031 19229 0 2 38458 102031 165043 78404 0 1 78404 165043 603505 47638 0 1 47638 603505 603505 47638 0 2 95276 603505 603505 47638 0 4 190552 603505 603505 47638 8 1 47638 222401 603505 47638 8 2 95276 222401 ...

These traces (values of the variables *x, y, q, a, b, r*) are obtained at location `li1`

in the program

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){ printf("li1: %d %d %d %d %d %d\n",x,y,q,a,b,r); //traces if (!(r >= 2*b)) break; a = 2*a; b = 2*b; } r=r-b; q=q+a; } return q; }

Thus DIG finds the *nonlinear* equalities `a*y = b, q*y + r = x`

at location `l1i`

of `cohendiv`

. The directory `../programs/polynomials/`

contains many programs having such nonlinear invariants.

### Array Invariants

**Flat array invariants**

sage: dig = DIG('../traces/Examples/array_flat.tcs') ... sage: dig.get_flat_array() dig:Info:*** FlatArray *** dig:Info:Select traces dig:Info:Compute invs over 9 tcs .... dig:Info:Detected 2 invs for FlatArray: 0: (-A[A0]) + ((7) *B[2*A0]) + (3*A0) == 0 1: ((7) *B[B0]) + (-A[1/2*B0]) + (3/2*B0) == 0

Here DIG discovers the array invariants `A[i] = 7*B[2i] + 3i`

from the traces in `../traces/Examples/array_flat.tcs`

A B [-546,-641,34] [-78,3,-92,-34,4] [-448,-585,118] [-64,40,-84,78,16] [539,-487,517] [77,55,-70,74,73] [-7,-18,482] [-1,51,-3,-19,68] [-119,192,216] [-17,80,27,32,30] [-273,591,699] [-39,13,84,56,99] [133,-333,-323] [19,96,-48,-80,-47] [-168,157,643] [-24,8,22,-61,91] [-84,-18,300] [-12,-60,-3,-16,42]

**Nested array invariants**

sage: dig = DIG('../traces/Examples/array_nested.tcs') ... sage: dig.get_nested_array() dig:Info:*** NestedArray *** dig:Info:Select traces ... dig:Info:Detected 2 invs for NestedArray: 0: A[i1] == B[-2*i1 + 5] 1: A[i1] == B[C[2*i1 + 1]]

Here DIG discovers the array invariants `A[i] = B[C[2i+1]]`

from the traces in `../traces/Examples/array_nested.tcs`

A B C [7,1,-3] [1,-3,5,1,0,7,1] [8,5,6,6,2,1,4]

The directory `../programs/AES/`

contains many programs having such array invariants.

## Publications

Additional information on DIG can be found from these papers:

- Automating Program Verification and Repair Using Invariant Analysis and Test-input Generation Nguyen, T. Ph.D. Thesis, University of New Mexico, August 2014.
- ThanhVu Nguyen, Deepak Kapur, Westley Weimer, Stephanie Forrest, "DIG: A Dynamic Invariant Generator for Polynomial and Array Invariants", ACM Trans. on Software Engineering and Methodology, pages 30:1-30:30, 2014.
- Using Dynamic Analysis to Generate Disjunctive Invariants Nguyen, T.; Kapur, D.; Weimer, W.; and Forrest, S. In International Conference on Software Engineering, pages 608-619, 2014.
- Using Dynamic Analysis to Discover Polynomial and Array Invariants Nguyen, T.; Kapur, D.; Weimer, W.; and Forrest, S. In International Conference on Software Engineering, pages 683-693, 2012.

Updated