Skip to content

Commit 1405144

Browse files
author
Remi Delmas
committed
Add new pointer_equals predicate
Havoc to invalid for function contracts
1 parent 958e5ab commit 1405144

29 files changed

+726
-61
lines changed

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

Lines changed: 16 additions & 0 deletions
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

Lines changed: 20 additions & 0 deletions
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: FAILURE$
5+
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
6+
^\[foo.assigns.\d+\] line 8 Check that \*y is assignable: FAILURE$
7+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer NULL in \*y: FAILURE$
8+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer invalid in \*y: UNKNOWN$
9+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: deallocated dynamic object in \*y: FAILURE$
10+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: dead object in \*y: FAILURE$
11+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*y: FAILURE$
12+
^\[foo.pointer_dereference.\d+\] line 8 dereference failure: invalid integer address in \*y: UNKNOWN$
13+
^EXIT=10$
14+
^SIGNAL=0$
15+
^VERIFICATION FAILED$
16+
--
17+
--
18+
This test checks that when `__CPROVER_pointer_in_range_dfcc` is disjunctions,
19+
the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to
20+
false the target pointer of the predicate remains undefined.

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

Lines changed: 34 additions & 0 deletions
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

Lines changed: 32 additions & 0 deletions
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 16 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)x\): SUCCESS$
6+
^\[foo.assigns.\d+\] line 17 Check that \*x is assignable: SUCCESS$
7+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer NULL in \*x: SUCCESS$
8+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer invalid in \*x: SUCCESS$
9+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: deallocated dynamic object in \*x: SUCCESS$
10+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: dead object in \*x: SUCCESS$
11+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: pointer outside object bounds in \*x: SUCCESS$
12+
^\[foo.pointer_dereference.\d+\] line 17 dereference failure: invalid integer address in \*x: SUCCESS$
13+
^\[foo.assertion.\d+\] line 21 assertion 0: FAILURE$
14+
^\[foo.assertion.\d+\] line 22 assertion x == \(\(.*\)NULL\): SUCCESS$
15+
^\[foo.assertion.\d+\] line 23 assertion __CPROVER_POINTER_OBJECT\(\(.*\)a\) == __CPROVER_POINTER_OBJECT\(\(.*\)y\): SUCCESS$
16+
^\[foo.assigns.\d+\] line 24 Check that \*y is assignable: SUCCESS$
17+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer NULL in \*y: SUCCESS$
18+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*y: SUCCESS$
19+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*y: SUCCESS$
20+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*y: SUCCESS$
21+
^\[foo.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*y: SUCCESS$
22+
^\[foo.pointer_dereference.\d+\] line 24 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_in_range_dfcc` under disjunctions in assume contexts.
29+
The precondition of `foo` describes a disjunction of cases, either `x` is in range of `a` and `y` is null,
30+
or `x` is null and `y` is in range of `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

Lines changed: 28 additions & 0 deletions
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

Lines changed: 17 additions & 0 deletions
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 24 dereference failure: pointer NULL in \*x: FAILURE$
5+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer invalid in \*x: UNKNOWN$
6+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: deallocated dynamic object in \*x: FAILURE$
7+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: dead object in \*x: FAILURE$
8+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: pointer outside object bounds in \*x: FAILURE$
9+
^\[bar.pointer_dereference.\d+\] line 24 dereference failure: invalid integer address in \*x: UNKNOWN$
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
^VERIFICATION FAILED$
13+
--
14+
--
15+
This test checks that when `__CPROVER_pointer_in_range_dfcc` is disjunctions,
16+
the program accepts models where `__CPROVER_pointer_in_range_dfcc` evaluates to
17+
false the target pointer remains undefined.

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

Lines changed: 49 additions & 0 deletions
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

Lines changed: 32 additions & 0 deletions
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 35 assertion 0: FAILURE$
5+
^\[bar.assertion.\d+\] line 36 assertion __CPROVER_POINTER_OBJECT\(\(.*\)x\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
6+
^\[bar.assigns.\d+\] line 37 Check that \*x is assignable: SUCCESS$
7+
^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer NULL in \*x: SUCCESS$
8+
^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer invalid in \*x: SUCCESS$
9+
^\[bar.pointer_dereference.\d+\] line 37 dereference failure: deallocated dynamic object in \*x: SUCCESS$
10+
^\[bar.pointer_dereference.\d+\] line 37 dereference failure: dead object in \*x: SUCCESS$
11+
^\[bar.pointer_dereference.\d+\] line 37 dereference failure: pointer outside object bounds in \*x: SUCCESS$
12+
^\[bar.pointer_dereference.\d+\] line 37 dereference failure: invalid integer address in \*x: SUCCESS$
13+
^\[bar.assertion.\d+\] line 41 assertion 0: FAILURE$
14+
^\[bar.assertion.\d+\] line 42 assertion x == \(\(.*\)NULL\): SUCCESS$
15+
^\[bar.assertion.\d+\] line 43 assertion __CPROVER_POINTER_OBJECT\(\(.*\)y\) == __CPROVER_POINTER_OBJECT\(\(.*\)a\): SUCCESS$
16+
^\[bar.assigns.\d+\] line 44 Check that \*y is assignable: SUCCESS$
17+
^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer NULL in \*y: SUCCESS$
18+
^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer invalid in \*y: SUCCESS$
19+
^\[bar.pointer_dereference.\d+\] line 44 dereference failure: deallocated dynamic object in \*y: SUCCESS$
20+
^\[bar.pointer_dereference.\d+\] line 44 dereference failure: dead object in \*y: SUCCESS$
21+
^\[bar.pointer_dereference.\d+\] line 44 dereference failure: pointer outside object bounds in \*y: SUCCESS$
22+
^\[bar.pointer_dereference.\d+\] line 44 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_in_range` under disjunctions in assume contexts.
29+
The postcondition of `foo` describes a disjunction of cases: either `x` is in range of `a` and `y` is null,
30+
or `x` is null and `y` is in range of `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

Lines changed: 13 additions & 1 deletion
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

Lines changed: 1 addition & 0 deletions
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

0 commit comments

Comments
 (0)