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 the rust toolchain to nightly-2023-12-03 #2913

Merged
merged 17 commits into from
Dec 8, 2023

Conversation

tautschnig
Copy link
Member

Changes required due to:

Resolves #2911

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

Changes required due to:
- rust-lang/rust@99ac405b96 Move MetadataLoader{,Dyn} to rustc_metadata.
- rust-lang/rust@c997c6d822 Add more information to stable Instance
@tautschnig tautschnig requested a review from a team as a code owner December 3, 2023 22:13
@github-actions github-actions bot added the Z-BenchCI Tag a PR to run benchmark CI label Dec 3, 2023
@celinval celinval enabled auto-merge (squash) December 6, 2023 19:31
@celinval
Copy link
Contributor

celinval commented Dec 6, 2023

@tautschnig I pushed a few patches, but we're still not there yet.

  1. I pushed a workaround the regression on is_foreign_item. If the fix on the rust side lands before this PR, we could remove the workaround.
  2. I revisited the simd fix, and we don't need to change the model at all. The way portable_simd invokes the intrinsic hasn't changed. Only the return value has, which only required a change to the unit test.

The simd harness is still failing though, but it's not related to simd_bitmask model. I removed the model, and the index out of bounds failure still happen. I talked to @adpaco-aws and he kindly agreed to take a look at it. My current hypothesis is that this is an issue with simd_shuffle. I added a harness that only invoke resize of a simd vector, and the same issue happens.

The change was only needed in the test case, since the way
portable simd invokes the intrinsic is still the same

My current hypothesis is that the current failure could be an
issue with simd_shuffle
@adpaco-aws
Copy link
Contributor

adpaco-aws commented Dec 7, 2023

I've pushed the fix for the simd_shuffle issue in addition to some tests, but I think that the PR is blocked because of the other issue with is_foreign_item:

failures:

---- [expected] expected/issue-2589/issue_2589.rs stdout ----

error: test failed: expected output to contain the line(s):
error: Type `std::string::String` does not implement trait `Dummy`. This is likely because `original` is used as a stub but its generic bounds are not being met.
status: exit status: 1
command: "kani" "/home/ubuntu/kani/tests/expected/issue-2589/issue_2589.rs" "-Z" "stubbing"
stdout:
------------------------------------------
Kani Rust Verifier 0.42.0 (standalone)
error: /home/ubuntu/kani/target/kani/bin/kani-compiler exited with status exit status: 101

------------------------------------------
stderr:
------------------------------------------
warning: function `stub` is never used
  --> /home/ubuntu/kani/tests/expected/issue-2589/issue_2589.rs:12:4
   |
12 | fn stub<T: Dummy>() {
   |    ^^^^
   |
   = note: `#[warn(dead_code)]` on by default

warning: 1 warning emitted

warning: function `stub` is never used
  --> /home/ubuntu/kani/tests/expected/issue-2589/issue_2589.rs:12:4
   |
12 | fn stub<T: Dummy>() {
   |    ^^^^
   |
   = note: `#[warn(dead_code)]` on by default

thread 'rustc' panicked at compiler/rustc_smir/src/rustc_smir/builder.rs:63:17:
internal error: entered unreachable code: Failed to evaluate instance constant: Unevaluated(UnevaluatedConst { def: DefId(0:6 ~ issue_2589[bc6b]::Dummy::TRUE), args: [std::string::String], promoted: None }, bool)
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] no current codegen item.
[Kani] no current codegen location.
warning: 1 warning emitted


------------------------------------------



failures:
    [expected] expected/issue-2589/issue_2589.rs

test result: FAILED. 206 passed; 1 failed; 2 ignored; 0 measured; 0 filtered out; finished in 44.78s

Some tests failed in compiletest suite=expected mode=expected host=(none) target=(none)

I'm guessing the workaround doesn't take this case into account? I've also tried to push the toolchain pointer to nightly-2023-12-07 but that doesn't solve this issue: I'm getting the same error in addition to two more.

@adpaco-aws
Copy link
Contributor

adpaco-aws commented Dec 7, 2023

Actually, it looks like the perf suite is failing as well... For a different reason:

VERIFICATION:- FAILED
Verification Time: 28.527027s

Summary:
Verification failed for - fmt_u8
Verification failed for - fmt_i8
Complete - 0 successfully verified harnesses, 2 failures, 2 total.

------------------------------------------
stderr:
------------------------------------------
   Compiling format v0.1.0 (/home/runner/work/kani/kani/tests/perf/format)
    Finished test [unoptimized + debuginfo] target(s) in 0.69s

------------------------------------------



failures:
    [cargo-kani-test] perf/format/expected

test result: FAILED. 13 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; finished in 1442.94s

@celinval
Copy link
Contributor

celinval commented Dec 8, 2023

Yeah, unfortunately the fix for the foreign item didn't make it to Dec 7th nightly.

@celinval
Copy link
Contributor

celinval commented Dec 8, 2023

I have a new workaround... I'll push it to the branch in a bit. I am looking at the new failures you mentioned with Dec 7th

- Use internal to go around is_foreign_item() issue
- Update tests after an issue:
  rust-lang/rust#116915
- Update the toolchain
@celinval celinval enabled auto-merge (squash) December 8, 2023 03:55
@celinval celinval enabled auto-merge (squash) December 8, 2023 03:55
@celinval celinval enabled auto-merge (squash) December 8, 2023 03:57
@celinval celinval merged commit 63af43d into model-checking:main Dec 8, 2023
19 of 20 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Z-BenchCI Tag a PR to run benchmark CI
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Toolchain upgrade to nightly-2023-12-02 failed
3 participants