make metrics a mdbook preprocessor instead

.github/workflows/book.yml

@@ -10,7 +10,6 @@ on:
     paths:
       - 'doc/**'
       - '.github/workflows/book.yml'
-      - 'scripts/kani-std-analysis/**'
 
 jobs:
   build:
@@ -19,23 +18,6 @@ jobs:
       - name: Checkout
         uses: actions/checkout@v4
 
-      - name: Set up Python
-        uses: actions/setup-python@v4
-        with:
-          python-version: '3.x'
-
-      - name: Install Python dependencies
-        run: |
-          python -m pip install --upgrade pip
-          pip install -r scripts/kani-std-analysis/requirements.txt
-
-      - name: Generate Metrics Graphs
-        run: |
-          cd scripts/kani-std-analysis/
-          python kani_std_analysis.py --plot-only
-          cd ../..
-          mv scripts/kani-std-analysis/*.png doc/src/metrics/kani/
-
       - name: Install mdbook
         run: |
           cargo install mdbook --version "^0.4" --locked

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,9 +9,6 @@
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
 
-- [Metrics](./metrics.md)
-  - [Kani](./metrics/kani/kani.md)
-
 ---
 
 - [Challenges](./challenges.md)

scripts/kani-std-analysis/kani_std_analysis.py

@@ -9,6 +9,7 @@
 import matplotlib.pyplot as plt
 import matplotlib.dates as mdates
 from matplotlib.ticker import FixedLocator
+import os
 
 # Output metrics about Kani's application to the standard library by:
 #   1. Postprocessing results from running `kani list`, which collects data about Kani harnesses and contracts.
@@ -239,7 +240,7 @@ def compute_metrics(self, kani_list_filepath, analysis_results_dir):
         print(f"Wrote metrics data for date {self.date} to {self.metrics_file}")    
 
     # Make a single plot with specified data, title, and filename
-    def plot_single(self, data, title, outfile):
+    def plot_single(self, data, title, filename, plot_dir):
         plt.figure(figsize=(14, 8))
 
         colors = ['#1f77b4', '#ff7f0e', '#2ca02c', '#d62728', '#946F7bd', '#8c564b', '#e377c2', '#7f7f7f', '#bcbd22', '#17becf']
@@ -271,15 +272,17 @@ def plot_single(self, data, title, outfile):
         plt.tight_layout()
         plt.legend(bbox_to_anchor=(1.05, 1), loc='upper left')
 
+        outfile = os.path.join(plot_dir, filename)
+
         plt.savefig(outfile, bbox_inches='tight', dpi=300)
         plt.close()
 
         print(f"PNG graph generated: {outfile}")
 
-    def plot(self):
-        self.plot_single(self.unsafe_plot_data, title="Contracts on Unsafe Functions in core", outfile="core_unsafe_metrics.png")
-        self.plot_single(self.safe_abstr_plot_data, title="Contracts on Safe Abstractions in core", outfile="core_safe_abstractions_metrics.png")
-        self.plot_single(self.safe_plot_data, title="Contracts on Safe Functions in core", outfile="core_safe_metrics.png")
+    def plot(self, plot_dir):
+        self.plot_single(self.unsafe_plot_data, title="Contracts on Unsafe Functions in core", filename="core_unsafe_metrics.png", plot_dir=plot_dir)
+        self.plot_single(self.safe_abstr_plot_data, title="Contracts on Safe Abstractions in core", filename="core_safe_abstractions_metrics.png", plot_dir=plot_dir)
+        self.plot_single(self.safe_plot_data, title="Contracts on Safe Functions in core", filename="core_safe_metrics.png", plot_dir=plot_dir)
 
 def main():
     parser = argparse.ArgumentParser(description="Generate metrics about Kani's application to the standard library.")
@@ -299,12 +302,16 @@ def main():
     parser.add_argument('--plot-only', 
                     action='store_true',
                     help="Instead of computing the metrics, just read existing metrics from --metrics-file and plot the results.")
+    parser.add_argument('--plot-dir',
+                        default=".",
+                        help="Path to the folder where the plots should be saved (default: current directory). Only used if --plot-only is provided.")
+
     args = parser.parse_args()
 
     metrics = KaniSTDMetricsOverTime(args.metrics_file)
 
     if args.plot_only:
-        metrics.plot()
+        metrics.plot(args.plot_dir)
     else:
         metrics.compute_metrics(args.kani_list_file, args.analysis_results_dir)