Feature Request: Vast `cargo kani` output simplification

[weaversa]

Requested feature: Improvements to the user (layperson) experience when running cargo kani.

Use case: Folks I'd like to introduce this technology to (Rust developers / evaluators, who I also image is your target user-base) don't have a background in automated reasoning and will likely be turned off by the massive amount of cruft one has to sift through to find out whether or not their code has an issue. Eliding non-relevant information (non-relevant from a user perspective) is also pertinent to CI integration -- "why did this CI run fail?" -- also CI log sizes are typically limited.

Here's an example run on a pretty simple program --

< PRINTED THOUSANDS OF TIMES >
Unwinding loop _RNvXs9_NtNtCs4bv2lBw1mAj_4core4iter5rangeINtNtNtB9_3ops5range14RangeInclusivejENtB5_26RangeInclusiveIteratorImpl9spec_nextCs8cGVXT8IZMx_8aes_rust.2 iteration 1 file /rustc/bc4b39c271bbd36736cbf1c0a1ac23d5df38d365/library/core/src/ops/range.rs line 540 column 9 function <std::ops::RangeInclusive<usize> as std::iter::range::RangeInclusiveIteratorImpl>::spec_next thread 0
Unwinding loop _RNvXs9_NtNtCs4bv2lBw1mAj_4core4iter5rangeINtNtNtB9_3ops5range14RangeInclusivejENtB5_26RangeInclusiveIteratorImpl9spec_nextCs8cGVXT8IZMx_8aes_rust.0 iteration 1 file /rustc/bc4b39c271bbd36736cbf1c0a1ac23d5df38d365/library/core/src/iter/range.rs line 1005 column 12 function <std::ops::RangeInclusive<usize> as std::iter::range::RangeInclusiveIteratorImpl>::spec_next thread 0
Unwinding loop _RNvCs8cGVXT8IZMx_8aes_rust4xorb.0 iteration 15 file /local/packages/aes-rust/src/main.rs line 271 column 3 function xorb thread 0
Unwinding loop _RNvXs9_NtNtCs4bv2lBw1mAj_4core4iter5rangeINtNtNtB9_3ops5range14RangeInclusivejENtB5_26RangeInclusiveIteratorImpl9spec_nextCs8cGVXT8IZMx_8aes_rust.2 iteration 1 file /rustc/bc4b39c271bbd36736cbf1c0a1ac23d5df38d365/library/core/src/ops/range.rs line 540 column 9 function <std::ops::RangeInclusive<usize> as std::iter::range::RangeInclusiveIteratorImpl>::spec_next thread 0
Unwinding loop _RNvXs9_NtNtCs4bv2lBw1mAj_4core4iter5rangeINtNtNtB9_3ops5range14RangeInclusivejENtB5_26RangeInclusiveIteratorImpl9spec_nextCs8cGVXT8IZMx_8aes_rust.0 iteration 1 file /rustc/bc4b39c271bbd36736cbf1c0a1ac23d5df38d365/library/core/src/iter/range.rs line 1005 column 12 function <std::ops::RangeInclusive<usize> as std::iter::range::RangeInclusiveIteratorImpl>::spec_next thread 0
Unwinding loop _RNvCs8cGVXT8IZMx_8aes_rust4xorb.0 iteration 16 file local/packages/aes-rust/src/main.rs line 271 column 3 function xorb thread 0
Unwinding loop _RNvXs9_NtNtCs4bv2lBw1mAj_4core4iter5rangeINtNtNtB9_3ops5range14RangeInclusivejENtB5_26RangeInclusiveIteratorImpl9spec_nextCs8cGVXT8IZMx_8aes_rust.1 iteration 1 file /rustc/bc4b39c271bbd36736cbf1c0a1ac23d5df38d365/library/core/src/iter/range.rs line 1005 column 12 function <std::ops::RangeInclusive<usize> as std::iter::range::RangeInclusiveIteratorImpl>::spec_next thread 0
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 4 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 5 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 6 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 7 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 8 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 9 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 10 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 11 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 12 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 13 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 14 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 15 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 16 file <builtin-library-memcmp> line 25 function memcmp thread 0
Runtime Symex: 255.182s
size of program expression: 2812596 steps
slicing removed 1853734 assignments
Generated 972478 VCC(s), 155801 remaining after simplification
Runtime Postprocess Equation: 2.46339s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 225.859s
Running propositional reduction
Post-processing
Runtime Post-process: 2.4369e-05s
Solving with MiniSAT 2.2.1 with simplifier
15248398 variables, 31897971 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 81.1218s
< HANG FOR AN INDEFINITE PERIOD OF TIME >

Information such as _RNvXs9_NtNtCs4bv2lBw1mAj_4core4iter5rangeINtNtNtB9_3ops5range14RangeInclusivejENtB5_26RangeInclusiveIteratorImpl9spec_nextCs8cGVXT8IZMx_8aes_rust.0 iteration 1 file is better guarded by your verbose/debug output flags. As well, top says cbmc has been running for 20 minutes, and I have no idea what's it's trying to solve.

Some suggestions would be to have cargo kani (the default way to run the tool) output only information relevant to a layperson and ensure that operations that may take time are prefixed w/ some indication of that.

[tedinski]

Folks I'd like to introduce this technology to (Rust developers / evaluators, who I also image is your target user-base) don't have a background in automated reasoning and will likely be turned off by the massive amount of cruft one has to sift through to find out whether or not their code has an issue.

Understood and we're in complete agreement.

There is some amount of difficulty here: one problem we have to cope with (somehow) is that unwinding can sometimes fail to terminate. We actually made a significant improvement here recently in that this output gets written out as it comes, and not all buffered up until the "end." (which may never come!)

So there's a balance that needs striking where we DO need to provide some kind of output from cbmc "live" so that this failure mode can be spotted. But obviously it needs to be better.

What's more, a lot of this output from CBMC is just strings, so we'll probably have to bite the bullet and parse things here...

[weaversa]

Thanks @tedinski!

Since there are plans for other backends, rather than parsing CBMC output have you considered a backend management layer that would, by default, elide all output from the backend and respond generically, for example:

Working on proving 'assert(x == y)` in `myfile.rs` line 12 using backend `CBMC`.
  Starting symbolic execution.
    Unwinding loops in function 'f'.
  Symbolic execution complete in 28.125s.
  Discharging 47 safety proofs.
  Safety proofs discharged in 3.401s.
  Discharging main assertion `assert(x == y)`.
  Assertion discharged in 2.401s.
Proved 'assert(x == y)` in `myfile.rs` line 12 in 34.9.27s

And, if there are any errors along the way then Kani could report them generically, such as "Symbolic execution failed, rerun with --verbose_sym = 1 to see more information about the failure."

[zhassan-aws]

Totally agree! We appreciate the feedback. We've been putting some effort into simplifying the output, but there's still a lot to be done. One related issue is https://github.com/model-checking/kani/issues/1194, which we should perhaps turn into an RFC and gather user feedback on what they would like to see (and not see!).

[weaversa]

Totally agree! We appreciate the feedback. We've been putting some effort into simplifying the output, but there's still a lot to be done. One related issue is #1194, which we should perhaps turn into an RFC and gather user feedback on what they would like to see (and not see!).

Thanks for the pointer to #1194. I'll close this issue in favor of that and a potential RFC.