diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 34cff4b17ad7..c8501e977096 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -35,6 +35,9 @@ //! 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. #[allow(clippy::crate_in_macro_def)] #[macro_export] @@ -154,13 +157,27 @@ macro_rules! kani_mem { ::Metadata: PtrProperties, { let (thin_ptr, metadata) = ptr.to_raw_parts(); - // Need to assert `is_initialized` because non-determinism is used under the hood, so it - // does not make sense to use it inside assumption context. + // Need to assert `is_initialized` because non-determinism is used under the hood, so it + // does not make sense to use it inside assumption context. is_inbounds(&metadata, thin_ptr) && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } + /// Check if two pointers points to the same allocated object, and that both pointers + /// are in bounds of that object. + /// + /// A pointer is still considered in-bounds if it points to 1-byte past the allocation. + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] + #[allow(clippy::not_unsafe_ptr_arg_deref)] + pub fn same_allocation(ptr1: *const T, ptr2: *const T) -> bool { + cbmc::same_allocation(ptr1, ptr2) + } + /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. /// /// This will panic if `data_ptr` points to an invalid `non_null` @@ -317,16 +334,30 @@ macro_rules! kani_mem { true } + pub(super) mod cbmc { + use super::*; + /// CBMC specific implementation of [super::same_allocation]. + pub fn same_allocation(ptr1: *const T, ptr2: *const T) -> bool { + let obj1 = crate::kani::mem::pointer_object(ptr1); + (obj1 == crate::kani::mem::pointer_object(ptr2)) && { + crate::kani::assert( + unsafe { + is_allocated(ptr1 as *const (), 0) || is_allocated(ptr2 as *const (), 0) + }, + "Kani does not support reasoning about pointer to unallocated memory", + ); + unsafe { + is_allocated(ptr1 as *const (), 0) && is_allocated(ptr2 as *const (), 0) + } + } + } + } + /// Get the object ID of the given pointer. #[doc(hidden)] - #[crate::kani::unstable_feature( - feature = "ghost-state", - issue = 3184, - reason = "experimental ghost state/shadow memory API" - )] #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] - pub fn pointer_object(_ptr: *const T) -> usize { + pub(crate) fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } diff --git a/tests/expected/shadow/unsupported_num_objects/test.rs b/tests/expected/shadow/unsupported_num_objects/test.rs index 88b1171ef09d..bb9233afc648 100644 --- a/tests/expected/shadow/unsupported_num_objects/test.rs +++ b/tests/expected/shadow/unsupported_num_objects/test.rs @@ -16,13 +16,11 @@ fn check_max_objects() { // - the object ID for `i` while i < N { let x: Box = Box::new(i); - assert_eq!(kani::mem::pointer_object(&*x as *const usize), 2 * 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), 2 * 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 { diff --git a/tests/kani/MemPredicates/same_allocation.rs b/tests/kani/MemPredicates/same_allocation.rs new file mode 100644 index 000000000000..63d59e857ba2 --- /dev/null +++ b/tests/kani/MemPredicates/same_allocation.rs @@ -0,0 +1,56 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z mem-predicates +//! Check same allocation predicate. + +extern crate kani; + +use kani::mem::same_allocation; +use kani::{AllocationStatus, ArbitraryPointer, PointerGenerator}; + +#[kani::proof] +fn check_inbounds() { + let mut generator = PointerGenerator::<100>::new(); + let ArbitraryPointer { ptr: ptr1, .. } = generator.any_in_bounds::(); + let ArbitraryPointer { ptr: ptr2, .. } = generator.any_in_bounds::(); + assert!(same_allocation(ptr1, ptr2)); +} + +#[kani::proof] +fn check_inbounds_other_alloc() { + let mut generator1 = PointerGenerator::<100>::new(); + let mut generator2 = PointerGenerator::<100>::new(); + let ArbitraryPointer { ptr: ptr1, .. } = generator1.any_in_bounds::(); + let ArbitraryPointer { ptr: ptr2, .. } = generator2.any_in_bounds::(); + assert!(!same_allocation(ptr1, ptr2)); +} + +#[kani::proof] +fn check_dangling() { + let mut generator = PointerGenerator::<100>::new(); + let ArbitraryPointer { ptr: ptr1, status: status1, .. } = generator.any_alloc_status::(); + let ArbitraryPointer { ptr: ptr2, status: status2, .. } = generator.any_alloc_status::(); + kani::assume(status1 == AllocationStatus::Dangling && status2 == AllocationStatus::InBounds); + assert!(!same_allocation(ptr1, ptr2)); +} + +#[kani::proof] +fn check_one_dead() { + let mut generator = PointerGenerator::<100>::new(); + let ArbitraryPointer { ptr: ptr1, status: status1, .. } = generator.any_alloc_status::(); + let ArbitraryPointer { ptr: ptr2, status: status2, .. } = generator.any_alloc_status::(); + kani::assume(status1 == AllocationStatus::DeadObject && status2 == AllocationStatus::InBounds); + assert!(!same_allocation(ptr1, ptr2)); +} + +#[kani::proof] +fn check_dyn_alloc() { + let mut generator1 = Box::new(PointerGenerator::<100>::new()); + let mut generator2 = Box::new(PointerGenerator::<100>::new()); + let ArbitraryPointer { ptr: ptr1a, .. } = generator1.any_in_bounds::(); + let ArbitraryPointer { ptr: ptr1b, .. } = generator1.any_in_bounds::(); + assert!(same_allocation(ptr1a, ptr1b)); + + let ArbitraryPointer { ptr: ptr2, .. } = generator2.any_in_bounds::(); + assert!(!same_allocation(ptr1a, ptr2)); +}