From 95d11f330b67d440ad0ccff4f9a4b375d3cccba9 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 22 Oct 2024 09:46:48 -0700 Subject: [PATCH 01/19] f32 test harness & contracts --- library/core/src/num/f32.rs | 7 +++++++ library/core/src/num/mod.rs | 12 +++++++++++- 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index c1adcc753f2e5..2b17d327c2f04 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -17,6 +17,11 @@ use crate::intrinsics; use crate::mem; use crate::num::FpCategory; +use safety::{requires, ensures}; + +#[cfg(kani)] +use crate::kani; + /// The radix or base of the internal representation of `f32`. /// Use [`f32::RADIX`] instead. /// @@ -1086,6 +1091,8 @@ impl f32 { without modifying the original"] #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] + #[requires(!self.is_nan() && !self.is_infinite())] + #[requires(self >= Self::MIN && self <= Self::MAX)] 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 b123d998a8466..64232558c7a33 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1590,7 +1590,7 @@ from_str_radix_size_impl! { i64 isize, u64 usize } #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; - +/* // Verify `unchecked_{add, sub, mul}` macro_rules! generate_unchecked_math_harness { ($type:ty, $method:ident, $harness_name:ident) => { @@ -1967,4 +1967,14 @@ mod verify { 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); +*/ + + #[kani::proof_for_contract(f32::to_int_unchecked)] + pub fn checked_to_int_unchecked_f32() { + let num1: f32 = kani::any::(); + + let result = unsafe { num1.to_int_unchecked::() }; + + assert_eq!(result, num1 as i32); + } } From 227d9ac7886258bfb62ee42ef87eab0bff92451c Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 23 Oct 2024 21:02:27 -0700 Subject: [PATCH 02/19] Fix contracts && Initial draft of macro and harnesses --- library/core/src/num/f32.rs | 4 +-- library/core/src/num/mod.rs | 53 ++++++++++++++++++++++++++++++------- 2 files changed, 45 insertions(+), 12 deletions(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index 2b17d327c2f04..df21835cbae20 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -1091,8 +1091,8 @@ impl f32 { without modifying the original"] #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] - #[requires(!self.is_nan() && !self.is_infinite())] - #[requires(self >= Self::MIN && self <= Self::MAX)] + // 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/mod.rs b/library/core/src/num/mod.rs index 64232558c7a33..8cdade6d3afb5 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1590,7 +1590,7 @@ from_str_radix_size_impl! { i64 isize, u64 usize } #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; -/* + // Verify `unchecked_{add, sub, mul}` macro_rules! generate_unchecked_math_harness { ($type:ty, $method:ident, $harness_name:ident) => { @@ -1700,6 +1700,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: @@ -1967,14 +1982,32 @@ mod verify { 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); -*/ - - #[kani::proof_for_contract(f32::to_int_unchecked)] - pub fn checked_to_int_unchecked_f32() { - let num1: f32 = kani::any::(); - let result = unsafe { num1.to_int_unchecked::() }; - - assert_eq!(result, num1 as i32); - } + // `f32::to_int_unchecked` proofs + // + // Target integer types: + // i{8,16,32,64,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!(f32, + i8, checked_f32_to_int_unchecked_i8, + i16, checked_f32_to_int_unchecked_i16, + i32, checked_f32_to_int_unchecked_i32, + i64, checked_f32_to_int_unchecked_i64, + i128, checked_f32_to_int_unchecked_i128, + isize, checked_f32_to_int_unchecked_isize, + u8, checked_f32_to_int_unchecked_u8, + u16, checked_f32_to_int_unchecked_u16, + u32, checked_f32_to_int_unchecked_u32, + u64, checked_f32_to_int_unchecked_u64, + u128, checked_f32_to_int_unchecked_u128, + usize, checked_f32_to_int_unchecked_usize + ); } From 082ea5ade17ca30fc01144d9818f6c243b882b19 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Wed, 30 Oct 2024 00:39:47 -0700 Subject: [PATCH 03/19] f128_float_to_int proofs --- library/core/src/num/f128.rs | 5 +++++ library/core/src/num/mod.rs | 30 +++++++++++++++++++++++++++++- 2 files changed, 34 insertions(+), 1 deletion(-) diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index d4236e47bfe3b..47098a8fdd5c8 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -16,6 +16,9 @@ use crate::convert::FloatToInt; 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")] @@ -886,6 +889,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/mod.rs b/library/core/src/num/mod.rs index 8987bc58f1283..3d0634aa2c2b7 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2084,4 +2084,32 @@ mod verify { u128, checked_f32_to_int_unchecked_u128, usize, checked_f32_to_int_unchecked_usize ); -} \ No newline at end of file + + // `f128::to_int_unchecked` proofs + // + // Target integer types: + // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total + // + // Target contracts: + // 1. Float is not `NaN` or 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!(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 bb00a726a36242f9fc8fcb1fadb292732173ebd4 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 30 Oct 2024 09:19:55 -0700 Subject: [PATCH 04/19] Fix comment --- library/core/src/num/mod.rs | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 3d0634aa2c2b7..7b1375eef1b1b 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2057,7 +2057,7 @@ mod verify { generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128); generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize); - // `f32::to_int_unchecked` proofs + // `f{16,32,64,128}::to_int_unchecked` proofs // // Target integer types: // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total @@ -2085,19 +2085,6 @@ mod verify { usize, checked_f32_to_int_unchecked_usize ); - // `f128::to_int_unchecked` proofs - // - // Target integer types: - // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total - // - // Target contracts: - // 1. Float is not `NaN` or 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!(f128, i8, checked_f128_to_int_unchecked_i8, i16, checked_f128_to_int_unchecked_i16, From 573e0a8573c61451d30db24aef26e4491edb2364 Mon Sep 17 00:00:00 2001 From: MWDZ Date: Thu, 7 Nov 2024 00:33:57 -0800 Subject: [PATCH 05/19] f64_float_to_int proofs --- library/core/src/num/f64.rs | 6 ++++++ library/core/src/num/mod.rs | 15 +++++++++++++++ 2 files changed, 21 insertions(+) diff --git a/library/core/src/num/f64.rs b/library/core/src/num/f64.rs index e6406771ad333..8f62d72fbb8e5 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.rs @@ -16,6 +16,10 @@ use crate::convert::FloatToInt; use crate::intrinsics; use crate::mem; use crate::num::FpCategory; +use safety::{requires, ensures}; + +#[cfg(kani)] +use crate::kani; /// The radix or base of the internal representation of `f64`. /// Use [`f64::RADIX`] instead. @@ -1083,6 +1087,8 @@ impl f64 { without modifying the original"] #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] + // 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/mod.rs b/library/core/src/num/mod.rs index 7b1375eef1b1b..7198209b99380 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2085,6 +2085,21 @@ mod verify { usize, checked_f32_to_int_unchecked_usize ); + generate_to_int_unchecked_harness!(f64, + i8, checked_f64_to_int_unchecked_i8, + i16, checked_f64_to_int_unchecked_i16, + i32, checked_f64_to_int_unchecked_i32, + i64, checked_f64_to_int_unchecked_i64, + i128, checked_f64_to_int_unchecked_i128, + isize, checked_f64_to_int_unchecked_isize, + u8, checked_f64_to_int_unchecked_u8, + u16, checked_f64_to_int_unchecked_u16, + u32, checked_f64_to_int_unchecked_u32, + u64, checked_f64_to_int_unchecked_u64, + u128, checked_f64_to_int_unchecked_u128, + usize, checked_f64_to_int_unchecked_usize + ); + generate_to_int_unchecked_harness!(f128, i8, checked_f128_to_int_unchecked_i8, i16, checked_f128_to_int_unchecked_i16, From 454b66b17df6d1ff19e8efd1c535773456b1ddd5 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 13 Nov 2024 12:45:28 -0800 Subject: [PATCH 06/19] Remove f128 proofs; will be added later --- library/core/src/num/mod.rs | 17 +---------------- 1 file changed, 1 insertion(+), 16 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 59a5e551a7e0c..6897d9d084777 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1686,7 +1686,7 @@ from_str_radix_size_impl! { signed i64 isize, unsigned u64 usize } #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] -mod verify { +pub mod verify { use super::*; // Verify `unchecked_{add, sub, mul}` @@ -2197,19 +2197,4 @@ mod verify { u128, checked_f64_to_int_unchecked_u128, usize, checked_f64_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 c2f79317eb2ac9261d1122b7064b61fa74d5e3f2 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 18 Nov 2024 17:10:07 -0800 Subject: [PATCH 07/19] remove f128 contract; will added in PR#163 --- library/core/src/num/f128.rs | 5 ----- 1 file changed, 5 deletions(-) diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index 722d613de3ac7..e8161cce2fe29 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -16,9 +16,6 @@ use crate::convert::FloatToInt; 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")] @@ -884,8 +881,6 @@ 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, From 277216ce2722524528e0847f008dc4a2ac380e94 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 25 Nov 2024 14:58:52 -0800 Subject: [PATCH 08/19] Remove incorrect contract code --- library/core/src/num/f32.rs | 2 +- library/core/src/num/f64.rs | 2 +- library/core/src/num/mod.rs | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index 0952767f369de..b27dfcbee7487 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -1070,7 +1070,7 @@ impl f32 { #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] // 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/f64.rs b/library/core/src/num/f64.rs index 7f41c6547d3d5..b8584c5159e9e 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.rs @@ -1070,7 +1070,7 @@ impl f64 { #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] // 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/mod.rs b/library/core/src/num/mod.rs index 6897d9d084777..834f6f873d3aa 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2164,7 +2164,7 @@ pub mod verify { // 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)] + // [requires(self.is_finite() && /* FIXME */)] // // Target function: // pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt From 26a02d92abad2ce1b0488a4af2469f79c924e986 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 26 Nov 2024 22:50:37 -0800 Subject: [PATCH 09/19] Add placeholder for f32,f64 to_int_unchecked contract --- library/core/src/num/f32.rs | 2 +- library/core/src/num/f64.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index b27dfcbee7487..0d4143fd605ff 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -1070,7 +1070,7 @@ impl f32 { #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] // is_finite() checks if the given float is neither infinite nor NaN. - #[requires(self.is_finite() && /* FIXME */)] + #[requires(self.is_finite() && /* FIXME: 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/f64.rs b/library/core/src/num/f64.rs index b8584c5159e9e..370c99ae62427 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.rs @@ -1070,7 +1070,7 @@ impl f64 { #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] // is_finite() checks if the given float is neither infinite nor NaN. - #[requires(self.is_finite() && /* FIXME */)] + #[requires(self.is_finite() && /* FIXME: kani::float::float_to_int_in_range::(self) */)] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, From 149fe91cd1f0e2d3f56f4aace270bc7dd1483f3e Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 27 Nov 2024 21:17:05 -0800 Subject: [PATCH 10/19] Fix contracts --- library/core/src/num/f32.rs | 2 +- library/core/src/num/f64.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index 0d4143fd605ff..90da14b584f1e 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -1070,7 +1070,7 @@ impl f32 { #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] // is_finite() checks if the given float is neither infinite nor NaN. - #[requires(self.is_finite() && /* FIXME: kani::float::float_to_int_in_range::(self) */)] + #[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/f64.rs b/library/core/src/num/f64.rs index 370c99ae62427..7be0f36737cdb 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.rs @@ -1070,7 +1070,7 @@ impl f64 { #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] // is_finite() checks if the given float is neither infinite nor NaN. - #[requires(self.is_finite() && /* FIXME: kani::float::float_to_int_in_range::(self) */)] + #[requires(self.is_finite() && kani::float::float_to_int_in_range::(self))] pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt, From 3590276aa2de7600016952f2fd0f282ac06529b8 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 27 Nov 2024 23:35:10 -0800 Subject: [PATCH 11/19] Fix code and comments --- library/core/src/num/mod.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 834f6f873d3aa..f71d70af6e0ec 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1686,7 +1686,7 @@ from_str_radix_size_impl! { signed i64 isize, unsigned u64 usize } #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] -pub mod verify { +mod verify { use super::*; // Verify `unchecked_{add, sub, mul}` @@ -1843,7 +1843,7 @@ pub mod verify { } } - // Part 3: Float to Integer Conversion function Harness Generation Macros + // Part 3: Float to Integer Conversion function Harness Generation Macro macro_rules! generate_to_int_unchecked_harness { ($floatType:ty, $($intType:ty, $harness_name:ident),+) => { $( @@ -2164,7 +2164,7 @@ pub mod verify { // 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() && /* FIXME */)] + // [requires(self.is_finite() && kani::float::float_to_int_in_range::(self))] // // Target function: // pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt From 8151c17cabc9b84e83c3ed7aaaf8792a3eaf84f3 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Thu, 28 Nov 2024 15:47:40 -0800 Subject: [PATCH 12/19] Remove unused import --- library/core/src/num/f32.rs | 2 +- library/core/src/num/f64.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index 90da14b584f1e..1a309655d36cc 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -17,7 +17,7 @@ use crate::intrinsics; use crate::mem; use crate::num::FpCategory; -use safety::{requires, ensures}; +use safety::requires; #[cfg(kani)] use crate::kani; diff --git a/library/core/src/num/f64.rs b/library/core/src/num/f64.rs index 7be0f36737cdb..ec1e37f9dfac9 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.rs @@ -16,7 +16,7 @@ use crate::convert::FloatToInt; use crate::intrinsics; use crate::mem; use crate::num::FpCategory; -use safety::{requires, ensures}; +use safety::requires; #[cfg(kani)] use crate::kani; From 1b08327f1023dcaa3c6e7edaae7fb67c9f55a97c Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 2 Dec 2024 13:39:01 -0800 Subject: [PATCH 13/19] Enable float-lib in kani script --- scripts/run-kani.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index e32bb22c23f56..fc6df656578cb 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -214,6 +214,7 @@ main() { -Z function-contracts \ -Z mem-predicates \ -Z loop-contracts \ + -Z float-lib \ --output-format=terse \ $command_args \ --enable-unstable \ From 895f055741b4baf1bd581ba488e01c35eccbadb7 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 2 Dec 2024 14:10:10 -0800 Subject: [PATCH 14/19] Add float_to_int_in_range to ub_checks && Fix contracts --- library/core/src/num/f32.rs | 3 ++- library/core/src/num/f64.rs | 3 ++- library/core/src/ub_checks.rs | 11 +++++++++++ 3 files changed, 15 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index 349d11aa548cf..5742ae8ae4fd5 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -19,6 +19,7 @@ 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; @@ -1060,7 +1061,7 @@ impl f32 { #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] // 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/f64.rs b/library/core/src/num/f64.rs index fb90a20de9044..05f442767782f 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.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; @@ -1060,7 +1061,7 @@ impl f64 { #[stable(feature = "float_approx_unchecked_to", since = "1.44.0")] #[inline] // 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/ub_checks.rs b/library/core/src/ub_checks.rs index 5598c7bb41d38..2856e155f9fbf 100644 --- a/library/core/src/ub_checks.rs +++ b/library/core/src/ub_checks.rs @@ -2,6 +2,7 @@ //! common preconditions. use crate::intrinsics::{self, const_eval_select}; +use crate::convert::FloatToInt; /// Checks that the preconditions of an unsafe function are followed. /// @@ -219,12 +220,22 @@ mod predicates { let _ = (src, dst); true } + + /// Check if a float is representable in the given integer type + pub fn float_to_int_in_range(value: Float) -> bool + where + Float: FloatToInt { + let _ = value; + true + } } #[cfg(kani)] mod predicates { pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned, same_allocation}; + + pub use crate::kani::float::float_to_int_in_range; } /// This trait should be used to specify and check type safety invariants for a From 8aefc7c9ae8c26dadd9022d6d52fb2285ec714cf Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 2 Dec 2024 14:17:27 -0800 Subject: [PATCH 15/19] Fix dummy float_to_int_in_range --- library/core/src/ub_checks.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs index 2856e155f9fbf..bff0c277a61b5 100644 --- a/library/core/src/ub_checks.rs +++ b/library/core/src/ub_checks.rs @@ -224,7 +224,7 @@ mod predicates { /// Check if a float is representable in the given integer type pub fn float_to_int_in_range(value: Float) -> bool where - Float: FloatToInt { + Float: core::convert::FloatToInt { let _ = value; true } @@ -234,7 +234,6 @@ mod predicates { mod predicates { pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned, same_allocation}; - pub use crate::kani::float::float_to_int_in_range; } From e4d69a79d409cf33d11be6d1af22a2321776a6fa Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 3 Dec 2024 11:30:52 -0800 Subject: [PATCH 16/19] Fix import and format --- library/core/src/ub_checks.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs index bff0c277a61b5..9b7a64a43000e 100644 --- a/library/core/src/ub_checks.rs +++ b/library/core/src/ub_checks.rs @@ -2,7 +2,6 @@ //! common preconditions. use crate::intrinsics::{self, const_eval_select}; -use crate::convert::FloatToInt; /// Checks that the preconditions of an unsafe function are followed. /// @@ -224,7 +223,8 @@ mod predicates { /// Check if a float is representable in the given integer type pub fn float_to_int_in_range(value: Float) -> bool where - Float: core::convert::FloatToInt { + Float: core::convert::FloatToInt + { let _ = value; true } From 3afbb9d30a2055dffd831db4e5bf0b4a91ab86bf Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 3 Dec 2024 15:22:33 -0800 Subject: [PATCH 17/19] Fix import --- library/core/src/num/f32.rs | 4 +++- library/core/src/num/f64.rs | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index 5742ae8ae4fd5..816e84a63b1ec 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -19,11 +19,13 @@ 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; + /// The radix or base of the internal representation of `f32`. /// Use [`f32::RADIX`] instead. /// diff --git a/library/core/src/num/f64.rs b/library/core/src/num/f64.rs index 05f442767782f..9729d0aff24b2 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.rs @@ -18,11 +18,13 @@ 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; + /// The radix or base of the internal representation of `f64`. /// Use [`f64::RADIX`] instead. /// From 7b978eb8260969c3a9328f507ff616e6b60f9d7c Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 3 Dec 2024 19:51:38 -0800 Subject: [PATCH 18/19] Add -Z float-lib to list command --- scripts/run-kani.sh | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index fc6df656578cb..a576717849aca 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -221,9 +221,8 @@ main() { --cbmc-args --object-bits 12 elif [[ "$run_command" == "list" ]]; then echo "Running Kani list command..." - "$kani_path" list -Z list -Z function-contracts -Z mem-predicates ./library --std > $path/kani_list.txt + "$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std > $path/kani_list.txt fi } main - From 5efede86649d4008ff31384a19eed7ca5d8658ec Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 3 Dec 2024 23:20:56 -0800 Subject: [PATCH 19/19] Fix import --- library/core/src/num/f32.rs | 2 +- library/core/src/num/f64.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index 816e84a63b1ec..fffc403470508 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -23,7 +23,7 @@ use safety::requires; #[cfg(kani)] use crate::kani; -#[cfg(kani)] +#[allow(unused_imports)] use crate::ub_checks::float_to_int_in_range; /// The radix or base of the internal representation of `f32`. diff --git a/library/core/src/num/f64.rs b/library/core/src/num/f64.rs index 9729d0aff24b2..166fb2d329a5a 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.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; /// The radix or base of the internal representation of `f64`.