Merge branch 'main' into toolchain-issue

tautschnig · Sep 1, 2023 · 2e1f34e · 2e1f34e
2 parents b2efb32 + b119b0e
commit 2e1f34e
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`.