Here, we list all benchmarks from Complexity_C_Size_Non_Linear and provide sources and context for all 15 programs. The benchmarks can be downloaded here. To test our benchmarks, we suggest to use our web interface for C programs.
size01.c
This benchmark is a simple linear loop which has linear size bounds. It corresponds to the loop from our paper.
int size01(int a, int b, int c, int d) {
while(a > 0) {
a = a - 1;
int b_ = b;
int c_ = c;
b = 3*b_ + 2*c_;
c = -5*b_ -3*c_;
d = a*a + d;
}
return 0;
}
size02.c
This benchmark consists of the benchmark size01.c and a consecutive loop.
int size02(int a, int b, int c, int d) {
while(a > 0) {
a = a - 1;
int b_ = b;
int c_ = c;
b = 3*b_ + 2*c_;
c = -5*b_ -3*c_;
d = a*a + d;
}
while(b + c > 0) {
b = b - 1;
c = c - 1;
}
return 0;
}
size03.c
This benchmark consists of the benchmark size01.c and a consecutive loop.
int size03(int a, int b, int c, int d) {
while(a > 0) {
a = a - 1;
int b_ = b;
int c_ = c;
b = 3*b_ + 2*c_;
c = -5*b_ -3*c_;
d = a*a + d;
}
while(d > 0) {
d = d - 1;
}
return 0;
}
size04.c
This benchmark is a combination of size02.c and size03.c.
int size04(int a, int b, int c, int d) {
while(a > 0) {
a = a - 1;
int b_ = b;
int c_ = c;
b = 3*b_ + 2*c_;
c = -5*b_ -3*c_;
d = a*a + d;
}
while(b + c + d > 0) {
b = b - 1;
c = c - 1;
d = d - 1;
}
return 0;
}
size05.c
The first loop needs our twn-technique to prove termination.
int size05(int a, int b, int c) {
while(a > 0 && c != 0) {
a = a - b*b;
b = b + c*c;
}
while(b > 0) {
b = b - 1;
}
return 0;
}
size06.c
This program consists of three consecutive loops.
The first loop can be solved by MΦRFs of depth 2 (see Ben-Amram & Genaim here, Table 1 - Loop 20) or our twn-technique.
The second loop is a twn-loop which terminates as a eventually outgrows b*b.
The last loop decreases a until it becomes non-positive.
int size06(int a, int b, int c) {
if(a > 0) {
while(c > 0) {
a = a + c;
c = c - 1;
}
while(a < b*b) {
a = a + c*c;
b = b + 1;
c = c + 1;
}
while(a > 0) {
a = a - 1;
}
}
return 0;
}
size07.c
The first loop has the eigenvalues 0 and 1. The second loop only has the eigenvalue 1. Hence, both loops are unit prs loops and thus both have polynomial size bounds. This benchmark also contains non-linear arithmetic.
int size07(int a, int b, int c, int d) {
while(a > 0) {
a = a - 1;
int b_ = b;
int c_ = c;
b = 3*b_ + c_;
c = -6*b_ - 2*c_;
d = d + 2*a*a;
}
while(b + d > 0) {
b = b - 1;
d = d - 1;
}
return 0;
}
size08.c
This benchmark is a terminating version of the twn-loop Frohn et al., Ex. 24) with a consecutive second loop.
To ensure termination, we have added the precondition and invariant c < 0.
Thus, the value of a always decreases, and at some point is less than -b*b.
Additionally, we have added a consecutive loop to decrease b.
int size08(int a, int b, int c) {
if (c < 0) {
while(a + b*b > 0) {
a = a + b*b*c;
b = b - 2*c*c;
c = c;
}
}
b = b*b;
while(b > 0) {
b = b - 1;
}
return 0;
}
size09.c
This benchmark corresponds to the running example of our paper.
int size09(int a, int b, int c, int d, int e) {
if(a > 0 && e > 0) {
while(e > 0) {
while(a > 0) {
a = a - 1;
int b_ = b;
int c_ = c;
b = 3*b_ + 2*c_;
c = -5*b_ -3*c_;
d = a*a + d;
}
while(b > 0) {
b = b - 1;
}
a = e;
b = 2*e;
c = 3*e;
d = a;
e = e - 1;
}
}
return 0;
}
size10.c
This benchmark is an advanced version of our running example size09.c.
int size10(int a, int b, int c, int d, int e) {
if(a > 0 && e > 0) {
while(e > 0) {
while(a > 0) {
a = a - 1;
int b_ = b;
int c_ = c;
b = 3*b_ + 2*c_;
c = -5*b_ -3*c_;
d = a*a + d;
}
while(b + d > 0) {
b = b - 1;
d = d - 1;
}
a = e;
b = 2*e;
c = 3*e;
d = a;
e = e - 1;
}
}
return 0;
}
size11.c
This program is the example of Ben-Amram et al. but we have added a consecutive loop which decreases a until it is negative.
Note that all variables have polynomial size bounds in this program.
However, KoAT2 currently only infers polynomial bounds for b and e.
extern int __VERIFIER_nondet_int(void);
int size11(int a, int b, int c, int d, int e) {
while(e > 0) {
e = e - 1;
int u = __VERIFIER_nondet_int();
if(u > 0) {
c = a + b;
d = b;
} else {
c = b;
d = a + b;
}
a = c + d;
}
while(a > 0) {
a = a - 1;
}
return 0;
}
size12.c
This program is the motivating example of Ben-Amram and Hamilton. Again, all variables have polynomial size bounds in this program.
extern int __VERIFIER_nondet_int(void);
int size12(int a, int b, int c, int d) {
int t1 = a;
int t2 = 0;
while(t1 > 0) {
t1 = t1 - 1;
t2 = b + c;
while(t2 > 0) {
t2 = t2 - 1;
int u = __VERIFIER_nondet_int();
if(u > 0) {
c = a;
b = d;
} else {
c = d;
b = a;
}
}
d = b + c;
}
while(d > 0) {
d = d - 1;
int u = __VERIFIER_nondet_int();
if(u > 0) {
c = a + b + c;
} else {
c = b;
b = a;
}
}
return 0;
}
size13.c
A simplified variant of size13.koat where we additionally added non-linear arithmetic.
int size13(int a, int b, int c, int d) {
int t1 = a;
int t2 = 0;
int t3 = 0;
while(t1 > 0) {
t1 = t1 - 1;
t2 = b + c;
t3 = t3 + t1*t1;
while(t2 > 0) {
t2 = t2 - 1;
c = a;
b = d;
}
d = b;
}
while(t3 > 0) {
t3 = t3 - 1;
}
return 0;
}
size14.c
The first loop is not a solvable loop.
However, the update still admits a closed form for b.
Currently, KoAT cannot handle this example and thus does not infer a (super-exponential) runtime bound.
int size14(int a, int b) {
b = 2;
while(a > 0) {
a = a - 1;
b = b*b;
}
while(b > 0) {
b = b - 1;
}
return 0;
}
size15.c
This example combines an integer program which needs control-flow refinement (see Giesl et al. here, Fig.7) to be solved, a twn-loop, and a consecutive loop counting down b.
extern int __VERIFIER_nondet_int(void);
void size15(int x, int y, int f, int a, int b, int c) {
int u = __VERIFIER_nondet_int();
int v = __VERIFIER_nondet_int();
x = u;
f = v;
while (1) {
if (1 <= x && x <= 3 && f == 0) {
x = x + 1;
v = __VERIFIER_nondet_int();
f = v;
} else if (y > 1 && f == 1) {
y = y - 1;
v = __VERIFIER_nondet_int();
f = v;
} else {
while(a < b && c != 0) {
a = a + c*c*c;
b = b + c*c;
c = c + 1;
}
break;
}
}
while(b > 0) {
b = b - 1;
}
}