Kani does not flag out-of-bounds dereference with kani::vec::any_vec

[zhassan-aws]

I tried this code:

#[kani::proof]
fn main() {
    let v = kani::vec::any_vec::<u8, 2>();
    if v.len() == 1 {
        let x = unsafe { *v.as_slice().as_ptr().add(1) };
        println!("{x}");
    }
}

using the following command line invocation:

kani test.rs

with Kani version: 7136495

I expected to see this happen: Kani flags the out-of-bounds pointer dereference.

Instead, this happened: Verification is successful.

[zhassan-aws]

This unsoundness is similar to the one reported in #1009.

[arctic-alpaca]

Adding v.shrink_to(real_length); at https://github.com/model-checking/kani/blob/main/library/kani/src/vec.rs#L15 seems to fix this in my limited testing. I can't run the regression tests locally so I'm not sure whether this affects anything else.

[arctic-alpaca]

It should actually be possible to remove the unsafe part of any_vec() by replacing set_len() with truncate() :

Current impl:

pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
where
    T: Arbitrary,
    [(); std::mem::size_of::<[T; MAX_LENGTH]>()]:,
{
    let mut v = exact_vec::<T, MAX_LENGTH>();
    let real_length: usize = any();
    assume(real_length <= MAX_LENGTH);
    unsafe { v.set_len(real_length) };

    v
}

Proposed impl:

pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
where
    T: Arbitrary,
    [(); std::mem::size_of::<[T; MAX_LENGTH]>()]:,
{
    let mut v = exact_vec::<T, MAX_LENGTH>();
    let real_length: usize = any();
    assume(real_length <= MAX_LENGTH);
    v.truncate(real_length);
    v.shrink_to(real_length)

    v
}

Again only tested with the code from the first post in this issue.

[zhassan-aws]

Thanks @arctic-alpaca. The diff that I was going to propose is doing exactly that:

$ git diff
diff --git a/library/kani/src/vec.rs b/library/kani/src/vec.rs
index 5deb90d0ec1..4df6fafe457 100644
--- a/library/kani/src/vec.rs
+++ b/library/kani/src/vec.rs
@@ -11,7 +11,8 @@ pub fn any_vec<T, const MAX_LENGTH: usize>() -> Vec<T>
     let mut v = exact_vec::<T, MAX_LENGTH>();
     let real_length: usize = any();
     assume(real_length <= MAX_LENGTH);
-    unsafe { v.set_len(real_length) };
+    v.truncate(real_length);
+    v.shrink_to_fit();
 
     v
 }