search

dynaroars / dig

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.
https://github.com/dynaroars/dig
MIT License
39 stars 6 forks source link

Run DIG on HOLA programs #5

Closed nguyenthanhvuh closed 3 years ago

ishimwed commented 4 years ago

Report: Every program run as expected except for the following: H08.java H11.java H41.java all produced invariants that are not strong enough. H34.java H36.java do not run because DIG cannot obtain symstates H30.java and H32.java do not run (I haven't figured out why)

nguyenthanhvuh commented 4 years ago

This is for 08 and just added an option -notermfilter , could you try to run DIG with that option for the Hola programs to see if it fix the issue with H08 ?

For H11, we need to also get the traces for n For H41, we need to get the traces for z,n,i,j, not just z,n
For H34, also need to add more vars

Also, when running Hola, we use maxdeg 2, so the whole command line is time sage -python dig.py ../tests/hola/H41.java -log 4 -maxdeg 2 -notermfilter

Haen't looked at 36,30,32 yet.

ishimwed commented 4 years ago

H34 still produces weak invariant Dig invariants:

  1. x^2 - 4xy + 4y^2 - x + 2y == 0
  2. nx - 4xy + 4y^2 - x + 2*y == 0
  3. m - 10 == 0
  4. i - x == 0
  5. -i <= 0
  6. -i + n <= 0 Known assertion: if (i==m) assert(x=2*y)