fix saturating float-to-int cast (#4573)

The issue is that Kani computes int_max_as_float by casting u64::MAX to
f64. But u64::MAX (2^64 - 1) isn't exactly representable in f64, so it
rounds *up* to 2^64. The old code used a greater-than operation, which
would mean a float value equal to exactly 2^64 fails this check, falls
through the raw truncation path, and produces a wrong result instead of
saturating to u64::MAX.

Instead we use greater-than-or-equal so that the boundary value 2^64
correctly saturates. This is safe for types where the max IS exactly
representable.

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

Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>

Author: Rexicon226

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

@@ -1198,7 +1198,7 @@ impl GotocCtx<'_, '_> {
         // 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
+        // 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);
@@ -1208,11 +1208,11 @@ impl GotocCtx<'_, '_> {
 
         // Check for special cases:
         // 1. isnan(src) -> result is 0
-        // 2. src > int_max -> result is MAX
+        // 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 above_max = src_expr.clone().ge(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)

tests/kani/Cast/float_to_int_saturating.rs

@@ -1,6 +1,8 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+#![feature(f128)]
+
 //! Regression test for float-to-int saturating cast (GitHub issue #4536).
 //! Since Rust 1.45, `as` performs saturating casts from float to int.
 
@@ -68,3 +70,17 @@ fn check_f32_truncation() {
     let y: i8 = (-99.9f32) as i8;
     assert!(y == -99);
 }
+
+#[kani::proof]
+fn check_f64_to_u64_saturation() {
+    let x: f64 = u64::MAX as f64; // = 2^64 in f64
+    let y: u64 = x as u64;
+    kani::assert(y == u64::MAX, "matches");
+}
+
+#[kani::proof]
+fn check_f64_to_u128_saturation() {
+    let x: f64 = u128::MAX as f64; // = 2^128 in f64
+    let y: u128 = x as u128;
+    kani::assert(y == u128::MAX, "matches");
+}