Fix float-to-int saturating cast bug

[tautschnig]

Since Rust 1.45, the as keyword performs a saturating cast when casting from float to int. See Rust Reference: Numeric cast.

Co-authored-by: Kani autonomous agent

Resolves #4536

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

[Copilot]

Pull request overview

This pull request fixes a bug where Kani was incorrectly implementing float-to-int casts. Since Rust 1.45, the as keyword performs saturating casts when converting from floating-point to integer types, but Kani was using wrapping (modulo) semantics instead. For example, 300.0f32 as u8 should produce 255 (saturating to u8::MAX), but Kani was incorrectly producing 44 (300 % 256).

Changes:

• Implemented saturating cast semantics for float-to-int conversions with proper handling of NaN, infinity, and out-of-bounds values
• Added comprehensive regression tests covering various edge cases of float-to-int saturating casts
• Extended expression bindings with IsNan and IsInf unary operators for CBMC integration

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

File	Description
tests/kani/Cast/float_to_int_saturating.rs	Regression tests for float-to-int saturating cast covering NaN, infinity, out-of-bounds, and in-range cases for f32 and f64
kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs	Core implementation of saturating cast logic with special handling for NaN (→0), infinity and out-of-bounds values (→MIN/MAX), and in-range truncation
cprover_bindings/src/goto_program/expr.rs	Added IsNan and IsInf unary operators and corresponding helper methods for float type checking
cprover_bindings/src/irep/to_irep.rs	Added IREP ID mappings for IsNan and IsInf operators to interface with CBMC

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.