Support pointer arithmetic in quantifier predicates (#4583)

Lower wrapping pointer arithmetic intrinsics (`wrapping_add`,
`wrapping_byte_offset`) directly to CBMC pointer `Plus` expressions in
the pure expression inliner. These intrinsics have no GOTO body to
inline, so they need special handling.

## Problem

Quantifier predicates that dereference pointers with offsets — e.g.,
`*ptr.wrapping_byte_offset(i as isize)` — failed because the
`inline_as_pure_expr` inliner couldn't resolve pointer arithmetic
intrinsics. These functions have no body in the symbol table (they're
compiler intrinsics), so the inliner returned the original expression
unchanged, leaving unresolved function calls that CBMC rejected.

## Solution

In `inline_call_as_pure_expr` (`goto_ctx.rs`), before attempting to look
up the function body, check if the function name matches a known
wrapping pointer arithmetic intrinsic (`wrapping_add`,
`wrapping_byte_offset`). If so, directly emit `ptr.plus(offset)` — the
CBMC expression for pointer arithmetic. A type guard
(`arguments[0].typ().is_pointer()`) prevents misapplication to
non-pointer functions.

Non-wrapping variants (`offset`, `add`, `arith_offset`) are
intentionally excluded because they trigger CBMC bounds checks inside
quantifier bodies, which fail in the symbolic evaluation context.

## Example

```rust
kani::forall!(|i in (0, len)| unsafe { *ptr.wrapping_byte_offset(i as isize) == 0 })
```

## Changes

- `goto_ctx.rs`: Recognize wrapping pointer arithmetic intrinsics and
lower to `ptr.plus(offset)`
- `rfc/src/rfcs/0010-quantifiers.md`: Document pointer arithmetic
intrinsic lowering in the Detailed Design section
- `tests/kani/Quantifiers/pointer_arithmetic.rs`: 4 harnesses covering
`wrapping_byte_offset` (forall + exists) and `wrapping_add` (u32 + u8)

---

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: feliperodri

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -515,6 +515,56 @@ impl GotocCtx<'_, '_> {
             return original_expr.clone();
         }
 
+        // Lower known pointer arithmetic intrinsics directly to CBMC expressions.
+        // These intrinsics have no GOTO body to inline, so we handle them specially.
+        // We check that the function name contains a pointer-type path segment to
+        // avoid false-positives on user-defined functions with similar names.
+        //
+        // CBMC's pointer Plus scales the offset by the pointee size. So:
+        // - For element-offset variants (wrapping_add, wrapping_sub, wrapping_offset),
+        //   we apply Plus directly on the original pointer type (count is in elements of T).
+        // - For byte-offset variants (wrapping_byte_offset, wrapping_byte_add,
+        //   wrapping_byte_sub), we first cast the pointer to `*u8` so Plus scales by 1.
+        // - Sub variants negate the offset before adding.
+        //
+        // TODO: Replace name-based heuristic with a proper intrinsic registry
+        // (e.g., matching on DefId or a dedicated KaniIntrinsic enum) for
+        // robustness against mangling variations.
+        let fn_name = fn_id.to_string();
+        let is_ptr_fn = fn_name.contains("::ptr::") || fn_name.contains("const_ptr");
+        let ptr_op = if is_ptr_fn {
+            if fn_name.contains("wrapping_byte_offset") || fn_name.contains("wrapping_byte_add") {
+                Some((/*is_byte*/ true, /*is_sub*/ false))
+            } else if fn_name.contains("wrapping_byte_sub") {
+                Some((true, true))
+            } else if fn_name.contains("wrapping_add") || fn_name.contains("wrapping_offset") {
+                Some((false, false))
+            } else if fn_name.contains("wrapping_sub") {
+                Some((false, true))
+            } else {
+                None
+            }
+        } else {
+            None
+        };
+        if let Some((is_byte, is_sub)) = ptr_op
+            && arguments.len() >= 2
+            && arguments[0].typ().is_pointer()
+        {
+            let original_ptr_typ = arguments[0].typ().clone();
+            let ptr = self.inline_as_pure_expr(&arguments[0], visited);
+            let offset = self.inline_as_pure_expr(&arguments[1], visited);
+            let offset = if is_sub { offset.neg() } else { offset };
+            // For byte-offset variants, cast the pointer to `*u8` so CBMC's Plus
+            // scales the offset by 1 byte (matching the Rust semantics that
+            // first casts `self.cast::<u8>()`), then cast the result back to the
+            // original pointer type so the surrounding expression sees the
+            // expected type.
+            let base = if is_byte { ptr.cast_to(Type::unsigned_int(8).to_pointer()) } else { ptr };
+            let result = base.plus(offset);
+            return if is_byte { result.cast_to(original_ptr_typ) } else { result };
+        }
+
         let function_body = self.symbol_table.lookup(*fn_id).and_then(|sym| match &sym.value {
             SymbolValues::Stmt(stmt) => Some(stmt.clone()),
             _ => None,

rfc/src/rfcs/0010-quantifiers.md

@@ -234,6 +234,19 @@ To solve this, Kani generates **pure expression trees** for quantifier bodies:
    are inlined by looking up the function body in the symbol table, resolving its
    return expression, and substituting parameters — producing a pure expression.
 
+5. **Pointer arithmetic intrinsic lowering**: Wrapping pointer arithmetic functions
+   (`wrapping_add`, `wrapping_sub`, `wrapping_offset`, `wrapping_byte_offset`,
+   `wrapping_byte_add`, `wrapping_byte_sub`) are compiler intrinsics with no GOTO
+   body to inline. The inliner recognizes these by name and lowers them directly to
+   CBMC pointer `Plus` expressions. Since CBMC's pointer `Plus` scales the offset by
+   the pointee size, byte-offset variants first cast the pointer to `*u8` so the
+   scaling is by 1 byte, and `sub` variants negate the offset before adding.
+   Non-wrapping variants (`offset`, `add`) are not supported because they trigger
+   CBMC bounds checks inside quantifier bodies. Example:
+   ```rust
+   kani::forall!(|i in (0, len)| unsafe { *ptr.wrapping_byte_offset(i as isize) == 0 })
+   ```
+
 ### Typed quantifier variables
 
 The `forall!` and `exists!` macros support an optional type annotation:

tests/kani/Quantifiers/pointer_arithmetic.rs

@@ -0,0 +1,91 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z quantifiers
+
+//! Tests for pointer arithmetic inside quantifier predicates.
+//! These exercise the intrinsic lowering in `inline_call_as_pure_expr`
+//! which converts wrapping_byte_offset/wrapping_add to CBMC Plus.
+//!
+//! Quantifier ranges are half-open: `|i in (lo, hi)|` means `lo <= i < hi`.
+//! All ranges below match the array lengths to stay in-bounds.
+
+#[kani::proof]
+fn check_wrapping_byte_offset_forall() {
+    let arr: [u8; 8] = [0; 8];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(kani::forall!(|i in (0, 8)| *ptr.wrapping_byte_offset(i as isize) == 0));
+    }
+}
+
+#[kani::proof]
+fn check_wrapping_byte_offset_exists() {
+    let arr: [u8; 8] = [0, 0, 0, 42, 0, 0, 0, 0];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(kani::exists!(|i in (0, 8)| *ptr.wrapping_byte_offset(i as isize) == 42));
+    }
+}
+
+#[kani::proof]
+fn check_wrapping_add_forall() {
+    let arr: [u32; 4] = [10, 20, 30, 40];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(kani::forall!(|i in (0, 4)| *ptr.wrapping_add(i) >= 10));
+    }
+}
+
+/// Tests `ptr.wrapping_add(i)` with a different element type (u8 vs u32).
+#[kani::proof]
+fn check_wrapping_add_u8_forall() {
+    let arr: [u8; 4] = [1, 2, 3, 4];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(kani::forall!(|i in (0, 4)| *ptr.wrapping_add(i) > 0));
+    }
+}
+
+#[kani::proof]
+fn check_wrapping_add_exists() {
+    let arr: [u32; 4] = [10, 20, 30, 40];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(kani::exists!(|i in (0, 4)| *ptr.wrapping_add(i) == 30));
+    }
+}
+
+/// Tests `wrapping_byte_offset` on a non-`u8` pointee.
+/// Each `u32` is 4 bytes, so valid byte offsets are 0, 4, 8, 12.
+/// This catches a bug where the offset was scaled by the pointee size
+/// (would scale by 4) instead of by 1 (bytes).
+#[kani::proof]
+fn check_wrapping_byte_offset_u32() {
+    let arr: [u32; 4] = [0x11111111, 0x22222222, 0x33333333, 0x44444444];
+    let ptr = arr.as_ptr();
+    unsafe {
+        assert!(
+            kani::forall!(|i in (0, 4)| *ptr.wrapping_byte_offset((i * 4) as isize) >= 0x11111111)
+        );
+    }
+}
+
+#[kani::proof]
+fn check_wrapping_sub_forall() {
+    let arr: [u32; 4] = [10, 20, 30, 40];
+    let end_ptr = unsafe { arr.as_ptr().add(4) };
+    unsafe {
+        // end_ptr.wrapping_sub(i) for i in 1..=4 points to arr[4-i]
+        assert!(kani::forall!(|i in (1, 5)| *end_ptr.wrapping_sub(i) >= 10));
+    }
+}
+
+#[kani::proof]
+fn check_wrapping_byte_sub_forall() {
+    let arr: [u32; 4] = [10, 20, 30, 40];
+    let end_ptr = unsafe { arr.as_ptr().add(4) };
+    unsafe {
+        // 4-byte stride: end_ptr.wrapping_byte_sub(i*4) for i in 1..=4
+        assert!(kani::forall!(|i in (1, 5)| *end_ptr.wrapping_byte_sub(i * 4) >= 10));
+    }
+}