Fix regression

Author: celinval

kani-compiler/src/kani_middle/transform/check_values.rs

@@ -505,11 +505,27 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
                         // We only care about *mut T as *mut U
                         return;
                     };
+                    if dest_pointee_ty.kind().is_unit() {
+                        // Ignore cast to *mut () since nothing can be written to it.
+                        // This is a common pattern
+                        return;
+                    }
+
                     let src_ty = op.ty(self.locals).unwrap();
                     debug!(?src_ty, ?dest_ty, "visit_rvalue mutcast");
                     let TyKind::RigidTy(RigidTy::RawPtr(src_pointee_ty, _)) = src_ty.kind() else {
                         unreachable!()
                     };
+
+                    if src_pointee_ty.kind().is_unit() {
+                        // We cannot track what was the initial type. Thus, fail.
+                        self.push_target(SourceOp::UnsupportedCheck {
+                            check: "mutable cast".to_string(),
+                            ty: src_ty,
+                        });
+                        return;
+                    }
+
                     if let Ok(src_validity) =
                         ty_validity_per_offset(&self.machine, src_pointee_ty, 0)
                     {
@@ -558,6 +574,8 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
                         })
                     }
                 }
+                // `DynStar` is not currently supported in Kani.
+                // TODO: https://github.com/model-checking/kani/issues/1784
                 CastKind::DynStar => self.push_target(UnsupportedCheck {
                     check: "Dyn*".to_string(),
                     ty: (rvalue.ty(self.locals).unwrap()),

library/kani/src/mem.rs

@@ -63,16 +63,23 @@ 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)
 }
 
-/// Assert that the pointer is valid for access according to [crate::mem] conditions 1, 2 and 3.
+/// Check if the pointer is valid for unaligned write access according to [crate::mem] conditions
+/// 1, 2 and 3.
 ///
 /// Note this function succeeds for unaligned pointers. See [self::can_write] if you also
 /// want to check pointer alignment.
 ///
-/// This function will either panic or return `true`. This is to make it easier to use it in
+/// This function will panic today if the pointer is not null, and it points to an unallocated or
+/// deallocated memory location. This is an existing Kani limitation.
+/// See <https://github.com/model-checking/kani/issues/2690> for more details.
 #[crate::unstable(
     feature = "mem-predicates",
     issue = 2690,
@@ -96,7 +103,9 @@ where
 /// TODO: Kani should automatically add those checks when a de-reference happens.
 /// <https://github.com/model-checking/kani/issues/2975>
 ///
-/// Invoking this with an invalid pointer will panic due to a memory violation error.
+/// This function will panic today if the pointer is not null, and it points to an unallocated or
+/// deallocated memory location. This is an existing Kani limitation.
+/// See <https://github.com/model-checking/kani/issues/2690> for more details.
 #[crate::unstable(
     feature = "mem-predicates",
     issue = 2690,
@@ -114,6 +123,33 @@ where
         && unsafe { has_valid_value(ptr) }
 }
 
+/// Checks that pointer `ptr` point to a valid value of type `T`.
+///
+/// For that, the pointer has to be a valid pointer according to [crate::mem] conditions 1, 2
+/// and 3,
+/// and the value stored must respect the validity invariants for type `T`.
+///
+/// Note this function succeeds for unaligned pointers. See [self::can_dereference] if you also
+/// want to check pointer alignment.
+///
+/// This function will panic today if the pointer is not null, and it points to an unallocated or
+/// deallocated memory location. This is an existing Kani limitation.
+/// See <https://github.com/model-checking/kani/issues/2690> for more details.
+#[crate::unstable(
+    feature = "mem-predicates",
+    issue = 2690,
+    reason = "experimental memory predicate API"
+)]
+#[allow(clippy::not_unsafe_ptr_arg_deref)]
+pub fn can_read_unaligned<T>(ptr: *const T) -> bool
+where
+    T: ?Sized,
+    <T as Pointee>::Metadata: PtrProperties<T>,
+{
+    let (thin_ptr, metadata) = ptr.to_raw_parts();
+    is_inbounds(&metadata, thin_ptr) && unsafe { has_valid_value(ptr) }
+}
+
 /// 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`
@@ -244,6 +280,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 +292,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 +346,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/expected/function-contract/valid_ptr.expected

@@ -1,11 +1,11 @@
 Checking harness pre_condition::harness_invalid_ptr...
-Failed Checks: Expected valid pointer, but found dangling pointer
+Failed Checks: Kani does not support reasoning about pointer to unallocated memory
+VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
 
 Checking harness pre_condition::harness_stack_ptr...
 VERIFICATION:- SUCCESSFUL
 
 Checking harness pre_condition::harness_head_ptr...
 VERIFICATION:- SUCCESSFUL
 
-Verification failed for - pre_condition::harness_invalid_ptr
-Complete - 2 successfully verified harnesses, 1 failures, 3 total
+Complete - 3 successfully verified harnesses, 0 failures, 3 total

tests/expected/function-contract/valid_ptr.rs

@@ -2,14 +2,13 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 // kani-flags: -Zfunction-contracts -Zmem-predicates
 
-//! Test that it is sound to use `assert_valid_ptr` inside a contract pre-condition.
+//! Test that it is sound to use memory predicates inside a contract pre-condition.
 //! We cannot validate post-condition yet. This can be done once we fix:
 //! <https://github.com/model-checking/kani/issues/2997>
-#![feature(pointer_is_aligned)]
 
 mod pre_condition {
     /// This contract should succeed only if the input is a valid pointer.
-    #[kani::requires(kani::mem::assert_valid_ptr(ptr) && ptr.is_aligned())]
+    #[kani::requires(kani::mem::can_dereference(ptr))]
     unsafe fn read_ptr(ptr: *const i32) -> i32 {
         *ptr
     }
@@ -29,6 +28,7 @@ mod pre_condition {
     }
 
     #[kani::proof_for_contract(read_ptr)]
+    #[kani::should_panic]
     fn harness_invalid_ptr() {
         let ptr = std::ptr::NonNull::<i32>::dangling().as_ptr();
         assert_eq!(unsafe { read_ptr(ptr) }, -20);
@@ -40,7 +40,7 @@ mod pre_condition {
 mod post_condition {
 
     /// This contract should fail since we are creating a dangling pointer.
-    #[kani::ensures(kani::mem::assert_valid_ptr(result.0))]
+    #[kani::ensures(kani::mem::can_dereference(result.0))]
     unsafe fn new_invalid_ptr() -> PtrWrapper<char> {
         let var = 'c';
         PtrWrapper(&var as *const _)

tests/kani/MemPredicates/fat_ptr_validity.rs

@@ -5,35 +5,33 @@
 
 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');
     }
 
     #[kani::proof]
     pub fn check_valid_zst() {
         let slice_ptr = Vec::<char>::new().as_slice() as *const [char];
-        assert_valid_ptr(slice_ptr);
+        assert!(can_dereference(slice_ptr));
 
         let str_ptr = String::new().as_str() as *const str;
-        assert_valid_ptr(str_ptr);
+        assert!(can_dereference(str_ptr));
     }
 }
 
@@ -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 {