Introduce documentation for building a larger cargo project

README.md

@@ -159,7 +159,7 @@ For example, we will describe using RMC as a backend to build the [`rand-core` c
 2. Clone `rand` and navigate to the `rand-core` directory:
    ```
    git clone git@github.com:rust-random/rand.git
-   cd rand/rand-core
+   cd rand/rand_core
    ```
 3. Next, we need to add an entry-point for CBMC to the crate's source. For now, we will just pick an existing unit test. Open `src/le.rs` and find the `test_read` function at the bottom of the file. Add the following attribute to keep the function name unmangled, so we can later pass it to CBMC. 
 

rmc-docs/src/SUMMARY.md

@@ -4,7 +4,7 @@
   - [Installation](./install-guide.md)
   - [Comparison with other tools](./tool-comparison.md)
   - [RMC on a single file](./rmc-single-file.md)
-  - [RMC on a crate]()
+  - [RMC on a package](./cargo-rmc.md)
   - [Debugging failures]()
   - [Debugging non-termination]()
   - [Debugging coverage]()

rmc-docs/src/cargo-rmc.md

@@ -0,0 +1,52 @@
+# RMC on a package
+
+> RMC currently ships with a `cargo-rmc` script, but this support is deeply limited (e.g. to a single crate).
+> This will be corrected soon, and this documentation updated.
+> In the meantime, we document the current build process for a larger project with dependencies here.
+
+To build a larger project (one with dependencies or multiple crates) with RMC, you currently need to:
+
+1. Build the project with an appropriate set of flags to output CBMC "symbol table" `.json` files.
+2. Link these together into a single "goto binary", with appropriate preprocessing flags.
+3. Directly call CBMC on this resulting binary.
+
+We give an example of this kind of script, with explanations, below.
+
+# Building and running
+
+Let's assume you have a project you can build with `cargo build` and you've written a proof harness somewhere in it that you want to run RMC on:
+
+```rust
+#[no_mangle]
+#[cfg(rmc)]
+fn my_harness() {
+}
+```
+
+A sample build script might start like this:
+
+```bash
+{{#include sample-rmc-build.sh:cargo}}
+```
+
+This allows us to re-use the `cargo` build system, but with flags that override `rustc` with RMC instead.
+More specifically, by setting the `RUSTC` environment variable to `rmc-rustc`, each Rust source file targeted by `cargo build` is "compiled" with RMC instead of `rustc`.
+The result of running `rmc-rustc` on a source file is a symbol table json file written in the CBMC Goto-C language.
+The use of an alternate target directory ensures RMC and rustc don't confuse each other with different intermediate output.
+
+Next we can convert the symbol tables into goto binaries, in parallel, and then link them together:
+
+```bash
+{{#include sample-rmc-build.sh:linking}}
+```
+
+At this point we have the project built, but now we want to transform it into something that will run a specific proof harness.
+To do that, we specialize it, preprocess it, and then run CBMC on the result:
+(In practice, we might want to do the above steps once, then repeat the below steps for each proof harness.)
+
+```bash
+{{#include sample-rmc-build.sh:cbmc}}
+```
+
+At this point we have a complete script and should now be able to run `./sample-rmc-build my_harness` to run a particular proof harness.
+Even in very large projects the removal of unreachable code should mean only the parts relevant to that proof harness are preserved in the RMC run.

rmc-docs/src/sample-rmc-build.sh

@@ -0,0 +1,70 @@
+#!/bin/bash
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# ANCHOR: cargo
+set -eux
+
+# The argument to this script will be the proof harness, e.g. 'my_harness' above
+ENTRY_POINT=$1
+
+export CARGO_TARGET_DIR=target-rmc
+
+env \
+  RUST_BACKTRACE=1 \
+  RUSTC=rmc-rustc \
+  RUSTFLAGS="-Z trim-diagnostic-paths=no -Z codegen-backend=gotoc --cfg=rmc" \
+  cargo build --target x86_64-unknown-linux-gnu
+# ANCHOR_END: cargo
+
+
+# ANCHOR: linking
+cd $CARGO_TARGET_DIR/x86_64-unknown-linux-gnu/debug/deps
+
+# Independently translate each symbol table into a goto binary
+ls *.json | parallel symtab2gb {} --out {.}.out
+
+# Link everything together
+goto-cc *.out -o linked-binary.out
+# ANCHOR_END: linking
+
+
+# TEMPORARY FIX
+# Empty C file so CBMC inserts its header
+touch empty.c
+# without this, we get cbmc errors about __CPROVER_dead_object missing
+
+
+# ANCHOR: cbmc
+# Now for each harness we specialize a binary:
+HARNESS_BIN="harness_${ENTRY_POINT}.out"
+goto-cc --function ${ENTRY_POINT} linked-binary.out empty.c -o "${HARNESS_BIN}"
+
+# Perform some preprocessing
+INSTRUMENT_ARGS=(
+  --drop-unused-functions
+)
+goto-instrument "${INSTRUMENT_ARGS[@]}" "${HARNESS_BIN}" "${HARNESS_BIN}"
+
+# Run CBMC, passing along appropriate CBMC arguments:
+CBMC_ARGS=(
+  # RMC defaults
+  --unwinding-assertions
+  --bounds-check
+  --pointer-check
+  --pointer-primitive-check
+  --pointer-overflow-check
+  --signed-overflow-check
+  --undefined-shift-check
+  --unsigned-overflow-check
+  --conversion-check
+  --div-by-zero-check
+  --float-overflow-check
+  --nan-check
+  # Additional options
+  --unwind 0
+  --object-bits 11
+)
+
+cbmc "${CBMC_ARGS[@]}" "${HARNESS_BIN}"
+# ANCHOR_END: cbmc