Merge pull request #6533 from remi-delmas-3000/function-contracts-prune-write-set

Function contracts: check loop freeness before instrumentation, skip assignments to locals and prune write set using CFG info.

Author: remi-delmas-3000

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$
 --
 --