model-checking
Stub panics during MIR transformation
Modifies the RustcIntrinsicsPass to stub out panic functions during body transformation at the MIR level. This avoids having to bring in (and do transformation passes on) the large amounts of code they use for string formatting. Our panic hook has been modified to then detect these stubs during codegen and still generate the same Goto code for them.
The results of this change on the MIR bloat of panic!() and its callers is shown below:
| test | lines of MIR (before) | lines of MIR (w/ panic stubbing) |
|---|---|---|
Option<usize>::unwrap() |
292 | 217 |
Option<usize>::expect() |
8664 | 225 |
Result<usize, usize>::unwrap() |
20461 | 20374 |
Result<usize, usize>::expect() |
20463 | 20376 |
panic!("hello!") |
8498 | 41 |
panic!("hello {x}!") (x being a &'static str) |
8502 | 45 |
The lack of significant improvement on the two Result functions is elaborated on in #4168 and will take additional consideration to fix.
Resolves #2835
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
@zhassan-aws I just added a test that runs kani on three of the panic!() examples from above and checks to make sure that the emitted MIR properly contains our panic stub.