Add experimental API to generate arbitrary pointers (#3538)

This change adds a pointer generator that can non-deterministically
generate a pointer with different properties.

This generator allows users to build pointers with different allocation
status, initialization and alignment.
It contains an internal buffer that it uses to generate `InBounds` and
`OutOfBounds` pointers.
In those cases, the pointers will have the same provenance as the
generator, and the same lifetime.

This approach is different than generating a pointer from an arbitrary
`usize`. Kani uses demonic non-determinism to track
allocation lifetimes, which makes hard to reason about during
verification. I.e., one cannot assume a pointer is valid, and
initialized, and this can only be accomplished by manually tracking the
pointer status.

I added the new API under `-Z mem-predicates` since it allows reasoning
about memory, and I was hoping this wouldn't need another unstable flag.
:smile:

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>

library/kani_core/src/arbitrary.rs

@@ -7,11 +7,16 @@
 //! by an unconstrained symbolic value of their size (e.g., `u8`, `u16`, `u32`, etc.).
 //!
 //! TODO: Use this inside kani library so that we dont have to maintain two copies of the same proc macro for arbitrary.
+
+mod pointer;
+
 #[macro_export]
 #[allow(clippy::crate_in_macro_def)]
 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 +162,15 @@ macro_rules! generate_arbitrary {
             }
         }
 
+        impl<T> Arbitrary for MaybeUninit<T>
+        where
+            T: Arbitrary,
+        {
+            fn any() -> Self {
+                if crate::kani::any() { MaybeUninit::new(T::any()) } else { MaybeUninit::uninit() }
+            }
+        }
+
         arbitrary_tuple!(A);
         arbitrary_tuple!(A, B);
         arbitrary_tuple!(A, B, C);
@@ -169,6 +183,11 @@ 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);
+
+        pub use self::arbitrary_ptr::*;
+        mod arbitrary_ptr {
+            kani_core::ptr_generator!();
+        }
     };
 }
 

library/kani_macros/src/derive.rs

@@ -18,10 +18,37 @@ use syn::{
     parse_quote,
 };
 
+#[cfg(feature = "no_core")]
+macro_rules! kani_path {
+    ($span:expr) => {
+        quote_spanned! { $span => core::kani }
+    };
+    () => {
+        quote! { core::kani }
+    };
+}
+
+#[cfg(not(feature = "no_core"))]
+macro_rules! kani_path {
+    ($span:expr) => {
+        quote_spanned! { $span => kani }
+    };
+    () => {
+        quote! { kani }
+    };
+}
+
+/// Generate the Arbitrary implementation for the given type.
+///
+/// Note that we cannot use `proc_macro_crate::crate_name()` to discover the name for `kani` crate
+/// since we define it as an extern crate via `rustc` command line.
+///
+/// In order to support core, we check the `no_core` feature.
 pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::TokenStream {
     let trait_name = "Arbitrary";
     let derive_item = parse_macro_input!(item as DeriveInput);
     let item_name = &derive_item.ident;
+    let kani_path = kani_path!();
 
     let body = fn_any_body(&item_name, &derive_item.data);
     // Get the safety constraints (if any) to produce type-safe values
@@ -36,19 +63,19 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok
         let field_refs = field_refs(&item_name, &derive_item.data);
         quote! {
             // The generated implementation.
-            impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
+            impl #impl_generics #kani_path::Arbitrary for #item_name #ty_generics #where_clause {
                 fn any() -> Self {
                     let obj = #body;
                     #field_refs
-                    kani::assume(#safety_conds);
+                    #kani_path::assume(#safety_conds);
                     obj
                 }
             }
         }
     } else {
         quote! {
             // The generated implementation.
-            impl #impl_generics kani::Arbitrary for #item_name #ty_generics #where_clause {
+            impl #impl_generics #kani_path::Arbitrary for #item_name #ty_generics #where_clause {
                 fn any() -> Self {
                     #body
                 }
@@ -60,9 +87,10 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok
 
 /// Add a bound `T: Arbitrary` to every type parameter T.
 fn add_trait_bound_arbitrary(mut generics: Generics) -> Generics {
+    let kani_path = kani_path!();
     generics.params.iter_mut().for_each(|param| {
         if let GenericParam::Type(type_param) = param {
-            type_param.bounds.push(parse_quote!(kani::Arbitrary));
+            type_param.bounds.push(parse_quote!(#kani_path::Arbitrary));
         }
     });
     generics
@@ -222,8 +250,10 @@ fn init_symbolic_item(ident: &Ident, fields: &Fields) -> TokenStream {
             // Expands to an expression like
             // Self(kani::any(), kani::any(), ..., kani::any());
             let init = fields.unnamed.iter().map(|field| {
-                quote_spanned! {field.span()=>
-                    kani::any()
+                let span = field.span();
+                let kani_path = kani_path!(span);
+                quote_spanned! {span=>
+                    #kani_path::any()
                 }
             });
             quote! {
@@ -349,8 +379,9 @@ fn fn_any_enum(ident: &Ident, data: &DataEnum) -> TokenStream {
             }
         });
 
+        let kani_path = kani_path!();
         quote! {
-            match kani::any() {
+            match #kani_path::any() {
                 #(#arms)*
             }
         }
@@ -376,6 +407,7 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok
     let trait_name = "Invariant";
     let derive_item = parse_macro_input!(item as DeriveInput);
     let item_name = &derive_item.ident;
+    let kani_path = kani_path!();
 
     let safe_body = safe_body_with_calls(&item_name, &derive_item, trait_name);
     let field_refs = field_refs(&item_name, &derive_item.data);
@@ -387,7 +419,7 @@ pub fn expand_derive_invariant(item: proc_macro::TokenStream) -> proc_macro::Tok
 
     let expanded = quote! {
         // The generated implementation.
-        impl #impl_generics kani::Invariant for #item_name #ty_generics #where_clause {
+        impl #impl_generics #kani_path::Invariant for #item_name #ty_generics #where_clause {
             fn is_safe(&self) -> bool {
                 let obj = self;
                 #field_refs
@@ -463,9 +495,10 @@ fn has_field_safety_constraints_inner(_ident: &Ident, fields: &Fields) -> bool {
 
 /// Add a bound `T: Invariant` to every type parameter T.
 pub fn add_trait_bound_invariant(mut generics: Generics) -> Generics {
+    let kani_path = kani_path!();
     generics.params.iter_mut().for_each(|param| {
         if let GenericParam::Type(type_param) = param {
-            type_param.bounds.push(parse_quote!(kani::Invariant));
+            type_param.bounds.push(parse_quote!(#kani_path::Invariant));
         }
     });
     generics

tests/expected/arbitrary/ptrs/pointer_generator.expected

@@ -0,0 +1,21 @@
+Checking harness check_arbitrary_ptr...
+
+Status: SUCCESS\
+Description: ""OutOfBounds""
+
+Status: SUCCESS\
+Description: ""InBounds""
+
+Status: SUCCESS\
+Description: ""NullPtr""
+
+Status: FAILURE\
+Description: ""DeadObject""
+
+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::{AllocationStatus, PointerGenerator, cover};
+
+/// Harness that checks that all cases are covered and the code behaves as expected.
+///
+/// Note that for `DeadObject`, `Dangling`, and `OutOfBounds` the predicate will fail due to demonic non-determinism.
+#[kani::proof]
+fn check_arbitrary_ptr() {
+    let mut generator = PointerGenerator::<10>::new();
+    let arbitrary = generator.any_alloc_status::<char>();
+    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::DeadObject => {
+            // Due to demonic non-determinism, the API will trigger an error.
+            assert!(!kani::mem::can_write_unaligned(ptr), "DeadObject");
+        }
+        AllocationStatus::OutOfBounds => {
+            assert!(!kani::mem::can_write_unaligned(ptr), "OutOfBounds");
+        }
+        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,9 @@
+error[E0080]: evaluation of `kani::PointerGenerator::<0>::VALID` failed\
+
+the evaluated program panicked at 'PointerGenerator requires at least one byte.'
+
+note: the above error was encountered while instantiating `fn kani::PointerGenerator::<0>::new`\
+pointer_generator_error.rs\
+|\
+|     let _generator = PointerGenerator::<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::<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: SUCCESS\
+Description: ""Aligned""
+
+Status: SUCCESS\
+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,56 @@
+// 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 (`-Z uninit-checks`) once we add support to unions.
+//! The current instrumentation does not work in the presence of MaybeUninit which we use
+//! to implement PointerGenerator.
+//! Kani will detect the usage of MaybeUninit and fail the verification.
+extern crate kani;
+
+use kani::PointerGenerator;
+
+#[kani::proof]
+fn check_inbounds() {
+    let mut generator = kani::pointer_generator::<char, 3>();
+    let ptr = generator.any_in_bounds::<char>().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 = kani::pointer_generator::<char, 3>();
+    let arbitrary = generator.any_in_bounds::<char>();
+    kani::assume(arbitrary.is_initialized);
+    assert!(kani::mem::can_read_unaligned(arbitrary.ptr), "ValidRead");
+}
+
+#[kani::proof]
+fn check_alignment() {
+    let mut generator = kani::pointer_generator::<char, 2>();
+    let ptr: *mut char = generator.any_in_bounds().ptr;
+    if ptr.is_aligned() {
+        assert!(kani::mem::can_write(ptr), "Aligned");
+    } else {
+        assert!(!kani::mem::can_write(ptr), "Not aligned");
+        assert!(kani::mem::can_write_unaligned(ptr), "Unaligned");
+    }
+}
+
+#[kani::proof]
+fn check_overlap() {
+    let mut generator = kani::pointer_generator::<u16, 5>();
+    let ptr_1 = generator.any_in_bounds::<u16>().ptr;
+    let ptr_2 = generator.any_in_bounds::<u16>().ptr;
+    kani::cover!(ptr_1 == ptr_2, "Same");
+    kani::cover!(ptr_1 == unsafe { ptr_2.byte_add(1) }, "Overlap");
+
+    let distance = unsafe { ptr_1.offset_from(ptr_2) };
+    kani::cover!(distance > 0, "Greater");
+    kani::cover!(distance < 0, "Smaller");
+
+    assert!(distance >= -4 && distance <= 4, "Expected a maximum distance of 4 elements");
+}

tests/script-based-pre/verify_std_cmd/verify_core.rs

@@ -76,4 +76,15 @@ pub mod verify {
     unsafe fn add_one(inout: *mut [u32]) {
         inout.as_mut_unchecked().iter_mut().for_each(|e| *e += 1)
     }
+
+    /// Test that arbitrary pointer works as expected.
+    /// Disable it for uninit checks, since these checks do not support `MaybeUninit` which is used
+    /// by the pointer generator.
+    #[kani::proof]
+    #[cfg(not(uninit_checks))]
+    fn check_any_ptr() {
+        let mut generator = kani::PointerGenerator::<8>::new();
+        let ptr = generator.any_in_bounds::<i32>().ptr;
+        assert!(kani::mem::can_write_unaligned(ptr));
+    }
 }

tests/script-based-pre/verify_std_cmd/verify_std.expected

@@ -15,10 +15,13 @@ VERIFICATION:- SUCCESSFUL
 Checking harness verify::check_swap_tuple...
 VERIFICATION:- SUCCESSFUL
 
+Checking harness verify::check_any_ptr...
+VERIFICATION:- SUCCESSFUL
+
 Checking harness num::verify::check_non_zero...
 VERIFICATION:- SUCCESSFUL
 
-Complete - 6 successfully verified harnesses, 0 failures, 6 total.
+Complete - 7 successfully verified harnesses, 0 failures, 7 total.
 
 [TEST] Run kani verify-std -Z uninit-checks