Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit b7fe5c3

Browse files
dbeyerdbeyer
authored
Merge pull request #1155 from divyeshunadkat/master
Fixing benchmarks with overflows from nla-digibench
2 parents 0a87f6c + 9166aa3 commit b7fe5c3

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

69 files changed

+1498
-43
lines changed

‎c/nla-digbench/bresenham-ll.c‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
/*
2+
Bresenham's line drawing algorithm
3+
from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10
4+
*/
5+
extern void abort(void);
6+
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
7+
void reach_error() { __assert_fail("0", "bresenham-ll.c", 7, "reach_error"); }
8+
extern int __VERIFIER_nondet_int(void);
9+
extern void abort(void);
10+
void assume_abort_if_not(int cond) {
11+
if(!cond) {abort();}
12+
}
13+
void __VERIFIER_assert(int cond) {
14+
if (!(cond)) {
15+
ERROR:
16+
{reach_error();}
17+
}
18+
return;
19+
}
20+
21+
int main() {
22+
int X, Y;
23+
long long x, y, v, xy, yx;
24+
X = __VERIFIER_nondet_int();
25+
Y = __VERIFIER_nondet_int();
26+
v = ((long long) 2 * Y) - X; // cast required to avoid int overflow
27+
y = 0;
28+
x = 0;
29+
30+
while (1) {
31+
yx = (long long) Y*x;
32+
xy = (long long) X*y;
33+
__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
34+
if (!(x <= X))
35+
break;
36+
// out[x] = y
37+
38+
if (v < 0) {
39+
v = v + (long long) 2 * Y;
40+
} else {
41+
v = v + 2 * ((long long) Y - X);
42+
y++;
43+
}
44+
x++;
45+
}
46+
xy = (long long) x*y;
47+
yx = (long long) Y*x;
48+
__VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
49+
50+
return 0;
51+
}

‎c/nla-digbench/bresenham-ll.yml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
format_version: '2.0'
2+
input_files: 'bresenham-ll.c'
3+
properties:
4+
- property_file: ../properties/unreach-call.prp
5+
expected_verdict: true
6+
- property_file: ../properties/no-overflow.prp
7+
expected_verdict: true
8+
9+
options:
10+
language: C
11+
data_model: ILP32

‎c/nla-digbench/bresenham.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
format_version: '2.0'
22
input_files: 'bresenham.c'
33
properties:
4-
- property_file: ../properties/unreach-call.prp
5-
expected_verdict: true
4+
- property_file: ../properties/no-overflow.prp
5+
expected_verdict: false
66

77
options:
88
language: C

‎c/nla-digbench/cohencu-ll.c‎

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
/*
2+
Printing consecutive cubes, by Cohen
3+
http://www.cs.upc.edu/~erodri/webpage/polynomial_invariants/cohencu.htm
4+
*/
5+
6+
extern void abort(void);
7+
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
8+
void reach_error() { __assert_fail("0", "cohencu-ll.c", 8, "reach_error"); }
9+
extern unsigned short __VERIFIER_nondet_unsigned_short(void);
10+
extern void abort(void);
11+
void assume_abort_if_not(int cond) {
12+
if(!cond) {abort();}
13+
}
14+
void __VERIFIER_assert(int cond) {
15+
if (!(cond)) {
16+
ERROR:
17+
{reach_error();}
18+
}
19+
return;
20+
}
21+
22+
int main() {
23+
short a;
24+
long long n, x, y, z;
25+
a = __VERIFIER_nondet_unsigned_short();
26+
27+
n = 0;
28+
x = 0;
29+
y = 1;
30+
z = 6;
31+
32+
while (1) {
33+
__VERIFIER_assert(z == 6 * n + 6);
34+
__VERIFIER_assert(y == 3 * n * n + 3 * n + 1);
35+
__VERIFIER_assert(x == n * n * n);
36+
__VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
37+
__VERIFIER_assert((z*z) - 12*y - 6*z + 12 == 0);
38+
if (!(n <= a))
39+
break;
40+
41+
n = n + 1;
42+
x = x + y;
43+
y = y + z;
44+
z = z + 6;
45+
}
46+
47+
__VERIFIER_assert(z == 6*n + 6);
48+
__VERIFIER_assert(6*a*x - x*z + 12*x == 0);
49+
__VERIFIER_assert(a*z - 6*a - 2*y + 2*z - 10 == 0);
50+
__VERIFIER_assert(2*y*y - 3*x*z - 18*x - 10*y + 3*z - 10 == 0);
51+
__VERIFIER_assert(z*z - 12*y - 6*z + 12 == 0);
52+
__VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
53+
54+
return 0;
55+
}

‎c/nla-digbench/cohencu-ll.yml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
format_version: '2.0'
2+
input_files: 'cohencu-ll.c'
3+
properties:
4+
- property_file: ../properties/unreach-call.prp
5+
expected_verdict: true
6+
- property_file: ../properties/no-overflow.prp
7+
expected_verdict: true
8+
9+
options:
10+
language: C
11+
data_model: ILP32

‎c/nla-digbench/cohencu.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
format_version: '2.0'
22
input_files: 'cohencu.c'
33
properties:
4-
- property_file: ../properties/unreach-call.prp
5-
expected_verdict: true
4+
- property_file: ../properties/no-overflow.prp
5+
expected_verdict: false
66

77
options:
88
language: C

‎c/nla-digbench/cohendiv-ll.c‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
/*
2+
Cohen's integer division
3+
returns x % y
4+
http://www.cs.upc.edu/~erodri/webpage/polynomial_invariants/cohendiv.htm
5+
*/
6+
extern void abort(void);
7+
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
8+
void reach_error() { __assert_fail("0", "cohendiv-ll.c", 8, "reach_error"); }
9+
extern int __VERIFIER_nondet_int(void);
10+
extern void abort(void);
11+
void assume_abort_if_not(int cond) {
12+
if(!cond) {abort();}
13+
}
14+
void __VERIFIER_assert(int cond) {
15+
if (!(cond)) {
16+
ERROR:
17+
{reach_error();}
18+
}
19+
return;
20+
}
21+
22+
int main() {
23+
int x, y;
24+
long long q, r, a, b;
25+
26+
x = __VERIFIER_nondet_int();
27+
y = __VERIFIER_nondet_int();
28+
29+
assume_abort_if_not(y >= 1);
30+
31+
q = 0;
32+
r = x;
33+
a = 0;
34+
b = 0;
35+
36+
while (1) {
37+
__VERIFIER_assert(b == y*a);
38+
__VERIFIER_assert(x == q*y + r);
39+
40+
if (!(r >= y))
41+
break;
42+
a = 1;
43+
b = y;
44+
45+
while (1) {
46+
__VERIFIER_assert(b == y*a);
47+
__VERIFIER_assert(x == q*y + r);
48+
__VERIFIER_assert(r >= 0);
49+
50+
if (!(r >= 2 * b))
51+
break;
52+
53+
__VERIFIER_assert(r >= 2 * y * a);
54+
55+
a = 2 * a;
56+
b = 2 * b;
57+
}
58+
r = r - b;
59+
q = q + a;
60+
}
61+
62+
__VERIFIER_assert(x == q*y + r);
63+
return 0;
64+
}

‎c/nla-digbench/cohendiv-ll.yml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
format_version: '2.0'
2+
input_files: 'cohendiv-ll.c'
3+
properties:
4+
- property_file: ../properties/unreach-call.prp
5+
expected_verdict: true
6+
- property_file: ../properties/no-overflow.prp
7+
expected_verdict: true
8+
9+
options:
10+
language: C
11+
data_model: ILP32

‎c/nla-digbench/cohendiv.yml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
format_version: '2.0'
22
input_files: 'cohendiv.c'
33
properties:
4-
- property_file: ../properties/unreach-call.prp
5-
expected_verdict: true
4+
- property_file: ../properties/no-overflow.prp
5+
expected_verdict: false
66

77
options:
88
language: C

‎c/nla-digbench/dijkstra-u.c‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
/* Compute the floor of the square root, by Dijkstra */
2+
3+
extern void abort(void);
4+
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
5+
void reach_error() { __assert_fail("0", "dijkstra-u.c", 5, "reach_error"); }
6+
extern unsigned int __VERIFIER_nondet_unsigned_int(void);
7+
extern void abort(void);
8+
void assume_abort_if_not(int cond) {
9+
if(!cond) {abort();}
10+
}
11+
void __VERIFIER_assert(int cond) {
12+
if (!(cond)) {
13+
ERROR:
14+
{reach_error();}
15+
}
16+
return;
17+
}
18+
19+
int main() {
20+
unsigned int n, p, q, r, h;
21+
22+
n = __VERIFIER_nondet_unsigned_int();
23+
assume_abort_if_not(n < 4294967295 / 4); // Avoid non-terminating loop
24+
25+
p = 0;
26+
q = 1;
27+
r = n;
28+
h = 0;
29+
while (1) {
30+
if (!(q <= n))
31+
break;
32+
33+
q = 4 * q;
34+
}
35+
//q == 4^n
36+
37+
while (1) {
38+
__VERIFIER_assert(r < 2 * p + q);
39+
__VERIFIER_assert(p*p + r*q == n*q);
40+
__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);
41+
__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);
42+
__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);
43+
__VERIFIER_assert(p * p - n * q + q * r == 0);
44+
45+
if (!(q != 1))
46+
break;
47+
48+
q = q / 4;
49+
h = p + q;
50+
p = p / 2;
51+
if (r >= h) {
52+
p = p + q;
53+
r = r - h;
54+
}
55+
}
56+
__VERIFIER_assert(h*h*h - 12*h*n + 16*n*p + 12*h*r - 16*p*r - h - 4*p == 0);
57+
__VERIFIER_assert(p*p - n + r == 0);
58+
__VERIFIER_assert(h*h*p - 4*h*n + 4*n*p + 4*h*r - 4*p*r - p == 0);
59+
return 0;
60+
}

0 commit comments

Comments
 (0)