Add scalar assigns clause to code contracts.

Expanding CBMC code contracts to include an
assigns clause for scalar variables and
their pointers.

Author: Christopher Wagner

doc/cprover-manual/assigns-clause.md

@@ -0,0 +1,51 @@
+## CBMC Assigns Clause
+
+### Introduction
+Here is described the syntax and semantics of the "assigns" clause as implemented in CBMC. This construct allows the user to specify a list of memory locations which may be written within a particular scope. While an assigns clause may, in general, be interpreted with either "writes" or "modifies" semantics, this design is based on the former.
+This means that memory not captured by the assigns clause must not be written within the given scope, even if the value(s) therein are not modified.
+
+### Scalar Variables
+The initial iteration of this design focuses on specifying an assigns clause for simple variable types and their pointers. Arrays, structured data, and pointers are left to future contibutions.
+
+
+##### Syntax
+A special construct is introduced to specify assigns clauses. Its syntax is defined as follows.
+
+```
+ <assigns_clause> := __CPROVER_assigns ( <target_list> )
+```
+```
+ <target_list> := <target>
+                | <target> , <target_list>
+```
+```
+ <target> := <identifier>
+           | * <target>
+```
+
+
+The `<assigns_clause>` states that only the memory identified by the dereference expressions and identifiers listed in the contained `<target_list>` may be written within the associated scope, as follows.
+
+##### Semantics
+The semantics of an assigns clause *c* of some function *f* can be understood in two contexts. First, one may consider how the expressions in *c* are treated when a call to *f* is replaced by its contract specification, assuming the contract specification is a sound characterization of the behavior of *f*. Second, one may consider how *c* is applied the function body of *f* in order to determine whether *c* is a sound characterization of the behavior of *f*. We begin by exploring these two perspectives for assigns clauses which contain only scalar expressions.
+
+Let the i<sup>th</sup> expression in some assigns clause *c* be denoted *exprs*<sub>*c*</sub>[i], the j<sup>th</sup> formal parameter of some function *f* be denoted *params*<sub>*f*</sub>[j], and the k<sup>th</sup> argument passed in a call to function *f* be denoted *args*<sub>*f*</sub>[k] (an identifying index may be added to distinguish a *particular* call to *f*, but for simplicity it is omitted here).
+
+###### Replacement
+Assuming an assigns clause *c* is a sound characterization of the behavior of the function *f*, a call  to *f* may be replaced a series of non-deterministic assignments. For each expression *e* &#8712; *exprs*<sub>*c*</sub>, let there be an assignment &#632; := &#8727;, where &#632; is *args*<sub>*f*</sub>[i] if *e* is identical to some *params*<sub>*f*</sub>[i], and *e* otherwise.
+
+###### Enforcement
+In order to determine whether an assigns clause *c* is a sound characterization of the behavior of a function *f*, the body of the function should be instrumented with additional statements as follows.
+
+- For each expression *e* &#8712; *exprs*<sub>*c*</sub>, create a temporary variable *tmp*<sub>*e*</sub> to store \&(*e*), the address of *e*, at the start of *f*.
+- Before each assignment statement, *lhs* := *rhs*, add an assertion (structured as a disjunction)
+
+assert(&#8707; *tmp*<sub>*e*</sub>. __CPROVER_same_object(\&(*lhs*), *tmp*<sub>*e*</sub>)
+- Before each function call with an assigns clause *a*, add an assertion for each *e*<sub>*a*</sub> &#8712; *exprs*<sub>*a*</sub> (also formulated as a disjunction)
+
+assert(&#8707; *tmp*<sub>*e*</sub>. __CPROVER_same_object(\&(*e*<sub>*a*</sub>), *tmp*<sub>*e*</sub>)
+
+Here, __CPROVER_same_object is a predicate indicating that the two pointers reference the same object in the CBMC memory model. Additionally, for each function call without an assigns clause, add an assertion assert(*false*) to ensure that the assigns contract will only hold if all called functions have an assigns clause which is compatible with that of the calling function. 
+
+
+

regression/contracts/assigns_enforce_01/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int z;
+
+int foo(int *x) __CPROVER_assigns(z, *x)
+  __CPROVER_ensures(__CPROVER_return_value == *x + 5)
+{
+  *x = *x + 0;
+  return *x + 5;
+}
+
+int main()
+{
+  int n = 4;
+  n = foo(&n);
+
+  return 0;
+}

regression/contracts/assigns_enforce_01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function.
+
+Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point).
+
+To make such assumptions would cause verification to fail.

regression/contracts/assigns_enforce_02/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+
+int z;
+
+int foo(int *x) __CPROVER_assigns(z)
+  __CPROVER_ensures(__CPROVER_return_value == *x + 5)
+{
+  *x = *x + 0;
+  return *x + 5;
+}
+
+int main()
+{
+  int n = 4;
+  n = foo(&n);
+
+  return 0;
+}

regression/contracts/assigns_enforce_02/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails if an expression outside the assigns clause is assigned within the function.

regression/contracts/assigns_enforce_03/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3)
+{
+  *x3 = *x3 + 1;
+  *y3 = *y3 + 1;
+  *z3 = *z3 + 1;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f1(&p, &q, &r);
+
+  return 0;
+}

regression/contracts/assigns_enforce_03/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds when assigns clauses are respected through multiple function calls.

regression/contracts/assigns_enforce_04/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3)
+{
+  *x3 = *x3 + 1;
+  *y3 = *y3 + 1;
+  *z3 = *z3 + 1;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f1(&p, &q, &r);
+
+  return 0;
+}

regression/contracts/assigns_enforce_04/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when an assigns clause is not respected through multiple function calls.

regression/contracts/assigns_enforce_05/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3)
+{
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f1(&p, &q, &r);
+
+  return 0;
+}

regression/contracts/assigns_enforce_05/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when a function with an assigns clause calls a function without an assigns clause.

regression/contracts/assigns_enforce_06/main.c

@@ -0,0 +1,43 @@
+#include <assert.h>
+
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3)
+{
+  *x3 = *x3 + 1;
+  *y3 = *y3 + 1;
+  *z3 = *z3 + 1;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+
+  for(int i = 0; i < 3; ++i)
+  {
+    if(i == 0)
+    {
+      f1(&p, &q, &r);
+    }
+    if(i == 1)
+    {
+      f2(&p, &q, &r);
+    }
+    if(i == 2)
+    {
+      f3(&p, &q, &r);
+    }
+  }
+
+  return 0;
+}

regression/contracts/assigns_enforce_06/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds when functions with assigns clauses are called from within a loop.

regression/contracts/assigns_enforce_07/main.c

@@ -0,0 +1,43 @@
+#include <assert.h>
+
+void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+{
+  f2(x1, y1, z1);
+}
+
+void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+{
+  f3(x2, y2, z2);
+}
+
+void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3)
+{
+  *x3 = *x3 + 1;
+  *y3 = *y3 + 1;
+  *z3 = *z3 + 1;
+}
+
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+
+  for(int i = 0; i < 3; ++i)
+  {
+    if(i == 0)
+    {
+      f1(&p, &q, &r);
+    }
+    if(i == 1)
+    {
+      f2(&p, &q, &r);
+    }
+    if(i == 2)
+    {
+      f3(&p, &q, &r);
+    }
+  }
+
+  return 0;
+}

regression/contracts/assigns_enforce_07/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification fails when functions with assigns clauses are called within a loop and one of them does not obey its assigns clause.

regression/contracts/assigns_enforce_08/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+void f1(int *x) __CPROVER_assigns(*x)
+{
+  int *a = x;
+  f2(&a);
+}
+void f2(int **y) __CPROVER_assigns(**y)
+{
+  **y = 5;
+}
+
+int main()
+{
+  int n = 3;
+  f1(&n);
+
+  return 0;
+}

regression/contracts/assigns_enforce_08/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds when a function with an assigns clause calls another with an additional level of indirection, and that functions respects the assigns clause of the caller.

regression/contracts/assigns_enforce_09/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+void f1(int **x) __CPROVER_assigns(*x)
+{
+  f2(x);
+}
+void f2(int **y) __CPROVER_assigns(**y)
+{
+  **y = 5;
+}
+
+int main()
+{
+  int p = 3;
+  int *q = &p;
+  f1(&q);
+
+  return 0;
+}

regression/contracts/assigns_enforce_09/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This test checks that verification failes when a function with an assigns clause calls another with an assigns clause that adds one too many dereferences.