Enable -Z stubbing and error out instead of ignore stub (model-chec…

…king#2678) Enable `-Z stubbing`, deprecate `--enable-stubbing`, and emit an error if the user tries to verify a harness that has stubs without explicitly enabling stubs. This used to be a warning before which was easy to miss. It was also hard to debug when the harness would take a while to run. Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com>
tautschnig · Aug 30, 2023 · b119b0e · b119b0e
1 parent 03d9331
commit b119b0e
Show file tree

Hide file tree

Showing 44 changed files with 115 additions and 91 deletions.
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
@@ -299,7 +299,7 @@ pub struct VerificationArgs {
         requires("enable_unstable"),
         conflicts_with("concrete_playback")
     )]
-    pub enable_stubbing: bool,
+    enable_stubbing: bool,
 
     /// Enable Kani coverage output alongside verification result
     #[arg(long, hide_short_help = true)]
@@ -345,6 +345,12 @@ impl VerificationArgs {
             Some(Some(x)) => Some(x), // -j=x
         }
     }
+
+    /// Is experimental stubbing enabled?
+    pub fn is_stubbing_enabled(&self) -> bool {
+        self.enable_stubbing
+            || self.common_args.unstable_features.contains(&UnstableFeatures::Stubbing)
+    }
 }
 
 #[derive(Copy, Clone, Debug, PartialEq, Eq, ValueEnum)]
@@ -617,6 +623,10 @@ 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(&UnstableFeatures::ConcretePlayback)
         {

diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
@@ -92,7 +92,7 @@ impl KaniSession {
             flags.push("--write-json-symtab".into());
         }
 
-        if self.args.enable_stubbing {
+        if self.args.is_stubbing_enabled() {
             flags.push("--enable-stubbing".into());
         }
 

diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
@@ -4,14 +4,13 @@
 use anyhow::{bail, Result};
 use kani_metadata::{ArtifactType, HarnessMetadata};
 use rayon::prelude::*;
-use std::cmp::Ordering;
 use std::path::Path;
 
 use crate::args::OutputFormat;
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
 use crate::project::Project;
 use crate::session::KaniSession;
-use crate::util::{error, warning};
+use crate::util::error;
 
 /// A HarnessRunner is responsible for checking all proof harnesses. The data in this structure represents
 /// "background information" that the controlling driver (e.g. cargo-kani or kani) computed.
@@ -38,6 +37,8 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
         &self,
         harnesses: &'pr [&HarnessMetadata],
     ) -> Result<Vec<HarnessResult<'pr>>> {
+        self.check_stubbing(harnesses)?;
+
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
 
         let pool = {
@@ -70,6 +71,33 @@ impl<'sess, 'pr> HarnessRunner<'sess, 'pr> {
 
         Ok(results)
     }
+
+    /// Return an error if the user is trying to verify a harness with stubs without enabling the
+    /// experimental feature.
+    fn check_stubbing(&self, harnesses: &[&HarnessMetadata]) -> Result<()> {
+        if !self.sess.args.is_stubbing_enabled() {
+            let with_stubs: Vec<_> = harnesses
+                .iter()
+                .filter_map(|harness| {
+                    (!harness.attributes.stubs.is_empty()).then_some(harness.pretty_name.as_str())
+                })
+                .collect();
+            match with_stubs.as_slice() {
+                [] => { /* do nothing */ }
+                [harness] => bail!(
+                    "Use of unstable feature 'stubbing' in harness `{}`.\n\
+                    To enable stubbing, pass option `-Z stubbing`",
+                    harness
+                ),
+                harnesses => bail!(
+                    "Use of unstable feature 'stubbing' in harnesses `{}`.\n\
+                    To enable stubbing, pass option `-Z stubbing`",
+                    harnesses.join("`, `")
+                ),
+            }
+        }
+        Ok(())
+    }
 }
 
 impl KaniSession {
@@ -108,33 +136,6 @@ impl KaniSession {
         }
     }
 
-    /// Prints a warning at the end of the verification if harness contained a stub but stubs were
-    /// not enabled.
-    fn stubbing_statuses(&self, results: &[HarnessResult]) {
-        if !self.args.enable_stubbing {
-            let ignored_stubs: Vec<_> = results
-                .iter()
-                .filter_map(|result| {
-                    (!result.harness.attributes.stubs.is_empty())
-                        .then_some(result.harness.pretty_name.as_str())
-                })
-                .collect();
-            match ignored_stubs.len().cmp(&1) {
-                Ordering::Equal => warning(&format!(
-                    "harness `{}` contained stubs which were ignored.\n\
-                    To enable stubbing, pass options `--enable-unstable --enable-stubbing`",
-                    ignored_stubs[0]
-                )),
-                Ordering::Greater => warning(&format!(
-                    "harnesses `{}` contained stubs which were ignored.\n\
-                    To enable stubbing, pass options `--enable-unstable --enable-stubbing`",
-                    ignored_stubs.join("`, `")
-                )),
-                Ordering::Less => {}
-            }
-        }
-    }
-
     /// Concludes a session by printing a summary report and exiting the process with an
     /// error code (if applicable).
     ///
@@ -195,8 +196,6 @@ impl KaniSession {
             }
         }
 
-        self.stubbing_statuses(results);
-
         if failing > 0 {
             // Failure exit code without additional error message
             drop(self);

diff --git a/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml b/tests/cargo-kani/stubbing-do-not-resolve/Cargo.toml
@@ -11,5 +11,5 @@ edition = "2021"
 other_crate1 = { path = "other_crate1" }
 other_crate2 = { path = "other_crate2" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml b/tests/cargo-kani/stubbing-double-extern-path/harness/Cargo.toml
@@ -11,6 +11,7 @@ description = "Should test invoking double extern but found cycle issue"
 crate_b = { path = "../crate_b" }
 
 [package.metadata.kani.flags]
-enable-unstable = true
-enable-stubbing = true
 harness = ["check_inverted"]
+
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-extern-path/Cargo.toml b/tests/cargo-kani/stubbing-extern-path/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-foreign-method/Cargo.toml b/tests/cargo-kani/stubbing-foreign-method/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml b/tests/cargo-kani/stubbing-private-foreign-function/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml b/tests/cargo-kani/stubbing-public-foreign-function/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml b/tests/cargo-kani/stubbing-resolve-extern-crate-as/Cargo.toml
@@ -10,5 +10,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-as-foreign/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-use-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-foreign/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-glob-foreign/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml b/tests/cargo-kani/stubbing-use-in-foreign/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 other_crate = { path = "other_crate" }
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-validate-random/Cargo.toml b/tests/cargo-kani/stubbing-validate-random/Cargo.toml
@@ -8,5 +8,5 @@ edition = "2021"
 [dependencies]
 rand = "0.8.5"
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-kani/stubbing-ws-packages/Cargo.toml b/tests/cargo-kani/stubbing-ws-packages/Cargo.toml
@@ -5,6 +5,5 @@
 [workspace]
 members = ["dependency", "top"]
 
-[workspace.metadata.kani.flags]
-enable-unstable=true
-enable-stubbing=true
+[workspace.metadata.kani.unstable]
+stubbing=true
diff --git a/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml b/tests/cargo-ui/function-stubbing-trait-mismatch/Cargo.toml
@@ -7,5 +7,5 @@ edition = "2021"
 
 [dependencies]
 
-[package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true }
+[package.metadata.kani.unstable]
+stubbing = true
diff --git a/tests/cargo-ui/stubbing-flag/Cargo.toml b/tests/cargo-ui/stubbing-flag/Cargo.toml
@@ -8,4 +8,5 @@ edition = "2021"
 [dependencies]
 
 [package.metadata.kani]
-flags = { enable-unstable=true, enable-stubbing=true, harness="main" }
+flags = { harness="main" }
+unstable = { stubbing=true }
diff --git a/tests/expected/function-stubbing-error/expected b/tests/expected/function-stubbing-error/expected
@@ -0,0 +1,2 @@
+error: Use of unstable feature 'stubbing' in harness `main`.
+To enable stubbing, pass option `-Z stubbing`
diff --git a/...xpected/function-stubbing-warning/main.rs → .../expected/function-stubbing-error/main.rs b/...xpected/function-stubbing-warning/main.rs → .../expected/function-stubbing-error/main.rs
@@ -3,8 +3,7 @@
 //
 // kani-flags: --harness main
 //
-//! This tests whether we issue a warning if a stub is specified for a harness
-//! but stubbing is not enabled.
+//! This tests whether we abort if a stub is specified for a harness but stubbing is not enabled.
 
 fn foo() -> u32 {
     0

diff --git a/tests/expected/function-stubbing-warning/expected b/tests/expected/function-stubbing-warning/expected
diff --git a/tests/kani/Stubbing/enum_method.rs b/tests/kani/Stubbing/enum_method.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 stubbing for methods in local enums.
 

diff --git a/tests/kani/Stubbing/fixme_issue_1953.rs b/tests/kani/Stubbing/fixme_issue_1953.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --enable-stubbing --harness main
+// kani-flags: -Z stubbing --harness main
 //
 // We currently require a stub and the original/function method to have the same
 // names for generic parameters; instead, we should allow for renaming.

diff --git a/tests/kani/Stubbing/foreign_functions.rs b/tests/kani/Stubbing/foreign_functions.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --enable-stubbing
+// kani-flags: -Z stubbing
 //
 //! Check support for stubbing out foreign functions.
 

diff --git a/tests/kani/Stubbing/glob_cycle.rs b/tests/kani/Stubbing/glob_cycle.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness check_stub --enable-unstable --enable-stubbing
+// kani-flags: --harness check_stub -Z stubbing
 //! Test that stub can solve glob cycles.
 
 pub mod mod_a {

diff --git a/tests/kani/Stubbing/glob_path.rs b/tests/kani/Stubbing/glob_path.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness check_stub --enable-unstable --enable-stubbing
+// kani-flags: --harness check_stub -Z stubbing
 //! Test that stub can solve glob cycles even when the path expands the cycle.
 
 pub mod mod_a {

diff --git a/tests/kani/Stubbing/method_generic_type.rs b/tests/kani/Stubbing/method_generic_type.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 stubbing for methods of a local type that has generic parameters.
 

diff --git a/tests/kani/Stubbing/multiple_harnesses.rs b/tests/kani/Stubbing/multiple_harnesses.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --enable-unstable --enable-stubbing
+// kani-flags: -Z stubbing
 //! Check that Kani can handle a different combination of stubs in
 //! the same crate.
 

diff --git a/tests/kani/Stubbing/partial_harness_name.rs b/tests/kani/Stubbing/partial_harness_name.rs
@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //
-// kani-flags: --harness mod2::harness --enable-unstable --enable-stubbing
+// kani-flags: --harness mod2::harness -Z stubbing
 //
 //! This tests whether we correctly find harnesses during stubbing that are
 //! specified with a partially qualified name.

diff --git a/tests/kani/Stubbing/private_function.rs b/tests/kani/Stubbing/private_function.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 stubbing for private local functions.
 

diff --git a/tests/kani/Stubbing/public_function.rs b/tests/kani/Stubbing/public_function.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 stubbing for public local functions.
 

diff --git a/tests/kani/Stubbing/qualifiers.rs b/tests/kani/Stubbing/qualifiers.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 resolving stubs with the path qualifiers `self`, `super`, and
 //! `crate`.