Contracts & Harnesses for [f16, f128] to_int_unchecked (#163)

Author: MWDZ

library/core/src/num/f128.rs

@@ -17,7 +17,13 @@ use crate::intrinsics;
 use crate::mem;
 use crate::num::FpCategory;
 use crate::panic::const_assert;
+use safety::requires;
 
+#[cfg(kani)]
+use crate::kani;
+
+#[allow(unused_imports)]
+use crate::ub_checks::float_to_int_in_range;
 /// Basic mathematical constants.
 #[unstable(feature = "f128", issue = "116909")]
 pub mod consts {
@@ -869,6 +875,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() && float_to_int_in_range::<Self, Int>(self))]
     pub unsafe fn to_int_unchecked<Int>(self) -> Int
     where
         Self: FloatToInt<Int>,

library/core/src/num/f16.rs

@@ -17,7 +17,13 @@ use crate::intrinsics;
 use crate::mem;
 use crate::num::FpCategory;
 use crate::panic::const_assert;
+use safety::requires;
 
+#[cfg(kani)]
+use crate::kani;
+
+#[allow(unused_imports)]
+use crate::ub_checks::float_to_int_in_range;
 /// Basic mathematical constants.
 #[unstable(feature = "f16", issue = "116909")]
 pub mod consts {
@@ -855,6 +861,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() && float_to_int_in_range::<Self, Int>(self))]
     pub unsafe fn to_int_unchecked<Int>(self) -> Int
     where
         Self: FloatToInt<Int>,

library/core/src/num/mod.rs

@@ -2185,4 +2185,34 @@ mod verify {
         u128, checked_f64_to_int_unchecked_u128,
         usize, checked_f64_to_int_unchecked_usize
     );
+      
+    generate_to_int_unchecked_harness!(f16,
+        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,
+        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
+    );
 }