Add fn that checks pointers point to same allocation (#3583)

This changes adds a new function that returns whether two pointers
points to the same allocated object. Since we cannot reason about
addresses to objects that are dead or haven't been allocated, we panic
if the user provides dangling pointers.

## Call-out:

- Creating this as draft for now for early feedback

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

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 {
             <T as Pointee>::Metadata: PtrProperties<T>,
         {
             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<T>(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<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/expected/shadow/unsupported_num_objects/test.rs

@@ -16,13 +16,11 @@ fn check_max_objects<const N: usize>() {
     // - the object ID for `i`
     while i < N {
         let x: Box<usize> = 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 {

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));
+}