From f46a41d0a194cf670c59ded1288b5aec6399d242 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 8 Oct 2024 16:16:32 -0700 Subject: [PATCH 1/3] Add fn that checks pointers point to same allocation --- library/kani_core/src/mem.rs | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 34cff4b17ad7..0676f4e2256c 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -154,13 +154,34 @@ 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. + /// + /// Note that a pointer is still 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 { + let obj1 = crate::mem::pointer_object(ptr1); + (obj1 == crate::mem::pointer_object(ptr2)) && { + super::assert( + unsafe { is_allocated(obj1 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) } + } + } + /// 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` From 5e335cd8c80b0b2598a9fca5137519d6ee619b99 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 15 Oct 2024 19:11:01 -0700 Subject: [PATCH 2/3] Finish implementation + add test --- library/kani_core/src/mem.rs | 40 +++++++++------ tests/kani/MemPredicates/same_allocation.rs | 56 +++++++++++++++++++++ 2 files changed, 81 insertions(+), 15 deletions(-) create mode 100644 tests/kani/MemPredicates/same_allocation.rs diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 0676f4e2256c..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] @@ -164,7 +167,7 @@ macro_rules! kani_mem { /// Check if two pointers points to the same allocated object, and that both pointers /// are in bounds of that object. /// - /// Note that a pointer is still in-bounds if it points to 1-byte past the allocation. + /// 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, @@ -172,14 +175,7 @@ macro_rules! kani_mem { )] #[allow(clippy::not_unsafe_ptr_arg_deref)] pub fn same_allocation(ptr1: *const T, ptr2: *const T) -> bool { - let obj1 = crate::mem::pointer_object(ptr1); - (obj1 == crate::mem::pointer_object(ptr2)) && { - super::assert( - unsafe { is_allocated(obj1 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) } - } + cbmc::same_allocation(ptr1, ptr2) } /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. @@ -338,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/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)); +} From a5bf2e30fdb3c72ed8cc77eb7888fcec53a65a56 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 15 Oct 2024 20:12:05 -0700 Subject: [PATCH 3/3] Remove call to pointer_object from test The test doesn't need the calls --- tests/expected/shadow/unsupported_num_objects/test.rs | 2 -- 1 file changed, 2 deletions(-) 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 {