Skip to content

Commit

Permalink
Deprecate any_slice (#2789)
Browse files Browse the repository at this point in the history
Deprecate kani::slice::any_slice in Kani 0.38.0 (and the related AnySlice struct), and remove it in a later version.

Motivation: The Kani library's `slice::any_slice` API is doing more harm than benefit: it is meant to provide a convenient way for users to generate non-deterministic slices, but its current implementation aims to avoid any unsoundness by making sure that for the non-deterministic slice returned by the API, accessing memory beyond the slice length is flagged as an out-of-bounds access (see #1009 for details). However, in practical scenarios, using it ends up causing memory to blowup for CBMC. Given that users may not care about this type of unsoundness, which is only possible through using a pointer dereference inside an unsafe block (see discussion in #2634). Thus, we should leave it to the user to decide the suitable method for generating slices that fits their verification needs. For example, they can use Kani's alternative API, `any_slice_of_array` that extracts a slice of a non-deterministic start and end from a given array.
  • Loading branch information
zhassan-aws authored Sep 26, 2023
1 parent 6b1a09d commit 8480dc6
Show file tree
Hide file tree
Showing 11 changed files with 62 additions and 66 deletions.
14 changes: 14 additions & 0 deletions library/kani/src/slice.rs
Original file line number Diff line number Diff line change
Expand Up @@ -47,12 +47,17 @@ fn any_range<const LENGTH: usize>() -> (usize, usize) {
/// 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
Expand Down Expand Up @@ -103,6 +108,7 @@ impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
}
}

#[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 {
Expand All @@ -114,6 +120,7 @@ impl<T, const MAX_SLICE_LENGTH: usize> Drop for AnySlice<T, MAX_SLICE_LENGTH> {
}
}

#[allow(deprecated)]
impl<T, const MAX_SLICE_LENGTH: usize> Deref for AnySlice<T, MAX_SLICE_LENGTH> {
type Target = [T];

Expand All @@ -122,15 +129,22 @@ impl<T, const MAX_SLICE_LENGTH: usize> Deref for AnySlice<T, MAX_SLICE_LENGTH> {
}
}

#[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()
}
7 changes: 4 additions & 3 deletions tests/expected/nondet-slice-i32-oob/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,12 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

// This test checks that Kani reports out-of-bound accesses on a non-det slice
// created using kani::slice::any_slice
// created using `kani::slice::any_slice_of_array`

#[kani::proof]
fn check_out_of_bounds() {
let bytes = kani::slice::any_slice::<i32, 8>();
let val = unsafe { *bytes.get_slice().as_ptr().offset(1) };
let arr: [i32; 8] = kani::any();
let bytes = kani::slice::any_slice_of_array(&arr);
let val = unsafe { *bytes.as_ptr().offset(1) };
assert_eq!(val - val, 0);
}
19 changes: 14 additions & 5 deletions tests/expected/nondet-slice-len/expected
Original file line number Diff line number Diff line change
@@ -1,5 +1,14 @@
Failed Checks: assertion failed: s.len() != 0
Failed Checks: assertion failed: s.len() != 1
Failed Checks: assertion failed: s.len() != 2
Failed Checks: assertion failed: s.len() != 3
Failed Checks: assertion failed: s.len() != 4
Status: SATISFIED\
Description: "cover condition: s.len() == 0"

Status: SATISFIED\
Description: "cover condition: s.len() == 1"

Status: SATISFIED\
Description: "cover condition: s.len() == 2"

Status: SATISFIED\
Description: "cover condition: s.len() == 3"

Status: SATISFIED\
Description: "cover condition: s.len() == 4"
15 changes: 8 additions & 7 deletions tests/expected/nondet-slice-len/main.rs
Original file line number Diff line number Diff line change
@@ -1,15 +1,16 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// This test checks that non-det slices created using kani::slice::any_slice can
// This test checks that non-det slices created using `kani::slice::any_slice_of_array`
// assume any length up the specified maximum

#[kani::proof]
fn check_possible_slice_lengths() {
let s = kani::slice::any_slice::<i32, 4>();
assert!(s.len() != 0);
assert!(s.len() != 1);
assert!(s.len() != 2);
assert!(s.len() != 3);
assert!(s.len() != 4);
let arr: [i32; 4] = kani::any();
let s = kani::slice::any_slice_of_array(&arr);
kani::cover!(s.len() == 0);
kani::cover!(s.len() == 1);
kani::cover!(s.len() == 2);
kani::cover!(s.len() == 3);
kani::cover!(s.len() == 4);
}
7 changes: 4 additions & 3 deletions tests/expected/nondet-slice-u8-oob/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,13 @@
// SPDX-License-Identifier: Apache-2.0 OR MIT

// This test checks that Kani reports out-of-bound accesses on a non-det slice
// created using kani::slice::any_slice
// created using `kani::slice::any_slice_of_array`

#[kani::proof]
fn check_out_of_bounds() {
let mut bytes = kani::slice::any_slice::<u8, 5>();
let val = unsafe { *bytes.get_slice().as_ptr().add(4) };
let arr: [u8; 5] = kani::any();
let mut bytes = kani::slice::any_slice_of_array(&arr);
let val = unsafe { *bytes.as_ptr().add(4) };
kani::assume(val != 0);
assert_ne!(val, 0);
}
5 changes: 3 additions & 2 deletions tests/kani/NondetSlices/test2.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,8 @@ fn check(s: &[u8]) {

#[kani::proof]
fn main() {
// returns a slice of length between 0 and 5 with non-det content
let slice: kani::slice::AnySlice<u8, 5> = kani::slice::any_slice();
let arr: [u8; 5] = kani::any();
// returns a slice of length between 0 and 5
let slice = kani::slice::any_slice_of_array(&arr);
check(&slice);
}
5 changes: 3 additions & 2 deletions tests/kani/NondetSlices/test3.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,14 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

// This test uses kani::slice::any_slice of i32
// This test uses `kani::slice::any_slice_of_array` with `i32`

// kani-flags: --default-unwind 6

#[kani::proof]
fn check_any_slice_i32() {
let s = kani::slice::any_slice::<i32, 5>();
let a: [i32; 5] = kani::any();
let s = kani::slice::any_slice_of_array(&a);
s.iter().for_each(|x| kani::assume(*x < 10 && *x > -20));
let sum = s.iter().fold(0, |acc, x| acc + x);
assert!(sum <= 45); // 9 * 5
Expand Down
19 changes: 0 additions & 19 deletions tests/kani/NondetSlices/test4.rs

This file was deleted.

25 changes: 0 additions & 25 deletions tests/kani/Slice/slice-drop.rs

This file was deleted.

2 changes: 2 additions & 0 deletions tests/ui/any-slice-deprecated/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
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
10 changes: 10 additions & 0 deletions tests/ui/any-slice-deprecated/test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
// 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<i32, 5> = kani::slice::any_slice();
}

0 comments on commit 8480dc6

Please sign in to comment.