ostd/mm/
pod.rs

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

ostd/mm/
pod.rs
