Generate Kani Metrics

.github/workflows/book.yml

@@ -10,6 +10,7 @@ on:
     paths:
       - 'doc/**'
       - '.github/workflows/book.yml'
+      - 'scripts/kani-std-analysis/**'
 
 jobs:
   build:
@@ -18,6 +19,23 @@ 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

.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/src/SUMMARY.md

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

doc/src/metrics/kani/kani.md

@@ -0,0 +1,10 @@
+# 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)