diff --git a/CHANGELOG.md b/CHANGELOG.md index ff4343d5f3b2..d93685e865be 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,12 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. +## [0.41.0] + +### Breaking Changes + +* Delete `any_slice` which has been deprecated since Kani 0.38.0. by @zhassan-aws in https://github.com/model-checking/kani/pull/2860 + ## [0.40.0] ### What's Changed diff --git a/library/kani/src/slice.rs b/library/kani/src/slice.rs index 27a4a6a5d8fd..1b13de29d589 100644 --- a/library/kani/src/slice.rs +++ b/library/kani/src/slice.rs @@ -1,8 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::{any, assume, Arbitrary}; -use std::alloc::{alloc, dealloc, Layout}; -use std::ops::{Deref, DerefMut}; +use crate::{any, assume}; /// Given an array `arr` of length `LENGTH`, this function returns a **valid** /// slice of `arr` with non-deterministic start and end points. This is useful @@ -34,117 +32,3 @@ fn any_range() -> (usize, usize) { assume(from <= to); (from, to) } - -/// A struct that stores a slice of type `T` with a non-deterministic length -/// between `0..=MAX_SLICE_LENGTH` and with non-deterministic content. This is -/// useful in situations where one wants to verify that all slices with any -/// content and with a length up to `MAX_SLICE_LENGTH` satisfy a certain -/// property. Use `any_slice` to create an instance of this struct. -/// -/// # Example: -/// -/// ```rust -/// let slice: kani::slice::AnySlice = kani::slice::any_slice(); -/// foo(&slice); // where foo is a function that takes a slice and verifies a property about it -/// ``` -#[deprecated( - since = "0.38.0", - note = "Use `any_slice_of_array` or `any_slice_of_array_mut` instead" -)] -pub struct AnySlice { - layout: Layout, - ptr: *mut T, - slice_len: usize, -} - -#[allow(deprecated)] -impl AnySlice { - fn new() -> Self - where - T: Arbitrary, - { - let any_slice = AnySlice::::alloc_slice(); - unsafe { - let mut i = 0; - // Note: even though the guard `i < MAX_SLICE_LENGTH` is redundant - // since the assumption above guarantees that `slice_len` <= - // `MAX_SLICE_LENGTH`, without it, CBMC fails to infer the required - // unwind value, and requires specifying one, which is inconvenient. - // CBMC also fails to infer the unwinding if the loop is simply - // written as: - // for i in 0..slice_len { - // *(ptr as *mut T).add(i) = any(); - // } - while i < any_slice.slice_len && i < MAX_SLICE_LENGTH { - std::ptr::write(any_slice.ptr.add(i), any()); - i += 1; - } - } - any_slice - } - - fn alloc_slice() -> Self { - let slice_len = any(); - assume(slice_len <= MAX_SLICE_LENGTH); - let layout = Layout::array::(slice_len).unwrap(); - let ptr = if slice_len == 0 { std::ptr::null() } else { unsafe { alloc(layout) } }; - Self { layout, ptr: ptr as *mut T, slice_len } - } - - pub fn get_slice(&self) -> &[T] { - if self.slice_len == 0 { - &[] - } else { - unsafe { std::slice::from_raw_parts(self.ptr, self.slice_len) } - } - } - - pub fn get_slice_mut(&mut self) -> &mut [T] { - if self.slice_len == 0 { - &mut [] - } else { - unsafe { std::slice::from_raw_parts_mut(self.ptr, self.slice_len) } - } - } -} - -#[allow(deprecated)] -impl Drop for AnySlice { - fn drop(&mut self) { - if self.slice_len > 0 { - assert!(!self.ptr.is_null()); - unsafe { - dealloc(self.ptr as *mut u8, self.layout); - } - } - } -} - -#[allow(deprecated)] -impl Deref for AnySlice { - type Target = [T]; - - fn deref(&self) -> &Self::Target { - self.get_slice() - } -} - -#[allow(deprecated)] -impl DerefMut for AnySlice { - fn deref_mut(&mut self) -> &mut Self::Target { - self.get_slice_mut() - } -} - -#[deprecated( - since = "0.38.0", - note = "Use `any_slice_of_array` or `any_slice_of_array_mut` instead" -)] -#[allow(deprecated)] -pub fn any_slice() -> AnySlice -where - T: Arbitrary, -{ - #[allow(deprecated)] - AnySlice::::new() -} diff --git a/tests/ui/any-slice-deprecated/expected b/tests/ui/any-slice-deprecated/expected deleted file mode 100644 index db7d5dc3e970..000000000000 --- a/tests/ui/any-slice-deprecated/expected +++ /dev/null @@ -1,2 +0,0 @@ -warning: use of deprecated function `kani::slice::any_slice`: Use `any_slice_of_array` or `any_slice_of_array_mut` instead -warning: use of deprecated struct `kani::slice::AnySlice`: Use `any_slice_of_array` or `any_slice_of_array_mut` instead diff --git a/tests/ui/any-slice-deprecated/test.rs b/tests/ui/any-slice-deprecated/test.rs deleted file mode 100644 index 0561986ece73..000000000000 --- a/tests/ui/any-slice-deprecated/test.rs +++ /dev/null @@ -1,10 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! A test that checks that Kani emits the deprecated message for `any_slice` -//! and `AnySlice` - -#[kani::proof] -fn check_any_slice_deprecated() { - let _s: kani::slice::AnySlice = kani::slice::any_slice(); -}