diff --git a/library/kani/src/vec.rs b/library/kani/src/vec.rs index 5deb90d0ec14..626d152f02d4 100644 --- a/library/kani/src/vec.rs +++ b/library/kani/src/vec.rs @@ -1,6 +1,6 @@ // 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() -> Vec @@ -8,12 +8,18 @@ where T: Arbitrary, [(); std::mem::size_of::<[T; MAX_LENGTH]>()]:, { - let mut v = exact_vec::(); - 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::(), + _ => { + let mut any_vec = exact_vec::(); + 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. diff --git a/tests/expected/any_vec/exact_length.expected b/tests/expected/any_vec/exact_length.expected new file mode 100644 index 000000000000..641db7843ff1 --- /dev/null +++ b/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 diff --git a/tests/expected/any_vec/exact_length.rs b/tests/expected/any_vec/exact_length.rs new file mode 100644 index 000000000000..999e6cd7d1c7 --- /dev/null +++ b/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::(); + 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::(); + assert_eq!(data.len(), 17); + assert_eq!(data.capacity(), data.len()); + + let val = unsafe { *data.get_unchecked(17) }; + kani::cover!(val.0 == 0); +} diff --git a/tests/expected/any_vec/out_bounds.expected b/tests/expected/any_vec/out_bounds.expected new file mode 100644 index 000000000000..167fefe6d6f4 --- /dev/null +++ b/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 + + diff --git a/tests/expected/any_vec/out_bounds.rs b/tests/expected/any_vec/out_bounds.rs new file mode 100644 index 000000000000..a41813a3ae12 --- /dev/null +++ b/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` +//! +extern crate kani; +use kani::cover; + +#[kani::proof] +#[kani::unwind(22)] +fn check_always_out_bounds() { + let data = kani::vec::any_vec::(); + + // 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); +}