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;