Generate Kani Metrics (#235)

Add a new "Kani Metrics" workflow (that runs every week) that calls
`./scripts/run-kani --run metrics`, then creates a pull request to this
repository with the computed metrics. See
[here](carolynzech#38) for an
example of what the pull request will look like. Also update our "Build
Book" workflow to publish graphs of the metrics.

Callouts:
- This is a separate workflow from the Kani workflow because it is a
cronjob instead of running on every pull request. I thought the plots
would be too noisy if we ran on every PR.
- See the "Notes" section of `kani_std_analysis.py` for other callouts.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

.github/workflows/kani-metrics.yml

@@ -0,0 +1,42 @@
+name: Kani Metrics Update
+
+on:
+  schedule:
+    - cron: '0 0 * * 0'  # Run at 00:00 UTC every Sunday
+  workflow_dispatch:
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  update-kani-metrics:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout Repository
+      uses: actions/checkout@v4
+      with:
+        submodules: true
+
+    # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
+    - name: Set up Python
+      uses: actions/setup-python@v4
+      with:
+        python-version: '3.x'
+
+    - name: Compute Kani Metrics
+      run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
+
+    - name: Create Pull Request
+      uses: peter-evans/create-pull-request@v7
+      with:
+        commit-message: Update Kani metrics
+        title: 'Update Kani Metrics'
+        body: |
+          This is an automated PR to update Kani metrics.
+          
+          The metrics have been updated by running `./scripts/run-kani.sh --run metrics`.
+        branch: update-kani-metrics
+        delete-branch: true
+        base: main

.gitignore

@@ -26,6 +26,8 @@ library/target
 *.rmeta
 *.mir
 Cargo.lock
+/doc/mdbook-metrics/target
+*.png
 
 ## Temporary files
 *~
@@ -46,7 +48,6 @@ package-lock.json
 ## Kani
 *.out
 
-
 # Added by cargo
 #
 # already existing elements were commented out

doc/book.toml

@@ -19,5 +19,11 @@ runnable = false
 
 [output.linkcheck]
 
+[preprocessor.metrics]
+# Note that the manifest-path is doc/mdbook-metrics, meaning that to build this book, you need to run "mdbook build doc"
+# rather than "mdbook build" from inside the doc/ directory.
+# We choose the former because our "Build Book" Github workflow runs "mdbook build doc."
+command = "cargo run --manifest-path=doc/mdbook-metrics/Cargo.toml"
+
 [rust]
 edition = "2021"

doc/mdbook-metrics/Cargo.toml

@@ -0,0 +1,8 @@
+[package]
+name = "mdbook-kani-metrics"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+mdbook = { version = "^0.4" }
+serde_json = "1.0.132"

doc/mdbook-metrics/src/main.rs

@@ -0,0 +1,106 @@
+use mdbook::book::{Book, Chapter};
+use mdbook::errors::Error;
+use mdbook::preprocess::{CmdPreprocessor, Preprocessor, PreprocessorContext};
+use mdbook::BookItem;
+use std::{env, io, path::Path, process::Command};
+
+fn main() {
+    let mut args = std::env::args().skip(1);
+    match args.next().as_deref() {
+        Some("supports") => {
+            // Supports all renderers.
+            return;
+        }
+        Some(arg) => {
+            eprintln!("unknown argument: {arg}");
+            std::process::exit(1);
+        }
+        None => {}
+    }
+
+    if let Err(e) = handle_preprocessing() {
+        eprintln!("{}", e);
+        std::process::exit(1);
+    }
+}
+
+// Plot the Kani metrics.
+// The mdbook builder reads the postprocessed book from stdout,
+// so suppress all Command output to avoid having its output interpreted as part of the book
+fn run_kani_metrics_script() -> Result<(), Error> {
+    // This will be the absolute path to the "doc/" folder
+    let original_dir = env::current_dir()?;
+    let tools_path = original_dir.join(Path::new("doc/src/tools"));
+
+    let kani_std_analysis_path = Path::new("scripts/kani-std-analysis");
+    env::set_current_dir(kani_std_analysis_path)?;
+
+    Command::new("pip")
+        .args(&["install", "-r", "requirements.txt"])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    Command::new("python")
+        .args(&[
+            "kani_std_analysis.py",
+            "--plot-only",
+            "--plot-dir",
+            &tools_path.to_string_lossy(),
+        ])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    env::set_current_dir(&original_dir)?;
+
+    Ok(())
+}
+
+struct AddKaniGraphs;
+
+impl Preprocessor for AddKaniGraphs {
+    fn name(&self) -> &str {
+        "add-metrics"
+    }
+
+    fn run(&self, _ctx: &PreprocessorContext, mut book: Book) -> Result<Book, Error> {
+        book.for_each_mut(|item| {
+            if let BookItem::Chapter(ch) = item {
+                if ch.name == "Kani" {
+                    add_graphs(ch);
+                    return;
+                }
+            }
+        });
+        Ok(book)
+    }
+}
+
+fn add_graphs(chapter: &mut Chapter) {
+    let new_content = r#"
+## Kani Metrics
+
+Note that these metrics are for x86-64 architectures.
+
+## `core`
+![Unsafe Metrics](core_unsafe_metrics.png)
+
+![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
+
+![Safe Metrics](core_safe_metrics.png)
+"#;
+
+    chapter.content.push_str(new_content);
+}
+
+pub fn handle_preprocessing() -> Result<(), Error> {
+    run_kani_metrics_script()?;
+    let pre = AddKaniGraphs;
+    let (ctx, book) = CmdPreprocessor::parse_input(io::stdin())?;
+
+    let processed_book = pre.run(&ctx, book)?;
+    serde_json::to_writer(io::stdout(), &processed_book)?;
+
+    Ok(())
+}

doc/src/SUMMARY.md

@@ -9,7 +9,6 @@
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
 
-
 ---
 
 - [Challenges](./challenges.md)