Skip to content

Commit 3a1a5ac

Browse files
author
Remi Delmas
committed
CONTRACTS: hotfix for is_fresh performance
Solves a major performance issue and aligns the behavior of is_fresh with that of malloc with respect to size assertions/assumptions. malloc is now inlined in the body of `__CPROVER_contract_is_fresh` and the failure logic is simplified in assumption contexts.
1 parent 4aceefd commit 3a1a5ac

File tree

22 files changed

+275
-59
lines changed

22 files changed

+275
-59
lines changed

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@ main.c
77
^SIGNAL=0$
88
^VERIFICATION SUCCESSFUL$
99
--
10-
This test checks assuming is_fresh(ptr, size) with a non-deterministic size
11-
does not result in spurious falsifications when checking assigns clauses.
12-
An implicit strict upper bound of __CPROVER_max_malloc_size is imposed on the size by
13-
__CPROVER_is_fresh which guarantees the absence of pointer overflow when computing
14-
the address `ptr + size`.
10+
This test checks that assuming is_fresh(ptr, size) with a non-deterministic size
11+
checks that size < __CPROVER_max_malloc_size and then assumes it.
12+
This guarantees that the address `ptr + size` can always be computed and
13+
represented without offset bits overflowing into the object bits in the pointer
14+
model used by CBMC.

‎regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_fail/vect.h‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,9 @@ void resize_vec(vect *v, size_t incr)
1111
// clang-format off
1212
__CPROVER_requires(
1313
__CPROVER_is_fresh(v, sizeof(vect)) &&
14-
__CPROVER_is_fresh(v->arr, v->size) &&
15-
0 < v->size && v->size <= __CPROVER_max_malloc_size &&
16-
0 < incr && incr < __CPROVER_max_malloc_size - v->size
14+
0 < v->size && v->size < __CPROVER_max_malloc_size &&
15+
0 < incr && incr < __CPROVER_max_malloc_size - v->size &&
16+
__CPROVER_is_fresh(v->arr, v->size)
1717
)
1818
__CPROVER_assigns(v->size, v->arr, __CPROVER_object_whole(v->arr))
1919
__CPROVER_frees(v->arr)
@@ -34,9 +34,9 @@ void resize_vec_incr10(vect *v)
3434
// clang-format off
3535
__CPROVER_requires(
3636
__CPROVER_is_fresh(v, sizeof(vect)) &&
37-
__CPROVER_is_fresh(v->arr, v->size) &&
38-
0 < v->size && v->size <= __CPROVER_max_malloc_size &&
39-
v->size + 10 < __CPROVER_max_malloc_size
37+
0 < v->size && v->size < __CPROVER_max_malloc_size &&
38+
v->size + 10 < __CPROVER_max_malloc_size &&
39+
__CPROVER_is_fresh(v->arr, v->size)
4040
)
4141
__CPROVER_assigns(v->size)
4242
__CPROVER_ensures(

‎regression/contracts-dfcc/assigns_replace_havoc_dependent_targets_pass/vect.h‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ void resize_vec(vect *v, size_t incr)
1111
// clang-format off
1212
__CPROVER_requires(
1313
__CPROVER_is_fresh(v, sizeof(vect)) &&
14+
0 < v->size && v->size < __CPROVER_max_malloc_size &&
1415
__CPROVER_is_fresh(v->arr, v->size) &&
15-
0 < v->size && v->size <= __CPROVER_max_malloc_size &&
1616
0 < incr && incr < __CPROVER_max_malloc_size - v->size
1717
)
1818
__CPROVER_assigns(v->size, v->arr, __CPROVER_object_whole(v->arr))
@@ -34,8 +34,8 @@ void resize_vec_incr10(vect *v)
3434
// clang-format off
3535
__CPROVER_requires(
3636
__CPROVER_is_fresh(v, sizeof(vect)) &&
37+
0 < v->size && v->size < __CPROVER_max_malloc_size &&
3738
__CPROVER_is_fresh(v->arr, v->size) &&
38-
0 < v->size && v->size <= __CPROVER_max_malloc_size &&
3939
v->size + 10 < __CPROVER_max_malloc_size
4040
)
4141
__CPROVER_assigns(*v, __CPROVER_object_whole(v->arr))

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ typedef void (*arr_fun_t)(char *arr, size_t size);
99
// resets the first element to zero
1010
void arr_fun_contract(char *arr, size_t size)
1111
// clang-format off
12-
__CPROVER_requires(size > 0 && __CPROVER_is_fresh(arr, size))
12+
__CPROVER_requires(0 < size && __CPROVER_is_fresh(arr, size))
1313
__CPROVER_assigns(arr[0])
1414
__CPROVER_ensures(arr[0] == 0)
1515
// clang-format on

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--restrict-function-pointer foo.CALL/arr_fun_contract --dfcc main --enforce-contract foo
3+
--malloc-may-fail --malloc-fail-null --restrict-function-pointer foo.CALL/arr_fun_contract --dfcc main --enforce-contract foo
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ __CPROVER_requires(__CPROVER_is_fresh(arr, size))
66
__CPROVER_assigns(__CPROVER_object_from(arr))
77
// clang-format on
88
{
9-
assert(__CPROVER_same_object(arr, arr + size));
9+
__CPROVER_assert(arr != NULL, "arr is not NULL");
10+
__CPROVER_assert(size < __CPROVER_max_malloc_size, "size is capped");
1011
if(size > 0)
1112
{
1213
arr[0] = 0;

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

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
#include <stdlib.h>
2+
3+
const size_t MAX_SIZE = 5000000;
4+
void foo(char *arr, size_t size)
5+
// clang-format off
6+
__CPROVER_requires(size < MAX_SIZE)
7+
__CPROVER_requires(__CPROVER_is_fresh(arr, size))
8+
__CPROVER_assigns(__CPROVER_object_from(arr))
9+
// clang-format on
10+
{
11+
__CPROVER_assert(arr != NULL, "arr is not NULL");
12+
__CPROVER_assert(size < __CPROVER_max_malloc_size, "size is capped");
13+
if(size > 0)
14+
{
15+
arr[0] = 0;
16+
arr[size - 1] = 0;
17+
}
18+
}
19+
20+
int main()
21+
{
22+
char *arr;
23+
size_t size;
24+
foo(arr, size);
25+
}

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

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
main_bounded.c
3+
--malloc-may-fail --malloc-fail-assert --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
4+
^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh max allocation size exceeded: SUCCESS$
5+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
6+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
7+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$
8+
^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$
9+
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$
10+
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$
11+
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
12+
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
13+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$
14+
^EXIT=0$
15+
^SIGNAL=0$
16+
^VERIFICATION SUCCESSFUL$
17+
--
18+
--
19+
This tests shows that using is_fresh with --malloc-fail-assert active and
20+
imposing a limit on the size parameter succeeds.

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
CORE
2+
main.c
3+
--malloc-may-fail --malloc-fail-assert --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
4+
^\[__CPROVER_contracts_is_fresh.assertion.\d+\] line \d+ __CPROVER_is_fresh max allocation size exceeded: FAILURE$
5+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
6+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
7+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$
8+
^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$
9+
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$
10+
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$
11+
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
12+
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
13+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$
14+
^EXIT=10$
15+
^SIGNAL=0$
16+
^VERIFICATION FAILED$
17+
--
18+
--
19+
This tests shows that using is_fresh with --malloc-fail-assert active and
20+
without imposing a limit on the size parameter results in an failed assertion
21+
in is_fresh that detects that the size may be too large, but also results in an
22+
implicit assumption that the size is less than the maximum allocation size
23+
(just like when used with malloc).

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
CORE
2+
main_bounded.c
3+
--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
4+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: SUCCESS$
5+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$
6+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$
7+
^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$
8+
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$
9+
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$
10+
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
11+
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$
12+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$
13+
^EXIT=0$
14+
^SIGNAL=0$
15+
^VERIFICATION SUCCESSFUL$
16+
--
17+
--
18+
This tests shows that using is_fresh without malloc failure modes active and
19+
imposing a limit on the size parameter succeeds.

0 commit comments

Comments
 (0)