Skip to content

Commit 985021f

Browse files
authored
Delete any_slice which has been deprecated since Kani 0.38.0. (rust-lang#2860)
Kani's `any_slice` function (and related code) has been deprecated since Kani 0.38.0 (see rust-lang#2789). This PR officially obsoletes it by deleting the code. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent a8a2346 commit 985021f

File tree

4 files changed

+7
-129
lines changed

4 files changed

+7
-129
lines changed

CHANGELOG.md

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,12 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
44

55
This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
66

7+
## [0.41.0]
8+
9+
### Breaking Changes
10+
11+
* Delete `any_slice` which has been deprecated since Kani 0.38.0. by @zhassan-aws in https://github.com/model-checking/kani/pull/2860
12+
713
## [0.40.0]
814

915
### What's Changed

library/kani/src/slice.rs

Lines changed: 1 addition & 117 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
3-
use crate::{any, assume, Arbitrary};
4-
use std::alloc::{alloc, dealloc, Layout};
5-
use std::ops::{Deref, DerefMut};
3+
use crate::{any, assume};
64

75
/// Given an array `arr` of length `LENGTH`, this function returns a **valid**
86
/// slice of `arr` with non-deterministic start and end points. This is useful
@@ -34,117 +32,3 @@ fn any_range<const LENGTH: usize>() -> (usize, usize) {
3432
assume(from <= to);
3533
(from, to)
3634
}
37-
38-
/// A struct that stores a slice of type `T` with a non-deterministic length
39-
/// between `0..=MAX_SLICE_LENGTH` and with non-deterministic content. This is
40-
/// useful in situations where one wants to verify that all slices with any
41-
/// content and with a length up to `MAX_SLICE_LENGTH` satisfy a certain
42-
/// property. Use `any_slice` to create an instance of this struct.
43-
///
44-
/// # Example:
45-
///
46-
/// ```rust
47-
/// let slice: kani::slice::AnySlice<u8, 5> = kani::slice::any_slice();
48-
/// foo(&slice); // where foo is a function that takes a slice and verifies a property about it
49-
/// ```
50-
#[deprecated(
51-
since = "0.38.0",
52-
note = "Use `any_slice_of_array` or `any_slice_of_array_mut` instead"
53-
)]
54-
pub struct AnySlice<T, const MAX_SLICE_LENGTH: usize> {
55-
layout: Layout,
56-
ptr: *mut T,
57-
slice_len: usize,
58-
}
59-
60-
#[allow(deprecated)]
61-
impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
62-
fn new() -> Self
63-
where
64-
T: Arbitrary,
65-
{
66-
let any_slice = AnySlice::<T, MAX_SLICE_LENGTH>::alloc_slice();
67-
unsafe {
68-
let mut i = 0;
69-
// Note: even though the guard `i < MAX_SLICE_LENGTH` is redundant
70-
// since the assumption above guarantees that `slice_len` <=
71-
// `MAX_SLICE_LENGTH`, without it, CBMC fails to infer the required
72-
// unwind value, and requires specifying one, which is inconvenient.
73-
// CBMC also fails to infer the unwinding if the loop is simply
74-
// written as:
75-
// for i in 0..slice_len {
76-
// *(ptr as *mut T).add(i) = any();
77-
// }
78-
while i < any_slice.slice_len && i < MAX_SLICE_LENGTH {
79-
std::ptr::write(any_slice.ptr.add(i), any());
80-
i += 1;
81-
}
82-
}
83-
any_slice
84-
}
85-
86-
fn alloc_slice() -> Self {
87-
let slice_len = any();
88-
assume(slice_len <= MAX_SLICE_LENGTH);
89-
let layout = Layout::array::<T>(slice_len).unwrap();
90-
let ptr = if slice_len == 0 { std::ptr::null() } else { unsafe { alloc(layout) } };
91-
Self { layout, ptr: ptr as *mut T, slice_len }
92-
}
93-
94-
pub fn get_slice(&self) -> &[T] {
95-
if self.slice_len == 0 {
96-
&[]
97-
} else {
98-
unsafe { std::slice::from_raw_parts(self.ptr, self.slice_len) }
99-
}
100-
}
101-
102-
pub fn get_slice_mut(&mut self) -> &mut [T] {
103-
if self.slice_len == 0 {
104-
&mut []
105-
} else {
106-
unsafe { std::slice::from_raw_parts_mut(self.ptr, self.slice_len) }
107-
}
108-
}
109-
}
110-
111-
#[allow(deprecated)]
112-
impl<T, const MAX_SLICE_LENGTH: usize> Drop for AnySlice<T, MAX_SLICE_LENGTH> {
113-
fn drop(&mut self) {
114-
if self.slice_len > 0 {
115-
assert!(!self.ptr.is_null());
116-
unsafe {
117-
dealloc(self.ptr as *mut u8, self.layout);
118-
}
119-
}
120-
}
121-
}
122-
123-
#[allow(deprecated)]
124-
impl<T, const MAX_SLICE_LENGTH: usize> Deref for AnySlice<T, MAX_SLICE_LENGTH> {
125-
type Target = [T];
126-
127-
fn deref(&self) -> &Self::Target {
128-
self.get_slice()
129-
}
130-
}
131-
132-
#[allow(deprecated)]
133-
impl<T, const MAX_SLICE_LENGTH: usize> DerefMut for AnySlice<T, MAX_SLICE_LENGTH> {
134-
fn deref_mut(&mut self) -> &mut Self::Target {
135-
self.get_slice_mut()
136-
}
137-
}
138-
139-
#[deprecated(
140-
since = "0.38.0",
141-
note = "Use `any_slice_of_array` or `any_slice_of_array_mut` instead"
142-
)]
143-
#[allow(deprecated)]
144-
pub fn any_slice<T, const MAX_SLICE_LENGTH: usize>() -> AnySlice<T, MAX_SLICE_LENGTH>
145-
where
146-
T: Arbitrary,
147-
{
148-
#[allow(deprecated)]
149-
AnySlice::<T, MAX_SLICE_LENGTH>::new()
150-
}

tests/ui/any-slice-deprecated/expected

Lines changed: 0 additions & 2 deletions
This file was deleted.

tests/ui/any-slice-deprecated/test.rs

Lines changed: 0 additions & 10 deletions
This file was deleted.

0 commit comments

Comments
 (0)