Loop unwinding

CBMC is a bounded model checker for C. CBMC works by unwinding the loops in our code (by inlining a finite number of iterations of the loop). CBMC needs to know a bound on the number of times it is expected to unwind any particular loop in our code. In the same way, CBMC needs to know a bound on the number of times to invoke any recursive function in our code.

Sometimes CBMC can figure this out on its own. Consider the program loop1.c

#include<assert.h>

int main() {
  unsigned array[10];

  for (int i = 0; i < 10; i++) {
    array[i] = 0;
  }

  for (int i = 0; i < 10; i++) {
    assert(array[i] == 0);
  }
  return 0;
}

and run CBMC with

cbmc loop1.c

and CBMC will print

[main.assertion.1] line 11 assertion array[i] == 0: SUCCESS
VERIFICATION SUCCESSFUL

Sometimes CBMC needs help. Consider the program loop2.c

#include<assert.h>

int main() {
  unsigned bound;
  unsigned array[bound];

  for (int i = 0; i < bound; i++) {
    array[i] = 0;
  }

  for (int i = 0; i < bound; i++) {
    assert(array[i] == 0);
  }
  return 0;
}

and run CBMC with

cbmc loop2.c

and CBMC will unwind the first loop until it runs out of resources or the loop index wraps around. We need to tell CBMC how many times to unwind the loops in the program. Run CBMC with

cbmc --unwind 11 loop2.c

and CBMC will unwind every loop in the program 10 times (not 11 times!) and print

[main.assertion.1] line 11 assertion array[i] == 0: SUCCESS
VERIFICATION SUCCESSFUL

In summary, we use the flag --unwind to tell CBMC to bound the unwinding of loops in the program. We use --unwind 11 to bound loop unwinding to 11 iterations. We can use the flag --unwindset to give different bounds to different loops. CBMC names the loops in a program with the name of the function containing the loop and the position of the loop within the function. We can ask CBMC to display loop names with the --show-loops flag

cbmc --show-loops loop2.c

and see that the two loops in loop2.c are named main.0 and main.1. We can run CBMC with

cbmc --unwindset main.0:11 --unwindset main.1:11 loop2.c

and get the same successful verification result as with --unwind 11. The flags --unwind and --unwindset can be used together and with different bounds. CBMC will use the --unwind bound by default and use the --unwindset bound for the loop it names.

Loop unwinding assertions

Now, however, we have a problem. CBMC has proved that there is no assertion failure in the program as long as we limit loops to 10 iterations. But how do we know that 10 iterations is enough? What if it is possible for a loop to iterate 11 times, and the error we are looking for occurs on the 11th iteration, and we missed it?

CBMC has a solution for this called loop unwinding assertions. We can ask CBMC to insert loop unwinding assertions with the flag --unwinding-assertions. Now, after CBMC has unrolled a loop, it will insert immediately after the unrolled loop an assertion that the loop termination is true. In other words, CBMC will check that it has completely unrolled the loop. For example, running CBMC on the first program loop1.c with

cbmc --unwind 11 --unwinding-assertions loop1.c

succeeds with

VERIFICATION SUCCESSFUL

but running CBMC on the second program loop2.c with

cbmc --unwind 11 --unwinding-assertions loop2.c

fails with output that includes

[main.unwind.0] line 7 unwinding assertion loop 0: FAILURE
VERIFICATION FAILED