From 4490c38a1c980f0e32054d691330ae2172efd306 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 31 May 2024 16:26:23 -0700 Subject: [PATCH] Add module documentation --- library/kani/src/shadow.rs | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs index 3c51757a4125..a7ea57c6fd40 100644 --- a/library/kani/src/shadow.rs +++ b/library/kani/src/shadow.rs @@ -1,6 +1,32 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains an API for shadow memory. +//! Shadow memory is a mechanism by which we can store metadata on memory +//! locations, e.g. whether a memory location is initialized. +//! +//! The main data structure provided by this module is the `ShadowMem` struct, +//! which allows us to store metadata on a given memory location. +//! +//! # Example +//! +//! ``` +//! use kani::shadow::ShadowMem; +//! use std::alloc::{alloc, Layout}; +//! +//! let mut sm = ShadowMem::new(false); +//! +//! unsafe { +//! let ptr = alloc(Layout::new::()); +//! // assert the memory location is not initialized +//! assert!(!sm.get(ptr)); +//! // write to the memory location +//! *ptr = 42; +//! // update the shadow memory to indicate that this location is now initialized +//! sm.set(ptr, true); +//! } +//! ``` + const MAX_NUM_OBJECTS: usize = 1024; const MAX_OBJECT_SIZE: usize = 64; @@ -8,6 +34,10 @@ const MAX_NUM_OBJECTS_ASSERT_MSG: &str = "The number of objects exceeds the maxi const MAX_OBJECT_SIZE_ASSERT_MSG: &str = "The object size exceeds the maximum size supported by Kani's shadow memory model (64)"; +/// A shadow memory data structure that contains a two-dimensional array of a +/// generic type `T`. +/// Each element of the outer array represents an object, and each element of +/// the inner array represents a byte in the object. pub struct ShadowMem { mem: [[T; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], }