From d2f5dbe04ade9bafd72d0dcf174e0d71e245f1ee Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 4 Oct 2024 20:04:11 -0400 Subject: [PATCH 1/3] 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 | 19 + library/kani_core/src/arbitrary/pointer.rs | 371 ++++++++++++++++++ library/kani_macros/src/derive.rs | 51 ++- .../arbitrary/ptrs/pointer_generator.expected | 21 + .../arbitrary/ptrs/pointer_generator.rs | 38 ++ .../ptrs/pointer_generator_error.expected | 9 + .../arbitrary/ptrs/pointer_generator_error.rs | 12 + .../arbitrary/ptrs/pointer_inbounds.expected | 39 ++ .../arbitrary/ptrs/pointer_inbounds.rs | 56 +++ .../verify_std_cmd/verify_core.rs | 11 + .../verify_std_cmd/verify_std.expected | 5 +- .../verify_std_cmd/verify_std.sh | 9 +- .../arbitrary-ptr-doc/doc_examples.expected | 24 ++ tests/ui/arbitrary-ptr-doc/doc_examples.rs | 90 +++++ 14 files changed, 743 insertions(+), 12 deletions(-) create mode 100644 library/kani_core/src/arbitrary/pointer.rs create mode 100644 tests/expected/arbitrary/ptrs/pointer_generator.expected create mode 100644 tests/expected/arbitrary/ptrs/pointer_generator.rs create mode 100644 tests/expected/arbitrary/ptrs/pointer_generator_error.expected create mode 100644 tests/expected/arbitrary/ptrs/pointer_generator_error.rs create mode 100644 tests/expected/arbitrary/ptrs/pointer_inbounds.expected create mode 100644 tests/expected/arbitrary/ptrs/pointer_inbounds.rs create mode 100644 tests/ui/arbitrary-ptr-doc/doc_examples.expected create mode 100644 tests/ui/arbitrary-ptr-doc/doc_examples.rs diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs index 8c6cfd335104..1dc30feca566 100644 --- a/library/kani_core/src/arbitrary.rs +++ b/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 Arbitrary for MaybeUninit + 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!(); + } }; } diff --git a/library/kani_core/src/arbitrary/pointer.rs b/library/kani_core/src/arbitrary/pointer.rs new file mode 100644 index 000000000000..0e987b1260c6 --- /dev/null +++ b/library/kani_core/src/arbitrary/pointer.rs @@ -0,0 +1,371 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This macro generates the logic required to generate pointers with arbitrary statuses. +#[allow(clippy::crate_in_macro_def)] +#[macro_export] +macro_rules! ptr_generator { + () => { + use core::marker::PhantomData; + use core::mem::MaybeUninit; + use core::ptr::{self, addr_of_mut}; + use crate::kani; + + /// Pointer generator that can be used to generate arbitrary pointers. + /// + /// This generator allows users to build pointers with different safety properties. + /// This is different than creating a pointer that can have any address, since it will never + /// point to a previously allocated object. + /// See [this section](crate::PointerGenerator#pointer-generator-vs-pointer-with-any-address) + /// for more details. + /// + /// The generator contains an internal buffer of a constant generic size, `BYTES`, that it + /// uses to generate `InBounds` and `OutOfBounds` pointers. + /// In those cases, the generated pointers will have the same provenance as the generator, + /// and the same lifetime. + /// The address of an `InBounds` pointer will represent all possible addresses in the range + /// of the generator's buffer address. + /// + /// For other allocation statuses, the generator will create a pointer that satisfies the + /// given condition. + /// The pointer address will **not** represent all possible addresses that satisfies the + /// given allocation status. + /// + /// For example: + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # fn harness() { + /// let mut generator = PointerGenerator::<10>::new(); + /// let arbitrary = generator.any_alloc_status::(); + /// kani::assume(arbitrary.status == AllocationStatus::InBounds); + /// // Pointer may be unaligned, but it should be in-bounds, so it is safe to write to + /// unsafe { arbitrary.ptr.write_unaligned(kani::any()) } + /// # } + /// ``` + /// + /// The generator is parameterized by the number of bytes of its internal buffer. + /// See [pointer_generator] function if you would like to create a generator that fits + /// a minimum number of objects of a given type. Example: + /// + /// ```no_run + /// # use kani::*; + /// # #[allow(unused)] + /// # #[kani::proof] + /// # fn harness() { + /// // These generators have the same capacity of 6 bytes. + /// let generator1 = PointerGenerator::<6>::new(); + /// let generator2 = pointer_generator::(); + /// # } + /// ``` + /// + /// ## Buffer size + /// + /// The internal buffer is used to generate pointers, and its size determines the maximum + /// number of pointers it can generate without overlapping. + /// Larger values will impact the maximum distance between generated pointers. + /// + /// We recommend that you pick a size that is at least big enough to + /// cover the cases where all pointers produced are non-overlapping. + /// The buffer size in bytes must be big enough to fit distinct objects for each call + /// of generate pointer. + /// For example, generating two `*mut u8` and one `*mut u32` requires a buffer + /// of at least 6 bytes. + /// + /// This guarantees that your harness covers cases where all generated pointers + /// point to allocated positions that do not overlap. For example: + /// + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # fn harness() { + /// let mut generator = PointerGenerator::<6>::new(); + /// let ptr1: *mut u8 = generator.any_in_bounds().ptr; + /// let ptr2: *mut u8 = generator.any_in_bounds().ptr; + /// let ptr3: *mut u32 = generator.any_in_bounds().ptr; + /// // This cover is satisfied. + /// cover!((ptr1 as usize) >= (ptr2 as usize) + size_of::() + /// && (ptr2 as usize) >= (ptr3 as usize) + size_of::()); + /// // As well as having overlapping pointers. + /// cover!((ptr1 as usize) == (ptr3 as usize)); + /// # } + /// ``` + /// + /// The first cover will be satisfied, since there exists at least one path where + /// the generator produces inbounds pointers that do not overlap. Such as this scenario: + /// + /// ```text + /// +--------+--------+--------+--------+--------+--------+ + /// | Byte 0 | Byte 1 | Byte 2 | Byte 3 | Byte 4 | Byte 5 | + /// +--------+--------+--------+--------+--------+--------+ + /// <--------------- ptr3 --------------><--ptr2-><--ptr1-> + /// ``` + /// + /// I.e., the generator buffer is large enough to fit all 3 objects without overlapping. + /// + /// In contrast, if we had used a size of 1 element, all calls to `any_in_bounds()` would + /// return elements that overlap, and the first cover would no longer be satisfied. + /// + /// Note that the generator requires a minimum number of 1 byte, otherwise the + /// `InBounds` case would never be covered. + /// Compilation will fail if you try to create a generator of size `0`. + /// + /// Additionally, the verification will fail if you try to generate a pointer for a type + /// with size greater than the buffer size. + /// + /// Use larger buffer size if you want to cover scenarios where the distance + /// between the generated pointers matters. + /// + /// The only caveats of using very large numbers are: + /// 1. The value cannot exceed the solver maximum object size (currently 2^48 by default), neither Rust's + /// maximum object size (`isize::MAX`). + /// 2. Larger sizes could impact performance as they can lead to an exponential increase in the number of possibilities of pointer placement within the buffer. + /// + /// # Pointer provenance + /// + /// The pointer returned in the `InBounds` and `OutOfBounds` case will have the same + /// provenance as the generator. + /// + /// Use the same generator if you want to handle cases where 2 or more pointers may overlap. E.g.: + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # fn harness() { + /// let mut generator = pointer_generator::(); + /// let ptr1 = generator.any_in_bounds::().ptr; + /// let ptr2 = generator.any_in_bounds::().ptr; + /// // This cover is satisfied. + /// cover!(ptr1 == ptr2) + /// # } + /// ``` + /// + /// If you want to cover cases where two or more pointers may not have the same + /// provenance, you will need to instantiate multiple generators. + /// You can also apply non-determinism to cover cases where the pointers may or may not + /// have the same provenance. E.g.: + /// + /// ```no_run + /// # use kani::*; + /// # unsafe fn my_target(_ptr1: *const T, _ptr2: *const T) {} + /// # #[kani::proof] + /// # fn harness() { + /// let mut generator1 = pointer_generator::(); + /// let mut generator2 = pointer_generator::(); + /// let ptr1: *const char = generator1.any_in_bounds().ptr; + /// let ptr2: *const char = if kani::any() { + /// // Pointers will have same provenance and may overlap. + /// generator1.any_in_bounds().ptr + /// } else { + /// // Pointers will have different provenance and will not overlap. + /// generator2.any_in_bounds().ptr + /// }; + /// // Invoke the function under verification + /// unsafe { my_target(ptr1, ptr2) }; + /// # } + /// ``` + /// + /// # Pointer Generator vs Pointer with any address + /// + /// Creating a pointer using the generator is different than generating a pointer + /// with any address. + /// + /// I.e.: + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # #[allow(unused)] + /// # fn harness() { + /// // This pointer represents any address, and it may point to anything in memory, + /// // allocated or not. + /// let ptr1 = kani::any::() as *const u8; + /// + /// // This pointer address will either point to unallocated memory, to a dead object + /// // or to allocated memory within the generator address space. + /// let mut generator = PointerGenerator::<5>::new(); + /// let ptr2: *const u8 = generator.any_alloc_status().ptr; + /// # } + /// ``` + /// + /// Kani cannot reason about a pointer allocation status (except for asserting its validity). + /// Thus, the generator was introduced to help writing harnesses that need to impose + /// constraints to the arbitrary pointer allocation status. + /// It also allow us to restrict the pointer provenance, excluding for example the address of + /// variables that are not available in the current context. + /// As a limitation, it will not cover the entire address space that a pointer can take. + /// + /// If your harness does not need to reason about pointer allocation, for example, verifying + /// pointer wrapping arithmetic, using a pointer with any address will allow you to cover + /// all possible scenarios. + #[derive(Debug)] + pub struct PointerGenerator { + // Internal allocation that may be used to generate valid pointers. + buf: MaybeUninit<[u8; BYTES]>, + } + + /// 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 + DeadObject, + /// Null pointers + Null, + /// In bounds pointer (it may be unaligned) + InBounds, + /// The pointer cannot be read / written to for the given type since one or more bytes + /// would be out of bounds of the current allocation. + OutOfBounds, + } + + /// 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 PointerGenerator { + const BUF_LEN: usize = BYTES; + const VALID : () = assert!(BYTES > 0, "PointerGenerator requires at least one byte."); + + /// Create a new PointerGenerator. + #[kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicates and manipulation feature" + )] + pub fn new() -> Self { + 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. + #[kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicates and manipulation feature" + )] + pub fn any_alloc_status<'a, T>(&'a mut self) -> ArbitraryPointer<'a, T> + where T: kani::Arbitrary + { + assert!(core::mem::size_of::() <= Self::BUF_LEN, + "Cannot generate in-bounds object of the requested type. Buffer is not big enough." + ); + + let status = kani::any(); + let ptr = match status { + AllocationStatus::Dangling => { + // Generate potentially unaligned pointer. + let offset = kani::any_where(|b: &usize| *b < size_of::()); + crate::ptr::NonNull::::dangling().as_ptr().wrapping_add(offset) + } + AllocationStatus::DeadObject => { + let mut obj: T = kani::any(); + &mut obj as *mut _ + } + AllocationStatus::Null => crate::ptr::null_mut::(), + AllocationStatus::InBounds => { + return self.create_in_bounds_ptr(); + } + AllocationStatus::OutOfBounds => { + // Generate potentially unaligned pointer. + let buf_ptr = addr_of_mut!(self.buf) as *mut u8; + let offset = kani::any_where(|b: &usize| *b < size_of::()); + unsafe { buf_ptr.add(Self::BUF_LEN - offset) as *mut T } + } + }; + + ArbitraryPointer { + ptr, + is_initialized: false, + status, + phantom: PhantomData, + } + } + + /// 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. + /// + /// ```no_run + /// # use kani::*; + /// # #[kani::proof] + /// # fn check_distance() { + /// let mut generator = PointerGenerator::<6>::new(); + /// let ptr1: *mut u8 = generator.any_in_bounds().ptr; + /// let ptr2: *mut u8 = generator.any_in_bounds().ptr; + /// // SAFETY: Both pointers have the same provenance. + /// let distance = unsafe { ptr1.offset_from(ptr2) }; + /// assert!(distance > -5 && distance < 5) + /// # } + /// ``` + #[kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicates and manipulation feature" + )] + pub fn any_in_bounds<'a, T>(&'a mut self) -> ArbitraryPointer<'a, T> + where T: kani::Arbitrary { + assert!(core::mem::size_of::() <= Self::BUF_LEN, + "Cannot generate in-bounds object of the requested type. Buffer is not big enough." + ); + self.create_in_bounds_ptr() + } + + /// This is the inner logic to create an arbitrary pointer that is inbounds. + /// + /// Note that pointer may be unaligned. + fn create_in_bounds_ptr<'a, T>(&'a mut self) -> ArbitraryPointer<'a, T> + where T: kani::Arbitrary { + assert!(core::mem::size_of::() <= Self::BUF_LEN, + "Cannot generate in-bounds object of the requested type. Buffer is not big enough." + ); + let buf_ptr = addr_of_mut!(self.buf) as *mut u8; + let offset = kani::any_where(|b: &usize| *b <= Self::BUF_LEN - size_of::()); + let ptr = unsafe { buf_ptr.add(offset) as *mut T }; + let is_initialized = kani::any(); + if is_initialized { + unsafe { ptr.write_unaligned(kani::any()) }; + } + ArbitraryPointer { + ptr, + is_initialized, + status: AllocationStatus::InBounds, + phantom: PhantomData, + } + } + } + + kani_core::ptr_generator_fn!(); + }; +} + +#[cfg(not(feature = "no_core"))] +#[macro_export] +macro_rules! ptr_generator_fn { + () => { + /// Create a pointer generator that fits at least `N` elements of type `T`. + pub fn pointer_generator() + -> PointerGenerator<{ size_of::() * NUM_ELTS }> { + PointerGenerator::<{ size_of::() * NUM_ELTS }>::new() + } + }; +} + +/// Don't generate the pointer_generator function here since it requires generic constant +/// expression. +#[cfg(feature = "no_core")] +#[macro_export] +macro_rules! ptr_generator_fn { + () => {}; +} diff --git a/library/kani_macros/src/derive.rs b/library/kani_macros/src/derive.rs index 04b288069387..258afc36af77 100644 --- a/library/kani_macros/src/derive.rs +++ b/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,11 +63,11 @@ 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 } } @@ -48,7 +75,7 @@ pub fn expand_derive_arbitrary(item: proc_macro::TokenStream) -> proc_macro::Tok } 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 diff --git a/tests/expected/arbitrary/ptrs/pointer_generator.expected b/tests/expected/arbitrary/ptrs/pointer_generator.expected new file mode 100644 index 000000000000..4627d354aebb --- /dev/null +++ b/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 diff --git a/tests/expected/arbitrary/ptrs/pointer_generator.rs b/tests/expected/arbitrary/ptrs/pointer_generator.rs new file mode 100644 index 000000000000..214c7fad2bfa --- /dev/null +++ b/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::(); + 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"); + } + }; +} diff --git a/tests/expected/arbitrary/ptrs/pointer_generator_error.expected b/tests/expected/arbitrary/ptrs/pointer_generator_error.expected new file mode 100644 index 000000000000..a0592c586a03 --- /dev/null +++ b/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();\ +| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/expected/arbitrary/ptrs/pointer_generator_error.rs b/tests/expected/arbitrary/ptrs/pointer_generator_error.rs new file mode 100644 index 000000000000..30b50f3699e3 --- /dev/null +++ b/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(); +} diff --git a/tests/expected/arbitrary/ptrs/pointer_inbounds.expected b/tests/expected/arbitrary/ptrs/pointer_inbounds.expected new file mode 100644 index 000000000000..838829163a36 --- /dev/null +++ b/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. diff --git a/tests/expected/arbitrary/ptrs/pointer_inbounds.rs b/tests/expected/arbitrary/ptrs/pointer_inbounds.rs new file mode 100644 index 000000000000..36e4abeff48b --- /dev/null +++ b/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::(); + 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 = kani::pointer_generator::(); + 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 = kani::pointer_generator::(); + 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::(); + let ptr_1 = generator.any_in_bounds::().ptr; + let ptr_2 = generator.any_in_bounds::().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"); +} diff --git a/tests/script-based-pre/verify_std_cmd/verify_core.rs b/tests/script-based-pre/verify_std_cmd/verify_core.rs index 9bdabb32dde3..551345653c7b 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_core.rs +++ b/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::().ptr; + assert!(kani::mem::can_write_unaligned(ptr)); + } } diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.expected b/tests/script-based-pre/verify_std_cmd/verify_std.expected index 16705ffcfefa..157adb94ba16 100644 --- a/tests/script-based-pre/verify_std_cmd/verify_std.expected +++ b/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 diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh index f06e8a8f9921..022e7b79de4a 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -52,10 +52,15 @@ cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs echo "[TEST] Run kani verify-std" export RUST_BACKTRACE=1 -kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing -Z mem-predicates +kani verify-std -Z unstable-options "${TMP_DIR}/library" \ + --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \ + -Z mem-predicates echo "[TEST] Run kani verify-std -Z uninit-checks" -RUSTFLAGS="--cfg=uninit_checks" kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing -Z mem-predicates -Z uninit-checks +export RUSTFLAGS="--cfg=uninit_checks" +kani verify-std -Z unstable-options "${TMP_DIR}/library" \ + --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing \ + -Z mem-predicates -Z uninit-checks # Cleanup rm -r ${TMP_DIR} diff --git a/tests/ui/arbitrary-ptr-doc/doc_examples.expected b/tests/ui/arbitrary-ptr-doc/doc_examples.expected new file mode 100644 index 000000000000..19c01006f313 --- /dev/null +++ b/tests/ui/arbitrary-ptr-doc/doc_examples.expected @@ -0,0 +1,24 @@ +Checking harness check_distance... +VERIFICATION:- SUCCESSFUL + +Checking harness diff_from_usize... +VERIFICATION:- SUCCESSFUL + +Checking harness usage_example... +VERIFICATION:- SUCCESSFUL + +Checking harness pointer_may_be_same... + ** 1 of 1 cover properties satisfied +VERIFICATION:- SUCCESSFUL + +Checking harness generator_large_enough... + ** 2 of 2 cover properties satisfied +VERIFICATION:- SUCCESSFUL + +Checking harness same_capacity... +VERIFICATION:- SUCCESSFUL + +Checking harness basic_inbounds... +VERIFICATION:- SUCCESSFUL + +Complete - 7 successfully verified harnesses, 0 failures, 7 total. diff --git a/tests/ui/arbitrary-ptr-doc/doc_examples.rs b/tests/ui/arbitrary-ptr-doc/doc_examples.rs new file mode 100644 index 000000000000..319863f6f6ef --- /dev/null +++ b/tests/ui/arbitrary-ptr-doc/doc_examples.rs @@ -0,0 +1,90 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// kani-flags: -Z mem-predicates + +//! These are copies of the examples we added to our documentation. +//! We currently cannot run our examples using Kani. +//! We may be able to leverage `--runtool` from rustdoc once its stabilized. See +//! . +#![allow(unused)] + +extern crate kani; + +use kani::*; +#[kani::proof] +fn basic_inbounds() { + let mut generator = PointerGenerator::<10>::new(); + let arbitrary = generator.any_alloc_status::(); + kani::assume(arbitrary.status == AllocationStatus::InBounds); + // Pointer may be unaligned, but it should be in-bounds, so it is safe to write to + unsafe { arbitrary.ptr.write_unaligned(kani::any()) } +} + +#[kani::proof] +fn same_capacity() { + // These generators have the same capacity of 6 bytes. + let generator1 = PointerGenerator::<6>::new(); + let generator2 = pointer_generator::(); +} + +#[kani::proof] +fn generator_large_enough() { + let mut generator = PointerGenerator::<6>::new(); + let ptr1: *mut u8 = generator.any_in_bounds().ptr; + let ptr2: *mut u8 = generator.any_in_bounds().ptr; + let ptr3: *mut u32 = generator.any_in_bounds().ptr; + // This cover is satisfied. + cover!( + (ptr1 as usize) >= (ptr2 as usize) + size_of::() + && (ptr2 as usize) >= (ptr3 as usize) + size_of::() + ); + // As well as having overlapping pointers. + cover!((ptr1 as usize) == (ptr3 as usize)); +} + +#[kani::proof] +fn pointer_may_be_same() { + let mut generator = pointer_generator::(); + let ptr1 = generator.any_in_bounds::().ptr; + let ptr2 = generator.any_in_bounds::().ptr; + // This cover is satisfied. + cover!(ptr1 == ptr2) +} +unsafe fn my_target(_ptr1: *const T, _ptr2: *const T) {} + +#[kani::proof] +fn usage_example() { + let mut generator1 = pointer_generator::(); + let mut generator2 = pointer_generator::(); + let ptr1: *const char = generator1.any_in_bounds().ptr; + let ptr2: *const char = if kani::any() { + // Pointers will have same provenance and may overlap. + generator1.any_in_bounds().ptr + } else { + // Pointers will have different provenance and will not overlap. + generator2.any_in_bounds().ptr + }; + // Invoke the function under verification + unsafe { my_target(ptr1, ptr2) }; +} +#[kani::proof] +fn diff_from_usize() { + // This pointer represents any address, and it may point to anything in memory, + // allocated or not. + let ptr1 = kani::any::() as *const u8; + + // This pointer address will either point to unallocated memory, to a dead object + // or to allocated memory within the generator address space. + let mut generator = PointerGenerator::<5>::new(); + let ptr2: *const u8 = generator.any_alloc_status().ptr; +} +#[kani::proof] +fn check_distance() { + let mut generator = PointerGenerator::<6>::new(); + let ptr1: *mut u8 = generator.any_in_bounds().ptr; + let ptr2: *mut u8 = generator.any_in_bounds().ptr; + // SAFETY: Both pointers have the same provenance. + let distance = unsafe { ptr1.offset_from(ptr2) }; + assert!(distance >= -5 && distance <= 5) +} From 74228dd07cb53210dcfb5f18bcb85127bab39b09 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 7 Oct 2024 11:49:14 -0400 Subject: [PATCH 2/3] Automatic cargo update to 2024-10-07 (#3572) Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com> --- Cargo.lock | 39 ++++++++++++++++++--------------------- 1 file changed, 18 insertions(+), 21 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index acc0cc485bdb..0cd3c1af05f4 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -147,9 +147,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.5.18" +version = "4.5.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0956a43b323ac1afaffc053ed5c4b7c1f1800bacd1683c353aabbb752515dd3" +checksum = "7be5744db7978a28d9df86a214130d106a89ce49644cbc4e3f0c22c3fba30615" dependencies = [ "clap_builder", "clap_derive", @@ -157,9 +157,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.18" +version = "4.5.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4d72166dd41634086d5803a47eb71ae740e61d84709c36f3c34110173db3961b" +checksum = "a5fbc17d3ef8278f55b282b2a2e75ae6f6c7d4bb70ed3d0382375104bfafdb4b" dependencies = [ "anstream", "anstyle", @@ -411,6 +411,12 @@ dependencies = [ "ahash", ] +[[package]] +name = "hashbrown" +version = "0.15.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e087f84d4f86bf4b218b927129862374b72199ae7d8657835f1e89000eea4fb" + [[package]] name = "heck" version = "0.5.0" @@ -428,12 +434,12 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.5.0" +version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68b900aa2f7301e21c36462b170ee99994de34dff39a4a6a528e80e7376d07e5" +checksum = "707907fe3c25f5424cce2cb7e1cbcafee6bdbe735ca90ef77c29e84591e5b9da" dependencies = [ "equivalent", - "hashbrown", + "hashbrown 0.15.0", ] [[package]] @@ -720,12 +726,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.20.1" +version = "1.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "82881c4be219ab5faaf2ad5e5e5ecdff8c66bd7402ca3160975c93b24961afd1" -dependencies = [ - "portable-atomic", -] +checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" [[package]] name = "os_info" @@ -788,12 +791,6 @@ version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02" -[[package]] -name = "portable-atomic" -version = "1.9.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cc9c68a3f6da06753e9335d63e27f6b9754dd1920d941135b7ea8224f141adb2" - [[package]] name = "powerfmt" version = "0.2.0" @@ -901,9 +898,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.6" +version = "0.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "355ae415ccd3a04315d3f8246e86d67689ea74d88d915576e1589a351062a13b" +checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" dependencies = [ "bitflags", ] @@ -1117,7 +1114,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1c6a0d765f5807e98a091107bae0a56ea3799f66a5de47b2c84c94a39c09974e" dependencies = [ "cfg-if", - "hashbrown", + "hashbrown 0.14.5", "serde", ] From 1c38609ec35f591898b94ec39427d1b5b0cad824 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 7 Oct 2024 10:29:25 -0700 Subject: [PATCH 3/3] Bump tests/perf/s2n-quic from `2a735a9` to `17171ec` (#3573) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `2a735a9` to `17171ec`.
Commits
  • 17171ec build(deps): update hashbrown requirement from 0.14 to 0.15 (#2341)
  • c9a86c3 feat(s2n-quic-dc): shrink path secret & fix fixed-map allocation (#2340)
  • cb5087c feat(s2n-quic-dc): Further shrink path secret entry (#2339)
  • See full diff in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) ---
Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- tests/perf/s2n-quic | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 2a735a983a54..17171ece180d 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 2a735a983a5426b13c926d19090d32ea0a99ea36 +Subproject commit 17171ece180d6512f21dd98cdc8637e33646d994