rapx/verify/
primitive.rs

1//! Primitive API classification for verifier transfer functions.
2//!
3//! The staged verifier still needs semantic summaries for compiler/std
4//! primitives whose MIR body does not expose the address or memory effect we
5//! want to reason about.  This module keeps the name-based recognition in one
6//! small registry.  Higher layers translate the classified primitive into
7//! dependency summaries, forward effects, and SMT assumptions.
8
9/// Std/core primitive calls with verifier-specific transfer functions.
10#[derive(Clone, Copy, Debug, PartialEq, Eq)]
11pub enum PrimitiveCall {
12    AsPtr,
13    AsMutPtr,
14    AsPtrRange,
15    AsMutPtrRange,
16    PtrCast,
17    PtrAdd,
18    PtrSub,
19    PtrOffset,
20    PtrByteAdd,
21    PtrByteSub,
22    PtrByteOffset,
23    PtrRead,
24    PtrWrite,
25    Len,
26    MaybeUninitUninit,
27    AlignOf,
28    SizeOf,
29    FromRawParts,
30    FromRawPartsMut,
31    SplitAt,
32    SplitAtMut,
33}
34
35impl PrimitiveCall {
36    /// Classify a stable rustc def-path string as a known primitive call.
37    pub fn classify(name: &str) -> Option<Self> {
38        if name.ends_with("::as_ptr")
39            || (name.contains("::as_ptr") && !name.ends_with("::as_ptr_range"))
40        {
41            return Some(Self::AsPtr);
42        }
43        if name.ends_with("::as_mut_ptr")
44            || (name.contains("::as_mut_ptr") && !name.ends_with("::as_mut_ptr_range"))
45        {
46            return Some(Self::AsMutPtr);
47        }
48        if name.ends_with("::as_ptr_range") || name.contains("::as_ptr_range") {
49            return Some(Self::AsPtrRange);
50        }
51        if name.ends_with("::as_mut_ptr_range") || name.contains("::as_mut_ptr_range") {
52            return Some(Self::AsMutPtrRange);
53        }
54        if name.contains("::cast") || name.contains("cast_array") || name.contains("cast_const") || name.contains("cast_mut") {
55            return Some(Self::PtrCast);
56        }
57        if name.contains("::byte_add") || name.contains("::wrapping_byte_add") {
58            return Some(Self::PtrByteAdd);
59        }
60        if name.contains("::byte_sub") || name.contains("::wrapping_byte_sub") {
61            return Some(Self::PtrByteSub);
62        }
63        if name.contains("::byte_offset") || name.contains("::wrapping_byte_offset") {
64            return Some(Self::PtrByteOffset);
65        }
66        if name.contains("::add") || name.contains("::wrapping_add") {
67            return Some(Self::PtrAdd);
68        }
69        if name.contains("::sub") || name.contains("::wrapping_sub") {
70            return Some(Self::PtrSub);
71        }
72        if name.contains("::offset") || name.contains("::wrapping_offset") {
73            return Some(Self::PtrOffset);
74        }
75        if name.contains("::read") || name.ends_with("read") {
76            return Some(Self::PtrRead);
77        }
78        if (name.contains("::write") || name.ends_with("write"))
79            && !name.contains("write_bytes")
80            && !name.contains("write_unaligned")
81            && !name.contains("write_volatile")
82        {
83            return Some(Self::PtrWrite);
84        }
85        if name.ends_with("::len") || name.contains("::len") {
86            return Some(Self::Len);
87        }
88        if name.contains("MaybeUninit") && name.ends_with("::uninit") {
89            return Some(Self::MaybeUninitUninit);
90        }
91        if name.contains("align_of") {
92            return Some(Self::AlignOf);
93        }
94        if name.contains("size_of") {
95            return Some(Self::SizeOf);
96        }
97        if name.ends_with("::from_raw_parts_mut") || name.contains("::from_raw_parts_mut") {
98            return Some(Self::FromRawPartsMut);
99        }
100        if name.contains("::split_at") || name.ends_with("::split_at_mut") {
101            if name.contains("_mut") {
102                return Some(Self::SplitAtMut);
103            }
104            return Some(Self::SplitAt);
105        }
106        if name.ends_with("::from_raw_parts") || name.contains("::from_raw_parts") {
107            return Some(Self::FromRawParts);
108        }
109        None
110    }
111
112    /// Return true for calls that extract a raw pointer from an aggregate.
113    pub fn is_as_ptr_like(self) -> bool {
114        matches!(self, Self::AsPtr | Self::AsMutPtr | Self::PtrCast)
115    }
116
117    /// Return true for pointer arithmetic calls with `base + offset * stride`.
118    pub fn is_pointer_add_like(self) -> bool {
119        matches!(
120            self,
121            Self::PtrAdd | Self::PtrOffset | Self::PtrByteAdd | Self::PtrByteOffset
122        )
123    }
124
125    /// Return true for pointer arithmetic calls with `base - offset * stride`.
126    pub fn is_pointer_sub_like(self) -> bool {
127        matches!(self, Self::PtrSub | Self::PtrByteSub)
128    }
129
130    /// Return true for any pointer arithmetic primitive.
131    pub fn is_pointer_arithmetic(self) -> bool {
132        matches!(
133            self,
134            Self::PtrAdd
135                | Self::PtrSub
136                | Self::PtrOffset
137                | Self::PtrByteAdd
138                | Self::PtrByteSub
139                | Self::PtrByteOffset
140        )
141    }
142
143    /// Return true when the arithmetic count is measured in bytes.
144    pub fn is_byte_pointer_arithmetic(self) -> bool {
145        matches!(
146            self,
147            Self::PtrByteAdd | Self::PtrByteSub | Self::PtrByteOffset
148        )
149    }
150
151    /// Return true when the arithmetic count can be negative.
152    pub fn is_signed_pointer_arithmetic(self) -> bool {
153        matches!(self, Self::PtrOffset | Self::PtrByteOffset)
154    }
155
156    /// Return true for compile-time layout constant producers.
157    pub fn is_layout_constant(self) -> bool {
158        matches!(self, Self::AlignOf | Self::SizeOf)
159    }
160}
rapx/verify/primitive.rs

rapx/verify/
primitive.rs
