From 2a0e9bdbb65459b05f499f687285cb764e654354 Mon Sep 17 00:00:00 2001 From: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> Date: Tue, 6 Aug 2024 11:59:15 -0400 Subject: [PATCH] Unify kani library and kani core logic (#3333) 1. Unifies `Kani library` and `kani_core` for `Arbitrary`, `mem` and `intrinsics` along with the `internal` module. 2. Adjusts some regression expected files to reflect the new underlying source of Arbitrary Related to #https://github.com/model-checking/kani/issues/3257 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- Cargo.lock | 1 + library/kani/Cargo.toml | 2 + library/kani/src/arbitrary.rs | 146 +----- library/kani/src/internal.rs | 160 ------- library/kani/src/lib.rs | 310 +------------ library/kani/src/mem.rs | 433 ------------------ library/kani_core/Cargo.toml | 2 +- library/kani_core/src/lib.rs | 5 + library/kani_core/src/mem.rs | 76 ++- library/kani_macros/Cargo.toml | 2 +- .../modifies/check_invalid_modifies.expected | 7 +- .../function-contract/valid_ptr.expected | 1 - .../verify_std_cmd/verify_std.sh | 2 +- .../non_arbitrary_param/expected | 6 +- 14 files changed, 71 insertions(+), 1082 deletions(-) delete mode 100644 library/kani/src/internal.rs delete mode 100644 library/kani/src/mem.rs diff --git a/Cargo.lock b/Cargo.lock index dcd7b057b3d8..7d7580e3b742 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -434,6 +434,7 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" name = "kani" version = "0.53.0" dependencies = [ + "kani_core", "kani_macros", ] diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 91fee3dabf30..1fba7875672a 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -10,6 +10,8 @@ publish = false [dependencies] kani_macros = { path = "../kani_macros" } +kani_core = { path = "../kani_core" } [features] concrete_playback = [] +no_core=["kani_macros/no_core"] diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs index 83b113d64927..f16f06165d29 100644 --- a/library/kani/src/arbitrary.rs +++ b/library/kani/src/arbitrary.rs @@ -4,151 +4,7 @@ //! This module introduces the `Arbitrary` trait as well as implementation for //! primitive types and other std containers. -use std::{ - marker::{PhantomData, PhantomPinned}, - num::*, -}; - -/// This trait should be used to generate symbolic variables that represent any valid value of -/// its type. -pub trait Arbitrary -where - Self: Sized, -{ - fn any() -> Self; - fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - [(); MAX_ARRAY_LENGTH].map(|_| Self::any()) - } -} - -/// The given type can be represented by an unconstrained symbolic value of size_of::. -macro_rules! trivial_arbitrary { - ( $type: ty ) => { - impl Arbitrary for $type { - #[inline(always)] - fn any() -> Self { - // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic. - unsafe { crate::any_raw_internal::() } - } - fn any_array() -> [Self; MAX_ARRAY_LENGTH] { - unsafe { crate::any_raw_array::() } - } - } - }; -} - -trivial_arbitrary!(u8); -trivial_arbitrary!(u16); -trivial_arbitrary!(u32); -trivial_arbitrary!(u64); -trivial_arbitrary!(u128); -trivial_arbitrary!(usize); - -trivial_arbitrary!(i8); -trivial_arbitrary!(i16); -trivial_arbitrary!(i32); -trivial_arbitrary!(i64); -trivial_arbitrary!(i128); -trivial_arbitrary!(isize); - -// We do not constrain floating points values per type spec. Users must add assumptions to their -// verification code if they want to eliminate NaN, infinite, or subnormal. -trivial_arbitrary!(f32); -trivial_arbitrary!(f64); - -// Similarly, we do not constraint values for non-standard floating types. -trivial_arbitrary!(f16); -trivial_arbitrary!(f128); - -trivial_arbitrary!(()); - -impl Arbitrary for bool { - #[inline(always)] - fn any() -> Self { - let byte = u8::any(); - crate::assume(byte < 2); - byte == 1 - } -} - -/// Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF] -/// Ref: -impl Arbitrary for char { - #[inline(always)] - fn any() -> Self { - // Generate an arbitrary u32 and constrain it to make it a valid representation of char. - let val = u32::any(); - crate::assume(val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val)); - unsafe { char::from_u32_unchecked(val) } - } -} - -macro_rules! nonzero_arbitrary { - ( $type: ty, $base: ty ) => { - impl Arbitrary for $type { - #[inline(always)] - fn any() -> Self { - let val = <$base>::any(); - crate::assume(val != 0); - unsafe { <$type>::new_unchecked(val) } - } - } - }; -} - -nonzero_arbitrary!(NonZeroU8, u8); -nonzero_arbitrary!(NonZeroU16, u16); -nonzero_arbitrary!(NonZeroU32, u32); -nonzero_arbitrary!(NonZeroU64, u64); -nonzero_arbitrary!(NonZeroU128, u128); -nonzero_arbitrary!(NonZeroUsize, usize); - -nonzero_arbitrary!(NonZeroI8, i8); -nonzero_arbitrary!(NonZeroI16, i16); -nonzero_arbitrary!(NonZeroI32, i32); -nonzero_arbitrary!(NonZeroI64, i64); -nonzero_arbitrary!(NonZeroI128, i128); -nonzero_arbitrary!(NonZeroIsize, isize); - -impl Arbitrary for [T; N] -where - T: Arbitrary, -{ - fn any() -> Self { - T::any_array() - } -} - -impl Arbitrary for Option -where - T: Arbitrary, -{ - fn any() -> Self { - if bool::any() { Some(T::any()) } else { None } - } -} - -impl Arbitrary for Result -where - T: Arbitrary, - E: Arbitrary, -{ - fn any() -> Self { - if bool::any() { Ok(T::any()) } else { Err(E::any()) } - } -} - -impl Arbitrary for std::marker::PhantomData { - fn any() -> Self { - PhantomData - } -} - -impl Arbitrary for std::marker::PhantomPinned { - fn any() -> Self { - PhantomPinned - } -} +use crate::Arbitrary; impl Arbitrary for std::boxed::Box where diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs deleted file mode 100644 index 68b15316b4c1..000000000000 --- a/library/kani/src/internal.rs +++ /dev/null @@ -1,160 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use crate::arbitrary::Arbitrary; -use std::ptr; - -/// Helper trait for code generation for `modifies` contracts. -/// -/// We allow the user to provide us with a pointer-like object that we convert as needed. -#[doc(hidden)] -pub trait Pointer { - /// Type of the pointed-to data - type Inner: ?Sized; - - /// used for havocking on replecement of a `modifies` clause. - unsafe fn assignable(self) -> *mut Self::Inner; -} - -impl Pointer for &T { - type Inner = T; - unsafe fn assignable(self) -> *mut Self::Inner { - self as *const T as *mut T - } -} - -impl Pointer for &mut T { - type Inner = T; - - unsafe fn assignable(self) -> *mut Self::Inner { - self as *mut T - } -} - -impl Pointer for *const T { - type Inner = T; - - unsafe fn assignable(self) -> *mut Self::Inner { - self as *mut T - } -} - -impl Pointer for *mut T { - type Inner = T; - unsafe fn assignable(self) -> *mut Self::Inner { - self - } -} - -/// A way to break the ownerhip rules. Only used by contracts where we can -/// guarantee it is done safely. -/// TODO: Remove this! This is not safe. Users should be able to use `ptr::read` and `old` if -/// they really need to. See . -#[inline(never)] -#[doc(hidden)] -#[rustc_diagnostic_item = "KaniUntrackedDeref"] -pub fn untracked_deref(_: &T) -> T { - todo!() -} - -/// CBMC contracts currently has a limitation where `free` has to be in scope. -/// However, if there is no dynamic allocation in the harness, slicing removes `free` from the -/// scope. -/// -/// Thus, this function will basically translate into: -/// ```c -/// // This is a no-op. -/// free(NULL); -/// ``` -#[inline(never)] -#[doc(hidden)] -#[rustc_diagnostic_item = "KaniInitContracts"] -pub fn init_contracts() {} - -/// This should only be used within contracts. The intent is to -/// perform type inference on a closure's argument -/// TODO: This should be generated inside the function that has contract. This is used for -/// remembers. -#[doc(hidden)] -pub fn apply_closure bool>(f: U, x: &T) -> bool { - f(x) -} - -/// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object. -/// Only for use within function contracts and will not be replaced if the recursive or function stub -/// replace contracts are not used. -#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] -#[rustc_diagnostic_item = "KaniWriteAny"] -#[inline(never)] -#[doc(hidden)] -pub unsafe fn write_any(_pointer: *mut T) { - // This function should not be reacheable. - // Users must include `#[kani::recursion]` in any function contracts for recursive functions; - // otherwise, this might not be properly instantiate. We mark this as unreachable to make - // sure Kani doesn't report any false positives. - unreachable!() -} - -/// Fill in a slice with kani::any. -/// Intended as a post compilation replacement for write_any -#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] -#[rustc_diagnostic_item = "KaniWriteAnySlice"] -#[inline(always)] -pub unsafe fn write_any_slice(slice: *mut [T]) { - (*slice).fill_with(T::any) -} - -/// Fill in a pointer with kani::any. -/// Intended as a post compilation replacement for write_any -#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] -#[rustc_diagnostic_item = "KaniWriteAnySlim"] -#[inline(always)] -pub unsafe fn write_any_slim(pointer: *mut T) { - ptr::write(pointer, T::any()) -} - -/// Fill in a str with kani::any. -/// Intended as a post compilation replacement for write_any. -/// Not yet implemented -#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")] -#[rustc_diagnostic_item = "KaniWriteAnyStr"] -#[inline(always)] -pub unsafe fn write_any_str(_s: *mut str) { - //TODO: strings introduce new UB - //(*s).as_bytes_mut().fill_with(u8::any) - //TODO: String validation - unimplemented!("Kani does not support creating arbitrary `str`") -} - -/// Function that calls a closure used to implement contracts. -/// -/// In contracts, we cannot invoke the generated closures directly, instead, we call register -/// contract. This function is a no-op. However, in the reality, we do want to call the closure, -/// so we swap the register body by this function body. -#[doc(hidden)] -#[allow(dead_code)] -#[rustc_diagnostic_item = "KaniRunContract"] -#[crate::unstable( - feature = "function-contracts", - issue = "none", - reason = "internal function required to run contract closure" -)] -fn run_contract_fn T>(func: F) -> T { - func() -} - -/// This is used by contracts to select which version of the contract to use during codegen. -#[doc(hidden)] -pub type Mode = u8; - -/// Keep the original body. -pub const ORIGINAL: Mode = 0; - -/// Run the check with recursion support. -pub const RECURSION_CHECK: Mode = 1; - -/// Run the simple check with no recursion support. -pub const SIMPLE_CHECK: Mode = 2; - -/// Stub the body with its contract. -pub const REPLACE: Mode = 3; diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 046c6e7a0667..59a89622a52d 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -28,19 +28,13 @@ pub mod arbitrary; mod concrete_playback; pub mod futures; pub mod invariant; -pub mod mem; pub mod shadow; pub mod slice; -pub mod tuple; pub mod vec; -#[doc(hidden)] -pub mod internal; - mod mem_init; mod models; -pub use arbitrary::Arbitrary; #[cfg(feature = "concrete_playback")] pub use concrete_playback::concrete_playback_run; pub use invariant::Invariant; @@ -53,287 +47,19 @@ pub fn concrete_playback_run(_: Vec>, _: F) { pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin}; -/// Creates an assumption that will be valid after this statement run. Note that the assumption -/// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the -/// program will exit successfully. -/// -/// # Example: -/// -/// The code snippet below should never panic. -/// -/// ```rust -/// let i : i32 = kani::any(); -/// kani::assume(i > 10); -/// if i < 0 { -/// panic!("This will never panic"); -/// } -/// ``` -/// -/// The following code may panic though: -/// -/// ```rust -/// let i : i32 = kani::any(); -/// assert!(i < 0, "This may panic and verification should fail."); -/// kani::assume(i > 10); -/// ``` -#[inline(never)] -#[rustc_diagnostic_item = "KaniAssume"] -#[cfg(not(feature = "concrete_playback"))] -pub fn assume(cond: bool) { - let _ = cond; -} - -#[inline(never)] -#[rustc_diagnostic_item = "KaniAssume"] -#[cfg(feature = "concrete_playback")] -pub fn assume(cond: bool) { - assert!(cond, "`kani::assume` should always hold"); -} - -/// `implies!(premise => conclusion)` means that if the `premise` is true, so -/// must be the `conclusion`. -/// -/// This simply expands to `!premise || conclusion` and is intended to make checks more readable, -/// as the concept of an implication is more natural to think about than its expansion. -#[macro_export] -macro_rules! implies { - ($premise:expr => $conclusion:expr) => { - !($premise) || ($conclusion) - }; -} - -/// Creates an assertion of the specified condition and message. -/// -/// # Example: -/// -/// ```rust -/// let x: bool = kani::any(); -/// let y = !x; -/// kani::assert(x || y, "ORing a boolean variable with its negation must be true") -/// ``` -#[cfg(not(feature = "concrete_playback"))] -#[inline(never)] -#[rustc_diagnostic_item = "KaniAssert"] -pub const fn assert(cond: bool, msg: &'static str) { - let _ = cond; - let _ = msg; -} - -#[cfg(feature = "concrete_playback")] -#[inline(never)] -#[rustc_diagnostic_item = "KaniAssert"] -pub const fn assert(cond: bool, msg: &'static str) { - assert!(cond, "{}", msg); -} - -/// Creates an assertion of the specified condition, but does not assume it afterwards. -/// -/// # Example: -/// -/// ```rust -/// let x: bool = kani::any(); -/// let y = !x; -/// kani::check(x || y, "ORing a boolean variable with its negation must be true") -/// ``` -#[cfg(not(feature = "concrete_playback"))] -#[inline(never)] -#[rustc_diagnostic_item = "KaniCheck"] -pub const fn check(cond: bool, msg: &'static str) { - let _ = cond; - let _ = msg; -} - -#[cfg(feature = "concrete_playback")] -#[inline(never)] -#[rustc_diagnostic_item = "KaniCheck"] -pub const fn check(cond: bool, msg: &'static str) { - assert!(cond, "{}", msg); -} - -/// Creates a cover property with the specified condition and message. -/// -/// # Example: -/// -/// ```rust -/// kani::cover(slice.len() == 0, "The slice may have a length of 0"); -/// ``` -/// -/// A cover property checks if there is at least one execution that satisfies -/// the specified condition at the location in which the function is called. -/// -/// Cover properties are reported as: -/// - SATISFIED: if Kani found an execution that satisfies the condition -/// - UNSATISFIABLE: if Kani proved that the condition cannot be satisfied -/// - UNREACHABLE: if Kani proved that the cover property itself is unreachable (i.e. it is vacuously UNSATISFIABLE) -/// -/// This function is called by the [`cover!`] macro. The macro is more -/// convenient to use. -/// -#[inline(never)] -#[rustc_diagnostic_item = "KaniCover"] -pub const fn cover(_cond: bool, _msg: &'static str) {} +// Kani proc macros must be in a separate crate +pub use kani_macros::*; -/// This creates an symbolic *valid* value of type `T`. You can assign the return value of this -/// function to a variable that you want to make symbolic. -/// -/// # Example: -/// -/// In the snippet below, we are verifying the behavior of the function `fn_under_verification` -/// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero. -/// -/// ```rust -/// let inputA = kani::any::(); -/// fn_under_verification(inputA); -/// ``` -/// -/// Note: This is a safe construct and can only be used with types that implement the `Arbitrary` -/// trait. The Arbitrary trait is used to build a symbolic value that represents all possible -/// valid values for type `T`. -#[rustc_diagnostic_item = "KaniAny"] -#[inline(always)] -pub fn any() -> T { - T::any() -} +// Declare common Kani API such as assume, assert +kani_core::kani_lib!(kani); -/// This function is only used for function contract instrumentation. -/// It behaves exaclty like `kani::any()`, except it will check for the trait bounds -/// at compilation time. It allows us to avoid type checking errors while using function -/// contracts only for verification. -#[rustc_diagnostic_item = "KaniAnyModifies"] -#[inline(never)] +// Used to bind `core::assert` to a different name to avoid possible name conflicts if a +// crate uses `extern crate std as core`. See +// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187 #[doc(hidden)] -pub fn any_modifies() -> T { - // This function should not be reacheable. - // Users must include `#[kani::recursion]` in any function contracts for recursive functions; - // otherwise, this might not be properly instantiate. We mark this as unreachable to make - // sure Kani doesn't report any false positives. - unreachable!() -} - -/// This creates a symbolic *valid* value of type `T`. -/// The value is constrained to be a value accepted by the predicate passed to the filter. -/// You can assign the return value of this function to a variable that you want to make symbolic. -/// -/// # Example: -/// -/// In the snippet below, we are verifying the behavior of the function `fn_under_verification` -/// under all possible `u8` input values between 0 and 12. -/// -/// ```rust -/// let inputA: u8 = kani::any_where(|x| *x < 12); -/// fn_under_verification(inputA); -/// ``` -/// -/// Note: This is a safe construct and can only be used with types that implement the `Arbitrary` -/// trait. The Arbitrary trait is used to build a symbolic value that represents all possible -/// valid values for type `T`. -#[inline(always)] -pub fn any_where bool>(f: F) -> T { - let result = T::any(); - assume(f(&result)); - result -} - -/// This function creates a symbolic value of type `T`. This may result in an invalid value. -/// -/// # Safety -/// -/// This function is unsafe and it may represent invalid `T` values which can lead to many -/// undesirable undefined behaviors. Because of that, this function can only be used -/// internally when we can guarantee that the type T has no restriction regarding its bit level -/// representation. -/// -/// This function is also used to find concrete values in the CBMC output trace -/// and return those concrete values in concrete playback mode. -/// -/// Note that SIZE_T must be equal the size of type T in bytes. -#[inline(never)] -#[cfg(not(feature = "concrete_playback"))] -unsafe fn any_raw_internal() -> T { - any_raw::() -} - -/// This is the same as [any_raw_internal] for verification flow, but not for concrete playback. -#[inline(never)] #[cfg(not(feature = "concrete_playback"))] -unsafe fn any_raw_array() -> [T; N] { - any_raw::<[T; N]>() -} - -#[cfg(feature = "concrete_playback")] -use concrete_playback::{any_raw_array, any_raw_internal}; - -/// This low-level function returns nondet bytes of size T. -#[rustc_diagnostic_item = "KaniAnyRaw"] -#[inline(never)] -#[allow(dead_code)] -fn any_raw() -> T { - kani_intrinsic() -} - -/// Function used to generate panic with a static message as this is the only one currently -/// supported by Kani display. -/// -/// During verification this will get replaced by `assert(false)`. For concrete executions, we just -/// invoke the regular `std::panic!()` function. This function is used by our standard library -/// overrides, but not the other way around. -#[inline(never)] -#[rustc_diagnostic_item = "KaniPanic"] -#[doc(hidden)] -pub const fn panic(message: &'static str) -> ! { - panic!("{}", message) -} +pub use core::assert as __kani__workaround_core_assert; -/// 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 { - #[allow(clippy::empty_loop)] - loop {} -} -/// A macro to check if a condition is satisfiable at a specific location in the -/// code. -/// -/// # Example 1: -/// -/// ```rust -/// let mut set: BTreeSet = BTreeSet::new(); -/// set.insert(kani::any()); -/// set.insert(kani::any()); -/// // check if the set can end up with a single element (if both elements -/// // inserted were the same) -/// kani::cover!(set.len() == 1); -/// ``` -/// The macro can also be called without any arguments to check if a location is -/// reachable. -/// -/// # Example 2: -/// -/// ```rust -/// match e { -/// MyEnum::A => { /* .. */ } -/// MyEnum::B => { -/// // make sure the `MyEnum::B` variant is possible -/// kani::cover!(); -/// // .. -/// } -/// } -/// ``` -/// -/// A custom message can also be passed to the macro. -/// -/// # Example 3: -/// -/// ```rust -/// kani::cover!(x > y, "x can be greater than y") -/// ``` #[macro_export] macro_rules! cover { () => { @@ -347,15 +73,17 @@ macro_rules! cover { }; } -// Used to bind `core::assert` to a different name to avoid possible name conflicts if a -// crate uses `extern crate std as core`. See -// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187 -#[doc(hidden)] -#[cfg(not(feature = "concrete_playback"))] -pub use core::assert as __kani__workaround_core_assert; - -// Kani proc macros must be in a separate crate -pub use kani_macros::*; +/// `implies!(premise => conclusion)` means that if the `premise` is true, so +/// must be the `conclusion`. +/// +/// This simply expands to `!premise || conclusion` and is intended to make checks more readable, +/// as the concept of an implication is more natural to think about than its expansion. +#[macro_export] +macro_rules! implies { + ($premise:expr => $conclusion:expr) => { + !($premise) || ($conclusion) + }; +} pub(crate) use kani_macros::unstable_feature as unstable; diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs deleted file mode 100644 index f718c09ec38d..000000000000 --- a/library/kani/src/mem.rs +++ /dev/null @@ -1,433 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! This module contains functions useful for checking unsafe memory access. -//! -//! Given the following validity rules provided in the Rust documentation: -//! (accessed Feb 6th, 2024) -//! -//! 1. A null pointer is never valid, not even for accesses of size zero. -//! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer -//! be dereferenceable: the memory range of the given size starting at the pointer must all be -//! within the bounds of a single allocated object. Note that in Rust, every (stack-allocated) -//! variable is considered a separate allocated object. -//! ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory, -//! i.e., deallocation makes pointers invalid even for zero-sized operations.~~ -//! ZST access is not OK for any pointer. -//! See: -//! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized -//! accesses, even if some memory happens to exist at that address and gets deallocated. -//! This corresponds to writing your own allocator: allocating zero-sized objects is not very -//! hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is -//! `NonNull::dangling`. -//! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic -//! operations used to synchronize between threads. -//! This means it is undefined behavior to perform two concurrent accesses to the same location -//! from different threads unless both accesses only read from memory. -//! Notice that this explicitly includes `read_volatile` and `write_volatile`: -//! Volatile accesses cannot be used for inter-thread synchronization. -//! 5. The result of casting a reference to a pointer is valid for as long as the underlying -//! object is live and no reference (just raw pointers) is used to access the same memory. -//! That is, reference and pointer accesses cannot be interleaved. -//! -//! Kani is able to verify #1 and #2 today. -//! -//! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if -//! the address matches `NonNull::<()>::dangling()`. -//! 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}; - -/// Check if the pointer is valid for write access according to [crate::mem] conditions 1, 2 -/// and 3. -/// -/// Note this function also checks for pointer alignment. Use [self::can_write_unaligned] -/// if you don't want to fail for unaligned pointers. -/// -/// This function does not check if the value stored is valid for the given type. Use -/// [self::can_dereference] for that. -/// -/// 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 for more details. -#[crate::unstable( - feature = "mem-predicates", - issue = 2690, - reason = "experimental memory predicate API" -)] -pub fn can_write(ptr: *mut T) -> bool -where - T: ?Sized, - ::Metadata: PtrProperties, -{ - // 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) -} - -/// 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 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 for more details. -#[crate::unstable( - feature = "mem-predicates", - issue = 2690, - reason = "experimental memory predicate API" -)] -pub fn can_write_unaligned(ptr: *const T) -> bool -where - T: ?Sized, - ::Metadata: PtrProperties, -{ - let (thin_ptr, metadata) = ptr.to_raw_parts(); - is_inbounds(&metadata, thin_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`. -/// -/// TODO: Kani should automatically add those checks when a de-reference happens. -/// -/// -/// 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 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_dereference(ptr: *const T) -> bool -where - T: ?Sized, - ::Metadata: PtrProperties, -{ - let (thin_ptr, metadata) = ptr.to_raw_parts(); - // Need to assert `is_initialized` because non-determinism is used under the hood, so it does - // not make sense to use it inside assumption context. - metadata.is_ptr_aligned(thin_ptr, Internal) - && is_inbounds(&metadata, thin_ptr) - && assert_is_initialized(ptr) - && 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 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(ptr: *const T) -> bool -where - T: ?Sized, - ::Metadata: PtrProperties, -{ - let (thin_ptr, metadata) = ptr.to_raw_parts(); - // Need to assert `is_initialized` because non-determinism is used under the hood, so it does - // not make sense to use it inside assumption context. - is_inbounds(&metadata, thin_ptr) - && assert_is_initialized(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` -fn is_inbounds(metadata: &M, data_ptr: *const ()) -> bool -where - M: PtrProperties, - T: ?Sized, -{ - let sz = metadata.pointee_size(Internal); - if sz == 0 { - true // ZST pointers are always valid including nullptr. - } else if data_ptr.is_null() { - false - } else { - // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be - // stubbed. - // We first assert that the data_ptr - crate::assert( - unsafe { is_allocated(data_ptr, 0) }, - "Kani does not support reasoning about pointer to unallocated memory", - ); - unsafe { is_allocated(data_ptr, sz) } - } -} - -mod private { - /// Define like this to restrict usage of PtrProperties functions outside Kani. - #[derive(Copy, Clone)] - pub struct Internal; -} - -/// Trait that allow us to extract information from pointers without de-referencing them. -#[doc(hidden)] -pub trait PtrProperties { - fn pointee_size(&self, _: Internal) -> usize; - - /// A pointer is aligned if its address is a multiple of its minimum alignment. - fn is_ptr_aligned(&self, ptr: *const (), internal: Internal) -> bool { - let min = self.min_alignment(internal); - ptr as usize % min == 0 - } - - fn min_alignment(&self, _: Internal) -> usize; - - fn dangling(&self, _: Internal) -> *const (); -} - -/// Get the information for sized types (they don't have metadata). -impl PtrProperties for () { - fn pointee_size(&self, _: Internal) -> usize { - size_of::() - } - - fn min_alignment(&self, _: Internal) -> usize { - align_of::() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::::dangling().as_ptr() as *const _ - } -} - -/// Get the information from the str metadata. -impl PtrProperties for usize { - #[inline(always)] - fn pointee_size(&self, _: Internal) -> usize { - *self - } - - /// String slices are a UTF-8 representation of characters that have the same layout as slices - /// of type [u8]. - /// - fn min_alignment(&self, _: Internal) -> usize { - align_of::() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::::dangling().as_ptr() as _ - } -} - -/// Get the information from the slice metadata. -impl PtrProperties<[T]> for usize { - fn pointee_size(&self, _: Internal) -> usize { - *self * size_of::() - } - - fn min_alignment(&self, _: Internal) -> usize { - align_of::() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::::dangling().as_ptr() as _ - } -} - -/// Get the information from the vtable. -impl PtrProperties for DynMetadata -where - T: ?Sized, -{ - fn pointee_size(&self, _: Internal) -> usize { - self.size_of() - } - - 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`. -/// -/// # Safety -/// -/// This function should only be called to ensure a pointer is always valid, i.e., in an assertion -/// context. -/// -/// I.e.: This function always returns `true` if the pointer is valid. -/// Otherwise, it returns non-det boolean. -#[rustc_diagnostic_item = "KaniIsAllocated"] -#[inline(never)] -unsafe fn is_allocated(_ptr: *const (), _size: usize) -> bool { - kani_intrinsic() -} - -/// 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(_ptr: *const T) -> bool { - kani_intrinsic() -} - -/// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. -#[rustc_diagnostic_item = "KaniIsInitialized"] -#[inline(never)] -pub(crate) fn is_initialized(_ptr: *const T) -> bool { - kani_intrinsic() -} - -/// A helper to assert `is_initialized` to use it as a part of other predicates. -fn assert_is_initialized(ptr: *const T) -> bool { - crate::check(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer"); - true -} - -/// Get the object ID of the given pointer. -#[doc(hidden)] -#[crate::unstable( - feature = "ghost-state", - issue = 3184, - reason = "experimental ghost state/shadow memory API" -)] -#[rustc_diagnostic_item = "KaniPointerObject"] -#[inline(never)] -pub fn pointer_object(_ptr: *const T) -> usize { - kani_intrinsic() -} - -/// Get the object offset of the given pointer. -#[doc(hidden)] -#[crate::unstable( - feature = "ghost-state", - issue = 3184, - reason = "experimental ghost state/shadow memory API" -)] -#[rustc_diagnostic_item = "KaniPointerOffset"] -#[inline(never)] -pub fn pointer_offset(_ptr: *const T) -> usize { - kani_intrinsic() -} - -#[cfg(test)] -mod tests { - use super::{can_dereference, can_write, PtrProperties}; - use crate::mem::private::Internal; - use std::fmt::Debug; - use std::intrinsics::size_of; - use std::mem::{align_of, align_of_val, size_of_val}; - use std::ptr; - use std::ptr::{NonNull, Pointee}; - - fn size_of_t(ptr: *const T) -> usize - where - T: ?Sized, - ::Metadata: PtrProperties, - { - let (_, metadata) = ptr.to_raw_parts(); - metadata.pointee_size(Internal) - } - - fn align_of_t(ptr: *const T) -> usize - where - T: ?Sized, - ::Metadata: PtrProperties, - { - let (_, metadata) = ptr.to_raw_parts(); - metadata.min_alignment(Internal) - } - - #[test] - fn test_size_of() { - assert_eq!(size_of_t("hi"), size_of_val("hi")); - assert_eq!(size_of_t(&0u8), size_of_val(&0u8)); - assert_eq!(size_of_t(&0u8 as *const dyn std::fmt::Display), size_of_val(&0u8)); - assert_eq!(size_of_t(&[0u8, 1u8] as &[u8]), size_of_val(&[0u8, 1u8])); - assert_eq!(size_of_t(&[] as &[u8]), size_of_val::<[u8; 0]>(&[])); - assert_eq!( - size_of_t(NonNull::::dangling().as_ptr() as *const dyn std::fmt::Display), - size_of::() - ); - } - - #[test] - 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(&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::::dangling().as_ptr() as *const dyn std::fmt::Display), - align_of::() - ); - } - - #[test] - pub fn test_empty_slice() { - let slice_ptr = Vec::::new().as_mut_slice() as *mut [char]; - assert!(can_write(slice_ptr)); - } - - #[test] - pub fn test_empty_str() { - let slice_ptr = String::new().as_mut_str() as *mut str; - assert!(can_write(slice_ptr)); - } - - #[test] - fn test_dangling_zst() { - test_dangling_of_zst::<()>(); - test_dangling_of_zst::<[(); 10]>(); - } - - fn test_dangling_of_zst() { - let dangling: *mut T = NonNull::::dangling().as_ptr(); - assert!(can_write(dangling)); - - let vec_ptr = Vec::::new().as_mut_ptr(); - assert!(can_write(vec_ptr)); - } - - #[test] - fn test_null_fat_ptr() { - assert!(!can_dereference(ptr::null::() as *const dyn Debug)); - } - - #[test] - fn test_null_char() { - assert!(!can_dereference(ptr::null::())); - } - - #[test] - fn test_null_mut() { - assert!(!can_write(ptr::null_mut::())); - } -} diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index ec12209f0e08..5388dcfb9427 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -10,7 +10,7 @@ publish = false description = "Define core constructs to use with Kani" [dependencies] -kani_macros = { path = "../kani_macros", features = ["no_core"] } +kani_macros = { path = "../kani_macros"} [features] no_core=["kani_macros/no_core"] diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index b7263816800a..6cbe98d30df2 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -52,6 +52,10 @@ macro_rules! kani_lib { pub use kani_core::*; kani_core::kani_intrinsics!(std); kani_core::generate_arbitrary!(std); + + pub mod mem { + kani_core::kani_mem!(std); + } }; } @@ -298,6 +302,7 @@ macro_rules! kani_intrinsics { loop {} } + #[doc(hidden)] pub mod internal { use crate::kani::Arbitrary; use core::ptr; diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 0b029ad53089..34cff4b17ad7 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -36,6 +36,7 @@ //! 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. +#[allow(clippy::crate_in_macro_def)] #[macro_export] macro_rules! kani_mem { ($core:tt) => { @@ -56,12 +57,11 @@ macro_rules! kani_mem { /// 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 for more details. - // TODO: Add this back! We might need to rename the attribute. - //#[crate::unstable( - // feature = "mem-predicates", - // issue = 2690, - // reason = "experimental memory predicate API" - //)] + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] pub fn can_write(ptr: *mut T) -> bool where T: ?Sized, @@ -84,12 +84,11 @@ macro_rules! kani_mem { /// 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 for more details. - // TODO: Add this back! We might need to rename the attribute. - //#[crate::unstable( - // feature = "mem-predicates", - // issue = 2690, - // reason = "experimental memory predicate API" - //)] + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] pub fn can_write_unaligned(ptr: *const T) -> bool where T: ?Sized, @@ -111,11 +110,11 @@ macro_rules! kani_mem { /// 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 for more details. - //#[crate::unstable( - // feature = "mem-predicates", - // issue = 2690, - // reason = "experimental memory predicate API" - //)] + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] #[allow(clippy::not_unsafe_ptr_arg_deref)] pub fn can_dereference(ptr: *const T) -> bool where @@ -143,12 +142,11 @@ macro_rules! kani_mem { /// 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 for more details. - // TODO: Add this back! We might need to rename the attribute. - //#[crate::unstable( - // feature = "mem-predicates", - // issue = 2690, - // reason = "experimental memory predicate API" - //)] + #[crate::kani::unstable_feature( + feature = "mem-predicates", + issue = 2690, + reason = "experimental memory predicate API" + )] #[allow(clippy::not_unsafe_ptr_arg_deref)] pub fn can_read_unaligned(ptr: *const T) -> bool where @@ -180,7 +178,7 @@ macro_rules! kani_mem { // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be // stubbed. // We first assert that the data_ptr - assert!( + super::assert( unsafe { is_allocated(data_ptr, 0) }, "Kani does not support reasoning about pointer to unallocated memory", ); @@ -320,30 +318,28 @@ macro_rules! kani_mem { } /// Get the object ID of the given pointer. - // TODO: Add this back later, as there is no unstable attribute here. - // #[doc(hidden)] - // #[crate::unstable( - // feature = "ghost-state", - // issue = 3184, - // reason = "experimental ghost state/shadow memory API" - // )] + #[doc(hidden)] + #[crate::kani::unstable_feature( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" + )] #[rustc_diagnostic_item = "KaniPointerObject"] #[inline(never)] - pub(crate) fn pointer_object(_ptr: *const T) -> usize { + pub fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } /// Get the object offset of the given pointer. - // TODO: Add this back later, as there is no unstable attribute here. - // #[doc(hidden)] - // #[crate::unstable( - // feature = "ghost-state", - // issue = 3184, - // reason = "experimental ghost state/shadow memory API" - // )] + #[doc(hidden)] + #[crate::kani::unstable_feature( + feature = "ghost-state", + issue = 3184, + reason = "experimental ghost state/shadow memory API" + )] #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] - pub(crate) fn pointer_offset(_ptr: *const T) -> usize { + pub fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } }; diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index 5917c322729e..42eb37a56584 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -22,4 +22,4 @@ syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-tra rustc_private = true [features] -no_core = [] \ No newline at end of file +no_core = [] diff --git a/tests/expected/function-contract/modifies/check_invalid_modifies.expected b/tests/expected/function-contract/modifies/check_invalid_modifies.expected index 660430705aa2..c0ce839c3aae 100644 --- a/tests/expected/function-contract/modifies/check_invalid_modifies.expected +++ b/tests/expected/function-contract/modifies/check_invalid_modifies.expected @@ -1,7 +1,2 @@ -error: `&str` doesn't implement `kani::Arbitrary`\ - -->\ -| -| T::any() -| ^^^^^^^^ -| +error: `&str` doesn't implement `kani::Arbitrary`. = help: All objects in the modifies clause must implement the Arbitrary. The return type must also implement the Arbitrary trait if you are checking recursion or using verified stub. diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected index 1b62781adaaf..4014a0723029 100644 --- a/tests/expected/function-contract/valid_ptr.expected +++ b/tests/expected/function-contract/valid_ptr.expected @@ -1,5 +1,4 @@ Checking harness pre_condition::harness_invalid_ptr... -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... 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 3a24bf15241e..6a95c667b71b 100755 --- a/tests/script-based-pre/verify_std_cmd/verify_std.sh +++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh @@ -51,7 +51,7 @@ 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 +kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing -Z mem-predicates # Cleanup rm -r ${TMP_DIR} diff --git a/tests/ui/derive-arbitrary/non_arbitrary_param/expected b/tests/ui/derive-arbitrary/non_arbitrary_param/expected index 55f12678cf9a..68e3710d6dcb 100644 --- a/tests/ui/derive-arbitrary/non_arbitrary_param/expected +++ b/tests/ui/derive-arbitrary/non_arbitrary_param/expected @@ -1,4 +1,4 @@ error[E0277]: the trait bound `Void: kani::Arbitrary` is not satisfied - |\ -14 | let _wrapper: Wrapper = kani::any();\ - | ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`, which is required by `Wrapper: kani::Arbitrary`\ +|\ +| let _wrapper: Wrapper = kani::any();\ +| ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`, which is required by `Wrapper: kani::Arbitrary`\