Fix float-to-int saturating cast bug

cprover_bindings/src/goto_program/expr.rs

@@ -262,6 +262,10 @@ pub enum UnaryOperator {
     IsDynamicObject,
     /// `isfinite(self)`
     IsFinite,
+    /// `isinf(self)`
+    IsInf,
+    /// `isnan(self)`
+    IsNan,
     /// `!self`
     Not,
     /// `__CPROVER_OBJECT_SIZE(self)`
@@ -1402,7 +1406,7 @@ impl Expr {
             Bitnot | BitReverse | Bswap | Popcount => arg.typ.is_integer(),
             CountLeadingZeros { .. } | CountTrailingZeros { .. } => arg.typ.is_integer(),
             IsDynamicObject | ObjectSize | PointerObject => arg.typ().is_pointer(),
-            IsFinite => arg.typ().is_floating_point(),
+            IsFinite | IsInf | IsNan => arg.typ().is_floating_point(),
             PointerOffset => arg.typ == Type::void_pointer(),
             Not => arg.typ.is_bool(),
             UnaryMinus => arg.typ().is_numeric(),
@@ -1415,7 +1419,7 @@ impl Expr {
             CountLeadingZeros { .. } | CountTrailingZeros { .. } => Type::unsigned_int(32),
             ObjectSize | PointerObject => Type::size_t(),
             PointerOffset => Type::ssize_t(),
-            IsDynamicObject | IsFinite | Not => Type::bool(),
+            IsDynamicObject | IsFinite | IsInf | IsNan | Not => Type::bool(),
             Popcount => Type::unsigned_int(32),
         }
     }
@@ -1451,6 +1455,16 @@ impl Expr {
         self.unop(IsFinite)
     }
 
+    /// `isinf(self)`
+    pub fn is_inf(self) -> Self {
+        self.unop(IsInf)
+    }
+
+    /// `isnan(self)`
+    pub fn is_nan(self) -> Self {
+        self.unop(IsNan)
+    }
+
     /// `-self`
     pub fn neg(self) -> Expr {
         self.unop(UnaryMinus)

cprover_bindings/src/irep/to_irep.rs

@@ -117,6 +117,8 @@ impl ToIrepId for UnaryOperator {
             UnaryOperator::CountTrailingZeros { .. } => IrepId::CountTrailingZeros,
             UnaryOperator::IsDynamicObject => IrepId::IsDynamicObject,
             UnaryOperator::IsFinite => IrepId::IsFinite,
+            UnaryOperator::IsInf => IrepId::Isinf,
+            UnaryOperator::IsNan => IrepId::Isnan,
             UnaryOperator::Not => IrepId::Not,
             UnaryOperator::ObjectSize => IrepId::ObjectSize,
             UnaryOperator::PointerObject => IrepId::PointerObject,

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -27,8 +27,8 @@ use rustc_public::mir::{
 };
 use rustc_public::rustc_internal;
 use rustc_public::ty::{
-    Binder, ClosureKind, ExistentialPredicate, IntTy, RigidTy, Size, Ty, TyConst, TyKind, UintTy,
-    VariantIdx,
+    Binder, ClosureKind, ExistentialPredicate, FloatTy, IntTy, RigidTy, Size, Ty, TyConst, TyKind,
+    UintTy, VariantIdx,
 };
 use std::collections::BTreeMap;
 use tracing::{debug, trace, warn};
@@ -1086,6 +1086,15 @@ impl GotocCtx<'_, '_> {
         let src_ty_kind = src_ty.kind();
         let dst_ty_kind = dst_ty.kind();
 
+        // Float to integer casting requires special handling for saturating semantics.
+        // Since Rust 1.45, the `as` keyword performs a saturating cast when casting
+        // from float to int. See https://doc.rust-lang.org/reference/expressions/operator-expr.html#numeric-cast
+        if let TyKind::RigidTy(RigidTy::Float(_)) = src_ty_kind
+            && dst_ty_kind.is_integral()
+        {
+            return self.codegen_float_to_int_saturating_cast(src, dst_ty);
+        }
+
         // number casting
         if src_ty_kind.is_numeric() && dst_ty_kind.is_numeric() {
             return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_ty));
@@ -1162,6 +1171,143 @@ impl GotocCtx<'_, '_> {
         }
     }
 
+    /// Codegen a float-to-int cast with Rust's saturating semantics.
+    ///
+    /// Since Rust 1.45, the `as` keyword performs a *saturating cast* when casting from float to int:
+    /// - If the value is NaN, the result is 0
+    /// - If the value exceeds the upper bound, the result is MAX
+    /// - If the value is below the lower bound, the result is MIN (or 0 for unsigned types)
+    /// - If the value is positive infinity, the result is MAX
+    /// - If the value is negative infinity, the result is MIN (or 0 for unsigned types)
+    /// - Otherwise, the value is truncated toward zero
+    ///
+    /// See: https://doc.rust-lang.org/reference/expressions/operator-expr.html#numeric-cast
+    fn codegen_float_to_int_saturating_cast(&mut self, src: &Operand, dst_ty: Ty) -> Expr {
+        let src_expr = self.codegen_operand_stable(src);
+        let dst_goto_ty = self.codegen_ty_stable(dst_ty);
+        let mm = self.symbol_table.machine_model();
+
+        // Get the integer type bounds
+        let int_min = dst_goto_ty.min_int_expr(mm);
+        let int_max = dst_goto_ty.max_int_expr(mm);
+
+        // Get the source float type for creating bound constants
+        let src_ty = self.operand_ty_stable(src);
+
+        // Get the integer bounds as float constants for comparison.
+        // Note: We convert the integer bounds to float for comparison.
+        // For very large integer types (i128, u128), the float conversion may lose precision,
+        // but this is acceptable because:
+        // 1. Any float value that's truly larger than MAX_INT will still compare as > MAX_INT
+        // 2. Any float value that's truly smaller than MIN_INT will still compare as < MIN_INT
+        let int_min_as_float = self.int_bounds_as_float(dst_ty, false, src_ty);
+        let int_max_as_float = self.int_bounds_as_float(dst_ty, true, src_ty);
+
+        // Determine if the destination type is signed
+        let dst_is_signed = matches!(dst_ty.kind(), TyKind::RigidTy(RigidTy::Int(_)));
+
+        // Check for special cases:
+        // 1. isnan(src) -> result is 0
+        // 2. src > int_max -> result is MAX
+        // 3. src < int_min -> result is MIN (or 0 for unsigned)
+        // 4. Otherwise -> truncate toward zero
+        let is_nan = src_expr.clone().is_nan();
+        let above_max = src_expr.clone().gt(int_max_as_float.clone());
+        let below_min = src_expr.clone().lt(int_min_as_float);
+
+        // The truncated value (normal cast behavior for values in range)
+        let truncated = src_expr.cast_to(dst_goto_ty.clone());
+
+        // Build the nested ternary expression:
+        // below_min ? MIN : (above_max ? MAX : (isnan ? 0 : truncated))
+        let int_zero = dst_goto_ty.zero();
+        let min_value = if dst_is_signed { int_min } else { int_zero.clone() };
+
+        // Note: For positive infinity, above_max will be true.
+        // For negative infinity, below_min will be true.
+        // So infinity cases are handled by the bounds checks.
+        below_min
+            .ternary(min_value, above_max.ternary(int_max, is_nan.ternary(int_zero, truncated)))
+    }
+
+    /// Convert an integer bound (min or max) to a float constant for the given float type.
+    fn int_bounds_as_float(&self, int_ty: Ty, is_max: bool, float_ty: Ty) -> Expr {
+        let mm = self.symbol_table.machine_model();
+
+        // Get the integer bound value
+        let bound_value: f64 = match int_ty.kind() {
+            TyKind::RigidTy(RigidTy::Int(int_kind)) => {
+                if is_max {
+                    match int_kind {
+                        IntTy::I8 => i8::MAX as f64,
+                        IntTy::I16 => i16::MAX as f64,
+                        IntTy::I32 => i32::MAX as f64,
+                        IntTy::I64 => i64::MAX as f64,
+                        IntTy::I128 => i128::MAX as f64,
+                        IntTy::Isize => {
+                            if mm.pointer_width == 32 {
+                                i32::MAX as f64
+                            } else {
+                                i64::MAX as f64
+                            }
+                        }
+                    }
+                } else {
+                    match int_kind {
+                        IntTy::I8 => i8::MIN as f64,
+                        IntTy::I16 => i16::MIN as f64,
+                        IntTy::I32 => i32::MIN as f64,
+                        IntTy::I64 => i64::MIN as f64,
+                        IntTy::I128 => i128::MIN as f64,
+                        IntTy::Isize => {
+                            if mm.pointer_width == 32 {
+                                i32::MIN as f64
+                            } else {
+                                i64::MIN as f64
+                            }
+                        }
+                    }
+                }
+            }
+            TyKind::RigidTy(RigidTy::Uint(uint_kind)) => {
+                if is_max {
+                    match uint_kind {
+                        UintTy::U8 => u8::MAX as f64,
+                        UintTy::U16 => u16::MAX as f64,
+                        UintTy::U32 => u32::MAX as f64,
+                        UintTy::U64 => u64::MAX as f64,
+                        UintTy::U128 => u128::MAX as f64,
+                        UintTy::Usize => {
+                            if mm.pointer_width == 32 {
+                                u32::MAX as f64
+                            } else {
+                                u64::MAX as f64
+                            }
+                        }
+                    }
+                } else {
+                    0.0 // MIN for unsigned is always 0
+                }
+            }
+            _ => unreachable!("Expected integer type"),
+        };
+
+        // Create the float constant in the appropriate float type
+        match float_ty.kind() {
+            TyKind::RigidTy(RigidTy::Float(FloatTy::F16)) => {
+                Expr::float16_constant(bound_value as f16)
+            }
+            TyKind::RigidTy(RigidTy::Float(FloatTy::F32)) => {
+                Expr::float_constant(bound_value as f32)
+            }
+            TyKind::RigidTy(RigidTy::Float(FloatTy::F64)) => Expr::double_constant(bound_value),
+            TyKind::RigidTy(RigidTy::Float(FloatTy::F128)) => {
+                Expr::float128_constant(bound_value as f128)
+            }
+            _ => unreachable!("Expected float type"),
+        }
+    }
+
     /// "Pointer casts" are particular kinds of pointer-to-pointer casts.
     /// See the [`PointerCoercion`] type for specifics.
     /// Note that this does not include all casts involving pointers,

tests/kani/Cast/float_to_int_saturating.rs

@@ -0,0 +1,70 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Regression test for float-to-int saturating cast (GitHub issue #4536).
+//! Since Rust 1.45, `as` performs saturating casts from float to int.
+
+// Test case from issue #4536
+#[kani::proof]
+fn check_issue_4536_f32_to_u8() {
+    let x: f32 = 300.0;
+    let y: u8 = x as u8;
+    assert!(y == 255); // Should saturate to u8::MAX
+}
+
+// f32 saturating casts
+#[kani::proof]
+fn check_f32_to_u8_above_max() {
+    let y: u8 = 300.0f32 as u8;
+    assert!(y == u8::MAX);
+}
+
+#[kani::proof]
+fn check_f32_to_u8_below_min() {
+    let y: u8 = (-10.0f32) as u8;
+    assert!(y == 0);
+}
+
+#[kani::proof]
+fn check_f32_to_u8_nan() {
+    let y: u8 = f32::NAN as u8;
+    assert!(y == 0);
+}
+
+#[kani::proof]
+fn check_f32_to_u8_infinity() {
+    let y: u8 = f32::INFINITY as u8;
+    assert!(y == u8::MAX);
+}
+
+#[kani::proof]
+fn check_f32_to_i8_above_max() {
+    let y: i8 = 200.0f32 as i8;
+    assert!(y == i8::MAX);
+}
+
+#[kani::proof]
+fn check_f32_to_i8_below_min() {
+    let y: i8 = (-200.0f32) as i8;
+    assert!(y == i8::MIN);
+}
+
+// f64 saturating casts
+#[kani::proof]
+fn check_f64_to_u8_above_max() {
+    let y: u8 = 300.0f64 as u8;
+    assert!(y == u8::MAX);
+}
+
+#[kani::proof]
+fn check_f64_to_i8_below_min() {
+    let y: i8 = (-200.0f64) as i8;
+    assert!(y == i8::MIN);
+}
+
+// In-range casts should truncate toward zero
+#[kani::proof]
+fn check_f32_truncation() {
+    let y: i8 = (-99.9f32) as i8;
+    assert!(y == -99);
+}