diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 9f70c16430e5..9b2f9e770d32 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/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, + assign_to: &Place, + target: Option, + 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, + assign_to: &Place, + target: Option, + 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), diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 878b468dbdc3..d7b73678a836 100644 --- a/kani_metadata/src/unstable.rs +++ b/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 { diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 25b1b389a2b1..341dd6752916 100644 --- a/library/kani/src/lib.rs +++ b/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; diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs index c485ee16a562..c40a1aa696e3 100644 --- a/library/kani/src/mem.rs +++ b/library/kani/src/mem.rs @@ -290,6 +290,20 @@ unsafe fn has_valid_value(_ptr: *const T) -> bool { kani_intrinsic() } +/// Get the object ID of the given pointer. +#[rustc_diagnostic_item = "KaniPointerObject"] +#[inline(never)] +pub fn pointer_object(_ptr: *const T) -> usize { + kani_intrinsic() +} + +/// Get the object offset of the given pointer. +#[rustc_diagnostic_item = "KaniPointerOffset"] +#[inline(never)] +pub fn pointer_offset(_ptr: *const T) -> usize { + kani_intrinsic() +} + #[cfg(test)] mod tests { use super::{can_dereference, can_write, PtrProperties}; diff --git a/library/kani/src/shadow.rs b/library/kani/src/shadow.rs new file mode 100644 index 000000000000..a7ea57c6fd40 --- /dev/null +++ b/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::()); +//! // 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 { + mem: [[T; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], +} + +impl ShadowMem { + /// 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(&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(&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; + } +} diff --git a/tests/expected/shadow/uninit_array/expected b/tests/expected/shadow/uninit_array/expected new file mode 100644 index 000000000000..1d5f70698010 --- /dev/null +++ b/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. diff --git a/tests/expected/shadow/uninit_array/test.rs b/tests/expected/shadow/uninit_array/test.rs new file mode 100644 index 000000000000..8a9536e5a8e8 --- /dev/null +++ b/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 = 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::(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()); +} diff --git a/tests/expected/shadow/unsupported_num_objects/expected b/tests/expected/shadow/unsupported_num_objects/expected new file mode 100644 index 000000000000..da3b5a671969 --- /dev/null +++ b/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. diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs new file mode 100644 index 000000000000..f60d0020e989 --- /dev/null +++ b/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 = kani::shadow::ShadowMem::new(false); + +fn check_max_objects() { + 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>(); +} diff --git a/tests/expected/shadow/unsupported_object_size/expected b/tests/expected/shadow/unsupported_object_size/expected new file mode 100644 index 000000000000..a4598b5aac82 --- /dev/null +++ b/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. diff --git a/tests/expected/shadow/unsupported_object_size/test.rs b/tests/expected/shadow/unsupported_object_size/test.rs new file mode 100644 index 000000000000..d22ff1a6ca41 --- /dev/null +++ b/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 = kani::shadow::ShadowMem::new(false); + +fn check_max_objects() { + 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>(); +}