Add support for float_to_int_unchecked

docs/src/rust-feature-support/intrinsics.md

@@ -156,7 +156,7 @@ fabsf32 | Yes | |
 fabsf64 | Yes | |
 fadd_fast | Yes | |
 fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
-float_to_int_unchecked | No | |
+float_to_int_unchecked | Partial | [#3629](https://github.com/model-checking/kani/issues/3629) |
 floorf32 | Yes | |
 floorf64 | Yes | |
 fmaf32 | Partial | Results are overapproximated |

kani-compiler/src/intrinsics.rs

@@ -63,6 +63,7 @@ pub enum Intrinsic {
     FabsF64,
     FaddFast,
     FdivFast,
+    FloatToIntUnchecked,
     FloorF32,
     FloorF64,
     FmafF32,
@@ -283,6 +284,14 @@ impl Intrinsic {
                 assert_sig_matches!(sig, _, _ => _);
                 Self::FdivFast
             }
+            "float_to_int_unchecked" => {
+                assert_sig_matches!(sig, RigidTy::Float(_) => _);
+                assert!(matches!(
+                    sig.output().kind(),
+                    TyKind::RigidTy(RigidTy::Int(_)) | TyKind::RigidTy(RigidTy::Uint(_))
+                ));
+                Self::FloatToIntUnchecked
+            }
             "fmul_fast" => {
                 assert_sig_matches!(sig, _, _ => _);
                 Self::FmulFast

kani-compiler/src/main.rs

@@ -16,6 +16,7 @@
 #![feature(f128)]
 #![feature(f16)]
 #![feature(non_exhaustive_omitted_patterns_lint)]
+#![feature(float_next_up_down)]
 extern crate rustc_abi;
 extern crate rustc_ast;
 extern crate rustc_ast_pretty;

tests/expected/intrinsics/float-to-int/non_finite.expected

@@ -0,0 +1,5 @@
+Failed Checks: float_to_int_unchecked: attempt to convert a non-finite value to an integer
+Verification failed for - check_neg_inf
+Verification failed for - check_inf
+Verification failed for - check_nan
+Complete - 0 successfully verified harnesses, 3 failures, 3 total.

tests/expected/intrinsics/float-to-int/non_finite.rs

@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(core_intrinsics)]
+
+//! Check that Kani flags a conversion of a NaN or INFINITY to an int via
+//! `float_to_int_unchecked`
+
+#[kani::proof]
+fn check_nan() {
+    let f: f32 = f32::NAN;
+    let _i: u32 = unsafe { std::intrinsics::float_to_int_unchecked(f) };
+}
+
+#[kani::proof]
+fn check_inf() {
+    let f: f32 = f32::INFINITY;
+    let _i: u32 = unsafe { std::intrinsics::float_to_int_unchecked(f) };
+}
+
+#[kani::proof]
+fn check_neg_inf() {
+    let f: f32 = f32::NEG_INFINITY;
+    let _i: u32 = unsafe { std::intrinsics::float_to_int_unchecked(f) };
+}

tests/expected/intrinsics/float-to-int/oob.expected

@@ -0,0 +1,14 @@
+Failed Checks: float_to_int_unchecked: attempt to convert a value out of range of the target integer
+
+Verification failed for - check_u16_upper
+Verification failed for - check_u64_upper
+Verification failed for - check_usize_upper
+Verification failed for - check_u32_upper
+Verification failed for - check_u8_upper
+Verification failed for - check_u128_lower
+Verification failed for - check_u32_lower
+Verification failed for - check_u8_lower
+Verification failed for - check_u64_lower
+Verification failed for - check_usize_lower
+Verification failed for - check_u16_lower
+Complete - 1 successfully verified harnesses, 11 failures, 12 total.

tests/expected/intrinsics/float-to-int/oob.rs

@@ -0,0 +1,41 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(core_intrinsics)]
+
+//! Check that Kani flags a conversion of an out-of-bounds float value to an int
+//! via `float_to_int_unchecked`
+
+macro_rules! check_unsigned_lower {
+    ($name:ident, $t:ty) => {
+        #[kani::proof]
+        fn $name() {
+            let x: f32 = kani::any_where(|v: &f32| v.is_finite() && *v <= -1.0);
+            let _u: $t = unsafe { std::intrinsics::float_to_int_unchecked(x) };
+        }
+    };
+}
+
+check_unsigned_lower!(check_u8_lower, u8);
+check_unsigned_lower!(check_u16_lower, u16);
+check_unsigned_lower!(check_u32_lower, u32);
+check_unsigned_lower!(check_u64_lower, u64);
+check_unsigned_lower!(check_u128_lower, u128);
+check_unsigned_lower!(check_usize_lower, usize);
+
+macro_rules! check_unsigned_upper {
+    ($name:ident, $t:ty, $v:expr) => {
+        #[kani::proof]
+        fn $name() {
+            let x: f32 = kani::any_where(|v: &f32| v.is_finite() && *v >= $v);
+            let _u: $t = unsafe { std::intrinsics::float_to_int_unchecked(x) };
+        }
+    };
+}
+
+check_unsigned_upper!(check_u8_upper, u8, (1u128 << 8) as f32);
+check_unsigned_upper!(check_u16_upper, u16, (1u128 << 16) as f32);
+check_unsigned_upper!(check_u32_upper, u32, (1u128 << 32) as f32);
+check_unsigned_upper!(check_u64_upper, u64, (1u128 << 64) as f32);
+// this harness should pass
+check_unsigned_upper!(check_u128_upper, u128, f32::INFINITY);
+check_unsigned_upper!(check_usize_upper, usize, (1u128 << 64) as f32);

tests/kani/Intrinsics/FloatToInt/float_to_int.rs

@@ -0,0 +1,49 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(core_intrinsics)]
+
+// Check that the `float_to_int_unchecked` intrinsic works as expected
+
+use std::intrinsics::float_to_int_unchecked;
+
+macro_rules! check_float_to_int_unchecked {
+    ($float_ty:ty, $int_ty:ty) => {
+        let f: $float_ty = kani::any_where(|f: &$float_ty| {
+            f.is_finite() && *f > <$int_ty>::MIN as $float_ty && *f < <$int_ty>::MAX as $float_ty
+        });
+        let u: $int_ty = unsafe { float_to_int_unchecked(f) };
+        assert_eq!(u as $float_ty, f.trunc());
+    };
+}
+
+#[kani::proof]
+fn check_f32_to_int_unchecked() {
+    check_float_to_int_unchecked!(f32, u8);
+    check_float_to_int_unchecked!(f32, u16);
+    check_float_to_int_unchecked!(f32, u32);
+    check_float_to_int_unchecked!(f32, u64);
+    check_float_to_int_unchecked!(f32, u128);
+    check_float_to_int_unchecked!(f32, usize);
+    check_float_to_int_unchecked!(f32, i8);
+    check_float_to_int_unchecked!(f32, i16);
+    check_float_to_int_unchecked!(f32, i32);
+    check_float_to_int_unchecked!(f32, i64);
+    check_float_to_int_unchecked!(f32, i128);
+    check_float_to_int_unchecked!(f32, isize);
+}
+
+#[kani::proof]
+fn check_f64_to_int_unchecked() {
+    check_float_to_int_unchecked!(f64, u8);
+    check_float_to_int_unchecked!(f64, u16);
+    check_float_to_int_unchecked!(f64, u32);
+    check_float_to_int_unchecked!(f64, u64);
+    check_float_to_int_unchecked!(f64, u128);
+    check_float_to_int_unchecked!(f64, usize);
+    check_float_to_int_unchecked!(f64, i8);
+    check_float_to_int_unchecked!(f64, i16);
+    check_float_to_int_unchecked!(f64, i32);
+    check_float_to_int_unchecked!(f64, i64);
+    check_float_to_int_unchecked!(f64, i128);
+    check_float_to_int_unchecked!(f64, isize);
+}