From 46bdb75d6ea887ddd21b2e90c6bf32c110978751 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Thu, 29 Feb 2024 17:07:43 -0500 Subject: [PATCH] Upgrade Rust toolchain to `nightly-2024-02-25` (#3048) Upgrades the Rust toolchain to `nightly-2024-02-25`. The Rust compiler PRs that triggered changes in this upgrades are: * https://github.com/rust-lang/rust/pull/121209 * https://github.com/rust-lang/rust/pull/121309 * https://github.com/rust-lang/rust/pull/120863 * https://github.com/rust-lang/rust/pull/117772 * https://github.com/rust-lang/rust/pull/117658 With https://github.com/rust-lang/rust/pull/121309 some intrinsics became inlineable so their names became qualified. This made our `match` on the intrinsic name to fail in those cases, leaving them as unsupported constructs as in this example: ``` warning: Found the following unsupported constructs: - _RNvNtCscyGW2MM2t5j_4core10intrinsics8unlikelyCs1eohKeNmpdS_5arith (3) - caller_location (1) - foreign function (1) Verification will fail if one or more of these constructs is reachable. See https://model-checking.github.io/kani/rust-feature-support.html for more details. [...] Failed Checks: _RNvNtCscyGW2MM2t5j_4core10intrinsics8unlikelyCs1eohKeNmpdS_5arith is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose File: "/home/ubuntu/.rustup/toolchains/nightly-2024-02-18-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/num/mod.rs", line 25, in core::num::::checked_add ``` We use `trimmed_name()` to work around this, but that may include type arguments if the intrinsic is defined on generics. So in those cases, we just take the first part of the name so we can keep the rest as before. Resolves #3044 --- cprover_bindings/src/goto_program/location.rs | 1 - cprover_bindings/src/goto_program/typ.rs | 1 - .../codegen_cprover_gotoc/codegen/assert.rs | 1 - .../codegen_cprover_gotoc/codegen/function.rs | 1 - .../codegen/intrinsic.rs | 19 ++++++++++++++++++- .../compiler_interface.rs | 5 ++--- kani-compiler/src/kani_compiler.rs | 4 +--- kani-compiler/src/kani_middle/metadata.rs | 1 - kani-compiler/src/kani_middle/provide.rs | 1 - kani-compiler/src/kani_middle/reachability.rs | 2 +- kani-driver/src/args/playback_args.rs | 2 -- rust-toolchain.toml | 2 +- tests/expected/any_vec/exact_length.expected | 4 ++-- tests/expected/any_vec/out_bounds.expected | 2 +- .../Atomic/Stable/AtomicPtr/main.rs | 2 +- tests/kani/Intrinsics/Likely/main.rs | 8 +++++++- tools/bookrunner/librustdoc/html/markdown.rs | 1 - tools/compiletest/src/runtest.rs | 1 - 18 files changed, 34 insertions(+), 24 deletions(-) diff --git a/cprover_bindings/src/goto_program/location.rs b/cprover_bindings/src/goto_program/location.rs index 79b123ad8b0e..4097d075276d 100644 --- a/cprover_bindings/src/goto_program/location.rs +++ b/cprover_bindings/src/goto_program/location.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::cbmc_string::{InternStringOption, InternedString}; -use std::convert::TryInto; use std::fmt::Debug; /// A `Location` represents a source location. diff --git a/cprover_bindings/src/goto_program/typ.rs b/cprover_bindings/src/goto_program/typ.rs index dd07c150bb3f..da943b26ab19 100644 --- a/cprover_bindings/src/goto_program/typ.rs +++ b/cprover_bindings/src/goto_program/typ.rs @@ -7,7 +7,6 @@ use super::super::MachineModel; use super::{Expr, SymbolTable}; use crate::cbmc_string::InternedString; use std::collections::BTreeMap; -use std::convert::TryInto; use std::fmt::Debug; /////////////////////////////////////////////////////////////////////////////////////////////// diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 68573cd2a1cd..cad3595bca50 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -22,7 +22,6 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, Location, Stmt, Type}; use cbmc::InternedString; use stable_mir::ty::Span as SpanStable; -use std::convert::AsRef; use strum_macros::{AsRefStr, EnumString}; use tracing::debug; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index d4061d4271db..78c7e2b6cbd6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -12,7 +12,6 @@ use stable_mir::mir::{Body, Local}; use stable_mir::ty::{RigidTy, TyKind}; use stable_mir::CrateDef; use std::collections::BTreeMap; -use std::iter::FromIterator; use tracing::{debug, debug_span}; /// Codegen MIR functions into gotoc diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index badf07d4e132..7996d434c351 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -112,7 +112,7 @@ impl<'tcx> GotocCtx<'tcx> { place: &Place, span: Span, ) -> Stmt { - let intrinsic_sym = instance.mangled_name(); + let intrinsic_sym = instance.trimmed_name(); let intrinsic = intrinsic_sym.as_str(); let loc = self.codegen_span_stable(span); debug!(?instance, "codegen_intrinsic"); @@ -288,6 +288,23 @@ impl<'tcx> GotocCtx<'tcx> { }}; } + /// Gets the basename of an intrinsic given its trimmed name. + /// + /// For example, given `arith_offset::` this returns `arith_offset`. + fn intrinsic_basename(name: &str) -> &str { + let scope_sep_count = name.matches("::").count(); + // We expect at most one `::` separator from trimmed intrinsic names + debug_assert!( + scope_sep_count < 2, + "expected at most one `::` in intrinsic name, but found {scope_sep_count} in `{name}`" + ); + let name_split = name.split_once("::"); + if let Some((base_name, _type_args)) = name_split { base_name } else { name } + } + // The trimmed name includes type arguments if the intrinsic was defined + // on generic types, but we only need the basename for the match below. + let intrinsic = intrinsic_basename(intrinsic); + if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") { assert!(fargs.len() == 3, "`simd_shuffle` had unexpected arguments {fargs:?}"); let n: u64 = self.simd_shuffle_length(stripped, farg_types, span); diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 810c5707aad4..91e6c2538195 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -53,7 +53,6 @@ use std::ffi::OsString; use std::fmt::Write; use std::fs::File; use std::io::BufWriter; -use std::iter::FromIterator; use std::path::{Path, PathBuf}; use std::process::Command; use std::sync::{Arc, Mutex}; @@ -353,10 +352,10 @@ impl CodegenBackend for GotocCodegenBackend { ongoing_codegen: Box, _sess: &Session, _filenames: &OutputFilenames, - ) -> Result<(CodegenResults, FxIndexMap), ErrorGuaranteed> { + ) -> (CodegenResults, FxIndexMap) { match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() { - Ok(val) => Ok(*val), + Ok(val) => *val, Err(val) => panic!("unexpected error: {:?}", (*val).type_id()), } } diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 118821f5995f..48b4318db5bf 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -465,10 +465,8 @@ fn metadata_output_path(tcx: TyCtxt) -> PathBuf { #[cfg(test)] mod tests { use super::*; - use kani_metadata::{HarnessAttributes, HarnessMetadata}; + use kani_metadata::HarnessAttributes; use rustc_data_structures::fingerprint::Fingerprint; - use rustc_hir::definitions::DefPathHash; - use std::collections::HashMap; fn mock_next_harness_id() -> HarnessId { static mut COUNTER: u64 = 0; diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs index 02f5da107556..9236de48308f 100644 --- a/kani-compiler/src/kani_middle/metadata.rs +++ b/kani-compiler/src/kani_middle/metadata.rs @@ -3,7 +3,6 @@ //! This module handles Kani metadata generation. For example, generating HarnessMetadata for a //! given function. -use std::default::Default; use std::path::Path; use crate::kani_middle::attributes::test_harness_name; diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index 70e046d6f9d6..d5495acb67a7 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -10,7 +10,6 @@ use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_ite use crate::kani_middle::stubbing; use crate::kani_queries::QueryDb; use rustc_hir::def_id::{DefId, LocalDefId}; -use rustc_interface; use rustc_middle::util::Providers; use rustc_middle::{mir::Body, query::queries, ty::TyCtxt}; use stable_mir::mir::mono::MonoItem; diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 63ed41bfd4c1..11ba57cb1cff 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -31,7 +31,7 @@ use stable_mir::mir::{ TerminatorKind, }; use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind}; -use stable_mir::{self, CrateItem}; +use stable_mir::CrateItem; use stable_mir::{CrateDef, ItemKind}; use crate::kani_middle::coercion; diff --git a/kani-driver/src/args/playback_args.rs b/kani-driver/src/args/playback_args.rs index bdad446a1158..ad82d9632a7a 100644 --- a/kani-driver/src/args/playback_args.rs +++ b/kani-driver/src/args/playback_args.rs @@ -100,8 +100,6 @@ impl ValidateArgs for PlaybackArgs { #[cfg(test)] mod tests { - use clap::Parser; - use super::*; #[test] diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 42f6af899b43..408b2e859604 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-02-17" +channel = "nightly-2024-02-25" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/any_vec/exact_length.expected b/tests/expected/any_vec/exact_length.expected index 93feecb214e5..f64d2830a7b8 100644 --- a/tests/expected/any_vec/exact_length.expected +++ b/tests/expected/any_vec/exact_length.expected @@ -1,12 +1,12 @@ Checking harness check_access_length_17... Failed Checks: assumption failed\ -in std::hint::assert_unchecked +in >::get_unchecked Checking harness check_access_length_zero... Failed Checks: assumption failed\ -in std::hint::assert_unchecked +in >::get_unchecked Verification failed for - check_access_length_17 Verification failed for - check_access_length_zero diff --git a/tests/expected/any_vec/out_bounds.expected b/tests/expected/any_vec/out_bounds.expected index 71132a64f67d..24121aee4ee8 100644 --- a/tests/expected/any_vec/out_bounds.expected +++ b/tests/expected/any_vec/out_bounds.expected @@ -1,6 +1,6 @@ Checking harness check_always_out_bounds... Failed Checks: assumption failed -in std::hint::assert_unchecked +in >::get_unchecked Verification failed for - check_always_out_bounds diff --git a/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs b/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs index c703c7c7125f..4e9d68619fd7 100644 --- a/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs +++ b/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs @@ -18,7 +18,7 @@ fn check_fetch_byte_add() { #[kani::proof] fn check_fetch_byte_sub() { - let atom = AtomicPtr::::new(core::ptr::invalid_mut(1)); + let atom = AtomicPtr::::new(core::ptr::without_provenance_mut(1)); assert_eq!(atom.fetch_byte_sub(1, Ordering::Relaxed).addr(), 1); assert_eq!(atom.load(Ordering::Relaxed).addr(), 0); } diff --git a/tests/kani/Intrinsics/Likely/main.rs b/tests/kani/Intrinsics/Likely/main.rs index 524fbd18ddc8..14643241ef90 100644 --- a/tests/kani/Intrinsics/Likely/main.rs +++ b/tests/kani/Intrinsics/Likely/main.rs @@ -28,9 +28,15 @@ fn check_unlikely(x: i32, y: i32) { } #[kani::proof] -fn main() { +fn check_likely_main() { let x = kani::any(); let y = kani::any(); check_likely(x, y); +} + +#[kani::proof] +fn check_unlikely_main() { + let x = kani::any(); + let y = kani::any(); check_unlikely(x, y); } diff --git a/tools/bookrunner/librustdoc/html/markdown.rs b/tools/bookrunner/librustdoc/html/markdown.rs index 1bcd5dad7532..3f827b77ff2b 100644 --- a/tools/bookrunner/librustdoc/html/markdown.rs +++ b/tools/bookrunner/librustdoc/html/markdown.rs @@ -7,7 +7,6 @@ use rustc_span::edition::Edition; -use std::default::Default; use std::str; use std::{borrow::Cow, marker::PhantomData}; diff --git a/tools/compiletest/src/runtest.rs b/tools/compiletest/src/runtest.rs index ee89c252dc4f..7925ed83e6e5 100644 --- a/tools/compiletest/src/runtest.rs +++ b/tools/compiletest/src/runtest.rs @@ -23,7 +23,6 @@ use std::process::{Command, ExitStatus, Output, Stdio}; use std::str; use serde::{Deserialize, Serialize}; -use serde_yaml; use tracing::*; use wait_timeout::ChildExt;