Remove --dry-run from Kani. (rust-lang#1943)

Author: celinval

kani-driver/src/args.rs

@@ -67,7 +67,7 @@ pub struct KaniArgs {
     #[arg(
         long,
         requires("enable_unstable"),
-        conflicts_with_all(&["visualize", "dry_run"]),
+        conflicts_with_all(&["visualize"]),
         ignore_case = true,
         value_enum
     )]
@@ -89,10 +89,9 @@ pub struct KaniArgs {
     #[arg(long, hide_short_help = true)]
     pub enable_unstable: bool,
 
-    // Hide this since it depends on function that is a hidden option.
-    /// Print commands instead of running them. This command uses "harness" as a place holder for
-    /// name of the target harness.
-    #[arg(long, hide = true, requires("enable_unstable"))]
+    /// We no longer support dry-run. Use `--verbose` to see the commands being printed during
+    /// Kani execution.
+    #[arg(long, hide = true)]
     pub dry_run: bool,
 
     /// Generate C file equivalent to inputted program.
@@ -118,11 +117,10 @@ pub struct KaniArgs {
 
     /// Entry point for verification (symbol name).
     /// This is an unstable feature. Consider using --harness instead
-    #[arg(long, hide = true, requires("enable_unstable"), conflicts_with("dry_run"))]
+    #[arg(long, hide = true, requires("enable_unstable"))]
     pub function: Option<String>,
     /// Entry point for verification (proof harness)
-    // In a dry-run, we don't have kani-metadata.json to read, so we can't use this flag
-    #[arg(long, conflicts_with = "function", conflicts_with = "dry_run")]
+    #[arg(long, conflicts_with = "function")]
     pub harness: Option<String>,
 
     /// Link external C files referenced by Rust code.
@@ -448,6 +446,13 @@ impl KaniArgs {
             ));
         }
 
+        if self.dry_run {
+            return Err(Error::raw(
+                ErrorKind::ValueValidation,
+                "The `--dry-run` option is obsolete. Use --verbose instead.",
+            ));
+        }
+
         Ok(())
     }
 }
@@ -510,11 +515,11 @@ mod tests {
     }
 
     #[test]
-    fn check_dry_run_harness_conflicts() {
-        // harness needs metadata which we don't have with dry-run
-        let args = vec!["kani", "file.rs", "--dry-run", "--harness", "foo"];
-        let err = StandaloneArgs::try_parse_from(args).unwrap_err();
-        assert_eq!(err.kind(), ErrorKind::ArgumentConflict);
+    fn check_dry_run_fails() {
+        // We don't support --dry-run anymore but we print a friendly reminder for now.
+        let args = vec!["kani", "file.rs", "--dry-run"];
+        let err = StandaloneArgs::parse_from(&args).common_opts.validate_inner().unwrap_err();
+        assert_eq!(err.kind(), ErrorKind::ValueValidation);
     }
 
     #[test]

kani-driver/src/call_cargo.rs

@@ -121,15 +121,6 @@ impl KaniSession {
         if !found_target {
             bail!("No supported targets were found.");
         }
-        if self.args.dry_run {
-            // mock an answer: mostly the same except we don't/can't expand the globs
-            return Ok(CargoOutputs {
-                outdir: outdir.clone(),
-                symtabs: vec![outdir.join("*.symtab.json")],
-                metadata: vec![outdir.join("*.kani-metadata.json")],
-                restrictions: self.args.restrict_vtable().then_some(outdir),
-            });
-        }
 
         Ok(CargoOutputs {
             outdir: outdir.clone(),

kani-driver/src/harness_runner.rs

@@ -103,12 +103,8 @@ impl KaniSession {
             let result = self.run_cbmc(binary, harness)?;
 
             // When quiet, we don't want to print anything at all.
-            // When dry-run, we don't have real results to print.
             // When output is old, we also don't have real results to print.
-            if !self.args.quiet
-                && !self.args.dry_run
-                && self.args.output_format != OutputFormat::Old
-            {
+            if !self.args.quiet && self.args.output_format != OutputFormat::Old {
                 println!("{}", result.render(&self.args.output_format));
             }
 

kani-driver/src/metadata.rs

@@ -13,17 +13,6 @@ use std::io::{BufReader, BufWriter};
 
 use crate::session::KaniSession;
 
-fn generate_mock_harness() -> HarnessMetadata {
-    HarnessMetadata {
-        pretty_name: String::from("harness"),
-        mangled_name: String::from("harness"),
-        original_file: String::from("target_file.rs"),
-        original_start_line: 0,
-        original_end_line: 0,
-        unwind_value: None,
-    }
-}
-
 /// From either a file or a path with multiple files, output the CBMC restrictions file we should use.
 pub fn collect_and_link_function_pointer_restrictions(
     path: &Path,
@@ -127,19 +116,10 @@ fn merge_kani_metadata(files: Vec<KaniMetadata>) -> KaniMetadata {
 impl KaniSession {
     /// Reads a collection of kani-metadata.json files and merges the results.
     pub fn collect_kani_metadata(&self, files: &[PathBuf]) -> Result<KaniMetadata> {
-        if self.args.dry_run {
-            // Mock an answer
-            Ok(KaniMetadata {
-                proof_harnesses: vec![generate_mock_harness()],
-                unsupported_features: vec![],
-                test_harnesses: vec![],
-            })
-        } else {
-            // TODO: one possible future improvement here would be to return some kind of Lazy
-            // value, that only computes this metadata if it turns out we need it.
-            let results: Result<Vec<_>, _> = files.iter().map(|x| read_kani_metadata(x)).collect();
-            Ok(merge_kani_metadata(results?))
-        }
+        // TODO: one possible future improvement here would be to return some kind of Lazy
+        // value, that only computes this metadata if it turns out we need it.
+        let results: Result<Vec<_>, _> = files.iter().map(|x| read_kani_metadata(x)).collect();
+        Ok(merge_kani_metadata(results?))
     }
 
     /// Determine which function to use as entry point, based on command-line arguments and kani-metadata.

kani-driver/src/session.rs

@@ -95,7 +95,7 @@ pub enum ReachabilityMode {
 
 impl Drop for KaniSession {
     fn drop(&mut self) {
-        if !self.args.keep_temps && !self.args.dry_run {
+        if !self.args.keep_temps {
             let temporaries = self.temporaries.lock().unwrap();
 
             for file in temporaries.iter() {
@@ -108,7 +108,7 @@ impl Drop for KaniSession {
 
 impl KaniSession {
     // The below suite of helper functions for executing Commands are meant to be a common handler
-    // for various cmdline flags like 'dry-run' and 'quiet'. These functions are temporary: in the
+    // for various cmdline flags like 'verbose' and 'quiet'. These functions are temporary: in the
     // longer run we'll switch to a graph-interpreter style of constructing and executing jobs.
     // (In other words: higher-level data structures, rather than passing around Commands.)
     // (e.g. to support emitting Litani build graphs, or to better parallelize our work)
@@ -126,12 +126,8 @@ impl KaniSession {
             cmd.stdout(std::process::Stdio::null());
             cmd.stderr(std::process::Stdio::null());
         }
-        if self.args.verbose || self.args.dry_run {
-            println!("{}", render_command(&cmd).to_string_lossy());
-            if self.args.dry_run {
-                // Short circuit
-                return Ok(());
-            }
+        if self.args.verbose {
+            println!("[Kani] Running: `{}`", render_command(&cmd).to_string_lossy());
         }
         let result = cmd
             .status()
@@ -144,7 +140,7 @@ impl KaniSession {
 
     /// Run a job, but only output (unless --quiet) if it fails, and fail if there's a problem.
     pub fn run_suppress(&self, mut cmd: Command) -> Result<()> {
-        if self.args.quiet || self.args.debug || self.args.verbose || self.args.dry_run {
+        if self.args.quiet || self.args.debug || self.args.verbose {
             return self.run_terminal(cmd);
         }
         let result = cmd
@@ -165,12 +161,12 @@ impl KaniSession {
 
     /// Run a job, redirect its output to a file, and allow the caller to decide what to do with failure.
     pub fn run_redirect(&self, mut cmd: Command, stdout: &Path) -> Result<ExitStatus> {
-        if self.args.verbose || self.args.dry_run {
-            println!("{} > {}", render_command(&cmd).to_string_lossy(), stdout.display());
-            if self.args.dry_run {
-                // Short circuit. Difficult to mock an ExitStatus :(
-                return Ok(<ExitStatus as std::os::unix::prelude::ExitStatusExt>::from_raw(0));
-            }
+        if self.args.verbose {
+            println!(
+                "[Kani] Running: `{} > {}`",
+                render_command(&cmd).to_string_lossy(),
+                stdout.display()
+            );
         }
         let output_file = std::fs::File::create(&stdout)?;
         cmd.stdout(output_file);
@@ -184,11 +180,8 @@ impl KaniSession {
     /// NOTE: Unlike other `run_` functions, this function does not attempt to indicate
     /// the process exit code, you need to remember to check this yourself.
     pub fn run_piped(&self, mut cmd: Command) -> Result<Option<Child>> {
-        if self.args.verbose || self.args.dry_run {
-            println!("{}", render_command(&cmd).to_string_lossy());
-            if self.args.dry_run {
-                return Ok(None);
-            }
+        if self.args.verbose {
+            println!("[Kani] Running: `{}`", render_command(&cmd).to_string_lossy());
         }
         // Run the process as a child process
         let process = cmd

tests/cargo-ui/dry-run/expected

@@ -4,8 +4,9 @@
 name = "dry-run"
 version = "0.1.0"
 edition = "2021"
+description = "Check that --verbose include the commands ran by Kani"
 
 [dependencies]
 
 [package.metadata.kani]
-flags = { dry-run=true, enable-unstable=true }
+flags = { verbose=true }

tests/cargo-ui/dry-run/src/lib.rs

@@ -0,0 +1,7 @@
+KANIFLAGS=
+RUSTC=
+cargo rustc
+Running: `goto-cc
+Running: `goto-instrument
+Checking harness dummy_harness...
+Running: `cbmc

tests/cargo-ui/dry-run/Cargo.toml renamed to tests/cargo-ui/verbose-cmds/Cargo.toml

@@ -0,0 +1,9 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! The --verbose will print the commands executed by Kani before invoking them.
+
+#[kani::proof]
+pub fn dummy_harness() {
+    assert!(true);
+}

tests/cargo-ui/verbose-cmds/expected

@@ -0,0 +1,4 @@
+Running: `goto-cc
+Running: `goto-instrument
+Running: `cbmc
+VERIFICATION:- SUCCESSFUL

tests/cargo-ui/verbose-cmds/src/lib.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --verbose
+
+// `--verbose` causes Kani to print out commands before running them
+// In `expected` you will find substrings of these commands for easy maintenence.
+#[kani::proof]
+fn real_harness() {
+    assert_eq!(1 + 1, 2);
+}