Skip to content

Commit

Permalink
Update Rust toolchain to 2023-11-06 (#2858)
Browse files Browse the repository at this point in the history
Update to the latest Rust toolchain (2023-11-06).

The relevant changes are:
- rust-lang/rust#117507: this required changing
the import of `Span` from `rustc_span::source_map::Span` to
`rustc_span::Span`.
- rust-lang/rust#114208: this changed the data
field for the `OffsetOf` variant of `NullOp` from `List<FieldIdx>` to
`List<(VariantIdx, FieldIdx)>`, which required updating the relevant
code in `rvalue.rs`.
- rust-lang/rust#115626: the unchecked shift
operators have been separated from the `unchecked_math` feature, so this
required changing the feature annotation in
`tests/ui/should-panic-attribute/unexpected-failures/test.rs`
- Some rustc change (not sure which one) result in a line in
`tests/coverage/unreachable/variant/main.rs` getting optimized out. To
maintain what this test is testing, I changed the `match` to make it a
bit less-prone to optimization.
- A change in `cargo` (rust-lang/cargo#12779)
resulted in an update to Kani's workspace `Cargo.toml` when `cargo add`
is executed inside `tests/script-based-pre/build-cache-bin`. This is
apparently intended behavior, so I had to make the `exclude` in the
`Cargo.toml` more specific to make sure this doesn't happen (I tried
using a glob, but that didn't work, apparently because of
rust-lang/cargo#6009.

Resolves #2848 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
zhassan-aws authored Nov 6, 2023
1 parent 6cb6526 commit a8a2346
Show file tree
Hide file tree
Showing 7 changed files with 10 additions and 7 deletions.
2 changes: 2 additions & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -67,4 +67,6 @@ exclude = [
"tests/slow",
"tests/assess-scan-test-scaffold",
"tests/script-based-pre",
"tests/script-based-pre/build-cache-bin/target/new_dep",
"tests/script-based-pre/build-cache-dirty/target/new_dep",
]
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -727,7 +727,7 @@ impl<'tcx> GotocCtx<'tcx> {
.with_size_of_annotation(self.codegen_ty(t)),
NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()),
NullOp::OffsetOf(fields) => Expr::int_constant(
layout.offset_of_subfield(self, fields.iter().map(|f| f.index())).bytes(),
layout.offset_of_subfield(self, fields.iter()).bytes(),
Type::size_t(),
),
}
Expand Down
3 changes: 2 additions & 1 deletion kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,8 @@ use rustc_middle::ty::layout::{
TyAndLayout,
};
use rustc_middle::ty::{self, Instance, Ty, TyCtxt};
use rustc_span::source_map::{respan, Span};
use rustc_span::source_map::respan;
use rustc_span::Span;
use rustc_target::abi::call::FnAbi;
use rustc_target::abi::{HasDataLayout, TargetDataLayout};

Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -2,5 +2,5 @@
# SPDX-License-Identifier: Apache-2.0 OR MIT

[toolchain]
channel = "nightly-2023-10-31"
channel = "nightly-2023-11-06"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
2 changes: 1 addition & 1 deletion tests/coverage/unreachable/variant/expected
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
coverage/unreachable/variant/main.rs, 15, FULL
coverage/unreachable/variant/main.rs, 15, PARTIAL
coverage/unreachable/variant/main.rs, 16, NONE
coverage/unreachable/variant/main.rs, 17, NONE
coverage/unreachable/variant/main.rs, 18, FULL
Expand Down
4 changes: 2 additions & 2 deletions tests/coverage/unreachable/variant/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,9 @@ fn print_direction(dir: Direction) {
Direction::Up => println!("Going up!"),
Direction::Down => println!("Going down!"),
Direction::Left => println!("Going left!"),
Direction::Right => println!("Going right!"),
Direction::Right if 1 == 1 => println!("Going right!"),
// This part is unreachable since we cover all variants in the match.
_ => {}
_ => println!("Not going anywhere!"),
}
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@

//! Checks that verfication fails when `#[kani::should_panic]` is used but not
//! all failures encountered are panics.
#![feature(unchecked_math)]
#![feature(unchecked_shifts)]

fn trigger_overflow() {
let x: u32 = kani::any();
Expand Down

0 comments on commit a8a2346

Please sign in to comment.