Support pointer arithmetic in quantifier predicates

[feliperodri]

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

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.

[adpaco-aws]

You need to cast back to the original pointer type after the offset:

Suggested change

	let base = if is_byte { ptr.cast_to(Type::unsigned_int(8).to_pointer()) } else { ptr };
	return base.plus(offset);
	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(arguments[0].typ().clone()) } else { result };

It seems to be working now for some reason (maybe CBMC is doing it automatically?), but it might produce the wrong results in other cases.