Skip to content

Commit

Permalink
update readme (rust-lang#91)
Browse files Browse the repository at this point in the history 
* Update README.md
* Split off a separate DEVELOPER-GUIDE
  • Loading branch information
@danielsn @tedinski
danielsn authored and tedinski committed Apr 22, 2021
1 parent 0623b87 commit 1f71216
Show file tree
Hide file tree
Showing 2 changed files with 166 additions and 72 deletions.
50 changes: 50 additions & 0 deletions DEVELOPER-GUIDE.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,50 @@
# RMC Developer Guide

## Building RMC
1. Follow [the quickstart instructions](README.md#quickstart) to initially build RMC.
1. Subsequent builds can be done incrementally, using
```
./x.py build -i --stage 1 library/std --keep-stage 1
```
1. If you encounter unexpected issues, do a full rebuild
```
./x.py clean
./x.py build -i --stage 1 library/std
```

## Submitting / updating PRs
1. Ensure that your changes are rebased against the latest `main-<upstream-version>-yyyy-mm-dd`.
If your PR is open across a `main*` branch update, we recommend doing a rebase and force push.
1. Ensure that your code is properly formatted.
```
./x.py fmt
```
1. Ensure that all regressions pass
```
./scripts/rmc-regression.sh
```

## Architecture
TODO

## Branch structure
RMC is implemented as an additional codegen backend for the
[Rust compiler](https://github.com/rust-lang/rust).
The `master` branch from the upstream compiler is mirrored as `upstream-master`.
The RMC code itself is maintained as a set of rebased patches,
on branches named `main-<upstream-version>-yyyy-mm-dd`.
These branches are updated on a weekly cadence.
The most recent of these branches is set as the `default` branch for the repository.
This is the branch that you should build and use, and this is the branch that you should make PRs against.

### Patch structure
The `main-<upstream-version>-yyyy-mm-dd` branches have the following git structure:

* A set of commits representing RMC feature code.
These patches only affect RMC files.
Any API changes are contained in a single commit, described below.
* A single patch which renames any upstream files that conflict with RMC files
* A single patch that applies any API changes needed to the upstream code for RMC to link
* The upstream `master` branch as of the date `yyyy-mm-dd`.


188 changes: 116 additions & 72 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -1,91 +1,135 @@
# Rust Model Checker (RMC)
The Rust Model Checker (RMC) aims to be a bit-precise model-checker for Rust.

## Disclaimer
## Project Status
RMC is currently in the initial development phase.
It **does not support all rust language features**.
Some unsupported (or partially supported) features will cause panics when RMC runs.
In other cases, RMC will "successfully" compile the rust code under test, but may inaccuratly give either false positives or false negatives.
If you encounter either false positives, or false negatives, please report them as an issue on this repository.
We are working to extend our support of language features.
If you encounter issues when using RMC we encourage you to
[report them to us](https://github.com/model-checking/rmc/issues/new/choose).

## Quickstart

## Security
See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.
1. Install all dependencies required for upstream-rust, as per the
[README](UPSTREAM-README.md#building-on-a-unix-like-system).

1. Install CBMC.
CBMC has prebuilt releases
[available for major platforms](https://github.com/diffblue/cbmc/releases).
RMC currently works with CBMC versions 5.26 or greater.
If you want to build CBMC from source, follow
[the cmake instructions from the CBMC repo](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#working-with-cmake).
We recommend using `ninja` as the CBMC build system.

1. Configure RMC.
We recommend using the following options:
```
./configure \
--debuginfo-level-rustc=2 \
--enable-debug \
--set=llvm.download-ci-llvm=true \
--set=rust.debug-assertions-std=false \
--set=rust.deny-warnings=false \
--set=rust.incremental=true
```

1. Build RMC
```
./x.py build -i --stage 1 library/std
```

1. Run the RMC test-suite
```
./scripts/rmc-regression.sh
```

## Running RMC
RMC currently supports command-line invocation on single files.
We are actively working to integrate RMC into `cargo`.
Until then, the easiest way to use RMC is as follows


1. Add `rmc/scripts` to your path
1. Go to a folder that contains a rust file you would like to verify with RMC.
For example, `cd rmc/rust-tests/cbmc-reg/Parenths`.
By default, `rmc` uses `main()` as the entry point.
1. Execute RMC on the file
```
rmc main.rs
```
You should see output that looks like the following
```
** Results:
main.rs function main
[main.assertion.1] line 7 attempt to compute `move _6 + const 1_i32`, which would overflow: SUCCESS
[main.assertion.2] line 7 attempt to compute `move _4 * move _5`, which would overflow: SUCCESS
[main.assertion.3] line 8 assertion failed: c == 88: SUCCESS
[main.assertion.4] line 11 attempt to compute `move _16 * move _17`, which would overflow: SUCCESS
[main.assertion.5] line 11 attempt to compute `move _15 + const 1_i32`, which would overflow: SUCCESS
[main.assertion.6] line 11 attempt to compute `move _14 * move _20`, which would overflow: SUCCESS
[main.assertion.7] line 12 assertion failed: e == 10 * (500 + 5): SUCCESS
```
1. Write your own test file, add your own assertions, and try it out!

### Advanced flags
RMC supports a set of advanced flags that give you control over the verification process.
For example, consider the `CopyIntrinsics` regression test:
1. `cd rmc/rust-tests/cbmc-reg/CopyIntrinsics`
1. Execute RMC on the file
`rmc main.rs`
1. Note that this will unwind forever
```
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 4 file <builtin-library-memcmp> line 25 function memcmp thread 0
Unwinding loop memcmp.0 iteration 5 file <builtin-library-memcmp> line 25 function memcmp thread 0
...
```
1. You can pass additional arguments to the CBMC backend using the syntax:
```
rmc filename.rs -- <additional CBMC arguments>
```
To see which arguments CBMC supports, run `cbmc --help`.
In this case, we want the `--unwind` argument to limit the unwinding.
We also use the `--unwinding-assertions` argument to ensure that our unwind bounds are sufficient.
Note that:
```
rmc main.rs -- --unwind 1 --unwinding-assertions
```
produces an unwinding failure, while
```
rmc main.rs -- --unwind 17 --unwinding-assertions
```
leads to all assertions passing.
1. You can check for undefined behaviour using builtin checks from CBMC.
Try using `--pointer-check`, or `--unsigned-overflow-check`.
You can see the full list of available checks by running `cbmc --help`.

### Looking under the hood
1. To see "under the hood" of what RMC is doing, try passing the `--gen-c` flag to RMC
```
rmc --gen-c main.rs <other-args>
```
This generates a file `main.c` which contains a "C" like formatting of the CBMC IR.
1. You can also view the raw CBMC internal representation using the `--keep-temps` option.

## Architecture
TODO
## Security
See [SECURITY](https://github.com/model-checking/rmc/security/policy) for more information.

## Developer guide
TODO
See [DEVELOPER-GUIDE.md](DEVELOPER-GUIDE.md).

## License
### Rust compiler
RMC is a fork of the rust compiler, which is primarily primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
RMC contains code from the Rust compiler.
The rust compiler is primarily distributed under the terms of both the MIT license
and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.

See [LICENSE-APACHE](LICENSE-APACHE), [LICENSE-MIT](LICENSE-MIT), and
[UPSTREAM-COPYRIGHT](UPSTREAM-COPYRIGHT) for details.

### RMC additions
RMC is Rdistributed under the terms of both the MIT license and the Apache License (Version 2.0).

See [LICENSE-APACHE](LICENSE-APACHE) and [LICENSE-MIT](LICENSE-MIT)for details.

## Quickstart
RMC is distributed under the terms of both the MIT license and the Apache License (Version 2.0).

The following will build and test `rmc`:

```
./scripts/rmc-regression.sh
```

## Build frontend

```
cd RustToCBMC
cp config.toml.example config.toml
sed -i "" \
-e "s/^#debug = .*/debug = true/" \
-e "s/^#debug-assertions-std = .*/debug-assertions-std = false/" \
-e "s/^#incremental = .*/incremental = true/" \
-e "s/^#deny-warnings = .*/deny-warnings = false/" \
config.toml
./x.py build -i --stage 1 library/std
export RMC_RUSTC=`find \`pwd\`/build -name "rustc" -print | grep stage1`
export PATH=`pwd`/scripts:$PATH
```

Note: You almost certainly want to use the local llvm installation instead
of building llvm from scratch. You do this by setting llvm-config to the
path of the local llvm-config tool in the target section of config.toml
for the target you are building. For example, on MacOS,
```
brew install llvm
echo '' >> config.toml
echo '[target.x86_64-apple-darwin]' >> config.toml
echo 'llvm-config = "/usr/local/opt/llvm/bin/llvm-config"' >> config.toml
```

Note: You almost certainly want full debug information for debugging
under gdb or lldb. You do this by setting debuginfo-level-rustc to 2.
```
sed -i "" \
-e "s/^#debuginfo-level-rustc = .*/debuginfo-level-rustc = 2/" \
config.toml
```

## Install CBMC

CBMC has prebuilt releases [available for major platforms](https://github.com/diffblue/cbmc/releases).
RMC currently works with CBMC versions 5.26 or greater.

### Building CBMC from source

If you want to build CBMC from source, however, do
```
git clone https://github.com/diffblue/cbmc.git
cd cbmc
cmake -S. -Bbuild -DCMAKE_BUILD_TYPE=Release -DWITH_JBMC=OFF
cd build
make -j
export PATH=$(pwd)/bin:$PATH
```
See [LICENSE-APACHE](LICENSE-APACHE) and [LICENSE-MIT](LICENSE-MIT) for details.

0 comments on commit 1f71216

Please sign in to comment.