add unsafe-finder tool

[patricklam]

This pull request adds a tool to identify functions that contain unsafe code but are not unsafe, as well as pub unsafe functions.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

Can you explain why this repository is the right place for such a tool? (It seems like a general Rust tool, not specific to the standard library.) We also have the scanner tool in the Kani repository, which produces CSV files that have (what I believe to be) equivalent information. See https://github.com/model-checking/verify-rust-std/blob/main/scripts/kani-std-analysis/std-analysis.sh or https://github.com/model-checking/kani/tree/main/tests/script-based-pre/tool-scanner.

[carolynzech]

We also have the scanner tool in the Kani repository, which produces CSV files that have (what I believe to be) equivalent information

See https://github.com/model-checking/kani/tree/main/tools/scanner/src for the scanner code and model-checking/kani#4037 for the PR that added the unsafe distance metric.

[patricklam]

Thanks. The kani repo is perhaps a better place than the stdlib for this tool, yes.

I couldn't quite figure out how to run the scanner tool, though I have seen the kani metrics being committed to the repo. I tried to run, for instance, tests/script-based-pre/tool-scanner/scanner.test.sh and it says "cannot stat test.rs'. Running the scanner tool on, for instance, rc.rs gives a bunch of compiler errors.

Unsafe distance of 0 and 1 is similar to what my tool reports, but I only see counts as the output from the scanner tool (without running it). If it doesn't do it already, the scanner tool could also be modified to report names, like my tool does, and that might be better. I used my tool to collect the list of functions for my proposed challenges, because I figured that doing it manually was a losing game.

[carolynzech]

I couldn't quite figure out how to run the scanner tool, though I have seen the kani metrics being committed to the repo. I tried to run, for instance, tests/script-based-pre/tool-scanner/scanner.test.sh and it says "cannot stat test.rs'. Running the scanner tool on, for instance, rc.rs gives a bunch of compiler errors.

Run the ./std-analysis.sh script here: https://github.com/model-checking/verify-rust-std/blob/main/scripts/kani-std-analysis/std-analysis.sh.

On my local machine, I would run:

cmzech@80a9971b5e20 rust % ./scripts/kani-std-analysis/std-analysis.sh ~/kani/

[patricklam]

Thanks. Yes, the std-analysis.sh script returns a superset of the information that my tool provides, but I'd suggest that it would have required some postprocessing to use it to generate the list of functions for a challenge.

If there is interest, I could write a tool that uses the std-analysis.sh tool to produce nicely-formatted output for a challenge; it is probably better to have a single source of truth, rather than a bunch of tools which have slightly different opinions on what to report.

There's also the question of what repo this should live in. As is, the script to run the tool lives in the verify-rust-std repo, while the tool itself (which is not actually Kani-specific) lives in the kani repo. Neither of these are really ideal.

[carolynzech]

If there is interest, I could write a tool that uses the std-analysis.sh tool to produce nicely-formatted output for a challenge; it is probably better to have a single source of truth, rather than a bunch of tools which have slightly different opinions on what to report.

Agreed. Your idea to tailor the output more closely to directories/files to make it easier to guide challenge development is a good one; the scanner tool outputs quite a bit of data right now. We'd prefer to coalesce around a single "std scanner" tool just for ease of maintenance, but we're very happy to have contributions that build on that tool. It seems like in this case, we can add some filtering to the scanner tool to reduce the output to what you're interested in.

There's also the question of what repo this should live in. As is, the script to run the tool lives in the verify-rust-std repo, while the tool itself (which is not actually Kani-specific) lives in the kani repo. Neither of these are really ideal.

Agreed. std-analysis.sh used to live in Kani too; we moved it here to make it a bit less awkward. The original idea was that the scanner tool isn't specific to the standard library, so it made more sense for it to live in Kani and be more "general purpose" than to live here. I think at this point though, we only ever use it for the standard library, and having it be in the Kani repo makes it harder for other contributors such as yourself to find. So I'd be in favor of moving it here. If @tautschnig agrees, I can open a PR to do that.

[patricklam]

I've updated this tool so that it uses the output from std-analysis.sh. I noticed that kani_std_analysis.py creates a lot of graphs, but it does not produce a list of unsafe functions / unsafe abstractions, which I think is still useful.

The tool now takes e.g. core_scan_functions.csv as output by std_analysis and produces a grouped list of functions. It would also be useful to combine it with the check for Kani annotations, I think. Is anyone else interested in this tool, possibly with the addition of a Kani filter? (There are, of course, also some things that are verified by VeriFast and by the SIMD checking approach, but they are currently not much code.) @carolynzech @tautschnig

[Copilot]

Pull request overview

Adds an unsafe-finder tool for analyzing Kani scanner output and reporting unsafe-related functions.

Changes:

• Adds CSV parsing, function-name analysis, and tests.
• Adds usage documentation.
• Adds package configuration and dual licensing.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
tools/unsafe-finder/src/main.rs	Implements analysis and reporting.
tools/unsafe-finder/README.md	Documents purpose and usage.
tools/unsafe-finder/Cargo.toml	Defines the Rust package.
tools/unsafe-finder/LICENSE-MIT	Adds the MIT license.
tools/unsafe-finder/LICENSE-APACHE	Adds the Apache 2.0 license.

Suppressed comments (1)

tools/unsafe-finder/README.md:31

• The implementation accepts Kani scanner CSV files only; it neither parses .rs files nor traverses directories, and its output is module/debug grouping rather than the impl blocks shown below. The documented rc.rs invocation will try to deserialize Rust source as CSV and fail. Document the actual _scan_functions.csv interface and remove the unattainable sample output.

This tool takes a directory or a list of .rs files as input and prints
out a list of impls and traits that have functions in categories (1)
through (3), as well as the involved functions.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

@patricklam could you address all copilot comments before I do a full review of this PR?

[feliperodri]

Review: add unsafe-finder tool

Verdict: Request changes. This is a genuinely useful auxiliary tool — it surfaces pub unsafe fns and safe-but-unsafe-containing functions from the scanner CSV, which is exactly the kind of prioritization the verification effort needs. It's a standalone crate under tools/ and doesn't touch library/, so there's no risk to the verification target. Thank you for it. There are three blocking issues though, all reproduced locally (rustc/cargo from the repo's pinned nightly-2025-11-25), plus some robustness/idiom cleanups.

Blocking

1. The scripts/kani-std-analysis/std-analysis.sh change looks like an unrelated regression. Switching uname -sm → uname -msp and matching the literal "Linux x86_64 unknown" hard-codes the assumption that uname -p returns unknown. On my machine uname -msp returns "Linux x86_64 x86_64" (because uname -p reports the real CPU there), so the platform check fails, TARGET is never set, and — with set -eu in force — the next use of $TARGET aborts the whole metrics run. This also seems out of scope for "add unsafe-finder tool." Please drop this hunk (keep the harmless comment fixes if you like) or split it into its own PR with justification.
2. parse_fn_name panics on any function name that contains no ::. parts[1] is indexed unconditionally at src/main.rs:171. I reproduced it by feeding a row named foo: thread 'main' panicked ... index out of bounds: the len is 1 but the index is 1, which aborts the entire run. A defensive analysis tool shouldn't crash on one odd/short name — please bounds-check.
3. cargo fmt --check fails across src/main.rs (tabs mixed with spaces, import ordering, brace/spacing). Please run cargo fmt.

Should fix

4. The </> depth counter in split_by_double_colons / split_by_commas breaks on ->. A function-pointer/closure return type inside a generic argument decrements bracket_level at the > of ->, so nesting is miscounted. Reproduced: mymod::<fn()->bar::Baz>::the_item splits to ["mymod", "<fn()->bar", "Baz>", "the_item"] instead of 3 parts. Demangled std names do contain fn-pointer/closure types, so this will misparse real rows. Consider special-casing -> (and note >> shift / >= can't be distinguished either).
5. 7 clippy warnings (redundant field names ×4, empty else {}, needless borrow, immediately-dereferenced reference). cargo clippy --fix clears them all.
6. parse_fn_name has no unit tests — it's the most complex and the only panic-prone function, yet only the two splitter helpers are covered (9 tests, all passing). Adding a couple of cases (trait-impl, generic, and the no-:: edge case from item 2) would lock down the parsing.

Minor / questions

• Every trait-impl function is bucketed under an empty module_path (modules []), so the module grouping is effectively a no-op for the majority of results. Intended?
• Category (1) is filtered to is_public, but category (2) reports both public and private — yet the README argues private unsafe functions also "should have contracts and be verified." Is the asymmetry deliberate?
• Leftover TODO in main: // should we only handle files named "_scan_functions.csv"?.
• Nothing invokes the tool from CI (std-analysis.sh generates the CSV but never calls unsafe-finder). Fine if it's meant to be run manually — just confirming that's the intent rather than a missing wiring step.
• edition = "2024" means the crate won't build on stable 1.84; it's fine under the repo's pinned nightly, just flagging for anyone building it standalone.

Happy to re-review once the blocking items are addressed, @patricklam.

[feliperodri]

This change looks unrelated to the tool and is a regression. uname prints selected fields in a fixed canonical order regardless of flag order, so uname -msp = kernel + machine + processor. uname -p is unreliable on Linux: it returns unknown on some systems but the real CPU on others. On my box uname -msp = "Linux x86_64 x86_64", so this check fails, TARGET is never set, and with set -eu the next $TARGET use aborts the run. Please revert to uname -sm / "Linux x86_64" (or split this into its own PR with rationale).

[feliperodri]

Panic risk: if raw_name has no ::, parts.len() == 1, the parts.len() == 2 branch above is skipped, and this parts[parts_index] (index 1) panics with index out of bounds. Reproduced on a row named foo — it aborts the whole run. Please guard the length before indexing.

[feliperodri]

The </> depth counter miscounts on ->: the > of a fn-pointer/closure return type decrements bracket_level even though no < opened it. mymod::<fn()->bar::Baz>::the_item then splits into 4 parts instead of 3. Demangled std names do contain such types. Consider skipping the > when the previous char is - (and note >>/>= are also ambiguous).

[feliperodri]

clippy: redundant field names — is_public: is_public / typ: typ here and at 190/191 can be the shorthand is_public, / typ,. This is one of 7 clippy warnings (also an empty else {} at 233, a needless borrow, and an immediately-dereferenced reference); cargo clippy --fix clears them all.

[feliperodri]

edition = "2024" requires cargo ≥ 1.85. It builds fine under the repo's pinned nightly-2025-11-25, but won't build on stable 1.84 — worth confirming that's acceptable for this tool, or dropping to 2021 since nothing here needs 2024-specific features.