Strip the crate prefix from scanner names to match kani list

Cargo.lock

@@ -1972,6 +1972,7 @@ version = "0.0.0"
 dependencies = [
  "csv",
  "graph-cycles",
+ "kani_metadata",
  "petgraph",
  "serde",
  "strum",

kani-compiler/src/kani_middle/mod.rs

@@ -56,48 +56,11 @@ pub fn nonnull_pointee(ty: Ty) -> Option<Ty> {
     })
 }
 
-/// Strip the local crate name from an absolute item path, restoring the
-/// crate-relative form Kani used before rust-lang/rust#149401. That change made
-/// `def_path_str` prefix the local crate name at *every* local path component,
-/// so it appears not just at the start (`my_crate::f`) but also inside
-/// qualifiers and generic args (`<my_crate::T as my_crate::Tr>::m`,
-/// `f::<my_crate::T>`). Remove `<crate>::` at each path-component boundary
-/// (start of string or after a non-identifier char) so these become `f`,
-/// `<T as Tr>::m`, `f::<T>`. Non-local paths (which begin with a different
-/// crate name) are unaffected.
+/// Strip the local crate name from an absolute item path; see
+/// [`kani_metadata::strip_crate_prefix`] for the rules. `tools/scanner` uses the
+/// same function, so its CSVs and `kani list` agree on names.
 pub fn strip_local_crate_prefix(name: String) -> String {
-    let needle = format!("{}::", local_crate().name);
-    if !name.contains(&needle) {
-        return name;
-    }
-    let mut out = String::with_capacity(name.len());
-    let mut rest = name.as_str();
-    // The previous char in the input, used to decide whether a `<crate>::` here
-    // is a crate-root *qualifier* (droppable) or a path *continuation* segment
-    // (a module/item that happens to share the crate's name, which must be
-    // kept). A qualifier appears at the start or after a type/path delimiter
-    // (`<`, `,`, ` `, `&`, `*`, `(`, `[`, ...); a continuation appears after
-    // `::`. So drop `<crate>::` only when the previous char is neither part of
-    // an identifier nor `:`. After dropping, pretend the previous char is `:`
-    // so an immediately following same-named segment is treated as a
-    // continuation (e.g. `main::main::{closure#0}` -> `main::{closure#0}`).
-    let mut prev: Option<char> = None;
-    loop {
-        let at_qualifier = match prev {
-            None => true,
-            Some(c) => !c.is_alphanumeric() && c != '_' && c != ':',
-        };
-        if at_qualifier && rest.starts_with(&needle) {
-            rest = &rest[needle.len()..];
-            prev = Some(':');
-            continue;
-        }
-        let Some(ch) = rest.chars().next() else { break };
-        out.push(ch);
-        prev = Some(ch);
-        rest = &rest[ch.len_utf8()..];
-    }
-    out
+    kani_metadata::strip_crate_prefix(&name, &local_crate().name)
 }
 
 pub mod abi;

kani_metadata/src/lib.rs

@@ -135,3 +135,85 @@ pub struct Location {
 pub struct CompilerArtifactStub {
     pub metadata_path: PathBuf,
 }
+
+/// Strip a crate's name from an absolute item path, restoring the crate-relative
+/// form Kani uses in `kani list`, harness names, and stub targets. Since
+/// rust-lang/rust#149401, `def_path_str` prefixes the local crate name at
+/// *every* local path component, so it appears not just at the start
+/// (`my_crate::f`) but also inside qualifiers and generic args
+/// (`<my_crate::T as my_crate::Tr>::m`, `f::<my_crate::T>`). Remove `<crate>::`
+/// at each path-component boundary (start of string or after a non-identifier
+/// char) so these become `f`, `<T as Tr>::m`, `f::<T>`. Paths of other crates
+/// are unaffected.
+///
+/// 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 {
+    let needle = format!("{krate}::");
+    if !name.contains(&needle) {
+        return name.to_string();
+    }
+    let mut out = String::with_capacity(name.len());
+    let mut rest = name;
+    // The previous char in the input, used to decide whether a `<crate>::` here
+    // is a crate-root *qualifier* (droppable) or a path *continuation* segment
+    // (a module/item that happens to share the crate's name, which must be
+    // kept). A qualifier appears at the start or after a type/path delimiter
+    // (`<`, `,`, ` `, `&`, `*`, `(`, `[`, ...); a continuation appears after
+    // `::`. So drop `<crate>::` only when the previous char is neither part of
+    // an identifier nor `:`. After dropping, pretend the previous char is `:`
+    // so an immediately following same-named segment is treated as a
+    // continuation (e.g. `main::main::{closure#0}` -> `main::{closure#0}`).
+    let mut prev: Option<char> = None;
+    loop {
+        let at_qualifier = match prev {
+            None => true,
+            Some(c) => !c.is_alphanumeric() && c != '_' && c != ':',
+        };
+        if at_qualifier && rest.starts_with(&needle) {
+            rest = &rest[needle.len()..];
+            prev = Some(':');
+            continue;
+        }
+        let Some(ch) = rest.chars().next() else { break };
+        out.push(ch);
+        prev = Some(ch);
+        rest = &rest[ch.len_utf8()..];
+    }
+    out
+}
+
+#[cfg(test)]
+mod tests {
+    use super::strip_crate_prefix;
+
+    /// The prefix is dropped only at a path-component boundary, including inside a
+    /// `<T as Trait>` qualifier; a segment that merely shares the crate's name stays.
+    #[test]
+    fn strips_crate_root_qualifiers_only() {
+        let cases = [
+            (
+                "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"),
+            ("my_crate", "<my_crate::T as my_crate::Tr>::m", "<T as Tr>::m"),
+            ("my_crate", "f::<my_crate::T>", "f::<T>"),
+        ];
+        for (krate, name, expected) in cases {
+            assert_eq!(strip_crate_prefix(name, krate), expected, "{name}");
+        }
+    }
+
+    /// Not idempotent, by design: a second application would eat a continuation
+    /// segment. Callers must apply it exactly once, to a raw `def_path_str`.
+    #[test]
+    fn strips_one_qualifier_per_boundary() {
+        assert_eq!(strip_crate_prefix("main::main::{closure#0}", "main"), "main::{closure#0}");
+        assert_eq!(strip_crate_prefix("core::core::foo", "core"), "core::foo");
+    }
+}

tests/script-based-pre/tool-scanner/scanner-test.expected

@@ -16,3 +16,5 @@ check_outer_coercion;1
 with_iterator;2
 current_id;0
 generic;0
+
+OK: no crate-prefixed names

tests/script-based-pre/tool-scanner/scanner-test.sh

@@ -22,5 +22,14 @@ wc -l *csv
 echo "Unsafe Distance Results"
 cat test_scan_unsafe_distance.csv
 
+# 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 -qE '(^|[^[:alnum:]_:])test::' *.csv; then
+    echo "FAIL: crate-prefixed names in the CSVs"
+else
+    echo "OK: no crate-prefixed names"
+fi
+
 popd
 rm -rf ${OUT_DIR}

tools/scanner/Cargo.toml

@@ -12,6 +12,7 @@ publish = false
 
 [dependencies]
 csv = "1.3"
+kani_metadata = { path = "../../kani_metadata" }
 serde = {version = "1", features = ["derive"]}
 strum = "0.28"
 strum_macros = "0.28"

tools/scanner/src/analysis.rs

@@ -3,7 +3,7 @@
 
 //! Provide passes that perform intra-function analysis on the crate under compilation
 
-use crate::info;
+use crate::{info, item_name};
 use csv::WriterBuilder;
 use graph_cycles::Cycles;
 use petgraph::graph::Graph;
@@ -45,7 +45,7 @@ struct FnStats {
 impl FnStats {
     fn new(fn_item: CrateItem) -> FnStats {
         FnStats {
-            name: fn_item.name(),
+            name: item_name(&fn_item),
             is_unsafe: None,
             has_unsafe_ops: None,
             has_unsupported_input: None,
@@ -127,7 +127,8 @@ impl OverallStats {
                     return None;
                 };
                 let fn_sig = kind.fn_sig().unwrap();
-                let props = FnInputProps::new(item.name()).collect(fn_sig.skip_binder().inputs());
+                let props =
+                    FnInputProps::new(item_name(&item)).collect(fn_sig.skip_binder().inputs());
                 self.fn_stats.get_mut(&item).unwrap().has_unsupported_input =
                     Some(!props.is_supported());
                 Some(props)
@@ -151,7 +152,7 @@ impl OverallStats {
                     return None;
                 };
                 let unsafe_ops =
-                    FnUnsafeOperations::new(item.name()).collect(&item.expect_body(), tcx);
+                    FnUnsafeOperations::new(item_name(&item)).collect(&item.expect_body(), tcx);
                 let fn_sig = kind.fn_sig().unwrap();
                 let is_unsafe = fn_sig.skip_binder().safety == Safety::Unsafe;
                 self.fn_stats.get_mut(&item).unwrap().has_unsafe_ops =
@@ -180,7 +181,7 @@ impl OverallStats {
                 if !kind.is_fn() {
                     return None;
                 };
-                Some(FnLoops::new(item.name()).collect(&item.expect_body()))
+                Some(FnLoops::new(item_name(&item)).collect(&item.expect_body()))
             })
             .partition::<Vec<_>, _>(|props| props.has_loops());
 
@@ -192,7 +193,7 @@ impl OverallStats {
                 if !kind.is_fn() {
                     return None;
                 };
-                Some(FnLoops::new(item.name()).collect(&item.expect_body()))
+                Some(FnLoops::new(item_name(&item)).collect(&item.expect_body()))
             })
             .partition::<Vec<_>, _>(|props| props.has_iterators());
 
@@ -203,7 +204,7 @@ impl OverallStats {
                 if !kind.is_fn() {
                     return None;
                 };
-                let fn_props = FnLoops::new(item.name()).collect(&item.expect_body());
+                let fn_props = FnLoops::new(item_name(&item)).collect(&item.expect_body());
                 self.fn_stats.get_mut(&item).unwrap().has_loop_or_iterator =
                     Some(fn_props.has_iterators() || fn_props.has_loops());
                 Some(fn_props)
@@ -234,7 +235,7 @@ impl OverallStats {
                 .iter()
                 .map(|def| {
                     (
-                        def.name(),
+                        item_name(def),
                         if recursions.recursive_fns.contains(def) { "recursive" } else { "" },
                     )
                 })

tools/scanner/src/call_graph.rs

@@ -67,7 +67,9 @@ impl OverallStats {
         let krate = rustc_public::local_crate();
         let transitive_unsafe = visited
             .into_iter()
-            .filter_map(|(def, distance)| (def.krate() == krate).then_some((def.name(), distance)))
+            .filter_map(|(def, distance)| {
+                (def.krate() == krate).then_some((crate::item_name(&def), distance))
+            })
             .collect::<Vec<_>>();
         self.counters.push(("transitive_unsafe", transitive_unsafe.len()));
         crate::analysis::dump_csv(filename, &transitive_unsafe);
@@ -88,7 +90,7 @@ impl Node {
             return None;
         };
         let has_unsafe = if let Some(body) = def.body() {
-            let unsafe_ops = FnUnsafeOperations::new(def.name()).collect(&body, tcx);
+            let unsafe_ops = FnUnsafeOperations::new(crate::item_name(&def)).collect(&body, tcx);
             unsafe_ops.has_unsafe()
         } else {
             true

tools/scanner/src/lib.rs

@@ -34,6 +34,14 @@ use strum_macros::{AsRefStr, EnumIter};
 // Use a static variable for simplicity.
 static VERBOSE: AtomicBool = AtomicBool::new(false);
 
+/// The name of a local item as `kani list` reports it: `def_path_str` prefixes
+/// 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 {
+    kani_metadata::strip_crate_prefix(&def.name(), &rustc_public::local_crate().name)
+}
+
 pub fn run_all(rustc_args: Vec<String>, verbose: bool) -> ExitCode {
     run_analyses(rustc_args, &Analysis::iter().collect::<Vec<_>>(), verbose)
 }