From 5d800efacc5afc0fee088eaf4af544c77f46afd6 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Sun, 1 Dec 2024 16:47:18 -0500 Subject: [PATCH 1/5] clamp --- library/core/src/num/nonzero.rs | 51 +++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index ac7b1fca9fa87..4129810aacd3f 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2265,3 +2265,54 @@ 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_clamp { + use super::*; + macro_rules! nonzero_check_clamp { + ($t:ty, $nonzero_type:ty, $nonzero_check_clamp_for:ident) => { + #[kani::proof] + pub fn $nonzero_check_clamp_for() { + let x: $t = kani::any(); + kani::assume(x != 0); + let min: $t = kani::any(); + kani::assume(min != 0); + let max: $t = kani::any(); + kani::assume(max != 0); + + // Ensure min <= max + kani::assume(min <= max); + + unsafe { + let x = <$nonzero_type>::new_unchecked(x); + let min = <$nonzero_type>::new_unchecked(min); + let max = <$nonzero_type>::new_unchecked(max); + } + + // Use the clamp function and check the result + let result = x.clamp(min, max); + if x < min { + assert!(result == min); + } else if x > max { + assert!(result == max); + } else { + assert!(result == x); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_clamp!(i8, core::num::NonZeroI8, nonzero_check_clamp_for_i8); + nonzero_check_clamp!(i16, core::num::NonZeroI16, nonzero_check_clamp_for_16); + nonzero_check_clamp!(i32, core::num::NonZeroI32, nonzero_check_clamp_for_32); + nonzero_check_clamp!(i64, core::num::NonZeroI64, nonzero_check_clamp_for_64); + nonzero_check_clamp!(i128, core::num::NonZeroI128, nonzero_check_clamp_for_128); + nonzero_check_clamp!(isize, core::num::NonZeroIsize, nonzero_check_clamp_for_isize); + nonzero_check_clamp!(u8, core::num::NonZeroU8, nonzero_check_clamp_for_u8); + nonzero_check_clamp!(u16, core::num::NonZeroU16, nonzero_check_clamp_for_u16); + nonzero_check_clamp!(u32, core::num::NonZeroU32, nonzero_check_clamp_for_u32); + nonzero_check_clamp!(u64, core::num::NonZeroU64, nonzero_check_clamp_for_u64); + nonzero_check_clamp!(u128, core::num::NonZeroU128, nonzero_check_clamp_for_u128); + nonzero_check_clamp!(usize, core::num::NonZeroUsize, nonzero_check_clamp_for_usize); +} \ No newline at end of file From 8e81c29751d5067fd99a3a4f87c8fa24d5511e02 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 3 Dec 2024 20:41:38 -0500 Subject: [PATCH 2/5] directly use nonezero type for kani::any instead of using primitive integers --- library/core/src/num/nonzero.rs | 47 +++++++++++++-------------------- 1 file changed, 18 insertions(+), 29 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 4129810aacd3f..47d0c79e415a9 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2270,25 +2270,14 @@ mod verify { mod macro_nonzero_check_clamp { use super::*; macro_rules! nonzero_check_clamp { - ($t:ty, $nonzero_type:ty, $nonzero_check_clamp_for:ident) => { + ($nonzero_type:ty, $nonzero_check_clamp_for:ident) => { #[kani::proof] pub fn $nonzero_check_clamp_for() { - let x: $t = kani::any(); - kani::assume(x != 0); - let min: $t = kani::any(); - kani::assume(min != 0); - let max: $t = kani::any(); - kani::assume(max != 0); - - // Ensure min <= max + let x: $nonzero_type = kani::any(); + let min: $nonzero_type = kani::any(); + let max: $nonzero_type = kani::any(); + // Ensure min <= max, so the function should no panic kani::assume(min <= max); - - unsafe { - let x = <$nonzero_type>::new_unchecked(x); - let min = <$nonzero_type>::new_unchecked(min); - let max = <$nonzero_type>::new_unchecked(max); - } - // Use the clamp function and check the result let result = x.clamp(min, max); if x < min { @@ -2303,16 +2292,16 @@ mod macro_nonzero_check_clamp { } // Use the macro to generate different versions of the function for multiple types - nonzero_check_clamp!(i8, core::num::NonZeroI8, nonzero_check_clamp_for_i8); - nonzero_check_clamp!(i16, core::num::NonZeroI16, nonzero_check_clamp_for_16); - nonzero_check_clamp!(i32, core::num::NonZeroI32, nonzero_check_clamp_for_32); - nonzero_check_clamp!(i64, core::num::NonZeroI64, nonzero_check_clamp_for_64); - nonzero_check_clamp!(i128, core::num::NonZeroI128, nonzero_check_clamp_for_128); - nonzero_check_clamp!(isize, core::num::NonZeroIsize, nonzero_check_clamp_for_isize); - nonzero_check_clamp!(u8, core::num::NonZeroU8, nonzero_check_clamp_for_u8); - nonzero_check_clamp!(u16, core::num::NonZeroU16, nonzero_check_clamp_for_u16); - nonzero_check_clamp!(u32, core::num::NonZeroU32, nonzero_check_clamp_for_u32); - nonzero_check_clamp!(u64, core::num::NonZeroU64, nonzero_check_clamp_for_u64); - nonzero_check_clamp!(u128, core::num::NonZeroU128, nonzero_check_clamp_for_u128); - nonzero_check_clamp!(usize, core::num::NonZeroUsize, nonzero_check_clamp_for_usize); -} \ No newline at end of file + nonzero_check_clamp!(core::num::NonZeroI8, nonzero_check_clamp_for_i8); + nonzero_check_clamp!(core::num::NonZeroI16, nonzero_check_clamp_for_16); + nonzero_check_clamp!(core::num::NonZeroI32, nonzero_check_clamp_for_32); + nonzero_check_clamp!(core::num::NonZeroI64, nonzero_check_clamp_for_64); + nonzero_check_clamp!(core::num::NonZeroI128, nonzero_check_clamp_for_128); + nonzero_check_clamp!(core::num::NonZeroIsize, nonzero_check_clamp_for_isize); + nonzero_check_clamp!(core::num::NonZeroU8, nonzero_check_clamp_for_u8); + nonzero_check_clamp!(core::num::NonZeroU16, nonzero_check_clamp_for_u16); + nonzero_check_clamp!(core::num::NonZeroU32, nonzero_check_clamp_for_u32); + nonzero_check_clamp!(core::num::NonZeroU64, nonzero_check_clamp_for_u64); + nonzero_check_clamp!(core::num::NonZeroU128, nonzero_check_clamp_for_u128); + nonzero_check_clamp!(core::num::NonZeroUsize, nonzero_check_clamp_for_usize); +} From 24f90a22284437f5f4fad7c0e9a84eb852ae9a0c Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Tue, 3 Dec 2024 20:44:17 -0500 Subject: [PATCH 3/5] macro for clamp in case it should panic --- library/core/src/num/nonzero.rs | 41 +++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 47d0c79e415a9..ae14e76d2427e 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2305,3 +2305,44 @@ mod macro_nonzero_check_clamp { nonzero_check_clamp!(core::num::NonZeroU128, nonzero_check_clamp_for_u128); nonzero_check_clamp!(core::num::NonZeroUsize, nonzero_check_clamp_for_usize); } + +#[cfg(kani)] +mod macro_nonzero_check_clamp_panic { + use super::*; + macro_rules! nonzero_check_clamp_panic { + ($nonzero_type:ty, $nonzero_check_clamp_for:ident) => { + #[kani::proof] + #[kani::should_panic] + pub fn $nonzero_check_clamp_for() { + let x: $nonzero_type = kani::any(); + let min: $nonzero_type = kani::any(); + let max: $nonzero_type = kani::any(); + // Ensure min > max, so the function should panic + kani::assume(min > max); + // Use the clamp function and check the result + let result = x.clamp(min, max); + if x < min { + assert!(result == min); + } else if x > max { + assert!(result == max); + } else { + assert!(result == x); + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check_clamp_panic!(core::num::NonZeroI8, nonzero_check_clamp_panic_for_i8); + nonzero_check_clamp_panic!(core::num::NonZeroI16, nonzero_check_clamp_panic_for_16); + nonzero_check_clamp_panic!(core::num::NonZeroI32, nonzero_check_clamp_panic_for_32); + nonzero_check_clamp_panic!(core::num::NonZeroI64, nonzero_check_clamp_panic_for_64); + nonzero_check_clamp_panic!(core::num::NonZeroI128, nonzero_check_clamp_panic_for_128); + nonzero_check_clamp_panic!(core::num::NonZeroIsize, nonzero_check_clamp_panic_for_isize); + nonzero_check_clamp_panic!(core::num::NonZeroU8, nonzero_check_clamp_panic_for_u8); + nonzero_check_clamp_panic!(core::num::NonZeroU16, nonzero_check_clamp_panic_for_u16); + nonzero_check_clamp_panic!(core::num::NonZeroU32, nonzero_check_clamp_panic_for_u32); + nonzero_check_clamp_panic!(core::num::NonZeroU64, nonzero_check_clamp_panic_for_u64); + nonzero_check_clamp_panic!(core::num::NonZeroU128, nonzero_check_clamp_panic_for_u128); + nonzero_check_clamp_panic!(core::num::NonZeroUsize, nonzero_check_clamp_panic_for_usize); +} From 33e0316c8c5944694a1438225e01081d95b6933f Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Wed, 4 Dec 2024 21:43:22 -0500 Subject: [PATCH 4/5] no -> not Co-authored-by: Michael Tautschnig --- 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 ae14e76d2427e..2384c664e1a83 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2276,7 +2276,7 @@ mod macro_nonzero_check_clamp { let x: $nonzero_type = kani::any(); let min: $nonzero_type = kani::any(); let max: $nonzero_type = kani::any(); - // Ensure min <= max, so the function should no panic + // Ensure min <= max, so the function should not panic kani::assume(min <= max); // Use the clamp function and check the result let result = x.clamp(min, max); From cdaaa9ea159e5b7e0ef8e310ec64d94355595782 Mon Sep 17 00:00:00 2001 From: Aaron Lang Date: Wed, 4 Dec 2024 21:46:10 -0500 Subject: [PATCH 5/5] delete the checking on clamp result in panic case --- library/core/src/num/nonzero.rs | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index 2384c664e1a83..e0ce92d09e9c5 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -2319,15 +2319,8 @@ mod macro_nonzero_check_clamp_panic { let max: $nonzero_type = kani::any(); // Ensure min > max, so the function should panic kani::assume(min > max); - // Use the clamp function and check the result + // Use the clamp function which should cause panic let result = x.clamp(min, max); - if x < min { - assert!(result == min); - } else if x > max { - assert!(result == max); - } else { - assert!(result == x); - } } }; }