Function contracts

A function contract is a function specification. It consists of

• a precondition that must be true when the function is called,
• a postcondition that will be true when the function returns, and
• a write set giving the set of all memory locations that may be changed by the funciton (nothing outside the write set will be changed).

We check that a function contract satisfies its specification by proving that for all memory states and for all function arguments, if then memory and function arguments satisfy the precondition when we invoke the function, then only memory locations in the write set will change and the memory and return arguments will satisfy the postcondition.

We can use a function specification in place of a function invocation by checking that the memory and function arguments satisfy the precondition, and then replacing the values of memory locations in the write set with arbitrary values satisfying the postcondition.

The value of function contracts is proof abstraction:

• API specifications: If we can write function contracts for every function in an interface, then we can validate any code using the interface without reasoning about the details of the interface implementation at the same time. The proof becomes valid for any implementation of the API, and what might otherwise be a large and complicated problem for CBMC to solve may become much smaller and more tractible.
• Proof scaling: Applying CBMC directly to a code base quickly becomes intractible. A function with a complicated call graph may simply not fit within the capacity of CBMC on any computer of reasonable size. But suppose we think of the function call graph as a computation tree, and suppose we can find a small set of functions such that we get a collection of subtrees of reasonable size if we prune the computation tree at the invocations of these functions. If we can write function contracts for these functions, and if we can prove that these functions satisfy their contracts, then we can use these function contracts in the proofs of other function contracts for other functions that depend on them. In this way, we can use function contracts to scale CBMC proof to code bases larger than CBMC can validate directly.

Writing function contracts

We write a function contract by annotating the function definition with

• requires clauses that describe the precondition,
• ensures clauses that describe the postcondition, and
• assigns clauses that describe the write set.

Recall our string buffer example

typedef struct { size_t length; char* buffer; } strbuf;

char cache;
void cache_fifth_char(strbuf* str) { cache = str->buffer[4]; }

and our final proof harness for this function

main() {
  size_t len;
  strbuf* str = strbuf_allocate(len);

  __CPROVER_assume(strbuf_is_valid(str));
  __CPROVER_assume(str->length > 4);

  cache_fifth_char(str);

  __CPROVER_assert(strbuf_is_valid(str), "String buffer remains valid");
  __CPROVER_assert(str->length > 4, "String buffer remains length >4");
}

This proof harness is --- as explicitly as possible --- describing the preconditions and postconditions for the function. Let's simplify this proof harness by writing a function contract for the function.

Checking function contracts

Using function contracts

Warning: Check before use!