Merge pull request #5403 from azcwagner/assigns-clause-scalars

Added scalar assigns clause to code contracts

Author: NlightNFotis

doc/cprover-manual/assigns-clause.md

@@ -0,0 +1,89 @@
+## CBMC Assigns Clause
+
+
+### Introduction
+The _assigns_ clause 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
+primitive types and their pointers. Arrays, structured data, and pointers are
+left to future contributions.
+
+
+##### 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 to 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 returns true if two pointers
+reference the same object in the CBMC memory model. Additionally, for each
+function call without an assigns clause, CBMC adds 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,14 @@
+int foo(int *x) __CPROVER_assigns(*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,16 @@
+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,26 @@
+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,26 @@
+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,23 @@
+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;
+}