From ff9a1000b9d8dade9f0ce2c561e6a87870eeba8f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 18 Jun 2025 12:10:28 +0000 Subject: [PATCH 1/5] Upgrade Rust toolchain to 2025-06-17 (#4163) Relevant upstream PR: https://github.com/rust-lang/rust/pull/137944 (Sized Hierarchy: Part I). This PR implements a part of [RFC 3729](https://github.com/rust-lang/rfcs/pull/3729), which prescribes a hierarchy of `Sized` traits. Notably, this disallows instantiation of `size_of_val` and `align_of_val` with extern types. Consequently, the code in test `unsized_foreign.rs` no longer compiles instead of panicking, as it previously did. This test is therefore removed. Work in progress: figure out whether we can make `foreign_type.rs` work. Resolves: #4165 --- rust-toolchain.toml | 2 +- ...{foreign_type.rs => fixme_foreign_type.rs} | 0 .../kani/SizeAndAlignOfDst/unsized_foreign.rs | 48 ------------------- 3 files changed, 1 insertion(+), 49 deletions(-) rename tests/kani/MemPredicates/{foreign_type.rs => fixme_foreign_type.rs} (100%) delete mode 100644 tests/kani/SizeAndAlignOfDst/unsized_foreign.rs 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/fixme_foreign_type.rs similarity index 100% rename from tests/kani/MemPredicates/foreign_type.rs rename to tests/kani/MemPredicates/fixme_foreign_type.rs 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); -} From 1980ac0d006405fa2dee4c8f4208ed62da8cd181 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 18 Jun 2025 17:19:26 +0000 Subject: [PATCH 2/5] Try what the RFC suggests --- library/kani/src/lib.rs | 1 + library/kani_core/src/mem.rs | 31 ++++++++++--------- ...{fixme_foreign_type.rs => foreign_type.rs} | 4 ++- 3 files changed, 20 insertions(+), 16 deletions(-) rename tests/kani/MemPredicates/{fixme_foreign_type.rs => foreign_type.rs} (95%) 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..f8a2316612fc 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -13,6 +13,7 @@ macro_rules! kani_mem { ($core:tt) => { use super::kani_intrinsic; use $core::ptr::{DynMetadata, NonNull, Pointee}; + use $core::marker::MetaSized; /// Check if the pointer is valid for write access according to [crate::mem] conditions 1, 2 /// and 3. @@ -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,12 @@ 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 +136,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 +154,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 +181,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 +204,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 +238,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 +278,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 +291,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/tests/kani/MemPredicates/fixme_foreign_type.rs b/tests/kani/MemPredicates/foreign_type.rs similarity index 95% rename from tests/kani/MemPredicates/fixme_foreign_type.rs rename to tests/kani/MemPredicates/foreign_type.rs index 52e525c62b33..08dbfaab4eb5 100644 --- a/tests/kani/MemPredicates/fixme_foreign_type.rs +++ b/tests/kani/MemPredicates/foreign_type.rs @@ -5,15 +5,17 @@ //! types since it cannot compute its size. #![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, } From 8902a9c052afcdeb9876e1693a8a6f267637053b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Jun 2025 10:30:48 +0000 Subject: [PATCH 3/5] Remove test that can no longer be expected to compile, fmt --- library/kani_core/src/mem.rs | 7 ++- tests/kani/MemPredicates/foreign_type.rs | 79 ------------------------ 2 files changed, 5 insertions(+), 81 deletions(-) delete mode 100644 tests/kani/MemPredicates/foreign_type.rs diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index f8a2316612fc..a5d03cdcca63 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -12,8 +12,8 @@ macro_rules! kani_mem { ($core:tt) => { use super::kani_intrinsic; - use $core::ptr::{DynMetadata, NonNull, Pointee}; 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 /// and 3. @@ -122,7 +122,10 @@ macro_rules! kani_mem { } #[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) diff --git a/tests/kani/MemPredicates/foreign_type.rs b/tests/kani/MemPredicates/foreign_type.rs deleted file mode 100644 index 08dbfaab4eb5..000000000000 --- a/tests/kani/MemPredicates/foreign_type.rs +++ /dev/null @@ -1,79 +0,0 @@ -// 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. -#![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 { - _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. -#[kani::proof] -pub fn check_write_with_extern() { - let mut var = 0usize; - let ptr = &mut var as *mut _ as *mut __CPROVER_size_t; - unsafe { - __CPROVER_havoc_object(ptr as *mut c_void); - }; -} - -/// 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, and -/// any side effect will be taken into consideration in the verification. -#[kani::proof] -#[kani::should_panic] -pub fn check_write_with_extern_side_effect() { - let mut var = 0usize; - let ptr = &mut var as *mut _ as *mut __CPROVER_size_t; - unsafe { - __CPROVER_havoc_object(ptr as *mut c_void); - }; - 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)); -} From a00da58647bfc711cf85b30dbcc06e00b261c30a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Jun 2025 08:29:03 +0000 Subject: [PATCH 4/5] Revert "Remove test that can no longer be expected to compile, fmt" This reverts commit 8902a9c052afcdeb9876e1693a8a6f267637053b. --- tests/kani/MemPredicates/foreign_type.rs | 79 ++++++++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 tests/kani/MemPredicates/foreign_type.rs diff --git a/tests/kani/MemPredicates/foreign_type.rs b/tests/kani/MemPredicates/foreign_type.rs new file mode 100644 index 000000000000..08dbfaab4eb5 --- /dev/null +++ b/tests/kani/MemPredicates/foreign_type.rs @@ -0,0 +1,79 @@ +// 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. +#![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 { + _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. +#[kani::proof] +pub fn check_write_with_extern() { + let mut var = 0usize; + let ptr = &mut var as *mut _ as *mut __CPROVER_size_t; + unsafe { + __CPROVER_havoc_object(ptr as *mut c_void); + }; +} + +/// 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, and +/// any side effect will be taken into consideration in the verification. +#[kani::proof] +#[kani::should_panic] +pub fn check_write_with_extern_side_effect() { + let mut var = 0usize; + let ptr = &mut var as *mut _ as *mut __CPROVER_size_t; + unsafe { + __CPROVER_havoc_object(ptr as *mut c_void); + }; + 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)); +} From 8f29b1be46ff7d8ec47e940af8f1ee72c21263c6 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Jun 2025 08:37:06 +0000 Subject: [PATCH 5/5] Reduce test to viable subset --- tests/kani/MemPredicates/foreign_type.rs | 35 ++++-------------------- 1 file changed, 5 insertions(+), 30 deletions(-) diff --git a/tests/kani/MemPredicates/foreign_type.rs b/tests/kani/MemPredicates/foreign_type.rs index 08dbfaab4eb5..e81b8252e815 100644 --- a/tests/kani/MemPredicates/foreign_type.rs +++ b/tests/kani/MemPredicates/foreign_type.rs @@ -1,17 +1,17 @@ // 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)] @@ -21,27 +21,11 @@ struct Wrapper { } 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. @@ -68,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)); -}