Skip to main content

synth_core/
backend.rs

1//! Backend trait and registry for multi-backend compilation
2//!
3//! Every compiler backend (ARM, aWsm, wasker, w2c2) implements the `Backend`
4//! trait, allowing the CLI and verification framework to treat them uniformly.
5
6use crate::target::TargetSpec;
7use crate::wasm_decoder::DecodedModule;
8use crate::wasm_op::WasmOp;
9use crate::wsc_facts::WscFact;
10use std::collections::HashMap;
11use thiserror::Error;
12
13/// Errors from backend compilation
14#[derive(Debug, Error)]
15pub enum BackendError {
16    #[error("compilation failed: {0}")]
17    CompilationFailed(String),
18
19    #[error("backend not available: {0}")]
20    NotAvailable(String),
21
22    #[error("unsupported configuration: {0}")]
23    UnsupportedConfig(String),
24
25    #[error("external tool error: {0}")]
26    ExternalToolError(String),
27}
28
29/// Memory-bounds safety strategy. Phase 1 of `docs/binary-safety-design.md` §3.1.
30///
31/// - `Mpu`/PMP: rely on hardware (ARM MPU or RV32 PMP) — no inline check.
32/// - `Software`: emit a `CMP/BHS Trap_Handler` (ARM) or `bgeu addr, mem_size, ebreak` (RV32)
33///   before every load/store.
34/// - `Mask`: emit `AND addr, addr, #(mem_size - 1)` — only valid when memory size
35///   is a power of two. Wraps on OOB rather than trapping (fuzz-profile semantics).
36/// - `None`: no bounds enforcement.
37#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
38pub enum SafetyBounds {
39    /// No bounds check (caller assumes the WASM module is trusted)
40    #[default]
41    None,
42    /// ARM MPU / RV32 PMP — hardware enforcement, no inline guard
43    Mpu,
44    /// Software CMP/BHS (ARM) or BGEU+EBREAK (RV32) per access
45    Software,
46    /// AND-mask, requires power-of-two memory size
47    Mask,
48}
49
50impl SafetyBounds {
51    /// Parse the `--safety-bounds` argument value.
52    pub fn parse(s: &str) -> std::result::Result<Self, String> {
53        match s {
54            "none" => Ok(SafetyBounds::None),
55            "mpu" | "pmp" => Ok(SafetyBounds::Mpu),
56            "software" | "soft" => Ok(SafetyBounds::Software),
57            "mask" | "masking" => Ok(SafetyBounds::Mask),
58            other => Err(format!(
59                "unknown --safety-bounds value '{}'; expected one of: none, mpu, software, mask",
60                other
61            )),
62        }
63    }
64
65    /// String form used in the safety manifest.
66    pub fn as_str(self) -> &'static str {
67        match self {
68            SafetyBounds::None => "none",
69            SafetyBounds::Mpu => "mpu",
70            SafetyBounds::Software => "software",
71            SafetyBounds::Mask => "mask",
72        }
73    }
74}
75
76/// The absolute SRAM address the OPTIMIZED (non-relocatable) ARM path
77/// materializes as its linear-memory base (`MOVW/MOVT R12, #base` before each
78/// const-address access, and the #468 base-CSE R11 hoist). Historical value:
79/// 256 bytes above the SRAM start — the differential-harness contract for
80/// optimized-path fixtures maps linmem here. `CompileConfig::linmem_base`
81/// defaults to this; `--stack-layout=low` (#687) shifts it up by the reserved
82/// stack size so the moved layout reaches user code, not just the startup.
83pub const OPTIMIZED_LINMEM_BASE: u32 = 0x2000_0100;
84
85/// Configuration for a compilation run
86#[derive(Debug, Clone)]
87pub struct CompileConfig {
88    /// Optimization level (0 = none, 1 = fast, 2 = default, 3 = aggressive)
89    pub opt_level: u8,
90    /// Target specification
91    pub target: TargetSpec,
92    /// Legacy: enable software bounds checking for memory operations.
93    /// Deprecated in favor of `safety_bounds`. When set, equivalent to
94    /// `SafetyBounds::Software`. Kept for backwards compatibility with
95    /// callers that haven't migrated yet.
96    pub bounds_check: bool,
97    /// Phase-1 unified safety-bounds knob. If `bounds_check` is `true` and
98    /// this is `None`, the legacy field wins (back-compat). If both are set,
99    /// `safety_bounds` wins.
100    pub safety_bounds: SafetyBounds,
101    /// Hardware profile name (e.g. "nrf52840", "stm32f407")
102    pub hardware: String,
103    /// Skip optimization passes (direct instruction selection)
104    pub no_optimize: bool,
105    /// Use Loom-compatible optimization preset
106    pub loom_compat: bool,
107    /// Number of imported functions (calls to indices below this use Meld dispatch)
108    pub num_imports: u32,
109    /// AAPCS integer-argument count per function, indexed by full WASM function
110    /// index (imports first, then locals). Lets `Call` marshal the right number
111    /// of operand-stack values into R0–R3 (issue #195). Empty = pass no args
112    /// (pre-#195 behaviour).
113    pub func_arg_counts: Vec<u32>,
114    /// #851: result (return-value) count per function, indexed by full WASM
115    /// function index (imports first). `0` = void, `1` = one value. The AArch64
116    /// direct-`call` lowering needs the 0-vs-1 distinction to decide whether to
117    /// push the `x0` result — `func_ret_i64/f32/f64` carry the result TYPE but
118    /// conflate void and i32. Empty on backends/paths that do not lower calls
119    /// this way (byte-invisible there).
120    pub func_result_counts: Vec<u32>,
121    /// AAPCS integer-argument count per function type, indexed by type index.
122    /// Used by `call_indirect` (issue #195).
123    pub type_arg_counts: Vec<u32>,
124    /// Produce relocatable (ET_REL) host-link output. When set, the backend
125    /// uses the direct instruction selector (`select_with_stack`) rather than
126    /// the optimized path: the optimizer materializes an *absolute* linear-
127    /// memory base (0x20000100) and does not preserve caller-saved registers
128    /// across calls, both wrong for a host-linked object where the linmem base
129    /// is supplied via `fp` at runtime and callees follow AAPCS. Imports are
130    /// also emitted as direct `func_N` BLs (resolved to the wasm field name)
131    /// instead of `__meld_dispatch_import`. (#197 — follow-up to #188/#171.)
132    pub relocatable: bool,
133
134    /// #275: the SELF-CONTAINED Thumb-2 `--cortex-m` image path lowers
135    /// `call_indirect` through a flash-resident funcref table addressed
136    /// PC-RELATIVE (an `LdrSym` literal-pool pointer to
137    /// [`FUNC_TABLE_SYMBOL`]) — NEVER through R11, which is the linear-memory
138    /// base (the v0.42 #717 collision). Set by the CLI ONLY when the image
139    /// builder that emits and patches that table
140    /// (`build_multi_func_cortex_m_elf`) will run: Cortex-M family, not
141    /// `--relocatable`, no imported functions. Every other self-contained
142    /// configuration keeps the loud #275 decline. Default `false`.
143    pub self_contained_funcref_table: bool,
144
145    /// #687 (`--stack-layout=low`): the absolute linear-memory base the
146    /// OPTIMIZED ARM path materializes into user code. Defaults to
147    /// [`OPTIMIZED_LINMEM_BASE`] (`0x2000_0100`, byte-identical to every
148    /// pre-#687 compile). Under the low stack layout the CLI shifts it up by
149    /// the reserved stack size so const-address loads/stores land in the moved
150    /// linear memory instead of the stack region. Only the optimized
151    /// (non-relocatable) path consumes it — the direct selector is R11/fp
152    /// - relative and follows the startup's R11 init instead.
153    pub linmem_base: u32,
154
155    /// #237: emit wasm function-static data as a base-independent `.data`
156    /// section (`__synth_wasm_data`) addressed via MOVW/MOVT symbol relocations,
157    /// so a host-pointer drop-in (linmem base = 0 for native `*ptr` derefs)
158    /// doesn't mis-resolve the statics. Off by default — only the leaves'
159    /// base-relative `[R11+const]` path is used unless explicitly requested.
160    pub native_pointer_abi: bool,
161
162    /// #237: wasm linear-memory minimum size in bytes — the full static-data
163    /// extent (initialized `(data)` segments plus the zero-init/BSS region).
164    /// Under `native_pointer_abi`, a const memory address below this is a wasm
165    /// static → symbol-relative; any address beyond it is a runtime host pointer
166    /// → `[R11=0 + addr]`.
167    pub linear_memory_bytes: u32,
168
169    /// VCR-MEM-002 phase 1 (#406): initial size in 64 KiB pages of EACH linear
170    /// memory, indexed by memory index. Consulted only by the multi-memory
171    /// lowering arms (loads/stores wrapped in `WasmOp::MultiMemory`,
172    /// `memory.size`/`grow` with a non-zero index) — memory-0 lowering never
173    /// reads it, so single-memory output is byte-identical whether it is set
174    /// or empty. Empty (the default) means "no multi-memory context": any
175    /// multi-memory op then declines loudly.
176    pub memory_pages: Vec<u32>,
177
178    /// #237: the wasm stack-pointer global as `(index, init_value)`, if the
179    /// module has one. Under `native_pointer_abi` the backend register-promotes
180    /// it: `global.get` materializes `__synth_wasm_data + init` (the real stack
181    /// top) and the init value doubles as the static-data base that separates
182    /// pointer consts (`>= init`) from frame-size scalars (`< init`).
183    pub stack_pointer_global: Option<(u32, i32)>,
184    /// #311: per-function (full index) / per-type "returns i64" — the call
185    /// lowering must tag i64 results as a register pair or the hi half is
186    /// invisible to liveness.
187    pub func_ret_i64: Vec<bool>,
188    pub type_ret_i64: Vec<bool>,
189    /// #643: byte width of each defined global's storage slot, indexed by
190    /// global index — 4 for i32/f32, 8 for i64/f64, 16 for v128 (from the
191    /// module's global section). The globals table is laid out by SUMMING
192    /// these widths: an i64 global needs a register-PAIR store/load at
193    /// `[R9, off]`/`[R9, off+4]`, and every later global's offset shifts.
194    /// Empty ⇒ every global assumed 4 bytes (the legacy `idx * 4` layout;
195    /// hand-built op streams and i32-only modules are byte-identical).
196    pub global_widths: Vec<u32>,
197    /// #359: declared parameter widths per *function* (full index, imports
198    /// first): `func_params_i64[f][k]` is true when param `k` of function `f` is
199    /// i64/f64. The AAPCS stack-argument path needs the *declared* widths
200    /// (op-stream inference can't see an unused i64 param that still shifts the
201    /// incoming-stack layout). The source of truth — a per-function driver loop
202    /// (`compile_module` / the CLI loop) indexes it by `func.index` and copies
203    /// the slice into [`current_func_params_i64`] before each `compile_function`.
204    /// Empty → every param assumed i32 (the legacy path; keeps every function
205    /// with <=4 params, or all-i32 params, byte-identical).
206    pub func_params_i64: Vec<Vec<bool>>,
207    /// #359: declared parameter widths of the function CURRENTLY being compiled
208    /// — `current_func_params_i64[k]` is true when param `k` is i64/f64. Set per
209    /// function (a cheap clone of the config) from [`func_params_i64`] by the
210    /// driver loop, because `compile_function` is shared across backends and
211    /// carries no function index. Empty → assume i32.
212    pub current_func_params_i64: Vec<bool>,
213    /// GI-FPU-002 (#619/#369): per-function declared f32-param mask (full index,
214    /// imports first). The driver copies `func_params_f32[f]` into
215    /// [`current_func_params_f32`] before each `compile_function`. Empty ⇒
216    /// all-non-f32 (byte-identical to before).
217    pub func_params_f32: Vec<Vec<bool>>,
218    /// GI-FPU-002: declared f32-param mask of the function CURRENTLY being
219    /// compiled — `current_func_params_f32[k]` is true when param `k` is f32.
220    /// Set per function from [`func_params_f32`], mirroring
221    /// [`current_func_params_i64`]. Empty ⇒ no f32 params.
222    pub current_func_params_f32: Vec<bool>,
223    /// GI-FPU-002 phase 2 (#369): per-function declared f64-param mask (full
224    /// index, imports first) and the CURRENT function's slice. Hard-float
225    /// targets decline f64-param functions loudly — the legacy width
226    /// inference treats an f64 param as an i64 CORE-register pair, which
227    /// reads the wrong registers under AAPCS-VFP (the caller put it in a
228    /// D-register). Empty ⇒ no f64 params (byte-identical legacy path).
229    pub func_params_f64: Vec<Vec<bool>>,
230    /// See [`func_params_f64`](Self::func_params_f64).
231    pub current_func_params_f64: Vec<bool>,
232    /// GI-FPU-002 phase 2 (#719/#369): whether the function CURRENTLY being
233    /// compiled returns f32. Set per function from the decoder's `func_ret_f32`.
234    /// The direct selector's epilogue uses it to loudly decline a result that
235    /// reaches the return in a core register instead of an S-register (a call
236    /// that returned f32 as integer-tagged R0 would otherwise be a silent
237    /// miscompile — the AAPCS-VFP caller reads S0). `false` for hand-built op
238    /// streams / non-f32 returns (byte-identical to before).
239    pub current_func_ret_f32: bool,
240    /// GI-FPU-002 phase 2 (#719/#369): whether the function CURRENTLY being
241    /// compiled returns f64 (D0 under AAPCS-VFP). Same epilogue-soundness role.
242    pub current_func_ret_f64: bool,
243    /// GI-FPU-002 phase 2 (#719/#369): per-function (full index, imports first)
244    /// "returns f32/f64" tables. The direct selector declines a `call` to an
245    /// f32/f64-returning callee LOUDLY at the call site — the result arrives in
246    /// S0/D0 (AAPCS-VFP), which this increment does not marshal into the operand
247    /// stack; tagging it as an integer R0 would be a silent miscompile. Also the
248    /// source for [`current_func_ret_f32`]/[`current_func_ret_f64`] in the
249    /// per-function driver loops. Empty ⇒ callees assumed non-float-returning
250    /// (hand-built op streams; byte-identical legacy behaviour).
251    pub func_ret_f32: Vec<bool>,
252    /// See [`func_ret_f32`](Self::func_ret_f32).
253    pub func_ret_f64: Vec<bool>,
254    /// GI-FPU-002 phase 2 (#719/#369): per-type "returns f32/f64" — the
255    /// `call_indirect` analogue of [`func_ret_f32`](Self::func_ret_f32).
256    pub type_ret_f32: Vec<bool>,
257    /// See [`type_ret_f32`](Self::type_ret_f32).
258    pub type_ret_f64: Vec<bool>,
259    /// #457: DECLARED parameter count of the function CURRENTLY being compiled,
260    /// from the module's type section (`func_arg_counts[func.index]`). Set per
261    /// function by the driver loops like [`current_func_params_i64`].
262    ///
263    /// The backends otherwise INFER the param count from local-access patterns
264    /// (`count_params`: a local whose first access is a read is assumed to be a
265    /// param) — which cannot distinguish a param from a read-before-write
266    /// non-param local. WASM zero-initializes non-param locals, so such a local
267    /// must read 0; the inference instead homed it in a parameter register and
268    /// read caller garbage (#457).
269    ///
270    /// When this is `Some(declared)`, every backend uses
271    /// `min(`[`referenced_locals`](crate::referenced_locals)`(ops), declared)`
272    /// — the highest index the body touches, clamped by the signature. That is
273    /// EXACT in both directions: a genuine non-param local can never be
274    /// mistaken for a param (the clamp), and a param can never be demoted to a
275    /// local (the max over ALL accesses, reads and writes alike). The earlier
276    /// rule capped the READ-FIRST inference instead, which demoted a
277    /// conditionally-written param and produced an uninitialised-frame-slot
278    /// read on ARM and RISC-V and a zero-init local on AArch64 (#970/#851).
279    ///
280    /// `None` → declared signature unknown (hand-built op streams, direct
281    /// `compile_function` callers) → pure inference, the legacy behaviour.
282    /// HONEST RESIDUAL (#970, unchanged from #851): on that path a write-first
283    /// index is genuinely AMBIGUOUS — a param whose incoming value is dead, or
284    /// a non-param local — and both readings can be wrong. The read-first rule
285    /// keeps the #457 behaviour rather than reading caller garbage for a
286    /// zero-init local. The CLI always supplies a declared count.
287    pub current_func_param_count: Option<u32>,
288    /// (#778 phase 4 / #49) The WASM index of the function CURRENTLY being compiled,
289    /// so the WCET pass can identify this function's OWN `func_<idx>` self-call label
290    /// (a self-recursive `BL func_N` where N == this index) and prove/decline the
291    /// self-recursion depth. Set per function by the driver loop (like
292    /// [`current_func_params_i64`]). `None` → unknown (hand-built op streams, direct
293    /// `compile_function` callers) → no self-recursion certificate is attempted.
294    pub current_func_index: Option<u32>,
295    /// #509: blocktype-arity side-table of the function CURRENTLY being compiled
296    /// — `(param_count, result_count)` of the k-th `Block`/`Loop`/`If` in its op
297    /// stream (ordinal-keyed; see [`FunctionOps::block_arity`]). Set per function
298    /// by the driver loop (like [`current_func_params_i64`]). The direct selector
299    /// uses it to land a value carried by `br`/`br_if`/`br_table` in the target
300    /// block's designated result register instead of dropping it. Empty → every
301    /// block treated as void (the legacy lowering; hand-built op streams).
302    ///
303    /// [`FunctionOps::block_arity`]: crate::wasm_decoder::FunctionOps::block_arity
304    pub current_func_block_arity: Vec<(u8, u8)>,
305
306    /// #543 Phase 1 — integrator-marked volatile linear-memory segments (the DMA
307    /// transfer window). Each range `[base, base+len)` names a region of the fused
308    /// linear memory that an EXTERNAL agent (the DMA engine, modelled by gale as a
309    /// Component-Model `own<buffer>` handoff — gale decision `DD-DMA-REGION-001`,
310    /// gale#124) rewrites out-of-band. Loads and stores whose address falls inside
311    /// a marked range must eventually be treated as VOLATILE: not cached, hoisted,
312    /// or reordered across the transfer boundary.
313    ///
314    /// PHASE-2 CONTRACT (implemented — issue #543): the optimizer's
315    /// address-caching passes HONOR these ranges. Consumption points:
316    ///  - the #468 base-CSE / const-address-fold
317    ///    (`optimizer_bridge::plan_base_cse`, DEFAULT-ON, opt-out
318    ///    `SYNTH_BASE_CSE=0`): a const-address access whose 4-byte window
319    ///    intersects a marked range is EXCLUDED from the fold set — it keeps
320    ///    its verbatim per-access materialize-and-access codegen, while
321    ///    accesses outside the range still fold;
322    ///  - const-CSE (`liveness::apply_const_cse` wired in `arm_backend.rs`,
323    ///    DEFAULT-ON, opt-out `SYNTH_CONST_CSE=0`; the former bridge-level
324    ///    inline cache is retired, #242): declines WHOLESALE while any range is
325    ///    marked — a cached constant cannot be classified address-vs-data at
326    ///    that level, so the conservative stance for statically-unknown
327    ///    addressing is to re-materialize every constant at each occurrence.
328    ///
329    /// Passes that only touch SP-relative frame slots (stack-reload forwarding,
330    /// frame-slot DCE, spill re-choice) are unaffected by design: these ranges
331    /// are LINEAR-MEMORY addresses, and frame slots are never linmem. Nothing on
332    /// the pipeline deletes, forwards, or reorders a linear-memory access (IR CSE
333    /// deliberately never CSEs `MemLoad`s; DCE removes only unreachable blocks),
334    /// so every marked access is issued verbatim, in program order.
335    ///
336    /// Empty (the default): zero behavior change by construction — every gate
337    /// reduces to the pre-#543 path, so the emitted `.text` is byte-identical
338    /// with or without this code (the frozen-codegen gate holds). See rivet
339    /// `VCR-DMA-001`.
340    pub volatile_segments: Vec<VolatileRange>,
341
342    /// #778 phase 2 — the parsed `--wcet-hints` file (UNTRUSTED per-function
343    /// loop-bound hints, the scry seam). Consulted ONLY by the WCET sidecar
344    /// computation over the final instruction stream; NEVER by codegen — the
345    /// emitted bytes are byte-identical with or without hints. Every hint is
346    /// soundly verified before use and rejected with a machine reason
347    /// otherwise.
348    pub wcet_hints: Option<crate::wcet::WcetHints>,
349
350    /// VCR-PERF-002 Phase 1 (#494) — proven invariants forwarded by loom in
351    /// the `wsc.facts` custom section (encoding:
352    /// `docs/design/wsc-facts-encoding.md`; program:
353    /// `docs/design/proof-carrying-specialization.md`), whole-module table
354    /// keyed by `(func_index, value_id)`. The compile driver copies the
355    /// current function's slice into [`current_func_facts`] (the
356    /// `func_params_i64` → `current_func_params_i64` pattern), because
357    /// `compile_function` carries no function index.
358    ///
359    /// PHASE-1 CONTRACT: threaded but NOT consumed — no codegen path reads
360    /// facts, so emitted bytes are unchanged whether or not the module
361    /// carries the section (locked by `wsc_facts_ingestion_494.rs`). Phase 2
362    /// turns each fact into a premise for a flag-gated (`SYNTH_FACT_SPEC`),
363    /// per-elision ordeal-validated specialization; the facts-absent compile
364    /// stays byte-identical by construction (empty ⇒ every gate vacuous).
365    ///
366    /// [`current_func_facts`]: CompileConfig::current_func_facts
367    pub wsc_facts: Vec<WscFact>,
368    /// VCR-PERF-002 Phase 1 (#494): the `wsc.facts` invariants of the function
369    /// CURRENTLY being compiled (`fact.func_index == func.index`), set per
370    /// function by the driver loops like [`current_func_params_i64`]. This is
371    /// the field a Phase-2 selector pass will read its premises from. Empty →
372    /// no facts → no specialization may ever fire (the fail-safe default).
373    ///
374    /// [`current_func_params_i64`]: CompileConfig::current_func_params_i64
375    pub current_func_facts: Vec<WscFact>,
376    /// VCR-PERF-002 Phase 2b (#494, divisor-nonzero): op indices (into the op
377    /// stream passed to `compile_function`) of `div`/`rem` ops whose
378    /// DIVIDE-BY-ZERO trap guard is proven dead — the fact-spec pass
379    /// discharged `UNSAT(P ∧ divisor == 0)` per site through the
380    /// certificate-checked ordeal solver BEFORE the driver set this field.
381    /// Consumed by the ARM direct selector (`select_with_stack`); every other
382    /// path ignores it (guards stay — sound). Empty (the default) ⇒ every
383    /// guard is emitted, byte-identical to today.
384    pub fact_div_zero_elide: Vec<usize>,
385    /// VCR-PERF-002 Phase 2b (#494): op indices of `div_s` ops whose
386    /// `INT_MIN / -1` OVERFLOW trap guard is proven dead — a SEPARATE
387    /// obligation (`UNSAT(P ∧ dividend == INT_MIN ∧ divisor == -1)`). A
388    /// divisor-nonzero fact alone NEVER lands here: divisor ≠ 0 does not
389    /// exclude -1 (#633/#634 two-guard distinction). Empty ⇒ guard emitted.
390    pub fact_div_ovf_elide: Vec<usize>,
391    /// #494 bounds-elision (#390 `guard_bool`): op indices of i32 memory
392    /// accesses whose `--safety-bounds software` inline guard is proven dead
393    /// — the fact-spec pass discharged
394    /// `UNSAT(P ∧ trap_mem_oob(zext64(index) + offset, size,
395    /// min_memory_bytes))` per site through the certificate-checked ordeal
396    /// solver BEFORE the driver set this field (ordeal 0.9.1 `trap_mem_oob`
397    /// shape, wraparound-safe 64-bit extension). Consumed by the ARM direct
398    /// selector (`select_with_stack`); every other path ignores it (guards
399    /// stay — sound). Empty (the default) ⇒ every guard is emitted,
400    /// byte-identical to today.
401    pub fact_mem_bounds_elide: Vec<usize>,
402    /// VCR-MEM-004 (#901): op indices of linear-memory accesses whose
403    /// `--safety-bounds software` inline guard is elided on an EXTERNAL proof
404    /// — scry's sound abstract interpretation proved the access in-bounds
405    /// against the memory's guaranteed minimum size, and the verdict file
406    /// cleared every fail-closed gate ([`crate::proven_safe::ingest`]:
407    /// `module_sha256` bound to the exact bytes being compiled,
408    /// `memory_min_bytes` equal to this module's declared floor, and each
409    /// entry's `(func, pc)` key validated against the decoded operator at
410    /// that index).
411    ///
412    /// Kept SEPARATE from [`CompileConfig::fact_mem_bounds_elide`] on purpose:
413    /// the two strip the same guard at the same consumption point, but on
414    /// different AUTHORITIES (a per-site ordeal certificate vs a whole-module
415    /// external AI), and the `synth-proven-safe-elisions-v1` attestation
416    /// records which one covered each site. The ARM backend unions them.
417    /// Empty (the default) ⇒ every guard is emitted, byte-identical to today.
418    pub proven_safe_mem_elide: Vec<usize>,
419    /// #642: `call_indirect` guard inputs — the compile-time table size for
420    /// the runtime bounds check and the per-expected-type closed-world type
421    /// verdicts — computed from the decoded module by
422    /// [`crate::wasm_decoder::DecodedModule::call_indirect_guards`] and set by
423    /// the driver loops. The default (`table_size: None`, empty verdicts)
424    /// DECLINES every `call_indirect` lowering: an unchecked indirect branch
425    /// is never emitted (WASM Core §4.4.8 requires OOB/type-mismatch traps).
426    pub call_indirect_guards: crate::wasm_decoder::CallIndirectGuards,
427    /// #851 lane L3: result count per FUNCTION TYPE (see
428    /// [`crate::wasm_decoder::DecodedModule::type_result_counts`]). The aarch64
429    /// `call_indirect` lowering needs the 0-vs-1 result distinction for a callee
430    /// it knows only by its static type.
431    pub type_result_counts: Vec<u32>,
432    /// #851 lane L3: the STRUCTURAL signature class id per function type (see
433    /// [`crate::wasm_decoder::DecodedModule::structural_type_class_ids`]). The
434    /// aarch64 `call_indirect` type check compares this, not the raw type index
435    /// — WASM type equality is structural. Distinct from
436    /// `call_indirect_guards.type_class_ids`, which the ARM path populates only
437    /// when its heterogeneous-table sidecar exists.
438    pub type_class_ids: Vec<u32>,
439    /// #851 lane L3, aarch64 only — the driver has EMITTED the module-level
440    /// substrate the globals and `call_indirect` lowerings address: the `.data`
441    /// globals image (`__synth_globals`) and the `.text` funcref table
442    /// (`__synth_func_table`), both produced by
443    /// `synth_backend_aarch64::substrate::plan`.
444    ///
445    /// FAIL-SAFE BY DEFAULT (`false`): the aarch64 selector LOUD-DECLINES
446    /// `global.get`/`global.set`/`call_indirect` unless this is set, so a driver
447    /// that compiles function bodies but never emits the regions cannot ship
448    /// code addressing a symbol that does not exist. Set only on the two paths
449    /// that call `plan()` and place its output in the object.
450    pub a64_substrate_emitted: bool,
451    /// RQ-63-RVGLOBAL (#242): how many globals the module IMPORTS. The op
452    /// stream's `global.get`/`global.set` index space is imports-FIRST, while
453    /// [`CompileConfig::global_widths`] / [`CompileConfig::global_mutable`]
454    /// are indexed by DEFINED global (the decoder's `WasmGlobal::index`), so a
455    /// backend maps an op index `i` to defined global `i - num_imported_globals`
456    /// and must decline `i < num_imported_globals` (an imported global's value
457    /// arrives at instantiation, which a synth-emitted region cannot bind).
458    pub num_imported_globals: u32,
459    /// RQ-63-RVGLOBAL (#242): per DEFINED global, its declared mutability.
460    /// Indexed like [`CompileConfig::global_widths`]. A validated module never
461    /// `global.set`s an immutable global, but the RV32 lowering declines it
462    /// anyway rather than write through a `const` — defence in depth, since
463    /// the decoder does not run the wasm validator. Empty ⇒ every global is
464    /// treated as mutable (hand-built op streams).
465    pub global_mutable: Vec<bool>,
466    /// RQ-63-RVGLOBAL (#242): whether the driver WILL place the RV32 globals
467    /// region (`__synth_globals`, a synth-emitted `.data` image carrying every
468    /// defined global's decoded initializer — `synth_backend_riscv::globals`)
469    /// in the object it assembles. FAIL-SAFE BY DEFAULT (`false`): the RV32
470    /// selector LOUD-DECLINES `global.get`/`global.set` unless this is set,
471    /// so a driver that compiles function bodies but never emits the region
472    /// cannot ship code relocating against a symbol nothing defines (the
473    /// #1102 dangling-reference class). The aarch64 `a64_substrate_emitted`
474    /// contract, ported.
475    pub rv32_globals_emitted: bool,
476}
477
478/// #543 — an integrator-marked volatile linear-memory segment (the DMA transfer
479/// window): the half-open byte range `[base, base + len)` of the fused linear
480/// memory that an external agent rewrites out-of-band. Parsed from the CLI
481/// `--volatile-segment <base>:<len>` flag. See [`CompileConfig::volatile_segments`]
482/// for the Phase-1/Phase-2 split.
483#[derive(Debug, Clone, Copy, PartialEq, Eq)]
484pub struct VolatileRange {
485    /// Start address of the volatile region, in linear-memory bytes.
486    pub base: u32,
487    /// Length of the volatile region, in bytes. The region is `[base, base+len)`.
488    pub len: u32,
489}
490
491impl CompileConfig {
492    /// Resolve the effective safety-bounds setting, honouring the legacy
493    /// `bounds_check` field as a fallback. Used by backends to pick the
494    /// inline-check shape.
495    pub fn effective_safety_bounds(&self) -> SafetyBounds {
496        match (self.safety_bounds, self.bounds_check) {
497            (SafetyBounds::None, true) => SafetyBounds::Software,
498            (s, _) => s,
499        }
500    }
501}
502
503impl Default for CompileConfig {
504    fn default() -> Self {
505        Self {
506            opt_level: 2,
507            target: TargetSpec::cortex_m4(),
508            bounds_check: false,
509            safety_bounds: SafetyBounds::None,
510            hardware: String::new(),
511            no_optimize: false,
512            loom_compat: false,
513            num_imports: 0,
514            func_arg_counts: Vec::new(),
515            func_result_counts: Vec::new(),
516            type_arg_counts: Vec::new(),
517            relocatable: false,
518            // #275: self-contained funcref-table dispatch is opt-in by the
519            // CLI's cortex-m image path; everything else keeps the decline.
520            self_contained_funcref_table: false,
521            // #687: the historical optimized-path absolute base — every
522            // default compile stays byte-identical.
523            linmem_base: OPTIMIZED_LINMEM_BASE,
524            native_pointer_abi: false,
525            linear_memory_bytes: 0,
526            // #406: empty ⇒ no multi-memory context ⇒ multi-memory ops decline
527            // loudly; memory-0 lowering never reads it.
528            memory_pages: Vec::new(),
529            stack_pointer_global: None,
530            func_ret_i64: Vec::new(),
531            type_ret_i64: Vec::new(),
532            // #643: empty ⇒ legacy all-4-byte global slots (i32-only modules).
533            global_widths: Vec::new(),
534            func_params_i64: Vec::new(),
535            current_func_params_i64: Vec::new(),
536            func_params_f32: Vec::new(),
537            current_func_params_f32: Vec::new(),
538            // GI-FPU-002 phase 2 (#719/#369): false ⇒ non-float return (or a
539            // hand-built op stream); driver loops set it per function.
540            current_func_ret_f32: false,
541            current_func_ret_f64: false,
542            // GI-FPU-002 phase 2 (#719/#369): empty ⇒ callees assumed
543            // non-float-returning (hand-built op streams).
544            func_params_f64: Vec::new(),
545            current_func_params_f64: Vec::new(),
546            func_ret_f32: Vec::new(),
547            func_ret_f64: Vec::new(),
548            type_ret_f32: Vec::new(),
549            type_ret_f64: Vec::new(),
550            // #457: None ⇒ declared signature unknown ⇒ param-count inference
551            // only (unit tests / hand-built op streams); driver loops fill it.
552            current_func_param_count: None,
553            current_func_index: None,
554            // #509: empty ⇒ legacy void-block lowering (unit tests / hand-built
555            // op streams); the driver loops fill it per function.
556            current_func_block_arity: Vec::new(),
557            // #543 Phase 1: no volatile segments unless the CLI flag names them.
558            // Empty ⇒ inert ⇒ emitted bytes unchanged.
559            volatile_segments: Vec::new(),
560            // VCR-PERF-002 Phase 1 (#494): no facts unless the module carries
561            // a parseable `wsc.facts` section. Empty ⇒ inert (and Phase 1 has
562            // no consumer anyway) ⇒ emitted bytes unchanged.
563            wsc_facts: Vec::new(),
564            current_func_facts: Vec::new(),
565            // VCR-PERF-002 Phase 2b (#494): no guard-elision marks unless the
566            // fact-spec pass discharged the per-site obligations. Empty ⇒
567            // every div/rem trap guard is emitted, byte-identical.
568            fact_div_zero_elide: Vec::new(),
569            fact_div_ovf_elide: Vec::new(),
570            fact_mem_bounds_elide: Vec::new(),
571            proven_safe_mem_elide: Vec::new(),
572            // #642: no guard inputs ⇒ every call_indirect lowering declines
573            // loudly (never an unchecked indirect branch). Driver loops fill
574            // this from the decoded module.
575            call_indirect_guards: crate::wasm_decoder::CallIndirectGuards::default(),
576            type_result_counts: Vec::new(),
577            type_class_ids: Vec::new(),
578            a64_substrate_emitted: false,
579            // RQ-63-RVGLOBAL: no imports, every global mutable, and — fail-safe
580            // — NO globals region placed, so the RV32 selector declines.
581            num_imported_globals: 0,
582            global_mutable: Vec::new(),
583            rv32_globals_emitted: false,
584            // #778 phase 2: no --wcet-hints file ⇒ no hints. Consulted ONLY by
585            // the WCET sidecar computation — never by codegen (the emitted
586            // bytes are byte-identical with or without hints).
587            wcet_hints: None,
588        }
589    }
590}
591
592/// #275: the base symbol of the SELF-CONTAINED funcref table — the
593/// flash-resident region `build_multi_func_cortex_m_elf` appends after the
594/// function code: one 4-byte code pointer per table slot across ALL tables in
595/// declaration order (the same contiguous layout the `--relocatable` R11
596/// contract uses — `TableGuards::base_byte_offset` stays valid verbatim),
597/// null slots as ZERO words (#664), followed by the #676 type-id sidecar at
598/// `type_ids_byte_offset` when a heterogeneous table needs it. The dispatch
599/// reaches it through an `LdrSym` literal-pool word (an `Abs32` reloc against
600/// this symbol) that the image builder patches post-layout — never through
601/// R11, which is the linear-memory base (the #717 collision).
602pub const FUNC_TABLE_SYMBOL: &str = "__synth_func_table";
603
604/// A relocation entry produced during compilation
605///
606/// Records that a BL instruction at `offset` bytes into the function's code
607/// targets an external symbol (e.g., `__meld_dispatch_import`). The linker
608/// resolves these when combining the Synth object with the Kiln bridge.
609#[derive(Debug, Clone, Copy, PartialEq, Eq)]
610pub enum RelocKind {
611    /// R_ARM_THM_CALL (ELF type 10) — a THUMB BL call site (#167). Correct
612    /// only for a Thumb-state `bl`, whose 32-bit placeholder is `f7ff fffe`
613    /// (branch-to-self, addend -4 for the +4 pipeline bias).
614    ThmCall,
615    /// R_ARM_CALL (ELF type 28) — an ARM-STATE (A32) BL call site (#1040).
616    /// The A32 analogue of [`RelocKind::ThmCall`], exactly as
617    /// [`RelocKind::AArch64Call26`] and [`RelocKind::RiscvCallPlt`] are the
618    /// analogues for their ISAs — the ISA is fixed at the site that KNOWS it,
619    /// never re-derived at the ELF emitter where the information is gone.
620    ///
621    /// Emitting `ThmCall` for an A32 `bl` was #1040: a consumer that trusts
622    /// the declared type patches Thumb halfwords into an ARM-state word (or
623    /// emits an interwork veneer), producing an invalid instruction. The
624    /// matching A32 placeholder is `ebfffffe` (branch-to-self, addend -8 for
625    /// the +8 pipeline bias) — `gas` emits exactly that for `bl <extern>` in
626    /// ARM mode, and `eb000000` (addend 0) lands two instructions past the
627    /// callee entry, the A32 twin of #174.
628    ArmCall,
629    /// R_ARM_MOVW_ABS_NC — the MOVW half of a symbol-relative address (#237).
630    MovwAbs,
631    /// R_ARM_MOVT_ABS — the MOVT half of a symbol-relative address (#237).
632    MovtAbs,
633    /// R_ARM_ABS32 — a 32-bit absolute address held in a `.text` literal-pool
634    /// word, loaded via `LDR rX, [pc, #off]` (#345). The link-survivable
635    /// replacement for the inline-immediate MOVW/MOVT-ABS pair: `ld`/bfd patches
636    /// the data word at link time (`S + A`, the addend living in the word, REL
637    /// semantics), which survives placement into a large multi-object image —
638    /// whereas an inline-instruction MOVW_ABS immediate can be mangled.
639    Abs32,
640    /// R_AARCH64_CALL26 (ELF type 283) — an AArch64 `BL` call site (#851). The
641    /// AArch64 analogue of [`RelocKind::ThmCall`]: the linker patches the 26-bit
642    /// word-offset immediate of the `bl` at `offset` to reach the target symbol.
643    /// Emitted only by the `EM_AARCH64` backend's `.rela.text`.
644    AArch64Call26,
645    /// R_AARCH64_JUMP26 (ELF type 282) — an AArch64 `B` (tail-branch) site
646    /// (#851 lane L3). Same 26-bit word-offset immediate as
647    /// [`RelocKind::AArch64Call26`], but for a branch that does NOT set `x30`:
648    /// the aarch64 `call_indirect` funcref table is a `.text`-resident array of
649    /// `b func_N` trampolines, so the dispatch's `blr` sets the return address
650    /// and the trampoline tail-branches into the callee (which returns straight
651    /// to the dispatcher).
652    AArch64Jump26,
653    /// R_AARCH64_ADR_PREL_PG_HI21 (ELF type 275) — the `adrp` half of a
654    /// PC-relative symbol address (#851 lane L3). Patches the 21-bit page delta
655    /// (`immlo`[30:29] + `immhi`[23:5]) so `adrp xd, sym` reaches the 4 KiB page
656    /// containing `sym`. Always paired with an
657    /// [`RelocKind::AArch64AddAbsLo12Nc`] on the next instruction. This pair is
658    /// how aarch64 reaches a synth-EMITTED region (the globals `.data` image,
659    /// the funcref table) with NO dedicated base register — so neither feature
660    /// adds an embedder precondition alongside `x28`.
661    AArch64AdrPrelPgHi21,
662    /// R_AARCH64_ADD_ABS_LO12_NC (ELF type 277) — the `add xd, xd, :lo12:sym`
663    /// half of a PC-relative symbol address (#851 lane L3). Patches the 12-bit
664    /// immediate field [21:10] with `(S + A) & 0xFFF`.
665    AArch64AddAbsLo12Nc,
666    /// R_RISCV_CALL_PLT (ELF type 19) — a RISC-V `auipc`+`jalr` call pair
667    /// (#871). The RV32 analogue of [`RelocKind::ThmCall`]: `offset` points at
668    /// the `auipc` of an 8-byte `auipc ra, 0 ; jalr ra, 0(ra)` placeholder and
669    /// the linker patches BOTH instructions' immediates to reach the target
670    /// symbol (the modern form; `R_RISCV_CALL` is deprecated). Emitted only by
671    /// the `EM_RISCV` backend's `.rela.text`.
672    RiscvCallPlt,
673    /// R_RISCV_HI20 (ELF type 26) — the `lui` half of an ABSOLUTE symbol
674    /// address (RQ-63-RVGLOBAL, #242). `offset` points at a `lui rd, 0`
675    /// placeholder whose 20-bit immediate the linker patches to
676    /// `((S + A) + 0x800) >> 12`. Always paired with an
677    /// [`RelocKind::RiscvLo12I`] on the next instruction. This pair is how
678    /// RV32 reaches a synth-EMITTED region (the globals `.data` image,
679    /// `__synth_globals`) with NO dedicated base register — the RV32 twin of
680    /// the aarch64 `adrp`+`add :lo12:` pair, so globals add no embedder
681    /// precondition beside `s11`. Absolute rather than PC-relative because the
682    /// RV32 object is always statically host-linked into a fixed-address
683    /// bare-metal image (the `medlow` code model), which needs no per-site
684    /// local symbol.
685    RiscvHi20,
686    /// R_RISCV_LO12_I (ELF type 27) — the `addi rd, rd, 0` half of an absolute
687    /// symbol address (RQ-63-RVGLOBAL). The linker patches the 12-bit I-type
688    /// immediate with the low bits of `S + A`.
689    RiscvLo12I,
690}
691
692#[derive(Debug, Clone, PartialEq, Eq)]
693pub struct CodeRelocation {
694    /// Byte offset within the function's machine code where the reloc applies
695    pub offset: u32,
696    /// Target symbol name (e.g., "__meld_dispatch_import", "__synth_wasm_data")
697    pub symbol: String,
698    /// Which ARM relocation type to emit for this site.
699    pub kind: RelocKind,
700}
701
702/// Symbol BINDING — whether a symbol takes part in cross-object resolution
703/// (#656 ARM, #1180 / RQ-65-FUNCN aarch64).
704///
705/// This is a CONTAINER-INDEPENDENT concept, which is why it lives here and
706/// not in a writer: ELF spells it `STB_LOCAL` / `STB_GLOBAL` / `STB_WEAK` in
707/// `st_info`'s high nibble (the discriminants below are exactly those
708/// values), Mach-O spells `Local` as `N_EXT` CLEAR and `Global` as `N_EXT`
709/// SET on the `nlist_64`. The decision that a synth-invented name — a
710/// `func_N` call label, `__synth_globals`, `__synth_func_table` — is
711/// `Local` while a wasm export or import is `Global` is made ONCE, at the
712/// object PLAN, and every container reads it from there. Two independently
713/// compiled synth objects both define `func_1`; a `Global` binding made
714/// linking them into one program a `duplicate symbol` refusal, in every
715/// container (measured on ELF `ld.lld` and Mach-O Apple `ld`, #1180).
716#[derive(Debug, Clone, Copy, PartialEq, Eq)]
717pub enum SymbolBinding {
718    /// File-local: resolves relocations within its own object (they bind by
719    /// symbol INDEX, not by name) and is invisible to every other object.
720    Local = 0,
721    /// Visible to the link: the name an embedder calls, or the import it
722    /// defines.
723    Global = 1,
724    /// Weak (ELF `STB_WEAK`); no synth writer emits it today.
725    Weak = 2,
726}
727
728/// The locals-first symbol order, computed ONCE for every container that
729/// needs it (#656, #1180).
730///
731/// ELF requires every `STB_LOCAL` symbol to precede every non-local one in
732/// `.symtab`, with the section's `sh_info` = index of the first non-local.
733/// Mach-O's `LC_DYSYMTAB` requires the same partition (locals, then external
734/// defined, then undefined). The ARM ELF32 builder (`synth-backend`,
735/// `ElfBuilder::build`) and the aarch64 object plan (`synth-backend-aarch64`,
736/// `plan_object`) both apply THIS permutation, so the rule is written once —
737/// a second hand-written copy in a second writer is the mirror the North
738/// Star forbids, and the way the two backends diverged in the first place.
739///
740/// The permutation is a STABLE sort on `binding != Local`: with zero locals
741/// it is the identity, which is what keeps every pre-#656 / pre-#1180 object
742/// byte-identical.
743#[derive(Debug, Clone, PartialEq, Eq)]
744pub struct LocalsFirst {
745    /// `order[new] = old`: the symbol emitted at position `new` is the caller's
746    /// symbol `old`.
747    pub order: Vec<usize>,
748    /// `old_to_new[old] = new`: where the caller's symbol `old` landed. Every
749    /// relocation that names a symbol by index is rewritten through this.
750    pub old_to_new: Vec<usize>,
751    /// The number of `Local` symbols — the length of the local prefix. ELF's
752    /// `sh_info` is `local_count + 1` (the null symbol at index 0 counts as
753    /// local); Mach-O's `nlocalsym` is `local_count`.
754    pub local_count: usize,
755}
756
757/// Compute the [`LocalsFirst`] permutation for `bindings` (in the caller's
758/// current order).
759pub fn locals_first(bindings: impl IntoIterator<Item = SymbolBinding>) -> LocalsFirst {
760    let bindings: Vec<SymbolBinding> = bindings.into_iter().collect();
761    let mut order: Vec<usize> = (0..bindings.len()).collect();
762    // Stable: locals keep their relative order, and so do non-locals.
763    order.sort_by_key(|&i| bindings[i] != SymbolBinding::Local);
764    let mut old_to_new = vec![0usize; bindings.len()];
765    for (new, &old) in order.iter().enumerate() {
766        old_to_new[old] = new;
767    }
768    let local_count = bindings
769        .iter()
770        .filter(|b| **b == SymbolBinding::Local)
771        .count();
772    LocalsFirst {
773        order,
774        old_to_new,
775        local_count,
776    }
777}
778
779/// VCR-DBG-001: a per-instruction source map — `(machine_offset_within_code,
780/// wasm_op_index)` pairs, one per emitted machine instruction. A `None` op-index
781/// marks an instruction with no originating wasm op (prologue/epilogue, literal
782/// pool). Consumed by the DWARF `.debug_line` emitter; empty when no source map
783/// was produced.
784pub type LineMap = Vec<(u32, Option<usize>)>;
785
786/// VCR-DEC-003 (#396, witness#130): the object-level control-flow class of one
787/// emitted machine instruction, captured at encode time alongside [`LineMap`].
788/// It is the piece post-hoc CLI derivation cannot recover — `line_map` records
789/// which wasm op an instruction came from, but not whether that instruction IS a
790/// conditional branch, an unconditional branch, or a predicated (IT-block) move.
791/// The `synth-provenance-v1` emitter needs it to enumerate the ACTUAL object
792/// conditional branches (so it can prove "every object branch resolves to a
793/// source condition", not just "every source branch has an object PC").
794#[derive(Debug, Clone, Copy, PartialEq, Eq)]
795pub enum BranchClass {
796    /// A conditional branch (`Bcc`/`Blo`/`Bhs`/`BCondOffset`) — an object-level
797    /// decision point MC/DC must account for.
798    CondBranch,
799    /// An unconditional branch (`B`/`BOffset`) — control flow, not a decision.
800    UncondBranch,
801    /// A predicated conditional move (`SelectMove`, the IT-block form the
802    /// cmp→select fuse produces) — a folded decision with no branch.
803    Predicated,
804    /// Anything else (data-processing, load/store, call, prologue/epilogue).
805    Other,
806}
807
808/// VCR-DEC-003: per-instruction object-branch class, parallel to [`LineMap`]
809/// (same length, same order — one entry per emitted machine instruction).
810/// `(machine_offset_within_code, class)`. Empty when provenance is not being
811/// produced (never serialized into `.text`; frozen-safe additive metadata).
812pub type BranchMap = Vec<(u32, BranchClass)>;
813
814/// A single compiled function
815#[derive(Debug, Clone)]
816pub struct CompiledFunction {
817    /// Function name (from WASM export or generated)
818    pub name: String,
819    /// Raw machine code bytes
820    pub code: Vec<u8>,
821    /// Original WASM ops (retained for verification)
822    pub wasm_ops: Vec<WasmOp>,
823    /// Relocations for external symbol references (BL to bridge functions)
824    pub relocations: Vec<CodeRelocation>,
825    /// VCR-DBG-001: per-instruction source map for DWARF `.debug_line` emission —
826    /// `(machine_offset_within_code, wasm_op_index)` captured at encode time, one
827    /// entry per emitted machine instruction. A `None` op-index marks an
828    /// instruction with no originating wasm op (prologue/epilogue, literal-pool
829    /// word). This is purely additive metadata: it is never serialized unless
830    /// `.debug_line` emission is requested, so the emitted `.text` is
831    /// byte-identical with or without it. Empty for backends/paths that do not
832    /// yet produce a source map (RISC-V, the optimized ARM path).
833    pub line_map: LineMap,
834    /// VCR-DEC-003 (#396): per-instruction object-branch class, parallel to
835    /// `line_map`. Lets the `synth-provenance-v1` emitter enumerate the real
836    /// object conditional branches (not just re-walk the wasm branch ops).
837    /// Purely additive metadata: never serialized into `.text`, so emitted bytes
838    /// are byte-identical with or without it. Empty for backends/paths that do
839    /// not produce it (RISC-V, the optimized ARM path).
840    pub branch_map: BranchMap,
841    /// #778 (v0.46): the SOUND static worst-case-cycle bound for this function,
842    /// or a loud decline, computed over the final Thumb-2 instruction stream (see
843    /// [`crate::wcet`]). `Some` only when the ARM backend produced it (the RISC-V
844    /// and AArch64 backends carry no cycle model yet → `None`). Purely additive
845    /// metadata: derived from the already-decided instruction list, never
846    /// serialized into `.text`, so emitted bytes are byte-identical with or
847    /// without it (frozen-safe). Emitted as the `<output>.wcet.json` sidecar only
848    /// under `--emit-wcet`.
849    pub wcet: Option<crate::wcet::WcetFunction>,
850    /// #778 phase 3: the per-function WCET INTERMEDIATE (own-body cycles + direct
851    /// call sites, or a composition-independent decline) BEFORE inter-procedural
852    /// composition. The module driver composes these across the direct call graph
853    /// into the final per-function bounds (a caller's bound = its own body + each
854    /// direct callee's bound × the call site's proven execution count). `Some` only
855    /// on the Thumb-2 path that produced `wcet`. Purely additive, `.text`-invisible
856    /// (frozen-safe) — derived from the already-decided instruction list.
857    pub wcet_intermediate: Option<crate::wcet::WcetIntermediate>,
858}
859
860/// Result of compiling a full module
861#[derive(Debug)]
862pub struct CompilationResult {
863    /// Compiled functions
864    pub functions: Vec<CompiledFunction>,
865    /// Complete ELF binary (if backend produces one directly)
866    pub elf: Option<Vec<u8>>,
867    /// Name of the backend that produced this result
868    pub backend_name: String,
869}
870
871/// What a backend can and cannot do
872#[derive(Debug, Clone)]
873pub struct BackendCapabilities {
874    /// Backend produces complete ELF files (external backends like aWsm)
875    pub produces_elf: bool,
876    /// Backend supports per-rule verification (only our custom ARM backend)
877    pub supports_rule_verification: bool,
878    /// Backend supports binary-level verification (all backends via disassembly)
879    pub supports_binary_verification: bool,
880    /// Backend is an external tool (not a library)
881    pub is_external: bool,
882}
883
884/// Trait that every compilation backend implements
885pub trait Backend: Send + Sync {
886    /// Human-readable backend name
887    fn name(&self) -> &str;
888
889    /// What this backend can do
890    fn capabilities(&self) -> BackendCapabilities;
891
892    /// Which targets this backend supports
893    fn supported_targets(&self) -> Vec<TargetSpec>;
894
895    /// Compile an entire decoded WASM module
896    fn compile_module(
897        &self,
898        module: &DecodedModule,
899        config: &CompileConfig,
900    ) -> std::result::Result<CompilationResult, BackendError>;
901
902    /// Compile a single function from WASM ops to machine code
903    fn compile_function(
904        &self,
905        name: &str,
906        ops: &[WasmOp],
907        config: &CompileConfig,
908    ) -> std::result::Result<CompiledFunction, BackendError>;
909
910    /// Check if this backend is available (external tools installed, etc.)
911    fn is_available(&self) -> bool;
912}
913
914/// Registry of available backends
915pub struct BackendRegistry {
916    backends: HashMap<String, Box<dyn Backend>>,
917}
918
919impl BackendRegistry {
920    pub fn new() -> Self {
921        Self {
922            backends: HashMap::new(),
923        }
924    }
925
926    /// Register a backend under its name
927    pub fn register(&mut self, backend: Box<dyn Backend>) {
928        let name = backend.name().to_string();
929        self.backends.insert(name, backend);
930    }
931
932    /// Get a backend by name
933    pub fn get(&self, name: &str) -> Option<&dyn Backend> {
934        self.backends.get(name).map(|b| b.as_ref())
935    }
936
937    /// List all registered backends
938    pub fn list(&self) -> Vec<&dyn Backend> {
939        self.backends.values().map(|b| b.as_ref()).collect()
940    }
941
942    /// List backends that are actually available (installed and working)
943    pub fn available(&self) -> Vec<&dyn Backend> {
944        self.backends
945            .values()
946            .filter(|b| b.is_available())
947            .map(|b| b.as_ref())
948            .collect()
949    }
950}
951
952impl Default for BackendRegistry {
953    fn default() -> Self {
954        Self::new()
955    }
956}
957
958#[cfg(test)]
959mod tests {
960    use super::*;
961
962    #[test]
963    fn test_registry_empty() {
964        let reg = BackendRegistry::new();
965        assert!(reg.list().is_empty());
966        assert!(reg.available().is_empty());
967        assert!(reg.get("arm").is_none());
968    }
969
970    #[test]
971    fn test_compile_config_default() {
972        let config = CompileConfig::default();
973        assert_eq!(config.opt_level, 2);
974        assert!(!config.bounds_check);
975        assert_eq!(config.safety_bounds, SafetyBounds::None);
976        assert!(!config.no_optimize);
977    }
978
979    #[test]
980    fn safety_bounds_parse_round_trip() {
981        for s in ["none", "mpu", "software", "mask"] {
982            let sb = SafetyBounds::parse(s).unwrap();
983            assert_eq!(sb.as_str(), s);
984        }
985        assert_eq!(SafetyBounds::parse("pmp").unwrap(), SafetyBounds::Mpu);
986        assert_eq!(SafetyBounds::parse("soft").unwrap(), SafetyBounds::Software);
987        assert!(SafetyBounds::parse("nonsense").is_err());
988    }
989
990    #[test]
991    fn effective_safety_bounds_legacy_promotes_to_software() {
992        let cfg = CompileConfig {
993            bounds_check: true,
994            ..Default::default()
995        };
996        assert_eq!(cfg.effective_safety_bounds(), SafetyBounds::Software);
997    }
998
999    #[test]
1000    fn effective_safety_bounds_new_field_wins() {
1001        let cfg = CompileConfig {
1002            bounds_check: true,
1003            safety_bounds: SafetyBounds::Mpu,
1004            ..Default::default()
1005        };
1006        assert_eq!(cfg.effective_safety_bounds(), SafetyBounds::Mpu);
1007    }
1008}