FEAT-043 (v2.6): weight shadow-stack bound by resolved call_indirect targets#79
Merged
Conversation
…ect targets DD-016 slice-3. The worst-case shadow-stack longest-path previously weighted EVERY call_indirect by the WHOLE table (build_static_call_graph). Now it uses the RESOLVED target set (FEAT-006 index-interval resolution) — a sound superset, tighter when the index is constrained (a constant index → one table entry). - resolved_stack_callees: per gap-free function, the union of its call_graph edges' resolved_targets (sound superset, SCRY-001); a function WITH a FEAT-040 gap (degraded / control-region havoc → possibly unrecorded calls) falls back to the conservative whole-table static_callees. Recursion + topo stay on static_callees (conservative). Sound: resolved_targets ⊇ concrete and the gap-gate never drops a callee. - Enabler: model global.get (push ⊤) / global.set (pop) in the interpreter instead of degrading the function. Stack prologues read the SP global, so every frame-bearing function previously fully degraded (losing its call_indirect index resolution); now they stay analyzed. Sound (globals are untracked ⊤; locals/stack unaffected by global ops). Also a general precision win — prologue functions keep their interval/relational facts. Test feat043_indirect_stack_weighted_by_resolved_target: entry (frame 8) with a const-index call_indirect to table[0]=$small(16) is bounded 8+16=24, not the whole-table 8+64=72. 46 core tests (incl. all 6 FEAT-021 stack tests unchanged); clippy + fmt clean. FEAT-043 accepted (release v2.6.0). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…-room) Clean-room found a real UNDER-COUNT: a void call (empty write-set) inside an `if` region is havocked, so its edge is never recorded in call_graph — yet the function had no gap (the gap was gated on write-set non-empty), so resolved_stack_callees trusted the incomplete call_graph and DROPPED the callee's frame (reported 256 vs true 264). The downstream memory reservation (synth#383) would have been too small. Fix: havoc_region records a gap when the region contains ANY call op (Call/CallIndirect/ReturnCall/ReturnCallIndirect), not only when it widens a local — restoring the invariant "a gap-free function's call_graph is complete" that resolved_stack_callees (and the FEAT-040 gap report) rely on. The gapped function falls back to the conservative whole-table static_callees → sound 264. Also documented the pre-existing FEAT-036-class limitation (passive/declared elem segments under-report indirect targets in BOTH static_callees and resolved_targets — FEAT-043 is no less sound than the prior whole-table weighting on that case; tracked separately). Regression test feat043_call_in_havocked_if_not_dropped (264, not 256). 47 core tests; clippy + fmt clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…oom concern #1) A function dispatching an arbitrary funcref (call_ref / return_call_ref, function-references proposal) calls a target neither the resolved nor the whole-table graph enumerates, so its stack contribution is genuinely UNKNOWN — report StackBound::Unknown rather than a false finite bound that omits the funcref-dispatched subtree. Unknown propagates soundly through sb_add/sb_max (and Unbounded still dominates). Closes the remaining funcref-dispatch under-count flagged alongside the return_call finding; the passive/declared-elem table under-report stays documented as a pre-existing FEAT-036-class limitation. 49 core tests; clippy + fmt clean. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #79 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
A call_indirect/return_call_indirect against a table scry cannot fully
enumerate must yield StackBound::Unknown, not a finite under-count that
silently drops the dispatched callee's frame. Unenumerable = a non-zero
table index, or a table-0 whose contents are not fully known (growable,
or populated by a passive/non-const elem segment).
compute_stack_usage now takes table0_contents_known and the
has_unresolvable_call guard covers CallRef|ReturnCallRef and
CallIndirect|ReturnCallIndirect{table_index!=0 || !contents_known}.
Regression: feat043_unenumerable_indirect_is_unknown (table-1 dispatch ->
Unknown). feat043_indirect_stack_weighted_by_resolved_target switched to a
bounded (non-growable) table so it still exercises the finite resolved-
weighting path.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…an-room #4) The element-segment shape gives the table's INITIAL contents, but a Wasm table is mutable module-global state. If any defined function can write table 0 (table.set/fill/grow on it, or it is the dst of table.copy/init), an active-segment-resolved slot may be overwritten at runtime with a deeper-framed callee — so resolving call_indirect to the declared target under-counts the stack. Fix: after the body-collection pass, scan for any table-0 mutator and, if present, clear func_table.contents_known. This makes every downstream consumer (resolved stack weighting, interpret-time resolution, and the compute_stack_usage Unknown guard) fall back to the conservative whole- table over-approximation / StackBound::Unknown. Regression: feat043_runtime_table_mutation_is_unknown (table.set overwrites slot0 with a 4096-byte-frame callee -> Unknown, not Bytes under-count). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Final feature of v2.6.0 (DD-016 slice-3). Tightens the worst-case shadow-stack bound.
What
call_indirectby the whole table. Now it uses the resolved target set (FEAT-006 index resolution) — a sound superset, tighter when the index is constrained.resolved_stack_callees: for a gap-free function (FEAT-040), the union of itscall_graphedges'resolved_targets; a function with a gap (degraded / havocked → calls maybe unrecorded) falls back to the conservative whole-table. Recursion + topo stay conservative.global.get(push ⊤) /global.set(pop) instead of degrading. Stack prologues read the SP global, so frame-bearing functions used to fully degrade (losing index resolution); now they stay analyzed — a general precision win too.Soundness
resolved_targets ⊇ concrete(SCRY-001); the gap-gate never drops a callee; recursion stays conservative. The bound never under-counts. Globals modeled as untracked ⊤ (sound); locals/stack unaffected.Test:
feat043_…— entry (8) → const-indexcall_indirect→ table[0]=$small(16) ⇒24, not the whole-table72. 46 core tests (all 6 FEAT-021 stack tests unchanged). Traces DD-016.release: v2.6.0.🤖 Generated with Claude Code