forked from rust-lang/rust
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Introduce documentation for building a larger cargo project (rust-lan…
…g#554) * Introduce documentation for building a larger cargo project * copyright on script * Edits in response to feedback
- Loading branch information
Showing
4 changed files
with
124 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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 [email protected]: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. | ||
|
||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |