From a54d6c1974b65097c1972579e8249506878609e7 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 19 Mar 2026 07:43:59 +0100 Subject: [PATCH] feat: add complex control flow tests and platform/CM rivet artifacts Complex test case (#36): 17 end-to-end control flow tests covering nested blocks, loops with br_if exit, if/else, br_table dispatch, fibonacci, factorial, deeply nested blocks, loop re-entry, call in loop, early return, unreachable traps, and sequential loops. Rivet artifacts for full traceability: - component-model.yaml: 14 artifacts (CM-001..005 system-reqs, CM-TR-001..006 sw-reqs, CM-VER-001..003 verification) tracing WASI Component Model integration with kiln via BA RFC #46 - target-platforms.yaml: 8 artifacts (TP-001..008) capturing Cortex-M4F/M7/M33 targets, STM32F407/nRF52840 board profiles, vector tables, MPU, and Renode emulation platform - zephyr-integration.yaml: 10 artifacts (ZI-001..010) for Zephyr RTOS integration including CMake build, AAPCS compliance, memory domains, calculator app, PID demo, and linker scripts Closes #36 Implements: FR-002 Implements: FR-005 Trace: skip Co-Authored-By: Claude Opus 4.6 (1M context) --- artifacts/component-model.yaml | 436 +++++++ artifacts/target-platforms.yaml | 261 ++++ artifacts/zephyr-integration.yaml | 341 +++++ .../src/instruction_selector.rs | 1127 +++++++++++++++++ 4 files changed, 2165 insertions(+) create mode 100644 artifacts/component-model.yaml create mode 100644 artifacts/target-platforms.yaml create mode 100644 artifacts/zephyr-integration.yaml diff --git a/artifacts/component-model.yaml b/artifacts/component-model.yaml new file mode 100644 index 0000000..7119ba3 --- /dev/null +++ b/artifacts/component-model.yaml @@ -0,0 +1,436 @@ +# Component Model Integration (ASPICE SYS.2 / SWE.1) +# +# System: Synth -- WebAssembly-to-ARM Cortex-M AOT compiler +# +# Defines the WASI Component Model integration between synth (AOT compiler) +# and kiln (runtime). Captures the dependency on kiln for Component Model +# runtime support, the BA RFC #46 lower-component architecture, and the +# canonical ABI contract that synth-abi must satisfy. +# +# References: +# - BA RFC #46: https://github.com/bytecodealliance/rfcs/pull/46 +# - Component Model Canonical ABI: https://github.com/WebAssembly/component-model/blob/main/design/mvp/CanonicalABI.md +# - WIT specification: https://github.com/WebAssembly/component-model/blob/main/design/mvp/WIT.md +# +# Format: rivet generic-yaml + +artifacts: + # --------------------------------------------------------------------------- + # System-level requirements for Component Model integration + # --------------------------------------------------------------------------- + + - id: CM-001 + type: system-req + title: Canonical ABI compatibility with kiln runtime + description: > + Synth's canonical ABI implementation (synth-abi crate) shall produce + lift/lower sequences that are byte-compatible with kiln's canonical ABI + implementation (kiln-component canonical_abi module). This covers type + sizes, field alignment, string encoding (UTF-8, UTF-16, Latin-1), + discriminant layout for variants/options/results, and list (ptr, len) + representation. Disagreement between synth-abi and kiln's canonical ABI + on any type layout is a blocking defect (per kiln:SR-11 cross-toolchain + requirement). + status: draft + tags: [component-model, canonical-abi, cross-toolchain, kiln-dependency] + links: + - type: derives-from + target: BR-003 + - type: traces-to + target: FR-001 + - type: traces-to + target: kiln:SR-11 + - type: traces-to + target: kiln:SR-10 + - type: traces-to + target: kiln:SR-9 + fields: + req-type: interface + priority: must + spec-reference: "Component Model Canonical ABI specification" + verification-criteria: > + Shared type layout fixtures exercised through both synth-abi and + kiln canonical_abi produce identical byte sequences for all WIT + type families (primitives, records, variants, options, results, + lists, strings, enums, flags). + + - id: CM-002 + type: system-req + title: Component lowering to core module (BA RFC #46 architecture) + description: > + Synth shall support the BA RFC #46 lower-component architecture where + WebAssembly components are lowered to core modules before AOT compilation. + In this architecture, component imports/exports are resolved to core + module imports/exports with canonical ABI wrappers, and host intrinsics + (memory management, stream I/O, resource lifecycle) are provided by + kiln-builtins or meld's fuser. Synth's role is to AOT-compile the + resulting core module to ARM machine code; kiln provides the runtime + host intrinsics that the compiled code calls via the __meld_dispatch_import + bridge interface. + status: draft + tags: [component-model, rfc46, lower-component, kiln-dependency] + links: + - type: derives-from + target: BR-002 + - type: derives-from + target: BR-003 + - type: traces-to + target: FR-001 + - type: traces-to + target: FR-004 + - type: traces-to + target: kiln:REQ_FUNC_014 + - type: traces-to + target: kiln:REQ_HELPER_ABI_001 + fields: + req-type: functional + priority: must + spec-reference: "BA RFC #46 — lower-component tool" + verification-criteria: > + A WASM component lowered via meld's fuser compiles through synth + to an ARM ELF binary that successfully calls kiln-builtins host + intrinsics at runtime. + + - id: CM-003 + type: system-req + title: Host intrinsic ABI stability contract with kiln + description: > + Synth-compiled code shall call kiln-builtins host intrinsics using + the stable C ABI defined by kiln:SR-BUILTIN-ABI. The function + signatures for memory operations (kiln_memory_copy, kiln_memory_fill, + kiln_memory_grow), atomic operations (kiln_atomic_wait, + kiln_atomic_notify), and Component Model runtime operations (resource + new/rep/drop, stream read/write, waitable set operations) shall be + consumed from a machine-readable ABI definition (WIT or C header) + at synth build time. ABI version mismatches shall be detected at + link time, not at runtime. + status: draft + tags: [component-model, abi-stability, kiln-dependency, rfc46] + links: + - type: derives-from + target: BR-001 + - type: derives-from + target: BR-003 + - type: traces-to + target: FR-001 + - type: traces-to + target: FR-004 + - type: traces-to + target: kiln:SR-BUILTIN-ABI + - type: traces-to + target: kiln:SR-MELD-COMPAT + fields: + req-type: interface + priority: must + spec-reference: "BA RFC #46 — Host-Guest C API" + verification-criteria: > + Integration test compiles a component through meld+synth and + executes against kiln-builtins; CI detects ABI signature + mismatches between synth codegen and kiln-builtins declarations. + + - id: CM-004 + type: system-req + title: WASI Preview 2 dispatch compatibility + description: > + Synth-compiled modules calling WASI Preview 2 interfaces shall use + the same canonical ABI lowered calling convention as kiln's unified + WASI dispatcher (kiln:REQ_FUNC_034). WASI calls from synth-compiled + code pass through the HostImportHandler trait interface, which kiln's + WasiDispatcher implements. The dispatch path shall support both + dispatch_core (canonical ABI lowered i32/i64 + memory pointers) and + dispatch_core_v2 (two-phase allocation for host-side cabi_realloc). + status: draft + tags: [component-model, wasi, canonical-abi, kiln-dependency] + links: + - type: derives-from + target: BR-003 + - type: traces-to + target: FR-001 + - type: traces-to + target: kiln:REQ_FUNC_034 + - type: traces-to + target: kiln:AC-WASI + fields: + req-type: interface + priority: must + spec-reference: "WASI Preview 2" + verification-criteria: > + Synth-compiled module calling wasi:cli/stdout produces output + when executed with kiln's WasiDispatcher as the host import + handler. + + - id: CM-005 + type: system-req + title: RFC #46 async intrinsic support for AOT compilation + description: > + Synth shall support AOT compilation of modules that use RFC #46 async + intrinsics (thread management, stream/future I/O, waitable sets). + For AOT-compiled code on embedded targets, async operations shall be + backed by kiln-builtins host intrinsics that delegate to the target + RTOS (e.g., gale tasks on gale targets, Zephyr threads on Zephyr + targets). Synth generates the call stubs; kiln provides the runtime + implementation. + status: planned + tags: [component-model, rfc46, async, kiln-dependency] + links: + - type: derives-from + target: BR-002 + - type: derives-from + target: BR-003 + - type: traces-to + target: FR-001 + - type: traces-to + target: FR-004 + - type: traces-to + target: kiln:FR-RFC46-THREAD + - type: traces-to + target: kiln:FR-RFC46-STREAM + - type: traces-to + target: kiln:FR-RFC46-RESOURCE + - type: traces-to + target: kiln:FR-RFC46-WAITABLE + fields: + req-type: functional + priority: should + spec-reference: "BA RFC #46 — Thread/Stream/Future/Waitable intrinsics" + verification-criteria: > + Synth-compiled module using thread_new and stream_read/write + compiles to ARM code containing correct host intrinsic call + sequences; execution verified on Renode with kiln-builtins stub. + + # --------------------------------------------------------------------------- + # Software-level requirements for synth-abi canonical ABI implementation + # --------------------------------------------------------------------------- + + - id: CM-TR-001 + type: sw-req + title: Canonical ABI type layout computation + description: > + synth-abi shall compute type sizes and alignments for all WIT type + families exactly matching the Component Model Canonical ABI + specification: primitives (bool=1, s8/u8=1, s16/u16=2, s32/u32/f32/ + char=4, s64/u64/f64=8), strings and lists (ptr+len = 8 bytes, align 4), + records (field offsets via align_up, total size rounded to max + alignment), variants/options/results (discriminant + aligned payload), + tuples, enums, and flags. The align_to function shall use + ceiling division: align_to(x, a) = ((x + a - 1) / a) * a. + status: implemented + tags: [canonical-abi, type-layout, synth-abi] + links: + - type: derives-from + target: CM-001 + - type: refines + target: FR-001 + fields: + req-type: functional + priority: must + crate: synth-abi + verification-criteria: > + Unit tests verify size_of and alignment_of for all WIT type + families; cross-validation against kiln canonical_abi sizes. + + - id: CM-TR-002 + type: sw-req + title: Canonical ABI lift/lower for primitive types + description: > + synth-abi shall implement lift (core WASM values to Component Model + values) and lower (Component Model values to core WASM values) for + all primitive types: bool, s8, u8, s16, u16, s32, u32, s64, u64, + f32, f64. Roundtrip identity shall hold: lift(lower(v)) == v for + all valid values. + status: implemented + tags: [canonical-abi, lift-lower, primitives, synth-abi] + links: + - type: derives-from + target: CM-001 + - type: refines + target: FR-001 + fields: + req-type: functional + priority: must + crate: synth-abi + verification-criteria: > + Roundtrip tests for all primitive types; edge cases (min/max + values, NaN for floats) verified. + + - id: CM-TR-003 + type: sw-req + title: Canonical ABI lift/lower for compound types + description: > + synth-abi shall implement lift/lower for compound types: strings + (UTF-8, UTF-16, Latin-1 encodings via AbiOptions), lists (element + size and alignment-aware), records (field-by-field with alignment), + variants (discriminant + payload), options (None/Some discriminant), + results (Ok/Err discriminant), enums (case index), and flags + (bitset). All compound type operations use the Memory trait for + linear memory access. + status: implemented + tags: [canonical-abi, lift-lower, compound-types, synth-abi] + links: + - type: derives-from + target: CM-001 + - type: refines + target: FR-001 + fields: + req-type: functional + priority: must + crate: synth-abi + verification-criteria: > + Roundtrip tests for all compound types; string encoding + roundtrips (UTF-8, UTF-16, Latin-1); record alignment verified; + variant/option/result discriminant layout verified. + + - id: CM-TR-004 + type: sw-req + title: Memory trait for portable linear memory access + description: > + synth-abi shall define a Memory trait abstracting linear memory + operations (read, write, allocate, free) with bounds-checked access. + Out-of-bounds access shall return AbiError::Trap. The trait shall + be implementable by both synth's test harness (SimpleMemory) and + kiln's runtime memory (via adapter). The allocator shall support + alignment-aware allocation for the canonical ABI realloc pattern. + status: implemented + tags: [canonical-abi, memory, synth-abi] + links: + - type: derives-from + target: CM-001 + - type: refines + target: FR-003 + fields: + req-type: functional + priority: must + crate: synth-abi + verification-criteria: > + Memory trait operations are bounds-checked; SimpleMemory tests + verify alignment-aware allocation; out-of-bounds access produces + AbiError::Trap. + + # --------------------------------------------------------------------------- + # SW-level requirements for component lowering codegen (planned) + # --------------------------------------------------------------------------- + + - id: CM-TR-005 + type: sw-req + title: Import dispatch stub generation for lowered components + description: > + synth-synthesis shall generate ARM call stubs for component import + dispatch via the __meld_dispatch_import bridge. Each component import + shall be lowered to: (1) canonical ABI lower of arguments into linear + memory, (2) a BL (branch-and-link) call to the host intrinsic import + stub, (3) canonical ABI lift of return values. The stub generation + shall be driven by the WIT interface type signatures extracted during + frontend parsing. + status: planned + tags: [component-model, codegen, import-dispatch, synth-synthesis] + links: + - type: derives-from + target: CM-002 + - type: derives-from + target: CM-003 + fields: + req-type: functional + priority: must + crate: synth-synthesis + verification-criteria: > + Generated ARM stubs for a test WIT interface contain correct + BL instruction to import dispatch; argument lowering verified + by Z3 SMT or Renode execution. + + - id: CM-TR-006 + type: sw-req + title: Host intrinsic signature validation at compile time + description: > + synth-cli shall validate that all host intrinsic imports in a + meld-fused core module match the expected kiln-builtins ABI + signatures before beginning synthesis. Signature mismatches + (parameter count, parameter types, return types) shall produce + a compile-time error with the expected vs actual signature. + status: planned + tags: [component-model, validation, abi-stability, synth-cli] + links: + - type: derives-from + target: CM-003 + fields: + req-type: functional + priority: must + crate: synth-cli + verification-criteria: > + Module with mismatched host intrinsic signature rejected at + compile time; valid signatures accepted. + + # --------------------------------------------------------------------------- + # Verification artifacts for Component Model integration + # --------------------------------------------------------------------------- + + - id: CM-VER-001 + type: sw-verification + title: Canonical ABI roundtrip tests + description: > + Tests verifying that lift(lower(v)) == v for all supported WIT type + families in synth-abi. Covers primitives, strings (all three + encodings), records, variants, options, results, enums, flags, and + lists. These tests exercise the same code paths that synth-compiled + modules use for component boundary crossings. + status: implemented + tags: [canonical-abi, roundtrip, synth-abi] + links: + - type: verifies + target: CM-TR-001 + - type: verifies + target: CM-TR-002 + - type: verifies + target: CM-TR-003 + - type: verifies + target: CM-TR-004 + fields: + method: automated-test + steps: + run: "cargo test -p synth-abi" + coverage: "Roundtrip tests for all WIT type families; Memory trait tests" + + - id: CM-VER-002 + type: sw-verification + title: Cross-toolchain canonical ABI compatibility tests + description: > + Integration tests verifying that synth-abi and kiln's canonical ABI + produce identical byte layouts for shared type fixtures. Tests + exercise type size computation, field alignment, string encoding, + and discriminant layout across both implementations. Required by + kiln:SR-24 (shared wit-bindgen fixtures). + status: planned + tags: [canonical-abi, cross-toolchain, integration] + links: + - type: verifies + target: CM-TR-001 + fields: + method: automated-test + steps: + run: "Shared fixture suite (planned)" + coverage: "Type layout compatibility across synth-abi and kiln canonical_abi" + + - id: CM-VER-003 + type: sw-verification + title: Component lowering end-to-end test + description: > + End-to-end test verifying that a WASM component, lowered via meld's + fuser to a core module, compiles through synth to an ARM ELF binary + that successfully executes with kiln-builtins host intrinsics on a + Cortex-M4 target (Renode emulation). Validates the full BA RFC #46 + pipeline: component -> meld fuse -> synth compile -> kiln execute. + status: planned + tags: [rfc46, end-to-end, integration, cross-toolchain] + links: + - type: verifies + target: CM-TR-005 + - type: verifies + target: CM-TR-006 + fields: + method: simulation + preconditions: + - Meld fuser available + - Kiln-builtins compiled for ARM target + - Renode emulator available + steps: + run: "bazel test //tests/component-model/... (planned)" + coverage: "Component -> core lowering -> AOT compile -> execute" diff --git a/artifacts/target-platforms.yaml b/artifacts/target-platforms.yaml new file mode 100644 index 0000000..94291b2 --- /dev/null +++ b/artifacts/target-platforms.yaml @@ -0,0 +1,261 @@ +# Target Platform Requirements (ASPICE SYS.2 / SWE.1) +# +# System: Synth -- WebAssembly-to-ARM Cortex-M AOT compiler +# +# Defines target hardware platforms, board support, and memory maps. +# These requirements capture the concrete hardware targets synth must +# support for Zephyr-based and bare-metal deployments. +# +# Format: rivet generic-yaml + +artifacts: + # --------------------------------------------------------------------------- + # Target Cortex-M variant requirements + # --------------------------------------------------------------------------- + + - id: TP-001 + type: system-req + title: Cortex-M4F primary target support + description: > + Synth shall produce correct bare-metal ELF binaries for ARM Cortex-M4F + targets (ARMv7E-M architecture, Thumb-2 ISA, single-precision FPU, + 8 MPU regions). This is the primary compilation target for both Renode + emulation testing and Zephyr RTOS deployment. The Renode test platform + emulates a Cortex-M4 at 0x0 flash / 0x20000000 SRAM with 72 MHz + SysTick (synth_cortex_m.repl). + status: implemented + tags: [cortex-m4, target, primary] + links: + - type: refines + target: FR-005 + - type: derives-from + target: BR-003 + fields: + req-type: functional + priority: must + verification-criteria: > + Cortex-M4 Renode emulation tests pass (bazel test //tests/...); + generated ELF boots and executes add(5,3)=8 on emulated target. + + - id: TP-002 + type: system-req + title: STM32F407 board profile + description: > + Synth shall include an STM32F407 board profile with correct memory + map (flash at 0x08000000, 1 MB; SRAM at 0x20000000, 128 KB + 64 KB + CCM), 8 MPU regions, single-precision VFP, and STM32-standard linker + script generation (ENTRY(Reset_Handler), .isr_vector, .text, .data + AT> FLASH, .bss, .stack, .heap sections). This covers STM32F4-Discovery + and Nucleo-F407ZG boards used with Zephyr. + status: implemented + tags: [stm32f407, board-profile, zephyr] + links: + - type: derives-from + target: BR-003 + - type: refines + target: FR-005 + - type: refines + target: FR-003 + - type: traces-to + target: ARCH-003 + - type: traces-to + target: ARCH-005 + fields: + req-type: functional + priority: must + board: STM32F407 + cpu: cortex-m4f + flash-base: "0x08000000" + flash-size: "1 MB" + ram-base: "0x20000000" + ram-size: "192 KB (128 KB SRAM + 64 KB CCM)" + mpu-regions: 8 + fpu: single-precision + verification-criteria: > + HardwareCapabilities::stm32f407() returns correct values; + LinkerScriptGenerator::new_stm32() produces valid linker script + with 0x08000000 flash origin. + + - id: TP-003 + type: system-req + title: Nordic nRF52840 board profile + description: > + Synth shall include a Nordic nRF52840 board profile with correct + memory map (flash at 0x00000000, 1 MB; SRAM at 0x20000000, 256 KB), + 8 MPU regions, single-precision VFP, and BLE-friendly memory layout. + The nRF52840-DK is a primary Zephyr development board for PulseEngine + hardware testing (issue #22). + status: implemented + tags: [nrf52840, board-profile, zephyr, ble] + links: + - type: refines + target: FR-005 + - type: derives-from + target: BR-003 + - type: traces-to + target: ARCH-003 + - type: traces-to + target: ARCH-005 + fields: + req-type: functional + priority: must + board: nRF52840-DK + cpu: cortex-m4f + flash-base: "0x00000000" + flash-size: "1 MB" + ram-base: "0x20000000" + ram-size: "256 KB" + mpu-regions: 8 + fpu: single-precision + verification-criteria: > + HardwareCapabilities::nrf52840() returns correct values; + MPUAllocator with nrf52840 config allocates regions correctly + (test_nrf52840_configuration test). + + - id: TP-004 + type: system-req + title: Cortex-M7 extended target support + description: > + Synth shall support ARM Cortex-M7 targets (ARMv7E-M, Thumb-2 ISA) + with both single-precision and double-precision FPU variants (M7 + and M7DP in CortexMVariant), 16 MPU regions, and higher-performance + memory configurations. Targets include STM32H7 and i.MX RT series. + status: draft + tags: [cortex-m7, target, extended] + links: + - type: refines + target: FR-005 + - type: derives-from + target: BR-003 + fields: + req-type: functional + priority: should + cpu: cortex-m7 + mpu-regions: 16 + fpu: "single or double precision" + verification-criteria: > + TargetSpec::cortex_m7() and cortex_m7dp() return correct specs; + double-precision FPU flag correctly set for M7DP variant. + + - id: TP-005 + type: system-req + title: Cortex-M33 TrustZone target support + description: > + Synth shall support ARM Cortex-M33 targets (ARMv8-M Mainline) with + TrustZone security extensions (SAU, IDAU) for secure/non-secure + partitioning. The M33 variant in CortexMVariant shall report + has_trustzone()=true. This enables future integration with Zephyr's + TF-M (Trusted Firmware-M) support for secure WASM module isolation. + status: draft + tags: [cortex-m33, trustzone, target, security] + links: + - type: refines + target: FR-005 + - type: refines + target: FR-008 + - type: derives-from + target: BR-003 + fields: + req-type: functional + priority: should + cpu: cortex-m33 + triple: "thumbv8m.main-none-eabi" + verification-criteria: > + CortexMVariant::M33.has_trustzone() returns true; + TargetSpec from_triple("thumbv8m.main-none-eabi") succeeds + (currently not in from_triple -- needs implementation). + + - id: TP-006 + type: system-req + title: Vector table and startup code generation + description: > + Synth shall generate correct ARM Cortex-M vector tables and startup + code for all supported target variants. The vector table shall + include initial stack pointer, Reset_Handler, and 14 standard + exception handlers (NMI, HardFault, MemManage, BusFault, + UsageFault, SVC, DebugMon, PendSV, SysTick) plus configurable + external IRQ handlers. Reset handler startup code shall initialize + R11 as WASM linear memory base (0x20000000), optionally enable FPU + (CPACR CP10+CP11), and transfer control to user code. All handler + addresses shall have Thumb bit (bit 0) set. + status: implemented + tags: [vector-table, startup, cortex-m] + links: + - type: derives-from + target: BR-003 + - type: refines + target: FR-005 + - type: refines + target: FR-002 + - type: traces-to + target: ARCH-003 + fields: + req-type: functional + priority: must + verification-criteria: > + Vector table binary has correct Thumb-mode addresses; + startup code initializes R11 to 0x20000000; + FPU enable code writes CPACR at 0xE000ED88 with DSB+ISB barriers. + + - id: TP-007 + type: system-req + title: MPU region allocation for WASM memories + description: > + Synth shall generate MPU region configurations that map WASM linear + memories to power-of-2 sized hardware protection regions. The MPU + allocator shall respect the target's available region count (8 for + M3/M4, 16 for M7), validate base address alignment to region size, + detect overlapping regions, and generate C initialization code + (MPU_TYPE, MPU_CTRL, MPU_RNR, MPU_RBAR, MPU_RASR register writes). + Subregion disable masks shall be supported for finer-grained + protection within a region. + status: implemented + tags: [mpu, memory-protection, cortex-m] + links: + - type: derives-from + target: BR-001 + - type: refines + target: FR-003 + - type: refines + target: FR-008 + - type: traces-to + target: ARCH-003 + - type: traces-to + target: ARCH-005 + fields: + req-type: functional + priority: must + verification-criteria: > + MPUAllocator allocates correct region sizes for 64KB WASM pages; + RBAR and RASR register values encode permissions and attributes; + overlapping allocation is rejected with error. + + - id: TP-008 + type: system-req + title: Generic Cortex-M emulation platform + description: > + Synth shall support a generic Cortex-M memory layout (flash at 0x0, + 256 KB; RAM at 0x20000000, 64 KB) suitable for QEMU and Renode + emulation testing. The Renode platform description (synth_cortex_m.repl) + uses this layout with NVIC at 0xE000E000 and 72 MHz SysTick frequency. + This is the default target when --cortex-m is specified without a + board name. + status: implemented + tags: [emulation, renode, qemu, testing] + links: + - type: derives-from + target: BR-003 + - type: refines + target: FR-002 + - type: refines + target: FR-005 + fields: + req-type: functional + priority: must + flash-base: "0x00000000" + flash-size: "256 KB" + ram-base: "0x20000000" + ram-size: "64 KB" + verification-criteria: > + MemoryLayout::generic() returns correct values; + Renode cortex_m_test.robot passes with synth_cortex_m.repl platform. diff --git a/artifacts/zephyr-integration.yaml b/artifacts/zephyr-integration.yaml new file mode 100644 index 0000000..30b9d6d --- /dev/null +++ b/artifacts/zephyr-integration.yaml @@ -0,0 +1,341 @@ +# Zephyr RTOS Integration Requirements (ASPICE SYS.2 / SWE.1) +# +# System: Synth -- WebAssembly-to-ARM Cortex-M AOT compiler +# +# Defines how synth-generated ELF binaries integrate with Zephyr RTOS, +# covering the build system interface, memory model, platform abstraction, +# and application patterns. Addresses open issues #21 (Create Zephyr +# calculator application) and #22 (Test calculator on real hardware). +# +# Format: rivet generic-yaml + +artifacts: + # --------------------------------------------------------------------------- + # Zephyr build system integration + # --------------------------------------------------------------------------- + + - id: ZI-001 + type: system-req + title: Zephyr CMake build integration + description: > + Synth-compiled WASM functions shall be linkable with Zephyr + applications via the standard Zephyr CMake build system. + The integration pattern is: synth produces an ARM assembly file + (.s) from a WASM module; the Zephyr CMakeLists.txt includes this + assembly file via target_sources(app PRIVATE src/function.s). + The assembly file shall use .syntax unified, .thumb, .global + directives compatible with the arm-none-eabi-gcc assembler + shipped with the Zephyr SDK. Demonstrated in + examples/zephyr-poc/CMakeLists.txt. + status: implemented + tags: [zephyr, cmake, build-system] + links: + - type: derives-from + target: BR-003 + - type: refines + target: FR-002 + - type: refines + target: TR-003 + - type: traces-to + target: ARCH-003 + fields: + req-type: interface + priority: must + verification-criteria: > + examples/zephyr-poc/ builds with west build for at least one + Zephyr-supported board (nrf52840dk/nrf52840 or qemu_cortex_m3); + synth-compiled assembly links without undefined symbol errors. + + - id: ZI-002 + type: system-req + title: Zephyr AAPCS calling convention compliance + description: > + Synth-generated functions shall use the ARM Architecture Procedure + Call Standard (AAPCS) calling convention: arguments in R0-R3, + return value in R0, callee-saved registers R4-R11 preserved. + This allows Zephyr C code to call synth-compiled WASM functions + via extern declarations (e.g., extern int32_t synth_add(int32_t a, + int32_t b)) without ABI glue. The R11 register is reserved by + synth as the WASM linear memory base pointer; when integrating + with Zephyr, R11 must be saved/restored across calls if Zephyr + code uses it as the frame pointer. + status: implemented + tags: [zephyr, abi, calling-convention, aapcs] + links: + - type: derives-from + target: BR-003 + - type: refines + target: FR-004 + - type: refines + target: FR-005 + - type: traces-to + target: ARCH-002 + - type: traces-to + target: ARCH-006 + fields: + req-type: interface + priority: must + verification-criteria: > + Renode test executes add(5,3)=8 with R0/R1 arguments and R0 + result; Zephyr POC calls synth_add() successfully from C. + + - id: ZI-003 + type: system-req + title: Zephyr Memory Domain integration + description: > + The synth-memory crate's MemoryPlatform trait shall support a + Zephyr backend that maps WASM linear memories to Zephyr Memory + Domains (k_mem_domain). On Zephyr, the MPU region configuration + shall delegate to Zephyr's memory management APIs + (k_mem_domain_add_partition, k_mem_partition) rather than + writing MPU registers directly. The MemoryDescriptor.platform_data + field stores the Zephyr partition pointer. The "zephyr" cargo + feature in synth-memory enables this backend. + status: draft + tags: [zephyr, memory-domains, mpu, platform-abstraction] + links: + - type: derives-from + target: BR-001 + - type: refines + target: FR-003 + - type: refines + target: FR-008 + - type: traces-to + target: ARCH-005 + fields: + req-type: functional + priority: must + verification-criteria: > + synth-memory compiles with --features=zephyr; + MemoryPlatform::configure_mpu_region maps to Zephyr + k_mem_partition API; platform_data stores partition pointer. + + - id: ZI-004 + type: system-req + title: Zephyr prj.conf configuration for synth modules + description: > + Synth shall document the minimal Zephyr Kconfig settings required + for running synth-compiled WASM modules. The base configuration + requires CONFIG_PRINTK=y and CONFIG_CONSOLE=y for output. + For MPU-protected memories, CONFIG_ARM_MPU=y and + CONFIG_MPU_ALLOW_FLASH_WRITE=n are required. For multi-threaded + WASM execution, CONFIG_USERSPACE=y enables Zephyr Memory Domains. + Demonstrated in examples/zephyr-poc/prj.conf. + status: draft + tags: [zephyr, configuration, kconfig] + links: + - type: derives-from + target: BR-003 + - type: refines + target: TR-004 + - type: refines + target: FR-003 + fields: + req-type: interface + priority: should + verification-criteria: > + examples/zephyr-poc/prj.conf contains required Kconfig settings; + application builds with west build using these settings. + + # --------------------------------------------------------------------------- + # Zephyr application patterns + # --------------------------------------------------------------------------- + + - id: ZI-005 + type: system-req + title: Zephyr calculator application (issue #21) + description: > + Synth shall provide a Zephyr calculator application example that + compiles examples/calculator/calculator.wat to ARM assembly and + links it with a Zephyr application. The calculator module exports + add, subtract, multiply, divide, and modulo functions. The Zephyr + application shall call each function, display results via printk, + and demonstrate that synth-compiled WASM functions integrate + seamlessly with Zephyr RTOS. The application shall build for + both qemu_cortex_m3 (CI) and nrf52840dk/nrf52840 (hardware). + status: draft + tags: [zephyr, calculator, example, issue-21] + links: + - type: derives-from + target: BR-003 + - type: refines + target: FR-002 + - type: refines + target: FR-005 + - type: refines + target: TR-003 + - type: traces-to + target: SWA-001 + fields: + req-type: functional + priority: must + github-issue: 21 + verification-criteria: > + west build -b qemu_cortex_m3 examples/calculator-zephyr succeeds; + west build -b nrf52840dk/nrf52840 examples/calculator-zephyr succeeds; + QEMU run produces correct arithmetic results via printk. + + - id: ZI-006 + type: system-req + title: Hardware testing on real Cortex-M board (issue #22) + description: > + Synth-compiled binaries shall be tested on real ARM Cortex-M + hardware via Zephyr's west flash and west debug workflows. + The primary hardware target is the nRF52840-DK. Testing shall + verify that synth-compiled calculator functions produce correct + results when executed on physical silicon, not just emulation. + J-Link or OpenOCD debug probes shall be used for flashing. + status: draft + tags: [zephyr, hardware-testing, nrf52840, issue-22] + links: + - type: refines + target: FR-005 + - type: derives-from + target: BR-003 + - type: traces-to + target: VER-005 + fields: + req-type: functional + priority: should + github-issue: 22 + verification-criteria: > + west flash succeeds on nRF52840-DK; + serial console output shows correct calculator results; + synth_add(5, 42) returns 47 on real hardware. + + - id: ZI-007 + type: system-req + title: PID controller Zephyr demonstration + description: > + Synth shall provide a PID controller demonstration running on + Zephyr that showcases formally verified WASM compilation for + safety-critical control loops. The PID demo uses synth-compiled + f32 operations (synth_pid_error, synth_pid_integral, + synth_pid_simple) called from a Zephyr application at 10 Hz + update rate. This demonstrates synth's value for safety-critical + embedded systems where provably correct arithmetic is required. + Demonstrated in examples/pid-controller/. + status: draft + tags: [zephyr, pid-controller, safety-critical, demo] + links: + - type: refines + target: FR-005 + - type: refines + target: FR-006 + - type: refines + target: FR-008 + - type: derives-from + target: BR-001 + fields: + req-type: functional + priority: should + verification-criteria: > + PID controller demo builds for qemu_cortex_m3; + temperature converges to setpoint within 50 seconds of + simulated time; all PID operations use synth-compiled functions. + + # --------------------------------------------------------------------------- + # Linker integration + # --------------------------------------------------------------------------- + + - id: ZI-008 + type: system-req + title: Zephyr-compatible linker script generation + description: > + When generating standalone ELF binaries for Zephyr targets, synth's + LinkerScriptGenerator shall produce GNU ld scripts compatible with + Zephyr's linking requirements. For linked-with-Zephyr mode (assembly + integration), synth output shall be position-independent or use + symbols that Zephyr's linker resolves. For standalone mode, + the generated linker script shall define standard ARM startup symbols + (_estack, _sidata, _sdata, _edata, _sbss, _ebss) that the synth + Reset_Handler references for .data copy and .bss zero-fill. + The .isr_vector section shall use KEEP() and 128-byte alignment. + status: implemented + tags: [zephyr, linker-script, elf] + links: + - type: derives-from + target: BR-003 + - type: refines + target: TR-002 + - type: refines + target: FR-002 + - type: traces-to + target: ARCH-003 + - type: traces-to + target: SWA-005 + fields: + req-type: functional + priority: must + verification-criteria: > + Generated linker scripts contain ENTRY(Reset_Handler); + .isr_vector section with KEEP and ALIGN(128); + .data with AT> FLASH for flash-to-RAM copy at startup. + + - id: ZI-009 + type: system-req + title: Meld runtime integration with Zephyr + description: > + Synth shall support Meld runtime integration within Zephyr + applications, enabling WASM component import dispatch via the + __meld_dispatch_import and __meld_get_memory_base bridge + functions. The linker script shall include .meld_import_table and + .meld.imports sections with EXTERN declarations for meld symbols. + This enables synth-compiled components to call Zephyr subsystems + (e.g., sensor drivers, networking) through Meld's component + composition layer. + status: draft + tags: [zephyr, meld, runtime, component-model] + links: + - type: derives-from + target: BR-003 + - type: refines + target: FR-001 + - type: refines + target: FR-004 + - type: traces-to + target: ARCH-003 + - type: traces-to + target: ARCH-006 + fields: + req-type: interface + priority: should + verification-criteria: > + LinkerScriptGenerator::with_meld_integration() produces sections + with __meld_dispatch_import and __meld_get_memory_base EXTERNs; + .meld_import_table section placed in FLASH. + + # --------------------------------------------------------------------------- + # Bounds checking integration + # --------------------------------------------------------------------------- + + - id: ZI-010 + type: system-req + title: Bounds checking strategy selection for Zephyr targets + description: > + Synth shall select the appropriate bounds checking strategy based + on the Zephyr target's hardware capabilities. On targets with MPU + (Cortex-M3/M4/M7/M33), MpuBoundsChecker shall be preferred for + zero-overhead hardware protection. On targets without MPU or when + MPU regions are exhausted, SoftwareBoundsChecker shall be used as + fallback (25-40% overhead). MaskingBoundsChecker is available for + power-of-2 memory sizes where wrapping is acceptable (5% overhead). + The ProtectionStrategy enum encodes this choice per-memory. + status: implemented + tags: [bounds-checking, mpu, safety, zephyr] + links: + - type: derives-from + target: BR-001 + - type: refines + target: FR-003 + - type: refines + target: FR-008 + - type: traces-to + target: ARCH-005 + fields: + req-type: functional + priority: must + verification-criteria: > + SoftwareBoundsChecker traps on out-of-bounds access; + MaskingBoundsChecker wraps addresses for power-of-2 sizes; + MpuBoundsChecker delegates to hardware fault handling. diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index e30fb5f..8ce535f 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -3014,4 +3014,1131 @@ mod tests { "br(0) in loop should branch back to loop_start label" ); } + + // ========================================================================= + // Complex control flow tests (GitHub issue #36) + // + // These exercise the control flow compilation paths landed in PR #52: + // nested blocks, loops with conditional exit, if/else with nested blocks, + // br_table dispatch, and realistic multi-construct programs like + // factorial and fibonacci. + // ========================================================================= + + /// Helper: create a fresh InstructionSelector with no optimization rules + fn fresh_selector() -> InstructionSelector { + InstructionSelector::new(vec![]) + } + + /// Helper: collect all Label names from an instruction sequence + fn collect_labels(instrs: &[ArmInstruction]) -> Vec { + instrs + .iter() + .filter_map(|i| { + if let ArmOp::Label { name } = &i.op { + Some(name.clone()) + } else { + None + } + }) + .collect() + } + + /// Helper: collect all unconditional branch targets (B { label }) + fn collect_branch_targets(instrs: &[ArmInstruction]) -> Vec { + instrs + .iter() + .filter_map(|i| { + if let ArmOp::B { label } = &i.op { + Some(label.clone()) + } else { + None + } + }) + .collect() + } + + /// Helper: collect all conditional branch targets (Bcc { label, .. }) + fn collect_cond_branch_targets(instrs: &[ArmInstruction]) -> Vec<(Condition, String)> { + instrs + .iter() + .filter_map(|i| { + if let ArmOp::Bcc { cond, label } = &i.op { + Some((*cond, label.clone())) + } else { + None + } + }) + .collect() + } + + /// Helper: count instructions of a given kind + fn count_op bool>(instrs: &[ArmInstruction], pred: F) -> usize { + instrs.iter().filter(|i| pred(&i.op)).count() + } + + // ----- Test 1: Nested blocks with branch-out (br to outer block) ----- + + #[test] + fn test_complex_nested_blocks_br_to_outer() { + // WASM equivalent: + // (block $outer ;; depth 2 from innermost + // (block $middle ;; depth 1 from innermost + // (block $inner ;; depth 0 + // i32.const 1 + // br 2 ;; jump to $outer end + // ) + // i32.const 2 ;; skipped by br 2 + // ) + // i32.const 3 ;; also skipped by br 2 + // ) + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Block, // $outer + WasmOp::Block, // $middle + WasmOp::Block, // $inner + WasmOp::I32Const(1), + WasmOp::Br(2), // jump to $outer end + WasmOp::End, // end $inner + WasmOp::I32Const(2), + WasmOp::End, // end $middle + WasmOp::I32Const(3), + WasmOp::End, // end $outer + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 0).unwrap(); + + // Should have 3 block end labels (one per block) + let labels = collect_labels(&instrs); + assert!( + labels.len() >= 3, + "Three nested blocks should produce at least 3 end labels, got {}", + labels.len() + ); + + // The br(2) should generate a B instruction + let branches = collect_branch_targets(&instrs); + assert!( + !branches.is_empty(), + "br(2) should generate an unconditional branch" + ); + + // The branch target should be the outer block's end label (the first + // label pushed on block_labels, which is the outermost block end) + let outer_end_label = &labels[labels.len() - 1]; // last label emitted is outermost end + assert!( + branches.contains(outer_end_label), + "br(2) should target the outermost block end label '{}', targets: {:?}", + outer_end_label, + branches + ); + } + + // ----- Test 2: Loop with conditional exit (br_if) ----- + + #[test] + fn test_complex_loop_with_conditional_exit() { + // WASM equivalent (countdown loop): + // (block $exit + // (loop $loop + // local.get 0 ;; counter + // i32.eqz + // br_if 1 ;; if counter == 0, exit block + // local.get 0 + // i32.const 1 + // i32.sub + // local.set 0 ;; counter -= 1 + // br 0 ;; loop back + // ) + // ) + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Block, // $exit + WasmOp::Loop, // $loop + WasmOp::LocalGet(0), // counter + WasmOp::I32Eqz, // counter == 0? + WasmOp::BrIf(1), // if zero, exit to $exit end + WasmOp::LocalGet(0), + WasmOp::I32Const(1), + WasmOp::I32Sub, // counter - 1 + WasmOp::LocalSet(0), // counter = counter - 1 + WasmOp::Br(0), // loop back to $loop start + WasmOp::End, // end $loop + WasmOp::End, // end $exit + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 1).unwrap(); + + // Should have a loop_start label + let loop_labels: Vec<_> = collect_labels(&instrs) + .into_iter() + .filter(|l| l.contains("loop_start")) + .collect(); + assert_eq!( + loop_labels.len(), + 1, + "Should have exactly one loop_start label" + ); + + // Should have an unconditional branch back to loop_start (br 0) + let branches = collect_branch_targets(&instrs); + assert!( + branches.contains(&loop_labels[0]), + "br(0) should branch back to loop_start label" + ); + + // Should have a conditional branch (br_if 1) targeting exit block end + let cond_branches = collect_cond_branch_targets(&instrs); + let ne_branches: Vec<_> = cond_branches + .iter() + .filter(|(c, _)| *c == Condition::NE) + .collect(); + assert!( + !ne_branches.is_empty(), + "br_if should generate a BNE conditional branch" + ); + + // Should emit a SUB for counter decrement + let has_sub = instrs.iter().any(|i| matches!(&i.op, ArmOp::Sub { .. })); + assert!(has_sub, "Should emit SUB for i32.sub (counter -= 1)"); + } + + // ----- Test 3: If/else with computation in both arms ----- + + #[test] + fn test_complex_if_else_with_computation() { + // WASM equivalent: + // local.get 0 ;; condition from param + // (if + // (then + // local.get 1 + // i32.const 10 + // i32.add + // local.set 1 ;; x += 10 + // local.get 1 + // i32.const 100 + // i32.mul + // local.set 1 ;; x *= 100 + // ) + // (else + // local.get 1 + // i32.const 20 + // i32.sub + // local.set 1 ;; x -= 20 + // local.get 1 + // i32.const 2 + // i32.mul + // local.set 1 ;; x *= 2 + // ) + // ) + // local.get 1 ;; return x + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::LocalGet(0), // condition + WasmOp::If, + // then-arm: x += 10, x *= 100 + WasmOp::LocalGet(1), + WasmOp::I32Const(10), + WasmOp::I32Add, + WasmOp::LocalSet(1), + WasmOp::LocalGet(1), + WasmOp::I32Const(100), + WasmOp::I32Mul, + WasmOp::LocalSet(1), + WasmOp::Else, + // else-arm: x -= 20, x *= 2 + WasmOp::LocalGet(1), + WasmOp::I32Const(20), + WasmOp::I32Sub, + WasmOp::LocalSet(1), + WasmOp::LocalGet(1), + WasmOp::I32Const(2), + WasmOp::I32Mul, + WasmOp::LocalSet(1), + WasmOp::End, // end if + WasmOp::LocalGet(1), // return x + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 2).unwrap(); + + // Should have CMP for condition + let cmp_count = count_op(&instrs, |op| matches!(op, ArmOp::Cmp { .. })); + assert!(cmp_count >= 1, "If should emit CMP for condition"); + + // Should have conditional branch to else (BEQ) + let beq_count = count_op(&instrs, |op| { + matches!( + op, + ArmOp::Bcc { + cond: Condition::EQ, + .. + } + ) + }); + assert!(beq_count >= 1, "If should emit BEQ to skip to else"); + + // Should have unconditional branch to skip else at end of then + let b_count = count_op(&instrs, |op| matches!(op, ArmOp::B { .. })); + assert!( + b_count >= 1, + "End of then-arm should emit B to skip else, got {}", + b_count + ); + + // Should have labels for else and if_end + let labels = collect_labels(&instrs); + let else_labels: Vec<_> = labels.iter().filter(|l| l.contains("else")).collect(); + let end_labels: Vec<_> = labels.iter().filter(|l| l.contains("if_end")).collect(); + assert!(!else_labels.is_empty(), "Should have an else label"); + assert!(!end_labels.is_empty(), "Should have an if_end label"); + + // Should have ADD for then-arm and SUB for else-arm + let add_count = count_op(&instrs, |op| matches!(op, ArmOp::Add { .. })); + assert!(add_count >= 1, "Then-arm should have ADD"); + let sub_count = count_op(&instrs, |op| matches!(op, ArmOp::Sub { .. })); + assert!(sub_count >= 1, "Else-arm should have SUB"); + + // Should have MUL instructions for both arms + let mul_count = count_op(&instrs, |op| matches!(op, ArmOp::Mul { .. })); + assert_eq!( + mul_count, 2, + "Should have 2 MUL instructions (one per arm), got {}", + mul_count + ); + } + + // ----- Test 4: br_table (switch-like dispatch) ----- + + #[test] + fn test_complex_br_table_switch_dispatch() { + // WASM equivalent (switch with 3 cases + default): + // (block $case2 + // (block $case1 + // (block $case0 + // (block $default + // local.get 0 ;; switch index + // br_table 0 1 2 3 ;; targets=[0,1,2], default=3 + // ) + // ;; default body + // i32.const 99 + // br 2 + // ) + // ;; case 0 body + // i32.const 0 + // br 1 + // ) + // ;; case 1 body + // i32.const 1 + // br 0 + // ) + // ;; case 2 falls through here + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Block, // $case2 + WasmOp::Block, // $case1 + WasmOp::Block, // $case0 + WasmOp::Block, // $default + WasmOp::LocalGet(0), // switch index + WasmOp::BrTable { + targets: vec![0, 1, 2], // case 0->$default, 1->$case0, 2->$case1 + default: 3, // default->$case2 + }, + WasmOp::End, // end $default + WasmOp::I32Const(99), // default body + WasmOp::Br(2), // skip to $case2 end + WasmOp::End, // end $case0 + WasmOp::I32Const(0), // case 0 body + WasmOp::Br(1), // skip to $case2 end + WasmOp::End, // end $case1 + WasmOp::I32Const(1), // case 1 body + WasmOp::Br(0), // skip to $case2 end + WasmOp::End, // end $case2 + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 1).unwrap(); + + // br_table should emit CMP+BEQ for each target (3 targets) + let cmp_count = count_op(&instrs, |op| matches!(op, ArmOp::Cmp { .. })); + assert!( + cmp_count >= 3, + "br_table with 3 targets should emit at least 3 CMPs, got {}", + cmp_count + ); + + let beq_count = count_op(&instrs, |op| { + matches!( + op, + ArmOp::Bcc { + cond: Condition::EQ, + .. + } + ) + }); + assert!( + beq_count >= 3, + "br_table with 3 targets should emit at least 3 BEQs, got {}", + beq_count + ); + + // Should emit a default unconditional branch + let b_count = count_op(&instrs, |op| matches!(op, ArmOp::B { .. })); + assert!( + b_count >= 4, + "Should have at least 4 B instructions (1 default + 3 case br), got {}", + b_count + ); + + // Should have 4 block end labels + let labels = collect_labels(&instrs); + let block_end_labels: Vec<_> = labels.iter().filter(|l| l.contains("block_end")).collect(); + assert_eq!( + block_end_labels.len(), + 4, + "Should have 4 block_end labels for 4 blocks, got {}", + block_end_labels.len() + ); + } + + // ----- Test 5: Factorial (loop + if + arithmetic) ----- + + #[test] + fn test_complex_factorial() { + // WASM equivalent of iterative factorial: + // (func $factorial (param $n i32) (result i32) + // (local $result i32) + // i32.const 1 + // local.set 1 ;; result = 1 + // (block $exit + // (loop $loop + // local.get 0 ;; n + // i32.const 1 + // i32.le_s + // br_if 1 ;; if n <= 1, exit + // local.get 1 ;; result + // local.get 0 ;; n + // i32.mul + // local.set 1 ;; result *= n + // local.get 0 + // i32.const 1 + // i32.sub + // local.set 0 ;; n -= 1 + // br 0 ;; loop + // ) + // ) + // local.get 1 ;; return result + // ) + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::I32Const(1), + WasmOp::LocalSet(1), // result = 1 + WasmOp::Block, // $exit + WasmOp::Loop, // $loop + WasmOp::LocalGet(0), // n + WasmOp::I32Const(1), + WasmOp::I32LeS, // n <= 1? + WasmOp::BrIf(1), // exit if true + WasmOp::LocalGet(1), // result + WasmOp::LocalGet(0), // n + WasmOp::I32Mul, // result * n + WasmOp::LocalSet(1), // result = result * n + WasmOp::LocalGet(0), // n + WasmOp::I32Const(1), + WasmOp::I32Sub, // n - 1 + WasmOp::LocalSet(0), // n = n - 1 + WasmOp::Br(0), // loop back + WasmOp::End, // end $loop + WasmOp::End, // end $exit + WasmOp::LocalGet(1), // return result + ]; + + // 2 params: $n in r0, $result in r1 (via local.set 1) + let instrs = selector.select_with_stack(&wasm_ops, 2).unwrap(); + + // Should have a loop_start label + let labels = collect_labels(&instrs); + let loop_starts: Vec<_> = labels.iter().filter(|l| l.contains("loop_start")).collect(); + assert_eq!(loop_starts.len(), 1, "Should have exactly one loop_start"); + + // Should have backward branch (br 0) to loop + let branches = collect_branch_targets(&instrs); + assert!( + branches.contains(loop_starts[0]), + "br(0) should branch back to loop_start" + ); + + // Should have conditional exit (br_if 1) + let cond_branches = collect_cond_branch_targets(&instrs); + assert!( + !cond_branches.is_empty(), + "br_if(1) should emit conditional branch to exit" + ); + + // Should have MUL for result * n + let mul_count = count_op(&instrs, |op| matches!(op, ArmOp::Mul { .. })); + assert_eq!(mul_count, 1, "Should have exactly one MUL for result * n"); + + // Should have SUB for n - 1 + let sub_count = count_op(&instrs, |op| matches!(op, ArmOp::Sub { .. })); + assert_eq!(sub_count, 1, "Should have exactly one SUB for n - 1"); + + // Should have BX LR at the end for function return + let has_bx_lr = instrs + .iter() + .any(|i| matches!(&i.op, ArmOp::Bx { rm: Reg::LR })); + assert!(has_bx_lr, "Function should end with BX LR"); + } + + // ----- Test 6: Fibonacci (loop + if + arithmetic) ----- + + #[test] + fn test_complex_fibonacci() { + // WASM equivalent of iterative fibonacci: + // (func $fib (param $n i32) (result i32) + // (local $a i32) ;; local 1 = 0 + // (local $b i32) ;; local 2 = 1 + // (local $tmp i32) ;; local 3 + // i32.const 0 + // local.set 1 ;; a = 0 + // i32.const 1 + // local.set 2 ;; b = 1 + // (block $exit + // (loop $loop + // local.get 0 ;; n + // i32.eqz + // br_if 1 ;; if n == 0, exit + // local.get 1 ;; a + // local.get 2 ;; b + // i32.add + // local.set 3 ;; tmp = a + b + // local.get 2 + // local.set 1 ;; a = b + // local.get 3 + // local.set 2 ;; b = tmp + // local.get 0 + // i32.const 1 + // i32.sub + // local.set 0 ;; n -= 1 + // br 0 ;; loop + // ) + // ) + // local.get 1 ;; return a + // ) + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::I32Const(0), + WasmOp::LocalSet(1), // a = 0 + WasmOp::I32Const(1), + WasmOp::LocalSet(2), // b = 1 + WasmOp::Block, // $exit + WasmOp::Loop, // $loop + WasmOp::LocalGet(0), // n + WasmOp::I32Eqz, // n == 0? + WasmOp::BrIf(1), // exit if n == 0 + WasmOp::LocalGet(1), // a + WasmOp::LocalGet(2), // b + WasmOp::I32Add, // a + b + WasmOp::LocalSet(3), // tmp = a + b + WasmOp::LocalGet(2), // b + WasmOp::LocalSet(1), // a = b + WasmOp::LocalGet(3), // tmp + WasmOp::LocalSet(2), // b = tmp + WasmOp::LocalGet(0), // n + WasmOp::I32Const(1), + WasmOp::I32Sub, // n - 1 + WasmOp::LocalSet(0), // n = n - 1 + WasmOp::Br(0), // loop + WasmOp::End, // end $loop + WasmOp::End, // end $exit + WasmOp::LocalGet(1), // return a + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 4).unwrap(); + + // Should have loop_start label + let labels = collect_labels(&instrs); + let loop_starts: Vec<_> = labels.iter().filter(|l| l.contains("loop_start")).collect(); + assert_eq!(loop_starts.len(), 1, "Should have one loop_start"); + + // Should have backward branch + let branches = collect_branch_targets(&instrs); + assert!( + branches.contains(loop_starts[0]), + "Should branch back to loop_start" + ); + + // Should have ADD for a + b + let add_count = count_op(&instrs, |op| matches!(op, ArmOp::Add { .. })); + assert!(add_count >= 1, "Should have ADD for a + b"); + + // Should have SUB for n - 1 + let sub_count = count_op(&instrs, |op| matches!(op, ArmOp::Sub { .. })); + assert!(sub_count >= 1, "Should have SUB for n - 1"); + + // Should have conditional branch for br_if + let cond_branches = collect_cond_branch_targets(&instrs); + let ne_branches: Vec<_> = cond_branches + .iter() + .filter(|(c, _)| *c == Condition::NE) + .collect(); + assert!( + !ne_branches.is_empty(), + "br_if should generate BNE for conditional exit" + ); + } + + // ----- Test 7: Empty blocks ----- + + #[test] + fn test_complex_empty_blocks() { + // Empty blocks should compile without error and produce minimal code + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Block, + WasmOp::End, + WasmOp::Block, + WasmOp::Block, + WasmOp::End, + WasmOp::End, + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 0).unwrap(); + + // Should succeed and produce labels + let labels = collect_labels(&instrs); + assert!( + labels.len() >= 3, + "Three empty blocks should produce at least 3 labels, got {}", + labels.len() + ); + + // No branches should be emitted (no br instructions) + let b_count = count_op(&instrs, |op| matches!(op, ArmOp::B { .. })); + assert_eq!( + b_count, 0, + "Empty blocks should not emit branches, got {}", + b_count + ); + } + + // ----- Test 8: Deeply nested blocks (5 levels) ----- + + #[test] + fn test_complex_deeply_nested_blocks() { + // 5 levels of nesting with br from innermost to outermost + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Block, // depth 4 from innermost + WasmOp::Block, // depth 3 + WasmOp::Block, // depth 2 + WasmOp::Block, // depth 1 + WasmOp::Block, // depth 0 (innermost) + WasmOp::I32Const(42), + WasmOp::Br(4), // jump to outermost block end + WasmOp::End, // end depth 0 + WasmOp::End, // end depth 1 + WasmOp::End, // end depth 2 + WasmOp::End, // end depth 3 + WasmOp::End, // end depth 4 + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 0).unwrap(); + + // Should have 5 block end labels + let labels = collect_labels(&instrs); + let block_end_labels: Vec<_> = labels.iter().filter(|l| l.contains("block_end")).collect(); + assert_eq!( + block_end_labels.len(), + 5, + "5 nested blocks should have 5 end labels, got {}", + block_end_labels.len() + ); + + // The br(4) should branch to the outermost block's end + let branches = collect_branch_targets(&instrs); + assert_eq!(branches.len(), 1, "Should have exactly one branch (br 4)"); + + // The target should be the last label emitted (outermost end) + let outermost_label = block_end_labels.last().unwrap(); + assert_eq!( + &branches[0], *outermost_label, + "br(4) should target outermost block end" + ); + } + + // ----- Test 9: Loop re-entry via br 0 ----- + + #[test] + fn test_complex_loop_reentry() { + // Multiple br 0 in a loop body (different code paths re-enter the loop) + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Loop, // $loop + WasmOp::LocalGet(0), // condition + WasmOp::If, + WasmOp::I32Const(1), + WasmOp::LocalSet(0), + WasmOp::Br(1), // re-enter loop from then-arm + WasmOp::Else, + WasmOp::I32Const(0), + WasmOp::LocalSet(0), + WasmOp::Br(1), // re-enter loop from else-arm + WasmOp::End, // end if + WasmOp::End, // end loop + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 1).unwrap(); + + // Should have loop_start label + let labels = collect_labels(&instrs); + let loop_labels: Vec<_> = labels.iter().filter(|l| l.contains("loop_start")).collect(); + assert_eq!(loop_labels.len(), 1, "Should have one loop_start label"); + + // Should have two unconditional branches targeting loop_start (br 1 from both arms) + // Plus the B that skips else at end of then-arm + let branches = collect_branch_targets(&instrs); + let loop_branches: Vec<_> = branches + .iter() + .filter(|b| b.contains("loop_start")) + .collect(); + assert_eq!( + loop_branches.len(), + 2, + "Both br(1) should branch to loop_start, got {} branches to loop_start", + loop_branches.len() + ); + } + + // ----- Test 10: Mixed control flow — block containing loop containing if/else ----- + + #[test] + fn test_complex_block_loop_if_combined() { + // WASM equivalent: + // (block $outer + // (loop $loop + // local.get 0 + // i32.const 10 + // i32.gt_s + // (if + // (then + // br 2 ;; exit $outer + // ) + // (else + // local.get 0 + // i32.const 1 + // i32.add + // local.set 0 + // br 1 ;; re-enter $loop + // ) + // ) + // ) + // ) + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Block, // $outer + WasmOp::Loop, // $loop + WasmOp::LocalGet(0), // counter + WasmOp::I32Const(10), + WasmOp::I32GtS, // counter > 10? + WasmOp::If, + // then: exit outer + WasmOp::Br(2), // exit $outer + WasmOp::Else, + // else: increment and loop + WasmOp::LocalGet(0), + WasmOp::I32Const(1), + WasmOp::I32Add, + WasmOp::LocalSet(0), + WasmOp::Br(1), // re-enter $loop + WasmOp::End, // end if + WasmOp::End, // end loop + WasmOp::End, // end outer + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 1).unwrap(); + + // Verify structural elements + let labels = collect_labels(&instrs); + + // Should have loop_start + let loop_starts: Vec<_> = labels.iter().filter(|l| l.contains("loop_start")).collect(); + assert_eq!(loop_starts.len(), 1, "Should have one loop_start"); + + // Should have block_end for outer block + let block_ends: Vec<_> = labels.iter().filter(|l| l.contains("block_end")).collect(); + assert!( + !block_ends.is_empty(), + "Should have block_end label for outer block" + ); + + // Should have else and if_end labels + let else_labels: Vec<_> = labels.iter().filter(|l| l.contains("else")).collect(); + assert!(!else_labels.is_empty(), "Should have an else label"); + + let if_end_labels: Vec<_> = labels.iter().filter(|l| l.contains("if_end")).collect(); + assert!(!if_end_labels.is_empty(), "Should have an if_end label"); + + // Verify branches + let branches = collect_branch_targets(&instrs); + + // br(2) should target outer block end + assert!( + branches.iter().any(|b| b.contains("block_end")), + "br(2) should target outer block_end, branches: {:?}", + branches + ); + + // br(1) should target loop_start + assert!( + branches.iter().any(|b| b.contains("loop_start")), + "br(1) should target loop_start, branches: {:?}", + branches + ); + + // Should have ADD for counter + 1 + let add_count = count_op(&instrs, |op| matches!(op, ArmOp::Add { .. })); + assert!(add_count >= 1, "Should have ADD for counter + 1"); + } + + // ----- Test 11: br_table within a loop ----- + + #[test] + fn test_complex_br_table_in_loop() { + // State machine pattern: loop with br_table dispatch + // (loop $loop + // (block $state2 + // (block $state1 + // (block $state0 + // local.get 0 ;; state variable + // br_table 0 1 2 ;; dispatch to state blocks + // ) + // ;; state 0 body + // i32.const 1 + // local.set 0 ;; state = 1 + // br 2 ;; continue loop + // ) + // ;; state 1 body + // i32.const 2 + // local.set 0 ;; state = 2 + // br 1 ;; continue loop + // ) + // ;; state 2: exit (fall through to end) + // ) + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Loop, // $loop + WasmOp::Block, // $state2 + WasmOp::Block, // $state1 + WasmOp::Block, // $state0 + WasmOp::LocalGet(0), // state + WasmOp::BrTable { + targets: vec![0, 1, 2], // dispatch per state + default: 2, // default -> $state2 (exit) + }, + WasmOp::End, // end $state0 + WasmOp::I32Const(1), + WasmOp::LocalSet(0), // state = 1 + WasmOp::Br(2), // back to $loop + WasmOp::End, // end $state1 + WasmOp::I32Const(2), + WasmOp::LocalSet(0), // state = 2 + WasmOp::Br(1), // back to $loop + WasmOp::End, // end $state2 + WasmOp::End, // end $loop + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 1).unwrap(); + + // Should have loop_start label + let labels = collect_labels(&instrs); + let loop_labels: Vec<_> = labels.iter().filter(|l| l.contains("loop_start")).collect(); + assert_eq!(loop_labels.len(), 1, "Should have one loop_start"); + + // br_table should emit 3 CMP + BEQ pairs + let cmp_count = count_op(&instrs, |op| matches!(op, ArmOp::Cmp { .. })); + assert!( + cmp_count >= 3, + "br_table should emit at least 3 CMPs, got {}", + cmp_count + ); + + // Should have branches back to loop_start (br 2 and br 1 target loop) + let branches = collect_branch_targets(&instrs); + let to_loop: Vec<_> = branches + .iter() + .filter(|b| b.contains("loop_start")) + .collect(); + assert!( + to_loop.len() >= 2, + "Should have at least 2 branches back to loop_start (from state 0 and 1), got {}", + to_loop.len() + ); + } + + // ----- Test 12: Nested if/else without inner else clause ----- + + #[test] + fn test_complex_nested_if_no_else() { + // Nested if without else exercises the else-label dedup path + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::I32Const(1), // outer condition + WasmOp::If, + WasmOp::I32Const(1), // inner condition + WasmOp::If, + WasmOp::I32Const(42), // deeply nested body + WasmOp::End, // end inner if (no else) + WasmOp::End, // end outer if (no else) + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 0).unwrap(); + + // Each if-without-else should emit both else label and if_end label + let labels = collect_labels(&instrs); + let else_labels: Vec<_> = labels.iter().filter(|l| l.contains("else")).collect(); + let end_labels: Vec<_> = labels.iter().filter(|l| l.contains("if_end")).collect(); + + assert!( + else_labels.len() >= 2, + "Two if-without-else should emit at least 2 else labels, got {}", + else_labels.len() + ); + assert!( + end_labels.len() >= 2, + "Two if blocks should emit at least 2 if_end labels, got {}", + end_labels.len() + ); + + // Should have 2 BEQ instructions (one per if) + let beq_count = count_op(&instrs, |op| { + matches!( + op, + ArmOp::Bcc { + cond: Condition::EQ, + .. + } + ) + }); + assert_eq!( + beq_count, 2, + "Two if blocks should emit 2 BEQ, got {}", + beq_count + ); + } + + // ----- Test 13: Function call within loop ----- + + #[test] + fn test_complex_call_in_loop() { + // Loop that calls a function each iteration + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Block, // $exit + WasmOp::Loop, // $loop + WasmOp::LocalGet(0), // counter + WasmOp::I32Eqz, // counter == 0? + WasmOp::BrIf(1), // exit if zero + WasmOp::LocalGet(0), // pass counter as arg + WasmOp::Call(5), // call func_5 + WasmOp::Drop, // discard return value + WasmOp::LocalGet(0), + WasmOp::I32Const(1), + WasmOp::I32Sub, + WasmOp::LocalSet(0), // counter -= 1 + WasmOp::Br(0), // loop + WasmOp::End, // end loop + WasmOp::End, // end block + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 1).unwrap(); + + // Should have a BL func_5 call + let has_bl = instrs + .iter() + .any(|i| matches!(&i.op, ArmOp::Bl { label } if label == "func_5")); + assert!(has_bl, "Should emit BL func_5 for Call(5)"); + + // Should have loop_start and backward branch + let labels = collect_labels(&instrs); + let loop_labels: Vec<_> = labels.iter().filter(|l| l.contains("loop_start")).collect(); + assert_eq!(loop_labels.len(), 1, "Should have one loop_start"); + + let branches = collect_branch_targets(&instrs); + assert!( + branches.contains(loop_labels[0]), + "Should branch back to loop_start" + ); + } + + // ----- Test 14: Early return from nested control flow ----- + + #[test] + fn test_complex_return_from_nested() { + // Return from inside a nested block+loop+if + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::Block, + WasmOp::Loop, + WasmOp::LocalGet(0), + WasmOp::I32Const(0), + WasmOp::I32Eq, + WasmOp::If, + WasmOp::I32Const(42), + WasmOp::Return, // early return from inside if inside loop inside block + WasmOp::End, // end if + WasmOp::Br(0), // loop + WasmOp::End, // end loop + WasmOp::End, // end block + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 1).unwrap(); + + // Should have BX LR for the Return instruction (plus the one at function end) + let bx_count = count_op(&instrs, |op| matches!(op, ArmOp::Bx { rm: Reg::LR })); + assert!( + bx_count >= 2, + "Should have at least 2 BX LR (early return + function epilogue), got {}", + bx_count + ); + + // Should have loop_start + let labels = collect_labels(&instrs); + assert!( + labels.iter().any(|l| l.contains("loop_start")), + "Should have loop_start label" + ); + + // Should have if-related labels + assert!( + labels + .iter() + .any(|l| l.contains("if_end") || l.contains("else")), + "Should have if-related labels" + ); + } + + // ----- Test 15: Unreachable inside control flow ----- + + #[test] + fn test_complex_unreachable_in_block() { + // Unreachable trap inside a conditional block + let mut selector = fresh_selector(); + let wasm_ops = vec![ + WasmOp::I32Const(0), + WasmOp::If, + WasmOp::Unreachable, // trap if condition is true + WasmOp::Else, + WasmOp::I32Const(1), // normal path + WasmOp::End, + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 0).unwrap(); + + // Should have UDF for unreachable + let udf_count = count_op(&instrs, |op| matches!(op, ArmOp::Udf { .. })); + assert_eq!(udf_count, 1, "Should have exactly one UDF for unreachable"); + + // Should still have proper if/else structure + let labels = collect_labels(&instrs); + assert!( + labels.iter().any(|l| l.contains("else")), + "Should have else label" + ); + assert!( + labels.iter().any(|l| l.contains("if_end")), + "Should have if_end label" + ); + } + + // ----- Test 16: Multiple loops (sequential, not nested) ----- + + #[test] + fn test_complex_sequential_loops() { + // Two loops in sequence (not nested) + let mut selector = fresh_selector(); + let wasm_ops = vec![ + // First loop: count up + WasmOp::Block, + WasmOp::Loop, + WasmOp::LocalGet(0), + WasmOp::I32Const(10), + WasmOp::I32GeS, + WasmOp::BrIf(1), // exit if >= 10 + WasmOp::LocalGet(0), + WasmOp::I32Const(1), + WasmOp::I32Add, + WasmOp::LocalSet(0), + WasmOp::Br(0), // loop + WasmOp::End, + WasmOp::End, + // Second loop: count down + WasmOp::Block, + WasmOp::Loop, + WasmOp::LocalGet(0), + WasmOp::I32Eqz, + WasmOp::BrIf(1), // exit if == 0 + WasmOp::LocalGet(0), + WasmOp::I32Const(1), + WasmOp::I32Sub, + WasmOp::LocalSet(0), + WasmOp::Br(0), // loop + WasmOp::End, + WasmOp::End, + ]; + + let instrs = selector.select_with_stack(&wasm_ops, 1).unwrap(); + + // Should have 2 loop_start labels + let labels = collect_labels(&instrs); + let loop_labels: Vec<_> = labels.iter().filter(|l| l.contains("loop_start")).collect(); + assert_eq!( + loop_labels.len(), + 2, + "Should have 2 loop_start labels for sequential loops, got {}", + loop_labels.len() + ); + + // Each loop should have a backward branch + let branches = collect_branch_targets(&instrs); + for ll in &loop_labels { + assert!( + branches.contains(ll), + "Should branch back to loop_start '{}', branches: {:?}", + ll, + branches + ); + } + } + + // ----- Test 17: Instruction count sanity checks ----- + + #[test] + fn test_complex_instruction_count_sanity() { + // Verify that control flow constructs produce a reasonable number of + // instructions (not zero, not explosively large) + let mut selector = fresh_selector(); + + // Simple block with one instruction + let wasm_ops = vec![WasmOp::Block, WasmOp::I32Const(1), WasmOp::End]; + let instrs = selector.select_with_stack(&wasm_ops, 0).unwrap(); + // MOV for const + Label for block end + BX LR + assert!( + instrs.len() <= 5, + "Simple block should produce <= 5 ARM instructions, got {}", + instrs.len() + ); + assert!( + instrs.len() >= 2, + "Simple block should produce >= 2 ARM instructions, got {}", + instrs.len() + ); + + // Loop with br should produce bounded output + selector.reset(); + let wasm_ops = vec![WasmOp::Loop, WasmOp::Br(0), WasmOp::End]; + let instrs = selector.select_with_stack(&wasm_ops, 0).unwrap(); + assert!( + instrs.len() <= 5, + "Simple loop+br should produce <= 5 ARM instructions, got {}", + instrs.len() + ); + } }