@@ -67,14 +67,64 @@ macro_rules! kani_lib {
6767 kani_core:: generate_models!( ) ;
6868
6969 pub mod float {
70+ //! This module contains functions useful for float-related checks
7071:: generate_float!( std) ;
7172 }
7273
7374 pub mod mem {
75+ //! This module contains functions useful for checking unsafe memory access.
76+ //!
77+ //! Given the following validity rules provided in the Rust documentation:
78+ //! <https://doc.rust-lang.org/std/ptr/index.html> (accessed Feb 6th, 2024)
79+ //!
80+ //! 1. A null pointer is never valid, not even for accesses of size zero.
81+ //! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer
82+ //! be dereferenceable: the memory range of the given size starting at the pointer must all be
83+ //! within the bounds of a single allocated object. Note that in Rust, every (stack-allocated)
84+ //! variable is considered a separate allocated object.
85+ //! ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory,
86+ //! i.e., deallocation makes pointers invalid even for zero-sized operations.~~
87+ //! ZST access is not OK for any pointer.
88+ //! See: <https://github.com/rust-lang/unsafe-code-guidelines/issues/472>
89+ //! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized
90+ //! accesses, even if some memory happens to exist at that address and gets deallocated.
91+ //! This corresponds to writing your own allocator: allocating zero-sized objects is not very
92+ //! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is
93+ //! `NonNull::dangling`.
94+ //! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic
95+ //! operations used to synchronize between threads.
96+ //! This means it is undefined behavior to perform two concurrent accesses to the same location
97+ //! from different threads unless both accesses only read from memory.
98+ //! Notice that this explicitly includes `read_volatile` and `write_volatile`:
99+ //! Volatile accesses cannot be used for inter-thread synchronization.
100+ //! 5. The result of casting a reference to a pointer is valid for as long as the underlying
101+ //! object is live and no reference (just raw pointers) is used to access the same memory.
102+ //! That is, reference and pointer accesses cannot be interleaved.
103+ //!
104+ //! Kani is able to verify #1 and #2 today.
105+ //!
106+ //! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if
107+ //! the address matches `NonNull::<()>::dangling()`.
108+ //! The way Kani tracks provenance is not enough to check if the address was the result of a cast
109+ //! from a non-zero integer literal.
110+ //!
74111:: kani_mem!( std) ;
75112 }
76113
77114 mod mem_init {
115+ //! This module provides instrumentation for tracking memory initialization of raw pointers.
116+ //!
117+ //! Currently, memory initialization is tracked on per-byte basis, so each byte of memory pointed to
118+ //! by raw pointers could be either initialized or uninitialized. Padding bytes are always
119+ //! considered uninitialized when read as data bytes. Each type has a type layout to specify which
120+ //! bytes are considered to be data and which -- padding. This is determined at compile time and
121+ //! statically injected into the program (see `Layout`).
122+ //!
123+ //! Compiler automatically inserts calls to `is_xxx_initialized` and `set_xxx_initialized` at
124+ //! appropriate locations to get or set the initialization status of the memory pointed to.
125+ //!
126+ //! Note that for each harness, tracked object and tracked offset are chosen non-deterministically,
127+ //! so calls to `is_xxx_initialized` should be only used in assertion contexts.
78128:: kani_mem_init!( std) ;
79129 }
80130 } ;
0 commit comments