Module mem

This module contains functions useful for checking unsafe memory access.

Given the following validity rules provided in the Rust documentation: https://doc.rust-lang.org/std/ptr/index.html (accessed May 20th, 2025)

1. For memory accesses of size zero, every pointer is valid, including the null pointer. The following points are only concerned with non-zero-sized accesses.
2. A null pointer is never valid.
3. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer be dereferenceable: the memory range of the given size starting at the pointer must all be within the bounds of a single allocated object. Note that in Rust, every (stack-allocated) variable is considered a separate allocated object.
4. All accesses performed by functions in this module are non-atomic in the sense of atomic operations used to synchronize between threads. This means it is undefined behavior to perform two concurrent accesses to the same location from different threads unless both accesses only read from memory. Notice that this explicitly includes read_volatile and write_volatile: Volatile accesses cannot be used for inter-thread synchronization.
5. The result of casting a reference to a pointer is valid for as long as the underlying object is live and no reference (just raw pointers) is used to access the same memory. That is, reference and pointer accesses cannot be interleaved.

Kani is able to verify #1, #2, and #3 today.

Functions

can_dereference

Checks that pointer ptr point to a valid value of type T.

can_read_unaligned

Checks that pointer ptr point to a valid value of type T.

can_write

Check if the pointer is valid for write access according to crate::mem conditions 1, 2 and 3.

can_write_unaligned

Check if the pointer is valid for unaligned write access according to crate::mem conditions 1, 2 and 3.

checked_align_of_raw

Compute the size of the val pointed to if safe.

checked_size_of_raw

Compute the size of the val pointed to if it is safe to do so.

is_inbounds

Checks that ptr points to an allocation that can hold data of size calculated from T.

same_allocation

Check if two pointers points to the same allocated object, and that both pointers are in bounds of that object.