Attribute cfg(kani) harnesses to their crate in log_parser#609
Open
MavenRain wants to merge 1 commit into
Open
Attribute cfg(kani) harnesses to their crate in log_parser#609MavenRain wants to merge 1 commit into
MavenRain wants to merge 1 commit into
Conversation
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/<crate>/`, 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 model-checking#463 Signed-off-by: Onyeka Obi <softwareengineerasaservant@isurvivable.cv>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Manual (non-contract) Kani harnesses are written inside
#[cfg(kani)] mod verifyblocks. In
results.jsonthese harnesses are reported with"crate": null, sothe dashboard cannot attribute them to a crate. This is the problem reported in
#463 (the example there is
time::duration_verify::duration_as_nanos_panics).Root cause
log_parser.pyrecovers a standard harness's crate by first deducing thetarget function name from the harness name with a set of hand-written regexes
(
harness_pattern1..6), then looking that name up in the scanner's per-cratefunction tables. The deduced names do not match the scanner's type-qualified
names, so the lookup misses and the crate falls through to
null:time::duration_verify::duration_as_nanos_panicstime::duration::as_nanostime::Duration::as_nanosnum::nonzero::verify::nonzero_check_clamp_for_u8num::nonzero::clamp_for_u8<num::nonzero::NonZero<T> as cmp::Ord>::clampAs the module docstring already notes, there is no reliable way to recover a
non-contract harness's target function from its name, so patching the regexes
cannot fix this in general. (The
--cfg=kanichange in #464 did not helpbecause the scanner already compiles and records these functions; the failure
is in name matching, not in compilation.)
Fix
Recover the crate from the harness source file instead. Harnesses live under
library/<crate>/, which is unambiguous and does not depend on the targetfunction name. A small helper
crate_from_fileextracts it (normalizing thedirectory name to the crate id, e.g.
compiler-builtinstocompiler_builtins)and uses 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. This keeps a
library/path segment that is not a realstandard-library crate (a dependency's own
library/directory, or Kani'sinternal
kani_build/library/kani_core/scaffolding) from producing afabricated crate value that the rest of the pipeline never assigns. Only the
cratefield is affected; the heuristicfunction/function_safenessfieldsare unchanged (they remain unresolved for these harnesses, so an entry can now
have a non-null
cratewith a nullfunction_safeness).Validation
I re-ran the parser against the artifacts of a recent CI run
(
kani-list.json, the scanner CSVs, andautoharness-verification.log) andcompared the output against the same run's published
results.json:results.jsonexactly (theonly difference is the ordering within multi-crate lists, which is not
affected here).
nullharness entries are attributed totheir crate (900
core, 2alloc). The Kani scanner fails to detect harnesses that are gated behind#[cfg(kani)]#463 example now reports"crate": "core".other than
cratechanged on any entry. Thejqexample in the moduledocstring returns the same count before and after (it co-filters on
function_safeness, so the newly-attributed entries are excluded from it).already-attributed
library/entries (0 disagreements), so the fallbackmatches the existing attribution rather than introducing a different rule.
The remaining
nullentries are autoharness summary rows for skippedfunctions (generic function / did not match filters / no body); these have no
associated harness or source file and are out of scope for this issue.
Resolves #463
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Drafted with AI assistance; reviewed, run against real CI artifacts, and verified by me.