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:
 * rust-lang/rust#121209
 * rust-lang/rust#121309
 * rust-lang/rust#120863
 * rust-lang/rust#117772
 * rust-lang/rust#117658

With rust-lang/rust#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::<impl i8>::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

Author: adpaco-aws

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");
@@ -288,6 +288,23 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
+        /// Gets the basename of an intrinsic given its trimmed name.
+        ///
+        /// For example, given `arith_offset::<u8>` 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);

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/Atomic/Stable/AtomicPtr/main.rs

@@ -18,7 +18,7 @@ fn check_fetch_byte_add() {
 
 #[kani::proof]
 fn check_fetch_byte_sub() {
-    let atom = AtomicPtr::<i64>::new(core::ptr::invalid_mut(1));
+    let atom = AtomicPtr::<i64>::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);
 }

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;