Proof harnesses

This section gives simple examples of writing a proof harness for CBMC. The purpose of a proof harness is to build a model of the environment of the function under test.

• Modeling input
• Modeling global state
• Modeling interfaces

Modeling input

For simple functions, the model of the environment is just the input to the function.

Suppose we have a library library1.c

    #include <assert.h>

    int alpha1(int a) {
      return a+1;
    }

    int beta1(int b) {
      int bb = alpha1(b);
      assert(bb == b);
    }

and we want to test function beta1. The input to function beta1 is an integer b. We write a proof harness harness1.c

    int beta1(int b);

    main() {
      int x;
      beta1(x);
    }

that allocates an unconstrained integer named x and invokes beta1 on x.

We run CBMC on the result with

    goto-cc -o library1.goto library1.c
    goto-cc -o harness1.goto harness1.c
    goto-cc -o proof1.goto library1.goto harness1.goto
    cbmc proof1.goto

and we see a violation of the assertion bb == b. Correcting this assertion to bb == b + 1 fixes the problem.

Modeling global state

Sometimes a function depends on gobal state. A common example is low-level system code that depends on a system table, and we want to know the code works no matter what has been stored in the system table.

Suppose we have a library library2.c

    #include <assert.h>

    int counter = 0;

    int alpha2(int a) {
      counter = counter + 1;
      return a+counter;
    }

    int beta2(int b) {
      int bb = alpha2(b);
      assert(bb == b + 1);
    }

and we want to test function beta2. This time the function beta2 depends on its input b, but it also depends on a global variable counter that is initialized to 0 but is changed with each invocation of beta2. We want to know that beta2 always works, no matter how many times beta2 has been invoked in the past.

We do this by writing a proof harness that choses an unconstrained value for both the function input b and the global variable counter. We write a proof harness harness2.c

    extern int counter;
    int beta2(int b);

    main() {
      int cnt;
      counter = cnt;

      int x;
      beta2(x);
    }

We run CBMC on the result with

    goto-cc -o library2.goto library2.c
    goto-cc -o harness2.goto harness2.c
    goto-cc -o proof2.goto library2.goto harness2.goto
    cbmc proof2.goto

and see a violation of the assertion bb == b + 1. We correct this to bb >= b + 1 and we are done.

Modeling interfaces

Sometimes a function depends on an implementation of an interface that we don't care to test. A common example is a function the depends on a network communication protocol like HTTP with send and receive methods. We want our code to work independent of the protocol implementation, so we replace the implementations of the functions in the protocol interface with stubs that over-approximate the behaviors of the implementations.

Suppose we have a library library3.c

    #include <assert.h>

    void send(int msg);
    int receive();

    int alpha(int x) {
      int y = receive();
      assert(y > 0);
      return y+1;
    }

that depends on send and receive methods from a network interface. We stub out the network interface with network3.c

    int receive() {
      // model receiving an unconstrained integer value from the network
      int msg;
      return msg;
    }

    void send(int msg) {
      // model sending an integer over the network (nothing to do)
      return;
    }

We write the proof harness harness3.c

    int alpha(int x);

    main() {
      int x;
      alpha(x);
    }

We run CBMC with

    goto-cc -o network3.goto network3.c
    goto-cc -o library3.goto library3.c
    goto-cc -o harness3.goto harness3.c
    goto-cc -o proof3.goto network3.goto library3.goto harness3.goto
    cbmc proof3.goto

and we get a failure of the assertion y > 0.

Suppose the mistake is in our model of the network. Suppose our network only transmits positive integers. Then we can fix our stub of the receive method to return not an unconstrained integer but an unconstrained positive integer. We change our stubs for the network to network3a.c

    int receive() {
      // model receiving an unconstrained POSTIVE integer value from the network
      int msg;
      __CPROVER_assume(msg > 0);
      return msg;
    }

    void send(int msg) {
      // model sending an integer over the network (nothing to do)
      return;
    }

We run CBMC with

    goto-cc -o network3a.goto network3a.c
    goto-cc -o library3.goto library3.c
    goto-cc -o harness3.goto harness3.c
    goto-cc -o proof3.goto network3a.goto library3.goto harness3.goto
    cbmc proof3.goto

and declare victory at the successful verification.