v2.2.0 (FEAT-036, synth#54): interprocedural parameter ranges#68
Merged
Conversation
scry now surfaces, per function, the join of the argument values observed across its call sites — a sound interprocedural fact for downstream specialization (synth). - CallEdge.arg_ranges: abstract args at each call site, in param order (direct calls; empty for call_indirect / signature-unknown imports). - FunctionSummary.param_ranges: per param, the join of arg_ranges over all DIRECT call sites reaching the function. Sound by construction — ⊤ for every param of a function that is exported / the start function / reachable via call_indirect (external or over-approximate entries whose args scry can't bound), and ⊤ if any indirect edge is unsound; otherwise the over-approximate incoming value (e.g. called with 5 and 10 → [5,10]). Never narrower than some reachable call permits. Both fields library-only (read off scry-sai-core AnalysisResult); WIT + frozen v1 JSON contract unchanged; the wasm wrapper ignores them (field-access). Traceability: FEAT-036 (traces REQ-004), accepted. Tests: feat036_interproc_param_ranges (join 5⊔10=[5,10]) + feat036_exported_params_are_top (exported → ⊤). 19 core tests pass; clippy clean. Additive fields → SemVer-minor 2.1.1 → 2.2.0. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #68 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
…-room finding) Clean-room verification refuted the original param_ranges gate: it forced ⊤ only for functions whose index appeared in some indirect edge's resolved target set. But scry's static table model UNDER-reports indirect targets — passive/declared element segments, runtime table.init/table.set, and non-constant dispatch indices all leave the resolved set incomplete (and the `UnsoundFallback` clause the gate relied on was never produced). So a function reachable only via an unmodelled indirect edge would be narrowed on direct-call evidence alone: an UNSOUND under-approximation. Fix (the conservative, provably-sound slice-1): if the module contains ANY call_indirect, force every function's param_ranges to ⊤. Narrowing now happens only in indirect-call-free modules, where the recorded direct call sites are provably the complete caller set (the join over them over-approximates every reachable call). A future slice can recover precision with whole-table-mutation analysis. - Replace the dead `any_unsound_edge` / `indirect_targets` machinery with a single `any_indirect_call = call_graph.iter().any(|e| e.indirect)` gate. - Add regression test `feat036_indirect_call_forces_top`: a non-exported function called directly with a constant, in a module that also contains a call_indirect, keeps ⊤ params (would be [7,7] under the old gate). (Note: the indirect call lives in its own function — an unsupported op like `drop` degrades a function to ⊤ and skips later ops, which would mask the call_indirect edge.) - CHANGELOG + FEAT-036 AC: document the whole-module bail and the finding. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…c), not indirect edges
Second clean-room pass refuted the call_indirect-edge gate with two more
under-approximations:
(1) An EXPORTED funcref table lets the HOST call_indirect a defined function
with arbitrary args, even though the module has no call_indirect of its
own — so an edge-based gate sees nothing and narrows the function.
(2) return_call_indirect / call_ref are unsupported ops that scrub to ⊤ and
record NO call-graph edge, so `any_indirect_call` stays false while the
function IS reachable indirectly.
Root cause: a non-null funcref to a defined function can only originate from a
`ref.func` instruction or a table (element segments). Replace the edge-based
`any_indirect_call` with the root-cause predicate:
callers_fully_known = !module_has_table && !any_ref_func
- module_has_table: set if the module declares (TableSection) OR imports
(TypeRef::Table) any table, of any element type.
- any_ref_func: any defined function body contains an Operator::RefFunc.
If neither holds, no funcref to any defined function can exist anywhere (code,
table, global, or returned to the host), so no indirect/host dispatch is
possible and the recorded direct calls are provably the complete caller set —
the only case where narrowing is sound. Narrowing still fires for clean
direct-call modules (feat036_interproc_param_ranges → [5,10] unchanged).
Regression tests for both new counterexamples:
- feat036_exported_table_forces_top (exported funcref table, no in-module
call_indirect → ⊤)
- feat036_ref_func_forces_top (ref.func takes a func's address → ⊤)
CHANGELOG + FEAT-036 AC updated to document all three findings and the
root-cause-sound rule.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Belt-and-suspenders on top of the funcref-container predicate: match RefFunc / CallIndirect / ReturnCallIndirect / CallRef operators directly, so the gate stays sound even for malformed modules (a call_indirect with no table) and for dispatch ops the value interpreter scrubs to top without recording an edge. In valid Wasm these already imply module_has_table; this just removes the dependency on table-detection completeness — the class of 'an op slipped through' the clean-room kept finding. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…so escapes (clean-room)
Third clean-room pass refuted the funcref-container gate with a fourth
under-approximation: a `ref.func` to a defined function can appear in a GLOBAL
INIT EXPRESSION (or an element-segment item), with NO table and NO ref.func in
any function BODY. The body-only operator scan (`any_funcref_escape`) misses it,
so the gate narrowed a function whose reference the host can read from an
exported funcref global and `call_ref` with arbitrary args.
(module
(func (param i32) (result i32) local.get 0) ;; func 0
(global (export "g") funcref (ref.func 0)) ;; escapes func 0 to host
(func (export "direct") (result i32) i32.const 7 call 0))
-> old: param_ranges[func0] = [7,7] (UNSOUND)
-> new: param_ranges[func0] = Unknown (sound)
Fix: scan const positions too. New `func_ref_taken_in_const` flag, ORed into
`callers_fully_known`:
- GlobalSection: `const_expr_takes_func_ref(&g.init_expr)` (ref.func in init).
- ElementSection: `element_items_take_func_ref(&element.items)` — any segment
(active/passive/declared) naming functions or carrying a ref.func expression.
Two small helpers added next to `const_i32_offset`.
Regression test feat036_global_init_ref_func_forces_top. All 23 core tests +
clippy + fmt + rivet green. CHANGELOG + FEAT-036 AC document all four findings.
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.
The next planned loop (synth wishlist, #54): sound interprocedural parameter ranges.
What
CallEdge.arg_ranges: Vec<AbstractValue>— the abstract arguments at each call site, in parameter order (populated for direct calls; empty forcall_indirect/ signature-unknown imports).FunctionSummary.param_ranges: Vec<AbstractValue>— per parameter, the join ofarg_rangesover every direct call site reaching the function (e.g. a function called with5and10→[5, 10]).Soundness (the crux)
param_rangesisUnknown(⊤) for every parameter of a function that is exported, the start function, or reachable viacall_indirect— the external / over-approximate entry points whose arguments scry cannot bound — and ⊤ if any indirect edge is unsound. Only when scry has accounted for every caller (a non-exported, non-start function reached solely by direct, fully-resolved calls) does it join their arguments. So aparam_rangesentry is never narrower than some reachable call permits — it's an over-approximation of the incoming value, never an under-approximation.The args are harvested from the actual values
handle_callpops (not a fragile post-hoc stack lookup), so they're exactly what the call consumes.Surface
Both fields are library-only (read off the
scry-sai-coreAnalysisResult); the wasm wrapper ignores them (field-access mapping), so the WIT mirror and the frozen v1 JSON contract are unchanged — consistent withoperand_stack/function_meta.Traceability + tests
rivet validatePASS.feat036_interproc_param_ranges(join 5⊔10 = [5,10]) +feat036_exported_params_are_top(exported → ⊤). 19 core tests pass; clippy clean.Falsification statement
If a
param_rangesentry excludes an argument value that some reachable call actually passes — i.e. it's an under-approximation — the soundness claim is false. (Being clean-room-verified, focusing on the eligibility gating.)🤖 Generated with Claude Code