Description
CBMC version: 5.59.0
Operating system: macOS 12.3.1
Exact command line resulting in the issue:
goto-cc main.c
goto-instrument --apply-loop-contracts a.out b.out
goto-instrument --pointer-check b.out c.out
cbmc c.out
I ran the above command lines on the following c program
static void foo() {
unsigned i;
for (i = 0; i < 16; i++)
__CPROVER_loop_invariant(1 == 1) { int v = 1; }
}
static void bar() {
unsigned i;
for (i = 0; i < 16; i++)
__CPROVER_loop_invariant(1 == 1) { int v = 1; }
}
int main() {
bar();
foo();
foo();
}The result shows that, although the function foo and bar are exactly the same, the validity check of v failed in the function foo but not in bar. This is the report
** Results:
assign.c function bar
[bar.1] line 13 Check loop invariant before entry: SUCCESS
[bar.2] line 13 Check that loop invariant is preserved: SUCCESS
[bar.3] line 13 Check that loop instrumentation was not truncated: SUCCESS
[bar.assigns.2] line 13 Check that i is valid: SUCCESS
[bar.assigns.3] line 13 Check that i is assignable: SUCCESS
[bar.assigns.1] line 14 Check that v is valid: SUCCESS
assign.c function foo
[foo.1] line 4 Check loop invariant before entry: SUCCESS
[foo.2] line 4 Check that loop invariant is preserved: SUCCESS
[foo.3] line 4 Check that loop instrumentation was not truncated: SUCCESS
[foo.assigns.2] line 4 Check that i is valid: SUCCESS
[foo.assigns.3] line 4 Check that i is assignable: SUCCESS
[foo.assigns.1] line 5 Check that v is valid: FAILURE
The validity check checks if v is a dead object, i.e.,
!(POINTER_OBJECT(&v) == POINTER_OBJECT(__CPROVER_dead_object))
The check happens before the loop body where v is declared. When the abstracted loop is executed for the first time, v is undeclared and not dead, which is the reason why the check success in bar. At the end of the first abstracted loop, v will be dead and set to be a dead object
// 49 file assign.c line 5 function foo
ASSIGN __CPROVER_dead_object := (side_effect statement="nondet" is_nondet_nullable="1" ? cast(address_of(foo::1::1::1::v), empty*) : __CPROVER_dead_object)
// 50 file assign.c line 5 function foo
DEAD foo::1::1::1::v
Therefore, at the second time we execute the loop, v is not re-declared yet and is dead, that is why the check failed in foo.
A possible fix is not to check validity of local variables at the beginning of loops. @remi-delmas-3000 Do you have any thoughts