ostd/specs/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    #[verifier::external_body]
43    fn as_bytes_mut(&mut self) -> (r: &mut [u8])
44        ensures
45            r.len() == core::mem::size_of::<Self>(),
46    {
47        let ptr = self as *mut Self as *mut u8;
48        let len = core::mem::size_of::<Self>();
49
50        unsafe { core::slice::from_raw_parts_mut(ptr, len) }
51    }
52
53    /// As an immutable slice of bytes.
54    #[verifier::external_body]
55    fn as_bytes_ref(&self) -> (r: &[u8])
56        ensures
57            r.len() == core::mem::size_of::<Self>(),
58    {
59        let ptr = self as *const Self as *const u8;
60        let len = core::mem::size_of::<Self>();
61
62        unsafe { core::slice::from_raw_parts(ptr, len) }
63    }
64}
65
66/// A marker trait for POD types that can be read or written with one instruction.
67///
68/// We currently rely on this trait to ensure that the memory operation created by
69/// [`core::ptr::read_volatile`] and [`core::ptr::write_volatile`] doesn't tear. However, the Rust documentation
70/// makes no such guarantee, and even the wording in the LLVM LangRef is ambiguous.
71///
72/// At this point, we can only _hope_ that this doesn't break in future versions of the Rust or
73/// LLVM compilers. However, this is unlikely to happen in practice, since the Linux kernel also
74/// uses "volatile" semantics to implement `READ_ONCE`/`WRITE_ONCE`.
75pub trait PodOnce: Pod {
76
77}
78
79} // verus!
ostd/specs/mm/pod.rs

ostd/specs/mm/
pod.rs
