Update Rust toolchain from nightly-2024-05-17 to nightly-2024-05-23

cprover_bindings/src/goto_program/expr.rs

@@ -1055,6 +1055,7 @@ impl Expr {
     ///     <https://github.com/rust-lang/rfcs/blob/master/text/1199-simd-infrastructure.md#comparisons>).
     ///     The signedness doesn't matter, as the result for each element is
     ///     either "all ones" (true) or "all zeros" (false).
+    ///
     /// For example, one can use `simd_eq` on two `f64x4` vectors and assign the
     /// result to a `u64x4` vector. But it's not possible to assign it to: (1) a
     /// `u64x2` because they don't have the same length; or (2) another `f64x4`
@@ -1665,7 +1666,7 @@ impl Expr {
                         continue;
                     }
                     let name = field.name();
-                    exprs.insert(name, self.clone().member(&name.to_string(), symbol_table));
+                    exprs.insert(name, self.clone().member(name.to_string(), symbol_table));
                 }
             }
         }

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -78,11 +78,9 @@ pub fn read_goto_binary_file(filename: &Path) -> io::Result<()> {
 /// [NumberedIrep] from its unique number.
 ///
 /// In practice:
-/// - the forward directon from [IrepKey] to unique numbers is
-/// implemented using a `HashMap<IrepKey,usize>`
-/// - the inverse direction from unique numbers to [NumberedIrep] is implemented
-/// using a `Vec<NumberedIrep>` called the `index` that stores [NumberedIrep]
-/// under their unique number.
+/// - the forward directon from [IrepKey] to unique numbers is implemented using a `HashMap<IrepKey,usize>`
+/// - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec<NumberedIrep>`
+///   called the `index` that stores [NumberedIrep] under their unique number.
 ///
 /// Earlier we said that an [NumberedIrep] is conceptually a pair formed of
 /// an [IrepKey] and its unique number. It is represented using only

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

@@ -204,7 +204,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let body = self.transformer.body(self.tcx, instance);
         self.set_current_fn(instance, &body);
         debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function");
-        self.ensure(&self.symbol_name_stable(instance), |ctx, fname| {
+        self.ensure(self.symbol_name_stable(instance), |ctx, fname| {
             Symbol::function(
                 fname,
                 ctx.fn_typ(instance, &body),

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -871,6 +871,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// its primary argument and returns a tuple that contains:
     ///  * the previous value
     ///  * a boolean value indicating whether the operation was successful or not
+    ///
     /// In a sequential context, the update is always sucessful so we assume the
     /// second value to be true.
     /// -------------------------
@@ -955,9 +956,10 @@ impl<'tcx> GotocCtx<'tcx> {
     ///  * Both `src`/`dst` must be valid for reads/writes of `count *
     ///      size_of::<T>()` bytes (done by calls to `memmove`)
     ///  * (Exclusive to nonoverlapping copy) The region of memory beginning
-    ///      at `src` with a size of `count * size_of::<T>()` bytes must *not*
-    ///      overlap with the region of memory beginning at `dst` with the same
-    ///      size.
+    ///    at `src` with a size of `count * size_of::<T>()` bytes must *not*
+    ///    overlap with the region of memory beginning at `dst` with the same
+    ///    size.
+    ///
     /// In addition, we check that computing `count` in bytes (i.e., the third
     /// argument of the copy built-in call) would not overflow.
     pub fn codegen_copy(
@@ -1834,7 +1836,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// TODO: Add a check for the condition:
     ///  * `src` must point to a properly initialized value of type `T`
-    /// See <https://github.com/model-checking/kani/issues/920> for more details
+    ///    See <https://github.com/model-checking/kani/issues/920> for more details
     fn codegen_volatile_load(
         &mut self,
         mut fargs: Vec<Expr>,
@@ -1894,6 +1896,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Undefined behavior if any of these conditions are violated:
     ///  * `dst` must be valid for writes (done by memset writable check)
     ///  * `dst` must be properly aligned (done by `align_check` below)
+    ///
     /// In addition, we check that computing `bytes` (i.e., the third argument
     /// for the `memset` call) would not overflow
     fn codegen_write_bytes(

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -393,7 +393,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Generate a goto expression for a pointer to a static or thread-local variable.
     fn codegen_instance_pointer(&mut self, instance: Instance, is_thread_local: bool) -> Expr {
-        let sym = self.ensure(&instance.mangled_name(), |ctx, name| {
+        let sym = self.ensure(instance.mangled_name(), |ctx, name| {
             // Rust has a notion of "extern static" variables. These are in an "extern" block,
             // and so aren't initialized in the current codegen unit. For example (from std):
             //      extern "C" {

kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -333,8 +333,9 @@ impl<'tcx> GotocCtx<'tcx> {
     ///      assert!(v.0 == [1, 2]); // refers to the entire array
     ///    }
     /// ```
-    /// * Note that projection inside SIMD structs may eventually become illegal.
-    /// See <https://github.com/rust-lang/stdarch/pull/1422#discussion_r1176415609> thread.
+    ///
+    /// Note that projection inside SIMD structs may eventually become illegal.
+    /// See thread <https://github.com/rust-lang/stdarch/pull/1422#discussion_r1176415609>.
     ///
     /// Since the goto representation for both is the same, we use the expected type to decide
     /// what to return.

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -73,7 +73,7 @@ impl TypeExt for Type {
                     && components.iter().any(|x| x.name() == "vtable" && x.typ().is_pointer())
             }
             Type::StructTag(tag) => {
-                st.lookup(&tag.to_string()).unwrap().typ.is_rust_trait_fat_ptr(st)
+                st.lookup(tag.to_string()).unwrap().typ.is_rust_trait_fat_ptr(st)
             }
             _ => false,
         }
@@ -1140,7 +1140,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Mapping enums to CBMC types is rather complicated. There are a few cases to consider:
     /// 1. When there is only 0 or 1 variant, this is straightforward as the code shows
     /// 2. When there are more variants, rust might decides to apply the typical encoding which
-    /// regard enums as tagged union, or an optimized form, called niche encoding.
+    ///    regard enums as tagged union, or an optimized form, called niche encoding.
     ///
     /// The direct encoding is straightforward. Enums are just mapped to C as a struct of union of structs.
     /// e.g.

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -11,6 +11,7 @@
 //! This file is for defining the data-structure itself.
 //!   1. Defines `GotocCtx<'tcx>`
 //!   2. Provides constructors, getters and setters for the context.
+//!
 //! Any MIR specific functionality (e.g. codegen etc) should live in specialized files that use
 //! this structure as input.
 use super::current_fn::CurrentFnCtx;

kani-compiler/src/kani_compiler.rs

@@ -110,9 +110,10 @@ struct CrateInfo {
 ///      compilation. The crate metadata is stored here (even if no codegen was actually performed).
 ///    - [CompilationStage::CompilationSkipped] no compilation was actually performed.
 ///      No work needs to be done.
-/// - Note: In a scenario where the compilation fails, the compiler will exit immediately,
-///  independent on the stage. Any artifact produced shouldn't be used.
-/// I.e.:
+///
+/// Note: In a scenario where the compilation fails, the compiler will exit immediately,
+/// independent on the stage. Any artifact produced shouldn't be used. I.e.:
+///
 /// ```dot
 /// graph CompilationStage {
 ///   Init -> {CodegenNoStubs, CompilationSkipped}

kani-compiler/src/kani_middle/reachability.rs

@@ -303,7 +303,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
 /// 1. Every function / method / closures that may be directly invoked.
 /// 2. Every function / method / closures that may have their address taken.
 /// 3. Every method that compose the impl of a trait for a given type when there's a conversion
-/// from the type to the trait.
+///    from the type to the trait.
 ///    - I.e.: If we visit the following code:
 ///      ```
 ///      let var = MyType::new();
@@ -313,7 +313,8 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
 /// 4. Every Static variable that is referenced in the function or constant used in the function.
 /// 5. Drop glue.
 /// 6. Static Initialization
-/// This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`.
+///
+/// Remark: This code has been mostly taken from `rustc_monomorphize::collector::MirNeighborCollector`.
 impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
     /// Collect the following:
     /// - Trait implementations when casting from concrete to dyn Trait.

kani-driver/src/args_toml.rs

@@ -90,8 +90,11 @@ fn cargo_locate_project(input_args: &[OsString]) -> Result<PathBuf> {
 /// We currently support the following entries:
 /// - flags: Flags that get directly passed to Kani.
 /// - unstable: Unstable features (it will be passed using `-Z` flag).
+///
 /// The tables supported are:
-/// "workspace.metadata.kani", "package.metadata.kani", "kani"
+/// - "workspace.metadata.kani"
+/// - "package.metadata.kani"
+/// - "kani"
 fn toml_to_args(tomldata: &str) -> Result<(Vec<OsString>, Vec<OsString>)> {
     let config = tomldata.parse::<Value>()?;
     // To make testing easier, our function contract is to produce a stable ordering of flags for a given input.

kani-driver/src/call_cargo.rs

@@ -112,7 +112,7 @@ impl KaniSession {
                 let mut cmd = setup_cargo_command()?;
                 cmd.args(&cargo_args)
                     .args(vec!["-p", &package.name])
-                    .args(&verification_target.to_args())
+                    .args(verification_target.to_args())
                     .args(&pkg_args)
                     .env("RUSTC", &self.kani_compiler)
                     // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
@@ -315,13 +315,16 @@ fn validate_package_names(package_names: &[String], packages: &[Package]) -> Res
 }
 
 /// Extract the packages that should be verified.
-/// If `--package <pkg>` is given, return the list of packages selected.
-/// If `--exclude <pkg>` is given, return the list of packages not excluded.
-/// If `--workspace` is given, return the list of workspace members.
-/// If no argument provided, return the root package if there's one or all members.
+///
+/// The result is build following these rules:
+/// - If `--package <pkg>` is given, return the list of packages selected.
+/// - If `--exclude <pkg>` is given, return the list of packages not excluded.
+/// - If `--workspace` is given, return the list of workspace members.
+/// - If no argument provided, return the root package if there's one or all members.
 ///   - I.e.: Do whatever cargo does when there's no `default_members`.
 ///   - This is because `default_members` is not available in cargo metadata.
 ///     See <https://github.com/rust-lang/cargo/issues/8033>.
+///
 /// In addition, if either `--package <pkg>` or `--exclude <pkg>` is given,
 /// validate that `<pkg>` is a package name in the workspace, or return an error
 /// otherwise.

kani-driver/src/cbmc_property_renderer.rs

@@ -700,6 +700,7 @@ fn update_properties_with_reach_status(
 /// Update the results of `code_coverage` (NOT `cover`) properties.
 /// - `SUCCESS` -> `UNCOVERED`
 /// - `FAILURE` -> `COVERED`
+///
 /// Note that these statuses are intermediate statuses that aren't reported to
 /// users but rather internally consumed and reported finally as `PARTIAL`, `FULL`
 /// or `NONE` based on aggregated line coverage results.
@@ -720,9 +721,10 @@ fn update_results_of_code_covererage_checks(mut properties: Vec<Property>) -> Ve
 
 /// Update the results of cover properties.
 /// We encode cover(cond) as assert(!cond), so if the assertion
-/// fails, then the cover property is satisfied and vice versa.
+/// fails, then the cover property is satisfied and vice versa:
 /// - SUCCESS -> UNSATISFIABLE
 /// - FAILURE -> SATISFIED
+///
 /// Note that if the cover property was unreachable, its status at this point
 /// will be `CheckStatus::Unreachable` and not `CheckStatus::Success` since
 /// `update_properties_with_reach_status` is called beforehand

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-05-17"
+channel = "nightly-2024-05-23"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

scripts/setup/ubuntu/install_deps.sh

@@ -16,6 +16,7 @@ DEPS=(
   gpg-agent
   jq
   libssl-dev
+  lld
   lsb-release
   make
   ninja-build

tests/script-based-pre/build-rs-conditional/Cargo.toml

@@ -7,3 +7,5 @@ edition = "2021"
 
 [dependencies]
 
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/cargo_playback_build/sample_crate/Cargo.toml

@@ -4,3 +4,6 @@
 name = "sample_crate"
 version = "0.1.0"
 edition = "2021"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/cargo_playback_opts/sample_crate/Cargo.toml

@@ -4,3 +4,6 @@
 name = "sample_crate"
 version = "0.1.0"
 edition = "2021"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/cargo_playback_target/sample_crate/Cargo.toml

@@ -15,3 +15,5 @@ doctest = false
 name = "bar"
 doctest = false
 
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tests/script-based-pre/concrete_playback_e2e/sample_crate/Cargo.toml

@@ -10,3 +10,6 @@ concrete-playback = "inplace"
 
 [package.metadata.kani.unstable]
 concrete-playback = true
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }

tools/compiletest/src/main.rs

@@ -388,7 +388,7 @@ fn collect_expected_tests_from_dir(
             && (file_path.to_str().unwrap().ends_with(".expected")
                 || "expected" == file_path.file_name().unwrap())
         {
-            fs::create_dir_all(&build_dir.join(file_path.file_stem().unwrap())).unwrap();
+            fs::create_dir_all(build_dir.join(file_path.file_stem().unwrap())).unwrap();
             let paths =
                 TestPaths { file: file_path, relative_dir: relative_dir_path.to_path_buf() };
             tests.push(make_test(config, &paths, inputs));
@@ -446,7 +446,7 @@ fn collect_exec_tests_from_dir(
         }
 
         // Create directory for test and add it to the tests to be run
-        fs::create_dir_all(&build_dir.join(file_path.file_stem().unwrap())).unwrap();
+        fs::create_dir_all(build_dir.join(file_path.file_stem().unwrap())).unwrap();
         let paths = TestPaths { file: file_path, relative_dir: relative_dir_path.to_path_buf() };
         tests.push(make_test(config, &paths, inputs));
     }