Skip to content

Commit 9bade97

Browse files
tautschnigtautschnig
authored
Merge pull request #8603 from remi-delmas-3000/weaken-is-fresh-assert
CONTRACTS: is_fresh now tracks separation at the byte level instead of whole objects
2 parents 29c588c + d4a1c6d commit 9bade97

File tree

10 files changed

+214
-23
lines changed

10 files changed

+214
-23
lines changed

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

+1-3
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,7 @@
11
CORE dfcc-only
22
main.c
3-
--no-malloc-may-fail --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: FAILURE$
3+
--no-malloc-may-fail --dfcc main --enforce-contract foo
54
^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$
6-
^\*\* 2 of \d+ failed
75
^EXIT=10$
86
^SIGNAL=0$
97
^VERIFICATION FAILED$

‎regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/main.c

+37
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
#include <stdlib.h>
2+
int nondet_int();
3+
4+
void foo(int *a, int **b_out, int **c_out)
5+
// clang-format off
6+
__CPROVER_requires(__CPROVER_is_fresh(a, 2*sizeof(int)))
7+
__CPROVER_requires(__CPROVER_is_fresh(b_out, sizeof(int*)))
8+
__CPROVER_requires(__CPROVER_is_fresh(c_out, sizeof(int*)))
9+
__CPROVER_ensures(__CPROVER_is_fresh(*b_out, sizeof(int)))
10+
__CPROVER_ensures(__CPROVER_is_fresh(*c_out, sizeof(int)))
11+
__CPROVER_assigns(*b_out, *c_out)
12+
__CPROVER_ensures(**b_out == a[0])
13+
__CPROVER_ensures(**c_out == a[1])
14+
// clang-format on
15+
{
16+
if(nondet_int())
17+
{
18+
*b_out = malloc(sizeof(int));
19+
__CPROVER_assume(*b_out != NULL);
20+
*c_out = malloc(sizeof(int));
21+
__CPROVER_assume(*c_out != NULL);
22+
}
23+
else
24+
{
25+
*b_out = malloc(2 * sizeof(int));
26+
__CPROVER_assume(*b_out != NULL);
27+
*c_out = *b_out; // not separated, expect failure
28+
}
29+
**b_out = a[0];
30+
**c_out = a[1];
31+
}
32+
33+
int main()
34+
{
35+
int *a, **b_out, **c_out;
36+
foo(a, b_out, c_out);
37+
}

‎regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_fail/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^VERIFICATION FAILED$
8+
--
9+
--
10+
This test checks that when __CPROVER_is_fresh is asserted in ensures clauses
11+
in contract checking mode, it detects byte interval separation failure
12+
within the same object.

‎regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/main.c

+37
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
#include <stdlib.h>
2+
int nondet_int();
3+
4+
void foo(int *a, int **b_out, int **c_out)
5+
// clang-format off
6+
__CPROVER_requires(__CPROVER_is_fresh(a, 2*sizeof(int)))
7+
__CPROVER_requires(__CPROVER_is_fresh(b_out, sizeof(int*)))
8+
__CPROVER_requires(__CPROVER_is_fresh(c_out, sizeof(int*)))
9+
__CPROVER_ensures(__CPROVER_is_fresh(*b_out, sizeof(int)))
10+
__CPROVER_ensures(__CPROVER_is_fresh(*c_out, sizeof(int)))
11+
__CPROVER_assigns(*b_out, *c_out)
12+
__CPROVER_ensures(**b_out == a[0])
13+
__CPROVER_ensures(**c_out == a[1])
14+
// clang-format on
15+
{
16+
if(nondet_int())
17+
{
18+
*b_out = malloc(sizeof(int));
19+
__CPROVER_assume(*b_out != NULL);
20+
*c_out = malloc(sizeof(int));
21+
__CPROVER_assume(*c_out != NULL);
22+
}
23+
else
24+
{
25+
*b_out = malloc(2 * sizeof(int));
26+
__CPROVER_assume(*b_out != NULL);
27+
*c_out = *b_out + 1;
28+
}
29+
**b_out = a[0];
30+
**c_out = a[1];
31+
}
32+
33+
int main()
34+
{
35+
int *a, **b_out, **c_out;
36+
foo(a, b_out, c_out);
37+
}

‎regression/contracts-dfcc/test_is_fresh_weak_assert_ensures_pass/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[foo.postcondition.\d+\].*Check ensures clause of contract contract::foo for function foo: SUCCESS$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--
10+
This test checks that when __CPROVER_is_fresh is asserted in ensures clauses
11+
in contract checking mode, it allows both objet level separation and byte
12+
interval separation within the same object.

‎regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/main.c

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#include <stdlib.h>
2+
3+
void foo(int *a, int *b)
4+
// clang-format off
5+
__CPROVER_requires(__CPROVER_is_fresh(a, 3*sizeof(int)))
6+
__CPROVER_requires(__CPROVER_is_fresh(b, 3*sizeof(int)))
7+
__CPROVER_assigns(__CPROVER_object_upto(a, 3*sizeof(int)))
8+
__CPROVER_ensures(a[0] == b[0])
9+
__CPROVER_ensures(a[1] == b[1])
10+
__CPROVER_ensures(a[2] == b[2])
11+
;
12+
13+
int nondet_int();
14+
15+
void bar()
16+
{
17+
int a[6];
18+
int b[3];
19+
// c is either either a slice of `a` that overlaps a[0..2] or `b`
20+
int *c = nondet_int() ? &a[0] + 2: &b[0];
21+
int old_c0 = c[0];
22+
int old_c1 = c[1];
23+
int old_c2 = c[2];
24+
foo(a, c); // failure of preconditions
25+
__CPROVER_assert(a[0] == c[0], "same value 0");
26+
__CPROVER_assert(a[1] == c[1], "same value 1");
27+
__CPROVER_assert(a[2] == c[2], "same value 2");
28+
__CPROVER_assert(old_c0 == c[0], "unmodified 0");
29+
__CPROVER_assert(old_c1 == c[1], "unmodified 1");
30+
__CPROVER_assert(old_c2 == c[2], "unmodified 2");
31+
}
32+
33+
int main()
34+
{
35+
bar();
36+
}

‎regression/contracts-dfcc/test_is_fresh_weak_assert_requires_fail/test.desc

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract bar --replace-call-with-contract foo
4+
^\[bar.assertion.\d+\].* unmodified 0: FAILURE$
5+
^\[foo.precondition.\d+\].*Check requires clause of contract contract::foo for function foo: FAILURE$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
^VERIFICATION FAILED$
9+
--
10+
--
11+
This test checks that when __CPROVER_is_fresh is asserted in requires clauses
12+
in contract replacement mode, it detects byte interval separation failure within
13+
the same object.

‎regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/main.c

+36
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
#include <stdlib.h>
2+
3+
void foo(int *a, int *b)
4+
// clang-format off
5+
__CPROVER_requires(__CPROVER_is_fresh(a, 3*sizeof(int)))
6+
__CPROVER_requires(__CPROVER_is_fresh(b, 3*sizeof(int)))
7+
__CPROVER_assigns(__CPROVER_object_upto(a, 3*sizeof(int)))
8+
__CPROVER_ensures(a[0] == b[0])
9+
__CPROVER_ensures(a[1] == b[1])
10+
__CPROVER_ensures(a[2] == b[2])
11+
;
12+
13+
int nondet_int();
14+
15+
void bar()
16+
{
17+
int a[6];
18+
int b[3];
19+
// c is either either a slice of `a` disjoint from a[0..2] or `b`
20+
int *c = nondet_int() ? &a[0] + 3: &b[0];
21+
int old_c0 = c[0];
22+
int old_c1 = c[1];
23+
int old_c2 = c[2];
24+
foo(a, c); // success of preconditions
25+
__CPROVER_assert(a[0] == c[0], "same value 0");
26+
__CPROVER_assert(a[1] == c[1], "same value 1");
27+
__CPROVER_assert(a[2] == c[2], "same value 2");
28+
__CPROVER_assert(old_c0 == c[0], "unmodified 0");
29+
__CPROVER_assert(old_c1 == c[1], "unmodified 1");
30+
__CPROVER_assert(old_c2 == c[2], "unmodified 2");
31+
}
32+
33+
int main()
34+
{
35+
bar();
36+
}

‎regression/contracts-dfcc/test_is_fresh_weak_assert_requires_pass/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract bar --replace-call-with-contract foo _ --z3 --slice-formula
4+
^\[foo.precondition.\d+\].*Check requires clause of contract contract::foo for function foo: SUCCESS$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
^VERIFICATION SUCCESSFUL$
8+
--
9+
--
10+
This test checks that when __CPROVER_is_fresh in preconditions replacement checks
11+
succeed when separation and size are as expected.

‎src/ansi-c/library/cprover_contracts.c

+19-20
Original file line numberDiff line numberDiff line change
@@ -72,13 +72,7 @@ typedef __CPROVER_contracts_obj_set_t *__CPROVER_contracts_obj_set_ptr_t;
7272
/// pointer equals, pointer_in_range_dfcc, pointer_is_fresh, obeys_contract.
7373
typedef struct
7474
{
75-
/// \brief Nondet variable ranging over the set of objects allocated
76-
/// by __CPROVER_contracts_is_fresh. Used to check separation constraints
77-
/// in __CPROVER_contracts_is_fresh.
78-
void *fresh_ptr;
79-
/// \brief Nondet variable ranging over the set of locations storing
80-
/// pointers on which predicates were assumed/asserted. Used to ensure
81-
/// that at most one predicate is assumed per pointer.
75+
__CPROVER_contracts_car_t fresh_car;
8276
void **ptr_pred;
8377
} __CPROVER_contracts_ptr_pred_ctx_t;
8478

@@ -419,7 +413,8 @@ void __CPROVER_contracts_ptr_pred_ctx_init(
419413
__CPROVER_contracts_ptr_pred_ctx_ptr_t set)
420414
{
421415
__CPROVER_HIDE:;
422-
set->fresh_ptr = (void *)0;
416+
set->fresh_car = (__CPROVER_contracts_car_t){
417+
.is_writable = 0, .size = 0, .lb = (void *)0, .ub = (void *)0};
423418
set->ptr_pred = (void **)0;
424419
}
425420

@@ -1345,10 +1340,10 @@ __CPROVER_HIDE:;
13451340
__VERIFIER_nondet___CPROVER_bool()
13461341
? elem
13471342
: write_set->linked_ptr_pred_ctx->ptr_pred;
1348-
write_set->linked_ptr_pred_ctx->fresh_ptr =
1343+
write_set->linked_ptr_pred_ctx->fresh_car =
13491344
__VERIFIER_nondet___CPROVER_bool()
1350-
? ptr
1351-
: write_set->linked_ptr_pred_ctx->fresh_ptr;
1345+
? __CPROVER_contracts_car_create(ptr, size)
1346+
: write_set->linked_ptr_pred_ctx->fresh_car;
13521347

13531348
// record the object size for non-determistic bounds checking
13541349
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
@@ -1403,10 +1398,10 @@ __CPROVER_HIDE:;
14031398
__VERIFIER_nondet___CPROVER_bool()
14041399
? elem
14051400
: write_set->linked_ptr_pred_ctx->ptr_pred;
1406-
write_set->linked_ptr_pred_ctx->fresh_ptr =
1401+
write_set->linked_ptr_pred_ctx->fresh_car =
14071402
__VERIFIER_nondet___CPROVER_bool()
1408-
? ptr
1409-
: write_set->linked_ptr_pred_ctx->fresh_ptr;
1403+
? __CPROVER_contracts_car_create(ptr, size)
1404+
: write_set->linked_ptr_pred_ctx->fresh_car;
14101405

14111406
// record the object size for non-determistic bounds checking
14121407
__CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
@@ -1440,11 +1435,15 @@ __CPROVER_HIDE:;
14401435
(write_set->assume_ensures_ctx == 0),
14411436
"only one context flag at a time");
14421437
#endif
1438+
// check separation
14431439
void *ptr = *elem;
1440+
__CPROVER_contracts_car_t car = __CPROVER_contracts_car_create(ptr, size);
1441+
__CPROVER_contracts_car_t fresh_car =
1442+
write_set->linked_ptr_pred_ctx->fresh_car;
14441443
if(
1445-
ptr != (void *)0 &&
1446-
!__CPROVER_same_object(write_set->linked_ptr_pred_ctx->fresh_ptr, ptr) &&
1447-
__CPROVER_r_ok(ptr, size))
1444+
ptr != (void *)0 && __CPROVER_r_ok(ptr, size) &&
1445+
(!__CPROVER_same_object(car.lb, fresh_car.lb) ||
1446+
(car.ub <= fresh_car.lb) || (fresh_car.ub <= car.lb)))
14481447
{
14491448
__CPROVER_assert(
14501449
write_set->linked_ptr_pred_ctx->ptr_pred != elem,
@@ -1454,10 +1453,10 @@ __CPROVER_HIDE:;
14541453
__VERIFIER_nondet___CPROVER_bool()
14551454
? elem
14561455
: write_set->linked_ptr_pred_ctx->ptr_pred;
1457-
write_set->linked_ptr_pred_ctx->fresh_ptr =
1456+
write_set->linked_ptr_pred_ctx->fresh_car =
14581457
__VERIFIER_nondet___CPROVER_bool()
1459-
? ptr
1460-
: write_set->linked_ptr_pred_ctx->fresh_ptr;
1458+
? car
1459+
: write_set->linked_ptr_pred_ctx->fresh_car;
14611460
return 1;
14621461
}
14631462
return 0;

0 commit comments

Comments
 (0)