Strip the crate prefix from scanner names to match kani list - #4903
Tianshu-Huang wants to merge 1 commit into
Conversation
github-actions
Bot
added
Z-EndToEndBenchCI
| /// Every producer of item names that a consumer joins by name (the compiler's | ||
| /// metadata and the `scanner` tool's CSVs) must go through this one function, | ||
| /// so the two never disagree. | ||
| pub fn strip_crate_prefix(name: &str, krate: &str) -> String { |
There was a problem hiding this comment.
Moved from kani_middle::strip_local_crate_prefix. The loop is unchanged, but the
signature is different. The crate name is a parameter, since this crate can't call local_crate(), and
name is now &str rather than String.
| # Names must be crate-relative, as `kani list` reports them, so the two outputs | ||
| # can be joined by name (kani#4868). The crate is `test`, so no name may start | ||
| # with `test::`. | ||
| if grep -q '^test::' *.csv; then |
There was a problem hiding this comment.
This check fails on main. The CSVs there contain test::with_for_loop, so the script prints FAIL. The expected file requires the OK line.
| /// the local crate name (rust-lang/rust#149401), and the compiler strips it with | ||
| /// this same function, so every name the scanner writes goes through here and | ||
| /// the two outputs can be joined by name (kani#4868). | ||
| pub(crate) fn item_name<T: rustc_public::CrateDef>(def: &T) -> String { |
There was a problem hiding this comment.
Every name the scanner writes goes through this function. If someone later writes name() straight to a CSV without it, the prefix comes back.
| # Names must be crate-relative, as `kani list` reports them, so the two outputs | ||
| # can be joined by name (kani#4868). The crate is `test`, so no name may start | ||
| # with `test::`. | ||
| if grep -q '^test::' *.csv; then |
There was a problem hiding this comment.
Nit: match the prefix at any path-component boundary, not only at line start, so a qualified or generic name (<test::T as test::Tr>::m, f::<test::T>) would also trip the check if test.rs ever gains one.
| if grep -q '^test::' *.csv; then | |
| if grep -qE '(^|[^[:alnum:]_:])test::' *.csv; then |
This branch has not been deployed
2 participants
Two Kani outputs disagree on the name of the same function. kani list says ptr::align_offset; the scanner's CSVs say core::ptr::align_offset. Anything that joins the two matches nothing, which is how verify-rust-std's contract metrics have read 0 since its Kani pin moved past rust-lang/rust#149401 (model-checking/verify-rust-std#696 works around it on that side).
The cause is one-sided: that rustc change made def_path_str carry the crate prefix, kani-compiler compensates with strip_local_crate_prefix, and tools/scanner calls name() directly and inherited the prefix.
The fix: the function moves to kani_metadata, which both crates already can depend on, and the scanner routes every name it writes through it. strip_local_crate_prefix stays as a one-line wrapper, so none of its callers change.
The six cases from #696's review are pinned as unit tests in kani_metadata, including the two non-idempotent ones. The scanner test now checks that no CSV name starts with test::; on main it prints test::with_for_loop and fails, with this change it passes. The list, cargo_autoharness_filter, and stubbing suites pass locally; clippy and rustfmt clean.
Resolves #4868
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.