safety_tag/
lib.rs

1pub mod invariants {
2    #![allow(private_interfaces, unused_variables, non_snake_case)]
3
4    pub trait SafetyProperty {
5        /// A tuple of SP arguments.
6        type Args: SafetyPropertyArg;
7
8        /// Single ident name of an SP.
9        fn name() -> &'static str;
10
11        /// Static string, or dynamic interpolated string based on tag arguments.
12        fn description(args: Self::Args) -> String;
13
14        /// Kani macros for the SP.
15        fn kani(args: Self::Args) -> Option<String> {
16            None
17        }
18    }
19
20    pub trait SafetyPropertyArg {
21        fn name() -> &'static str;
22    }
23
24    macro_rules! sp_arg {
25        ($name:ident) => {
26            enum $name {}
27            impl SafetyPropertyArg for $name {
28                fn name() -> &'static str { stringify!($name) }
29            }
30        };
31        ($( $name:ident)+ ) => {
32            $( sp_arg!{ $name } )+
33        }
34    }
35
36    sp_arg! { Pointer Type Len Num Allocator }
37
38    /// Official ptr safety doc: <https://doc.rust-lang.org/std/ptr/index.html#safety>.
39    ///
40    /// Formal: `Size(T, 0) || (!Size(T,0) && Deref(p, T, len) )`
41    ///
42    /// where
43    /// - [Size]
44    /// - [Deref]
45    ///
46    /// # Unsafe Function directly requiring this SP
47    ///
48    /// - [crate::foo]
49    pub fn ValidPtr(p: Pointer, T: Type, len: Len) {}
50
51    /// Formal: `sizeof(T) = c, c ∈ {num, unknown, any}`
52    ///
53    /// # Unsafe Function indirectly requiring this SP
54    ///
55    /// - [crate::foo]
56    pub fn Size(T: Type, c: Num) {}
57
58    /// Formal: `Deref(p, T, len) = Allocated(p, T, len, *) && InBound(p, T, len)`
59    ///
60    /// where
61    /// - [Allocated]
62    /// - [InBound]
63    ///
64    /// # Unsafe Function indirectly requiring this SP
65    ///
66    /// - [crate::foo]
67    pub fn Deref(p: Pointer, T: Type, len: Len) {}
68
69    /// Formal: `Allocated(p, T, len, A): ∀ i ∈ 0..sizeof(T)*len, allocator(p+i) = A`
70    ///
71    /// # Unsafe Function indirectly requiring this SP
72    ///
73    /// - [crate::foo]
74    pub fn Allocated(p: Pointer, T: Type, len: Len, A: Allocator) {}
75
76    /// Formal: `InBound(p, T, len): mem(p, p+ sizeof(T) * len) ∈ single allocated object`
77    ///
78    /// # Unsafe Function indirectly requiring this SP
79    ///
80    /// - [crate::foo]
81    pub fn InBound(p: Pointer, T: Type, len: Len) {}
82}
83
84#[cfg(doc)]
85use invariants::*;
86
87// #[safety { ValidPtr(ptr) }] expands to:
88/// # Safety
89///
90/// - [ValidPtr] : ptr must be [valid](https://doc.rust-lang.org/std/ptr/index.html#safety)
91pub unsafe fn foo(ptr: *const ()) {}
safety_tag/lib.rs

safety_tag/
lib.rs
