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.