Skip to content

Commit 8fc0f1d

Browse files
author
Remi Delmas
committed
Add new __CPROVER_pointer_equals(p, q) predicate
Meant to replace `p == q in contract clauses, works as a hook to override equality behaviour in assume contexts to make it constructive.
1 parent f65790d commit 8fc0f1d

File tree

25 files changed

+606
-4
lines changed

25 files changed

+606
-4
lines changed

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

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
void foo(int *x, int *y)
2+
// clang-format off
3+
__CPROVER_requires(__CPROVER_is_fresh(x, sizeof(int)))
4+
__CPROVER_requires(__CPROVER_pointer_equals(y, x) || 1)
5+
__CPROVER_assigns(*y)
6+
// clang-format on
7+
{
8+
*y = 0;
9+
}
10+
11+
void main()
12+
{
13+
int *x;
14+
int *y;
15+
foo(x, y);
16+
}

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

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
5+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: (UNKNOWN|FAILURE)$
6+
^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: (UNKNOWN|FAILURE)$
7+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: (UNKNOWN|FAILURE)$
8+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: (UNKNOWN|FAILURE)$
9+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: (UNKNOWN|FAILURE)$
10+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: (UNKNOWN|FAILURE)$
11+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: (UNKNOWN|FAILURE)$
12+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: (UNKNOWN|FAILURE)$
13+
^EXIT=10$
14+
^SIGNAL=0$
15+
^VERIFICATION FAILED$
16+
--
17+
--
18+
This test checks that when `__CPROVER_pointer_equals` is used in disjunctions,
19+
the program accepts models where `__CPROVER_pointer_equals` evaluates to
20+
false and the target pointer remains invalid.

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

+34
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
#include <stdlib.h>
2+
void foo(int *a, int *x, int *y)
3+
// clang-format off
4+
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(int)))
5+
__CPROVER_requires(
6+
(__CPROVER_pointer_equals(x,a) && y == NULL) ||
7+
(x == NULL && __CPROVER_pointer_equals(y,a))
8+
)
9+
__CPROVER_assigns(y == NULL: *x)
10+
__CPROVER_assigns(x == NULL: *y)
11+
// clang-format on
12+
{
13+
if(y == NULL)
14+
{
15+
assert(0);
16+
assert(__CPROVER_same_object(a, x));
17+
*x = 0;
18+
}
19+
else
20+
{
21+
assert(0);
22+
assert(x == NULL);
23+
assert(__CPROVER_same_object(a, y));
24+
*y = 0;
25+
}
26+
}
27+
28+
void main()
29+
{
30+
int *a;
31+
int *x;
32+
int *y;
33+
foo(a, x, y);
34+
}

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

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --enforce-contract foo
4+
^\[foo.assertion.\d+\] line 15 assertion 0: FAILURE$
5+
^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$
6+
^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
7+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$
8+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$
9+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$
10+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$
11+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$
12+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$
13+
^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$
14+
^\[foo.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$
15+
^\[foo.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$
16+
^\[foo.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
17+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$
18+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$
19+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$
20+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$
21+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$
22+
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$
23+
^EXIT=10$
24+
^SIGNAL=0$
25+
^VERIFICATION FAILED$
26+
--
27+
--
28+
Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts.
29+
The precondition of `foo` describes a disjunction of cases, either `x` equals `a` and `y` is null,
30+
or `x` is null and `y` equals `a`. The function `foo` branches on `y == NULL`.
31+
The test suceeds if the two `assert(0)` in `foo` are falsifiable, which which shows
32+
that both cases of the disjunction expressed in the requires clause are reachable.

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

+28
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
2+
typedef struct
3+
{
4+
int *a;
5+
int *x;
6+
} ret_t;
7+
8+
ret_t foo()
9+
// clang-format off
10+
__CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, sizeof(int)))
11+
__CPROVER_ensures(
12+
__CPROVER_pointer_equals(
13+
__CPROVER_return_value.x,
14+
__CPROVER_return_value.a) || 1)
15+
// clang-format on
16+
;
17+
18+
void bar()
19+
{
20+
ret_t ret = foo();
21+
int *x = ret.x;
22+
*x = 0; //expected to fail
23+
}
24+
25+
void main()
26+
{
27+
bar();
28+
}

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

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --replace-call-with-contract foo
4+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: (UNKNOWN|FAILURE)$
5+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: (UNKNOWN|FAILURE)$
6+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: (UNKNOWN|FAILURE)$
7+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: (UNKNOWN|FAILURE)$
8+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: (UNKNOWN|FAILURE)$
9+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: (UNKNOWN|FAILURE)$
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
^VERIFICATION FAILED$
13+
--
14+
--
15+
This test checks that when `__CPROVER_pointer_equals` is used in disjunctions,
16+
the program accepts models where `__CPROVER_pointer_equals` evaluates to
17+
false and the target pointer remains invalid.

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

+49
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
#include <stdlib.h>
2+
typedef struct
3+
{
4+
int *a;
5+
int *x;
6+
int *y;
7+
} ret_t;
8+
9+
ret_t foo()
10+
// clang-format off
11+
__CPROVER_ensures(__CPROVER_is_fresh(__CPROVER_return_value.a, sizeof(int)))
12+
__CPROVER_ensures((
13+
__CPROVER_pointer_equals(
14+
__CPROVER_return_value.x,
15+
__CPROVER_return_value.a) &&
16+
__CPROVER_return_value.y == NULL
17+
) || (
18+
__CPROVER_return_value.x == NULL &&
19+
__CPROVER_pointer_equals(
20+
__CPROVER_return_value.y,
21+
__CPROVER_return_value.a)))
22+
// clang-format on
23+
;
24+
25+
void bar()
26+
{
27+
ret_t ret = foo();
28+
int *a = ret.a;
29+
int *x = ret.x;
30+
int *y = ret.y;
31+
if(y == NULL)
32+
{
33+
assert(0);
34+
assert(__CPROVER_same_object(x, a));
35+
*x = 0;
36+
}
37+
else
38+
{
39+
assert(0);
40+
assert(x == NULL);
41+
assert(__CPROVER_same_object(y, a));
42+
*y = 0;
43+
}
44+
}
45+
46+
void main()
47+
{
48+
bar();
49+
}

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

+32
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
CORE dfcc-only
2+
main.c
3+
--dfcc main --replace-call-with-contract foo
4+
^\[bar.assertion.\d+\] line 33 assertion 0: FAILURE$
5+
^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)x\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
6+
^\[bar.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
7+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: SUCCESS$
8+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: SUCCESS$
9+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: SUCCESS$
10+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: SUCCESS$
11+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: SUCCESS$
12+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: SUCCESS$
13+
^\[bar.assertion.\d+\] line 39 assertion 0: FAILURE$
14+
^\[bar.assertion.\d+\] line \d+ assertion x == \(\(.*\)NULL\): SUCCESS$
15+
^\[bar.assertion.\d+\] line \d+ assertion __CPROVER_POINTER_OBJECT\(\(.*\)y\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
16+
^\[bar.assigns.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
17+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*y: SUCCESS$
18+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*y: SUCCESS$
19+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*y: SUCCESS$
20+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*y: SUCCESS$
21+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*y: SUCCESS$
22+
^\[bar.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*y: SUCCESS$
23+
^EXIT=10$
24+
^SIGNAL=0$
25+
^VERIFICATION FAILED$
26+
--
27+
--
28+
Illustrates the behaviour of `__CPROVER_pointer_equals` under disjunctions in assume contexts.
29+
The postcondition of `foo` describes a disjunction of cases: either `x` equals `a` and `y` is null,
30+
or `x` is null and `y` equals `a`. The function `bar` branches on `y == NULL`.
31+
The test succeeds if the two `assert(0)` are falsifiable, which which shows that
32+
both cases of the disjunction expressed in the ensures clause of `foo` are reachable.

‎src/ansi-c/c_typecheck_expr.cpp

+13-1
Original file line numberDiff line numberDiff line change
@@ -2591,7 +2591,19 @@ exprt c_typecheck_baset::do_special_functions(
25912591

25922592
const irep_idt &identifier=to_symbol_expr(f_op).get_identifier();
25932593

2594-
if(identifier == CPROVER_PREFIX "is_fresh")
2594+
if(identifier == CPROVER_PREFIX "pointer_equals")
2595+
{
2596+
if(expr.arguments().size() != 2)
2597+
{
2598+
error().source_location = f_op.source_location();
2599+
error() << CPROVER_PREFIX "pointer_equals expects two operands; "
2600+
<< expr.arguments().size() << "provided." << eom;
2601+
throw 0;
2602+
}
2603+
typecheck_function_call_arguments(expr);
2604+
return nil_exprt();
2605+
}
2606+
else if(identifier == CPROVER_PREFIX "is_fresh")
25952607
{
25962608
if(expr.arguments().size() != 2)
25972609
{

‎src/ansi-c/cprover_builtin_headers.h

+1
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ void __CPROVER_fence(const char *kind, ...);
4444
// contract-related functions
4545
__CPROVER_bool __CPROVER_is_freeable(const void *mem);
4646
__CPROVER_bool __CPROVER_was_freed(const void *mem);
47+
__CPROVER_bool __CPROVER_pointer_equals(void *p, void *q);
4748
__CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size);
4849
__CPROVER_bool __CPROVER_obeys_contract(void (*)(void), void (*)(void));
4950
// same as pointer_in_range with experimental support in contracts

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

+56
Original file line numberDiff line numberDiff line change
@@ -1162,6 +1162,62 @@ void __CPROVER_contracts_make_invalid_pointer(void **ptr)
11621162
#endif
11631163
}
11641164

1165+
/// \brief Implementation of the `pointer_equals` front-end predicate.
1166+
///
1167+
/// \param ptr1 First argument of the `pointer_equals` predicate
1168+
/// \param ptr2 Second argument of the `pointer_equals` predicate
1169+
/// \param write_set Write set which conveys the invocation context
1170+
/// (requires/ensures clause, assert/assume context);
1171+
///
1172+
/// \details The behaviour is as follows:
1173+
/// When \p set->assume_requires_ctx or \p set->assume_ensures_ctx is `true`,
1174+
/// the predicate nondeterministically invalidates `*ptr1` and returns `false`,
1175+
/// or checks that `ptr2` is either NULL or valid, and assigns `*ptr1` to `ptr2`.
1176+
/// When \p set->assert_requires_ctx or \p set->assert_ensures_ctx is `true`,
1177+
/// the predicate checks that both `*ptr1` and `ptr2` are either NULL or valid,
1178+
/// and returns the value of (*ptr1 == ptr2).
1179+
__CPROVER_bool __CPROVER_contracts_pointer_equals(
1180+
void **ptr1,
1181+
void *ptr2,
1182+
__CPROVER_contracts_write_set_ptr_t write_set)
1183+
{
1184+
__CPROVER_HIDE:;
1185+
__CPROVER_assert(
1186+
(write_set != 0) & ((write_set->assume_requires_ctx == 1) |
1187+
(write_set->assert_requires_ctx == 1) |
1188+
(write_set->assume_ensures_ctx == 1) |
1189+
(write_set->assert_ensures_ctx == 1)),
1190+
"__CPROVER_is_fresh is used only in requires or ensures clauses");
1191+
#ifdef __CPROVER_DFCC_DEBUG_LIB
1192+
__CPROVER_assert(
1193+
__CPROVER_rw_ok(write_set, sizeof(__CPROVER_contracts_write_set_t)),
1194+
"set readable");
1195+
#endif
1196+
if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
1197+
{
1198+
if(__VERIFIER_nondet___CPROVER_bool())
1199+
{
1200+
__CPROVER_contracts_make_invalid_pointer(ptr1);
1201+
return 0;
1202+
}
1203+
__CPROVER_assert(
1204+
(ptr2 == 0) || __CPROVER_r_ok(ptr2, 0),
1205+
"pointer_equals is only called with valid pointers");
1206+
*ptr1 = ptr2;
1207+
return 1;
1208+
}
1209+
else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
1210+
{
1211+
void *derefd = *ptr1;
1212+
__CPROVER_assert(
1213+
(derefd == 0) || __CPROVER_r_ok(derefd, 0),
1214+
"pointer_equals is only called with valid pointers");
1215+
__CPROVER_assert(
1216+
(ptr2 == 0) || __CPROVER_r_ok(ptr2, 0),
1217+
"pointer_equals is only called with valid pointers");
1218+
return derefd == ptr2;
1219+
}
1220+
}
11651221

11661222
/// \brief Implementation of the `is_fresh` front-end predicate.
11671223
///

‎src/goto-instrument/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ SRC = accelerate/accelerate.cpp \
2929
contracts/dynamic-frames/dfcc_instrument_loop.cpp \
3030
contracts/dynamic-frames/dfcc_library.cpp \
3131
contracts/dynamic-frames/dfcc_is_cprover_symbol.cpp \
32+
contracts/dynamic-frames/dfcc_pointer_equals.cpp \
3233
contracts/dynamic-frames/dfcc_is_fresh.cpp \
3334
contracts/dynamic-frames/dfcc_pointer_in_range.cpp \
3435
contracts/dynamic-frames/dfcc_is_freeable.cpp \

‎src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md

+1
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@ Each of these translation passes is implemented in a specific class:
2929
@ref dfcc_instrumentt | Implements @ref contracts-dev-spec-dfcc for @ref goto_functiont, @ref goto_programt, or subsequences of instructions of @ref goto_programt
3030
@ref dfcc_is_fresht | Implements @ref contracts-dev-spec-is-fresh
3131
@ref dfcc_pointer_in_ranget | Implements @ref contracts-dev-spec-pointer-in-range
32+
@ref dfcc_pointer_equalst | Implements @ref contracts-dev-spec-pointer-equals
3233
@ref dfcc_lift_memory_predicatest | Implements @ref contracts-dev-spec-memory-predicates-rewriting
3334
@ref dfcc_is_freeablet | Implements @ref contracts-dev-spec-is-freeable
3435
@ref dfcc_obeys_contractt | Implements @ref contracts-dev-spec-obeys-contract

‎src/goto-instrument/contracts/doc/developer/contracts-dev-spec-dfcc-instrument.md

+3
Original file line numberDiff line numberDiff line change
@@ -174,6 +174,9 @@ Calls to `__CPROVER_obeys_contract` are rewritten as described in
174174
Calls to `__CPROVER_pointer_in_range_dfcc` are rewritten as described in
175175
@subpage contracts-dev-spec-pointer-in-range
176176
177+
Calls to `__CPROVER_pointer_equals` are rewritten as described in
178+
@subpage contracts-dev-spec-pointer-equals
179+
177180
For all other function or function pointer calls, we proceed as follows.
178181
179182
If the function call has an LHS (i.e. its result is assigned to a return value

‎src/goto-instrument/contracts/doc/developer/contracts-dev-spec-memory-predicates-rewriting.md

+3
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,9 @@ The C extensions for contract specification provide three pointer-related memory
88
predicates:
99

1010
```c
11+
// Holds iff ptr1 and ptr2 are both either null or valid and are equal.
12+
__CPROVER_bool __CPROVER_pointer_equals(void *ptr1, void* ptr2);
13+
1114
// Holds iff ptr is pointing to an object distinct to all objects pointed to by
1215
// other __CPROVER_is_fresh occurrences in the contract's pre and post conditions
1316
__CPROVER_bool __CPROVER_is_fresh(void *ptr, size_t size);

‎src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-equals.md

+25
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
# Rewriting Calls to the __CPROVER_pointer_equals Predicate {#contracts-dev-spec-pointer-equals}
2+
3+
Back to top @ref contracts-dev-spec
4+
5+
@tableofcontents
6+
7+
In goto programs encoding pre or post conditions (generated from the contract
8+
clauses) and in all user-defined functions, we simply replace calls to
9+
`__CPROVER_pointer_equals` with calls to the library implementation.
10+
11+
```c
12+
__CPROVER_contracts_pointer_equals(
13+
void **ptr1,
14+
void *ptr2,
15+
__CPROVER_contracts_write_set_ptr_t write_set);
16+
```
17+
18+
This function implements the `__CPROVER_pointer_equals` behaviour in all
19+
possible contexts (contract checking vs replacement, requires vs ensures clause
20+
context, as described by the flags carried by the write set parameter).
21+
22+
---
23+
Prev | Next
24+
:-----|:------
25+
@ref contracts-dev | @ref contracts-dev-spec-reminder

‎src/goto-instrument/contracts/doc/developer/contracts-dev-spec-pointer-in-range.md

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,4 +23,4 @@ context, as described by the flags carried by the write set parameter).
2323
---
2424
Prev | Next
2525
:-----|:------
26-
@ref contracts-dev | @ref contracts-dev-spec-reminder
26+
@ref contracts-dev | @ref contracts-dev-spec-pointer-equals

0 commit comments

Comments
 (0)