From b45a315f849b4963110a81bd82a4e51898a6a9a5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 11 Feb 2026 14:08:35 +0000 Subject: [PATCH 1/2] Fix float-to-int saturating cast bug Since Rust 1.45, the `as` keyword performs a *saturating cast* when casting from float to int. See [Rust Reference: Numeric cast](https://doc.rust-lang.org/reference/expressions/operator-expr.html#numeric-cast). Co-authored-by: Kani autonomous agent Resolves #4536 --- cprover_bindings/src/goto_program/expr.rs | 18 ++- cprover_bindings/src/irep/to_irep.rs | 2 + .../codegen_cprover_gotoc/codegen/rvalue.rs | 150 +++++++++++++++++- tests/kani/Cast/float_to_int_saturating.rs | 70 ++++++++ 4 files changed, 236 insertions(+), 4 deletions(-) create mode 100644 tests/kani/Cast/float_to_int_saturating.rs diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 0ebeeef7a023..72c01338c320 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/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) diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs index 688e7f64e874..cd263e2a3c9f 100644 --- a/cprover_bindings/src/irep/to_irep.rs +++ b/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, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 57103a915cbd..8c82a38644b2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/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: + // isnan ? 0 : (above_max ? MAX : (below_min ? MIN : 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, diff --git a/tests/kani/Cast/float_to_int_saturating.rs b/tests/kani/Cast/float_to_int_saturating.rs new file mode 100644 index 000000000000..16e110a4ff6e --- /dev/null +++ b/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); +} From 29168a978f6541acb6207939413e291478dac0f7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 11 Feb 2026 14:30:48 +0000 Subject: [PATCH 2/2] Fix comment --- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 8c82a38644b2..309627812706 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -1219,7 +1219,7 @@ impl GotocCtx<'_, '_> { let truncated = src_expr.cast_to(dst_goto_ty.clone()); // Build the nested ternary expression: - // isnan ? 0 : (above_max ? MAX : (below_min ? MIN : truncated)) + // 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() };