model-checking
Avoid `rustc` re-lowering when Kani options change?
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.
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: https://github.com/model-checking/kani/blob/192911d28486f26a36cee6dc0ce817bccd5d9952/kani-driver/src/call_cargo.rs#L219
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: https://github.com/model-checking/kani/blob/192911d28486f26a36cee6dc0ce817bccd5d9952/kani-driver/src/call_single_file.rs#L259-L268
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
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.
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!