[kani] Prove some PtrInner methods

gherrit-pr-id: Ic1e352d3d92a45ff86d8ca85b8221bccfb07033b

Author: joshlf

src/lib.rs

@@ -377,7 +377,7 @@ use std::io;
 
 use crate::pointer::invariant::{self, BecauseExclusive};
 
-#[cfg(any(feature = "alloc", test))]
+#[cfg(any(feature = "alloc", test, kani))]
 extern crate alloc;
 #[cfg(any(feature = "alloc", test))]
 use alloc::{boxed::Box, vec::Vec};
@@ -738,8 +738,13 @@ pub unsafe trait KnownLayout {
     /// The type of metadata stored in a pointer to `Self`.
     ///
     /// This is `()` for sized types and `usize` for slice DSTs.
+    #[cfg(not(kani))]
     type PointerMetadata: PointerMetadata;
 
+    #[cfg(kani)]
+    #[allow(missing_docs)]
+    type PointerMetadata: PointerMetadata + kani::Arbitrary;
+
     /// A maybe-uninitialized analog of `Self`
     ///
     /// # Safety

src/pointer/inner.rs

@@ -519,3 +519,232 @@ mod tests {
         }
     }
 }
+
+#[cfg(kani)]
+mod proofs {
+    use crate::{SizeInfo, TrailingSliceLayout};
+
+    use super::*;
+
+    impl<T> kani::Arbitrary for PtrInner<'static, T>
+    where
+        T: ?Sized + KnownLayout,
+    {
+        fn any() -> Self {
+            let (size, meta) = match T::LAYOUT.size_info {
+                SizeInfo::Sized { size } => (size, T::PointerMetadata::from_elem_count(0)),
+                SizeInfo::SliceDst(TrailingSliceLayout { .. }) => {
+                    let meta = T::PointerMetadata::from_elem_count(kani::any());
+                    let size = meta.size_for_metadata(T::LAYOUT);
+                    kani::assume(size.is_some());
+                    let size = size.unwrap();
+                    kani::assume(size <= isize::MAX as usize);
+
+                    (size, meta)
+                }
+            };
+
+            let layout =
+                alloc::alloc::Layout::from_size_align(size, T::LAYOUT.align.get()).unwrap();
+
+            let ptr = if layout.size() == 0 {
+                NonNull::dangling()
+            } else {
+                let ptr = unsafe { alloc::alloc::alloc(layout) };
+                NonNull::new(ptr).unwrap_or_else(|| alloc::alloc::handle_alloc_error(layout))
+            };
+
+            let ptr = T::raw_from_ptr_len(ptr, meta);
+            unsafe { PtrInner::new(ptr) }
+        }
+    }
+
+    impl<'a, T> PtrInner<'a, T>
+    where
+        T: ?Sized + KnownLayout,
+    {
+        fn assert_invariants(&self) {
+            let ptr = self.as_non_null();
+            let size = T::size_of_val_raw(ptr).unwrap();
+            assert!(size <= isize::MAX as usize);
+
+            let addr = ptr.addr().get();
+            // Assert that the referent doesn't wrap around the address space.
+            assert!(addr.checked_add(size).is_some());
+        }
+    }
+
+    macro_rules! prove_foreach {
+        ($generic:ident { $($concrete:ident = $ty:ty,)* }) => {
+            $(
+                #[kani::proof]
+                fn $concrete() {
+                    $generic::<$ty>();
+                }
+            )*
+        };
+    }
+
+    fn prove_arbitrary<T: 'static + ?Sized + KnownLayout>() {
+        let ptr: PtrInner<'static, T> = kani::any();
+        ptr.assert_invariants();
+    }
+
+    // On 64-bit targets, Rust uses 2^61 - 1 rather than 2^63 - 1 as the maximum
+    // object size [1].
+    //
+    // [1] https://github.com/rust-lang/rust/blob/493c38ba371929579fe136df26eccd9516347c7a/compiler/rustc_abi/src/lib.rs#L410
+    const MAX_SIZE: usize = 1 << 61 - 1;
+
+    prove_foreach! {
+        prove_arbitrary {
+            prove_arbitrary_empty_tuple = (),
+            prove_arbitrary_u8 = u8,
+            prove_arbitrary_u16 = u16,
+            prove_arbitrary_slice_u8 = [u8],
+            prove_arbitrary_slice_u16 = [u16],
+            prove_arbitrary_large_u8 = [u8; MAX_SIZE],
+            prove_arbitrary_large_slice_u8 = [[u8; MAX_SIZE]],
+            prove_arbitrary_large_u16 = [u16; (MAX_SIZE)/2],
+            prove_arbitrary_large_slice_u16 = [[u16; (MAX_SIZE)/2]],
+        }
+    }
+
+    fn prove_slice_unchecked<T: 'static>() {
+        let ptr: PtrInner<'static, [T]> = kani::any();
+        let start = kani::any();
+        let end = kani::any();
+
+        kani::assume(start <= end);
+        kani::assume(end <= ptr.len());
+
+        let slc = unsafe { ptr.slice_unchecked(Range { start, end }) };
+        slc.assert_invariants();
+
+        assert_eq!(slc.len(), end - start);
+
+        let begin = unsafe { slc.as_non_null().cast::<T>().sub(start) };
+        assert_eq!(begin, ptr.as_non_null().cast::<T>());
+    }
+
+    prove_foreach! {
+        prove_slice_unchecked {
+            prove_slice_unchecked_empty_tuple = (),
+            prove_slice_unchecked_u8 = u8,
+            prove_slice_unchecked_u16 = u16,
+            prove_slice_unchecked_large_u8 = [u8; MAX_SIZE],
+            prove_slice_unchecked_large_u16 = [u16; (MAX_SIZE)/2],
+        }
+    }
+
+    fn prove_split_at<T: 'static>() {
+        let ptr: PtrInner<'static, [T]> = kani::any();
+        let l_len = kani::any();
+
+        kani::assume(l_len <= ptr.len());
+
+        let (left, right) = unsafe { ptr.split_at(l_len) };
+        left.assert_invariants();
+        right.assert_invariants();
+
+        assert_eq!(left.len(), l_len);
+        assert_eq!(left.len() + right.len(), ptr.len());
+        assert_eq!(left.as_non_null().cast::<T>(), ptr.as_non_null().cast::<T>());
+    }
+
+    prove_foreach! {
+        prove_split_at {
+            prove_split_at_empty_tuple = (),
+            prove_split_at_u8 = u8,
+            prove_split_at_u16 = u16,
+            prove_split_at_large_u8 = [u8; MAX_SIZE],
+            prove_split_at_large_u16 = [u16; (MAX_SIZE)/2],
+        }
+    }
+
+    #[kani::proof]
+    fn prove_as_slice() {
+        fn inner<T: 'static, const N: usize>() {
+            let ptr: PtrInner<'static, [T; N]> = kani::any();
+            let slc = ptr.as_slice();
+            slc.assert_invariants();
+
+            assert_eq!(ptr.as_non_null().cast::<T>(), slc.as_non_null().cast::<T>());
+            assert_eq!(slc.len(), N);
+        }
+
+        inner::<(), 0>();
+        inner::<(), 1>();
+        inner::<(), MAX_SIZE>();
+
+        inner::<u8, 0>();
+        inner::<u8, 1>();
+        inner::<u8, MAX_SIZE>();
+
+        inner::<[u8; MAX_SIZE / 2], 0>();
+        inner::<[u8; MAX_SIZE / 2], 1>();
+        inner::<[u8; MAX_SIZE / 2], 2>();
+
+        inner::<[u8; MAX_SIZE], 0>();
+        inner::<[u8; MAX_SIZE], 1>();
+    }
+
+    impl kani::Arbitrary for CastType {
+        fn any() -> CastType {
+            if kani::any() {
+                CastType::Prefix
+            } else {
+                CastType::Suffix
+            }
+        }
+    }
+
+    fn prove_try_cast_into<T: 'static + ?Sized + KnownLayout>() {
+        let ptr: PtrInner<'static, [u8]> = kani::any();
+        let cast_type = kani::any();
+        let meta = kani::any();
+
+        match ptr.try_cast_into::<T>(cast_type, meta) {
+            Ok((t, rest)) => {
+                t.assert_invariants();
+
+                let ptr_u8 = ptr.as_non_null().cast::<u8>();
+                let t_u8 = t.as_non_null().cast::<u8>();
+                let rest_u8 = rest.as_non_null().cast::<u8>();
+                match cast_type {
+                    CastType::Prefix => {
+                        assert_eq!(t_u8, ptr_u8);
+                        // TODO: Assert that `t` and `rest` are contiguous and
+                        // non-overlapping.
+                    }
+                    CastType::Suffix => {
+                        assert_eq!(rest_u8, ptr_u8);
+                        // Asserts that `rest` and `t` are contiguous and
+                        // non-overlapping.
+                        assert_eq!(unsafe { rest_u8.add(rest.len()) }, t_u8);
+                    }
+                }
+            }
+            Err(CastError::Alignment(_)) => {
+                // TODO: Prove that there would have been an alignment problem.
+            }
+            Err(CastError::Size(_)) => {
+                // TODO: Prove that there would have been a size problem.
+            }
+        }
+    }
+
+    prove_foreach! {
+        prove_try_cast_into {
+            prove_try_cast_into_empty_tuple = (),
+            prove_try_cast_into_u8 = u8,
+            prove_try_cast_into_u16 = u16,
+            prove_try_cast_into_slice_u8 = [u8],
+            prove_try_cast_into_slice_u16 = [u16],
+            prove_try_cast_into_large_u8 = [u8; MAX_SIZE],
+            prove_try_cast_into_large_slice_u8 = [[u8; MAX_SIZE]],
+            prove_try_cast_into_large_u16 = [u16; (MAX_SIZE)/2],
+            prove_try_cast_into_large_slice_u16 = [[u16; (MAX_SIZE)/2]],
+        }
+    }
+}