Add live streaming JSON output from CBMC to prevent Kani output hang

kani-driver/src/args.rs

@@ -148,13 +148,20 @@ pub struct KaniArgs {
     /// This option may impact the soundness of the analysis and may cause false proofs and/or counterexamples
     #[structopt(long, hidden_short_help(true), requires("enable-unstable"))]
     pub ignore_global_asm: bool,
+
+    /// This flag turns on streaming output as opposed to caching cbmc output.
+    /// This is an experimental feature and requires `--enable-unstable` to be used
+    /// TODO: Use the flag for non termination issue
+    /// https://github.com/model-checking/kani/issues/493
+    #[structopt(long, hidden = true, requires("enable-unstable"))]
+    pub use_piped_output: bool,
     /*
     The below is a "TODO list" of things not yet implemented from the kani_flags.py script.
 
         add_flag(group, "--gen-c-runnable", default=False, action=BooleanOptionalAction,
-                 help="Generate C file equivalent to inputted program; "
-                      "performs additional processing to produce valid C code "
-                      "at the cost of some readability")
+                help="Generate C file equivalent to inputted program; "
+                    "performs additional processing to produce valid C code "
+                    "at the cost of some readability")
         */
 }
 

kani-driver/src/call_cbmc.rs

@@ -42,18 +42,30 @@ impl KaniSession {
             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?)
+            // Check cbmc output flag and extract cbmc output either as a live stream or in a cache
+            if self.args.use_piped_output {
+                // Use streaming output from CBMC
+                let format_result_live = self.run_piped(cmd);
+                if format_result_live.is_err() {
+                    return Ok(VerificationStatus::Failure);
+                }
+            } else {
+                // Write cbmc output to a file
+                let _cbmc_result = self.run_redirect(cmd, &output_filename)?;
+                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?)
+                }
             }
+
             println!("Verification Time: {}s", elapsed);
         }
 

kani-driver/src/call_display_results.rs

@@ -28,4 +28,25 @@ impl KaniSession {
 
         Ok(())
     }
+
+    /// Display the results of a CBMC run in a user-friendly manner.
+    pub fn format_cbmc_output_live(&self) -> Result<Command> {
+        // Add flag --read-cbmc-from-stream for the parser
+        let mut python_args: Vec<OsString> = vec![
+            self.cbmc_json_parser_py.clone().into(),
+            "--read-cbmc-from-stream".into(),
+            self.args.output_format.to_string().to_lowercase().into(),
+        ];
+
+        if self.args.extra_pointer_checks {
+            python_args.push("--extra-ptr-check".into());
+        }
+
+        // This is the equivalent to running the command
+        // > cbmc --flags test_file.out.for-main --json | python --read-cbmc-from-stream regular
+        let mut python_command = Command::new("python3");
+        python_command.args(python_args);
+
+        Ok(python_command)
+    }
 }

kani-driver/src/session.rs

@@ -3,11 +3,11 @@
 
 use crate::args::KaniArgs;
 use crate::util::render_command;
-use anyhow::{bail, Context, Result};
+use anyhow::{bail, Context, Ok, Result};
 use std::cell::RefCell;
 use std::io::Write;
 use std::path::{Path, PathBuf};
-use std::process::{Command, ExitStatus};
+use std::process::{Command, ExitStatus, Stdio};
 
 /// Contains information about the execution environment and arguments that affect operations
 pub struct KaniSession {
@@ -140,6 +140,34 @@ impl KaniSession {
 
         cmd.status().context(format!("Failed to invoke {}", cmd.get_program().to_string_lossy()))
     }
+
+    /// Run a job, redirect its output to a file, and allow the caller to decide what to do with failure.
+    pub fn run_piped(&self, mut cmd: Command) -> Result<ExitStatus> {
+        if self.args.verbose || self.args.dry_run {
+            if self.args.dry_run {
+                // Short circuit. Difficult to mock an ExitStatus :(
+                return Ok(<ExitStatus as std::os::unix::prelude::ExitStatusExt>::from_raw(0));
+            }
+        }
+
+        // Create python command to parse cbmc outpu and print final result
+        let mut python_command = self.format_cbmc_output_live()?;
+
+        // Run the cbmc command as a child process
+        let mut cbmc_output = cmd.stdout(Stdio::piped()).spawn()?;
+
+        // Collect live streamed output from cbmc and pass it to the python parser
+        // Execute python command and print final output
+        if let Some(cbmc_stdout) = cbmc_output.stdout.take() {
+            let python_output_child = python_command.stdin(cbmc_stdout).status();
+            return python_output_child.context(format!(
+                "Failed to invoke {}",
+                python_command.get_program().to_string_lossy()
+            ));
+        } else {
+            Ok(<ExitStatus as std::os::unix::prelude::ExitStatusExt>::from_raw(0))
+        }
+    }
 }
 
 /// Return the path for the folder where the current executable is located.

scripts/cbmc_json_parser.py

@@ -29,6 +29,8 @@
 from enum import Enum
 from os import path
 
+from stat import S_ISFIFO
+
 # Enum to store the style of output that is given by the argument flags
 output_style_switcher = {
     'default': 'regular',
@@ -56,12 +58,14 @@ class GlobalMessages(str, Enum):
     CHECK_ID_RE = CHECK_ID + r"_.*_([0-9])*"
     UNSUPPORTED_CONSTRUCT_DESC = "is not currently supported by Kani"
     UNWINDING_ASSERT_DESC = "unwinding assertion loop"
-
+    READ_FROM_STREAM = "--read-cbmc-from-stream"
+    READ_FROM_FILE = "cbmc_output"
 
 def usage_error(msg):
     """ Prints an error message followed by the expected usage. Then exit process. """
     print(f"Error: {msg} Usage:")
-    print("cbmc_json_parser.py <cbmc_output.json> <format> [--extra-ptr-check]")
+    print(
+        "cbmc_json_parser.py {<cbmc_output.json>|--use-piped-output} <format> [--extra-ptr-check]\n")
     sys.exit(1)
 
 
@@ -70,6 +74,7 @@ def main(argv):
     Script main function.
     Usage:
       > cbmc_json_parser.py <cbmc_output.json> <format> [--extra-ptr-check]
+      > cbmc_json_parser.py --read-cbmc-from-stream <format> [--extra-ptr-check]
     """
     # We expect [3, 4] arguments.
     if len(argv) < 3:
@@ -83,22 +88,49 @@ def main(argv):
     if not output_style:
         usage_error(f"Invalid output format '{argv[2]}'.")
 
+    # Check the mode of the output
+    mode = os.fstat(sys.stdin.fileno()).st_mode
     extra_ptr_check = False
+
+    # The cbmc output can be either file mode (default) or stream mode (--read-cbmc-from-stream)
+    cbmc_output_mode = argv[1].split(".")[-1]
+    if not ((cbmc_output_mode == GlobalMessages.READ_FROM_FILE) or (
+            cbmc_output_mode == GlobalMessages.READ_FROM_STREAM)):
+        usage_error(f"CBMC output mode invalid\n")
+
     if len(argv) == 4:
         if argv[3] == "--extra-ptr-check":
             extra_ptr_check = True
         else:
             usage_error(f"Unexpected argument '{argv[3]}'.")
 
-    # parse the input json file
-    with open(argv[1]) as f:
-        sample_json_file_parsing = f.read()
+    if argv[1] == GlobalMessages.READ_FROM_STREAM:
+        # Print each streaming line live from cbmc without writing to file
+        # temporary output, will change to be parsed like the regular json objects
+        # that are written to a file
 
-    # the main function should take a json file as input
-    return_code = transform_cbmc_output(sample_json_file_parsing,
-                                        output_style, extra_ptr_check)
-    sys.exit(return_code)
+        # Check if the stdin input comes from the pipe
+        if S_ISFIFO(mode):
+            try:
+                for line in sys.stdin:
+                    print(line)
+            except BaseException:
+                # Throw custom error & sys.exit(1)
+                print(f"Unable to complete parsing CBMC Output\n")
+                sys.exit(1)
+            return_code = 0
+        else:
+            usage_error(f"CBMC Output not piped to post-processing\n")
+    else:
+        # parse the input json file
+        with open(argv[1]) as f:
+            sample_json_file_parsing = f.read()
 
+        # the main function should take a json file as input
+        return_code = transform_cbmc_output(sample_json_file_parsing,
+                                            output_style, extra_ptr_check)
+
+    sys.exit(return_code)
 
 class SourceLocation:
     def __init__(self, source_location={}):

scripts/test_cbmc_json_parser.py

@@ -35,15 +35,19 @@ def parse_with_error(self, args):
     def test_missing_arguments(self):
         self.parse_with_error("cbmc_json_parser.py".split())
         self.parse_with_error("cbmc_json_parser.py input.json".split())
+        self.parse_with_error("cbmc_json_parser.py --read-cbmc-from-stream".split())
 
     def test_invalid_format(self):
         self.parse_with_error("cbmc_json_parser.py input.json dummy_format".split())
+        self.parse_with_error("cbmc_json_parser.py --read-cbmc-from-stream dummy_format".split())
 
     def test_invalid_flag(self):
         self.parse_with_error("cbmc_json_parser.py input.json terse --invalid-flag".split())
+        self.parse_with_error("cbmc_json_parser.py --read-cbmc-from-stream terse --invalid-flag".split())
 
     def test_too_many_args(self):
         self.parse_with_error("cbmc_json_parser.py input.json terse --extra-ptr-check --extra".split())
+        self.parse_with_error("cbmc_json_parser.py --read-cbmc-from-stream terse --extra-ptr-check --extra".split())
 
 
 class SourceLocationTest(unittest.TestCase):

tests/ui/cbmc-livestream/arithmetic_overflow/expected

@@ -0,0 +1,11 @@
+"description": "attempt to compute unchecked_mul which would overflow",
+"property": "core::num::<impl u8>::unchecked_mul.arithmetic_overflow.1",
+"status": "SUCCESS"
+
+"description": "attempt to compute unchecked_add which would overflow",
+"property": "core::num::<impl u8>::unchecked_add.arithmetic_overflow.1",
+"status": "SUCCESS"
+
+"description": "attempt to compute unchecked_sub which would overflow",
+"property": "core::num::<impl u8>::unchecked_sub.arithmetic_overflow.1",
+"status": "SUCCESS"

tests/ui/cbmc-livestream/arithmetic_overflow/main.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --enable-unstable --use-piped-output
+//
+// Check that none of these operations trigger spurious overflow checks.
+#![feature(unchecked_math)]
+
+macro_rules! verify_no_overflow {
+    ($cf: ident, $uf: ident) => {{
+        let a: u8 = kani::nondet();
+        let b: u8 = kani::nondet();
+        let checked = a.$cf(b);
+        kani::assume(checked.is_some());
+        let unchecked = unsafe { a.$uf(b) };
+        assert!(checked.unwrap() == unchecked);
+    }};
+}
+
+#[kani::proof]
+fn main() {
+    verify_no_overflow!(checked_add, unchecked_add);
+    verify_no_overflow!(checked_sub, unchecked_sub);
+    verify_no_overflow!(checked_mul, unchecked_mul);
+}

tests/ui/cbmc-livestream/exact_div/expected

@@ -0,0 +1,3 @@
+"description": "exact_div arguments divide exactly",
+"property": "main.exact_div.1",
+"status": "SUCCESS"

tests/ui/cbmc-livestream/exact_div/main.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --enable-unstable --use-piped-output
+
+#![feature(core_intrinsics)]
+
+#[kani::proof]
+fn main() {
+    let a: u8 = 8;
+    let b: u8 = 4;
+    let i = unsafe { std::intrinsics::exact_div(a, b) };
+    assert!(i == 2);
+}

tests/ui/cbmc-livestream/expect_fail/expected

@@ -0,0 +1,3 @@
+"description": "resume instruction",
+"property": "<T as kani::Arbitrary>::any.unsupported_construct.1",
+"status": "SUCCESS"

tests/ui/cbmc-livestream/expect_fail/main.rs

@@ -0,0 +1,11 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --enable-unstable --use-piped-output
+
+#[kani::proof]
+fn main() {
+    let i: i32 = kani::any();
+    kani::assume(i < 10);
+    kani::expect_fail(i > 20, "Blocked by assumption above.");
+}