Complex test case

[cpetig]

Another much more complex example is available in three modules at https://osxcar.com/examples/anti-pinch/ (the wasm binaries are encoded in base64 though).

[avrabe]

Analysis: Anti-Pinch Control System Feasibility

Thanks for the test case — this is exactly the kind of real-world automotive workload that validates (or exposes) Synth's capabilities.

Current Status

The anti-pinch control system would involve:

Capability	Status	Notes
Integer arithmetic	✅ Supported	ADD, SUB, MUL, DIV, REM all work
Bitwise operations	✅ Supported	AND, OR, XOR, shifts, rotations
Memory load/store	✅ Supported	With optional bounds checking
Control flow	✅ Supported	Block, loop, br, br_if, call
Multi-function modules	✅ Fixed	Now compiles all exports by default
Floating-point (PID loops)	❌ Rejected	Requires VFP/NEON hardware
Global variables	❌ Not yet	Needed for configuration state
i64 operations	❌ Not yet	Needs register pairs on 32-bit ARM

The Float Problem

A PID controller for motor control inherently uses floating-point arithmetic. As of commit 48f76e6, the transcoder explicitly rejects float operations rather than silently generating NOPs (which was the previous behavior — producing valid ARM binaries with completely wrong semantics).

Path Forward

In the PulseEngine architecture, this use case demonstrates exactly why mixed-mode execution matters:

1. Hot integer path → Synth transcodes to native ARM (provably correct)
2. Float-heavy PID/control loops → Run on the Kiln interpreter

The Kiln interpreter has complete WASM instruction coverage including all float operations. For an anti-pinch system:

• State machine logic, GPIO bit manipulation, timing → Synth (native ARM)
• PID computation, current sensing math → Kiln (interpreted, correct floats)

Alternatively, for Cortex-M4F targets with hardware FPU, we could add VFP instruction encoding in the future — but that's a significant extension beyond the current i32 transcoding table.

For Now

An integer-only version of the anti-pinch control is feasible today with fixed-point arithmetic (Q16.16 format using i32 ops). This is actually common practice in automotive embedded systems where deterministic timing matters more than floating-point precision.

[avrabe]

Triage Note

Good test case for validating real-world automotive workloads. The analysis comment above correctly identifies the gaps:

• Floating-point: Rejected at transcoding (correct behavior since commit 48f76e6)
• Global variables: Not yet supported
• i64 operations: Needs register pair support on 32-bit ARM

The integer-only subset could be tested today with fixed-point arithmetic (Q16.16). Full support requires either hardware FPU encoding (VFP/NEON for Cortex-M4F) or mixed-mode execution via Kiln interpreter (issue #34 M3+).

Keeping open as a tracking issue for this test case.

[avrabe]

Roadmap: Full Anti-Pinch Support

Analysis of the three WASM modules from https://osxcar.com/examples/anti-pinch/ shows the following feature gaps. All modules will arrive as flat core WASM (Meld fuses the Component Model away), so Synth only needs core instruction support.

Module Feature Matrix

Feature	Anti-Pinch (13KB)	Motor Driver (2.5KB)	Soft Start/Stop (1.8KB)
i32 ops	1,525 ops	193 ops	263 ops
f32 ops	170 ops	45 ops	95 ops
f64 ops	236 ops	177 ops	40 ops
i64 ops	3 ops	20 ops	—
global.get/set	33 uses	yes	yes
br_table	4	—	1
select	10	—	—
data segments	2	1	—

All three modules use floats deeply interleaved with integer logic (PID loops, PWM ramps, motor physics). No Kiln fallback — must be native ARM for cycle budget.

What Already Exists

The data model is ~80% there — the gap is in instruction selection and binary encoding:

• WasmOp: All f32/f64/i64 operations defined in synth-core/src/wasm_op.rs
• ArmOp: 66+ VFP pseudo-instructions defined in synth-synthesis/src/rules.rs
• Coq: VFP instruction variants declared in ArmInstructions.v
• Select: Optimizer bridge already transforms if-else→select (optimizer_bridge.rs)
• Missing: Instruction selector rejects all floats, ARM encoder has no VFP binary encoding

---

Task 1: ARM Target Profiles (Cortex-M3 / M4F / M7)

Currently hardcoded for Cortex-M3 (no FPU). Need configurable target that gates available instructions.

• Define target profiles: CortexM3 (no FPU), CortexM4F (FPv4-SP-D16), CortexM7 (FPv5-D16)
• CLI flag: --target cortex-m4f (default remains M3 for backwards compat)
• FPU initialization in startup code: enable CP10/CP11 via CPACR register
• Gate VFP instruction selection on target profile
• Instruction selector returns clear error when float ops hit a non-FPU target

Files: synth-core (target types), synth-backend/src/cortex_m.rs (FPU init), synth-cli (CLI flag), synth-synthesis/src/instruction_selector.rs (gating)

Task 2: global.get / global.set Support

All three modules use global.get/global.set for stack pointer management (~33 uses in anti-pinch alone). Foundational — nothing compiles without this.

• Runtime global storage: dedicated memory region or register mapping
• Stack pointer global (index 0) → map to dedicated ARM register or memory slot
• General globals → table in .bss section, indexed by global index
• Instruction selection: GlobalGet(n) → LDR from global table; GlobalSet(n) → STR to global table
• Handle mutable vs immutable globals
• Initialize globals from WASM global section (init expressions)

Files: synth-synthesis/src/instruction_selector.rs, synth-backend/src/elf_builder.rs (global table section)

Task 3: select and br_table Control Flow

State machine dispatch (br_table) and conditional values (select) are needed for anti-pinch logic.

select (partially done — optimizer path works, need direct selector):

• Wire WasmOp::Select → ArmOp::Select in instruction selector
• ARM encoding: CMP rcond, #0 + IT block + conditional MOV pair
• Already have Select { rd, rval1, rval2, rcond } pseudo-instruction

br_table (jump table dispatch):

• Instruction selection: BrTable → jump table pattern
• ARM encoding: TBB/TBH (table branch byte/halfword) for Thumb-2
• Emit jump table data in .text section after the TBB instruction
• Handle default branch target

Files: synth-synthesis/src/instruction_selector.rs, synth-backend/src/arm_encoder.rs

Task 4: VFP Floating-Point (f32 / f64)

The core work. Pseudo-instructions already defined — need selection rules and binary encoding.

VFP register file:

• VFP register allocator: S0–S31 (f32), D0–D15 (f64), S regs alias D regs
• Calling convention: S0 return, S0–S3 args (AAPCS-VFP)

Instruction selection (map WASM → ARM VFP):

• f32 arithmetic: F32Add→VADD.F32, F32Sub→VSUB.F32, F32Mul→VMUL.F32, F32Div→VDIV.F32
• f64 arithmetic: F64Add→VADD.F64, F64Sub→VSUB.F64, F64Mul→VMUL.F64, F64Div→VDIV.F64
• f32/f64 math: Abs→VABS, Neg→VNEG, Sqrt→VSQRT
• f32/f64 comparisons: VCMP + VMRS APSR_nzcv + conditional MOV
• Conversions: VCVT (f32↔f64, i32↔f32, i32↔f64)
• Float constants: VMOV immediate or literal pool (VLDR from .rodata)
• Float load/store: VLDR/VSTR (word-aligned)
• Min/Max/Copysign/Ceil/Floor/Trunc/Nearest: multi-instruction sequences

ARM binary encoding (VFP uses different encoding format from core ARM):

• VFP data processing encoding (cond | 1110 | opc1 | Vn | Vd | 101x | opc2 | Vm)
• VFP load/store encoding (VLDR/VSTR)
• VMOV variants (ARM↔VFP, immediate)
• VMRS/VMSR (status register transfer)
• Thumb-2 VFP encoding (T32 format)

Files: synth-synthesis/src/instruction_selector.rs, synth-backend/src/arm_encoder.rs, synth-synthesis/src/rules.rs (register types)

Task 5: i64 Register Pairs

Anti-pinch uses 3 i64 ops, motor driver uses 20. On 32-bit ARM, i64 requires register pairs.

• Register pair allocation: map i64 values to (Rn, Rn+1) pairs
• i64.const → two MOV instructions (lo + hi)
• i64.load / i64.store → LDRD / STRD (double-word)
• i64.extend_i32_s → sign-extend to register pair (MOV + ASR docs: Archive obsolete documentation #31)
• i64.and → AND on both halves
• i64.shl → complex: LSLS hi + ORR + LSL lo (3-4 instructions)
• i64.gt_u → CMP hi + conditional CMP lo (with carry)
• i64 arithmetic (add/sub) → ADDS/ADC, SUBS/SBC pairs

Files: synth-synthesis/src/instruction_selector.rs, synth-backend/src/arm_encoder.rs

---

Dependency Chain

Task 1 (ARM targets)     ← gates Task 4 (VFP)
Task 2 (globals)         ← foundational, all modules need it
Task 3 (select/br_table) ← independent
Task 4 (VFP f32/f64)     ← biggest effort, needs Task 1
Task 5 (i64 pairs)       ← independent of Task 4

Suggested order: 1 → 2 → 3 → 4 → 5

After all 5 tasks, the soft_start_stop module should compile first (no i64), then motor_driver and anti_pinch.

Milestone: Soft Start/Stop Compiles

First target — simplest module (1.8KB, no i64, 1 br_table):

• Needs: Tasks 1, 2, 3, 4
• Would validate the entire VFP pipeline end-to-end