diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 4c0fe98cc65d..3cb4c9a1c98e 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -129,19 +129,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`. @@ -315,9 +307,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 @@ -532,18 +524,6 @@ impl ValidateArgs for VerificationArgs { ); } - 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"); - } - } - if self.mir_linker { print_obsolete(&self.common_args, "--mir-linker"); } diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs index 81d50865cc13..e71246af7ce4 100644 --- a/kani-driver/src/call_cbmc.rs +++ b/kani-driver/src/call_cbmc.rs @@ -75,7 +75,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"); // Spawn the CBMC process and process its output below @@ -138,10 +139,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 992e226e45db..fdc795f457b5 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -52,8 +52,6 @@ impl<'sess, 'pr> HarnessRunner<'sess, '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(); @@ -63,7 +61,7 @@ impl<'sess, 'pr> HarnessRunner<'sess, '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::>>() @@ -105,35 +103,28 @@ 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")?; - // When quiet, we don't want to print anything at all. - // When output is old, we also don't have real results to print. - if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old { - println!( - "{}", - result.render( - &self.args.output_format, - harness.attributes.should_panic, - self.args.coverage - ) - ); - } - self.gen_and_add_concrete_playback(harness, &mut result)?; - Ok(result) + // When quiet, we don't want to print anything at all. + // When output is old, we also don't have real results to print. + if !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old { + println!( + "{}", + result.render( + &self.args.output_format, + harness.attributes.should_panic, + self.args.coverage + ) + ); } + 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 @@ -159,7 +150,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 3bb38ed1294c..80c727de497d 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -22,7 +22,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 2bc0845cdb46..4663c80356b8 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 collection of artifacts kept as part of this project. artifacts: Vec, 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/tests/perf/s2n-quic b/tests/perf/s2n-quic index 37335c196fb5..59ef366af76e 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 37335c196fb5755dcbe2532e5a3820e46906d5ea +Subproject commit 59ef366af76edfb4f89bd39137865db2a1ad041d