cprover
|
Back to Code Contracts User Documentation
CBMC offers support for loop contracts, which includes four basic clauses:
The three clauses need to be declared in this sequence to avoid errors. Each loop contract should only have one assigns clause that contains all assigned targets. Loop contracts are not used by default. To enable CBMC to check for loop contracts, add the --apply-loop-contract flag at the goto-instrument step.
These clauses formally describe an abstraction of a loop for the purpose of an unbounded proof. CBMC also provides a series of built-in constructs to aid writing loop contracts (e.g., history variables and quantifiers). CBMC will use the abstraction in place of the loop and prove the invariants of the loop only if the loop contracts describes a sound and inductive abstraction of the loop.
Consider an implementation of the binary search algorithm below.
The function stores a lower bound lb and an upper bound ub initialized to the bounds on the buffer buf, i.e., to 0 and size-1 respectively. In each iteration, the midpoint mid is compared against the target value val and in case of a mismatch either the lower half or the upper half of the buffer is searched recursively. A developer might be interested in verifying two high-level properties on the loop on all possible buffers buf and values val:
To prove the first (memory-safety) property, we may declare a loop invariant that must be preserved across all loop iterations. In this case, two invariant clauses would together imply that buf[mid] lookup is always safe. The first invariant clause would establish that the bounds (lb and ub) are always valid:
Note that in the second conjunct, the lb - 1 == ub case is possible when the value val is not found in the buffer buf. The second invariant clause would establish that the midpoint mid is always a valid index. In this particular case we can in fact establish a stronger invariant, that mid is indeed always the midpoint of lb and ub in every iteration:
To prove the second (termination) property, we may declare a decreases clause that indicates a bounded numeric measure which must monotonically decrease with each loop iteration. In this case, it is easy to see that lb and ub are approaching closer together with each iteration, since either lb must increase or ub must decrease in each iteration.
The loop together with all its contracts is shown below.
With CBMC we can now generate an unbounded proof using these contracts:
The first command compiles the program to a GOTO binary, next we instrument the loops using the annotated loop contracts, and finally we verify the instrumented GOTO binary with desired checks.
This example uses the forall quantifiers hence requires solving with the --smt2 flag.
Due to the nature of Assigns Clauses, we need to be aware of the non-deterministic value of the assigned target. In the example below,
If t < 256 is not included in the outer loop invariant, the inner loop invariant t < 256 will immediately fail at loop entry because, in the inductive step of the outer loop, the assigns target t of the outer loop will be a non-deterministic value which can be greater than 256. With the predicate t<256 in the outer loop's invariants will restrict t to be less than 256 in the proof of the inductive step of the outer loop.