From 09a3aaad15d9e34d7004bce086847caead5e9e7a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Jul 2026 06:41:26 +0000 Subject: [PATCH] Fix unsound f128 -> i128 lower bound in float-to-int range check F128_I128_LOWER encoded -2^128, but the largest f128 less than or equal to i128::MIN - 1 is -(2^127 + 2^15): f128 has a 113-bit significand, so the ulp at magnitude 2^127 is 2^15. With the exclusive greater-than comparison used by codegen_in_range_expr, the wrong constant admitted every f128 in (-2^128, -(2^127 + 2^15)], all of which truncate below i128::MIN, making both kani::float::float_to_int_in_range and the UB check for the float_to_int_unchecked intrinsic unsound for this type pair. All 60 bound constants were validated against exact rational arithmetic; F128_I128_LOWER is the only incorrect one. The bug dates back to the introduction of f128 support (#3701) but was masked by CBMC's out-of-range float-to-int conversion behavior until the CBMC 6.10 upgrade, when the checked_f128_to_int_unchecked_i128 harness in verify-rust-std started failing. Add regression harnesses covering both the exact boundary values and the symbolic form of the verify-rust-std harness that caught this. Resolves: #4662 Co-authored-by: Kiro --- .../utils/float_utils.rs | 2 +- tests/kani/FloatToIntInRange/test.rs | 30 +++++++++++++++++++ 2 files changed, 31 insertions(+), 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 cea999cba563..84acf23cf2dc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs @@ -160,7 +160,7 @@ const F128_I64_UPPER: [u8; 16] = [ 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x3E, 0x40, ]; const F128_I128_LOWER: [u8; 16] = [ - 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7F, 0xC0, + 0x01, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7E, 0xC0, ]; const F128_I128_UPPER: [u8; 16] = [ 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x7E, 0x40, diff --git a/tests/kani/FloatToIntInRange/test.rs b/tests/kani/FloatToIntInRange/test.rs index 2fca679f477a..354dc7f6106d 100644 --- a/tests/kani/FloatToIntInRange/test.rs +++ b/tests/kani/FloatToIntInRange/test.rs @@ -1,6 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfloat-lib +#![feature(f128)] //! This test checks that `kani::float::float_to_int_in_range` works as expected @@ -24,3 +25,32 @@ fn check_float_to_int_in_range() { let i: u32 = unsafe { f.to_int_unchecked() }; assert_eq!(i, 1_000_000); } + +/// The `f128` -> `i128` lower bound used to be wrong (-2^128 instead of +/// -(2^127 + 2^15)), so `float_to_int_in_range` accepted values whose +/// truncation is below `i128::MIN`. +/// See https://github.com/model-checking/kani/issues/4662 +#[kani::proof] +fn check_f128_to_i128_in_range_boundary() { + // i128::MIN is exactly representable in f128 and must be accepted... + let f: f128 = i128::MIN as f128; + assert!(kani::float::float_to_int_in_range::(f)); + let i: i128 = unsafe { f.to_int_unchecked() }; + assert_eq!(i, i128::MIN); + + // ...but the next f128 below it (-(2^127 + 2^15), whose truncation is + // out of range) must be rejected. + let g: f128 = -170141183460469231731687303715884138496.0; + assert!(!kani::float::float_to_int_in_range::(g)); +} + +/// Symbolic variant, mirroring the harness in verify-rust-std that caught +/// the wrong bound: for any value that `float_to_int_in_range` accepts, +/// `to_int_unchecked` must agree with the saturating `as` cast. +#[kani::proof] +fn check_f128_to_i128_in_range_symbolic() { + let f: f128 = kani::any(); + kani::assume(kani::float::float_to_int_in_range::(f)); + let i: i128 = unsafe { f.to_int_unchecked() }; + assert_eq!(i, f as i128); +}