Skip to content

Commit

Permalink
Delete any_slice which has been deprecated since Kani 0.38.0. (#2860)
Browse files Browse the repository at this point in the history
Kani's `any_slice` function (and related code) has been deprecated since
Kani 0.38.0 (see #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.
  • Loading branch information
zhassan-aws authored Nov 7, 2023
1 parent a8a2346 commit 985021f
Show file tree
Hide file tree
Showing 4 changed files with 7 additions and 129 deletions.
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};

/// 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.

0 comments on commit 985021f

Please sign in to comment.