Strip the crate prefix from scanner names so contract metrics match again

.github/workflows/kani.yml

@@ -256,6 +256,11 @@ jobs:
         with:
           python-version: '3.x'
 
+      - name: Test the metrics script
+        run: |
+          pip install -r scripts/kani-std-analysis/requirements.txt
+          python3 -m unittest discover -s scripts/kani-std-analysis
+
       # Step 2: Run list on the std library
       - name: Run Kani Metrics
         run: |

scripts/kani-std-analysis/kani_std_analysis.py

@@ -38,6 +38,31 @@ def str_to_bool(string: str):
             sys.exit(1)
 
 
+# Scanner names are crate-prefixed (`core::ptr::align_offset`) since rust-lang/rust#149401;
+# `kani list` names are not (`ptr::align_offset`). Strip the prefix so they match again, but
+# only where `<crate>::` is a path qualifier, never a continuation segment (like Kani does).
+def strip_crate_prefix(name: str, crate: str) -> str:
+    needle = f"{crate}::"
+    if needle not in name:
+        return name
+    out = []
+    rest = name
+    prev = None
+    while True:
+        at_qualifier = prev is None or (not prev.isalnum() and prev not in "_:")
+        if at_qualifier and rest.startswith(needle):
+            rest = rest[len(needle):]
+            prev = ":"
+            continue
+        if not rest:
+            break
+        ch = rest[0]
+        out.append(ch)
+        prev = ch
+        rest = rest[1:]
+    return "".join(out)
+
+
 # Process the results from Kani's std-analysis.sh script for each crate.
 class GenericSTDMetrics():
     def __init__(self, results_dir, crate):
@@ -89,6 +114,7 @@ def read_scan_functions(self):
                 if len(row) >= 5:
                     name, is_unsafe, has_unsafe_ops = row[0], row[1], row[2]
                     has_unsupported_input, has_loop = row[3], row[4]
+                    name = strip_crate_prefix(name, self.crate)
                     # An unsafe function is a function for which is_unsafe=true
                     if str_to_bool(is_unsafe):
                         self.unsafe_fns.append(name)

scripts/kani-std-analysis/test_kani_std_analysis.py

@@ -0,0 +1,27 @@
+import unittest
+
+from kani_std_analysis import strip_crate_prefix
+
+
+class StripCratePrefixTest(unittest.TestCase):
+    # Pinned to Kani's `strip_local_crate_prefix`: only a crate-root qualifier
+    # is dropped, a path segment that merely shares the crate's name is kept.
+    def test_matches_kani(self):
+        cases = [
+            # crate, scanner name, expected `kani list` name
+            ("core", "<char as core::ascii::AsciiExt>::is_ascii",
+             "<char as ascii::AsciiExt>::is_ascii"),
+            ("core", "core::core_simd::vector::Simd", "core_simd::vector::Simd"),
+            ("core", "ptr::align_offset", "ptr::align_offset"),
+            ("core", "alloc::vec::Vec", "alloc::vec::Vec"),
+            # Not idempotent, like Kani's copy: apply exactly once.
+            ("main", "main::main::{closure#0}", "main::{closure#0}"),
+            ("core", "core::core::foo", "core::foo"),
+        ]
+        for crate, name, expected in cases:
+            with self.subTest(name=name):
+                self.assertEqual(strip_crate_prefix(name, crate), expected)
+
+
+if __name__ == "__main__":
+    unittest.main()