diff --git a/regression/cbmc/pointer-arithmetic-offset-wrap-nondet/main.c b/regression/cbmc/pointer-arithmetic-offset-wrap-nondet/main.c new file mode 100644 index 00000000000..6bd1352348c --- /dev/null +++ b/regression/cbmc/pointer-arithmetic-offset-wrap-nondet/main.c @@ -0,0 +1,27 @@ +#include +#include + +int main() +{ + char x, y; + char *p = &x; + char *p2 = &y; + uint64_t k; + + char *w1 = p + k; + char *w2 = p2 + k; + + if(k == (1ULL << 48)) + { + // Pointer arithmetic whose result offset does not fit the offset field + // yields a pointer to an unknown (nondeterministic) address: neither + // equality nor inequality between two such pointers is provable. In + // particular, equality must NOT be provable (identically-shifted + // pointers into disjoint objects are never equal under any concrete + // address assignment). + assert(w1 == w2); + assert(w1 != w2); + } + + return 0; +} diff --git a/regression/cbmc/pointer-arithmetic-offset-wrap-nondet/test.desc b/regression/cbmc/pointer-arithmetic-offset-wrap-nondet/test.desc new file mode 100644 index 00000000000..28e15c78fdd --- /dev/null +++ b/regression/cbmc/pointer-arithmetic-offset-wrap-nondet/test.desc @@ -0,0 +1,16 @@ +CORE no-new-smt +main.c +--object-bits 16 +^\[main.assertion.1\] line \d+ assertion w1 == w2: FAILURE$ +^\[main.assertion.2\] line \d+ assertion w1 != w2: FAILURE$ +^\*\* 2 of \d+ failed +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Out-of-encoding-range pointer arithmetic results have nondeterministic +addresses; both equality and inequality of two such pointers must be +refutable (provable equality would be unsound: disjoint objects shifted +identically never collide under any concrete address assignment). diff --git a/regression/cbmc/pointer-arithmetic-offset-wrap/main.c b/regression/cbmc/pointer-arithmetic-offset-wrap/main.c new file mode 100644 index 00000000000..837129c11f4 --- /dev/null +++ b/regression/cbmc/pointer-arithmetic-offset-wrap/main.c @@ -0,0 +1,29 @@ +#include +#include + +int main() +{ + char x; + char *p = &x; + uint64_t k; + + char *r = p + k; + + // The propositional encoding used to wrap pointer offsets at + // 2^(pointer_width - object_bits), making r alias p for k a non-zero + // multiple of that value, while the simplifier and constant propagation + // compute pointer arithmetic in full-width arithmetic. Both must agree + // that adding a non-zero k (modulo the full address width) yields a + // different pointer. + if(k == (1ULL << 48)) + assert(r != p); + + if(k != 0) + assert(r != p); + + // Constant-offset variant (folded by constant propagation). + char *q = p + (1ULL << 48); + assert(q != p); + + return 0; +} diff --git a/regression/cbmc/pointer-arithmetic-offset-wrap/test.desc b/regression/cbmc/pointer-arithmetic-offset-wrap/test.desc new file mode 100644 index 00000000000..fbecbbca4f6 --- /dev/null +++ b/regression/cbmc/pointer-arithmetic-offset-wrap/test.desc @@ -0,0 +1,13 @@ +CORE no-new-smt +main.c +--object-bits 16 +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Pointer arithmetic whose result offset does not fit the offset field of the +pointer encoding must not silently wrap around within the object; the result +is directed to the invalid object instead, keeping the propositional encoding +consistent with the simplifier's full-width pointer arithmetic. diff --git a/regression/cbmc/pointer-overflow3/no-simplify.desc b/regression/cbmc/pointer-overflow3/no-simplify.desc index da08a190e50..bd3ff5ec5b5 100644 --- a/regression/cbmc/pointer-overflow3/no-simplify.desc +++ b/regression/cbmc/pointer-overflow3/no-simplify.desc @@ -2,10 +2,11 @@ CORE no-new-smt main.c --no-malloc-may-fail --pointer-overflow-check --no-simplify ^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ (\(signed (long (long )?)?int\))?10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer invalid in p - (\(signed (long (long )?)?int\))?10: FAILURE ^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - (\(signed (long (long )?)?int\))?10: FAILURE ^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ (\(signed (long (long )?)?int\))?10: FAILURE ^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - (\(signed (long (long )?)?int\))?10: FAILURE -^\*\* 4 of \d+ failed +^\*\* 5 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 52482e8b060..4526ebcf80c 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -483,8 +483,11 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) count == 1, "there should be exactly one pointer-type operand in a pointer-type sum"); - const std::size_t offset_bits = get_offset_width(type); - bvt sum = bv_utils.build_constant(0, offset_bits); + // Sum the integer operands at full address width; offsets that do not + // fit the pointer encoding's offset field are detected in + // offset_arithmetic below rather than being silently truncated here. + const std::size_t address_bits = get_address_width(type); + bvt sum = bv_utils.build_constant(0, address_bits + 1); for(const auto &operand : plus_expr.operands()) { @@ -505,9 +508,13 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) bvt op = convert_bv(operand); CHECK_RETURN(!op.empty()); - op = bv_utils.extension(op, offset_bits, rep); + if(op.size() < sum.size()) + op = bv_utils.extension(op, sum.size(), rep); + else if(op.size() > sum.size()) + sum = bv_utils.extension( + sum, op.size(), bv_utilst::representationt::SIGNED); - sum=bv_utils.add(sum, op); + sum = bv_utils.add(sum, op); } return offset_arithmetic(type, bv, size, sum); @@ -804,10 +811,13 @@ bvt bv_pointerst::offset_arithmetic( const bvt &bv, const mp_integer &x) { - const std::size_t offset_bits = get_offset_width(type); + // Build the constant at full address width so that offsets that do not + // fit the pointer encoding's offset field are not silently truncated; + // offset_arithmetic below detects them instead. + const std::size_t address_bits = get_address_width(type); return offset_arithmetic( - type, bv, 1, bv_utils.build_constant(x, offset_bits)); + type, bv, 1, bv_utils.build_constant(x, address_bits + 1)); } bvt bv_pointerst::offset_arithmetic( @@ -822,8 +832,11 @@ bvt bv_pointerst::offset_arithmetic( index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED: bv_utilst::representationt::UNSIGNED; - const std::size_t offset_bits = get_offset_width(type); - bv_index=bv_utils.extension(bv_index, offset_bits, rep); + // Extend rather than truncate: offsets that do not fit the pointer + // encoding's offset field are detected in offset_arithmetic below. + const std::size_t address_bits = get_address_width(type); + bv_index = bv_utils.extension( + bv_index, std::max(bv_index.size(), address_bits) + 1, rep); return offset_arithmetic(type, bv, factor, bv_index); } @@ -844,8 +857,11 @@ bvt bv_pointerst::offset_arithmetic( bv_index = bv_utils.multiplier(bv_index, bv_factor, rep); - const std::size_t offset_bits = get_offset_width(type); - bv_index = bv_utils.extension(bv_index, offset_bits, rep); + // Extend rather than truncate: offsets that do not fit the pointer + // encoding's offset field are detected in offset_arithmetic below. + const std::size_t address_bits = get_address_width(type); + bv_index = bv_utils.extension( + bv_index, std::max(bv_index.size(), address_bits) + 1, rep); return offset_arithmetic(type, bv, 1, bv_index); } @@ -867,13 +883,53 @@ bvt bv_pointerst::offset_arithmetic( } const std::size_t offset_bits = get_offset_width(type); - bv_index = bv_utils.zero_extension(bv_index, offset_bits); - bvt offset_bv = offset_literals(bv, type); - - bvt bv_tmp = bv_utils.add(offset_bv, bv_index); + // Perform the addition at a width that can represent the mathematical + // result: any offset that does not fit the offset field of the pointer + // encoding must not silently wrap around within the object (the + // simplifier and constant propagation compute pointer arithmetic in + // full-width arithmetic, and silent wrap-around makes the propositional + // encoding disagree with them; see + // https://github.com/model-checking/kani/issues/1150). Instead, direct + // any out-of-range result to the "invalid object", mirroring what the + // integer-to-pointer conversion does for unknown addresses. + const std::size_t ext_bits = std::max(bv_index.size(), offset_bits) + 1; + + // The index is a signed quantity (negative offsets move towards the + // start of the object); the current offset is unsigned. + bvt bv_index_ext = + bv_utils.extension(bv_index, ext_bits, bv_utilst::representationt::SIGNED); - return object_offset_encoding(object_literals(bv, type), bv_tmp); + bvt offset_bv = offset_literals(bv, type); + bvt offset_ext = bv_utils.extension( + offset_bv, ext_bits, bv_utilst::representationt::UNSIGNED); + + bvt sum_ext = bv_utils.add(offset_ext, bv_index_ext); + + // The result is representable iff the extension bits (all bits from + // offset_bits upwards, including the sign bit) are zero. + bvt high_bits(sum_ext.begin() + offset_bits, sum_ext.end()); + literalt overflow = prop.lor(high_bits); + + bvt bv_tmp(sum_ext.begin(), sum_ext.begin() + offset_bits); + + // On overflow, replace the object by the invalid object and the offset by + // a nondeterministic value: the result is a pointer to an unknown address. + // Keeping the truncated offset would identify identically-shifted pointers + // into *different* objects (both would encode as the invalid object with + // the same offset), proving equalities that do not hold under any concrete + // address assignment. With a nondeterministic offset, neither equality nor + // inequality between such pointers is provable, matching the intended + // semantics that the address of an out-of-range pointer is unconstrained. + bvt object_bv = object_literals(bv, type); + bvt invalid_object_bv = + object_literals(encode(pointer_logic.get_invalid_object(), type), type); + bvt new_object_bv = bv_utils.select(overflow, invalid_object_bv, object_bv); + + bvt nondet_offset_bv = prop.new_variables(offset_bits); + bvt new_offset_bv = bv_utils.select(overflow, nondet_offset_bv, bv_tmp); + + return object_offset_encoding(new_object_bv, new_offset_bv); } bvt bv_pointerst::add_addr(const exprt &expr)