Metrics test

.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

@@ -46,7 +46,6 @@ package-lock.json
 ## Kani
 *.out
 
-
 # Added by cargo
 #
 # already existing elements were commented out

doc/book.toml

@@ -19,5 +19,8 @@ runnable = false
 
 [output.linkcheck]
 
+[preprocessor.metrics]
+command = "cargo run --manifest-path=mdbook-metrics/Cargo.toml --locked"
+
 [rust]
 edition = "2021"

doc/mdbook-metrics/.gitignore

@@ -0,0 +1 @@
+target

doc/mdbook-metrics/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "mdbook-kani-metrics"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+mdbook = { version = "^0.4" }
+pulldown-cmark = { version = "0.12.2", default-features = false }
+pulldown-cmark-to-cmark = "18.0.0"
+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("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)

doc/src/metrics.md

@@ -0,0 +1,3 @@
+# Metrics
+
+Each approved tool can (optionally) publish metrics here about how their tool has been applied to the effort thus far.