diff --git a/Cargo.lock b/Cargo.lock index e6775698de59..e6a3f78b93f3 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1972,6 +1972,7 @@ version = "0.0.0" dependencies = [ "csv", "graph-cycles", + "kani_metadata", "petgraph", "serde", "strum", diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index f5861d967a39..3c13eee44787 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -56,48 +56,11 @@ pub fn nonnull_pointee(ty: Ty) -> Option { }) } -/// 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 (`::m`, -/// `f::`). Remove `::` at each path-component boundary -/// (start of string or after a non-identifier char) so these become `f`, -/// `::m`, `f::`. 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 `::` 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 `::` 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 = 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; diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs index 861636f5972d..e2db5d79d1ed 100644 --- a/kani_metadata/src/lib.rs +++ b/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 +/// (`::m`, `f::`). Remove `::` +/// at each path-component boundary (start of string or after a non-identifier +/// char) so these become `f`, `::m`, `f::`. 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 `::` 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 `::` 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 = 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 + /// `` qualifier; a segment that merely shares the crate's name stays. + #[test] + fn strips_crate_root_qualifiers_only() { + let cases = [ + ( + "core", + "::is_ascii", + "::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", "::m", "::m"), + ("my_crate", "f::", "f::"), + ]; + 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"); + } +} diff --git a/tests/script-based-pre/tool-scanner/scanner-test.expected b/tests/script-based-pre/tool-scanner/scanner-test.expected index 67bd14fc0e46..4f2b59041dd6 100644 --- a/tests/script-based-pre/tool-scanner/scanner-test.expected +++ b/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 diff --git a/tests/script-based-pre/tool-scanner/scanner-test.sh b/tests/script-based-pre/tool-scanner/scanner-test.sh index 468bb61dcf0d..4393e4f10593 100755 --- a/tests/script-based-pre/tool-scanner/scanner-test.sh +++ b/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} diff --git a/tools/scanner/Cargo.toml b/tools/scanner/Cargo.toml index 4a03658b5375..8f85d9563606 100644 --- a/tools/scanner/Cargo.toml +++ b/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" diff --git a/tools/scanner/src/analysis.rs b/tools/scanner/src/analysis.rs index c90deaf469fb..a2d822a3bdfe 100644 --- a/tools/scanner/src/analysis.rs +++ b/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::, _>(|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::, _>(|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 { "" }, ) }) diff --git a/tools/scanner/src/call_graph.rs b/tools/scanner/src/call_graph.rs index f97d02c5b571..e21888614ec3 100644 --- a/tools/scanner/src/call_graph.rs +++ b/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::>(); 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 diff --git a/tools/scanner/src/lib.rs b/tools/scanner/src/lib.rs index 5a49c8e1e663..2c992244c1c1 100644 --- a/tools/scanner/src/lib.rs +++ b/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(def: &T) -> String { + kani_metadata::strip_crate_prefix(&def.name(), &rustc_public::local_crate().name) +} + pub fn run_all(rustc_args: Vec, verbose: bool) -> ExitCode { run_analyses(rustc_args, &Analysis::iter().collect::>(), verbose) }