From 26c078e097025499baf6e360210a21989d3605e0 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Fri, 8 Nov 2024 15:56:03 -0800 Subject: [PATCH] Remove CBMC viewer and visualize option (#3699) This builds upon @jaisnan's changes in https://github.com/model-checking/kani/pull/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 --- .github/workflows/release.yml | 4 +- docs/src/build-from-source.md | 3 +- docs/src/install-guide.md | 1 - docs/src/usage.md | 2 - kani-dependencies | 5 - kani-driver/src/args/mod.rs | 26 +---- kani-driver/src/call_cbmc.rs | 26 +---- kani-driver/src/call_cbmc_viewer.rs | 97 ------------------- kani-driver/src/harness_runner.rs | 21 ++-- kani-driver/src/main.rs | 1 - kani-driver/src/project.rs | 2 + kani-driver/src/session.rs | 35 +------ scripts/check-cbmc-viewer-version.py | 56 ----------- scripts/kani-regression.sh | 3 - scripts/setup/al2/install_deps.sh | 1 - scripts/setup/al2/install_viewer.sh | 19 ---- scripts/setup/macos/install_deps.sh | 1 - scripts/setup/macos/install_viewer.sh | 25 ----- scripts/setup/ubuntu/install_deps.sh | 1 - scripts/setup/ubuntu/install_viewer.sh | 19 ---- src/lib.rs | 2 +- src/setup.rs | 19 ---- tests/cargo-kani/rectangle-example/README.md | 7 +- tests/cargo-kani/simple-visualize/Cargo.toml | 13 --- .../cargo-kani/simple-visualize/main.expected | 2 - tests/cargo-kani/simple-visualize/src/main.rs | 6 -- tools/build-kani/license-notes.txt | 3 - tools/build-kani/src/main.rs | 2 - 28 files changed, 21 insertions(+), 381 deletions(-) delete mode 100644 kani-driver/src/call_cbmc_viewer.rs delete mode 100755 scripts/check-cbmc-viewer-version.py delete mode 100755 scripts/setup/al2/install_viewer.sh delete mode 100755 scripts/setup/macos/install_viewer.sh delete mode 100755 scripts/setup/ubuntu/install_viewer.sh delete mode 100644 tests/cargo-kani/simple-visualize/Cargo.toml delete mode 100644 tests/cargo-kani/simple-visualize/main.expected delete mode 100644 tests/cargo-kani/simple-visualize/src/main.rs diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index ad2e339f19e1..36aee463061a 100644 --- 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 index 01860f5f37e4..253fcf351073 100644 --- 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 index 776209987ba1..d64ad3c89ce0 100644 --- 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 index aaa5d3fa234c..60592aa56c9a 100644 --- 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 `: By default, Kani checks all proof harnesses it finds. diff --git a/kani-dependencies b/kani-dependencies index ac6b353733a2..1f4428827e4e 100644 --- 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 index a46e71b7c5dc..2be3ff58f2fc 100644 --- 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 `/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, /// 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 index 670a81f9d665..4e10cb98c650 100644 --- 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, 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 deleted file mode 100644 index 41c6247ee121..000000000000 --- a/kani-driver/src/call_cbmc_viewer.rs +++ /dev/null @@ -1,97 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -use anyhow::Result; -use kani_metadata::HarnessMetadata; -use std::ffi::OsString; -use std::path::Path; -use std::process::Command; - -use crate::session::KaniSession; -use crate::util::{alter_extension, warning}; - -impl KaniSession { - /// Run CBMC appropriately to produce 3 output XML files, then run cbmc-viewer on them to produce a report. - /// Viewer doesn't give different error codes depending on verification failure, so as long as it works, we report success. - pub fn run_visualize( - &self, - file: &Path, - report_dir: &Path, - harness_metadata: &HarnessMetadata, - ) -> Result<()> { - let results_filename = alter_extension(file, "results.xml"); - let property_filename = alter_extension(file, "property.xml"); - - self.record_temporary_file(&results_filename); - self.record_temporary_file(&property_filename); - - self.cbmc_variant(file, &["--xml-ui", "--trace"], &results_filename, harness_metadata)?; - self.cbmc_variant( - file, - &["--xml-ui", "--show-properties"], - &property_filename, - harness_metadata, - )?; - - let args: Vec = vec![ - "--result".into(), - results_filename.into(), - "--property".into(), - property_filename.into(), - "--srcdir".into(), - ".".into(), // os.path.realpath(srcdir), - "--wkdir".into(), - ".".into(), // os.path.realpath(wkdir), - "--goto".into(), - file.into(), - "--reportdir".into(), - report_dir.into(), - ]; - - // TODO get cbmc-viewer path from self - let mut cmd = Command::new("cbmc-viewer"); - cmd.args(args); - - self.run_suppress(cmd)?; - - // Let the user know - if !self.args.common_args.quiet { - println!("Report written to: {}/html/index.html", report_dir.to_string_lossy()); - warning("coverage information has been disabled for `--visualize` reports"); - // If using VS Code with Remote-SSH, suggest an option for remote viewing: - if std::env::var("VSCODE_IPC_HOOK_CLI").is_ok() - && std::env::var("SSH_CONNECTION").is_ok() - { - println!( - "VS Code automatically forwards ports for locally hosted servers. To view the report remotely,\nTry: python3 -m http.server --directory {}/html", - report_dir.to_string_lossy() - ); - } - } - - Ok(()) - } - - fn cbmc_variant( - &self, - file: &Path, - extra_args: &[&str], - output: &Path, - harness: &HarnessMetadata, - ) -> Result<()> { - let mut args = self.cbmc_flags(file, harness)?; - args.extend(extra_args.iter().map(|x| x.into())); - - // TODO fix this hack, abstractions are wrong - if extra_args.contains(&"--cover") { - if let Some(i) = args.iter().position(|x| x == "--unwinding-assertions") { - args.remove(i); - } - } - - // Expect and allow failures... maybe we should do better here somehow - let _result = self.call_cbmc(args, output); - - Ok(()) - } -} diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index f34e150efbad..ee14992cba78 100644 --- 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> { - 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::>>() @@ -148,24 +146,17 @@ impl KaniSession { pub(crate) fn check_harness( &self, binary: &Path, - report_dir: &Path, harness: &HarnessMetadata, ) -> Result { 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 index 88f92b3a70f6..b0fa22334da0 100644 --- 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 index 363050958d61..0af517ca84bc 100644 --- a/kani-driver/src/project.rs +++ b/kani-driver/src/project.rs @@ -32,6 +32,8 @@ pub struct Project { pub metadata: Vec, /// 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 index 2cf394184b4d..187a17ae6981 100644 --- 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 { - 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 { 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 { - 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. /// diff --git a/scripts/check-cbmc-viewer-version.py b/scripts/check-cbmc-viewer-version.py deleted file mode 100755 index 88c0f7ed31cb..000000000000 --- a/scripts/check-cbmc-viewer-version.py +++ /dev/null @@ -1,56 +0,0 @@ -#!/usr/bin/env python3 -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -import argparse -import re -import sys -import subprocess -from subprocess import PIPE - - -EXIT_CODE_SUCCESS = 0 -EXIT_CODE_MISMATCH = 1 -EXIT_CODE_FAIL = 2 - - -def cbmc_viewer_version(): - cmd = ["cbmc-viewer", "--version"] - try: - version = subprocess.run(cmd, stdout=PIPE, stderr=PIPE, check=True, - universal_newlines=True) - except (OSError, subprocess.SubprocessError) as error: - print(error) - print(f"Can't run command '{' '.join(cmd)}'") - sys.exit(EXIT_CODE_FAIL) - - match = re.match("CBMC viewer ([0-9]+).([0-9]+)", version.stdout) - if not match: - print(f"Can't parse CBMC-viewer version string: '{version.stdout.strip()}'") - sys.exit(EXIT_CODE_FAIL) - - return match.groups() - -def complete_version(*version): - numbers = [int(num) if num else 0 for num in version] - return (numbers + [0, 0])[:2] - -def main(): - parser = argparse.ArgumentParser( - description='Check CBMC-viewer version matches major/minor') - parser.add_argument('--major', required=True) - parser.add_argument('--minor', required=True) - args = parser.parse_args() - - current_version = complete_version(*cbmc_viewer_version()) - desired_version = complete_version(args.major, args.minor) - - if desired_version > current_version: - version_string = '.'.join([str(num) for num in current_version]) - desired_version_string = '.'.join([str(num) for num in desired_version]) - print(f'ERROR: CBMC-viewer version is {version_string}, expected at least {desired_version_string}') - sys.exit(EXIT_CODE_MISMATCH) - - -if __name__ == "__main__": - main() diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh index 728129d784b6..88215bdf0317 100755 --- 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 index ce901ab8afa5..648715e9b055 100755 --- 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 deleted file mode 100755 index c8ba7b7b838e..000000000000 --- a/scripts/setup/al2/install_viewer.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/bin/bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eu - -# Install cbmc-viewer - -# Source kani-dependencies to get CBMC_VIEWER_VERSION -source kani-dependencies - -if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then - echo "$0: Error: CBMC_VIEWER_VERSION is not specified" - exit 1 -fi - -set -x - -python3 -m pip install cbmc-viewer==$CBMC_VIEWER_VERSION diff --git a/scripts/setup/macos/install_deps.sh b/scripts/setup/macos/install_deps.sh index 179bf8c1237f..112e34680b11 100755 --- 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 deleted file mode 100755 index b55eca370d82..000000000000 --- a/scripts/setup/macos/install_viewer.sh +++ /dev/null @@ -1,25 +0,0 @@ -#!/bin/bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eu - -# Install cbmc-viewer - -# Source kani-dependencies to get CBMC_VIEWER_VERSION -source kani-dependencies - -if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then - echo "$0: Error: CBMC_VIEWER_VERSION is not specified" - exit 1 -fi - -set -x - -# brew doesn't recognize specific versions of viewer -# Build from source, since there's only a macos-12 bottle which doesn't seem to work. -# Install Python 3.12 first while ignoring errors: the system may provide this -# version, which will hinder brew from installing symlinks -brew install python@3.12 || true -brew install -s aws/tap/cbmc-viewer -echo "Installed: $(cbmc-viewer --version)" diff --git a/scripts/setup/ubuntu/install_deps.sh b/scripts/setup/ubuntu/install_deps.sh index b93602691222..2633607744c5 100755 --- 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 deleted file mode 100755 index c8ba7b7b838e..000000000000 --- a/scripts/setup/ubuntu/install_viewer.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/bin/bash -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT - -set -eu - -# Install cbmc-viewer - -# Source kani-dependencies to get CBMC_VIEWER_VERSION -source kani-dependencies - -if [ -z "${CBMC_VIEWER_VERSION:-}" ]; then - echo "$0: Error: CBMC_VIEWER_VERSION is not specified" - exit 1 -fi - -set -x - -python3 -m pip install cbmc-viewer==$CBMC_VIEWER_VERSION diff --git a/src/lib.rs b/src/lib.rs index f24163d3213c..5b79ec504d4c 100644 --- 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 index 0901de9a8b00..96daf82e4a27 100644 --- 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) 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 index b07c61a96c9c..b16c1d464881 100644 --- 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/tests/cargo-kani/simple-visualize/Cargo.toml b/tests/cargo-kani/simple-visualize/Cargo.toml deleted file mode 100644 index 24f2576ca69f..000000000000 --- a/tests/cargo-kani/simple-visualize/Cargo.toml +++ /dev/null @@ -1,13 +0,0 @@ -# Copyright Kani Contributors -# SPDX-License-Identifier: Apache-2.0 OR MIT -[package] -name = "simple-visualize" -version = "0.1.0" -edition = "2018" - -[dependencies] - -[workspace] - -[package.metadata.kani] -flags = {enable-unstable = true, visualize = true} diff --git a/tests/cargo-kani/simple-visualize/main.expected b/tests/cargo-kani/simple-visualize/main.expected deleted file mode 100644 index 1d0839175310..000000000000 --- a/tests/cargo-kani/simple-visualize/main.expected +++ /dev/null @@ -1,2 +0,0 @@ -warning: The `--visualize` option is deprecated. This option will be removed soon. Consider using `--concrete-playback` instead -report-main/html/index.html diff --git a/tests/cargo-kani/simple-visualize/src/main.rs b/tests/cargo-kani/simple-visualize/src/main.rs deleted file mode 100644 index 390a15b9c89d..000000000000 --- a/tests/cargo-kani/simple-visualize/src/main.rs +++ /dev/null @@ -1,6 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -#[kani::proof] -fn main() { - assert!(1 == 2); -} diff --git a/tools/build-kani/license-notes.txt b/tools/build-kani/license-notes.txt index 6e717c98012b..04070480ccd0 100644 --- 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 index 8f36f4598e88..c45e9a72b189 100644 --- 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(())