Add a Kani function that checks if the range of a float is valid for conversion to int (#3742)

This introduces a new generic Kani function,
`kani::float::float_to_int_in_range`, that can be used for checking if a
floating-point value satisfies the range requirement of the
`to_int_unchecked` methods, e.g
https://doc.rust-lang.org/std/primitive.f32.html#method.to_int_unchecked
and
https://doc.rust-lang.org/std/primitive.f64.html#method.to_int_unchecked.

Resolves #3711 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: zhassan-aws

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -8,8 +8,8 @@
 //! It would be too nasty if we spread around these sort of undocumented hooks in place, so
 //! this module addresses this issue.
 
-use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::codegen_cprover_gotoc::codegen::{PropertyClass, bb_label};
+use crate::codegen_cprover_gotoc::{GotocCtx, utils};
 use crate::kani_middle::attributes;
 use crate::kani_middle::kani_functions::{KaniFunction, KaniHook};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
@@ -19,6 +19,7 @@ use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Place};
+use stable_mir::ty::RigidTy;
 use stable_mir::{CrateDef, ty::Span};
 use std::collections::HashMap;
 use std::rc::Rc;
@@ -315,6 +316,53 @@ impl GotocHook for IsAllocated {
     }
 }
 
+/// This is the hook for the `kani::float::float_to_int_in_range` intrinsic
+/// TODO: This should be replaced by a Rust function instead so that it's
+/// independent of the backend
+struct FloatToIntInRange;
+impl GotocHook for FloatToIntInRange {
+    fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
+        unreachable!("{UNEXPECTED_CALL}")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        instance: Instance,
+        mut fargs: Vec<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 1);
+        let float = fargs.remove(0);
+        let target = target.unwrap();
+        let loc = gcx.codegen_span_stable(span);
+
+        let generic_args = instance.args().0;
+        let RigidTy::Float(float_ty) = *generic_args[0].expect_ty().kind().rigid().unwrap() else {
+            unreachable!()
+        };
+        let integral_ty = generic_args[1].expect_ty().kind().rigid().unwrap().clone();
+
+        let is_in_range = utils::codegen_in_range_expr(
+            &float,
+            float_ty,
+            integral_ty,
+            gcx.symbol_table.machine_model(),
+        )
+        .cast_to(Type::CInteger(CIntType::Bool));
+
+        let pe = unwrap_or_return_codegen_unimplemented_stmt!(
+            gcx,
+            gcx.codegen_place_stable(assign_to, loc)
+        )
+        .goto_expr;
+
+        Stmt::block(vec![pe.assign(is_in_range, loc), Stmt::goto(bb_label(target), loc)], loc)
+    }
+}
+
 /// Encodes __CPROVER_pointer_object(ptr)
 struct PointerObject;
 impl GotocHook for PointerObject {
@@ -663,6 +711,7 @@ pub fn fn_hooks() -> GotocHooks {
         (KaniHook::PointerOffset, Rc::new(PointerOffset)),
         (KaniHook::UntrackedDeref, Rc::new(UntrackedDeref)),
         (KaniHook::InitContracts, Rc::new(InitContracts)),
+        (KaniHook::FloatToIntInRange, Rc::new(FloatToIntInRange)),
     ];
     GotocHooks {
         kani_lib_hooks: HashMap::from(kani_lib_hooks),

kani-compiler/src/kani_middle/kani_functions.rs

@@ -125,6 +125,9 @@ pub enum KaniHook {
     Check,
     #[strum(serialize = "CoverHook")]
     Cover,
+    // TODO: this is temporarily implemented as a hook, but should be implemented as an intrinsic
+    #[strum(serialize = "FloatToIntInRangeHook")]
+    FloatToIntInRange,
     #[strum(serialize = "InitContractsHook")]
     InitContracts,
     #[strum(serialize = "IsAllocatedHook")]

kani_metadata/src/unstable.rs

@@ -100,6 +100,8 @@ pub enum UnstableFeature {
     UnstableOptions,
     /// The list subcommand [RFC 13](https://model-checking.github.io/kani/rfc/rfcs/0013-list.html)
     List,
+    /// Kani APIs related to floating-point operations (e.g. `float_to_int_in_range`)
+    FloatLib,
 }
 
 impl UnstableFeature {

library/kani/src/lib.rs

@@ -20,6 +20,7 @@
 #![feature(ptr_metadata)]
 #![feature(f16)]
 #![feature(f128)]
+#![feature(convert_float_to_int)]
 
 // Allow us to use `kani::` to access crate features.
 extern crate self as kani;

library/kani_core/src/float.rs

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module contains functions useful for float-related checks
+
+#[allow(clippy::crate_in_macro_def)]
+#[macro_export]
+macro_rules! generate_float {
+    ($core:path) => {
+        use super::kani_intrinsic;
+        use core::convert::FloatToInt;
+        /// Returns whether the given float `value` satisfies the range
+        /// condition of the `to_int_unchecked` methods, namely that the `value`
+        /// after truncation is in range of the target `Int`
+        ///
+        /// # Example:
+        ///
+        /// ```no_run
+        /// let f: f32 = 145.7;
+        /// let fits_in_i8 = kani::float::float_to_int_in_range::<f32, i8>(f);
+        /// // doesn't fit in `i8` because the value after truncation (`145.0`) is larger than `i8::MAX`
+        /// assert!(!fits_in_i8);
+        ///
+        /// let f: f64 = 1e6;
+        /// let fits_in_u32 = kani::float::float_to_int_in_range::<f64, u32>(f);
+        /// // fits in `u32` because the value after truncation (`1e6`) is smaller than `u32::MAX`
+        /// assert!(fits_in_u32);
+        /// ```
+        #[crate::kani::unstable_feature(
+            feature = "float-lib",
+            issue = "none",
+            reason = "experimental floating-point API"
+        )]
+        #[kanitool::fn_marker = "FloatToIntInRangeHook"]
+        #[inline(never)]
+        pub fn float_to_int_in_range<Float, Int>(value: Float) -> bool
+        where
+            Float: FloatToInt<Int>,
+        {
+            kani_intrinsic()
+        }
+    };
+}

library/kani_core/src/lib.rs

@@ -21,6 +21,7 @@
 #![feature(f128)]
 
 mod arbitrary;
+mod float;
 mod mem;
 mod mem_init;
 mod models;
@@ -45,6 +46,10 @@ macro_rules! kani_lib {
             kani_core::generate_arbitrary!(core);
             kani_core::generate_models!();
 
+            pub mod float {
+                kani_core::generate_float!(core);
+            }
+
             pub mod mem {
                 kani_core::kani_mem!(core);
             }
@@ -61,6 +66,10 @@ macro_rules! kani_lib {
         kani_core::generate_arbitrary!(std);
         kani_core::generate_models!();
 
+        pub mod float {
+            kani_core::generate_float!(std);
+        }
+
         pub mod mem {
             kani_core::kani_mem!(std);
         }

tests/expected/float-to-int-in-range/invalid_float.expected

@@ -0,0 +1,5 @@
+error[E0277]: the trait bound `i32: std::convert::FloatToInt<u8>` is not satisfied
+invalid_float.rs:
+|     let _c = kani::float::float_to_int_in_range::<i32, u8>(i);
+|                                                   ^^^ the trait `std::convert::FloatToInt<u8>` is not implemented for `i32`
+|

tests/expected/float-to-int-in-range/invalid_float.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that Kani emits an error when
+//! `kani::float::float_to_int_in_range` is instantiated with a non-float type
+
+#[kani::proof]
+fn check_invalid_float() {
+    let i: i32 = 5;
+    let _c = kani::float::float_to_int_in_range::<i32, u8>(i);
+}

tests/expected/float-to-int-in-range/invalid_int.expected

@@ -0,0 +1,5 @@
+error[E0277]: the trait bound `f32: std::convert::FloatToInt<bool>` is not satisfied
+invalid_int.rs:
+|     let _c = kani::float::float_to_int_in_range::<f32, bool>(f);
+|                                                   ^^^ the trait `std::convert::FloatToInt<bool>` is not implemented for `f32`
+|

tests/expected/float-to-int-in-range/invalid_int.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that Kani emits an error when
+//! `kani::float::float_to_int_in_range` is instantiated with a non-integer type
+
+#[kani::proof]
+fn check_invalid_integer() {
+    let f: f32 = kani::any();
+    let _c = kani::float::float_to_int_in_range::<f32, bool>(f);
+}