From f6d33854ca95e25cbd52d52f3ca842b7eb07793f Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 2 Jul 2024 22:44:22 -0700 Subject: [PATCH] Remove deprecated `--enable-stubbing` (#3309) Part of #2279 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- kani-driver/src/args/mod.rs | 41 ++++++++----------- tests/cargo-ui/stubbing-flag/src/main.rs | 3 +- .../function-stubbing-no-harness/main.rs | 2 +- .../expected/stubbing-ambiguous-path/main.rs | 2 +- tests/ui/function-stubbing-error/main.rs | 2 +- .../deprecated-enable-stable/deprecated.rs | 16 -------- .../deprecated-enable-stable/expected | 2 - tests/ui/stubbing/invalid-path/invalid.rs | 2 +- tests/ui/stubbing/stubbing-flag/main.rs | 4 +- .../trait_mismatch.rs | 2 +- .../stubbing-type-validation/type_mismatch.rs | 2 +- 11 files changed, 28 insertions(+), 50 deletions(-) delete mode 100644 tests/ui/stubbing/deprecated-enable-stable/deprecated.rs delete mode 100644 tests/ui/stubbing/deprecated-enable-stable/expected diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 4c0fe98cc65d..d043035bcab2 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -282,17 +282,6 @@ pub struct VerificationArgs { #[arg(long)] pub randomize_layout: Option>, - /// Enable the stubbing of functions and methods. - // TODO: Stubbing should in principle work with concrete playback. - // - #[arg( - long, - hide_short_help = true, - requires("enable_unstable"), - conflicts_with("concrete_playback") - )] - enable_stubbing: bool, - /// Enable Kani coverage output alongside verification result #[arg(long, hide_short_help = true)] pub coverage: bool, @@ -345,8 +334,7 @@ impl VerificationArgs { /// Is experimental stubbing enabled? pub fn is_stubbing_enabled(&self) -> bool { - self.enable_stubbing - || self.common_args.unstable_features.contains(UnstableFeature::Stubbing) + self.common_args.unstable_features.contains(UnstableFeature::Stubbing) || self.is_function_contracts_enabled() } } @@ -579,6 +567,13 @@ impl ValidateArgs for VerificationArgs { --output-format=old.", )); } + if self.concrete_playback.is_some() && self.is_stubbing_enabled() { + // Concrete playback currently does not work with contracts or stubbing. + return Err(Error::raw( + ErrorKind::ArgumentConflict, + "Conflicting options: --concrete-playback isn't compatible with stubbing.", + )); + } if self.concrete_playback.is_some() && self.jobs() != Some(1) { // Concrete playback currently embeds a lot of assumptions about the order in which harnesses get called. return Err(Error::raw( @@ -606,10 +601,6 @@ impl ValidateArgs for VerificationArgs { } } - if self.enable_stubbing { - print_deprecated(&self.common_args, "--enable-stubbing", "-Z stubbing"); - } - if self.concrete_playback.is_some() && !self.common_args.unstable_features.contains(UnstableFeature::ConcretePlayback) { @@ -880,14 +871,18 @@ mod tests { #[test] fn check_enable_stubbing() { - check_unstable_flag!("--enable-stubbing --harness foo", enable_stubbing); + let res = parse_unstable_disabled("--harness foo").unwrap(); + assert!(!res.verify_opts.is_stubbing_enabled()); - check_unstable_flag!("--enable-stubbing", enable_stubbing); + let res = parse_unstable_disabled("--harness foo -Z stubbing").unwrap(); + assert!(res.verify_opts.is_stubbing_enabled()); - // `--enable-stubbing` cannot be called with `--concrete-playback` - let err = - parse_unstable_enabled("--enable-stubbing --harness foo --concrete-playback=print") - .unwrap_err(); + // `-Z stubbing` cannot be called with `--concrete-playback` + let res = parse_unstable_disabled( + "--harness foo --concrete-playback=print -Z concrete-playback -Z stubbing", + ) + .unwrap(); + let err = res.validate().unwrap_err(); assert_eq!(err.kind(), ErrorKind::ArgumentConflict); } diff --git a/tests/cargo-ui/stubbing-flag/src/main.rs b/tests/cargo-ui/stubbing-flag/src/main.rs index db26e366005e..1ef312b852ff 100644 --- a/tests/cargo-ui/stubbing-flag/src/main.rs +++ b/tests/cargo-ui/stubbing-flag/src/main.rs @@ -1,7 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -//! This tests that the `--enable-stubbing` and `--harness` arguments flow from `kani-driver` to `kani-compiler`. +//! This tests that enabling stubbing and using `--harness` arguments flow from +//! `kani-driver` to `kani-compiler`. #[kani::proof] fn main() {} diff --git a/tests/expected/function-stubbing-no-harness/main.rs b/tests/expected/function-stubbing-no-harness/main.rs index 1819c8dce862..d69192ae2180 100644 --- a/tests/expected/function-stubbing-no-harness/main.rs +++ b/tests/expected/function-stubbing-no-harness/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness foo --enable-unstable --enable-stubbing +// kani-flags: --harness foo -Z stubbing // //! This tests whether we detect missing harnesses during stubbing. diff --git a/tests/expected/stubbing-ambiguous-path/main.rs b/tests/expected/stubbing-ambiguous-path/main.rs index 7a406d51d227..9ab25b501a44 100644 --- a/tests/expected/stubbing-ambiguous-path/main.rs +++ b/tests/expected/stubbing-ambiguous-path/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main --enable-unstable --enable-stubbing +// kani-flags: --harness main -Z stubbing // //! This tests that we raise an error if a path in a `kani::stub` attribute can //! resolve to multiple functions. diff --git a/tests/ui/function-stubbing-error/main.rs b/tests/ui/function-stubbing-error/main.rs index 2f5a10ff18cb..c433e352e740 100644 --- a/tests/ui/function-stubbing-error/main.rs +++ b/tests/ui/function-stubbing-error/main.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main --enable-unstable --enable-stubbing +// kani-flags: --harness main -Z stubbing // //! This tests whether we detect syntactically misformed `kani::stub` annotations. diff --git a/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs b/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs deleted file mode 100644 index a5686af20a35..000000000000 --- a/tests/ui/stubbing/deprecated-enable-stable/deprecated.rs +++ /dev/null @@ -1,16 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: --enable-unstable --enable-stubbing -//! Checks that the `kani::stub` attribute is accepted - -fn foo() { - unreachable!(); -} - -fn bar() {} - -#[kani::proof] -#[kani::stub(foo, bar)] -fn main() { - foo(); -} diff --git a/tests/ui/stubbing/deprecated-enable-stable/expected b/tests/ui/stubbing/deprecated-enable-stable/expected deleted file mode 100644 index eb05b8cf9812..000000000000 --- a/tests/ui/stubbing/deprecated-enable-stable/expected +++ /dev/null @@ -1,2 +0,0 @@ -warning: The `--enable-stubbing` option is deprecated. This option will be removed soon. Consider using `-Z stubbing` instead -VERIFICATION:- SUCCESSFUL diff --git a/tests/ui/stubbing/invalid-path/invalid.rs b/tests/ui/stubbing/invalid-path/invalid.rs index d24c757fd0cd..04d3c786b0d7 100644 --- a/tests/ui/stubbing/invalid-path/invalid.rs +++ b/tests/ui/stubbing/invalid-path/invalid.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness invalid_stub --enable-unstable --enable-stubbing +// kani-flags: --harness invalid_stub -Z stubbing pub mod mod_a { use crate::mod_b::noop; diff --git a/tests/ui/stubbing/stubbing-flag/main.rs b/tests/ui/stubbing/stubbing-flag/main.rs index f9b788e94d82..a5172ad9d0cd 100644 --- a/tests/ui/stubbing/stubbing-flag/main.rs +++ b/tests/ui/stubbing/stubbing-flag/main.rs @@ -1,9 +1,9 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness main --enable-unstable --enable-stubbing +// kani-flags: --harness main -Z stubbing // -//! This tests that the `--enable-stubbing` and `--harness` arguments flow from `kani-driver` to `kani-compiler`. +//! This tests that enabling stubbing and `--harness` argument flow from `kani-driver` to `kani-compiler`. #[kani::proof] fn main() {} diff --git a/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs b/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs index e934141664bf..c49552d942e2 100644 --- a/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs +++ b/tests/ui/stubbing/stubbing-trait-validation/trait_mismatch.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness harness --enable-unstable --enable-stubbing +// kani-flags: --harness harness -Z stubbing // //! This tests that we catch trait mismatches between the stub and the original //! function/method. In particular, this tests the case when the program is diff --git a/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs b/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs index 9f98ae302a22..bc8343658f9e 100644 --- a/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs +++ b/tests/ui/stubbing/stubbing-type-validation/type_mismatch.rs @@ -1,7 +1,7 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --harness harness --enable-unstable --enable-stubbing +// kani-flags: --harness harness -Z stubbing // //! This tests that we catch type mismatches between the stub and the original //! function/method.