notesum.ai
Published at December 9Fearless unsafe. Safety Property is all you need
cs.SE
Released Date: December 9, 2024
Authors: Mohan Cui1, Penglei Mao1, Shuran Sun1, Yangfan Zhou1, Hui Xu1
Aff.: 1Fudan University

| Safety Property | SUM | Definition and the safety requirement of each Safety Property. | Unsafe API Example |
| Precondition Safety Property | |||
| Allocated | 172 | Non-Null : A null pointer is never valid, not even for accesses of size zero. | impl¡T: Sized¿ NonNull¡T¿::new_unchecked |
| Non-Dangling : The value must not be pointing to the deallocated memory even for operations of size zero, including data stored in the stack frame and heap chunk. | trait SliceIndex¡T: ?Sized¿::get_unchecked | ||
| Bounded | 141 | Numerical: The relationship expressions based on numerical operations exhibit clear numerical boundaries. The terms of the expressions can be constants, variables, or the return values of function calls. There are six relational operators including EQ, NE, LT, GT, LE, and GE. | impl¡T: ?Sized¿ *mut T::offset_from |
| Dereferencable: The memory range of the given size starting at the pointer must all be within the bounds of a single allocated object. | impl¡T: ?Sized¿ *mut T::copy_from | ||
| Initialized | 104 | Initialized : The value that has been initialized can be divided into two scenarios: fully initialized and partially initialized. | impl¡T¿ MaybeUninit¡T¿::assume_init |
| Typed : The bit pattern of the initialized value must be valid at the given type and uphold additional invariants for generics. | impl¡T: ?Sized¿ *mut T::read | ||
| Encoded : The encoding format of the string includes UTF-8 string, ASCII string (in bytes), and C-compatible string (nul-terminated trailing with no nul bytes in the middle). | impl String::from_utf8_unchecked | ||
| Layout | 109 | Sized : The restrictions on Exotically Sized Types (EST), including Dynamically Sized Types (DST) that lack a statically known size, such as trait objects and slices; and Zero Sized Types (ZST) that occupy no space. | core::mem::size_of_raw |
| Aligned : The value is properly aligned via a specific allocator or the attribute #[repr], including the alignment and the padding. | impl¡T: ?Sized¿ *mut T::swap | ||
| Fitted : The layout (including size and alignment) must be the same layout that was used to allocate that block of memory. | trait GlobalAlloc::dealloc | ||
| SystemIO | 26 | The variable is related to the system IO and depends on the target platform, including TCP sockets, handles, and file descriptors. | trait FromRawFd::from_raw_fd |
| Thread | 2 | Send: The type can be transferred across threads. | core::marker::Send |
| Sync: The type can be safe to share references between threads. | core::marker::Sync | ||
| Unreachable | 5 | The specific value will trigger unreachable data flow, such as enumeration index (variance), boolean value, etc. | impl¡T¿ Option¡T¿::unwrap_unchecked |
| Postcondition Safety Property | |||
| Aliased | 32 | Aliased : The value may have multiple mutable references or simultaneously have mutable and shared references. | impl¡T: ?Sized¿ *mut T::as_mut |
| Mutated : The value, which is owned by an immutable binding or pointed by shared reference, may be mutated. | impl¡T: ?Sized¿ *const T::as_ref | ||
| Outlived : The arbitrary lifetime (unbounded) that becomes as big as context demands may outlive the pointed memory. | impl CStr::from_ptr | ||
| DualOwned | 46 | It may create multiple overlapped owners in the ownership system that share the same memory via retaking the owner or creating a bitwise copy. | impl¡T: ?Sized¿ Box¡T¿::from_raw |
| Untyped | 37 | The value may not be in the initialized state, or the byte pattern represents an invalid value of its type. | core::mem::zeroed |
| Freed | 19 | The value may be manually freed or automated dropped. | impl¡T: ?Sized¿ ManuallyDrop¡T¿::drop |
| Leaked | 35 | The value may be leaked or escaped from the ownership system. | impl¡T: ?Sized¿ *mut T::write |
| Pinned | 5 | The value may be moved, although it ought to be pinned. | impl¡P: Deref¿ Pin¡P¿::new_unchecked |