cargo-rmc tracking issue

[tedinski]

This is an overall tracking issue for cargo-rmc. The milestone of closing this issue should correspond to "cargo-rmc is good enough to make our first real release of RMC."

Core critical path: (The things needing tackling first, to enable other dependent work)

• Replace single-file rmc script with scripty rust.
  • Command-line flag parsing. Invoking rmc-rustc. Invoking symtab2gb, goto-cc, cbmc.
• Replace python cargo-rmc script with scripty rust.
• Implement proof harness parsing / handling. (out of scope: good output. For first pass, just run all of them in sequence and maybe summarize at the end.)

Followup tasks not on the critical path: (Continuation of the above, but doesn't impact other dependent work)

• Eliminate the "shell-scripty-ness" of the rust implementation. (e.g. do not shell out to parallel, invoke commands in parallel ourselves. Necessary to remove OS dependencies we don't want to ask users to install.)
• Ensure rmc correctly re-builds the rmc prelude as part of the build. (cargo-rmc should be able to expect rmc as a dev-dependency)
• We need expanded tests written for cargo-rmc

"Nice to have":

• Do the build ourselves instead of invoking cargo test --no-run. (i.e. look into cargo metadata etc)
• [probably defer this until after release] cargo rmc plan to help with a litani integration. Perhaps a --ci mode that changes output defaults.

Output improvements:

• The initial state of the rust port will save cbmc output to a file and invoke cbmc_json_parser.py
• Port that python to rust
• Improve output handling for multiple proof harnesses (Jai)
• Introduce handling for asserts so we can report e.g. unknown/unreachable/always-fails (Zyad)
• Get "warnings" information through rmc-metadata.json and report potential soundness issues somehow (DSN)
• Clarifying properties that mention temporary variables (Celina)

Installation experience dependencies:

• Get cargo-rmc into crates.io.
• Implement "download binaries on first run" (and cargo-rmc prepare command to explicitly trigger that)

---

Tracking potential improvements from #738

• Refactor InstallType once we're sure of how we should be detecting/handling different installation types.
• Possibly revisit the idea of having --flag and --no-flag, something pythong argparse handled but Rust arg libraries don't, so it's not idiomatic anymore.
• Unwind tip (+ unsupported tip?) #839 (unwind portion completed. Issue open for additional tips.)
• Possibly revisit the idea of removing the cargo-kani and kani bash scripts that we use for development purposes
• Refactor how arguments are passed to cbmc from call_cbmc_viewer. In particular, the 'checks' shouldn't be present for the 'cover' run of cbmc, but the rest of the arguments should be.
• Parallelization opportunities in linking (and in multiple cbmc runs for viewer)
• the cargo location-project todo Cargo-rmc cannot locate workspace Cargo.toml #717
• support development release builds? Fix hard-coded assumptions about debug target #841
• Update to clap 3 instead of structopt
• Improve cargo-kani --help output
• --gen-c-runnable restored to working order
• Checking for dependencies in PATH (cbmc, viewer, etc) (at least in the dev mode when we want them in PATH)
• Improve communication between python parser and rust code, so exceptions get reported as such, but verification failure can be clearly separated from other failures
• Error code expectations for --visualize right now I think it return status 0, regardless of verificaiton failure/success
• cargo-kani should probably not delete some/all of the intermediate files it puts in target-dir (in contrast to standalone kani, which should clean up its mess in the local directory.)

[celinval]

Closing this issue since it's no longer relevant.