Add fn that checks pointers point to same allocation

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,22 +167,15 @@ 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,
             reason = "experimental memory predicate API"
         )]
         #[allow(clippy::not_unsafe_ptr_arg_deref)]
         pub fn same_allocation<T>(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<T>(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<T: ?Sized>(_ptr: *const T) -> usize {
+        pub(crate) fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
             kani_intrinsic()
         }
 

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::<u8>();
+    let ArbitraryPointer { ptr: ptr2, .. } = generator.any_in_bounds::<u8>();
+    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::<u8>();
+    let ArbitraryPointer { ptr: ptr2, .. } = generator2.any_in_bounds::<u8>();
+    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::<u8>();
+    let ArbitraryPointer { ptr: ptr2, status: status2, .. } = generator.any_alloc_status::<u8>();
+    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::<u8>();
+    let ArbitraryPointer { ptr: ptr2, status: status2, .. } = generator.any_alloc_status::<u8>();
+    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::<u8>();
+    let ArbitraryPointer { ptr: ptr1b, .. } = generator1.any_in_bounds::<u8>();
+    assert!(same_allocation(ptr1a, ptr1b));
+
+    let ArbitraryPointer { ptr: ptr2, .. } = generator2.any_in_bounds::<u8>();
+    assert!(!same_allocation(ptr1a, ptr2));
+}