Documentation for decreases clauses

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.

doc/cprover-manual/contracts-invariant.md → 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);

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,20 +96,20 @@ 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;
      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;
 }

regression/contracts/loop_contracts_binary_search/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+#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);
+}

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.