Replace CBMC output parser (#1433)

model-checking · Aug 9, 2022 · bca694a · bca694a
1 parent cecd55f
commit bca694a
Show file tree

Hide file tree

Showing 16 changed files with 1,085 additions and 1,044 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -156,6 +156,20 @@ dependencies = [
  "walkdir",
 ]
 
+[[package]]
+name = "console"
+version = "0.15.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "89eab4d20ce20cea182308bca13088fecea9c05f6776cf287205d41a0ed3c847"
+dependencies = [
+ "encode_unicode",
+ "libc",
+ "once_cell",
+ "terminal_size",
+ "unicode-width",
+ "winapi",
+]
+
 [[package]]
 name = "cprover_bindings"
 version = "0.7.0"
@@ -185,6 +199,12 @@ version = "1.7.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3f107b87b6afc2a64fd13cac55fe06d6c8859f12d4b14cbcdd2c67d0976781be"
 
+[[package]]
+name = "encode_unicode"
+version = "0.3.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f"
+
 [[package]]
 name = "getopts"
 version = "0.2.21"
@@ -318,8 +338,12 @@ dependencies = [
  "anyhow",
  "cargo_metadata",
  "clap",
+ "console",
  "glob",
  "kani_metadata",
+ "once_cell",
+ "pathdiff",
+ "regex",
  "serde",
  "serde_json",
  "structopt",
@@ -549,6 +573,12 @@ dependencies = [
  "windows-sys",
 ]
 
+[[package]]
+name = "pathdiff"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8835116a5c179084a830efb3adc117ab007512b535bc1a21c991d3b32a6b44dd"
+
 [[package]]
 name = "pin-project-lite"
 version = "0.2.9"
@@ -831,6 +861,16 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "terminal_size"
+version = "0.1.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "633c1a546cee861a1a6d0dc69ebeca693bf4296661ba7852b9d21d159e0506df"
+dependencies = [
+ "libc",
+ "winapi",
+]
+
 [[package]]
 name = "textwrap"
 version = "0.11.0"

diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
@@ -15,12 +15,16 @@ publish = false
 kani_metadata = { path = "../kani_metadata" }
 cargo_metadata = "0.15.0"
 anyhow = "1"
+console = "0.15.1"
+once_cell = "1.13.0"
 serde = { version = "1", features = ["derive"] }
 serde_json = "1"
 structopt = "0.3"
 clap = "2.34"
 glob = "0.3"
 toml = "0.5"
+regex = "1.6"
+pathdiff = "0.2.1"
 
 # A good set of suggested dependencies can be found in rustup:
 # https://github.com/rust-lang/rustup/blob/master/Cargo.toml

diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
@@ -9,6 +9,7 @@ use std::process::Command;
 use std::time::Instant;
 
 use crate::args::KaniArgs;
+use crate::cbmc_output_parser::process_cbmc_output;
 use crate::session::KaniSession;
 
 #[derive(PartialEq, Eq)]
@@ -24,7 +25,7 @@ impl KaniSession {
 
         {
             let mut temps = self.temporaries.borrow_mut();
-            temps.push(output_filename.clone());
+            temps.push(output_filename);
         }
 
         let args: Vec<OsString> = self.cbmc_flags(file, harness)?;
@@ -33,32 +34,41 @@ impl KaniSession {
         let mut cmd = Command::new("cbmc");
         cmd.args(args);
 
-        if self.args.output_format == crate::args::OutputFormat::Old {
+        let now = Instant::now();
+
+        let verification_result = if self.args.output_format == crate::args::OutputFormat::Old {
             if self.run_terminal(cmd).is_err() {
-                return Ok(VerificationStatus::Failure);
+                Ok(VerificationStatus::Failure)
+            } else {
+                Ok(VerificationStatus::Success)
             }
         } else {
-            // extra argument
+            // Add extra argument to receive the output in JSON format.
+            // Done here because `--visualize` uses the XML format instead.
             cmd.arg("--json-ui");
 
-            let now = Instant::now();
-            let _cbmc_result = self.run_redirect(cmd, &output_filename)?;
-            let elapsed = now.elapsed().as_secs_f32();
-            let format_result = self.format_cbmc_output(&output_filename);
-
-            if format_result.is_err() {
-                // Because of things like --assertion-reach-checks and other future features,
-                // we now decide if we fail or not based solely on the output of the formatter.
-                return Ok(VerificationStatus::Failure);
-                // todo: this is imperfect, since we don't know why failure happened.
-                // the best possible fix is port to rust instead of using python, or getting more
-                // feedback than just exit status (or using a particular magic exit code?)
+            // Spawn the CBMC process and process its output below
+            let cbmc_process_opt = self.run_piped(cmd)?;
+            if let Some(cbmc_process) = cbmc_process_opt {
+                // The introduction of reachability checks forces us to decide
+                // the verification result based on the postprocessing of CBMC results.
+                let processed_result = process_cbmc_output(
+                    cbmc_process,
+                    self.args.extra_pointer_checks,
+                    &self.args.output_format,
+                );
+                Ok(processed_result)
+            } else {
+                Ok(VerificationStatus::Failure)
             }
-            // TODO: We should print this even the verification fails but not if it crashes.
+        };
+        // TODO: We should print this even the verification fails but not if it crashes.
+        if !self.args.dry_run {
+            let elapsed = now.elapsed().as_secs_f32();
             println!("Verification Time: {}s", elapsed);
         }
 
-        Ok(VerificationStatus::Success)
+        verification_result
     }
 
     /// used by call_cbmc_viewer, invokes different variants of CBMC.

diff --git a/kani-driver/src/call_display_results.rs b/kani-driver/src/call_display_results.rs