only run on Ubuntu

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)

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
+    }
+  ]
+}

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
 }