diff --git a/regression/cbmc-incr-smt2/pointers-conversions/byte_update.desc b/regression/cbmc-incr-smt2/pointers-conversions/byte_update.desc index c22e0fcc8d3..8916b0c4cf6 100644 --- a/regression/cbmc-incr-smt2/pointers-conversions/byte_update.desc +++ b/regression/cbmc-incr-smt2/pointers-conversions/byte_update.desc @@ -10,7 +10,7 @@ Assumption: file byte_update\.c line \d+ function main offset >= 0u && offset < 4u State \d+ file byte_update\.c function main line \d+ thread \d+ - byte_extract_little_endian\(x, \(signed long( long)? int\)offset, uint8_t\)=1 \(00000001\) + byte_extract_little_endian\(x, \(.*\)offset, uint8_t\)=1 \(00000001\) Violated property: file byte_update.c function main line \d+ thread \d+ assertion x != 256u diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free-01/test.desc index a727d0817d0..975d36515ec 100644 --- a/regression/cbmc-library/free-01/test.desc +++ b/regression/cbmc-library/free-01/test.desc @@ -1,7 +1,7 @@ CORE main.c --pointer-check --bounds-check --stop-on-fail -free argument must be (NULL or valid pointer|dynamic object) +free argument (must be (NULL or valid pointer|dynamic object)|has offset zero) ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc b/regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc index a9c36d41d2c..02383fd37d9 100644 --- a/regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc +++ b/regression/cbmc-library/strlen-02/test-c-with-string-abstraction.desc @@ -1,7 +1,7 @@ CORE test.c --string-abstraction --show-goto-functions -ASSIGN strlen#return_value := cast\(cast\(\*strlen::s::s#str\.length, signedbv\[.*\]\) - pointer_offset\(strlen::s\), unsignedbv\[.*\]\) +ASSIGN strlen#return_value := \*strlen::s::s#str\.length - pointer_offset\(strlen::s\) ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc b/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc index 6490ffd9fd5..5e71e5b8485 100644 --- a/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc +++ b/regression/cbmc-primitives/pointer-offset-01/test-no-cp.desc @@ -3,11 +3,11 @@ main.c --no-simplify --no-propagation ^EXIT=10$ ^SIGNAL=0$ -\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE +\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: SUCCESS \[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE -- ^warning: ignoring -- -Check that both positive and negative offsets can be chosen for uninitialized -pointers. We use --no-simplify and --no-propagation to ensure that the case is -not solved by the constant propagation and thus tests the constraint encoding. +Check that positive offsets can be chosen for uninitialized pointers. We +use --no-simplify and --no-propagation to ensure that the case is not solved +by the constant propagation and thus tests the constraint encoding. diff --git a/regression/cbmc-primitives/pointer-offset-01/test.desc b/regression/cbmc-primitives/pointer-offset-01/test.desc index 4a8f37710bd..b6d13bdf66f 100644 --- a/regression/cbmc-primitives/pointer-offset-01/test.desc +++ b/regression/cbmc-primitives/pointer-offset-01/test.desc @@ -3,15 +3,13 @@ main.c ^EXIT=10$ ^SIGNAL=0$ -\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: FAILURE +\[main.assertion.1\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) >= 0: SUCCESS \[main.assertion.2\] line \d+ assertion __CPROVER_POINTER_OFFSET\(p\) < 0: FAILURE -- ^warning: ignoring -- -For uninitialised pointers, CBMC chooses a nondeterministic value (though no memory -is allocated). Since the offset of pointers is signed, negative offsets should be -able to be chosen (along with positive ones) non-deterministically. -`__CPROVER_POINTER_OFFSET` is the CBMC primitive that gets the pointer offset -from the base address of the object. This test guards this, and especially -against the case where we could only observe some cases where offsets were only -positive (in some CI configurations, for instance). +For uninitialised pointers, CBMC chooses a nondeterministic value (though no +memory is allocated). Since the offset of pointers is unsigned, negative +offsets cannot be chosen. `__CPROVER_POINTER_OFFSET` is the CBMC primitive +that gets the pointer offset from the base address of the object. This test +guards this. diff --git a/regression/cbmc/address_space_size_limit3/test.desc b/regression/cbmc/address_space_size_limit3/test.desc index 3faf34bf16b..84ba893a1e1 100644 --- a/regression/cbmc/address_space_size_limit3/test.desc +++ b/regression/cbmc/address_space_size_limit3/test.desc @@ -1,6 +1,6 @@ CORE thorough-smt-backend main.i ---32 --little-endian --object-bits 25 --pointer-check +--32 --little-endian --object-bits 26 --pointer-check ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc index c88637311c2..111f234d20d 100644 --- a/regression/cbmc/memory_allocation2/test.desc +++ b/regression/cbmc/memory_allocation2/test.desc @@ -3,9 +3,9 @@ main.c --bounds-check ^EXIT=10$ ^SIGNAL=0$ -^\[main\.array_bounds\.[1-5]\] .*: SUCCESS$ -^\[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$ -^\*\* 1 of 6 failed +^\[main\.array_bounds\.[1-2]\] .*: SUCCESS$ +^\[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$ +^\*\* 1 of 3 failed ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc/pointer-offset-01/main.c b/regression/cbmc/pointer-offset-01/main.c new file mode 100644 index 00000000000..5e9a5b3dca0 --- /dev/null +++ b/regression/cbmc/pointer-offset-01/main.c @@ -0,0 +1,38 @@ +#include +#include + +int main(void) +{ + size_t size; + size_t max_malloc_size = __CPROVER_max_malloc_size; + __CPROVER_assume(0 <= size && size <= max_malloc_size); + char *lb = malloc(size); + size_t offset_lb = __CPROVER_POINTER_OFFSET(lb); + size_t object_lb = __CPROVER_POINTER_OBJECT(lb); + + char *ub = lb + size; + size_t offset_ub = __CPROVER_POINTER_OFFSET(ub); + size_t object_ub = __CPROVER_POINTER_OBJECT(ub); + + char *ubp1 = lb + size + 1; + size_t offset_ubp1 = __CPROVER_POINTER_OFFSET(ubp1); + size_t object_ubp1 = __CPROVER_POINTER_OBJECT(ubp1); + + assert(object_ub == object_lb); // proved + assert(object_ubp1 == object_lb); // proved + assert(ubp1 > ub); // proved + assert(offset_ubp1 > offset_ub); // proved + assert(offset_ubp1 == offset_ub + 1); // falsified + + size_t idx; + if(idx < size) + { + char *lb_idx = lb + idx; + void *dummy_ub = ub; + assert(lb <= lb_idx); // proved + assert(lb_idx <= ub); // proved + } + + // to produce a trace so that we can observe some intermittent values + assert(size < max_malloc_size); +} diff --git a/regression/cbmc/pointer-offset-01/test.desc b/regression/cbmc/pointer-offset-01/test.desc new file mode 100644 index 00000000000..182da63953a --- /dev/null +++ b/regression/cbmc/pointer-offset-01/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--trace +^\s*ub.*=\(char \*\)&dynamic_object \+ \d+ +^\s*offset_ubp1=\d+ul* \(00000000 1[0 ]+1\)$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +^\s*ub.*=\(char \*\)&dynamic_object \+ -\d+ +^\s*offset_ubp1=\d+ul* \(11111111 1 +-- +Verifies that all offsets use unsigned arithmetic. diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main.c b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main.c index fd067ed97ce..21ee9a08b2d 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main.c +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/main.c @@ -7,8 +7,8 @@ __CPROVER_assigns(__CPROVER_object_from(arr)) // clang-format on { __CPROVER_assert(arr != NULL, "arr is not NULL"); - __CPROVER_assert(size < __CPROVER_max_malloc_size, "size is capped"); - if(size > 0) + __CPROVER_assert(size <= __CPROVER_max_malloc_size, "size is capped"); + if(size > 0 && size <= __CPROVER_max_malloc_size) { arr[0] = 0; arr[size - 1] = 0; 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 90c456ffc0a..7eaa04afab1 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 @@ -2,14 +2,8 @@ CORE main.c --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$ -^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$ -^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$ ^\[foo.assertion.\d+\] line \d+ size is capped: FAILURE$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: FAILURE$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$ -^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): FAILURE$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: FAILURE$ +^\*\* 2 of \d+ failed ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c index 02723e23e92..191ad3b4f02 100644 --- a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c +++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/main.c @@ -4,13 +4,13 @@ void foo(char *arr, size_t size, char *cur) // clang-format off __CPROVER_requires(0 < size && __CPROVER_is_fresh(arr, size) && - __CPROVER_pointer_in_range_dfcc(arr, cur, arr + size)) -__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(arr, cur, arr + size)) + __CPROVER_pointer_in_range_dfcc(arr, cur, arr + (size - 1))) +__CPROVER_ensures(__CPROVER_pointer_in_range_dfcc(arr, cur, arr + (size - 1))) // clang-format on { assert(__CPROVER_r_ok(arr, size)); assert(__CPROVER_same_object(arr, cur)); - assert(arr <= cur && cur <= arr + size); + assert(arr <= cur && cur <= arr + (size - 1)); } int main() diff --git a/regression/contracts/no_redudant_checks/test.desc b/regression/contracts/no_redudant_checks/test.desc index c2100ee2a71..ed318ccbec3 100644 --- a/regression/contracts/no_redudant_checks/test.desc +++ b/regression/contracts/no_redudant_checks/test.desc @@ -23,7 +23,8 @@ main.c ^\[main.pointer_arithmetic.15\].*: SUCCESS ^\[main.pointer_arithmetic.16\].*: SUCCESS ^\[main.pointer_arithmetic.17\].*: SUCCESS -^\*\* 0 of 20 failed \(1 iterations\) +^\[main.pointer_arithmetic.18\].*: SUCCESS +^\*\* 0 of 21 failed \(1 iterations\) ^VERIFICATION SUCCESSFUL$ -- ^\[main.overflow.\d+\].*: FAILURE @@ -35,7 +36,7 @@ Checks that assertions generated by the first --pointer-overflow-check: We expect 20 assertions to be generated: In the goto-instrument run: - 2 for using malloc -- 17 caused by --pointer-overflow-check +- 18 caused by --pointer-overflow-check In the final cbmc run: - 0 caused by --pointer-overflow-check diff --git a/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc b/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc index 4344f2ea81c..dd6f4658cca 100644 --- a/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc +++ b/regression/goto-synthesizer/loop_contracts_synthesis_02/test_dump.desc @@ -4,6 +4,6 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \"sources"\: \[ \"main\.c\" \] -\"main\"\: \[ \"loop 1 invariant i \>\= 80u \|\| \_\_CPROVER\_POINTER\_OFFSET\(array\) +\"main\"\: \[ \"loop 1 invariant i \>\= 80u \|\| -- This test case checks if synthesized contracts are correctly dumped. diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 184db687496..2463de8d629 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -59,7 +59,7 @@ void __CPROVER_loop_entry(const void *); __CPROVER_bool __CPROVER_LIVE_OBJECT(const void *); __CPROVER_bool __CPROVER_WRITEABLE_OBJECT(const void *); __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *); -__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *); +__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *); __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *); __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *); __CPROVER_bool __CPROVER_pointer_in_range(const void *, const void *, const void *); diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 2780b5944ef..25f8a32c23c 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -1571,7 +1571,7 @@ void goto_check_ct::bounds_check_index( effective_offset, p_offset.type())}; } - exprt zero = from_integer(0, ode.offset().type()); + exprt zero = from_integer(0, effective_offset.type()); // the final offset must not be negative binary_relation_exprt inequality( diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 2a4de2cc6ff..33b7954cb47 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -114,12 +114,11 @@ __CPROVER_HIDE:; ((ptr == 0) | __CPROVER_rw_ok(ptr, size)), "ptr NULL or writable up to size"); __CPROVER_assert( - size < __CPROVER_max_malloc_size, + size <= __CPROVER_max_malloc_size, "CAR size is less than __CPROVER_max_malloc_size"); - __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr); + __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr); __CPROVER_assert( - !(offset > 0) | - ((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size), + !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size), "no offset bits overflow on CAR upper bound computation"); return (__CPROVER_contracts_car_t){ .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size}; @@ -163,12 +162,11 @@ __CPROVER_HIDE:; ((ptr == 0) | __CPROVER_rw_ok(ptr, size)), "ptr NULL or writable up to size"); __CPROVER_assert( - size < __CPROVER_max_malloc_size, + size <= __CPROVER_max_malloc_size, "CAR size is less than __CPROVER_max_malloc_size"); - __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr); + __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr); __CPROVER_assert( - !(offset > 0) | - ((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size), + !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size), "no offset bits overflow on CAR upper bound computation"); __CPROVER_contracts_car_t *elem = set->elems + idx; *elem = (__CPROVER_contracts_car_t){ @@ -783,14 +781,13 @@ __CPROVER_HIDE:; // Compute the upper bound, perform inclusion check against contract-assigns __CPROVER_assert( - size < __CPROVER_max_malloc_size, + size <= __CPROVER_max_malloc_size, "CAR size is less than __CPROVER_max_malloc_size"); - __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(ptr); + __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(ptr); __CPROVER_assert( - !(offset > 0) | - ((__CPROVER_size_t)offset + size < __CPROVER_max_malloc_size), + !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size), "no offset bits overflow on CAR upper bound computation"); void *ub = (void *)((char *)ptr + size); __CPROVER_contracts_car_t *elem = set->contract_assigns.elems; @@ -1198,7 +1195,7 @@ __CPROVER_HIDE:; { // When --malloc-may-fail --malloc-fail-null // add implicit assumption that the size is capped - __CPROVER_assume(size < __CPROVER_max_malloc_size); + __CPROVER_assume(size <= __CPROVER_max_malloc_size); } else if( __CPROVER_malloc_failure_mode == @@ -1208,9 +1205,9 @@ __CPROVER_HIDE:; // check if max allocation size is exceeded and // add implicit assumption that the size is capped __CPROVER_assert( - size < __CPROVER_max_malloc_size, + size <= __CPROVER_max_malloc_size, "__CPROVER_is_fresh max allocation size exceeded"); - __CPROVER_assume(size < __CPROVER_max_malloc_size); + __CPROVER_assume(size <= __CPROVER_max_malloc_size); } void *ptr = __CPROVER_allocate(size, 0); @@ -1255,16 +1252,16 @@ __CPROVER_HIDE:; __CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_return_null) { - __CPROVER_assume(size < __CPROVER_max_malloc_size); + __CPROVER_assume(size <= __CPROVER_max_malloc_size); } else if( __CPROVER_malloc_failure_mode == __CPROVER_malloc_failure_mode_assert_then_assume) { __CPROVER_assert( - size < __CPROVER_max_malloc_size, - "__CPROVER_is_fresh requires size < __CPROVER_max_malloc_size"); - __CPROVER_assume(size < __CPROVER_max_malloc_size); + size <= __CPROVER_max_malloc_size, + "__CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size"); + __CPROVER_assume(size <= __CPROVER_max_malloc_size); } void *ptr = __CPROVER_allocate(size, 0); @@ -1360,8 +1357,8 @@ __CPROVER_HIDE:; __CPROVER_assert( __CPROVER_same_object(lb, ub), "lb and ub pointers must have the same object"); - __CPROVER_ssize_t lb_offset = __CPROVER_POINTER_OFFSET(lb); - __CPROVER_ssize_t ub_offset = __CPROVER_POINTER_OFFSET(ub); + __CPROVER_size_t lb_offset = __CPROVER_POINTER_OFFSET(lb); + __CPROVER_size_t ub_offset = __CPROVER_POINTER_OFFSET(ub); __CPROVER_assert( lb_offset <= ub_offset, "lb and ub pointers must be ordered"); if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx) @@ -1373,14 +1370,14 @@ __CPROVER_HIDE:; __CPROVER_size_t offset = __VERIFIER_nondet_size(); // this cast is safe because we prove that ub and lb are ordered - __CPROVER_size_t max_offset = (__CPROVER_size_t)(ub_offset - lb_offset); + __CPROVER_size_t max_offset = ub_offset - lb_offset; __CPROVER_assume(offset <= max_offset); *ptr = (char *)lb + offset; return 1; } else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */ { - __CPROVER_ssize_t offset = __CPROVER_POINTER_OFFSET(*ptr); + __CPROVER_size_t offset = __CPROVER_POINTER_OFFSET(*ptr); return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset && offset <= ub_offset; } diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp index d03449e8d8b..1fe3acf7d44 100644 --- a/src/cprover/bv_pointers_wide.cpp +++ b/src/cprover/bv_pointers_wide.cpp @@ -769,7 +769,7 @@ exprt bv_pointers_widet::bv_get_rec( pointer_logict::pointert pointer{ numeric_cast_v(binary2integer(value_addr, false)), - binary2integer(value_offset, true)}; + binary2integer(value_offset, false)}; return annotated_pointer_constant_exprt{ bvrep, pointer_logic.pointer_expr(pointer, pt)}; diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index 6b082e63b4e..fafe7cad353 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -517,7 +517,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( const index_exprt index_expr( symbol_expr, - pointer_offset(pointer_expr), + typecast_exprt::conditional_cast( + pointer_offset(pointer_expr), + to_array_type(memory_symbol.type).index_type()), to_array_type(memory_symbol.type).element_type()); valuet result; @@ -532,7 +534,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( { const index_exprt index_expr( symbol_expr, - pointer_offset(pointer_expr), + typecast_exprt::conditional_cast( + pointer_offset(pointer_expr), + to_array_type(memory_symbol.type).index_type()), to_array_type(memory_symbol.type).element_type()); valuet result; @@ -768,7 +772,11 @@ bool value_set_dereferencet::memory_model_bytes( { // yes, can use 'index', but possibly need to convert result = typecast_exprt::conditional_cast( - index_exprt(value, offset, to_array_type(from_type).element_type()), + index_exprt( + value, + typecast_exprt::conditional_cast( + offset, to_array_type(from_type).index_type()), + to_array_type(from_type).element_type()), to_type); } else diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index e0e4724dfa6..09973306a93 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -194,13 +194,14 @@ literalt bv_pointerst::convert_rest(const exprt &expr) if(same_object_lit.is_false()) return same_object_lit; + // The comparison is UNSIGNED, to match the type of pointer_offsett return prop.land( same_object_lit, bv_utils.rel( offset_bv0, expr.id(), offset_bv1, - bv_utilst::representationt::SIGNED)); + bv_utilst::representationt::UNSIGNED)); } } @@ -615,12 +616,12 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) const pointer_typet &lhs_pt = to_pointer_type(minus_expr.lhs().type()); const bvt &lhs = convert_bv(minus_expr.lhs()); const bvt lhs_offset = - bv_utils.sign_extension(offset_literals(lhs, lhs_pt), width); + bv_utils.zero_extension(offset_literals(lhs, lhs_pt), width); const pointer_typet &rhs_pt = to_pointer_type(minus_expr.rhs().type()); const bvt &rhs = convert_bv(minus_expr.rhs()); const bvt rhs_offset = - bv_utils.sign_extension(offset_literals(rhs, rhs_pt), width); + bv_utils.zero_extension(offset_literals(rhs, rhs_pt), width); bvt difference = bv_utils.sub(lhs_offset, rhs_offset); @@ -686,8 +687,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) bvt offset_bv = offset_literals(pointer_bv, to_pointer_type(pointer.type())); - // we do a sign extension to permit negative offsets - return bv_utils.sign_extension(offset_bv, width); + return bv_utils.zero_extension(offset_bv, width); } else if( const auto object_size = expr_try_dynamic_cast(expr)) @@ -785,7 +785,7 @@ exprt bv_pointerst::bv_get_rec( pointer_logict::pointert pointer{ numeric_cast_v(binary2integer(value_addr, false)), - binary2integer(value_offset, true)}; + binary2integer(value_offset, false)}; return annotated_pointer_constant_exprt{ bvrep, pointer_logic.pointer_expr(pointer, pt)}; @@ -871,7 +871,7 @@ bvt bv_pointerst::offset_arithmetic( } const std::size_t offset_bits = get_offset_width(type); - bv_index = bv_utils.sign_extension(bv_index, offset_bits); + bv_index = bv_utils.zero_extension(bv_index, offset_bits); bvt offset_bv = offset_literals(bv, type); diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index c42c1bbd2cc..02986e1442a 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -434,17 +434,20 @@ static exprt::operandst instantiate_byte_array( src.operands().begin() + narrow_cast(upper_bound)}; } - PRECONDITION(src.type().id() == ID_array || src.type().id() == ID_vector); + const typet &element_type = src.type().id() == ID_array + ? to_array_type(src.type()).element_type() + : to_vector_type(src.type()).element_type(); + const typet index_type = src.type().id() == ID_array + ? to_array_type(src.type()).index_type() + : to_vector_type(src.type()).index_type(); PRECONDITION( - can_cast_type( - to_type_with_subtype(src.type()).subtype()) && - to_bitvector_type(to_type_with_subtype(src.type()).subtype()).get_width() == - bits_per_byte); + can_cast_type(element_type) && + to_bitvector_type(element_type).get_width() == bits_per_byte); exprt::operandst bytes; bytes.reserve(upper_bound - lower_bound); for(std::size_t i = lower_bound; i < upper_bound; ++i) { - const index_exprt idx{src, from_integer(i, c_index_type())}; + const index_exprt idx{src, from_integer(i, index_type)}; bytes.push_back(simplify_expr(idx, ns)); } return bytes; @@ -465,6 +468,10 @@ static exprt unpack_array_vector_no_known_bounds( const std::size_t bits_per_byte, const namespacet &ns) { + const typet index_type = src.type().id() == ID_array + ? to_array_type(src.type()).index_type() + : to_vector_type(src.type()).index_type(); + // TODO we either need a symbol table here or make array comprehensions // introduce a scope static std::size_t array_comprehension_index_counter = 0; @@ -472,12 +479,11 @@ static exprt unpack_array_vector_no_known_bounds( symbol_exprt array_comprehension_index{ "$array_comprehension_index_a_v" + std::to_string(array_comprehension_index_counter), - c_index_type()}; + index_type}; index_exprt element{ src, - div_exprt{ - array_comprehension_index, from_integer(el_bytes, c_index_type())}}; + div_exprt{array_comprehension_index, from_integer(el_bytes, index_type)}}; exprt sub = unpack_rec(element, little_endian, {}, {}, bits_per_byte, ns, false); @@ -577,6 +583,9 @@ static exprt unpack_array_vector( num_elements = *max_bytes; const exprt src_simp = simplify_expr(src, ns); + const typet index_type = src_simp.type().id() == ID_array + ? to_array_type(src_simp.type()).index_type() + : to_vector_type(src_simp.type()).index_type(); for(mp_integer i = first_element; i < *num_elements; ++i) { @@ -591,7 +600,7 @@ static exprt unpack_array_vector( } else { - element = index_exprt(src_simp, from_integer(i, c_index_type())); + element = index_exprt(src_simp, from_integer(i, index_type)); } // recursively unpack each element so that we eventually just have an array @@ -1022,14 +1031,17 @@ static exprt unpack_rec( src, bv_typet{numeric_cast_v(total_bits)}); auto const byte_type = bv_typet{bits_per_byte}; exprt::operandst byte_operands; + array_typet array_type{ + bv_typet{bits_per_byte}, from_integer(0, size_type())}; + for(; bit_offset < last_bit; bit_offset += bits_per_byte) { PRECONDITION( pointer_offset_bits(src_as_bitvector.type(), ns).has_value()); extractbits_exprt extractbits( src_as_bitvector, - from_integer(bit_offset + bits_per_byte - 1, c_index_type()), - from_integer(bit_offset, c_index_type()), + from_integer(bit_offset + bits_per_byte - 1, array_type.index_type()), + from_integer(bit_offset, array_type.index_type()), byte_type); // endianness_mapt should be the point of reference for mapping out @@ -1042,9 +1054,8 @@ static exprt unpack_rec( } const std::size_t size = byte_operands.size(); - return array_exprt( - std::move(byte_operands), - array_typet{bv_typet{bits_per_byte}, from_integer(size, size_type())}); + array_type.size() = from_integer(size, size_type()); + return array_exprt{std::move(byte_operands), std::move(array_type)}; } return array_exprt( @@ -1112,7 +1123,7 @@ static exprt lower_byte_extract_array_vector( symbol_exprt array_comprehension_index{ "$array_comprehension_index_a" + std::to_string(array_comprehension_index_counter), - c_index_type()}; + array_type.index_type()}; plus_exprt new_offset{ unpacked.offset(), @@ -1347,10 +1358,17 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) const exprt &offset = unpacked.offset(); optionalt subtype; + optionalt index_type; if(root.type().id() == ID_vector) + { subtype = to_vector_type(root.type()).element_type(); + index_type = to_vector_type(root.type()).index_type(); + } else + { subtype = to_array_type(root.type()).element_type(); + index_type = to_array_type(root.type()).index_type(); + } auto subtype_bits = pointer_offset_bits(*subtype, ns); @@ -1383,7 +1401,9 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) // the most significant byte comes first in the concatenation! std::size_t offset_int = little_endian ? (width_bytes - i - 1) : i; - plus_exprt offset_i(from_integer(offset_int, offset.type()), offset); + plus_exprt offset_i{ + from_integer(offset_int, *index_type), + typecast_exprt::conditional_cast(offset, *index_type)}; simplify(offset_i, ns); mp_integer index = 0; @@ -1447,7 +1467,7 @@ static exprt lower_byte_update_byte_array_vector_non_const( symbol_exprt array_comprehension_index{ "$array_comprehension_index_u_a_v" + std::to_string(array_comprehension_index_counter), - c_index_type()}; + to_array_type(src.type()).index_type()}; binary_predicate_exprt lower_bound{ typecast_exprt::conditional_cast( @@ -1514,6 +1534,10 @@ static exprt lower_byte_update_byte_array_vector( src.id() == ID_byte_update_big_endian); const bool little_endian = src.id() == ID_byte_update_little_endian; + const typet index_type = src.type().id() == ID_array + ? to_array_type(src.type()).index_type() + : to_vector_type(src.type()).index_type(); + // apply 'array-update-with' num_elements times exprt result = src.op(); @@ -1522,7 +1546,10 @@ static exprt lower_byte_update_byte_array_vector( const exprt &element = value_as_byte_array.operands()[i]; exprt where = simplify_expr( - plus_exprt{src.offset(), from_integer(i, src.offset().type())}, ns); + plus_exprt{ + typecast_exprt::conditional_cast(src.offset(), index_type), + from_integer(i, index_type)}, + ns); // skip elements that wouldn't change (skip over typecasts as we might have // some signed/unsigned char conversions) @@ -1593,9 +1620,10 @@ static exprt lower_byte_update_array_vector_unbounded( symbol_exprt array_comprehension_index{ "$array_comprehension_index_u_a_v_u" + std::to_string(array_comprehension_index_counter), - c_index_type()}; + to_array_type(src.type()).index_type()}; // all arithmetic uses offset/index types + PRECONDITION(array_comprehension_index.type() == src.offset().type()); PRECONDITION(subtype_size.type() == src.offset().type()); PRECONDITION(initial_bytes.type() == src.offset().type()); PRECONDITION(first_index.type() == src.offset().type()); @@ -1644,10 +1672,12 @@ static exprt lower_byte_update_array_vector_unbounded( // The size of a partial update at the end of the updated range, may be zero. mod_exprt tail_size{ - minus_exprt{ - typecast_exprt::conditional_cast( - non_const_update_bound, initial_bytes.type()), - initial_bytes}, + typecast_exprt::conditional_cast( + minus_exprt{ + typecast_exprt::conditional_cast( + non_const_update_bound, initial_bytes.type()), + initial_bytes}, + subtype_size.type()), subtype_size}; // The bound where updates end, which is conditional on the partial update @@ -1727,6 +1757,8 @@ static exprt lower_byte_update_array_vector_non_const( // compute the index of the first element of the array/vector that may be // updated + PRECONDITION( + src.offset().type() == to_array_type(src.op().type()).index_type()); exprt first_index = div_exprt{src.offset(), subtype_size}; simplify(first_index, ns); @@ -1862,10 +1894,17 @@ static exprt lower_byte_update_array_vector( { const bool is_array = src.type().id() == ID_array; exprt size; + typet index_type; if(is_array) + { size = to_array_type(src.type()).size(); + index_type = to_array_type(src.type()).index_type(); + } else + { size = to_vector_type(src.type()).size(); + index_type = to_vector_type(src.type()).index_type(); + } auto subtype_bits = pointer_offset_bits(subtype, ns); @@ -1894,7 +1933,7 @@ static exprt lower_byte_update_array_vector( (i + 1) * *subtype_bits <= offset_bytes * src.get_bits_per_byte(); ++i) { - elements.push_back(index_exprt{src.op(), from_integer(i, c_index_type())}); + elements.push_back(index_exprt{src.op(), from_integer(i, index_type)}); } // the modified elements @@ -1932,7 +1971,7 @@ static exprt lower_byte_update_array_vector( const byte_update_exprt bu{ src.id(), - index_exprt{src.op(), from_integer(i, c_index_type())}, + index_exprt{src.op(), from_integer(i, index_type)}, from_integer(update_offset < 0 ? 0 : update_offset, src.offset().type()), array_exprt{ std::move(update_values), @@ -1945,7 +1984,7 @@ static exprt lower_byte_update_array_vector( // copy the tail not affected by the update for(; i < num_elements; ++i) - elements.push_back(index_exprt{src.op(), from_integer(i, c_index_type())}); + elements.push_back(index_exprt{src.op(), from_integer(i, index_type)}); if(is_array) return simplify_expr( diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 429fe4b6417..9c65ef8614e 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -37,7 +37,7 @@ exprt object_size(const exprt &pointer) exprt pointer_offset(const exprt &pointer) { - return pointer_offset_exprt(pointer, signed_size_type()); + return pointer_offset_exprt(pointer, size_type()); } exprt deallocated(const exprt &pointer, const namespacet &ns) @@ -73,30 +73,45 @@ exprt object_upper_bound( const exprt &pointer, const exprt &access_size) { - // this is - // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer) + exprt object_offset = pointer_offset(pointer); exprt object_size_expr=object_size(pointer); - exprt object_offset=pointer_offset(pointer); - - // need to add size - irep_idt op=ID_ge; - exprt sum=object_offset; + std::size_t max_width = std::max( + to_bitvector_type(object_offset.type()).get_width(), + to_bitvector_type(object_size_expr.type()).get_width()); + // We add the size to the offset, if given. if(access_size.is_not_nil()) { - op=ID_gt; + // This is + // POINTER_OFFSET(p)+access_size>OBJECT_SIZE(pointer) + // We enlarge all bit-vectors to avoid an overflow on the addition. + + max_width = + std::max(max_width, to_bitvector_type(access_size.type()).get_width()); + + auto type = unsignedbv_typet(max_width + 1); + + auto sum = plus_exprt( + typecast_exprt::conditional_cast(object_offset, type), + typecast_exprt::conditional_cast(access_size, type)); - sum = plus_exprt( - typecast_exprt::conditional_cast(object_offset, access_size.type()), - access_size); + return binary_relation_exprt( + sum, ID_gt, typecast_exprt::conditional_cast(object_size_expr, type)); } + else + { + // This is + // POINTER_OFFSET(p)>=OBJECT_SIZE(pointer) + + auto type = unsignedbv_typet(max_width); - return binary_relation_exprt( - typecast_exprt::conditional_cast(sum, object_size_expr.type()), - op, - object_size_expr); + return binary_relation_exprt( + typecast_exprt::conditional_cast(object_offset, type), + ID_ge, + typecast_exprt::conditional_cast(object_size_expr, type)); + } } exprt object_lower_bound( diff --git a/src/util/replace_expr.cpp b/src/util/replace_expr.cpp index 9575c8abf65..1a0df0bef89 100644 --- a/src/util/replace_expr.cpp +++ b/src/util/replace_expr.cpp @@ -11,6 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com bool replace_expr(const exprt &what, const exprt &by, exprt &dest) { + PRECONDITION_WITH_DIAGNOSTICS( + what.type() == by.type(), + "types to be replaced should match. old type:\n" + what.type().pretty() + + "\nnew type:\n" + by.type().pretty()); + bool no_change = true; for(auto it = dest.depth_begin(), itend = dest.depth_end(); @@ -39,6 +44,11 @@ bool replace_expr(const replace_mapt &what, exprt &dest) replace_mapt::const_iterator findit = what.find(*it); if(findit != what.end()) { + PRECONDITION_WITH_DIAGNOSTICS( + it->type() == findit->second.type(), + "types to be replaced should match. old type:\n" + it->type().pretty() + + "\nnew type:\n" + findit->second.type().pretty()); + it.mutate() = findit->second; no_change = false; it.next_sibling_or_parent(); diff --git a/unit/util/pointer_expr.cpp b/unit/util/pointer_expr.cpp index 07fe9e725ca..6001773005c 100644 --- a/unit/util/pointer_expr.cpp +++ b/unit/util/pointer_expr.cpp @@ -10,14 +10,14 @@ TEST_CASE("pointer_offset_exprt", "[core][util]") { const exprt pointer = symbol_exprt{"foo", pointer_type(void_type())}; - const pointer_offset_exprt pointer_offset{pointer, signed_size_type()}; + const pointer_offset_exprt pointer_offset{pointer, size_type()}; SECTION("Is equivalent to free function.") { CHECK(::pointer_offset(pointer) == pointer_offset); } SECTION("Result type") { - CHECK(pointer_offset.type() == signed_size_type()); + CHECK(pointer_offset.type() == size_type()); } SECTION("Pointer operand accessor") {