kani-driver: Get json messages from cargo invocations

[tedinski]

Instead of simply running cargo build or cargo test --no-run with environment variables set so that cargo invokes kani-compiler appropriately, we should use something like cargo build --build-plan -Z unstable-options to get the build plan, then execute it ourselves. Alternatively, investigate how much of cargo is available as a library. Perhaps we can get cargo to compute a plan, modify it, and then ask cargo to execute that plan via library, rather than by calling out to external executables.

There's a couple of reasons to want this:

1. We can change invocations of rustc to run kani-compiler directly, instead of trying to bodge things into working with environment variables.
2. We can properly extract which targets need to be built. Presently we just link all symtab together into one binary, and this could create collisions. cargo kani --tests fails on crates with integration tests #1448
3. We can properly identify which symtabs to use. Builds can leave old files laying around, identified by different hashes. cargo clean required between cargo kani invocations #1591

(Further benefits should be added to this issue.)

[zhassan-aws]

I looked into this a bit yesterday, and unfortunately, it seems that there are no plans to stabilize the --build-plan option anytime soon. In fact, the option even seems to be broken and there's been discussions to delete it: rust-lang/cargo#7614

An alternative heavy-weight approach is to use the cargo crate as a dependency. One downside would be increasing Kani's build time (the cargo crate takes ~45 seconds to build by itself).

For reasons 2 and 3, it might be sufficient to use the cargo_metadata crate, which we're already using in the Kani driver.

[celinval]

One thing to be careful about is the compilation of proc_macros and build scripts. One of the reasons we have the hacky --kani-flags today is because we want to compile "host" code with regular rustc, since they will be executed as part of the compilation (this might help us get rid of the hack, but it is unstable: https://doc.rust-lang.org/cargo/reference/unstable.html#host-config).

There are a few workarounds described here: rust-lang/cargo#7178 that we could use too.

[tedinski]

I believe we came to the conclusion we didn't want to build ourselves. Instead, we want to parse the json output from cargo build so we know all the artifacts, etc that were produced.

[celinval]

I think our main concern was to depend on cargo build-plans, since it may eventually get deleted: rust-lang/cargo#7614

[celinval]

We have changed kani-driver to parse the messages from cargo as part of #2166