Here, we list all benchmarks from Complexity_C_Non_Linear and provide sources and context for all 20 programs. The benchmarks can be downloaded here. To test our benchmarks, we suggest to use our web interface for C programs.
twn01.c
This benchmark is a simple linear loop which does not have a ranking function over the reals (see Leike & Heizmann here, Thm. 4.5) but can be solved by our twn-technique.
int twn01(int a, int b) {
while(a < b && a > 0) {
a = 3*a;
b = 2*b;
}
return 0;
}
twn02.c
This benchmark is an advanced, slightly changed version of twn01.c by adding non-linear arithmetic.
int twn02(int a, int b, int c) {
while(a < b*b && a > 0) {
a = 5*a + c*c;
b = 2*b;
}
return 0;
}
twn03.c
This program consists of two 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 corresponds to the loop in twn02.c.
int twn03(int a, int b, int c) {
if(a > 0) {
while(c > 0) {
a = a + c;
c = c - 1;
}
while(a < b*b) {
a = 5*a + c*c;
b = 2*b;
}
}
return 0;
}
twn04.c
This example consists of two nested loops.
The inner loop corresponds to the loop in twn02.c.
The outer loop is evaluated at most c times and resets both variables a and b in every iteration.
int twn04(int a, int b, int c, int d, int e) {
if(d > 0) {
a = d;
b = e;
while(c > 0) {
while(a < b*b && a > 0) {
a = 5*a + c*c;
b = 2*b;
}
a = d;
b = e;
c = c - 1;
}
}
return 0;
}
twn05.c
This benchmark is an advanced version of twn04.c.
While twn04.c contains two loops, this program consists of three loops by adding the loop at Line 6 to Line 9.
This additional loop can be solved by MΦRFs of depth 2 (see Ben-Amram & Genaim here, Table 1 - Loop 20) or our twn-technique.
int twn05(int a, int b, int c, int d, int e, int f) {
if(f > 0) {
a = d;
b = e;
while(f > 0) {
while(c > 0) {
a = a + c;
c = c - 1;
}
while(a < b*b && a > 0) {
a = 5*a + c*c;
b = 2*b;
}
a = d;
b = e;
c = f;
f = f - 1;
}
}
return 0;
}
twn06.c
This benchmark is similar to twn05.c.
However, as the second inner loop, instead of a twn-loop, this example uses a solvable loop (see Xu & Li here, Ex. 3.3 & 3.4).
int twn06(int a, int b, int c, int d, int e, int f) {
if(d > 0) {
a = d;
b = e;
while(c > 0) {
while(c > 0) {
a = a + c;
c = c - 1;
}
c = f;
while(b*b > 1 && a*c + 2*a > 0) {
a = a;
int b1 = b;
int c1 = c;
b = 3*b1 - 4*c1;
c = 4*b1 - 3*c1;
d = 5*d;
e = 5*e - a*a;
}
a = d;
b = e;
f = f - 1;
}
}
return 0;
}
twn07.c
This program consists of two consecutive loops such that one needs to compute size bounds for the first loop with non-linear arithmetic in order to handle the second loop.
int twn07(int a, int b, int c) {
while(a > 0) {
a = a - 1;
b = b + c*c*c;
}
while(b > 0) {
b = b - 1;
}
return 0;
}
twn08.c
This example combines an integer program which needs control-flow refinement (see Giesl et al. here, Fig.7) to be solved and the twn-loop twn02.c.
extern int __VERIFIER_nondet_int(void);
void f(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*b && a > 0) {
a = 5*a + c*c;
b = 2*b;
}
break;
}
}
}
twn09.c
Our approach can not only handle twn-self-loops but simple cycles which correspond to twn-loops.
To this end, we introduce the following benchmark where we update a and c twice in the inner loop.
int twn09(int a, int b, int c) {
if(a > 0) {
while(c > 0) {
a = a + c;
c = c - 1;
}
if(c <= 0) {
while(a < b*b) {
c = -2*b;
a = 5*a;
c = b + c;
a = a + c*c*c*c;
b = 2*b;
c = b + c;
}
}
}
return 0;
}
twn10.c
This program is a twn-loop (see Frohn & Giesl here, Ex. 2).
int twn10(int a, int b, int c, int d) {
while(c + d > 0) {
a = 2;
b = b + 1;
c = -2*c - a;
d = b;
}
return 0;
}
twn11.c
This benchmark corresponds to a loop which can be transformed into a twn-loop by automorphisms (see Frohn et al. here, Ex. 24).
int twn11(int a, int b, int c) {
while(4*b*b + a + b + c > 0) {
a = a + 8*a*b*b + 16*b*b*b + 16*b*b*c;
b = b - a*a - 4*a*b - 4*a*c - 4*b*b - 8*b*c - 4*c*c;
c = c - 4*a*b*b - 8*b*b*b - 8*b*b*c + a*a + 4*a*b + 4*a*c + 4*b*b + 8*b*c + 4*c*c;
}
return 0;
}
twn12.c
This program is a non-terminating twn-loop (see Frohn et al. here, Ex. 24).
int twn12(int a, int b, int c) {
while(a + b*b > 0) {
a = a + b*b*c;
b = b - 2*c*c;
c = c;
}
return 0;
}
twn13.c
This benchmark is a terminating version of twn12.c.
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.
int twn13(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;
}
}
return 0;
}
twn14.c
This program is a simplified implementation of our running example (see Fig. 1).
Here, we only consider the condition d > 0, respectively the path evaluating t1, and not the path evaluating t₃ and t₄.
This example differs from the benchmark twn14.koat.
int twn14(int a, int b, int c, int d, int e) {
while(a > 0) {
b = a;
c = e;
if(d > 0) {
while (b != 0 && b*b + d*d*d*d*d < c) {
b = -2*b;
c = 3*c - d*d*d;
}
}
a = a - 1;
}
return 0;
}
twn15.c
This benchmark is an implementation of our running example (see Fig. 1).
Here, we consider both paths t₂ and t₃ * t₄.
This example differs from the benchmark twn15.koat.
Note that here, we do not consider the non-deterministic choice as in Fig. 1.
Our implementation instead first regards the path t₃ * t₄ and only if this path is not applicable, then the path t₂ is evaluated.
int twn15(int a, int b, int c, int d, int e) {
while(a > 0) {
b = a;
c = e;
if(-5 <= d && d <= 5) {
while (b != 0 && b*b + d*d*d*d*d < c) {
b = -2*b;
c = 3*c - d*d*d;
}
}
else if (d > 0) {
while (b != 0 && b*b + d*d*d*d*d < c) {
b = -2*b;
c = 3*c - d*d*d;
}
}
a = a - 1;
}
return 0;
}
twn16.c
This program has constant runtime and our twn-approach indeed infers a constant runtime bound. In contrast, linear ranking functions only infer a linear bound for this example. Therefore, both configurations KoAT2 + TWN + RF or KoAT2 + TWN + MΦRF5 infer a non-constant linear runtime bound here, since they always search for linear ranking functions first and only if they do not succeed in inferring a finite runtime bound, then these configurations apply our twn-technique.
int twn16(int y) {
while(y <= 42 && y > 0) {
y = 2*y;
}
return 0;
}
twn17.c
This benchmark is an advanced version of twn15.c.
Here, we added a fourth consecutive loop which decreases the value of b by 1 until it is non-positive.
However, as the value of b can have exponential size w.r.t. the initial values (since both inner loops double the absolute value of b iteratively), this benchmark has exponential runtime.
int twn17(int a, int b, int c, int d, int e) {
while(a > 0) {
b = a;
c = e;
if(-5 <= d && d <= 5) {
while (b != 0 && b*b + d*d*d*d*d < c) {
b = -2*b;
c = 3*c - d*d*d;
}
}
else if (d > 0) {
while (b != 0 && b*b + d*d*d*d*d < c) {
b = -2*b;
c = 3*c - d*d*d;
}
}
a = a - 1;
}
while(b > 0) {
b = b - 1;
}
return 0;
}
twn18.c
This program is a solvable loop (see Xu & Li here, Ex. 3.3 & 3.4).
int twn18(int a, int b, int c, int d, int e) {
while(b*b > 1 && a*c + 2*a > 0) {
a = a;
int b1 = b;
int c1 = c;
b = 3*b1 - 4*c1;
c = 4*b1 - 3*c1;
d = 5*d;
e = 5*e - a*a;
}
return 0;
}
twn19.c
This benchmark corresponds to the isolated transition t₅ as in Fig. 1. Note that only our tool with our twn-technique is able to solve this example, i.e., tools based on ranking functions already fail on t₅ alone.
int twn19(int a, int b, int c) {
if(c > 0) {
while(a*a + c*c*c*c*c < b && a != 0) {
a = -2*a;
b = 3*b - 2*c*c*c;
c = c;
}
}
return 0;
}
twn20.c
This program corresponds to the chained version of the isolated transition t₅, i.e., it corresponds to t₅ * t₅, as in Fig. 1. Again, only our tool with our twn-technique is able to solve this example.
int twn20(int a, int b, int c) {
if(c > 0) {
while(a*a + c*c*c*c*c < b && a != 0) {
a = 4*a;
b = 9*b - 8*c*c*c;
c = c;
}
}
return 0;
}