Force any_vec capacity to match length (model-checking#2765)

library/kani/src/vec.rs

@@ -1,19 +1,25 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::{any, assume, Arbitrary};
+use crate::{any, any_where, Arbitrary};
 
 /// Generates an arbitrary vector whose length is at most MAX_LENGTH.
 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
+    let real_length: usize = any_where(|sz| *sz <= MAX_LENGTH);
+    match real_length {
+        0 => vec![],
+        exact if exact == MAX_LENGTH => exact_vec::<T, MAX_LENGTH>(),
+        _ => {
+            let mut any_vec = exact_vec::<T, MAX_LENGTH>();
+            any_vec.truncate(real_length);
+            any_vec.shrink_to_fit();
+            assert!(any_vec.capacity() == any_vec.len());
+            any_vec
+        }
+    }
 }
 
 /// Generates an arbitrary vector that is exactly EXACT_LENGTH long.

tests/expected/any_vec/exact_length.expected

@@ -0,0 +1,12 @@
+Checking harness check_access_length_17...
+
+Failed Checks: dereference failure: pointer outside object bounds\
+in check_access_length_17
+
+Checking harness check_access_length_zero...
+
+Failed Checks: dereference failure: pointer outside object bounds\
+in check_access_length_zero
+
+Verification failed for - check_access_length_17
+Verification failed for - check_access_length_zero

tests/expected/any_vec/exact_length.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test `exact_vec` API
+#[kani::proof]
+fn check_access_length_zero() {
+    let data = kani::vec::exact_vec::<u8, 0>();
+    assert_eq!(data.len(), 0);
+    assert_eq!(data.capacity(), data.len());
+    let val = unsafe { *data.get_unchecked(0) };
+    kani::cover!(val == 0);
+}
+
+#[derive(kani::Arbitrary, Copy, Clone)]
+struct Dummy(i32, u8);
+
+#[kani::proof]
+fn check_access_length_17() {
+    let data = kani::vec::exact_vec::<Dummy, 17>();
+    assert_eq!(data.len(), 17);
+    assert_eq!(data.capacity(), data.len());
+
+    let val = unsafe { *data.get_unchecked(17) };
+    kani::cover!(val.0 == 0);
+}

tests/expected/any_vec/out_bounds.expected

@@ -0,0 +1,61 @@
+check_always_out_bounds::check_0.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer NULL"\
+function check_always_out_bounds::check_0
+
+check_always_out_bounds::check_0.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+function check_always_out_bounds::check_0
+
+check_always_out_bounds::check_0.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: invalid integer address"\
+function check_always_out_bounds::check_0
+
+check_always_out_bounds::check_1.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+function check_always_out_bounds::check_1
+
+check_always_out_bounds::check_2.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+function check_always_out_bounds::check_2
+
+check_always_out_bounds::check_3.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+function check_always_out_bounds::check_3
+
+check_always_out_bounds::check_4.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+function check_always_out_bounds::check_4
+
+check_always_out_bounds::check_5.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+function check_always_out_bounds::check_5
+
+check_always_out_bounds::check_6.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+function check_always_out_bounds::check_6
+
+check_always_out_bounds::check_7.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+function check_always_out_bounds::check_7
+
+check_always_out_bounds::check_8.pointer_dereference\
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+function check_always_out_bounds::check_8
+
+check_always_out_bounds::check_9.cover\
+Status: UNREACHABLE\
+Description: "cover condition: *val == 0"\
+function check_always_out_bounds::check_9
+
+

tests/expected/any_vec/out_bounds.rs

@@ -0,0 +1,45 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Test for #2759: Kani does not flag out-of-bounds dereference with `kani::vec::any_vec`
+//! <https://github.com/model-checking/kani/issues/2759>
+extern crate kani;
+use kani::cover;
+
+#[kani::proof]
+#[kani::unwind(22)]
+fn check_always_out_bounds() {
+    let data = kani::vec::any_vec::<u8, 8>();
+
+    // Capacity must match length.
+    assert_eq!(data.capacity(), data.len());
+
+    // Create invalid reference.
+    let invalid = unsafe { data.get_unchecked(data.len()) };
+
+    macro_rules! cover_len {
+        ($fn_name:tt, $val:literal) => {
+            fn $fn_name(val: &u8) {
+                cover!(*val == 0);
+            }
+
+            if data.len() == $val {
+                $fn_name(invalid);
+            }
+        };
+    }
+
+    // Ensure any length between 0..=8 can trigger a failure.
+    cover_len!(check_0, 0);
+    cover_len!(check_1, 1);
+    cover_len!(check_2, 2);
+    cover_len!(check_3, 3);
+    cover_len!(check_4, 4);
+    cover_len!(check_5, 5);
+    cover_len!(check_6, 6);
+    cover_len!(check_7, 7);
+    cover_len!(check_8, 8);
+
+    // This shouldn't be covered.
+    cover_len!(check_9, 9);
+}