Software Verification with PDR: An Implementation of the State of the Art
5
1
extern void __VERIFIER_error() __attribute__
→ ((__noreturn__));
2
extern unsigned int __VERIFIER_nondet_uint(void);
3
void __VERIFIER_assert(int cond) {
4
if (!(cond)) {
5
ERROR: __VERIFIER_error();
6
}
7
return;
8
}
9
int main(void) {
10
unsigned int w = __VERIFIER_nondet_uint();
11
unsigned int x = w;
12
unsigned int y = w + 1;
13
unsigned int z = x + 1;
14
while (__VERIFIER_nondet_uint()) {
15
y++;
16
z++;
17
}
18
__VERIFIER_assert(y == z);
19
return 0;
20
}
Fig. 1: Example C program eq2.c
that at this point, w and x are equal to each other, and y and z are also equal to
each other. Then, from line 14 to line 17, a loop with a nondeterministic exit
condition (and therefore an unknown number of iterations) increments in each
iteration both variables y and z. Lastly, line 18 asserts that after the loop, y and z
are (still) equal to each other. Since y and z are equal before the loop, and are
always incremented together within the loop, the invariant y = z is inductive.
However, since there is no direct connection between y and z but only an indirect
one via their shared dependency on w, naïve data-flow-based techniques may fail
to find this invariant. In fact, we tried several configurations of the verification
framework CPAchecker, and found that many of them fail to prove this program:
• Plain k -induction without auxiliary-invariant generation fails, because it
never checks if y = z is a loop invariant and instead only checks the reachability of the assertion failure (located after loop). The reachability of the
assertion failure, in turn, depends on the nondeterministic loop-exit condition.
Therefore we cannot conclude from “the assertion failure was not reached in
k previous iterations” that “the assertion failure cannot be reached in the
next iteration”: In the absence of auxiliary invariants, a valid counterexample
to this induction hypothesis would always be that in the previous iterations
the assertion condition was in fact violated and an assertion failure was not
reached only because the loop was not exited.
• A data-flow analysis based on the abstract domain of Boxes [21] fails, because
it is not able to track variable equalities.
• A data-flow analysis based on a template Eq for tracking the equality of pairs
of variables fails, because while it detects the invariant w = x, it is unable to
5
1
extern void __VERIFIER_error() __attribute__
→ ((__noreturn__));
2
extern unsigned int __VERIFIER_nondet_uint(void);
3
void __VERIFIER_assert(int cond) {
4
if (!(cond)) {
5
ERROR: __VERIFIER_error();
6
}
7
return;
8
}
9
int main(void) {
10
unsigned int w = __VERIFIER_nondet_uint();
11
unsigned int x = w;
12
unsigned int y = w + 1;
13
unsigned int z = x + 1;
14
while (__VERIFIER_nondet_uint()) {
15
y++;
16
z++;
17
}
18
__VERIFIER_assert(y == z);
19
return 0;
20
}
Fig. 1: Example C program eq2.c
that at this point, w and x are equal to each other, and y and z are also equal to
each other. Then, from line 14 to line 17, a loop with a nondeterministic exit
condition (and therefore an unknown number of iterations) increments in each
iteration both variables y and z. Lastly, line 18 asserts that after the loop, y and z
are (still) equal to each other. Since y and z are equal before the loop, and are
always incremented together within the loop, the invariant y = z is inductive.
However, since there is no direct connection between y and z but only an indirect
one via their shared dependency on w, naïve data-flow-based techniques may fail
to find this invariant. In fact, we tried several configurations of the verification
framework CPAchecker, and found that many of them fail to prove this program:
• Plain k -induction without auxiliary-invariant generation fails, because it
never checks if y = z is a loop invariant and instead only checks the reachability of the assertion failure (located after loop). The reachability of the
assertion failure, in turn, depends on the nondeterministic loop-exit condition.
Therefore we cannot conclude from “the assertion failure was not reached in
k previous iterations” that “the assertion failure cannot be reached in the
next iteration”: In the absence of auxiliary invariants, a valid counterexample
to this induction hypothesis would always be that in the previous iterations
the assertion condition was in fact violated and an assertion failure was not
reached only because the loop was not exited.
• A data-flow analysis based on the abstract domain of Boxes [21] fails, because
it is not able to track variable equalities.
• A data-flow analysis based on a template Eq for tracking the equality of pairs
of variables fails, because while it detects the invariant w = x, it is unable to