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;
 }

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -1,11 +1,10 @@
 CORE
 main.c
---enforce-contract assigns_range
-^EXIT=10$
+--enforce-contract uses_assigns
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^\[assigns_ptr\.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether verification fails when an assigns clause of a function
-indicates the pointer might change, but one of its internal function only
-modified its content.
+Checks whether verification succeeds for array elements at a symbolic index. 

regression/contracts/assigns_enforce_detect_local_statics/test.desc

@@ -1,13 +1,12 @@
 CORE
 main.c
 --enforce-contract bar
+^\[foo.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS
+^\[foo.\d+\] line 17 Check that \*y is assignable: SUCCESS
+^\[foo.\d+\] line 20 Check that \*yy is assignable: FAILURE
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that \*yy is assignable: FAILURE$
-^VERIFICATION FAILED$
 --
 --
 Checks whether static local and global variables are correctly tracked

regression/contracts/assigns_enforce_free_dead/test.desc

@@ -7,12 +7,6 @@ main.c
 ^\[foo.\d+\] line \d+ Check that \*q is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*w is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that q is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$
 ^EXIT=10$
 ^SIGNAL=0$
@@ -22,16 +16,7 @@ main.c
 ^\[foo.\d+\] line \d+ Check that \*q is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that \*w is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that \*x is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that q is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that w is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$
-^.*__car_valid.*: FAILURE$
-^.*__car_lb.*: FAILURE$
-^.*__car_ub.*: FAILURE$
 --
 Checks that invalidated CARs are correctly tracked on `free` and `DEAD`.
 
@@ -40,6 +25,3 @@ we rule out all failures using the negative regex matches above.
 
 We also check (using positive regex matches above) that
 `**p` should be assignable in one case and should not be assignable in the other.
-
-Finally, we check that there should be no "internal" assertion failures
-on `__car_valid`, `__car_ub`, `__car_lb` variables used to track CARs.

regression/contracts/assigns_enforce_malloc_01/main.c

@@ -1,16 +1,15 @@
 #include <stdlib.h>
 
-int f1(int *a, int *b) __CPROVER_assigns(*a, b)
+int f(int *a) __CPROVER_assigns()
 {
-  b = (int *)malloc(sizeof(int));
-  *b = 5;
+  a = (int *)malloc(sizeof(int));
+  *a = 5;
 }
 
 int main()
 {
   int m = 4;
-  int n = 3;
-  f1(&m, &n);
+  f(&m);
 
   return 0;
 }

regression/contracts/assigns_enforce_malloc_01/test.desc

@@ -1,9 +1,12 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f
 ^EXIT=0$
 ^SIGNAL=0$
+^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that verification succeeds when a formal parameter pointer outside of the assigns clause is instead pointed as freshly allocated memory before being assigned.
+This test checks that verification succeeds when a formal parameter
+with a pointer type is first updated to point to a locally malloc'd object
+before being assigned to.

regression/contracts/assigns_enforce_malloc_02/test.desc

@@ -1,9 +1,11 @@
 CORE
 main.c
 --enforce-contract f1
-^EXIT=6$
+^Invariant check failed$
+^Condition: is_loop_free
+^Reason: Loops remain in function 'f1', assigns clause checking instrumentation cannot be applied\.
+^EXIT=(127|134)$
 ^SIGNAL=0$
-Unable to complete instrumentation, as this malloc may be in a loop.$
 --
 --
 This test checks that an error is thrown when malloc is called within a loop.

regression/contracts/assigns_enforce_multi_file_02/header.h

@@ -14,7 +14,7 @@ struct pair_of_pairs
 
 int f1(int *a, struct pair *b);
 
-int f1(int *a, struct pair *b) __CPROVER_assigns(*a, b)
+int f1(int *a, struct pair *b) __CPROVER_assigns(*a)
 {
   struct pair_of_pairs *pop =
     (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));

regression/contracts/assigns_enforce_multi_file_02/test.desc

@@ -3,6 +3,7 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
+^\[f1\.\d+\] line \d+ Check that b->y is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/contracts/assigns_enforce_statics/test.desc

@@ -3,7 +3,6 @@ main.c
 --enforce-contract foo _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_structs_01/main.c

@@ -6,18 +6,17 @@ struct pair
   int y;
 };
 
-int f1(int *a, int *b) __CPROVER_assigns(*a, b)
+int f(int *a) __CPROVER_assigns()
 {
   struct pair *p = (struct pair *)malloc(sizeof(struct pair));
-  b = &(p->y);
-  *b = 5;
+  a = &(p->y);
+  *a = 5;
 }
 
 int main()
 {
   int m = 4;
-  int n = 3;
-  f1(&m, &n);
+  f(&m);
 
   return 0;
 }

regression/contracts/assigns_enforce_structs_01/test.desc

@@ -1,11 +1,12 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f
 ^EXIT=0$
 ^SIGNAL=0$
+^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether verification succeeds when a formal parameter pointer outside
-of the assigns clause is instead pointed at the location of a member of a
-freshly allocated struct before being assigned.
+Checks whether verification succeeds when a pointer deref that is not
+specified in the assigns clause is first pointed at a member of a
+locally malloc'd struct before being assigned.

regression/contracts/assigns_enforce_structs_02/main.c

@@ -12,19 +12,18 @@ struct pair_of_pairs
   struct pair p2;
 };
 
-int f1(int *a, int *b) __CPROVER_assigns(*a, b)
+int f(int *a) __CPROVER_assigns()
 {
   struct pair_of_pairs *pop =
     (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));
-  b = &(pop->p2.x);
-  *b = 5;
+  a = &(pop->p2.x);
+  *a = 5;
 }
 
 int main()
 {
   int m = 4;
-  int n = 3;
-  f1(&m, &n);
+  f(&m);
 
   return 0;
 }

regression/contracts/assigns_enforce_structs_02/test.desc

@@ -1,13 +1,12 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f
 ^EXIT=0$
 ^SIGNAL=0$
+^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether verification succeeds when a formal parameter pointer outside
-of the assigns clause is assigned after being pointed at the location of a
-member of a sub-struct of a freshly allocated struct before being assigned.
-This is meant to show that all contained members (and their contained members)
-of assignable structs are valid to assign.
+Checks whether verification succeeds when a pointer deref that is not
+specified in the assigns clause is first pointed at a member of a locally
+malloc'd struct before being assigned (with extra nesting).

regression/contracts/assigns_enforce_structs_03/main.c

@@ -12,19 +12,18 @@ struct pair_of_pairs
   struct pair p2;
 };
 
-int f1(int *a, struct pair *b) __CPROVER_assigns(*a, b)
+int f(struct pair *a) __CPROVER_assigns()
 {
   struct pair_of_pairs *pop =
     (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));
-  b = &(pop->p2);
-  b->y = 5;
+  a = &(pop->p2);
+  a->y = 5;
 }
 
 int main()
 {
-  int m = 4;
-  struct pair n;
-  f1(&m, &n);
+  struct pair m;
+  f(&m);
 
   return 0;
 }

regression/contracts/assigns_enforce_structs_03/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts/assigns_enforce_structs_04/test.desc

@@ -6,7 +6,6 @@ main.c
 ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$
 ^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$
 ^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
-^\[f4.\d+\] line \d+ Check that p is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --