Do not silently wrap pointer offsets in the propositional encoding

regression/cbmc/pointer-arithmetic-offset-wrap-nondet/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdint.h>
+
+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;
+}

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).

regression/cbmc/pointer-arithmetic-offset-wrap/main.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+#include <stdint.h>
+
+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;
+}

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.

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$

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)