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 1/8] 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 0000000..1be3da1
--- /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 0000000..9e9acee
--- /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 0000000..62a40d7
--- /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 0000000..4b43f7e
--- /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 72aa8ef..06a377c 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 2/8] 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 1be3da1..9d2c157 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 3/8] 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 9d2c157..ec02d40 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 4/8] 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 ec02d40..e43e839 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 8629980114d3b29d154dbaa4152fc4e172dc2745 Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 11:54:21 -0500
Subject: [PATCH 5/8] update metrics to update x86-only harnesses; ignore
 kani-list.json

---
 .gitignore                                         |  2 +-
 scripts/kani-std-analysis/kani_std_analysis.py     | 14 ++++++++------
 .../kani-std-analysis/metrics-data.json            |  4 ++--
 scripts/run-kani.sh                                |  4 ++--
 4 files changed, 13 insertions(+), 11 deletions(-)
 rename metrics-data.json => scripts/kani-std-analysis/metrics-data.json (89%)

diff --git a/.gitignore b/.gitignore
index 5bfc180..23e9ce4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -45,7 +45,7 @@ package-lock.json
 # Tools
 ## Kani
 *.out
-
+kani-list.*
 
 # Added by cargo
 #
diff --git a/scripts/kani-std-analysis/kani_std_analysis.py b/scripts/kani-std-analysis/kani_std_analysis.py
index 62a40d7..c40e2b2 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 as of writing, we have a few Kani harnesses that only run on x86-64 architectures,
+# so if you are running this script locally on a different architecture, you will get slightly different totals than the Github workflow that runs this job 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/metrics-data.json b/scripts/kani-std-analysis/metrics-data.json
similarity index 89%
rename from metrics-data.json
rename to scripts/kani-std-analysis/metrics-data.json
index 9e9acee..dfba3f6 100644
--- a/metrics-data.json
+++ b/scripts/kani-std-analysis/metrics-data.json
@@ -10,7 +10,7 @@
       "verified_safe_abstractions_under_contract": 40,
       "safe_fns_under_contract": 18,
       "verified_safe_fns_under_contract": 18,
-      "total_functions_under_contract": 167
+      "total_functions_under_contract": 168
     },
     {
       "date": "2025-01-01",
@@ -22,7 +22,7 @@
       "verified_safe_abstractions_under_contract": 41,
       "safe_fns_under_contract": 39,
       "verified_safe_fns_under_contract": 38,
-      "total_functions_under_contract": 223
+      "total_functions_under_contract": 224
     }
   ]
 }
\ No newline at end of file
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 06a377c..a86526d 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 e8c4d9cf671e83ef1ff6a2579b79c0a8e0c3408f Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 11:57:26 -0500
Subject: [PATCH 6/8] cat files for debugging

---
 scripts/run-kani.sh | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index a86526d..975d2bb 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -304,6 +304,8 @@ main() {
         echo "Running Kani's std-analysis command..."
         pushd $build_dir
         ./scripts/std-analysis.sh
+        cat /tmp/std_lib_analysis/results/core_scan_overall.csv
+        cat /tmp/std_lib_analysis/results/core_scan_functions.csv
         popd
         pushd scripts/kani-std-analysis
         pip install -r requirements.txt

From 76972c23116361c623c46af8600c6e67ebcb4b8e Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 12:03:15 -0500
Subject: [PATCH 7/8] run generic metrics first to get output faster

---
 scripts/run-kani.sh | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh
index 975d2bb..054b949 100755
--- a/scripts/run-kani.sh
+++ b/scripts/run-kani.sh
@@ -298,15 +298,15 @@ main() {
         "$kani_path" list -Z list $unstable_args ./library --std --format markdown
     elif [[ "$run_command" == "metrics" ]]; then
         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
         cat /tmp/std_lib_analysis/results/core_scan_overall.csv
         cat /tmp/std_lib_analysis/results/core_scan_functions.csv
         popd
+        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
         pushd scripts/kani-std-analysis
         pip install -r requirements.txt
         ./kani_std_analysis.py

From 1cd69e8172d4ef459c7d2dfb5c066d47032c22de Mon Sep 17 00:00:00 2001
From: Carolyn Zech <cmzech@amazon.com>
Date: Wed, 8 Jan 2025 12:14:43 -0500
Subject: [PATCH 8/8] also run on macOS to see if the metrics differences are
 os-specific

---
 .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 e43e839..635aaf7 100644
--- a/.github/workflows/kani-metrics.yml
+++ b/.github/workflows/kani-metrics.yml
@@ -11,7 +11,7 @@ defaults:
 
 jobs:
   update-kani-metrics:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-latest, macos-latest
     
     steps:
     - name: Checkout Repository