Function contracts: performance optimisation for assigns clause checking.

- don't instrument assignments to locals and function parameters,
- don't add function parameters and non-dirty locals to the write set,
- remove from the local write set CARs that are provably not alive,
- remove function parameters and locals from assigns clauses in tests.

Sanity checks:
- change GOTO instruction with false guards into SKIP instructions
  (removes artificial loops),
- check loop-freeness before assigns clause instrumentation
  (required for soundness of assigns clause checking).

The net effect of these changes is a better proof performance because
of a reduction in the number of generated assertions and of their
size, but otherwise the contract checking functionality remains
unchanged.

Rationale:

Assigning to local variables or function parameter is always
legal so we skip instrumenting these assignments. We avoid adding
function parameters and local variables to the local write set, except
when their address is taken at some point in the program and can later
be assigned to indirectly via pointers.

When generating inclusion checks for assignments, we remove from the
local write set targets which are not possibly alive at the ASSIGN
instruction that gets instrumented.

Author: Remi Delmas

regression/contracts/assigns_enforce_04/test.desc

@@ -3,12 +3,6 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that x2 is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that y2 is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that z2 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that x3 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that y3 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that z3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$

regression/contracts/assigns_enforce_05/test.desc

@@ -3,7 +3,6 @@ main.c
 --enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.1\] line \d+ .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/contracts/assigns_enforce_18/test.desc

@@ -7,9 +7,6 @@ main.c
 ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
 ^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$

regression/contracts/assigns_enforce_21/test.desc

@@ -6,9 +6,6 @@ main.c
 main.c function bar
 ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$
-^\[baz.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_enforce_arrays_01/main.c

@@ -1,4 +1,4 @@
-void f1(int a[], int len) __CPROVER_assigns(a)
+void f1(int a[], int len) __CPROVER_assigns()
 {
   int b[10];
   a = b;

regression/contracts/assigns_enforce_arrays_03/main.c

@@ -1,4 +1,4 @@
-void assign_out_under(int a[], int len) __CPROVER_assigns(a)
+void assign_out_under(int a[], int len) __CPROVER_assigns()
 {
   a[1] = 5;
 }

regression/contracts/assigns_enforce_arrays_03/test.desc

@@ -6,5 +6,6 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Checks whether verification fails when an assigns clause contains pointer,
-but function only modifies its content.
+Checks whether verification fails when a function has an array 
+as parameter, an empty assigns clause and attempts to modify the object
+pointed to by the pointer.

regression/contracts/assigns_enforce_arrays_04/main.c

@@ -1,21 +1,20 @@
-void assigns_single(int a[], int len) __CPROVER_assigns(a)
+void assigns_single(int a[], int len)
 {
+  int i;
+  __CPROVER_assume(0 <= i && i < len);
+  a[i] = 0;
 }
 
-void assigns_range(int a[], int len) __CPROVER_assigns(a)
-{
-}
-
-void assigns_big_range(int a[], int len) __CPROVER_assigns(a)
+void uses_assigns(int a[], int len)
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
 {
   assigns_single(a, len);
-  assigns_range(a, len);
 }
 
 int main()
 {
   int arr[10];
-  assigns_big_range(arr, 10);
+  uses_assigns(arr, 10);
 
   return 0;
 }

regression/contracts/assigns_enforce_arrays_04/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract assigns_single --enforce-contract assigns_range --enforce-contract assigns_big_range
+--enforce-contract uses_assigns
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_arrays_05/main.c

@@ -1,18 +1,23 @@
-void assigns_ptr(int *x) __CPROVER_assigns(*x)
+void assigns_ptr(int *x)
 {
   *x = 200;
 }
 
-void assigns_range(int a[], int len) __CPROVER_assigns(a)
+void uses_assigns(int a[], int i, int len)
+  // clang-format off
+ __CPROVER_requires(0 <= i && i < len)
+  __CPROVER_assigns(*(&a[i]))
+// clang-format on
 {
-  int *ptr = &(a[7]);
+  int *ptr = &(a[i]);
   assigns_ptr(ptr);
 }
 
 int main()
 {
   int arr[10];
-  assigns_range(arr, 10);
-
+  int i;
+  __CPROVER_assume(0 <= i && i < 10);
+  uses_assigns(arr, i, 10);
   return 0;
 }