From a8a2346448722c6a441e8e7ed3697b7945ec1467 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Mon, 6 Nov 2023 12:49:04 -0800 Subject: [PATCH] Update Rust toolchain to 2023-11-06 (#2858) Update to the latest Rust toolchain (2023-11-06). The relevant changes are: - https://github.com/rust-lang/rust/pull/117507: this required changing the import of `Span` from `rustc_span::source_map::Span` to `rustc_span::Span`. - https://github.com/rust-lang/rust/pull/114208: this changed the data field for the `OffsetOf` variant of `NullOp` from `List` to `List<(VariantIdx, FieldIdx)>`, which required updating the relevant code in `rvalue.rs`. - https://github.com/rust-lang/rust/pull/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` (https://github.com/rust-lang/cargo/pull/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 https://github.com/rust-lang/cargo/issues/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. --- Cargo.toml | 2 ++ kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs | 3 ++- rust-toolchain.toml | 2 +- tests/coverage/unreachable/variant/expected | 2 +- tests/coverage/unreachable/variant/main.rs | 4 ++-- tests/ui/should-panic-attribute/unexpected-failures/test.rs | 2 +- 7 files changed, 10 insertions(+), 7 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 481c701f7af4..75d146eacb48 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -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", ] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index db792d6cb6af..c781f272fb2d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -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(), ), } diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 342e0e0b296b..01fb198d16fa 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -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}; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 0dc024954b3d..4adf74fe6563 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -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"] diff --git a/tests/coverage/unreachable/variant/expected b/tests/coverage/unreachable/variant/expected index 8fa3ec8b870f..08a2f824da83 100644 --- a/tests/coverage/unreachable/variant/expected +++ b/tests/coverage/unreachable/variant/expected @@ -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 diff --git a/tests/coverage/unreachable/variant/main.rs b/tests/coverage/unreachable/variant/main.rs index ca53b8ccfd18..76a589147bca 100644 --- a/tests/coverage/unreachable/variant/main.rs +++ b/tests/coverage/unreachable/variant/main.rs @@ -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!"), } } diff --git a/tests/ui/should-panic-attribute/unexpected-failures/test.rs b/tests/ui/should-panic-attribute/unexpected-failures/test.rs index 625a15c89683..c96eeb71efaf 100644 --- a/tests/ui/should-panic-attribute/unexpected-failures/test.rs +++ b/tests/ui/should-panic-attribute/unexpected-failures/test.rs @@ -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();