Repository navigation
Evaluate overflow_checks() to the session's setting - #4980
srivatsansamraj wants to merge 2 commits into
Conversation
|
@CYJ904 @Tianshu-Huang @wodex1nhaoIeng @acearyanarun for review. Rust's |
github-actions
Bot
added
Z-EndToEndBenchCI
f0dfe67 to
990fadc
Compare
There was a problem hiding this comment.
Warning
Copilot couldn't run its full agentic review because it didn't start before the timeout. Make sure your repository has a runner available, or add a copilot-code-review.yml file specifying one with the runs-on attribute. See the docs for more details.
Copilot review overview
2 open issues
What changed in this PR
Aligns Kani’s codegen behavior for core::intrinsics::overflow_checks() with the active rustc session overflow-checks setting, fixing incorrect library branching that previously masked overflows/panics.
Changes:
- Evaluate
Operand::RuntimeChecks::OverflowChecksusingtcx.sess.overflow_checks()instead of hard-codingfalse. - Keep
ub_checks()andcontract_checks()evaluated tofalsewhen they reach codegen. - Add a regression test and expected output to ensure
overflow_checks()istrueand overflow-dependent library behavior matches Rust.
| File | Description |
|---|---|
| tests/expected/intrinsics/overflow-checks/main.rs | Adds regression harnesses covering overflow_checks(), pow, funnel shifts, and RangeFrom overflow behavior. |
| tests/expected/intrinsics/overflow-checks/expected | Captures expected Kani results demonstrating panic/assertion failures for overflow paths and correct harness counts. |
| kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs | Implements session-driven evaluation for OverflowChecks while leaving UbChecks/ContractChecks disabled. |
Review effort: Lite
| @@ -0,0 +1,19 @@ | |||
| check_overflow_checks_intrinsic.assertion\ | |||
| Status: SUCCESS\ | |||
| Description: "assertion failed: core::intrinsics::overflow_checks()" | |||
There was a problem hiding this comment.
Status: SUCCESS is the assertion holding, which is the expected result here.
|
|
||
| #[kani::proof] | ||
| fn check_funnel_shl_overflow() { | ||
| let _ = u32::MAX.funnel_shl(u32::MAX, u32::BITS); |
There was a problem hiding this comment.
Done in 7a1933b49: both harnesses that rely on a panic now have a cover after the call.
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
The fix is right: overflow_checks() now matches the session's setting, as rustc does, so Kani reports the overflow panics a native build hits.
Before merge:
- Before this change, Kani reported success where a native build panics, so this is a soundness gap. Please add
[F] Soundnessand[C] Bug. - The expected output adds a failure in
<u8 as Step>::forward. Please say in the description whether it's intended, and why. - Please add a
kani::cover!marker tocheck_overflow_checks_intrinsic, like thepowharnesses. auditfails. Please confirm it fails onmain. Three jobs are cancelled. Please re-run them.
Kani evaluated every `Operand::RuntimeChecks` to `false`, including `overflow_checks()`, although it compiles every crate with `-Coverflow-checks=on` and refuses to run without it. Library code that branches on the intrinsic therefore took its path without overflow checks: `pow` on signed and unsigned integers wrapped instead of panicking on overflow (model-checking#4970), `funnel_shl` and `funnel_shr` wrapped the shift amount, and the iterator of `core::range::RangeFrom` reported an overflow one call before Rust panics. `overflow_checks()` now evaluates to the session's overflow-checks setting, as rustc's own codegen does, and `ub_checks()` and `contract_checks()` calls that reach codegen stay `false`. The arms name each variant, so a new kind of runtime check cannot fall into `false` unnoticed. `tests/expected/intrinsics/overflow-checks` checks that `overflow_checks()` itself is `true`, that unsigned and signed `pow` and `funnel_shl` report their overflow panics, that `2u32.pow(31)` still verifies, and that the `RangeFrom` iterator yields its maximum value and panics on the call after it. Without the change, the intrinsic check fails, the three overflow harnesses verify and the iterator fails at its maximum value.
The funnel shift and the `RangeFrom` harnesses passed only because the call panics; a cover after each call now fails the test if the call returns.
990fadc to
7a1933b
Compare
Kani evaluated every
Operand::RuntimeCheckstofalse, includingoverflow_checks(), although it compiles every crate with-Coverflow-checks=onand refuses to run without it. Library code that branches on the intrinsic took itsfalsebranch:powwrapped where Rust panics on overflow, so Kani reported success for code that panics (#4970);funnel_shlandfunnel_shrwrapped the shift amount; and the iterator ofcore::range::RangeFromreported an overflow one call before Rust panics.overflow_checks()now evaluates to the session's overflow-checks setting, as rustc's codegen does, andub_checks()andcontract_checks()calls that reach codegen stayfalse.On the standard library (verify-rust-std
cd371e035c7), the 18 automatic harnesses for unsignedpowand the funnel shifts now report the overflow panic in place of success, and the 6 for signedpowfail on the overflow in place of an unwinding assertion. The checked path costs more on symbolic inputs: thei128powautomatic harness went from 0.48 s to 10 s, and au64powwith symbolic base and exponent from 0.3-0.7 s to 53-109 s to find the overflow. Thetests/perfs2n-quic varint proofs, five of which callpowwith constant exponents, went from 49.5 s to 50.7 s.tests/expected/intrinsics/overflow-checkschecks thatoverflow_checks()istrue, that unsigned and signedpowandfunnel_shlreport their overflow panics, that2u32.pow(31)still verifies, and that theRangeFromiterator yields its maximum value and panics on the next call. Onmainthe intrinsic check fails, the three overflow harnesses verify and the iterator fails at its maximum value.Resolves #4970
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.