CBMC as unit testing

Think of CBMC as a form of unit testing: If you can write a unit test, then you can write a CBMC proof. One of the things we can do with unit testing is to run a function on a set of inputs, and to compare the result with the expected result. Think of CBMC as a unit tester that runs the function on all possible inputs.

Here is a function quartile from quartile.c that returns the quartile of an integer between 0 and 99.

int quartile(int x) {
  int y;

  if (x < 0 || x > 99) return 0;

  if (x < 50)
    if (x < 25)
      y = 1;
    else
      y = 2;
  else
    if (x < 75)
      y = 3;
    else
      y = 4;

  return y;
}

Here a unit test from unit-test.c that tests quartile using a number from the first quartile.

#include <assert.h>
int quartile(int x);

int main() {
  int x = 1;
  int result = quartile(x);
  assert(result == 1);
}

We can build the unit test with gcc and run it. When we do, the unit test runs successfully, and the assertion does not fail:

gcc quartile.c unit-test.c -o unit-test
./unit-test

We can also build the unit test with goto-cc, which is a drop-in replacement for gcc that comes with CBMC. Now we can use CBMC to run the unit test, and again the assertion does not fail:

goto-cc quartile.c unit-test.c -o unit-test
cbmc ./unit-test

** Results:
unit-test.c function main
[main.assertion.1] line 8 assertion result == 1: SUCCESS

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

For examples as simple as this, we can actually run CBMC directly on the source files (without explicitly invoking goto-cc):

cbmc quartile.c unit-test.c

** Results:
unit-test.c function main
[main.assertion.1] line 8 assertion result == 1: SUCCESS

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

But now we can do something interesting with CBMC. The unit test currently initializes the variable x to 1, and CBMC considers 1 to be the initial value of x. If we remove the initializer, CBMC allows any integer value to be the initial value of x. This is a general rule: If CBMC encounters an uninitialized variable, then CBMC allows any value from the variable's type to be the variable's initial value. We say that CBMC treats uninitialized variables as having unconstrained initial values.

If we rewrite the unit test

#include <assert.h>
int quartile(int x);

int main() {
  int x; // The value of x is now any value of type int
  int result = quartile(x);
  assert(result == 1);
}

and rerun CBMC

cbmc quartile.c unit-test.c

** Results:
unit-test.c function main
[main.assertion.1] line 8 assertion result == 1: FAILURE

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

we can see that the assertion has failed. We can ask CBMC to produce an error trace that demonstrates one way in which the assertion can fail

cbmc quartile.c unit-test.c --trace

** Results:
unit-test.c function main
[main.assertion.1] line 8 assertion result == 1: FAILURE

Trace for main.assertion.1:

State 21 file unit-test.c function main line 6 thread 0
----------------------------------------------------
  x=-2147483547 (10000000 00000000 00000000 01100101)

State 22 file unit-test.c function main line 7 thread 0
----------------------------------------------------
  result=0 (00000000 00000000 00000000 00000000)

State 26 file unit-test.c function main line 7 thread 0
----------------------------------------------------
  x=-2147483547 (10000000 00000000 00000000 01100101)

State 27 file quartile.c function quartile line 2 thread 0
----------------------------------------------------
  y=0 (00000000 00000000 00000000 00000000)

State 33 file unit-test.c function main line 7 thread 0
----------------------------------------------------
  result=0 (00000000 00000000 00000000 00000000)

Violated property:
  file unit-test.c function main line 8 thread 0
  assertion result == 1
  !((signed long int)(signed long int)!(result == 1) != 0l)

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

and we see that in the first step of this error trace the variable x is initialized to the integer value x=-2147483547.

Well, that's not quite what we intended, but we don't expect quartile to return 1 on every integer, just on integers in the first quartile. We can constrain x to be an integer in the first quartile by adding an assumption to the unit test:

#include <assert.h>
int quartile(int x);

int main() {
  int x;
  __CPROVER_assume(0 <= x && x < 25);    // this is a precondition
  int result = quartile(x);
  assert(result == 1);                   // this is a postcondition
}

Rerunning CBMC, we see that the assertion is always true:

cbmc quartile.c unit-test.c

** Results:
unit-test.c function main
[main.assertion.1] line 9 assertion result == 1: SUCCESS

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

Let's pause for a moment to notice that we have already done something interesting. We have proved that the function quartile returns 1 when it is called on any integer in the first quartile. We have partially specified the behavior of the function using a precondition (the assumption that x is in the first quartile) and a postcondition (the assertion that the return value is 1). If the function is called with an input that satisfies the precondition, then the function returns with a value that satisfies the postcondition. Of course, we have only partially specified the behavior of the function. What happens when it is called with an integer in the second quartile? The specification doesn't say. But we have taken the first step toward specification and verification of our function.