From 5a04e6ec52b9039935c745b778d1a5f70586aa76 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 09:59:24 -0500
Subject: [PATCH 01/17] Add metrics collection to run-kani script

---
 .github/workflows/kani-metrics.yml            |  41 +++
 metrics-data.json                             |  28 ++
 .../kani-std-analysis/kani_std_analysis.py    | 273 ++++++++++++++++++
 scripts/kani-std-analysis/requirements.txt    |   1 +
 scripts/run-kani.sh                           |  19 +-
 5 files changed, 359 insertions(+), 3 deletions(-)
 create mode 100644 .github/workflows/kani-metrics.yml
 create mode 100644 metrics-data.json
 create mode 100755 scripts/kani-std-analysis/kani_std_analysis.py
 create mode 100644 scripts/kani-std-analysis/requirements.txt

diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml
new file mode 100644
index 0000000000000..1be3da1c2de5f
--- /dev/null
+++ b/.github/workflows/kani-metrics.yml
@@ -0,0 +1,41 @@
+name: Kani Metrics Update
+
+on:
+  schedule:
+    - cron: '0 0 1,15 * *'  # Run on the 1st and 15th of every month
+  workflow_dispatch:
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  update-kani-metrics:
+    runs-on: ubuntu-latest
+    
+    steps:
+    - name: Checkout Repository
+      uses: actions/checkout@v4
+    
+    # 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: head//scripts/run-kani.sh --run metrics
+
+    - name: Create Pull Request
+      uses: peter-evans/create-pull-request@v7
+      with:
+        token: ${{ secrets.GITHUB_TOKEN }}
+        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
\ No newline at end of file
diff --git a/metrics-data.json b/metrics-data.json
new file mode 100644
index 0000000000000..9e9aceefc0b7f
--- /dev/null
+++ b/metrics-data.json
@@ -0,0 +1,28 @@
+{
+  "results": [
+    {
+      "date": "2024-12-01",
+      "total_unsafe_fns": 4552,
+      "total_safe_abstractions": 1748,
+      "unsafe_fns_under_contract": 109,
+      "verified_unsafe_fns_under_contract": 99,
+      "safe_abstractions_under_contract": 40,
+      "verified_safe_abstractions_under_contract": 40,
+      "safe_fns_under_contract": 18,
+      "verified_safe_fns_under_contract": 18,
+      "total_functions_under_contract": 167
+    },
+    {
+      "date": "2025-01-01",
+      "total_unsafe_fns": 4552,
+      "total_safe_abstractions": 1748,
+      "unsafe_fns_under_contract": 143,
+      "verified_unsafe_fns_under_contract": 132,
+      "safe_abstractions_under_contract": 41,
+      "verified_safe_abstractions_under_contract": 41,
+      "safe_fns_under_contract": 39,
+      "verified_safe_fns_under_contract": 38,
+      "total_functions_under_contract": 223
+    }
+  ]
+}
\ No newline at end of file
diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
new file mode 100755
index 0000000000000..62a40d7362a0d
--- /dev/null
+++ b/scripts/kani-std-analysis/kani_std_analysis.py
@@ -0,0 +1,273 @@
+#!/usr/bin/env python3
+
+import argparse
+from collections import defaultdict
+import csv
+import json
+import sys
+from datetime import datetime
+import matplotlib.pyplot as plt
+import matplotlib.dates as mdates
+from matplotlib.ticker import FixedLocator
+
+# 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.
+#   2. Postprocessing results from std-analysis.sh, which outputs metrics about the standard library unrelated to Kani (e.g., a list of the functions in each crate).
+#   3. Comparing the output of steps #1 and #2 to compare the Kani-verified portion of the standard library to the overall library,
+#      e.g., what fraction of unsafe functions have Kani contracts.
+# Note that this script assumes that std-analysis.sh and `kani list` have already run, since we expect to invoke this script from `run-kani.sh`.
+
+# Process the results from Kani's std-analysis.sh script for each crate.
+# TODO For now, we just handle "core", but we should process all crates in the library.
+class GenericSTDMetrics():
+    def __init__(self):
+        self.results_directory = "/tmp/std_lib_analysis/results"
+        self.unsafe_fns_count = 0
+        self.safe_abstractions_count = 0
+        self.unsafe_fns = []
+        self.safe_abstractions = []
+
+        self.read_std_analysis()
+        
+    # Read {crate}_overall_counts.csv
+    # and return the number of unsafe functions and safe abstractions
+    def read_overall_counts(self):
+        file_path = f"{self.results_directory}/core_scan_overall.csv"
+        with open(file_path, 'r') as f:
+            csv_reader = csv.reader(f, delimiter=';')
+            counts = {row[0]: int(row[1]) for row in csv_reader if len(row) >= 2}
+        self.unsafe_fns_count = counts.get('unsafe_fns', 0)
+        self.safe_abstractions_count = counts.get('safe_abstractions', 0)
+
+    # Read {crate}_scan_functions.csv
+    # and return an array of the unsafe functions and the safe abstractions
+    def read_scan_functions(self):
+        expected_header_start = "name;is_unsafe;has_unsafe_ops"
+        file_path = f"{self.results_directory}/core_scan_functions.csv"
+
+        with open(file_path, 'r') as f:
+            csv_reader = csv.reader(f, delimiter=';', quotechar='"')
+            
+            # The row parsing logic below assumes the column structure in expected_header_start,
+            # so assert that is how the header begins before continuing
+            header = next(csv_reader)
+            header_str = ';'.join(header[:3])
+            if not header_str.startswith(expected_header_start):
+                print(f"Error: Unexpected CSV header in {file_path}")
+                print(f"Expected header to start with: {expected_header_start}")
+                print(f"Actual header: {header_str}")
+                sys.exit(1)
+
+            for row in csv_reader:
+                if len(row) >= 3:
+                    name, is_unsafe, has_unsafe_ops = row[0], row[1], row[2]
+                    # An unsafe function is a function for which is_unsafe=true
+                    if is_unsafe.strip() == "true":
+                        self.unsafe_fns.append(name)
+                    # A safe abstraction is a function that is not unsafe (is_unsafe=false) but has unsafe ops
+                    elif is_unsafe.strip() == "false" and has_unsafe_ops.strip() == "true":
+                        self.safe_abstractions.append(name)
+
+    def read_std_analysis(self):
+        self.read_overall_counts()
+        self.read_scan_functions()
+
+        # Sanity checks for the CSV parsing
+        if len(self.unsafe_fns) != self.unsafe_fns_count:
+            print(f"Number of unsafe functions does not match core_scan_functions.csv")
+            print(f"UNSAFE_FNS_COUNT: {self.unsafe_fns_count}")
+            print(f"UNSAFE_FNS length: {len(self.unsafe_fns)}")
+            sys.exit(1)
+
+        if len(self.safe_abstractions) != self.safe_abstractions_count:
+            print(f"Number of safe abstractions does not match core_scan_functions.csv")
+            print(f"SAFE_ABSTRACTIONS_COUNT: {self.safe_abstractions_count}")
+            print(f"SAFE_ABSTRACTIONS length: {len(self.safe_abstractions)}")
+            sys.exit(1)
+
+# Process the results of running `kani list` against the standard library,
+# i.e., the Kani STD metrics for a single date (whichever day this script is running).
+class KaniListSTDMetrics():
+    def __init__(self, kani_list_filepath):
+        self.total_fns_under_contract = 0
+        # List of (fn, has_harnesses) tuples, where fn is a function under contract and has_harnesses=true iff the contract has at least one harness
+        self.fns_under_contract = []
+        self.expected_kani_list_version = "0.1"
+
+        self.read_kani_list_data(kani_list_filepath)
+
+    def read_kani_list_data(self, kani_list_filepath):
+        try:
+            with open(kani_list_filepath, 'r') as f:
+                kani_list_data = json.load(f)
+        except FileNotFoundError:
+            print(f"Kani list JSON file not found.")
+            sys.exit(1)
+        
+        if kani_list_data.get("file-version") != self.expected_kani_list_version:
+            print(f"Kani list JSON file version does not match expected version {self.expected_kani_list_version}")
+            sys.exit(1)
+
+        for contract in kani_list_data.get('contracts', []):
+            func_under_contract = contract.get('function', '')
+            has_harnesses = len(contract.get('harnesses', [])) > 0
+            self.fns_under_contract.append((func_under_contract, has_harnesses))
+
+        self.total_fns_under_contract = kani_list_data.get('totals', {}).get('functions-under-contract', 0)
+
+# Generate metrics about Kani's application to the standard library over time
+# by reading past metrics from metrics_file, then computing today's metrics.
+class KaniSTDMetricsOverTime():
+    def __init__(self, metrics_file):
+        self.dates = []
+        self.unsafe_metrics = ['total_unsafe_fns', 'unsafe_fns_under_contract', 'verified_unsafe_fns_under_contract']
+        self.safe_abstr_metrics = ['total_safe_abstractions', 'safe_abstractions_under_contract', 'verified_safe_abstractions_under_contract']
+        # Generate two plots per crate: one with metrics about unsafe functions, and one with metrics about safe abstractions.
+        # The keys in these dictionaries are unsafe_metrics and safe_abstr_metrics, respectively; see update_plot_metrics()
+        self.unsafe_plot_data = defaultdict(list)
+        self.safe_abstr_plot_data = defaultdict(list)
+
+        self.date = datetime.today().date()
+        self.metrics_file = metrics_file
+
+        self.read_historical_data()
+
+    # Read historical data from self.metrics_file and initialize the date range.    
+    def read_historical_data(self):
+        try:
+            with open(self.metrics_file, 'r') as f:
+                all_data = json.load(f)["results"]
+                self.update_plot_metrics(all_data)
+        except FileNotFoundError:
+            all_data = {}
+        
+        self.dates = [datetime.strptime(data["date"], '%Y-%m-%d').date() for data in all_data]
+        self.dates.append(self.date)
+        
+        print(f"Dates are {self.dates}\n")
+    
+    # TODO For now, we don't plot how many of the contracts have been verified, since the line overlaps with how many are under contract.
+    # If we want to plot this data, we should probably generate separate plots.
+    # Update the plot data with the provided data.
+    def update_plot_metrics(self, all_data):
+        for data in all_data:
+            for metric in self.unsafe_metrics:
+                if not metric.startswith("verified"):
+                    self.unsafe_plot_data[metric].append(data[metric])
+        
+            for metric in self.safe_abstr_metrics:
+                if not metric.startswith("verified"):
+                    self.safe_abstr_plot_data[metric].append(data[metric])
+
+    # Read output from kani list and std-analysis.sh, then compare their outputs to compute Kani-specific metrics
+    # and write the results to {self.metrics_file}
+    def compute_metrics(self, kani_list_filepath):
+        # Process the `kani list` and `std-analysis.sh` data
+        kani_data = KaniListSTDMetrics(kani_list_filepath)
+        generic_metrics = GenericSTDMetrics()
+
+        print("Comparing kani-list output to std-analysis.sh output and computing metrics...")
+
+        (unsafe_fns_under_contract, verified_unsafe_fns_under_contract) = (0, 0)
+        (safe_abstractions_under_contract, verified_safe_abstractions_under_contract) = (0, 0)
+        (safe_fns_under_contract, verified_safe_fns_under_contract) = (0, 0)
+
+        for (func_under_contract, has_harnesses) in kani_data.fns_under_contract:
+            if func_under_contract in generic_metrics.unsafe_fns:
+                unsafe_fns_under_contract += 1
+                if has_harnesses:
+                    verified_unsafe_fns_under_contract += 1
+            elif func_under_contract in generic_metrics.safe_abstractions:
+                safe_abstractions_under_contract += 1
+                if has_harnesses:
+                    verified_safe_abstractions_under_contract += 1
+            else:
+                safe_fns_under_contract += 1
+                if has_harnesses:
+                    verified_safe_fns_under_contract += 1
+
+        data = {
+            "date": self.date,
+            "total_unsafe_fns": generic_metrics.unsafe_fns_count,
+            "total_safe_abstractions": generic_metrics.safe_abstractions_count,
+            "unsafe_fns_under_contract": unsafe_fns_under_contract,
+            "verified_unsafe_fns_under_contract": verified_unsafe_fns_under_contract,
+            "safe_abstractions_under_contract": safe_abstractions_under_contract,
+            "verified_safe_abstractions_under_contract": verified_safe_abstractions_under_contract,
+            "safe_fns_under_contract": safe_fns_under_contract,
+            "verified_safe_fns_under_contract": verified_safe_fns_under_contract,
+            "total_functions_under_contract": kani_data.total_fns_under_contract,
+        }
+
+        self.update_plot_metrics([data])
+
+        # Update self.metrics_file so that these results are included in our historical data for next time
+        with open(self.metrics_file, 'r') as f:
+            content = json.load(f)
+            content["results"].append(data)
+        
+        with open(self.metrics_file, 'w') as f:
+            json.dump(content, f, indent=2, default=str)
+        
+        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):
+        plt.figure(figsize=(14, 8))
+
+        colors = ['#1f77b4', '#ff7f0e', '#2ca02c', '#d62728', '#946F7bd', '#8c564b', '#e377c2', '#7f7f7f', '#bcbd22', '#17becf']
+        
+        for i, (metric, values) in enumerate(data.items()):
+            color = colors[i % len(colors)]
+            plt.plot(self.dates, values, 'o-', color=color, label=metric, markersize=6)
+            
+            # Mark each point on the line with the y value
+            for x, y in zip(self.dates, values):
+                plt.annotate(str(y), 
+                            (mdates.date2num(x), y), 
+                            xytext=(0, 5), 
+                            textcoords='offset points',
+                            ha='center', 
+                            va='bottom',
+                            color=color,
+                            fontweight='bold')
+
+        plt.title(title)
+        plt.xlabel("Date")
+        plt.ylabel("Count")
+        
+        # Set x-axis to only show ticks for the dates we have
+        plt.gca().xaxis.set_major_locator(FixedLocator(mdates.date2num(self.dates)))
+        plt.gca().xaxis.set_major_formatter(mdates.DateFormatter('%Y-%m-%d'))
+        
+        plt.gcf().autofmt_xdate()
+        plt.tight_layout()
+        plt.legend(bbox_to_anchor=(1.05, 1), loc='upper left')
+        
+        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_std_lib_metrics.png")
+        self.plot_single(self.safe_abstr_plot_data, title="Contracts on Safe Abstractions in core", outfile="core_safe_abstractions_std_lib_metrics.png")
+
+def main():
+    parser = argparse.ArgumentParser(description="Generate metrics about Kani's application to the standard library.")
+    parser.add_argument('--metrics-file', 
+                        type=str, 
+                        required=True, 
+                        help="Path to the JSON file containing metrics data")
+    parser.add_argument('--kani-list-file', 
+                        type=str, 
+                        required=True, 
+                        help="Path to the JSON file containing the Kani list data")
+    args = parser.parse_args()
+
+    metrics = KaniSTDMetricsOverTime(args.metrics_file)
+    metrics.compute_metrics(args.kani_list_file)
+    metrics.plot()
+
+if __name__ == "__main__":
+    main()
\ No newline at end of file
diff --git a/scripts/kani-std-analysis/requirements.txt b/scripts/kani-std-analysis/requirements.txt
new file mode 100644
index 0000000000000..4b43f7e68658e
--- /dev/null
+++ b/scripts/kani-std-analysis/requirements.txt
@@ -0,0 +1 @@
+matplotlib
\ No newline at end of file
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 72aa8ef176056..06a377cb54c79 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -7,7 +7,7 @@ usage() {
     echo "Options:"
     echo "  -h, --help         Show this help message"
     echo "  -p, --path <path>  Optional: Specify a path to a copy of the std library. For example, if you want to run the script from an outside directory."
-    echo "  --run <verify-std|list>  Optional: Specify whether to run 'verify-std' or 'list' command. Defaults to 'verify-std' if not specified."
+    echo "  --run <verify-std|list|metrics>  Optional: Specify whether to run the 'kani verify-std' command, 'kani list' command, or collect Kani-specific metrics. Defaults to 'verify-std' if not specified."
     echo "  --kani-args  <command arguments to kani>  Optional: Arguments to pass to the command. Simply pass them in the same way you would to the Kani binary. This should be the last argument."
     exit 1
 }
@@ -34,11 +34,11 @@ while [[ $# -gt 0 ]]; do
             fi
             ;;
         --run)
-            if [[ -n $2 && ($2 == "verify-std" || $2 == "list") ]]; then
+            if [[ -n $2 && ($2 == "verify-std" || $2 == "list" || $2 == "metrics") ]]; then
                 run_command=$2
                 shift 2
             else
-                echo "Error: Invalid run command. Must be 'verify-std' or 'list'."
+                echo "Error: Invalid run command. Must be 'verify-std', 'list', or 'metrics'."
                 usage
             fi
             ;;
@@ -296,6 +296,19 @@ main() {
     elif [[ "$run_command" == "list" ]]; then
         echo "Running Kani list command..."
         "$kani_path" list -Z list $unstable_args ./library --std --format markdown
+    elif [[ "$run_command" == "metrics" ]]; then
+        local current_dir=$(pwd)
+        echo "Computing Kani-specific metrics..."
+        echo "Running Kani list command..."
+        "$kani_path" list -Z list $unstable_args ./library --std --format json
+        echo "Running Kani's std-analysis command..."
+        pushd $build_dir
+        ./scripts/std-analysis.sh
+        popd
+        pushd scripts/kani-std-analysis
+        pip install -r requirements.txt
+        ./kani_std_analysis.py --metrics-file ${current_dir}/metrics-data.json --kani-list-file ${current_dir}/kani-list.json
+        popd
     fi
 }
 

From b86fd5c380fc78371f9869ef58b0013a2d356053 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 10:16:58 -0500
Subject: [PATCH 02/17] fix file not found in workflow

---
 .github/workflows/kani-metrics.yml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml
index 1be3da1c2de5f..9d2c157441fd3 100644
--- a/.github/workflows/kani-metrics.yml
+++ b/.github/workflows/kani-metrics.yml
@@ -16,6 +16,9 @@ jobs:
     steps:
     - name: Checkout Repository
       uses: actions/checkout@v4
+      with:
+        path: head
+        submodules: true
     
     # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
     - name: Set up Python
@@ -24,7 +27,7 @@ jobs:
         python-version: '3.x'
 
     - name: Compute Kani Metrics
-      run: head//scripts/run-kani.sh --run metrics
+      run: head/scripts/run-kani.sh --run metrics
 
     - name: Create Pull Request
       uses: peter-evans/create-pull-request@v7
@@ -38,4 +41,4 @@ jobs:
           The metrics have been updated by running `./scripts/run-kani.sh --run metrics`.
         branch: update-kani-metrics
         delete-branch: true
-        base: main
\ No newline at end of file
+        base: main

From 648e6edb5903bfb23a63e04e1e9669fad889af6c Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 10:20:35 -0500
Subject: [PATCH 03/17] try passing --path to fix tool_config file not found

---
 .github/workflows/kani-metrics.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml
index 9d2c157441fd3..ec02d40de7f90 100644
--- a/.github/workflows/kani-metrics.yml
+++ b/.github/workflows/kani-metrics.yml
@@ -27,7 +27,7 @@ jobs:
         python-version: '3.x'
 
     - name: Compute Kani Metrics
-      run: head/scripts/run-kani.sh --run metrics
+      run: head/scripts/run-kani.sh --run metrics --path ${{github.workspace}}/head
 
     - name: Create Pull Request
       uses: peter-evans/create-pull-request@v7

From 320f6680b0896479839484d02b23fb852c914b92 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 10:52:44 -0500
Subject: [PATCH 04/17] try removing path: head to fix PR creation job

---
 .github/workflows/kani-metrics.yml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml
index ec02d40de7f90..e43e839db247e 100644
--- a/.github/workflows/kani-metrics.yml
+++ b/.github/workflows/kani-metrics.yml
@@ -17,7 +17,6 @@ jobs:
     - name: Checkout Repository
       uses: actions/checkout@v4
       with:
-        path: head
         submodules: true
     
     # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
@@ -27,12 +26,11 @@ jobs:
         python-version: '3.x'
 
     - name: Compute Kani Metrics
-      run: head/scripts/run-kani.sh --run metrics --path ${{github.workspace}}/head
+      run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
 
     - name: Create Pull Request
       uses: peter-evans/create-pull-request@v7
       with:
-        token: ${{ secrets.GITHUB_TOKEN }}
         commit-message: Update Kani metrics
         title: 'Update Kani Metrics'
         body: |

From 93676cdd44af9da216e50129bc76e8bf93c5dea0 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 14:37:56 -0500
Subject: [PATCH 05/17] ignore kani-list.json

---
 .gitignore | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.gitignore b/.gitignore
index 5bfc180d4d58e..23e9ce434bad4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -45,7 +45,7 @@ package-lock.json
 # Tools
 ## Kani
 *.out
-
+kani-list.*
 
 # Added by cargo
 #

From f5a4899c790d053b07585592b771cf4e34855024 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 14:38:38 -0500
Subject: [PATCH 06/17] only run on Ubuntu

---
 metrics-data.json                             | 28 -------------------
 .../kani-std-analysis/kani_std_analysis.py    | 14 ++++++----
 scripts/kani-std-analysis/metrics-data.json   | 16 +++++++++++
 scripts/run-kani.sh                           |  4 +--
 4 files changed, 26 insertions(+), 36 deletions(-)
 delete mode 100644 metrics-data.json
 create mode 100644 scripts/kani-std-analysis/metrics-data.json

diff --git a/metrics-data.json b/metrics-data.json
deleted file mode 100644
index 9e9aceefc0b7f..0000000000000
--- a/metrics-data.json
+++ /dev/null
@@ -1,28 +0,0 @@
-{
-  "results": [
-    {
-      "date": "2024-12-01",
-      "total_unsafe_fns": 4552,
-      "total_safe_abstractions": 1748,
-      "unsafe_fns_under_contract": 109,
-      "verified_unsafe_fns_under_contract": 99,
-      "safe_abstractions_under_contract": 40,
-      "verified_safe_abstractions_under_contract": 40,
-      "safe_fns_under_contract": 18,
-      "verified_safe_fns_under_contract": 18,
-      "total_functions_under_contract": 167
-    },
-    {
-      "date": "2025-01-01",
-      "total_unsafe_fns": 4552,
-      "total_safe_abstractions": 1748,
-      "unsafe_fns_under_contract": 143,
-      "verified_unsafe_fns_under_contract": 132,
-      "safe_abstractions_under_contract": 41,
-      "verified_safe_abstractions_under_contract": 41,
-      "safe_fns_under_contract": 39,
-      "verified_safe_fns_under_contract": 38,
-      "total_functions_under_contract": 223
-    }
-  ]
-}
\ No newline at end of file
diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
index 62a40d7362a0d..81c96db6cc3aa 100755
--- a/scripts/kani-std-analysis/kani_std_analysis.py
+++ b/scripts/kani-std-analysis/kani_std_analysis.py
@@ -16,6 +16,8 @@
 #   3. Comparing the output of steps #1 and #2 to compare the Kani-verified portion of the standard library to the overall library,
 #      e.g., what fraction of unsafe functions have Kani contracts.
 # Note that this script assumes that std-analysis.sh and `kani list` have already run, since we expect to invoke this script from `run-kani.sh`.
+# Also note that the results are architecture-dependent: the standard library has functions that are only present for certain architectures, 
+# and https://github.com/model-checking/verify-rust-std/pull/122 has Kani harnesses that only run on x86-64.
 
 # Process the results from Kani's std-analysis.sh script for each crate.
 # TODO For now, we just handle "core", but we should process all crates in the library.
@@ -256,13 +258,13 @@ def plot(self):
 def main():
     parser = argparse.ArgumentParser(description="Generate metrics about Kani's application to the standard library.")
     parser.add_argument('--metrics-file', 
-                        type=str, 
-                        required=True, 
-                        help="Path to the JSON file containing metrics data")
+                    type=str, 
+                    default="metrics-data.json", 
+                    help="Path to the JSON file containing metrics data (default: metrics-data.json)")
     parser.add_argument('--kani-list-file', 
-                        type=str, 
-                        required=True, 
-                        help="Path to the JSON file containing the Kani list data")
+                    type=str, 
+                    default="kani-list.json", 
+                    help="Path to the JSON file containing the Kani list data (default: kani-list.json)")
     args = parser.parse_args()
 
     metrics = KaniSTDMetricsOverTime(args.metrics_file)
diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json
new file mode 100644
index 0000000000000..855007af7958b
--- /dev/null
+++ b/scripts/kani-std-analysis/metrics-data.json
@@ -0,0 +1,16 @@
+{
+  "results": [
+    {
+      "date": "2025-01-01",
+      "total_unsafe_fns": 6987,
+      "total_safe_abstractions": 1704,
+      "unsafe_fns_under_contract": 144,
+      "verified_unsafe_fns_under_contract": 132,
+      "safe_abstractions_under_contract": 41,
+      "verified_safe_abstractions_under_contract": 41,
+      "safe_fns_under_contract": 39,
+      "verified_safe_fns_under_contract": 38,
+      "total_functions_under_contract": 224
+    }
+  ]
+}
\ No newline at end of file
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 06a377cb54c79..a86526d3fc0e1 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -297,17 +297,17 @@ main() {
         echo "Running Kani list command..."
         "$kani_path" list -Z list $unstable_args ./library --std --format markdown
     elif [[ "$run_command" == "metrics" ]]; then
-        local current_dir=$(pwd)
         echo "Computing Kani-specific metrics..."
         echo "Running Kani list command..."
         "$kani_path" list -Z list $unstable_args ./library --std --format json
+        mv $(pwd)/kani-list.json scripts/kani-std-analysis/kani-list.json
         echo "Running Kani's std-analysis command..."
         pushd $build_dir
         ./scripts/std-analysis.sh
         popd
         pushd scripts/kani-std-analysis
         pip install -r requirements.txt
-        ./kani_std_analysis.py --metrics-file ${current_dir}/metrics-data.json --kani-list-file ${current_dir}/kani-list.json
+        ./kani_std_analysis.py
         popd
     fi
 }

From df2e643b1a343f7e9993192730f99d8e9bdf9218 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 15:49:28 -0500
Subject: [PATCH 07/17] Plot safe functions (which includes safe abstractions)

---
 .../kani-std-analysis/kani_std_analysis.py    | 38 ++++++++++++++-----
 scripts/kani-std-analysis/metrics-data.json   |  5 ++-
 2 files changed, 32 insertions(+), 11 deletions(-)

diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
index 81c96db6cc3aa..3dfbd9d7213b0 100755
--- a/scripts/kani-std-analysis/kani_std_analysis.py
+++ b/scripts/kani-std-analysis/kani_std_analysis.py
@@ -26,8 +26,10 @@ def __init__(self):
         self.results_directory = "/tmp/std_lib_analysis/results"
         self.unsafe_fns_count = 0
         self.safe_abstractions_count = 0
+        self.safe_fns_count = 0
         self.unsafe_fns = []
         self.safe_abstractions = []
+        self.safe_fns = [] 
 
         self.read_std_analysis()
         
@@ -40,6 +42,7 @@ def read_overall_counts(self):
             counts = {row[0]: int(row[1]) for row in csv_reader if len(row) >= 2}
         self.unsafe_fns_count = counts.get('unsafe_fns', 0)
         self.safe_abstractions_count = counts.get('safe_abstractions', 0)
+        self.safe_fns_count = counts.get('safe_fns', 0)
 
     # Read {crate}_scan_functions.csv
     # and return an array of the unsafe functions and the safe abstractions
@@ -66,15 +69,18 @@ def read_scan_functions(self):
                     # An unsafe function is a function for which is_unsafe=true
                     if is_unsafe.strip() == "true":
                         self.unsafe_fns.append(name)
-                    # A safe abstraction is a function that is not unsafe (is_unsafe=false) but has unsafe ops
-                    elif is_unsafe.strip() == "false" and has_unsafe_ops.strip() == "true":
-                        self.safe_abstractions.append(name)
+                    else:
+                        assert is_unsafe.strip() == "false" # sanity check against malformed data
+                        self.safe_fns.append(name)
+                        # A safe abstraction is a safe function with unsafe ops
+                        if has_unsafe_ops.strip() == "true":
+                            self.safe_abstractions.append(name)
 
     def read_std_analysis(self):
         self.read_overall_counts()
         self.read_scan_functions()
 
-        # Sanity checks for the CSV parsing
+        # Sanity checks
         if len(self.unsafe_fns) != self.unsafe_fns_count:
             print(f"Number of unsafe functions does not match core_scan_functions.csv")
             print(f"UNSAFE_FNS_COUNT: {self.unsafe_fns_count}")
@@ -86,6 +92,12 @@ def read_std_analysis(self):
             print(f"SAFE_ABSTRACTIONS_COUNT: {self.safe_abstractions_count}")
             print(f"SAFE_ABSTRACTIONS length: {len(self.safe_abstractions)}")
             sys.exit(1)
+        
+        if len(self.safe_fns) != self.safe_fns_count:
+            print(f"Number of safe functions does not match core_scan_functions.csv")
+            print(f"SAFE_FNS_COUNT: {self.safe_fns_count}")
+            print(f"SAFE_FNS length: {len(self.safe_fns)}")
+            sys.exit(1)
 
 # Process the results of running `kani list` against the standard library,
 # i.e., the Kani STD metrics for a single date (whichever day this script is running).
@@ -124,10 +136,11 @@ def __init__(self, metrics_file):
         self.dates = []
         self.unsafe_metrics = ['total_unsafe_fns', 'unsafe_fns_under_contract', 'verified_unsafe_fns_under_contract']
         self.safe_abstr_metrics = ['total_safe_abstractions', 'safe_abstractions_under_contract', 'verified_safe_abstractions_under_contract']
-        # Generate two plots per crate: one with metrics about unsafe functions, and one with metrics about safe abstractions.
+        self.safe_metrics = ['total_safe_fns', 'safe_fns_under_contract', 'verified_safe_fns_under_contract']
         # The keys in these dictionaries are unsafe_metrics and safe_abstr_metrics, respectively; see update_plot_metrics()
         self.unsafe_plot_data = defaultdict(list)
         self.safe_abstr_plot_data = defaultdict(list)
+        self.safe_plot_data = defaultdict(list)
 
         self.date = datetime.today().date()
         self.metrics_file = metrics_file
@@ -160,6 +173,10 @@ def update_plot_metrics(self, all_data):
             for metric in self.safe_abstr_metrics:
                 if not metric.startswith("verified"):
                     self.safe_abstr_plot_data[metric].append(data[metric])
+            
+            for metric in self.safe_metrics:
+                if not metric.startswith("verified"):
+                    self.safe_plot_data[metric].append(data[metric])
 
     # Read output from kani list and std-analysis.sh, then compare their outputs to compute Kani-specific metrics
     # and write the results to {self.metrics_file}
@@ -179,19 +196,21 @@ def compute_metrics(self, kani_list_filepath):
                 unsafe_fns_under_contract += 1
                 if has_harnesses:
                     verified_unsafe_fns_under_contract += 1
-            elif func_under_contract in generic_metrics.safe_abstractions:
+            if func_under_contract in generic_metrics.safe_abstractions:
                 safe_abstractions_under_contract += 1
                 if has_harnesses:
                     verified_safe_abstractions_under_contract += 1
-            else:
+            if func_under_contract in generic_metrics.safe_fns:
                 safe_fns_under_contract += 1
                 if has_harnesses:
                     verified_safe_fns_under_contract += 1
 
+        # Keep the keys here in sync with unsafe_metrics, safe_metrics, and safe_abstr_metrics
         data = {
             "date": self.date,
             "total_unsafe_fns": generic_metrics.unsafe_fns_count,
             "total_safe_abstractions": generic_metrics.safe_abstractions_count,
+            "total_safe_fns": generic_metrics.safe_fns_count,
             "unsafe_fns_under_contract": unsafe_fns_under_contract,
             "verified_unsafe_fns_under_contract": verified_unsafe_fns_under_contract,
             "safe_abstractions_under_contract": safe_abstractions_under_contract,
@@ -252,8 +271,9 @@ def plot_single(self, data, title, outfile):
         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_std_lib_metrics.png")
-        self.plot_single(self.safe_abstr_plot_data, title="Contracts on Safe Abstractions in core", outfile="core_safe_abstractions_std_lib_metrics.png")
+        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 main():
     parser = argparse.ArgumentParser(description="Generate metrics about Kani's application to the standard library.")
diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json
index 855007af7958b..2a3ff34d5b51c 100644
--- a/scripts/kani-std-analysis/metrics-data.json
+++ b/scripts/kani-std-analysis/metrics-data.json
@@ -4,12 +4,13 @@
       "date": "2025-01-01",
       "total_unsafe_fns": 6987,
       "total_safe_abstractions": 1704,
+      "total_safe_fns": 14666,
       "unsafe_fns_under_contract": 144,
       "verified_unsafe_fns_under_contract": 132,
       "safe_abstractions_under_contract": 41,
       "verified_safe_abstractions_under_contract": 41,
-      "safe_fns_under_contract": 39,
-      "verified_safe_fns_under_contract": 38,
+      "safe_fns_under_contract": 80,
+      "verified_safe_fns_under_contract": 79,
       "total_functions_under_contract": 224
     }
   ]

From 2397e53d801b89d1795579743927d64ca3de940c Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 17:03:25 -0500
Subject: [PATCH 08/17] add clarifying documentation about totals

---
 scripts/kani-std-analysis/kani_std_analysis.py | 13 ++++++++++---
 scripts/kani-std-analysis/metrics-data.json    |  4 ++--
 2 files changed, 12 insertions(+), 5 deletions(-)

diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
index 3dfbd9d7213b0..87e16d476ae7f 100755
--- a/scripts/kani-std-analysis/kani_std_analysis.py
+++ b/scripts/kani-std-analysis/kani_std_analysis.py
@@ -15,9 +15,16 @@
 #   2. Postprocessing results from std-analysis.sh, which outputs metrics about the standard library unrelated to Kani (e.g., a list of the functions in each crate).
 #   3. Comparing the output of steps #1 and #2 to compare the Kani-verified portion of the standard library to the overall library,
 #      e.g., what fraction of unsafe functions have Kani contracts.
-# Note that this script assumes that std-analysis.sh and `kani list` have already run, since we expect to invoke this script from `run-kani.sh`.
-# Also note that the results are architecture-dependent: the standard library has functions that are only present for certain architectures, 
-# and https://github.com/model-checking/verify-rust-std/pull/122 has Kani harnesses that only run on x86-64.
+
+# Notes:
+# - This script assumes that std-analysis.sh and `kani list` have already run, since we expect to invoke this script from `run-kani.sh`.
+# - The results are architecture-dependent: the standard library has functions that are only present for certain architectures, 
+#   and https://github.com/model-checking/verify-rust-std/pull/122 has Kani harnesses that only run on x86-64.
+# - The total functions under contract are not necessarily equal to the sum of unsafe and safe functions under contract.
+#   We've added a few functions (three, as of writing) with contracts to this fork, e.g. ffi::c_str::is_null_terminated.
+#   Since std-analysis.sh runs on the standard library given a toolchain (not this fork), it doesn't know about this function and therefore can't classify it as safe or unsafe.
+#   But `kani list` runs on this fork, so it can still see it and add it to the total functions under contract.
+# - See #TODOs for known limitations.
 
 # Process the results from Kani's std-analysis.sh script for each crate.
 # TODO For now, we just handle "core", but we should process all crates in the library.
diff --git a/scripts/kani-std-analysis/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json
index 2a3ff34d5b51c..75a71c0301483 100644
--- a/scripts/kani-std-analysis/metrics-data.json
+++ b/scripts/kani-std-analysis/metrics-data.json
@@ -9,8 +9,8 @@
       "verified_unsafe_fns_under_contract": 132,
       "safe_abstractions_under_contract": 41,
       "verified_safe_abstractions_under_contract": 41,
-      "safe_fns_under_contract": 80,
-      "verified_safe_fns_under_contract": 79,
+      "safe_fns_under_contract": 77,
+      "verified_safe_fns_under_contract": 77,
       "total_functions_under_contract": 224
     }
   ]

From 6ff62753a7e17a8d9bf435aff18057ded163cff2 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Thu, 9 Jan 2025 09:43:58 -0500
Subject: [PATCH 09/17] pass results_directory on the command line

---
 scripts/kani-std-analysis/kani_std_analysis.py | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
index 87e16d476ae7f..21ab143ae8dba 100755
--- a/scripts/kani-std-analysis/kani_std_analysis.py
+++ b/scripts/kani-std-analysis/kani_std_analysis.py
@@ -29,8 +29,8 @@
 # Process the results from Kani's std-analysis.sh script for each crate.
 # TODO For now, we just handle "core", but we should process all crates in the library.
 class GenericSTDMetrics():
-    def __init__(self):
-        self.results_directory = "/tmp/std_lib_analysis/results"
+    def __init__(self, results_dir):
+        self.results_directory = results_dir
         self.unsafe_fns_count = 0
         self.safe_abstractions_count = 0
         self.safe_fns_count = 0
@@ -187,10 +187,10 @@ def update_plot_metrics(self, all_data):
 
     # Read output from kani list and std-analysis.sh, then compare their outputs to compute Kani-specific metrics
     # and write the results to {self.metrics_file}
-    def compute_metrics(self, kani_list_filepath):
+    def compute_metrics(self, kani_list_filepath, analysis_results_dir):
         # Process the `kani list` and `std-analysis.sh` data
         kani_data = KaniListSTDMetrics(kani_list_filepath)
-        generic_metrics = GenericSTDMetrics()
+        generic_metrics = GenericSTDMetrics(analysis_results_dir)
 
         print("Comparing kani-list output to std-analysis.sh output and computing metrics...")
 
@@ -292,10 +292,15 @@ def main():
                     type=str, 
                     default="kani-list.json", 
                     help="Path to the JSON file containing the Kani list data (default: kani-list.json)")
+    # The default is /tmp/std_lib_analysis/results because, as of writing, that's always where std-analysis.sh outputs its results.
+    parser.add_argument('--analysis-results-dir', 
+                    type=str, 
+                    default="/tmp/std_lib_analysis/results", 
+                    help="Path to the folder file containing the std-analysis.sh results (default: /tmp/std_lib_analysis/results)")
     args = parser.parse_args()
 
     metrics = KaniSTDMetricsOverTime(args.metrics_file)
-    metrics.compute_metrics(args.kani_list_file)
+    metrics.compute_metrics(args.kani_list_file, args.analysis_results_dir)
     metrics.plot()
 
 if __name__ == "__main__":

From d518e96b85274f6cc6b954304aaa5c6d3ea35ad2 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Thu, 9 Jan 2025 09:44:10 -0500
Subject: [PATCH 10/17] delete kani-list.json instead of ignoring it

---
 .gitignore          | 1 -
 scripts/run-kani.sh | 7 ++++---
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/.gitignore b/.gitignore
index 23e9ce434bad4..b6d6d2aa718af 100644
--- a/.gitignore
+++ b/.gitignore
@@ -45,7 +45,6 @@ package-lock.json
 # Tools
 ## Kani
 *.out
-kani-list.*
 
 # Added by cargo
 #
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index a86526d3fc0e1..234b2fda9e0f3 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -297,18 +297,19 @@ main() {
         echo "Running Kani list command..."
         "$kani_path" list -Z list $unstable_args ./library --std --format markdown
     elif [[ "$run_command" == "metrics" ]]; then
-        echo "Computing Kani-specific metrics..."
+        local current_dir=$(pwd)
         echo "Running Kani list command..."
         "$kani_path" list -Z list $unstable_args ./library --std --format json
-        mv $(pwd)/kani-list.json scripts/kani-std-analysis/kani-list.json
         echo "Running Kani's std-analysis command..."
         pushd $build_dir
         ./scripts/std-analysis.sh
         popd
         pushd scripts/kani-std-analysis
         pip install -r requirements.txt
-        ./kani_std_analysis.py
+        echo "Computing Kani-specific metrics..."
+        ./kani_std_analysis.py --kani-list-file $current_dir/kani-list.json
         popd
+        rm kani-list.json
     fi
 }
 

From 679eaffd52206ab3bdd5381be97928a944d1b9c4 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Tue, 14 Jan 2025 09:55:08 -0500
Subject: [PATCH 11/17] update comment

---
 scripts/kani-std-analysis/kani_std_analysis.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
index 21ab143ae8dba..09bb219d899f9 100755
--- a/scripts/kani-std-analysis/kani_std_analysis.py
+++ b/scripts/kani-std-analysis/kani_std_analysis.py
@@ -144,7 +144,7 @@ def __init__(self, metrics_file):
         self.unsafe_metrics = ['total_unsafe_fns', 'unsafe_fns_under_contract', 'verified_unsafe_fns_under_contract']
         self.safe_abstr_metrics = ['total_safe_abstractions', 'safe_abstractions_under_contract', 'verified_safe_abstractions_under_contract']
         self.safe_metrics = ['total_safe_fns', 'safe_fns_under_contract', 'verified_safe_fns_under_contract']
-        # The keys in these dictionaries are unsafe_metrics and safe_abstr_metrics, respectively; see update_plot_metrics()
+        # The keys in these dictionaries are unsafe_metrics, safe_abstr_metrics, and safe_metrics, respectively; see update_plot_metrics()
         self.unsafe_plot_data = defaultdict(list)
         self.safe_abstr_plot_data = defaultdict(list)
         self.safe_plot_data = defaultdict(list)

From 65bb370e317e4878feeb8da0ec2e15f95be7f133 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Tue, 14 Jan 2025 10:24:43 -0500
Subject: [PATCH 12/17] run cronjob weekly instead

---
 .github/workflows/kani-metrics.yml             | 2 +-
 scripts/kani-std-analysis/kani_std_analysis.py | 2 +-
 scripts/kani-std-analysis/requirements.txt     | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/kani-metrics.yml b/.github/workflows/kani-metrics.yml
index e43e839db247e..84945e236a4ed 100644
--- a/.github/workflows/kani-metrics.yml
+++ b/.github/workflows/kani-metrics.yml
@@ -2,7 +2,7 @@ name: Kani Metrics Update
 
 on:
   schedule:
-    - cron: '0 0 1,15 * *'  # Run on the 1st and 15th of every month
+    - cron: '0 0 * * 0'  # Run at 00:00 UTC every Sunday
   workflow_dispatch:
 
 defaults:
diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
index 09bb219d899f9..5371ebc4b7d7a 100755
--- a/scripts/kani-std-analysis/kani_std_analysis.py
+++ b/scripts/kani-std-analysis/kani_std_analysis.py
@@ -304,4 +304,4 @@ def main():
     metrics.plot()
 
 if __name__ == "__main__":
-    main()
\ No newline at end of file
+    main()
diff --git a/scripts/kani-std-analysis/requirements.txt b/scripts/kani-std-analysis/requirements.txt
index 4b43f7e68658e..6ccafc3f904ba 100644
--- a/scripts/kani-std-analysis/requirements.txt
+++ b/scripts/kani-std-analysis/requirements.txt
@@ -1 +1 @@
-matplotlib
\ No newline at end of file
+matplotlib

From 098c031b0dd2a26d14080a9124a1a170f53fe6c6 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Tue, 14 Jan 2025 14:48:36 -0500
Subject: [PATCH 13/17] split script into computing metrics xor plotting

---
 scripts/kani-std-analysis/kani_std_analysis.py | 15 ++++++++++-----
 1 file changed, 10 insertions(+), 5 deletions(-)

diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
index 5371ebc4b7d7a..f44663ea18199 100755
--- a/scripts/kani-std-analysis/kani_std_analysis.py
+++ b/scripts/kani-std-analysis/kani_std_analysis.py
@@ -164,9 +164,6 @@ def read_historical_data(self):
             all_data = {}
         
         self.dates = [datetime.strptime(data["date"], '%Y-%m-%d').date() for data in all_data]
-        self.dates.append(self.date)
-        
-        print(f"Dates are {self.dates}\n")
     
     # TODO For now, we don't plot how many of the contracts have been verified, since the line overlaps with how many are under contract.
     # If we want to plot this data, we should probably generate separate plots.
@@ -188,6 +185,8 @@ def update_plot_metrics(self, all_data):
     # Read output from kani list and std-analysis.sh, then compare their outputs to compute Kani-specific metrics
     # and write the results to {self.metrics_file}
     def compute_metrics(self, kani_list_filepath, analysis_results_dir):
+        self.dates.append(self.date)
+
         # Process the `kani list` and `std-analysis.sh` data
         kani_data = KaniListSTDMetrics(kani_list_filepath)
         generic_metrics = GenericSTDMetrics(analysis_results_dir)
@@ -297,11 +296,17 @@ def main():
                     type=str, 
                     default="/tmp/std_lib_analysis/results", 
                     help="Path to the folder file containing the std-analysis.sh results (default: /tmp/std_lib_analysis/results)")
+    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.")
     args = parser.parse_args()
 
     metrics = KaniSTDMetricsOverTime(args.metrics_file)
-    metrics.compute_metrics(args.kani_list_file, args.analysis_results_dir)
-    metrics.plot()
+
+    if args.plot_only:
+        metrics.plot()
+    else:
+        metrics.compute_metrics(args.kani_list_file, args.analysis_results_dir)
 
 if __name__ == "__main__":
     main()

From 31aed2a8f1d9a20e3e58fef764fef425e2609116 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Thu, 16 Jan 2025 09:35:03 -0500
Subject: [PATCH 14/17] add metrics to the book

---
 .github/workflows/book.yml   | 18 ++++++++++++++++++
 doc/src/SUMMARY.md           |  2 ++
 doc/src/metrics.md           |  3 +++
 doc/src/metrics/kani/kani.md | 10 ++++++++++
 4 files changed, 33 insertions(+)
 create mode 100644 doc/src/metrics.md
 create mode 100644 doc/src/metrics/kani/kani.md

diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml
index 200068be74745..48f5a414b90bd 100644
--- a/.github/workflows/book.yml
+++ b/.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
diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
index e6b2a9c78e598..6b5a60cf43bec 100644
--- a/doc/src/SUMMARY.md
+++ b/doc/src/SUMMARY.md
@@ -9,6 +9,8 @@
 - [Verification Tools](./tools.md)
   - [Kani](./tools/kani.md)
 
+- [Metrics](./metrics.md)
+  - [Kani](./metrics/kani/kani.md)
 
 ---
 
diff --git a/doc/src/metrics.md b/doc/src/metrics.md
new file mode 100644
index 0000000000000..a3b5220635eda
--- /dev/null
+++ b/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.
\ No newline at end of file
diff --git a/doc/src/metrics/kani/kani.md b/doc/src/metrics/kani/kani.md
new file mode 100644
index 0000000000000..505b817170c86
--- /dev/null
+++ b/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)

From 864be39219127f51f4dd198a97915d340eb41edd Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Fri, 17 Jan 2025 17:53:57 -0500
Subject: [PATCH 15/17] make metrics a mdbook preprocessor instead

---
 .github/workflows/book.yml                    |  18 ---
 doc/book.toml                                 |   3 +
 doc/mdbook-metrics/.gitignore                 |   1 +
 doc/mdbook-metrics/Cargo.toml                 |  10 ++
 doc/mdbook-metrics/src/main.rs                | 106 ++++++++++++++++++
 doc/src/SUMMARY.md                            |   3 -
 doc/src/metrics/kani/kani.md                  |  10 --
 .../kani-std-analysis/kani_std_analysis.py    |  19 +++-
 8 files changed, 133 insertions(+), 37 deletions(-)
 create mode 100644 doc/mdbook-metrics/.gitignore
 create mode 100644 doc/mdbook-metrics/Cargo.toml
 create mode 100644 doc/mdbook-metrics/src/main.rs
 delete mode 100644 doc/src/metrics/kani/kani.md

diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml
index 48f5a414b90bd..200068be74745 100644
--- a/.github/workflows/book.yml
+++ b/.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
diff --git a/doc/book.toml b/doc/book.toml
index 078022e148f1f..7cf45aa2a8080 100644
--- a/doc/book.toml
+++ b/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"
diff --git a/doc/mdbook-metrics/.gitignore b/doc/mdbook-metrics/.gitignore
new file mode 100644
index 0000000000000..1de565933b05f
--- /dev/null
+++ b/doc/mdbook-metrics/.gitignore
@@ -0,0 +1 @@
+target
\ No newline at end of file
diff --git a/doc/mdbook-metrics/Cargo.toml b/doc/mdbook-metrics/Cargo.toml
new file mode 100644
index 0000000000000..2bf37c3b6dc59
--- /dev/null
+++ b/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"
diff --git a/doc/mdbook-metrics/src/main.rs b/doc/mdbook-metrics/src/main.rs
new file mode 100644
index 0000000000000..b05d753f61c16
--- /dev/null
+++ b/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(())
+}
diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
index 6b5a60cf43bec..59f08d58e63d5 100644
--- a/doc/src/SUMMARY.md
+++ b/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)
diff --git a/doc/src/metrics/kani/kani.md b/doc/src/metrics/kani/kani.md
deleted file mode 100644
index 505b817170c86..0000000000000
--- a/doc/src/metrics/kani/kani.md
+++ /dev/null
@@ -1,10 +0,0 @@
-# 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)
diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
index f44663ea18199..82050a7e1baf2 100755
--- a/scripts/kani-std-analysis/kani_std_analysis.py
+++ b/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)
 

From de5954703e1826240babfda388dad7ddb17871cd Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Fri, 17 Jan 2025 18:21:32 -0500
Subject: [PATCH 16/17] fix mdbook build error

---
 .gitignore                     | 2 ++
 doc/book.toml                  | 5 ++++-
 doc/mdbook-metrics/.gitignore  | 1 -
 doc/mdbook-metrics/Cargo.toml  | 2 --
 doc/mdbook-metrics/src/main.rs | 4 ++--
 5 files changed, 8 insertions(+), 6 deletions(-)
 delete mode 100644 doc/mdbook-metrics/.gitignore

diff --git a/.gitignore b/.gitignore
index b6d6d2aa718af..a3cdde9bde1ac 100644
--- a/.gitignore
+++ b/.gitignore
@@ -26,6 +26,8 @@ library/target
 *.rmeta
 *.mir
 Cargo.lock
+/doc/mdbook-metrics/target
+*.png
 
 ## Temporary files
 *~
diff --git a/doc/book.toml b/doc/book.toml
index 7cf45aa2a8080..9cb0a205ad086 100644
--- a/doc/book.toml
+++ b/doc/book.toml
@@ -20,7 +20,10 @@ runnable = false
 [output.linkcheck]
 
 [preprocessor.metrics]
-command = "cargo run --manifest-path=mdbook-metrics/Cargo.toml --locked"
+# 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"
diff --git a/doc/mdbook-metrics/.gitignore b/doc/mdbook-metrics/.gitignore
deleted file mode 100644
index 1de565933b05f..0000000000000
--- a/doc/mdbook-metrics/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-target
\ No newline at end of file
diff --git a/doc/mdbook-metrics/Cargo.toml b/doc/mdbook-metrics/Cargo.toml
index 2bf37c3b6dc59..ba6583c62361d 100644
--- a/doc/mdbook-metrics/Cargo.toml
+++ b/doc/mdbook-metrics/Cargo.toml
@@ -5,6 +5,4 @@ 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"
diff --git a/doc/mdbook-metrics/src/main.rs b/doc/mdbook-metrics/src/main.rs
index b05d753f61c16..cd261d241e8c1 100644
--- a/doc/mdbook-metrics/src/main.rs
+++ b/doc/mdbook-metrics/src/main.rs
@@ -30,9 +30,9 @@ fn main() {
 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 tools_path = original_dir.join(Path::new("doc/src/tools"));
 
-    let kani_std_analysis_path = Path::new("../scripts/kani-std-analysis");
+    let kani_std_analysis_path = Path::new("scripts/kani-std-analysis");
     env::set_current_dir(kani_std_analysis_path)?;
 
     Command::new("pip")

From 7ecb200abc99cb696d0ac4c2e9cd319ebc2764db Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Fri, 17 Jan 2025 18:33:39 -0500
Subject: [PATCH 17/17] delete metrics chapter from book

---
 doc/src/metrics.md | 3 ---
 1 file changed, 3 deletions(-)
 delete mode 100644 doc/src/metrics.md

diff --git a/doc/src/metrics.md b/doc/src/metrics.md
deleted file mode 100644
index a3b5220635eda..0000000000000
--- a/doc/src/metrics.md
+++ /dev/null
@@ -1,3 +0,0 @@
-# Metrics
-
-Each approved tool can (optionally) publish metrics here about how their tool has been applied to the effort thus far.
\ No newline at end of file