Kani misses out of bounds index for `get_unchecked` with raw pointer to slice

[carolynzech]

I tried this code:

#![feature(slice_ptr_get)]
use core::ptr::NonNull;

#[kani::proof]
fn out_of_bounds_get_unchecked() {
    const ARR_SIZE: usize = 10;
    let mut arr: [i32; ARR_SIZE] = kani::any();
    let ptr = NonNull::slice_from_raw_parts(
        NonNull::new(arr.as_mut_ptr()).unwrap(),
        ARR_SIZE,
    );

    unsafe {
        let _ = ptr.get_unchecked_mut(100000000);
    }
}

with Kani version: 0.56.0

I expected to see this happen: Verification failed because the index is out of bounds

Instead, this happened: Verification succeeded

[zhassan-aws]

This can be reproduced without NonNull as well:

#[kani::proof]
fn out_of_bounds_get_unchecked() {
    const ARR_SIZE: usize = 10;
    let mut arr: [i32; ARR_SIZE] = kani::any();
    let ptr = std::ptr::slice_from_raw_parts_mut(
        arr.as_mut_ptr(),
        ARR_SIZE,
    );

    unsafe {
        let _ = ptr.get_unchecked_mut(100);
    }
}

$ cargo kani
...
SUMMARY:
 ** 0 of 5 failed

VERIFICATION:- SUCCESSFUL

[celinval]

This doesn't seem related to slice_from_raw_parts though. This also succeeds See https://github.com/model-checking/kani/issues/3707#issuecomment-2471563366 example instead.

#[kani::proof]
fn out_of_bounds_get_unchecked() {
    const ARR_SIZE: usize = 10;
    let mut arr: [i32; ARR_SIZE] = kani::any();
    let ptr = std::ptr::slice_from_raw_parts_mut(
        arr.as_mut_ptr(),
        ARR_SIZE,
    );

    unsafe {
        let _ = ptr.get_unchecked_mut(100);
    }
}

[carolynzech]

This doesn't seem related to slice_from_raw_parts though. This also succeeds

#[kani::proof]
fn out_of_bounds_get_unchecked() {
    const ARR_SIZE: usize = 10;
    let mut arr: [i32; ARR_SIZE] = kani::any();
    let ptr = std::ptr::slice_from_raw_parts_mut(
        arr.as_mut_ptr(),
        ARR_SIZE,
    );

    unsafe {
        let _ = ptr.get_unchecked_mut(100);
    }
}

@celinval I'm confused -- this example also calls slice_from_raw_parts (the mutable version, but presumably these issues have similar root causes). I can broaden the title to talk about slice_from_raw_parts_mut too.

[celinval]

oops... wrong copy and paste.

#[kani::proof]
fn out_of_bounds_get_unchecked() {
    const ARR_SIZE: usize = 10;
    let mut arr: [i32; ARR_SIZE] = kani::any();
    let ptr = &mut arr as *mut _;

    unsafe {
        let i = ptr.get_unchecked_mut(100);
    }
}

[celinval]

I believe the issue here is similar to https://github.com/model-checking/kani/issues/1233. We had disabled bounds checks in some intrinsics a long time ago because the semantics were still up in the air when handling offset operations with count 0 and dangling pointers. However, the behavior is well defined, and we need enable those bounds checks again.

In the implementation of get_unchecked_mut, I believe the UB comes from invoking the pointer add, that will eventually invoke the offset intrinsic.