Fix regression

library/kani/src/mem.rs

@@ -63,6 +63,10 @@ where
     T: ?Sized,
     <T as Pointee>::Metadata: PtrProperties<T>,
 {
+    // The interface takes a mutable pointer to improve readability of the signature.
+    // However, using constant pointer avoid unnecessary instrumentation, and it is as powerful.
+    // Hence, cast to `*const T`.
+    let ptr: *const T = ptr;
     let (thin_ptr, metadata) = ptr.to_raw_parts();
     metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr)
 }
@@ -244,6 +248,10 @@ unsafe fn is_allocated(_ptr: *const (), _size: usize) -> bool {
 }
 
 /// Check if the value stored in the given location satisfies type `T` validity requirements.
+///
+/// # Safety
+///
+/// - Users have to ensure that the pointer is aligned the pointed memory is allocated.
 #[rustc_diagnostic_item = "KaniValidValue"]
 #[inline(never)]
 unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
@@ -252,7 +260,7 @@ unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
 
 #[cfg(test)]
 mod tests {
-    use super::{can_write, PtrProperties};
+    use super::{can_dereference, can_write, PtrProperties};
     use crate::mem::private::Internal;
     use std::fmt::Debug;
     use std::intrinsics::size_of;
@@ -306,39 +314,42 @@ mod tests {
 
     #[test]
     pub fn test_empty_slice() {
-        let slice_ptr = Vec::<char>::new().as_slice() as *const [char];
-        can_write(slice_ptr);
+        let slice_ptr = Vec::<char>::new().as_mut_slice() as *mut [char];
+        assert!(can_write(slice_ptr));
     }
 
     #[test]
     pub fn test_empty_str() {
-        let slice_ptr = String::new().as_str() as *const str;
-        can_write(slice_ptr);
+        let slice_ptr = String::new().as_mut_str() as *mut str;
+        assert!(can_write(slice_ptr));
     }
 
     #[test]
     fn test_dangling_zst() {
-        test_dangling_of_t::<()>();
-        test_dangling_of_t::<[(); 10]>();
+        test_dangling_of_zst::<()>();
+        test_dangling_of_zst::<[(); 10]>();
     }
 
-    fn test_dangling_of_t<T>() {
-        let dangling: *const T = NonNull::<T>::dangling().as_ptr();
-        can_write(dangling);
+    fn test_dangling_of_zst<T>() {
+        let dangling: *mut T = NonNull::<T>::dangling().as_ptr();
+        assert!(can_write(dangling));
 
-        let vec_ptr = Vec::<T>::new().as_ptr();
-        can_write(vec_ptr);
+        let vec_ptr = Vec::<T>::new().as_mut_ptr();
+        assert!(can_write(vec_ptr));
     }
 
     #[test]
-    #[should_panic(expected = "Expected valid pointer, but found `null`")]
     fn test_null_fat_ptr() {
-        can_write(ptr::null::<char>() as *const dyn Debug);
+        assert!(!can_dereference(ptr::null::<char>() as *const dyn Debug));
     }
 
     #[test]
-    #[should_panic(expected = "Expected valid pointer, but found `null`")]
     fn test_null_char() {
-        can_write(ptr::null::<char>());
+        assert!(!can_dereference(ptr::null::<char>()));
+    }
+
+    #[test]
+    fn test_null_mut() {
+        assert!(!can_write(ptr::null_mut::<String>()));
     }
 }

tests/kani/MemPredicates/fat_ptr_validity.rs

@@ -5,24 +5,22 @@
 
 extern crate kani;
 
-use kani::mem::assert_valid_ptr;
+use kani::mem::{can_dereference, can_write};
 
 mod valid_access {
     use super::*;
     #[kani::proof]
     pub fn check_valid_dyn_ptr() {
-        let boxed: Box<dyn PartialEq<u8>> = Box::new(10u8);
-        let raw_ptr = Box::into_raw(boxed);
-        assert_valid_ptr(raw_ptr);
-        let boxed = unsafe { Box::from_raw(raw_ptr) };
-        assert_ne!(*boxed, 0);
+        let mut var = 10u8;
+        let fat_ptr: *mut dyn PartialEq<u8> = &mut var as *mut _;
+        assert!(can_write(fat_ptr));
     }
 
     #[kani::proof]
     pub fn check_valid_slice_ptr() {
         let array = ['a', 'b', 'c'];
         let slice = &array as *const [char];
-        assert_valid_ptr(slice);
+        assert!(can_dereference(slice));
         assert_eq!(unsafe { &*slice }[0], 'a');
         assert_eq!(unsafe { &*slice }[2], 'c');
     }
@@ -43,14 +41,14 @@ mod invalid_access {
     #[kani::should_panic]
     pub fn check_invalid_dyn_ptr() {
         let raw_ptr: *const dyn PartialEq<u8> = unsafe { new_dead_ptr::<u8>(0) };
-        assert_valid_ptr(raw_ptr);
+        assert!(can_dereference(raw_ptr));
     }
 
     #[kani::proof]
     #[kani::should_panic]
     pub fn check_invalid_slice_ptr() {
         let raw_ptr: *const [char] = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) };
-        assert_valid_ptr(raw_ptr);
+        assert!(can_dereference(raw_ptr));
     }
 
     #[kani::proof]
@@ -59,7 +57,7 @@ mod invalid_access {
         let array = [10usize; 10];
         let invalid: *const [usize; 11] = &array as *const [usize; 10] as *const [usize; 11];
         let ptr: *const [usize] = invalid as *const _;
-        assert_valid_ptr(ptr);
+        assert!(can_dereference(ptr));
     }
 
     unsafe fn new_dead_ptr<T>(val: T) -> *const T {

tests/kani/MemPredicates/thin_ptr_validity.rs

@@ -5,27 +5,27 @@
 
 extern crate kani;
 
-use kani::mem::assert_valid_ptr;
+use kani::mem::can_dereference;
 use std::ptr::NonNull;
 
 mod valid_access {
     use super::*;
     #[kani::proof]
     pub fn check_dangling_zst() {
         let dangling = NonNull::<()>::dangling().as_ptr();
-        assert_valid_ptr(dangling);
+        assert!(can_dereference(dangling));
 
         let vec_ptr = Vec::<()>::new().as_ptr();
-        assert_valid_ptr(vec_ptr);
+        assert!(can_dereference(vec_ptr));
 
         let dangling = NonNull::<[char; 0]>::dangling().as_ptr();
-        assert_valid_ptr(dangling);
+        assert!(can_dereference(dangling));
     }
 
     #[kani::proof]
     pub fn check_valid_array() {
         let array = ['a', 'b', 'c'];
-        assert_valid_ptr(&array);
+        assert!(can_dereference(&array));
     }
 }
 
@@ -35,22 +35,22 @@ mod invalid_access {
     #[kani::should_panic]
     pub fn check_invalid_ptr() {
         let raw_ptr = unsafe { new_dead_ptr::<u8>(0) };
-        assert_valid_ptr(raw_ptr);
+        assert!(!can_dereference(raw_ptr));
     }
 
     #[kani::proof]
     #[kani::should_panic]
     pub fn check_invalid_array() {
         let raw_ptr = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) };
-        assert_valid_ptr(raw_ptr);
+        assert!(can_dereference(raw_ptr));
     }
 
     #[kani::proof]
     pub fn check_invalid_zst() {
         let raw_ptr: *const [char; 0] =
             unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) } as *const _;
         // ZST pointer are always valid
-        assert_valid_ptr(raw_ptr);
+        assert!(can_dereference(raw_ptr));
     }
 
     unsafe fn new_dead_ptr<T>(val: T) -> *const T {