From d4a1c6d33ab41b3ef416bb5fd812d2050ecc9fd7 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 27 Feb 2025 15:35:04 -0500 Subject: [PATCH] CONTRACTS: is_fresh now checks separation of byte-intervals instead of whole objects. When assumed, is_fresh still builds distinct objects. When asserted, it allows for either distinct objects, or distinct byte intervals within the same object. A function foo(int *a, int *b) that requires is_fresh(a) and is_fresh(b) is checked under the assumption that a and b are distinct objects, but can still be used in contexts where a and b are distinct slices within the same base object. This is sound because the function is checked under the stronger precondition and hence is proved to not perform any operation that requires that a and b be in the same object, such as pointer differences or comparisons. --- .../test-fail-none.desc | 4 +- .../main.c | 37 ++++++++++++++++++ .../test.desc | 12 ++++++ .../main.c | 37 ++++++++++++++++++ .../test.desc | 12 ++++++ .../main.c | 36 +++++++++++++++++ .../test.desc | 13 +++++++ .../main.c | 36 +++++++++++++++++ .../test.desc | 11 ++++++ src/ansi-c/library/cprover_contracts.c | 39 +++++++++---------- 10 files changed, 214 insertions(+), 23 deletions(-) create mode 100644 regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/main.c create mode 100644 regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/test.desc create mode 100644 regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/main.c create mode 100644 regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/test.desc create mode 100644 regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/main.c create mode 100644 regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/test.desc create mode 100644 regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/main.c create mode 100644 regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/test.desc 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 index ed2faa39166..d5451924419 100644 --- 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 @@ -1,9 +1,7 @@ CORE dfcc-only main.c ---no-malloc-may-fail --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$ +--no-malloc-may-fail --dfcc main --enforce-contract foo ^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$ -^\*\* 2 of \d+ failed ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/main.c b/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/main.c new file mode 100644 index 00000000000..c1627849259 --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/main.c @@ -0,0 +1,37 @@ +#include +int nondet_int(); + +void foo(int *a, int **b_out, int **c_out) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(a, 2*sizeof(int))) +__CPROVER_requires(__CPROVER_is_fresh(b_out, sizeof(int*))) +__CPROVER_requires(__CPROVER_is_fresh(c_out, sizeof(int*))) +__CPROVER_ensures(__CPROVER_is_fresh(*b_out, sizeof(int))) +__CPROVER_ensures(__CPROVER_is_fresh(*c_out, sizeof(int))) +__CPROVER_assigns(*b_out, *c_out) +__CPROVER_ensures(**b_out == a[0]) +__CPROVER_ensures(**c_out == a[1]) +// clang-format on +{ + if(nondet_int()) + { + *b_out = malloc(sizeof(int)); + __CPROVER_assume(*b_out != NULL); + *c_out = malloc(sizeof(int)); + __CPROVER_assume(*c_out != NULL); + } + else + { + *b_out = malloc(2 * sizeof(int)); + __CPROVER_assume(*b_out != NULL); + *c_out = *b_out; // not separated, expect failure + } + **b_out = a[0]; + **c_out = a[1]; +} + +int main() +{ + int *a, **b_out, **c_out; + foo(a, b_out, c_out); +} diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/test.desc b/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/test.desc new file mode 100644 index 00000000000..94dffe4f960 --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/test.desc @@ -0,0 +1,12 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when __CPROVER_is_fresh is asserted in ensures clauses +in contract checking mode, it detects byte interval separation failure +within the same object. diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/main.c b/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/main.c new file mode 100644 index 00000000000..9c9c71ad9f0 --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/main.c @@ -0,0 +1,37 @@ +#include +int nondet_int(); + +void foo(int *a, int **b_out, int **c_out) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(a, 2*sizeof(int))) +__CPROVER_requires(__CPROVER_is_fresh(b_out, sizeof(int*))) +__CPROVER_requires(__CPROVER_is_fresh(c_out, sizeof(int*))) +__CPROVER_ensures(__CPROVER_is_fresh(*b_out, sizeof(int))) +__CPROVER_ensures(__CPROVER_is_fresh(*c_out, sizeof(int))) +__CPROVER_assigns(*b_out, *c_out) +__CPROVER_ensures(**b_out == a[0]) +__CPROVER_ensures(**c_out == a[1]) +// clang-format on +{ + if(nondet_int()) + { + *b_out = malloc(sizeof(int)); + __CPROVER_assume(*b_out != NULL); + *c_out = malloc(sizeof(int)); + __CPROVER_assume(*c_out != NULL); + } + else + { + *b_out = malloc(2 * sizeof(int)); + __CPROVER_assume(*b_out != NULL); + *c_out = *b_out + 1; + } + **b_out = a[0]; + **c_out = a[1]; +} + +int main() +{ + int *a, **b_out, **c_out; + foo(a, b_out, c_out); +} diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/test.desc new file mode 100644 index 00000000000..61e39729553 --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/test.desc @@ -0,0 +1,12 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract foo +^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that when __CPROVER_is_fresh is asserted in ensures clauses +in contract checking mode, it allows both objet level separation and byte +interval separation within the same object. diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/main.c b/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/main.c new file mode 100644 index 00000000000..25ef3bd9809 --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/main.c @@ -0,0 +1,36 @@ +#include + +void foo(int *a, int *b) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(a, 3*sizeof(int))) +__CPROVER_requires(__CPROVER_is_fresh(b, 3*sizeof(int))) +__CPROVER_assigns(__CPROVER_object_upto(a, 3*sizeof(int))) +__CPROVER_ensures(a[0] == b[0]) +__CPROVER_ensures(a[1] == b[1]) +__CPROVER_ensures(a[2] == b[2]) +; + +int nondet_int(); + +void bar() +{ + int a[6]; + int b[3]; + // c is either either a slice of `a` that overlaps a[0..2] or `b` + int *c = nondet_int() ? &a[0] + 2: &b[0]; + int old_c0 = c[0]; + int old_c1 = c[1]; + int old_c2 = c[2]; + foo(a, c); // failure of preconditions + __CPROVER_assert(a[0] == c[0], "same value 0"); + __CPROVER_assert(a[1] == c[1], "same value 1"); + __CPROVER_assert(a[2] == c[2], "same value 2"); + __CPROVER_assert(old_c0 == c[0], "unmodified 0"); + __CPROVER_assert(old_c1 == c[1], "unmodified 1"); + __CPROVER_assert(old_c2 == c[2], "unmodified 2"); +} + +int main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/test.desc b/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/test.desc new file mode 100644 index 00000000000..3265d54a864 --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/test.desc @@ -0,0 +1,13 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract bar --replace-call-with-contract foo +^\[bar.assertion.\d+\].* unmodified 0: FAILURE$ +^\[foo.precondition.\d+\].*Check requires clause of contract contract::foo for function foo: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that when __CPROVER_is_fresh is asserted in requires clauses +in contract replacement mode, it detects byte interval separation failure within +the same object. diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/main.c b/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/main.c new file mode 100644 index 00000000000..efd6c7db4de --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/main.c @@ -0,0 +1,36 @@ +#include + +void foo(int *a, int *b) + // clang-format off +__CPROVER_requires(__CPROVER_is_fresh(a, 3*sizeof(int))) +__CPROVER_requires(__CPROVER_is_fresh(b, 3*sizeof(int))) +__CPROVER_assigns(__CPROVER_object_upto(a, 3*sizeof(int))) +__CPROVER_ensures(a[0] == b[0]) +__CPROVER_ensures(a[1] == b[1]) +__CPROVER_ensures(a[2] == b[2]) +; + +int nondet_int(); + +void bar() +{ + int a[6]; + int b[3]; + // c is either either a slice of `a` disjoint from a[0..2] or `b` + int *c = nondet_int() ? &a[0] + 3: &b[0]; + int old_c0 = c[0]; + int old_c1 = c[1]; + int old_c2 = c[2]; + foo(a, c); // success of preconditions + __CPROVER_assert(a[0] == c[0], "same value 0"); + __CPROVER_assert(a[1] == c[1], "same value 1"); + __CPROVER_assert(a[2] == c[2], "same value 2"); + __CPROVER_assert(old_c0 == c[0], "unmodified 0"); + __CPROVER_assert(old_c1 == c[1], "unmodified 1"); + __CPROVER_assert(old_c2 == c[2], "unmodified 2"); +} + +int main() +{ + bar(); +} diff --git a/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/test.desc new file mode 100644 index 00000000000..05a0e95438b --- /dev/null +++ b/regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/test.desc @@ -0,0 +1,11 @@ +CORE dfcc-only +main.c +--dfcc main --enforce-contract bar --replace-call-with-contract foo _ --z3 --slice-formula +^\[foo.precondition.\d+\].*Check requires clause of contract contract::foo for function foo: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that when __CPROVER_is_fresh in preconditions replacement checks +succeed when separation and size are as expected. diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 00370455016..0087501ed6c 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -72,13 +72,7 @@ typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t; /// pointer equals, pointer_in_range_dfcc, pointer_is_fresh, obeys_contract. typedef struct { - /// \brief Nondet variable ranging over the set of objects allocated - /// by __CPROVER_contracts_is_fresh. Used to check separation constraints - /// in __CPROVER_contracts_is_fresh. - void *fresh_ptr; - /// \brief Nondet variable ranging over the set of locations storing - /// pointers on which predicates were assumed/asserted. Used to ensure - /// that at most one predicate is assumed per pointer. + __CPROVER_contracts_car_t fresh_car; void **ptr_pred; } __CPROVER_contracts_ptr_pred_ctx_t; @@ -419,7 +413,8 @@ void __CPROVER_contracts_ptr_pred_ctx_init( __CPROVER_contracts_ptr_pred_ctx_ptr_t set) { __CPROVER_HIDE:; - set->fresh_ptr = (void *)0; + set->fresh_car = (__CPROVER_contracts_car_t){ + .is_writable = 0, .size = 0, .lb = (void *)0, .ub = (void *)0}; set->ptr_pred = (void **)0; } @@ -1345,10 +1340,10 @@ __CPROVER_HIDE:; __VERIFIER_nondet___CPROVER_bool() ? elem : write_set->linked_ptr_pred_ctx->ptr_pred; - write_set->linked_ptr_pred_ctx->fresh_ptr = + write_set->linked_ptr_pred_ctx->fresh_car = __VERIFIER_nondet___CPROVER_bool() - ? ptr - : write_set->linked_ptr_pred_ctx->fresh_ptr; + ? __CPROVER_contracts_car_create(ptr, size) + : write_set->linked_ptr_pred_ctx->fresh_car; // record the object size for non-determistic bounds checking __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool(); @@ -1403,10 +1398,10 @@ __CPROVER_HIDE:; __VERIFIER_nondet___CPROVER_bool() ? elem : write_set->linked_ptr_pred_ctx->ptr_pred; - write_set->linked_ptr_pred_ctx->fresh_ptr = + write_set->linked_ptr_pred_ctx->fresh_car = __VERIFIER_nondet___CPROVER_bool() - ? ptr - : write_set->linked_ptr_pred_ctx->fresh_ptr; + ? __CPROVER_contracts_car_create(ptr, size) + : write_set->linked_ptr_pred_ctx->fresh_car; // record the object size for non-determistic bounds checking __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool(); @@ -1440,11 +1435,15 @@ __CPROVER_HIDE:; (write_set->assume_ensures_ctx == 0), "only one context flag at a time"); #endif + // check separation void *ptr = *elem; + __CPROVER_contracts_car_t car = __CPROVER_contracts_car_create(ptr, size); + __CPROVER_contracts_car_t fresh_car = + write_set->linked_ptr_pred_ctx->fresh_car; if( - ptr != (void *)0 && - !__CPROVER_same_object(write_set->linked_ptr_pred_ctx->fresh_ptr, ptr) && - __CPROVER_r_ok(ptr, size)) + ptr != (void *)0 && __CPROVER_r_ok(ptr, size) && + (!__CPROVER_same_object(car.lb, fresh_car.lb) || + (car.ub <= fresh_car.lb) || (fresh_car.ub <= car.lb))) { __CPROVER_assert( write_set->linked_ptr_pred_ctx->ptr_pred != elem, @@ -1454,10 +1453,10 @@ __CPROVER_HIDE:; __VERIFIER_nondet___CPROVER_bool() ? elem : write_set->linked_ptr_pred_ctx->ptr_pred; - write_set->linked_ptr_pred_ctx->fresh_ptr = + write_set->linked_ptr_pred_ctx->fresh_car = __VERIFIER_nondet___CPROVER_bool() - ? ptr - : write_set->linked_ptr_pred_ctx->fresh_ptr; + ? car + : write_set->linked_ptr_pred_ctx->fresh_car; return 1; } return 0;