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 <[email protected]>
model-checking · Jul 3, 2024 · f6d3385 · f6d3385
1 parent d926482
commit f6d3385
Show file tree

Hide file tree

Showing 11 changed files with 28 additions and 50 deletions.
diff --git 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<Option<u64>>,
 
-    /// Enable the stubbing of functions and methods.
-    // TODO: Stubbing should in principle work with concrete playback.
-    // <https://github.com/model-checking/kani/issues/1842>
-    #[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
@@ -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
@@ -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
@@ -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
@@ -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
diff --git a/tests/ui/stubbing/deprecated-enable-stable/expected b/tests/ui/stubbing/deprecated-enable-stable/expected
diff --git 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
@@ -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
@@ -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
@@ -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.