From 90993884fd88f634bf99867b5b34a0c221de0fe2 Mon Sep 17 00:00:00 2001 From: Onyeka Obi Date: Wed, 15 Jul 2026 22:31:04 -0700 Subject: [PATCH] Attribute cfg(kani) harnesses to their crate in log_parser Standard (non-contract) Kani harnesses live inside `#[cfg(kani)] mod verify` blocks. log_parser.py deduces each such harness's target function name with a set of hand-written regexes and then looks that name up in the scanner's per-crate function tables to recover the crate. Those deduced names do not match the scanner's type-qualified names, so the lookup misses and the harness is reported with `"crate": null` in results.json. For example the harness `time::duration_verify::duration_as_nanos_panics` is mapped to the function `time::duration::as_nanos`, but the scanner records the same method as `time::Duration::as_nanos`; the two never match. Recover the crate from the harness source file instead. Harnesses live under `library//`, an unambiguous signal that does not depend on the target function name. Apply it as a fallback wherever the scanner lookup fails, for both standard and contract harnesses. The candidate is accepted only when it names a crate the scanner actually reported, so a `library/` path segment that is not a real standard-library crate (a dependency's own `library/` directory, or Kani's internal `kani_build/library/kani_core/` scaffolding) is skipped and the crate stays null instead of getting a fabricated value. The scanner reports some crate ids with underscores where the directory uses hyphens (e.g. compiler-builtins), so the directory name is normalized accordingly. Validated against the artifacts of a recent CI run: 902 previously-null harness entries (900 core, 2 alloc) are now attributed to their crate, with no change to any already-attributed entry and no field other than `crate` touched. The file-path crate agrees with the scanner's own crate on all 18438 already-attributed library entries, so the fallback is consistent with the existing attribution rather than a new heuristic. Resolves #463 Signed-off-by: Onyeka Obi --- scripts/kani-std-analysis/log_parser.py | 42 +++++++++++++++++++++++-- 1 file changed, 40 insertions(+), 2 deletions(-) diff --git a/scripts/kani-std-analysis/log_parser.py b/scripts/kani-std-analysis/log_parser.py index 32b7c7f9c1c03..8f25ffea614e0 100755 --- a/scripts/kani-std-analysis/log_parser.py +++ b/scripts/kani-std-analysis/log_parser.py @@ -52,6 +52,38 @@ import sys +# Standard-library crates live under `library//`. The directory name +# uses hyphens for some crates (e.g. `compiler-builtins`) whereas the crate +# identifier the scanner reports uses underscores. +library_crate_pattern = re.compile(r'/library/([^/]+)/') + + +def crate_from_file(file_name, known_crates): + """Best-effort mapping from a source file path to its crate name. + + Used as a fallback for the `crate` field when a harness cannot be matched + to an entry in the scanner's per-crate function tables. This happens for + manual, non-contract harnesses: there is no reliable way to recover their + target function name (see `read_kani_list`), so the scanner lookup misses + and the crate would otherwise be reported as null even though the harness + plainly lives in a known standard-library crate. + + The result is only accepted when it names a crate the scanner actually + reported (`known_crates`). A `library/` path segment that does not + correspond to a real standard-library crate (a dependency's own `library/` + directory, or Kani's internal `kani_build/library/kani_core/` scaffolding) + is skipped, so the crate stays null rather than being given a value the + rest of the pipeline never assigns. + """ + if file_name is None: + return None + for match in library_crate_pattern.finditer(file_name): + crate = match.group(1).replace('-', '_') + if crate in known_crates: + return crate + return None + + def read_scanner_results(scanner_results_dir): """Parse information produced by Kani's scanner tool.""" crate_pattern = re.compile(r'^.*/(.+)_scan_functions.csv$') @@ -93,6 +125,12 @@ def read_kani_list(kani_list_file, scanner_data): with open(kani_list_file, 'r') as f: harnesses = json.load(f) + # Crates the scanner actually reported, used to validate the file-path + # fallback in `crate_from_file`. + known_crates = {crate + for info in scanner_data.values() + for crate in info} + # There is no reasonable way to reliably deduce which function a # non-contract harness is targeting for verification, so we apply a bunch # of patterns that we know are being used. We expect that, over time, @@ -130,7 +168,7 @@ def read_kani_list(kani_list_file, scanner_data): if fn_info is None: standard_harnesses[h] = { 'file_name': file_name, - 'crate': None, + 'crate': crate_from_file(file_name, known_crates), 'function': fn, 'target_safeness': None, 'public_target': None @@ -164,7 +202,7 @@ def read_kani_list(kani_list_file, scanner_data): assert contract_harnesses.get(h) is None contract_harnesses[h] = { 'file_name': file_name, - 'crate': None, + 'crate': crate_from_file(file_name, known_crates), 'target_safeness': None, 'public_target': None }