Remove CBMC viewer and visualize option (#3699)

This builds upon @jaisnan's changes in #3302. The PR removes the `--visualize` option and the CBMC viewer from the Kani installation and CI. There is still some room for clean-up, specifically with the python dependency. This can be handled in a separate PR. 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: Jaisurya Nanduri <[email protected]>
model-checking · Nov 8, 2024 · 26c078e · 26c078e
1 parent 8400296
commit 26c078e
Show file tree

Hide file tree

Showing 28 changed files with 21 additions and 381 deletions.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -272,7 +272,7 @@ jobs:
       - name: Run tests
         # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests.
         run: |
-          for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
+          for dir in simple-lib build-rs-works simple-kissat; do
             >&2 echo "Running test $dir"
             pushd tests/cargo-kani/$dir
             cargo kani
@@ -312,7 +312,7 @@ jobs:
 
       - name: Run installed tests
         run: |
-          for dir in simple-lib simple-visualize build-rs-works simple-kissat; do
+          for dir in simple-lib build-rs-works simple-kissat; do
             >&2 echo "Running test $dir"
             docker run -v /var/run/docker.sock:/var/run/docker.sock \
               -w /tmp/kani/tests/cargo-kani/$dir kani-18-04 cargo kani

diff --git a/docs/src/build-from-source.md b/docs/src/build-from-source.md
@@ -12,8 +12,7 @@ In general, the following dependencies are required to build Kani from source.
 
 1. Cargo installed via [rustup](https://rustup.rs/)
 2. [CBMC](https://github.com/diffblue/cbmc) (latest release)
-3. [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc) (latest release)
-4. [Kissat](https://github.com/arminbiere/kissat) (Release 3.1.1)
+3. [Kissat](https://github.com/arminbiere/kissat) (Release 3.1.1)
 
 Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms.
 

diff --git a/docs/src/install-guide.md b/docs/src/install-guide.md
@@ -16,7 +16,6 @@ The following must already be installed:
 
 * **Python version 3.7 or newer** and the package installer `pip`.
 * Rust 1.58 or newer installed via `rustup`.
-* `ctags` is required for Kani's `--visualize` option to work correctly. [Universal ctags](https://ctags.io/) is recommended.
 
 ## Installing the latest version
 

diff --git a/docs/src/usage.md b/docs/src/usage.md
@@ -28,8 +28,6 @@ Common to both `kani` and `cargo kani` are many command-line flags:
  If used with `print`, Kani will only print the unit test to stdout.
  If used with `inplace`, Kani will automatically add the unit test to the user's source code, next to the proof harness. For more detailed instructions, see the [concrete playback](./experimental/concrete-playback.md) section.
 
- * `--visualize`: _Experimental_, `--enable-unstable` feature that generates an HTML report providing traces (i.e., counterexamples) for each failure found by Kani.
-
  * `--tests`: Build in "[test mode](https://doc.rust-lang.org/rustc/tests/index.html)", i.e. with `cfg(test)` set and `dev-dependencies` available (when using `cargo kani`).
 
  * `--harness <name>`: By default, Kani checks all proof harnesses it finds.

diff --git a/kani-dependencies b/kani-dependencies
@@ -2,9 +2,4 @@ CBMC_MAJOR="6"
 CBMC_MINOR="4"
 CBMC_VERSION="6.4.0"
 
-# If you update this version number, remember to bump it in `src/setup.rs` too
-CBMC_VIEWER_MAJOR="3"
-CBMC_VIEWER_MINOR="10"
-CBMC_VIEWER_VERSION="3.10"
-
 KISSAT_VERSION="3.1.1"
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
@@ -184,19 +184,11 @@ pub struct VerificationArgs {
     #[arg(long, hide = true, requires("enable_unstable"))]
     pub assess: bool,
 
-    /// Generate visualizer report to `<target-dir>/report/html/index.html`
-    #[arg(long)]
-    pub visualize: bool,
     /// Generate concrete playback unit test.
     /// If value supplied is 'print', Kani prints the unit test to stdout.
     /// If value supplied is 'inplace', Kani automatically adds the unit test to your source code.
     /// This option does not work with `--output-format old`.
-    #[arg(
-        long,
-        conflicts_with_all(&["visualize"]),
-        ignore_case = true,
-        value_enum
-    )]
+    #[arg(long, ignore_case = true, value_enum)]
     pub concrete_playback: Option<ConcretePlaybackMode>,
     /// Keep temporary files generated throughout Kani process. This is already the default
     /// behavior for `cargo-kani`.
@@ -355,9 +347,9 @@ impl VerificationArgs {
         // if we flip the default, this will become: !self.no_restrict_vtable
     }
 
-    /// Assertion reachability checks should be disabled when running with --visualize
+    /// Assertion reachability checks should be disabled
     pub fn assertion_reach_checks(&self) -> bool {
-        !self.no_assertion_reach_checks && !self.visualize
+        !self.no_assertion_reach_checks
     }
 
     /// Suppress our default value, if the user has supplied it explicitly in --cbmc-args
@@ -577,18 +569,6 @@ impl ValidateArgs for VerificationArgs {
             print_obsolete(&self.common_args, "--write-json-symtab");
         }
 
-        if self.visualize {
-            if !self.common_args.enable_unstable {
-                return Err(Error::raw(
-                    ErrorKind::MissingRequiredArgument,
-                    "Missing argument: --visualize now requires --enable-unstable
-                    due to open issues involving incorrect results.",
-                ));
-            } else {
-                print_deprecated(&self.common_args, "--visualize", "--concrete-playback");
-            }
-        }
-
         // TODO: these conflicting flags reflect what's necessary to pass current tests unmodified.
         // We should consider improving the error messages slightly in a later pull request.
         if natives_unwind && extra_unwind {

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
@@ -10,7 +10,6 @@ use std::collections::btree_map::Entry;
 use std::ffi::OsString;
 use std::fmt::Write;
 use std::path::Path;
-use std::process::Command;
 use std::sync::OnceLock;
 use std::time::{Duration, Instant};
 use tokio::process::Command as TokioCommand;
@@ -94,7 +93,8 @@ impl KaniSession {
             }
         } else {
             // Add extra argument to receive the output in JSON format.
-            // Done here because `--visualize` uses the XML format instead.
+            // Done here because now removed `--visualize` used the XML format instead.
+            // TODO: move this now that we don't use --visualize
             cmd.arg("--json-ui");
 
             self.runtime.block_on(self.run_cbmc_piped(cmd, harness))?
@@ -167,23 +167,6 @@ impl KaniSession {
         Ok(verification_results)
     }
 
-    /// used by call_cbmc_viewer, invokes different variants of CBMC.
-    // TODO: this could use some cleanup and refactoring.
-    pub fn call_cbmc(&self, args: Vec<OsString>, output: &Path) -> Result<()> {
-        // TODO get cbmc path from self
-        let mut cmd = Command::new("cbmc");
-        cmd.args(args);
-
-        let result = self.run_redirect(cmd, output)?;
-
-        if !result.success() {
-            bail!("cbmc exited with status {}", result);
-        }
-        // TODO: We 'bail' above, but then ignore it in 'call_cbmc_viewer' ...
-
-        Ok(())
-    }
-
     /// "Internal," but also used by call_cbmc_viewer
     pub fn cbmc_flags(
         &self,
@@ -209,10 +192,7 @@ impl KaniSession {
             args.push("--validate-ssa-equation".into());
         }
 
-        if !self.args.visualize
-            && self.args.concrete_playback.is_none()
-            && !self.args.no_slice_formula
-        {
+        if self.args.concrete_playback.is_none() && !self.args.no_slice_formula {
             args.push("--slice-formula".into());
         }
 

diff --git a/kani-driver/src/call_cbmc_viewer.rs b/kani-driver/src/call_cbmc_viewer.rs
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
@@ -56,8 +56,6 @@ impl<'pr> HarnessRunner<'_, 'pr> {
             sorted_harnesses
                 .par_iter()
                 .map(|harness| -> Result<HarnessResult<'pr>> {
-                    let harness_filename = harness.pretty_name.replace("::", "-");
-                    let report_dir = self.project.outdir.join(format!("report-{harness_filename}"));
                     let goto_file =
                         self.project.get_harness_artifact(&harness, ArtifactType::Goto).unwrap();
 
@@ -67,7 +65,7 @@ impl<'pr> HarnessRunner<'_, 'pr> {
                         self.sess.synthesize_loop_contracts(goto_file, &goto_file, &harness)?;
                     }
 
-                    let result = self.sess.check_harness(goto_file, &report_dir, harness)?;
+                    let result = self.sess.check_harness(goto_file, harness)?;
                     Ok(HarnessResult { harness, result })
                 })
                 .collect::<Result<Vec<_>>>()
@@ -148,24 +146,17 @@ impl KaniSession {
     pub(crate) fn check_harness(
         &self,
         binary: &Path,
-        report_dir: &Path,
         harness: &HarnessMetadata,
     ) -> Result<VerificationResult> {
         if !self.args.common_args.quiet {
             println!("Checking harness {}...", harness.pretty_name);
         }
 
-        if self.args.visualize {
-            self.run_visualize(binary, report_dir, harness)?;
-            // Strictly speaking, we're faking success here. This is more "no error"
-            Ok(VerificationResult::mock_success())
-        } else {
-            let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
+        let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
 
-            self.process_output(&result, harness);
-            self.gen_and_add_concrete_playback(harness, &mut result)?;
-            Ok(result)
-        }
+        self.process_output(&result, harness);
+        self.gen_and_add_concrete_playback(harness, &mut result)?;
+        Ok(result)
     }
 
     /// Concludes a session by printing a summary report and exiting the process with an
@@ -191,7 +182,7 @@ impl KaniSession {
         }
 
         // We currently omit a summary if there was just 1 harness
-        if !self.args.common_args.quiet && !self.args.visualize {
+        if !self.args.common_args.quiet {
             if failing > 0 {
                 println!("Summary:");
             }

diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
@@ -24,7 +24,6 @@ mod args_toml;
 mod assess;
 mod call_cargo;
 mod call_cbmc;
-mod call_cbmc_viewer;
 mod call_goto_cc;
 mod call_goto_instrument;
 mod call_goto_synthesizer;

diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
@@ -32,6 +32,8 @@ pub struct Project {
     pub metadata: Vec<KaniMetadata>,
     /// The directory where all outputs should be directed to. This path represents the canonical
     /// version of outdir.
+    /// NOTE: This needs to be marked as dead_code even when it's clearly not
+    #[allow(dead_code)]
     pub outdir: PathBuf,
     /// The path to the input file the project was built from.
     /// Note that it will only be `Some(...)` if this was built from a standalone project.

diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
@@ -9,7 +9,7 @@ use anyhow::{Context, Result, bail};
 use std::io::IsTerminal;
 use std::io::Write;
 use std::path::{Path, PathBuf};
-use std::process::{Child, Command, ExitStatus, Stdio};
+use std::process::{Child, Command, Stdio};
 use std::sync::Mutex;
 use std::time::Instant;
 use strum_macros::Display;
@@ -134,11 +134,6 @@ impl KaniSession {
         run_suppress(&self.args.common_args, cmd)
     }
 
-    /// Call [run_redirect] with the verbosity configured by the user.
-    pub fn run_redirect(&self, cmd: Command, stdout: &Path) -> Result<ExitStatus> {
-        run_redirect(&self.args.common_args, cmd, stdout)
-    }
-
     /// Call [run_piped] with the verbosity configured by the user.
     pub fn run_piped(&self, cmd: Command) -> Result<Child> {
         run_piped(&self.args.common_args, cmd)
@@ -164,7 +159,6 @@ impl KaniSession {
 //               Default  Quiet  Verbose   Default  Quiet  Verbose
 // run_terminal  Y        N      Y         Y        N      Y         (inherits terminal)
 // run_suppress  N        N      Y         Y        N      Y         (buffered text only)
-// run_redirect  (not applicable, always to the file)                (only option where error is acceptable)
 
 /// Run a job, leave it outputting to terminal (unless --quiet), and fail if there's a problem.
 pub fn run_terminal(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()> {
@@ -254,33 +248,6 @@ pub fn run_suppress(verbosity: &impl Verbosity, mut cmd: Command) -> Result<()>
     Ok(())
 }
 
-/// Run a job, redirect its output to a file, and allow the caller to decide what to do with failure.
-pub fn run_redirect(
-    verbosity: &impl Verbosity,
-    mut cmd: Command,
-    stdout: &Path,
-) -> Result<ExitStatus> {
-    if verbosity.verbose() {
-        println!(
-            "[Kani] Running: `{} > {}`",
-            render_command(&cmd).to_string_lossy(),
-            stdout.display()
-        );
-    }
-    let output_file = std::fs::File::create(stdout)?;
-    cmd.stdout(output_file);
-
-    let program = cmd.get_program().to_string_lossy().to_string();
-    with_timer(
-        verbosity,
-        || {
-            cmd.status()
-                .context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))
-        },
-        &program,
-    )
-}
-
 /// Run a job and pipe its output to this process.
 /// Returns an error if the process could not be spawned.
 ///