Upgrade Rust toolchain to nightly-2024-02-25

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.

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;
 
 ///////////////////////////////////////////////////////////////////////////////////////////////

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;
 

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

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");
@@ -268,6 +268,13 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
+        // If the intrinsic is defined on generic types, its trimmed name will
+        // include type arguments (e.g., `arith_offset::<u8>`). In that case, we
+        // remove them to simplify the match below.
+        let intrinsic_split = intrinsic.split_once("::");
+        let intrinsic =
+            if let Some((base_name, _type_args)) = intrinsic_split { base_name } else { 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);

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<dyn Any>,
         _sess: &Session,
         _filenames: &OutputFilenames,
-    ) -> Result<(CodegenResults, FxIndexMap<WorkProductId, WorkProduct>), ErrorGuaranteed> {
+    ) -> (CodegenResults, FxIndexMap<WorkProductId, WorkProduct>) {
         match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap<WorkProductId, WorkProduct>)>()
         {
-            Ok(val) => Ok(*val),
+            Ok(val) => *val,
             Err(val) => panic!("unexpected error: {:?}", (*val).type_id()),
         }
     }

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;

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;

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;

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;

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]

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"]

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 <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Checking harness check_access_length_zero...
 
 Failed Checks: assumption failed\
-in std::hint::assert_unchecked
+in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_access_length_17
 Verification failed for - check_access_length_zero

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 <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_always_out_bounds

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);
 }

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};
 

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;