From 286484208d320f89c2f5bfe4f4911462afa8bec8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 17 Jan 2023 12:25:16 +0000 Subject: [PATCH 1/5] Memory predicates test: avoid undefined behaviour There already is an assertion in place to guard against undefined behaviour. We shouldn't have to match on particular outcomes of undefined behaviour that occurs after that assertion. --- .../memory-predicates-is-fresh-failure-modes/main.c | 2 +- .../test-fail-none.desc | 8 +------- 2 files changed, 2 insertions(+), 8 deletions(-) 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..9c0119a554f 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 @@ -8,7 +8,7 @@ __CPROVER_assigns(__CPROVER_object_from(arr)) { __CPROVER_assert(arr != NULL, "arr is not NULL"); __CPROVER_assert(size < __CPROVER_max_malloc_size, "size is capped"); - if(size > 0) + 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$ From 47df3baa7f95ee8ba38f609ba3ccf93f88fe5325 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Jan 2023 13:11:05 +0000 Subject: [PATCH 2/5] Byte-operator lowering: ensure index type consistency We must not assume that byte-operator offsets and arrays indices use the same type (without at least checking that they do). Always use types available from the context, and type cast as needed. --- src/util/lower_byte_operators.cpp | 83 ++++++++++++++++++++++--------- 1 file changed, 60 insertions(+), 23 deletions(-) diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index c42c1bbd2cc..16cc9d6e98d 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()); @@ -1727,6 +1755,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 +1892,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 +1931,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 +1969,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 +1982,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( From 9b6d003b59312f315259d0c4504831af0a78daf8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Jan 2023 13:12:41 +0000 Subject: [PATCH 3/5] replace_expr: check type consistency Make sure that replace_expr cannot introduce type-inconsistent expressions. This wouldn't be a fault of replace_expr, but rather requires fixing the caller. Add preconditions to check this. --- src/util/replace_expr.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) 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(); From f8cc13a88e81e1a20c9c40645a8198e8e5996b9e Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 27 May 2022 11:15:34 +0300 Subject: [PATCH 4/5] make pointer_offset_exprt unsigned This commit changes the type of __CPROVER_POINTER_OFFSET from ssize_t to size_t. To match, relational operators on pointers are now unsigned, to enable p+PTRDIFF_MAX+1 > p. The rationale is subtle. The ISO C 11 standard 6.5.8 par 5 suggests that a pair of pointers can be compared if either the pointers point into the object, or one beyond the end of the sequence. The behavior in the case of a pointer that points before the sequence is undefined. There is a similar narrative for pointer arithmetic. A pointer with an offset that has a set most significant bit should thus compare "less than" a pointer with an offset that has a zero MSB. This suggests an unsigned encoding. --- .../pointers-conversions/byte_update.desc | 2 +- regression/cbmc-library/free-01/test.desc | 2 +- .../test-c-with-string-abstraction.desc | 2 +- .../pointer-offset-01/test-no-cp.desc | 8 ++-- .../pointer-offset-01/test.desc | 14 +++--- .../cbmc/address_space_size_limit3/test.desc | 2 +- regression/cbmc/memory_allocation2/test.desc | 6 +-- regression/cbmc/pointer-offset-01/main.c | 38 +++++++++++++++ regression/cbmc/pointer-offset-01/test.desc | 14 ++++++ .../contracts/no_redudant_checks/test.desc | 5 +- .../test_dump.desc | 2 +- src/ansi-c/cprover_builtin_headers.h | 2 +- src/ansi-c/goto_check_c.cpp | 2 +- src/ansi-c/library/cprover_contracts.c | 2 +- src/cprover/bv_pointers_wide.cpp | 2 +- .../value_set_dereference.cpp | 14 ++++-- src/solvers/flattening/bv_pointers.cpp | 14 +++--- src/util/lower_byte_operators.cpp | 10 ++-- src/util/pointer_predicates.cpp | 47 ++++++++++++------- unit/util/pointer_expr.cpp | 4 +- 20 files changed, 134 insertions(+), 58 deletions(-) create mode 100644 regression/cbmc/pointer-offset-01/main.c create mode 100644 regression/cbmc/pointer-offset-01/test.desc 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/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..486a8fb8523 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -786,7 +786,7 @@ __CPROVER_HIDE:; 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) | 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 16cc9d6e98d..02986e1442a 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -1672,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 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/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") { From 7cb83c11ccc1535a0174b31018e10ca7637a33a8 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Tue, 17 Jan 2023 19:48:04 +0000 Subject: [PATCH 5/5] CONTRACTS: take unsigned offsets into account --- .../main.c | 4 +- .../main.c | 6 +-- src/ansi-c/library/cprover_contracts.c | 41 +++++++++---------- 3 files changed, 24 insertions(+), 27 deletions(-) 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 9c0119a554f..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 && size < __CPROVER_max_malloc_size) + __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-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/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 486a8fb8523..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_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; }