New reachability mode for unit tests #2062
Description
When we generate a goto program from MIR normally today we build with "proof reachability" as the default mode: only code reachable from proof harnesses is included. This applies to any build target type. We only fall back to legacy mode if --legacy-linker is provided, and fall back to "public functions" mode if --function is used.
For assess, I added a "test reachability" mode: instead of treating proofs as roots, treat tests as roots.
However, this mode might be too narrow. Much discussion in #2029 centered around whether we'd miss codegen'ing unimplemented features that are part of the public interface of a library, but not covered by a tests. Assess's operating hypothesis is that if it's not tested, it probably won't be proved either, but we might still want some signal here.
We could introduce a new reachability mode: "lib-pub-fns and tests". This reachability mode would be used by assess for the "cargo unit tests" target (but assess would still use the existing "test reachability" mode for "cargo integration test" targets i.e. the targets under tests/).
This would allow the metadata about encountered unsupported features to include everything reachable from the public interface of the crate, even if it's not covered by a test.
However, this is not as simple as the union of these two modes: when building with tests enabled, the "pub-fns" reachability mode see the test running machinery as the public roots, where we'd want it to see the same pub-fns as if the target had built normally. It's not clear to me if this is an at all easy thing to do.
The priority for this feature depends on how much code there is out there that is:
- Not covered by any tests,
- Should/Could be covered by a proof,
And whether any of our prioritization decisions will be driven by getting data from such code.