Kani does not detect UB when generating an invalid slice reference from an invalid slice pointer

[celinval]

I tried this code:

//! Converting a raw pointer to a reference should trigger UB if the metadata is not valid.
#![feature(set_ptr_value)]

// Generate invalid fat pointer by incrementing the pointer address without adjusting the metadata.
#[kani::proof]
fn check_invalid_read() {
    let data = "hello";
    let ptr = data as *const str;
    // This should trigger UB since the metadata does not get adjusted.
    let val = unsafe { &*ptr.byte_add(1) };
    assert_eq!(val.len(), data.len());
}

// Generate invalid fat pointer by combining the metadata.
#[kani::proof]
fn check_with_metadata() {
    let short = [0u32; 2];
    let long = [0u32; 10];
    let ptr = &short as *const [u32];
    // This should trigger UB since the slice is not valid for the new length.
    let fake_long = unsafe { &*ptr.with_metadata_of(&long) };
    assert_eq!(fake_long.len(), long.len());
}

using the following command line invocation:

kani invalid_fat_reference.rs

with Kani version: 0.54.0-dev

I expected to see this happen: Both harnesses should fail due to UB. Note that both cases fail in MIRI.

Instead, this happened: Verification succeeds

[celinval]

I believe this is related to #2975, but we probably forgot to check for fat pointers.

[celinval]

Actually, Kani does find an error with the version of check_with_metadata described in the issue. But if you replace the array by a string slice, verification succeeds. 😮

#[kani::proof]
fn check_with_metadata() {
    let short = "sh";
    let long = "longer";
    let ptr = short as *const str;
    // This should trigger UB since the slice is not valid for the new length.
    let fake_long = unsafe { &*ptr.with_metadata_of(long) };
    assert_eq!(fake_long.len(), long.len());
}