Merge pull request #8377 from QinyuanWu/develop

Add documentation to loop contracts, __CPROVER_loop_entry

src/goto-instrument/contracts/doc/user/contracts-assigns.md

@@ -43,6 +43,7 @@ For a loop contract, the condition and target expressions in the assigns clause
 may involve any identifier that is in scope at loop entry
 (parameters of the surrounding function, local variables, global variables,
 type identifiers in `sizeof` or cast expressions, etc.).
+In case of nested loops, the assigns clause of the outer loop should contain all assigns targets of the inner loops.
 The target expression must be free of function calls and side-effects.
 The condition expression may contain calls to side-effect-free functions.
 

src/goto-instrument/contracts/doc/user/contracts-history-variables.md

@@ -42,7 +42,34 @@ __CPROVER_assigns(*out)
 
 ## In Loop Contracts
 
-TODO: Document `__CPROVER_loop_entry` and `__CPROVER_loop_old`.
+### Syntax
+
+```c
+__CPROVER_loop_entry(*identifier*)
+```
+
+### Parameters
+`__CPROVER_loop_entry` takes a variable name that is in scope at the place of the loop contract.
+
+### Semantics
+`__CPROVER_loop_entry` takes a snapshot of the variable value right before the **first iteration** of the loop.
+
+### Example
+In this example the loop invariant asserts that `x <= 200` is upheld before and after every iteration of the `while` loop:
+```c
+void my_function()
+{
+  unsigned x = 200;
+  while( x >= 64 )
+  __CPROVER_loop_invariant(x <= __CPROVER_loop_entry(x)) //equivalent to x <= 200
+  {
+    ...
+    x -= 64;
+  }
+}
+```
+
+
 
 ## Additional Resources
 

src/goto-instrument/contracts/doc/user/contracts-loops.md

@@ -5,16 +5,24 @@ Back to @ref contracts-user
 @tableofcontents
 
 CBMC offers support for loop contracts, which includes four basic clauses:
+- an _assigns_ clause for declaring the memory locations assignable by the loop,
 - an _invariant_ clause for establishing safety properties,
 - a _decreases_ clause for establishing termination,
-- an _assigns_ clause for declaring the memory locations assignable by the loop,
-- a _frees_ clause for declaring the pointers freeable by the loop.
 
-These clauses formally describe an abstraction of a loop for the purpose of a proof.
+**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.
+
+## Examples
 
-## Overview
+### Binary Search Unbounded Proof 
 
 Consider an implementation of the [binary search algorithm] below.
 
@@ -141,6 +149,50 @@ 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.
 
+### Array Wipe Unbounded Proof
+This example uses the __forall__ quantifiers hence requires solving with the  `--smt2` flag.
+```c
+void array_wipe(__CPROVER_size_t len, char * array)
+{  
+  __CPROVER_assume(array != NULL); // pre-condition
+
+  for (__CPROVER_size_t i = 0; i < len; i++)
+  __CPROVER_assigns(i, __CPROVER_object_upto(array, len))
+  __CPROVER_loop_invariant(i >= 0 && i <= len)
+  __CPROVER_loop_invariant(__CPROVER_forall { size_t j; (0 <= j && j < i) ==> array[j] == 0 } )
+  {
+      array[i] = 0; //set all array indices to 0
+  }
+
+  __CPROVER_assert(__CPROVER_forall { size_t j; (0 <= j && j < len) ==> array[j] == 0 }, "array is set to 0"); // post-condition
+}
+```
+
+### Caution With Nested Loop
+Due to the nature of @ref contracts-assigns, we need to be aware of the non-deterministic value of the assigned target.
+In the example below, 
+```c
+const unsigned table[256] = {1, 2, 3, ..., 256};
+
+void nested_loop_example() {
+        unsigned t = 0;
+        for( j=0; j<18; j++ )
+        __CPROVER_assigns(t, j, k) // t and k are also assigns targets of the outer loop as they are assigned in the inner loop
+        __CPROVER_loop_invariant(0 <= j && j <= 18 && t < 256) // without t < 256, the program state for the inductive step allows t to have arbitrary value
+        __CPROVER_decreases(18 - j)
+        {
+            for( k=0; k<48; k++ )
+            __CPROVER_assigns(t, k)
+            __CPROVER_loop_invariant(0 <= k && k <= 48 && t < 256)
+            __CPROVER_decreases(48 - k)
+            {
+                t = table[t];
+            }
+        }
+}
+```
+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.
+
 ## Additional Resources
 
 [binary search algorithm]: https://en.wikipedia.org/wiki/Binary_search_algorithm

src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md

@@ -25,7 +25,7 @@ external environment (in a precondition), or returning it to the calling context
 
 `__CPROVER_is_fresh` takes two arguments: a pointer and an allocation size.
 The first argument is the pointer to be checked for "freshness" (i.e., not previously
-allocated), and the second is the expected size in bytes for the memory
+allocated), and the second is the expected size **in bytes** for the memory
 available at the pointer.
 
 #### Return Value