Spurious failure in pointer offset

[zhassan-aws]

I tried this code:

#[kani::proof]
fn check_foo() {
    let x: u8 = 0;
    let ptr: *const u8 = &x as *const u8;
    let count = isize::MAX - 800;
    let _ = ptr.wrapping_offset(count);
}

using the following command line invocation:

kani lib.rs

with Kani version: fe17fdc

I expected to see this happen: Verification successful.

Instead, this happened: Verification failed:

RESULTS:
Check 1: std::ptr::const_ptr::<impl *const u8>::wrapping_offset.arithmetic_overflow.1
         - Status: SUCCESS
         - Description: "arith_offset: attempt to compute number in bytes which would overflow"
         - Location: ../../../.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:481:18 in function std::ptr::const_ptr::<impl *const u8>::wrapping_offset

Check 2: std::ptr::const_ptr::<impl *const u8>::wrapping_offset.arithmetic_overflow.2
         - Status: FAILURE
         - Description: "attempt to compute offset which would overflow"
         - Location: ../../../.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:481:18 in function std::ptr::const_ptr::<impl *const u8>::wrapping_offset

Check 3: check_foo.assertion.1
         - Status: SUCCESS
         - Description: "attempt to subtract with overflow"
         - Location: lib.rs:5:17 in function check_foo


SUMMARY:
 ** 1 of 3 failed
Failed Checks: attempt to compute offset which would overflow
 File: "/home/ubuntu/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs", line 481, in std::ptr::const_ptr::<impl *const u8>::wrapping_offset

VERIFICATION:- FAILED

[zhassan-aws]

I get a similar failure if using offset as well, which should fail due to the pointer going out of bounds, but not due to an overflow in the computation of the number of bytes (since size_of::<u8> is 1):

#[kani::proof]
fn check_foo() {
    let x: u8 = 0;
    let ptr: *const u8 = &x as *const u8;
    let count = isize::MAX - 800;
    let _ = unsafe { ptr.offset(count) };
}

RESULTS:
Check 1: check_foo.assertion.1
         - Status: SUCCESS
         - Description: "attempt to subtract with overflow"
         - Location: lib.rs:5:17 in function check_foo

Check 2: std::ptr::const_ptr::<impl *const u8>::offset.arithmetic_overflow.1
         - Status: FAILURE
         - Description: "offset: attempt to compute number in bytes which would overflow"
         - Location: ../../../.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:399:18 in function std::ptr::const_ptr::<impl *const u8>::offset

Check 3: std::ptr::const_ptr::<impl *const u8>::offset.arithmetic_overflow.2
         - Status: SUCCESS
         - Description: "attempt to compute offset which would overflow"
         - Location: ../../../.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:399:18 in function std::ptr::const_ptr::<impl *const u8>::offset


SUMMARY:
 ** 1 of 3 failed
Failed Checks: offset: attempt to compute number in bytes which would overflow
 File: "/home/ubuntu/.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs", line 399, in std::ptr::const_ptr::<impl *const u8>::offset

VERIFICATION:- FAILED

[zhassan-aws]

The generated C indicates that we're computing the size of the pointer as opposed to the size of the pointee:

unsigned char * std::ptr::const_ptr::<impl *const u8>::offset(unsigned char *self, long int count)
{
  unsigned char *var_0;

bb0:
  ;
  unsigned char *tmp_statement_expression;
  /* offset: attempt to compute number in bytes which would overflow */
  assert(!overflow("*", long int, count, (long int)sizeof(unsigned char *) /*8*/ ));

It should be sizeof(unsigned char).

[zhassan-aws]

Unfortunately, Kani's incorrect encoding of the pointer arithmetic overflow check could lead to a soundness issue.

For instance, on the following program:

use std::convert::TryFrom;

struct Foo {
    arr: [i32; 4096],
}

#[cfg_attr(kani, kani::proof)]
fn main() {
    let f = Foo { arr: [0; 4096] };
    assert_eq!(std::mem::size_of::<Foo>(), 16384);
    // a large enough count that causes `count * size_of::<Foo>()` to overflow
    // `isize` without overflowing `usize`
    let count: usize = 562949953421320;
    // the `unwrap` ensures that it indeed doesn't overflow `usize`
    let bytes = count.checked_mul(std::mem::size_of::<Foo>()).unwrap();
    // ensure that it overflows `isize`:
    assert!(isize::try_from(bytes).is_err());

    let ptr: *const Foo = &f as *const Foo;
    // this should fail because `count * size_of::<Foo>` overflows `isize`
    let _p = unsafe { ptr.offset(count as isize) };
}

Verification incorrectly succeeds:

SUMMARY:
 ** 0 of 13 failed

VERIFICATION:- SUCCESSFUL

whereas MIRI points out the overflow:

error: Undefined Behavior: overflowing pointer arithmetic: the total offset in bytes does not fit in an `isize`
  --> src/main.rs:21:23
   |
21 |     let _p = unsafe { ptr.offset(count as isize) };
   |                       ^^^^^^^^^^^^^^^^^^^^^^^^^^ overflowing pointer arithmetic: the total offset in bytes does not fit in an `isize`
   |
   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
   = note: BACKTRACE:
   = note: inside `main` at src/main.rs:21:23: 21:49

The generated C indicates that the overflow expression is in terms of the size of Foo* as opposed to Foo:

struct Foo * std::ptr::const_ptr::<impl *const Foo>::offset(struct Foo *self, long int count)
{
  struct Foo *var_0;

bb0:
  ;
  struct Foo *tmp_statement_expression;
  /* offset: attempt to compute number in bytes which would overflow */
  assert(!overflow("*", long int, count, (long int)sizeof(struct Foo *) /*8*/ ));

[zhassan-aws]

Some remarks from an offline conversation with @tautschnig:

1. The reason why we're considering the failure with wrapping_offset to be spurious is that its documentation says the operation is always safe.
2. Internally, wrapping_offset is implemented in terms of the arith_offset intrinsic which is implemented in Kani using codegen_offset
3. While codegen_offset was previously used for implementing both the offset and arith_offset intrinsics, the offset intrinsic is now lowered to BinOp::Offset, so codegen_offset is now exclusively used for arith_offset
4. It's not clear whether an overflow in computing the number of bytes of an offset should cause a failure for wrapping_offset. Its documentation is not clear in that regard. I tried MIRI, and it doesn't report any issue even though count * 4 overflows:

fn main() {
    let x: i32 = 0;
    let ptr: *const i32 = &x as *const i32;
    let count = (isize::MAX / 4) + 1;
    println!("{ptr:?}");
    println!("{}", count.wrapping_mul(4));
    println!("{}", (count as usize) * 4);
    let p = ptr.wrapping_offset(count);
    println!("{p:?}");
}

$ cargo miri run
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.00s
     Running `/home/ubuntu/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/bin/cargo-miri runner target/miri/x86_64-unknown-linux-gnu/debug/disc-99-4`
0x26af0
-9223372036854775808
9223372036854775808
0x8000000000026af0

5. Based on that, I think we should at least remove the overflow check for the addition operation in codegen_offset, and perhaps also the overflow check for the multiplication operation.
6. For offset, the failure in the following program:

#[cfg_attr(kani, kani::proof)]
fn main() {
    let x: u8 = 0;
    let ptr: *const u8 = &x as *const u8;
    let count = isize::MAX - 10000;
    let _ = unsafe { ptr.offset(count) };
}

Check 2: std::ptr::const_ptr::<impl *const u8>::wrapping_offset.arithmetic_overflow.2
         - Status: FAILURE
         - Description: "attempt to compute offset which would overflow"
         - Location: ../../.rustup/toolchains/nightly-2024-10-03-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs:481:18 in function std::ptr::const_ptr::<impl *const u8>::wrapping_offset

is not spurious because depending on the value of the pointer, the addition operation could indeed overflow an isize.

[QinyuanWu]

@zhassan-aws For point 6, does that mean we shouldn't call self.as_ptr().offset(count as isize) in the contract when count = kani::any() because a large count value could overflow isize?

[zhassan-aws]

@QinyuanWu Yes. We should use wrapping_offset instead.