Add more tests and adjust a few issues with ZST

library/kani/src/lib.rs

@@ -216,13 +216,7 @@ pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
 #[inline(never)]
 #[allow(dead_code)]
 fn any_raw_inner<T>() -> T {
-    // while we could use `unreachable!()` or `panic!()` as the body of this
-    // function, both cause Kani to produce a warning on any program that uses
-    // kani::any() (see https://github.com/model-checking/kani/issues/2010).
-    // This function is handled via a hook anyway, so we just need to put a body
-    // that rustc does not complain about. An infinite loop works out nicely.
-    #[allow(clippy::empty_loop)]
-    loop {}
+    kani_intrinsic()
 }
 
 /// Function used to generate panic with a static message as this is the only one currently
@@ -238,6 +232,20 @@ pub const fn panic(message: &'static str) -> ! {
     panic!("{}", message)
 }
 
+/// An empty body that can be used to define Kani intrinsic functions.
+///
+/// A Kani intrinsic is a function that is interpreted by Kani compiler.
+/// While we could use `unreachable!()` or `panic!()` as the body of a kani intrinsic
+/// function, both cause Kani to produce a warning since we don't support caller location.
+/// (see https://github.com/model-checking/kani/issues/2010).
+///
+/// This function is dead, since its caller is always  handled via a hook anyway,
+/// so we just need to put a body that rustc does not complain about.
+/// An infinite loop works out nicely.
+fn kani_intrinsic<T>() -> T {
+    #[allow(clippy::empty_loop)]
+    loop {}
+}
 /// A macro to check if a condition is satisfiable at a specific location in the
 /// code.
 ///

library/kani/src/mem.rs

@@ -34,12 +34,15 @@
 //! 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.
 
+use crate::kani_intrinsic;
 use crate::mem::private::Internal;
 use std::mem::{align_of, size_of};
 use std::ptr::{DynMetadata, NonNull, Pointee};
 
 /// Assert that the pointer is valid for access according to [crate::mem] conditions 1, 2 and 3.
 ///
+/// Note that a unaligned pointer is still considered valid.
+///
 /// TODO: Kani will automatically add those checks when a de-reference happens.
 /// https://github.com/model-checking/kani/issues/2975
 ///
@@ -60,25 +63,30 @@ where
     crate::assert(!ptr.is_null(), "Expected valid pointer, but found `null`");
 
     let (thin_ptr, metadata) = ptr.to_raw_parts();
-    metadata.can_read(thin_ptr, Internal)
+    can_read(&metadata, thin_ptr)
 }
 
-#[crate::unstable(
-    feature = "mem-predicates",
-    issue = 2690,
-    reason = "experimental memory predicate API"
-)]
-pub fn is_ptr_aligned<T>(ptr: *const T) -> bool
+fn can_read<M, T>(metadata: &M, data_ptr: *const ()) -> bool
 where
+    M: PtrProperties<T>,
     T: ?Sized,
-    <T as Pointee>::Metadata: PtrProperties<T>,
 {
-    let (thin_ptr, metadata) = ptr.to_raw_parts();
-    thin_ptr as usize % metadata.min_alignment(Internal) == 0
+    let marker = Internal;
+    let sz = metadata.pointee_size(marker);
+    if metadata.dangling(marker) as *const _ == data_ptr {
+        crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access")
+    } else {
+        crate::assert(
+            is_read_ok(data_ptr, sz),
+            "Expected valid pointer, but found dangling pointer",
+        );
+    }
+    true
 }
 
 mod private {
     /// Define like this to restrict usage of PtrProperties functions outside Kani.
+    #[derive(Copy, Clone)]
     pub struct Internal;
 }
 
@@ -89,15 +97,10 @@ pub trait PtrProperties<T: ?Sized> {
 
     fn min_alignment(&self, _: Internal) -> usize;
 
-    fn can_read(&self, thin_ptr: *const (), _: Internal) -> bool {
-        crate::assert(
-            is_read_ok(thin_ptr, self.pointee_size(Internal)),
-            "Expected valid pointer, but found dangling pointer",
-        );
-        true
-    }
+    fn dangling(&self, _: Internal) -> *const ();
 }
 
+/// Get the information for sized types (they don't have metadata).
 impl<T> PtrProperties<T> for () {
     fn pointee_size(&self, _: Internal) -> usize {
         size_of::<T>()
@@ -107,21 +110,14 @@ impl<T> PtrProperties<T> for () {
         align_of::<T>()
     }
 
-    fn can_read(&self, thin_ptr: *const (), _: Internal) -> bool {
-        let sz = size_of::<T>();
-        if NonNull::<T>::dangling().as_ptr() as *const _ as *const () == thin_ptr {
-            crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access")
-        } else {
-            crate::assert(
-                is_read_ok(thin_ptr, sz),
-                "Expected valid pointer, but found dangling pointer",
-            );
-        }
-        true
+    fn dangling(&self, _: Internal) -> *const () {
+        NonNull::<T>::dangling().as_ptr() as *const _
     }
 }
 
+/// Get the information from the str metadata.
 impl PtrProperties<str> for usize {
+    #[inline(always)]
     fn pointee_size(&self, _: Internal) -> usize {
         *self
     }
@@ -132,18 +128,28 @@ impl PtrProperties<str> for usize {
     fn min_alignment(&self, _: Internal) -> usize {
         align_of::<u8>()
     }
+
+    fn dangling(&self, _: Internal) -> *const () {
+        NonNull::<u8>::dangling().as_ptr() as _
+    }
 }
 
+/// Get the information from the slice metadata.
 impl<T> PtrProperties<[T]> for usize {
     fn pointee_size(&self, _: Internal) -> usize {
-        *self
+        *self * size_of::<T>()
     }
 
     fn min_alignment(&self, _: Internal) -> usize {
         align_of::<T>()
     }
+
+    fn dangling(&self, _: Internal) -> *const () {
+        NonNull::<T>::dangling().as_ptr() as _
+    }
 }
 
+/// Get the information from the vtable.
 impl<T> PtrProperties<T> for DynMetadata<T>
 where
     T: ?Sized,
@@ -155,6 +161,10 @@ where
     fn min_alignment(&self, _: Internal) -> usize {
         self.align_of()
     }
+
+    fn dangling(&self, _: Internal) -> *const () {
+        NonNull::<&T>::dangling().as_ptr() as _
+    }
 }
 
 /// Check if the pointer `_ptr` contains an allocated address of size equal or greater than `_size`.
@@ -165,14 +175,12 @@ where
 #[rustc_diagnostic_item = "KaniIsReadOk"]
 #[inline(never)]
 fn is_read_ok(_ptr: *const (), _size: usize) -> bool {
-    // This will be replaced by Kani codegen.
-    #[allow(clippy::empty_loop)]
-    loop {}
+    kani_intrinsic()
 }
 
 #[cfg(test)]
 mod tests {
-    use super::PtrProperties;
+    use super::{assert_valid_ptr, PtrProperties};
     use crate::mem::private::Internal;
     use std::intrinsics::size_of;
     use std::mem::{align_of, align_of_val, size_of_val};
@@ -213,12 +221,50 @@ mod tests {
     fn test_alignment() {
         assert_eq!(align_of_t("hi"), align_of_val("hi"));
         assert_eq!(align_of_t(&0u8), align_of_val(&0u8));
-        assert_eq!(align_of_t(&0u8 as *const dyn std::fmt::Display), align_of_val(&0u8));
-        assert_eq!(align_of_t(&[0u8, 1u8] as &[u8]), align_of_val(&[0u8, 1u8]));
+        assert_eq!(align_of_t(&0u32 as *const dyn std::fmt::Display), align_of_val(&0u32));
+        assert_eq!(align_of_t(&[0isize, 1isize] as &[isize]), align_of_val(&[0isize, 1isize]));
         assert_eq!(align_of_t(&[] as &[u8]), align_of_val::<[u8; 0]>(&[]));
         assert_eq!(
             align_of_t(NonNull::<u32>::dangling().as_ptr() as *const dyn std::fmt::Display),
             align_of::<u32>()
         );
     }
+
+    #[test]
+    pub fn test_empty_slice() {
+        let slice_ptr = Vec::<char>::new().as_slice() as *const [char];
+        assert_valid_ptr(slice_ptr);
+    }
+
+    #[test]
+    pub fn test_empty_str() {
+        let slice_ptr = String::new().as_str() as *const str;
+        assert_valid_ptr(slice_ptr);
+    }
+
+    #[test]
+    fn test_dangling_zst() {
+        test_dangling_of_t::<()>();
+        test_dangling_of_t::<[(); 10]>();
+    }
+
+    fn test_dangling_of_t<T>() {
+        let dangling: *const T = NonNull::<T>::dangling().as_ptr();
+        assert_valid_ptr(dangling);
+
+        let vec_ptr = Vec::<T>::new().as_ptr();
+        assert_valid_ptr(vec_ptr);
+    }
+
+    #[test]
+    #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")]
+    fn test_dangling_char() {
+        test_dangling_of_t::<char>();
+    }
+
+    #[test]
+    #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")]
+    fn test_dangling_slice() {
+        test_dangling_of_t::<&str>();
+    }
 }

scripts/kani-regression.sh

@@ -41,7 +41,8 @@ cargo test -p cprover_bindings
 cargo test -p kani-compiler
 cargo test -p kani-driver
 cargo test -p kani_metadata
-cargo test -p kani --lib # skip doc tests.
+# skip doc tests and enable assertions to fail
+cargo test -p kani --lib --features concrete_playback
 # Test the actual macros, skipping doc tests and enabling extra traits for "syn"
 # so we can debug print AST
 RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib

tests/kani/MemPredicates/fat_ptr_validity.rs

@@ -6,7 +6,6 @@
 extern crate kani;
 
 use kani::mem::assert_valid_ptr;
-use std::fmt::Debug;
 
 mod valid_access {
     use super::*;
@@ -27,20 +26,44 @@ mod valid_access {
         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);
+
+        let str_ptr = String::new().as_str() as *const str;
+        assert_valid_ptr(str_ptr);
+    }
 }
 
 mod invalid_access {
     use super::*;
     #[kani::proof]
     #[kani::should_panic]
     pub fn check_invalid_dyn_ptr() {
-        let raw_ptr: *const dyn PartialEq<u8> = unsafe { new_dead_ptr::<u8>() };
+        let raw_ptr: *const dyn PartialEq<u8> = unsafe { new_dead_ptr::<u8>(0) };
         assert_valid_ptr(raw_ptr);
-        assert_eq!(*unsafe { &*raw_ptr }, 0u8);
     }
 
-    unsafe fn new_dead_ptr<T: Default>() -> *const T {
-        let var = T::default();
-        &var as *const _
+    #[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);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn check_invalid_slice_len() {
+        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);
+    }
+
+    unsafe fn new_dead_ptr<T>(val: T) -> *const T {
+        let local = val;
+        &local as *const _
     }
 }

tests/kani/MemPredicates/thin_ptr_validity.rs

@@ -0,0 +1,60 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z mem-predicates
+//! Check that Kani's memory predicates work for thin pointers.
+
+extern crate kani;
+
+use kani::mem::assert_valid_ptr;
+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);
+
+        let vec_ptr = Vec::<()>::new().as_ptr();
+        assert_valid_ptr(vec_ptr);
+
+        let dangling = NonNull::<[char; 0]>::dangling().as_ptr();
+        assert_valid_ptr(dangling);
+    }
+
+    #[kani::proof]
+    pub fn check_valid_array() {
+        let array = ['a', 'b', 'c'];
+        assert_valid_ptr(&array);
+    }
+}
+
+mod invalid_access {
+    use super::*;
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn check_invalid_ptr() {
+        let raw_ptr = unsafe { new_dead_ptr::<u8>(0) };
+        assert_valid_ptr(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);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn check_invalid_zst() {
+        let raw_ptr: *const [char; 0] =
+            unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) } as *const _;
+        assert_valid_ptr(raw_ptr);
+    }
+
+    unsafe fn new_dead_ptr<T>(val: T) -> *const T {
+        let local = val;
+        &local as *const _
+    }
+}