Generate and publish dashboard into documentation

.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' }}

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[@]}"