Run compiletest on rmc documentation code

rmc-docs/README.md

@@ -8,3 +8,15 @@ ssh -t -L 3000:127.0.0.1:3000 rmc-host 'cd rmc/rmc-docs/ && ./mdbook serve'
 
 This command will connect to `rmc-host` where it assumes RMC is checked out in `rmc/` and the documentation has been built once successfully.
 It will automatically detect changes to the docs and rebuild, allowing you to quickly refresh in your local browser when you visit: `http://127.0.0.1:3000/`
+
+## Documentation tests
+
+The code in `src/tutorial/` is tested with `compiletest`.
+This means each file should be buildable independently (i.e. you can run `rmc` on each `.rs` file).
+It also means the necessary `rmc-` flag-comments must appear in each file.
+
+To run just these tests, return to the RMC root directory and run:
+
+```
+./x.py test -i --stage 1 rmc-docs
+```

rmc-docs/build-docs.sh

@@ -42,6 +42,9 @@ mkdir -p book
 ./mdbook build
 touch book/.nojekyll
 
-# TODO: Test all the code examples from our documentation
+# Testing of the code in the documentation is done via the usual
+# ./scripts/rmc-regression.sh script. A note on running just the
+# doc tests is in README.md. We don't run them here because
+# that would cause CI to run these tests twice.
 
 echo "Finished documentation build successfully."

rmc-docs/src/dev-documentation.md

@@ -21,7 +21,7 @@
 ```
 ```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
+./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc rmc-docs
 ```
 ```bash
 # Dashboard run

rmc-docs/src/tutorial/kinds-of-failure/tests/bounds-check.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // ANCHOR: code
 /// Wrap "too-large" indexes back into a valid range for the array

rmc-docs/src/tutorial/kinds-of-failure/tests/overflow-quicksort.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // ANCHOR: code
 fn find_midpoint(low: u32, high: u32) -> u32 {

rmc-docs/src/tutorial/kinds-of-failure/tests/overflow.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // ANCHOR: code
 fn simple_addition(a: u32, b: u32) -> u32 {

rmc-docs/src/tutorial/loops-unwinding/src/lib.rs

@@ -1,5 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-flags: --cbmc-args --unwind 11
+// rmc-verify-fail
 
 // ANCHOR: code
 fn initialize_prefix(length: usize, buffer: &mut [u8]) {

rmc-docs/src/tutorial/rmc-first-steps/src/lib.rs

@@ -1,5 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// rmc-verify-fail
 
 // ANCHOR: code
 fn estimate_size(x: u32) -> u32 {

scripts/rmc-regression.sh

@@ -25,7 +25,7 @@ check-cbmc-viewer-version.py --major 2 --minor 5
 ./scripts/setup/build_rmc_lib.sh
 
 # Standalone rmc tests, expected tests, and cargo tests
-./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc
+./x.py test -i --stage 1 rmc firecracker prusti smack expected cargo-rmc rmc-docs
 ./x.py test -i --stage 0 compiler/cbmc
 
 # Check codegen for the standard library

src/bootstrap/builder.rs

@@ -473,6 +473,7 @@ impl<'a> Builder<'a> {
                 test::Expected,
                 test::Dashboard,
                 test::Stub,
+                test::RmcDocs,
                 // Run run-make last, since these won't pass without make on Windows
                 test::RunMake,
             ),

src/bootstrap/test.rs

@@ -1229,6 +1229,8 @@ default_test!(Expected { path: "src/test/expected", mode: "expected", suite: "ex
 
 default_test!(Dashboard { path: "src/test/dashboard", mode: "rmc", suite: "dashboard" });
 
+default_test!(RmcDocs { path: "src/test/rmc-docs", mode: "rmc", suite: "rmc-docs" });
+
 default_test!(Stub { path: "src/test/stub-tests", mode: "stub-tests", suite: "stub-tests" });
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]

src/test/rmc-docs

@@ -0,0 +1 @@
+../../rmc-docs/src/tutorial