Skip to content

Commit 0db37ee

Browse files
committed
Strip the crate prefix from scanner function names so contract metrics match again
1 parent 67dfd8c commit 0db37ee

1 file changed

Lines changed: 26 additions & 0 deletions

File tree

‎scripts/kani-std-analysis/kani_std_analysis.py‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,31 @@ def str_to_bool(string: str):
3838
sys.exit(1)
3939

4040

41+
# Scanner names are crate-prefixed (`core::ptr::align_offset`) since rust-lang/rust#149401;
42+
# `kani list` names are not (`ptr::align_offset`). Strip the prefix so they match again, but
43+
# only where `<crate>::` is a path qualifier, never a continuation segment (like Kani does).
44+
def strip_crate_prefix(name: str, crate: str) -> str:
45+
needle = f"{crate}::"
46+
if needle not in name:
47+
return name
48+
out = []
49+
rest = name
50+
prev = None
51+
while True:
52+
at_qualifier = prev is None or (not prev.isalnum() and prev not in "_:")
53+
if at_qualifier and rest.startswith(needle):
54+
rest = rest[len(needle):]
55+
prev = ":"
56+
continue
57+
if not rest:
58+
break
59+
ch = rest[0]
60+
out.append(ch)
61+
prev = ch
62+
rest = rest[1:]
63+
return "".join(out)
64+
65+
4166
# Process the results from Kani's std-analysis.sh script for each crate.
4267
class GenericSTDMetrics():
4368
def __init__(self, results_dir, crate):
@@ -89,6 +114,7 @@ def read_scan_functions(self):
89114
if len(row) >= 5:
90115
name, is_unsafe, has_unsafe_ops = row[0], row[1], row[2]
91116
has_unsupported_input, has_loop = row[3], row[4]
117+
name = strip_crate_prefix(name, self.crate)
92118
# An unsafe function is a function for which is_unsafe=true
93119
if str_to_bool(is_unsafe):
94120
self.unsafe_fns.append(name)

0 commit comments

Comments
 (0)