From 8de24f5387a4f80b9152e3015beddd78522a0751 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 1 Oct 2024 11:07:56 -0700 Subject: [PATCH 1/5] Remove obsolete linker options --- kani-driver/src/args/mod.rs | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 72de44e36014..6e8cd67dad47 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -189,14 +189,6 @@ pub struct VerificationArgs { #[arg(long, hide_short_help = true)] pub only_codegen: bool, - /// Deprecated flag. This is a no-op since we no longer support the legacy linker and - /// it will be removed in a future Kani release. - #[arg(long, hide = true, conflicts_with("mir_linker"))] - pub legacy_linker: bool, - /// Deprecated flag. This is a no-op since we no longer support any other linker. - #[arg(long, hide = true)] - pub mir_linker: bool, - /// Specify the value used for loop unwinding in CBMC #[arg(long)] pub default_unwind: Option, @@ -524,14 +516,6 @@ impl ValidateArgs for VerificationArgs { } } - if self.mir_linker { - print_obsolete(&self.common_args, "--mir-linker"); - } - - if self.legacy_linker { - print_obsolete(&self.common_args, "--legacy-linker"); - } - // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified. // We should consider improving the error messages slightly in a later pull request. if natives_unwind && extra_unwind { From fdfb51f600c9c0461da1ecf55356af484dc96dd6 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 1 Oct 2024 11:26:07 -0700 Subject: [PATCH 2/5] Allow dead code --- kani-driver/src/args/mod.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 6e8cd67dad47..573ad21ab31a 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -40,6 +40,7 @@ where .unwrap() } +#[allow(dead_code)] pub fn print_obsolete(verbosity: &CommonArgs, option: &str) { if !verbosity.quiet { warning(&format!( From 385348171f28ad15abf54c0d15e45d13f2f39910 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 1 Oct 2024 12:07:08 -0700 Subject: [PATCH 3/5] Remove --mir-linker from tests --- tests/cargo-kani/mir-linker/Cargo.toml | 13 --------- tests/cargo-kani/mir-linker/expected | 3 -- tests/cargo-kani/mir-linker/src/lib.rs | 29 ------------------- tests/kani/UnsizedCoercion/basic_coercion.rs | 1 - .../UnsizedCoercion/basic_inner_coercion.rs | 1 - .../UnsizedCoercion/basic_outer_coercion.rs | 1 - tests/kani/UnsizedCoercion/box_coercion.rs | 1 - .../UnsizedCoercion/box_inner_coercion.rs | 1 - .../UnsizedCoercion/box_outer_coercion.rs | 1 - .../UnsizedCoercion/custom_outer_coercion.rs | 1 - tests/kani/UnsizedCoercion/double_coercion.rs | 1 - .../kani/UnsizedCoercion/rc_outer_coercion.rs | 1 - .../trait_to_trait_coercion.rs | 1 - tests/perf/string/src/any_str.rs | 5 ---- .../Strings/copy_empty_string_by_intrinsic.rs | 1 - .../mir-linker/generic-harness/incorrect.rs | 2 -- 16 files changed, 63 deletions(-) delete mode 100644 tests/cargo-kani/mir-linker/Cargo.toml delete mode 100644 tests/cargo-kani/mir-linker/expected delete mode 100644 tests/cargo-kani/mir-linker/src/lib.rs diff --git a/tests/cargo-kani/mir-linker/Cargo.toml b/tests/cargo-kani/mir-linker/Cargo.toml deleted file mode 100644 index 39d5016a407b..000000000000 --- a/tests/cargo-kani/mir-linker/Cargo.toml +++ /dev/null @@ -1,13 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -[package] -name = "mir-linker" -version = "0.1.0" -edition = "2021" -description = "Ensures that the mir-linker works accross crates" - -[dependencies] -semver = "1.0" - -[package.metadata.kani] -flags = { mir-linker=true, enable-unstable=true } diff --git a/tests/cargo-kani/mir-linker/expected b/tests/cargo-kani/mir-linker/expected deleted file mode 100644 index 2a5a5ac367ba..000000000000 --- a/tests/cargo-kani/mir-linker/expected +++ /dev/null @@ -1,3 +0,0 @@ -Status: SUCCESS\ -Next is greater\ -in function check_version diff --git a/tests/cargo-kani/mir-linker/src/lib.rs b/tests/cargo-kani/mir-linker/src/lib.rs deleted file mode 100644 index a1514d454828..000000000000 --- a/tests/cargo-kani/mir-linker/src/lib.rs +++ /dev/null @@ -1,29 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! Dummy test to check --mir-linker runs on a cargo project. -use semver::{BuildMetadata, Prerelease, Version}; - -#[kani::proof] -fn check_version() { - let next_major: u64 = kani::any(); - let next_minor: u64 = kani::any(); - kani::assume(next_major != 0 || next_minor != 0); - - // Check whether this requirement matches version 1.2.3-alpha.1 (no) - let v0 = Version { - major: 0, - minor: 0, - patch: 0, - pre: Prerelease::EMPTY, - build: BuildMetadata::EMPTY, - }; - let next = Version { - major: next_major, - minor: next_minor, - patch: 0, - pre: Prerelease::EMPTY, - build: BuildMetadata::EMPTY, - }; - assert!(next > v0, "Next is greater"); -} diff --git a/tests/kani/UnsizedCoercion/basic_coercion.rs b/tests/kani/UnsizedCoercion/basic_coercion.rs index a60a76aec3be..ee8c80e87011 100644 --- a/tests/kani/UnsizedCoercion/basic_coercion.rs +++ b/tests/kani/UnsizedCoercion/basic_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using built-in references and pointers. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/basic_inner_coercion.rs b/tests/kani/UnsizedCoercion/basic_inner_coercion.rs index efc84b61ea1e..19d8f39fed7e 100644 --- a/tests/kani/UnsizedCoercion/basic_inner_coercion.rs +++ b/tests/kani/UnsizedCoercion/basic_inner_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using built-in references and pointers. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/basic_outer_coercion.rs b/tests/kani/UnsizedCoercion/basic_outer_coercion.rs index a2b5bfae3129..633dfbdaa995 100644 --- a/tests/kani/UnsizedCoercion/basic_outer_coercion.rs +++ b/tests/kani/UnsizedCoercion/basic_outer_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using built-in references and pointers. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/box_coercion.rs b/tests/kani/UnsizedCoercion/box_coercion.rs index e022bdef06e1..106f586f8eed 100644 --- a/tests/kani/UnsizedCoercion/box_coercion.rs +++ b/tests/kani/UnsizedCoercion/box_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using boxes. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/box_inner_coercion.rs b/tests/kani/UnsizedCoercion/box_inner_coercion.rs index 35f10373d5ef..4e8a8b56624c 100644 --- a/tests/kani/UnsizedCoercion/box_inner_coercion.rs +++ b/tests/kani/UnsizedCoercion/box_inner_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using boxes. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/box_outer_coercion.rs b/tests/kani/UnsizedCoercion/box_outer_coercion.rs index 586f54003cdf..2d91360cd576 100644 --- a/tests/kani/UnsizedCoercion/box_outer_coercion.rs +++ b/tests/kani/UnsizedCoercion/box_outer_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using boxes. //! Tests are broken down into different crates to ensure that the reachability works for each case. mod defs; diff --git a/tests/kani/UnsizedCoercion/custom_outer_coercion.rs b/tests/kani/UnsizedCoercion/custom_outer_coercion.rs index 7f7d68ef6e84..6d75204223c1 100644 --- a/tests/kani/UnsizedCoercion/custom_outer_coercion.rs +++ b/tests/kani/UnsizedCoercion/custom_outer_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using a custom CoerceUnsized implementation. //! Tests are broken down into different crates to ensure that the reachability works for each case. #![feature(coerce_unsized)] diff --git a/tests/kani/UnsizedCoercion/double_coercion.rs b/tests/kani/UnsizedCoercion/double_coercion.rs index 26cfb585821e..76158c811c00 100644 --- a/tests/kani/UnsizedCoercion/double_coercion.rs +++ b/tests/kani/UnsizedCoercion/double_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion when using box of box. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/kani/UnsizedCoercion/rc_outer_coercion.rs b/tests/kani/UnsizedCoercion/rc_outer_coercion.rs index 2543498cca80..7a608d7d1d57 100644 --- a/tests/kani/UnsizedCoercion/rc_outer_coercion.rs +++ b/tests/kani/UnsizedCoercion/rc_outer_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using reference counter. //! Tests are broken down into different crates to ensure that the reachability works for each case. mod defs; diff --git a/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs b/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs index 32875f8b8e22..b7750db487e2 100644 --- a/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs +++ b/tests/kani/UnsizedCoercion/trait_to_trait_coercion.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --mir-linker --enable-unstable //! Check the basic coercion from using built-in references and pointers. //! Tests are broken down into different crates to ensure that the reachability works for each case. diff --git a/tests/perf/string/src/any_str.rs b/tests/perf/string/src/any_str.rs index 3b58d56750a7..6b3f9cffbc37 100644 --- a/tests/perf/string/src/any_str.rs +++ b/tests/perf/string/src/any_str.rs @@ -1,10 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// -// kani-flags: --enable-unstable --mir-linker -// -//! This test is to check MIR linker state of the art. -//! I.e.: Currently, this should fail with missing function definition. #[kani::proof] #[kani::unwind(4)] diff --git a/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs b/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs index a0c1bef7d003..596bedaa7825 100644 --- a/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs +++ b/tests/slow/kani/Strings/copy_empty_string_by_intrinsic.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --mir-linker //! Make sure we can handle explicit copy_nonoverlapping on empty string //! This used to trigger an issue: https://github.com/model-checking/kani/issues/241 diff --git a/tests/ui/mir-linker/generic-harness/incorrect.rs b/tests/ui/mir-linker/generic-harness/incorrect.rs index e68eba6ec834..e52b06801517 100644 --- a/tests/ui/mir-linker/generic-harness/incorrect.rs +++ b/tests/ui/mir-linker/generic-harness/incorrect.rs @@ -1,8 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --enable-unstable --mir-linker -// //! Checks that we correctly fail if the harness is a generic function. #[kani::proof] From 040ab6feac70ce9ac2bb97c3aa138688d4aed6a3 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 1 Oct 2024 14:02:56 -0700 Subject: [PATCH 4/5] Remove --mir-linker from Cargo.toml --- tests/cargo-kani/asm/global/Cargo.toml | 2 +- tests/cargo-ui/ws-integ-tests/Cargo.toml | 2 -- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/tests/cargo-kani/asm/global/Cargo.toml b/tests/cargo-kani/asm/global/Cargo.toml index 21ff904a2f99..79ffab9377c1 100644 --- a/tests/cargo-kani/asm/global/Cargo.toml +++ b/tests/cargo-kani/asm/global/Cargo.toml @@ -13,4 +13,4 @@ crate_with_global_asm = { path = "crate_with_global_asm" } [package.metadata.kani] # Issue with MIR Linker on static constant. -flags = { enable-unstable = true, ignore-global-asm = true, mir-linker = true } +flags = { enable-unstable = true, ignore-global-asm = true } diff --git a/tests/cargo-ui/ws-integ-tests/Cargo.toml b/tests/cargo-ui/ws-integ-tests/Cargo.toml index b09d4c9a5f19..93c4baebe120 100644 --- a/tests/cargo-ui/ws-integ-tests/Cargo.toml +++ b/tests/cargo-ui/ws-integ-tests/Cargo.toml @@ -15,5 +15,3 @@ members = [ [workspace.metadata.kani.flags] workspace = true tests = true -enable-unstable=true -mir-linker=true From b751ad8698404be4405f4a0d3c5cd22d83e8b733 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Tue, 1 Oct 2024 14:34:25 -0700 Subject: [PATCH 5/5] Add back test --- tests/cargo-kani/mir-linker/Cargo.toml | 10 +++++++++ tests/cargo-kani/mir-linker/expected | 3 +++ tests/cargo-kani/mir-linker/src/lib.rs | 29 ++++++++++++++++++++++++++ 3 files changed, 42 insertions(+) create mode 100644 tests/cargo-kani/mir-linker/Cargo.toml create mode 100644 tests/cargo-kani/mir-linker/expected create mode 100644 tests/cargo-kani/mir-linker/src/lib.rs diff --git a/tests/cargo-kani/mir-linker/Cargo.toml b/tests/cargo-kani/mir-linker/Cargo.toml new file mode 100644 index 000000000000..f00d4c687864 --- /dev/null +++ b/tests/cargo-kani/mir-linker/Cargo.toml @@ -0,0 +1,10 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "mir-linker" +version = "0.1.0" +edition = "2021" +description = "Ensures that the mir-linker works accross crates" + +[dependencies] +semver = "1.0" diff --git a/tests/cargo-kani/mir-linker/expected b/tests/cargo-kani/mir-linker/expected new file mode 100644 index 000000000000..2a5a5ac367ba --- /dev/null +++ b/tests/cargo-kani/mir-linker/expected @@ -0,0 +1,3 @@ +Status: SUCCESS\ +Next is greater\ +in function check_version diff --git a/tests/cargo-kani/mir-linker/src/lib.rs b/tests/cargo-kani/mir-linker/src/lib.rs new file mode 100644 index 000000000000..a1514d454828 --- /dev/null +++ b/tests/cargo-kani/mir-linker/src/lib.rs @@ -0,0 +1,29 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Dummy test to check --mir-linker runs on a cargo project. +use semver::{BuildMetadata, Prerelease, Version}; + +#[kani::proof] +fn check_version() { + let next_major: u64 = kani::any(); + let next_minor: u64 = kani::any(); + kani::assume(next_major != 0 || next_minor != 0); + + // Check whether this requirement matches version 1.2.3-alpha.1 (no) + let v0 = Version { + major: 0, + minor: 0, + patch: 0, + pre: Prerelease::EMPTY, + build: BuildMetadata::EMPTY, + }; + let next = Version { + major: next_major, + minor: next_minor, + patch: 0, + pre: Prerelease::EMPTY, + build: BuildMetadata::EMPTY, + }; + assert!(next > v0, "Next is greater"); +}