From 055d1384c6d592e53618e7fc994110f7f6c9396a Mon Sep 17 00:00:00 2001 From: MWDZ Date: Wed, 13 Nov 2024 17:07:47 -0800 Subject: [PATCH 1/7] feat: add f16, f128 to_int harness --- library/core/src/num/f128.rs | 5 ++++ library/core/src/num/f16.rs | 6 ++++ library/core/src/num/mod.rs | 58 ++++++++++++++++++++++++++++++++++++ 3 files changed, 69 insertions(+) diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index e8161cce2fe29..fa5b6df45e84c 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -17,6 +17,9 @@ use crate::intrinsics; use crate::mem; use crate::num::FpCategory; +use safety::{requires, ensures}; +#[cfg(kani)] +use crate::kani; /// Basic mathematical constants. #[unstable(feature = "f128", issue = "116909")] pub mod consts { @@ -881,6 +884,8 @@ impl f128 { #[inline] #[unstable(feature = "f128", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] + // is_finite() checks if the given float is neither infinite nor NaN. + #[requires(self.is_finite() && self >= Self::MIN && self <= Self::MAX)] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, diff --git a/library/core/src/num/f16.rs b/library/core/src/num/f16.rs index 8b3f3b7d19bf7..631dc943ef2da 100644 --- a/library/core/src/num/f16.rs +++ b/library/core/src/num/f16.rs @@ -17,6 +17,10 @@ use crate::intrinsics; use crate::mem; use crate::num::FpCategory; +use safety::{requires, ensures}; + +#[cfg(kani)] +use crate::kani; /// Basic mathematical constants. #[unstable(feature = "f16", issue = "116909")] pub mod consts { @@ -894,6 +898,8 @@ impl f16 { /// # } /// ``` #[inline] + #[requires(!self.is_nan() && !self.is_infinite())] + #[requires(self >= Self::MIN && self <= Self::MAX)] #[unstable(feature = "f16", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] pub const fn to_bits(self) -> u16 { diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 765052e9cbaa6..8f66cf837a2ab 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1843,6 +1843,21 @@ mod verify { } } + // Part 3: Float to Integer Conversion function Harness Generation Macros + macro_rules! generate_to_int_unchecked_harness { + ($floatType:ty, $($intType:ty, $harness_name:ident),+) => { + $( + #[kani::proof_for_contract($floatType::to_int_unchecked)] + pub fn $harness_name() { + let num1: $floatType = kani::any::<$floatType>(); + let result = unsafe { num1.to_int_unchecked::<$intType>() }; + + assert_eq!(result, num1 as $intType); + } + )+ + } + } + // `unchecked_add` proofs // // Target types: @@ -2140,4 +2155,47 @@ mod verify { generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128); generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize); + // `f{16,128}::to_int_unchecked` proofs + // + // Target integer types: + // i{8,128,size} and u{8,16,32,64,128,size} -- 12 types in total + // + // Target contracts: + // 1. Float is not `NaN` and infinite + // 2. Float is representable in the return type `Int`, after truncating + // off its fractional part + // [requires(self.is_finite() && self >= Self::MIN && self <= Self::MAX)] + // + // Target function: + // pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt + generate_to_int_unchecked_harness!(f16, + i8, checked_f128_to_int_unchecked_i8, + i16, checked_f128_to_int_unchecked_i16, + i32, checked_f128_to_int_unchecked_i32, + i64, checked_f128_to_int_unchecked_i64, + i128, checked_f128_to_int_unchecked_i128, + isize, checked_f128_to_int_unchecked_isize, + u8, checked_f128_to_int_unchecked_u8, + u16, checked_f128_to_int_unchecked_u16, + u32, checked_f128_to_int_unchecked_u32, + u64, checked_f128_to_int_unchecked_u64, + u128, checked_f128_to_int_unchecked_u128, + usize, checked_f128_to_int_unchecked_usize + ); + + generate_to_int_unchecked_harness!(f128, + i8, checked_f128_to_int_unchecked_i8, + i16, checked_f128_to_int_unchecked_i16, + i32, checked_f128_to_int_unchecked_i32, + i64, checked_f128_to_int_unchecked_i64, + i128, checked_f128_to_int_unchecked_i128, + isize, checked_f128_to_int_unchecked_isize, + u8, checked_f128_to_int_unchecked_u8, + u16, checked_f128_to_int_unchecked_u16, + u32, checked_f128_to_int_unchecked_u32, + u64, checked_f128_to_int_unchecked_u64, + u128, checked_f128_to_int_unchecked_u128, + usize, checked_f128_to_int_unchecked_usize + ); + } From 1293c9ce200655243e03aa6d8cd03a90623c2b8c Mon Sep 17 00:00:00 2001 From: MWDZ Date: Mon, 25 Nov 2024 15:12:12 -0800 Subject: [PATCH 2/7] fix: add placeholder to to_int_uncheck --- library/core/src/num/f128.rs | 2 +- library/core/src/num/f16.rs | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index fa5b6df45e84c..76357449334a6 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -885,7 +885,7 @@ impl f128 { #[unstable(feature = "f128", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] // is_finite() checks if the given float is neither infinite nor NaN. - #[requires(self.is_finite() && self >= Self::MIN && self <= Self::MAX)] + #[requires(self.is_finite() && /* FIXME */)] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, diff --git a/library/core/src/num/f16.rs b/library/core/src/num/f16.rs index 631dc943ef2da..031dd31ea3da2 100644 --- a/library/core/src/num/f16.rs +++ b/library/core/src/num/f16.rs @@ -869,6 +869,7 @@ impl f16 { #[inline] #[unstable(feature = "f16", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] + #[requires(self.is_finite() && /* FIXME */)] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, @@ -898,8 +899,6 @@ impl f16 { /// # } /// ``` #[inline] - #[requires(!self.is_nan() && !self.is_infinite())] - #[requires(self >= Self::MIN && self <= Self::MAX)] #[unstable(feature = "f16", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] pub const fn to_bits(self) -> u16 { From a9276e61ca34c7d3a7611cbfa8108a2a03b66c26 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Fri, 29 Nov 2024 21:34:24 -0800 Subject: [PATCH 3/7] Fix contracts, import, comments --- library/core/src/num/f128.rs | 4 ++-- library/core/src/num/f16.rs | 5 ++--- library/core/src/num/mod.rs | 14 -------------- 3 files changed, 4 insertions(+), 19 deletions(-) diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index c47ac5f3b3cf7..bc01f19c6abe1 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -17,8 +17,8 @@ use crate::intrinsics; use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; +use safety::requires; -use safety::{requires, ensures}; #[cfg(kani)] use crate::kani; /// Basic mathematical constants. @@ -873,7 +873,7 @@ impl f128 { #[unstable(feature = "f128", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] // is_finite() checks if the given float is neither infinite nor NaN. - #[requires(self.is_finite() && /* FIXME */)] + #[requires(self.is_finite() && kani::float::float_to_int_in_range::(self))] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, diff --git a/library/core/src/num/f16.rs b/library/core/src/num/f16.rs index 218ccbc60adb8..91f275549f16d 100644 --- a/library/core/src/num/f16.rs +++ b/library/core/src/num/f16.rs @@ -17,8 +17,7 @@ use crate::intrinsics; use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; - -use safety::{requires, ensures}; +use safety::requires; #[cfg(kani)] use crate::kani; @@ -859,7 +858,7 @@ impl f16 { #[inline] #[unstable(feature = "f16", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] - #[requires(self.is_finite() && /* FIXME */)] + #[requires(self.is_finite() && kani::float::float_to_int_in_range::(self))] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 7fa3ea9c4f6d4..7a2d32587baeb 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2143,19 +2143,6 @@ mod verify { generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128); generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize); - // `f{16,128}::to_int_unchecked` proofs - // - // Target integer types: - // i{8,128,size} and u{8,16,32,64,128,size} -- 12 types in total - // - // Target contracts: - // 1. Float is not `NaN` and infinite - // 2. Float is representable in the return type `Int`, after truncating - // off its fractional part - // [requires(self.is_finite() && self >= Self::MIN && self <= Self::MAX)] - // - // Target function: - // pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt generate_to_int_unchecked_harness!(f16, i8, checked_f128_to_int_unchecked_i8, i16, checked_f128_to_int_unchecked_i16, @@ -2185,5 +2172,4 @@ mod verify { u128, checked_f128_to_int_unchecked_u128, usize, checked_f128_to_int_unchecked_usize ); - } From 63ae66b0f01d51dad126b7e3672621e0c8c16021 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Fri, 29 Nov 2024 21:37:32 -0800 Subject: [PATCH 4/7] Fix harness names --- library/core/src/num/mod.rs | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 7a2d32587baeb..d22463b24ce44 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1845,7 +1845,7 @@ mod verify { )+ } } - +/* // `unchecked_add` proofs // // Target types: @@ -2141,21 +2141,21 @@ mod verify { generate_wrapping_shift_harness!(u32, wrapping_shr, checked_wrapping_shr_u32); generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64); generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128); - generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize); + generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);*/ generate_to_int_unchecked_harness!(f16, - i8, checked_f128_to_int_unchecked_i8, - i16, checked_f128_to_int_unchecked_i16, - i32, checked_f128_to_int_unchecked_i32, - i64, checked_f128_to_int_unchecked_i64, - i128, checked_f128_to_int_unchecked_i128, - isize, checked_f128_to_int_unchecked_isize, - u8, checked_f128_to_int_unchecked_u8, - u16, checked_f128_to_int_unchecked_u16, - u32, checked_f128_to_int_unchecked_u32, - u64, checked_f128_to_int_unchecked_u64, - u128, checked_f128_to_int_unchecked_u128, - usize, checked_f128_to_int_unchecked_usize + i8, checked_f16_to_int_unchecked_i8, + i16, checked_f16_to_int_unchecked_i16, + i32, checked_f16_to_int_unchecked_i32, + i64, checked_f16_to_int_unchecked_i64, + i128, checked_f16_to_int_unchecked_i128, + isize, checked_f16_to_int_unchecked_isize, + u8, checked_f16_to_int_unchecked_u8, + u16, checked_f16_to_int_unchecked_u16, + u32, checked_f16_to_int_unchecked_u32, + u64, checked_f16_to_int_unchecked_u64, + u128, checked_f16_to_int_unchecked_u128, + usize, checked_f16_to_int_unchecked_usize ); generate_to_int_unchecked_harness!(f128, From 2727cedc4813a34e61ebcc970277c22478441c3e Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 2 Dec 2024 14:11:35 -0800 Subject: [PATCH 5/7] Fix contracts --- library/core/src/num/f128.rs | 3 ++- library/core/src/num/f16.rs | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index bc01f19c6abe1..abb1997bf49e7 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -18,6 +18,7 @@ use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; use safety::requires; +use crate::ub_checks::float_to_int_in_range; #[cfg(kani)] use crate::kani; @@ -873,7 +874,7 @@ impl f128 { #[unstable(feature = "f128", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] // is_finite() checks if the given float is neither infinite nor NaN. - #[requires(self.is_finite() && kani::float::float_to_int_in_range::(self))] + #[requires(self.is_finite() && float_to_int_in_range::(self))] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, diff --git a/library/core/src/num/f16.rs b/library/core/src/num/f16.rs index 91f275549f16d..c5cc617635525 100644 --- a/library/core/src/num/f16.rs +++ b/library/core/src/num/f16.rs @@ -18,6 +18,7 @@ use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; use safety::requires; +use crate::ub_checks::float_to_int_in_range; #[cfg(kani)] use crate::kani; @@ -858,7 +859,7 @@ impl f16 { #[inline] #[unstable(feature = "f16", issue = "116909")] #[must_use = "this returns the result of the operation, without modifying the original"] - #[requires(self.is_finite() && kani::float::float_to_int_in_range::(self))] + #[requires(self.is_finite() && float_to_int_in_range::(self))] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, From 5cae656d9793ef682f204cf5cb709de8bbb76388 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 3 Dec 2024 15:23:46 -0800 Subject: [PATCH 6/7] Fix import --- library/core/src/num/f128.rs | 4 +++- library/core/src/num/f16.rs | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index abb1997bf49e7..896d7684b80cc 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -18,10 +18,12 @@ use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; use safety::requires; -use crate::ub_checks::float_to_int_in_range; #[cfg(kani)] use crate::kani; + +#[cfg(kani)] +use crate::ub_checks::float_to_int_in_range; /// Basic mathematical constants. #[unstable(feature = "f128", issue = "116909")] pub mod consts { diff --git a/library/core/src/num/f16.rs b/library/core/src/num/f16.rs index c5cc617635525..72c27b09857cc 100644 --- a/library/core/src/num/f16.rs +++ b/library/core/src/num/f16.rs @@ -18,10 +18,12 @@ use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; use safety::requires; -use crate::ub_checks::float_to_int_in_range; #[cfg(kani)] use crate::kani; + +#[cfg(kani)] +use crate::ub_checks::float_to_int_in_range; /// Basic mathematical constants. #[unstable(feature = "f16", issue = "116909")] pub mod consts { From 2d3c57f40f9c87261fe31b86853bd59fcc8f5e3b Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 3 Dec 2024 23:22:12 -0800 Subject: [PATCH 7/7] Fix import --- library/core/src/num/f128.rs | 2 +- library/core/src/num/f16.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index 896d7684b80cc..1bccfe4f7f278 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -22,7 +22,7 @@ use safety::requires; #[cfg(kani)] use crate::kani; -#[cfg(kani)] +#[allow(unused_imports)] use crate::ub_checks::float_to_int_in_range; /// Basic mathematical constants. #[unstable(feature = "f128", issue = "116909")] diff --git a/library/core/src/num/f16.rs b/library/core/src/num/f16.rs index 72c27b09857cc..41a37321f4870 100644 --- a/library/core/src/num/f16.rs +++ b/library/core/src/num/f16.rs @@ -22,7 +22,7 @@ use safety::requires; #[cfg(kani)] use crate::kani; -#[cfg(kani)] +#[allow(unused_imports)] use crate::ub_checks::float_to_int_in_range; /// Basic mathematical constants. #[unstable(feature = "f16", issue = "116909")]