Fix unsound f128 -> i128 lower bound in float-to-int range check#4663
Merged
tautschnig merged 3 commits intoJul 23, 2026
Merged
Conversation
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 (model-checking#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: model-checking#4662 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
github-actions
Bot
added
Z-EndToEndBenchCI
Contributor
There was a problem hiding this comment.
Pull request overview
This PR fixes an unsound lower-bound constant used by Kani’s float-to-int range checking for the f128 -> i128 conversion path in the CBMC backend, and adds regression harnesses to prevent the issue from reoccurring.
Changes:
- Correct
F128_I128_LOWERto the proper binary128 value corresponding to the next representablef128belowi128::MIN(i.e.,-(2^127 + 2^15)), closing an unsoundness in the range predicate used by bothkani::float::float_to_int_in_rangeand thefloat_to_int_uncheckedUB check. - Extend the existing
FloatToIntInRangeregression test to cover the exactf128/i128boundary and a symbolic harness mirroring the failing verify-rust-std scenario.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| tests/kani/FloatToIntInRange/test.rs | Adds f128 -> i128 boundary and symbolic proof harnesses to catch the previously-admitted out-of-range values. |
| kani-compiler/src/codegen_cprover_gotoc/utils/float_utils.rs | Fixes the binary128 lower-bound byte pattern used by the backend-generated in-range expression for f128 -> i128. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
added a commit
to model-checking/verify-rust-std
that referenced
this pull request
Jul 20, 2026
Two harness failures surfaced in CI once compilation was fixed: * alloc::layout::verify::check_repeat: rust-lang#148769 changed Layout::repeat to not include padding after the trailing element, so on success the resulting size is (n - 1) * stride + self.size() rather than n * stride. Our postcondition size >= stride is thus violated for n == 1 whenever self needs padding (e.g. size 6, align 4: size 6 < stride 8). Update the exact (non-kani) postconditions to the new semantics and weaken the Kani-checkable variant to n <= 1 || size >= stride. * num::verify::checked_f128_to_int_unchecked_i128: Kani's f128 -> i128 lower bound in float_to_int_in_range is unsound (-2^128 instead of -(2^127 + 2^15)), so the contract instrumentation admits values that truncate below i128::MIN; the CBMC 6.10 upgrade in the new Kani pin exposed this (previously such conversions happened to saturate the same way as the 'as' oracle). Reported as model-checking/kani#4662, fix proposed in model-checking/kani#4663. Until that fix is in the pinned Kani version, hand-write this harness with an explicit sound input range. Verified locally with the pinned Kani commit: both harnesses pass, and 'cargo check -p core' stays clean. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
feliperodri
approved these changes
Jul 21, 2026
github-merge-queue
Bot
removed this pull request from the merge queue due to failed status checks
Jul 21, 2026
tautschnig
enabled auto-merge
July 23, 2026 18:11
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
F128_I128_LOWERinfloat_utils.rsencoded-2^128, but the largest f128 less than or equal toi128::MIN - 1is-(2^127 + 2^15)(f128 has a 113-bit significand, so the ulp at magnitude 2^127 is 2^15). With the exclusive>comparison used bycodegen_in_range_expr, the wrong constant admitted every f128 in(-2^128, -(2^127 + 2^15)]— all of which truncate belowi128::MIN— making bothkani::float::float_to_int_in_rangeand the UB check for thefloat_to_int_uncheckedintrinsic unsound for thef128 -> i128pair. See #4662 for the full analysis.I validated all 60
F{16,32,64,128}_{I,U}*_{LOWER,UPPER}constants against exact rational arithmetic;F128_I128_LOWERis the only incorrect one. The bug dates back to the introduction of f16/f128 support (#3701) but was masked by CBMC's out-of-range conversion behavior until the CBMC 6.10 upgrade, at which point thenum::verify::checked_f128_to_int_unchecked_i128harness in verify-rust-std (model-checking/verify-rust-std#613) began failing.Manual testing performed:
tests/kaniFloatToInt suite andtests/expectedfloat suites pass.num::verify::checked_f128_to_int_unchecked_i128verifies successfully with the fixed compiler.Resolves #4662
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.