Difference in behavior of `cbmc --unwind N` and `goto-instrument --unwind N`

[gsingh93]

CBMC version: 5.42.0 (cbmc-5.42.0-2-g038a53b50)
Operating system: Debian
Exact command line resulting in the issue: cbmc --unwind 8 --unwinding-assertions test.c --function foo
What behaviour did you expect: No assertions should fail
What happened instead: Assertions fail, unless I use --unwind 9 instead of --unwind 8

I have the following code in test.c:

int foo(void) {
  int sum = 0;
  for (int i = 0; i < 8; i++) {
    sum += i;
  }
  return sum;
}

The loop should iterate 8 times. If I perform the unwinding with goto-instrument, everything works as expected:

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

In the output I have no verification errors and I see [foo.1] line 3 assertion: SUCCESS. If I use --unwind 7 instead it fails as expected.

But when I use CBMC directly, this fails:

cbmc --unwind 8 --unwinding-assertions test.c --function foo

I see [foo.unwind.0] line 3 unwinding assertion loop 0: FAILURE. However, using --unwind 9 works.

Is there an off-by-one issue here, or am I misunderstanding something?

[gsingh93]

I'm actually not sure if --unwind 9 is working, this doesn't seem right (there are no VCCs):

Runtime Symex: 0.0015976s
size of program expression: 78 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 2.2844e-05s
VERIFICATION SUCCESSFUL

[martin-cs]

The CBMC unwinder and the goto-instrument unwinder are actually different bits of code that work differently. The CBMC unwinder is done as part of symbolic execution and counts the number of back-edges taken. The goto-instrument unwinder works by manipulating the goto-program by copying the loop body.

The CBMC symex does constant folding which is why you are seeing no VCCs with --unwind 9, if you allow the back edge to be taken 9 times, on the 9th one i = 8 so the branch condition fails and so the unwinding assertion is not generated as it can never be reached.

This is, sort of, an off-by-one error but it is more that the numbers are measuring different things. This is, from a user point of view, not really ideal.