-
Notifications
You must be signed in to change notification settings - Fork 126
Skip codegen for unneeded harnesses #4213
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Skip codegen for unneeded harnesses #4213
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks! Can you check if we have tests for these flags and add some if not? My goal is to make sure that this doesn't break the existing --harness
behavior, so I'd be fine with some expected tests in the ui
folder that demonstrate that we only run proofs for the filtered functions. If you're feeling fancy, you could try to write a script that lists the goto files being generated to ensure that we're only doing codegen for the ones we filter on too, but not necessary.
* remove unneeded comment * rename overloaded `harnesses` variable * add `tracing` as a dependency
I think we might already be covered! For doing unneeded codegen: I'd added a general debug assertion (here) that checks to ensure we didn't codegen any harnesses that we won't use for verification. Since our tests are run in debug mode, these should always run and double check that we're doing no extra harness codegen. For doing too little codegen: I think this would be caught by our existing tests failing (specifically |
210b6c3
### Context When working on #4211 & #4213, I was initially very confused by all the machinery in [`call_cargo.rs`](https://github.com/model-checking/kani/blob/main/kani-driver/src/call_cargo.rs) and [`call_single_file.rs`](https://github.com/model-checking/kani/blob/main/kani-driver/src/call_single_file.rs) that we used to pass arguments to the different layers of the compiler. The main source of my confusion was that there were many arguments all destined for different places (e.g. cargo, rustc, or kani-compiler) that all had to be encoded in differing ways (e.g. through the `--llvm-args` flag or the `CARGO_ENCODED_RUSTFLAGS` environment variable) but were mixed together sharing the same `String` type and similar-sounding variable names. Although misconfiguration would often be caught at runtime with a section of the compiler complaining about unexpected arguments, this confusion silently bit me a few times where argument names were shared. ### Fix This PR represents an attempt to encode the way arguments target different portions of the compiler into the type system using specific wrapper types for each kind of argument we use. You can convert transparently into these wrapper types, but then can only convert between them or pass them to a cargo command using the proper encoding methods. Although not perfect (you could still convert into the wrong kind of argument wrapper initially), this does seem to add some slight guardrails on the way we call cargo, especially against smaller changes to the existing patterns like the ones I was making in my PRs. It also may make the code easier to parse. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
from the autogenerated : ## What's Changed * Ensure that contract closures are FnOnce by @vonaka in #4151 * Adjust sized hierarchy for Kani's memory predicates by @tautschnig in #4193 * Update to Rust edition 2024 by @tautschnig in #4197 * `ptr_offset_from`: Replace arithmetic over pointers by offset arithmetic by @tautschnig in #4180 * Automatic cargo update to 2025-07-07 by @github-actions[bot] in #4208 * Bump tests/perf/s2n-quic from `b8f8cca` to `8715fdf` by @dependabot[bot] in #4209 * Upgrade Rust toolchain to 2025-07-04 by @tautschnig in #4199 * Upgrade Rust toolchain to 2025-07-10 by @thanhnguyen-aws in #4215 * Update CBMC dependency to 6.7.1 by @tautschnig in #4178 * Split compiler flags to avoid dependency recompilation by @AlexanderPortland in #4211 * Fix the bug that assign clause cannot be inferred for the inner loop of nested loops by @thanhnguyen-aws in #4179 * Upgrade Rust toolchain to 2025-07-11 by @thanhnguyen-aws in #4219 * Automatic toolchain upgrade to nightly-2025-07-12 by @github-actions[bot] in #4222 * Fix bug: `goto-cc` crash when there are two quantifers in one proof by @thanhnguyen-aws in #4221 * Automatic toolchain upgrade to nightly-2025-07-13 by @github-actions[bot] in #4223 * Automatic cargo update to 2025-07-14 by @github-actions[bot] in #4224 * Cleanup links to issues that have been addressed by @tautschnig in #4200 * Selectively enable and fix (slow) Tokio tests by @tautschnig in #4203 * Bump tests/perf/s2n-quic from `32ba87d` to `1cbd879` by @dependabot[bot] in #4227 * Implement support for Cargo.toml's default-members by @tautschnig in #4201 * Do not invoke memset with count of zero by @tautschnig in #4205 * Support bitwuzla, cvc5, z3 as solver attribute values by @tautschnig in #4218 * Use CBMC's shuffle_vector expression by @tautschnig in #4204 * Move tests from slow/kani back to regular suite by @tautschnig in #4202 * Automatic toolchain upgrade to nightly-2025-07-14 by @github-actions[bot] in #4225 * Enable GitHub Linux/Arm runners in CI by @tautschnig in #3841 * Automatic cargo update to 2025-07-21 by @github-actions[bot] in #4231 * Skip codegen for unneeded harnesses by @AlexanderPortland in #4213 * Strongly type differing compiler args for clarity by @AlexanderPortland in #4220 * Remove StableMIR ICE workaround by @carolynzech in #4235 * Fix bug: Kani unwinds loops with contract in generic function (with -Z loop-contracts) by @thanhnguyen-aws in #4232 * Automatic cargo update to 2025-07-28 by @github-actions[bot] in #4238 * Bump tests/perf/s2n-quic from `1cbd879` to `4938450` by @dependabot[bot] in #4242 * Upgrade Rust toolchain to 2025-07-21 by @tautschnig in #4241 * Remove `pretty_ty` and use rustc_public's formatter instead by @tautschnig in #4243 * Upgrade Rust toolchain to 2025-07-24 by @tautschnig in #4244 * Documentation cleanup of UB detected by Kani by @tautschnig in #4245 * Upgrade Rust toolchain to 2025-07-29 by @tautschnig in #4247 * Automatic toolchain upgrade to nightly-2025-07-30 by @github-actions[bot] in #4253 * Add unstable option prove-safety-only by @tautschnig in #4239 * Set bits_per_byte in byte_extract expressions by @tautschnig in #4255 * `KaniAttributes` Path Resolution Refactor by @carolynzech in #4249 * Automatic toolchain upgrade to nightly-2025-07-31 by @github-actions[bot] in #4256 * Support contracts & stubs in trait implementations (partial fix) by @carolynzech in #4250 * [Breaking Changes] Remove unstable list feature and default memory checks by @carolynzech in #4258 * Upgrade Rust toolchain to 2025-08-01 by @tautschnig in #4261 * Autoharness: add support for references by @tautschnig in #4234 * Turn off debug assertions under `--prove-safety-only` by @tautschnig in #4262 * Automatic toolchain upgrade to nightly-2025-08-02 by @github-actions[bot] in #4264 * Automatic toolchain upgrade to nightly-2025-08-03 by @github-actions[bot] in #4265 * Automatic cargo update to 2025-08-04 by @github-actions[bot] in #4267 * Automatic toolchain upgrade to nightly-2025-08-04 by @github-actions[bot] in #4266 * Introduce thread pool for writing goto binaries in parallel by @AlexanderPortland in #4236 * Major-version update cargo dependencies by @tautschnig in #4240 * Bump tests/perf/s2n-quic from `4938450` to `8f510f0` by @dependabot[bot] in #4270 * Automatic toolchain upgrade to nightly-2025-08-05 by @github-actions[bot] in #4271 * Automatic toolchain upgrade to nightly-2025-08-06 by @github-actions[bot] in #4272 * Avoid updating irrelevant symbols when handling quantifiers by @AlexanderPortland in #4268 * Lazily evaluate debug info by @AlexanderPortland in #4269 * Clone a template `BodyTransformer` to avoid re-initialization by @AlexanderPortland in #4259 * Ensuring that MIR constants are marked as static consts by @vonaka in #4233 * Fix release job dependencies by @tautschnig in #4273 ## New Contributors * @vonaka made their first contribution in #4151 **Full Changelog**: kani-0.64.0...kani-0.65.0 --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
This PR moves the logic for filtering out specific harnesses (as specified by the
--harness
&--exact
Kani arguments) to the compiler, allowing us to skip codegen for harnesses that will end up being blocked by the filter. I’ve also added a dev-build-only assertion to double check that we’re not doing codegen for any unused harnesses.Based on testing, something like running
cargo kani --harness estimator
ons2n-quic-codec
used to take ~11s locally to compile 66 harnesses, but only 5 would end up being analyzed. Now, the same command compiles only the 5 needed harnesses, taking just ~5s.The downside of this is that the target crate now has to be recompiled if the user runs Kani with differing harness filters but, if the idea in #4212 is possible, that too could be avoided.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.