diff --git a/doc/cprover-manual/contracts-decreases.md b/doc/cprover-manual/contracts-decreases.md index 2fc455d48e1..93d05f164ba 100644 --- a/doc/cprover-manual/contracts-decreases.md +++ b/doc/cprover-manual/contracts-decreases.md @@ -1,3 +1,172 @@ -# Decreases Clause +# Decreases Clauses -TODO: Document `__CPROVER_decreases` +A _decreases_ clause specifies a measure that must strictly decrease at every iteration of a loop. +By demonstrating that the measure + +1. is bounded from below, and +2. strictly decreases at each iteration + +we can prove termination of loops. +This is because the measure must eventually hit the lower bound +at which point the loop must terminate, +since the measure cannot strictly decrease further. +This technique for proving termination was proposed by Robert Floyd, +and interested readers may refer to his seminal paper +"[_Assigning Meaning to Programs_](https://people.eecs.berkeley.edu/~necula/Papers/FloydMeaning.pdf)". + +### Syntax + +A one-dimensional (1D) decreases clause for a loop is an arithmetic expression `e` +over the variables visible at the same scope as the loop, +specified as `__CPROVER_decreases(e)`. + +Like invariant clauses, decreases clauses may be specified just after the loop guard. +An example of a 1D decreases clause is shown below. + +```c +for(int i = 0; i < n; i += 2) +__CPROVER_loop_invariant(0 <= i && i <= n) +__CPROVER_decreases(n - i) +{ ... } +``` + +Please see the [invariant clauses](contracts-invariants.md) page +for more examples on `for` and `do...while` loops. + +To help prove termination of more complex loops, +CBMC also supports multi-dimensional decreases clauses. +A multi-dimensional decreases clause is an [ordered tuple](https://en.wikipedia.org/wiki/Tuple) +of arithmetic expressions, specified as `__CPROVER_decreases(e_1, e_2, ..., e_n)`. +An example of a multi-dimensional decreases clause is given below. + +```c +while(i < n) +__CPROVER_loop_invariant(0 <= i && i <= n) +__CPROVER_loop_invariant(0 <= j && j <= n) +__CPROVER_decreases(n - i, n - j) +{ + if (j < n) + j++; + else + { + i++; + j = 0; + } +} +``` + +We extend the strict arithmetic comparison for 1D decreases clauses +to a strict [lexicographic comparison](https://en.wikipedia.org/wiki/Lexicographic_order) +for multi-dimensional decreases clauses. + +**Important.** +Like invariant clauses, decreases clauses must be free of side effects, +for example, mutation of local or global variables. +Otherwise, CBMC raises an error message during compilation: +``` +Decreases clause is not side-effect free. (at: file main.c line 4 function main) +``` + +### Semantics + +A decreases clause extends the loop abstraction introduced in the [invariants clause](contracts-invariants.md) manual. +In addition to the inductiveness check asserted at the end of a single arbitrary iteration, +CBMC would also assert the strict decrement of the measure specified in the decreases clause. +At a high level, in addition to the assumptions and assertions introduced by the invariant clause, +a decreases clause expands to three key steps: +1. At the beginning of the loop body, record the initial value of the measure specified in the decreases clause. +2. At the end of the loop body, record the final value of the measure specified in the decreases clause. +3. After the loop iteration, assert that the final value is strictly smaller than the initial one. + +For a 1D decreases clause, we use the strict arithmetic comparison (i.e., `<`). +For a multi-dimensional decreases clause, say `(e_1, ..., e_n)`, +we extend the strict arithmetic comparison to a strict lexicographic comparison. + +As an example, consider our binary search implementation again, +this time with a decreases clause annotation to prove its termination: + +```c +int binary_search(int val, int *buf, int size) +{ + if(size <= 0 || buf == NULL) return NOT_FOUND; + + long long lb = 0, ub = size - 1; + long long mid = ((unsigned int)lb + (unsigned int)ub) >> 1; + + while(lb <= ub) + __CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size) + __CPROVER_loop_invariant(mid == ((unsigned int)lb + (unsigned int)ub) >> 1) + __CPROVER_decreases(ub - lb) + { + if(buf[mid] == val) break; + if(buf[mid] < val) + lb = mid + 1; + else + ub = mid - 1; + mid = ((unsigned int)lb + (unsigned int)ub) >> 1; + } + return lb > ub ? NOT_FOUND : mid; +} +``` + +The instrumented GOTO program is conceptually similar to the following high-level C program: + +```c +int binary_search(int val, int *buf, int size) +{ + if(size <= 0 || buf == NULL) return NOT_FOUND; + + long long lb = 0, ub = size - 1; + long long mid = ((unsigned int)lb + (unsigned int)ub) >> 1; + + /* 1. assert invariant at loop entry */ + assert(0L <= lb && lb - 1L <= ub && ub < size); + assert(mid == ((unsigned int)lb + (unsigned int)ub) >> 1); + + /* 2. create a non-deterministic state for modified variables */ + havoc(lb, ub, mid); + + /* 3. establish invariant to model state at an arbitrary iteration */ + __CPROVER_assume(0L <= lb && lb - 1L <= ub && ub < size); + __CPROVER_assume(mid == ((unsigned int)lb + (unsigned int)ub) >> 1); + + /* 4. perform a single arbitrary iteration (or exit the loop) */ + if(lb <= ub) + { + /* 5. declare variables for tracking the loop variant */ + int old_measure, new_measure; + + /* 6. evaluate the variant at the start of the loop body */ + old_measure = ub - lb; + + if(buf[mid] == val) break; + if(buf[mid] < val) + lb = mid + 1; + else + ub = mid - 1; + mid = ((unsigned int)lb + (unsigned int)ub) >> 1; + + /* 7. assert the invariant to establish inductiveness */ + assert(0L <= lb && lb - 1L <= ub && ub < size); + assert(mid == ((unsigned int)lb + (unsigned int)ub) >> 1); + + /* 8. evaluate the variant at the end of the loop body */ + new_measure = ub - lb; + + /* 9. assert the decreases clause */ + assert(new_measure < old_measure); + + /* 10. terminate this symbolic execution path; similar to "exit" */ + __CPROVER_assume(false); + } + return lb > ub ? NOT_FOUND : mid; +} +``` + +The instrumented code points (5), (6), (8), and (9) are specific to the decreases clause. + +**Important.** +Decreases clauses work in conjunction with [loop invariants](contract-invariants.md), +which model an arbitrary loop iteration at which the decreases clause is checked. +If a decreases clause is annotated on a loop without an invariant clause, +then the weakest possible invariant (i.e, `true`) is used to model an arbitrary iteration. diff --git a/doc/cprover-manual/contracts-invariant.md b/doc/cprover-manual/contracts-invariants.md similarity index 83% rename from doc/cprover-manual/contracts-invariant.md rename to doc/cprover-manual/contracts-invariants.md index 8a59b0cd544..0c14a2fe9f6 100644 --- a/doc/cprover-manual/contracts-invariant.md +++ b/doc/cprover-manual/contracts-invariants.md @@ -1,4 +1,4 @@ -# Invariant Clause +# Invariant Clauses An _invariant_ clause specifies a property that must be preserved by every iteration of a loop. @@ -46,11 +46,14 @@ __CPROVER_loop_invariant(i <= n); **Important.** Invariant clauses must be free of _side effects_, for example, mutation of local or global variables. - +Otherwise, CBMC raises an error message during compilation: +``` +Loop invariant is not side-effect free. (at: file main.c line 4 function main) +``` ### Semantics -The loop invariant clause expands to several assumptions and assertions: +A loop invariant clause expands to several assumptions and assertions: 1. The invariant is _asserted_ just before the first iteration. 2. The invariant is _assumed_ on a non-deterministic state to model a non-deterministic iteration. 3. The invariant is finally _asserted_ again to establish its inductiveness. @@ -71,20 +74,19 @@ int binary_search(int val, int *buf, int size) { if(size <= 0 || buf == NULL) return NOT_FOUND; - long lb = 0, ub = size - 1; - long mid = (lb + ub) / 2; + long long lb = 0, ub = size - 1; + long long mid = ((unsigned int)lb + (unsigned int)ub) >> 1; while(lb <= ub) __CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size) - __CPROVER_loop_invariant(mid == (lb + ub) / 2L) - __CPROVER_decreases(ub - lb) + __CPROVER_loop_invariant(mid == ((unsigned int)lb + (unsigned int)ub) >> 1) { if(buf[mid] == val) break; if(buf[mid] < val) lb = mid + 1; else ub = mid - 1; - mid = (lb + ub) / 2; + mid = ((unsigned int)lb + (unsigned int)ub) >> 1; } return lb > ub ? NOT_FOUND : mid; } @@ -97,19 +99,19 @@ int binary_search(int val, int *buf, int size) { if(size <= 0 || buf == NULL) return NOT_FOUND; - long lb = 0, ub = size - 1; - long mid = (lb + ub) / 2; + long long lb = 0, ub = size - 1; + long long mid = ((unsigned int)lb + (unsigned int)ub) >> 1; /* 1. assert invariant at loop entry */ assert(0L <= lb && lb - 1L <= ub && ub < size); - assert(mid == (lb + ub) / 2L); + assert(mid == ((unsigned int)lb + (unsigned int)ub) >> 1); /* 2. create a non-deterministic state for modified variables */ havoc(lb, ub, mid); /* 3. establish invariant to model state at an arbitrary iteration */ - __CPROVER_assume(0L <= lb && lb - 1L <= ub && ub < size) - __CPROVER_assume(mid == (lb + ub) / 2L) + __CPROVER_assume(0L <= lb && lb - 1L <= ub && ub < size); + __CPROVER_assume(mid == ((unsigned int)lb + (unsigned int)ub) >> 1); /* 4. perform a single arbitrary iteration (or exit the loop) */ if(lb <= ub) @@ -119,11 +121,11 @@ int binary_search(int val, int *buf, int size) lb = mid + 1; else ub = mid - 1; - mid = (lb + ub) / 2; + mid = ((unsigned int)lb + (unsigned int)ub) >> 1; /* 5. assert the invariant to establish inductiveness */ assert(0L <= lb && lb - 1L <= ub && ub < size); - assert(mid == (lb + ub) / 2L); + assert(mid == ((unsigned int)lb + (unsigned int)ub) >> 1); /* 6. terminate this symbolic execution path; similar to "exit" */ __CPROVER_assume(false); diff --git a/doc/cprover-manual/contracts-loops.md b/doc/cprover-manual/contracts-loops.md index 4b48d54bbb1..080462bc154 100644 --- a/doc/cprover-manual/contracts-loops.md +++ b/doc/cprover-manual/contracts-loops.md @@ -24,8 +24,8 @@ int binary_search(int val, int *buf, int size) { if(size <= 0 || buf == NULL) return NOT_FOUND; - long lb = 0, ub = size - 1; - long mid = (lb + ub) / 2; + int lb = 0, ub = size - 1; + int mid = ((unsigned int)lb + (unsigned int)ub) >> 1; while(lb <= ub) { @@ -34,7 +34,7 @@ int binary_search(int val, int *buf, int size) lb = mid + 1; else ub = mid - 1; - mid = (lb + ub) / 2; + mid = ((unsigned int)lb + (unsigned int)ub) >> 1; } return lb > ub ? NOT_FOUND : mid; } @@ -96,12 +96,12 @@ int binary_search(int val, int *buf, int size) { if(size <= 0 || buf == NULL) return NOT_FOUND; - long lb = 0, ub = size - 1; - long mid = (lb + ub) / 2; + int lb = 0, ub = size - 1; + int mid = ((unsigned int)lb + (unsigned int)ub) >> 1; while(lb <= ub) __CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size) - __CPROVER_loop_invariant(mid == (lb + ub) / 2L) + __CPROVER_loop_invariant(mid == ((unsigned int)lb + (unsigned int)ub) >> 1) __CPROVER_decreases(ub - lb) { if(buf[mid] == val) break; @@ -109,7 +109,7 @@ int binary_search(int val, int *buf, int size) lb = mid + 1; else ub = mid - 1; - mid = (lb + ub) / 2; + mid = ((unsigned int)lb + (unsigned int)ub) >> 1; } return lb > ub ? NOT_FOUND : mid; } diff --git a/regression/contracts/loop_contracts_binary_search/main.c b/regression/contracts/loop_contracts_binary_search/main.c new file mode 100644 index 00000000000..18a3cd67ff3 --- /dev/null +++ b/regression/contracts/loop_contracts_binary_search/main.c @@ -0,0 +1,41 @@ +#include +#include +#include + +#define NOT_FOUND (-1) + +int binary_search(int val, int *buf, int size) +{ + if(size <= 0 || buf == NULL) + return NOT_FOUND; + + int lb = 0, ub = size - 1; + int mid = ((unsigned int)lb + (unsigned int)ub) >> 1; + + while(lb <= ub) + // clang-format off + __CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size) + __CPROVER_loop_invariant(mid == ((unsigned int)lb + (unsigned int)ub) >> 1) + __CPROVER_decreases(ub - lb) + // clang-format on + { + if(buf[mid] == val) + break; + if(buf[mid] < val) + lb = mid + 1; + else + ub = mid - 1; + mid = ((unsigned int)lb + (unsigned int)ub) >> 1; + } + return lb > ub ? NOT_FOUND : mid; +} + +int main() +{ + int val, size; + int *buf = size >= 0 ? malloc(size * sizeof(int)) : NULL; + + int idx = binary_search(val, buf, size); + if(idx != NOT_FOUND) + assert(buf[idx] == val); +} diff --git a/regression/contracts/loop_contracts_binary_search/test.desc b/regression/contracts/loop_contracts_binary_search/test.desc new file mode 100644 index 00000000000..57b27eb77c5 --- /dev/null +++ b/regression/contracts/loop_contracts_binary_search/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--apply-loop-contracts _ --pointer-check --bounds-check --signed-overflow-check +^EXIT=0$ +^SIGNAL=0$ +^\[binary_search.1\] .* Check loop invariant before entry: SUCCESS$ +^\[binary_search.2\] .* Check that loop invariant is preserved: SUCCESS$ +^\[binary_search.3\] .* Check decreases clause on loop iteration: SUCCESS$ +^\[main.assertion.1\] .* assertion buf\[idx\] == val: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test case verifies memory safety and termination of a binary search implementation.