Add an experimental API for shadow memory (#3200)

Introduces a data structure, `ShadowMem<T>`, with two methods:
```rust
pub fn set<U>(&mut self, ptr: *const U, val: T)
pub fn get<U>(&self, ptr: *const U) -> T
```
for setting and getting values of type `T` associated with the memory location that `ptr` points to.

Towards #3184 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -242,6 +242,74 @@ impl GotocHook for IsAllocated {
     }
 }
 
+/// Encodes __CPROVER_pointer_object(ptr)
+struct PointerObject;
+impl GotocHook for PointerObject {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniPointerObject")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 1);
+        let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer());
+        let target = target.unwrap();
+        let loc = gcx.codegen_caller_span_stable(span);
+        let ret_place =
+            unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to));
+        let ret_type = ret_place.goto_expr.typ().clone();
+
+        Stmt::block(
+            vec![
+                ret_place.goto_expr.assign(Expr::pointer_object(ptr).cast_to(ret_type), loc),
+                Stmt::goto(bb_label(target), loc),
+            ],
+            loc,
+        )
+    }
+}
+
+/// Encodes __CPROVER_pointer_offset(ptr)
+struct PointerOffset;
+impl GotocHook for PointerOffset {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniPointerOffset")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 1);
+        let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer());
+        let target = target.unwrap();
+        let loc = gcx.codegen_caller_span_stable(span);
+        let ret_place =
+            unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to));
+        let ret_type = ret_place.goto_expr.typ().clone();
+
+        Stmt::block(
+            vec![
+                ret_place.goto_expr.assign(Expr::pointer_offset(ptr).cast_to(ret_type), loc),
+                Stmt::goto(bb_label(target), loc),
+            ],
+            loc,
+        )
+    }
+}
+
 struct RustAlloc;
 // Removing this hook causes regression failures.
 // https://github.com/model-checking/kani/issues/1170
@@ -399,6 +467,8 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(Cover),
             Rc::new(Nondet),
             Rc::new(IsAllocated),
+            Rc::new(PointerObject),
+            Rc::new(PointerOffset),
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
             Rc::new(UntrackedDeref),

kani_metadata/src/unstable.rs

@@ -87,6 +87,8 @@ pub enum UnstableFeature {
     /// Automatically check that no invalid value is produced which is considered UB in Rust.
     /// Note that this does not include checking uninitialized value.
     ValidValueChecks,
+    /// Ghost state and shadow memory APIs
+    GhostState,
 }
 
 impl UnstableFeature {

library/kani/src/lib.rs

@@ -24,6 +24,7 @@ pub mod arbitrary;
 mod concrete_playback;
 pub mod futures;
 pub mod mem;
+pub mod shadow;
 pub mod slice;
 pub mod tuple;
 pub mod vec;

library/kani/src/mem.rs

@@ -290,6 +290,20 @@ unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
     kani_intrinsic()
 }
 
+/// Get the object ID of the given pointer.
+#[rustc_diagnostic_item = "KaniPointerObject"]
+#[inline(never)]
+pub fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
+    kani_intrinsic()
+}
+
+/// Get the object offset of the given pointer.
+#[rustc_diagnostic_item = "KaniPointerOffset"]
+#[inline(never)]
+pub fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
+    kani_intrinsic()
+}
+
 #[cfg(test)]
 mod tests {
     use super::{can_dereference, can_write, PtrProperties};

library/kani/src/shadow.rs

@@ -0,0 +1,83 @@
+// 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::<u8>());
+//!     // 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;
+
+const MAX_NUM_OBJECTS_ASSERT_MSG: &str = "The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024)";
+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<T: Copy> {
+    mem: [[T; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS],
+}
+
+impl<T: Copy> ShadowMem<T> {
+    /// Create a new shadow memory instance initialized with the given value
+    #[crate::unstable(
+        feature = "ghost-state",
+        issue = 3184,
+        reason = "experimental ghost state/shadow memory API"
+    )]
+    pub const fn new(val: T) -> Self {
+        Self { mem: [[val; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] }
+    }
+
+    /// Get the shadow memory value of the given pointer
+    #[crate::unstable(
+        feature = "ghost-state",
+        issue = 3184,
+        reason = "experimental ghost state/shadow memory API"
+    )]
+    pub fn get<U>(&self, ptr: *const U) -> T {
+        let obj = crate::mem::pointer_object(ptr);
+        let offset = crate::mem::pointer_offset(ptr);
+        crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG);
+        crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG);
+        self.mem[obj][offset]
+    }
+
+    /// Set the shadow memory value of the given pointer
+    #[crate::unstable(
+        feature = "ghost-state",
+        issue = 3184,
+        reason = "experimental ghost state/shadow memory API"
+    )]
+    pub fn set<U>(&mut self, ptr: *const U, val: T) {
+        let obj = crate::mem::pointer_object(ptr);
+        let offset = crate::mem::pointer_offset(ptr);
+        crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG);
+        crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG);
+        self.mem[obj][offset] = val;
+    }
+}

tests/expected/shadow/uninit_array/expected

@@ -0,0 +1,3 @@
+Failed Checks: assertion failed: SM.get(p)
+Verification failed for - check_init_any
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/expected/shadow/uninit_array/test.rs

@@ -0,0 +1,59 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zghost-state
+
+// This is a basic test for the shadow memory implementation.
+// It checks that shadow memory can be used to track whether a memory location
+// is initialized.
+
+use std::alloc::{alloc, dealloc, Layout};
+
+static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
+
+fn write(ptr: *mut i8, offset: usize, x: i8) {
+    unsafe {
+        let p = ptr.offset(offset as isize);
+        p.write(x);
+        SM.set(p as *const i8, true);
+    };
+}
+
+fn check_init(b: bool) {
+    // allocate an array of 5 i8's
+    let layout = Layout::array::<i8>(5).unwrap();
+    let ptr = unsafe { alloc(layout) as *mut i8 };
+
+    // unconditionally write to all 5 locations except for the middle element
+    write(ptr, 0, 0);
+    write(ptr, 1, 1);
+    if b {
+        write(ptr, 2, 2)
+    };
+    write(ptr, 3, 3);
+    write(ptr, 4, 4);
+
+    // non-deterministically read from any of the elements and assert that:
+    // 1. The memory location is initialized
+    // 2. It has the expected value
+    // This would fail if `b` is false and `index == 2`
+    let index: usize = kani::any();
+    if index < 5 {
+        unsafe {
+            let p = ptr.offset(index as isize);
+            let x = p.read();
+            assert!(SM.get(p));
+            assert_eq!(x, index as i8);
+        }
+    }
+    unsafe { dealloc(ptr as *mut u8, layout) };
+}
+
+#[kani::proof]
+fn check_init_true() {
+    check_init(true);
+}
+
+#[kani::proof]
+fn check_init_any() {
+    check_init(kani::any());
+}

tests/expected/shadow/unsupported_num_objects/expected

@@ -0,0 +1,3 @@
+Failed Checks: The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024)
+Verification failed for - check_max_objects_fail
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/expected/shadow/unsupported_num_objects/test.rs

@@ -0,0 +1,41 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zghost-state
+
+// This test checks the maximum number of objects supported by Kani's shadow
+// memory model (currently 1024)
+
+static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
+
+fn check_max_objects<const N: usize>() {
+    let mut i = 0;
+    // A dummy loop that creates `N`` objects.
+    // After the loop, CBMC's object ID counter should be at `N` + 2:
+    // - `N` created in the loop +
+    // - the NULL pointer whose object ID is 0, and
+    // - the object ID for `i`
+    while i < N {
+        let x = i;
+        assert_eq!(kani::mem::pointer_object(&x as *const usize), i + 2);
+        i += 1;
+    }
+
+    // create a new object whose ID is `N` + 2
+    let x = 42;
+    assert_eq!(kani::mem::pointer_object(&x as *const i32), N + 2);
+    // the following call to `set` would fail if the object ID for `x` exceeds
+    // the maximum allowed by Kani's shadow memory model
+    unsafe {
+        SM.set(&x as *const i32, true);
+    }
+}
+
+#[kani::proof]
+fn check_max_objects_pass() {
+    check_max_objects::<1021>();
+}
+
+#[kani::proof]
+fn check_max_objects_fail() {
+    check_max_objects::<1022>();
+}

tests/expected/shadow/unsupported_object_size/expected

@@ -0,0 +1,3 @@
+Failed Checks: The object size exceeds the maximum size supported by Kani's shadow memory model (64)
+Verification failed for - check_max_object_size_fail
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/expected/shadow/unsupported_object_size/test.rs

@@ -0,0 +1,29 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zghost-state
+
+// This test checks the maximum object size supported by Kani's shadow
+// memory model (currently 64)
+
+static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
+
+fn check_max_objects<const N: usize>() {
+    let arr: [u8; N] = [0; N];
+    let last = &arr[N - 1];
+    assert_eq!(kani::mem::pointer_offset(last as *const u8), N - 1);
+    // the following call to `set_init` would fail if the object offset for
+    // `last` exceeds the maximum allowed by Kani's shadow memory model
+    unsafe {
+        SM.set(last as *const u8, true);
+    }
+}
+
+#[kani::proof]
+fn check_max_object_size_pass() {
+    check_max_objects::<64>();
+}
+
+#[kani::proof]
+fn check_max_object_size_fail() {
+    check_max_objects::<65>();
+}