CONTACTS: update regression test suite for DFCC

Remi Delmas · Remi Delmas · commit 24ba3bdd69ae · 2022-09-22T11:39:55.000-04:00
Updated tests
- update assigns-enforce-malloc-zero
- update assigns-local-composite
- update assigns-replace-ignored-return-value
- update assigns-replace-malloc-zero
- update assigns-slice-targets
- update assigns-slice-targets
- update assigns_enforce_01
- update assigns_enforce_02
- update assigns_enforce_03
- update assigns_enforce_04
- update assigns_enforce_05
- update assigns_enforce_06
- update assigns_enforce_07
diff --git a/regression/contracts/assigns-enforce-malloc-zero/main.c b/regression/contracts/assigns-enforce-malloc-zero/main.c
@@ -6,7 +6,7 @@ int foo(char *a, int size)
   // clang-format off
   __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
   __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size))
-  __CPROVER_assigns(a: __CPROVER_POINTER_OBJECT(a))
+  __CPROVER_assigns(a: __CPROVER_whole_object(a))
   __CPROVER_ensures(
     a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
 // clang-format on
diff --git a/regression/contracts/assigns-enforce-malloc-zero/test.desc b/regression/contracts/assigns-enforce-malloc-zero/test.desc
@@ -1,7 +1,6 @@
 CORE
 main.c
---enforce-contract foo _ --malloc-may-fail --malloc-fail-null
-^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$
+--dfcc main --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
 ^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns-local-composite/test.desc b/regression/contracts/assigns-local-composite/test.desc
@@ -1,12 +1,12 @@
 CORE
 main.c
---enforce-contract foo
+--dfcc main --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Checks that assigns clause checking explicitly checks assignments to locally 
+Checks that assigns clause checking explicitly checks assignments to locally
 declared symbols with composite types, when they are dirty.
-Out of bounds accesses to locally declared arrays, structs, etc. 
+Out of bounds accesses to locally declared arrays, structs, etc.
 will be detected by assigns clause checking.
diff --git a/regression/contracts/assigns-replace-ignored-return-value/test.desc b/regression/contracts/assigns-replace-ignored-return-value/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
+--dfcc main --replace-call-with-contract bar --replace-call-with-contract baz --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/assigns-replace-malloc-zero/main.c b/regression/contracts/assigns-replace-malloc-zero/main.c
@@ -6,7 +6,7 @@ int foo(char *a, int size)
   // clang-format off
 __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
 __CPROVER_requires(a == NULL || __CPROVER_rw_ok(a, size))
-__CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
+__CPROVER_assigns(__CPROVER_whole_object(a))
 __CPROVER_ensures(
     a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
 // clang-format on
diff --git a/regression/contracts/assigns-replace-malloc-zero/test.desc b/regression/contracts/assigns-replace-malloc-zero/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
+--dfcc main --replace-call-with-contract foo _ --malloc-may-fail --malloc-fail-null
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$
diff --git a/regression/contracts/assigns-slice-targets/test-enforce.desc b/regression/contracts/assigns-slice-targets/test-enforce.desc
@@ -1,6 +1,6 @@
 CORE
 main-enforce.c
---enforce-contract foo
+--dfcc main --enforce-contract foo
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
diff --git a/regression/contracts/assigns-slice-targets/test-replace.desc b/regression/contracts/assigns-slice-targets/test-replace.desc
@@ -1,6 +1,6 @@
 CORE
 main-replace.c
---replace-call-with-contract foo
+--dfcc main --replace-call-with-contract foo
 ^\[main.assertion.\d+\].*assertion s.a == 0: SUCCESS$
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)0\] == 0: FAILURE$
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)1\] == 0: FAILURE$
diff --git a/regression/contracts/assigns_enforce_01/test.desc b/regression/contracts/assigns_enforce_01/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract foo
+--dfcc main --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/assigns_enforce_02/test.desc b/regression/contracts/assigns_enforce_02/test.desc
@@ -1,7 +1,6 @@
 CORE
 main.c
---enforce-contract foo
-^\[foo.assigns.\d+\] line 3 Check that z is valid: SUCCESS$
+--dfcc main --enforce-contract foo
 ^\[foo.assigns.\d+\] line 6 Check that \*x is assignable: FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/contracts/assigns_enforce_03/test.desc b/regression/contracts/assigns_enforce_03/test.desc
@@ -1,15 +1,6 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2 --enforce-contract f3
-^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$
-^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$
-^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$
-^\[f2.assigns.\d+\] line 6 Check that \*x2 is valid: SUCCESS$
-^\[f2.assigns.\d+\] line 6 Check that \*y2 is valid: SUCCESS$
-^\[f2.assigns.\d+\] line 6 Check that \*z2 is valid: SUCCESS$
-^\[f3.assigns.\d+\] line 11 Check that \*x3 is valid: SUCCESS$
-^\[f3.assigns.\d+\] line 11 Check that \*y3 is valid: SUCCESS$
-^\[f3.assigns.\d+\] line 12 Check that \*z3 is valid: SUCCESS$
+--dfcc main --enforce-contract f1
 ^\[f3.assigns.\d+\] line 14 Check that \*x3 is assignable: SUCCESS$
 ^\[f3.assigns.\d+\] line 15 Check that \*y3 is assignable: SUCCESS$
 ^\[f3.assigns.\d+\] line 16 Check that \*z3 is assignable: SUCCESS$
@@ -18,4 +9,5 @@ main.c
 ^SIGNAL=0$
 --
 --
-This test checks that verification succeeds when assigns clauses are respected through multiple function calls.
+This test checks that verification succeeds when assigns clauses are respected
+through multiple function calls.
diff --git a/regression/contracts/assigns_enforce_04/test.desc b/regression/contracts/assigns_enforce_04/test.desc
@@ -1,9 +1,6 @@
 CORE
 main.c
---enforce-contract f1
-^\[f1.assigns.\d+\] line 1 Check that \*x1 is valid: SUCCESS$
-^\[f1.assigns.\d+\] line 1 Check that \*y1 is valid: SUCCESS$
-^\[f1.assigns.\d+\] line 1 Check that \*z1 is valid: SUCCESS$
+--dfcc main --enforce-contract f1
 ^\[f3.assigns.\d+\] line 13 Check that \*x3 is assignable: SUCCESS$
 ^\[f3.assigns.\d+\] line 14 Check that \*y3 is assignable: SUCCESS$
 ^\[f3.assigns.\d+\] line 15 Check that \*z3 is assignable: SUCCESS$
diff --git a/regression/contracts/assigns_enforce_05/test.desc b/regression/contracts/assigns_enforce_05/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2 --enforce-contract f3
+--dfcc main --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/assigns_enforce_06/main.c b/regression/contracts/assigns_enforce_06/main.c
@@ -1,41 +1,44 @@
-void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+void f1(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z)
 {
-  f2(x1, y1, z1);
+  f2(x, y, z);
 }
 
-void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+void f2(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z)
 {
-  f3(x2, y2, z2);
+  f3(x, y, z);
 }
 
-void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*x3, *y3, *z3)
+void f3(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z)
 {
-  *x3 = *x3 + 1;
-  *y3 = *y3 + 1;
-  *z3 = *z3 + 1;
+  *x = *x + 1;
+  *y = *y + 1;
+  *z = *z + 1;
 }
 
-int main()
+void f(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z)
 {
-  int p = 1;
-  int q = 2;
-  int r = 3;
-
   for(int i = 0; i < 3; ++i)
   {
     if(i == 0)
     {
-      f1(&p, &q, &r);
+      f1(x, y, z);
     }
     if(i == 1)
     {
-      f2(&p, &q, &r);
+      f2(x, y, z);
     }
     if(i == 2)
     {
-      f3(&p, &q, &r);
+      f3(x, y, z);
     }
   }
+}
 
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f(&p, &q, &r);
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_06/test.desc b/regression/contracts/assigns_enforce_06/test.desc
@@ -1,9 +1,10 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2 --enforce-contract f3
+--dfcc main --enforce-contract f
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that verification succeeds when functions with assigns clauses are called from within a loop.
+This test checks that verification succeeds when functions
+are called from within a loop.
diff --git a/regression/contracts/assigns_enforce_07/main.c b/regression/contracts/assigns_enforce_07/main.c
@@ -1,41 +1,46 @@
-void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1)
+void f1(int *x, int *y, int *z) __CPROVER_assigns(*x, *y)
 {
-  f2(x1, y1, z1);
+  *x = *x + 1;
+  *y = *y + 1;
 }
 
-void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2)
+void f2(int *x, int *y, int *z) __CPROVER_assigns(*x, *y)
 {
-  f3(x2, y2, z2);
+  *x = *x + 1;
+  *y = *y + 1;
 }
 
-void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3)
+void f3(int *x, int *y, int *z) __CPROVER_assigns(*x, *y, *z)
 {
-  *x3 = *x3 + 1;
-  *y3 = *y3 + 1;
-  *z3 = *z3 + 1;
+  *x = *x + 1;
+  *y = *y + 1;
+  *z = *z + 1;
 }
 
-int main()
+void f(int *x, int *y, int *z) __CPROVER_assigns(*x, *y)
 {
-  int p = 1;
-  int q = 2;
-  int r = 3;
-
   for(int i = 0; i < 3; ++i)
   {
     if(i == 0)
     {
-      f1(&p, &q, &r);
+      f1(x, y, z);
     }
     if(i == 1)
     {
-      f2(&p, &q, &r);
+      f2(x, y, z);
     }
     if(i == 2)
     {
-      f3(&p, &q, &r);
+      f3(x, y, z);
     }
   }
+}
 
+int main()
+{
+  int p = 1;
+  int q = 2;
+  int r = 3;
+  f(&p, &q, &r);
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_07/test.desc b/regression/contracts/assigns_enforce_07/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract f2 --enforce-contract f3
+--dfcc main --enforce-contract f
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/contracts/frees-clause-and-predicates/main.c b/regression/contracts/frees-clause-and-predicates/main.c
@@ -1,43 +1,75 @@
+#include <stdbool.h>
 #include <stdlib.h>
 
-// A function defining a conditionally freeable target
-__CPROVER_freeable_t
-foo_frees(char *arr, const size_t size, const size_t new_size)
+// A function defining an assignable target
+__CPROVER_assignable_t foo_assigns(char *arr, const size_t size)
+{
+  __CPROVER_object_upto(arr, size);
+}
+
+// A function defining an freeable target
+__CPROVER_freeable_t foo_frees(char *arr, const size_t size)
 {
   __CPROVER_freeable(arr);
 }
 
-char *foo(char *arr, const size_t size, const size_t new_size)
+bool is_freeable(void *ptr)
+{
+  bool is_dynamic_object = (ptr == 0) | __CPROVER_DYNAMIC_OBJECT(ptr);
+  bool has_offset_zero = (ptr == 0) | (__CPROVER_POINTER_OFFSET(ptr) == 0);
+  return is_dynamic_object & has_offset_zero;
+}
+
+char *foo(char *ptr, const size_t size, const size_t new_size)
   // clang-format off
-__CPROVER_requires(__CPROVER_is_freeable(arr))
-__CPROVER_assigns(__CPROVER_whole_object(arr))
-__CPROVER_frees(foo_frees(arr, size, new_size))
+__CPROVER_requires(__CPROVER_is_freeable(ptr))
+__CPROVER_assigns(foo_assigns(ptr, size))
+__CPROVER_frees(foo_frees(ptr, size))
 __CPROVER_ensures(
-  (arr && new_size > size) ==>
+  (ptr && new_size > size) ==>
     __CPROVER_is_fresh(__CPROVER_return_value, new_size))
 __CPROVER_ensures(
-  (arr && new_size > size) ==>
-    __CPROVER_is_freed(__CPROVER_old(arr)))
+  (ptr && new_size > size) ==>
+    __CPROVER_is_freed(ptr))
 __CPROVER_ensures(
-    !(arr && new_size > size) ==>
-      __CPROVER_return_value == __CPROVER_old(arr))
+    !(ptr && new_size > size) ==>
+      __CPROVER_return_value == __CPROVER_old(ptr))
 // clang-format on
 {
-  if(arr && new_size > size)
+  // The harness  allows to add a nondet offset to the pointer passed to foo.
+  // Proving this assertion shows that the __CPROVER_is_freeable(ptr) assumption
+  // is in effect as expected for the verification
+  __CPROVER_assert(is_freeable(ptr), "ptr is freeable");
+
+  if(ptr && new_size > size)
   {
-    free(arr);
-    return malloc(new_size);
+    free(ptr);
+    ptr = malloc(new_size);
+
+    // write at some nondet i (should be always allowed since ptr is fresh)
+    size_t i;
+    if(i < new_size)
+      ptr[i] = 0;
+
+    return ptr;
   }
   else
   {
-    return arr;
+    // write at some nondet i
+    size_t i;
+    if(i < size)
+      ptr[i] = 0;
+
+    return ptr;
   }
 }
 
 int main()
 {
   size_t size;
   size_t new_size;
+  __CPROVER_assume(size < __CPROVER_max_malloc_size);
+  __CPROVER_assume(new_size < __CPROVER_max_malloc_size);
   char *arr = malloc(size);
   arr = foo(arr, size, new_size);
   return 0;
diff --git a/regression/contracts/frees-clause-and-predicates/test.desc b/regression/contracts/frees-clause-and-predicates/test.desc
@@ -1,17 +1,13 @@
 CORE
 main.c
---enforce-contract foo
-^\[foo.postcondition.\d+\] line \d+ Check ensures clause: FAILURE$
-^VERIFICATION FAILED$
-^EXIT=10$
+-dfcc main --enforce-contract foo
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
 ^SIGNAL=0$
 --
 --
-This test checks that the front end parses and typchecks correct uses of:
+This test checks that using the -dffdfcc flag we can check contracts that use:
 - __CPROVER_freeable_t function calls as frees clause targets
-- the predicate __CPROVER_freeable
-- the predicate __CPROVER_is_freeable
-- the predicate __CPROVER_is_freed
-
-The post condition of the contract is expected to fail because the predicates
-have no interpretation in the back-end yet.
+- the __CPROVER_freeable built-in
+- the __CPROVER_is_freeable built-in predicate
+- the __CPROVER_is_freed built-in predicate
