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 <jaisnan@amazon.com>

Author: zhassan-aws

.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

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.
 

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
 

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.

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"

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 {

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());
         }
 

kani-driver/src/call_cbmc_viewer.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:");
             }

kani-driver/src/harness_runner.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;