Contracts & Harnesses for to_int_unchecked

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")]
@@ -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<Int>(self) -> Int
     where
         Self: FloatToInt<Int>,

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.
 ///
@@ -1064,6 +1069,8 @@ impl f32 {
                   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<Int>(self) -> Int
     where
         Self: FloatToInt<Int>,

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.
@@ -1065,6 +1069,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<Int>(self) -> Int
     where
         Self: FloatToInt<Int>,

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,61 @@ 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,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
+    //
+    // 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<Int>(self) -> Int where Self: FloatToInt<Int>
+    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
+    );
+
+    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,
+        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
+    );
 }