From 9065d5a131e7763d8c48db54f370bf4cc0bedfe1 Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Wed, 20 Oct 2021 20:05:42 +0000 Subject: [PATCH 1/2] Introduce dev command 'cheat sheets' --- rmc-docs/src/SUMMARY.md | 6 +- rmc-docs/src/dev-documentation.md | 118 ++++++++++++++++++++++++++++++ 2 files changed, 123 insertions(+), 1 deletion(-) create mode 100644 rmc-docs/src/dev-documentation.md diff --git a/rmc-docs/src/SUMMARY.md b/rmc-docs/src/SUMMARY.md index 86ebc789d7e2..a885a8480558 100644 --- a/rmc-docs/src/SUMMARY.md +++ b/rmc-docs/src/SUMMARY.md @@ -15,6 +15,10 @@ - [Loops, unwinding, and bounds](./tutorial-loops-unwinding.md) - [Where to start on real code](./tutorial-real-code.md) -- [RMC developer documentation]() +- [RMC developer documentation](dev-documentation.md) + - [Architecture diagrams]() + - [Code tour]() + - [Testing]() + - [Setting up a dev environment]() - [RMC dashboard](./dashboard.md) diff --git a/rmc-docs/src/dev-documentation.md b/rmc-docs/src/dev-documentation.md new file mode 100644 index 000000000000..6a19fb52396b --- /dev/null +++ b/rmc-docs/src/dev-documentation.md @@ -0,0 +1,118 @@ +# RMC developer documentation + +## Build command cheat sheet + +```bash +# Normal build +./x.py build -i --stage 1 library/std +``` +```bash +# Full regression suite +./scripts/rmc-regression.sh +``` +```bash +# Test suite run (to run a specific suite from src/test/, just remove the others) +./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc +``` +```bash +# Dashboard run +./scripts/setup/install_dashboard_deps.sh +./x.py run -i --stage 1 dashboard +``` +```bash +# Documentation build +cd rmc-docs +./build-docs.sh +``` + +### Resolving development issues + +```bash +# "error[E0514]: found crate `std` compiled by an incompatible version of rustc" +# or similar error? Clean build RMC: +rm -rf target build +./x.py build -i --stage 1 library/std +``` +```bash +# firecracker build problem with rmc-regression? Probably a similar issue: +rm -rf firecracker/build +``` + +## Git command cheat sheet + +RMC follows the "squash and merge pull request" pattern. +As a result, the "main commit message" will be the title of your pull request. +The individual commit message bodies you commit during development will by default be a bulleted list in the squashed commit message body, but these are editable at merge time. +So you don't have to worry about a series of "oops typo fix" messages while fixing up your pull request, these can be edited out of the final message when you click merge. + +```bash +# Set up your git fork +git remote add fork git@github.com:${USER}/rmc.git +``` +```bash +# Reset everything. Don't have any uncommitted changes! +git clean -xffd +git submodule foreach --recursive git clean -xffd +git submodule update --init +# Don't forget to re-configure your RMC build: +./configure \ + --enable-debug \ + --set=llvm.download-ci-llvm=true \ + --set=rust.debug-assertions-std=false \ + --set=rust.deny-warnings=false +``` +```bash +# Done with that PR, time for a new one? +git switch main +git pull origin +git submodule update --init +./x.py build -i --stage 1 library/std +``` +```bash +# Need to update local branch (e.g. for an open pull request?) +git fetch origin +git merge origin/main +``` +```bash +# Search only git-tracked files +git grep codegen_panic +``` +```bash +# See all commits that are part of RMC, not part of Rust +git log --graph --oneline origin/upstream-rustc..origin/main +``` +```bash +# See all files modified by RMC (compared to upstream Rust) +git diff --stat origin/upstream-rustc..origin/main +``` + +## RMC command cheat sheet + +These can help understand what RMC is generating or encountering on an example or test file: + +```bash +# Enable `debug!` macro logging output when running RMC: +rmc --debug file.rs +``` +```bash +# Keep CBMC Symbol Table and Goto-C output (.json and .goto) +rmc --keep-temps file.rs +``` +```bash +# Generate "C code" from CBMC IR: +rmc --gen-c file.rs +``` + +## CBMC command cheat sheet + +```bash +# See CBMC IR from a C file: +goto-cc file.c -o file.out +goto-instrument --print-internal-representation file.out +# or (for json symbol table) +cbmc --show-symbol-table --json-ui file.out +``` +```bash +# Recover C from goto-c binary +goto-instrument --dump-c file.out > file.gen.c +``` From da7fe2e2168462e8b128f9b9bffa1b154c0878fe Mon Sep 17 00:00:00 2001 From: Ted Kaminski Date: Wed, 27 Oct 2021 01:08:46 +0000 Subject: [PATCH 2/2] edits in response to feedback --- rmc-docs/src/SUMMARY.md | 6 +----- rmc-docs/src/dev-documentation.md | 15 ++++++++++----- 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/rmc-docs/src/SUMMARY.md b/rmc-docs/src/SUMMARY.md index a885a8480558..c1bc014f750e 100644 --- a/rmc-docs/src/SUMMARY.md +++ b/rmc-docs/src/SUMMARY.md @@ -15,10 +15,6 @@ - [Loops, unwinding, and bounds](./tutorial-loops-unwinding.md) - [Where to start on real code](./tutorial-real-code.md) -- [RMC developer documentation](dev-documentation.md) - - [Architecture diagrams]() - - [Code tour]() - - [Testing]() - - [Setting up a dev environment]() +- [RMC developer documentation](./dev-documentation.md) - [RMC dashboard](./dashboard.md) diff --git a/rmc-docs/src/dev-documentation.md b/rmc-docs/src/dev-documentation.md index 6a19fb52396b..2cafeddf9105 100644 --- a/rmc-docs/src/dev-documentation.md +++ b/rmc-docs/src/dev-documentation.md @@ -7,6 +7,11 @@ ./x.py build -i --stage 1 library/std ``` ```bash +# Once built successfully once, do a faster rebuild +./x.py build -i --stage 1 library/std --keep-stage 1 +``` +([`--keep-stage` comes with caveats](https://rustc-dev-guide.rust-lang.org/building/suggested.html#incremental-builds-with---keep-stage). Know that it may cause spurious build failures.) +```bash # Full regression suite ./scripts/rmc-regression.sh ``` @@ -33,10 +38,6 @@ cd rmc-docs rm -rf target build ./x.py build -i --stage 1 library/std ``` -```bash -# firecracker build problem with rmc-regression? Probably a similar issue: -rm -rf firecracker/build -``` ## Git command cheat sheet @@ -72,6 +73,8 @@ git submodule update --init # Need to update local branch (e.g. for an open pull request?) git fetch origin git merge origin/main +# Or rebase, but that requires a force push, +# and because we squash and merge, an extra merge commit in a PR doesn't hurt. ``` ```bash # Search only git-tracked files @@ -99,7 +102,7 @@ rmc --debug file.rs rmc --keep-temps file.rs ``` ```bash -# Generate "C code" from CBMC IR: +# Generate "C code" from CBMC IR (.c) rmc --gen-c file.rs ``` @@ -111,6 +114,8 @@ goto-cc file.c -o file.out goto-instrument --print-internal-representation file.out # or (for json symbol table) cbmc --show-symbol-table --json-ui file.out +# or (an alternative concise format) +cbmc --show-goto-functions file.out ``` ```bash # Recover C from goto-c binary