Skip to content

Commit e913535

Browse files
tautschnigtautschnig
authored
Merge pull request #6893 from diffblue/unsigned_pointer_offset
make pointer_offset_exprt unsigned
2 parents fb65095 + 7cb83c1 commit e913535

File tree

24 files changed

+229
-115
lines changed

24 files changed

+229
-115
lines changed

‎regression/cbmc-incr-smt2/pointers-conversions/byte_update.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Assumption:
1010
file byte_update\.c line \d+ function main
1111
offset >= 0u && offset < 4u
1212
State \d+ file byte_update\.c function main line \d+ thread \d+
13-
byte_extract_little_endian\(x, \(signed long( long)? int\)offset, uint8_t\)=1 \(00000001\)
13+
byte_extract_little_endian\(x, \(.*\)offset, uint8_t\)=1 \(00000001\)
1414
Violated property:
1515
file byte_update.c function main line \d+ thread \d+
1616
assertion x != 256u

‎regression/cbmc-library/free-01/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--pointer-check --bounds-check --stop-on-fail
4-
free argument must be (NULL or valid pointer|dynamic object)
4+
free argument (must be (NULL or valid pointer|dynamic object)|has offset zero)
55
^EXIT=10$
66
^SIGNAL=0$
77
^VERIFICATION FAILED$

‎regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
test.c
33
--string-abstraction --show-goto-functions
4-
ASSIGN strlen#return_value := cast\(cast\(\*strlen::s::s#str\.length, signedbv\[.*\]\) - pointer_offset\(strlen::s\), unsignedbv\[.*\]\)
4+
ASSIGN strlen#return_value := \*strlen::s::s#str\.length - pointer_offset\(strlen::s\)
55
^EXIT=0$
66
^SIGNAL=0$
77
--

‎regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33
--no-simplify --no-propagation
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE
6+
\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: SUCCESS
77
\[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE
88
--
99
^warning: ignoring
1010
--
11-
Check that both positive and negative offsets can be chosen for uninitialized
12-
pointers. We use --no-simplify and --no-propagation to ensure that the case is
13-
not solved by the constant propagation and thus tests the constraint encoding.
11+
Check that positive offsets can be chosen for uninitialized pointers. We
12+
use --no-simplify and --no-propagation to ensure that the case is not solved
13+
by the constant propagation and thus tests the constraint encoding.

‎regression/cbmc-primitives/pointer-offset-01/test.desc

+6-8
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,13 @@ main.c
33

44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE
6+
\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: SUCCESS
77
\[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE
88
--
99
^warning: ignoring
1010
--
11-
For uninitialised pointers, CBMC chooses a nondeterministic value (though no memory
12-
is allocated). Since the offset of pointers is signed, negative offsets should be
13-
able to be chosen (along with positive ones) non-deterministically.
14-
`__CPROVER_POINTER_OFFSET` is the CBMC primitive that gets the pointer offset
15-
from the base address of the object. This test guards this, and especially
16-
against the case where we could only observe some cases where offsets were only
17-
positive (in some CI configurations, for instance).
11+
For uninitialised pointers, CBMC chooses a nondeterministic value (though no
12+
memory is allocated). Since the offset of pointers is unsigned, negative
13+
offsets cannot be chosen. `__CPROVER_POINTER_OFFSET` is the CBMC primitive
14+
that gets the pointer offset from the base address of the object. This test
15+
guards this.

‎regression/cbmc/address_space_size_limit3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE thorough-smt-backend
22
main.i
3-
--32 --little-endian --object-bits 25 --pointer-check
3+
--32 --little-endian --object-bits 26 --pointer-check
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

‎regression/cbmc/memory_allocation2/test.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ main.c
33
--bounds-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$
7-
^\[main\.array_bounds\.[67]\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$
8-
^\*\* 1 of 6 failed
6+
^\[main\.array_bounds\.[1-2]\] .*: SUCCESS$
7+
^\[main\.array_bounds\.3\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$
8+
^\*\* 1 of 3 failed
99
^VERIFICATION FAILED$
1010
--
1111
^warning: ignoring

‎regression/cbmc/pointer-offset-01/main.c

+38
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
int main(void)
5+
{
6+
size_t size;
7+
size_t max_malloc_size = __CPROVER_max_malloc_size;
8+
__CPROVER_assume(0 <= size && size <= max_malloc_size);
9+
char *lb = malloc(size);
10+
size_t offset_lb = __CPROVER_POINTER_OFFSET(lb);
11+
size_t object_lb = __CPROVER_POINTER_OBJECT(lb);
12+
13+
char *ub = lb + size;
14+
size_t offset_ub = __CPROVER_POINTER_OFFSET(ub);
15+
size_t object_ub = __CPROVER_POINTER_OBJECT(ub);
16+
17+
char *ubp1 = lb + size + 1;
18+
size_t offset_ubp1 = __CPROVER_POINTER_OFFSET(ubp1);
19+
size_t object_ubp1 = __CPROVER_POINTER_OBJECT(ubp1);
20+
21+
assert(object_ub == object_lb); // proved
22+
assert(object_ubp1 == object_lb); // proved
23+
assert(ubp1 > ub); // proved
24+
assert(offset_ubp1 > offset_ub); // proved
25+
assert(offset_ubp1 == offset_ub + 1); // falsified
26+
27+
size_t idx;
28+
if(idx < size)
29+
{
30+
char *lb_idx = lb + idx;
31+
void *dummy_ub = ub;
32+
assert(lb <= lb_idx); // proved
33+
assert(lb_idx <= ub); // proved
34+
}
35+
36+
// to produce a trace so that we can observe some intermittent values
37+
assert(size < max_malloc_size);
38+
}

‎regression/cbmc/pointer-offset-01/test.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--trace
4+
^\s*ub.*=\(char \*\)&dynamic_object \+ \d+
5+
^\s*offset_ubp1=\d+ul* \(00000000 1[0 ]+1\)$
6+
^VERIFICATION FAILED$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
^\s*ub.*=\(char \*\)&dynamic_object \+ -\d+
12+
^\s*offset_ubp1=\d+ul* \(11111111 1
13+
--
14+
Verifies that all offsets use unsigned arithmetic.

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,8 @@ __CPROVER_assigns(__CPROVER_object_from(arr))
77
// clang-format on
88
{
99
__CPROVER_assert(arr != NULL, "arr is not NULL");
10-
__CPROVER_assert(size < __CPROVER_max_malloc_size, "size is capped");
11-
if(size > 0)
10+
__CPROVER_assert(size <= __CPROVER_max_malloc_size, "size is capped");
11+
if(size > 0 && size <= __CPROVER_max_malloc_size)
1212
{
1313
arr[0] = 0;
1414
arr[size - 1] = 0;

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

+1-7
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,8 @@ CORE
22
main.c
33
--dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check --pointer-overflow-check
44
^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ CAR size is less than __CPROVER_max_malloc_size: FAILURE$
5-
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
6-
^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
75
^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$
8-
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: FAILURE$
9-
^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: FAILURE$
10-
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$
11-
^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$
12-
^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: FAILURE$
6+
^\*\* 2 of \d+ failed
137
^EXIT=10$
148
^SIGNAL=0$
159
^VERIFICATION FAILED$

‎regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -4,13 +4,13 @@
44
void foo(char *arr, size_t size, char *cur)
55
// clang-format off
66
__CPROVER_requires(0 < size && __CPROVER_is_fresh(arr, size) &&
7-
__CPROVER_pointer_in_range_dfcc(arr, cur, arr + size))
8-
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(arr, cur, arr + size))
7+
__CPROVER_pointer_in_range_dfcc(arr, cur, arr + (size - 1)))
8+
__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(arr, cur, arr + (size - 1)))
99
// clang-format on
1010
{
1111
assert(__CPROVER_r_ok(arr, size));
1212
assert(__CPROVER_same_object(arr, cur));
13-
assert(arr <= cur && cur <= arr + size);
13+
assert(arr <= cur && cur <= arr + (size - 1));
1414
}
1515

1616
int main()

‎regression/contracts/no_redudant_checks/test.desc

+3-2
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,8 @@ main.c
2323
^\[main.pointer_arithmetic.15\].*: SUCCESS
2424
^\[main.pointer_arithmetic.16\].*: SUCCESS
2525
^\[main.pointer_arithmetic.17\].*: SUCCESS
26-
^\*\* 0 of 20 failed \(1 iterations\)
26+
^\[main.pointer_arithmetic.18\].*: SUCCESS
27+
^\*\* 0 of 21 failed \(1 iterations\)
2728
^VERIFICATION SUCCESSFUL$
2829
--
2930
^\[main.overflow.\d+\].*: FAILURE
@@ -35,7 +36,7 @@ Checks that assertions generated by the first --pointer-overflow-check:
3536
We expect 20 assertions to be generated:
3637
In the goto-instrument run:
3738
- 2 for using malloc
38-
- 17 caused by --pointer-overflow-check
39+
- 18 caused by --pointer-overflow-check
3940

4041
In the final cbmc run:
4142
- 0 caused by --pointer-overflow-check

‎regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,6 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
\"sources"\: \[ \"main\.c\" \]
7-
\"main\"\: \[ \"loop 1 invariant i \>\= 80u \|\| \_\_CPROVER\_POINTER\_OFFSET\(array\)
7+
\"main\"\: \[ \"loop 1 invariant i \>\= 80u \|\|
88
--
99
This test case checks if synthesized contracts are correctly dumped.

‎src/ansi-c/cprover_builtin_headers.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ void __CPROVER_loop_entry(const void *);
5959
__CPROVER_bool __CPROVER_LIVE_OBJECT(const void *);
6060
__CPROVER_bool __CPROVER_WRITEABLE_OBJECT(const void *);
6161
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
62-
__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
62+
__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *);
6363
__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
6464
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);
6565
__CPROVER_bool __CPROVER_pointer_in_range(const void *, const void *, const void *);

‎src/ansi-c/goto_check_c.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -1571,7 +1571,7 @@ void goto_check_ct::bounds_check_index(
15711571
effective_offset, p_offset.type())};
15721572
}
15731573

1574-
exprt zero = from_integer(0, ode.offset().type());
1574+
exprt zero = from_integer(0, effective_offset.type());
15751575

15761576
// the final offset must not be negative
15771577
binary_relation_exprt inequality(

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

+20-23
Original file line numberDiff line numberDiff line change
@@ -114,12 +114,11 @@ __CPROVER_HIDE:;
114114
((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
115115
"ptr NULL or writable up to size");
116116
__CPROVER_assert(
117-
size < __CPROVER_max_malloc_size,
117+
size <= __CPROVER_max_malloc_size,
118118
"CAR size is less than __CPROVER_max_malloc_size");
119-
__CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr);
119+
__CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
120120
__CPROVER_assert(
121-
!(offset > 0) |
122-
((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size),
121+
!(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
123122
"no offset bits overflow on CAR upper bound computation");
124123
return (__CPROVER_contracts_car_t){
125124
.is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
@@ -163,12 +162,11 @@ __CPROVER_HIDE:;
163162
((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
164163
"ptr NULL or writable up to size");
165164
__CPROVER_assert(
166-
size < __CPROVER_max_malloc_size,
165+
size <= __CPROVER_max_malloc_size,
167166
"CAR size is less than __CPROVER_max_malloc_size");
168-
__CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr);
167+
__CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
169168
__CPROVER_assert(
170-
!(offset > 0) |
171-
((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size),
169+
!(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
172170
"no offset bits overflow on CAR upper bound computation");
173171
__CPROVER_contracts_car_t *elem = set->elems + idx;
174172
*elem = (__CPROVER_contracts_car_t){
@@ -783,14 +781,13 @@ __CPROVER_HIDE:;
783781

784782
// Compute the upper bound, perform inclusion check against contract-assigns
785783
__CPROVER_assert(
786-
size < __CPROVER_max_malloc_size,
784+
size <= __CPROVER_max_malloc_size,
787785
"CAR size is less than __CPROVER_max_malloc_size");
788786

789-
__CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr);
787+
__CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr);
790788

791789
__CPROVER_assert(
792-
!(offset > 0) |
793-
((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size),
790+
!(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
794791
"no offset bits overflow on CAR upper bound computation");
795792
void *ub = (void *)((char *)ptr + size);
796793
__CPROVER_contracts_car_t *elem = set->contract_assigns.elems;
@@ -1198,7 +1195,7 @@ __CPROVER_HIDE:;
11981195
{
11991196
// When --malloc-may-fail --malloc-fail-null
12001197
// add implicit assumption that the size is capped
1201-
__CPROVER_assume(size < __CPROVER_max_malloc_size);
1198+
__CPROVER_assume(size <= __CPROVER_max_malloc_size);
12021199
}
12031200
else if(
12041201
__CPROVER_malloc_failure_mode ==
@@ -1208,9 +1205,9 @@ __CPROVER_HIDE:;
12081205
// check if max allocation size is exceeded and
12091206
// add implicit assumption that the size is capped
12101207
__CPROVER_assert(
1211-
size < __CPROVER_max_malloc_size,
1208+
size <= __CPROVER_max_malloc_size,
12121209
"__CPROVER_is_fresh max allocation size exceeded");
1213-
__CPROVER_assume(size < __CPROVER_max_malloc_size);
1210+
__CPROVER_assume(size <= __CPROVER_max_malloc_size);
12141211
}
12151212

12161213
void *ptr = __CPROVER_allocate(size, 0);
@@ -1255,16 +1252,16 @@ __CPROVER_HIDE:;
12551252
__CPROVER_malloc_failure_mode ==
12561253
__CPROVER_malloc_failure_mode_return_null)
12571254
{
1258-
__CPROVER_assume(size < __CPROVER_max_malloc_size);
1255+
__CPROVER_assume(size <= __CPROVER_max_malloc_size);
12591256
}
12601257
else if(
12611258
__CPROVER_malloc_failure_mode ==
12621259
__CPROVER_malloc_failure_mode_assert_then_assume)
12631260
{
12641261
__CPROVER_assert(
1265-
size < __CPROVER_max_malloc_size,
1266-
"__CPROVER_is_fresh requires size < __CPROVER_max_malloc_size");
1267-
__CPROVER_assume(size < __CPROVER_max_malloc_size);
1262+
size <= __CPROVER_max_malloc_size,
1263+
"__CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size");
1264+
__CPROVER_assume(size <= __CPROVER_max_malloc_size);
12681265
}
12691266

12701267
void *ptr = __CPROVER_allocate(size, 0);
@@ -1360,8 +1357,8 @@ __CPROVER_HIDE:;
13601357
__CPROVER_assert(
13611358
__CPROVER_same_object(lb, ub),
13621359
"lb and ub pointers must have the same object");
1363-
__CPROVER_ssize_t lb_offset = __CPROVER_POINTER_OFFSET(lb);
1364-
__CPROVER_ssize_t ub_offset = __CPROVER_POINTER_OFFSET(ub);
1360+
__CPROVER_size_t lb_offset = __CPROVER_POINTER_OFFSET(lb);
1361+
__CPROVER_size_t ub_offset = __CPROVER_POINTER_OFFSET(ub);
13651362
__CPROVER_assert(
13661363
lb_offset <= ub_offset, "lb and ub pointers must be ordered");
13671364
if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
@@ -1373,14 +1370,14 @@ __CPROVER_HIDE:;
13731370
__CPROVER_size_t offset = __VERIFIER_nondet_size();
13741371

13751372
// this cast is safe because we prove that ub and lb are ordered
1376-
__CPROVER_size_t max_offset = (__CPROVER_size_t)(ub_offset - lb_offset);
1373+
__CPROVER_size_t max_offset = ub_offset - lb_offset;
13771374
__CPROVER_assume(offset <= max_offset);
13781375
*ptr = (char *)lb + offset;
13791376
return 1;
13801377
}
13811378
else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
13821379
{
1383-
__CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(*ptr);
1380+
__CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(*ptr);
13841381
return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
13851382
offset <= ub_offset;
13861383
}

‎src/cprover/bv_pointers_wide.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -769,7 +769,7 @@ exprt bv_pointers_widet::bv_get_rec(
769769

770770
pointer_logict::pointert pointer{
771771
numeric_cast_v<std::size_t>(binary2integer(value_addr, false)),
772-
binary2integer(value_offset, true)};
772+
binary2integer(value_offset, false)};
773773

774774
return annotated_pointer_constant_exprt{
775775
bvrep, pointer_logic.pointer_expr(pointer, pt)};

‎src/pointer-analysis/value_set_dereference.cpp

+11-3
Original file line numberDiff line numberDiff line change
@@ -517,7 +517,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
517517

518518
const index_exprt index_expr(
519519
symbol_expr,
520-
pointer_offset(pointer_expr),
520+
typecast_exprt::conditional_cast(
521+
pointer_offset(pointer_expr),
522+
to_array_type(memory_symbol.type).index_type()),
521523
to_array_type(memory_symbol.type).element_type());
522524

523525
valuet result;
@@ -532,7 +534,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
532534
{
533535
const index_exprt index_expr(
534536
symbol_expr,
535-
pointer_offset(pointer_expr),
537+
typecast_exprt::conditional_cast(
538+
pointer_offset(pointer_expr),
539+
to_array_type(memory_symbol.type).index_type()),
536540
to_array_type(memory_symbol.type).element_type());
537541

538542
valuet result;
@@ -768,7 +772,11 @@ bool value_set_dereferencet::memory_model_bytes(
768772
{
769773
// yes, can use 'index', but possibly need to convert
770774
result = typecast_exprt::conditional_cast(
771-
index_exprt(value, offset, to_array_type(from_type).element_type()),
775+
index_exprt(
776+
value,
777+
typecast_exprt::conditional_cast(
778+
offset, to_array_type(from_type).index_type()),
779+
to_array_type(from_type).element_type()),
772780
to_type);
773781
}
774782
else

0 commit comments

Comments
 (0)