Merge branch 'main' into cbmc-6.4.0

model-checking · Nov 6, 2024 · be8085a · be8085a
2 parents 0338dcd + 4aa739f
commit be8085a
Show file tree

Hide file tree

Showing 2 changed files with 51 additions and 10 deletions.
diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
@@ -174,7 +174,7 @@ macro_rules! kani_mem {
             reason = "experimental memory predicate API"
         )]
         #[allow(clippy::not_unsafe_ptr_arg_deref)]
-        pub fn same_allocation<T>(ptr1: *const T, ptr2: *const T) -> bool {
+        pub fn same_allocation<T: ?Sized>(ptr1: *const T, ptr2: *const T) -> bool {
             cbmc::same_allocation(ptr1, ptr2)
         }
 
@@ -337,18 +337,16 @@ macro_rules! kani_mem {
         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)) && {
+            pub fn same_allocation<T: ?Sized>(ptr1: *const T, ptr2: *const T) -> bool {
+                let addr1 = ptr1 as *const ();
+                let addr2 = ptr2 as *const ();
+                let obj1 = crate::kani::mem::pointer_object(addr1);
+                (obj1 == crate::kani::mem::pointer_object(addr2)) && {
                     crate::kani::assert(
-                        unsafe {
-                            is_allocated(ptr1 as *const (), 0) || is_allocated(ptr2 as *const (), 0)
-                        },
+                        unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) },
                         "Kani does not support reasoning about pointer to unallocated memory",
                     );
-                    unsafe {
-                        is_allocated(ptr1 as *const (), 0) && is_allocated(ptr2 as *const (), 0)
-                    }
+                    unsafe { is_allocated(addr1, 0) && is_allocated(addr2, 0) }
                 }
             }
         }

diff --git a/tests/kani/MemPredicates/same_allocation.rs b/tests/kani/MemPredicates/same_allocation.rs
@@ -7,6 +7,7 @@ extern crate kani;
 
 use kani::mem::same_allocation;
 use kani::{AllocationStatus, ArbitraryPointer, PointerGenerator};
+use std::any::Any;
 
 #[kani::proof]
 fn check_inbounds() {
@@ -54,3 +55,45 @@ fn check_dyn_alloc() {
     let ArbitraryPointer { ptr: ptr2, .. } = generator2.any_in_bounds::<u8>();
     assert!(!same_allocation(ptr1a, ptr2));
 }
+
+#[kani::proof]
+fn check_same_alloc_dyn_ptr() {
+    let mut generator = PointerGenerator::<100>::new();
+    let ArbitraryPointer { ptr: ptr1, .. } = generator.any_in_bounds::<()>();
+    let ArbitraryPointer { ptr: ptr2, .. } = generator.any_in_bounds::<char>();
+    let dyn_1 = ptr1 as *const dyn Any;
+    let dyn_2 = ptr2 as *const dyn Any;
+    assert!(same_allocation(dyn_1, dyn_2));
+}
+
+#[kani::proof]
+fn check_not_same_alloc_dyn_ptr() {
+    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::<char>();
+    let dyn_1 = ptr1 as *const dyn Any;
+    let dyn_2 = ptr2 as *const dyn Any;
+    assert!(!same_allocation(dyn_1, dyn_2));
+}
+
+#[kani::proof]
+fn check_same_alloc_slice() {
+    let mut generator = PointerGenerator::<100>::new();
+    let ArbitraryPointer { ptr: ptr1, .. } = generator.any_in_bounds::<[u16; 4]>();
+    let ArbitraryPointer { ptr: ptr2, .. } = generator.any_in_bounds::<[u16; 10]>();
+    let slice_1 = ptr1 as *const [_];
+    let slice_2 = ptr2 as *const [_];
+    assert!(same_allocation(slice_1, slice_2));
+}
+
+#[kani::proof]
+fn check_not_same_alloc_slice() {
+    let mut generator1 = PointerGenerator::<100>::new();
+    let mut generator2 = PointerGenerator::<100>::new();
+    let ArbitraryPointer { ptr: ptr1, .. } = generator1.any_in_bounds::<[u16; 4]>();
+    let ArbitraryPointer { ptr: ptr2, .. } = generator2.any_in_bounds::<[u16; 10]>();
+    let slice_1 = ptr1 as *const [_];
+    let slice_2 = ptr2 as *const [_];
+    assert!(!same_allocation(slice_1, slice_2));
+}