From 1812ba9d265f6f2846b2256b0e329acfe28002ca Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Sun, 1 Dec 2024 16:37:40 -0500 Subject: [PATCH 1/3] max_min --- library/core/src/num/nonzero.rs | 86 +++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index ac7b1fca9fa87..1c85844d64480 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2265,3 +2265,89 @@ 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); } + +#[cfg(kani)] +mod macro_nonzero_check_max { + use super::*; + macro_rules! nonzero_check_max { + ($t:ty, $nonzero_type:ty, $nonzero_check_max_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_max_for() { + let x: $t = kani::any(); + kani::assume(x != 0); + let y: $t = kani::any(); + kani::assume(y != 0); + + unsafe { + let x = <$nonzero_type>::new_unchecked(x); + let y = <$nonzero_type>::new_unchecked(y); + } + + // Use the max function and check the result + let result = x.max(y); + if x > y { + assert!(result == x); + } else { + assert!(result == y); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_max!(i8, core::num::NonZeroI8, nonzero_check_max_for_i8); + nonzero_check_max!(i16, core::num::NonZeroI16, nonzero_check_max_for_16); + nonzero_check_max!(i32, core::num::NonZeroI32, nonzero_check_max_for_32); + nonzero_check_max!(i64, core::num::NonZeroI64, nonzero_check_max_for_64); + nonzero_check_max!(i128, core::num::NonZeroI128, nonzero_check_max_for_128); + nonzero_check_max!(isize, core::num::NonZeroIsize, nonzero_check_max_for_isize); + nonzero_check_max!(u8, core::num::NonZeroU8, nonzero_check_max_for_u8); + nonzero_check_max!(u16, core::num::NonZeroU16, nonzero_check_max_for_u16); + nonzero_check_max!(u32, core::num::NonZeroU32, nonzero_check_max_for_u32); + nonzero_check_max!(u64, core::num::NonZeroU64, nonzero_check_max_for_u64); + nonzero_check_max!(u128, core::num::NonZeroU128, nonzero_check_max_for_u128); + nonzero_check_max!(usize, core::num::NonZeroUsize, nonzero_check_max_for_usize); +} + +#[cfg(kani)] +mod macro_nonzero_check_min { + use super::*; + macro_rules! nonzero_check_min { + ($t:ty, $nonzero_type:ty, $nonzero_check_min_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_min_for() { + let x: $t = kani::any(); + kani::assume(x != 0); + let y: $t = kani::any(); + kani::assume(y != 0); + + unsafe { + let x = <$nonzero_type>::new_unchecked(x); + let y = <$nonzero_type>::new_unchecked(y); + } + + // Use the min function and check the result + let result = x.min(y); + if x < y { + assert!(result == x); + } else { + assert!(result == y); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_min!(i8, core::num::NonZeroI8, nonzero_check_min_for_i8); + nonzero_check_min!(i16, core::num::NonZeroI16, nonzero_check_min_for_16); + nonzero_check_min!(i32, core::num::NonZeroI32, nonzero_check_min_for_32); + nonzero_check_min!(i64, core::num::NonZeroI64, nonzero_check_min_for_64); + nonzero_check_min!(i128, core::num::NonZeroI128, nonzero_check_min_for_128); + nonzero_check_min!(isize, core::num::NonZeroIsize, nonzero_check_min_for_isize); + nonzero_check_min!(u8, core::num::NonZeroU8, nonzero_check_min_for_u8); + nonzero_check_min!(u16, core::num::NonZeroU16, nonzero_check_min_for_u16); + nonzero_check_min!(u32, core::num::NonZeroU32, nonzero_check_min_for_u32); + nonzero_check_min!(u64, core::num::NonZeroU64, nonzero_check_min_for_u64); + nonzero_check_min!(u128, core::num::NonZeroU128, nonzero_check_min_for_u128); + nonzero_check_min!(usize, core::num::NonZeroUsize, nonzero_check_min_for_usize); +} \ No newline at end of file From 2af75f9bfb2eddcca5249813c025e2dfdf188ef6 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 3 Dec 2024 16:56:28 -0500 Subject: [PATCH 2/3] avoid name reused in min and max --- library/core/src/num/nonzero.rs | 58 +++++++++++++++------------------ 1 file changed, 26 insertions(+), 32 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 1c85844d64480..0314fc40494e6 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2273,23 +2273,20 @@ mod macro_nonzero_check_max { ($t:ty, $nonzero_type:ty, $nonzero_check_max_for:ident) => { #[kani::proof] pub fn $nonzero_check_max_for() { - let x: $t = kani::any(); - kani::assume(x != 0); - let y: $t = kani::any(); - kani::assume(y != 0); - + let int_x: $t = kani::any(); + kani::assume(int_x != 0); + let int_y: $t = kani::any(); + kani::assume(int_y != 0); unsafe { - let x = <$nonzero_type>::new_unchecked(x); - let y = <$nonzero_type>::new_unchecked(y); - } - - // Use the max function and check the result - let result = x.max(y); - if x > y { - assert!(result == x); - } else { - assert!(result == y); - } + let x = <$nonzero_type>::new_unchecked(int_x); + let y = <$nonzero_type>::new_unchecked(int_y); + let result = x.max(y); + if x > y { + assert!(result == x); + } else { + assert!(result == y); + } + } } }; } @@ -2316,22 +2313,19 @@ mod macro_nonzero_check_min { ($t:ty, $nonzero_type:ty, $nonzero_check_min_for:ident) => { #[kani::proof] pub fn $nonzero_check_min_for() { - let x: $t = kani::any(); - kani::assume(x != 0); - let y: $t = kani::any(); - kani::assume(y != 0); - + let int_x: $t = kani::any(); + kani::assume(int_x != 0); + let int_y: $t = kani::any(); + kani::assume(int_y != 0); unsafe { - let x = <$nonzero_type>::new_unchecked(x); - let y = <$nonzero_type>::new_unchecked(y); - } - - // Use the min function and check the result - let result = x.min(y); - if x < y { - assert!(result == x); - } else { - assert!(result == y); + let x = <$nonzero_type>::new_unchecked(int_x); + let y = <$nonzero_type>::new_unchecked(int_y); + let result = x.min(y); + if x < y { + assert!(result == x); + } else { + assert!(result == y); + } } } }; @@ -2350,4 +2344,4 @@ mod macro_nonzero_check_min { nonzero_check_min!(u64, core::num::NonZeroU64, nonzero_check_min_for_u64); nonzero_check_min!(u128, core::num::NonZeroU128, nonzero_check_min_for_u128); nonzero_check_min!(usize, core::num::NonZeroUsize, nonzero_check_min_for_usize); -} \ No newline at end of file +} From afc4d5ffec5ee4d4985a5c9bf4828694151f8709 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 3 Dec 2024 21:14:49 -0500 Subject: [PATCH 3/3] avoid use of unsafe code block by generate nonezero from any() directly --- library/core/src/num/nonzero.rs | 96 ++++++++++++++------------------- 1 file changed, 41 insertions(+), 55 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 0314fc40494e6..b607a0350acc5 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2270,78 +2270,64 @@ mod verify { mod macro_nonzero_check_max { use super::*; macro_rules! nonzero_check_max { - ($t:ty, $nonzero_type:ty, $nonzero_check_max_for:ident) => { + ($nonzero_type:ty, $nonzero_check_max_for:ident) => { #[kani::proof] pub fn $nonzero_check_max_for() { - let int_x: $t = kani::any(); - kani::assume(int_x != 0); - let int_y: $t = kani::any(); - kani::assume(int_y != 0); - unsafe { - let x = <$nonzero_type>::new_unchecked(int_x); - let y = <$nonzero_type>::new_unchecked(int_y); - let result = x.max(y); - if x > y { - assert!(result == x); - } else { - assert!(result == y); - } - } + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x.max(y); + if x > y { + assert!(result == x); + } else { + assert!(result == y); + } } }; } - // Use the macro to generate different versions of the function for multiple types - nonzero_check_max!(i8, core::num::NonZeroI8, nonzero_check_max_for_i8); - nonzero_check_max!(i16, core::num::NonZeroI16, nonzero_check_max_for_16); - nonzero_check_max!(i32, core::num::NonZeroI32, nonzero_check_max_for_32); - nonzero_check_max!(i64, core::num::NonZeroI64, nonzero_check_max_for_64); - nonzero_check_max!(i128, core::num::NonZeroI128, nonzero_check_max_for_128); - nonzero_check_max!(isize, core::num::NonZeroIsize, nonzero_check_max_for_isize); - nonzero_check_max!(u8, core::num::NonZeroU8, nonzero_check_max_for_u8); - nonzero_check_max!(u16, core::num::NonZeroU16, nonzero_check_max_for_u16); - nonzero_check_max!(u32, core::num::NonZeroU32, nonzero_check_max_for_u32); - nonzero_check_max!(u64, core::num::NonZeroU64, nonzero_check_max_for_u64); - nonzero_check_max!(u128, core::num::NonZeroU128, nonzero_check_max_for_u128); - nonzero_check_max!(usize, core::num::NonZeroUsize, nonzero_check_max_for_usize); + nonzero_check_max!(core::num::NonZeroI8, nonzero_check_max_for_i8); + nonzero_check_max!(core::num::NonZeroI16, nonzero_check_max_for_i16); + nonzero_check_max!(core::num::NonZeroI32, nonzero_check_max_for_i32); + nonzero_check_max!(core::num::NonZeroI64, nonzero_check_max_for_i64); + nonzero_check_max!(core::num::NonZeroI128, nonzero_check_max_for_i128); + nonzero_check_max!(core::num::NonZeroIsize, nonzero_check_max_for_isize); + nonzero_check_max!(core::num::NonZeroU8, nonzero_check_max_for_u8); + nonzero_check_max!(core::num::NonZeroU16, nonzero_check_max_for_u16); + nonzero_check_max!(core::num::NonZeroU32, nonzero_check_max_for_u32); + nonzero_check_max!(core::num::NonZeroU64, nonzero_check_max_for_u64); + nonzero_check_max!(core::num::NonZeroU128, nonzero_check_max_for_u128); + nonzero_check_max!(core::num::NonZeroUsize, nonzero_check_max_for_usize); } #[cfg(kani)] mod macro_nonzero_check_min { use super::*; macro_rules! nonzero_check_min { - ($t:ty, $nonzero_type:ty, $nonzero_check_min_for:ident) => { + ($nonzero_type:ty, $nonzero_check_min_for:ident) => { #[kani::proof] pub fn $nonzero_check_min_for() { - let int_x: $t = kani::any(); - kani::assume(int_x != 0); - let int_y: $t = kani::any(); - kani::assume(int_y != 0); - unsafe { - let x = <$nonzero_type>::new_unchecked(int_x); - let y = <$nonzero_type>::new_unchecked(int_y); - let result = x.min(y); - if x < y { - assert!(result == x); - } else { - assert!(result == y); - } + let x: $nonzero_type = kani::any(); + let y: $nonzero_type = kani::any(); + let result = x.min(y); + if x < y { + assert!(result == x); + } else { + assert!(result == y); } } }; } - // Use the macro to generate different versions of the function for multiple types - nonzero_check_min!(i8, core::num::NonZeroI8, nonzero_check_min_for_i8); - nonzero_check_min!(i16, core::num::NonZeroI16, nonzero_check_min_for_16); - nonzero_check_min!(i32, core::num::NonZeroI32, nonzero_check_min_for_32); - nonzero_check_min!(i64, core::num::NonZeroI64, nonzero_check_min_for_64); - nonzero_check_min!(i128, core::num::NonZeroI128, nonzero_check_min_for_128); - nonzero_check_min!(isize, core::num::NonZeroIsize, nonzero_check_min_for_isize); - nonzero_check_min!(u8, core::num::NonZeroU8, nonzero_check_min_for_u8); - nonzero_check_min!(u16, core::num::NonZeroU16, nonzero_check_min_for_u16); - nonzero_check_min!(u32, core::num::NonZeroU32, nonzero_check_min_for_u32); - nonzero_check_min!(u64, core::num::NonZeroU64, nonzero_check_min_for_u64); - nonzero_check_min!(u128, core::num::NonZeroU128, nonzero_check_min_for_u128); - nonzero_check_min!(usize, core::num::NonZeroUsize, nonzero_check_min_for_usize); + nonzero_check_min!(core::num::NonZeroI8, nonzero_check_min_for_i8); + nonzero_check_min!(core::num::NonZeroI16, nonzero_check_min_for_i16); + nonzero_check_min!(core::num::NonZeroI32, nonzero_check_min_for_i32); + nonzero_check_min!(core::num::NonZeroI64, nonzero_check_min_for_i64); + nonzero_check_min!(core::num::NonZeroI128, nonzero_check_min_for_i128); + nonzero_check_min!(core::num::NonZeroIsize, nonzero_check_min_for_isize); + nonzero_check_min!(core::num::NonZeroU8, nonzero_check_min_for_u8); + nonzero_check_min!(core::num::NonZeroU16, nonzero_check_min_for_u16); + nonzero_check_min!(core::num::NonZeroU32, nonzero_check_min_for_u32); + nonzero_check_min!(core::num::NonZeroU64, nonzero_check_min_for_u64); + nonzero_check_min!(core::num::NonZeroU128, nonzero_check_min_for_u128); + nonzero_check_min!(core::num::NonZeroUsize, nonzero_check_min_for_usize); }