Add heuristic to order harness codegen

[AlexanderPortland]

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 handle harness that will generate a lot of code near the end of compilation, the main compiler thread can get stuck waiting for worker threads to export that code, slowing down overall compilation. If we could ensure that more difficult to export harnesses are handled first, the thread pool will have more time to write them to disk off the critical path of compilation.

Approach

This PR switches reachability analysis for all harnesses to happen before codegen. It can then use the information we gather from reachability to reorder codegen based on the total number of items reachable from each harness (MostReachableItems).

This heuristic was chosen because it is:

• simple -- only requiring a single field access for each harness, and taking only ~10µs to fully sort a typical CodegenUnit of 66 harnesses (acceptable given it took ~20ms to codegen the fastest harnesses in that same CodegenUnit)
• seemingly effective -- on the s2n-codec benchmark it only ever places a slower-to-export harness after a faster one if their actual export times were within 10ms (or 7%). Since the goal is just to roughly order harnesses based on order of magnitude, this is a very good result 🎉

Results

This change made a small, but not insignificant 2.9% reduction in the end to end compile time of the standard library (@ commit 177d0fd).

And below is a recreation of the graph of the compiler's per-thread CPU usage from #4248 now that codegen is ordered.

While functionally complete on its own, this change will not really make a performance impact until #4236 is merged.

Resolves #4248

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

Let's get #4236 merged first so that this PR can get concrete data points in its PR description.

[tautschnig]

#4236 has now been merged, so this one should be ready to be acted upon.

[zhassan-aws]

Thanks! Is it possible to add a test that ensures the order is what we expect it to be?

[Copilot]

Pull request overview

This PR aims to improve kani-compiler end-to-end compile performance when exporting goto binaries in parallel by ordering harness codegen so “larger” harnesses (by reachable-item count) are handled earlier, keeping export work off the main thread’s critical path.

Changes:

• Introduces ReachabilityInfo to package reachability results (starting items, reachable items, call graph) for reuse across phases.
• Adds a MostReachableItems heuristic and iterator adaptor to reorder harnesses within codegen units based on reachable item count.
• Refactors the cprover gotoc backend to run reachability before harness codegen and plumb reachability data through codegen_items.

Reviewed changes

Copilot reviewed 5 out of 5 changed files in this pull request and generated 6 comments.

Show a summary per file

File	Description
kani-compiler/src/kani_middle/reachability.rs	Adds ReachabilityInfo wrapper to reuse reachability results.
kani-compiler/src/kani_middle/mod.rs	Exposes new codegen_order module.
kani-compiler/src/kani_middle/codegen_order.rs	Implements heuristic-based harness ordering utilities.
kani-compiler/src/codegen_cprover_gotoc/mod.rs	Re-exports HarnessWithReachable for use by ordering code.
kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs	Refactors harness codegen pipeline to precompute reachability and (intended) ordering.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[feliperodri]

Pushed a new revision that gets this PR back to a compiling, reviewable state and resolves the peak-memory regression discussed in the earlier comments.

The branch no longer compiled. The last merge from main left codegen_crate half-refactored (ordered_harnesses was undefined while a leftover per-unit loop still referenced an out-of-scope unit). This was the root cause behind the failing CI jobs (Kani CI, Check Std Verification, Release Bundle, Kani Extra, and the format check). It now builds cleanly on the current toolchain.

Bounded-memory rework

The previous approach ran reachability for every harness up front and retained each harness's full result (reachable set, call graph, and its own BodyTransformation) so it could sort before codegen. On the standard library this tripled peak memory (~2 GB → ~6 GB), because all of a codegen unit's harnesses were held in memory at once.

The new approach:

• Orders harnesses within each codegen unit, preserving main's single shared-transformer-per-unit model.
• Retains only the heuristic rating — a single usize per harness — not the reachable set or call graph.
• Runs the rating pass with the unit's shared transformer, which warms its body cache; codegen then recomputes reachability but hits that cache, so only the (cheap) graph traversal is repeated, not body transformation.

Net effect: peak memory matches codegening the unit in its original order, and codegen_items is now byte-for-byte identical to the pre-PR version — per-harness codegen semantics are unchanged, only the order within a unit differs.

The ordering logic now lives in kani_middle::codegen_order: a CodegenHeuristic trait, the MostReachableItems heuristic, and an order_harnesses helper.

Scope note

MostReachableItems orders harnesses within each codegen unit; units themselves are still processed in their original order. This matches the original intent, but flagging it in case global ordering was expected.

[Copilot]

Pull request overview

Copilot reviewed 3 out of 3 changed files in this pull request and generated no new comments.

Suppressed comments (1)

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:413

• This runs an extra full reachability traversal for every multi-harness unit even when no export worker exists. thread_pool_size returns 0 on single-core builds, and ThreadPool::send_work then exports synchronously (file_writing_pool.rs:58-64), so ordering cannot hide any export latency and only increases compilation time. Gate the heuristic on the worker count.

                        let ordered_harnesses = order_harnesses::<MostReachableItems>(
                            &unit.harnesses,
                            tcx,
                            &mut shared_unit_transformer,
                        );