Programs with Nonlinear Properties (#808)

* initial set of files

* add post for Dijkstra

* add sqrt1.c

* add misc files

* add freire2.c

* add egcd

* add egcd2

* add egcd3

* add lcm1

* add new files, reformat

* reformat

* all nla files

* add bresenham

* updates

* various updates

* updates

* updates expected properties and add files to ReachSafety-Loops.set

* fix a complain from travis ?

* Update README.md

c/ReachSafety-Loops.set

@@ -7,3 +7,4 @@ loop-new/*.yml
 loop-industry-pattern/*.yml
 loops-crafted-1/*.yml
 loop-invariants/*.yml
+nla-digbench/*.yml

c/nla-digbench/LICENSE.txt

@@ -0,0 +1 @@
+../../LICENSE.Apache-2.0.txt

c/nla-digbench/Makefile

@@ -0,0 +1,2 @@
+LEVEL := ../
+include $(LEVEL)/Makefile.config

c/nla-digbench/README.md

@@ -0,0 +1,48 @@
+The benchmarks in this directory were submitted by 
+ThanhVu Nguyen ([email protected]) and 
+Timos Antonopoulos ([email protected]).
+
+These programs contain nonlinear polynomial properties 
+(mostly equalities) that are challenging for program analysis.
+They were collected from various sources and  have been used in the 
+DIG (Dynamic Invariant Generation) work:
+
+* ThahhVu Nguyen, Timos Antopoulos, Andrew Ruef, and Michael Hicks. A Counterexample-guided Approach to Finding Numerical Invariants. 11th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE), pages 605--615. ACM, 2017. 
+* ThanhVu Nguyen, Matthew Dwyer, and William Visser. SymInfer: Inferring Program Invariants using Symbolic States. 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 804--814. IEEE, 2017.
+* ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. Using Dynamic Analysis to Discover Polynomial and Array Invariants.  International Conference on Software Engineering (ICSE), pages 683--693. IEEE, 2012. 
+
+
+
+## Programs
+
+|    | Programs  | Description      | Variable types | Status |
+|----|-----------|------------------|----------------|--------|
+| 1  | cohendiv  | integer division | integer        | done   |
+| 2  | divbin    | integer division | integer        | done   |
+| 3  | mannadiv  | integer division | integer        | done   |
+| 4  | hard      | integer division | integer        | done   |
+| 5  | sqrt1     | square root      | integer        | done   |
+| 6  | dijkstra  | square root      | integer        | done   |
+| 7  | freire1   | square root      | double         | done?  |
+| 8  | freire2   | cubic root       | double         | done?  |
+| 9  | cohencu   | cubic sum        | integer        | done   |
+| 10 | egcd      | gcd              | integer        | done   |
+| 11 | egcd2     | gcd              | integer        | done?  |
+| 12 | egcd3     | gcd              | integer        | done?  |
+| 13 | prodbin   | gcd, lcm         | double         | done   |
+| 14 | prod4br   | gcd, lcm         | integer        | done   |
+| 15 | knuth     | product          | integer        | done   |
+| 16 | fermat1   | product          | double         | done   |
+| 17 | fermat2   | divisor          | double         | done   |
+| 18 | lcm1      | divisor          | integer        | done   |
+| 19 | lcm2      | divisor          | integer        | done   |
+| 20 | geo1      | geometric series | integer        | done   |
+| 21 | geo2      | geometric series | integer        | done   |
+| 22 | geo3      | geometric series | integer        | done   |
+| 23 | ps2       | power sum        | integer        | done   |
+| 24 | ps3       | power sum        | integer        | done   |
+| 25 | ps4       | power sum        | integer        | done   |
+| 26 | ps5       | power sum        | integer        | done   |
+| 27 | ps6       | power sum        | integer        | done   |
+| 28 | bresenham | draw             | integer        | done   |
+

c/nla-digbench/bresenham.c

@@ -0,0 +1,42 @@
+/*
+  Bresenham's line drawing algorithm 
+  from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10 
+*/
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+
+int main() {
+    int X, Y;
+    int v, x, y;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    v = 2 * Y - X;
+    y = 0;
+    x = 0;
+
+    while (1) {
+	__VERIFIER_assert(2*Y*x - 2*X*y - X + 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + 2 * Y;
+        } else {
+            v = v + 2 * (Y - X);
+            y++;
+        }
+        x++;
+    }
+    __VERIFIER_assert(2*Y*x - 2*x*y - X + 2*Y - v + 2*y == 0);
+
+    return 0;
+}

c/nla-digbench/bresenham.yml

@@ -0,0 +1,5 @@
+format_version: '1.0'
+input_files: 'bresenham.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true

c/nla-digbench/cohencu.c

@@ -0,0 +1,48 @@
+/*
+Printing consecutive cubes, by Cohen
+http://www.cs.upc.edu/~erodri/webpage/polynomial_invariants/cohencu.htm
+*/
+
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+
+int main() {
+    int a, n, x, y, z;
+    a = __VERIFIER_nondet_int();
+    n = 0;
+    x = 0;
+    y = 1;
+    z = 6;
+
+    while (1) {
+        __VERIFIER_assert(z == 6 * n + 6);
+        __VERIFIER_assert(y == 3 * n * n + 3 * n + 1);
+        __VERIFIER_assert(x == n * n * n);
+	__VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
+	__VERIFIER_assert((z*z) - 12*y - 6*z + 12 == 0);
+        if (!(n <= a))
+            break;
+
+        n = n + 1;
+        x = x + y;
+        y = y + z;
+        z = z + 6;
+    }
+
+    __VERIFIER_assert(z == 6*n + 6);
+    __VERIFIER_assert(6*a*x - x*z + 12*x == 0);
+    __VERIFIER_assert(a*z - 6*a - 2*y + 2*z - 10 == 0);
+    __VERIFIER_assert(2*y*y - 3*x*z - 18*x - 10*y + 3*z - 10 == 0);
+    __VERIFIER_assert(z*z - 12*y - 6*z + 12 == 0);
+    __VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
+
+    return 0;
+}

c/nla-digbench/cohencu.yml

@@ -0,0 +1,5 @@
+format_version: '1.0'
+input_files: 'cohencu.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true

c/nla-digbench/cohendiv.c

@@ -0,0 +1,58 @@
+/*
+  Cohen's integer division
+  returns x % y
+  http://www.cs.upc.edu/~erodri/webpage/polynomial_invariants/cohendiv.htm
+*/
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+	__VERIFIER_error();
+    }
+    return;
+}
+
+int main() {
+    int x, y, q, r, a, b;
+
+    x = __VERIFIER_nondet_int();
+    y = __VERIFIER_nondet_int();
+
+    __VERIFIER_assume(y >= 1);
+
+    q = 0;
+    r = x;
+    a = 0;
+    b = 0;
+
+    while (1) {
+	__VERIFIER_assert(b == y*a);
+	__VERIFIER_assert(x == q*y + r);
+
+	if (!(r >= y))
+	    break;
+	a = 1;
+	b = y;
+
+	while (1) {            
+	    __VERIFIER_assert(b == y*a);
+	    __VERIFIER_assert(x == q*y + r);
+	    __VERIFIER_assert(r >= 0);
+
+	    if (!(r >= 2 * b))
+		break;
+
+	    __VERIFIER_assert(r >= 2 * y * a);
+
+	    a = 2 * a;
+	    b = 2 * b;
+	}
+	r = r - b;
+	q = q + a;
+    }
+
+    __VERIFIER_assert(x == q*y + r);
+    return 0;
+}

c/nla-digbench/cohendiv.yml

@@ -0,0 +1,5 @@
+format_version: '1.0'
+input_files: 'cohendiv.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true

c/nla-digbench/dijkstra.c

@@ -0,0 +1,54 @@
+/* Compute the floor of the square root, by Dijkstra */
+
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+
+int main() {
+    int n, p, q, r, h;
+
+    n = __VERIFIER_nondet_int();
+
+    p = 0;
+    q = 1;
+    r = n;
+    h = 0;
+    while (1) {
+        if (!(q <= n))
+            break;
+
+        q = 4 * q;
+    }
+    //q == 4^n
+
+    while (1) {
+        __VERIFIER_assert(r < 2 * p + q);
+        __VERIFIER_assert(p*p + r*q == n*q);
+        __VERIFIER_assert(h * h * h - 12 * h * n * q + 16 * n * p * q - h * q * q - 4 * p * q * q + 12 * h * q * r - 16 * p * q * r == 0);
+        __VERIFIER_assert(h * h * n - 4 * h * n * p + 4 * (n * n) * q - n * q * q - h * h * r + 4 * h * p * r - 8 * n * q * r + q * q * r + 4 * q * r * r == 0);
+        __VERIFIER_assert(h * h * p - 4 * h * n * q + 4 * n * p * q - p * q * q + 4 * h * q * r - 4 * p * q * r == 0);
+        __VERIFIER_assert(p * p - n * q + q * r == 0);
+
+        if (!(q != 1))
+            break;
+
+        q = q / 4;
+        h = p + q;
+        p = p / 2;
+        if (r >= h) {
+            p = p + q;
+            r = r - h;
+        }
+    }
+    __VERIFIER_assert(h*h*h - 12*h*n + 16*n*p + 12*h*r - 16*p*r - h - 4*p == 0);
+    __VERIFIER_assert(p*p - n + r == 0);
+    __VERIFIER_assert(h*h*p - 4*h*n + 4*n*p + 4*h*r - 4*p*r - p == 0);
+    return 0;
+}

c/nla-digbench/dijkstra.yml

@@ -0,0 +1,5 @@
+format_version: '1.0'
+input_files: 'dijkstra.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true

c/nla-digbench/divbin.c

@@ -0,0 +1,48 @@
+/*
+  A division algorithm, by Kaldewaij
+  returns A//B
+*/
+
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+
+int main() {
+    int A, B;
+    int q, r, b;
+    A = __VERIFIER_nondet_int();
+    B = __VERIFIER_nondet_int();
+    __VERIFIER_assume(B >= 1);
+
+    q = 0;
+    r = A;
+    b = B;
+
+    while (1) {
+        if (!(r >= b)) break;
+        b = 2 * b;
+    }
+
+    while (1) {
+        __VERIFIER_assert(A == q * b + r);
+        if (!(b != B)) break;
+
+        q = 2 * q;
+        b = b / 2;
+        if (r >= b) {
+            q = q + 1;
+            r = r - b;
+        }
+    }
+
+    __VERIFIER_assert(A == q * b + r);
+    return 0;
+}
+

c/nla-digbench/divbin.yml

@@ -0,0 +1,5 @@
+format_version: '1.0'
+input_files: 'divbin.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true

c/nla-digbench/egcd.c

@@ -0,0 +1,52 @@
+/* extended Euclid's algorithm */
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+
+int main() {
+    int a, b, p, q, r, s;
+    int x, y;
+    x = __VERIFIER_nondet_int();
+    y = __VERIFIER_nondet_int();
+    __VERIFIER_assume(x >= 1);
+    __VERIFIER_assume(y >= 1);
+
+    a = x;
+    b = y;
+    p = 1;
+    q = 0;
+    r = 0;
+    s = 1;
+
+    while (1) {
+        __VERIFIER_assert(1 == p * s - r * q);
+        __VERIFIER_assert(a == y * r + x * p);
+        __VERIFIER_assert(b == x * q + y * s);
+
+        if (!(a != b))
+            break;
+
+        if (a > b) {
+            a = a - b;
+            p = p - q;
+            r = r - s;
+        } else {
+            b = b - a;
+            q = q - p;
+            s = s - r;
+        }
+    }
+
+    __VERIFIER_assert(a - b == 0);    
+    __VERIFIER_assert(p*x + r*y - b == 0);
+    __VERIFIER_assert(q*r - p*s + 1 == 0);
+    __VERIFIER_assert(q*x + s*y - b == 0);
+    return 0;
+}