ostd/mm/
pod.rs

1use vstd::prelude::*;
2use vstd_extra::array_ptr::{self, ArrayPtr, PointsToArray};
3
4use core::mem::MaybeUninit;
5
6verus! {
7
8/// A trait for Plain Old Data (POD) types.
9pub trait Pod: Copy + Sized {
10    /// Creates a new instance of Pod type that is filled with zeroes.
11    #[verifier::external_body]
12    fn new_zeroed() -> Self {
13        // SAFETY. An all-zero value of `T: Pod` is always valid.
14        unsafe { core::mem::zeroed() }
15    }
16
17    /// Creates a new instance of Pod type with uninitialized content.
18    #[verifier::external_body]
19    fn new_uninit() -> Self {
20        // SAFETY. A value of `T: Pod` can have arbitrary bits.
21        #[allow(clippy::uninit_assumed_init)]
22        unsafe { MaybeUninit::uninit().assume_init() }
23    }
24
25    /// As a slice of bytes.
26    #[verifier::external_body]
27    fn as_bytes<const N: usize>(&self) -> (slice: (
28        ArrayPtr<u8, N>,
29        Tracked<&array_ptr::PointsTo<u8, N>>,
30    ))
31        ensures
32            slice.1@.value().len() == core::mem::size_of::<Self>(),
33            slice.1@.wf(),
34            slice.0.addr() == slice.1@.addr(),
35    {
36        let ptr = self as *const Self as *const u8;
37
38        (ArrayPtr::from_addr(ptr as usize), Tracked::assume_new())
39    }
40
41    /// As a mutable slice of bytes.
42    ///
43    /// Note that this does not create the permission to mutate the Pod value as
44    /// mutable reference is not yet supported in Verus.
45    ///
46    /// Instead, the caller must uphold a separate permission to mutate the Pod value.
47    #[verifier::external_body]
48    fn as_bytes_mut(&mut self) -> (r: (usize, usize))
49        ensures
50            r.1 == core::mem::size_of::<Self>(),
51    {
52        let ptr = self as *mut Self as usize;
53        let len = core::mem::size_of::<Self>();
54
55        (ptr, len)
56    }
57}
58
59/// A marker trait for POD types that can be read or written with one instruction.
60///
61/// We currently rely on this trait to ensure that the memory operation created by
62/// [`core::ptr::read_volatile`] and [`core::ptr::write_volatile`] doesn't tear. However, the Rust documentation
63/// makes no such guarantee, and even the wording in the LLVM LangRef is ambiguous.
64///
65/// At this point, we can only _hope_ that this doesn't break in future versions of the Rust or
66/// LLVM compilers. However, this is unlikely to happen in practice, since the Linux kernel also
67/// uses "volatile" semantics to implement `READ_ONCE`/`WRITE_ONCE`.
68pub trait PodOnce: Pod {
69
70}
71
72} // verus!
ostd/mm/pod.rs

ostd/mm/
pod.rs
