Skip to content

feat(aarch64): div/rem + popcnt + f64↔i64 reinterpret — frontier to empty (#851)#858

Open
avrabe wants to merge 6 commits into
mainfrom
feat/aarch64-divrem-popcnt-851
Open

feat(aarch64): div/rem + popcnt + f64↔i64 reinterpret — frontier to empty (#851)#858
avrabe wants to merge 6 commits into
mainfrom
feat/aarch64-divrem-popcnt-851

Conversation

@avrabe

@avrabe avrabe commented Jul 23, 2026

Copy link
Copy Markdown
Contributor

Summary

L5 of the v0.51 hub. Flips the three op groups that previously loud-declined on -b aarch64. Gale's acceptance gate (scripts/repro/aarch64_matrix.sh) frontier goes popcnt div_s rem_s → empty (32 → 35 accepted ops, 86 → 91 native checks, all bit-identical vs wasmtime).

1. Integer div/rem (i32 + i64) — with WASM trap guards

div_{s,u} → A64 SDIV/UDIV; rem_{s,u}SDIV/UDIV + MSUB (rem = a − (a/b)·b).

Soundness (the #633/#666/#709 totality class): A64 divide is TOTAL where WASM is PARTIAL — SDIV/UDIV return 0 on ÷0 and INT_MIN on INT_MIN/−1, neither traps. So the lowering emits explicit WASM trap guards:

  • divisor == 0brkall four forms, full-width cbnz for i64 (a 32-bit test would miss a divisor like 0x1_0000_0000).
  • INT_MIN / −1 overflow → brksigned DIV only. rem_s(INT_MIN,−1) == 0 (no trap) falls out of MSUB naturally.

Aliasing follows the #776 rule: MSUB reads a, b AND the quotient at once, so every temp is allocated while a/b are still reserved on the value stack.

2. popcnt (i32 + i64)

A64 has no scalar popcount: fmov gpr→SIMD, CNT vN.8b, ADDV bN, vN.8b, fmov back. i32 uses fmov s (zero-fills upper lanes → CNT sees 4 value + 4 zero bytes); i64 uses fmov d.

3. f64↔i64 reinterpret (GI-FPU-001)

i64.reinterpret_f64 / f64.reinterpret_i64 → bit-preserving fmov x,d / fmov d,x. These WasmOp variants existed but were never decoded (convert_operator), so they globally declined. Un-dropping them at decode also un-blocks ARM's existing VFP lowering — verified every backend still emits OR loud-declines, never silent-drops: aarch64 + cortex-m7dp ARM emit; no-FPU ARM / single-precision Cortex-M / RV32 loud-decline. Cross-backend op-parity gate green.

Frontier: before → after

accepted ops native checks declined frontier
main (before) 32 86 popcnt div_s rem_s
this PR (after) 35 91 (empty)

Trap evidence

scripts/repro/aarch64_divrem_851_differential.py179 cases (34 trap cases) vs wasmtime, executed two ways: unicorn (brk→UcError) and natively on arm64 (each call forked, SIGTRAP observed by parent). Covers ÷0 (all forms, both widths), div_s INT_MIN/−1 TRAP, rem_s(INT_MIN,−1)==0, plus popcnt (both widths) and the reinterpret round-trip. Wired into the aarch64-oracle CI job (unicorn-gated there; native path exercised on the macos-latest native-matrix runner + locally). During bring-up the native matrix caught a real red — the div_s overflow-guard branch offset was off by one (+3+4), spuriously trapping div_s(7,2).

New encoders (llvm-mc ground-truth byte tests)

sdiv/udiv/msub (+64-bit), cnt_8b, addv_8b, cbnz64.

Verification

  • cargo test -p synth-backend-aarch64 --lib: 73/73
  • cargo test --workspace: green
  • cross-backend op-parity gate, frozen_codegen_bytes 10/10, all 7 aarch64 differentials, decline-honesty probe (3/3): green
  • fmt + clippy (synth-backend-aarch64, synth-core): clean
  • claim_check.py: 25/25 claims pass (the 2 generated-file staleness failures are status.json / FEATURE_MATRIX.md, regenerated by the coordinator at assembly per fix(claims): regenerate status.json + FEATURE_MATRIX for #803 trunc_sat ops (main is red) #805 — not hand-edited here)

Notes for coordinator / other lanes

  • Touches shared synth-core convert_operator (decode) — changes cross-backend op exposure for the two reinterpret ops. Behavior surface verified per-backend above; textual conflict risk with L3/L4 low.
  • The aarch64 selector op count rose (four new arm groups), so the generated aarch64_selector_ops figure changed — regenerate status.json + FEATURE_MATRIX.md at assembly.

Closes the div/rem/popcnt/reinterpret portion of #851.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

avrabe and others added 6 commits July 23, 2026 20:46
Lower the three op groups that previously loud-declined on -b aarch64:

- Integer div/rem (i32+i64): SDIV/UDIV, rem via MSUB (a-(a/b)*b). A64
  div is TOTAL where WASM is PARTIAL, so emit explicit WASM trap guards:
  divisor==0 -> brk (all four forms, full-width cbnz for i64) and, for
  SIGNED DIV only, INT_MIN/-1 overflow -> brk. rem_s(INT_MIN,-1)==0
  falls out of MSUB naturally (no overflow guard). Localized divrem
  closure; temps allocated while operands still reserved (the #776
  aliasing rule) so MSUB's simultaneous a/b/q reads never clobber.
- popcnt (i32+i64): SIMD fmov->CNT.8b->ADDV->fmov (A64 has no scalar
  popcnt). i32 uses fmov s (zero-fills upper lanes), i64 uses fmov d.
- f64<->i64 reinterpret (GI-FPU-001): fmov d,x / fmov x,d bit-casts.

New encoders (llvm-mc ground-truth byte tests): sdiv/udiv/msub (+64),
cnt_8b, addv_8b, cbnz64. All clang/llvm-mc verified.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L
…al (#851)

- Map F64ReinterpretI64/I64ReinterpretF64 in convert_operator (they had
  WasmOp variants but were never decoded, so globally declined). Now
  reaches the aarch64 fmov d,x / fmov x,d arms. Verified all backends
  either emit or LOUD-decline (never silent-drop): aarch64 emits;
  cortex-m7dp ARM emits i64_reinterpret_f64 / loud-declines the f64
  return (GI-FPU-002 ABI class); no-FPU ARM + RV32 loud-decline. Cross-
  backend op-parity gate green.
- Fix div_s INT_MIN/-1 overflow-guard branch offset (+3 -> +4: the two
  mov_imm halfwords make the skip span 3 insns, so b.ne targets +4 words).
  Caught red by the native matrix (div_s(7,2) spuriously TRAPped).
- New aarch64_divrem_851 execution differential: 152 wasmtime cases (34
  trap cases) verified native (SIGTRAP) + unicorn (brk). Proves div/rem
  by-zero (all forms, both widths) and div_s INT_MIN/-1 TRAP exactly
  where wasmtime traps; rem_s(INT_MIN,-1)==0 (no trap).

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

- Add the #851 div/rem trap-and-value execution oracle to the
  aarch64-oracle CI job.
- Remove div/rem/popcnt from the decline-honesty probe (they now lower
  and are execution-verified) and refresh the job comment. The probe now
  asserts only rounding + i64<->float conversions still loud-decline
  (3/3 green).

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

Extend the #851 differential beyond div/rem: i32/i64 popcnt (both widths,
including the i64 full-8-lane ADDV path) and the f64<->i64 reinterpret
round-trip (bit-identity) now execute vs wasmtime too — native SIGTRAP +
unicorn. 152 -> 179 cases. Gives the popcnt/reinterpret deliverables the
same execution bar as div/rem (previously byte-tested only).

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

codecov Bot commented Jul 23, 2026

Copy link
Copy Markdown

Codecov Report

❌ Patch coverage is 97.13115% with 7 lines in your changes missing coverage. Please review.

Files with missing lines Patch % Lines
crates/synth-backend-aarch64/src/selector.rs 97.56% 5 Missing ⚠️
crates/synth-core/src/wasm_decoder.rs 0.00% 2 Missing ⚠️

📢 Thoughts on this report? Let us know!

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