More cleanup

zhassan-aws · zhassan-aws · commit 207dabd6e6d0 · 2024-11-08T14:48:13.000-08:00
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/scripts/check-cbmc-viewer-version.py b/scripts/check-cbmc-viewer-version.py
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
@@ -23,11 +23,8 @@ source "${KANI_DIR}/kani-dependencies"
 # Sanity check dependencies values.
 [[ "${CBMC_MAJOR}.${CBMC_MINOR}" == "${CBMC_VERSION%.*}" ]] || \
     (echo "Conflicting CBMC versions"; exit 1)
-[[ "${CBMC_VIEWER_MAJOR}.${CBMC_VIEWER_MINOR}" == "${CBMC_VIEWER_VERSION}" ]] || \
-    (echo "Conflicting CBMC viewer versions"; exit 1)
 # Check if installed versions are correct.
 check-cbmc-version.py --major ${CBMC_MAJOR} --minor ${CBMC_MINOR}
-check-cbmc-viewer-version.py --major ${CBMC_VIEWER_MAJOR} --minor ${CBMC_VIEWER_MINOR}
 check_kissat_version.sh
 
 # Formatting check
diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh
@@ -31,7 +31,6 @@ python3 -m pip install autopep8
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 
 ${SCRIPT_DIR}/install_cbmc.sh
-${SCRIPT_DIR}/install_viewer.sh
 # The Kissat installation script is platform-independent, so is placed one level up
 ${SCRIPT_DIR}/../install_kissat.sh
 ${SCRIPT_DIR}/../install_rustup.sh
diff --git a/scripts/setup/al2/install_viewer.sh b/scripts/setup/al2/install_viewer.sh
diff --git a/scripts/setup/macos/install_deps.sh b/scripts/setup/macos/install_deps.sh
@@ -21,6 +21,5 @@ brew install universal-ctags wget jq
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 
 ${SCRIPT_DIR}/install_cbmc.sh
-${SCRIPT_DIR}/install_viewer.sh
 # The Kissat installation script is platform-independent, so is placed one level up
 ${SCRIPT_DIR}/../install_kissat.sh
diff --git a/scripts/setup/macos/install_viewer.sh b/scripts/setup/macos/install_viewer.sh
diff --git a/scripts/setup/ubuntu/install_deps.sh b/scripts/setup/ubuntu/install_deps.sh
@@ -57,6 +57,5 @@ fi
 SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
 
 ${SCRIPT_DIR}/install_cbmc.sh
-${SCRIPT_DIR}/install_viewer.sh
 # The Kissat installation script is platform-independent, so is placed one level up
 ${SCRIPT_DIR}/../install_kissat.sh
diff --git a/scripts/setup/ubuntu/install_viewer.sh b/scripts/setup/ubuntu/install_viewer.sh
diff --git a/src/lib.rs b/src/lib.rs
@@ -140,7 +140,7 @@ fn exec(bin: &str) -> Result<()> {
 
     // Allow python scripts to find dependencies under our pyroot
     let pythonpath = prepend_search_path(&[pyroot], env::var_os("PYTHONPATH"))?;
-    // Add: kani, cbmc, viewer (pyroot), and our rust toolchain directly to our PATH
+    // Add: kani, cbmc, and our rust toolchain directly to our PATH
     let path = prepend_search_path(&[bin_kani, bin_pyroot], env::var_os("PATH"))?;
 
     // Ensure our environment variables for linker search paths won't cause failures, before we execute:
diff --git a/src/setup.rs b/src/setup.rs
@@ -86,8 +86,6 @@ pub fn setup(
 
     setup_rust_toolchain(&kani_dir, use_local_toolchain)?;
 
-    setup_python_deps(&kani_dir)?;
-
     os_hacks::setup_os_hacks(&kani_dir, &os)?;
 
     println!("[5/5] Successfully completed Kani first-time setup.");
@@ -183,23 +181,6 @@ fn setup_rust_toolchain(kani_dir: &Path, use_local_toolchain: Option<OsString>)
     Ok(toolchain_version)
 }
 
-/// Install into the pyroot the python dependencies we need
-fn setup_python_deps(kani_dir: &Path) -> Result<()> {
-    println!("[4/5] Installing Kani python dependencies...");
-    let pyroot = kani_dir.join("pyroot");
-
-    // TODO: this is a repetition of versions from kani/kani-dependencies
-    let pkg_versions = &["cbmc-viewer==3.10"];
-
-    Command::new("python3")
-        .args(["-m", "pip", "install", "--target"])
-        .arg(&pyroot)
-        .args(pkg_versions)
-        .run()?;
-
-    Ok(())
-}
-
 // This ends the setup steps above.
 //
 // Just putting a bit of space between that and the helper functions below.
diff --git a/tests/cargo-kani/rectangle-example/README.md b/tests/cargo-kani/rectangle-example/README.md
@@ -31,17 +31,14 @@ $ cargo kani --harness stretched_rectangle_can_hold_original --output-format ter
 VERIFICATION:- FAILED
 ```
 
-In order to view a trace (a step-by-step execution of the program) use the `--visualize` flag:
+In order to view a counterexample use the `--concrete-playback` flag:
 
 ```bash
-$ cargo kani --harness stretched_rectangle_can_hold_original --output-format terse --visualize
+$ cargo kani --harness stretched_rectangle_can_hold_original --output-format terse -Zconcrete-playback --concrete-playback=print
 # --snip--
 VERIFICATION:- FAILED
-# and generates a html report in target/report/html/index.html
 ```
 
-And open the report in a browser.
-
 After fixing the problem we can re-run Kani (on the proof harness `stretched_rectangle_can_hold_original_fixed`). This time we expect verification success:
 
 ```bash
diff --git a/tools/build-kani/license-notes.txt b/tools/build-kani/license-notes.txt
@@ -17,9 +17,6 @@ Acknowledgement:
      Computer Science Department, University of Oxford
      Computer Science Department, Carnegie Mellon University
 
-cbmc-viewer: https://github.com/model-checking/cbmc-viewer
-License: Apache-2.0
-
 ## Notable Python dependencies
 
 voluptuous: https://github.com/alecthomas/voluptuous
diff --git a/tools/build-kani/src/main.rs b/tools/build-kani/src/main.rs
@@ -43,7 +43,6 @@ fn main() -> Result<()> {
             bundle_kani(dir)?;
             bundle_cbmc(dir)?;
             bundle_kissat(dir)?;
-            // cbmc-viewer isn't bundled, it's pip install'd on first-time setup
 
             create_release_bundle(dir, &bundle_name)?;
 
@@ -140,7 +139,6 @@ fn bundle_cbmc(dir: &Path) -> Result<()> {
     cp(&which::which("goto-instrument")?, &bin)?;
     cp(&which::which("goto-cc")?, &bin)?;
     cp(&which::which("symtab2gb")?, &bin)?;
-    // cbmc-viewer invokes this
     cp(&which::which("goto-analyzer")?, &bin)?;
 
     Ok(())
