From 8f1858498af8a5402d2e39b40739e208f8ef4756 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 24 Jan 2025 03:11:43 -0600 Subject: [PATCH] Move documentation of kani_core modules to right places --- library/kani_core/src/float.rs | 2 -- library/kani_core/src/lib.rs | 50 +++++++++++++++++++++++++++++++ library/kani_core/src/mem.rs | 37 +---------------------- library/kani_core/src/mem_init.rs | 14 --------- 4 files changed, 51 insertions(+), 52 deletions(-) diff --git a/library/kani_core/src/float.rs b/library/kani_core/src/float.rs index 44475af80a51..cb1c9039fbb6 100644 --- a/library/kani_core/src/float.rs +++ b/library/kani_core/src/float.rs @@ -1,8 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains functions useful for float-related checks - #[allow(clippy::crate_in_macro_def)] #[macro_export] macro_rules! generate_float { diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 3ba2f459470e..37a05821bd33 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -67,14 +67,64 @@ macro_rules! kani_lib { kani_core::generate_models!(); pub mod float { + //! This module contains functions useful for float-related checks kani_core::generate_float!(std); } pub mod mem { + //! This module contains functions useful for checking unsafe memory access. + //! + //! Given the following validity rules provided in the Rust documentation: + //! (accessed Feb 6th, 2024) + //! + //! 1. A null pointer is never valid, not even for accesses of size zero. + //! 2. 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. + //! ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory, + //! i.e., deallocation makes pointers invalid even for zero-sized operations.~~ + //! ZST access is not OK for any pointer. + //! See: + //! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized + //! accesses, even if some memory happens to exist at that address and gets deallocated. + //! This corresponds to writing your own allocator: allocating zero-sized objects is not very + //! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is + //! `NonNull::dangling`. + //! 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 and #2 today. + //! + //! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if + //! the address matches `NonNull::<()>::dangling()`. + //! The way Kani tracks provenance is not enough to check if the address was the result of a cast + //! from a non-zero integer literal. + //! kani_core::kani_mem!(std); } mod mem_init { + //! This module provides instrumentation for tracking memory initialization of raw pointers. + //! + //! Currently, memory initialization is tracked on per-byte basis, so each byte of memory pointed to + //! by raw pointers could be either initialized or uninitialized. Padding bytes are always + //! considered uninitialized when read as data bytes. Each type has a type layout to specify which + //! bytes are considered to be data and which -- padding. This is determined at compile time and + //! statically injected into the program (see `Layout`). + //! + //! Compiler automatically inserts calls to `is_xxx_initialized` and `set_xxx_initialized` at + //! appropriate locations to get or set the initialization status of the memory pointed to. + //! + //! Note that for each harness, tracked object and tracked offset are chosen non-deterministically, + //! so calls to `is_xxx_initialized` should be only used in assertion contexts. kani_core::kani_mem_init!(std); } }; diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index c09d67ca51ff..586f2779b4c6 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -1,41 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains functions useful for checking unsafe memory access. -//! -//! Given the following validity rules provided in the Rust documentation: -//! (accessed Feb 6th, 2024) -//! -//! 1. A null pointer is never valid, not even for accesses of size zero. -//! 2. 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. -//! ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory, -//! i.e., deallocation makes pointers invalid even for zero-sized operations.~~ -//! ZST access is not OK for any pointer. -//! See: -//! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized -//! accesses, even if some memory happens to exist at that address and gets deallocated. -//! This corresponds to writing your own allocator: allocating zero-sized objects is not very -//! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is -//! `NonNull::dangling`. -//! 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 and #2 today. -//! -//! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if -//! the address matches `NonNull::<()>::dangling()`. -//! The way Kani tracks provenance is not enough to check if the address was the result of a cast -//! from a non-zero integer literal. -//! + // TODO: This module is currently tightly coupled with CBMC's memory model, and it needs some // refactoring to be used with other backends. diff --git a/library/kani_core/src/mem_init.rs b/library/kani_core/src/mem_init.rs index 935f14d71c5d..2564de20c77d 100644 --- a/library/kani_core/src/mem_init.rs +++ b/library/kani_core/src/mem_init.rs @@ -1,20 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module provides instrumentation for tracking memory initialization of raw pointers. -//! -//! Currently, memory initialization is tracked on per-byte basis, so each byte of memory pointed to -//! by raw pointers could be either initialized or uninitialized. Padding bytes are always -//! considered uninitialized when read as data bytes. Each type has a type layout to specify which -//! bytes are considered to be data and which -- padding. This is determined at compile time and -//! statically injected into the program (see `Layout`). -//! -//! Compiler automatically inserts calls to `is_xxx_initialized` and `set_xxx_initialized` at -//! appropriate locations to get or set the initialization status of the memory pointed to. -//! -//! Note that for each harness, tracked object and tracked offset are chosen non-deterministically, -//! so calls to `is_xxx_initialized` should be only used in assertion contexts. - // Definitions in this module are not meant to be visible to the end user, only the compiler. #![allow(dead_code)]