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

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,54 @@ 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().clone()
+        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 +712,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-compiler/src/kani_middle/transform/kani_intrinsics.rs

@@ -10,7 +10,7 @@
 use crate::args::ExtraChecks;
 use crate::kani_middle::abi::LayoutOf;
 use crate::kani_middle::attributes::KaniAttributes;
-use crate::kani_middle::kani_functions::{KaniFunction, KaniIntrinsic, KaniModel};
+use crate::kani_middle::kani_functions::{KaniFunction, KaniHook, KaniIntrinsic, KaniModel};
 use crate::kani_middle::transform::body::{
     CheckType, InsertPosition, MutableBody, SourceInstruction,
 };
@@ -22,6 +22,8 @@ use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_
 use crate::kani_middle::transform::{TransformPass, TransformationType};
 use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
+use rustc_smir::rustc_internal;
+use stable_mir::CrateDef;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
     AggregateKind, BasicBlock, BinOp, Body, ConstOperand, Local, Mutability, Operand, Place,
@@ -77,6 +79,16 @@ impl TransformPass for IntrinsicGeneratorPass {
                 // This is handled in contracts pass for now.
                 KaniIntrinsic::WriteAny | KaniIntrinsic::AnyModifies => (false, body),
             }
+        } else if let Some(kani_hook) =
+            attributes.fn_marker().and_then(|name| KaniHook::from_str(name.as_str()).ok())
+        {
+            match kani_hook {
+                KaniHook::FloatToIntInRange => {
+                    IntrinsicGeneratorPass::check_float_to_int_in_range_valid_types(tcx, instance);
+                    (false, body)
+                }
+                _ => (false, body),
+            }
         } else {
             (false, body)
         }
@@ -606,6 +618,24 @@ impl IntrinsicGeneratorPass {
             Place::from(RETURN_LOCAL),
         );
     }
+
+    fn check_float_to_int_in_range_valid_types(tcx: TyCtxt, instance: Instance) {
+        let generic_args = instance.args().0;
+        let arg0 = generic_args[0].expect_ty();
+        if !arg0.kind().is_float() {
+            let msg = format!(
+                "Invalid type for first argument of `float_to_int_in_range` intrinsic. Expected a float type. Got `{arg0}`"
+            );
+            tcx.dcx().span_err(rustc_internal::internal(tcx, instance.def.span()), msg);
+        }
+        let arg1 = generic_args[1].expect_ty();
+        if !arg1.kind().is_integral() {
+            let msg = format!(
+                "Invalid type for second argument of `float_to_int_in_range` intrinsic. Expected an integer type. Got `{arg1}`"
+            );
+            tcx.dcx().span_err(rustc_internal::internal(tcx, instance.def.span()), msg);
+        }
+    }
 }
 
 /// Build an Rvalue `Some(val)`.

library/kani_core/src/float.rs

@@ -0,0 +1,31 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module contains functions useful for float-related checks
+
+#[macro_export]
+macro_rules! generate_float {
+    ($core:path) => {
+        /// 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);
+        /// ```
+        #[kanitool::fn_marker = "FloatToIntInRangeHook"]
+        pub fn float_to_int_in_range<Float, Int>(value: Float) -> bool {
+            kani::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 @@
+error: Invalid type for first argument of `float_to_int_in_range` intrinsic. Expected a float type. Got `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 @@
+error: Invalid type for second argument of `float_to_int_in_range` intrinsic. Expected an integer type. Got `bool`

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);
+}

tests/kani/FloatToIntInRange/test.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that `kani::float::float_to_int_in_range` works as expected
+
+#[kani::proof]
+fn check_float_to_int_in_range() {
+    let f: f32 = 5.6;
+    let fits_in_u16 = kani::float::float_to_int_in_range::<f32, u16>(f);
+    assert!(fits_in_u16);
+    let i: u16 = unsafe { f.to_int_unchecked() };
+    assert_eq!(i, 5);
+
+    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);
+    let i: u32 = unsafe { f.to_int_unchecked() };
+    assert_eq!(i, 1_000_000);
+}