From 04497e59c10c46ea3bafe5ebb4e2f4a05c65a3c4 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 23 May 2024 15:23:06 -0400 Subject: [PATCH 1/4] Update Rust toolchain from nightly-2024-05-17 to nightly-2024-05-23 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 78849f9db7f3..8cc564b125c4 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-05-17" +channel = "nightly-2024-05-23" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 194b96d6637bbeb7dac45db3dcb9e01e915a0a82 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 23 May 2024 15:46:02 -0400 Subject: [PATCH 2/4] Fix clippy warnings --- cprover_bindings/src/goto_program/expr.rs | 3 ++- cprover_bindings/src/irep/goto_binary_serde.rs | 8 +++----- .../src/codegen_cprover_gotoc/codegen/function.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 11 +++++++---- .../src/codegen_cprover_gotoc/codegen/operand.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/place.rs | 5 +++-- .../src/codegen_cprover_gotoc/codegen/typ.rs | 4 ++-- .../src/codegen_cprover_gotoc/context/goto_ctx.rs | 1 + kani-compiler/src/kani_compiler.rs | 7 ++++--- kani-compiler/src/kani_middle/reachability.rs | 5 +++-- kani-driver/src/args_toml.rs | 5 ++++- kani-driver/src/call_cargo.rs | 13 ++++++++----- kani-driver/src/cbmc_property_renderer.rs | 4 +++- tools/compiletest/src/main.rs | 4 ++-- 14 files changed, 44 insertions(+), 30 deletions(-) diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 905e47bc6034..c76b58023784 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -1055,6 +1055,7 @@ impl Expr { /// ). /// 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)); } } } diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs index 4eb1a0720f22..324c5e764d1a 100644 --- a/cprover_bindings/src/irep/goto_binary_serde.rs +++ b/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` -/// - the inverse direction from unique numbers to [NumberedIrep] is implemented -/// using a `Vec` called the `index` that stores [NumberedIrep] -/// under their unique number. +/// - the forward directon from [IrepKey] to unique numbers is implemented using a `HashMap` +/// - the inverse direction from unique numbers to [NumberedIrep] is implemented usign a `Vec` +/// 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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index d55696bfdc87..33ec70294d04 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/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), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 3a4e84a70d98..4e965b4105ef 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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::()` bytes (done by calls to `memmove`) /// * (Exclusive to nonoverlapping copy) The region of memory beginning - /// at `src` with a size of `count * size_of::()` 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::()` 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 for more details + /// See for more details fn codegen_volatile_load( &mut self, mut fargs: Vec, @@ -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( diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 6c75c6a5ad5a..c8aba08ba5ed 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/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" { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 56b7da2e7628..771a38ac922d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/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 thread. + /// + /// Note that projection inside SIMD structs may eventually become illegal. + /// See thread . /// /// Since the goto representation for both is the same, we use the expected type to decide /// what to return. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index df36189f4606..c091d0b74ead 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/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. diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 095f907228a4..9a81838b7fc2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/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; diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index fc5f5891ecae..1793165bdf81 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/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} diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 456d5425b245..71eb4931aad4 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/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. diff --git a/kani-driver/src/args_toml.rs b/kani-driver/src/args_toml.rs index aaa5b3260083..b9e994b38fec 100644 --- a/kani-driver/src/args_toml.rs +++ b/kani-driver/src/args_toml.rs @@ -90,8 +90,11 @@ fn cargo_locate_project(input_args: &[OsString]) -> Result { /// 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, Vec)> { let config = tomldata.parse::()?; // To make testing easier, our function contract is to produce a stable ordering of flags for a given input. diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 9d27e5853696..2d5d36306e21 100644 --- a/kani-driver/src/call_cargo.rs +++ b/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 ` is given, return the list of packages selected. -/// If `--exclude ` 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 ` is given, return the list of packages selected. +/// - If `--exclude ` 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 . +/// /// In addition, if either `--package ` or `--exclude ` is given, /// validate that `` is a package name in the workspace, or return an error /// otherwise. diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index c233959abd6a..7e4fffe42812 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/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) -> 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 diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs index 5418ad47f7fa..94cbd561aa51 100644 --- a/tools/compiletest/src/main.rs +++ b/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)); } From cc0323594b08c9c6864b887d20f0c2c771306e29 Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Thu, 23 May 2024 16:13:40 -0400 Subject: [PATCH 3/4] Silence linter warning on `cfg(kani)` --- tests/script-based-pre/build-rs-conditional/Cargo.toml | 2 ++ .../cargo_playback_build/sample_crate/Cargo.toml | 3 +++ .../cargo_playback_opts/sample_crate/Cargo.toml | 3 +++ .../cargo_playback_target/sample_crate/Cargo.toml | 2 ++ .../concrete_playback_e2e/sample_crate/Cargo.toml | 3 +++ 5 files changed, 13 insertions(+) diff --git a/tests/script-based-pre/build-rs-conditional/Cargo.toml b/tests/script-based-pre/build-rs-conditional/Cargo.toml index 136bae92250e..ecf681268dfe 100644 --- a/tests/script-based-pre/build-rs-conditional/Cargo.toml +++ b/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)'] } diff --git a/tests/script-based-pre/cargo_playback_build/sample_crate/Cargo.toml b/tests/script-based-pre/cargo_playback_build/sample_crate/Cargo.toml index c00d0ccc4bdb..99dfd67443f5 100644 --- a/tests/script-based-pre/cargo_playback_build/sample_crate/Cargo.toml +++ b/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)'] } diff --git a/tests/script-based-pre/cargo_playback_opts/sample_crate/Cargo.toml b/tests/script-based-pre/cargo_playback_opts/sample_crate/Cargo.toml index c00d0ccc4bdb..99dfd67443f5 100644 --- a/tests/script-based-pre/cargo_playback_opts/sample_crate/Cargo.toml +++ b/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)'] } diff --git a/tests/script-based-pre/cargo_playback_target/sample_crate/Cargo.toml b/tests/script-based-pre/cargo_playback_target/sample_crate/Cargo.toml index 30949391c0c7..5ece6c5e0f60 100644 --- a/tests/script-based-pre/cargo_playback_target/sample_crate/Cargo.toml +++ b/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)'] } diff --git a/tests/script-based-pre/concrete_playback_e2e/sample_crate/Cargo.toml b/tests/script-based-pre/concrete_playback_e2e/sample_crate/Cargo.toml index 4a7016cb51ed..39cfab289878 100644 --- a/tests/script-based-pre/concrete_playback_e2e/sample_crate/Cargo.toml +++ b/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)'] } From ff736e5426b37e2a4aef1b7197fb40af5237581c Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 24 May 2024 18:02:11 +0000 Subject: [PATCH 4/4] Add `lld` on ubuntu --- scripts/setup/ubuntu/install_deps.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/setup/ubuntu/install_deps.sh b/scripts/setup/ubuntu/install_deps.sh index 2830d0280498..b93602691222 100755 --- a/scripts/setup/ubuntu/install_deps.sh +++ b/scripts/setup/ubuntu/install_deps.sh @@ -16,6 +16,7 @@ DEPS=( gpg-agent jq libssl-dev + lld lsb-release make ninja-build