CONTRACTS: hotfix for is_fresh performance

In assumption contexts, turn a control
flow branch into an assert/assume pair
and inline the malloc function in
is_fresh, while removing the failure
mode logic.

Author: Remi Delmas

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

@@ -1,14 +1,15 @@
 CORE
 main.c
 --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo
+^\[__CPROVER_contracts_is_fresh.assertion.\d+] line \d+ __CPROVER_is_fresh requires size < __CPROVER_max_malloc_size: FAILURE$
 ^\[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$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
-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`.
+This test checks that assuming is_fresh(ptr, size) with a non-deterministic size
+checks that size < __CPROVER_max_malloc_size and then assumes it.
+This guarantees that the address `ptr + size` can always be computed and
+represented without offset bits overflowing into the object bits in the pointer
+model used by CBMC.

regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/vect.h

@@ -11,9 +11,9 @@ void resize_vec(vect *v, size_t incr)
   // clang-format off
 __CPROVER_requires(
   __CPROVER_is_fresh(v, sizeof(vect)) &&
-  __CPROVER_is_fresh(v->arr, v->size) &&
-  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
-  0 < incr && incr < __CPROVER_max_malloc_size - v->size
+  0 < v->size && v->size < __CPROVER_max_malloc_size &&
+  0 < incr && incr < __CPROVER_max_malloc_size - v->size &&
+  __CPROVER_is_fresh(v->arr, v->size)
 )
 __CPROVER_assigns(v->size, v->arr, __CPROVER_object_whole(v->arr))
 __CPROVER_frees(v->arr)
@@ -34,9 +34,9 @@ void resize_vec_incr10(vect *v)
   // clang-format off
 __CPROVER_requires(
   __CPROVER_is_fresh(v, sizeof(vect)) &&
-  __CPROVER_is_fresh(v->arr, v->size) &&
-  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
-  v->size + 10 < __CPROVER_max_malloc_size
+  0 < v->size && v->size < __CPROVER_max_malloc_size &&
+  v->size + 10 < __CPROVER_max_malloc_size &&
+  __CPROVER_is_fresh(v->arr, v->size)
 )
 __CPROVER_assigns(v->size)
 __CPROVER_ensures(

regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_pass/vect.h

@@ -11,8 +11,8 @@ void resize_vec(vect *v, size_t incr)
   // clang-format off
 __CPROVER_requires(
   __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size < __CPROVER_max_malloc_size &&
   __CPROVER_is_fresh(v->arr, v->size) &&
-  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
   0 < incr && incr < __CPROVER_max_malloc_size - v->size
 )
 __CPROVER_assigns(v->size, v->arr, __CPROVER_object_whole(v->arr))
@@ -34,8 +34,8 @@ void resize_vec_incr10(vect *v)
   // clang-format off
 __CPROVER_requires(
   __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size < __CPROVER_max_malloc_size &&
   __CPROVER_is_fresh(v->arr, v->size) &&
-  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
   v->size + 10 < __CPROVER_max_malloc_size
 )
 __CPROVER_assigns(*v, __CPROVER_object_whole(v->arr))

regression/contracts-dfcc/function-pointer-contracts-enforce/main.c

@@ -9,7 +9,8 @@ typedef void (*arr_fun_t)(char *arr, size_t size);
 // resets the first element to zero
 void arr_fun_contract(char *arr, size_t size)
   // clang-format off
-__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
+__CPROVER_requires(0 < size && size < __CPROVER_max_malloc_size &&
+ __CPROVER_is_fresh(arr, size))
 __CPROVER_assigns(arr[0])
 __CPROVER_ensures(arr[0] == 0)
   // clang-format on
@@ -20,7 +21,8 @@ __CPROVER_ensures(arr[0] == 0)
 // to establish post-conditions
 int foo(char *arr, size_t size, arr_fun_t arr_fun)
   // clang-format off
-__CPROVER_requires(arr == NULL || __CPROVER_is_fresh(arr, size))
+__CPROVER_requires(arr == NULL ||
+  size < __CPROVER_max_malloc_size && __CPROVER_is_fresh(arr, size))
 __CPROVER_requires(__CPROVER_obeys_contract(arr_fun, arr_fun_contract))
 __CPROVER_assigns(arr && size > 0 : arr[0])
 __CPROVER_ensures((__CPROVER_return_value == 0) ==> (arr[0] == 0))

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

@@ -2,7 +2,8 @@
 
 void foo(char *arr, size_t size)
   // clang-format off
-__CPROVER_requires(__CPROVER_is_fresh(arr, size))
+__CPROVER_requires(size < __CPROVER_max_malloc_size &&
+ __CPROVER_is_fresh(arr, size))
 __CPROVER_assigns(__CPROVER_object_from(arr))
 // clang-format on
 {

src/ansi-c/library/cprover_contracts.c

@@ -11,6 +11,7 @@ extern __CPROVER_size_t __CPROVER_max_malloc_size;
 extern const void *__CPROVER_alloca_object;
 extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_new_object;
+extern const void *__CPROVER_memory_leak;
 extern __CPROVER_bool __CPROVER_malloc_is_new_array;
 int __builtin_clzll(unsigned long long);
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
@@ -1191,17 +1192,24 @@ __CPROVER_HIDE:;
         (write_set->assert_ensures_ctx == 0),
       "only one context flag at a time");
 #endif
-    // fail if size is too big
-    if(size >= __CPROVER_max_malloc_size)
-      return 0;
+    __CPROVER_assert(
+      size < __CPROVER_max_malloc_size,
+      "__CPROVER_is_fresh requires size < __CPROVER_max_malloc_size");
+    __CPROVER_assume(size < __CPROVER_max_malloc_size);
 
-    // pass a null write set pointer to the instrumented malloc
-    void *ptr = __CPROVER_contracts_malloc(size, 0);
+    void *ptr = __CPROVER_allocate(size, 0);
     *elem = ptr;
-    // malloc can also return a NULL pointer if failure modes are active
-    if(!ptr)
-      return 0;
-      // record fresh object in the object set
+
+    // record the object size for non-determistic bounds checking
+    __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_malloc_is_new_array =
+      record_malloc ? 0 : __CPROVER_malloc_is_new_array;
+
+    // detect memory leaks
+    __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
+
+    // record fresh object in the object set
 #ifdef DFCC_DEBUG
     // manually inlined below
     __CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr);
@@ -1226,13 +1234,24 @@ __CPROVER_HIDE:;
       "only one context flag at a time");
 #endif
     // fail if size is too big
-    if(size >= __CPROVER_max_malloc_size)
-      return 0;
-    void *ptr = __CPROVER_contracts_malloc(size, 0);
+    __CPROVER_assert(
+      size < __CPROVER_max_malloc_size,
+      "__CPROVER_is_fresh requires size < __CPROVER_max_malloc_size");
+    __CPROVER_assume(size < __CPROVER_max_malloc_size);
+
+    void *ptr = __CPROVER_allocate(size, 0);
     *elem = ptr;
-    if(!ptr)
-      return 0;
-      // record fresh object in the caller's write set
+
+    // record the object size for non-determistic bounds checking
+    __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_malloc_is_new_array =
+      record_malloc ? 0 : __CPROVER_malloc_is_new_array;
+
+    // detect memory leaks
+    __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
+    __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
+
+    // record fresh object in the caller's write set
 #ifdef DFCC_DEBUG
     __CPROVER_contracts_obj_set_add(write_set->linked_allocated, ptr);
 #else