verify: exponential time in must_write_args_rec

[HardMax71]

cargo rapx verify takes exponential time in the depth and branching of the local call chain below a target. This crate takes 24 seconds:

fn l4(a: u32) -> u32 { a ^ 1 }

fn l3(mut a: u32) -> u32 {
    if a & 1 != 0 { a = l4(a) }
    if a & 2 != 0 { a = l4(a) }
    if a & 4 != 0 { a = l4(a) }
    if a & 8 != 0 { a = l4(a) }
    a
}

fn l2(mut a: u32) -> u32 {
    if a & 1 != 0 { a = l3(a) }
    if a & 2 != 0 { a = l3(a) }
    if a & 4 != 0 { a = l3(a) }
    if a & 8 != 0 { a = l3(a) }
    a
}

fn l1(mut a: u32) -> u32 {
    if a & 1 != 0 { a = l2(a) }
    if a & 2 != 0 { a = l2(a) }
    if a & 4 != 0 { a = l2(a) }
    if a & 8 != 0 { a = l2(a) }
    a
}

fn l0(mut a: u32) -> u32 {
    if a & 1 != 0 { a = l1(a) }
    if a & 2 != 0 { a = l1(a) }
    if a & 4 != 0 { a = l1(a) }
    if a & 8 != 0 { a = l1(a) }
    a
}

pub fn target(xs: &[u32]) -> String {
    format!("{}", l0(xs[0]))
}

Each function has K independent ifs with a call on the branch, chained D levels deep. target is a scan target because of the format!, and its slice parameter gives it the [T] invariants checked at the return. Seconds per run, same shape:

K	D = 3	D = 4	D = 5
3	0.5	1.0	6.0
4	1.2	24	596
5	10.8	823	over 1800

--postfix-repeat 0, 1 and auto make no difference. D = 6 costs the same as D = 5, which matches the depth > 4 cutoff.

A stuck run always sits in the same stack: must_write_args_rec nested five deep, under dependency_summary, under slicer::call_visit::visit, under the backward slicer in check_invariant_from_tree. must_write_args_rec (verify/call_summary/interprocedural.rs:1141) enumerates every whole-CFG path of the callee, up to 4000, and write_args_on_path recurses into it again for every call on each path (line 1358). Nothing is cached, so a callee is summarized once for every path that reaches it. On a real crate, where callees have hundreds of paths, one function ran for over 20 minutes without finishing. Caching the result per callee would likely remove most of it.

RAPx at 29cc910 (main), nightly-2026-09-22 (rustc 1.100.0-nightly 1303417c4 2026-09-21), on a lib crate holding only this file.

[hxuhack]

This overhead is introduced by the context-sensitive analysis. Addressing this issue involves a trade-off between efficiency and accuracy. Do you have any better solutions?

[HardMax71]

@hxuhack I don't think this needs a trade-off.

must_write_args_rec only gets the callee and the depth. Nothing from the call site reaches it, so the same (callee, depth) always gives the same result, and caching it can't change anything. The context-sensitive part, where the VM applies a summary on each path, stays as it is. Depth is part of the key because the depth cutoff makes deeper summaries less complete.

I also checked it. A build that ran the cached and uncached versions side by side over the whole test suite compared 311,508 queries and found no difference.

#303 still applies cleanly on current main. The K=4, D=4 repro goes from 25 s to 1 s, same verdict.

There's more to gain. Each query still starts with an empty cache, and the VM asks again for every call on every path. local_return_dependencies also depends only on the callee and rebuilds its graph each time. Keeping both for the whole run is just as exact.

I tried that locally on top of #303, with a thread-local cache (one rapx process checks one crate, so a DefId never outlives it). On one of our crates verify went from 398 s to 57 s with the same verdicts. Without #303 it didn't finish in 20 minutes.

If you'd rather avoid thread-local state, VerifyEngine could own the cache and pass it to the slicer and the VM instead. Same idea, more plumbing. Which would you prefer?

[hxuhack]

The idea proposed in #303 has been merged. Thanks!

However, context sensitivity matters. See this case:
https://raw.githubusercontent.com/safer-rust/RAPx/refs/heads/main/rapx/tests/verify_units/init_ctx_sound_1/src/lib.rs

Commit 98723db provides a refinement to address this case.