Skip to content

Commit 1f71216

Browse files
danielsntedinski
danielsn
authored and
tedinski
committed
update readme (rust-lang#91)
* Update README.md * Split off a separate DEVELOPER-GUIDE
1 parent 0623b87 commit 1f71216

File tree

2 files changed

+166
-72
lines changed

2 files changed

+166
-72
lines changed

Diff for: ‎DEVELOPER-GUIDE.md

+50
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
# RMC Developer Guide
2+
3+
## Building RMC
4+
1. Follow [the quickstart instructions](README.md#quickstart) to initially build RMC.
5+
1. Subsequent builds can be done incrementally, using
6+
```
7+
./x.py build -i --stage 1 library/std --keep-stage 1
8+
```
9+
1. If you encounter unexpected issues, do a full rebuild
10+
```
11+
./x.py clean
12+
./x.py build -i --stage 1 library/std
13+
```
14+
15+
## Submitting / updating PRs
16+
1. Ensure that your changes are rebased against the latest `main-<upstream-version>-yyyy-mm-dd`.
17+
If your PR is open across a `main*` branch update, we recommend doing a rebase and force push.
18+
1. Ensure that your code is properly formatted.
19+
```
20+
./x.py fmt
21+
```
22+
1. Ensure that all regressions pass
23+
```
24+
./scripts/rmc-regression.sh
25+
```
26+
27+
## Architecture
28+
TODO
29+
30+
## Branch structure
31+
RMC is implemented as an additional codegen backend for the
32+
[Rust compiler](https://github.com/rust-lang/rust).
33+
The `master` branch from the upstream compiler is mirrored as `upstream-master`.
34+
The RMC code itself is maintained as a set of rebased patches,
35+
on branches named `main-<upstream-version>-yyyy-mm-dd`.
36+
These branches are updated on a weekly cadence.
37+
The most recent of these branches is set as the `default` branch for the repository.
38+
This is the branch that you should build and use, and this is the branch that you should make PRs against.
39+
40+
### Patch structure
41+
The `main-<upstream-version>-yyyy-mm-dd` branches have the following git structure:
42+
43+
* A set of commits representing RMC feature code.
44+
These patches only affect RMC files.
45+
Any API changes are contained in a single commit, described below.
46+
* A single patch which renames any upstream files that conflict with RMC files
47+
* A single patch that applies any API changes needed to the upstream code for RMC to link
48+
* The upstream `master` branch as of the date `yyyy-mm-dd`.
49+
50+

Diff for: ‎README.md

+116-72
Original file line numberDiff line numberDiff line change
@@ -1,91 +1,135 @@
11
# Rust Model Checker (RMC)
22
The Rust Model Checker (RMC) aims to be a bit-precise model-checker for Rust.
33

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

11+
## Quickstart
1112

12-
## Security
13-
See [CONTRIBUTING](CONTRIBUTING.md#security-issue-notifications) for more information.
13+
1. Install all dependencies required for upstream-rust, as per the
14+
[README](UPSTREAM-README.md#building-on-a-unix-like-system).
15+
16+
1. Install CBMC.
17+
CBMC has prebuilt releases
18+
[available for major platforms](https://github.com/diffblue/cbmc/releases).
19+
RMC currently works with CBMC versions 5.26 or greater.
20+
If you want to build CBMC from source, follow
21+
[the cmake instructions from the CBMC repo](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#working-with-cmake).
22+
We recommend using `ninja` as the CBMC build system.
23+
24+
1. Configure RMC.
25+
We recommend using the following options:
26+
```
27+
./configure \
28+
--debuginfo-level-rustc=2 \
29+
--enable-debug \
30+
--set=llvm.download-ci-llvm=true \
31+
--set=rust.debug-assertions-std=false \
32+
--set=rust.deny-warnings=false \
33+
--set=rust.incremental=true
34+
```
35+
36+
1. Build RMC
37+
```
38+
./x.py build -i --stage 1 library/std
39+
```
40+
41+
1. Run the RMC test-suite
42+
```
43+
./scripts/rmc-regression.sh
44+
```
45+
46+
## Running RMC
47+
RMC currently supports command-line invocation on single files.
48+
We are actively working to integrate RMC into `cargo`.
49+
Until then, the easiest way to use RMC is as follows
50+
51+
52+
1. Add `rmc/scripts` to your path
53+
1. Go to a folder that contains a rust file you would like to verify with RMC.
54+
For example, `cd rmc/rust-tests/cbmc-reg/Parenths`.
55+
By default, `rmc` uses `main()` as the entry point.
56+
1. Execute RMC on the file
57+
```
58+
rmc main.rs
59+
```
60+
You should see output that looks like the following
61+
```
62+
** Results:
63+
main.rs function main
64+
[main.assertion.1] line 7 attempt to compute `move _6 + const 1_i32`, which would overflow: SUCCESS
65+
[main.assertion.2] line 7 attempt to compute `move _4 * move _5`, which would overflow: SUCCESS
66+
[main.assertion.3] line 8 assertion failed: c == 88: SUCCESS
67+
[main.assertion.4] line 11 attempt to compute `move _16 * move _17`, which would overflow: SUCCESS
68+
[main.assertion.5] line 11 attempt to compute `move _15 + const 1_i32`, which would overflow: SUCCESS
69+
[main.assertion.6] line 11 attempt to compute `move _14 * move _20`, which would overflow: SUCCESS
70+
[main.assertion.7] line 12 assertion failed: e == 10 * (500 + 5): SUCCESS
71+
```
72+
1. Write your own test file, add your own assertions, and try it out!
73+
74+
### Advanced flags
75+
RMC supports a set of advanced flags that give you control over the verification process.
76+
For example, consider the `CopyIntrinsics` regression test:
77+
1. `cd rmc/rust-tests/cbmc-reg/CopyIntrinsics`
78+
1. Execute RMC on the file
79+
`rmc main.rs`
80+
1. Note that this will unwind forever
81+
```
82+
Unwinding loop memcmp.0 iteration 1 file <builtin-library-memcmp> line 25 function memcmp thread 0
83+
Unwinding loop memcmp.0 iteration 2 file <builtin-library-memcmp> line 25 function memcmp thread 0
84+
Unwinding loop memcmp.0 iteration 3 file <builtin-library-memcmp> line 25 function memcmp thread 0
85+
Unwinding loop memcmp.0 iteration 4 file <builtin-library-memcmp> line 25 function memcmp thread 0
86+
Unwinding loop memcmp.0 iteration 5 file <builtin-library-memcmp> line 25 function memcmp thread 0
87+
...
88+
```
89+
1. You can pass additional arguments to the CBMC backend using the syntax:
90+
```
91+
rmc filename.rs -- <additional CBMC arguments>
92+
```
93+
To see which arguments CBMC supports, run `cbmc --help`.
94+
In this case, we want the `--unwind` argument to limit the unwinding.
95+
We also use the `--unwinding-assertions` argument to ensure that our unwind bounds are sufficient.
96+
Note that:
97+
```
98+
rmc main.rs -- --unwind 1 --unwinding-assertions
99+
```
100+
produces an unwinding failure, while
101+
```
102+
rmc main.rs -- --unwind 17 --unwinding-assertions
103+
```
104+
leads to all assertions passing.
105+
1. You can check for undefined behaviour using builtin checks from CBMC.
106+
Try using `--pointer-check`, or `--unsigned-overflow-check`.
107+
You can see the full list of available checks by running `cbmc --help`.
108+
109+
### Looking under the hood
110+
1. To see "under the hood" of what RMC is doing, try passing the `--gen-c` flag to RMC
111+
```
112+
rmc --gen-c main.rs <other-args>
113+
```
114+
This generates a file `main.c` which contains a "C" like formatting of the CBMC IR.
115+
1. You can also view the raw CBMC internal representation using the `--keep-temps` option.
14116

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

18120
## Developer guide
19-
TODO
121+
See [DEVELOPER-GUIDE.md](DEVELOPER-GUIDE.md).
20122

21123
## License
22124
### Rust compiler
23-
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.
125+
RMC contains code from the Rust compiler.
126+
The rust compiler is primarily distributed under the terms of both the MIT license
127+
and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
24128

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

28132
### RMC additions
29-
RMC is Rdistributed under the terms of both the MIT license and the Apache License (Version 2.0).
30-
31-
See [LICENSE-APACHE](LICENSE-APACHE) and [LICENSE-MIT](LICENSE-MIT)for details.
32-
33-
## Quickstart
133+
RMC is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
34134

35-
The following will build and test `rmc`:
36-
37-
```
38-
./scripts/rmc-regression.sh
39-
```
40-
41-
## Build frontend
42-
43-
```
44-
cd RustToCBMC
45-
cp config.toml.example config.toml
46-
sed -i "" \
47-
-e "s/^#debug = .*/debug = true/" \
48-
-e "s/^#debug-assertions-std = .*/debug-assertions-std = false/" \
49-
-e "s/^#incremental = .*/incremental = true/" \
50-
-e "s/^#deny-warnings = .*/deny-warnings = false/" \
51-
config.toml
52-
./x.py build -i --stage 1 library/std
53-
export RMC_RUSTC=`find \`pwd\`/build -name "rustc" -print | grep stage1`
54-
export PATH=`pwd`/scripts:$PATH
55-
```
56-
57-
Note: You almost certainly want to use the local llvm installation instead
58-
of building llvm from scratch. You do this by setting llvm-config to the
59-
path of the local llvm-config tool in the target section of config.toml
60-
for the target you are building. For example, on MacOS,
61-
```
62-
brew install llvm
63-
echo '' >> config.toml
64-
echo '[target.x86_64-apple-darwin]' >> config.toml
65-
echo 'llvm-config = "/usr/local/opt/llvm/bin/llvm-config"' >> config.toml
66-
```
67-
68-
Note: You almost certainly want full debug information for debugging
69-
under gdb or lldb. You do this by setting debuginfo-level-rustc to 2.
70-
```
71-
sed -i "" \
72-
-e "s/^#debuginfo-level-rustc = .*/debuginfo-level-rustc = 2/" \
73-
config.toml
74-
```
75-
76-
## Install CBMC
77-
78-
CBMC has prebuilt releases [available for major platforms](https://github.com/diffblue/cbmc/releases).
79-
RMC currently works with CBMC versions 5.26 or greater.
80-
81-
### Building CBMC from source
82-
83-
If you want to build CBMC from source, however, do
84-
```
85-
git clone https://github.com/diffblue/cbmc.git
86-
cd cbmc
87-
cmake -S. -Bbuild -DCMAKE_BUILD_TYPE=Release -DWITH_JBMC=OFF
88-
cd build
89-
make -j
90-
export PATH=$(pwd)/bin:$PATH
91-
```
135+
See [LICENSE-APACHE](LICENSE-APACHE) and [LICENSE-MIT](LICENSE-MIT) for details.

0 commit comments

Comments
 (0)