Skip to content

fix(#931): reconcile RV32 br exit edges onto the block's result register (CRITICAL) - #947

Open
avrabe wants to merge 3 commits into
mainfrom
fix/rv32-br-value-931
Open

fix(#931): reconcile RV32 br exit edges onto the block's result register (CRITICAL)#947
avrabe wants to merge 3 commits into
mainfrom
fix/rv32-br-value-931

Conversation

@avrabe

@avrabe avrabe commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

The bug

br out of a value-producing block discarded its value on RV32. The branch
computed into one register; the merge read a different one — the fallthrough
register. So the block yielded the not-taken path's value. synth compile
exited 0 with no warning.

(block $exit (result i32) (br $exit (i32.const 1)) (i32.const 0))

wasmtime → 1. RV32 → 0.

This is the most basic form of structured control flow carrying a value, so the
blast radius covers block, switch-style dispatch and label shadowing alike
(8 labels.wast assertions). Found by executing the official testsuite (#928).

Root cause

lower_br emitted a bare jal and moved nothing — and br does not pop. The
branch's value stayed on the vstack, so the fallthrough expression allocated a
different register to avoid the live one, and the merge read that one. The
stale vstack entry is the miscompile.

#343 already built this exact join for if/else arms (then_results /
reconcile_if_result). It was simply never applied to br edges. br_table's
own doc comment records that "plain Br/BrIf share the underlying
limitation" — br_table LOUD-DECLINES it, br shipped silent.

Fix

Every exit edge reconciles onto the frame's canonical result registers
(ControlFrame::br_results), and lower_br truncates the vstack to the
target's checkpoint so the fallthrough's own results are identifiable at end.

The fallthrough's moves are emitted before end_label, so they sit on the
fallthrough path only and the taken edge jumps over them — the same argument
#343 relies on. The first edge donates its own register where it safely can, so
the common single-br block emits no move at all.

Arity is the vstack delta above the frame checkpoint, so no block-type threading
(#509) is needed — the same delta br_table already uses. Edges that disagree
on arity LOUD-DECLINE rather than emit a half-reconciled join.

live_regs now also reserves open frames' br_results: after truncation the
canonical register is pinned by no vstack entry, and the fallthrough would
otherwise hand it straight back out as scratch.

Evidence — red-first, executed

scripts/repro/rv32_br_value_931_differential.py, CI-wired: 17 vectors run
under unicorn (RV32 ILP32) and compared against wasmtime.

result
pre-fix 9/17 FAIL
post-fix 17/17 PASS

Pre-fix failures are not all obvious: br64 returned 0x900000004 instead of
0x900000005 (subtly wrong i64, not visibly broken), carried returned 1
instead of 6, outer returned 0 instead of 42.

Vectors cover both edges of each shape — a fix that reconciled only one
direction would pass a single-edge vector: br_if taken/not-taken, two
value-carrying edges into one frame, i64 (both halves), a value live across
the block, arity-0 br, br 1 to an outer frame, and #930's nested shape
(correct on RV32 today by luck — pinned so it stays correct rather than lucky).

  • Frozen anchors 10/10 byte-identical (--test frozen_codegen_bytes)
  • cargo clippy --workspace --all-targets -- -D warnings → exit 0, 0 diagnostics
  • cargo test -p synth-backend-riscv257 passed, 0 failed

Two doc-vs-source defects found in the touched code

  1. live_regs claimed "locals/params are always copied into a fresh temp by
    lower_local_get". Falselower_local_get aliases a Port the ARM perf levers (cmp→select, local-promotion, imm-shift-fold) to the RISC-V backend — RV dissolved code is now behind ARM (2.12× vs 1.66× on silicon) #472-promoted
    local's s-register directly onto the vstack. Corrected.

  2. That aliasing is justified by "any op consuming this value allocates a fresh
    dst, so the s-reg is never clobbered by a consumer" — an argument that does
    not cover a br edge, which writes back into its operand at end.
    Donating a promoted local's register would clobber the local itself.

    What blocks it today is a rule in a different pass: promotion requires
    all_depth0, and br exists only at depth ≥ 1.
    canonicalize_edge_value guards it locally rather than borrowing soundness
    from that rule, and promotion_stays_depth0_or_931_guard_goes_live pins the
    coupling so relaxing all_depth0 reports here instead of silently
    miscompiling.

Not in scope

#930 (the thumb-2 sibling) is not fixed here. ARM has two codegen paths
(select_default vs select_with_stack, and --relocatable forces the direct
selector), so it needs its own red-first measurement to establish which path
is wrong. Separate PR — bundling it would make any frozen-byte movement
ambiguous to bisect.

Refs #931, #928

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

@avrabe

avrabe commented Aug 11, 2026

Copy link
Copy Markdown
Contributor Author

The chore: commit in this PR also un-reds main

main has been failing VCR-VER-004 instrument independence since 3eec0d37
(the wit-component 0.254→0.255 bump). Not a required context, so nothing was
blocked — but the cause is worth naming, because the oracle is fine and the
cleanup assertion is what fails:

OK   (1) validate_cfg_rewrite ACCEPTS the mutated rewrite
OK   (3) VCR-VER-004 REJECTS: result register R0 holds a different value ...
RESULT: PASS — the v0.53 mutation is now caught STATICALLY
##[group]Run git diff --exit-code
##[error]Process completed with exit code 1

The job asserts the mutation never persists, via git diff --exit-code. The
mutation was restored. What dirties the tree is Cargo.lock: the bump
changed the manifest but left an orphaned wasm-encoder 0.254.0 entry, so the
job's first cargo invocation regenerates the lock and the tree is no longer
clean.

Reproduced on a pristine origin/main worktree — clean before, and one
cargo metadata is enough:

before:  (clean)
after:   M Cargo.lock
         1 file changed, 21 deletions(-)

That is exactly the 21 lines the chore: commit here removes, so landing this
PR should restore that job. Worth watching on the next main run rather than
assuming.

It also makes #924's case concretely: the Version Pin Sweep does not gate
Cargo.lock, so a manifest bump can leave the lock stale, and the symptom
surfaces two commits later in an unrelated job's cleanup step.

@codecov

codecov Bot commented Aug 11, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 75.47170% with 39 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-backend-riscv/src/selector.rs 75.47% 39 Missing ⚠️

📢 Thoughts on this report? Let us know!

avrabe added a commit that referenced this pull request Aug 11, 2026
This branch's only failing check was **VCR-VER-004 instrument independence**,
and the oracle inside it PASSED — the failing step was its cleanup assert:

    ##[group]Run git diff --exit-code
    diff --git a/Cargo.lock b/Cargo.lock
    ##[error]Process completed with exit code 1

Not caused by anything in this PR. `main`'s wit-component 0.254->0.255 bump
left an orphaned `wasm-encoder 0.254.0` entry in the lock, so the job's first
cargo invocation regenerates it and the tree is no longer clean. `main` itself
has been red on this job since that bump.

Note the branch was clean LOCALLY before the rebase: it predated the bump, so
its lock matched its own manifest. CI checks out the branch MERGED with main,
where the new manifest meets the old lock. Rebasing onto main reproduces it,
and one `cargo metadata` fixes it — the same 21 deletions seen on a pristine
`origin/main` worktree and in #947.

Fixing the gate rather than merging past it: the check is not in main's
required nine, so this could have been waved through, but a red gate whose
cause is understood is a gate you can turn green.

Refs #929, #924

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Aug 11, 2026
Same cause as #947 and #943: main's wit-component 0.254->0.255 bump left an
orphaned `wasm-encoder 0.254.0` entry, so this job's first cargo invocation
regenerates the lock and its `git diff --exit-code` cleanup assert fails. The
oracle inside the job PASSES; only the tree-restore check is red.

Refs #928, #924

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
avrabe added a commit that referenced this pull request Aug 12, 2026
)

* RQ-56-CONF (#928): the wast assertions are EXECUTED, not discarded

tests/wast/ carries 381 assert_return and 2 assert_trap. Until now NONE were
checked: the only CI path over those files asserted that `synth compile` exits 0
and DISCARDED the expected values. The backend's primary correctness suite
graded 'did an ELF come out', not 'is it right' — the exit-0 vacuity class (#911,
the v0.54 sret_decide gate printing MISMATCH and exiting 0) sitting on the
correctness suite itself, and why three silent miscompiles (#929/#930/#931)
shipped and were found from outside.

The runner that CAN compare values (crates/synth-test) drives Renode over
telnet, so it cannot run on a stock runner and never has. This uses the
mechanism the differentials already use: compile, execute under unicorn, compare
against the .wast's OWN expected literal — the spec's answer, which is what
makes it conformance rather than a second opinion.

    #928 CHECKS=240/240 executed assertions over 25 wast files; 141 declined
      declined: i64-pair=118, memory-unmapped=23

From ZERO executed to 240. Declines are counted and NAMED, never silent; the 118
i64-pair declines are exactly where #929 lives, so enabling that is the
follow-up that would have caught it.

THE FIRST RUN FOUND A WRONG ASSERTION — ours, not synth's. large_compute(1):

    wasmtime   = 3538945
    synth      = 3538945   (agree)
    tests/wast = 287       (WRONG)

synth is correct; the hand-written expectation had drifted for free because it
had never once been executed. Corrected against wasmtime with the reasoning
recorded in the fixture. 239 of 240 hand-written expectations were right — but
nobody could have known which.

Non-vacuity in two places that cannot go quiet alone: the script FAILS on zero
executed assertions, and the CI step greps a three-digit CHECKS count.

Totals move to 137 oracles / 295,621 entries on all three pinned surfaces.
(Caught before push: `printf "%'d"` emitted the EUROPEAN separator, so the docs
briefly read 295.621 — and claim_check passed 43/43 anyway, because it pins
consistency ACROSS surfaces, not format correctness.)

fmt 0, clippy 0, 134 test suites, claim 43/43, wiring 161 scripts / 0 UNDECLARED.

Refs #928, RQ-56-CONF

* RQ-56-CONF: give the conformance gate a floor on the number that means something

Review catch on this PR: `# ci-checks: emulations >= 200` against a measured
263 let the executed-assertion count fall 240 -> 205 and still pass green. A
gate with that much slack does not detect the regression it exists to detect.

Two changes, because the obvious one alone is not enough:

1. `emulations >= 200` -> `>= 263` (the measured value; ratchet direction up).

2. A REAL floor inside the script, on `checked`. The `emulations` floor does
   NOT cover the executed count: `emulations` counts EMULATOR ENTRIES, and 23
   of the 263 are assertions that fault and then DECLINE (unmapped memory). So
   240 -> 205 executed could happen with `emulations` still at 263 and BOTH
   gates green. The old `if checked == 0` non-vacuity check is far too weak to
   catch it.

   The floor now lives on `checked`, asserted where it is computed:
   `min_executed = 240`.

Verified in both directions with true exit codes (not through a pipe, which
hides them): green leg exit 0; floor mutated to 999 -> exit 1 with the FAIL
message. The mutation was asserted to have applied before the run.

Ledger bumped with the floor: `--min-emulation-floor` 295621 -> 295684 in both
ci.yml and claims.yaml. `claim_check.py` 43/43; `oracle_wiring_check.py` exit 0.

Refs #928

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

* chore: regenerate Cargo.lock after rebase (un-reds VCR-VER-004)

Same cause as #947 and #943: main's wit-component 0.254->0.255 bump left an
orphaned `wasm-encoder 0.254.0` entry, so this job's first cargo invocation
regenerates the lock and its `git diff --exit-code` cleanup assert fails. The
oracle inside the job PASSES; only the tree-restore check is red.

Refs #928, #924

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

---------

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe and others added 3 commits August 12, 2026 06:13
…ter (CRITICAL)

`br` out of a value-producing `block` discarded its value: the branch computed
into one register and the merge read a different one, so the block yielded the
NOT-TAKEN path's value. `synth compile` exited 0 with no warning. This is the
most basic form of structured control flow carrying a value, so it broke
`block`, switch-style dispatch and label shadowing alike (8 `labels.wast`
assertions). Found by executing the official testsuite (#928).

    (block $exit (result i32) (br $exit (i32.const 1)) (i32.const 0))
    wasmtime -> 1        RV32 -> 0

## Root cause

`lower_br` emitted a bare `jal` and moved nothing, and `br` does not pop — so
the branch's value stayed on the vstack, the fallthrough expression allocated a
DIFFERENT register to avoid the live one, and the merge read that one. The
stale vstack entry IS the miscompile.

`#343` already built this exact join for `if`/`else` arms
(`then_results` / `reconcile_if_result`); it was simply never applied to `br`
edges. `br_table`'s doc comment even records that "plain Br/BrIf share the
underlying limitation" -- br_table LOUD-DECLINES it, `br` shipped silent.

## Fix

Every exit edge reconciles onto the frame's canonical result registers
(`ControlFrame::br_results`), and `lower_br` truncates the vstack to the
target's checkpoint so the fallthrough's own results are identifiable at `end`.
The moves for the fallthrough are emitted BEFORE `end_label`, so they sit on
the fallthrough path only and the taken edge jumps over them -- the same
argument #343 relies on. The first edge donates its own register where it
safely can, so the common single-`br` block emits no move at all.

Arity is the vstack delta above the frame checkpoint; no block-type threading
(#509) is needed. Edges that disagree on arity LOUD-DECLINE rather than emit a
half-reconciled join.

`live_regs` now also reserves open frames' `br_results`: after truncation the
canonical register is pinned by no vstack entry, and the fallthrough would
otherwise hand it straight back out as scratch.

## Evidence

`scripts/repro/rv32_br_value_931_differential.py` -- 17 vectors EXECUTED under
unicorn (RV32 ILP32) against wasmtime, CI-wired:

  pre-fix   9/17 FAIL   (simple=0 not 1; br64=0x900000004 not ...5 -- subtly
                         wrong, not obviously; carried=1 not 6; outer=0 not 42)
  post-fix 17/17 PASS

Covers both edges of each shape: br_if taken/not-taken, two value-carrying
edges into one frame, i64 (both halves), a value live ACROSS the block,
arity-0 `br`, `br 1` to an outer frame, and #930's nested shape (correct on
RV32 today by luck -- pinned so it stays correct rather than lucky).

Frozen anchors 10/10 byte-identical; clippy clean.

## Two doc-vs-source defects found in the touched code

- `live_regs` claimed "locals/params are always copied into a fresh temp by
  lower_local_get". False: `lower_local_get` aliases a #472-promoted local's
  s-register DIRECTLY onto the vstack. Corrected.
- That aliasing is justified by "any op consuming this value allocates a fresh
  dst, so the s-reg is never clobbered by a consumer" -- an argument that does
  NOT cover a `br` edge, which writes BACK into its operand at `end`. Donating
  a promoted local's register would clobber the local itself.

  What blocks it today is a rule in a DIFFERENT pass: promotion requires
  `all_depth0` and `br` exists only at depth >= 1. `canonicalize_edge_value`
  guards it locally anyway rather than borrowing soundness from that rule, and
  `promotion_stays_depth0_or_931_guard_goes_live` pins the coupling so
  relaxing `all_depth0` reports instead of silently miscompiling.

#930 (the thumb-2 sibling) is NOT fixed here -- ARM has two codegen paths and
needs its own red-first measurement. Separate PR.

Refs #931, #928

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…'s own floor

Review follow-ups on this PR. Both are about the same thing: a claim I made
without an instrument behind it.

## 1. Where the vstack-delta arity over-counts (the boundary was unpinned)

Arity is inferred as the vstack delta above the target frame's checkpoint,
because the decoder discards block types (#509). That OVER-COUNTS when
unrelated values sit on the stack below the branch's own value — which wasm
permits, since `br` is stack-polymorphic and discards the excess.

Measured both sides rather than reasoning about them:

  (block (result i32) (i32.const 9) (br 0 (i32.const 42)))
    -> COMPILES, executes, returns 42. Correct: the extra values are above the
       same checkpoint and the branch is the block's last act, so no
       fallthrough exists to disagree with.

  (block $a (result i32) (block $b (i32.const 9) (br $a (i32.const 42)))
                         (i32.const 7))
    -> LOUD-DECLINES. `$a`'s edge is credited with 2 values while its
       fallthrough produces 1, and without a declared arity there is no way to
       tell which position is the result.

Both are now unit tests. The second is a REACH REDUCTION and is documented as
one: v0.55 compiled that module and returned **0** where wasmtime says **42**,
so this replaces a silent wrong answer with a compile error. Threading real
block arities (#509) is what would let it compile.

I first read this shape as a miscompile in the new code. It was not — I had
executed a STALE object left behind by the previous run, because the compile
that should have replaced it failed and `-o` wrote nothing. Re-measured with
the artifact deleted first and the exit code checked; the decline is real
(exit 1, no object emitted).

## 2. The oracle printed a count instead of asserting one

`#931 EMULATIONS=17` printed `len(VECTORS)` — a constant, so it proved nothing
— and the header floor said `>= 16`, below the 17 measured. That is the same
defect this PR's sibling (#942) was just fixed for, shipped in the fix for it.

Now `executed` is counted where the emulator is actually entered, asserted
equal to the vector count, and the header raised to `>= 17`.

Verified by mutation, with the mutation asserted to have applied and the true
exit code read (not through a pipe): forcing one symbol lookup to miss yields
`EMULATIONS=16/17`, the FAIL line, and exit 1. A first mutation attempt was
discarded because it tripped wasmtime's export lookup instead of this
assertion — it would have "passed" for the wrong reason.

Refs #931

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
This PR adds `rv32_br_value_931_differential.py` with `ci-checks: emulations
>= 17`, taking the summed floor from 295684 (set by #942, merged) to 295701.

The gate is a MINIMUM, so leaving the ledger at 295684 would still have passed
— and that is exactly the drift this ledger exists to stop. A floor that
under-claims by 17 is a floor that would not notice 17 emulations
disappearing. Bumped in both surfaces it is pinned across.

`oracle_wiring_check.py --min-emulation-floor 295701` exit 0;
`claim_check.py` 43/43.

Refs #931

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
@avrabe
avrabe force-pushed the fix/rv32-br-value-931 branch from f1147eb to 0018b32 Compare August 12, 2026 04:13
avrabe added a commit that referenced this pull request Aug 12, 2026
…943)

* fix(#929): DECLINE a 64-bit call argument instead of miscompiling it

On thumb-2, a call whose parameter list contains an i64 marshalled arguments
into the wrong registers and exited 0 with no warning. gale measured, executed
under qemu against wasmtime:

    (func $g (param i64 i32) (result i32) (local.get 1))
    f(7)  -> wasmtime 7,  thumb-2 287454020
    f(42) -> wasmtime 42, thumb-2 287454020      (= 0x11223344, the i64 HIGH half)

ROOT CAUSE: emit_arg_moves maps ONE argument to ONE register
(arg_srcs[i] -> ARG_REGS[i]). AAPCS gives a 64-bit argument an EVEN-ALIGNED
register PAIR, so the high half was never placed and every later argument
shifted down one register.

Its docstring has always said it cannot do this — 'i64/f64 arguments, which
AAPCS passes in register *pairs*, are NOT marshalled' — and it marshalled them
anyway. A documented non-capability with nothing enforcing it is not a
limitation; it is a silent miscompile. pop_call_args already REFUSED the same
shape for STACK argument positions (#503); register positions never got the
equivalent. This adds it.

THE REFUSAL IS WIDER THAN THE REPORTED SHAPE, deliberately. gale recorded
(i32, i64) as correct. It is not: AAPCS places that i64 in r2:r3 while synth
puts its low half in r1. It looked right only because the callee under test
returned the i32, so the wrong i64 was never read. Refusing every i64 register
argument is the honest boundary; refusing only 'i64 not last' would leave an
accidental correctness in place to break later.

Outcome on the repro: the caller is OMITTED with a named #929 diagnostic
('1 of 2 functions were skipped'). No wrong bytes ship, and a consumer gets a
link error rather than a wrong answer.

FOLLOW-UP (named, and its oracle already exists): real AAPCS pair marshalling.
The #928 conformance gate declines 118 assertions as `i64-pair` — that is
exactly this capability, waiting to accept the implementation.

Red-first: removing the refusal fails both decline tests while the all-i32
regression guard stays GREEN, so the refusal is provably not a blanket one.

fmt 0, clippy 0, 135 test suites.

Refs #929, RQ-56-I64CALL

* chore: regenerate Cargo.lock after rebase (un-reds VCR-VER-004)

This branch's only failing check was **VCR-VER-004 instrument independence**,
and the oracle inside it PASSED — the failing step was its cleanup assert:

    ##[group]Run git diff --exit-code
    diff --git a/Cargo.lock b/Cargo.lock
    ##[error]Process completed with exit code 1

Not caused by anything in this PR. `main`'s wit-component 0.254->0.255 bump
left an orphaned `wasm-encoder 0.254.0` entry in the lock, so the job's first
cargo invocation regenerates it and the tree is no longer clean. `main` itself
has been red on this job since that bump.

Note the branch was clean LOCALLY before the rebase: it predated the bump, so
its lock matched its own manifest. CI checks out the branch MERGED with main,
where the new manifest meets the old lock. Rebasing onto main reproduces it,
and one `cargo metadata` fixes it — the same 21 deletions seen on a pristine
`origin/main` worktree and in #947.

Fixing the gate rather than merging past it: the check is not in main's
required nine, so this could have been waved through, but a red gate whose
cause is understood is a gate you can turn green.

Refs #929, #924

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

---------

Co-authored-by: Claude Opus 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

Development

Successfully merging this pull request may close these issues.

1 participant