|
1 | 1 | // Copyright Kani Contributors
|
2 | 2 | // 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}; |
6 | 4 |
|
7 | 5 | /// Given an array `arr` of length `LENGTH`, this function returns a **valid**
|
8 | 6 | /// 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) {
|
34 | 32 | assume(from <= to);
|
35 | 33 | (from, to)
|
36 | 34 | }
|
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 |
| -} |
0 commit comments