From 196da1247066f917c8d2902c7e9e9f8f698d2386 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Apr 2025 21:06:21 +0000 Subject: [PATCH 1/3] Add contracts for NonZero::from_mut_unchecked This PR should serve as a basis for discussion: I'm not sure how to refer to a parameter that is a mutable reference, and I don't know whether that is just a lack of Rust skills on my part or a fundamental Kani limitation. --- library/core/src/num/nonzero.rs | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 83ebd7fbe1922..f7c1694bbcf7a 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -452,6 +452,12 @@ where #[unstable(feature = "nonzero_from_mut", issue = "106290")] #[must_use] #[inline] + #[requires({ + let size = core::mem::size_of::(); + let ptr = n as *const T as *const u8; + let slice = unsafe { core::slice::from_raw_parts(ptr, size) }; + !slice.iter().all(|&byte| byte == 0) + })] pub unsafe fn from_mut_unchecked(n: &mut T) -> &mut Self { match Self::from_mut(n) { Some(n) => n, @@ -2415,6 +2421,32 @@ mod verify { nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); + macro_rules! nonzero_check_from_mut_unchecked { + ($t:ty, $nonzero_type:ty, $harness_name:ident) => { + #[kani::proof_for_contract(::from_mut_unchecked)] + pub fn $harness_name() { + let mut x: $t = kani::any(); + unsafe { + <$nonzero_type>::from_mut_unchecked(&mut x); + } + } + }; + } + + // Generate harnesses for multiple types + nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8); + nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16); + nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32); + nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64); + nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128); + nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize); + nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8); + nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16); + nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32); + nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64); + nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128); + nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize); + macro_rules! nonzero_check_cmp { ($nonzero_type:ty, $nonzero_check_cmp_for:ident) => { #[kani::proof] From 363984bd0e512b3d74be062c58e67cba4274da8c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 10 Jul 2025 16:20:47 +0000 Subject: [PATCH 2/3] Fix lookup --- library/core/src/num/nonzero.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 70358a6675a27..d1d05c9626d60 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2403,7 +2403,7 @@ mod verify { macro_rules! nonzero_check_from_mut_unchecked { ($t:ty, $nonzero_type:ty, $harness_name:ident) => { - #[kani::proof_for_contract(::from_mut_unchecked)] + #[kani::proof_for_contract(NonZero::<$t>::from_mut_unchecked)] pub fn $harness_name() { let mut x: $t = kani::any(); unsafe { From 3f6b2e1ed5ce85e5df46933b30e3243bc467df5e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 10 Jul 2025 16:33:40 +0000 Subject: [PATCH 3/3] Fmt --- library/core/src/num/nonzero.rs | 72 +++++++++++++++++++++++++++------ 1 file changed, 60 insertions(+), 12 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index d1d05c9626d60..e557161525152 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2414,18 +2414,66 @@ mod verify { } // Generate harnesses for multiple types - nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8); - nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16); - nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32); - nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64); - nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128); - nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize); - nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8); - nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16); - nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32); - nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64); - nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128); - nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize); + nonzero_check_from_mut_unchecked!( + i8, + core::num::NonZeroI8, + nonzero_check_from_mut_unchecked_i8 + ); + nonzero_check_from_mut_unchecked!( + i16, + core::num::NonZeroI16, + nonzero_check_from_mut_unchecked_i16 + ); + nonzero_check_from_mut_unchecked!( + i32, + core::num::NonZeroI32, + nonzero_check_from_mut_unchecked_i32 + ); + nonzero_check_from_mut_unchecked!( + i64, + core::num::NonZeroI64, + nonzero_check_from_mut_unchecked_i64 + ); + nonzero_check_from_mut_unchecked!( + i128, + core::num::NonZeroI128, + nonzero_check_from_mut_unchecked_i128 + ); + nonzero_check_from_mut_unchecked!( + isize, + core::num::NonZeroIsize, + nonzero_check_from_mut_unchecked_isize + ); + nonzero_check_from_mut_unchecked!( + u8, + core::num::NonZeroU8, + nonzero_check_from_mut_unchecked_u8 + ); + nonzero_check_from_mut_unchecked!( + u16, + core::num::NonZeroU16, + nonzero_check_from_mut_unchecked_u16 + ); + nonzero_check_from_mut_unchecked!( + u32, + core::num::NonZeroU32, + nonzero_check_from_mut_unchecked_u32 + ); + nonzero_check_from_mut_unchecked!( + u64, + core::num::NonZeroU64, + nonzero_check_from_mut_unchecked_u64 + ); + nonzero_check_from_mut_unchecked!( + u128, + core::num::NonZeroU128, + nonzero_check_from_mut_unchecked_u128 + ); + nonzero_check_from_mut_unchecked!( + usize, + core::num::NonZeroUsize, + nonzero_check_from_mut_unchecked_usize + ); macro_rules! nonzero_check_cmp { ($nonzero_type:ty, $nonzero_check_cmp_for:ident) => {