Alex Portland
Alex Portland
We have an existing `benchcomp` script to measure Kani's performance in CI, but it is prone to noise and only focuses on the end-to-end performance of compilation and verification together,...
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...
**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()`...
As far as I can tell we don't take advantage of GitHub's caching feature for CI. I think even just caching the cargo registry & kani dependencies could help with...
Hi! I'm working with `DatatypeBuilder`s, and it'd be really nice if you could construct a variant's fields with `Vec` as well as the existing `Vec`. Requiring string slices can be...
I’ve noticed that Kani will often repeatedly codegen elements that are similar or exactly the same (sometimes as many as ~500 times) while compiling a crate. The two biggest offenders...
## Motivation When compiling with more than a single thread (as in #4236), the order in which we codegen harnesses can have a non-negligable impact on performance. Specifically, if we...
**Proposed change:** It might make sense to add a simple heuristic to determine the order in which we codegen harnesses. **Motivation:** When working on #4236, I noticed that the main...
**Proposed change:** Based on discussion w/ @remi-delmas-3000, we think there's still a good potential for optimization in Kani's `cprover_bindings` code, specifically by combining the two serialization passes it currently uses....
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...