General notes on usability issues revealed by documentation writing

[tedinski]

I just wanted to publicly track the things I came across somewhere as I find them, so I don't forget.

Critical (ordered):

• Running --visualize still includes unnecessary CBMC checks in coverage run #368 This blocks using visualize (and so blocks getting traces) when unwind is needed
• Kani produces no output on non-termination #493 Blank output is very user-unfriendly
• cargo-rmc doesn't really work well (e.g. doesn't handle dependencies), and running rmc and cargo on a crate is currently a magic incantation. running cargo rmc fails with multiple dependencies #451
• A release of RMC, so users don't need to build from scratch.
  • Maybe just a brew package for RMC (CBMC has one, but CBMC viewer would also need one) (Or possibly just a cargo crate? cargo install rmc?)
• Needing the harness to be unmangled main is bothersome, I really think we want something like #[proof] Add a #[proof] attribute that allow us to mark proof harnesses #464
• We need to write these magic declarations for things like __nondet that really should be implicitly available already, and really should have more idiomatic names. We should have an RMC prelude that gives us rmc::assume and rmc::nondet etc.

High (unordered)

• MIR gives us a lot of generated variables that are mostly just copies and obfuscate traces. (e.g. var_10 = 0; then x = var_10;)
• There should be a "simpler" version of traces for the common case of "just tell me the nondet values in my proof harness"
• Possibly some "test case reduction" though this would be a CBMC feature. We get traces about (534, 535) that could have been (0, 1)

Medium

• "Assertion failed: blah: SUCCESS" is confusing. Failed...Success? Can we remove "assertion failed" from successful assertions? #189
• We should preserve color-coded output of rustc and cbmc. We also need to "stream" output instead of waiting until completion (for instance, to see log lines as they are printed when cbmc doesn't terminate.) I believe this is the same issue. We should connect the 'tty' instead of capturing output as a string and re-printing.
• We should be able to annotate individual loops with an unwind bound instead of having to resort to a global bound.
• A better summary view on the command line. Needing to | grep FAIL is not a good user experience. We should summarize failures at the end of a run. (CBMC task?)
• Can we prioritize (even heuristically) the failures in the output? Helping users understand what they should debug first is a good idea.
• Can we deal with unreachable assertions? Currently these will just report success, but maybe that wasn't intended. (Coverage debugging problem?)
• Visualize should also give good output on the command line, not just dump useless xml. (CBMC/viewer task?)

[avanhatt]

Re: point 3, previously filed this similar one: #189

[tedinski]

I think this one remaining item still has value:

There should be a "simpler" version of traces for the common case of "just tell me the nondet values in my proof harness"

But otherwise this tracking issue is largely complete and no longer useful. Closing.