Fixes for overflow issues

c/nla-digbench/divbin.c

@@ -3,8 +3,10 @@
   returns A//B
 */
 
+#include <limits.h>
+
 extern void __VERIFIER_error() __attribute__((__noreturn__));
-extern int __VERIFIER_nondet_int(void);
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
 extern void __VERIFIER_assume(int expression);
 void __VERIFIER_assert(int cond) {
     if (!(cond)) {
@@ -15,10 +17,11 @@ void __VERIFIER_assert(int cond) {
 }
 
 int main() {
-    int A, B;
-    int q, r, b;
-    A = __VERIFIER_nondet_int();
-    B = __VERIFIER_nondet_int();
+  unsigned A, B;
+  unsigned q, r, b;
+    A = __VERIFIER_nondet_unsigned_int();
+    B = __VERIFIER_nondet_unsigned_int();
+    __VERIFIER_assume(B < UINT_MAX/2);
     __VERIFIER_assume(B >= 1);
 
     q = 0;
@@ -45,4 +48,3 @@ int main() {
     __VERIFIER_assert(A == q * b + r);
     return 0;
 }
-

c/nla-digbench/divbin.i

@@ -0,0 +1,37 @@
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+int main() {
+  unsigned A, B;
+  unsigned q, r, b;
+    A = __VERIFIER_nondet_unsigned_int();
+    B = __VERIFIER_nondet_unsigned_int();
+    __VERIFIER_assume(B < (0x7fffffff * 2U + 1U)/2);
+    __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

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

c/nla-digbench/knuth.c

@@ -1,7 +1,9 @@
 /* algorithm searching for a divisor for factorization, by Knuth */
 
+#include <limits.h>
+
 extern void __VERIFIER_error() __attribute__((__noreturn__));
-extern int __VERIFIER_nondet_int(void);
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
 extern void __VERIFIER_assume(int expression);
 void __VERIFIER_assert(int cond) {
     if (!(cond)) {
@@ -14,10 +16,11 @@ void __VERIFIER_assert(int cond) {
 extern double sqrt(double);
 
 int main() {
-    int n, a;
-    int r, k, q, d, s, t;
-    n = __VERIFIER_nondet_int();
-    a = __VERIFIER_nondet_int();
+    unsigned n, a;
+    unsigned r, k, q, d, s, t;
+    n = __VERIFIER_nondet_unsigned_int();
+    a = __VERIFIER_nondet_unsigned_int();
+    __VERIFIER_assume(n < UINT_MAX/8);
     __VERIFIER_assume(a > 2);
 
     d = a;
@@ -35,18 +38,18 @@ int main() {
 
         if (!((s >= d) && (r != 0))) break;
 
-        if (2 * r - k + q < 0) {
+        if (2 * r  + q < k) {
             t = r;
             r = 2 * r - k + q + d + 2;
             k = t;
             q = q + 4;
             d = d + 2;
-        } else if ((2 * r - k + q >= 0) && (2 * r - k + q < d + 2)) {
+        } else if ((2 * r  + q >= k) && (2 * r + q < d + k + 2)) {
             t = r;
             r = 2 * r - k + q;
             k = t;
             d = d + 2;
-        } else if ((2 * r - k + q >= 0) && (2 * r - k + q >= d + 2) && (2 * r - k + q < 2 * d + 4)) {
+        } else if ((2 * r  + q >= k) && (2 * r + q >= d + k + 2) && (2 * r + q < 2 * d + k + 4)) {
             t = r;
             r = 2 * r - k + q - d - 2;
             k = t;

c/nla-digbench/knuth.i

@@ -0,0 +1,57 @@
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+extern double sqrt(double);
+int main() {
+    unsigned n, a;
+    unsigned r, k, q, d, s, t;
+    n = __VERIFIER_nondet_unsigned_int();
+    a = __VERIFIER_nondet_unsigned_int();
+    __VERIFIER_assume(n < (0x7fffffff * 2U + 1U)/8);
+    __VERIFIER_assume(a > 2);
+    d = a;
+    r = n % d;
+    t = 0;
+    k = n % (d - 2);
+    q = 4 * (n / (d - 2) - n / d);
+    s = sqrt(n);
+    while (1) {
+        __VERIFIER_assert(d * d * q - 2 * q * d - 4 * r * d + 4 * k * d + 8 * r == 8 * n);
+        __VERIFIER_assert(k * t == t * t);
+        __VERIFIER_assert(d * d * q - 2 * d * q - 4 * d * r + 4 * d * t + 4 * a * k - 4 * a * t - 8 * n + 8 * r == 0);
+        __VERIFIER_assert(d * k - d * t - a * k + a * t == 0);
+        if (!((s >= d) && (r != 0))) break;
+        if (2 * r + q < k) {
+            t = r;
+            r = 2 * r - k + q + d + 2;
+            k = t;
+            q = q + 4;
+            d = d + 2;
+        } else if ((2 * r + q >= k) && (2 * r + q < d + k + 2)) {
+            t = r;
+            r = 2 * r - k + q;
+            k = t;
+            d = d + 2;
+        } else if ((2 * r + q >= k) && (2 * r + q >= d + k + 2) && (2 * r + q < 2 * d + k + 4)) {
+            t = r;
+            r = 2 * r - k + q - d - 2;
+            k = t;
+            q = q - 4;
+            d = d + 2;
+        } else {
+            t = r;
+            r = 2 * r - k + q - 2 * d - 4;
+            k = t;
+            q = q - 8;
+            d = d + 2;
+        }
+    }
+    return 0;
+}

c/nla-digbench/knuth.yml

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

c/nla-digbench/lcm1.c

@@ -1,10 +1,10 @@
-/* 
- * algorithm for computing simultaneously the GCD and the LCM, 
- * by Sankaranarayanan 
+/*
+ * algorithm for computing simultaneously the GCD and the LCM,
+ * by Sankaranarayanan
  */
 
 extern void __VERIFIER_error() __attribute__((__noreturn__));
-extern int __VERIFIER_nondet_int(void);
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
 extern void __VERIFIER_assume(int expression);
 void __VERIFIER_assert(int cond) {
     if (!(cond)) {
@@ -15,13 +15,16 @@ void __VERIFIER_assert(int cond) {
 }
 
 int main() {
-    int a, b;
-    int x, y, u, v;
-    a = __VERIFIER_nondet_int();
-    b = __VERIFIER_nondet_int();
+    unsigned a, b;
+    unsigned x, y, u, v;
+    a = __VERIFIER_nondet_unsigned_int();
+    b = __VERIFIER_nondet_unsigned_int();
     __VERIFIER_assume(a >= 1);  //infinite loop if remove
     __VERIFIER_assume(b >= 1);
 
+    __VERIFIER_assume(a <= 65535);
+    __VERIFIER_assume(b <= 65535);
+
     x = a;
     y = b;
     u = b;
@@ -48,10 +51,10 @@ int main() {
             u = u + v;
         }
     }
-    
+
     __VERIFIER_assert(u*y + v*y == a*b);
     __VERIFIER_assert(x == y);
-    
+
     //x == gcd(a,b)
     //u + v == lcm(a,b)
     return 0;

c/nla-digbench/lcm2.c

@@ -1,6 +1,7 @@
 /* Algorithm for computing simultaneously the GCD and the LCM, by Dijkstra */
+
 extern void __VERIFIER_error() __attribute__((__noreturn__));
-extern int __VERIFIER_nondet_int(void);
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
 extern void __VERIFIER_assume(int expression);
 void __VERIFIER_assert(int cond) {
     if (!(cond)) {
@@ -13,11 +14,14 @@ void __VERIFIER_assert(int cond) {
 int main() {
     int a, b;
     int x, y, u, v;
-    a = __VERIFIER_nondet_int();
-    b = __VERIFIER_nondet_int();
+    a = __VERIFIER_nondet_unsigned_int();
+    b = __VERIFIER_nondet_unsigned_int();
     __VERIFIER_assume(a >= 1); //inf loop if remove
     __VERIFIER_assume(b >= 1);
 
+    __VERIFIER_assume(a <= 65535);
+    __VERIFIER_assume(b <= 65535);
+
     x = a;
     y = b;
     u = b;