diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 7c7a6a756917..deb53c470021 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -21,6 +21,7 @@ #![feature(f16)] #![feature(f128)] #![feature(convert_float_to_int)] +#![feature(sized_hierarchy)] // Allow us to use `kani::` to access crate features. extern crate self as kani; diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 91148fac5cc5..a5d03cdcca63 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -12,6 +12,7 @@ macro_rules! kani_mem { ($core:tt) => { use super::kani_intrinsic; + use $core::marker::MetaSized; use $core::ptr::{DynMetadata, NonNull, Pointee}; /// Check if the pointer is valid for write access according to [crate::mem] conditions 1, 2 @@ -31,7 +32,7 @@ macro_rules! kani_mem { issue = 2690, reason = "experimental memory predicate API" )] - pub fn can_write(ptr: *mut T) -> bool { + pub fn can_write(ptr: *mut T) -> bool { is_ptr_aligned(ptr) && is_inbounds(ptr) } @@ -49,7 +50,7 @@ macro_rules! kani_mem { issue = 2690, reason = "experimental memory predicate API" )] - pub fn can_write_unaligned(ptr: *const T) -> bool { + pub fn can_write_unaligned(ptr: *const T) -> bool { let (thin_ptr, metadata) = ptr.to_raw_parts(); is_inbounds(ptr) } @@ -72,7 +73,7 @@ macro_rules! kani_mem { reason = "experimental memory predicate API" )] #[allow(clippy::not_unsafe_ptr_arg_deref)] - pub fn can_dereference(ptr: *const T) -> bool { + pub fn can_dereference(ptr: *const T) -> bool { // 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_ptr_aligned(ptr) @@ -99,7 +100,7 @@ macro_rules! kani_mem { reason = "experimental memory predicate API" )] #[allow(clippy::not_unsafe_ptr_arg_deref)] - pub fn can_read_unaligned(ptr: *const T) -> bool { + pub fn can_read_unaligned(ptr: *const T) -> bool { 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. @@ -116,12 +117,15 @@ macro_rules! kani_mem { reason = "experimental memory predicate API" )] #[allow(clippy::not_unsafe_ptr_arg_deref)] - pub fn same_allocation(ptr1: *const T, ptr2: *const T) -> bool { + pub fn same_allocation(ptr1: *const T, ptr2: *const T) -> bool { same_allocation_internal(ptr1, ptr2) } #[allow(clippy::not_unsafe_ptr_arg_deref)] - pub(super) fn same_allocation_internal(ptr1: *const T, ptr2: *const T) -> bool { + pub(super) fn same_allocation_internal( + ptr1: *const T, + ptr2: *const T, + ) -> bool { let addr1 = ptr1 as *const (); let addr2 = ptr2 as *const (); cbmc::same_allocation(addr1, addr2) @@ -135,7 +139,7 @@ macro_rules! kani_mem { /// - The computed size exceeds `isize::MAX` (the maximum safe Rust allocation size). /// TODO: Optimize this if T is sized. #[kanitool::fn_marker = "CheckedSizeOfIntrinsic"] - pub fn checked_size_of_raw(ptr: *const T) -> Option { + pub fn checked_size_of_raw(ptr: *const T) -> Option { #[cfg(not(feature = "concrete_playback"))] return kani_intrinsic(); @@ -153,7 +157,7 @@ macro_rules! kani_mem { /// Return `None` if alignment information cannot be retrieved (foreign types), or if value /// is not power-of-two. #[kanitool::fn_marker = "CheckedAlignOfIntrinsic"] - pub fn checked_align_of_raw(ptr: *const T) -> Option { + pub fn checked_align_of_raw(ptr: *const T) -> Option { #[cfg(not(feature = "concrete_playback"))] return kani_intrinsic(); @@ -180,7 +184,7 @@ macro_rules! kani_mem { issue = 3946, reason = "experimental memory predicate API" )] - pub fn is_inbounds(ptr: *const T) -> bool { + pub fn is_inbounds(ptr: *const T) -> bool { // If size overflows, then pointer cannot be inbounds. let Some(sz) = checked_size_of_raw(ptr) else { return false }; if sz == 0 { @@ -203,7 +207,7 @@ macro_rules! kani_mem { // Return whether the pointer is aligned #[allow(clippy::manual_is_power_of_two)] - fn is_ptr_aligned(ptr: *const T) -> bool { + fn is_ptr_aligned(ptr: *const T) -> bool { // Cannot be aligned if pointer alignment cannot be computed. let Some(align) = checked_align_of_raw(ptr) else { return false }; if align > 0 && (align & (align - 1)) == 0 { @@ -237,19 +241,19 @@ macro_rules! kani_mem { /// - Users have to ensure that the pointed to memory is allocated. #[kanitool::fn_marker = "ValidValueIntrinsic"] #[inline(never)] - unsafe fn has_valid_value(_ptr: *const T) -> bool { + unsafe fn has_valid_value(_ptr: *const T) -> bool { kani_intrinsic() } /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. #[kanitool::fn_marker = "IsInitializedIntrinsic"] #[inline(never)] - pub(crate) fn is_initialized(_ptr: *const T) -> bool { + 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 { + fn assert_is_initialized(ptr: *const T) -> bool { super::internal::check( is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer", @@ -277,7 +281,7 @@ macro_rules! kani_mem { #[doc(hidden)] #[kanitool::fn_marker = "PointerObjectHook"] #[inline(never)] - pub(crate) fn pointer_object(_ptr: *const T) -> usize { + pub(crate) fn pointer_object(_ptr: *const T) -> usize { kani_intrinsic() } @@ -290,7 +294,7 @@ macro_rules! kani_mem { )] #[kanitool::fn_marker = "PointerOffsetHook"] #[inline(never)] - pub fn pointer_offset(_ptr: *const T) -> usize { + pub fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } }; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index a7a32f1f5cb6..8779bc9606f9 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-06-17" +channel = "nightly-2025-06-18" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/MemPredicates/foreign_type.rs b/tests/kani/MemPredicates/foreign_type.rs index 52e525c62b33..e81b8252e815 100644 --- a/tests/kani/MemPredicates/foreign_type.rs +++ b/tests/kani/MemPredicates/foreign_type.rs @@ -1,45 +1,31 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z mem-predicates -Z c-ffi -//! Check that Kani's memory predicates return that it's not safe to access pointers with foreign -//! types since it cannot compute its size. +// kani-flags: -Z c-ffi +//! We used to check that Kani's memory predicates return that it's not safe to access pointers +//! with foreign types since it cannot compute its size, but with the introduction of +//! sized_hierarchy compilation (expectedly) fails. So all we can check is values through extern +//! types. #![feature(ptr_metadata)] #![feature(extern_types)] +#![feature(sized_hierarchy)] extern crate kani; -use kani::mem::{can_dereference, can_read_unaligned, can_write}; use std::ffi::c_void; -use std::ptr; +use std::marker::PointeeSized; #[derive(Clone, Copy, kani::Arbitrary)] -struct Wrapper { +struct Wrapper { _size: U, _value: T, } extern "C" { - type Foreign; type __CPROVER_size_t; fn __CPROVER_havoc_object(p: *mut c_void); } -#[kani::proof] -pub fn check_write_is_unsafe() { - let mut var: Wrapper = kani::any(); - let ptr: *mut Wrapper = &mut var as *mut _ as *mut _; - assert!(!can_write(ptr)); -} - -#[kani::proof] -pub fn check_read_is_unsafe() { - let var: usize = kani::any(); - let ptr = &var as *const _ as *const __CPROVER_size_t; - assert!(!can_dereference(ptr)); - assert!(!can_read_unaligned(ptr)); -} - /// Kani APIs cannot tell if that's safe to write to a foreign type. /// /// However, foreign APIs that have knowledge of the type can still safely set new values. @@ -66,12 +52,3 @@ pub fn check_write_with_extern_side_effect() { }; assert!(var == 0); } - -/// Check that Kani can still build the foreign type using from_raw_parts. -#[kani::proof] -pub fn check_from_raw_parts() { - let mut var: Wrapper = kani::any(); - let ptr = &mut var as *mut _ as *mut (); - let fat_ptr: *mut __CPROVER_size_t = ptr::from_raw_parts_mut(ptr, ()); - assert!(!can_write(fat_ptr)); -} diff --git a/tests/kani/SizeAndAlignOfDst/unsized_foreign.rs b/tests/kani/SizeAndAlignOfDst/unsized_foreign.rs deleted file mode 100644 index 64cf042969f3..000000000000 --- a/tests/kani/SizeAndAlignOfDst/unsized_foreign.rs +++ /dev/null @@ -1,48 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! Ensure we fail verification if the user tries to compute the size of a foreign item. -//! -//! Although it is currently safe to call `size_of_val` and `align_of_val` on foreign types, -//! the behavior is not well-defined. -//! -//! For now, our implementation will trigger a panic to be on the safe side. -//! -//! From : -//! > an (unstable) extern type, then this function is always safe to call, -//! > but may panic or otherwise return the wrong value, as the extern type’s layout is not known. -//! -// kani-flags: --output-format terse - -#![feature(extern_types, layout_for_ptr)] - -extern "C" { - type ExternalType; -} - -#[kani::proof] -#[kani::should_panic] -fn check_size_of_foreign() { - let tup: (u32, usize) = kani::any(); - assert_eq!(std::mem::size_of_val(&tup), 16); - - let ptr: *const (u32, ExternalType) = &tup as *const _ as *const _; - let _size = unsafe { std::mem::size_of_val_raw(ptr) }; -} - -#[kani::proof] -#[kani::should_panic] -fn check_align_of_foreign() { - let tup: (u32, usize) = kani::any(); - assert_eq!(std::mem::align_of_val(&tup), 8); - - let ptr: *const (u32, ExternalType) = &tup as *const _ as *const _; - let _align = unsafe { std::mem::align_of_val_raw(ptr) }; -} - -#[kani::proof] -fn check_foreign_layout_unknown() { - let tup: (u32, usize) = kani::any(); - let ptr: *const (u32, ExternalType) = &tup as *const _ as *const _; - assert_eq!(kani::mem::checked_align_of_raw(ptr), None); - assert_eq!(kani::mem::checked_size_of_raw(ptr), None); -}