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

Upgrade the toolchain to nightly-2023-04-16 #2406

Merged
merged 13 commits into from
May 16, 2023

Conversation

celinval
Copy link
Contributor

@celinval celinval commented Apr 26, 2023

Description of changes:

Update the toolchain to use nightly-2023-04-16. Changes were related to the following changes to the toolchain:

Resolved issues:

Resolves #2383
Resolves #560

Related RFC:

Call-outs:

The checked shift right / left operations were optimized in this commit: rust-lang/rust#108282. The Rust compiler now adds an overflow check before actually performing the shift. With that, some of the CBMC shift overflow checks (which were already redundant) no longer fail. I updated the tests to either remove the expectation or to use the unchecked_[shl|shr]. However, these checks take u32 for the shift distance, hence the check for negative distance is probably useless now.

Testing:

  • How is this change tested? Existing tests + manually executed --visualize to check the trace

  • Is this a refactor change?

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

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

 - Fixed compilation errors but not runtime.
 - There are a few new variants that still need to be implemented.
  - Discriminant calculation
  - Implement Cast transmute
  - Misaligned assertion check error message
  - Codegen ZST constant
  - Is user variable detection
It looks like the `if cfg!()` is no longer being propagated and the
concrete playback code is increasing the logic that the compiler detects
as reachable.
Fix parenthesis
 Conflicts:
    cprover_bindings/src/goto_program/expr.rs
    kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
    kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
    library/kani/src/lib.rs
    tests/ui/cbmc_checks/signed-overflow/expected
    tests/ui/cbmc_checks/unsigned-overflow/expected
Remove CBMC failure expectations that are now caught by the rust
overflow check. This was due to the following Rust compiler change:
- rust-lang/rust#108282
@celinval celinval marked this pull request as ready for review May 1, 2023 20:14
@celinval celinval requested a review from a team as a code owner May 1, 2023 20:14
Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

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

LGTM

tests/expected/array/main.rs Outdated Show resolved Hide resolved
Conflicts:
    kani-compiler/src/kani_middle/attributes.rs
    kani-compiler/src/kani_middle/analysis.rs
@celinval
Copy link
Contributor Author

celinval commented May 4, 2023

Great... 😕

It looks like the rust compiler API to retrieve attributes no longer works for non-local items. @oli-obk, do you know if this was by design? I'm happy to try to submit a fix if needed (I should also try the latest rustc to see if it hasn't been fixed yet).

@celinval
Copy link
Contributor Author

celinval commented May 4, 2023

Great... confused

It looks like the rust compiler API to retrieve attributes no longer works for non-local items. @oli-obk, do you know if this was by design? I'm happy to try to submit a fix if needed (I should also try the latest rustc to see if it hasn't been fixed yet).

By the way, the error we are getting looks like:

thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `ClosureExpr`,
 right: `Ctor`', compiler/rustc_metadata/src/rmeta/decoder.rs:1127:17
stack backtrace:
   0: rust_begin_unwind
             at /rustc/5cdb7886a5ece816864fab177f0c266ad4dd5358/library/std/src/panicking.rs:578:5
   1: core::panicking::panic_fmt
             at /rustc/5cdb7886a5ece816864fab177f0c266ad4dd5358/library/core/src/panicking.rs:67:14
   2: core::panicking::assert_failed_inner
   3: core::panicking::assert_failed::<rustc_hir::definitions::DefPathData, rustc_hir::definitions::DefPathData>
   4: <rustc_metadata::creader::CrateMetadataRef>::get_item_attrs
   5: rustc_metadata::rmeta::decoder::cstore_impl::provide_extern::item_attrs
   6: rustc_query_system::query::plumbing::try_execute_query::<rustc_query_impl::queries::item_attrs, rustc_query_impl::plumbing::QueryCtxt>
   7: <rustc_query_impl::Queries as rustc_middle::ty::query::QueryEngine>::item_attrs
   8: <rustc_middle::ty::context::TyCtxt>::get_attrs_unchecked

@oli-obk
Copy link

oli-obk commented May 4, 2023

It looks like the rust compiler API to retrieve attributes no longer works for non-local items

It looks to me like this is specifically about closures, as we can definitely access attributes from non local items in general.

I don't know how that happened, none of the changes look like they could be at fault. rust-lang/rust#108944 is the most suspicious one, but it makes no sense for it to affect attributes.

I'll need to investigate with a computer, as it's too hard to do on mobile (I'm on sick leave). It may be until next week until I can get to it.

@celinval
Copy link
Contributor Author

celinval commented May 4, 2023

It looks like the rust compiler API to retrieve attributes no longer works for non-local items

It looks to me like this is specifically about closures, as we can definitely access attributes from non local items in general.

I don't know how that happened, none of the changes look like they could be at fault. rust-lang/rust#108944 is the most suspicious one, but it makes no sense for it to affect attributes.

Gotcha. Let me see if we can filter them out on our own since we don't care about them at this point. Thanks for taking a look though.

I'll need to investigate with a computer, as it's too hard to do on mobile (I'm on sick leave). It may be until next week until I can get to it.

Oh, that's too bad. I hope you get better soon. Take care!

@celinval celinval force-pushed the issue-2383-toolchain branch 2 times, most recently from a6f00a0 to 6d5ea83 Compare May 4, 2023 19:20
   - Support all instance types as part of the rechability analysis.
   - Skip assembly and closures for attribute checking due to rustc
     limitation.
   - Fix mir changes to the stats collector.
@celinval
Copy link
Contributor Author

celinval commented May 5, 2023

Just to give an update, the issue seems related to the unwinding of a recursive drop logic. I am trying to figure out the culprit. I am investigating if the issue could be related to an update to the standard library

@oli-obk
Copy link

oli-obk commented May 8, 2023

I only see the perf CI failing. How do I reproduce this failure you're seeing?

EDIT: Ah I see you fixed it by skipping closures, as you mentioned.

@celinval
Copy link
Contributor Author

celinval commented May 9, 2023

I've done some analysis with the patch from #2433, and I believe this issue might be related to how we encode drop_in_place, and how CBMC identifies candidate function pointers. This is very similar to the issue described in #1855.

To test this hypothesis, I commented out all the other harnesses from the s2n_quic code and ran:

cargo kani --tests --harness sync::spsc::tests::alloc_test

on my local machine, the verification takes about 42s.

@oli-obk
Copy link

oli-obk commented May 9, 2023

I found the issue. rust-lang/rust#109765 added should_encode_attrs and put Closure into the false arm.

While this makes sense for rustc, it's obviously an issue for analysis tools like kani. Unfortunately it's also performance relevant. I'll open a PR to see if there's a perf impact, if there is, we need to figure out how to let kani decide to encode that (or store these attributes in some other way).

matthiaskrgr added a commit to matthiaskrgr/rust that referenced this pull request May 10, 2023
Keep encoding attributes for closures

see model-checking/kani#2406 (comment) for some context.

We stopped encoding attributes for closures, but some tools need them
@oli-obk
Copy link

oli-obk commented May 11, 2023

The latest nightly should include rust-lang/rust#111381 now, if there are similar failures again in the future, you can use that PR to look up where to edit the match to keep more attributes in metadata

Conflicts:
    kani-compiler/src/kani_middle/attributes.rs

Required changes:
    kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@celinval
Copy link
Contributor Author

New update: My initial hypothesis was actually wrong. Sorry! The reachability per harness made a huge difference in my preliminary analysis because I had rewritten the alloc_test harness to invoke Kani's functions directly instead of via Bolero. In that case, the Bolero logic from other harnesses were affecting the analysis.

However, when rolling back my changes, the alloc_test usage of Bolero was enough to bring all the drop_in_places that are interfering with CBMC's analysis.

That said, @zhassan-aws helped me debug this issue further and understand why Bolero was having such a big impact in our analysis with this upgrade. We narrowed down to an issue with how if cfg!() statements are handled by this new compiler version.

We first noticed this issue during this upgrade and even created #2407 to fix it for our local crates.

I have now created camshaft/bolero#148 to update Bolero, which will hopefully unblock this PR.

Conflicts:
    kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
    kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

Required change:
    kani-compiler/src/kani_middle/attributes.rs
@celinval celinval enabled auto-merge (squash) May 16, 2023 01:53
@celinval celinval merged commit 6f7aa65 into model-checking:main May 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
4 participants