From 70094e0bcde12e07231810bd1c88c826eaa0a04c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 22 Jul 2026 19:04:03 +0000 Subject: [PATCH 1/2] Do not silently wrap pointer offsets in the propositional encoding The propositional encoding packs pointers into object bits and offset bits, and performed pointer arithmetic on the offset field only: any result offset outside [0, 2^offset_bits) silently wrapped around within the same object. The simplifier and constant propagation, however, compute pointer arithmetic in full-width arithmetic, so semantically identical programs produced contradictory verification results depending on whether the arithmetic was constant-folded, e.g.: char x, *p = &x; uint64_t k; char *r = p + k; if(k == (1ULL << 48)) assert(r != p); // was: refuted (with 16 object bits) char *q = p + (1ULL << 48); assert(q != p); // was: proved This inconsistency also defeated out-of-bounds checks built on top of the encoding: Kani's pointer-offset UB check missed genuine out-of-bounds offsets that are multiples of 2^(64 - object_bits) because the wrapped pointer aliased the base pointer and thus passed a same-allocation check (https://github.com/model-checking/kani/issues/1150). Perform offset arithmetic at full address width instead and, when the mathematical result does not fit the offset field, direct the result to the invalid object, mirroring what integer-to-pointer conversion does for unknown addresses. Out-of-encoding-range results thereby compare unequal to every pointer into the original object, consistent with full-width arithmetic, and is_invalid_pointer now correctly identifies them - pointer-overflow-check's "pointer invalid" assertion in regression/cbmc/pointer-overflow3 now fails for `p - 10` on a 5-element allocation, which is reflected in the updated test expectations. Co-authored-by: Kiro --- .../pointer-arithmetic-offset-wrap/main.c | 29 ++++++++ .../pointer-arithmetic-offset-wrap/test.desc | 13 ++++ .../cbmc/pointer-overflow3/no-simplify.desc | 3 +- src/solvers/flattening/bv_pointers.cpp | 73 +++++++++++++++---- 4 files changed, 104 insertions(+), 14 deletions(-) create mode 100644 regression/cbmc/pointer-arithmetic-offset-wrap/main.c create mode 100644 regression/cbmc/pointer-arithmetic-offset-wrap/test.desc 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..48c2f6b1d11 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,44 @@ 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); + + // 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); 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); - bvt bv_tmp = bv_utils.add(offset_bv, bv_index); + // On overflow, replace the object by the invalid object so that the + // result compares unequal to any pointer into the original object. + 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); - return object_offset_encoding(object_literals(bv, type), bv_tmp); + return object_offset_encoding(new_object_bv, bv_tmp); } bvt bv_pointerst::add_addr(const exprt &expr) From 22821644f33f8220fbcb4c12bd3b8f0c22516aac Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Jul 2026 11:40:36 +0000 Subject: [PATCH 2/2] Make out-of-range pointer-arithmetic offsets nondeterministic The previous commit directed pointer-arithmetic results whose offset does not fit the pointer encoding's offset field to the invalid object, but kept the truncated offset. Two identically-shifted pointers into *different* objects thereby received bit-identical encodings, making their equality provable: char x, y, *p = &x, *p2 = &y; uint64_t k; char *w1 = p + k, *w2 = p2 + k; if(k == (1ULL << 48)) assert(w1 == w2); // was: proved (16 object bits) No concrete address assignment can make disjoint objects shifted by the same amount collide, so proving this equality is unsound. Use a nondeterministic offset for out-of-range results instead: such a pointer now has an unknown address, so neither equality nor inequality between two of them is provable, and all previously established properties (inequality with any pointer into the original object, is_invalid_pointer identification) are preserved. This matches the overall model in which object base addresses are chosen arbitrarily and the address of an out-of-range pointer is unconstrained. Co-authored-by: Kiro --- .../main.c | 27 +++++++++++++++++++ .../test.desc | 16 +++++++++++ src/solvers/flattening/bv_pointers.cpp | 15 ++++++++--- 3 files changed, 55 insertions(+), 3 deletions(-) create mode 100644 regression/cbmc/pointer-arithmetic-offset-wrap-nondet/main.c create mode 100644 regression/cbmc/pointer-arithmetic-offset-wrap-nondet/test.desc 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/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 48c2f6b1d11..4526ebcf80c 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -913,14 +913,23 @@ bvt bv_pointerst::offset_arithmetic( bvt bv_tmp(sum_ext.begin(), sum_ext.begin() + offset_bits); - // On overflow, replace the object by the invalid object so that the - // result compares unequal to any pointer into the original object. + // 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); - return object_offset_encoding(new_object_bv, bv_tmp); + 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)