Add fn that checks pointers point to same allocation

library/kani_core/src/mem.rs

@@ -154,13 +154,34 @@ 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.
+        ///
+        /// 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<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) }
+            }
+        }
+
         /// 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`