From dffe30baa86decbbb6e92aeb568e1baa917d4e68 Mon Sep 17 00:00:00 2001 From: aaluna Date: Fri, 20 Sep 2024 14:38:41 -0400 Subject: [PATCH 01/13] Initial proof/contract/harness for nonzero: Added contract and placeholder harness --- library/core/src/num/nonzero.rs | 35 +++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 8b888f12da0b1..517b3d86746c1 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -8,6 +8,9 @@ use crate::ops::{BitOr, BitOrAssign, Div, DivAssign, Neg, Rem, RemAssign}; use crate::panic::{RefUnwindSafe, UnwindSafe}; use crate::str::FromStr; use crate::{fmt, intrinsics, ptr, ub_checks}; +use safety::{ensures, requires}; +#[cfg(kani)] +use crate::kani; /// A marker trait for primitive types which can be zero. /// @@ -348,6 +351,7 @@ where #[rustc_const_stable(feature = "const_nonzero_int_methods", since = "1.47.0")] #[must_use] #[inline] + pub const fn new(n: T) -> Option { // SAFETY: Memory layout optimization guarantees that `Option>` has // the same layout and size as `T`, with `0` representing `None`. @@ -364,6 +368,8 @@ where #[rustc_const_stable(feature = "nonzero", since = "1.28.0")] #[must_use] #[inline] + #[requires(n != T::zero())] + #[ensures(|result: Self| result.get() == n)] pub const unsafe fn new_unchecked(n: T) -> Self { match Self::new(n) { Some(n) => n, @@ -381,6 +387,10 @@ where } } + + + + /// Converts a reference to a non-zero mutable reference /// if the referenced value is not zero. #[unstable(feature = "nonzero_from_mut", issue = "106290")] @@ -442,6 +452,9 @@ where } } + + + macro_rules! nonzero_integer { ( #[$stability:meta] @@ -2171,3 +2184,25 @@ nonzero_integer! { swapped = "0x5634129078563412", reversed = "0x6a2c48091e6a2c48", } + +#[unstable(feature="kani", issue="none")] +#[cfg(kani)] + mod verify { + use core::num::NonZeroI32; // Use core::num instead of std::num + use super::*; + use NonZero; + + +// pub const unsafe fn newunchecked(n: T) -> Self +#[kani::proof_for_contract(NonZero::new_unchecked)] +fn nonzero_check_new_unchecked() { + let x: i32 = kani::any(); // Generates a symbolic value of type i32 + + // Only proceed if x is not zero, because passing zero would violate the precondition + kani::assume(x != 0); + + unsafe { + let _ = NonZeroI32::new_unchecked(x); // Calls NonZero::new_unchecked + } + } +} From daf157631b2bd5493fcb3b34901af92a43a722df Mon Sep 17 00:00:00 2001 From: SahithiMV Date: Sun, 6 Oct 2024 21:47:51 +0000 Subject: [PATCH 02/13] Bytewise comparision (new_unchecked contract) --- library/core/src/num/nonzero.rs | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 517b3d86746c1..2eff437b9e717 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -368,8 +368,23 @@ where #[rustc_const_stable(feature = "nonzero", since = "1.28.0")] #[must_use] #[inline] - #[requires(n != T::zero())] - #[ensures(|result: Self| result.get() == n)] + #[rustc_allow_const_fn_unstable(const_refs_to_cell)] + #[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) + })] + #[ensures(|result: &Self|{ + let size = core::mem::size_of::(); + let n_ptr: *const T = &n; + let result_inner: T = result.get(); + let result_ptr: *const T = &result_inner; + let n_slice = unsafe { core::slice::from_raw_parts(n_ptr as *const u8, size) }; + let result_slice = unsafe { core::slice::from_raw_parts(result_ptr as *const u8, size) }; + + n_slice == result_slice + })] pub const unsafe fn new_unchecked(n: T) -> Self { match Self::new(n) { Some(n) => n, From 21ae29ed22a257b6038cc8b088cc874c49b38adc Mon Sep 17 00:00:00 2001 From: aaluna Date: Tue, 8 Oct 2024 19:40:26 -0400 Subject: [PATCH 03/13] Removed kani assumes removed from proof_for_contract --- library/core/src/num/nonzero.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 2eff437b9e717..9774d500c719a 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2213,9 +2213,6 @@ nonzero_integer! { fn nonzero_check_new_unchecked() { let x: i32 = kani::any(); // Generates a symbolic value of type i32 - // Only proceed if x is not zero, because passing zero would violate the precondition - kani::assume(x != 0); - unsafe { let _ = NonZeroI32::new_unchecked(x); // Calls NonZero::new_unchecked } From 4241687f9f7230f1afa3d813d87aecf939572f0c Mon Sep 17 00:00:00 2001 From: SahithiMV Date: Sun, 13 Oct 2024 20:23:50 +0000 Subject: [PATCH 04/13] Macros for data types --- library/Cargo.lock | 86 +++++++++++++++++++++++++++++++++ library/core/Cargo.toml | 1 + library/core/src/num/nonzero.rs | 40 +++++++++++---- 3 files changed, 117 insertions(+), 10 deletions(-) diff --git a/library/Cargo.lock b/library/Cargo.lock index 54ad052c52322..695e3c4bcb306 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -72,6 +72,7 @@ version = "0.0.0" dependencies = [ "rand", "rand_xorshift", + "safety", ] [[package]] @@ -219,6 +220,39 @@ dependencies = [ "unwind", ] +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn 1.0.109", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.86" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" +dependencies = [ + "unicode-ident", +] + [[package]] name = "proc_macro" version = "0.0.0" @@ -236,6 +270,15 @@ dependencies = [ "core", ] +[[package]] +name = "quote" +version = "1.0.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" +dependencies = [ + "proc-macro2", +] + [[package]] name = "r-efi" version = "4.5.0" @@ -312,6 +355,16 @@ dependencies = [ "std", ] +[[package]] +name = "safety" +version = "0.1.0" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.79", +] + [[package]] name = "std" version = "0.0.0" @@ -353,6 +406,27 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "2.0.79" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "sysroot" version = "0.0.0" @@ -372,6 +446,12 @@ dependencies = [ "std", ] +[[package]] +name = "unicode-ident" +version = "1.0.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" + [[package]] name = "unicode-width" version = "0.1.13" @@ -405,6 +485,12 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "version_check" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" + [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml index 9121227bc2615..ca54c5ecc7b91 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -26,6 +26,7 @@ test = true [dependencies] safety = {path = "../contracts/safety" } +paste = "1.0" [dev-dependencies] rand = { version = "0.8.5", default-features = false } diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 9774d500c719a..cac0810b5c9d0 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -11,6 +11,7 @@ use crate::{fmt, intrinsics, ptr, ub_checks}; use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; +use paste::paste; /// A marker trait for primitive types which can be zero. /// @@ -2207,14 +2208,33 @@ nonzero_integer! { use super::*; use NonZero; - -// pub const unsafe fn newunchecked(n: T) -> Self -#[kani::proof_for_contract(NonZero::new_unchecked)] -fn nonzero_check_new_unchecked() { - let x: i32 = kani::any(); // Generates a symbolic value of type i32 - - unsafe { - let _ = NonZeroI32::new_unchecked(x); // Calls NonZero::new_unchecked - } + macro_rules! nonzero_check { + ($t:ty, $nonzero_type:ty) => { + paste! { + #[kani::proof_for_contract(NonZero::new_unchecked)] + pub fn []() { + let x: $t = kani::any(); // Generates a symbolic value of the provided type + + // Only proceed if x is not zero, because passing zero would violate the precondition + kani::assume(x != 0); + + unsafe { + let _ = <$nonzero_type>::new_unchecked(x); // Calls NonZero::new_unchecked for the specified NonZero type + } + } + } + }; } -} + + // Use the macro to generate different versions of the function for multiple types + nonzero_check!(i8, core::num::NonZeroI8); + nonzero_check!(i16, core::num::NonZeroI16); + nonzero_check!(i64, core::num::NonZeroI64); + nonzero_check!(i128, core::num::NonZeroI128); + nonzero_check!(u8, core::num::NonZeroU8); + nonzero_check!(u16, core::num::NonZeroU16); + nonzero_check!(u32, core::num::NonZeroU32); + nonzero_check!(u64, core::num::NonZeroU64); + nonzero_check!(u128, core::num::NonZeroU128); + nonzero_check!(usize, core::num::NonZeroUsize); +} \ No newline at end of file From 801f9a49f42ebe4b3edbf0356f6f883838d24611 Mon Sep 17 00:00:00 2001 From: SahithiMV Date: Sun, 13 Oct 2024 20:37:29 +0000 Subject: [PATCH 05/13] Adding i32 and isize --- library/core/src/num/nonzero.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index cac0810b5c9d0..9a8770cb4f2c8 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2229,6 +2229,7 @@ nonzero_integer! { // Use the macro to generate different versions of the function for multiple types nonzero_check!(i8, core::num::NonZeroI8); nonzero_check!(i16, core::num::NonZeroI16); + nonzero_check!(i32, core::num::NonZeroI32); nonzero_check!(i64, core::num::NonZeroI64); nonzero_check!(i128, core::num::NonZeroI128); nonzero_check!(u8, core::num::NonZeroU8); @@ -2237,4 +2238,5 @@ nonzero_integer! { nonzero_check!(u64, core::num::NonZeroU64); nonzero_check!(u128, core::num::NonZeroU128); nonzero_check!(usize, core::num::NonZeroUsize); + nonzero_check!(isize, core::num::NonZeroIsize); } \ No newline at end of file From eafef0b2b3d41e3e6c97ff1871e3215f8f20d905 Mon Sep 17 00:00:00 2001 From: aaluna Date: Sun, 20 Oct 2024 16:12:09 -0400 Subject: [PATCH 06/13] Pull Request fixes Corrected issues from Pull Request --- library/core/src/num/nonzero.rs | 49 +++++++++++++-------------------- 1 file changed, 19 insertions(+), 30 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 9a8770cb4f2c8..f8df437ae3fcc 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -11,8 +11,6 @@ use crate::{fmt, intrinsics, ptr, ub_checks}; use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; -use paste::paste; - /// A marker trait for primitive types which can be zero. /// /// This is an implementation detail for [NonZero]\ which may disappear or be replaced at any time. @@ -403,10 +401,6 @@ where } } - - - - /// Converts a reference to a non-zero mutable reference /// if the referenced value is not zero. #[unstable(feature = "nonzero_from_mut", issue = "106290")] @@ -2209,34 +2203,29 @@ nonzero_integer! { use NonZero; macro_rules! nonzero_check { - ($t:ty, $nonzero_type:ty) => { - paste! { - #[kani::proof_for_contract(NonZero::new_unchecked)] - pub fn []() { - let x: $t = kani::any(); // Generates a symbolic value of the provided type - - // Only proceed if x is not zero, because passing zero would violate the precondition - kani::assume(x != 0); - - unsafe { - let _ = <$nonzero_type>::new_unchecked(x); // Calls NonZero::new_unchecked for the specified NonZero type - } + ($t:ty, $nonzero_type:ty, $nonzero_check_new_unchecked_for:ident) => { + #[kani::proof_for_contract(NonZero::new_unchecked)] + pub fn $nonzero_check_new_unchecked_for() { + let x: $t = kani::any(); // Generates a symbolic value of the provided type + + unsafe { + <$nonzero_type>::new_unchecked(x); // Calls NonZero::new_unchecked for the specified NonZero type } } }; } // Use the macro to generate different versions of the function for multiple types - nonzero_check!(i8, core::num::NonZeroI8); - nonzero_check!(i16, core::num::NonZeroI16); - nonzero_check!(i32, core::num::NonZeroI32); - nonzero_check!(i64, core::num::NonZeroI64); - nonzero_check!(i128, core::num::NonZeroI128); - nonzero_check!(u8, core::num::NonZeroU8); - nonzero_check!(u16, core::num::NonZeroU16); - nonzero_check!(u32, core::num::NonZeroU32); - nonzero_check!(u64, core::num::NonZeroU64); - nonzero_check!(u128, core::num::NonZeroU128); - nonzero_check!(usize, core::num::NonZeroUsize); - nonzero_check!(isize, core::num::NonZeroIsize); + nonzero_check!(i8, core::num::NonZeroI8, nonzero_check_new_unchecked_for_i8); + nonzero_check!(i16, core::num::NonZeroI16, nonzero_check_new_unchecked_for_16); + nonzero_check!(i32, core::num::NonZeroI32, nonzero_check_new_unchecked_for_32); + nonzero_check!(i64, core::num::NonZeroI64, nonzero_check_new_unchecked_for_64); + nonzero_check!(i128, core::num::NonZeroI128, nonzero_check_new_unchecked_for_128); + nonzero_check!(isize, core::num::NonZeroIsize, nonzero_check_new_unchecked_for_isize); + nonzero_check!(u8, core::num::NonZeroU8, nonzero_check_new_unchecked_for_u8); + nonzero_check!(u16, core::num::NonZeroU16, nonzero_check_new_unchecked_for_u16); + nonzero_check!(u32, core::num::NonZeroU32, nonzero_check_new_unchecked_for_u32); + nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); + nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); + nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); } \ No newline at end of file From 3015febb3d8112a63d4eb672d0967737b63fa2ba Mon Sep 17 00:00:00 2001 From: aaluna Date: Mon, 21 Oct 2024 15:34:43 -0400 Subject: [PATCH 07/13] Pull Request fixes Restored previous cargo files --- library/Cargo.lock | 86 ----------------------------------------- library/core/Cargo.toml | 1 - 2 files changed, 87 deletions(-) diff --git a/library/Cargo.lock b/library/Cargo.lock index 695e3c4bcb306..54ad052c52322 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -72,7 +72,6 @@ version = "0.0.0" dependencies = [ "rand", "rand_xorshift", - "safety", ] [[package]] @@ -220,39 +219,6 @@ dependencies = [ "unwind", ] -[[package]] -name = "proc-macro-error" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" -dependencies = [ - "proc-macro-error-attr", - "proc-macro2", - "quote", - "syn 1.0.109", - "version_check", -] - -[[package]] -name = "proc-macro-error-attr" -version = "1.0.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" -dependencies = [ - "proc-macro2", - "quote", - "version_check", -] - -[[package]] -name = "proc-macro2" -version = "1.0.86" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77" -dependencies = [ - "unicode-ident", -] - [[package]] name = "proc_macro" version = "0.0.0" @@ -270,15 +236,6 @@ dependencies = [ "core", ] -[[package]] -name = "quote" -version = "1.0.37" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" -dependencies = [ - "proc-macro2", -] - [[package]] name = "r-efi" version = "4.5.0" @@ -355,16 +312,6 @@ dependencies = [ "std", ] -[[package]] -name = "safety" -version = "0.1.0" -dependencies = [ - "proc-macro-error", - "proc-macro2", - "quote", - "syn 2.0.79", -] - [[package]] name = "std" version = "0.0.0" @@ -406,27 +353,6 @@ dependencies = [ "rustc-std-workspace-core", ] -[[package]] -name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "unicode-ident", -] - -[[package]] -name = "syn" -version = "2.0.79" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - [[package]] name = "sysroot" version = "0.0.0" @@ -446,12 +372,6 @@ dependencies = [ "std", ] -[[package]] -name = "unicode-ident" -version = "1.0.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" - [[package]] name = "unicode-width" version = "0.1.13" @@ -485,12 +405,6 @@ dependencies = [ "rustc-std-workspace-core", ] -[[package]] -name = "version_check" -version = "0.9.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" - [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml index ca54c5ecc7b91..9121227bc2615 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -26,7 +26,6 @@ test = true [dependencies] safety = {path = "../contracts/safety" } -paste = "1.0" [dev-dependencies] rand = { version = "0.8.5", default-features = false } From ce918f8c01a5ed5bb808f78fe312a1c727120003 Mon Sep 17 00:00:00 2001 From: aaluna <166172412+MooniniteErr@users.noreply.github.com> Date: Sun, 27 Oct 2024 14:07:39 -0400 Subject: [PATCH 08/13] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index f8df437ae3fcc..47ab5a4847ec7 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -350,7 +350,6 @@ where #[rustc_const_stable(feature = "const_nonzero_int_methods", since = "1.47.0")] #[must_use] #[inline] - pub const fn new(n: T) -> Option { // SAFETY: Memory layout optimization guarantees that `Option>` has // the same layout and size as `T`, with `0` representing `None`. From 2304fadd45688c77a556fcc9db52264e3f66a37b Mon Sep 17 00:00:00 2001 From: aaluna <166172412+MooniniteErr@users.noreply.github.com> Date: Sun, 27 Oct 2024 14:12:13 -0400 Subject: [PATCH 09/13] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 47ab5a4847ec7..77eb453489749 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -461,9 +461,6 @@ where } } - - - macro_rules! nonzero_integer { ( #[$stability:meta] From 14a50e2357878ea2ce1e45db06715b5bc2f5ee57 Mon Sep 17 00:00:00 2001 From: aa-luna Date: Sun, 27 Oct 2024 14:13:31 -0400 Subject: [PATCH 10/13] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- library/core/src/num/nonzero.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 77eb453489749..eeaf8dc86ea39 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2194,9 +2194,7 @@ nonzero_integer! { #[unstable(feature="kani", issue="none")] #[cfg(kani)] mod verify { - use core::num::NonZeroI32; // Use core::num instead of std::num - use super::*; - use NonZero; + use super::*; macro_rules! nonzero_check { ($t:ty, $nonzero_type:ty, $nonzero_check_new_unchecked_for:ident) => { From acef65adac0658bbe404f82f89003bea43211d7b Mon Sep 17 00:00:00 2001 From: aa-luna Date: Sun, 27 Oct 2024 14:13:39 -0400 Subject: [PATCH 11/13] Update library/core/src/num/nonzero.rs Co-authored-by: Carolyn Zech --- 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 eeaf8dc86ea39..a9facd0c62997 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2222,4 +2222,4 @@ nonzero_integer! { nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); -} \ No newline at end of file +} From 4d3efd16f6e03a3dbeeba497ebf6b6c843dc5168 Mon Sep 17 00:00:00 2001 From: aa-luna Date: Sun, 27 Oct 2024 14:15:07 -0400 Subject: [PATCH 12/13] Update library/core/src/num/nonzero.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- 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 a9facd0c62997..28bc0e0752b72 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2193,7 +2193,7 @@ nonzero_integer! { #[unstable(feature="kani", issue="none")] #[cfg(kani)] - mod verify { +mod verify { use super::*; macro_rules! nonzero_check { From 7bc64eb68b36682d3e1e7dd4821a23a5a7a1ee50 Mon Sep 17 00:00:00 2001 From: aaluna Date: Sun, 3 Nov 2024 11:46:41 -0500 Subject: [PATCH 13/13] doc: add explanations for const function attribute --- library/core/src/num/nonzero.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 28bc0e0752b72..97964e8c86973 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -366,6 +366,10 @@ where #[rustc_const_stable(feature = "nonzero", since = "1.28.0")] #[must_use] #[inline] + // #[rustc_allow_const_fn_unstable(const_refs_to_cell)] enables byte-level + // comparisons within const functions. This is needed here to validate the + // contents of `T` by converting a pointer to a `u8` slice for our `requires` + // and `ensures` checks. #[rustc_allow_const_fn_unstable(const_refs_to_cell)] #[requires({ let size = core::mem::size_of::();