From 88a0af4ec7bd942bc307367b7576354744715bbc Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 29 Oct 2024 23:17:19 -0700
Subject: [PATCH 1/9] Add support for float_to_int_unchecked

---
 .../codegen/intrinsic.rs                      | 213 +++++++++++++++++-
 kani-compiler/src/intrinsics.rs               |   9 +
 .../Intrinsics/FloatToInt/float_to_int.rs     |  49 ++++
 3 files changed, 270 insertions(+), 1 deletion(-)
 create mode 100644 tests/kani/Intrinsics/FloatToInt/float_to_int.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index e8f566dafb15..7eedbdf02745 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -7,6 +7,7 @@ use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 use crate::codegen_cprover_gotoc::{GotocCtx, utils};
 use crate::intrinsics::Intrinsic;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
+use cbmc::MachineModel;
 use cbmc::goto_program::{
     ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
 };
@@ -15,7 +16,7 @@ use rustc_middle::ty::layout::ValidityRequirement;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Operand, Place};
-use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
+use stable_mir::ty::{FloatTy, GenericArgs, IntTy, RigidTy, Span, Ty, TyKind, UintTy};
 use tracing::debug;
 
 pub struct SizeAlign {
@@ -384,6 +385,14 @@ impl GotocCtx<'_> {
                 let binop_stmt = codegen_intrinsic_binop!(div);
                 self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
             }
+            Intrinsic::FloatToIntUnchecked => self.codegen_float_to_int_unchecked(
+                intrinsic_str,
+                fargs.remove(0),
+                farg_types[0],
+                place,
+                ret_ty,
+                loc,
+            ),
             Intrinsic::FloorF32 => codegen_simple_intrinsic!(Floorf),
             Intrinsic::FloorF64 => codegen_simple_intrinsic!(Floor),
             Intrinsic::FmafF32 => codegen_simple_intrinsic!(Fmaf),
@@ -1917,6 +1926,61 @@ impl GotocCtx<'_> {
             Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc)
         }
     }
+
+    /// Checks that the floating-point value is:
+    ///     1. Finite (i.e. neither infinite nor NaN)
+    ///     2. Is in range of the target integer
+    /// then performs the cast to the target type
+    pub fn codegen_float_to_int_unchecked(
+        &mut self,
+        intrinsic: &str,
+        expr: Expr,
+        ty: Ty,
+        place: &Place,
+        res_ty: Ty,
+        loc: Location,
+    ) -> Stmt {
+        let finite_check = self.codegen_assert_assume(
+            expr.clone().is_finite(),
+            PropertyClass::ArithmeticOverflow,
+            format!("{intrinsic}: attempt to convert a non-finite value to an integer").as_str(),
+            loc,
+        );
+
+        assert!(res_ty.kind().is_integral());
+        assert!(ty.kind().is_float());
+        let TyKind::RigidTy(integral_ty) = res_ty.kind() else {
+            panic!(
+                "Expected intrinsic `{}` type to be `RigidTy`, but found: `{:?}`",
+                intrinsic, res_ty
+            );
+        };
+        let TyKind::RigidTy(RigidTy::Float(float_type)) = ty.kind() else {
+            panic!("Expected intrinsic `{}` type to be `Float`, but found: `{:?}`", intrinsic, ty);
+        };
+        let mm = self.symbol_table.machine_model();
+        let (min, max) = match integral_ty {
+            RigidTy::Uint(uint_ty) => get_lower_upper_uint_expr(float_type, uint_ty, mm),
+            RigidTy::Int(int_ty) => get_lower_upper_int_expr(float_type, int_ty, mm),
+            _ => unreachable!(),
+        };
+
+        let int_type = self.codegen_ty_stable(res_ty);
+        let range_check = self.codegen_assert_assume(
+            expr.clone().gt(min).and(expr.clone().lt(max)),
+            PropertyClass::ArithmeticOverflow,
+            format!("{intrinsic}: attempt to convert a value out of range of the target integer")
+                .as_str(),
+            loc,
+        );
+
+        let cast = expr.cast_to(int_type);
+
+        Stmt::block(
+            vec![finite_check, range_check, self.codegen_expr_to_place_stable(place, cast, loc)],
+            loc,
+        )
+    }
 }
 
 fn instance_args(instance: &Instance) -> GenericArgs {
@@ -1929,3 +1993,150 @@ fn instance_args(instance: &Instance) -> GenericArgs {
     };
     args
 }
+
+fn get_lower_upper_uint_expr(
+    float_ty: FloatTy,
+    uint_ty: UintTy,
+    mm: &MachineModel,
+) -> (Expr, Expr) {
+    match float_ty {
+        FloatTy::F32 => {
+            let (lower, upper) = get_lower_upper_f32_uint(uint_ty, mm);
+            (Expr::float_constant(lower), Expr::float_constant(upper))
+        }
+        FloatTy::F64 => {
+            let (lower, upper) = get_lower_upper_f64_uint(uint_ty, mm);
+            (Expr::double_constant(lower), Expr::double_constant(upper))
+        }
+        _ => unimplemented!(),
+    }
+}
+
+fn get_lower_upper_int_expr(float_ty: FloatTy, int_ty: IntTy, mm: &MachineModel) -> (Expr, Expr) {
+    match float_ty {
+        FloatTy::F32 => {
+            let (lower, upper) = get_lower_upper_f32_int(int_ty, mm);
+            (Expr::float_constant(lower), Expr::float_constant(upper))
+        }
+        FloatTy::F64 => {
+            let (lower, upper) = get_lower_upper_f64_int(int_ty, mm);
+            (Expr::double_constant(lower), Expr::double_constant(upper))
+        }
+        _ => unimplemented!(),
+    }
+}
+
+/// upper is the smallest `f32` that after truncation is strictly larger than u<N>::MAX
+/// lower is the largest `f32` that after truncation is strictly smaller than u<N>::MIN
+///
+/// For example, for N = 8, upper is 256.0 because the previous f32 (i.e.
+/// `256_f32.next_down()` which is 255.9999847412109375) when truncated is 255.0,
+/// which is not strictly larger than `u8::MAX`
+///
+/// For all bit-widths, lower is -1.0 because the next higher number, when
+/// truncated is -0.0 (or 0.0) which is not strictly smaller than `u<N>::MIN`
+fn get_lower_upper_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
+    let lower: f32 = -1.0;
+    let upper: f32 = match uint_ty {
+        UintTy::U8 => (1u128 << 8) as f32,   // 256.0
+        UintTy::U16 => (1u128 << 16) as f32, // 65536.0
+        UintTy::U32 => (1u128 << 32) as f32, // 4294967296.0
+        UintTy::U64 => (1u128 << 64) as f32, // 18446744073709551616.0
+        UintTy::U128 => f32::INFINITY,       // all f32's fit in u128!
+        UintTy::Usize => match mm.pointer_width {
+            32 => (1u128 << 32) as f32,
+            64 => (1u128 << 64) as f32,
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+fn get_lower_upper_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
+    let lower = -1.0;
+    let upper = match uint_ty {
+        UintTy::U8 => (1u128 << 8) as f64,
+        UintTy::U16 => (1u128 << 16) as f64,
+        UintTy::U32 => (1u128 << 32) as f64,
+        UintTy::U64 => (1u128 << 64) as f64,
+        UintTy::U128 => unimplemented!(),
+        UintTy::Usize => match mm.pointer_width {
+            32 => (1u128 << 32) as f64,
+            64 => (1u128 << 64) as f64,
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+/// upper is the smallest `f32` that after truncation is strictly larger than i<N>::MAX
+/// lower is the largest `f32` that after truncation is strictly smaller than i<N>::MIN
+///
+/// For example, for N = 16, upper is 32768.0 because the previous f32 (i.e.
+/// `32768_f32.next_down()`) when truncated is 32767,
+/// which is not strictly larger than `i16::MAX`
+///
+/// Note that all upper bound values are computed using bit-shifts because all
+/// those values can be precisely represented in f32 (verified using
+/// https://www.h-schmidt.net/FloatConverter/IEEE754.html)
+/// However, for lower bound values, which should be -2^(w-1)-1 (i.e.
+/// i<N>::MIN-1), not all of them can be represented in f32.
+/// For instance, for w = 32, -2^(31)-1 = -2,147,483,649, but this number does
+/// **not** have an f32 representation, and the next **smaller** number is
+/// -2,147,483,904. Note that CBMC for example uses the formula above which
+/// leads to bugs, e.g.: https://github.com/diffblue/cbmc/issues/8488
+fn get_lower_upper_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
+    let lower = match int_ty {
+        IntTy::I8 => -129.0,
+        IntTy::I16 => -32769.0,
+        IntTy::I32 => -2147483904.0,
+        IntTy::I64 => -9223373136366403584.0,
+        IntTy::I128 => -170141203742878835383357727663135391744.0,
+        IntTy::Isize => match mm.pointer_width {
+            32 => -2147483904.0,
+            64 => -9223373136366403584.0,
+            _ => unreachable!(),
+        },
+    };
+    let upper = match int_ty {
+        IntTy::I8 => (1u128 << 7) as f32,   // 128.0
+        IntTy::I16 => (1u128 << 15) as f32, // 32768.0
+        IntTy::I32 => (1u128 << 31) as f32, // 2147483648.0
+        IntTy::I64 => (1u128 << 63) as f32, // 9223372036854775808.0
+        IntTy::I128 => (1u128 << 127) as f32,
+        IntTy::Isize => match mm.pointer_width {
+            32 => (1u128 << 31) as f32,
+            64 => (1u128 << 63) as f32,
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+fn get_lower_upper_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
+    let lower = match int_ty {
+        IntTy::I8 => -129.0,
+        IntTy::I16 => -32769.0,
+        IntTy::I32 => -2147483649.0,
+        IntTy::I64 => -9223372036854777856.0,
+        IntTy::I128 => unimplemented!(),
+        IntTy::Isize => match mm.pointer_width {
+            32 => -2147483649.0,
+            64 => -9223372036854777856.0,
+            _ => unreachable!(),
+        },
+    };
+    let upper = match int_ty {
+        IntTy::I8 => (1u128 << 7) as f64,
+        IntTy::I16 => (1u128 << 15) as f64,
+        IntTy::I32 => (1u128 << 31) as f64,
+        IntTy::I64 => (1u128 << 63) as f64,
+        IntTy::I128 => (1u128 << 127) as f64,
+        IntTy::Isize => match mm.pointer_width {
+            32 => (1u128 << 31) as f64,
+            64 => (1u128 << 63) as f64,
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs
index 13a12751bd07..0121975b11a2 100644
--- a/kani-compiler/src/intrinsics.rs
+++ b/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
diff --git a/tests/kani/Intrinsics/FloatToInt/float_to_int.rs b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs
new file mode 100644
index 000000000000..bbc048172a72
--- /dev/null
+++ b/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);
+}

From 293b7486f29daa8c7613d26c43a2a555601ccb44 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 29 Oct 2024 23:28:55 -0700
Subject: [PATCH 2/9] Add one more test

---
 .../float-to-int/non_finite.expected          |  5 ++++
 .../intrinsics/float-to-int/non_finite.rs     | 24 +++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 tests/expected/intrinsics/float-to-int/non_finite.expected
 create mode 100644 tests/expected/intrinsics/float-to-int/non_finite.rs

diff --git a/tests/expected/intrinsics/float-to-int/non_finite.expected b/tests/expected/intrinsics/float-to-int/non_finite.expected
new file mode 100644
index 000000000000..703853398bf2
--- /dev/null
+++ b/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.
diff --git a/tests/expected/intrinsics/float-to-int/non_finite.rs b/tests/expected/intrinsics/float-to-int/non_finite.rs
new file mode 100644
index 000000000000..1aace2f7d403
--- /dev/null
+++ b/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) };
+}

From 56ea3f309807257519e895c3dbac689afa7a2749 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Wed, 30 Oct 2024 17:38:57 -0700
Subject: [PATCH 3/9] Add more tests

---
 .../codegen/intrinsic.rs                      | 182 +++++++++++++++---
 kani-compiler/src/main.rs                     |   1 +
 .../intrinsics/float-to-int/oob.expected      |  14 ++
 tests/expected/intrinsics/float-to-int/oob.rs |  41 ++++
 .../Intrinsics/FloatToInt/float_to_int.rs     |   4 +-
 5 files changed, 217 insertions(+), 25 deletions(-)
 create mode 100644 tests/expected/intrinsics/float-to-int/oob.expected
 create mode 100644 tests/expected/intrinsics/float-to-int/oob.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 7eedbdf02745..fa31a451df42 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -1960,8 +1960,8 @@ impl GotocCtx<'_> {
         };
         let mm = self.symbol_table.machine_model();
         let (min, max) = match integral_ty {
-            RigidTy::Uint(uint_ty) => get_lower_upper_uint_expr(float_type, uint_ty, mm),
-            RigidTy::Int(int_ty) => get_lower_upper_int_expr(float_type, int_ty, mm),
+            RigidTy::Uint(uint_ty) => get_bounds_uint_expr(float_type, uint_ty, mm),
+            RigidTy::Int(int_ty) => get_bounds_int_expr(float_type, int_ty, mm),
             _ => unreachable!(),
         };
 
@@ -1994,32 +1994,28 @@ fn instance_args(instance: &Instance) -> GenericArgs {
     args
 }
 
-fn get_lower_upper_uint_expr(
-    float_ty: FloatTy,
-    uint_ty: UintTy,
-    mm: &MachineModel,
-) -> (Expr, Expr) {
+fn get_bounds_uint_expr(float_ty: FloatTy, uint_ty: UintTy, mm: &MachineModel) -> (Expr, Expr) {
     match float_ty {
         FloatTy::F32 => {
-            let (lower, upper) = get_lower_upper_f32_uint(uint_ty, mm);
+            let (lower, upper) = get_bounds_f32_uint(uint_ty, mm);
             (Expr::float_constant(lower), Expr::float_constant(upper))
         }
         FloatTy::F64 => {
-            let (lower, upper) = get_lower_upper_f64_uint(uint_ty, mm);
+            let (lower, upper) = get_bounds_f64_uint(uint_ty, mm);
             (Expr::double_constant(lower), Expr::double_constant(upper))
         }
         _ => unimplemented!(),
     }
 }
 
-fn get_lower_upper_int_expr(float_ty: FloatTy, int_ty: IntTy, mm: &MachineModel) -> (Expr, Expr) {
+fn get_bounds_int_expr(float_ty: FloatTy, int_ty: IntTy, mm: &MachineModel) -> (Expr, Expr) {
     match float_ty {
         FloatTy::F32 => {
-            let (lower, upper) = get_lower_upper_f32_int(int_ty, mm);
+            let (lower, upper) = get_bounds_f32_int(int_ty, mm);
             (Expr::float_constant(lower), Expr::float_constant(upper))
         }
         FloatTy::F64 => {
-            let (lower, upper) = get_lower_upper_f64_int(int_ty, mm);
+            let (lower, upper) = get_bounds_f64_int(int_ty, mm);
             (Expr::double_constant(lower), Expr::double_constant(upper))
         }
         _ => unimplemented!(),
@@ -2035,7 +2031,7 @@ fn get_lower_upper_int_expr(float_ty: FloatTy, int_ty: IntTy, mm: &MachineModel)
 ///
 /// For all bit-widths, lower is -1.0 because the next higher number, when
 /// truncated is -0.0 (or 0.0) which is not strictly smaller than `u<N>::MIN`
-fn get_lower_upper_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
+fn get_bounds_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
     let lower: f32 = -1.0;
     let upper: f32 = match uint_ty {
         UintTy::U8 => (1u128 << 8) as f32,   // 256.0
@@ -2052,14 +2048,14 @@ fn get_lower_upper_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
     (lower, upper)
 }
 
-fn get_lower_upper_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
+fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
     let lower = -1.0;
     let upper = match uint_ty {
         UintTy::U8 => (1u128 << 8) as f64,
         UintTy::U16 => (1u128 << 16) as f64,
         UintTy::U32 => (1u128 << 32) as f64,
         UintTy::U64 => (1u128 << 64) as f64,
-        UintTy::U128 => unimplemented!(),
+        UintTy::U128 => 340282366920938463463374607431768211456.0,
         UintTy::Usize => match mm.pointer_width {
             32 => (1u128 << 32) as f64,
             64 => (1u128 << 64) as f64,
@@ -2085,7 +2081,7 @@ fn get_lower_upper_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
 /// **not** have an f32 representation, and the next **smaller** number is
 /// -2,147,483,904. Note that CBMC for example uses the formula above which
 /// leads to bugs, e.g.: https://github.com/diffblue/cbmc/issues/8488
-fn get_lower_upper_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
+fn get_bounds_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
     let lower = match int_ty {
         IntTy::I8 => -129.0,
         IntTy::I16 => -32769.0,
@@ -2099,11 +2095,11 @@ fn get_lower_upper_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
         },
     };
     let upper = match int_ty {
-        IntTy::I8 => (1u128 << 7) as f32,   // 128.0
-        IntTy::I16 => (1u128 << 15) as f32, // 32768.0
-        IntTy::I32 => (1u128 << 31) as f32, // 2147483648.0
-        IntTy::I64 => (1u128 << 63) as f32, // 9223372036854775808.0
-        IntTy::I128 => (1u128 << 127) as f32,
+        IntTy::I8 => (1u128 << 7) as f32,     // 128.0
+        IntTy::I16 => (1u128 << 15) as f32,   // 32768.0
+        IntTy::I32 => (1u128 << 31) as f32,   // 2147483648.0
+        IntTy::I64 => (1u128 << 63) as f32,   // 9223372036854775808.0
+        IntTy::I128 => (1u128 << 127) as f32, // 170141183460469231731687303715884105728.0
         IntTy::Isize => match mm.pointer_width {
             32 => (1u128 << 31) as f32,
             64 => (1u128 << 63) as f32,
@@ -2113,13 +2109,13 @@ fn get_lower_upper_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
     (lower, upper)
 }
 
-fn get_lower_upper_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
+fn get_bounds_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
     let lower = match int_ty {
         IntTy::I8 => -129.0,
         IntTy::I16 => -32769.0,
         IntTy::I32 => -2147483649.0,
         IntTy::I64 => -9223372036854777856.0,
-        IntTy::I128 => unimplemented!(),
+        IntTy::I128 => -170141183460469269510619166673045815296.0,
         IntTy::Isize => match mm.pointer_width {
             32 => -2147483649.0,
             64 => -9223372036854777856.0,
@@ -2140,3 +2136,143 @@ fn get_lower_upper_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
     };
     (lower, upper)
 }
+
+#[cfg(test)]
+mod tests {
+    use std::str::FromStr;
+
+    /// Checks that the given decimal string value has a f32 representation
+    /// (i.e. it can be converted to a f32 without loss of precision)
+    fn has_f32_representation(value: &str) -> bool {
+        // only works for values containing a decimal point
+        assert!(value.contains('.'));
+        // convert to a f32
+        println!("{value}");
+        let f32_value = f32::from_str(value).unwrap();
+        // convert the f32 to a string with full precision
+        let f32_string = format!("{f32_value:.32}");
+        assert!(f32_string.contains('.'));
+        // trim zeros from both strings
+        let f32_string = f32_string.trim_end_matches('0');
+        let value = value.trim_end_matches('0');
+        // compare the strings
+        f32_string == value
+    }
+
+    #[test]
+    fn check_value_has_f32_representation() {
+        // sanity check the function
+        assert!(has_f32_representation("1.0"));
+        // the closest f32 is 4294967296.0
+        assert!(!has_f32_representation("4294967295.0"));
+    }
+
+    #[test]
+    fn check_f32_uint_bounds_representation() {
+        // check that all lower and upper bounds for the unsigned types are
+        // exactly representable in f32
+        assert!(has_f32_representation("-1.0"));
+        assert!(has_f32_representation("256.0"));
+        assert!(has_f32_representation("65536.0"));
+        assert!(has_f32_representation("4294967296.0"));
+        assert!(has_f32_representation("18446744073709551616.0"));
+    }
+
+    #[test]
+    fn check_f32_int_bounds_representation() {
+        // check that all lower and upper bounds for the signed types are
+        // exactly representable in f32
+        assert!(has_f32_representation("-129.0"));
+        assert!(has_f32_representation("-32769.0"));
+        assert!(has_f32_representation("-2147483904.0"));
+        assert!(has_f32_representation("-9223373136366403584.0"));
+        assert!(has_f32_representation("-170141203742878835383357727663135391744.0"));
+        assert!(has_f32_representation("128.0"));
+        assert!(has_f32_representation("32768.0"));
+        assert!(has_f32_representation("2147483648.0"));
+        assert!(has_f32_representation("9223372036854775808.0"));
+        assert!(has_f32_representation("170141183460469231731687303715884105728.0"));
+    }
+
+    /// Checks that the given decimal string value has a f64 representation
+    /// (i.e. it can be converted to a f64 without loss of precision)
+    fn has_f64_representation(value: &str) -> bool {
+        // only works for values containing a decimal point
+        assert!(value.contains('.'));
+        // convert to a f64
+        println!("{value}");
+        let f64_value = f64::from_str(value).unwrap();
+        // convert the f64 to a string with full precision
+        let f64_string = format!("{f64_value:.64}");
+        assert!(f64_string.contains('.'));
+        // trim zeros from both strings
+        let f64_string = f64_string.trim_end_matches('0');
+        let value = value.trim_end_matches('0');
+        // compare the strings
+        f64_string == value
+    }
+
+    #[test]
+    fn check_value_has_f64_representation() {
+        // sanity check the function
+        assert!(has_f64_representation("1.0"));
+        assert!(has_f64_representation("4294967295.0"));
+    }
+
+    #[test]
+    fn check_f64_uint_bounds_representation() {
+        // check that all lower and upper bounds for the unsigned types are
+        // exactly representable in f64
+        assert!(has_f64_representation("-1.0"));
+        assert!(has_f64_representation("256.0"));
+        assert!(has_f64_representation("65536.0"));
+        assert!(has_f64_representation("4294967296.0"));
+        assert!(has_f64_representation("18446744073709551616.0"));
+        assert!(has_f64_representation("340282366920938463463374607431768211456.0"));
+    }
+
+    #[test]
+    fn check_f64_int_bounds_representation() {
+        // check that all lower and upper bounds for the signed types are
+        // exactly representable in f64
+        assert!(has_f64_representation("-129.0"));
+        assert!(has_f64_representation("-32769.0"));
+        assert!(has_f64_representation("-2147483649.0"));
+        assert!(has_f64_representation("-9223372036854777856.0"));
+        assert!(has_f64_representation("-170141183460469269510619166673045815296.0"));
+        assert!(has_f64_representation("128.0"));
+        assert!(has_f64_representation("32768.0"));
+        assert!(has_f64_representation("2147483648.0"));
+        assert!(has_f64_representation("9223372036854775808.0"));
+        assert!(has_f64_representation("170141183460469231731687303715884105728.0"));
+    }
+
+    #[test]
+    fn check_f32_uint_bounds() {
+        // check that the bounds are correct, i.e. that for lower (upper) bounds:
+        //   1. the value when truncated is strictly smaller (larger) than u<N>::MIN (u<N>::MAX)
+        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to u<N>::MIN (u<N>::MAX)
+
+        let uint_lower: f32 = -1.0;
+        assert!((uint_lower.trunc() as i128) < 0);
+        assert!((uint_lower.next_up().trunc() as i128) >= 0);
+
+        let u8_upper: f32 = 256.0;
+        assert!((u8_upper.trunc() as u128) > u8::MAX as u128);
+        assert!((u8_upper.next_down().trunc() as u128) <= u8::MAX as u128);
+
+        let u16_upper: f32 = 65536.0;
+        assert!((u16_upper.trunc() as u128) > u16::MAX as u128);
+        assert!((u16_upper.next_down().trunc() as u128) <= u16::MAX as u128);
+
+        let u32_upper: f32 = 4294967296.0;
+        assert!((u32_upper.trunc() as u128) > u32::MAX as u128);
+        assert!((u32_upper.next_down().trunc() as u128) <= u32::MAX as u128);
+
+        let u64_upper: f32 = 18446744073709551616.0;
+        assert!((u64_upper.trunc() as u128) > u64::MAX as u128);
+        assert!((u64_upper.next_down().trunc() as u128) <= u64::MAX as u128);
+
+        // TODO: use BigInt for u128 or perhaps for all values
+    }
+}
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index 52b9331fb29d..9558b4159224 100644
--- a/kani-compiler/src/main.rs
+++ b/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;
diff --git a/tests/expected/intrinsics/float-to-int/oob.expected b/tests/expected/intrinsics/float-to-int/oob.expected
new file mode 100644
index 000000000000..f862df90f706
--- /dev/null
+++ b/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.
diff --git a/tests/expected/intrinsics/float-to-int/oob.rs b/tests/expected/intrinsics/float-to-int/oob.rs
new file mode 100644
index 000000000000..a49cf89ca82c
--- /dev/null
+++ b/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);
diff --git a/tests/kani/Intrinsics/FloatToInt/float_to_int.rs b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs
index bbc048172a72..4797669b9b61 100644
--- a/tests/kani/Intrinsics/FloatToInt/float_to_int.rs
+++ b/tests/kani/Intrinsics/FloatToInt/float_to_int.rs
@@ -38,12 +38,12 @@ fn check_f64_to_int_unchecked() {
     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, 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, i128);
     check_float_to_int_unchecked!(f64, isize);
 }

From d49291c372c2d1f6a7c3b0cdb74d7dc89da6f78a Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Wed, 30 Oct 2024 17:45:43 -0700
Subject: [PATCH 4/9] Update documentation

---
 docs/src/rust-feature-support/intrinsics.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md
index ce3c9fc1b7a2..a9e2740836e5 100644
--- a/docs/src/rust-feature-support/intrinsics.md
+++ b/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 |

From 08531f6e8d84c8c043a49579f6b2f9780ec03f4c Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Wed, 30 Oct 2024 23:39:58 -0700
Subject: [PATCH 5/9] Clean-up

---
 .../codegen/intrinsic.rs                      | 332 +++++++++---------
 1 file changed, 161 insertions(+), 171 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index fa31a451df42..98185ec6cb59 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -1959,21 +1959,21 @@ impl GotocCtx<'_> {
             panic!("Expected intrinsic `{}` type to be `Float`, but found: `{:?}`", intrinsic, ty);
         };
         let mm = self.symbol_table.machine_model();
-        let (min, max) = match integral_ty {
+        let (lower, upper) = match integral_ty {
             RigidTy::Uint(uint_ty) => get_bounds_uint_expr(float_type, uint_ty, mm),
             RigidTy::Int(int_ty) => get_bounds_int_expr(float_type, int_ty, mm),
             _ => unreachable!(),
         };
 
-        let int_type = self.codegen_ty_stable(res_ty);
         let range_check = self.codegen_assert_assume(
-            expr.clone().gt(min).and(expr.clone().lt(max)),
+            expr.clone().gt(lower).and(expr.clone().lt(upper)),
             PropertyClass::ArithmeticOverflow,
             format!("{intrinsic}: attempt to convert a value out of range of the target integer")
                 .as_str(),
             loc,
         );
 
+        let int_type = self.codegen_ty_stable(res_ty);
         let cast = expr.cast_to(int_type);
 
         Stmt::block(
@@ -2022,6 +2022,42 @@ fn get_bounds_int_expr(float_ty: FloatTy, int_ty: IntTy, mm: &MachineModel) -> (
     }
 }
 
+const F32_U_LOWER: [u8; 4] = [0x00, 0x00, 0x80, 0xBF]; // -1.0
+const F32_U8_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x43]; // 256.0
+const F32_U16_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x47]; // 65536.0
+const F32_U32_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x4F]; // 4294967296.0
+const F32_U64_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x5F]; // 18446744073709551616.0
+const F32_U128_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x7F]; // inf
+
+const F32_I8_LOWER: [u8; 4] = [0x00, 0x00, 0x01, 0xC3]; // -129.0
+const F32_I16_LOWER: [u8; 4] = [0x00, 0x01, 0x00, 0xC7]; // -32769.0
+const F32_I32_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xCF]; // -2147483904.0
+const F32_I64_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xDF]; // -9223373136366403584.0
+const F32_I128_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xFF]; // -170141203742878835383357727663135391744.0
+const F32_I8_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x43]; // 128.0
+const F32_I16_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x47]; // 32768.0
+const F32_I32_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x4F]; // 2147483648.0
+const F32_I64_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x5F]; // 9223372036854775808.0
+const F32_I128_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x7F]; // 170141183460469231731687303715884105728.0
+
+const F64_U_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0xBF]; // -1.0
+const F64_U8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x70, 0x40]; // 256.0
+const F64_U16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x40]; // 65536.0
+const F64_U32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x41]; // 4294967296.0
+const F64_U64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x43]; // 18446744073709551616.0
+const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]; // 340282366920938463463374607431768211456.0
+
+const F64_I8_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x20, 0x60, 0xC0]; // -129.0
+const F64_I16_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x20, 0x00, 0xE0, 0xC0]; // -32769.0
+const F64_I32_LOWER: [u8; 8] = [0x00, 0x00, 0x20, 0x00, 0x00, 0x00, 0xE0, 0xC1]; // -2147483649.0
+const F64_I64_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC3]; // -9223372036854777856.0
+const F64_I128_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC7]; // -170141183460469269510619166673045815296.0
+const F64_I8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x60, 0x40]; // 128.0
+const F64_I16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x40]; // 32768.0
+const F64_I32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x41]; // 2147483648.0
+const F64_I64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x43]; // 9223372036854775808.0
+const F64_I128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x47]; // 170141183460469231731687303715884105728.0
+
 /// upper is the smallest `f32` that after truncation is strictly larger than u<N>::MAX
 /// lower is the largest `f32` that after truncation is strictly smaller than u<N>::MIN
 ///
@@ -2032,16 +2068,16 @@ fn get_bounds_int_expr(float_ty: FloatTy, int_ty: IntTy, mm: &MachineModel) -> (
 /// For all bit-widths, lower is -1.0 because the next higher number, when
 /// truncated is -0.0 (or 0.0) which is not strictly smaller than `u<N>::MIN`
 fn get_bounds_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
-    let lower: f32 = -1.0;
+    let lower: f32 = f32::from_le_bytes(F32_U_LOWER);
     let upper: f32 = match uint_ty {
-        UintTy::U8 => (1u128 << 8) as f32,   // 256.0
-        UintTy::U16 => (1u128 << 16) as f32, // 65536.0
-        UintTy::U32 => (1u128 << 32) as f32, // 4294967296.0
-        UintTy::U64 => (1u128 << 64) as f32, // 18446744073709551616.0
-        UintTy::U128 => f32::INFINITY,       // all f32's fit in u128!
+        UintTy::U8 => f32::from_le_bytes(F32_U8_UPPER),
+        UintTy::U16 => f32::from_le_bytes(F32_U16_UPPER),
+        UintTy::U32 => f32::from_le_bytes(F32_U32_UPPER),
+        UintTy::U64 => f32::from_le_bytes(F32_U64_UPPER),
+        UintTy::U128 => f32::from_le_bytes(F32_U128_UPPER),
         UintTy::Usize => match mm.pointer_width {
-            32 => (1u128 << 32) as f32,
-            64 => (1u128 << 64) as f32,
+            32 => f32::from_le_bytes(F32_U32_UPPER),
+            64 => f32::from_le_bytes(F32_U64_UPPER),
             _ => unreachable!(),
         },
     };
@@ -2049,16 +2085,16 @@ fn get_bounds_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
 }
 
 fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
-    let lower = -1.0;
+    let lower = f64::from_le_bytes(F64_U_LOWER);
     let upper = match uint_ty {
-        UintTy::U8 => (1u128 << 8) as f64,
-        UintTy::U16 => (1u128 << 16) as f64,
-        UintTy::U32 => (1u128 << 32) as f64,
-        UintTy::U64 => (1u128 << 64) as f64,
-        UintTy::U128 => 340282366920938463463374607431768211456.0,
+        UintTy::U8 => f64::from_le_bytes(F64_U8_UPPER),
+        UintTy::U16 => f64::from_le_bytes(F64_U16_UPPER),
+        UintTy::U32 => f64::from_le_bytes(F64_U32_UPPER),
+        UintTy::U64 => f64::from_le_bytes(F64_U64_UPPER),
+        UintTy::U128 => f64::from_le_bytes(F64_U128_UPPER),
         UintTy::Usize => match mm.pointer_width {
-            32 => (1u128 << 32) as f64,
-            64 => (1u128 << 64) as f64,
+            32 => f64::from_le_bytes(F64_U32_UPPER),
+            64 => f64::from_le_bytes(F64_U64_UPPER),
             _ => unreachable!(),
         },
     };
@@ -2072,8 +2108,8 @@ fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
 /// `32768_f32.next_down()`) when truncated is 32767,
 /// which is not strictly larger than `i16::MAX`
 ///
-/// Note that all upper bound values are computed using bit-shifts because all
-/// those values can be precisely represented in f32 (verified using
+/// Note that all upper bound values are 2^(w-1) which can be precisely
+/// represented in f32 (verified using
 /// https://www.h-schmidt.net/FloatConverter/IEEE754.html)
 /// However, for lower bound values, which should be -2^(w-1)-1 (i.e.
 /// i<N>::MIN-1), not all of them can be represented in f32.
@@ -2083,26 +2119,27 @@ fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
 /// leads to bugs, e.g.: https://github.com/diffblue/cbmc/issues/8488
 fn get_bounds_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
     let lower = match int_ty {
-        IntTy::I8 => -129.0,
-        IntTy::I16 => -32769.0,
-        IntTy::I32 => -2147483904.0,
-        IntTy::I64 => -9223373136366403584.0,
-        IntTy::I128 => -170141203742878835383357727663135391744.0,
+        IntTy::I8 => f32::from_le_bytes(F32_I8_LOWER),
+        IntTy::I16 => f32::from_le_bytes(F32_I16_LOWER),
+        IntTy::I32 => f32::from_le_bytes(F32_I32_LOWER),
+        IntTy::I64 => f32::from_le_bytes(F32_I64_LOWER),
+        IntTy::I128 => f32::from_le_bytes(F32_I128_LOWER),
         IntTy::Isize => match mm.pointer_width {
-            32 => -2147483904.0,
-            64 => -9223373136366403584.0,
+            32 => f32::from_le_bytes(F32_I32_LOWER),
+            64 => f32::from_le_bytes(F32_I64_LOWER),
             _ => unreachable!(),
         },
     };
+
     let upper = match int_ty {
-        IntTy::I8 => (1u128 << 7) as f32,     // 128.0
-        IntTy::I16 => (1u128 << 15) as f32,   // 32768.0
-        IntTy::I32 => (1u128 << 31) as f32,   // 2147483648.0
-        IntTy::I64 => (1u128 << 63) as f32,   // 9223372036854775808.0
-        IntTy::I128 => (1u128 << 127) as f32, // 170141183460469231731687303715884105728.0
+        IntTy::I8 => f32::from_le_bytes(F32_I8_UPPER),
+        IntTy::I16 => f32::from_le_bytes(F32_I16_UPPER),
+        IntTy::I32 => f32::from_le_bytes(F32_I32_UPPER),
+        IntTy::I64 => f32::from_le_bytes(F32_I64_UPPER),
+        IntTy::I128 => f32::from_le_bytes(F32_I128_UPPER),
         IntTy::Isize => match mm.pointer_width {
-            32 => (1u128 << 31) as f32,
-            64 => (1u128 << 63) as f32,
+            32 => f32::from_le_bytes(F32_I32_UPPER),
+            64 => f32::from_le_bytes(F32_I64_UPPER),
             _ => unreachable!(),
         },
     };
@@ -2111,26 +2148,26 @@ fn get_bounds_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
 
 fn get_bounds_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
     let lower = match int_ty {
-        IntTy::I8 => -129.0,
-        IntTy::I16 => -32769.0,
-        IntTy::I32 => -2147483649.0,
-        IntTy::I64 => -9223372036854777856.0,
-        IntTy::I128 => -170141183460469269510619166673045815296.0,
+        IntTy::I8 => f64::from_le_bytes(F64_I8_LOWER),
+        IntTy::I16 => f64::from_le_bytes(F64_I16_LOWER),
+        IntTy::I32 => f64::from_le_bytes(F64_I32_LOWER),
+        IntTy::I64 => f64::from_le_bytes(F64_I64_LOWER),
+        IntTy::I128 => f64::from_le_bytes(F64_I128_LOWER),
         IntTy::Isize => match mm.pointer_width {
-            32 => -2147483649.0,
-            64 => -9223372036854777856.0,
+            32 => f64::from_le_bytes(F64_I32_LOWER),
+            64 => f64::from_le_bytes(F64_I64_LOWER),
             _ => unreachable!(),
         },
     };
     let upper = match int_ty {
-        IntTy::I8 => (1u128 << 7) as f64,
-        IntTy::I16 => (1u128 << 15) as f64,
-        IntTy::I32 => (1u128 << 31) as f64,
-        IntTy::I64 => (1u128 << 63) as f64,
-        IntTy::I128 => (1u128 << 127) as f64,
+        IntTy::I8 => f64::from_le_bytes(F64_I8_UPPER),
+        IntTy::I16 => f64::from_le_bytes(F64_I16_UPPER),
+        IntTy::I32 => f64::from_le_bytes(F64_I32_UPPER),
+        IntTy::I64 => f64::from_le_bytes(F64_I64_UPPER),
+        IntTy::I128 => f64::from_le_bytes(F64_I128_UPPER),
         IntTy::Isize => match mm.pointer_width {
-            32 => (1u128 << 31) as f64,
-            64 => (1u128 << 63) as f64,
+            32 => f64::from_le_bytes(F64_I32_UPPER),
+            64 => f64::from_le_bytes(F64_I64_UPPER),
             _ => unreachable!(),
         },
     };
@@ -2139,140 +2176,93 @@ fn get_bounds_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
 
 #[cfg(test)]
 mod tests {
-    use std::str::FromStr;
-
-    /// Checks that the given decimal string value has a f32 representation
-    /// (i.e. it can be converted to a f32 without loss of precision)
-    fn has_f32_representation(value: &str) -> bool {
-        // only works for values containing a decimal point
-        assert!(value.contains('.'));
-        // convert to a f32
-        println!("{value}");
-        let f32_value = f32::from_str(value).unwrap();
-        // convert the f32 to a string with full precision
-        let f32_string = format!("{f32_value:.32}");
-        assert!(f32_string.contains('.'));
-        // trim zeros from both strings
-        let f32_string = f32_string.trim_end_matches('0');
-        let value = value.trim_end_matches('0');
-        // compare the strings
-        f32_string == value
-    }
-
-    #[test]
-    fn check_value_has_f32_representation() {
-        // sanity check the function
-        assert!(has_f32_representation("1.0"));
-        // the closest f32 is 4294967296.0
-        assert!(!has_f32_representation("4294967295.0"));
-    }
-
-    #[test]
-    fn check_f32_uint_bounds_representation() {
-        // check that all lower and upper bounds for the unsigned types are
-        // exactly representable in f32
-        assert!(has_f32_representation("-1.0"));
-        assert!(has_f32_representation("256.0"));
-        assert!(has_f32_representation("65536.0"));
-        assert!(has_f32_representation("4294967296.0"));
-        assert!(has_f32_representation("18446744073709551616.0"));
-    }
-
-    #[test]
-    fn check_f32_int_bounds_representation() {
-        // check that all lower and upper bounds for the signed types are
-        // exactly representable in f32
-        assert!(has_f32_representation("-129.0"));
-        assert!(has_f32_representation("-32769.0"));
-        assert!(has_f32_representation("-2147483904.0"));
-        assert!(has_f32_representation("-9223373136366403584.0"));
-        assert!(has_f32_representation("-170141203742878835383357727663135391744.0"));
-        assert!(has_f32_representation("128.0"));
-        assert!(has_f32_representation("32768.0"));
-        assert!(has_f32_representation("2147483648.0"));
-        assert!(has_f32_representation("9223372036854775808.0"));
-        assert!(has_f32_representation("170141183460469231731687303715884105728.0"));
+    use super::*;
+    use num::BigInt;
+    use num::FromPrimitive;
+
+    macro_rules! check_lower_f32 {
+        ($val:ident, $min:expr) => {
+            let f = f32::from_le_bytes($val);
+            assert!(BigInt::from_f32(f.trunc()).unwrap() < BigInt::from($min));
+            assert!(BigInt::from_f32(f.next_up().trunc()).unwrap() >= BigInt::from($min));
+        };
     }
 
-    /// Checks that the given decimal string value has a f64 representation
-    /// (i.e. it can be converted to a f64 without loss of precision)
-    fn has_f64_representation(value: &str) -> bool {
-        // only works for values containing a decimal point
-        assert!(value.contains('.'));
-        // convert to a f64
-        println!("{value}");
-        let f64_value = f64::from_str(value).unwrap();
-        // convert the f64 to a string with full precision
-        let f64_string = format!("{f64_value:.64}");
-        assert!(f64_string.contains('.'));
-        // trim zeros from both strings
-        let f64_string = f64_string.trim_end_matches('0');
-        let value = value.trim_end_matches('0');
-        // compare the strings
-        f64_string == value
+    macro_rules! check_upper_f32 {
+        ($val:ident, $max:expr) => {
+            let f = f32::from_le_bytes($val);
+            assert!(BigInt::from_f32(f.trunc()).unwrap() > BigInt::from($max));
+            assert!(BigInt::from_f32(f.next_down().trunc()).unwrap() <= BigInt::from($max));
+        };
     }
 
     #[test]
-    fn check_value_has_f64_representation() {
-        // sanity check the function
-        assert!(has_f64_representation("1.0"));
-        assert!(has_f64_representation("4294967295.0"));
+    fn check_f32_bounds() {
+        // check that the bounds are correct, i.e. that for lower (upper) bounds:
+        //   1. the value when truncated is strictly smaller (larger) than {i, u}<N>::MIN ({i, u}<N>::MAX)
+        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to {i, u}<N>::MIN ({i, u}<N>::MAX)
+
+        check_lower_f32!(F32_U_LOWER, u8::MIN);
+
+        check_upper_f32!(F32_U8_UPPER, u8::MAX);
+        check_upper_f32!(F32_U16_UPPER, u16::MAX);
+        check_upper_f32!(F32_U32_UPPER, u32::MAX);
+        check_upper_f32!(F32_U64_UPPER, u64::MAX);
+        // 128 is not needed because the upper bounds is infinity
+
+        check_lower_f32!(F32_I8_LOWER, i8::MIN);
+        check_lower_f32!(F32_I16_LOWER, i16::MIN);
+        check_lower_f32!(F32_I32_LOWER, i32::MIN);
+        check_lower_f32!(F32_I64_LOWER, i64::MIN);
+        check_lower_f32!(F32_I128_LOWER, i128::MIN);
+
+        check_upper_f32!(F32_I8_UPPER, i8::MAX);
+        check_upper_f32!(F32_I16_UPPER, i16::MAX);
+        check_upper_f32!(F32_I32_UPPER, i32::MAX);
+        check_upper_f32!(F32_I64_UPPER, i64::MAX);
+        check_upper_f32!(F32_I128_UPPER, i128::MAX);
     }
 
-    #[test]
-    fn check_f64_uint_bounds_representation() {
-        // check that all lower and upper bounds for the unsigned types are
-        // exactly representable in f64
-        assert!(has_f64_representation("-1.0"));
-        assert!(has_f64_representation("256.0"));
-        assert!(has_f64_representation("65536.0"));
-        assert!(has_f64_representation("4294967296.0"));
-        assert!(has_f64_representation("18446744073709551616.0"));
-        assert!(has_f64_representation("340282366920938463463374607431768211456.0"));
+    macro_rules! check_lower_f64 {
+        ($val:ident, $min:expr) => {
+            let f = f64::from_le_bytes($val);
+            assert!(BigInt::from_f64(f.trunc()).unwrap() < BigInt::from($min));
+            assert!(BigInt::from_f64(f.next_up().trunc()).unwrap() >= BigInt::from($min));
+        };
     }
 
-    #[test]
-    fn check_f64_int_bounds_representation() {
-        // check that all lower and upper bounds for the signed types are
-        // exactly representable in f64
-        assert!(has_f64_representation("-129.0"));
-        assert!(has_f64_representation("-32769.0"));
-        assert!(has_f64_representation("-2147483649.0"));
-        assert!(has_f64_representation("-9223372036854777856.0"));
-        assert!(has_f64_representation("-170141183460469269510619166673045815296.0"));
-        assert!(has_f64_representation("128.0"));
-        assert!(has_f64_representation("32768.0"));
-        assert!(has_f64_representation("2147483648.0"));
-        assert!(has_f64_representation("9223372036854775808.0"));
-        assert!(has_f64_representation("170141183460469231731687303715884105728.0"));
+    macro_rules! check_upper_f64 {
+        ($val:ident, $max:expr) => {
+            let f = f64::from_le_bytes($val);
+            assert!(BigInt::from_f64(f.trunc()).unwrap() > BigInt::from($max));
+            assert!(BigInt::from_f64(f.next_down().trunc()).unwrap() <= BigInt::from($max));
+        };
     }
 
     #[test]
-    fn check_f32_uint_bounds() {
+    fn check_f64_bounds() {
         // check that the bounds are correct, i.e. that for lower (upper) bounds:
-        //   1. the value when truncated is strictly smaller (larger) than u<N>::MIN (u<N>::MAX)
-        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to u<N>::MIN (u<N>::MAX)
-
-        let uint_lower: f32 = -1.0;
-        assert!((uint_lower.trunc() as i128) < 0);
-        assert!((uint_lower.next_up().trunc() as i128) >= 0);
-
-        let u8_upper: f32 = 256.0;
-        assert!((u8_upper.trunc() as u128) > u8::MAX as u128);
-        assert!((u8_upper.next_down().trunc() as u128) <= u8::MAX as u128);
-
-        let u16_upper: f32 = 65536.0;
-        assert!((u16_upper.trunc() as u128) > u16::MAX as u128);
-        assert!((u16_upper.next_down().trunc() as u128) <= u16::MAX as u128);
-
-        let u32_upper: f32 = 4294967296.0;
-        assert!((u32_upper.trunc() as u128) > u32::MAX as u128);
-        assert!((u32_upper.next_down().trunc() as u128) <= u32::MAX as u128);
-
-        let u64_upper: f32 = 18446744073709551616.0;
-        assert!((u64_upper.trunc() as u128) > u64::MAX as u128);
-        assert!((u64_upper.next_down().trunc() as u128) <= u64::MAX as u128);
-
-        // TODO: use BigInt for u128 or perhaps for all values
+        //   1. the value when truncated is strictly smaller (larger) than {i, u}<N>::MIN ({i, u}<N>::MAX)
+        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to {i, u}<N>::MIN ({i, u}<N>::MAX)
+
+        check_lower_f64!(F64_U_LOWER, u8::MIN);
+
+        check_upper_f64!(F64_U8_UPPER, u8::MAX);
+        check_upper_f64!(F64_U16_UPPER, u16::MAX);
+        check_upper_f64!(F64_U32_UPPER, u32::MAX);
+        check_upper_f64!(F64_U64_UPPER, u64::MAX);
+        check_upper_f64!(F64_U128_UPPER, u128::MAX);
+
+        check_lower_f64!(F64_I8_LOWER, i8::MIN);
+        check_lower_f64!(F64_I16_LOWER, i16::MIN);
+        check_lower_f64!(F64_I32_LOWER, i32::MIN);
+        check_lower_f64!(F64_I64_LOWER, i64::MIN);
+        check_lower_f64!(F64_I128_LOWER, i128::MIN);
+
+        check_upper_f64!(F64_I8_UPPER, i8::MAX);
+        check_upper_f64!(F64_I16_UPPER, i16::MAX);
+        check_upper_f64!(F64_I32_UPPER, i32::MAX);
+        check_upper_f64!(F64_I64_UPPER, i64::MAX);
+        check_upper_f64!(F64_I128_UPPER, i128::MAX);
     }
 }

From f6a4d285320dca50b695ebd28f102f87e08288d4 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Wed, 30 Oct 2024 23:57:03 -0700
Subject: [PATCH 6/9] Clarify comment

---
 kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 98185ec6cb59..e58942baaa9d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -1929,7 +1929,7 @@ impl GotocCtx<'_> {
 
     /// Checks that the floating-point value is:
     ///     1. Finite (i.e. neither infinite nor NaN)
-    ///     2. Is in range of the target integer
+    ///     2. Its truncated value is in range of the target integer
     /// then performs the cast to the target type
     pub fn codegen_float_to_int_unchecked(
         &mut self,

From 5dbd3bcb110f6637c37eb1930a55844f90adfe58 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Thu, 31 Oct 2024 11:11:24 -0700
Subject: [PATCH 7/9] Include a check that u128::MAX does not need a bound

---
 kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index e58942baaa9d..403c483f54b5 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -2027,6 +2027,7 @@ const F32_U8_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x43]; // 256.0
 const F32_U16_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x47]; // 65536.0
 const F32_U32_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x4F]; // 4294967296.0
 const F32_U64_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x5F]; // 18446744073709551616.0
+// The largest f32 value fits in a u128, so there is no upper bound
 const F32_U128_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x7F]; // inf
 
 const F32_I8_LOWER: [u8; 4] = [0x00, 0x00, 0x01, 0xC3]; // -129.0
@@ -2209,6 +2210,8 @@ mod tests {
         check_upper_f32!(F32_U32_UPPER, u32::MAX);
         check_upper_f32!(F32_U64_UPPER, u64::MAX);
         // 128 is not needed because the upper bounds is infinity
+        // Instead, check that `u128::MAX` is larger than the largest f32 value
+        assert!(f32::MAX < u128::MAX as f32);
 
         check_lower_f32!(F32_I8_LOWER, i8::MIN);
         check_lower_f32!(F32_I16_LOWER, i16::MIN);

From 9a32883abc555e04bcd09e031070728d0ddad1fb Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 5 Nov 2024 18:24:59 -0800
Subject: [PATCH 8/9] Move code that computes in-range expression to a new
 module

---
 .../codegen/intrinsic.rs                      | 287 +-----------
 .../utils/float_utils.rs                      | 435 ++++++++++++++++++
 .../src/codegen_cprover_gotoc/utils/mod.rs    |   2 +
 3 files changed, 440 insertions(+), 284 deletions(-)
 create mode 100644 kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 72587cfb2cac..97b13e5f4185 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -7,7 +7,6 @@ use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 use crate::codegen_cprover_gotoc::{GotocCtx, utils};
 use crate::intrinsics::Intrinsic;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
-use cbmc::MachineModel;
 use cbmc::goto_program::{
     ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
 };
@@ -16,7 +15,7 @@ use rustc_middle::ty::layout::ValidityRequirement;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{BasicBlockIdx, Operand, Place};
-use stable_mir::ty::{FloatTy, GenericArgs, IntTy, RigidTy, Span, Ty, TyKind, UintTy};
+use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy};
 use tracing::debug;
 
 pub struct SizeAlign {
@@ -1959,14 +1958,10 @@ impl GotocCtx<'_> {
             panic!("Expected intrinsic `{}` type to be `Float`, but found: `{:?}`", intrinsic, ty);
         };
         let mm = self.symbol_table.machine_model();
-        let (lower, upper) = match integral_ty {
-            RigidTy::Uint(uint_ty) => get_bounds_uint_expr(float_type, uint_ty, mm),
-            RigidTy::Int(int_ty) => get_bounds_int_expr(float_type, int_ty, mm),
-            _ => unreachable!(),
-        };
+        let in_range = utils::codegen_in_range_expr(&expr, float_type, integral_ty, mm);
 
         let range_check = self.codegen_assert_assume(
-            expr.clone().gt(lower).and(expr.clone().lt(upper)),
+            in_range,
             PropertyClass::ArithmeticOverflow,
             format!("{intrinsic}: attempt to convert a value out of range of the target integer")
                 .as_str(),
@@ -1993,279 +1988,3 @@ fn instance_args(instance: &Instance) -> GenericArgs {
     };
     args
 }
-
-fn get_bounds_uint_expr(float_ty: FloatTy, uint_ty: UintTy, mm: &MachineModel) -> (Expr, Expr) {
-    match float_ty {
-        FloatTy::F32 => {
-            let (lower, upper) = get_bounds_f32_uint(uint_ty, mm);
-            (Expr::float_constant(lower), Expr::float_constant(upper))
-        }
-        FloatTy::F64 => {
-            let (lower, upper) = get_bounds_f64_uint(uint_ty, mm);
-            (Expr::double_constant(lower), Expr::double_constant(upper))
-        }
-        _ => unimplemented!(),
-    }
-}
-
-fn get_bounds_int_expr(float_ty: FloatTy, int_ty: IntTy, mm: &MachineModel) -> (Expr, Expr) {
-    match float_ty {
-        FloatTy::F32 => {
-            let (lower, upper) = get_bounds_f32_int(int_ty, mm);
-            (Expr::float_constant(lower), Expr::float_constant(upper))
-        }
-        FloatTy::F64 => {
-            let (lower, upper) = get_bounds_f64_int(int_ty, mm);
-            (Expr::double_constant(lower), Expr::double_constant(upper))
-        }
-        _ => unimplemented!(),
-    }
-}
-
-const F32_U_LOWER: [u8; 4] = [0x00, 0x00, 0x80, 0xBF]; // -1.0
-const F32_U8_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x43]; // 256.0
-const F32_U16_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x47]; // 65536.0
-const F32_U32_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x4F]; // 4294967296.0
-const F32_U64_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x5F]; // 18446744073709551616.0
-// The largest f32 value fits in a u128, so there is no upper bound
-const F32_U128_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x7F]; // inf
-
-const F32_I8_LOWER: [u8; 4] = [0x00, 0x00, 0x01, 0xC3]; // -129.0
-const F32_I16_LOWER: [u8; 4] = [0x00, 0x01, 0x00, 0xC7]; // -32769.0
-const F32_I32_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xCF]; // -2147483904.0
-const F32_I64_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xDF]; // -9223373136366403584.0
-const F32_I128_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xFF]; // -170141203742878835383357727663135391744.0
-const F32_I8_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x43]; // 128.0
-const F32_I16_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x47]; // 32768.0
-const F32_I32_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x4F]; // 2147483648.0
-const F32_I64_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x5F]; // 9223372036854775808.0
-const F32_I128_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x7F]; // 170141183460469231731687303715884105728.0
-
-const F64_U_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0xBF]; // -1.0
-const F64_U8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x70, 0x40]; // 256.0
-const F64_U16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x40]; // 65536.0
-const F64_U32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x41]; // 4294967296.0
-const F64_U64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x43]; // 18446744073709551616.0
-const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]; // 340282366920938463463374607431768211456.0
-
-const F64_I8_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x20, 0x60, 0xC0]; // -129.0
-const F64_I16_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x20, 0x00, 0xE0, 0xC0]; // -32769.0
-const F64_I32_LOWER: [u8; 8] = [0x00, 0x00, 0x20, 0x00, 0x00, 0x00, 0xE0, 0xC1]; // -2147483649.0
-const F64_I64_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC3]; // -9223372036854777856.0
-const F64_I128_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC7]; // -170141183460469269510619166673045815296.0
-const F64_I8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x60, 0x40]; // 128.0
-const F64_I16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x40]; // 32768.0
-const F64_I32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x41]; // 2147483648.0
-const F64_I64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x43]; // 9223372036854775808.0
-const F64_I128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x47]; // 170141183460469231731687303715884105728.0
-
-/// upper is the smallest `f32` that after truncation is strictly larger than u<N>::MAX
-/// lower is the largest `f32` that after truncation is strictly smaller than u<N>::MIN
-///
-/// For example, for N = 8, upper is 256.0 because the previous f32 (i.e.
-/// `256_f32.next_down()` which is 255.9999847412109375) when truncated is 255.0,
-/// which is not strictly larger than `u8::MAX`
-///
-/// For all bit-widths, lower is -1.0 because the next higher number, when
-/// truncated is -0.0 (or 0.0) which is not strictly smaller than `u<N>::MIN`
-fn get_bounds_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
-    let lower: f32 = f32::from_le_bytes(F32_U_LOWER);
-    let upper: f32 = match uint_ty {
-        UintTy::U8 => f32::from_le_bytes(F32_U8_UPPER),
-        UintTy::U16 => f32::from_le_bytes(F32_U16_UPPER),
-        UintTy::U32 => f32::from_le_bytes(F32_U32_UPPER),
-        UintTy::U64 => f32::from_le_bytes(F32_U64_UPPER),
-        UintTy::U128 => f32::from_le_bytes(F32_U128_UPPER),
-        UintTy::Usize => match mm.pointer_width {
-            32 => f32::from_le_bytes(F32_U32_UPPER),
-            64 => f32::from_le_bytes(F32_U64_UPPER),
-            _ => unreachable!(),
-        },
-    };
-    (lower, upper)
-}
-
-fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
-    let lower = f64::from_le_bytes(F64_U_LOWER);
-    let upper = match uint_ty {
-        UintTy::U8 => f64::from_le_bytes(F64_U8_UPPER),
-        UintTy::U16 => f64::from_le_bytes(F64_U16_UPPER),
-        UintTy::U32 => f64::from_le_bytes(F64_U32_UPPER),
-        UintTy::U64 => f64::from_le_bytes(F64_U64_UPPER),
-        UintTy::U128 => f64::from_le_bytes(F64_U128_UPPER),
-        UintTy::Usize => match mm.pointer_width {
-            32 => f64::from_le_bytes(F64_U32_UPPER),
-            64 => f64::from_le_bytes(F64_U64_UPPER),
-            _ => unreachable!(),
-        },
-    };
-    (lower, upper)
-}
-
-/// upper is the smallest `f32` that after truncation is strictly larger than i<N>::MAX
-/// lower is the largest `f32` that after truncation is strictly smaller than i<N>::MIN
-///
-/// For example, for N = 16, upper is 32768.0 because the previous f32 (i.e.
-/// `32768_f32.next_down()`) when truncated is 32767,
-/// which is not strictly larger than `i16::MAX`
-///
-/// Note that all upper bound values are 2^(w-1) which can be precisely
-/// represented in f32 (verified using
-/// https://www.h-schmidt.net/FloatConverter/IEEE754.html)
-/// However, for lower bound values, which should be -2^(w-1)-1 (i.e.
-/// i<N>::MIN-1), not all of them can be represented in f32.
-/// For instance, for w = 32, -2^(31)-1 = -2,147,483,649, but this number does
-/// **not** have an f32 representation, and the next **smaller** number is
-/// -2,147,483,904. Note that CBMC for example uses the formula above which
-/// leads to bugs, e.g.: https://github.com/diffblue/cbmc/issues/8488
-fn get_bounds_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
-    let lower = match int_ty {
-        IntTy::I8 => f32::from_le_bytes(F32_I8_LOWER),
-        IntTy::I16 => f32::from_le_bytes(F32_I16_LOWER),
-        IntTy::I32 => f32::from_le_bytes(F32_I32_LOWER),
-        IntTy::I64 => f32::from_le_bytes(F32_I64_LOWER),
-        IntTy::I128 => f32::from_le_bytes(F32_I128_LOWER),
-        IntTy::Isize => match mm.pointer_width {
-            32 => f32::from_le_bytes(F32_I32_LOWER),
-            64 => f32::from_le_bytes(F32_I64_LOWER),
-            _ => unreachable!(),
-        },
-    };
-
-    let upper = match int_ty {
-        IntTy::I8 => f32::from_le_bytes(F32_I8_UPPER),
-        IntTy::I16 => f32::from_le_bytes(F32_I16_UPPER),
-        IntTy::I32 => f32::from_le_bytes(F32_I32_UPPER),
-        IntTy::I64 => f32::from_le_bytes(F32_I64_UPPER),
-        IntTy::I128 => f32::from_le_bytes(F32_I128_UPPER),
-        IntTy::Isize => match mm.pointer_width {
-            32 => f32::from_le_bytes(F32_I32_UPPER),
-            64 => f32::from_le_bytes(F32_I64_UPPER),
-            _ => unreachable!(),
-        },
-    };
-    (lower, upper)
-}
-
-fn get_bounds_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
-    let lower = match int_ty {
-        IntTy::I8 => f64::from_le_bytes(F64_I8_LOWER),
-        IntTy::I16 => f64::from_le_bytes(F64_I16_LOWER),
-        IntTy::I32 => f64::from_le_bytes(F64_I32_LOWER),
-        IntTy::I64 => f64::from_le_bytes(F64_I64_LOWER),
-        IntTy::I128 => f64::from_le_bytes(F64_I128_LOWER),
-        IntTy::Isize => match mm.pointer_width {
-            32 => f64::from_le_bytes(F64_I32_LOWER),
-            64 => f64::from_le_bytes(F64_I64_LOWER),
-            _ => unreachable!(),
-        },
-    };
-    let upper = match int_ty {
-        IntTy::I8 => f64::from_le_bytes(F64_I8_UPPER),
-        IntTy::I16 => f64::from_le_bytes(F64_I16_UPPER),
-        IntTy::I32 => f64::from_le_bytes(F64_I32_UPPER),
-        IntTy::I64 => f64::from_le_bytes(F64_I64_UPPER),
-        IntTy::I128 => f64::from_le_bytes(F64_I128_UPPER),
-        IntTy::Isize => match mm.pointer_width {
-            32 => f64::from_le_bytes(F64_I32_UPPER),
-            64 => f64::from_le_bytes(F64_I64_UPPER),
-            _ => unreachable!(),
-        },
-    };
-    (lower, upper)
-}
-
-#[cfg(test)]
-mod tests {
-    use super::*;
-    use num::BigInt;
-    use num::FromPrimitive;
-
-    macro_rules! check_lower_f32 {
-        ($val:ident, $min:expr) => {
-            let f = f32::from_le_bytes($val);
-            assert!(BigInt::from_f32(f.trunc()).unwrap() < BigInt::from($min));
-            assert!(BigInt::from_f32(f.next_up().trunc()).unwrap() >= BigInt::from($min));
-        };
-    }
-
-    macro_rules! check_upper_f32 {
-        ($val:ident, $max:expr) => {
-            let f = f32::from_le_bytes($val);
-            assert!(BigInt::from_f32(f.trunc()).unwrap() > BigInt::from($max));
-            assert!(BigInt::from_f32(f.next_down().trunc()).unwrap() <= BigInt::from($max));
-        };
-    }
-
-    #[test]
-    fn check_f32_bounds() {
-        // check that the bounds are correct, i.e. that for lower (upper) bounds:
-        //   1. the value when truncated is strictly smaller (larger) than {i, u}<N>::MIN ({i, u}<N>::MAX)
-        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to {i, u}<N>::MIN ({i, u}<N>::MAX)
-
-        check_lower_f32!(F32_U_LOWER, u8::MIN);
-
-        check_upper_f32!(F32_U8_UPPER, u8::MAX);
-        check_upper_f32!(F32_U16_UPPER, u16::MAX);
-        check_upper_f32!(F32_U32_UPPER, u32::MAX);
-        check_upper_f32!(F32_U64_UPPER, u64::MAX);
-        // 128 is not needed because the upper bounds is infinity
-        // Instead, check that `u128::MAX` is larger than the largest f32 value
-        assert!(f32::MAX < u128::MAX as f32);
-
-        check_lower_f32!(F32_I8_LOWER, i8::MIN);
-        check_lower_f32!(F32_I16_LOWER, i16::MIN);
-        check_lower_f32!(F32_I32_LOWER, i32::MIN);
-        check_lower_f32!(F32_I64_LOWER, i64::MIN);
-        check_lower_f32!(F32_I128_LOWER, i128::MIN);
-
-        check_upper_f32!(F32_I8_UPPER, i8::MAX);
-        check_upper_f32!(F32_I16_UPPER, i16::MAX);
-        check_upper_f32!(F32_I32_UPPER, i32::MAX);
-        check_upper_f32!(F32_I64_UPPER, i64::MAX);
-        check_upper_f32!(F32_I128_UPPER, i128::MAX);
-    }
-
-    macro_rules! check_lower_f64 {
-        ($val:ident, $min:expr) => {
-            let f = f64::from_le_bytes($val);
-            assert!(BigInt::from_f64(f.trunc()).unwrap() < BigInt::from($min));
-            assert!(BigInt::from_f64(f.next_up().trunc()).unwrap() >= BigInt::from($min));
-        };
-    }
-
-    macro_rules! check_upper_f64 {
-        ($val:ident, $max:expr) => {
-            let f = f64::from_le_bytes($val);
-            assert!(BigInt::from_f64(f.trunc()).unwrap() > BigInt::from($max));
-            assert!(BigInt::from_f64(f.next_down().trunc()).unwrap() <= BigInt::from($max));
-        };
-    }
-
-    #[test]
-    fn check_f64_bounds() {
-        // check that the bounds are correct, i.e. that for lower (upper) bounds:
-        //   1. the value when truncated is strictly smaller (larger) than {i, u}<N>::MIN ({i, u}<N>::MAX)
-        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to {i, u}<N>::MIN ({i, u}<N>::MAX)
-
-        check_lower_f64!(F64_U_LOWER, u8::MIN);
-
-        check_upper_f64!(F64_U8_UPPER, u8::MAX);
-        check_upper_f64!(F64_U16_UPPER, u16::MAX);
-        check_upper_f64!(F64_U32_UPPER, u32::MAX);
-        check_upper_f64!(F64_U64_UPPER, u64::MAX);
-        check_upper_f64!(F64_U128_UPPER, u128::MAX);
-
-        check_lower_f64!(F64_I8_LOWER, i8::MIN);
-        check_lower_f64!(F64_I16_LOWER, i16::MIN);
-        check_lower_f64!(F64_I32_LOWER, i32::MIN);
-        check_lower_f64!(F64_I64_LOWER, i64::MIN);
-        check_lower_f64!(F64_I128_LOWER, i128::MIN);
-
-        check_upper_f64!(F64_I8_UPPER, i8::MAX);
-        check_upper_f64!(F64_I16_UPPER, i16::MAX);
-        check_upper_f64!(F64_I32_UPPER, i32::MAX);
-        check_upper_f64!(F64_I64_UPPER, i64::MAX);
-        check_upper_f64!(F64_I128_UPPER, i128::MAX);
-    }
-}
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
new file mode 100644
index 000000000000..3de22fc8d55e
--- /dev/null
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
@@ -0,0 +1,435 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module contains utilities related to floating-point types
+
+use cbmc::{MachineModel, goto_program::Expr};
+use stable_mir::ty::{FloatTy, IntTy, RigidTy, UintTy};
+
+/// This function creates a boolean expression that the given `float_expr` when truncated is in the range of `integral_ty`.
+///
+/// The expression it generates is in the form:
+///
+///     `float_expr > lower_bound && float_expr < upper_bound`
+///
+/// i.e., the comparison is performed in terms of floats
+///
+/// Generally, the lower bound for an integral type is `MIN - 1` and the upper bound is `MAX + 1`.
+/// For example, for `i16`, the lower bound is `i16::MIN - 1` (-32769) and the upper bound is `i16::MAX + 1` (32768)
+/// Similarly, for `u8`, the lower bound is `u8::MIN - 1` (-1) and the upper bound is `u8::MAX + 1` (256)
+///
+/// However, due to the floating-point imprecision, not every value has a representation.
+/// For example, while `i16::MIN - 1` (-32769) and `u8::MAX + 1` (256) can be accurately represented as `f32` and `f64`,
+/// `i32::MIN - 1` (-2147483649) cannot be represented in `f32` (the closest `f32` value is -2147483648).
+/// See https://www.h-schmidt.net/FloatConverter/IEEE754.html
+///
+/// If we were to just use `MIN - 1`, the resulting expression may exclude values that are actually in range.
+/// For example, `float_expr > ((i32::MIN - 1) as f32)` would expand to `float_expr > -2147483649 as f32` which
+/// would result in `float_expr > -2147483648.0`. This expression incorrectly exlcudes a valid `i32`
+/// value: `i32::MIN` = -2147483648.
+///
+/// Thus, to determine the lower bound, we need to find the **largest** floating-point value that is
+/// less than or equal to `MIN - 1`.
+/// For example, for `i32`, the largest such value is `-2147483904.0`
+/// Similarly, to determine the upper bound, we need to find the smallest floating-point value that is
+/// greater than or equal to `MAX + 1`.
+///
+/// An alternative approach would be to perform the float-to-int cast with a wider integer and
+/// then check if the wider integer value is in the range of the narrower integer value.
+/// This seems to be the approach used in MIRI:
+/// https://github.com/rust-lang/rust/blob/096277e989d6de11c3077472fc05778e261e7b8e/src/tools/miri/src/helpers.rs#L1003
+/// but it's not clear what it does for `i128` and `u128`.
+pub fn codegen_in_range_expr(
+    float_expr: &Expr,
+    float_ty: FloatTy,
+    integral_ty: RigidTy,
+    mm: &MachineModel,
+) -> Expr {
+    match float_ty {
+        FloatTy::F32 => {
+            let (lower, upper) = get_bounds_f32(integral_ty, mm);
+            let mut in_range = Expr::bool_true();
+            // Avoid unnecessary comparison against -∞ or ∞
+            if lower != f32::NEG_INFINITY {
+                in_range = in_range.and(float_expr.clone().gt(Expr::float_constant(lower)));
+            }
+            if upper != f32::INFINITY {
+                in_range = in_range.and(float_expr.clone().lt(Expr::float_constant(upper)));
+            }
+            in_range
+        }
+        FloatTy::F64 => {
+            let (lower, upper) = get_bounds_f64(integral_ty, mm);
+            let mut in_range = Expr::bool_true();
+            if lower != f64::NEG_INFINITY {
+                in_range = in_range.and(float_expr.clone().gt(Expr::double_constant(lower)));
+            }
+            if upper != f64::INFINITY {
+                in_range = in_range.and(float_expr.clone().lt(Expr::double_constant(upper)));
+            }
+            in_range
+        }
+        _ => unimplemented!(),
+    }
+}
+
+const F32_I8_LOWER: [u8; 4] = [0x00, 0x00, 0x01, 0xC3]; // -129.0
+const F32_I8_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x43]; // 128.0
+const F32_I16_LOWER: [u8; 4] = [0x00, 0x01, 0x00, 0xC7]; // -32769.0
+const F32_I16_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x47]; // 32768.0
+const F32_I32_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xCF]; // -2147483904.0
+const F32_I32_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x4F]; // 2147483648.0
+const F32_I64_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xDF]; // -9223373136366403584.0
+const F32_I64_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x5F]; // 9223372036854775808.0
+// The next value is determined manually and not via test:
+const F32_I128_LOWER: [u8; 4] = [0x01, 0x00, 0x00, 0xFF]; // -170141203742878835383357727663135391744.0
+const F32_I128_UPPER: [u8; 4] = [0x00, 0x00, 0x00, 0x7F]; // 170141183460469231731687303715884105728.0
+
+const F64_I8_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x20, 0x60, 0xC0]; // -129.0
+const F64_I8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x60, 0x40]; // 128.0
+const F64_I16_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x20, 0x00, 0xE0, 0xC0]; // -32769.0
+const F64_I16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x40]; // 32768.0
+const F64_I32_LOWER: [u8; 8] = [0x00, 0x00, 0x20, 0x00, 0x00, 0x00, 0xE0, 0xC1]; // -2147483649.0
+const F64_I32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x41]; // 2147483648.0
+const F64_I64_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC3]; // -9223372036854777856.0
+const F64_I64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x43]; // 9223372036854775808.0
+// The next value is determined manually and not via test:
+const F64_I128_LOWER: [u8; 8] = [0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0xC7]; // -170141183460469269510619166673045815296.0
+const F64_I128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xE0, 0x47]; // 170141183460469231731687303715884105728.0
+
+const F32_U_LOWER: [u8; 4] = [0x00, 0x00, 0x80, 0xBF]; // -1.0
+const F32_U8_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x43]; // 256.0
+const F32_U16_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x47]; // 65536.0
+const F32_U32_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x4F]; // 4294967296.0
+const F32_U64_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x5F]; // 18446744073709551616.0
+// The largest f32 value fits in a u128, so there is no upper bound
+const F32_U128_UPPER: [u8; 4] = [0x00, 0x00, 0x80, 0x7F]; // inf
+
+const F64_U_LOWER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0xBF]; // -1.0
+const F64_U8_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x70, 0x40]; // 256.0
+const F64_U16_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x40]; // 65536.0
+const F64_U32_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x41]; // 4294967296.0
+const F64_U64_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x43]; // 18446744073709551616.0
+const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]; // 340282366920938463463374607431768211456.0
+
+/// upper is the smallest `f32` that after truncation is strictly larger than i<N>::MAX or u<N>::MAX
+/// lower is the largest `f32` that after truncation is strictly smaller than i<N>::MIN or u<N>::MIN
+///
+/// For example, for `u8`, upper is 256.0 because the previous f32 (i.e.
+/// `256_f32.next_down()` which is 255.9999847412109375) when truncated is 255.0,
+/// which is not strictly larger than `u8::MAX`
+///
+/// For `i16`, upper is 32768.0 because the previous f32 (i.e.
+/// `32768_f32.next_down()`) when truncated is 32767,
+/// which is not strictly larger than `i16::MAX`
+///
+/// Note that all upper bound values are 2^(w-1) which can be precisely
+/// represented in f32 (verified using
+/// https://www.h-schmidt.net/FloatConverter/IEEE754.html)
+/// However, for lower bound values, which should be -2^(w-1)-1 (i.e.
+/// i<N>::MIN-1), not all of them can be represented in f32.
+/// For instance, for w = 32, -2^(31)-1 = -2,147,483,649, but this number does
+/// **not** have an f32 representation, and the next **smaller** number is
+/// -2,147,483,904. Note that CBMC for example uses the formula above which
+/// leads to bugs, e.g.: https://github.com/diffblue/cbmc/issues/8488
+
+/// For all unsigned types, lower is -1.0 because the next higher number, when
+/// truncated is -0.0 (or 0.0) which is not strictly smaller than `u<N>::MIN`
+fn get_bounds_f32(integral_ty: RigidTy, mm: &MachineModel) -> (f32, f32) {
+    match integral_ty {
+        RigidTy::Int(int_ty) => get_bounds_f32_int(int_ty, mm),
+        RigidTy::Uint(uint_ty) => get_bounds_f32_uint(uint_ty, mm),
+        _ => unreachable!(),
+    }
+}
+
+fn get_bounds_f64(integral_ty: RigidTy, mm: &MachineModel) -> (f64, f64) {
+    match integral_ty {
+        RigidTy::Int(int_ty) => get_bounds_f64_int(int_ty, mm),
+        RigidTy::Uint(uint_ty) => get_bounds_f64_uint(uint_ty, mm),
+        _ => unreachable!(),
+    }
+}
+
+fn get_bounds_f32_uint(uint_ty: UintTy, mm: &MachineModel) -> (f32, f32) {
+    let lower: f32 = f32::from_le_bytes(F32_U_LOWER);
+    let upper: f32 = match uint_ty {
+        UintTy::U8 => f32::from_le_bytes(F32_U8_UPPER),
+        UintTy::U16 => f32::from_le_bytes(F32_U16_UPPER),
+        UintTy::U32 => f32::from_le_bytes(F32_U32_UPPER),
+        UintTy::U64 => f32::from_le_bytes(F32_U64_UPPER),
+        UintTy::U128 => f32::from_le_bytes(F32_U128_UPPER),
+        UintTy::Usize => match mm.pointer_width {
+            32 => f32::from_le_bytes(F32_U32_UPPER),
+            64 => f32::from_le_bytes(F32_U64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+fn get_bounds_f64_uint(uint_ty: UintTy, mm: &MachineModel) -> (f64, f64) {
+    let lower = f64::from_le_bytes(F64_U_LOWER);
+    let upper = match uint_ty {
+        UintTy::U8 => f64::from_le_bytes(F64_U8_UPPER),
+        UintTy::U16 => f64::from_le_bytes(F64_U16_UPPER),
+        UintTy::U32 => f64::from_le_bytes(F64_U32_UPPER),
+        UintTy::U64 => f64::from_le_bytes(F64_U64_UPPER),
+        UintTy::U128 => f64::from_le_bytes(F64_U128_UPPER),
+        UintTy::Usize => match mm.pointer_width {
+            32 => f64::from_le_bytes(F64_U32_UPPER),
+            64 => f64::from_le_bytes(F64_U64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+fn get_bounds_f32_int(int_ty: IntTy, mm: &MachineModel) -> (f32, f32) {
+    let lower = match int_ty {
+        IntTy::I8 => f32::from_le_bytes(F32_I8_LOWER),
+        IntTy::I16 => f32::from_le_bytes(F32_I16_LOWER),
+        IntTy::I32 => f32::from_le_bytes(F32_I32_LOWER),
+        IntTy::I64 => f32::from_le_bytes(F32_I64_LOWER),
+        IntTy::I128 => f32::from_le_bytes(F32_I128_LOWER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f32::from_le_bytes(F32_I32_LOWER),
+            64 => f32::from_le_bytes(F32_I64_LOWER),
+            _ => unreachable!(),
+        },
+    };
+
+    let upper = match int_ty {
+        IntTy::I8 => f32::from_le_bytes(F32_I8_UPPER),
+        IntTy::I16 => f32::from_le_bytes(F32_I16_UPPER),
+        IntTy::I32 => f32::from_le_bytes(F32_I32_UPPER),
+        IntTy::I64 => f32::from_le_bytes(F32_I64_UPPER),
+        IntTy::I128 => f32::from_le_bytes(F32_I128_UPPER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f32::from_le_bytes(F32_I32_UPPER),
+            64 => f32::from_le_bytes(F32_I64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+fn get_bounds_f64_int(int_ty: IntTy, mm: &MachineModel) -> (f64, f64) {
+    let lower = match int_ty {
+        IntTy::I8 => f64::from_le_bytes(F64_I8_LOWER),
+        IntTy::I16 => f64::from_le_bytes(F64_I16_LOWER),
+        IntTy::I32 => f64::from_le_bytes(F64_I32_LOWER),
+        IntTy::I64 => f64::from_le_bytes(F64_I64_LOWER),
+        IntTy::I128 => f64::from_le_bytes(F64_I128_LOWER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f64::from_le_bytes(F64_I32_LOWER),
+            64 => f64::from_le_bytes(F64_I64_LOWER),
+            _ => unreachable!(),
+        },
+    };
+    let upper = match int_ty {
+        IntTy::I8 => f64::from_le_bytes(F64_I8_UPPER),
+        IntTy::I16 => f64::from_le_bytes(F64_I16_UPPER),
+        IntTy::I32 => f64::from_le_bytes(F64_I32_UPPER),
+        IntTy::I64 => f64::from_le_bytes(F64_I64_UPPER),
+        IntTy::I128 => f64::from_le_bytes(F64_I128_UPPER),
+        IntTy::Isize => match mm.pointer_width {
+            32 => f64::from_le_bytes(F64_I32_UPPER),
+            64 => f64::from_le_bytes(F64_I64_UPPER),
+            _ => unreachable!(),
+        },
+    };
+    (lower, upper)
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use num::BigInt;
+    use num::FromPrimitive;
+
+    macro_rules! check_lower_f32 {
+        ($val:ident, $min:expr) => {
+            let f = f32::from_le_bytes($val);
+            assert!(BigInt::from_f32(f.trunc()).unwrap() < BigInt::from($min));
+            assert!(BigInt::from_f32(f.next_up().trunc()).unwrap() >= BigInt::from($min));
+        };
+    }
+
+    macro_rules! check_upper_f32 {
+        ($val:ident, $max:expr) => {
+            let f = f32::from_le_bytes($val);
+            assert!(BigInt::from_f32(f.trunc()).unwrap() > BigInt::from($max));
+            assert!(BigInt::from_f32(f.next_down().trunc()).unwrap() <= BigInt::from($max));
+        };
+    }
+
+    #[test]
+    fn check_f32_bounds() {
+        // check that the bounds are correct, i.e. that for lower (upper) bounds:
+        //   1. the value when truncated is strictly smaller (larger) than i<N>::MIN or u<N>::MIN (i<N>::MAX or u<N>::MAX)
+        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to i<N>::MIN or u<N>::MIN (i<N>::MAX or u<N>::MAX)
+
+        check_lower_f32!(F32_U_LOWER, u8::MIN);
+
+        check_upper_f32!(F32_U8_UPPER, u8::MAX);
+        check_upper_f32!(F32_U16_UPPER, u16::MAX);
+        check_upper_f32!(F32_U32_UPPER, u32::MAX);
+        check_upper_f32!(F32_U64_UPPER, u64::MAX);
+        // 128 is not needed because the upper bounds is infinity
+        // Instead, check that `u128::MAX` is larger than the largest f32 value
+        assert!(f32::MAX < u128::MAX as f32);
+
+        check_lower_f32!(F32_I8_LOWER, i8::MIN);
+        check_lower_f32!(F32_I16_LOWER, i16::MIN);
+        check_lower_f32!(F32_I32_LOWER, i32::MIN);
+        check_lower_f32!(F32_I64_LOWER, i64::MIN);
+        check_lower_f32!(F32_I128_LOWER, i128::MIN);
+
+        check_upper_f32!(F32_I8_UPPER, i8::MAX);
+        check_upper_f32!(F32_I16_UPPER, i16::MAX);
+        check_upper_f32!(F32_I32_UPPER, i32::MAX);
+        check_upper_f32!(F32_I64_UPPER, i64::MAX);
+        check_upper_f32!(F32_I128_UPPER, i128::MAX);
+    }
+
+    macro_rules! check_lower_f64 {
+        ($val:ident, $min:expr) => {
+            let f = f64::from_le_bytes($val);
+            assert!(BigInt::from_f64(f.trunc()).unwrap() < BigInt::from($min));
+            assert!(BigInt::from_f64(f.next_up().trunc()).unwrap() >= BigInt::from($min));
+        };
+    }
+
+    macro_rules! check_upper_f64 {
+        ($val:ident, $max:expr) => {
+            let f = f64::from_le_bytes($val);
+            assert!(BigInt::from_f64(f.trunc()).unwrap() > BigInt::from($max));
+            assert!(BigInt::from_f64(f.next_down().trunc()).unwrap() <= BigInt::from($max));
+        };
+    }
+
+    #[test]
+    fn check_f64_bounds() {
+        // check that the bounds are correct, i.e. that for lower (upper) bounds:
+        //   1. the value when truncated is strictly smaller (larger) than {i, u}<N>::MIN ({i, u}<N>::MAX)
+        //   2. the next higher (lower) value when truncated is greater (smaller) than or equal to {i, u}<N>::MIN ({i, u}<N>::MAX)
+
+        check_lower_f64!(F64_U_LOWER, u8::MIN);
+
+        check_upper_f64!(F64_U8_UPPER, u8::MAX);
+        check_upper_f64!(F64_U16_UPPER, u16::MAX);
+        check_upper_f64!(F64_U32_UPPER, u32::MAX);
+        check_upper_f64!(F64_U64_UPPER, u64::MAX);
+        check_upper_f64!(F64_U128_UPPER, u128::MAX);
+
+        check_lower_f64!(F64_I8_LOWER, i8::MIN);
+        check_lower_f64!(F64_I16_LOWER, i16::MIN);
+        check_lower_f64!(F64_I32_LOWER, i32::MIN);
+        check_lower_f64!(F64_I64_LOWER, i64::MIN);
+        check_lower_f64!(F64_I128_LOWER, i128::MIN);
+
+        check_upper_f64!(F64_I8_UPPER, i8::MAX);
+        check_upper_f64!(F64_I16_UPPER, i16::MAX);
+        check_upper_f64!(F64_I32_UPPER, i32::MAX);
+        check_upper_f64!(F64_I64_UPPER, i64::MAX);
+        check_upper_f64!(F64_I128_UPPER, i128::MAX);
+    }
+
+    macro_rules! find_upper_fn {
+        ($fn_name:ident, $float_ty:ty) => {
+            fn $fn_name(start: u128) -> $float_ty {
+                let mut current = start + 1;
+                let mut f = current as $float_ty;
+
+                while f.trunc() as u128 <= start {
+                    let f1 = (current + 1) as $float_ty;
+                    let f2 = f.next_up();
+                    f = if f1 > f2 { f1 } else { f2 };
+                    current = f as u128;
+                }
+                f
+            }
+        };
+    }
+
+    macro_rules! find_lower_fn {
+        ($fn_name:ident, $float_ty:ty) => {
+            fn $fn_name(start: i128) -> $float_ty {
+                let mut current = start - 1;
+                let mut f = current as $float_ty;
+
+                while f.trunc() >= start as $float_ty {
+                    let f1 = (current - 1) as $float_ty;
+                    let f2 = f.next_down();
+                    f = if f1 < f2 { f1 } else { f2 };
+                    current = f as i128;
+                }
+                f
+            }
+        };
+    }
+
+    find_lower_fn!(find_lower_f32, f32);
+    find_upper_fn!(find_upper_f32, f32);
+    find_lower_fn!(find_lower_f64, f64);
+    find_upper_fn!(find_upper_f64, f64);
+
+    macro_rules! find_and_print {
+        (f32, $var_name:expr, $fn_name:ident, $start:expr) => {
+            let f = $fn_name($start);
+            let bytes = f.to_le_bytes();
+            println!("const {}: [u8; 4] = [0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}]; // {f:.1}", $var_name, bytes[0], bytes[1], bytes[2], bytes[3]);
+        };
+        (f64, $var_name:expr, $fn_name:ident, $start:expr) => {
+            let f = $fn_name($start);
+            let bytes = f.to_le_bytes();
+            println!("const {}: [u8; 8] = [0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}, 0x{:02X}]; // {f:.1}", $var_name, bytes[0], bytes[1], bytes[2], bytes[3], bytes[4], bytes[5], bytes[6], bytes[7]);
+        };
+    }
+
+    #[test]
+    /// This test generates most of the bounds. To run it do:
+    /// `cargo test -p kani-compiler generate_bounds -- --nocapture`
+    fn generate_bounds() {
+        find_and_print!(f32, "F32_I8_LOWER", find_lower_f32, i8::MIN as i128);
+        find_and_print!(f32, "F32_I8_UPPER", find_upper_f32, i8::MAX as u128);
+        find_and_print!(f32, "F32_I16_LOWER", find_lower_f32, i16::MIN as i128);
+        find_and_print!(f32, "F32_I16_UPPER", find_upper_f32, i16::MAX as u128);
+        find_and_print!(f32, "F32_I32_LOWER", find_lower_f32, i32::MIN as i128);
+        find_and_print!(f32, "F32_I32_UPPER", find_upper_f32, i32::MAX as u128);
+        find_and_print!(f32, "F32_I64_LOWER", find_lower_f32, i64::MIN as i128);
+        find_and_print!(f32, "F32_I64_UPPER", find_upper_f32, i64::MAX as u128);
+        // cannot use because of overflow
+        //find_and_print!(f32, "F32_I128_LOWER", find_lower_f32, i128::MIN as i128);
+        find_and_print!(f32, "F32_I128_UPPER", find_upper_f32, i128::MAX as u128);
+        println!();
+        find_and_print!(f64, "F64_I8_LOWER", find_lower_f64, i8::MIN as i128);
+        find_and_print!(f64, "F64_I8_UPPER", find_upper_f64, i8::MAX as u128);
+        find_and_print!(f64, "F64_I16_LOWER", find_lower_f64, i16::MIN as i128);
+        find_and_print!(f64, "F64_I16_UPPER", find_upper_f64, i16::MAX as u128);
+        find_and_print!(f64, "F64_I32_LOWER", find_lower_f64, i32::MIN as i128);
+        find_and_print!(f64, "F64_I32_UPPER", find_upper_f64, i32::MAX as u128);
+        find_and_print!(f64, "F64_I64_LOWER", find_lower_f64, i64::MIN as i128);
+        find_and_print!(f64, "F64_I64_UPPER", find_upper_f64, i64::MAX as u128);
+        // cannot use because of overflow
+        //find_and_print!(f64, "F64_I128_LOWER", find_lower_f64, i128::MIN as i128);
+        find_and_print!(f64, "F64_I128_UPPER", find_upper_f64, i128::MAX as u128);
+        println!();
+        find_and_print!(f32, "F32_U_LOWER", find_lower_f32, u8::MIN as i128);
+        find_and_print!(f32, "F32_U8_UPPER", find_upper_f32, u8::MAX as u128);
+        find_and_print!(f32, "F32_U16_UPPER", find_upper_f32, u16::MAX as u128);
+        find_and_print!(f32, "F32_U32_UPPER", find_upper_f32, u32::MAX as u128);
+        find_and_print!(f32, "F32_U64_UPPER", find_upper_f32, u64::MAX as u128);
+        // cannot use because of overflow
+        //find_and_print!(f32, "F32_U128_UPPER", find_upper_f32, u128::MAX as u128);
+        println!();
+        find_and_print!(f64, "F64_U_LOWER", find_lower_f64, u8::MIN as i128);
+        find_and_print!(f64, "F64_U8_UPPER", find_upper_f64, u8::MAX as u128);
+        find_and_print!(f64, "F64_U16_UPPER", find_upper_f64, u16::MAX as u128);
+        find_and_print!(f64, "F64_U32_UPPER", find_upper_f64, u32::MAX as u128);
+        find_and_print!(f64, "F64_U64_UPPER", find_upper_f64, u64::MAX as u128);
+        // cannot use because of overflow
+        //find_and_print!(f64, "F64_U128_UPPER", find_upper_f64, u128::MAX as u128);
+    }
+}
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs
index 9d832146e3e8..8f176510d348 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/mod.rs
@@ -4,12 +4,14 @@
 //! This module provides utils used across Kani
 
 mod debug;
+mod float_utils;
 mod names;
 #[allow(clippy::module_inception)]
 mod utils;
 
 // TODO clean this up
 
+pub use float_utils::*;
 pub use names::*;
 pub use utils::*;
 

From 7cce2a37b201ca7354c570bda585294f93fdefa6 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <zyadh@amazon.com>
Date: Tue, 5 Nov 2024 21:03:22 -0800
Subject: [PATCH 9/9] Clippy fix

---
 kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
index 3de22fc8d55e..a50353b7c96d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs
@@ -132,7 +132,7 @@ const F64_U128_UPPER: [u8; 8] = [0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xF0, 0x47]
 /// **not** have an f32 representation, and the next **smaller** number is
 /// -2,147,483,904. Note that CBMC for example uses the formula above which
 /// leads to bugs, e.g.: https://github.com/diffblue/cbmc/issues/8488
-
+///
 /// For all unsigned types, lower is -1.0 because the next higher number, when
 /// truncated is -0.0 (or 0.0) which is not strictly smaller than `u<N>::MIN`
 fn get_bounds_f32(integral_ty: RigidTy, mm: &MachineModel) -> (f32, f32) {