Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Delete any_slice which has been deprecated since Kani 0.38.0. #2860

Merged
merged 3 commits into from
Nov 7, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
118 changes: 1 addition & 117 deletions library/kani/src/slice.rs
Original file line number Diff line number Diff line change
@@ -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};
feliperodri marked this conversation as resolved.
Show resolved Hide resolved

/// 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
Expand Down Expand Up @@ -34,117 +32,3 @@ fn any_range<const LENGTH: usize>() -> (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<u8, 5> = 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<T, const MAX_SLICE_LENGTH: usize> {
layout: Layout,
ptr: *mut T,
slice_len: usize,
}

#[allow(deprecated)]
impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
fn new() -> Self
where
T: Arbitrary,
{
let any_slice = AnySlice::<T, MAX_SLICE_LENGTH>::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::<T>(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<T, const MAX_SLICE_LENGTH: usize> Drop for AnySlice<T, MAX_SLICE_LENGTH> {
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<T, const MAX_SLICE_LENGTH: usize> Deref for AnySlice<T, MAX_SLICE_LENGTH> {
type Target = [T];

fn deref(&self) -> &Self::Target {
self.get_slice()
}
}

#[allow(deprecated)]
impl<T, const MAX_SLICE_LENGTH: usize> DerefMut for AnySlice<T, MAX_SLICE_LENGTH> {
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<T, const MAX_SLICE_LENGTH: usize>() -> AnySlice<T, MAX_SLICE_LENGTH>
where
T: Arbitrary,
{
#[allow(deprecated)]
AnySlice::<T, MAX_SLICE_LENGTH>::new()
}
2 changes: 0 additions & 2 deletions tests/ui/any-slice-deprecated/expected

This file was deleted.

10 changes: 0 additions & 10 deletions tests/ui/any-slice-deprecated/test.rs

This file was deleted.