Skip to content

feat(codegen): sound null-funcref-slot call_indirect — runtime null check (#664)#669

Merged
avrabe merged 1 commit into
mainfrom
feat/664-null-slot-call-indirect
Jul 8, 2026
Merged

feat(codegen): sound null-funcref-slot call_indirect — runtime null check (#664)#669
avrabe merged 1 commit into
mainfrom
feat/664-null-slot-call-indirect

Conversation

@avrabe

@avrabe avrabe commented Jul 8, 2026

Copy link
Copy Markdown
Contributor

Fixes #664. Builds on #650/#653 (multi-table R11 region) and #646 (the #642 closed-world guards).

The gap

call_indirect on 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 a call_indirect reaching 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:

  • Decoder (synth-core): TableGuards gains has_null_slots. table_type_reject no 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.
  • Selector (synth-synthesis): resolve_call_indirect_guards returns the flag; both arms (select_with_stack + select_default) thread it as ArmOp::CallIndirect { null_check }.
  • Encoder (Thumb-2 + A32): when null_check, a three-insn null check lands between the pointer load and the BLX (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):
    ldr.w  ip, [r11, ip]     ; (or the #650 add/ldr-imm form)
    cmp.w  ip, #0            ; #664 — only when the table has null slots
    bne    .+4
    udf    #0                ; §4.4.8 uninitialized-element trap
    blx    ip
    

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-ELF cmp identity, 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:

Scope notes

Workspace tests green (108 suites), fmt clean, clippy -D warnings clean workspace-wide (chunked per-crate + full).

🤖 Generated with Claude Code

…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

codecov Bot commented Jul 8, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 97.07602% with 5 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-synthesis/src/instruction_selector.rs 92.30% 3 Missing ⚠️
crates/synth-core/src/wasm_decoder.rs 96.42% 2 Missing ⚠️

📢 Thoughts on this report? Let us know!

@avrabe avrabe merged commit 6502277 into main Jul 8, 2026
33 checks passed
@avrabe avrabe deleted the feat/664-null-slot-call-indirect branch July 8, 2026 21:29
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

1 participant