dynaroars / dig Goto Github PK

DIG is a numerical invariant generation tool. It infers program invariants or properties over (i) program execution traces or (ii) program source code. DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations.

Home Page: https://github.com/dynaroars/dig

License: MIT License

Python 89.33% Java 7.44% Makefile 0.04% Dockerfile 0.02% C 2.72% OCaml 0.45%

symbolic-execution invariant-generation dynamic-analysis machine-learning specification-mining loop-invariants program-verification neural-network-verification

dig's People

Contributors

Stargazers

Watchers

Forkers

abueide ruricolist letonchanh yuanzhou-yzhou santiago-yu binwensun

dig's Issues

Run Ultimate to check C programs

add beartype

Add beartype https://github.com/beartype/beartype for runtime type checking.

Emphasize Relational and Non-Relational Abstract Domains

Generate invariants for C programs with the functions from math.h

sqrt() is a function defined in the file of math.h for C programs. Unfortunately, when I generate the invariants for the following C program, it occurs the error: undefined reference to `sqrt' When I run the command
sage -python -O dig.py bench27_factor.c -log 4 -nominmax -nominmaxplus -nomp -maxdeg 2 -seed 0
How to solve this problem? @nguyenthanhvuh @ndkimhao @timosantonopoulos @abueide

#include <math.h>
#include <stdio.h>
#include <stdlib.h>

void vassume(int b){}
void vtrace1(int n, int dd, int r, int rp, int q, int d, int s, int t){} 
void vtrace2(int n, int dd, int r, int rp, int q, int d, int s, int t){} 
void vtrace3(int n, int dd, int r, int rp, int q, int d, int s, int t){} 
void vtrace4(int n, int dd, int r, int rp, int q, int d, int s, int t){} 

void mainQ(int n, int dd) {
	int r, rp, q, d, s, t;
	d = dd;
	if (d!=0 && d!=2){
	r = n % d;
	t=r;
	rp = n % (d - 2);
	q = 4*(n / (d-2) - n / d);
	s = (int) sqrt(n);
	}

	while (s >= d && r != 0) {// loop invariant:
		if(2*r-rp+q<0){
		vtrace1(n, dd, r, rp, q, d, s, t);
			t = r;
			r = 2*r-rp+q+d+2;
			rp = t;
			q = q+4;
			d = d+2;
		} else if((2*r-rp+q >=0)&&(2*r-rp+q<d+2)){
		vtrace2(n, dd, r, rp, q, d, s, t);
			t = r;
			r = 2*r-rp+q;
			rp = t;
			d = d+2;
		} else if((2*r-rp+q >=0)&&(2*r-rp+q>=d+2)
			&&(2*r-rp+q <2*d+4)) {
			vtrace3(n, dd, r, rp, q, d, s, t);
			t = r;
			r = 2*r-rp+q-d -2;
			rp = t;
			q = q -4;
			d = d+2;
		} else{
			// ((2*r-rp+q>=0)&&(2*r-rp+q>=2*d+4)) 
			vtrace4(n, dd, r, rp, q, d, s, t);
			t = r;
			r = 2*r-rp+q -2*d -4;
			rp = t;
			q = q -8;
			d = d+2;
		}
	}
}

void main(int argc, char **argv){
    mainQ(atoi(argv[1]),atoi(argv[2]));
}

Support Java analysis in Docker

Hi, we will work on adding Java support to the Docker. Note that you can manually install files to support Java files (essentially JDK 8 and Symbolic PathFinder).

Some problems encountered while testing custom cases

While testing the code from a previous issue #24, I used the command:

time ~/miniconda3/bin/python3 -O dig.py ../data/const_1-1.c -log 4 -maxdeg 2 -nominmax -nomp -nominmaxplus -seed 0

to test the following code:

#include <stdio.h>
#include <stdlib.h>

void vassume(int b){}
void vtrace1(int x, int y){} 

void mainQ( ){ 
  int x,y;
  x=1;
  y=0;
  vassume (x==1 && y==0);
  while(x<=100){// loop invariant:2x-y^2==y
    vtrace1(x,y);
    y=y+1;
    x=x+y;
   } 
}

void main(int argc, char **argv){
    mainQ();
}

However, I encountered the following error:

settings:INFO:2024-04-10 02:47:01.434439: dig.py ../data/const_1-1.c -log 4 -maxdeg 2 -nominmax -nomp -nominmaxplus -seed 0
alg:INFO:analyzing '../data/const_1-1.c'
alg:DEBUG:seed=0.0 (test 49)
Traceback (most recent call last):
  File "/dig/src/dig.py", line 271, in <module>
    dinvs = dig.start(seed=seed, maxdeg=args.maxdeg)
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/dig/src/alg.py", line 113, in start
    self.mysrc = self.mysrc_cls(self.filename, self.tmpdir_del)
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/dig/src/data/prog.py", line 357, in __init__
    typ = instrument(self.filename, self.tracefile, self.symexefile)
          ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/dig/src/c_instrument.py", line 170, in instrument
    vis.visit(ast_civl)
  File "/root/miniconda3/lib/python3.12/site-packages/pycparser/c_ast.py", line 158, in visit
    return visitor(node)
           ^^^^^^^^^^^^^
  File "/root/miniconda3/lib/python3.12/site-packages/pycparser/c_ast.py", line 165, in generic_visit
    self.visit(c)
  File "/root/miniconda3/lib/python3.12/site-packages/pycparser/c_ast.py", line 158, in visit
    return visitor(node)
           ^^^^^^^^^^^^^
  File "/dig/src/c_instrument.py", line 101, in visit_FuncDef
    nts = [(p.name , p.type.type.names[0]) for p in node.decl.type.args.params]
                                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^
AttributeError: 'NoneType' object has no attribute 'params'

show advantages of refinement

Experiment with no checking (pure dynamic)
Experiment with 1 checking (no cex, no refinement)
Experiment with refinement

How to analyze java in docker

root@5e5853a00882:/dig/src# time ~/miniconda3/bin/python3 -O dig.py /testaaa/tests/examples/Ex0.java
settings:INFO:2022-05-12 11:56:39.712264: dig.py /testaaa/tests/examples/Ex0.java
alg:INFO:analyzing '/testaaa/tests/examples/Ex0.java'
data.prog:ERROR:cmd '/usr/bin/java -cp /dig/src/java:/dig/src/java/asm-all-5.2.jar Instrument /var/tmp/dig_1637148626155009527_lbu2q4ig/delete_me/Ex0.class /var/tmp/dig_1637148626155009527_lbu2q4ig/delete_me/traces/Ex0.class /var/tmp/dig_1637148626155009527_lbu2q4ig/delete_me/symexe/Ex0.class' gives error
Error: Could not find or load main class Instrument
Caused by: java.lang.ClassNotFoundException: Instrument

Traceback (most recent call last):
File "/dig/src/dig.py", line 272, in
dinvs = dig.start(seed=seed, maxdeg=args.maxdeg)
File "/dig/src/alg.py", line 107, in start
self.mysrc = self.mysrc_cls(self.filename, self.tmpdir_del)
File "/dig/src/data/prog.py", line 268, in init
cp = subprocess.run(
File "/root/miniconda3/lib/python3.9/subprocess.py", line 528, in run
raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command '['/usr/bin/java', '-cp', '/dig/src/java:/dig/src/java/asm-all-5.2.jar', 'Instrument', '/var/tmp/dig_1637148626155009527_lbu2q4ig/delete_me/Ex0.class', '/var/tmp/dig_1637148626155009527_lbu2q4ig/delete_me/traces/Ex0.class', '/var/tmp/dig_1637148626155009527_lbu2q4ig/delete_me/symexe/Ex0.class']' returned non-zero exit status 1.

Get stats from Dig's results

Effect of depths
Number of generated inputs
Number of iterations
Compare quality over Dig's input generation vs random input generation

Experiment-Java programs

Let's rerun the experiments to get the results like those in Tab 1 in the SymInfer paper https://cse.unl.edu/~tnguyen/pubs/symtraces.pdf . Create a note that talk about anything interesting (e.g., programs that do not work, those that consistently give some strange invariants, etc)

In the SymInfer paper, read from the beginning of Section 5 up to (and including) 5B: Analyzing Program Correctness to see how the experiment was done.
Run dig on some of the NLA programs several times , e.g., CohenDiv, Ps4, etc so that you have a feel on what the results would look like. Each of these programs should have nonlinear invs at the considered locations (e.g., in CohenDiv, we have a*y + r == x, etc). Analyze Dig's results to see that it does give these invariants.
Identify programs that do not work: look at Tab 1 in the SymInfer paper, some of these do not work, run those and confirm that they do not work. Then create a new directory and move programs that do not work there. In the notes, mentioned these programs and reasons why they do not work (e.g., takes a long time on some parts .. look at the log, see what parts it get stuck on)
Run dig on all of these programs, there's a script called benchmark.py in the main src dir, you can run them like this

f=../results/nla_010220 ; rm -rf $f; python benchmark.py 2>&1 | tee $f

We want to collect results similar to those in Tab 1 (e.g., time, # of invs). We also want to show how many of the obtained invariants are nonlinear, oct, and max/min-plus.

Complexity Analysis

Could you run Dig on the complexity benchmarks and see if the results are consistent with those in the Syminfer paper and the notes in each program? Also report any errors etc.

Here's an example

time sage -python dig.py ../tests/complexity/Cav09_Fig1a.java  -log 4
...
*** '../tests/complexity/Cav09_Fig1a.java', 1 locs, 5 invs (1 Eqt, 2 Oct, 2 PrePost), 59 traces, 59 inps, time 4.47s, rand seed 1582581469.98, test 18 46:
vtrace_post (5 invs):
1. m*tCtr - tCtr^2 - 100*m + 200*tCtr - 10000 == 0
2. (m < 0) => tCtr == 100 p
3. (-m <= 0) => tCtr == m + 100 p
4. m - tCtr <= -10
5. -tCtr <= -10

check why Fuzzer still gen neg inputs when the rand inp generator does not allow neg range.

add ability to check user-supplied invariants in src code

e.g., support the syntax

// code ... vcheck(x > y);

Incremental Depth for finding upper-bounds

Bug? The memory footprint increases continually and DIG does not terminal, then it makes the computer crashed.

When I run DIG with the following command to generate invariant for the C program, the memory footprint increases continually (to 32+GB) and DIG does not terminal, then the computer crashed. (BTW, the DIG is installed correctly since it can generate invarinats for other C programs.)

time  sage -python -O dig.py bench17_potsumm2.c -log 4 -nominmax -nominmaxplus -nomp -maxdeg 2 -seed 0

C program

#include <stdio.h>
#include <stdlib.h>

void vassume(int b){}
void vtrace(int x, int y){} 

void mainQ( ){ 
  int x,y;
  x=1;
  y=0;
  vassume (x==1 && y==0);
  while(x<=100){// loop invariant:2x-y^2==y
    vtrace(x,y);
    y=y+1;
    x=x+y;
   } 
}

void main(int argc, char **argv){
    mainQ();
}

Is this problem caused by the bug of DIG?
@nguyenthanhvuh

Paper: some programs need modifications to restrict the bound for symbolic execution to work (e.g., Knuth, PS)

Rewrite script using os.system to avoid multiprocessing problems

Docker Issue (SARL Configuration Error: Mismatched Z3 Version)

Hello,

After successfully configuring the DIG Docker image as per the README, I was able to successfully execute and output the results for the command: time ~/miniconda3/bin/python3 -O dig.py ../examples/traces/cohendiv.csv -log 4.

However, when testing with time ~/miniconda3/bin/python3 -O dig.py ../benchmark/c/nla/cohendiv.c -maxdeg 2 -noieqs -nominmax -log 4, I encountered the following error:

root@3cbae472cec6:/dig/src# time ~/miniconda3/bin/python3 -O dig.py  ../benchmark/c/nla/cohendiv.c -maxdeg 2 -noieqs -nominmax -log 4
settings:INFO:2024-04-09 17:14:11.849360: dig.py ../benchmark/c/nla/cohendiv.c -maxdeg 2 -noieqs -nominmax -log 4
alg:INFO:analyzing '../benchmark/c/nla/cohendiv.c'
alg:DEBUG:seed=1712682851.81 (test 32)
helpers.miscs:DEBUG:getting symstates:running 11 jobs using 11 threads: [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1]
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=20 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=21 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=22 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=23 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=24 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=25 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=26 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=28 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=27 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=29 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:DEBUG:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=30 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=30 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=28 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=26 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=23 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=24 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=27 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=22 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=20 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=21 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=29 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:ERROR:/usr/bin/java -jar ../EXTERNAL_FILES/civl/lib/civl-1.22_5854.jar verify -maxdepth=25 /var/tmp/dig_1867732707234379619_teurrl55/delete_me/symexe/cohendiv.c
SARL configuration error: expected version 4.12.6 - 64 bit for z3 but found 4.13.0 - 64 bit

data.symstates:WARNING:cannot obtain symstates, unreachable locs?

Add ACSL examples in C and Java format for DIG

For acsl examples: There are 14 numeric programs, however 7 of which have no loops or recursion.

cannot generate inv from Timos & Ferhat

#include <stdio.h>
#include <stdlib.h>
void vassume(int b) {}
void vtrace(int g, int h) {}

// f(x) = x(x + 1)
int F(int x) { return x * x; }

void mainQ(int x1, int x2) {
  int x = x1 + x2;
  int y = x1 - x2;
  int f_x = F(x);
  int f_y = F(y);
  int f_x1 = F(x1);
  int f_x2 = F(x2);

  vtrace(f_x*f_x - 2*f_y*f_x + f_y*f_y, 16*f_x1*f_x2);  //  <--------------------------HERE
}

void main(int argc, char *argv[]) {
  mainQ(atoi(argv[1]), atoi(argv[2]));
}

Timos: In this code, on the line that says HERE, if we leave the coefficient 16 in the second term, we get the invariant g==h, but if we remove it, we are not getting the invariant g = 16*h that I would have expected.

@timosantonopoulos @ferhaterata

Get Dig to work on new Linux, document all steps

user term is broken

 ~/miniconda3/bin/python3  -O dig.py  ../benchmark/c/nla/sqrt1.c -nominmax -nocongruences -noeqts -uterms "y**2"

support float point numbers from traces

Run DIG on HOLA programs

Update examples on Knuth, Friere, etc, which no longer use sqrt or floating point

see Timo's email attachments.

Pure dynamic analysis , no symbolic states

Ability to run using pure dynamic analysis (i.e., automatically generate inputs). Not requiring symbolic traces.

Add these results for the programs that cannot use symbolic execution (e.g., those with doubles freire2 etc)

docker issue (ModuleNotFoundError: No module named 'pycparser')

Hi Vu,

The first example, which runs dig on a trace files, completes successfully as follows:

time ~/miniconda3/bin/python3 -O dig.py ../tests/traces/cohendiv.csv -log 4

root@fe8ccbdc800b:/dig/src# time ~/miniconda3/bin/python3 -O dig.py  ../tests/traces/cohendiv.csv -log 4
settings:INFO:2023-03-09 21:41:36.973133: dig.py ../tests/traces/cohendiv.csv -log 4
data.traces:DEBUG:vtrace1: 98
vtrace2: 83 traces
alg:INFO:analyzing '../tests/traces/cohendiv.csv'
alg:DEBUG:seed=1678398096.94 (test 33)
alg:INFO:got 181 traces over 2 locs
alg:DEBUG:vtrace1: 98
vtrace2: 83
helpers.miscs:DEBUG:autodeg 3
helpers.miscs:DEBUG:(pure) dynamic inference:running 8 jobs using 8 threads: [1, 1, 1, 1, 1, 1, 1, 1]
helpers.miscs:DEBUG:getting upperbounds:running 176 jobs using 8 threads: [22, 22, 22, 22, 22, 22, 22, 22]
helpers.miscs:DEBUG:getting upperbounds:running 1368 jobs using 8 threads: [171, 171, 171, 171, 171, 171, 171, 171]
helpers.miscs:DEBUG:getting upperbounds:running 32 jobs using 8 threads: [4, 4, 4, 4, 4, 4, 4, 4]
helpers.miscs:DEBUG:getting upperbounds:running 72 jobs using 8 threads: [9, 9, 9, 9, 9, 9, 9, 9]
helpers.miscs:DEBUG:solving 35 uks using 52 eqts
helpers.miscs:DEBUG:got 14 eqts after instantiating
helpers.miscs:DEBUG:ignoring large coefs 8*q**3 - 14*q**2*x - 80*q**2 + 7*q*x**2 + 140*q*x  ..
helpers.miscs:DEBUG:Grobner basis: from 13 to 3 ps
helpers.miscs:DEBUG:got 3 eqts after refinement
helpers.miscs:DEBUG:solving 84 uks using 98 eqts
helpers.miscs:DEBUG:got 19 eqts after instantiating
helpers.miscs:DEBUG:Grobner basis: from 19 to 3 ps
helpers.miscs:DEBUG:got 3 eqts after refinement
alg:DEBUG:check 546 invs using 181 traces
helpers.miscs:DEBUG:test_dinvs:running 2 jobs using 2 threads: [1, 1]
helpers.miscs:DEBUG:test:running 74 jobs using 8 threads: [9, 9, 9, 9, 9, 9, 10, 10]
helpers.miscs:DEBUG:test:running 472 jobs using 8 threads: [59, 59, 59, 59, 59, 59, 59, 59]
infer.inv:DEBUG:remove r**2 - r*x == 0
infer.inv:DEBUG:remove q*r == 0
helpers.miscs:DEBUG:test_dinvs: removed 2 invs in 1.39s (orig 546, new 544)
alg:INFO:check 546 invs using 181 traces (1.39s)
alg:DEBUG:simplify 544 invs
alg:DEBUG:vtrace1 (472 invs):
1. a*y - b == 0
2. q*y + r - x == 0
3. a*r - a*x + b*q == 0
4. -q <= 0
5. -b <= -1
6. -x <= -8
7. -r <= -1
8. -y <= -1
9. -a <= -1
10. a - b <= 0
11. a - r <= 0
12. b - x <= 0
13. r - x <= 0
14. b - r <= 0
15. -b + y <= 0
16. -r + y <= 0
17. q - x <= -1
18. a - x <= -5
19. -a - y <= -2
20. -x + y <= -6
21. ...
vtrace2 (72 invs):
1. q*y + r - x == 0
2. -r <= 0
3. -q <= 0
4. -x <= -1
5. -y <= -1
6. r - x <= 0
7. q - x <= 0
8. r - y <= -1
9. -q - r <= -1
10. -r - y <= -1
11. -q - y <= -5
12. -r - x <= -2
13. -q - x <= -1
14. -x - y <= -10
15. max(q, 0) - x <= 0
16. min(r, 0) - q <= 0
17. q - max(x, y) <= 0
18. min(r, y) - x <= 0
19. min(x, 0) - r <= 0
20. max(q, r) - x <= 0
21. ...
helpers.miscs:DEBUG:simplify:running 2 jobs using 2 threads: [1, 1]
helpers.miscs:DEBUG:_simplify_fast 58 mps_ieq:running 58 jobs using 8 threads: [7, 7, 7, 7, 7, 7, 8, 8]
helpers.miscs:DEBUG:_simplify_fast mps_ieq: removed 58 invs in 0.59s (orig 58, new 0)
helpers.miscs:DEBUG:_simplify_fast 9 octs:running 9 jobs using 8 threads: [1, 1, 1, 1, 1, 1, 1, 2]
helpers.miscs:DEBUG:_simplify_fast octs: removed 0 invs in 0.11s (orig 9, new 9)
helpers.miscs:DEBUG:_simplify_slow octs+mps: removed 6 invs in 0.29s (orig 9, new 3)
helpers.miscs:DEBUG:_simplify_slow octs_simple: removed 0 invs in 0.07s (orig 4, new 4)
helpers.miscs:DEBUG:_simplify_slow eqts: removed 1 invs in 1.81s (orig 3, new 2)
helpers.miscs:DEBUG:_simplify_fast 6 congruences:running 6 jobs using 6 threads: [1, 1, 1, 1, 1, 1]
helpers.miscs:DEBUG:_simplify_fast congruences: removed 0 invs in 0.06s (orig 6, new 6)
helpers.miscs:DEBUG:_simplify_slow congruences: removed 4 invs in 0.12s (orig 6, new 2)
helpers.miscs:DEBUG:_simplify_fast 432 mps_ieq:running 432 jobs using 8 threads: [54, 54, 54, 54, 54, 54, 54, 54]
helpers.miscs:DEBUG:_simplify_fast mps_ieq: removed 416 invs in 2.84s (orig 432, new 16)
helpers.miscs:DEBUG:_simplify_fast 23 octs:running 23 jobs using 8 threads: [2, 3, 3, 3, 3, 3, 3, 3]
helpers.miscs:DEBUG:_simplify_fast octs: removed 0 invs in 0.16s (orig 23, new 23)
helpers.miscs:DEBUG:_simplify_slow octs+mps: removed 30 invs in 0.86s (orig 39, new 9)
helpers.miscs:DEBUG:_simplify_slow octs_simple: removed 3 invs in 0.14s (orig 8, new 5)
infer.inv:DEBUG:done simplifying , time 5.989552021026611
helpers.miscs:DEBUG:simplify: removed 518 invs in 5.99s (orig 544, new 26)
alg:INFO:simplify 544 invs (5.99s)
vtrace1 (18 invs):
1. a*y - b == 0
2. q*y + r - x == 0
3. -q <= 0
4. -b <= -1
5. a - b <= 0
6. r - x <= 0
7. b - r <= 0
8. a - x <= -5
9. -b + y <= 0
10. -x + y <= -6
11. -a - q <= -1
12. -q - r <= -8
13. -x - y <= -10
14. -r - x <= -16
15. a + 2 - max(q, r, 0) <= 0
16. y + 2 - max(b, q, r, 0) <= 0
17. -q === 0 (mod 2)
18. -r - x === 0 (mod 2)
vtrace2 (8 invs):
1. q*y + r - x == 0
2. -r <= 0
3. -q <= 0
4. -x <= -1
5. r - x <= 0
6. q - x <= 0
7. r - y <= -1
8. -x - y <= -10

real	0m14.015s
user	1m4.844s
sys	0m1.995s

However, the other examples throw error: python cannot find pycparser although in the dockerfile I see that you'd added it.

root@fe8ccbdc800b:/dig/src# time ~/miniconda3/bin/python3 -O dig.py  ../benchmark/c/nla/cohendiv.c -maxdeg 2 -noieqs -nominmax -log 4
settings:INFO:2023-03-09 21:47:55.507143: dig.py ../benchmark/c/nla/cohendiv.c -maxdeg 2 -noieqs -nominmax -log 4
alg:INFO:analyzing '../benchmark/c/nla/cohendiv.c'
alg:DEBUG:seed=1678398475.5 (test 7)
data.prog:ERROR:cmd 'python3 /dig/src/c_instrument.py ../benchmark/c/nla/cohendiv.c /var/tmp/dig_1152921506285245451_f9yt35aq/delete_me/symexe/cohendiv.c /var/tmp/dig_1152921506285245451_f9yt35aq/delete_me/traces/cohendiv.c' gives error
Traceback (most recent call last):
  File "/dig/src/c_instrument.py", line 3, in <module>
    from pycparser import c_generator, c_ast, c_parser 
ModuleNotFoundError: No module named 'pycparser'

Traceback (most recent call last):
  File "/dig/src/dig.py", line 272, in <module>
    dinvs = dig.start(seed=seed, maxdeg=args.maxdeg)
  File "/dig/src/alg.py", line 113, in start
    self.mysrc = self.mysrc_cls(self.filename, self.tmpdir_del)
  File "/dig/src/data/prog.py", line 361, in __init__
    super().__init__(filename, tmpdir)
  File "/dig/src/data/prog.py", line 275, in __init__
    cp = subprocess.run(
  File "/root/miniconda3/lib/python3.10/subprocess.py", line 526, in run
    raise CalledProcessError(retcode, process.args,
subprocess.CalledProcessError: Command '['python3', '/dig/src/c_instrument.py', '../benchmark/c/nla/cohendiv.c', '/var/tmp/dig_1152921506285245451_f9yt35aq/delete_me/symexe/cohendiv.c', '/var/tmp/dig_1152921506285245451_f9yt35aq/delete_me/traces/cohendiv.c']' returned non-zero exit status 1.

real	0m0.658s
user	0m0.583s
sys	0m0.075s
root@fe8ccbdc800b:/dig/src#

Experiment-C programs

Run Dig on C programs (e.g., Hola), look at the results, and then do some quick comparison with the corresponding Java ones.
Create a table showing the programs, the time difference btw the Java and C, and the number of inferred invariants (especially the important invariants).

Issue with setting up using Docker

Hello Prof. Nguyen,

Below is the setup error I got using Docker:

PS C:\Users\yulez> git clone --depth 1 https://github.com/dynaroars/dig.git
Cloning into 'dig'...
remote: Enumerating objects: 789, done.
remote: Counting objects: 100% (789/789), done.
remote: Compressing objects: 100% (652/652), done.
remote: Total 789 (delta 174), reused 544 (delta 119), pack-reused 0
Receiving objects: 100% (789/789), 13.01 MiB | 34.08 MiB/s, done.
Resolving deltas: 100% (174/174), done.
PS C:\Users\yulez> cd dig
PS C:\Users\yulez\dig> docker build . -t='dig'
[+] Building 212.3s (19/23)
=> [internal] load build definition from Dockerfile 0.1s
=> => transferring dockerfile: 3.12kB 0.0s
=> [internal] load .dockerignore 0.1s
=> => transferring context: 2B 0.0s
=> [internal] load metadata for docker.io/library/debian:buster 1.4s
=> [ 1/20] FROM docker.io/library/debian:buster@sha256:e6fb8b88b411285ac71590459aa8d0a376acc86a3d17adf 5.9s
=> => resolve docker.io/library/debian:buster@sha256:e6fb8b88b411285ac71590459aa8d0a376acc86a3d17adfe4 0.0s
=> => sha256:e6fb8b88b411285ac71590459aa8d0a376acc86a3d17adfe45e806f522c54cc3 984B / 984B 0.0s
=> => sha256:1487e24b974ca8b859de513d40c7f30606949c1fa1e4057df81b2dc1915edc6a 529B / 529B 0.0s
=> => sha256:528ac3ebe42095912dc3c246715e7544a939c974532e2da1b93d2557a41c4567 1.46kB / 1.46kB 0.0s
=> => sha256:620af4e91dbf80032eee9f1ff66a8b04119d7a329b2a13e007d69c8a0b337bf0 50.45MB / 50.45MB 3.2s
=> => extracting sha256:620af4e91dbf80032eee9f1ff66a8b04119d7a329b2a13e007d69c8a0b337bf0 2.1s
=> [internal] load build context 2.4s
=> => transferring context: 31.65MB 2.3s
=> [ 2/20] RUN apt-get update -y 3.6s
=> [ 3/20] RUN apt-get install -y build-essential git software-properties-common emacs ocaml ocamlbu 131.9s
=> [ 4/20] RUN wget https://repo.anaconda.com/miniconda/Miniconda3-latest-Linux-x86_64.sh 6.1s
=> [ 5/20] RUN bash ./Miniconda3-latest-Linux-x86_64.sh -b 13.3s
=> [ 6/20] RUN /root/miniconda3/bin/conda install sympy pip -y 12.0s
=> [ 7/20] RUN /root/miniconda3/bin/pip3 install z3-solver 7.4s
=> [ 8/20] RUN /root/miniconda3/bin/pip3 install beartype 2.5s
=> [ 9/20] COPY . /dig 0.2s
=> [10/20] WORKDIR /dig/EXTERNAL_FILES 0.0s
=> [11/20] RUN unzip develop.zip && mv cil-develop cil 0.9s
=> [12/20] WORKDIR cil 0.0s
=> [13/20] RUN ./configure && make 26.1s
=> [14/20] WORKDIR /dig/src/ocaml 0.0s
=> ERROR [15/20] RUN make clean; make 0.6s

[15/20] RUN make clean; make:
#19 0.584 rm -f *.cmo *.cmi *.d *.cmx *.dx *.o instr.exe
#19 0.586 rm -rf *.pyc *.pyo
#19 0.590 Makefile:1: *** Recursive variable 'OCAML_OPTIONS' references itself (eventually). Stop.

executor failed running [/bin/sh -c make clean; make]: exit code: 2

Pull Dev branch into Master

How to generate invariants for C programs with array variables?

@nguyenthanhvuh @ndkimhao @timosantonopoulos @abueide
How to fix the following program with an array variable in order to generate the invariants for it?

#include <stdio.h>
#include <stdlib.h>

void vassume(int b){}
void vtrace1(int tmp, int h, int n, int c, int k, int m){} 


void mainQ(int a[], int h){ 
  int n = 0;
  int c = 0;
  int k = 1;
  int m = 6;
  while(n < h)
  // invariant 0 <= n <= h
  // invariant forall i : 0 <= i < n ==> a[i] == i*i*i
  // invariant c == n*n*n
  // invariant k == 3*n*n + 3*n + 1
  // invariant m == 6*n + 6
  {    
    a[n] = c;
    int tmp=a[n];
    vtrace1(tmp, h, n, c, k, m);
    c = c + k;
    k = k + m;
    m = m + 6;
    n = n + 1;
  }
  //postcondition 
  //assert(0 <= i < n && a[i] == i*i*i);
}

void main(int argc, char **argv){
    mainQ(atoi(argv[1]), atoi(argv[2]));
}

When I run the command sage -python -O dig.py bench15_Cubes3.c -log 4 -nominmax -nominmaxplus -nomp -maxdeg 2 -seed 0, it occurs the errors:

/home/ly/Music/benchmark-tasep/bench15_Cubes3.c: In function ‘main’:
/home/ly/Music/benchmark-tasep/bench15_Cubes3.c:34:11: warning: cast to pointer from integer of different size [-Wint-to-pointer-cast]
   34 |     mainQ((int *)atoi(argv[1]), atoi(argv[2]));
      |           ^
/var/tmp/dig_1752440666638579583_fwwx9u97/delete_me/traces/bench15_Cubes3.c: In function ‘main’:
/var/tmp/dig_1752440666638579583_fwwx9u97/delete_me/traces/bench15_Cubes3.c:624:9: warning: cast to pointer from integer of different size [-Wint-to-pointer-cast]
  624 |   mainQ((int *)tmp___0, tmp);
      |         ^
data.symstates:WARNING:cannot obtain symbolic states, unreachable locs?

Support purely random trace generation (no symbolic execution)

replace CIL with pycparser

Analysis bugs

total should be sum of median's

Remove trivial disj in pre/post conds

if a -> b is a tautology, then remove it

Support array invariants from traces

support nested arrays as in ICSE'12 paper

Support congruence domain (trace only)

Why can't I get the analysis results of this simple trace files?

At first I thought it was caused by floating-point numbers, but it's no use converting it to an integer. I think I can at least get their minimum and maximum? And what does the output of the program mean by the way?

root@a42077a01f4b:/dig/src# time ~/miniconda3/bin/python3 -O dig.py /data/dig-1639641266712/grp0_line71.csv -log 3
settings:INFO:2021-12-16 08:29:58.863661: dig.py /data/dig-1639641266712/grp0_line71.csv -log 3
alg:INFO:analyzing '/data/dig-1639641266712/grp0_line71.csv'
alg:INFO:got 62 traces over 1 locs
infer.eqt:WARNING:NO EQTS RESULTS, reducing deg to 6
infer.eqt:WARNING:NO EQTS RESULTS, reducing deg to 5
infer.eqt:WARNING:NO EQTS RESULTS, reducing deg to 4
infer.eqt:WARNING:NO EQTS RESULTS, reducing deg to 3
infer.eqt:WARNING:NO EQTS RESULTS, reducing deg to 2
infer.eqt:WARNING:NO EQTS RESULTS, reducing deg to 1
infer.eqt:WARNING:NO EQTS RESULTS, reducing deg to 0


real    0m1.518s
user    0m1.616s
sys     0m0.047s

file content:

vtrace1; I back; I right
vtrace1; 1388.0; 220.0
vtrace1; 1419.0; 221.0
vtrace1; 1493.0; 223.0
vtrace1; 1551.0; 173.0
vtrace1; 1571.0; 173.0
vtrace1; 1650.0; 234.0
vtrace1; 1695.0; 238.0
vtrace1; 1769.0; 237.0
vtrace1; 1804.0; 236.0
vtrace1; 1842.0; 239.0
vtrace1; 1891.0; 237.0
vtrace1; 1936.0; 241.0
vtrace1; 1986.0; 239.0
vtrace1; 2037.0; 265.0
vtrace1; 2089.0; 729.0
vtrace1; 2159.0; 737.0
vtrace1; 2159.0; 737.0
vtrace1; 2253.0; 740.0
vtrace1; 2307.0; 743.0
vtrace1; 2321.0; 746.0
vtrace1; 2369.0; 746.0
vtrace1; 2390.0; 744.0
vtrace1; 2390.0; 745.0
vtrace1; 2422.0; 745.0
vtrace1; 2422.0; 745.0
vtrace1; 2446.0; 745.0
vtrace1; 2451.0; 747.0
vtrace1; 2449.0; 746.0
vtrace1; 2451.0; 752.0
vtrace1; 2451.0; 735.0
vtrace1; 2429.0; 735.0
vtrace1; 2279.0; 756.0
vtrace1; 2025.0; 766.0
vtrace1; 1623.0; 781.0
vtrace1; 1267.0; 300.0
vtrace1; 1303.0; 282.0
vtrace1; 1400.0; 238.0
vtrace1; 1465.0; 236.0
vtrace1; 1519.0; 235.0
vtrace1; 1548.0; 234.0
vtrace1; 1606.0; 231.0
vtrace1; 1606.0; 243.0
vtrace1; 1633.0; 238.0
vtrace1; 1785.0; 551.0
vtrace1; 1873.0; 539.0
vtrace1; 1905.0; 540.0
vtrace1; 1967.0; 539.0
vtrace1; 2026.0; 538.0
vtrace1; 2083.0; 536.0
vtrace1; 2169.0; 534.0
vtrace1; 2254.0; 532.0
vtrace1; 2254.0; 541.0
vtrace1; 2281.0; 541.0
vtrace1; 2302.0; 531.0
vtrace1; 2290.0; 529.0
vtrace1; 2242.0; 531.0
vtrace1; 2242.0; 530.0
vtrace1; 2242.0; 533.0
vtrace1; 2250.0; 533.0
vtrace1; 2159.0; 539.0
vtrace1; 1984.0; 545.0
vtrace1; 1743.0; 556.0
vtrace1; 1431.0; 563.0
vtrace1; 1431.0; 573.0

Using dynamically generated invariants to help static analyzers to prove properties that they cannot prove previously

New Project Idea: Automatic way to help existing Verification tools
- Ultimate cannot verify a postcond
- Run DIG to get cand loop invariants
- Run Ultimate to verify candidate invs
  - Loop: do this until can verify all candidate invs (or find counterexamples to remove them)
  - The reason is that it could be that Ultimate cannot verify some candidate invariants and only can prove them AFTER proving some other candidate ones
- Assume proved invariants
- Run Ultimate to prove postcond it cannot prove before
Benchmarks
- SV-COMP NLA
- some other ones ?
- Multiple verification tools? Seahorn, Ultimate Tapan, Ultimate Anomizer, CPAChecker etc
Implementation Details
- Use multiple verifiers to prove properties, run them simultaneously

replace symbolic execution with fuzzing

AttributeError exception

Hi,

I have this problem when running Dig

sage -python -O src/dig.py tests/traces/CohenDiv.tcs 
Traceback (most recent call last):
  File "src/dig.py", line 239, in <module>
    dig.start(seed=seed, maxdeg=args.maxdeg)
  File "/tools/dig/src/alg.py", line 321, in start
    wrs = CM.run_mp("(pure) dynamic inference", tasks, f, settings.DO_MP)
AttributeError: module 'helpers.vcommon' has no attribute 'run_mp'

below is the input/output (force quit after running for 3 hours)

root@2f4594d66a76:/dig/src# sage -python -O dig.py  ../tests/paper/CohenDiv.java -log 3
settings:INFO:2021-09-10 00:09:12.407921: dig.py ../tests/paper/CohenDiv.java -log 3
alg:INFO:analyze '../tests/paper/CohenDiv.java'
get symstates:running 24 jobs using 8 threads: [3, 3, 3, 3, 3, 3, 3, 3]
symstates exprs:running 66 jobs using 8 threads: [8, 8, 8, 8, 8, 8, 9, 9]
alg:INFO:compute symbolic states (61.68s)
alg:INFO:infer invs at 3 locs: vtrace0, vtrace2, vtrace1
get traces:running 9 jobs using 8 threads: [1, 1, 1, 1, 1, 1, 1, 2]
get traces:running 112 jobs using 8 threads: [14, 14, 14, 14, 14, 14, 14, 14]
find eqts:running 3 jobs using 3 threads: [1, 1, 1]
prove:running 5 jobs using 5 threads: [1, 1, 1, 1, 1]
prove:running 3 jobs using 3 threads: [1, 1, 1]
prove:running 8 jobs using 8 threads: [1, 1, 1, 1, 1, 1, 1, 1]
prove:running 5 jobs using 5 threads: [1, 1, 1, 1, 1]
prove:running 8 jobs using 8 threads: [1, 1, 1, 1, 1, 1, 1, 1]
prove:running 2 jobs using 2 threads: [1, 1]
prove:running 5 jobs using 5 threads: [1, 1, 1, 1, 1]
prove:running 7 jobs using 7 threads: [1, 1, 1, 1, 1, 1, 1]
prove:running 7 jobs using 7 threads: [1, 1, 1, 1, 1, 1, 1]
prove:running 3 jobs using 3 threads: [1, 1, 1]
prove:running 6 jobs using 6 threads: [1, 1, 1, 1, 1, 1]
prove:running 9 jobs using 8 threads: [1, 1, 1, 1, 1, 1, 1, 2]
prove:running 4 jobs using 4 threads: [1, 1, 1, 1]
prove:running 4 jobs using 4 threads: [1, 1, 1, 1]
^CTraceback (most recent call last):
  File "/dig/src/dig.py", line 239, in <module>
    dig.start(seed=seed, maxdeg=args.maxdeg)
  File "/dig/src/alg.py", line 135, in start
    self.infer(self.EQTS, dinvs, lambda: self.infer_eqts(maxdeg, dtraces, inps))
  File "/dig/src/alg.py", line 186, in infer
    new_invs = f()  # get invs
  File "/dig/src/alg.py", line 135, in <lambda>
    self.infer(self.EQTS, dinvs, lambda: self.infer_eqts(maxdeg, dtraces, inps))
  File "/dig/src/alg.py", line 205, in infer_eqts
    dinvs = solver.gen(auto_deg, dtraces, inps)
  File "/dig/src/infer/eqt.py", line 44, in gen
    wrs = CM.run_mp("find eqts", tasks, f, settings.DO_MP)
  File "/dig/src/helpers/vcommon.py", line 165, in run_mp
    rs = Q.get()
  File "/usr/lib/python3.9/multiprocessing/queues.py", line 103, in get
    res = self._recv_bytes()
  File "/usr/lib/python3.9/multiprocessing/connection.py", line 221, in recv_bytes
    buf = self._recv_bytes(maxlength)
  File "/usr/lib/python3.9/multiprocessing/connection.py", line 419, in _recv_bytes
    buf = self._recv(4)
  File "/usr/lib/python3.9/multiprocessing/connection.py", line 384, in _recv
    chunk = read(handle, remaining)
  File "src/cysignals/signals.pyx", line 320, in cysignals.signals.python_check_interrupt
KeyboardInterrupt
^CError in atexit._run_exitfuncs:
Traceback (most recent call last):
  File "/usr/lib/python3.9/multiprocessing/popen_fork.py", line 27, in poll
    pid, sts = os.waitpid(self.pid, flag)
  File "src/cysignals/signals.pyx", line 320, in cysignals.signals.python_check_interrupt
KeyboardInterrupt

^Croot@2f4594d66a76:/dig/src# ^C