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

[TaihuLight]

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

[nguyenthanhvuh]

hm, I don't have any problem with this program. In 3.6s, DIG found 2 invs vtrace (2 invs):

1. y^2 - 2*x + y + 2 == 0
2. -y <= 0

I am using a powerful computer but older machine shouldn't have memory problem with this either.

You can try (i) remove the -nomp option, this allows DIG to run in parallel and takes advantage of multicore processing and may be (ii) reduce the loop from x <= 100 to x <= 10 to see if that helps in your case.

tnguyen@origin ~/d/src (dev)> time sage -python -O dig.py  t.c  -log 3
settings:INFO:2021-07-01 10:11:26.380328: dig.py t.c -log 3
alg:INFO:analyze 't.c'
alg:INFO:compute symbolic states (2.49s)
alg:INFO:infer invs at 1 locs: vtrace
infer.eqt:INFO:Reduce polynomial degree to 6, terms 36, uks 36
infer.eqt:INFO:Reduce polynomial degree to 5, terms 28, uks 28
infer.eqt:INFO:Reduce polynomial degree to 4, terms 21, uks 21
infer.eqt:INFO:Reduce polynomial degree to 3, terms 15, uks 15
infer.eqt:INFO:Reduce polynomial degree to 2, terms 10, uks 10
alg:INFO:found 1 eqts (0.75s)
data.symstates:WARNING:value of y changes frequently, skip
alg:INFO:found 3 ieqs (0.14s)
alg:INFO:found 4 minmax (0.14s)
alg:INFO:test 8 invs using 14 traces (0.04s)
alg:INFO:simplify 8 invs (0.07s)
* prog t locs 1;  invs 2 (Eqt: 1, Oct: 1) V 2 T 4 D 2;  NL 1 (2) ;
-> time eqts 0.8s, ieqs 0.1s, minmax 0.1s, simplify 0.1s, symbolic_states 2.5s, total 3.6s
-> checks  0 () change depths 0 () change vals 0 ()
-> max  0 () change depths 0 ()
runs 1
rand seed 1625152286.38, test (0, 76)
vtrace (2 invs):
1. y^2 - 2*x + y + 2 == 0
2. -y <= 0
tmpdir: /var/tmp/dig_876220609009146654_jkestvzc

[TaihuLight]

@nguyenthanhvuh Thank you. Your advice is useful, and the fixed command works in my case. However, I want to know that the generated invariants in the loop x <= 100 are same with the ones obtained in the modified loop x <= 10 ?

[nguyenthanhvuh]

As shown above, in the original program, DIG obtained 2 invariants

1. y^2 - 2*x + y + 2 == 0
2. -y <= 0

Did you get something else for the modified program?

[TaihuLight]

@nguyenthanhvuh There is no extra invariant generated for the modified program. That is, the generated invariants using DIG are same for the original and modified programs.

[TaihuLight]

@nguyenthanhvuh The newly updated DIG cannot generate trace for infer invariants from C programs. When I run the command sage -python -O dig.py bench17_potsumm2.c -log 3, DIG outputs the following result:

ly@INV:~/dig/src$ sage -python -O dig.py bench17_potsumm2.c -log 3
settings:INFO:2021-08-14 13:23:56.434022: dig.py bench17_potsumm2.c -log 3
alg:INFO:analyze 'bench17_potsumm2.c'
alg:INFO:compute symbolic states (4.60s)
alg:WARNING:vtrace: I x, I y: no symbolic states. Skip
alg:INFO:infer invs at 0 locs: 
Traceback (most recent call last):
  File "dig.py", line 252, in <module>
    dig.start(seed=seed, maxdeg=args.maxdeg)
  File "/home/ly/dig/src/alg.py", line 139, in start
    self.infer(self.EQTS, dinvs,
  File "/home/ly/dig/src/alg.py", line 200, in infer
    new_invs = f()  # get invs
  File "/home/ly/dig/src/alg.py", line 140, in <lambda>
    lambda: self.infer_eqts(maxdeg, dtraces, inps))
  File "/home/ly/dig/src/alg.py", line 217, in infer_eqts
    auto_deg = self.get_auto_deg(maxdeg)
  File "/home/ly/dig/src/alg.py", line 46, in get_auto_deg
    maxvars = max(self.inv_decls.values(), key=lambda d: len(d))
ValueError: max() arg is an empty sequence

Is there a bug that causes this problem 'no symbolic states. Skip' for the recently updated DIG? The related issue: https://github.com/unsat/dig/issues/10

[nguyenthanhvuh]

Try rebuild the instrumenter. Goto the ocaml dir and type make.

[TaihuLight]

The problem is solved. Thank you.