Support flags for function/method stubbing (rust-lang#1820)

Co-authored-by: Adrian Palacios <[email protected]>

Author: aaronbembenek-aws

kani-compiler/src/main.rs

@@ -106,6 +106,10 @@ fn main() -> Result<(), &'static str> {
     // Generate rustc args.
     let rustc_args = generate_rustc_args(&matches);
 
+    if matches.is_present(parser::ENABLE_STUBBING) {
+        eprintln!("warning: Kani currently does not perform any stubbing.");
+    }
+
     // Configure and run compiler.
     let mut callbacks = KaniCallbacks {};
     let mut compiler = RunCompiler::new(&rustc_args, &mut callbacks);

kani-compiler/src/parser.rs

@@ -47,6 +47,12 @@ pub const SYSROOT: &str = "sysroot";
 pub const REACHABILITY: &str = "reachability";
 pub const REACHABILITY_FLAG: &str = "--reachability";
 
+/// Option name used to specify which harness is the target.
+pub const HARNESS: &str = "harness";
+
+/// Option name used to enable stubbing.
+pub const ENABLE_STUBBING: &str = "enable-stubbing";
+
 /// Option name used to pass extra rustc-options.
 pub const RUSTC_OPTIONS: &str = "rustc-options";
 
@@ -157,6 +163,21 @@ pub fn parser<'a, 'b>() -> App<'a, 'b> {
             Arg::with_name(IGNORE_GLOBAL_ASM)
                 .long("--ignore-global-asm")
                 .help("Suppress error due to the existence of global_asm in a crate"),
+        )
+        .arg(
+            // TODO: Remove this argument once stubbing works for multiple harnesses at a time.
+            // <https://github.com/model-checking/kani/issues/1841>
+            Arg::with_name(HARNESS)
+                .long("--harness")
+                .help("Selects the harness to target.")
+                .value_name("HARNESS")
+                .takes_value(true),
+        )
+        .arg(
+            Arg::with_name(ENABLE_STUBBING)
+                .long("--enable-stubbing")
+                .help("Instruct the compiler to perform stubbing.")
+                .requires(HARNESS),
         );
     #[cfg(feature = "unsound_experiments")]
     let app = crate::unsound_experiments::arg_parser::add_unsound_experiments_to_parser(app);
@@ -214,6 +235,8 @@ pub fn command_arguments(args: &Vec<String>) -> Vec<String> {
 
 #[cfg(test)]
 mod parser_test {
+    use clap::ErrorKind;
+
     use super::*;
 
     #[test]
@@ -231,6 +254,19 @@ mod parser_test {
         assert_eq!(matches.value_of("kani-lib"), Some("some/path"));
     }
 
+    #[test]
+    fn test_stubbing_flags() {
+        let args = vec!["kani-compiler", "--enable-stubbing", "--harness", "foo"];
+        let matches = parser().get_matches_from(args);
+        assert!(matches.is_present("enable-stubbing"));
+        assert_eq!(matches.value_of("harness"), Some("foo"));
+
+        // `--enable-stubbing` cannot be called without `--harness`
+        let args = vec!["kani-compiler", "--enable-stubbing"];
+        let err = parser().get_matches_from_safe(args).unwrap_err();
+        assert_eq!(err.kind, ErrorKind::MissingRequiredArgument);
+    }
+
     #[test]
     fn test_cargo_kani_hack_noop() {
         let args = ["kani-compiler", "some/path"];

kani-driver/src/args.rs

@@ -226,6 +226,18 @@ pub struct KaniArgs {
     /// See the `-Z randomize-layout` and `-Z layout-seed` arguments of the rust compiler.
     #[structopt(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>
+    #[structopt(
+        long,
+        hidden_short_help(true),
+        requires("enable-unstable"),
+        requires("harness"),
+        conflicts_with("concrete-playback")
+    )]
+    pub enable_stubbing: bool,
     /*
     The below is a "TODO list" of things not yet implemented from the kani_flags.py script.
 
@@ -577,4 +589,19 @@ mod tests {
             ErrorKind::ArgumentConflict,
         );
     }
+
+    #[test]
+    fn check_enable_stubbing() {
+        check_unstable_flag("--enable-stubbing --harness foo");
+
+        // `--enable-stubbing` cannot be called without `--harness`
+        let err = parse_unstable_enabled("--enable-stubbing").unwrap_err();
+        assert_eq!(err.kind, ErrorKind::MissingRequiredArgument);
+
+        // `--enable-stubbing` cannot be called with `--concrete-playback`
+        let err =
+            parse_unstable_enabled("--enable-stubbing --harness foo --concrete-playback=print")
+                .unwrap_err();
+        assert_eq!(err.kind, ErrorKind::ArgumentConflict);
+    }
 }

kani-driver/src/call_single_file.rs

@@ -129,6 +129,13 @@ impl KaniSession {
             flags.push("--ignore-global-asm".into());
         }
 
+        if self.args.enable_stubbing {
+            flags.push("--enable-stubbing".into());
+        }
+        if let Some(harness) = &self.args.harness {
+            flags.push(format!("--harness={harness}").into());
+        }
+
         #[cfg(feature = "unsound_experiments")]
         flags.extend(self.args.unsound_experiments.process_args());
 

tests/cargo-ui/stubbing-flag/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "stubbing-flag"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+
+[package.metadata.kani]
+flags = { enable-unstable=true, enable-stubbing=true, harness="main" }

tests/cargo-ui/stubbing-flag/expected

@@ -0,0 +1,3 @@
+warning: Kani currently does not perform any stubbing.
+
+VERIFICATION:- SUCCESSFUL

tests/cargo-ui/stubbing-flag/src/main.rs

@@ -0,0 +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`
+//! (and that we warn that no actual stubbing is being performed).
+
+#[kani::proof]
+fn main() {}

tests/ui/stubbing-flag/expected

@@ -0,0 +1,3 @@
+warning: Kani currently does not perform any stubbing.
+
+VERIFICATION:- SUCCESSFUL

tests/ui/stubbing-flag/main.rs

@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --harness main --enable-unstable --enable-stubbing
+//
+//! This tests that the `--enable-stubbing` and `--harness` arguments flow from `kani-driver` to `kani-compiler`
+//! (and that we warn that no actual stubbing is being performed).
+
+#[kani::proof]
+fn main() {}