Avoid `rustc` re-lowering when Kani options change?

[AlexanderPortland]

This may be a dumb idea as I don't know much about Cargo's build system and incremental compilation strategy, but would it be possible to reuse existing compiler-generated MIR for the target crate even if Kani options change? So long as such options would only affect our codegen from MIR, theoretically it doesn't feel like there's a reason the compiler would have to re-lower everything to MIR just to get the same result anyway.

Maybe the answer is no because we'd have to pass those options to the kani-compiler, changing the way rustc is called and invalidating the build cache. However, even if that's an unfixable limitation of Cargo, it feels like there could still be a way to bypass that by writing options to env vars or a file or something.

[carolynzech]

Maybe the answer is no because we'd have to pass those options to the kani-compiler, changing the way rustc is called and invalidating the build cache.

Yes, exactly. We tell Cargo that rustc is kani-compiler here:

kani/kani-driver/src/call_cargo.rs

Line 219 in 192911d

.env("RUSTC", &self.kani_compiler)

Cargo uses fingerprints to tell whether to recompile something. This table says that "cargo rustc extra args" are included in the fingerprint, which means that any changes to the llvm-args we pass to Cargo (i.e., kani-compiler's arguments) invalidate the cache. See also our documentation about this:

kani/kani-driver/src/call_single_file.rs

Lines 259 to 268 in 192911d

	/// This function can be used to convert Kani compiler specific arguments into a rustc one.
	/// We currently pass Kani specific arguments using the `--llvm-args` structure which is the
	/// hacky mechanism used by other rustc backend to receive arguments unknown to rustc.
	///
	/// Note that Cargo caching mechanism takes the building context into consideration, which
	/// includes the value of the rust flags. By using `--llvm-args`, we ensure that Cargo takes into
	/// consideration all arguments that are used to configure Kani compiler. For example, enabling the
	/// reachability checks will force recompilation if they were disabled in previous build.
	/// For more details on this caching mechanism, see the
	/// [fingerprint documentation](https://github.com/rust-lang/cargo/blob/82c3bb79e3a19a5164e33819ef81bfc2c984bc56/src/cargo/core/compiler/fingerprint/mod.rs)

[carolynzech]

However, even if that's an unfixable limitation of Cargo, it feels like there could still be a way to bypass that by writing options to env vars or a file or something.

I think as long as we 1) pass kani-compiler arguments with llvm-args and 2) rely on Cargo's build cache, this is an unfixable limitation. We could always 1) try passing the arguments another way, although I don't think that's really possible unfortunately or 2) implement our own build cache, which is probably not worth the effort

[carolynzech]

So it's definitely not a dumb idea--it would be better if we invalidated the cache less often. I think the question is: can we figure out a way to do it that isn't 1) a ton of work and 2) risks getting it wrong?
It's also worth thinking about some common use cases here, i.e., when we expect people to invoke Kani a bunch of times in succession with different arguments and have to recompile. AFAIK most of our users aren't invoking Kani over and over again, so I'm not sure that this is a huge issue in practice.

[carolynzech]

I think we can still leave this issue open as a way to track this issue; I wouldn't be surprised if more work happens in the upstream Rust community that helps with this problem!