Fixing benchmarks with overflows from nla-digibench

c/nla-digbench/bresenham-ll.c

@@ -0,0 +1,51 @@
+/*
+  Bresenham's line drawing algorithm 
+  from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10 
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "bresenham-ll.c", 7, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int X, Y;
+    long long x, y, v, xy, yx;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
+    y = 0;
+    x = 0;
+
+    while (1) {
+        yx = (long long) Y*x;
+        xy = (long long) X*y;
+	__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + (long long) 2 * Y;
+        } else {
+            v = v + 2 * ((long long) Y - X);
+            y++;
+        }
+        x++;
+    }
+    xy = (long long) x*y;
+    yx = (long long) Y*x;
+    __VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
+
+    return 0;
+}

c/nla-digbench/bresenham-ll.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'bresenham-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/nla-digbench/bresenham.yml

@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'bresenham.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C

c/nla-digbench/cohencu-ll.c

@@ -0,0 +1,55 @@
+/*
+Printing consecutive cubes, by Cohen
+http://www.cs.upc.edu/~erodri/webpage/polynomial_invariants/cohencu.htm
+*/
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "cohencu-ll.c", 8, "reach_error"); }
+extern unsigned short __VERIFIER_nondet_unsigned_short(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    short a;
+    long long n, x, y, z;
+    a = __VERIFIER_nondet_unsigned_short();
+
+    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-ll.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'cohencu-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/nla-digbench/cohencu.yml

@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'cohencu.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C

c/nla-digbench/cohendiv-ll.c

@@ -0,0 +1,64 @@
+/*
+  Cohen's integer division
+  returns x % y
+  http://www.cs.upc.edu/~erodri/webpage/polynomial_invariants/cohendiv.htm
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "cohendiv-ll.c", 8, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+	{reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int x, y;
+    long long q, r, a, b;
+
+    x = __VERIFIER_nondet_int();
+    y = __VERIFIER_nondet_int();
+
+    assume_abort_if_not(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-ll.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'cohendiv-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/nla-digbench/cohendiv.yml

@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'cohendiv.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C

c/nla-digbench/dijkstra-u.c

@@ -0,0 +1,60 @@
+/* Compute the floor of the square root, by Dijkstra */
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "dijkstra-u.c", 5, "reach_error"); }
+extern unsigned int __VERIFIER_nondet_unsigned_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    unsigned int n, p, q, r, h;
+
+    n = __VERIFIER_nondet_unsigned_int();
+    assume_abort_if_not(n < 4294967295 / 4);  // Avoid non-terminating loop
+
+    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-u.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'dijkstra-u.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/nla-digbench/dijkstra.yml

@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'dijkstra.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C

c/nla-digbench/egcd-ll.c

@@ -0,0 +1,57 @@
+/* extended Euclid's algorithm */
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "egcd-ll.c", 4, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    long long a, b, p, q, r, s;
+    int x, y;
+    x = __VERIFIER_nondet_int();
+    y = __VERIFIER_nondet_int();
+    assume_abort_if_not(x >= 1);
+    assume_abort_if_not(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;
+}

c/nla-digbench/egcd-ll.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'egcd-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32