feat(codegen): sound null-funcref-slot call_indirect — runtime null check (#664)#669
Merged
Merged
Conversation
…heck (#664) A table with null (uninitialized) funcref slots no longer poisons the closed-world type check: the verdict relaxes to "every INITIALIZED slot type-equal", and the null-slot trap (WASM Core §4.4.8) is discharged at RUNTIME — the layout contract links null slots as ZERO words and the dispatch null-checks the loaded pointer (cmp ip,#0; bne ok; udf) between the #642 bounds guard and the BLX, on both Thumb-2 and A32. Fully-initialized tables emit null_check=false, keeping the pre-#664 dispatch bytes identical BY CONSTRUCTION (whole-ELF cmp verified on the #642/#650/#594/#597 fixtures x cortex-m3/r5/m7dp x relocatable/self). New CI-gated differential (call_indirect_664_differential.py): sparse 4-slot table (slots 1,3 initialized) — initialized slots match wasmtime, null and OOB indices stop at a UDF; red at compile on origin/main (capability upgrade). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Codecov Report❌ Patch coverage is
📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Jul 8, 2026
…ed rules, 81 bridge Qed (#673) * chore(release): v0.36.0 — unreachable traps + sparse tables + 40 rules + 81 bridge Qed (#668/#669/#670/#671) Pin sweep 0.35.0 -> 0.36.0 + CHANGELOG. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore: fold #672 (post-exhaustion quality) into the v0.36.0 changelog — merged ahead of the tag Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Fable 5 <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
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.
Fixes #664. Builds on #650/#653 (multi-table R11 region) and #646 (the #642 closed-world guards).
The gap
call_indirecton a table with any null (uninitialized funcref) slot loud-declined: the #646 closed-world verifier treated an uninitialized slot as breaking the closed world for EVERY type ("the raw code-pointer table has no runtime null/type id to check"). Sound, but incomplete — component-model tables legitimately carry null slots (falcon-flight v1.112's(table 1 41 41)is sparsely populated), and WASM Core §4.4.8 says acall_indirectreaching one simply traps. All 20 of falcon's dispatch functions declined on this.The relaxation (design)
The closed-world type verdict relaxes from "every slot in
[0, size)initialized + type-equal" to "every INITIALIZED slot type-equal"; null slots become trap-on-call at runtime:synth-core):TableGuardsgainshas_null_slots.table_type_rejectno longer all-rejects on an uninitialized slot — it type-checks the initialized image and reports the null flag. A null slot can never produce a live callee of the wrong type, because the null check traps before the branch — so the type relaxation is sound. Heterogeneous initialized slots, unverifiable segments, growable imports: all still reject exactly as before.synth-synthesis):resolve_call_indirect_guardsreturns the flag; both arms (select_with_stack+select_default) thread it asArmOp::CallIndirect { null_check }.null_check, a three-insn null check lands between the pointer load and theBLX(same trap idiom as the thumb-2: call_indirect emits no bounds-check and no type-check — OOB/wrong-type index does an uncontrolled indirect branch instead of trapping (WASM 4.4.8) #642 bounds guard):The null-region guarantee (emission finding)
synth does not emit the funcref table region — the #650 layout contract has the runtime/harness link it at R11. This PR extends that contract (documented on
CallIndirectGuards): every uninitialized slot MUST be linked as a ZERO word. Zero is never a valid code pointer in the region, so the null check turns it into the deterministic trap. The differential harness links per this contract; meld/falcon integration inherits the same one-line rule (a BSS/zero-filled region satisfies it for free).Single-table / fully-initialized byte-identity — BY CONSTRUCTION, then verified
null_check: false(any fully-initialized table) skips the encoder branch entirely — the #650 offset-0 trick. Verified against an origin/main-built binary: whole-ELFcmpidentity, 24/24 — #642/#650/#594/#597 fixtures × cortex-m3/cortex-r5/cortex-m7dp ×--relocatable/self-contained. Frozen anchors 10/10.Oracle (CI-gated:
call-indirect-664-nullslot-oracle)scripts/repro/call_indirect_664_differential.py+call_indirect_664_nullslot.wat: 4-slot table, slots 1,3 initialized (two segments — the falcon shape), 0,2 null. Per case, unicorn-executed synth code (null slots linked as zero, decoys past the region) vs wasmtime:viadeclines (SYMBOL MISSING). Capability upgrade: red = "declines today", green = sound sparse dispatch.viarepro now compiles clean oncortex-m7dp(0 skips).Scope notes
call_indirectwas never lowered on RV32 (pre-existingunsupported wasm oploud-skip) — unchanged; the decoder relaxation is shared, so the RV32 lowering inherits the flag when it lands.CallIndirectstill declines atoptimizer_bridge(thumb-2: call_indirect emits no bounds-check and no type-check — OOB/wrong-type index does an uncontrolled indirect branch instead of trapping (WASM 4.4.8) #642) → stays direct-selector-only, on the test(vcr-oracle): estimator↔encoder agreement oracle for the optimized path (#498, #242) #511 oracle's exclusion list — verified, no estimator change.(ref.null)entries inside a segment still poison contents (unverifiable-contents rule unchanged); this PR addresses slots not covered by any segment — the falcon case.Workspace tests green (108 suites), fmt clean, clippy
-D warningsclean workspace-wide (chunked per-crate + full).🤖 Generated with Claude Code