CONTRACTS: Support bounded user defined memory-predicates

regression/contracts-dfcc/assigns-enforce-malloc-zero/main.c

@@ -1,31 +1,32 @@
+#include <stdbool.h>
 #include <stdlib.h>
 
-// returns the index at which the write was performed if any
-// -1 otherwise
-int foo(char *a, int size)
+bool foo(char *a, size_t size, size_t *out)
   // 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_object_whole(a))
+  __CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out)))
+  __CPROVER_assigns(a: __CPROVER_object_from(a), *out)
   __CPROVER_ensures(
-    a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
+    a && __CPROVER_return_value ==>
+      (0 <= *out && *out < size &&
+      a[*out] == 0)
+  )
 // clang-format on
 {
-  if(!a)
-    return -1;
-  int i;
-  if(0 <= i && i < size)
+  size_t i;
+  if(a && 0 <= i && i < size)
   {
     a[i] = 0;
-    return i;
+    *out = i;
+    return true;
   }
-  return -1;
+  return false;
 }
 
-int main()
+void main()
 {
-  size_t size;
   char *a;
-  foo(a, size);
-  return 0;
+  size_t size;
+  size_t *out;
+  foo(a, size, out);
 }

regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc

@@ -1,11 +1,14 @@
 CORE
 main.c
---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$
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo
+^\[foo.assigns.\d+\] line \d+ Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that \*out is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-This test checks that objects of size zero or __CPROVER_max_malloc_size
-do not cause spurious falsifications in assigns clause instrumentation
-in contract enforcement mode.
+This test checks assuming is_fresh(ptr, size) with a non-deterministic size
+does not result in spurious falsifications when checking assigns clauses.
+An implicit strict upper bound of __CPROVER_max_malloc_size is imposed on the size by
+__CPROVER_is_fresh which guarantees the absence of pointer overflow when computing
+the address `ptr + size`.

regression/contracts-dfcc/assigns-replace-malloc-zero/main.c

@@ -1,37 +1,41 @@
+#include <stdbool.h>
 #include <stdlib.h>
 
-// returns the index at which the write was performed if any
-// -1 otherwise
-int foo(char *a, int size)
+bool foo(char *a, size_t size, size_t *out)
   // clang-format off
-__CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
-__CPROVER_requires(a == NULL || __CPROVER_rw_ok(a, size))
-__CPROVER_assigns(__CPROVER_object_whole(a))
-__CPROVER_ensures(
-    a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
+  __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size))
+  __CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out)))
+  __CPROVER_assigns(a: __CPROVER_object_from(a), *out)
+  __CPROVER_ensures(
+    a && __CPROVER_return_value ==>
+      (0 <= *out && *out < size &&
+      a[*out] == 0)
+  )
 // clang-format on
 {
-  if(!a)
-    return -1;
-  int i;
-  if(0 <= i && i < size)
+  size_t i;
+  if(a && 0 <= i && i < size)
   {
     a[i] = 0;
-    return i;
+    *out = i;
+    return true;
   }
-  return -1;
+  return false;
 }
 
-int main()
+int nondet_int();
+
+void bar(int size)
+{
+  size_t out;
+  char *a = malloc(size);
+  bool res = foo(a, size, &out);
+  if(a && res)
+    __CPROVER_assert(a[out] == 0, "expecting SUCCESS");
+}
+
+void main()
 {
-  int size;
-  if(size < 0)
-    size = 0;
-  if(size > __CPROVER_max_malloc_size)
-    size = __CPROVER_max_malloc_size;
-  char *a = malloc(size * sizeof(*a));
-  int res = foo(a, size);
-  if(a && res >= 0)
-    __CPROVER_assert(a[res] == 0, "expecting SUCCESS");
-  return 0;
+  size_t size;
+  bar(size);
 }

regression/contracts-dfcc/assigns-replace-malloc-zero/test.desc

@@ -1,9 +1,9 @@
 CORE
 main.c
---dfcc main --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$
+\[bar\.assertion\.\d+\] line \d+ expecting SUCCESS: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that objects of size zero or of __CPROVER_max_malloc_size

regression/contracts-dfcc/is_unique_01_replace/main.c

@@ -1,84 +1,38 @@
 #include <assert.h>
 #include <stdbool.h>
-#include <stddef.h>
-#include <stdint.h>
 #include <stdlib.h>
 
-bool dummy_for_definitions(int *n)
-{
-  assert(__CPROVER_is_fresh(&n, sizeof(int)));
-  int *x = malloc(sizeof(int));
-}
-
 bool ptr_ok(int *x)
 {
-  return *x < 5;
-}
-
-/*
-	Here are the meanings of the predicates: 
-
-static _Bool __foo_memory_map[__CPROVER_constant_infinity_uint]; 
-
-bool __foo_requires_is_fresh(void **elem, size_t size) {
-	*elem = malloc(size);
-	if (!*elem || (__foo_memory_map[__CPROVER_POINTER_OBJECT(*elem)] != 0)) return false;
-
-	__foo_memory_map[__CPROVER_POINTER_OBJECT(*elem)] = 1;
-	return true;
+  return 0 < *x && *x < 5;
 }
 
-bool __foo_ensures_is_fresh(void *elem, size_t size) {
-	bool ok = (__foo_memory_map[__CPROVER_POINTER_OBJECT(elem)] == 0 && 
-		  	   __CPROVER_r_ok(elem, size));
-	__foo_memory_map[__CPROVER_POINTER_OBJECT(elem)] = 1;
-	return ok;
-}
-
-
-_Bool __call_foo_requires_is_fresh(void *elem, size_t size) {
-	_Bool r_ok = __CPROVER_r_ok(elem, size);
-	if (!__CPROVER_r_ok(elem, size) || 
-	    __foo_memory_map[__CPROVER_POINTER_OBJECT(elem)]) return 0;
-	__foo_memory_map[__CPROVER_POINTER_OBJECT(elem)] = 1;
-	return 1;
-}
-
-// In the calling context, we assume freshness means new 
-// allocation from within the function.
-bool __call_foo_ensures_is_fresh(void **elem, size_t size) {
-	*elem = malloc(size);
-	return (*elem != NULL);
-}
-*/
-
 bool return_ok(int ret_value, int *x)
 {
-  int a;
-  a = *x;
-  return ret_value == *x + 5;
+  return ret_value == (*x + 5);
 }
 
-// The 'ensures' __CPROVER_is_fresh test is unnecessary, but left in just to test the function is working correctly.
-// If you remove the negation, the program will fail, because 'x' is not fresh.
-
-int foo(int *x, int y) __CPROVER_assigns(*x)
-  __CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)) && *x > 0 && ptr_ok(x))
-    __CPROVER_ensures(
-      !ptr_ok(x) && !__CPROVER_is_fresh(x, sizeof(int)) &&
-      return_ok(__CPROVER_return_value, x))
+int foo(int *x)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
+__CPROVER_requires(ptr_ok(x))
+__CPROVER_assigns(*x)
+__CPROVER_ensures(!ptr_ok(x))
+__CPROVER_ensures(return_ok(__CPROVER_return_value, x))
+// clang-format on
 {
   *x = *x + 4;
-  int y = *x + 5;
   return *x + 5;
 }
 
-int main()
+void main()
 {
-  int *n = malloc(sizeof(int));
-  assert(__CPROVER_r_ok(n, sizeof(int)));
-  *n = 3;
-  int o = foo(n, 10);
-  assert(o >= 10 && o == *n + 5);
-  return 0;
+  int x;
+  int *_x = &x;
+  if(ptr_ok(_x))
+  {
+    int ret_val = foo(_x);
+    assert(!ptr_ok(_x));
+    assert(return_ok(ret_val, _x));
+  }
 }

regression/contracts-dfcc/is_unique_01_replace/test.desc

@@ -6,8 +6,5 @@ main.c
 ^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.
+This test shows that replacing a call by a contract establishes the
+postconditions of the contracts.

regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/main.c

@@ -0,0 +1,22 @@
+#include <stdlib.h>
+
+void foo(char *arr, size_t size)
+  // clang-format off
+__CPROVER_requires(__CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(__CPROVER_object_from(arr))
+// clang-format on
+{
+  assert(__CPROVER_same_object(arr, arr + size));
+  if(size > 0)
+  {
+    arr[0] = 0;
+    arr[size - 1] = 0;
+  }
+}
+
+int main()
+{
+  char *arr;
+  size_t size;
+  foo(arr, size);
+}

regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This tests shows how assuming that a pointer is fresh with a nondeterministic
+size implicitly assumes that the size is strictly less than the max malloc
+size. This is in order to ensure that the internal representation used for
+assignable address ranges cannot suffer pointer overflows.

regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/main.c

@@ -0,0 +1,42 @@
+#include <stdbool.h>
+#include <stdlib.h>
+
+// A vtable is a struct containing function pointers
+typedef struct vtable_s
+{
+  int (*f)(void);
+} vtable_t;
+
+int return_0()
+{
+  return 0;
+}
+
+int return_1()
+{
+  return 1;
+}
+
+// we have two possible vtables
+vtable_t vtable_0 = {.f = &return_0};
+vtable_t vtable_1 = {.f = &return_1};
+
+// foo takes a vtable and calls f
+int foo(vtable_t *vtable)
+  // clang-format off
+__CPROVER_requires(
+  // vtable is nondeterministic pointer to one of two objects
+    __CPROVER_pointer_in_range_dfcc(&vtable_0, vtable, &vtable_0) ||
+    __CPROVER_pointer_in_range_dfcc(&vtable_1, vtable, &vtable_1))
+__CPROVER_ensures(__CPROVER_return_value == 0 || __CPROVER_return_value == 1)
+// clang-format on
+{
+CALL:
+  return vtable->f();
+}
+
+int main()
+{
+  vtable_t *vtable;
+  foo(vtable);
+}

regression/contracts-dfcc/memory-predicates-pointer-in-range-nondet/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--restrict-function-pointer foo.CALL/return_0,return_1 --nondet-static-exclude vtable_0 --nondet-static-exclude vtable_1 --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Demonstrates the use of __CPROVER_pointer_in_range_dfcc to define nondeterministic
+pointers to one or more targets.

regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c

@@ -0,0 +1,24 @@
+#include <assert.h>
+#include <stdlib.h>
+
+void foo(char *arr, size_t size, char *cur)
+  // clang-format off
+__CPROVER_requires(
+    (0 < size && size < __CPROVER_max_malloc_size) &&
+    __CPROVER_is_fresh(arr, size) &&
+    __CPROVER_pointer_in_range_dfcc(arr, cur, arr + size))
+__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(arr, cur, arr + size))
+// clang-format on
+{
+  assert(__CPROVER_r_ok(arr, size));
+  assert(__CPROVER_same_object(arr, cur));
+  assert(arr <= cur && cur <= arr + size);
+}
+
+int main()
+{
+  char *arr;
+  size_t size;
+  char *cur;
+  foo(arr, size, cur);
+}

regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks that assuming pointer-in-range as preconditions establishes a state
+in which the definition of the predicate holds.