Generate and publish dashboard into documentation (rust-lang#505)

* Generate and publish dashboard into documentation

* Add Litani deps & restrict workflow to 20.04

* Add setuptools

* Final edits

* Conform with rebase

* Install script for litani deps

* Add more docs for dashboard

* Enable dash run in CI (to be removed)

* Include dashboard deps script

* Dashboard deps permissions

* Uncomment workflow condition

* Update README quickstart section

* minor fix

Author: adpaco-aws

.github/workflows/rmc.yml

@@ -29,6 +29,10 @@ jobs:
       - name: Install Rust toolchain
         run: ./scripts/setup/install_rustup.sh
 
+      - name: Install dashboard dependencies
+        if: ${{ matrix.os == 'ubuntu-20.04' && github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }}
+        run: ./scripts/setup/install_dashboard_deps.sh
+
       - name: Set config.toml file
         run: |
           ./configure \
@@ -49,6 +53,10 @@ jobs:
       - name: Execute RMC regression
         run: ./scripts/rmc-regression.sh
 
+      - name: Generate RMC dashboard
+        if: ${{ matrix.os == 'ubuntu-20.04' && github.event_name == 'push' && startsWith('refs/heads/main', github.ref) }}
+        run: ./x.py run -i --stage 1 dashboard
+
       # On one OS only, build the documentation, too.
       - name: Build Documentation
         if: ${{ matrix.os == 'ubuntu-20.04' }}

README.md

@@ -3,36 +3,28 @@ The Rust Model Checker (RMC) aims to be a bit-precise model-checker for Rust.
 
 ## Project Status
 RMC is currently in the initial development phase.
-It **does not yet support all rust language features**.
+It **does not yet support all Rust language features**.
 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
 
-1. Install all dependencies required for upstream-rust, as per the 
-   [README](UPSTREAM-README.md#building-on-a-unix-like-system).
+1. Install the dependencies needed for [`rustc`](https://github.com/rust-lang/rust),
+   [CBMC](https://github.com/diffblue/cbmc) and
+   [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc/releases/latest).
 
-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. Install [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc/releases/latest).
+   The [RMC Installation Guide](https://model-checking.github.io/rmc/install-guide.html)
+   shows how to quickly install them using our setup scripts.
 
 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
+      --set=rust.deny-warnings=false
    ```
 
 1. Build RMC

rmc-docs/build-docs.sh

@@ -17,12 +17,25 @@ if [ ! -x mdbook ]; then
     tar zxf $FILE
 fi
 
+# Publish dashboard into our documentation
+RMC_DIR=$SCRIPT_DIR/..
+HTML_DIR=$RMC_DIR/build/output/latest/html/
+
+if [ -d $HTML_DIR ]; then
+    # Litani run is copied into `src` to avoid deletion by `mdbook`
+    cp -r $HTML_DIR src/dashboard/
+    # Remove unnecessary artifacts to save space
+    rm -r src/dashboard/artifacts
+    rm -r src/dashboard/run.json
+else
+    echo "WARNING: Could not find the latest dashboard run."
+fi
+
 # Build the book into ./book/
 mkdir -p book
 ./mdbook build
 touch book/.nojekyll
 
 # TODO: Test all the code examples from our documentation
-# TODO: Build the dashboard and publish into our documentation
 
 echo "Finished documentation build successfully."

rmc-docs/src/SUMMARY.md

@@ -14,3 +14,5 @@
   - [Loops, unwinding, and bounds](./tutorial-loops-unwinding.md)
 
 - [RMC developer documentation]()
+
+- [RMC dashboard](./dashboard.md)

rmc-docs/src/dashboard.md

@@ -0,0 +1,25 @@
+# RMC Dashboard
+
+The [RMC Dashboard](./dashboard/index.html) is a testing tool based on [Compiletest](https://rustc-dev-guide.rust-lang.org/tests/intro.html) and [Litani](https://github.com/awslabs/aws-build-accumulator).
+
+The purpose of the dashboard to show the level of support in RMC for all Rust features.
+To this end, we use Rust code snippet examples from the following general Rust documentation books:
+ * The Rust Reference
+ * The Rustonomicon
+ * The Rust Unstable Book
+ * Rust by Example
+
+However, not all examples from these books are suited for verification.
+Because of that, we run three different types of jobs when generating the dashboard:
+ * `check` jobs (`BUILD`): This check only uses the Rust front-end to detect if the example is valid Rust code.
+ * `codegen` jobs (`TEST`): This check uses the Rust front-end and the RMC back-end to determine if we can generate GotoC code.
+ * `verification` jobs (`REPORT`): This check uses all of above and CBMC to obtain a verification result.
+
+Before running the above mentioned jobs, we pre-process the examples to:
+ 1. Set the expected output according to flags present in the code snippet.
+ 2. Add any required compiler/RMC flags (e.g., CBMC unwinding flags).
+ 3. Include custom assertions for verification (only in the case of `verification` jobs).
+
+Finally, we run all jobs, collect their outputs and compare them against the expected outputs.
+
+The [RMC Dashboard](./dashboard/index.html) displays a summary of the obtained results.

scripts/setup/install_dashboard_deps.sh

@@ -0,0 +1,19 @@
+#!/bin/bash
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+set -eu
+
+# The RMC Dashboard is generated using [Litani](https://github.com/awslabs/aws-build-accumulator)
+
+# Litani's dependencies:
+DEPS=(
+  gnuplot # Not required but recommended
+  graphviz
+)
+
+PYTHON_DEPS=(
+  jinja2
+)
+
+python3 -m pip install "${PYTHON_DEPS[@]}"