Behavior of infinite loops with goto-instrument --unwind N --unwinding-assertions differs from cbmc --unwind N --unwinding-assertions

[gsingh93]

CBMC version: 5.42.0 (cbmc-5.42.0-2-g038a53b50)
Operating system: Debian
Exact command line resulting in the issue: goto-instrument --unwind 3 --unwinding-assertions test.gb test-unwinding.gb && cbmc test-unwinding.gb --function foo
What behaviour did you expect: No assertion failures
What happened instead: Two assertion failure

I have the following code in test.c:

int foo() {
  while (1) {
  }
  __CPROVER_assert(0, "reachable");
}

When I run cbmc --unwind 3 --unwinding-assertions test.c --function foo, I don't see any assertion failures:

[foo.assertion.1] line 4 reachable: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

Now I try to do the same thing with goto-instrument:

goto-cc test.c -o test.gb
goto-instrument --unwind 3 --unwinding-assertions test.gb test-unwinding.gb
cbmc test-unwinding.gb --function foo

And I see two failures:

[foo.1] line 2 assertion: FAILURE
[foo.assertion.1] line 4 reachable: FAILURE

** 2 of 2 failed (2 iterations)
VERIFICATION FAILED

The behavior I want is actually what cbmc does, which is to essentially treat the loop as assume(false). Why does goto-instrument behave differently, and is it intended to behave differently?

[jimgrundy]

CBMC has a special case for "while (1) {}" to convert to "assume(false);". There is a flag to disable this. This was added for code in SVCOMP. But, maybe the default should have been the other way around, or maybe we should be giving you a warning when this special case is invoked.

[martin-cs]

@jimgrundy is correct, while(1) {} is recognised by CBMC and treated as assume(false); ( It is not entirely clear to me how this interacts with --unwinding-assertion). So the reachable assertion should be safe, or, possibly not even considered because it is clearly unreachable.

As I described in #6432 (comment) the goto-instrument unwinder is a different piece of code. It will duplicate the body. This might break the heuristic that CBMC uses to recognise while(1) {}. It will also insert the unwinding assertion which will then fail. This is reasonably expected behaviour.

The "reachable" failing after seems weird and might well be a bug.

[tautschnig]

There seem to be at least three, perhaps even more issues hidden in here:

• The primary concern raised by @gsingh93 should be addressed by goto-symex: print status note and conditional warning for self-loops #6624.
• The supposedly unreachable failing assertion as noticed by @martin-cs requires adding unwinding assumptions in goto-instrument's unwinder. PR to follow.
• The unwinding assertion inserted by goto-instrument's unwinder should also be labelled as such. The state around these labels appears messy. PR to follow.

A possible further issue is that --partial-loops is considered conflicting with --unwinding-assertions for no good reason. PR to follow.