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 to 2022-12-11 #2045

Merged
merged 11 commits into from
Jan 20, 2023

Conversation

zhassan-aws
Copy link
Contributor

  • Update Rust toolchain to version 2022-12-04
  • Conform with changes to GenericArg
  • Conform with changes to NestedMetaItem
  • Make new ConstKind::Expr return on reach visitor
  • Conform with changes to Layout
  • Update rust toolchain version to 2022-12-11
  • Clippy fixes
  • More clippy/format fixes

Description of changes:

This PR builds on @adpaco-aws's commits in #1983, but bumps the version further to 2022-12-11 (instead of 2022-12-04), to include some of the later commits related to generators, which are necessary to fix how we codegen them.

The relevant PR is rust-lang/rust#105082 which was merged on 2022-12-10.

Another PR that required changes is rust-lang/rust#105234.

Resolved issues:

Towards #2044

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

I suggest reviewing by commit because the clippy fix commits touch many files.

Testing:

  • How is this change tested? Current regressions

  • Is this a refactor change? No

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 zhassan-aws requested a review from a team as a code owner December 28, 2022 03:00
@zhassan-aws
Copy link
Contributor Author

One of the harnesses in s2n-quic (packet::number::tests::round_trip) is failing, in particular this assertion:

https://github.com/aws/s2n-quic/blob/a15e731b84c70d93fbf7e459dd6bb246796091d2/quic/s2n-quic-core/src/packet/number/tests.rs#L87

I'm investigating.

@zhassan-aws
Copy link
Contributor Author

zhassan-aws commented Jan 18, 2023

@celinval I confirmed that regressions pass with this PR with CBMC's latest commit (diffblue/cbmc@f76d7fa): https://github.com/zhassan-aws/kani/actions/runs/3944422079

targets: &SwitchTargets,
loc: Location,
) -> Stmt {
let v = self.codegen_operand(discr);
let switch_ty = self.monomorphize(switch_ty);
let switch_ty = v.typ().clone();
Copy link
Contributor

Choose a reason for hiding this comment

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

Just confirming my reading of this: we remove the monomorphize because we are dealing with a "cbmc type" not a rust one anymore, and presumably the monomorphize happened as part of codegen_operand right?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Not really. The switch_ty field was removed from the SwitchInt struct in rust-lang/rust#105234 because it's redundant: its type is always the same as the type of the discr field. So my change just copies the type that we've already created for the discr field.

See this comment for more info: https://github.com/rust-lang/rust/pull/105234/files#diff-3a6077a453e9ef35b5b85b4419025066cc7a0f3bad1207ae98860902c817a252L531

Copy link
Contributor Author

Choose a reason for hiding this comment

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

But yes, AFAIK, the monomorphization happens in codegen_operand.

@@ -865,10 +878,10 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_alignment_padding(
&self,
size: Size,
layout: &Layout,
layout: &LayoutS<VariantIdx>,
Copy link
Contributor

Choose a reason for hiding this comment

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

Are you sure we should be switching to LayoutS? It seems like the sort of thing there's probably a better type we should be using here.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I brought in those changes from #1983. @adpaco-aws: do you know if there's a better type to use?

Copy link
Contributor

Choose a reason for hiding this comment

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

Given the little changes to the code that uses this type, this seems like a good fit. Further improvement should probably be orthogonal to updating the toolchain. I think this has to do with this PR: rust-lang/rust#103693

@@ -392,7 +390,7 @@ impl<'tcx> GotocCtx<'tcx> {
let cases = targets
.iter()
.map(|(c, bb)| {
Expr::int_constant(c, self.codegen_ty(switch_ty))
Expr::int_constant(c, switch_ty.clone())
Copy link
Contributor

Choose a reason for hiding this comment

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

nit: I don't think you need the clone here.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I also thought it shouldn't be needed, but the compiler corrected me :)

error[E0507]: cannot move out of `switch_ty`, a captured variable in an `FnMut` closure
   --> kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:393:43
    |
372 |         let switch_ty = v.typ().clone();
    |             --------- captured outer variable
...
392 |                 .map(|(c, bb)| {
    |                      --------- captured by this `FnMut` closure
393 |                     Expr::int_constant(c, switch_ty)
    |                                           ^^^^^^^^^ move occurs because `switch_ty` has type `cprover_bindings::goto_program::Type`, which does not implement the `Copy` trait

It's because it's used in a closure which might be called multiple times.

@@ -865,10 +878,10 @@ impl<'tcx> GotocCtx<'tcx> {
fn codegen_alignment_padding(
&self,
size: Size,
layout: &Layout,
layout: &LayoutS<VariantIdx>,
Copy link
Contributor

Choose a reason for hiding this comment

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

Given the little changes to the code that uses this type, this seems like a good fit. Further improvement should probably be orthogonal to updating the toolchain. I think this has to do with this PR: rust-lang/rust#103693

@zhassan-aws zhassan-aws merged commit 47014e6 into model-checking:main Jan 20, 2023
@zhassan-aws zhassan-aws deleted the toolchain-2022-12-11 branch January 20, 2023 20:09
celinval added a commit to celinval/kani-dev that referenced this pull request Jan 23, 2023
Compiletest behavior has changed to always failing fast after model-checking#2045.
This PR introduces a `--no-fail-fast` flag to compiletest which will
execute the entire suite regardless of failure.

The regression script uses `--no-fail-fast` so all failures in a suite
are printed as part of the CI.
@celinval celinval mentioned this pull request Jan 23, 2023
4 tasks
celinval added a commit that referenced this pull request Jan 23, 2023
Compiletest behavior has changed to always failing fast after #2045. This PR introduces a --no-fail-fast flag to compiletest which will execute the entire suite regardless of failure.

The regression script uses --no-fail-fast so all failures in a suite are printed as part of the CI.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants