Skip to content

Fix a bug codegening SwitchInts with only an otherwise branch #4095

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 3 commits into from
May 25, 2025
Merged

Fix a bug codegening SwitchInts with only an otherwise branch #4095

merged 3 commits into from
May 25, 2025
+45 −26

Conversation

bkirwi
Copy link
Contributor

@bkirwi bkirwi commented May 21, 2025 •
edited by carolynzech
Loading

The first commit adds a failing test: it exposes a bug dealing with dropping single-variant enums.

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:499:9:
assertion failed: targets.len() > 1
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: std::ptr::drop_in_place::<Reference>
_RINvNtCs4AkhfejoRTd_4core3ptr13drop_in_placeNtCs6S0fALEP9ee_19single_variant_enum9ReferenceEBI_
[Kani] current codegen location: Loc { file: "/Users/bkirwi/.rustup/toolchains/nightly-2025-05-20-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/mod.rs", function: None, start_line: 524, start_col: Some(1), end_line: 524, end_col: Some(56), pragmas: [] }
error: /Users/bkirwi/Code/kani/target/kani/bin/kani-compiler exited with status exit status: 101

This seems to affect both main and the latest release.

Resolves #4103

@bkirwi bkirwi requested a review from a team as a code owner May 21, 2025 20:42
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label May 21, 2025
@carolynzech carolynzech changed the title Fix a bug in single-variant enum handling Fix a bug codegening SwitchInts with only an otherwise branch May 25, 2025
carolynzech
carolynzech approved these changes May 25, 2025
View reviewed changes
Copy link
Contributor

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! Your fix looks good. I moved your test to a different folder--we like to put any test that fixes a crash in the kani subdirectory instead of ui. (If you're curious why, the ui folder has expected files where we assert that some particular substring is in the printed output. Here, we just care that the exit code is 0, i.e. that the proof went through successfully, which all we check for tests in the kani folder).

I also filed #4103 to document the bug for posterity. Thanks a lot for finding and fixing this!

@carolynzech carolynzech enabled auto-merge May 25, 2025 12:55
@carolynzech carolynzech added this pull request to the merge queue May 25, 2025
Merged via the queue into model-checking:main with commit 1612594 May 25, 2025
25 of 26 checks passed
github-merge-queue bot pushed a commit that referenced this pull request Jun 9, 2025
@zhassan-aws @carolynzech
Bump Kani Version (#4147)
37fb634 
These are the automatically-generated release notes:
```
## What's Changed
* Toolchain upgrade to nightly-2025-05-04 by @thanhnguyen-aws in #4059
* Automatic toolchain upgrade to nightly-2025-05-05 by @github-actions in #4060
* Automatic toolchain upgrade to nightly-2025-05-06 by @github-actions in #4061
* Enable target features: x87 and sse2 by @thanhnguyen-aws in #4062
* Fix the bug: Loop contracts are not composable with function contracts  by @thanhnguyen-aws in #3979
* Automatic cargo update to 2025-05-12 by @github-actions in #4066
* Bump tests/perf/s2n-quic from `6aa9975` to `5f323b7` by @dependabot in #4068
* Fix stabilization instructions in RFC intro by @carolynzech in #4067
* Add support for quantifiers by @qinheping in #3993
* Toolchain upgrade to nightly-2025-05-07 by @thanhnguyen-aws in #4070
* Automatic toolchain upgrade to nightly-2025-05-08 by @github-actions in #4071
* Automatic toolchain upgrade to nightly-2025-05-09 by @github-actions in #4072
* Automatic toolchain upgrade to nightly-2025-05-10 by @github-actions in #4073
* Clippy/Stylistic Fixes by @carolynzech in #4074
* Upgrade toolchain to 2025-05-14 by @zhassan-aws in #4076
* Autoharness argument validation: only error on `--quiet` if `--list` was passed by @carolynzech in #4069
* Upgrade Rust toolchain to 2025-05-16 by @zhassan-aws in #4080
* Automatic toolchain upgrade to nightly-2025-05-17 by @github-actions in #4081
* Add setup scripts for Ubuntu 20.04 by @zhassan-aws in #4082
* Automatic toolchain upgrade to nightly-2025-05-18 by @github-actions in #4083
* Automatic cargo update to 2025-05-19 by @github-actions in #4086
* Automatic toolchain upgrade to nightly-2025-05-19 by @github-actions in #4085
* Automatic toolchain upgrade to nightly-2025-05-20 by @github-actions in #4091
* Bump tests/perf/s2n-quic from `5f323b7` to `22434aa` by @dependabot in #4089
* Fix the error that Kani panics when there is no external parameter in quantifier's closure. by @thanhnguyen-aws in #4088
* Update toolchain to 2025-05-22 by @carolynzech in #4098
* Use our toolchain when invoking `cargo metadata` by @carolynzech in #4090
* Automatic toolchain upgrade to nightly-2025-05-23 by @github-actions in #4099
* Automatic toolchain upgrade to nightly-2025-05-24 by @github-actions in #4101
* Automatic toolchain upgrade to nightly-2025-05-25 by @github-actions in #4102
* Fix a bug codegening `SwitchInt`s with only an otherwise branch by @bkirwi in #4095
* Automatic toolchain upgrade to nightly-2025-05-26 by @github-actions in #4104
* Automatic cargo update to 2025-05-26 by @github-actions in #4105
* Bump tests/perf/s2n-quic from `22434aa` to `550afb3` by @dependabot in #4106
* Automatic toolchain upgrade to nightly-2025-05-27 by @github-actions in #4107
* Update `kani::mem` pointer validity documentation by @carolynzech in #4092
* Add support for edition 2018 crates using assert! (Fixes #3717) by @sintemal in #4096
* Automatic toolchain upgrade to nightly-2025-05-28 by @github-actions in #4113
* Automatic toolchain upgrade to nightly-2025-05-29 by @github-actions in #4115
* Automatic toolchain upgrade to nightly-2025-05-30 by @github-actions in #4118
* Handle generic defaults in BoundedArbitrary derives by @zhassan-aws in #4117
* Automatic cargo update to 2025-06-02 by @github-actions in #4121
* Bump tests/perf/s2n-quic from `550afb3` to `8f54b57` by @dependabot in #4122
* Upgrade Rust toolchain to 2025-06-02 by @zhassan-aws in #4123
* Automatic toolchain upgrade to nightly-2025-06-03 by @github-actions in #4125
* Finish deprecating `--enable-unstable`, `--restrict-vtable`, and `--write-json-symtab` by @carolynzech in #4110
* `ty_mangled_name`: only use non-mangled name if `-Zcffi` is enabled. by @carolynzech in #4114
* Improve Help Menu by @carolynzech in #4109
* Start stabilizing `--jobs` and `list`; deprecate default memory checks by @carolynzech in #4108
* Refactor simd_bitmask to reduce the number of iterations by @zhassan-aws in #4129
* Set target features depending on the target architecture by @zhassan-aws in #4127
* Bump some versions suggested by cargo-outdated by @zhassan-aws in #4131
* Improve linking error output for `#[no_std]` crates by @AlexanderPortland in #4126
* Fix the git log command in the toolchain update script by @zhassan-aws in #4139
* Gate quantifiers behind an experimental feature by @thanhnguyen-aws in #4141
* Automatic cargo update to 2025-06-09 by @github-actions in #4145

## New Contributors
* @bkirwi made their first contribution in #4095
* @sintemal made their first contribution in #4096
* @AlexanderPortland made their first contribution in #4126

**Full Changelog**: kani-0.62.0...kani-0.63.0
```


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: Carolyn Zech <carolynzech@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
1 more reviewer

@carolynzech carolynzech carolynzech approved these changes

Reviewers whose approvals may not affect merge requirements
Assignees
No one assigned
Labels
Z-EndToEndBenchCI Tag a PR to run benchmark CI
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Kani incorrectly assumes that SwitchInts have at least one branch
2 participants
@bkirwi @carolynzech