Cleanup Kani's output

[celinval]

Requested feature: Provide a cleaner user interface by default and allow users to control its verbosity. Use case: Kani output can be very verbose which makes it hard to read.

Test case: Kani prints 2000+ lines (400+ properties) in this testcase taken from tests/kani/Vectors/vector_extend.rs:

#[kani::proof]
fn main() {
    let mut v: Vec<u32> = Vec::new();
    v.extend(42..=42);
    assert!(v[0] == 42);
}

Proposed solution:

Provide the following verbosity options to kani and cargo-kani:

• Default: Similar to today's output but without CBMC stats and only include user assertions for each harness.
• --quiet: Similar interface to cargo test --quiet. I.e.:

running 5 harnesses
.....
verification result: ok. 5 passed; 0 failed; finished in 0.00s

with failure Kani displays the terse output for the failed tests:

running 5 harnesses
..F..
verification result: FAILED. 4 passed; 1 failed; finished in 0.00s

---- harness: <name> ----
VERIFICATION RESULT: 
 ** 1 of 100 failed (10 unreacheable)
Failed Checks: assertion failed: 1 + 1 == 3
 File: "/workspace/kani-project/kani/tests/ui/terse-output-format-fail/fail.rs", line 7, in main

VERIFICATION:- FAILED

failures:
    <harness_name>

• --verbose: Today's default interface including all checks.
• --debug: Verbose output that also include debug logs.
• --raw: Hidden option to print CBMC's output as is. Implies debug.

For simplicity, I would prefer if we retire today's --output-format.

Alternative solution:

We could use --output-format [quiet | regular | verbose | debug | raw].

[jaisnan]

1. I agree with changing the default output to what you are proposing and adding the other suggested outputs.
2. What about warnings? Do we still display them by default? or do we move them over to the --debug option?
3. What does "implies debug" mean in the case of --raw? From what I am understanding, we print the debug output as well as the cbmc output for the --raw option is what you suggest? Please correct me if I understood it wrong.

Would love to take the task up if the team comes to a consensus.

[celinval]

That's a good point. For question 2, I would say we print warnings for everything except the tests that pass when using the --quiet option.

For question 3, you got it right. I was thinking that it should only be used for debug purpose; hence, we assume debug verbosity.

[zhassan-aws]

I agree with the proposal.

For simplicity, I would prefer if we retire today's --output-format.

+1

--raw: Hidden option to print CBMC's output as is. Implies debug.

Can we reduce it to imply --verbose only? Debug logs can contain too much information.

[jaisnan]

@tedinski @danielsn any thoughts?

[tedinski]

I like the idea of a quiet mode. We do need to figure out how to communicate unwinding problems if we're going to suppress CBMC output (but we're already suppressing that when things don't terminate so... we need to solve that problem anyway...)

[Djazouli]

I also like the idea of a quiet mode. In fact, I really like the

Similar interface

in

--quiet: Similar interface to cargo test --quiet

I feel like the closer the interface gets to the one from the standard library, the easier it is to use.
I guess to fully follow this principle, even the user's assertions would get removed if the default verbosity option is used. This would also kind of automagically solve https://github.com/model-checking/kani/issues/1240#issue-1256966434 when the default verbosity is used.

[jaisnan]

Thank you very much for your input! @Djazouli, much appreciated.