Upgrade the toolchain to nightly-2023-04-16

[celinval]

Description of changes:

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

• Wrap the whole LocalInfo in ClearCrossCrate. rust-lang/rust#108944
• Implementing "<test_binary> --list --format json" for use by IDE test explorers / runners rust-lang/rust#108148
• Remove box_syntax rust-lang/rust#108471
• rustc: Remove unused Session argument from some attribute functions rust-lang/rust#109358
• Use FieldIdx in various things related to aggregates rust-lang/rust#109849
• Use &IndexSlice instead of &IndexVec where possible rust-lang/rust#109819
• Rename IndexVec::last → last_index rust-lang/rust#109718
• Make local query providers receive local keys rust-lang/rust#109092
• Remove DropAndReplace terminator rust-lang/rust#108856
• Rename assert_uninit_valid intrinsic rust-lang/rust#105613
• errors: generate typed identifiers in each crate rust-lang/rust#103042
• Move mir::Field → abi::FieldIdx rust-lang/rust#109716
• Remove type-traversal trait aliases rust-lang/rust#108340
• Refactor unwind in MIR rust-lang/rust#102906
• Insert alignment checks for pointer dereferences when debug assertions are enabled rust-lang/rust#98112
• Add a builtin FnPtr trait that is implemented for all function pointers rust-lang/rust#108080

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.

[zhassan-aws]

LGTM

[celinval]

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]

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]

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]

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]

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]

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]

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]

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).

[oli-obk]

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

[celinval]

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.