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

[jaisnan]

Description of changes:

CBMC currently reads the input from CBMC , waits for termination and writes the output to a file which goes to the parsing script. This runs into an issue when CBMC does not seemingly terminate, which makes Kani appear to be hung.

This PR changes that to show the JSON output live from CBMC which will later be consumed by the parsing to show the post processed Kani output.

For example, for the rust file -

fn rev(mut x: [i32; 4]) -> [i32; 4] {
    x.reverse();
    x
}

#[cfg(kani)]
#[kani::proof]
fn example() {
    let var = kani::any();
    let reversed = rev(var);
    let double_reversed = rev(reversed);

    assert_eq!(var, double_reversed);
}

Before -

After -

As we can , there is a long unwinding loop that's not being displayed to the user which can cause some confusion.
With this change, the user can be informed about the status of the verification live.

Resolved issues:

Related #493

Call-outs:

1. This Hides the live output behind a flag --use-piped-output for now.
2. This PR only streams the JSON output from CBMC. An incoming PR will convert the live JSON into the regular Kani output.

Testing:

• How is this change tested?
  Hidden behind a flag to be as non-invasive as possible.

• Is this a refactor change?
  Yes

Checklist

• Each commit message has a non-empty body, explaining why the change was made
• Methods or procedures are documented
• Regression or unit tests are included, or existing tests cover the modified code
• My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[adpaco-aws]

You should be able to define expected tests for this, no?

[adpaco-aws]

I would use an error code here.

[jaisnan]

I've added a custom exit string and an error code of 1 with -

print(f"Unable to complete parsing CBMC Output\n")
sys.exit(1)

Would this work?

[adpaco-aws]

Sorry, my comment here was not very clear.

If I'm not mistaken, this will print all lines from CBMC's output and return 0. If we change this to 1, do the regression tests still pass?

[jaisnan]

I should have expanded more in the comments. The return code is 1 if the stream of output is interrupted , either by a broken line or broken pipe or user interrupt (Ex - keyboard interrupt). If it completes printing all the lines from CBMC, then it returns 0. I shall add this clarification to the comments on the code.

I hope this is an acceptable usage of the error code?

[adpaco-aws]

A return code with value 0 basically means that verification is always successful.

[jaisnan]

You should be able to define expected tests for this, no?

I was able to add in a few tests and refactored the code as suggested. Let me know if they're as expected!

[adpaco-aws]

This call is right after the call to Instant::now(), so it's not measuring verification time anymore.

[adpaco-aws]

A return code with value 0 basically means that verification is always successful.

[adpaco-aws]

Closed in favor of #1433