From 4b65e2193d016a89af8099c248536a43e2222104 Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Sun, 22 Dec 2024 04:06:42 +0900 Subject: [PATCH 01/11] Add harnesses for safety of primitive conversions --- library/core/src/convert/num.rs | 256 ++++++++++++++++++++++++++++++++ 1 file changed, 256 insertions(+) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 0246d0627cafe..139c04362abd2 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -1,4 +1,8 @@ use crate::num::TryFromIntError; +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; mod private { /// This trait being unreachable from outside the crate @@ -25,6 +29,22 @@ macro_rules! impl_float_to_int { #[unstable(feature = "convert_float_to_int", issue = "67057")] impl FloatToInt<$Int> for $Float { #[inline] + #[requires( + !self.is_nan() && + !self.is_infinite() && + // Even if <$Int>::MIN < <$Float>::MIN or <$Int>::MAX > <$Float>::MAX, + // the bounds would be -Inf or Inf, so they'll work anyways + self > <$Int>::MIN as $Float - 1.0 && + self < <$Int>::MAX as $Float + 1.0 + )] + #[ensures(|&result|{ + let fract = self - result as $Float; + if self > 0.0 { + fract >= 0.0 && fract < 1.0 + } else { + fract <= 0.0 && fract > -1.0 + } + })] unsafe fn to_int_unchecked(self) -> $Int { // SAFETY: the safety contract must be upheld by the caller. unsafe { crate::intrinsics::float_to_int_unchecked(self) } @@ -540,3 +560,239 @@ impl_nonzero_int_try_from_nonzero_int!(i32 => u8, u16, u32, u64, u128, usize); impl_nonzero_int_try_from_nonzero_int!(i64 => u8, u16, u32, u64, u128, usize); impl_nonzero_int_try_from_nonzero_int!(i128 => u8, u16, u32, u64, u128, usize); impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize); + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + macro_rules! generate_nonzero_int_from_nonzero_int_harness { + ($Small:ty => $Large:ty, $harness:ident) => { + #[kani::proof] + pub fn $harness() { + let x_inner: $Small = kani::any(); + kani::assume(x_inner != 0); + + let x = NonZero::new(x_inner).unwrap(); + let y = NonZero::<$Large>::from(x); + + assert_eq!(x_inner as $Large, <$Large>::from(y)); + } + }; + } + + // non-zero unsigned integer -> non-zero unsigned integer + generate_nonzero_int_from_nonzero_int_harness!(u8 => u16, check_nonzero_u16_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u8 => u32, check_nonzero_u32_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u8 => u64, check_nonzero_u64_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u8 => u128, check_nonzero_u128_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u8 => usize, check_nonzero_usize_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u16 => u32, check_nonzero_u32_from_nonzero_u16); + generate_nonzero_int_from_nonzero_int_harness!(u16 => u64, check_nonzero_u64_from_nonzero_u16); + generate_nonzero_int_from_nonzero_int_harness!(u16 => u128, check_nonzero_u128_from_nonzero_u16); + generate_nonzero_int_from_nonzero_int_harness!(u16 => usize, check_nonzero_usize_from_nonzero_u16); + generate_nonzero_int_from_nonzero_int_harness!(u32 => u64, check_nonzero_u64_from_nonzero_u32); + generate_nonzero_int_from_nonzero_int_harness!(u32 => u128, check_nonzero_u128_from_nonzero_u32); + generate_nonzero_int_from_nonzero_int_harness!(u64 => u128, check_nonzero_u128_from_nonzero_u64); + + // non-zero signed integer -> non-zero signed integer + generate_nonzero_int_from_nonzero_int_harness!(i8 => i16, check_nonzero_i16_from_nonzero_i8); + generate_nonzero_int_from_nonzero_int_harness!(i8 => i32, check_nonzero_i32_from_nonzero_i8); + generate_nonzero_int_from_nonzero_int_harness!(i8 => i64, check_nonzero_i64_from_nonzero_i8); + generate_nonzero_int_from_nonzero_int_harness!(i8 => i128, check_nonzero_i128_from_nonzero_i8); + generate_nonzero_int_from_nonzero_int_harness!(i8 => isize, check_nonzero_isize_from_nonzero_i8); + generate_nonzero_int_from_nonzero_int_harness!(i16 => i32, check_nonzero_i32_from_nonzero_i16); + generate_nonzero_int_from_nonzero_int_harness!(i16 => i64, check_nonzero_i64_from_nonzero_i16); + generate_nonzero_int_from_nonzero_int_harness!(i16 => i128, check_nonzero_i128_from_nonzero_i16); + generate_nonzero_int_from_nonzero_int_harness!(i16 => isize, check_nonzero_isize_from_nonzero_i16); + generate_nonzero_int_from_nonzero_int_harness!(i32 => i64, check_nonzero_i64_from_nonzero_i32); + generate_nonzero_int_from_nonzero_int_harness!(i32 => i128, check_nonzero_i128_from_nonzero_i32); + generate_nonzero_int_from_nonzero_int_harness!(i64 => i128, check_nonzero_i128_from_nonzero_i64); + + // non-zero unsigned integer -> non-zero signed integer + generate_nonzero_int_from_nonzero_int_harness!(u8 => i16, check_nonzero_i16_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u8 => i32, check_nonzero_i32_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u8 => i64, check_nonzero_i64_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u8 => i128, check_nonzero_i128_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u8 => isize, check_nonzero_isize_from_nonzero_u8); + generate_nonzero_int_from_nonzero_int_harness!(u16 => i32, check_nonzero_i32_from_nonzero_u16); + generate_nonzero_int_from_nonzero_int_harness!(u16 => i64, check_nonzero_i64_from_nonzero_u16); + generate_nonzero_int_from_nonzero_int_harness!(u16 => i128, check_nonzero_i128_from_nonzero_u16); + generate_nonzero_int_from_nonzero_int_harness!(u32 => i64, check_nonzero_i64_from_nonzero_u32); + generate_nonzero_int_from_nonzero_int_harness!(u32 => i128, check_nonzero_i128_from_nonzero_u32); + generate_nonzero_int_from_nonzero_int_harness!(u64 => i128, check_nonzero_i128_from_nonzero_u64); + + macro_rules! generate_nonzero_int_try_from_nonzero_int_harness { + ($source:ty => $target:ty, $harness:ident) => { + #[kani::proof] + pub fn $harness() { + let x_inner: $source = kani::any(); + kani::assume(x_inner != 0); + + let x = NonZero::new(x_inner).unwrap(); + let y = NonZero::<$target>::try_from(x); + + let y_inner = <$target>::try_from(x_inner); + if let Ok(y_inner) = y_inner { + assert!(y.is_ok_and(|y| <$target>::from(y) == y_inner)); + } else { + assert!(y.is_err()); + } + } + }; + } + + // unsigned non-zero integer -> unsigned non-zero integer fallible + generate_nonzero_int_try_from_nonzero_int_harness!(u16 => u8, check_nonzero_u8_try_from_nonzero_u16); + generate_nonzero_int_try_from_nonzero_int_harness!(u32 => u8, check_nonzero_u8_try_from_nonzero_u32); + generate_nonzero_int_try_from_nonzero_int_harness!(u32 => u16, check_nonzero_u16_try_from_nonzero_u32); + generate_nonzero_int_try_from_nonzero_int_harness!(u32 => usize, check_nonzero_usize_try_from_nonzero_u32); + generate_nonzero_int_try_from_nonzero_int_harness!(u64 => u8, check_nonzero_u8_try_from_nonzero_u64); + generate_nonzero_int_try_from_nonzero_int_harness!(u64 => u16, check_nonzero_u16_try_from_nonzero_u64); + generate_nonzero_int_try_from_nonzero_int_harness!(u64 => u32, check_nonzero_u32_try_from_nonzero_u64); + generate_nonzero_int_try_from_nonzero_int_harness!(u64 => usize, check_nonzero_usize_try_from_nonzero_u64); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => u8, check_nonzero_u8_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => u16, check_nonzero_u16_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => u32, check_nonzero_u32_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => u64, check_nonzero_u64_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => usize, check_nonzero_usize_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => u8, check_nonzero_u8_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => u16, check_nonzero_u16_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => u32, check_nonzero_u32_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => u64, check_nonzero_u64_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => u128, check_nonzero_u128_try_from_nonzero_usize); + + // signed non-zero integer -> signed non-zero integer fallible + generate_nonzero_int_try_from_nonzero_int_harness!(i16 => i8, check_nonzero_i8_try_from_nonzero_i16); + generate_nonzero_int_try_from_nonzero_int_harness!(i32 => i8, check_nonzero_i8_try_from_nonzero_i32); + generate_nonzero_int_try_from_nonzero_int_harness!(i32 => i16, check_nonzero_i16_try_from_nonzero_i32); + generate_nonzero_int_try_from_nonzero_int_harness!(i32 => isize, check_nonzero_isize_try_from_nonzero_i32); + generate_nonzero_int_try_from_nonzero_int_harness!(i64 => i8, check_nonzero_i8_try_from_nonzero_i64); + generate_nonzero_int_try_from_nonzero_int_harness!(i64 => i16, check_nonzero_i16_try_from_nonzero_i64); + generate_nonzero_int_try_from_nonzero_int_harness!(i64 => i32, check_nonzero_i32_try_from_nonzero_i64); + generate_nonzero_int_try_from_nonzero_int_harness!(i64 => isize, check_nonzero_isize_try_from_nonzero_i64); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => i8, check_nonzero_i8_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => i16, check_nonzero_i16_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => i32, check_nonzero_i32_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => i64, check_nonzero_i64_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => isize, check_nonzero_isize_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => i8, check_nonzero_i8_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => i16, check_nonzero_i16_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => i32, check_nonzero_i32_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => i64, check_nonzero_i64_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => i128, check_nonzero_i128_try_from_nonzero_isize); + + // unsigned non-zero integer -> signed non-zero integer fallible + generate_nonzero_int_try_from_nonzero_int_harness!(u8 => i8, check_nonzero_i8_try_from_nonzero_u8); + generate_nonzero_int_try_from_nonzero_int_harness!(u16 => i8, check_nonzero_i8_try_from_nonzero_u16); + generate_nonzero_int_try_from_nonzero_int_harness!(u16 => i16, check_nonzero_i16_try_from_nonzero_u16); + generate_nonzero_int_try_from_nonzero_int_harness!(u16 => isize, check_nonzero_isize_try_from_nonzero_u16); + generate_nonzero_int_try_from_nonzero_int_harness!(u32 => i8, check_nonzero_i8_try_from_nonzero_u32); + generate_nonzero_int_try_from_nonzero_int_harness!(u32 => i16, check_nonzero_i16_try_from_nonzero_u32); + generate_nonzero_int_try_from_nonzero_int_harness!(u32 => i32, check_nonzero_i32_try_from_nonzero_u32); + generate_nonzero_int_try_from_nonzero_int_harness!(u32 => isize, check_nonzero_isize_try_from_nonzero_u32); + generate_nonzero_int_try_from_nonzero_int_harness!(u64 => i8, check_nonzero_i8_try_from_nonzero_u64); + generate_nonzero_int_try_from_nonzero_int_harness!(u64 => i16, check_nonzero_i16_try_from_nonzero_u64); + generate_nonzero_int_try_from_nonzero_int_harness!(u64 => i32, check_nonzero_i32_try_from_nonzero_u64); + generate_nonzero_int_try_from_nonzero_int_harness!(u64 => u64, check_nonzero_u64_try_from_nonzero_u64); + generate_nonzero_int_try_from_nonzero_int_harness!(u64 => isize, check_nonzero_isize_try_from_nonzero_u64); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i8, check_nonzero_i8_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i16, check_nonzero_i16_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i32, check_nonzero_i32_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i64, check_nonzero_i64_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i128, check_nonzero_i128_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(u128 => isize, check_nonzero_isize_try_from_nonzero_u128); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => i8, check_nonzero_i8_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => i16, check_nonzero_i16_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => i32, check_nonzero_i32_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => i64, check_nonzero_i64_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => i128, check_nonzero_i128_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!(usize => isize, check_nonzero_isize_try_from_nonzero_usize); + + // signed non-zero integer -> unsigned non-zero integer fallible + generate_nonzero_int_try_from_nonzero_int_harness!(i8 => u8, check_nonzero_u8_try_from_nonzero_i8); + generate_nonzero_int_try_from_nonzero_int_harness!(i16 => u8, check_nonzero_u8_try_from_nonzero_i16); + generate_nonzero_int_try_from_nonzero_int_harness!(i16 => u16, check_nonzero_u16_try_from_nonzero_i16); + generate_nonzero_int_try_from_nonzero_int_harness!(i16 => usize, check_nonzero_usize_try_from_nonzero_i16); + generate_nonzero_int_try_from_nonzero_int_harness!(i32 => u8, check_nonzero_u8_try_from_nonzero_i32); + generate_nonzero_int_try_from_nonzero_int_harness!(i32 => u16, check_nonzero_u16_try_from_nonzero_i32); + generate_nonzero_int_try_from_nonzero_int_harness!(i32 => u32, check_nonzero_u32_try_from_nonzero_i32); + generate_nonzero_int_try_from_nonzero_int_harness!(i32 => usize, check_nonzero_usize_try_from_nonzero_i32); + generate_nonzero_int_try_from_nonzero_int_harness!(i64 => u8, check_nonzero_u8_try_from_nonzero_i64); + generate_nonzero_int_try_from_nonzero_int_harness!(i64 => u16, check_nonzero_u16_try_from_nonzero_i64); + generate_nonzero_int_try_from_nonzero_int_harness!(i64 => u32, check_nonzero_u32_try_from_nonzero_i64); + generate_nonzero_int_try_from_nonzero_int_harness!(i64 => u64, check_nonzero_u64_try_from_nonzero_i64); + generate_nonzero_int_try_from_nonzero_int_harness!(i64 => usize, check_nonzero_usize_try_from_nonzero_i64); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u8, check_nonzero_u8_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u16, check_nonzero_u16_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u32, check_nonzero_u32_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u64, check_nonzero_u64_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u128, check_nonzero_u128_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(i128 => usize, check_nonzero_usize_try_from_nonzero_i128); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => u8, check_nonzero_u8_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => u16, check_nonzero_u16_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => u32, check_nonzero_u32_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => u64, check_nonzero_u64_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => u128, check_nonzero_u128_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!(isize => usize, check_nonzero_usize_try_from_nonzero_isize); + + macro_rules! generate_float_to_int_harness { + ($Float:ty => $Int:ty, $harness:ident) => { + #[kani::proof_for_contract(<$Float>::to_int_unchecked)] + pub fn $harness() { + let x: $Float = kani::any(); + let _: $Int = unsafe { x.to_int_unchecked() }; + } + }; + } + + // float -> integer unchecked + generate_float_to_int_harness!(f16 => u8, check_u8_from_f16_unchecked); + generate_float_to_int_harness!(f16 => u16, check_u16_from_f16_unchecked); + generate_float_to_int_harness!(f16 => u32, check_u32_from_f16_unchecked); + generate_float_to_int_harness!(f16 => u64, check_u64_from_f16_unchecked); + generate_float_to_int_harness!(f16 => u128, check_u128_from_f16_unchecked); + generate_float_to_int_harness!(f16 => usize, check_usize_from_f16_unchecked); + generate_float_to_int_harness!(f16 => i8, check_i8_from_f16_unchecked); + generate_float_to_int_harness!(f16 => i16, check_i16_from_f16_unchecked); + generate_float_to_int_harness!(f16 => i32, check_i32_from_f16_unchecked); + generate_float_to_int_harness!(f16 => i64, check_i64_from_f16_unchecked); + generate_float_to_int_harness!(f16 => i128, check_i128_from_f16_unchecked); + generate_float_to_int_harness!(f16 => isize, check_isize_from_f16_unchecked); + generate_float_to_int_harness!(f32 => u8, check_u8_from_f32_unchecked); + generate_float_to_int_harness!(f32 => u16, check_u16_from_f32_unchecked); + generate_float_to_int_harness!(f32 => u32, check_u32_from_f32_unchecked); + generate_float_to_int_harness!(f32 => u64, check_u64_from_f32_unchecked); + generate_float_to_int_harness!(f32 => u128, check_u128_from_f32_unchecked); + generate_float_to_int_harness!(f32 => usize, check_usize_from_f32_unchecked); + generate_float_to_int_harness!(f32 => i8, check_i8_from_f32_unchecked); + generate_float_to_int_harness!(f32 => i16, check_i16_from_f32_unchecked); + generate_float_to_int_harness!(f32 => i32, check_i32_from_f32_unchecked); + generate_float_to_int_harness!(f32 => i64, check_i64_from_f32_unchecked); + generate_float_to_int_harness!(f32 => i128, check_i128_from_f32_unchecked); + generate_float_to_int_harness!(f32 => isize, check_isize_from_f32_unchecked); + generate_float_to_int_harness!(f64 => u8, check_u8_from_f64_unchecked); + generate_float_to_int_harness!(f64 => u16, check_u16_from_f64_unchecked); + generate_float_to_int_harness!(f64 => u32, check_u32_from_f64_unchecked); + generate_float_to_int_harness!(f64 => u64, check_u64_from_f64_unchecked); + generate_float_to_int_harness!(f64 => u128, check_u128_from_f64_unchecked); + generate_float_to_int_harness!(f64 => usize, check_usize_from_f64_unchecked); + generate_float_to_int_harness!(f64 => i8, check_i8_from_f64_unchecked); + generate_float_to_int_harness!(f64 => i16, check_i16_from_f64_unchecked); + generate_float_to_int_harness!(f64 => i32, check_i32_from_f64_unchecked); + generate_float_to_int_harness!(f64 => i64, check_i64_from_f64_unchecked); + generate_float_to_int_harness!(f64 => i128, check_i128_from_f64_unchecked); + generate_float_to_int_harness!(f64 => isize, check_isize_from_f64_unchecked); + generate_float_to_int_harness!(f128 => u8, check_u8_from_f128_unchecked); + generate_float_to_int_harness!(f128 => u16, check_u16_from_f128_unchecked); + generate_float_to_int_harness!(f128 => u32, check_u32_from_f128_unchecked); + generate_float_to_int_harness!(f128 => u64, check_u64_from_f128_unchecked); + generate_float_to_int_harness!(f128 => u128, check_u128_from_f128_unchecked); + generate_float_to_int_harness!(f128 => usize, check_usize_from_f128_unchecked); + generate_float_to_int_harness!(f128 => i8, check_i8_from_f128_unchecked); + generate_float_to_int_harness!(f128 => i16, check_i16_from_f128_unchecked); + generate_float_to_int_harness!(f128 => i32, check_i32_from_f128_unchecked); + generate_float_to_int_harness!(f128 => i64, check_i64_from_f128_unchecked); + generate_float_to_int_harness!(f128 => i128, check_i128_from_f128_unchecked); + generate_float_to_int_harness!(f128 => isize, check_isize_from_f128_unchecked); +} From 5851327b338fe5a3fb7df5cd806d1985456a94cc Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Mon, 23 Dec 2024 22:05:25 +0900 Subject: [PATCH 02/11] Clean up the codes a bit --- library/core/src/convert/num.rs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 139c04362abd2..a93461a1d1d4c 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -570,12 +570,10 @@ mod verify { ($Small:ty => $Large:ty, $harness:ident) => { #[kani::proof] pub fn $harness() { - let x_inner: $Small = kani::any(); - kani::assume(x_inner != 0); - - let x = NonZero::new(x_inner).unwrap(); + let x: NonZero<$Small> = kani::any(); let y = NonZero::<$Large>::from(x); + let x_inner = <$Small>::from(x); assert_eq!(x_inner as $Large, <$Large>::from(y)); } }; @@ -626,14 +624,16 @@ mod verify { ($source:ty => $target:ty, $harness:ident) => { #[kani::proof] pub fn $harness() { - let x_inner: $source = kani::any(); - kani::assume(x_inner != 0); - - let x = NonZero::new(x_inner).unwrap(); + let x: NonZero<$source> = kani::any(); let y = NonZero::<$target>::try_from(x); + // The conversion must succeed if and only if the inner value of source type + // fits into the target type, i.e. inner type conversion succeeds. + let x_inner = <$source>::from(x); let y_inner = <$target>::try_from(x_inner); if let Ok(y_inner) = y_inner { + // And the inner value of converted nonzero must be equal to the direct + // conversion result. assert!(y.is_ok_and(|y| <$target>::from(y) == y_inner)); } else { assert!(y.is_err()); From 9c5889c811889b1468eff459a162f10d0014d5ce Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Sun, 29 Dec 2024 04:12:25 +0900 Subject: [PATCH 03/11] Clean the codes a bit --- library/core/src/convert/num.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index a93461a1d1d4c..b24530a317407 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -4,6 +4,9 @@ use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; +#[allow(unused_imports)] +use crate::ub_checks::float_to_int_in_range; + mod private { /// This trait being unreachable from outside the crate /// prevents other implementations of the `FloatToInt` trait, @@ -31,11 +34,8 @@ macro_rules! impl_float_to_int { #[inline] #[requires( !self.is_nan() && - !self.is_infinite() && - // Even if <$Int>::MIN < <$Float>::MIN or <$Int>::MAX > <$Float>::MAX, - // the bounds would be -Inf or Inf, so they'll work anyways - self > <$Int>::MIN as $Float - 1.0 && - self < <$Int>::MAX as $Float + 1.0 + self.is_finite() && + float_to_int_in_range::<$Float, $Int>(self) )] #[ensures(|&result|{ let fract = self - result as $Float; From 579a2572a856bd20a8d0d7db6745f2ea5e6ed573 Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Sat, 4 Jan 2025 07:48:23 +0900 Subject: [PATCH 04/11] Apply reviews --- library/core/src/convert/num.rs | 566 +++++++++++++++++++++++++------- 1 file changed, 451 insertions(+), 115 deletions(-) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index b24530a317407..07eec1798d7a9 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -1,5 +1,5 @@ use crate::num::TryFromIntError; -use safety::{ensures, requires}; +use safety::requires; #[cfg(kani)] use crate::kani; @@ -37,14 +37,6 @@ macro_rules! impl_float_to_int { self.is_finite() && float_to_int_in_range::<$Float, $Int>(self) )] - #[ensures(|&result|{ - let fract = self - result as $Float; - if self > 0.0 { - fract >= 0.0 && fract < 1.0 - } else { - fract <= 0.0 && fract > -1.0 - } - })] unsafe fn to_int_unchecked(self) -> $Int { // SAFETY: the safety contract must be upheld by the caller. unsafe { crate::intrinsics::float_to_int_unchecked(self) } @@ -571,10 +563,7 @@ mod verify { #[kani::proof] pub fn $harness() { let x: NonZero<$Small> = kani::any(); - let y = NonZero::<$Large>::from(x); - - let x_inner = <$Small>::from(x); - assert_eq!(x_inner as $Large, <$Large>::from(y)); + let _ = NonZero::<$Large>::from(x); } }; } @@ -621,120 +610,467 @@ mod verify { generate_nonzero_int_from_nonzero_int_harness!(u64 => i128, check_nonzero_i128_from_nonzero_u64); macro_rules! generate_nonzero_int_try_from_nonzero_int_harness { - ($source:ty => $target:ty, $harness:ident) => { + ($source:ty => $target:ty, $harness_pass:ident, $harness_panic:ident,) => { #[kani::proof] - pub fn $harness() { - let x: NonZero<$source> = kani::any(); - let y = NonZero::<$target>::try_from(x); - - // The conversion must succeed if and only if the inner value of source type - // fits into the target type, i.e. inner type conversion succeeds. - let x_inner = <$source>::from(x); - let y_inner = <$target>::try_from(x_inner); - if let Ok(y_inner) = y_inner { - // And the inner value of converted nonzero must be equal to the direct - // conversion result. - assert!(y.is_ok_and(|y| <$target>::from(y) == y_inner)); - } else { - assert!(y.is_err()); - } + pub fn $harness_pass() { + let x_inner: $source = kani::any_where(|&v| { + (v > 0 && (v as u128) <= (<$target>::MAX as u128)) || + (v < 0 && (v as i128) >= (<$target>::MIN as i128)) + }); + let x = NonZero::new(x_inner).unwrap(); + let _ = NonZero::<$target>::try_from(x).unwrap(); + } + + #[kani::proof] + #[kani::should_panic] + pub fn $harness_panic() { + let x_inner: $source = kani::any_where(|&v| { + (v > 0 && (v as u128) > (<$target>::MAX as u128)) || + (v < 0 && (v as i128) < (<$target>::MIN as i128)) + }); + let x = NonZero::new(x_inner).unwrap(); + let _ = NonZero::<$target>::try_from(x).unwrap(); } }; } // unsigned non-zero integer -> unsigned non-zero integer fallible - generate_nonzero_int_try_from_nonzero_int_harness!(u16 => u8, check_nonzero_u8_try_from_nonzero_u16); - generate_nonzero_int_try_from_nonzero_int_harness!(u32 => u8, check_nonzero_u8_try_from_nonzero_u32); - generate_nonzero_int_try_from_nonzero_int_harness!(u32 => u16, check_nonzero_u16_try_from_nonzero_u32); - generate_nonzero_int_try_from_nonzero_int_harness!(u32 => usize, check_nonzero_usize_try_from_nonzero_u32); - generate_nonzero_int_try_from_nonzero_int_harness!(u64 => u8, check_nonzero_u8_try_from_nonzero_u64); - generate_nonzero_int_try_from_nonzero_int_harness!(u64 => u16, check_nonzero_u16_try_from_nonzero_u64); - generate_nonzero_int_try_from_nonzero_int_harness!(u64 => u32, check_nonzero_u32_try_from_nonzero_u64); - generate_nonzero_int_try_from_nonzero_int_harness!(u64 => usize, check_nonzero_usize_try_from_nonzero_u64); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => u8, check_nonzero_u8_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => u16, check_nonzero_u16_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => u32, check_nonzero_u32_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => u64, check_nonzero_u64_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => usize, check_nonzero_usize_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => u8, check_nonzero_u8_try_from_nonzero_usize); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => u16, check_nonzero_u16_try_from_nonzero_usize); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => u32, check_nonzero_u32_try_from_nonzero_usize); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => u64, check_nonzero_u64_try_from_nonzero_usize); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => u128, check_nonzero_u128_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!( + u16 => u8, + check_nonzero_u8_try_from_nonzero_u16, + check_nonzero_u8_try_from_nonzero_u16_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u32 => u8, + check_nonzero_u8_try_from_nonzero_u32, + check_nonzero_u8_try_from_nonzero_u32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u32 => u16, + check_nonzero_u16_try_from_nonzero_u32, + check_nonzero_u16_try_from_nonzero_u32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u32 => usize, + check_nonzero_usize_try_from_nonzero_u32, + check_nonzero_usize_try_from_nonzero_u32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => u8, + check_nonzero_u8_try_from_nonzero_u64, + check_nonzero_u8_try_from_nonzero_u64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => u16, + check_nonzero_u16_try_from_nonzero_u64, + check_nonzero_u16_try_from_nonzero_u64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => u32, + check_nonzero_u32_try_from_nonzero_u64, + check_nonzero_u32_try_from_nonzero_u64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => usize, + check_nonzero_usize_try_from_nonzero_u64, + check_nonzero_usize_try_from_nonzero_u64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => u8, + check_nonzero_u8_try_from_nonzero_u128, + check_nonzero_u8_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => u16, + check_nonzero_u16_try_from_nonzero_u128, + check_nonzero_u16_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => u32, + check_nonzero_u32_try_from_nonzero_u128, + check_nonzero_u32_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => u64, + check_nonzero_u64_try_from_nonzero_u128, + check_nonzero_u64_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => usize, + check_nonzero_usize_try_from_nonzero_u128, + check_nonzero_usize_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => u8, + check_nonzero_u8_try_from_nonzero_usize, + check_nonzero_u8_try_from_nonzero_usize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => u16, + check_nonzero_u16_try_from_nonzero_usize, + check_nonzero_u16_try_from_nonzero_usize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => u32, + check_nonzero_u32_try_from_nonzero_usize, + check_nonzero_u32_try_from_nonzero_usize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => u64, + check_nonzero_u64_try_from_nonzero_usize, + check_nonzero_u64_try_from_nonzero_usize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => u128, + check_nonzero_u128_try_from_nonzero_usize, + check_nonzero_u128_try_from_nonzero_usize_should_panic, + ); // signed non-zero integer -> signed non-zero integer fallible - generate_nonzero_int_try_from_nonzero_int_harness!(i16 => i8, check_nonzero_i8_try_from_nonzero_i16); - generate_nonzero_int_try_from_nonzero_int_harness!(i32 => i8, check_nonzero_i8_try_from_nonzero_i32); - generate_nonzero_int_try_from_nonzero_int_harness!(i32 => i16, check_nonzero_i16_try_from_nonzero_i32); - generate_nonzero_int_try_from_nonzero_int_harness!(i32 => isize, check_nonzero_isize_try_from_nonzero_i32); - generate_nonzero_int_try_from_nonzero_int_harness!(i64 => i8, check_nonzero_i8_try_from_nonzero_i64); - generate_nonzero_int_try_from_nonzero_int_harness!(i64 => i16, check_nonzero_i16_try_from_nonzero_i64); - generate_nonzero_int_try_from_nonzero_int_harness!(i64 => i32, check_nonzero_i32_try_from_nonzero_i64); - generate_nonzero_int_try_from_nonzero_int_harness!(i64 => isize, check_nonzero_isize_try_from_nonzero_i64); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => i8, check_nonzero_i8_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => i16, check_nonzero_i16_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => i32, check_nonzero_i32_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => i64, check_nonzero_i64_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => isize, check_nonzero_isize_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => i8, check_nonzero_i8_try_from_nonzero_isize); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => i16, check_nonzero_i16_try_from_nonzero_isize); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => i32, check_nonzero_i32_try_from_nonzero_isize); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => i64, check_nonzero_i64_try_from_nonzero_isize); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => i128, check_nonzero_i128_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!( + i16 => i8, + check_nonzero_i8_try_from_nonzero_i16, + check_nonzero_i8_try_from_nonzero_i16_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i32 => i8, + check_nonzero_i8_try_from_nonzero_i32, + check_nonzero_i8_try_from_nonzero_i32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i32 => i16, + check_nonzero_i16_try_from_nonzero_i32, + check_nonzero_i16_try_from_nonzero_i32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i32 => isize, + check_nonzero_isize_try_from_nonzero_i32, + check_nonzero_isize_try_from_nonzero_i32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => i8, + check_nonzero_i8_try_from_nonzero_i64, + check_nonzero_i8_try_from_nonzero_i64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => i16, + check_nonzero_i16_try_from_nonzero_i64, + check_nonzero_i16_try_from_nonzero_i64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => i32, + check_nonzero_i32_try_from_nonzero_i64, + check_nonzero_i32_try_from_nonzero_i64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => isize, + check_nonzero_isize_try_from_nonzero_i64, + check_nonzero_isize_try_from_nonzero_i64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => i8, + check_nonzero_i8_try_from_nonzero_i128, + check_nonzero_i8_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => i16, + check_nonzero_i16_try_from_nonzero_i128, + check_nonzero_i16_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => i32, + check_nonzero_i32_try_from_nonzero_i128, + check_nonzero_i32_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => i64, + check_nonzero_i64_try_from_nonzero_i128, + check_nonzero_i64_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => isize, + check_nonzero_isize_try_from_nonzero_i128, + check_nonzero_isize_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => i8, + check_nonzero_i8_try_from_nonzero_isize, + check_nonzero_i8_try_from_nonzero_isize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => i16, + check_nonzero_i16_try_from_nonzero_isize, + check_nonzero_i16_try_from_nonzero_isize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => i32, + check_nonzero_i32_try_from_nonzero_isize, + check_nonzero_i32_try_from_nonzero_isize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => i64, + check_nonzero_i64_try_from_nonzero_isize, + check_nonzero_i64_try_from_nonzero_isize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => i128, + check_nonzero_i128_try_from_nonzero_isize, + check_nonzero_i128_try_from_nonzero_isize_should_panic, + ); // unsigned non-zero integer -> signed non-zero integer fallible - generate_nonzero_int_try_from_nonzero_int_harness!(u8 => i8, check_nonzero_i8_try_from_nonzero_u8); - generate_nonzero_int_try_from_nonzero_int_harness!(u16 => i8, check_nonzero_i8_try_from_nonzero_u16); - generate_nonzero_int_try_from_nonzero_int_harness!(u16 => i16, check_nonzero_i16_try_from_nonzero_u16); - generate_nonzero_int_try_from_nonzero_int_harness!(u16 => isize, check_nonzero_isize_try_from_nonzero_u16); - generate_nonzero_int_try_from_nonzero_int_harness!(u32 => i8, check_nonzero_i8_try_from_nonzero_u32); - generate_nonzero_int_try_from_nonzero_int_harness!(u32 => i16, check_nonzero_i16_try_from_nonzero_u32); - generate_nonzero_int_try_from_nonzero_int_harness!(u32 => i32, check_nonzero_i32_try_from_nonzero_u32); - generate_nonzero_int_try_from_nonzero_int_harness!(u32 => isize, check_nonzero_isize_try_from_nonzero_u32); - generate_nonzero_int_try_from_nonzero_int_harness!(u64 => i8, check_nonzero_i8_try_from_nonzero_u64); - generate_nonzero_int_try_from_nonzero_int_harness!(u64 => i16, check_nonzero_i16_try_from_nonzero_u64); - generate_nonzero_int_try_from_nonzero_int_harness!(u64 => i32, check_nonzero_i32_try_from_nonzero_u64); - generate_nonzero_int_try_from_nonzero_int_harness!(u64 => u64, check_nonzero_u64_try_from_nonzero_u64); - generate_nonzero_int_try_from_nonzero_int_harness!(u64 => isize, check_nonzero_isize_try_from_nonzero_u64); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i8, check_nonzero_i8_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i16, check_nonzero_i16_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i32, check_nonzero_i32_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i64, check_nonzero_i64_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => i128, check_nonzero_i128_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(u128 => isize, check_nonzero_isize_try_from_nonzero_u128); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => i8, check_nonzero_i8_try_from_nonzero_usize); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => i16, check_nonzero_i16_try_from_nonzero_usize); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => i32, check_nonzero_i32_try_from_nonzero_usize); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => i64, check_nonzero_i64_try_from_nonzero_usize); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => i128, check_nonzero_i128_try_from_nonzero_usize); - generate_nonzero_int_try_from_nonzero_int_harness!(usize => isize, check_nonzero_isize_try_from_nonzero_usize); + generate_nonzero_int_try_from_nonzero_int_harness!( + u8 => i8, + check_nonzero_i8_try_from_nonzero_u8, + check_nonzero_i8_try_from_nonzero_u8_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u16 => i8, + check_nonzero_i8_try_from_nonzero_u16, + check_nonzero_i8_try_from_nonzero_u16_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u16 => i16, + check_nonzero_i16_try_from_nonzero_u16, + check_nonzero_i16_try_from_nonzero_u16_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u16 => isize, + check_nonzero_isize_try_from_nonzero_u16, + check_nonzero_isize_try_from_nonzero_u16_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u32 => i8, + check_nonzero_i8_try_from_nonzero_u32, + check_nonzero_i8_try_from_nonzero_u32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u32 => i16, + check_nonzero_i16_try_from_nonzero_u32, + check_nonzero_i16_try_from_nonzero_u32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u32 => i32, + check_nonzero_i32_try_from_nonzero_u32, + check_nonzero_i32_try_from_nonzero_u32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u32 => isize, + check_nonzero_isize_try_from_nonzero_u32, + check_nonzero_isize_try_from_nonzero_u32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => i8, + check_nonzero_i8_try_from_nonzero_u64, + check_nonzero_i8_try_from_nonzero_u64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => i16, + check_nonzero_i16_try_from_nonzero_u64, + check_nonzero_i16_try_from_nonzero_u64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => i32, + check_nonzero_i32_try_from_nonzero_u64, + check_nonzero_i32_try_from_nonzero_u64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => u64, + check_nonzero_u64_try_from_nonzero_u64, + check_nonzero_u64_try_from_nonzero_u64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => isize, + check_nonzero_isize_try_from_nonzero_u64, + check_nonzero_isize_try_from_nonzero_u64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => i8, + check_nonzero_i8_try_from_nonzero_u128, + check_nonzero_i8_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => i16, + check_nonzero_i16_try_from_nonzero_u128, + check_nonzero_i16_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => i32, + check_nonzero_i32_try_from_nonzero_u128, + check_nonzero_i32_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => i64, + check_nonzero_i64_try_from_nonzero_u128, + check_nonzero_i64_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => i128, + check_nonzero_i128_try_from_nonzero_u128, + check_nonzero_i128_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + u128 => isize, + check_nonzero_isize_try_from_nonzero_u128, + check_nonzero_isize_try_from_nonzero_u128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => i8, + check_nonzero_i8_try_from_nonzero_usize, + check_nonzero_i8_try_from_nonzero_usize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => i16, + check_nonzero_i16_try_from_nonzero_usize, + check_nonzero_i16_try_from_nonzero_usize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => i32, + check_nonzero_i32_try_from_nonzero_usize, + check_nonzero_i32_try_from_nonzero_usize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => i64, + check_nonzero_i64_try_from_nonzero_usize, + check_nonzero_i64_try_from_nonzero_usize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => i128, + check_nonzero_i128_try_from_nonzero_usize, + check_nonzero_i128_try_from_nonzero_usize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => isize, + check_nonzero_isize_try_from_nonzero_usize, + check_nonzero_isize_try_from_nonzero_usize_should_panic, + ); // signed non-zero integer -> unsigned non-zero integer fallible - generate_nonzero_int_try_from_nonzero_int_harness!(i8 => u8, check_nonzero_u8_try_from_nonzero_i8); - generate_nonzero_int_try_from_nonzero_int_harness!(i16 => u8, check_nonzero_u8_try_from_nonzero_i16); - generate_nonzero_int_try_from_nonzero_int_harness!(i16 => u16, check_nonzero_u16_try_from_nonzero_i16); - generate_nonzero_int_try_from_nonzero_int_harness!(i16 => usize, check_nonzero_usize_try_from_nonzero_i16); - generate_nonzero_int_try_from_nonzero_int_harness!(i32 => u8, check_nonzero_u8_try_from_nonzero_i32); - generate_nonzero_int_try_from_nonzero_int_harness!(i32 => u16, check_nonzero_u16_try_from_nonzero_i32); - generate_nonzero_int_try_from_nonzero_int_harness!(i32 => u32, check_nonzero_u32_try_from_nonzero_i32); - generate_nonzero_int_try_from_nonzero_int_harness!(i32 => usize, check_nonzero_usize_try_from_nonzero_i32); - generate_nonzero_int_try_from_nonzero_int_harness!(i64 => u8, check_nonzero_u8_try_from_nonzero_i64); - generate_nonzero_int_try_from_nonzero_int_harness!(i64 => u16, check_nonzero_u16_try_from_nonzero_i64); - generate_nonzero_int_try_from_nonzero_int_harness!(i64 => u32, check_nonzero_u32_try_from_nonzero_i64); - generate_nonzero_int_try_from_nonzero_int_harness!(i64 => u64, check_nonzero_u64_try_from_nonzero_i64); - generate_nonzero_int_try_from_nonzero_int_harness!(i64 => usize, check_nonzero_usize_try_from_nonzero_i64); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u8, check_nonzero_u8_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u16, check_nonzero_u16_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u32, check_nonzero_u32_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u64, check_nonzero_u64_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => u128, check_nonzero_u128_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(i128 => usize, check_nonzero_usize_try_from_nonzero_i128); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => u8, check_nonzero_u8_try_from_nonzero_isize); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => u16, check_nonzero_u16_try_from_nonzero_isize); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => u32, check_nonzero_u32_try_from_nonzero_isize); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => u64, check_nonzero_u64_try_from_nonzero_isize); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => u128, check_nonzero_u128_try_from_nonzero_isize); - generate_nonzero_int_try_from_nonzero_int_harness!(isize => usize, check_nonzero_usize_try_from_nonzero_isize); + generate_nonzero_int_try_from_nonzero_int_harness!( + i8 => u8, + check_nonzero_u8_try_from_nonzero_i8, + check_nonzero_u8_try_from_nonzero_i8_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i16 => u8, + check_nonzero_u8_try_from_nonzero_i16, + check_nonzero_u8_try_from_nonzero_i16_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i16 => u16, + check_nonzero_u16_try_from_nonzero_i16, + check_nonzero_u16_try_from_nonzero_i16_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i16 => usize, + check_nonzero_usize_try_from_nonzero_i16, + check_nonzero_usize_try_from_nonzero_i16_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i32 => u8, + check_nonzero_u8_try_from_nonzero_i32, + check_nonzero_u8_try_from_nonzero_i32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i32 => u16, + check_nonzero_u16_try_from_nonzero_i32, + check_nonzero_u16_try_from_nonzero_i32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i32 => u32, + check_nonzero_u32_try_from_nonzero_i32, + check_nonzero_u32_try_from_nonzero_i32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i32 => usize, + check_nonzero_usize_try_from_nonzero_i32, + check_nonzero_usize_try_from_nonzero_i32_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => u8, + check_nonzero_u8_try_from_nonzero_i64, + check_nonzero_u8_try_from_nonzero_i64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => u16, + check_nonzero_u16_try_from_nonzero_i64, + check_nonzero_u16_try_from_nonzero_i64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => u32, + check_nonzero_u32_try_from_nonzero_i64, + check_nonzero_u32_try_from_nonzero_i64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => u64, + check_nonzero_u64_try_from_nonzero_i64, + check_nonzero_u64_try_from_nonzero_i64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => usize, + check_nonzero_usize_try_from_nonzero_i64, + check_nonzero_usize_try_from_nonzero_i64_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => u8, + check_nonzero_u8_try_from_nonzero_i128, + check_nonzero_u8_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => u16, + check_nonzero_u16_try_from_nonzero_i128, + check_nonzero_u16_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => u32, + check_nonzero_u32_try_from_nonzero_i128, + check_nonzero_u32_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => u64, + check_nonzero_u64_try_from_nonzero_i128, + check_nonzero_u64_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => u128, + check_nonzero_u128_try_from_nonzero_i128, + check_nonzero_u128_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + i128 => usize, + check_nonzero_usize_try_from_nonzero_i128, + check_nonzero_usize_try_from_nonzero_i128_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => u8, + check_nonzero_u8_try_from_nonzero_isize, + check_nonzero_u8_try_from_nonzero_isize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => u16, + check_nonzero_u16_try_from_nonzero_isize, + check_nonzero_u16_try_from_nonzero_isize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => u32, + check_nonzero_u32_try_from_nonzero_isize, + check_nonzero_u32_try_from_nonzero_isize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => u64, + check_nonzero_u64_try_from_nonzero_isize, + check_nonzero_u64_try_from_nonzero_isize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => u128, + check_nonzero_u128_try_from_nonzero_isize, + check_nonzero_u128_try_from_nonzero_isize_should_panic, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => usize, + check_nonzero_usize_try_from_nonzero_isize, + check_nonzero_usize_try_from_nonzero_isize_should_panic, + ); macro_rules! generate_float_to_int_harness { ($Float:ty => $Int:ty, $harness:ident) => { From f719688da4dc5c8ac490946b573d53530697b17d Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Sat, 4 Jan 2025 10:35:45 +0900 Subject: [PATCH 05/11] Handle some infallible cases --- library/core/src/convert/num.rs | 127 +++++++++++++++++++++++++++++--- 1 file changed, 117 insertions(+), 10 deletions(-) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 07eec1798d7a9..209ae5a9de270 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -632,6 +632,13 @@ mod verify { let _ = NonZero::<$target>::try_from(x).unwrap(); } }; + ($source:ty => $target:ty, $harness_infallible:ident,) => { + #[kani::proof] + pub fn $harness_infallible() { + let x: NonZero::<$source> = kani::any(); + let _ = NonZero::<$target>::try_from(x).unwrap(); + } + } } // unsigned non-zero integer -> unsigned non-zero integer fallible @@ -650,11 +657,20 @@ mod verify { check_nonzero_u16_try_from_nonzero_u32, check_nonzero_u16_try_from_nonzero_u32_should_panic, ); + + #[cfg(target_pointer_width = "16")] generate_nonzero_int_try_from_nonzero_int_harness!( u32 => usize, check_nonzero_usize_try_from_nonzero_u32, check_nonzero_usize_try_from_nonzero_u32_should_panic, ); + + #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] + generate_nonzero_int_try_from_nonzero_int_harness!( + u32 => usize, + check_nonzero_usize_try_from_nonzero_u32_infallible, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( u64 => u8, check_nonzero_u8_try_from_nonzero_u64, @@ -670,11 +686,20 @@ mod verify { check_nonzero_u32_try_from_nonzero_u64, check_nonzero_u32_try_from_nonzero_u64_should_panic, ); + + #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] generate_nonzero_int_try_from_nonzero_int_harness!( u64 => usize, check_nonzero_usize_try_from_nonzero_u64, check_nonzero_usize_try_from_nonzero_u64_should_panic, ); + + #[cfg(target_pointer_width = "64")] + generate_nonzero_int_try_from_nonzero_int_harness!( + u64 => usize, + check_nonzero_usize_try_from_nonzero_u64_infallible, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( u128 => u8, check_nonzero_u8_try_from_nonzero_u128, @@ -705,25 +730,40 @@ mod verify { check_nonzero_u8_try_from_nonzero_usize, check_nonzero_u8_try_from_nonzero_usize_should_panic, ); + + #[cfg(target_pointer_width = "16")] + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => u16, + check_nonzero_u16_try_from_nonzero_usize_infallible, + ); + + #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] generate_nonzero_int_try_from_nonzero_int_harness!( usize => u16, check_nonzero_u16_try_from_nonzero_usize, check_nonzero_u16_try_from_nonzero_usize_should_panic, ); + + #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => u32, + check_nonzero_u32_try_from_nonzero_usize_infallible, + ); + + #[cfg(target_pointer_width = "64")] generate_nonzero_int_try_from_nonzero_int_harness!( usize => u32, check_nonzero_u32_try_from_nonzero_usize, check_nonzero_u32_try_from_nonzero_usize_should_panic, ); + generate_nonzero_int_try_from_nonzero_int_harness!( usize => u64, - check_nonzero_u64_try_from_nonzero_usize, - check_nonzero_u64_try_from_nonzero_usize_should_panic, + check_nonzero_u64_try_from_nonzero_usize_infallible, ); generate_nonzero_int_try_from_nonzero_int_harness!( usize => u128, - check_nonzero_u128_try_from_nonzero_usize, - check_nonzero_u128_try_from_nonzero_usize_should_panic, + check_nonzero_u128_try_from_nonzero_usize_infallible, ); // signed non-zero integer -> signed non-zero integer fallible @@ -742,11 +782,20 @@ mod verify { check_nonzero_i16_try_from_nonzero_i32, check_nonzero_i16_try_from_nonzero_i32_should_panic, ); + + #[cfg(target_pointer_width = "16")] generate_nonzero_int_try_from_nonzero_int_harness!( i32 => isize, check_nonzero_isize_try_from_nonzero_i32, check_nonzero_isize_try_from_nonzero_i32_should_panic, ); + + #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] + generate_nonzero_int_try_from_nonzero_int_harness!( + i32 => isize, + check_nonzero_isize_try_from_nonzero_i32_infallible, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( i64 => i8, check_nonzero_i8_try_from_nonzero_i64, @@ -762,11 +811,20 @@ mod verify { check_nonzero_i32_try_from_nonzero_i64, check_nonzero_i32_try_from_nonzero_i64_should_panic, ); + + #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] generate_nonzero_int_try_from_nonzero_int_harness!( i64 => isize, check_nonzero_isize_try_from_nonzero_i64, check_nonzero_isize_try_from_nonzero_i64_should_panic, ); + + #[cfg(target_pointer_width = "64")] + generate_nonzero_int_try_from_nonzero_int_harness!( + i64 => isize, + check_nonzero_isize_try_from_nonzero_i64_infallible, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( i128 => i8, check_nonzero_i8_try_from_nonzero_i128, @@ -797,25 +855,40 @@ mod verify { check_nonzero_i8_try_from_nonzero_isize, check_nonzero_i8_try_from_nonzero_isize_should_panic, ); + + #[cfg(target_pointer_width = "16")] + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => i16, + check_nonzero_i16_try_from_nonzero_isize_infallible, + ); + + #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] generate_nonzero_int_try_from_nonzero_int_harness!( isize => i16, check_nonzero_i16_try_from_nonzero_isize, check_nonzero_i16_try_from_nonzero_isize_should_panic, ); + + #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] + generate_nonzero_int_try_from_nonzero_int_harness!( + isize => i32, + check_nonzero_i32_try_from_nonzero_isize_infallible, + ); + + #[cfg(target_pointer_width = "64")] generate_nonzero_int_try_from_nonzero_int_harness!( isize => i32, check_nonzero_i32_try_from_nonzero_isize, check_nonzero_i32_try_from_nonzero_isize_should_panic, ); + generate_nonzero_int_try_from_nonzero_int_harness!( isize => i64, - check_nonzero_i64_try_from_nonzero_isize, - check_nonzero_i64_try_from_nonzero_isize_should_panic, + check_nonzero_i64_try_from_nonzero_isize_infallible, ); generate_nonzero_int_try_from_nonzero_int_harness!( isize => i128, - check_nonzero_i128_try_from_nonzero_isize, - check_nonzero_i128_try_from_nonzero_isize_should_panic, + check_nonzero_i128_try_from_nonzero_isize_infallible, ); // unsigned non-zero integer -> signed non-zero integer fallible @@ -834,11 +907,20 @@ mod verify { check_nonzero_i16_try_from_nonzero_u16, check_nonzero_i16_try_from_nonzero_u16_should_panic, ); + + #[cfg(target_pointer_width = "16")] generate_nonzero_int_try_from_nonzero_int_harness!( u16 => isize, check_nonzero_isize_try_from_nonzero_u16, check_nonzero_isize_try_from_nonzero_u16_should_panic, ); + + #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] + generate_nonzero_int_try_from_nonzero_int_harness!( + u16 => isize, + check_nonzero_isize_try_from_nonzero_u16_infallible, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( u32 => i8, check_nonzero_i8_try_from_nonzero_u32, @@ -854,11 +936,20 @@ mod verify { check_nonzero_i32_try_from_nonzero_u32, check_nonzero_i32_try_from_nonzero_u32_should_panic, ); + + #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] generate_nonzero_int_try_from_nonzero_int_harness!( u32 => isize, check_nonzero_isize_try_from_nonzero_u32, check_nonzero_isize_try_from_nonzero_u32_should_panic, ); + + #[cfg(target_pointer_width = "64")] + generate_nonzero_int_try_from_nonzero_int_harness!( + u32 => isize, + check_nonzero_isize_try_from_nonzero_u32_infallible, + ); + generate_nonzero_int_try_from_nonzero_int_harness!( u64 => i8, check_nonzero_i8_try_from_nonzero_u64, @@ -924,20 +1015,36 @@ mod verify { check_nonzero_i16_try_from_nonzero_usize, check_nonzero_i16_try_from_nonzero_usize_should_panic, ); + + #[cfg(target_pointer_width = "16")] + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => i32, + check_nonzero_i32_try_from_nonzero_usize_infallible, + ); + + #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] generate_nonzero_int_try_from_nonzero_int_harness!( usize => i32, check_nonzero_i32_try_from_nonzero_usize, check_nonzero_i32_try_from_nonzero_usize_should_panic, ); + + #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] + generate_nonzero_int_try_from_nonzero_int_harness!( + usize => i64, + check_nonzero_i64_try_from_nonzero_usize_infallible, + ); + + #[cfg(target_pointer_width = "64")] generate_nonzero_int_try_from_nonzero_int_harness!( usize => i64, check_nonzero_i64_try_from_nonzero_usize, check_nonzero_i64_try_from_nonzero_usize_should_panic, ); + generate_nonzero_int_try_from_nonzero_int_harness!( usize => i128, - check_nonzero_i128_try_from_nonzero_usize, - check_nonzero_i128_try_from_nonzero_usize_should_panic, + check_nonzero_i128_try_from_nonzero_usize_infallible, ); generate_nonzero_int_try_from_nonzero_int_harness!( usize => isize, From fa12ca7784f33200b028d3f41e0195cd6d148b48 Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Sat, 4 Jan 2025 11:06:25 +0900 Subject: [PATCH 06/11] fmt --- library/core/src/convert/num.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 209ae5a9de270..21234b4a33324 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -614,8 +614,8 @@ mod verify { #[kani::proof] pub fn $harness_pass() { let x_inner: $source = kani::any_where(|&v| { - (v > 0 && (v as u128) <= (<$target>::MAX as u128)) || - (v < 0 && (v as i128) >= (<$target>::MIN as i128)) + (v > 0 && (v as u128) <= (<$target>::MAX as u128)) + || (v < 0 && (v as i128) >= (<$target>::MIN as i128)) }); let x = NonZero::new(x_inner).unwrap(); let _ = NonZero::<$target>::try_from(x).unwrap(); @@ -625,8 +625,8 @@ mod verify { #[kani::should_panic] pub fn $harness_panic() { let x_inner: $source = kani::any_where(|&v| { - (v > 0 && (v as u128) > (<$target>::MAX as u128)) || - (v < 0 && (v as i128) < (<$target>::MIN as i128)) + (v > 0 && (v as u128) > (<$target>::MAX as u128)) + || (v < 0 && (v as i128) < (<$target>::MIN as i128)) }); let x = NonZero::new(x_inner).unwrap(); let _ = NonZero::<$target>::try_from(x).unwrap(); @@ -635,10 +635,10 @@ mod verify { ($source:ty => $target:ty, $harness_infallible:ident,) => { #[kani::proof] pub fn $harness_infallible() { - let x: NonZero::<$source> = kani::any(); + let x: NonZero<$source> = kani::any(); let _ = NonZero::<$target>::try_from(x).unwrap(); } - } + }; } // unsigned non-zero integer -> unsigned non-zero integer fallible From bd26c0ba3b83b5f877f1e47138e0267f8e5157aa Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Sat, 4 Jan 2025 11:47:13 +0900 Subject: [PATCH 07/11] fix --- library/core/src/convert/num.rs | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 21234b4a33324..14f6c46066a47 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -1,9 +1,8 @@ -use crate::num::TryFromIntError; use safety::requires; #[cfg(kani)] use crate::kani; - +use crate::num::TryFromIntError; #[allow(unused_imports)] use crate::ub_checks::float_to_int_in_range; @@ -966,9 +965,9 @@ mod verify { check_nonzero_i32_try_from_nonzero_u64_should_panic, ); generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => u64, - check_nonzero_u64_try_from_nonzero_u64, - check_nonzero_u64_try_from_nonzero_u64_should_panic, + u64 => i64, + check_nonzero_i64_try_from_nonzero_u64, + check_nonzero_i64_try_from_nonzero_u64_should_panic, ); generate_nonzero_int_try_from_nonzero_int_harness!( u64 => isize, From 8b1ead26dcc7539c7ecfb58c3b26729cdda0915e Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Thu, 9 Jan 2025 01:38:21 +0900 Subject: [PATCH 08/11] Remove redundant requirement condition --- library/core/src/convert/num.rs | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 14f6c46066a47..69f16801b9952 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -32,9 +32,7 @@ macro_rules! impl_float_to_int { impl FloatToInt<$Int> for $Float { #[inline] #[requires( - !self.is_nan() && - self.is_finite() && - float_to_int_in_range::<$Float, $Int>(self) + self.is_finite() && float_to_int_in_range::<$Float, $Int>(self) )] unsafe fn to_int_unchecked(self) -> $Int { // SAFETY: the safety contract must be upheld by the caller. From 5326b61448647a307d26a13a42830eb9c0b2046f Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Wed, 22 Jan 2025 13:26:28 +0900 Subject: [PATCH 09/11] Simplify harness generations with more macros --- library/core/src/convert/num.rs | 799 +++++++++----------------------- 1 file changed, 211 insertions(+), 588 deletions(-) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 69f16801b9952..17d2c00fca58d 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -565,49 +565,63 @@ mod verify { }; } - // non-zero unsigned integer -> non-zero unsigned integer - generate_nonzero_int_from_nonzero_int_harness!(u8 => u16, check_nonzero_u16_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u8 => u32, check_nonzero_u32_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u8 => u64, check_nonzero_u64_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u8 => u128, check_nonzero_u128_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u8 => usize, check_nonzero_usize_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u16 => u32, check_nonzero_u32_from_nonzero_u16); - generate_nonzero_int_from_nonzero_int_harness!(u16 => u64, check_nonzero_u64_from_nonzero_u16); - generate_nonzero_int_from_nonzero_int_harness!(u16 => u128, check_nonzero_u128_from_nonzero_u16); - generate_nonzero_int_from_nonzero_int_harness!(u16 => usize, check_nonzero_usize_from_nonzero_u16); - generate_nonzero_int_from_nonzero_int_harness!(u32 => u64, check_nonzero_u64_from_nonzero_u32); - generate_nonzero_int_from_nonzero_int_harness!(u32 => u128, check_nonzero_u128_from_nonzero_u32); - generate_nonzero_int_from_nonzero_int_harness!(u64 => u128, check_nonzero_u128_from_nonzero_u64); - - // non-zero signed integer -> non-zero signed integer - generate_nonzero_int_from_nonzero_int_harness!(i8 => i16, check_nonzero_i16_from_nonzero_i8); - generate_nonzero_int_from_nonzero_int_harness!(i8 => i32, check_nonzero_i32_from_nonzero_i8); - generate_nonzero_int_from_nonzero_int_harness!(i8 => i64, check_nonzero_i64_from_nonzero_i8); - generate_nonzero_int_from_nonzero_int_harness!(i8 => i128, check_nonzero_i128_from_nonzero_i8); - generate_nonzero_int_from_nonzero_int_harness!(i8 => isize, check_nonzero_isize_from_nonzero_i8); - generate_nonzero_int_from_nonzero_int_harness!(i16 => i32, check_nonzero_i32_from_nonzero_i16); - generate_nonzero_int_from_nonzero_int_harness!(i16 => i64, check_nonzero_i64_from_nonzero_i16); - generate_nonzero_int_from_nonzero_int_harness!(i16 => i128, check_nonzero_i128_from_nonzero_i16); - generate_nonzero_int_from_nonzero_int_harness!(i16 => isize, check_nonzero_isize_from_nonzero_i16); - generate_nonzero_int_from_nonzero_int_harness!(i32 => i64, check_nonzero_i64_from_nonzero_i32); - generate_nonzero_int_from_nonzero_int_harness!(i32 => i128, check_nonzero_i128_from_nonzero_i32); - generate_nonzero_int_from_nonzero_int_harness!(i64 => i128, check_nonzero_i128_from_nonzero_i64); - - // non-zero unsigned integer -> non-zero signed integer - generate_nonzero_int_from_nonzero_int_harness!(u8 => i16, check_nonzero_i16_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u8 => i32, check_nonzero_i32_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u8 => i64, check_nonzero_i64_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u8 => i128, check_nonzero_i128_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u8 => isize, check_nonzero_isize_from_nonzero_u8); - generate_nonzero_int_from_nonzero_int_harness!(u16 => i32, check_nonzero_i32_from_nonzero_u16); - generate_nonzero_int_from_nonzero_int_harness!(u16 => i64, check_nonzero_i64_from_nonzero_u16); - generate_nonzero_int_from_nonzero_int_harness!(u16 => i128, check_nonzero_i128_from_nonzero_u16); - generate_nonzero_int_from_nonzero_int_harness!(u32 => i64, check_nonzero_i64_from_nonzero_u32); - generate_nonzero_int_from_nonzero_int_harness!(u32 => i128, check_nonzero_i128_from_nonzero_u32); - generate_nonzero_int_from_nonzero_int_harness!(u64 => i128, check_nonzero_i128_from_nonzero_u64); + macro_rules! generate_nonzero_int_from_nonzero_int_harnesses { + ($ns:ident, $Small:ty => $($Large:tt),+ $(,)?) => { + mod $ns { + use super::*; + + $( + mod $Large { + use super::*; + + generate_nonzero_int_from_nonzero_int_harness!( + $Small => $Large, + check_nonzero_int_from_nonzero_int + ); + } + )+ + } + }; + } + + // non-zero unsigned integer -> non-zero integer, infallible + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_u8, + u8 => u16, u32, u64, u128, usize, i16, i32, i64, i128, isize, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_u16, + u16 => u32, u64, u128, usize, i32, i64, i128, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_u32, + u32 => u64, u128, i64, i128, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_u64, + u64 => u128, i128, + ); + + // non-zero signed integer -> non-zero signed integer, infallible + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_i8, + i8 => i16, i32, i64, i128, isize, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_i16, + i16 => i32, i64, i128, isize, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_i32, + i32 => i64, i128, + ); + generate_nonzero_int_from_nonzero_int_harnesses!( + check_nonzero_int_from_i64, + i64 => i128, + ); macro_rules! generate_nonzero_int_try_from_nonzero_int_harness { - ($source:ty => $target:ty, $harness_pass:ident, $harness_panic:ident,) => { + ($source:ty => $target:ty, $harness_pass:ident, $harness_panic:ident $(,)?) => { #[kani::proof] pub fn $harness_pass() { let x_inner: $source = kani::any_where(|&v| { @@ -629,7 +643,7 @@ mod verify { let _ = NonZero::<$target>::try_from(x).unwrap(); } }; - ($source:ty => $target:ty, $harness_infallible:ident,) => { + ($source:ty => $target:ty, $harness_infallible:ident $(,)?) => { #[kani::proof] pub fn $harness_infallible() { let x: NonZero<$source> = kani::any(); @@ -638,542 +652,167 @@ mod verify { }; } - // unsigned non-zero integer -> unsigned non-zero integer fallible - generate_nonzero_int_try_from_nonzero_int_harness!( - u16 => u8, - check_nonzero_u8_try_from_nonzero_u16, - check_nonzero_u8_try_from_nonzero_u16_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u32 => u8, - check_nonzero_u8_try_from_nonzero_u32, - check_nonzero_u8_try_from_nonzero_u32_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u32 => u16, - check_nonzero_u16_try_from_nonzero_u32, - check_nonzero_u16_try_from_nonzero_u32_should_panic, - ); - - #[cfg(target_pointer_width = "16")] - generate_nonzero_int_try_from_nonzero_int_harness!( - u32 => usize, - check_nonzero_usize_try_from_nonzero_u32, - check_nonzero_usize_try_from_nonzero_u32_should_panic, - ); + macro_rules! generate_nonzero_int_try_from_nonzero_int_harnesses { + ($ns:ident, $source:ty => ([$($target:tt),* $(,)?], [$($infallible:tt),* $(,)?] $(,)?)) => { + mod $ns { + use super::*; + + $( + mod $target { + use super::*; + + generate_nonzero_int_try_from_nonzero_int_harness!( + $source => $target, + check_nonzero_int_try_from_nonzero_int, + check_nonzero_int_try_from_nonzero_int_should_panic, + ); + } + )* + $( + mod $infallible { + use super::*; + + generate_nonzero_int_try_from_nonzero_int_harness!( + $source => $infallible, + check_nonzero_int_try_from_nonzero_int_infallible, + ); + } + )* + } + }; + } + // unsigned non-zero integer -> non-zero integer fallible #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - u32 => usize, - check_nonzero_usize_try_from_nonzero_u32_infallible, - ); - - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => u8, - check_nonzero_u8_try_from_nonzero_u64, - check_nonzero_u8_try_from_nonzero_u64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => u16, - check_nonzero_u16_try_from_nonzero_u64, - check_nonzero_u16_try_from_nonzero_u64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => u32, - check_nonzero_u32_try_from_nonzero_u64, - check_nonzero_u32_try_from_nonzero_u64_should_panic, - ); - - #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => usize, - check_nonzero_usize_try_from_nonzero_u64, - check_nonzero_usize_try_from_nonzero_u64_should_panic, - ); - - #[cfg(target_pointer_width = "64")] - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => usize, - check_nonzero_usize_try_from_nonzero_u64_infallible, - ); - - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => u8, - check_nonzero_u8_try_from_nonzero_u128, - check_nonzero_u8_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => u16, - check_nonzero_u16_try_from_nonzero_u128, - check_nonzero_u16_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => u32, - check_nonzero_u32_try_from_nonzero_u128, - check_nonzero_u32_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => u64, - check_nonzero_u64_try_from_nonzero_u128, - check_nonzero_u64_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => usize, - check_nonzero_usize_try_from_nonzero_u128, - check_nonzero_usize_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => u8, - check_nonzero_u8_try_from_nonzero_usize, - check_nonzero_u8_try_from_nonzero_usize_should_panic, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u16, + u16 => ( + [u8, i8, i16], + [isize], + ) ); #[cfg(target_pointer_width = "16")] - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => u16, - check_nonzero_u16_try_from_nonzero_usize_infallible, - ); - - #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => u16, - check_nonzero_u16_try_from_nonzero_usize, - check_nonzero_u16_try_from_nonzero_usize_should_panic, - ); - - #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => u32, - check_nonzero_u32_try_from_nonzero_usize_infallible, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u16, + u16 => ( + [u8, i8, i16, isize], + [], + ) ); #[cfg(target_pointer_width = "64")] - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => u32, - check_nonzero_u32_try_from_nonzero_usize, - check_nonzero_u32_try_from_nonzero_usize_should_panic, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u32, + u32 => ( + [u8, u16, i8, i16, i32], + [usize, isize], + ) ); - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => u64, - check_nonzero_u64_try_from_nonzero_usize_infallible, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => u128, - check_nonzero_u128_try_from_nonzero_usize_infallible, - ); - - // signed non-zero integer -> signed non-zero integer fallible - generate_nonzero_int_try_from_nonzero_int_harness!( - i16 => i8, - check_nonzero_i8_try_from_nonzero_i16, - check_nonzero_i8_try_from_nonzero_i16_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i32 => i8, - check_nonzero_i8_try_from_nonzero_i32, - check_nonzero_i8_try_from_nonzero_i32_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i32 => i16, - check_nonzero_i16_try_from_nonzero_i32, - check_nonzero_i16_try_from_nonzero_i32_should_panic, + #[cfg(target_pointer_width = "32")] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u32, + u32 => ( + [u8, u16, usize, i8, i16, i32], + [isize], + ) ); #[cfg(target_pointer_width = "16")] - generate_nonzero_int_try_from_nonzero_int_harness!( - i32 => isize, - check_nonzero_isize_try_from_nonzero_i32, - check_nonzero_isize_try_from_nonzero_i32_should_panic, - ); - - #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - i32 => isize, - check_nonzero_isize_try_from_nonzero_i32_infallible, - ); - - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => i8, - check_nonzero_i8_try_from_nonzero_i64, - check_nonzero_i8_try_from_nonzero_i64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => i16, - check_nonzero_i16_try_from_nonzero_i64, - check_nonzero_i16_try_from_nonzero_i64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => i32, - check_nonzero_i32_try_from_nonzero_i64, - check_nonzero_i32_try_from_nonzero_i64_should_panic, - ); - - #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => isize, - check_nonzero_isize_try_from_nonzero_i64, - check_nonzero_isize_try_from_nonzero_i64_should_panic, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u32, + u32 => ( + [u8, u16, usize, i8, i16, i32, isize], + [], + ) ); #[cfg(target_pointer_width = "64")] - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => isize, - check_nonzero_isize_try_from_nonzero_i64_infallible, - ); - - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => i8, - check_nonzero_i8_try_from_nonzero_i128, - check_nonzero_i8_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => i16, - check_nonzero_i16_try_from_nonzero_i128, - check_nonzero_i16_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => i32, - check_nonzero_i32_try_from_nonzero_i128, - check_nonzero_i32_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => i64, - check_nonzero_i64_try_from_nonzero_i128, - check_nonzero_i64_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => isize, - check_nonzero_isize_try_from_nonzero_i128, - check_nonzero_isize_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => i8, - check_nonzero_i8_try_from_nonzero_isize, - check_nonzero_i8_try_from_nonzero_isize_should_panic, - ); - - #[cfg(target_pointer_width = "16")] - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => i16, - check_nonzero_i16_try_from_nonzero_isize_infallible, - ); - - #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => i16, - check_nonzero_i16_try_from_nonzero_isize, - check_nonzero_i16_try_from_nonzero_isize_should_panic, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u64, + u64 => ( + [u8, u16, u32, i8, i16, i32, i64, isize], + [usize], + ) ); #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => i32, - check_nonzero_i32_try_from_nonzero_isize_infallible, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u64, + u64 => ( + [u8, u16, u32, usize, i8, i16, i32, i64, isize], + [], + ) ); - #[cfg(target_pointer_width = "64")] - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => i32, - check_nonzero_i32_try_from_nonzero_isize, - check_nonzero_i32_try_from_nonzero_isize_should_panic, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_u128, + u128 => ( + [u8, u16, u32, u64, usize, i8, i16, i32, i64, i128, isize], + [], + ) ); - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => i64, - check_nonzero_i64_try_from_nonzero_isize_infallible, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => i128, - check_nonzero_i128_try_from_nonzero_isize_infallible, + // signed non-zero integer -> non-zero integer fallible + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i8, + i8 => ( + [u8, u16, u32, u64, u128, usize], + [], + ) ); - // unsigned non-zero integer -> signed non-zero integer fallible - generate_nonzero_int_try_from_nonzero_int_harness!( - u8 => i8, - check_nonzero_i8_try_from_nonzero_u8, - check_nonzero_i8_try_from_nonzero_u8_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u16 => i8, - check_nonzero_i8_try_from_nonzero_u16, - check_nonzero_i8_try_from_nonzero_u16_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u16 => i16, - check_nonzero_i16_try_from_nonzero_u16, - check_nonzero_i16_try_from_nonzero_u16_should_panic, - ); - - #[cfg(target_pointer_width = "16")] - generate_nonzero_int_try_from_nonzero_int_harness!( - u16 => isize, - check_nonzero_isize_try_from_nonzero_u16, - check_nonzero_isize_try_from_nonzero_u16_should_panic, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i16, + i16 => ( + [u8, u16, u32, u64, u128, usize, i8], + [], + ) ); #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - u16 => isize, - check_nonzero_isize_try_from_nonzero_u16_infallible, - ); - - generate_nonzero_int_try_from_nonzero_int_harness!( - u32 => i8, - check_nonzero_i8_try_from_nonzero_u32, - check_nonzero_i8_try_from_nonzero_u32_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u32 => i16, - check_nonzero_i16_try_from_nonzero_u32, - check_nonzero_i16_try_from_nonzero_u32_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u32 => i32, - check_nonzero_i32_try_from_nonzero_u32, - check_nonzero_i32_try_from_nonzero_u32_should_panic, - ); - - #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - u32 => isize, - check_nonzero_isize_try_from_nonzero_u32, - check_nonzero_isize_try_from_nonzero_u32_should_panic, - ); - - #[cfg(target_pointer_width = "64")] - generate_nonzero_int_try_from_nonzero_int_harness!( - u32 => isize, - check_nonzero_isize_try_from_nonzero_u32_infallible, - ); - - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => i8, - check_nonzero_i8_try_from_nonzero_u64, - check_nonzero_i8_try_from_nonzero_u64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => i16, - check_nonzero_i16_try_from_nonzero_u64, - check_nonzero_i16_try_from_nonzero_u64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => i32, - check_nonzero_i32_try_from_nonzero_u64, - check_nonzero_i32_try_from_nonzero_u64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => i64, - check_nonzero_i64_try_from_nonzero_u64, - check_nonzero_i64_try_from_nonzero_u64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u64 => isize, - check_nonzero_isize_try_from_nonzero_u64, - check_nonzero_isize_try_from_nonzero_u64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => i8, - check_nonzero_i8_try_from_nonzero_u128, - check_nonzero_i8_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => i16, - check_nonzero_i16_try_from_nonzero_u128, - check_nonzero_i16_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => i32, - check_nonzero_i32_try_from_nonzero_u128, - check_nonzero_i32_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => i64, - check_nonzero_i64_try_from_nonzero_u128, - check_nonzero_i64_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => i128, - check_nonzero_i128_try_from_nonzero_u128, - check_nonzero_i128_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - u128 => isize, - check_nonzero_isize_try_from_nonzero_u128, - check_nonzero_isize_try_from_nonzero_u128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => i8, - check_nonzero_i8_try_from_nonzero_usize, - check_nonzero_i8_try_from_nonzero_usize_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => i16, - check_nonzero_i16_try_from_nonzero_usize, - check_nonzero_i16_try_from_nonzero_usize_should_panic, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i32, + i32 => ( + [u8, u16, u32, u64, u128, usize, i8, i16], + [isize], + ) ); #[cfg(target_pointer_width = "16")] - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => i32, - check_nonzero_i32_try_from_nonzero_usize_infallible, - ); - - #[cfg(any(target_pointer_width = "32", target_pointer_width = "64"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => i32, - check_nonzero_i32_try_from_nonzero_usize, - check_nonzero_i32_try_from_nonzero_usize_should_panic, - ); - - #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => i64, - check_nonzero_i64_try_from_nonzero_usize_infallible, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i32, + i32 => ( + [u8, u16, u32, u64, u128, usize, i8, i16, isize], + [], + ) ); #[cfg(target_pointer_width = "64")] - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => i64, - check_nonzero_i64_try_from_nonzero_usize, - check_nonzero_i64_try_from_nonzero_usize_should_panic, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i64, + i64 => ( + [u8, u16, u32, u64, u128, usize, i8, i16, i32], + [isize], + ) ); - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => i128, - check_nonzero_i128_try_from_nonzero_usize_infallible, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - usize => isize, - check_nonzero_isize_try_from_nonzero_usize, - check_nonzero_isize_try_from_nonzero_usize_should_panic, + #[cfg(any(target_pointer_width = "16", target_pointer_width = "32"))] + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i64, + i64 => ( + [u8, u16, u32, u64, u128, usize, i8, i16, i32, isize], + [], + ) ); - // signed non-zero integer -> unsigned non-zero integer fallible - generate_nonzero_int_try_from_nonzero_int_harness!( - i8 => u8, - check_nonzero_u8_try_from_nonzero_i8, - check_nonzero_u8_try_from_nonzero_i8_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i16 => u8, - check_nonzero_u8_try_from_nonzero_i16, - check_nonzero_u8_try_from_nonzero_i16_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i16 => u16, - check_nonzero_u16_try_from_nonzero_i16, - check_nonzero_u16_try_from_nonzero_i16_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i16 => usize, - check_nonzero_usize_try_from_nonzero_i16, - check_nonzero_usize_try_from_nonzero_i16_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i32 => u8, - check_nonzero_u8_try_from_nonzero_i32, - check_nonzero_u8_try_from_nonzero_i32_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i32 => u16, - check_nonzero_u16_try_from_nonzero_i32, - check_nonzero_u16_try_from_nonzero_i32_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i32 => u32, - check_nonzero_u32_try_from_nonzero_i32, - check_nonzero_u32_try_from_nonzero_i32_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i32 => usize, - check_nonzero_usize_try_from_nonzero_i32, - check_nonzero_usize_try_from_nonzero_i32_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => u8, - check_nonzero_u8_try_from_nonzero_i64, - check_nonzero_u8_try_from_nonzero_i64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => u16, - check_nonzero_u16_try_from_nonzero_i64, - check_nonzero_u16_try_from_nonzero_i64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => u32, - check_nonzero_u32_try_from_nonzero_i64, - check_nonzero_u32_try_from_nonzero_i64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => u64, - check_nonzero_u64_try_from_nonzero_i64, - check_nonzero_u64_try_from_nonzero_i64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i64 => usize, - check_nonzero_usize_try_from_nonzero_i64, - check_nonzero_usize_try_from_nonzero_i64_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => u8, - check_nonzero_u8_try_from_nonzero_i128, - check_nonzero_u8_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => u16, - check_nonzero_u16_try_from_nonzero_i128, - check_nonzero_u16_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => u32, - check_nonzero_u32_try_from_nonzero_i128, - check_nonzero_u32_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => u64, - check_nonzero_u64_try_from_nonzero_i128, - check_nonzero_u64_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => u128, - check_nonzero_u128_try_from_nonzero_i128, - check_nonzero_u128_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - i128 => usize, - check_nonzero_usize_try_from_nonzero_i128, - check_nonzero_usize_try_from_nonzero_i128_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => u8, - check_nonzero_u8_try_from_nonzero_isize, - check_nonzero_u8_try_from_nonzero_isize_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => u16, - check_nonzero_u16_try_from_nonzero_isize, - check_nonzero_u16_try_from_nonzero_isize_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => u32, - check_nonzero_u32_try_from_nonzero_isize, - check_nonzero_u32_try_from_nonzero_isize_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => u64, - check_nonzero_u64_try_from_nonzero_isize, - check_nonzero_u64_try_from_nonzero_isize_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => u128, - check_nonzero_u128_try_from_nonzero_isize, - check_nonzero_u128_try_from_nonzero_isize_should_panic, - ); - generate_nonzero_int_try_from_nonzero_int_harness!( - isize => usize, - check_nonzero_usize_try_from_nonzero_isize, - check_nonzero_usize_try_from_nonzero_isize_should_panic, + generate_nonzero_int_try_from_nonzero_int_harnesses!( + check_nonzero_int_try_from_i128, + i128 => ( + [u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, isize], + [], + ) ); macro_rules! generate_float_to_int_harness { @@ -1186,53 +825,37 @@ mod verify { }; } + macro_rules! generate_float_to_int_harnesses { + ($ns:ident, $(($Float:tt => $($Int:tt),+ $(,)?)),+ $(,)?) => { + mod $ns { + use super::*; + + $( + mod $Float { + use super::*; + + $( + mod $Int { + use super::*; + + generate_float_to_int_harness!( + $Float => $Int, + check_float_to_int_unchecked + ); + } + )+ + } + )+ + } + }; + } + // float -> integer unchecked - generate_float_to_int_harness!(f16 => u8, check_u8_from_f16_unchecked); - generate_float_to_int_harness!(f16 => u16, check_u16_from_f16_unchecked); - generate_float_to_int_harness!(f16 => u32, check_u32_from_f16_unchecked); - generate_float_to_int_harness!(f16 => u64, check_u64_from_f16_unchecked); - generate_float_to_int_harness!(f16 => u128, check_u128_from_f16_unchecked); - generate_float_to_int_harness!(f16 => usize, check_usize_from_f16_unchecked); - generate_float_to_int_harness!(f16 => i8, check_i8_from_f16_unchecked); - generate_float_to_int_harness!(f16 => i16, check_i16_from_f16_unchecked); - generate_float_to_int_harness!(f16 => i32, check_i32_from_f16_unchecked); - generate_float_to_int_harness!(f16 => i64, check_i64_from_f16_unchecked); - generate_float_to_int_harness!(f16 => i128, check_i128_from_f16_unchecked); - generate_float_to_int_harness!(f16 => isize, check_isize_from_f16_unchecked); - generate_float_to_int_harness!(f32 => u8, check_u8_from_f32_unchecked); - generate_float_to_int_harness!(f32 => u16, check_u16_from_f32_unchecked); - generate_float_to_int_harness!(f32 => u32, check_u32_from_f32_unchecked); - generate_float_to_int_harness!(f32 => u64, check_u64_from_f32_unchecked); - generate_float_to_int_harness!(f32 => u128, check_u128_from_f32_unchecked); - generate_float_to_int_harness!(f32 => usize, check_usize_from_f32_unchecked); - generate_float_to_int_harness!(f32 => i8, check_i8_from_f32_unchecked); - generate_float_to_int_harness!(f32 => i16, check_i16_from_f32_unchecked); - generate_float_to_int_harness!(f32 => i32, check_i32_from_f32_unchecked); - generate_float_to_int_harness!(f32 => i64, check_i64_from_f32_unchecked); - generate_float_to_int_harness!(f32 => i128, check_i128_from_f32_unchecked); - generate_float_to_int_harness!(f32 => isize, check_isize_from_f32_unchecked); - generate_float_to_int_harness!(f64 => u8, check_u8_from_f64_unchecked); - generate_float_to_int_harness!(f64 => u16, check_u16_from_f64_unchecked); - generate_float_to_int_harness!(f64 => u32, check_u32_from_f64_unchecked); - generate_float_to_int_harness!(f64 => u64, check_u64_from_f64_unchecked); - generate_float_to_int_harness!(f64 => u128, check_u128_from_f64_unchecked); - generate_float_to_int_harness!(f64 => usize, check_usize_from_f64_unchecked); - generate_float_to_int_harness!(f64 => i8, check_i8_from_f64_unchecked); - generate_float_to_int_harness!(f64 => i16, check_i16_from_f64_unchecked); - generate_float_to_int_harness!(f64 => i32, check_i32_from_f64_unchecked); - generate_float_to_int_harness!(f64 => i64, check_i64_from_f64_unchecked); - generate_float_to_int_harness!(f64 => i128, check_i128_from_f64_unchecked); - generate_float_to_int_harness!(f64 => isize, check_isize_from_f64_unchecked); - generate_float_to_int_harness!(f128 => u8, check_u8_from_f128_unchecked); - generate_float_to_int_harness!(f128 => u16, check_u16_from_f128_unchecked); - generate_float_to_int_harness!(f128 => u32, check_u32_from_f128_unchecked); - generate_float_to_int_harness!(f128 => u64, check_u64_from_f128_unchecked); - generate_float_to_int_harness!(f128 => u128, check_u128_from_f128_unchecked); - generate_float_to_int_harness!(f128 => usize, check_usize_from_f128_unchecked); - generate_float_to_int_harness!(f128 => i8, check_i8_from_f128_unchecked); - generate_float_to_int_harness!(f128 => i16, check_i16_from_f128_unchecked); - generate_float_to_int_harness!(f128 => i32, check_i32_from_f128_unchecked); - generate_float_to_int_harness!(f128 => i64, check_i64_from_f128_unchecked); - generate_float_to_int_harness!(f128 => i128, check_i128_from_f128_unchecked); - generate_float_to_int_harness!(f128 => isize, check_isize_from_f128_unchecked); + generate_float_to_int_harnesses!( + check_f16_to_int_unchecked, + (f16 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize), + (f32 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize), + (f64 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize), + (f128 => u8, u16, u32, u64, u128, usize, i8, i16, i32, i64, i128, isize), + ); } From b8bd58b0b1ad79c4b874577f0218f89a32262fb4 Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Tue, 11 Feb 2025 22:10:12 +0900 Subject: [PATCH 10/11] Fix mistakes and errors --- library/core/src/convert/num.rs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 17d2c00fca58d..72afc1a7b4de3 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -638,6 +638,7 @@ mod verify { let x_inner: $source = kani::any_where(|&v| { (v > 0 && (v as u128) > (<$target>::MAX as u128)) || (v < 0 && (v as i128) < (<$target>::MIN as i128)) + || (v == 0) }); let x = NonZero::new(x_inner).unwrap(); let _ = NonZero::<$target>::try_from(x).unwrap(); @@ -714,8 +715,8 @@ mod verify { generate_nonzero_int_try_from_nonzero_int_harnesses!( check_nonzero_int_try_from_u32, u32 => ( - [u8, u16, usize, i8, i16, i32], - [isize], + [u8, u16, i8, i16, i32, isize], + [usize], ) ); From f3cbadea01e412c50745f57f1bf529f0b9c7fd52 Mon Sep 17 00:00:00 2001 From: Shoyu Vanilla Date: Wed, 12 Feb 2025 00:01:56 +0900 Subject: [PATCH 11/11] Supplement comments to the harness generating macros --- library/core/src/convert/num.rs | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/library/core/src/convert/num.rs b/library/core/src/convert/num.rs index 72afc1a7b4de3..38200a73b775f 100644 --- a/library/core/src/convert/num.rs +++ b/library/core/src/convert/num.rs @@ -555,6 +555,7 @@ impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize); mod verify { use super::*; + // Generate harnesses for `NonZero::::from(NonZero)`. macro_rules! generate_nonzero_int_from_nonzero_int_harness { ($Small:ty => $Large:ty, $harness:ident) => { #[kani::proof] @@ -565,6 +566,8 @@ mod verify { }; } + // This bundles the calls to `generate_nonzero_int_from_nonzero_int_harness` + // macro into segregated namespaces for better organization and usability. macro_rules! generate_nonzero_int_from_nonzero_int_harnesses { ($ns:ident, $Small:ty => $($Large:tt),+ $(,)?) => { mod $ns { @@ -620,7 +623,12 @@ mod verify { i64 => i128, ); + // Generates harnesses for `NonZero::::try_from(NonZero)`. + // Since the function may be fallible or infallible depending on `source` and `target`, + // this macro supports generating both cases. macro_rules! generate_nonzero_int_try_from_nonzero_int_harness { + // Passing two identities - one for pass and one for panic - generates harnesses + // for fallible cases. ($source:ty => $target:ty, $harness_pass:ident, $harness_panic:ident $(,)?) => { #[kani::proof] pub fn $harness_pass() { @@ -644,6 +652,7 @@ mod verify { let _ = NonZero::<$target>::try_from(x).unwrap(); } }; + // Passing a single identity generates harnesses for infallible cases. ($source:ty => $target:ty, $harness_infallible:ident $(,)?) => { #[kani::proof] pub fn $harness_infallible() { @@ -653,6 +662,11 @@ mod verify { }; } + // This bundles the calls to `generate_nonzero_int_try_from_nonzero_int_harness` + // macro into segregated namespaces for better organization and usability. + // Conversions from the source type to the target types inside the first pair + // of square brackets are fallible, while those to the second pairs are + // infallible. macro_rules! generate_nonzero_int_try_from_nonzero_int_harnesses { ($ns:ident, $source:ty => ([$($target:tt),* $(,)?], [$($infallible:tt),* $(,)?] $(,)?)) => { mod $ns { @@ -816,6 +830,7 @@ mod verify { ) ); + // Generate harnesses for `>::to_int_unchecked(self)`. macro_rules! generate_float_to_int_harness { ($Float:ty => $Int:ty, $harness:ident) => { #[kani::proof_for_contract(<$Float>::to_int_unchecked)] @@ -826,6 +841,8 @@ mod verify { }; } + // This bundles the calls to `generate_float_to_int_harness` macro into segregated + // namespaces for better organization and usability. macro_rules! generate_float_to_int_harnesses { ($ns:ident, $(($Float:tt => $($Int:tt),+ $(,)?)),+ $(,)?) => { mod $ns {