Add experimental API to generate arbitrary pointers

library/kani_core/src/arbitrary.rs

@@ -12,6 +12,8 @@
 macro_rules! generate_arbitrary {
     ($core:path) => {
         use core_path::marker::{PhantomData, PhantomPinned};
+        use core_path::mem::MaybeUninit;
+        use core_path::ptr::{self, addr_of_mut};
         use $core as core_path;
 
         pub trait Arbitrary
@@ -157,6 +159,15 @@ macro_rules! generate_arbitrary {
             }
         }
 
+        impl<T> Arbitrary for MaybeUninit<T>
+        where
+            T: Arbitrary,
+        {
+            fn any() -> Self {
+                if kani::any() { MaybeUninit::new(T::any()) } else { MaybeUninit::uninit() }
+            }
+        }
+
         arbitrary_tuple!(A);
         arbitrary_tuple!(A, B);
         arbitrary_tuple!(A, B, C);
@@ -169,6 +180,171 @@ macro_rules! generate_arbitrary {
         arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J);
         arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K);
         arbitrary_tuple!(A, B, C, D, E, F, G, H, I, J, K, L);
+
+        /// Enumeration with the cases currently covered by the pointer generator.
+        #[derive(Copy, Clone, Debug, PartialEq, Eq, kani::Arbitrary)]
+        pub enum AllocationStatus {
+            /// Dangling pointers
+            Dangling,
+            /// Pointer to dead object
+            DeadObj,
+            /// Null pointers
+            Null,
+            /// In bounds pointer (it may be unaligned)
+            InBounds,
+            /// Out of bounds
+            OutBounds,
+        }
+
+        /// Pointer generator that can be used to generate an arbitrary pointer.
+        ///
+        /// This generator allows users to build pointers with different safety properties.
+        /// It contains an internal buffer that it uses to generate `InBounds` and `OutBounds` pointers.
+        /// In those cases, the pointers will have the same provenance as the generator, and the same lifetime.
+        ///
+        /// For example:
+        /// ```ignore
+        ///     let generator = PointerGenerator<char, 5>::new();
+        ///     let arbitrary = generator.generate_ptr();
+        ///     kani::assume(arbitrary.status == AllocationStatus::InBounds);
+        ///     // Pointer may be unaligned but it should be in-bounds.
+        ///     unsafe { arbitrary.ptr.write_unaligned(kani::any() }
+        /// ```
+        ///
+        /// Use the same generator if you want to handle cases where 2 or more pointers may overlap. E.g.:
+        /// ```ignore
+        ///     let generator = PointerGenerator<char, 5>::new();
+        ///     let arbitrary = generator.generate_ptr();
+        ///     kani::assume(arbitrary.status == AllocationStatus::InBounds);
+        ///     let ptr = arbitrary.ptr;
+        ///     kani::cover!(arbitrary.ptr == generator.generate_ptr());
+        ///     kani::cover!(arbitrary.ptr != generator.generate_ptr());
+        /// ```
+        ///
+        /// Note: This code is different than generating a pointer with any address. I.e.:
+        /// ```ignore
+        ///     // This pointer represents any address.
+        ///     let ptr = kani::any::<usize>() as *const u8;
+        ///     // Which is different from:
+        ///     let generator = PointerGenerator<u8, 5>::new();
+        ///     let ptr = generator.generate_ptr().ptr;
+        /// ```
+        ///
+        /// Kani cannot reason about a pointer allocation status (except for asserting its validity).
+        /// Thus, this interface allow users to write harnesses that impose constraints to the arbitrary pointer.
+        #[derive(Debug)]
+        pub struct PointerGenerator<T, const BUF_LEN: usize> {
+            // Internal allocation that may be used to generate valid pointers.
+            buf: MaybeUninit<[T; BUF_LEN]>,
+        }
+
+        /// Holds information about a pointer that is generated non-deterministically.
+        #[derive(Debug)]
+        pub struct ArbitraryPointer<'a, T> {
+            /// The pointer that was generated.
+            pub ptr: *mut T,
+            /// The expected allocation status.
+            pub status: AllocationStatus,
+            /// Whether the pointer was generated with an initialized value or not.
+            pub is_initialized: bool,
+            /// Lifetime for this object.
+            phantom: PhantomData<&'a T>,
+        }
+
+        impl<T: kani::Arbitrary, const BUF_LEN: usize> PointerGenerator<T, BUF_LEN> {
+            const _VALID: () = assert!(BUF_LEN > 0, "PointerGenerator requires non-zero length.");
+
+            /// Create a new PointerGenerator.
+            #[crate::kani::unstable_feature(
+                feature = "mem-predicates",
+                issue = 2690,
+                reason = "experimental memory predicates and manipulation feature"
+            )]
+            pub fn new() -> Self {
+                // Use constant to trigger static length validation.
+                let _ = Self::_VALID;
+                PointerGenerator { buf: MaybeUninit::uninit() }
+            }
+
+            /// Creates a raw pointer with non-deterministic properties.
+            ///
+            /// The pointer returned is either dangling or has the same provenance of the generator.
+            #[crate::kani::unstable_feature(
+                feature = "mem-predicates",
+                issue = 2690,
+                reason = "experimental memory predicates and manipulation feature"
+            )]
+            pub fn any_alloc_status<'a>(&'a mut self) -> ArbitraryPointer<'a, T> {
+                // Create an arbitrary pointer, but leave `ptr` as unset for now.
+                let mut arbitrary = ArbitraryPointer {
+                    ptr: ptr::null_mut::<T>(),
+                    is_initialized: false,
+                    status: kani::any(),
+                    phantom: PhantomData,
+                };
+
+                let buf_ptr = addr_of_mut!(self.buf) as *mut T;
+
+                // Offset is used to potentially generate unaligned pointer.
+                let offset = kani::any_where(|b: &usize| *b < size_of::<T>());
+                arbitrary.ptr = match arbitrary.status {
+                    AllocationStatus::Dangling => {
+                        crate::ptr::NonNull::<T>::dangling().as_ptr().wrapping_add(offset)
+                    }
+                    AllocationStatus::DeadObj => {
+                        let mut obj: T = kani::any();
+                        &mut obj as *mut _
+                    }
+                    AllocationStatus::Null => crate::ptr::null_mut::<T>(),
+                    AllocationStatus::InBounds => {
+                        // Note that compilation fails if BUF_LEN is 0.
+                        let pos = kani::any_where(|i: &usize| *i < (BUF_LEN - 1));
+                        let ptr: *mut T = buf_ptr.wrapping_add(pos).wrapping_byte_add(offset);
+                        if kani::any() {
+                            arbitrary.is_initialized = true;
+                            // This should be in bounds of arbitrary.alloc.
+                            unsafe { ptr.write_unaligned(kani::any()) };
+                        }
+                        ptr
+                    }
+                    AllocationStatus::OutBounds => {
+                        if kani::any() {
+                            buf_ptr.wrapping_add(BUF_LEN).wrapping_byte_sub(offset)
+                        } else {
+                            buf_ptr.wrapping_add(BUF_LEN).wrapping_byte_add(offset)
+                        }
+                    }
+                };
+
+                arbitrary
+            }
+
+            /// Creates a in-bounds raw pointer with non-deterministic properties.
+            ///
+            /// The pointer points to an allocated location with the same provenance of the generator.
+            /// The pointer may be unaligned, and the pointee may be uninitialized.
+            #[crate::kani::unstable_feature(
+                feature = "mem-predicates",
+                issue = 2690,
+                reason = "experimental memory predicates and manipulation feature"
+            )]
+            pub fn any_in_bounds<'a>(&'a mut self) -> ArbitraryPointer<'a, T> {
+                let buf_ptr = addr_of_mut!(self.buf) as *mut T;
+                let pos = kani::any_where(|i: &usize| *i < (BUF_LEN - 1));
+                let offset = kani::any_where(|b: &usize| *b < size_of::<T>());
+                let ptr: *mut T = buf_ptr.wrapping_add(pos).wrapping_byte_add(offset);
+                let is_initialized = kani::any();
+                if is_initialized {
+                    unsafe { ptr.write_unaligned(kani::any()) };
+                }
+                ArbitraryPointer {
+                    ptr,
+                    is_initialized,
+                    status: AllocationStatus::InBounds,
+                    phantom: PhantomData,
+                }
+            }
+        }
     };
 }
 

tests/expected/arbitrary/ptrs/pointer_generator.expected

@@ -0,0 +1,21 @@
+Checking harness check_arbitrary_ptr...
+
+Status: SUCCESS\
+Description: ""OutBounds""
+
+Status: SUCCESS\
+Description: ""InBounds""
+
+Status: SUCCESS\
+Description: ""NullPtr""
+
+Status: FAILURE\
+Description: ""DeadObj""
+
+Status: SATISFIED\
+Description: "Dangling"
+
+Status: UNREACHABLE\
+Description: ""Dangling write""
+
+Verification failed for - check_arbitrary_ptr

tests/expected/arbitrary/ptrs/pointer_generator.rs

@@ -0,0 +1,38 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z mem-predicates
+//! Check the behavior of the new `PointerGenerator`.
+extern crate kani;
+
+use kani::{cover, AllocationStatus, PointerGenerator};
+
+/// Harness that checks that all cases are covered and the code behaves as expected.
+///
+/// Note that for `DeadObj`, `Dangling`, and `OutBounds` the predicate will fail due to demonic non-determinism.
+#[kani::proof]
+fn check_arbitrary_ptr() {
+    let mut generator = PointerGenerator::<char, 3>::new();
+    let arbitrary = generator.any_alloc_status();
+    let ptr = arbitrary.ptr;
+    match arbitrary.status {
+        AllocationStatus::Dangling => {
+            cover!(true, "Dangling");
+            assert!(!kani::mem::can_write_unaligned(ptr), "Dangling write");
+        }
+        AllocationStatus::Null => {
+            assert!(!kani::mem::can_write_unaligned(ptr), "NullPtr");
+        }
+        AllocationStatus::DeadObj => {
+            // Due to demonic non-determinism, the API will trigger an error.
+            assert!(!kani::mem::can_write_unaligned(ptr), "DeadObj");
+        }
+        AllocationStatus::OutBounds => {
+            assert!(!kani::mem::can_write_unaligned(ptr), "OutBounds");
+        }
+        AllocationStatus::InBounds => {
+            // This should always succeed
+            assert!(kani::mem::can_write_unaligned(ptr), "InBounds");
+        }
+    };
+}

tests/expected/arbitrary/ptrs/pointer_generator_error.expected

@@ -0,0 +1,10 @@
+error[E0080]: evaluation of `kani::PointerGenerator::<char, 0>::_VALID` failed
+
+the evaluated program panicked at 'PointerGenerator requires non-zero length.'
+
+note: the above error was encountered while instantiating `fn kani::PointerGenerator::<char, 0>::new`\
+pointer_generator_error.rs\
+|\
+|     let _generator = PointerGenerator::<char, 0>::new();\
+|                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+

tests/expected/arbitrary/ptrs/pointer_generator_error.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z mem-predicates
+//! Check misusage of pointer generator fails compilation.
+extern crate kani;
+
+use kani::PointerGenerator;
+
+pub fn check_invalid_generator() {
+    let _generator = PointerGenerator::<char, 0>::new();
+}

tests/expected/arbitrary/ptrs/pointer_inbounds.expected

@@ -0,0 +1,39 @@
+Checking harness check_overlap...
+
+Status: SATISFIED\
+Description: "Same"
+
+Status: SATISFIED\
+Description: "Overlap"
+
+Status: SATISFIED\
+Description: "Greater"
+
+Status: SATISFIED\
+Description: "Smaller"
+
+Checking harness check_alignment...
+
+Status: SATISFIED\
+Description: "Aligned"
+
+Status: SATISFIED\
+Description: "Unaligned"
+
+Checking harness check_inbounds_initialized...
+
+Status: SUCCESS\
+Description: ""ValidRead""
+
+Checking harness check_inbounds...
+
+Status: SATISFIED\
+Description: "Uninitialized"
+
+Status: SATISFIED\
+Description: "Initialized"
+
+Status: SUCCESS\
+Description: ""ValidWrite""
+
+Complete - 4 successfully verified harnesses, 0 failures, 4 total.

tests/expected/arbitrary/ptrs/pointer_inbounds.rs

@@ -0,0 +1,45 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: -Z mem-predicates
+//! Check different cases for `PointerGenerator` for in-bounds pointers.
+//! TODO: Enable initialization checks once we enable reasoning about unions.
+extern crate kani;
+
+use kani::PointerGenerator;
+
+#[kani::proof]
+fn check_inbounds() {
+    let mut generator = PointerGenerator::<char, 3>::new();
+    let ptr = generator.any_in_bounds().ptr;
+    kani::cover!(!kani::mem::can_read_unaligned(ptr), "Uninitialized");
+    kani::cover!(kani::mem::can_read_unaligned(ptr), "Initialized");
+    assert!(kani::mem::can_write_unaligned(ptr), "ValidWrite");
+}
+
+#[kani::proof]
+fn check_inbounds_initialized() {
+    let mut generator = PointerGenerator::<char, 3>::new();
+    let arbitrary = generator.any_in_bounds();
+    kani::assume(arbitrary.is_initialized);
+    assert!(kani::mem::can_read_unaligned(arbitrary.ptr), "ValidRead");
+}
+
+#[kani::proof]
+fn check_alignment() {
+    let mut generator = PointerGenerator::<char, 3>::new();
+    let ptr = generator.any_in_bounds().ptr;
+    kani::cover!(kani::mem::can_write(ptr), "Aligned");
+    kani::cover!(!kani::mem::can_write(ptr), "Unaligned");
+}
+
+#[kani::proof]
+fn check_overlap() {
+    let mut generator = PointerGenerator::<(u8, u32), 3>::new();
+    let ptr_1 = generator.any_in_bounds().ptr as usize;
+    let ptr_2 = generator.any_in_bounds().ptr as usize;
+    kani::cover!(ptr_1 == ptr_2, "Same");
+    kani::cover!(ptr_1 > ptr_2 && ptr_1 < ptr_2 + 8, "Overlap");
+    kani::cover!(ptr_1 > ptr_2 + 8, "Greater");
+    kani::cover!(ptr_2 > ptr_1 + 8, "Smaller");
+}