diff --git a/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc b/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc index caf6e623c0a..6a178fbc2a7 100644 --- a/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc +++ b/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. diff --git a/regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/vect.h b/regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/vect.h index 47a2acdfce3..9e5c708423d 100644 --- a/regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/vect.h +++ b/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( diff --git a/regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_pass/vect.h b/regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_pass/vect.h index 22b29307bfb..b9d28f6a6bb 100644 --- a/regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_pass/vect.h +++ b/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)) diff --git a/regression/contracts-dfcc/function-pointer-contracts-enforce/main.c b/regression/contracts-dfcc/function-pointer-contracts-enforce/main.c index 469bb10071b..b4907255320 100644 --- a/regression/contracts-dfcc/function-pointer-contracts-enforce/main.c +++ b/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 diff --git a/regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc b/regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc index 2a1130b1606..9c235f053f5 100644 --- a/regression/contracts-dfcc/function-pointer-contracts-enforce/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/main.c b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main.c similarity index 72% rename from regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/main.c rename to regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main.c index 6d3c2bfb9c1..fd067ed97ce 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/main.c +++ b/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; diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main_bounded.c b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main_bounded.c new file mode 100644 index 00000000000..38376af600c --- /dev/null +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main_bounded.c @@ -0,0 +1,25 @@ +#include + +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); +} diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc new file mode 100644 index 00000000000..7d845f9c092 --- /dev/null +++ b/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. diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc new file mode 100644 index 00000000000..f5ce8894ac5 --- /dev/null +++ b/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). diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc new file mode 100644 index 00000000000..d4d4ec91ae5 --- /dev/null +++ b/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. diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none.desc new file mode 100644 index 00000000000..90c456ffc0a --- /dev/null +++ b/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 diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc new file mode 100644 index 00000000000..10fb1343ffa --- /dev/null +++ b/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. diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc new file mode 100644 index 00000000000..06fbd42f029 --- /dev/null +++ b/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). diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/test.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/test.desc deleted file mode 100644 index f0a7357d53a..00000000000 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-requires-max-malloc-size/test.desc +++ /dev/null @@ -1,12 +0,0 @@ -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. diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c index 5acb55bedca..02723e23e92 100644 --- a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c +++ b/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 diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc index a96c3616508..e0e29589e13 100644 --- a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/main.c b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/main.c index 8eb18cc76eb..710bfbd2b59 100644 --- a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/main.c +++ b/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 */)) diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/test.desc b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/test.desc index f6e9098f119..3116264747b 100644 --- a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-01/test.desc +++ b/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$ diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/main.c b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/main.c index 126f296d545..36d6b80e250 100644 --- a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/main.c +++ b/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 diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/test.desc b/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/test.desc index 860036ca9cd..67c197865a0 100644 --- a/regression/contracts-dfcc/memory-predicates-pointer-in-range-typecheck-failure-02/test.desc +++ b/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$ diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 0a8459df020..2a4de2cc6ff 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -8,10 +8,11 @@ // external dependencies extern __CPROVER_size_t __CPROVER_max_malloc_size; -extern const void *__CPROVER_alloca_object; +const void *__CPROVER_alloca_object = 0; extern const void *__CPROVER_deallocated; -extern const void *__CPROVER_new_object; -extern __CPROVER_bool __CPROVER_malloc_is_new_array; +const void *__CPROVER_new_object = 0; +extern const void *__CPROVER_memory_leak; +__CPROVER_bool __CPROVER_malloc_is_new_array = 0; int __builtin_clzll(unsigned long long); __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); __CPROVER_size_t __VERIFIER_nondet_size(); @@ -1191,17 +1192,41 @@ __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; + if( + __CPROVER_malloc_failure_mode == + __CPROVER_malloc_failure_mode_return_null) + { + // When --malloc-may-fail --malloc-fail-null + // add implicit assumption that the size is capped + __CPROVER_assume(size < __CPROVER_max_malloc_size); + } + else if( + __CPROVER_malloc_failure_mode == + __CPROVER_malloc_failure_mode_assert_then_assume) + { + // When --malloc-may-fail --malloc-fail-assert + // check if max allocation size is exceeded and + // add implicit assumption that the size is capped + __CPROVER_assert( + size < __CPROVER_max_malloc_size, + "__CPROVER_is_fresh max allocation size exceeded"); + __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; + + // do not detect memory leaks when assuming a precondition of a contract + // for contract checking + // __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 +1251,37 @@ __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); + if( + __CPROVER_malloc_failure_mode == + __CPROVER_malloc_failure_mode_return_null) + { + __CPROVER_assume(size < __CPROVER_max_malloc_size); + } + else if( + __CPROVER_malloc_failure_mode == + __CPROVER_malloc_failure_mode_assert_then_assume) + { + __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 when is_fresh is assumed in a post condition + // of a replaced contract to model a malloc performed by the function + // being abstracted by the contract + __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 diff --git a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md index 13219022147..366129a870d 100644 --- a/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md +++ b/src/goto-instrument/contracts/doc/user/contracts-memory-predicates.md @@ -129,6 +129,40 @@ int foo() } ``` +#### Influence of memory allocation failure modes flags in assumption contexts + +CBMC models +[memory allocation failure modes](https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/memory-primitives.md#malloc-modelling). +When activated, these modesl result in different +behaviours for `__CPROVER_is_fresh` in assumption contexts (i.e. when used in a +requires clause of a contract being checked against a function, or in an +ensures clause of a contract being used to abstract a function call). + +1. **No failure mode** (no flags): + In this mode, `malloc` and `__CPROVER_is_fresh` never fail + and will accept a size parameter up to `SIZE_MAX` without triggerring errors. + However, pointer overflow and assigns clause checking errors will happen any + time one tries to access such objects beyond an offset of + `__CPROVER_max_malloc_size` (in bytes), by executing `ptr[size-1]` or + `ptr[size]` in user-code, or by writing + `__CPROVER_assigns(__CPROVER_object_from(ptr))` in a contract; +1. **Fail with NULL** (flags: `--malloc-may-fail --malloc-fail-null`): + In this mode, if `size` is larger than + `__CPROVER_max_malloc_size`, `malloc` returns a NULL pointer, and imposes an + implicit assumption that size is less than `__CPROVER_max_malloc_size` when + returning a non-NULL pointer. `__CPROVER_is_fresh` never fails in assumption + contexts, so it adds an implicit assumption that `size` is less + than `__CPROVER_max_malloc_size`. +1. **Fail assert** (flags: `--malloc-may-fail --malloc-fail-assert`): + In this mode, if `size` is larger + than `__CPROVER_max_malloc_size`, an `max allocation size exceeded` assertion + is triggered in `malloc` and execution continues under the assumption that + `size` is less than `__CPROVER_max_malloc_size`, with `malloc` returning a + non-NULL pointer. `__CPROVER_is_fresh` never fails in assumption contexts, + so it will trigger a `max allocation size exceeded` assertion and continue + execution under the implicit assumption that `size` is less than + `__CPROVER_max_malloc_size`. + ## The __CPROVER_pointer_in_range_dfcc predicate ### Syntax