From 11bcddd8dd838e4da6d65b4f67dcfd8d77724d71 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 8 Jul 2026 17:05:39 +0200 Subject: [PATCH] =?UTF-8?q?fix(globals):=20#649=20i64.const=20global=20ini?= =?UTF-8?q?tializers=20reach=20the=20emitted=20image=20=E2=80=94=20decoder?= =?UTF-8?q?=20captures=20both=20words,=20startup=20materializes=20the=20R9?= =?UTF-8?q?=20table?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The decoder's `init_i32` captured only a leading `i32.const`; an i64 global's init decoded to `None` and every consumer's `unwrap_or(0)` silently ZEROED the slot. #645 fixed the get/set PAIR lowering and the width-aware slot layout, but a nonzero `(global (mut i64) (i64.const X))` read before any set still returned garbage — the init existed nowhere in the output. Decoder: `WasmGlobal.init_i32` is RENAMED to `init: Option` (I32/I64) so no consumer survives by wildcard. f32/f64 inits stay `None` on purpose — float global access is the GI-FPU-001 (#369/#648) loud-skip lane and capturing bits here must not quietly unskip it. Consumers audited (all of them, post-rename): - `identify_stack_pointer_global`: matches `GlobalInit::I32` only (an SP is an i32 address; i64 inits are data, never promoted). - `--native-pointer-abi` `__synth_globals` region: stays 4-byte i32 slots; wide globals are already REFUSED up front (#643 bail — the decline-loudly arm), so only I32 inits can land. Byte-identical for i32-global modules (verified against origin/main). - Self-contained Cortex-M image (the #649 repro shape): globals were never materialized AT ALL — R9 was never even initialized. Now `generate_minimal_startup` gets the table words (#643 summed-width layout, i64 = two words lo-first), points R9 at `0x2000_0000 + linmem_size`, and stores every word before calling the user function; RAM sizing + the NoBits region cover the table. Both the all-exports and single-function builders. Tables past the STR.W #imm12 range decline loudly. No globals => the historical 28-byte startup blob and the whole ELF stay BYTE-IDENTICAL (verified). Red -> green: scripts/repro/i64_global_init_649_differential.py runs the default cortex-m4f image's REAL reset path in unicorn (artifact-derived, nothing fabricated), then the stateful export sequence vs one wasmtime instance. origin/main: FAIL (4 divergences — init reads return vector- table garbage). This branch: PASS (init reads, i32-after-i64 offset canary, #645 set-then-get pin, control). Gates: frozen anchors 10/10, #643 oracle PASS, cargo test --workspace green, fmt + clippy --workspace -D warnings clean. Fixes #649. Refs #645, #643, #648, #369. Co-Authored-By: Claude Fable 5 --- crates/synth-cli/src/main.rs | 334 ++++++++++++++---- crates/synth-core/src/wasm_decoder.rs | 91 ++++- crates/synth-synthesis/src/lib.rs | 3 +- scripts/repro/i64_global_init_649.wat | 41 +++ .../repro/i64_global_init_649_differential.py | 183 ++++++++++ 5 files changed, 562 insertions(+), 90 deletions(-) create mode 100644 scripts/repro/i64_global_init_649.wat create mode 100644 scripts/repro/i64_global_init_649_differential.py diff --git a/crates/synth-cli/src/main.rs b/crates/synth-cli/src/main.rs index d76cda41..a3f64153 100644 --- a/crates/synth-cli/src/main.rs +++ b/crates/synth-cli/src/main.rs @@ -20,7 +20,8 @@ use synth_core::target::TargetSpec; use synth_core::wasm_decoder::ImportEntry; use synth_core::wsc_facts::WscFact; use synth_synthesis::{ - FunctionOps, WasmGlobal, WasmMemory, WasmOp, decode_wasm_functions, decode_wasm_module, + FunctionOps, GlobalInit, WasmGlobal, WasmMemory, WasmOp, decode_wasm_functions, + decode_wasm_module, }; use tracing::{Level, info, warn}; use wast::parser::{self, ParseBuffer}; @@ -1254,6 +1255,9 @@ fn compile_command( // #643: per-global slot widths (8 for i64/f64) — type-aware globals-table // layout + register-pair global accesses. Empty for the demo path. let mut global_widths: Vec = Vec::new(); + // #649: initial R9 globals-table contents for the self-contained image + // (both words of an i64 init). Empty for the demo path. + let mut startup_globals_words: Vec = Vec::new(); let mut current_func_block_arity: Vec<(u8, u8)> = Vec::new(); // #509: value-carrying branches // VCR-PERF-002 Phase 1 (#494): loom `wsc.facts` premises — whole-module // table + this function's slice. Threaded to the CompileConfig; NOT yet @@ -1307,6 +1311,9 @@ fn compile_command( } global_widths[i] = g.slot_bytes; } + // #649: capture the initial globals-table contents so the + // self-contained image's startup can materialize them. + startup_globals_words = globals_table_words(&module.globals); let module_func_params_i64 = module.func_params_i64; let module_func_arg_counts = module.func_arg_counts; // VCR-PERF-002 Phase 1 (#494): whatever facts loom forwarded @@ -1500,7 +1507,7 @@ fn compile_command( } else if matches!(target_spec.family, synth_core::target::ArchFamily::RiscV) { build_riscv_elf(&code, &func_name)? } else if cortex_m { - build_cortex_m_elf(&code, &func_name, target_spec)? + build_cortex_m_elf(&code, &func_name, target_spec, &startup_globals_words)? } else { build_simple_elf(&code, &func_name)? }; @@ -2059,11 +2066,43 @@ fn identify_stack_pointer_global(globals: &[WasmGlobal], linmem_bytes: u32) -> O globals .iter() .filter(|g| g.mutable) - .filter_map(|g| g.init_i32.map(|v| (g.index, v))) + // #649: only an `i32.const` init can be a wasm stack pointer (the SP is + // an i32 address); i64 inits are ordinary data globals, never promoted. + .filter_map(|g| match g.init { + Some(GlobalInit::I32(v)) => Some((g.index, v)), + _ => None, + }) .filter(|&(_, v)| v > 0 && (v as u32) <= linmem_bytes) .max_by_key(|&(_, v)| v) } +/// #649: the initial CONTENTS of the R9 globals table for the self-contained +/// Cortex-M image, as little-endian words in the #643 summed-width layout — +/// global `i`'s offset is the sum of earlier globals' `slot_bytes` (an i64 +/// global occupies two consecutive words, low word first; every later global +/// shifts accordingly). Slots whose init was not captured (f32/f64 — the +/// GI-FPU-001 loud-skip lane — or a non-const init expr) stay ZERO: their +/// access-side handling is responsible, and we never fabricate a value. +fn globals_table_words(globals: &[WasmGlobal]) -> Vec { + let mut words: Vec = Vec::new(); + for g in globals { + let n = (g.slot_bytes.max(4) / 4) as usize; + let base = words.len(); + words.resize(base + n, 0); + match g.init { + Some(GlobalInit::I32(v)) => words[base] = v as u32, + Some(GlobalInit::I64(v)) => { + words[base] = v as u32; + if n > 1 { + words[base + 1] = ((v as u64) >> 32) as u32; + } + } + None => {} + } + } + words +} + fn reachable_from_exports( funcs: &[FunctionOps], num_imports: u32, @@ -2156,7 +2195,7 @@ fn compile_all_exports( type_arg_counts, all_data_segments, // #237: active data segments, for --native-pointer-abi stack_pointer_global_opt, // #237: (index, init) of the SP global, if any - all_globals, // #237: every defined global (index, init) — slot region under --native-pointer-abi + all_globals, // #237/#649: every defined global's full decl (init + width) — native-abi slots + image-materialized R9 table all_global_widths, // #643: per-global slot widths (8 for i64/f64) — type-aware R9 table layout all_func_ret_i64, // #311: per-function returns-i64 (pair tagging) all_type_ret_i64, // #311: per-type returns-i64 (call_indirect) @@ -2255,7 +2294,7 @@ fn compile_all_exports( merged_type_arg_counts, Vec::new(), // #237: data segments not threaded for WAST (single-module .wasm path covers it) None, // #237: SP-global promotion is single-module .wasm only - Vec::new(), // #237: globals slot region is single-module .wasm only + Vec::new(), // #237/#649: globals decls (slot region + init materialization) are single-module .wasm only Vec::new(), // #643: WAST fixture suite is i32-only — legacy 4-byte global slots Vec::new(), // #311: WAST runs the fixture suite; i32-only Vec::new(), @@ -2296,13 +2335,6 @@ fn compile_all_exports( // linmem extent gates the "plausible stack top" heuristic. let linmem_bytes = memories.first().map(|m| m.initial_bytes()).unwrap_or(0); let sp_global = identify_stack_pointer_global(&module.globals, linmem_bytes); - // #237: every defined global gets a materialized slot under the - // native-pointer ABI (init defaults to 0 for non-i32.const inits). - let globals: Vec<(u32, i32)> = module - .globals - .iter() - .map(|g| (g.index, g.init_i32.unwrap_or(0))) - .collect(); // #643: per-global slot widths (4 = i32/f32, 8 = i64/f64, 16 = v128), // indexed by global index — the selector lays the R9 globals table out // by summing these, giving i64 globals room for both words and @@ -2353,7 +2385,11 @@ fn compile_all_exports( type_arg_counts, data_segs, sp_global, - globals, + // #237/#649: the full global declarations — the native-pointer ABI + // derives its (index, i32-init) slot pairs from these, and the + // self-contained Cortex-M image materializes the width-aware + // (both-words for i64) R9 globals table from them. + module.globals, global_widths, module.func_ret_i64, module.type_ret_i64, @@ -2734,7 +2770,23 @@ fn compile_all_exports( // #237: used-extent sizing + globals slots, native-pointer ABI only. if native_pointer_abi { Some(NativeGlobalsLayout { - globals: all_globals.clone(), + // #649: the native-abi `__synth_globals` region stays + // 4-byte i32 slots — wide (i64/f64/v128) globals were + // REFUSED up front (#643 bail above), so only `i32.const` + // inits can land here. f32 slots (captured as `None` — + // the GI-FPU-001 loud-skip lane) stay zero. + globals: all_globals + .iter() + .map(|g| { + ( + g.index, + match g.init { + Some(GlobalInit::I32(v)) => v, + _ => 0, + }, + ) + }) + .collect(), sp_init: stack_pointer_global_opt.map(|(_, v)| v).unwrap_or(0), shadow_stack_size, }) @@ -2747,7 +2799,15 @@ fn compile_all_exports( !matches!(target_spec.isa, synth_core::target::IsaVariant::Arm32), )? } else if cortex_m { - build_multi_func_cortex_m_elf(&compiled_funcs, &all_memories, target_spec)? + // #649: the self-contained image materializes the R9 globals table — + // startup writes every global's captured init (both words for i64) + // into RAM just above linear memory and points R9 at it. + build_multi_func_cortex_m_elf( + &compiled_funcs, + &all_memories, + target_spec, + &globals_table_words(&all_globals), + )? } else { build_multi_func_simple_elf(&compiled_funcs)? }; @@ -3792,6 +3852,10 @@ fn build_multi_func_cortex_m_elf( funcs: &[ElfFunction], memories: &[WasmMemory], target: &TargetSpec, + // #649: initial R9 globals-table contents (little-endian words, #643 + // summed-width layout). Empty = no globals: startup, RAM sizing and the + // NoBits region are BYTE-IDENTICAL to the pre-#649 output. + globals_words: &[u32], ) -> Result> { let flash_base: u32 = 0x0000_0000; let ram_base: u32 = 0x2000_0000; @@ -3801,15 +3865,28 @@ fn build_multi_func_cortex_m_elf( let linear_memory_pages = memories.first().map(|m| m.initial_pages).unwrap_or(1); let linear_memory_size = linear_memory_pages * 64 * 1024; // 64KB per page + // #649: the R9 globals table lives immediately above linear memory. The + // startup materializer addresses it with `STR.W [R9, #imm12]` (max 4095). + let globals_table_bytes = (globals_words.len() as u32) * 4; + if globals_table_bytes > 4096 { + anyhow::bail!( + "globals table ({} bytes) exceeds the startup materializer's \ + STR.W #imm12 range (4096 bytes) — refusing to emit a partial \ + table (#649)", + globals_table_bytes + ); + } + // RAM layout: // 0x2000_0000: Linear memory (R11 points here) - // 0x2000_0000 + linear_memory_size: Stack base + // 0x2000_0000 + linear_memory_size: R9 globals table (#649, if any) + // above that: Stack base // ram_base + ram_size: Stack top (grows down) // - // Auto-scale RAM: linear memory + 8KB stack, rounded up to next 64KB boundary. - // Minimum 128KB for backwards compatibility. + // Auto-scale RAM: linear memory + globals table + 8KB stack, rounded up to + // next 64KB boundary. Minimum 128KB for backwards compatibility. let min_stack_size: u32 = 8 * 1024; - let needed = linear_memory_size + min_stack_size; + let needed = linear_memory_size + globals_table_bytes + min_stack_size; let ram_size: u32 = std::cmp::max(128 * 1024, (needed + 0xFFFF) & !0xFFFF); let stack_top = ram_base + ram_size; @@ -3831,7 +3908,7 @@ fn build_multi_func_cortex_m_elf( let vector_table_size: u32 = 128; let startup_addr = flash_base + vector_table_size; - let startup_code = generate_minimal_startup(linear_memory_size); + let startup_code = generate_minimal_startup(linear_memory_size, globals_words); let startup_size = startup_code.len() as u32; let default_handler_addr = startup_addr + startup_size; @@ -3960,11 +4037,13 @@ fn build_multi_func_cortex_m_elf( flash_image.push(0); } - // Startup code - patch literal pool to point to FIRST function - // Literal pool is at offset 24 (after R10/R11 init + LDR/BLX/B/padding) + // Startup code - patch literal pool to point to FIRST function. + // The literal pool is the LAST word of the startup blob (#649: the blob + // grows with the globals-table materializer, so no fixed offset 24). let mut patched_startup = startup_code.clone(); let first_func_addr = funcs_base | 1; // Thumb bit - patched_startup[24..28].copy_from_slice(&first_func_addr.to_le_bytes()); + let lit = patched_startup.len() - 4; + patched_startup[lit..].copy_from_slice(&first_func_addr.to_le_bytes()); flash_image.extend_from_slice(&patched_startup); // Default handler @@ -4018,11 +4097,15 @@ fn build_multi_func_cortex_m_elf( // Add linear memory section (BSS-like, no file data) // This section tells the loader about the RAM region for WASM linear memory if linear_memory_size > 0 { + // #649: cover the R9 globals table (just above linear memory) too, so + // a loader that maps by program header reserves it. 0 when no globals + // — the region stays byte-identical. + let ram_region_size = linear_memory_size + globals_table_bytes; // Program header for linear memory (READ | WRITE, no EXEC) // Use load_nobits since there's no file data, just memory allocation let ram_phdr = ProgramHeader::load_nobits( ram_base, - linear_memory_size, + ram_region_size, ProgramFlags::READ | ProgramFlags::WRITE, ); elf_builder.add_program_header(ram_phdr); @@ -4032,7 +4115,7 @@ fn build_multi_func_cortex_m_elf( .with_flags(SectionFlags::ALLOC | SectionFlags::WRITE) .with_addr(ram_base) .with_align(4) - .with_size(linear_memory_size); + .with_size(ram_region_size); elf_builder.add_section(linear_memory_section); @@ -4438,7 +4521,14 @@ fn build_simple_elf(code: &[u8], func_name: &str) -> Result> { } /// Build a complete Cortex-M ELF with vector table and startup code -fn build_cortex_m_elf(code: &[u8], func_name: &str, target: &TargetSpec) -> Result> { +fn build_cortex_m_elf( + code: &[u8], + func_name: &str, + target: &TargetSpec, + // #649: initial R9 globals-table contents (see `globals_table_words`). + // Empty = no globals: output byte-identical to the pre-#649 builder. + globals_words: &[u32], +) -> Result> { // Memory layout for generic Cortex-M (works with QEMU/Renode) let flash_base: u32 = 0x0000_0000; let ram_base: u32 = 0x2000_0000; @@ -4448,12 +4538,24 @@ fn build_cortex_m_elf(code: &[u8], func_name: &str, target: &TargetSpec) -> Resu // Default linear memory size (1 WASM page = 64KB) for single-function mode let linear_memory_size: u32 = 64 * 1024; + // #649: R9 globals table just above linear memory (0x2001_0000); the + // stack grows down from 0x2002_0000, leaving it 64KB of headroom. The + // startup materializer addresses the table with STR.W #imm12 (max 4095). + if globals_words.len() * 4 > 4096 { + anyhow::bail!( + "globals table ({} bytes) exceeds the startup materializer's \ + STR.W #imm12 range (4096 bytes) — refusing to emit a partial \ + table (#649)", + globals_words.len() * 4 + ); + } + // Calculate addresses let vector_table_addr = flash_base; let vector_table_size: u32 = 128; // 32 entries * 4 bytes let startup_addr = flash_base + vector_table_size; - let startup_code = generate_minimal_startup(linear_memory_size); + let startup_code = generate_minimal_startup(linear_memory_size, globals_words); let startup_size = startup_code.len() as u32; let default_handler_addr = startup_addr + startup_size; @@ -4506,11 +4608,13 @@ fn build_cortex_m_elf(code: &[u8], func_name: &str, target: &TargetSpec) -> Resu flash_image.push(0); } - // Startup code (patch the literal pool with actual function address) - // Literal pool is at offset 24 (after R10/R11 init + LDR/BLX/B/padding) + // Startup code (patch the literal pool with actual function address). + // The literal pool is the LAST word of the startup blob (#649: the blob + // grows with the globals-table materializer, so no fixed offset 24). let mut patched_startup = startup_code.clone(); let func_addr_thumb = code_addr | 1; // Thumb bit - patched_startup[24..28].copy_from_slice(&func_addr_thumb.to_le_bytes()); + let lit = patched_startup.len() - 4; + patched_startup[lit..].copy_from_slice(&func_addr_thumb.to_le_bytes()); flash_image.extend_from_slice(&patched_startup); // Default handler @@ -4603,11 +4707,19 @@ fn build_cortex_m_elf(code: &[u8], func_name: &str, target: &TargetSpec) -> Resu /// /// # Arguments /// * `memory_size` - Size of linear memory in bytes (for R10 bounds checking) +/// * `globals_words` - #649: initial R9 globals-table contents (little-endian +/// words, #643 summed-width layout). When non-empty, startup points R9 at +/// `0x2000_0000 + memory_size` and stores every word there BEFORE calling +/// the user function — this is where `i64.const`/`i32.const` global +/// initializers reach the running image (they exist nowhere else in a +/// self-contained ELF; a zeroed table silently dropped every nonzero init). +/// Empty (no globals) emits the historical 28-byte blob, byte-identical. /// /// # Memory Register Setup /// * R10 = memory_size (for bounds checking) /// * R11 = 0x20000000 (linear memory base) -fn generate_minimal_startup(memory_size: u32) -> Vec { +/// * R9 = 0x20000000 + memory_size (globals table; only when globals exist) +fn generate_minimal_startup(memory_size: u32, globals_words: &[u32]) -> Vec { // This startup code: // 1. Initializes R10 with memory size (for bounds checking) // 2. Initializes R11 with linear memory base (0x20000000) for WASM memory access @@ -4629,46 +4741,49 @@ fn generate_minimal_startup(memory_size: u32) -> Vec { let r10_movw = encode_thumb2_movw(10, (memory_size & 0xFFFF) as u16); let r10_movt = encode_thumb2_movt(10, (memory_size >> 16) as u16); - vec![ - // MOVW R10, #(memory_size & 0xFFFF) - r10_movw[0], - r10_movw[1], - r10_movw[2], - r10_movw[3], - // MOVT R10, #(memory_size >> 16) - r10_movt[0], - r10_movt[1], - r10_movt[2], - r10_movt[3], - // MOVW R11, #0x0000 - Thumb-2 32-bit encoding - 0x40, - 0xF2, - 0x00, - 0x0B, - // MOVT R11, #0x2000 - Thumb-2 32-bit encoding - 0xC2, - 0xF2, - 0x00, - 0x0B, - // LDR r0, [pc, #4] - Thumb 16-bit encoding: 0x4801 - // PC = current_addr + 4, literal at PC+4 - 0x01, - 0x48, - // BLX r0 - Thumb encoding: 0x4780 - 0x80, - 0x47, - // B . (branch to self) - Thumb encoding: 0xe7fe - 0xfe, - 0xe7, - // Padding for alignment (to make literal pool 4-byte aligned) - 0x00, - 0x00, - // Literal pool placeholder at offset 24 (will be patched with func_addr | 1) - 0x91, - 0x00, - 0x00, - 0x00, - ] + let mut code: Vec = Vec::new(); + // MOVW R10, #(memory_size & 0xFFFF) / MOVT R10, #(memory_size >> 16) + code.extend_from_slice(&r10_movw); + code.extend_from_slice(&r10_movt); + // MOVW R11, #0x0000 / MOVT R11, #0x2000 - Thumb-2 32-bit encodings + code.extend_from_slice(&[0x40, 0xF2, 0x00, 0x0B]); + code.extend_from_slice(&[0xC2, 0xF2, 0x00, 0x0B]); + + // #649: materialize the R9 globals table. R9 = table base; each captured + // init word is stored via the R12 scratch (IP — reserved to the encoder, + // never live here: this runs before any user code). Every insn is 4 bytes, + // so the LDR-literal alignment below is undisturbed. + if !globals_words.is_empty() { + let base = 0x2000_0000u32.wrapping_add(memory_size); + // MOVW/MOVT R9, #base + code.extend_from_slice(&encode_thumb2_movw(9, (base & 0xFFFF) as u16)); + code.extend_from_slice(&encode_thumb2_movt(9, (base >> 16) as u16)); + for (i, w) in globals_words.iter().enumerate() { + // MOVW/MOVT R12, #word + code.extend_from_slice(&encode_thumb2_movw(12, (w & 0xFFFF) as u16)); + code.extend_from_slice(&encode_thumb2_movt(12, (w >> 16) as u16)); + // STR.W R12, [R9, #i*4] — T3: 1111 1000 1100 Rn | Rt imm12. + // Callers reject tables past the #imm12 range (4095) up front. + let off = (i as u16) * 4; + let hw1: u16 = 0xF8C0 | 9; // Rn = R9 + let hw2: u16 = (12 << 12) | off; // Rt = R12 + code.extend_from_slice(&hw1.to_le_bytes()); + code.extend_from_slice(&hw2.to_le_bytes()); + } + } + + // LDR r0, [pc, #4] - Thumb 16-bit encoding: 0x4801 + // (PC = LDR addr + 4, already 4-aligned; literal sits at PC+4 = LDR+8) + code.extend_from_slice(&[0x01, 0x48]); + // BLX r0 - Thumb encoding: 0x4780 + code.extend_from_slice(&[0x80, 0x47]); + // B . (branch to self) - Thumb encoding: 0xe7fe + code.extend_from_slice(&[0xfe, 0xe7]); + // Padding for alignment (to make literal pool 4-byte aligned) + code.extend_from_slice(&[0x00, 0x00]); + // Literal pool placeholder — LAST word, patched with func_addr | 1 + code.extend_from_slice(&[0x91, 0x00, 0x00, 0x00]); + code } /// Encode Thumb-2 MOVW instruction (move 16-bit immediate to low half of register) @@ -5558,7 +5673,8 @@ mod tests { 0x1e, 0xff, 0x2f, 0xe1, // BX lr (ARM encoding) ]; - let elf_data = build_cortex_m_elf(&code, "test_func", &TargetSpec::cortex_m3()).unwrap(); + let elf_data = + build_cortex_m_elf(&code, "test_func", &TargetSpec::cortex_m3(), &[]).unwrap(); // Verify ELF magic assert_eq!(&elf_data[0..4], b"\x7fELF", "Invalid ELF magic"); @@ -5578,7 +5694,7 @@ mod tests { fn test_vector_table_structure() { let code = vec![0x00, 0x80, 0x80, 0xe0]; // ADD r0, r0, r1 - let elf_data = build_cortex_m_elf(&code, "test", &TargetSpec::cortex_m3()).unwrap(); + let elf_data = build_cortex_m_elf(&code, "test", &TargetSpec::cortex_m3(), &[]).unwrap(); // Find .text section (it starts after ELF headers) // For simplicity, look for the vector table pattern @@ -5632,7 +5748,7 @@ mod tests { fn test_startup_code_patching() { let code = vec![0x00, 0x80, 0x80, 0xe0]; - let elf_data = build_cortex_m_elf(&code, "patched", &TargetSpec::cortex_m3()).unwrap(); + let elf_data = build_cortex_m_elf(&code, "patched", &TargetSpec::cortex_m3(), &[]).unwrap(); // With the new startup code layout (28 bytes with R10/R11 init): // - Startup: 0x80 (28 bytes) @@ -5663,7 +5779,7 @@ mod tests { fn test_minimal_startup_generation() { // Test with 64KB memory size (0x10000) let memory_size: u32 = 64 * 1024; - let startup = generate_minimal_startup(memory_size); + let startup = generate_minimal_startup(memory_size, &[]); // Should be 28 bytes: // MOVW R10 + MOVT R10 + MOVW R11 + MOVT R11 + LDR + BLX + B + padding + literal @@ -5694,6 +5810,74 @@ mod tests { assert_eq!(startup[21], 0xe7); } + /// #649: the startup globals-table materializer — R9 points just above + /// linear memory and every captured init word (BOTH words of an i64) is + /// stored before the user function runs. The pre/post scaffolding stays + /// byte-identical to the historical 28-byte blob. + #[test] + fn test_startup_globals_materializer_649() { + let memory_size: u32 = 64 * 1024; + // i64 0x123456789ABCDEF0 (lo, hi) followed by an i32 canary. + let words = [0x9ABCDEF0u32, 0x12345678, 0x0C0FFEE1]; + let startup = generate_minimal_startup(memory_size, &words); + let empty = generate_minimal_startup(memory_size, &[]); + + // 16 scaffold + 8 (R9 movw/movt) + 3 * 12 (movw/movt/str) + 12 tail + assert_eq!(startup.len(), 16 + 8 + 36 + 12, "materializer size"); + // R10/R11 init unchanged. + assert_eq!(&startup[..16], &empty[..16], "R10/R11 scaffold unchanged"); + // R9 = 0x2001_0000 (ram_base + 64KB linear memory). + assert_eq!(&startup[16..20], &encode_thumb2_movw(9, 0x0000)); + assert_eq!(&startup[20..24], &encode_thumb2_movt(9, 0x2001)); + // First word: MOVW/MOVT R12, #0x9ABCDEF0; STR.W R12, [R9, #0]. + assert_eq!(&startup[24..28], &encode_thumb2_movw(12, 0xDEF0)); + assert_eq!(&startup[28..32], &encode_thumb2_movt(12, 0x9ABC)); + assert_eq!(&startup[32..36], &[0xC9, 0xF8, 0x00, 0xC0]); + // Second word (the i64 HIGH word — the #649 payload): STR at #4. + assert_eq!(&startup[36..40], &encode_thumb2_movw(12, 0x5678)); + assert_eq!(&startup[40..44], &encode_thumb2_movt(12, 0x1234)); + assert_eq!(&startup[44..48], &[0xC9, 0xF8, 0x04, 0xC0]); + // i32 canary after the i64: STR at #8 (the #643 layout shift). + assert_eq!(&startup[56..60], &[0xC9, 0xF8, 0x08, 0xC0]); + // Tail (LDR/BLX/B/pad/literal) identical to the no-globals blob. + assert_eq!(&startup[60..], &empty[16..], "call scaffold unchanged"); + // No globals => byte-identical historical 28-byte blob. + assert_eq!(empty.len(), 28); + } + + /// #649: `globals_table_words` lays inits out by the #643 summed-width + /// rule — i64 takes two words (lo first), an uncaptured (float) init + /// leaves its slot zeroed, later globals shift accordingly. + #[test] + fn test_globals_table_words_layout_649() { + let globals = vec![ + WasmGlobal { + index: 0, + init: Some(GlobalInit::I64(0x123456789ABCDEF0u64 as i64)), + mutable: true, + slot_bytes: 8, + }, + WasmGlobal { + index: 1, + init: Some(GlobalInit::I32(7)), + mutable: true, + slot_bytes: 4, + }, + // f64: init not captured (GI-FPU-001 loud-skip lane) — zero slot. + WasmGlobal { + index: 2, + init: None, + mutable: true, + slot_bytes: 8, + }, + ]; + assert_eq!( + globals_table_words(&globals), + vec![0x9ABCDEF0, 0x12345678, 7, 0, 0] + ); + assert!(globals_table_words(&[]).is_empty()); + } + #[test] fn test_default_handler_generation() { let handler = generate_default_handler(); diff --git a/crates/synth-core/src/wasm_decoder.rs b/crates/synth-core/src/wasm_decoder.rs index e156d974..df92e362 100644 --- a/crates/synth-core/src/wasm_decoder.rs +++ b/crates/synth-core/src/wasm_decoder.rs @@ -47,6 +47,21 @@ pub struct WasmMemory { pub shared: bool, } +/// A captured constant global initializer (#649). Only INTEGER `t.const` init +/// exprs are captured: `f32.const`/`f64.const` inits deliberately decode to +/// `None` — float-typed global ACCESS is the GI-FPU-001 (#369) loud-skip lane, +/// and fabricating a bit-pattern here must not quietly unskip it. Non-const +/// init exprs (e.g. `global.get` of an import) are not statically known and +/// also decode to `None`. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum GlobalInit { + /// A leading `i32.const` initializer. + I32(i32), + /// A leading `i64.const` initializer — BOTH words must reach the emitted + /// global slot (#649: `init_i32`-shaped capture silently zeroed these). + I64(i64), +} + /// A WASM global's declaration — its initial value and mutability (#237). /// Needed so the native-pointer ABI can recognize a global whose initializer is /// a linear-memory address (e.g. `$__stack_pointer = 65536`) and make it @@ -56,8 +71,10 @@ pub struct WasmMemory { pub struct WasmGlobal { /// Global index (defined globals; imported globals are not counted here). pub index: u32, - /// The `i32.const` initializer value (other init exprs decode to `None`). - pub init_i32: Option, + /// The captured constant initializer (#237/#649): `i32.const` or + /// `i64.const`. Float/non-const init exprs decode to `None` — see + /// [`GlobalInit`]. + pub init: Option, /// Whether the global is mutable. pub mutable: bool, /// #643: byte width of the global's storage slot, from its declared value @@ -494,18 +511,25 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { } } Payload::GlobalSection(reader) => { - // #237: capture each defined global's i32 initializer + mutability. - // The init is a const expr; we only decode a leading `i32.const` - // (the shape `$__stack_pointer`/data-layout globals use). Anything - // else (global.get, f32/f64, etc.) records `init_i32: None` and is - // left to the table-relative path. + // #237/#649: capture each defined global's constant initializer + // + mutability. The init is a const expr; we decode a leading + // `i32.const` (the `$__stack_pointer`/data-layout shape) or + // `i64.const` (#649: capturing only i32 silently ZEROED every + // nonzero i64 init). f32/f64 inits stay `None` on purpose — + // float global access is the GI-FPU-001 (#369) loud-skip lane — + // as do non-const init exprs (`global.get` of an import). for (idx, global) in reader.into_iter().enumerate() { let global = global.context("Failed to parse global")?; - let mut init_i32 = None; let mut ops = global.init_expr.get_operators_reader(); - if let Ok(wasmparser::Operator::I32Const { value }) = ops.read() { - init_i32 = Some(value); - } + let init = match ops.read() { + Ok(wasmparser::Operator::I32Const { value }) => { + Some(GlobalInit::I32(value)) + } + Ok(wasmparser::Operator::I64Const { value }) => { + Some(GlobalInit::I64(value)) + } + _ => None, + }; // #643: record the slot width from the DECLARED value type. // i64/f64 globals occupy 8 bytes (a register pair on the // 32-bit targets), v128 sixteen; laying every global out at @@ -517,7 +541,7 @@ pub fn decode_wasm_module(wasm_bytes: &[u8]) -> Result { }; globals.push(WasmGlobal { index: idx as u32, - init_i32, + init, mutable: global.ty.mutable, slot_bytes, }); @@ -2030,10 +2054,14 @@ mod tests { assert_eq!(module.globals.len(), 2, "both globals captured"); let sp = &module.globals[0]; assert_eq!(sp.index, 0); - assert_eq!(sp.init_i32, Some(65536), "stack-pointer init captured"); + assert_eq!( + sp.init, + Some(GlobalInit::I32(65536)), + "stack-pointer init captured" + ); assert!(sp.mutable, "stack pointer is mutable"); let c = &module.globals[1]; - assert_eq!(c.init_i32, Some(7)); + assert_eq!(c.init, Some(GlobalInit::I32(7))); assert!(!c.mutable, "second global is immutable"); assert_eq!(sp.slot_bytes, 4, "i32 global occupies one 4-byte slot"); assert_eq!(c.slot_bytes, 4); @@ -2061,6 +2089,41 @@ mod tests { assert_eq!(module.globals[2].slot_bytes, 8, "f64 global is 8 bytes"); } + /// #649: a nonzero `i64.const` initializer is captured as BOTH words — the + /// `init_i32`-shaped capture dropped it to `None` and every consumer's + /// `unwrap_or(0)` silently ZEROED the global. f32/f64 inits stay `None` + /// (GI-FPU-001/#369 loud-skip lane — never fabricate a float bit-pattern). + #[test] + fn test_decode_captures_i64_global_initializer_649() { + let wat = r#" + (module + (global $g (mut i64) (i64.const 0x123456789ABCDEF0)) + (global $n (mut i64) (i64.const -1)) + (global $f (mut f64) (f64.const 1.5)) + (global $h (mut f32) (f32.const 2.5)) + (func (export "f") (result i32) i32.const 0) + ) + "#; + let wasm = wat::parse_str(wat).expect("Failed to parse WAT"); + let module = decode_wasm_module(&wasm).expect("Failed to decode"); + + assert_eq!(module.globals.len(), 4); + assert_eq!( + module.globals[0].init, + Some(GlobalInit::I64(0x123456789ABCDEF0u64 as i64)), + "nonzero i64 init captured with both words" + ); + assert_eq!(module.globals[1].init, Some(GlobalInit::I64(-1))); + assert_eq!( + module.globals[2].init, None, + "f64 init is NOT captured (GI-FPU-001 loud-skip lane)" + ); + assert_eq!( + module.globals[3].init, None, + "f32 init is NOT captured (GI-FPU-001 loud-skip lane)" + ); + } + /// #509: the decoder records `(param_count, result_count)` for every /// `Block`/`Loop`/`If`, ordinal-keyed in op order, covering all three /// blocktype encodings: `Empty → (0,0)`, `ValType → (0,1)`, and diff --git a/crates/synth-synthesis/src/lib.rs b/crates/synth-synthesis/src/lib.rs index 2bacbb0a..a23e086e 100644 --- a/crates/synth-synthesis/src/lib.rs +++ b/crates/synth-synthesis/src/lib.rs @@ -33,7 +33,8 @@ pub use rules::{ RuleDatabase, ShiftType, SynthesisRule, VfpReg, WasmOp, }; pub use wasm_decoder::{ - DecodedModule, FunctionOps, WasmGlobal, WasmMemory, decode_wasm_functions, decode_wasm_module, + DecodedModule, FunctionOps, GlobalInit, WasmGlobal, WasmMemory, decode_wasm_functions, + decode_wasm_module, }; // Stub for PoC diff --git a/scripts/repro/i64_global_init_649.wat b/scripts/repro/i64_global_init_649.wat new file mode 100644 index 00000000..cd5f81a6 --- /dev/null +++ b/scripts/repro/i64_global_init_649.wat @@ -0,0 +1,41 @@ +;; #649: nonzero i64.const GLOBAL INITIALIZERS were silently ZEROED — the +;; decoder captured only a leading `i32.const` (init_i32), so an i64 global's +;; init never reached the emitted image: reads returned 0 until a set. +;; (#645 fixed the get/set PAIR lowering + slot layout, but not initializers.) +;; +;; Fixture shape: +;; * $g (i64, index 0) — nonzero i64 init straddling 32 bits, read via +;; global.get BEFORE any set: the red case. +;; * $c (i32, index 1) — declared AFTER the i64 global with its own nonzero +;; init: the OFFSET canary. Its init must land at the summed-width slot +;; ([r9,#8]), not idx*4 ([r9,#4] — which would alias $g's high word). +;; * set64/set32 + re-reads — the #645 set-then-get pin (no regression). +;; * get_lo is FIRST: the self-contained image's startup BLXes function 0, +;; so function 0 must not mutate the globals before the harness reads them. +;; * pure_add — global-free control. +(module + (global $g (mut i64) (i64.const 0x123456789ABCDEF0)) + (global $c (mut i32) (i32.const 0x0C0FFEE1)) + + (func (export "get_lo") (result i32) + (i32.wrap_i64 (global.get $g))) + + (func (export "get_hi") (result i32) + (i32.wrap_i64 (i64.shr_u (global.get $g) (i64.const 32)))) + + (func (export "get32") (result i32) + (global.get $c)) + + ;; store an i64 assembled from two i32 halves (#643 harness shape) + (func (export "set64") (param $lo i32) (param $hi i32) + (global.set $g + (i64.or + (i64.extend_i32_u (local.get $lo)) + (i64.shl (i64.extend_i32_u (local.get $hi)) (i64.const 32))))) + + (func (export "set32") (param i32) + (global.set $c (local.get 0))) + + ;; global-free control + (func (export "pure_add") (param i32 i32) (result i32) + (i32.add (local.get 0) (local.get 1)))) diff --git a/scripts/repro/i64_global_init_649_differential.py b/scripts/repro/i64_global_init_649_differential.py new file mode 100644 index 00000000..af0af249 --- /dev/null +++ b/scripts/repro/i64_global_init_649_differential.py @@ -0,0 +1,183 @@ +#!/usr/bin/env python3 +"""#649 — nonzero i64.const GLOBAL INITIALIZERS silently zeroed. + +The decoder's `init_i32` captured only a leading `i32.const`; an i64 global's +init decoded to `None` and every consumer's `unwrap_or(0)` zeroed the slot. +#645 fixed the get/set PAIR lowering + width-aware slot layout — but a +`(global (mut i64) (i64.const X))` read BEFORE any set still returned 0. + +This oracle runs the DEFAULT self-contained Cortex-M image (`--target +cortex-m4f`, the exact #649 verification shape) end to end, ARTIFACT-derived: + + 1. unicorn executes the image's REAL startup (reset path) up to — not + including — the `LDR r0,[pc]; BLX r0` call scaffold. With the fix the + startup materializes the R9 globals table (both words of the i64 init + + the i32 canary) and points R9 at it; on origin/main it sets only R10/R11. + 2. exports are then called with the startup's register state preserved + (symbols from the ELF symtab, never disasm text) and compared against + the SAME stateful sequence on ONE wasmtime instance: + + get_lo / get_hi # init read BEFORE any set — the RED case + get32 # i32-declared-AFTER-i64 offset canary (init) + set64(...); get_lo/get_hi # the #645 set-then-get pin (no regression) + set32(...); get32 # canary slot still independent after sets + pure_add # global-free control + +Red on origin/main (init reads diverge), green with the #649 fix. + +Run (needs wasmtime + unicorn + pyelftools): + SYNTH=./target/debug/synth /tmp/synthvenv/bin/python \ + scripts/repro/i64_global_init_649_differential.py +""" + +import os +import subprocess +import sys +from pathlib import Path + +import wasmtime +from elftools.elf.elffile import ELFFile +from unicorn import UC_ARCH_ARM, UC_MODE_THUMB, Uc, UcError +from unicorn.arm_const import ( + UC_ARM_REG_LR, + UC_ARM_REG_R0, + UC_ARM_REG_R1, + UC_ARM_REG_R9, + UC_ARM_REG_SP, +) + +WAT = Path(__file__).with_name("i64_global_init_649.wat") +SYNTH = os.environ.get("SYNTH", "./target/debug/synth") + +FLASH, RAM, RAM_SIZE = 0x0000_0000, 0x2000_0000, 0x40000 +RET = 0x000F_0000 # inside the flash map, far past any code + +I64_INIT = 0x123456789ABCDEF0 +I32_INIT = 0x0C0FFEE1 +SET64_VAL = 0xAABBCCDD11223344 + + +def compile_synth(out): + env = {"PATH": "/usr/bin:/bin"} + cmd = [SYNTH, "compile", str(WAT), "-o", out, "--all-exports", + "-b", "arm", "--target", "cortex-m4f"] + r = subprocess.run(cmd, capture_output=True, text=True, env=env) + if r.returncode != 0: + sys.exit(f"compile failed: {r.stderr}") + + +def load(elf): + f = ELFFile(open(elf, "rb")) + text = f.get_section_by_name(".text") + code, base = text.data(), text["sh_addr"] + syms = {} + for sec in f.iter_sections(): + if sec.header.sh_type == "SHT_SYMTAB": + for sy in sec.iter_symbols(): + if sy.name and sy["st_info"]["type"] == "STT_FUNC": + syms[sy.name] = sy["st_value"] + return code, base, syms + + +class ImageRunner: + """The DEFAULT self-contained image, startup included: one persistent + unicorn instance; the globals table (if any) is whatever the ARTIFACT's + own reset path materialized — the harness fabricates nothing.""" + + def __init__(self, code, base, syms): + self.base, self.syms = base, syms + self.mu = Uc(UC_ARCH_ARM, UC_MODE_THUMB) + self.mu.mem_map(FLASH, 0x100000) + self.mu.mem_map(RAM, RAM_SIZE) # zeroed RAM: inits must come from startup + self.mu.mem_write(base, code) + # Initial SP from vector table word 0 (the image's own stack top). + self.sp = int.from_bytes(code[0:4], "little") + reset = syms.get("Reset_Handler") + if reset is None: + sys.exit("Reset_Handler missing from symtab") + # Execute the real startup UP TO the `LDR r0,[pc,#4]; BLX r0` call + # scaffold (we drive the calls ourselves). Locate it by its exact + # 4-byte encoding within the startup region. + stop = code.find(b"\x01\x48\x80\x47", (reset & ~1) - base) + if stop < 0: + sys.exit("startup call scaffold (LDR r0/BLX r0) not found") + self.mu.reg_write(UC_ARM_REG_SP, self.sp) + self.mu.emu_start(reset | 1, base + stop, count=10000) + self.startup_r9 = self.mu.reg_read(UC_ARM_REG_R9) + + def call(self, fn, args=()): + faddr = self.syms.get(fn) + if faddr is None: + return f"ERR:symbol {fn} missing" + for reg, val in zip((UC_ARM_REG_R0, UC_ARM_REG_R1), args): + self.mu.reg_write(reg, val & 0xFFFFFFFF) + # SP/LR reset per call; R9/R10/R11 stay whatever STARTUP set them to. + self.mu.reg_write(UC_ARM_REG_SP, self.sp) + self.mu.reg_write(UC_ARM_REG_LR, RET | 1) + try: + self.mu.emu_start(faddr | 1, RET, count=100000) + except UcError as e: + return f"ERR:{e}" + return self.mu.reg_read(UC_ARM_REG_R0) & 0xFFFFFFFF + + +class WasmtimeRunner: + """Stateful ground truth: ONE instance for the whole sequence.""" + + def __init__(self): + engine = wasmtime.Engine() + module = wasmtime.Module.from_file(engine, str(WAT)) + self.store = wasmtime.Store(engine) + self.inst = wasmtime.Instance(self.store, module, []) + + def call(self, fn, args=()): + signed = [a - (1 << 32) if a >= (1 << 31) else a for a in args] + r = self.inst.exports(self.store)[fn](self.store, *signed) + return (r if r is not None else 0) & 0xFFFFFFFF + + +def sequence(): + lo, hi = SET64_VAL & 0xFFFFFFFF, SET64_VAL >> 32 + # The RED cases: init values read BEFORE any set. + yield ("init-read get_lo (RED case)", "get_lo", ()) + yield ("init-read get_hi (RED case)", "get_hi", ()) + yield ("init-read i32-after-i64 canary", "get32", ()) + # The #645 pin: set-then-get across calls still correct. + yield ("pin set64", "set64", (lo, hi)) + yield ("pin get_lo after set", "get_lo", ()) + yield ("pin get_hi after set", "get_hi", ()) + yield ("canary unclobbered by set64", "get32", ()) + yield ("pin set32", "set32", (0x5EED5EED,)) + yield ("pin get32 after set", "get32", ()) + yield ("control pure_add", "pure_add", (41, 1)) + + +def main(): + out = "/tmp/i64ginit649.elf" + compile_synth(out) + code, base, syms = load(out) + img = ImageRunner(code, base, syms) + gt = WasmtimeRunner() + print(f"=== #649 default image (cortex-m4f), startup R9 = " + f"{img.startup_r9:#010x} ===") + fails = 0 + for step, fn, fargs in sequence(): + exp = gt.call(fn, fargs) + got = img.call(fn, fargs) + is_get = fn not in ("set64", "set32") + if not is_get: + if isinstance(got, str): + fails += 1 + print(f" [BUG] {step}: {got}") + continue + match = got == exp + if not match: + fails += 1 + print(f" [{'ok ' if match else 'BUG'}] {step}: {fn}{fargs} -> " + f"{got if isinstance(got, str) else hex(got)} (wasmtime {exp:#x})") + print(f"\nORACLE: {'PASS' if fails == 0 else f'FAIL ({fails} divergences)'}") + sys.exit(0 if fails == 0 else 1) + + +if __name__ == "__main__": + main()