CONTRACTS: Hotfix for is_fresh performance

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

@@ -7,8 +7,8 @@ main.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 --
-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,7 @@ 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 && __CPROVER_is_fresh(arr, size))
 __CPROVER_assigns(arr[0])
 __CPROVER_ensures(arr[0] == 0)
   // clang-format on

regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---restrict-function-pointer foo.CALL/arr_fun_contract --dfcc main --enforce-contract foo
+--malloc-may-fail --malloc-fail-null --restrict-function-pointer foo.CALL/arr_fun_contract --dfcc main --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

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

@@ -6,7 +6,8 @@ __CPROVER_requires(__CPROVER_is_fresh(arr, size))
 __CPROVER_assigns(__CPROVER_object_from(arr))
 // clang-format on
 {
-  assert(__CPROVER_same_object(arr, arr + size));
+  __CPROVER_assert(arr != NULL, "arr is not NULL");
+  __CPROVER_assert(size < __CPROVER_max_malloc_size, "size is capped");
   if(size > 0)
   {
     arr[0] = 0;

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main_bounded.c

@@ -0,0 +1,25 @@
+#include <stdlib.h>
+
+const size_t MAX_SIZE = 5000000;
+void foo(char *arr, size_t size)
+  // clang-format off
+__CPROVER_requires(size < MAX_SIZE)
+__CPROVER_requires(__CPROVER_is_fresh(arr, size))
+__CPROVER_assigns(__CPROVER_object_from(arr))
+// clang-format on
+{
+  __CPROVER_assert(arr != NULL, "arr is not NULL");
+  __CPROVER_assert(size < __CPROVER_max_malloc_size, "size is capped");
+  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-failure-modes/test-fail-assert-bounded.desc

@@ -0,0 +1,20 @@
+CORE
+main_bounded.c
+--malloc-may-fail --malloc-fail-assert --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh max allocation size exceeded: SUCCESS$
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$
+^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This tests shows that using is_fresh with --malloc-fail-assert active and
+imposing a limit on the size parameter succeeds.

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc

@@ -0,0 +1,23 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-assert --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh max allocation size exceeded: FAILURE$
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$
+^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This tests shows that using is_fresh with --malloc-fail-assert active and
+without imposing a limit on the size parameter results in an failed assertion
+in is_fresh that detects that the size may be too large, but also results in an
+implicit assumption that the size is less than the maximum allocation size
+(just like when used with malloc).

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc

@@ -0,0 +1,19 @@
+CORE
+main_bounded.c
+--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$
+^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This tests shows that using is_fresh without malloc failure modes active and
+imposing a limit on the size parameter succeeds.

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc

@@ -0,0 +1,23 @@
+CORE
+main.c
+--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
+^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: FAILURE$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: FAILURE$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+--
+This tests shows that using is_fresh without malloc failure modes active and
+without imposing a limit on the size parameter results in failures:
+1. in the contracts library because the addressable range of the allocated object
+cannot be represented without pointer overflow
+2. in the assigns clause checking because the assignable range cannot be represented
+3. in pointer overflow checks generated by CBMC pointer checks

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc

@@ -0,0 +1,19 @@
+CORE
+main_bounded.c
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$
+^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This tests shows that using is_fresh with --malloc-fail-null active and
+imposing a limit on the size parameter succeeds.

regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc

@@ -0,0 +1,21 @@
+CORE
+main.c
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
+^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
+^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$
+^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This tests shows that using is_fresh with --malloc-fail-null active and
+without imposing a limit on the size parameter results in an implicit assumption
+that the size is less than the maximum allocation size
+(just like malloc does, except is_fresh does not fail).

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

@@ -3,9 +3,7 @@
 
 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_requires(0 < 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

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

@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/main.c

@@ -3,9 +3,7 @@
 
 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_requires(0 < 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 missing arg */))

regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
 ^.*error: __CPROVER_pointer_in_range_dfcc expects three arguments$
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/main.c

@@ -3,10 +3,8 @@
 
 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_requires(0 < size && __CPROVER_is_fresh(arr, size) &&
+  __CPROVER_pointer_in_range_dfcc(arr, cur, arr + size))
 __CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(
   arr, cur, 2 /* wrong type arg */))
 // clang-format on

regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
+--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
 ^.*error: __CPROVER_pointer_in_range_dfcc expects pointer-typed arguments$
 ^EXIT=(1|64)$
 ^SIGNAL=0$