Merge branch 'main' into toolchain-2023-09-15-manual

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);
+}