model-checking
Bloated MIR remains for `Result` functions
Proposed change:
Maybe some strategy for stubbing all string formatting could be helpful for bloat and not affect our correctness? At the very least finding a way to stub unwrap_failed() specifically would help these instances.
Motivation:
Result::unwrap() and Result::expect() seem to have unique call trees going through the core::result::unwrap_failed() that still cause significant MIR bloat even with panic stubbing. This seems to be due to the way the panic!() macro is called, causing it to expand into calls to display and debug format functions as well as the actual call to core::panic() that is eventually stubbed.
It seems that the issue is the internal use of the core::panic!() macro in unwrap_failed(). When a crate uses panic!() directly, the Kani compiler builds it with an --extern flag that will overwrite std (and the panic!() macro) with our own version that has no formatting code. However, this doesn't overwrite the macro in dependencies, so the unwrap_failed() function will still be compiled with the base version of std and use the real core::panic!() macro's complex formatting.