Skip to content
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.

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

Update rust toolchain version for Kani 0.24 #2283

Closed
celinval opened this issue Mar 8, 2023 · 6 comments
Closed

Update rust toolchain version for Kani 0.24 #2283

celinval opened this issue Mar 8, 2023 · 6 comments
Assignees
Labels
Z-Sync Upstream Fetch changes from rustc repository. Old Rebase

Comments

@celinval
Copy link
Contributor

celinval commented Mar 8, 2023

Biweekly update for the rust toolchain version. For Kani 0.24, we will target the new year version: nightly-2023-03-09.

@celinval celinval added the Z-Sync Upstream Fetch changes from rustc repository. Old Rebase label Mar 8, 2023
@celinval
Copy link
Contributor Author

celinval commented Mar 8, 2023

Please make sure you re-enable the rust compiler log that is being disabled in #2149

@celinval
Copy link
Contributor Author

celinval commented Mar 8, 2023

The related code is here:

// TODO: Enable rustc log when we upgrade the toolchain.
// <https://github.com/model-checking/kani/issues/2283>
//
// rustc_driver::init_rustc_env_logger();

@qinheping
Copy link
Contributor

@tautschnig
I tried to update toolchain to nightly-2023-03-09. I resolved all build error in #2293. However, there are still some compilation bugs. Here is the simplest way to reproduce the bug.

  1. In the main brach, modify the toolchain to nightly-2023-02-05---the earliest toolchain with which I can reproduce the bug. And build Kani.
  2. Run kani tests/kani/Arbitrary [arbitrary_structs.rs](http://arbitrary_structs.rs/)
  3. Error message:
thread 'rustc' panicked at 'not implemented', kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:318:50
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::from_raw_parts_mut::<[std::mem::MaybeUninit<PercentArbitrary>]>
_RINvNtNtCs7cJSzKcgVKk_4core3ptr8metadata18from_raw_parts_mutSINtNtNtB6_3mem12maybe_uninit11MaybeUninitNtCsaStLaCc7KW0_17arbitrary_structs16PercentArbitraryEEB1E_
[Kani] current codegen location: Loc { file: "/Users/qinhh/.rustup/toolchains/nightly-2023-02-05-x86_64-apple-darwin/lib/rustlib/src/rust/library/core/src/ptr/metadata.rs", function: None, start_line: 128, start_col: Some(1), end_line: 131, end_col: Some(12) }
error: /Users/qinhh/Repos/kani/qinheping/target/kani/bin/kani-compiler exited with status exit status: 101

I asked Celina about this bug, and here is what she found

it looks like the compiler changed how they deal with deaggregation rust-lang/rust#107267
so we will need to implement the rvalue aggregation for structs / unions

@zhassan-aws
Copy link
Contributor

For the record, this commit has the changes to the cranelift backend to handle the changes in rust-lang/rust#107267:

bjorn3/rustc_codegen_cranelift@8494882

It may give us a hint of the changes needed on the Kani side.

@tautschnig
Copy link
Member

tautschnig commented Mar 28, 2023

If I understand https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.AggregateKind.html#variant.Adt correctly, we need to generate struct or union expressions here while asserting that VariantIdx always be zero. GOTO has these, so generating shouldn't be very hard once it is clear where to obtain the type information and all the operands.

Edit: this is about https://github.com/model-checking/kani/blob/main/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs#L318; for struct expressions it should be the same code as the Tuple case handled in the lines just before.

@celinval celinval linked a pull request Apr 14, 2023 that will close this issue
4 tasks
@celinval
Copy link
Contributor Author

Unfortunately we were not able to do the update on time. We have now switched it to a tentative nightly update.

@celinval celinval closed this as not planned Won't fix, can't repro, duplicate, stale Apr 14, 2023
@celinval celinval removed a link to a pull request Apr 14, 2023
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-Sync Upstream Fetch changes from rustc repository. Old Rebase
Projects
No open projects
Status: No status
Development

Successfully merging a pull request may close this issue.

4 participants