update metrics to update x86-only harnesses; ignore kani-list.json

.gitignore

@@ -45,7 +45,7 @@ package-lock.json
 # Tools
 ## Kani
 *.out
-
+kani-list.*
 
 # Added by cargo
 #

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)

metrics-data.json → 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
     }
   ]
 }

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
 }