Skip to content

Read-before-write non-param local not zero-initialized (count_params misclassifies it as a param) #457

Description

@avrabe

Summary

A wasm non-param local that is read before it is first written is miscompiled by the ARM backend: it is read from a parameter register instead of yielding 0. Wasm semantics zero-initialize non-param locals, so such a read must produce 0.

Minimal repro

scripts/repro/read_before_write_local_zeroinit.wat:

(module
  (func (export "rbw") (param i32) (result i32)
    (local i32)                              ;; local 1: never written → must read 0
    (i32.add (local.get 0) (local.get 1))))  ;; must return p0 + 0 = p0
$ synth compile scripts/repro/read_before_write_local_zeroinit.wat -o /tmp/rbw.elf --target cortex-m4 --relocatable
$ arm-none-eabi-objdump -d -M force-thumb /tmp/rbw.elf
00000000 <func_0>:
   0: b510   push {r4, lr}
   2: 1842   adds r2, r0, r1   <-- reads incoming r1 (caller garbage); should add 0
   4: 4610   mov  r0, r2
   6: bd10   pop  {r4, pc}

Expected r0 = r0 (+ 0); actual r0 = r0 + r1 where r1 is undefined (function has one param).

Root cause

count_params (crates/synth-backend/src/arm_backend.rs:126) does not consult the declared function signature — it infers the param count from access patterns: a local whose first access is a read (is_read_first) is assumed to be a param, and num_params = max(read-first idx) + 1. A zero-init read-before-write local is therefore indistinguishable from a param: it gets homed in / read from a parameter register rather than zero-initialized.

This also surfaced as a spurious #359: function has N params; ... at most 8 scalar params refusal on a function with 2 real params + several read-before-write locals (the inferred count crossed 8).

Fix direction

Plumb the declared param count (already available as current_func_params_i64 / the function type) through CompileConfig → selector instead of inferring it in count_params. Then a read-before-write non-param local lands in compute_local_layout and must be zero-initialized at entry (mov r,#0 for a promoted reg / str of a zeroed reg for a frame slot, emitted once at function entry for any non-param local with no dominating write).

Reachability / severity

Real-producer reachability is unconfirmed — most C/Rust→wasm producers write locals before reading, but the wasm spec permits read-before-write and some optimizing passes (incl. loom dissolution) may rely on zero-init. Filing to track; severity depends on whether a real module hits it.

Relation to VCR-RA local promotion (#390, #242)

Found while building the local-promotion validation fixture. Promotion v1 declines read-before-write locals by construction (promotes only locals whose defining local.set dominates every read), so it does not reintroduce this as a register bug — but it cannot fix the underlying frame-path miscompile, hence this separate issue.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions