synth_verify/arm_semantics.rs
1//! ARM Semantics Encoding to SMT
2//!
3//! Encodes ARM operation semantics as SMT bitvector formulas.
4//! Each ARM operation is translated to a mathematical formula that precisely
5//! captures its behavior, including register updates and condition flags.
6
7use crate::term::{BV, Bool};
8use std::collections::HashMap;
9use synth_synthesis::rules::{ArmOp, Operand2, Reg, VfpReg};
10
11/// ARM processor state representation in SMT
12///
13/// Z3 0.19 uses thread-local context -- no lifetime parameters needed.
14pub struct ArmState {
15 /// General purpose registers R0-R15
16 pub registers: Vec<BV>,
17 /// Condition flags (N, Z, C, V)
18 pub flags: ConditionFlags,
19 /// VFP (floating-point) registers
20 pub vfp_registers: Vec<BV>,
21 /// Memory model (simplified for bounded verification)
22 pub memory: Vec<BV>,
23 /// Local variables (for WASM verification)
24 pub locals: Vec<BV>,
25 /// Global variables (for WASM verification)
26 pub globals: Vec<BV>,
27 /// VCR-VER-002 (#166): the accumulated condition under which the executed
28 /// sequence TRAPS (reaches a `UDF`). `false` in a fresh state; `encode_op`
29 /// sets it unconditionally on a `Udf`, and the branch-taking executor
30 /// [`ArmSemantics::encode_sequence_br`] conditions it on the path guard the
31 /// `UDF` is reached under — this is the ARM-side trap term the
32 /// trap-preservation VC compares against the WASM op's trap condition.
33 pub may_trap: Bool,
34 /// #923: the FIRST ARM op [`ArmSemantics::encode_op`] was asked to execute
35 /// and has no semantics for, recorded by the `_ => {}` default arm instead
36 /// of being silently dropped.
37 ///
38 /// Before this field existed the default arm was a silent register no-op,
39 /// which makes an unmodeled instruction INVISIBLE to the value VC: a
40 /// lowering that computes the right value and then destroys it (measured:
41 /// `i32.add → ADD r0,r0,r1 ; UXTB r0,r0`, which returns `(x+y) & 0xFF` on
42 /// silicon) came back `Verified`. The trap path already defended itself —
43 /// [`ArmSemantics::exec_trap_subset_op`]'s doc says this default "must
44 /// never green-wash a trap derivation" — but its defence was a
45 /// hand-maintained allowlist that had drifted: `Rsb` (a SHIPPED sel-DSL
46 /// rule's instruction), `I32TruncF32S` and `I32TruncF32U` were all
47 /// allowlisted to DELEGATE to `encode_op`, which does not model them.
48 ///
49 /// Recording it here rather than in a second list is deliberate: the
50 /// modeled set keeps exactly one source of truth (the `match` arms), so it
51 /// cannot rot. Consumers turn a set field into a loud decline —
52 /// [`crate::TranslationValidator`]'s value VC into
53 /// `VerificationError::UnsupportedOperation`, `exec_trap_subset_op` into
54 /// its own `Err`.
55 pub unmodeled: Option<String>,
56}
57
58/// ARM condition flags
59pub struct ConditionFlags {
60 pub n: Bool, // Negative
61 pub z: Bool, // Zero
62 pub c: Bool, // Carry
63 pub v: Bool, // Overflow
64}
65
66impl ArmState {
67 /// Create a new ARM state with symbolic values
68 pub fn new_symbolic() -> Self {
69 let registers = (0..16)
70 .map(|i| BV::new_const(format!("r{}", i), 32))
71 .collect();
72
73 let flags = ConditionFlags {
74 n: Bool::new_const("flag_n"),
75 z: Bool::new_const("flag_z"),
76 c: Bool::new_const("flag_c"),
77 v: Bool::new_const("flag_v"),
78 };
79
80 let memory = (0..256)
81 .map(|i| BV::new_const(format!("mem_{}", i), 32))
82 .collect();
83
84 let locals = (0..32)
85 .map(|i| BV::new_const(format!("local_{}", i), 32))
86 .collect();
87
88 let globals = (0..16)
89 .map(|i| BV::new_const(format!("global_{}", i), 32))
90 .collect();
91
92 let vfp_registers = (0..48)
93 .map(|i| BV::new_const(format!("vfp_{}", i), 32))
94 .collect();
95
96 Self {
97 registers,
98 flags,
99 vfp_registers,
100 memory,
101 locals,
102 globals,
103 may_trap: Bool::from_bool(false),
104 unmodeled: None,
105 }
106 }
107
108 /// Get register value
109 pub fn get_reg(&self, reg: &Reg) -> &BV {
110 let index = reg_to_index(reg);
111 &self.registers[index]
112 }
113
114 /// Set register value
115 pub fn set_reg(&mut self, reg: &Reg, value: BV) {
116 let index = reg_to_index(reg);
117 self.registers[index] = value;
118 }
119
120 /// Get VFP register value
121 pub fn get_vfp_reg(&self, reg: &VfpReg) -> &BV {
122 let index = vfp_reg_to_index(reg);
123 &self.vfp_registers[index]
124 }
125
126 /// Set VFP register value
127 pub fn set_vfp_reg(&mut self, reg: &VfpReg, value: BV) {
128 let index = vfp_reg_to_index(reg);
129 self.vfp_registers[index] = value;
130 }
131}
132
133/// The `ArmOp` variant name (`"Uxtb"` from `Uxtb { rd: R0, rm: R0 }`).
134///
135/// Derived from `Debug`, not a hand-written table — the same choice, for the
136/// same stated reason, as `synth_backend::wcet::op_mnemonic`: a hand-mirrored
137/// name table is a second source of truth that drifts from the enum it
138/// mirrors (#682, #890). A new `ArmOp` variant names itself here for free.
139fn op_variant_name(op: &ArmOp) -> String {
140 let s = format!("{op:?}");
141 s.split([' ', '{', '(']).next().unwrap_or("").to_string()
142}
143
144/// Convert register enum to index
145fn reg_to_index(reg: &Reg) -> usize {
146 match reg {
147 Reg::R0 => 0,
148 Reg::R1 => 1,
149 Reg::R2 => 2,
150 Reg::R3 => 3,
151 Reg::R4 => 4,
152 Reg::R5 => 5,
153 Reg::R6 => 6,
154 Reg::R7 => 7,
155 Reg::R8 => 8,
156 Reg::R9 => 9,
157 Reg::R10 => 10,
158 Reg::R11 => 11,
159 Reg::R12 => 12,
160 Reg::SP => 13,
161 Reg::LR => 14,
162 Reg::PC => 15,
163 }
164}
165
166/// Convert VFP register enum to index
167fn vfp_reg_to_index(reg: &VfpReg) -> usize {
168 match reg {
169 // Single-precision registers S0-S31 (indices 0-31)
170 VfpReg::S0 => 0,
171 VfpReg::S1 => 1,
172 VfpReg::S2 => 2,
173 VfpReg::S3 => 3,
174 VfpReg::S4 => 4,
175 VfpReg::S5 => 5,
176 VfpReg::S6 => 6,
177 VfpReg::S7 => 7,
178 VfpReg::S8 => 8,
179 VfpReg::S9 => 9,
180 VfpReg::S10 => 10,
181 VfpReg::S11 => 11,
182 VfpReg::S12 => 12,
183 VfpReg::S13 => 13,
184 VfpReg::S14 => 14,
185 VfpReg::S15 => 15,
186 VfpReg::S16 => 16,
187 VfpReg::S17 => 17,
188 VfpReg::S18 => 18,
189 VfpReg::S19 => 19,
190 VfpReg::S20 => 20,
191 VfpReg::S21 => 21,
192 VfpReg::S22 => 22,
193 VfpReg::S23 => 23,
194 VfpReg::S24 => 24,
195 VfpReg::S25 => 25,
196 VfpReg::S26 => 26,
197 VfpReg::S27 => 27,
198 VfpReg::S28 => 28,
199 VfpReg::S29 => 29,
200 VfpReg::S30 => 30,
201 VfpReg::S31 => 31,
202 // Double-precision registers D0-D15 (indices 32-47)
203 // Note: D0 = S0:S1, D1 = S2:S3, etc.
204 // We store the "low" part of each D register
205 VfpReg::D0 => 32,
206 VfpReg::D1 => 33,
207 VfpReg::D2 => 34,
208 VfpReg::D3 => 35,
209 VfpReg::D4 => 36,
210 VfpReg::D5 => 37,
211 VfpReg::D6 => 38,
212 VfpReg::D7 => 39,
213 VfpReg::D8 => 40,
214 VfpReg::D9 => 41,
215 VfpReg::D10 => 42,
216 VfpReg::D11 => 43,
217 VfpReg::D12 => 44,
218 VfpReg::D13 => 45,
219 VfpReg::D14 => 46,
220 VfpReg::D15 => 47,
221 }
222}
223
224/// ARM semantics encoder
225///
226/// Z3 0.19 uses thread-local context -- no lifetime parameters needed.
227pub struct ArmSemantics;
228
229impl Default for ArmSemantics {
230 fn default() -> Self {
231 Self::new()
232 }
233}
234
235impl ArmSemantics {
236 /// Create a new ARM semantics encoder
237 pub fn new() -> Self {
238 Self
239 }
240
241 /// Encode an ARM operation and return the resulting state
242 ///
243 /// This models the effect of executing the ARM instruction on the processor state.
244 pub fn encode_op(&self, op: &ArmOp, state: &mut ArmState) {
245 match op {
246 ArmOp::Add { rd, rn, op2 } => {
247 let rn_val = state.get_reg(rn).clone();
248 let op2_val = self.evaluate_operand2(op2, state);
249 let result = rn_val.bvadd(&op2_val);
250 state.set_reg(rd, result);
251 }
252
253 ArmOp::Sub { rd, rn, op2 } => {
254 let rn_val = state.get_reg(rn).clone();
255 let op2_val = self.evaluate_operand2(op2, state);
256 let result = rn_val.bvsub(&op2_val);
257 state.set_reg(rd, result);
258 }
259
260 ArmOp::Mul { rd, rn, rm } => {
261 let rn_val = state.get_reg(rn).clone();
262 let rm_val = state.get_reg(rm).clone();
263 let result = rn_val.bvmul(&rm_val);
264 state.set_reg(rd, result);
265 }
266
267 ArmOp::Umull { rdlo, rdhi, rn, rm } => {
268 // {rdhi:rdlo} = zext64(rn) * zext64(rm); rdhi = high 32 bits.
269 let rn64 = state.get_reg(rn).zero_ext(32);
270 let rm64 = state.get_reg(rm).zero_ext(32);
271 let prod = rn64.bvmul(&rm64);
272 state.set_reg(rdlo, prod.extract(31, 0));
273 state.set_reg(rdhi, prod.extract(63, 32));
274 }
275
276 ArmOp::Sdiv { rd, rn, rm } => {
277 let rn_val = state.get_reg(rn).clone();
278 let rm_val = state.get_reg(rm).clone();
279 let result = rn_val.bvsdiv(&rm_val);
280 state.set_reg(rd, result);
281 }
282
283 ArmOp::Udiv { rd, rn, rm } => {
284 let rn_val = state.get_reg(rn).clone();
285 let rm_val = state.get_reg(rm).clone();
286 let result = rn_val.bvudiv(&rm_val);
287 state.set_reg(rd, result);
288 }
289
290 ArmOp::Mls { rd, rn, rm, ra } => {
291 // MLS (Multiply and Subtract): Rd = Ra - Rn * Rm
292 // Used for remainder operations: a % b = a - (a/b) * b
293 let rn_val = state.get_reg(rn).clone();
294 let rm_val = state.get_reg(rm).clone();
295 let ra_val = state.get_reg(ra).clone();
296 let product = rn_val.bvmul(&rm_val);
297 let result = ra_val.bvsub(&product);
298 state.set_reg(rd, result);
299 }
300
301 ArmOp::And { rd, rn, op2 } => {
302 let rn_val = state.get_reg(rn).clone();
303 let op2_val = self.evaluate_operand2(op2, state);
304 let result = rn_val.bvand(&op2_val);
305 state.set_reg(rd, result);
306 }
307
308 ArmOp::Orr { rd, rn, op2 } => {
309 let rn_val = state.get_reg(rn).clone();
310 let op2_val = self.evaluate_operand2(op2, state);
311 let result = rn_val.bvor(&op2_val);
312 state.set_reg(rd, result);
313 }
314
315 ArmOp::Eor { rd, rn, op2 } => {
316 let rn_val = state.get_reg(rn).clone();
317 let op2_val = self.evaluate_operand2(op2, state);
318 let result = rn_val.bvxor(&op2_val);
319 state.set_reg(rd, result);
320 }
321
322 ArmOp::Lsl { rd, rn, shift } => {
323 let rn_val = state.get_reg(rn).clone();
324 let shift_val = BV::from_i64(*shift as i64, 32);
325 let result = rn_val.bvshl(&shift_val);
326 state.set_reg(rd, result);
327 }
328
329 ArmOp::Lsr { rd, rn, shift } => {
330 let rn_val = state.get_reg(rn).clone();
331 let shift_val = BV::from_i64(*shift as i64, 32);
332 let result = rn_val.bvlshr(&shift_val);
333 state.set_reg(rd, result);
334 }
335
336 ArmOp::Asr { rd, rn, shift } => {
337 let rn_val = state.get_reg(rn).clone();
338 let shift_val = BV::from_i64(*shift as i64, 32);
339 let result = rn_val.bvashr(&shift_val);
340 state.set_reg(rd, result);
341 }
342
343 ArmOp::Ror { rd, rn, shift } => {
344 // Rotate right - ARM ROR instruction
345 // ROR(x, n) rotates x right by n positions
346 let rn_val = state.get_reg(rn).clone();
347 let shift_val = BV::from_i64(*shift as i64, 32);
348 let result = rn_val.bvrotr(&shift_val);
349 state.set_reg(rd, result);
350 }
351
352 // ================================================================
353 // Register-amount shifts (#923). ARMv7-M ARM A7.7.68/70/12/117:
354 // every `<shift> (register)` form computes
355 // shift_n = UInt(R[m]<7:0>)
356 // — the LOW EIGHT BITS of Rm, NOT Rm mod 32 and NOT all 32 bits.
357 // This is the #682 class of unfaithfulness, in the other file:
358 // the model must apply the ISA's own masking rule, and the WASM
359 // source op's mod-32 rule must be supplied by the LOWERING (the
360 // shipped selector emits `AND Rm,#31` ahead of these), never
361 // assumed by the ARM model.
362 //
363 // With `shift_n ∈ [0,255]` an SMT shift is then EXACTLY the ARM
364 // result: `Shift_C` with `shift_n >= 32` yields 0 for LSL/LSR and
365 // a sign fill for ASR, which is what `bvshl`/`bvlshr`/`bvashr`
366 // give for those amounts. Feeding the RAW 32-bit Rm instead would
367 // diverge from silicon at e.g. `Rm = 0x100`: the core shifts by
368 // `Rm<7:0> = 0` (identity), an unmasked `bvshl` gives 0.
369 ArmOp::LslReg { rd, rn, rm } => {
370 let rn_val = state.get_reg(rn).clone();
371 let amount = Self::shift_amount_rm_7_0(state.get_reg(rm));
372 state.set_reg(rd, rn_val.bvshl(&amount));
373 }
374
375 ArmOp::LsrReg { rd, rn, rm } => {
376 let rn_val = state.get_reg(rn).clone();
377 let amount = Self::shift_amount_rm_7_0(state.get_reg(rm));
378 state.set_reg(rd, rn_val.bvlshr(&amount));
379 }
380
381 ArmOp::AsrReg { rd, rn, rm } => {
382 let rn_val = state.get_reg(rn).clone();
383 let amount = Self::shift_amount_rm_7_0(state.get_reg(rm));
384 state.set_reg(rd, rn_val.bvashr(&amount));
385 }
386
387 // ROR (register) also takes `Rm<7:0>`, but rotation is periodic
388 // with period 32 and 256 is a multiple of 32, so `Rm<7:0> mod 32
389 // == Rm mod 32`: the extract is redundant for THIS op. Applied
390 // anyway, so the arm states the ISA rule rather than relying on an
391 // arithmetic coincidence a future reader would have to re-derive.
392 ArmOp::RorReg { rd, rn, rm } => {
393 let rn_val = state.get_reg(rn).clone();
394 let amount = Self::shift_amount_rm_7_0(state.get_reg(rm));
395 state.set_reg(rd, rn_val.bvrotr(&amount));
396 }
397
398 // RSB (immediate): Rd = imm - Rn. Emitted by the SHIPPED sel-DSL
399 // rule table (`sel_dsl::generated`, the rotl/rotr amount negation)
400 // and allowlisted by `exec_trap_subset_op` to delegate here — but
401 // unmodeled until #923, so that delegation silently no-oped.
402 ArmOp::Rsb { rd, rn, imm } => {
403 let rn_val = state.get_reg(rn).clone();
404 let result = BV::from_u64(*imm as u64, 32).bvsub(&rn_val);
405 state.set_reg(rd, result);
406 }
407
408 // Sign/zero extension of the low byte/halfword (ARMv7-M A7.7.166,
409 // .168, .217, .219 with rotation 0, the only form emitted).
410 ArmOp::Sxtb { rd, rm } => {
411 let v = state.get_reg(rm).extract(7, 0).sign_ext(24);
412 state.set_reg(rd, v);
413 }
414
415 ArmOp::Sxth { rd, rm } => {
416 let v = state.get_reg(rm).extract(15, 0).sign_ext(16);
417 state.set_reg(rd, v);
418 }
419
420 ArmOp::Uxtb { rd, rm } => {
421 let v = state.get_reg(rm).extract(7, 0).zero_ext(24);
422 state.set_reg(rd, v);
423 }
424
425 ArmOp::Uxth { rd, rm } => {
426 let v = state.get_reg(rm).extract(15, 0).zero_ext(16);
427 state.set_reg(rd, v);
428 }
429
430 // MOVW writes the whole register (top halfword ZEROED — it is a
431 // move, not an insert); MOVT writes only bits 31:16 and PRESERVES
432 // bits 15:0. Getting MOVT's preservation wrong would model the
433 // shipped 32-bit-constant idiom `MOVW/MOVT` as producing only the
434 // high half.
435 ArmOp::Movw { rd, imm16 } => {
436 state.set_reg(rd, BV::from_u64(*imm16 as u64, 32));
437 }
438
439 ArmOp::Movt { rd, imm16 } => {
440 let low = state.get_reg(rd).bvand(BV::from_u64(0xFFFF, 32));
441 let v = low.bvor(BV::from_u64((*imm16 as u64) << 16, 32));
442 state.set_reg(rd, v);
443 }
444
445 // CMN: compare negated — flags from Rn + op2, no register write.
446 ArmOp::Cmn { rn, op2 } => {
447 let a = state.get_reg(rn).clone();
448 let b = self.evaluate_operand2(op2, state);
449 let result = a.bvadd(&b);
450 self.update_flags_add(state, &a, &b, &result);
451 }
452
453 ArmOp::Mov { rd, op2 } => {
454 let op2_val = self.evaluate_operand2(op2, state);
455 state.set_reg(rd, op2_val);
456 }
457
458 ArmOp::Mvn { rd, op2 } => {
459 let op2_val = self.evaluate_operand2(op2, state);
460 let result = op2_val.bvnot();
461 state.set_reg(rd, result);
462 }
463
464 ArmOp::Cmp { rn, op2 } => {
465 // Compare sets flags but doesn't write to a register
466 // CMP performs: Rn - Op2 and updates all condition flags
467 let rn_val = state.get_reg(rn).clone();
468 let op2_val = self.evaluate_operand2(op2, state);
469
470 // Compute result of subtraction
471 let result = rn_val.bvsub(&op2_val);
472
473 // Update all condition flags
474 self.update_flags_sub(state, &rn_val, &op2_val, &result);
475 }
476
477 ArmOp::Clz { rd, rm } => {
478 // Count leading zeros - ARM CLZ instruction
479 // Uses binary search algorithm matching WASM i32.clz semantics
480 let input = state.get_reg(rm).clone();
481 let result = self.encode_clz(&input);
482 state.set_reg(rd, result);
483 }
484
485 ArmOp::Rbit { rd, rm } => {
486 // Reverse bits - ARM RBIT instruction
487 // Reverses the bit order in a 32-bit value
488 let input = state.get_reg(rm).clone();
489 let result = self.encode_rbit(&input);
490 state.set_reg(rd, result);
491 }
492
493 ArmOp::Popcnt { rd, rm } => {
494 // Population count - count number of 1 bits
495 // This is a pseudo-instruction for verification
496 let input = state.get_reg(rm).clone();
497 let result = self.encode_popcnt(&input);
498 state.set_reg(rd, result);
499 }
500
501 ArmOp::Nop => {
502 // No operation - state unchanged
503 }
504
505 ArmOp::SetCond { rd, cond } => {
506 // SetCond evaluates a condition based on NZCV flags and sets rd to 0 or 1
507 // This is a pseudo-instruction for verification purposes
508 let cond_result = self.evaluate_condition(cond, &state.flags);
509 let result = self.bool_to_bv32(&cond_result);
510 state.set_reg(rd, result);
511 }
512
513 ArmOp::Select {
514 rd,
515 rval1,
516 rval2,
517 rcond,
518 } => {
519 // Select operation: if rcond != 0, select rval1, else rval2
520 // This is a pseudo-instruction for verification purposes
521 let val1 = state.get_reg(rval1).clone();
522 let val2 = state.get_reg(rval2).clone();
523 let cond = state.get_reg(rcond).clone();
524 let zero = BV::from_i64(0, 32);
525 let cond_bool = cond.eq(&zero).not(); // cond != 0
526 let result = cond_bool.ite(&val1, &val2);
527 state.set_reg(rd, result);
528 }
529
530 // Memory operations simplified for now
531 ArmOp::Ldr { rd, addr: _ } => {
532 // Load from memory
533 // Simplified: return symbolic value
534 let result = BV::new_const(format!("load_{:?}", rd), 32);
535 state.set_reg(rd, result);
536 }
537
538 ArmOp::Str { rd: _, addr: _ } => {
539 // Store to memory
540 // Simplified: memory updates not fully modeled yet
541 }
542
543 // Control flow operations
544 ArmOp::B { label: _ } => {
545 // Branch - would update PC in full model
546 // For bounded verification, we treat this symbolically
547 }
548
549 ArmOp::Bl { label: _ } => {
550 // Branch with link - would update PC and LR
551 }
552
553 ArmOp::Bx { rm: _ } => {
554 // Branch and exchange - would update PC
555 }
556
557 // Local/Global variable access (pseudo-instructions for verification)
558 ArmOp::LocalGet { rd, index } => {
559 // Load local variable into register
560 let value = state
561 .locals
562 .get(*index as usize)
563 .cloned()
564 .unwrap_or_else(|| BV::new_const(format!("local_{}", index), 32));
565 state.set_reg(rd, value);
566 }
567
568 ArmOp::LocalSet { rs, index } => {
569 // Store register into local variable
570 let value = state.get_reg(rs).clone();
571 if let Some(local) = state.locals.get_mut(*index as usize) {
572 *local = value;
573 }
574 }
575
576 ArmOp::LocalTee { rd, rs, index } => {
577 // Store register into local variable and also copy to destination
578 let value = state.get_reg(rs).clone();
579 if let Some(local) = state.locals.get_mut(*index as usize) {
580 *local = value.clone();
581 }
582 state.set_reg(rd, value);
583 }
584
585 ArmOp::GlobalGet { rd, index } => {
586 // Load global variable into register
587 let value = state
588 .globals
589 .get(*index as usize)
590 .cloned()
591 .unwrap_or_else(|| BV::new_const(format!("global_{}", index), 32));
592 state.set_reg(rd, value);
593 }
594
595 ArmOp::GlobalSet { rs, index } => {
596 // Store register into global variable
597 let value = state.get_reg(rs).clone();
598 if let Some(global) = state.globals.get_mut(*index as usize) {
599 *global = value;
600 }
601 }
602
603 ArmOp::BrTable {
604 rd,
605 index_reg,
606 targets,
607 default,
608 } => {
609 // Multi-way branch based on index
610 // For verification, we model the control flow symbolically
611 let _index = state.get_reg(index_reg).clone();
612 let result = BV::new_const(format!("br_table_{}_{}", targets.len(), default), 32);
613 state.set_reg(rd, result);
614 }
615
616 ArmOp::Call { rd, func_idx } => {
617 // Function call - model result symbolically
618 let result = BV::new_const(format!("call_{}", func_idx), 32);
619 state.set_reg(rd, result);
620 }
621
622 ArmOp::CallIndirect {
623 rd,
624 type_idx,
625 table_index_reg,
626 // #642: the bounds guard is a control-flow effect (trap), not
627 // modeled by the symbolic call result. #650: the table base
628 // offset only changes WHICH pointer is loaded, not the
629 // symbolic result shape. #664: the null check is likewise a
630 // trap (control-flow effect) on the loaded pointer.
631 table_size: _,
632 table_byte_offset: _,
633 null_check: _,
634 // #676: the runtime type check is likewise a trap
635 // (control-flow effect) on the sidecar-loaded class id.
636 type_check: _,
637 } => {
638 // Indirect function call through table
639 let _table_index = state.get_reg(table_index_reg).clone();
640 let result = BV::new_const(format!("call_indirect_{}", type_idx), 32);
641 state.set_reg(rd, result);
642 }
643
644 // ================================================================
645 // i64 Operations (Phase 2) - Simplified implementation
646 // ================================================================
647 // These use register pairs on ARM32 but simplified to single
648 // registers for initial implementation
649 ArmOp::I64Const { rdlo, rdhi, value } => {
650 // Load 64-bit constant into register pair
651 let low32 = (*value as u32) as i64;
652 let high32 = *value >> 32;
653 state.set_reg(rdlo, BV::from_i64(low32, 32));
654 state.set_reg(rdhi, BV::from_i64(high32, 32));
655 }
656
657 ArmOp::I64Add {
658 rdlo,
659 rdhi,
660 rnlo,
661 rnhi,
662 rmlo,
663 rmhi,
664 } => {
665 // 64-bit addition with register pairs and carry propagation
666 // ARM: ADDS rdlo, rnlo, rmlo ; Add low parts, set carry
667 // ADC rdhi, rnhi, rmhi ; Add high parts with carry
668
669 let n_low = state.get_reg(rnlo).clone();
670 let m_low = state.get_reg(rmlo).clone();
671 let n_high = state.get_reg(rnhi).clone();
672 let m_high = state.get_reg(rmhi).clone();
673
674 // Low part: simple addition
675 let result_low = n_low.bvadd(&m_low);
676 state.set_reg(rdlo, result_low.clone());
677
678 // Detect carry: overflow occurred if result < either operand
679 // For unsigned: carry = (result_low < n_low)
680 let carry = result_low.bvult(&n_low);
681 let carry_bv = carry.ite(BV::from_i64(1, 32), BV::from_i64(0, 32));
682
683 // High part: add with carry
684 let high_sum = n_high.bvadd(&m_high);
685 let result_high = high_sum.bvadd(&carry_bv);
686 state.set_reg(rdhi, result_high);
687 }
688
689 ArmOp::I64Eqz { rd, rnlo, rnhi } => {
690 // Check if 64-bit value is zero
691 // True if both low and high parts are zero
692 let zero = BV::from_i64(0, 32);
693 let low_zero = state.get_reg(rnlo).eq(&zero);
694 let high_zero = state.get_reg(rnhi).eq(&zero);
695 let both_zero = Bool::and(&[&low_zero, &high_zero]);
696 let result = self.bool_to_bv32(&both_zero);
697 state.set_reg(rd, result);
698 }
699
700 ArmOp::I32WrapI64 { rd, rnlo } => {
701 // Wrap 64-bit to 32-bit (take low 32 bits)
702 let low_val = state.get_reg(rnlo).clone();
703 state.set_reg(rd, low_val);
704 }
705
706 ArmOp::I64ExtendI32S { rdlo, rdhi, rn } => {
707 // Sign-extend 32-bit to 64-bit
708 let value = state.get_reg(rn).clone();
709 state.set_reg(rdlo, value.clone());
710
711 // High part is sign extension (all 0s or all 1s based on sign bit)
712 let sign_bit = value.extract(31, 31); // Extract bit 31
713 let all_ones = BV::from_i64(-1, 32);
714 let zero = BV::from_i64(0, 32);
715 // If sign bit is 1, high = 0xFFFFFFFF, else high = 0
716 let high_val = sign_bit.eq(BV::from_i64(1, 1)).ite(&all_ones, &zero);
717 state.set_reg(rdhi, high_val);
718 }
719
720 ArmOp::I64ExtendI32U { rdlo, rdhi, rn } => {
721 // Zero-extend 32-bit to 64-bit
722 let value = state.get_reg(rn).clone();
723 state.set_reg(rdlo, value);
724 // High part is always zero for unsigned extend
725 state.set_reg(rdhi, BV::from_i64(0, 32));
726 }
727
728 ArmOp::I64Sub {
729 rdlo,
730 rdhi,
731 rnlo,
732 rnhi,
733 rmlo,
734 rmhi,
735 } => {
736 // 64-bit subtraction with register pairs and borrow propagation
737 // ARM: SUBS rdlo, rnlo, rmlo ; Subtract low parts, set borrow
738 // SBC rdhi, rnhi, rmhi ; Subtract high parts with borrow
739
740 let n_low = state.get_reg(rnlo).clone();
741 let m_low = state.get_reg(rmlo).clone();
742 let n_high = state.get_reg(rnhi).clone();
743 let m_high = state.get_reg(rmhi).clone();
744
745 // Low part: simple subtraction
746 let result_low = n_low.bvsub(&m_low);
747 state.set_reg(rdlo, result_low.clone());
748
749 // Detect borrow: borrow occurred if n_low < m_low (unsigned)
750 let borrow = n_low.bvult(&m_low);
751 let borrow_bv = borrow.ite(BV::from_i64(1, 32), BV::from_i64(0, 32));
752
753 // High part: subtract with borrow
754 let high_diff = n_high.bvsub(&m_high);
755 let result_high = high_diff.bvsub(&borrow_bv);
756 state.set_reg(rdhi, result_high);
757 }
758
759 ArmOp::I64Mul {
760 rd_lo,
761 rd_hi,
762 rn_lo,
763 rn_hi,
764 rm_lo,
765 rm_hi,
766 } => {
767 // 64-bit multiplication: (a_hi:a_lo) * (b_hi:b_lo) → (result_hi:result_lo)
768 // Algorithm for 64x64→64 bit multiplication:
769 // result = (a_hi * b_lo * 2^32) + (a_lo * b_hi * 2^32) + (a_lo * b_lo)
770 // Only the low 64 bits are kept
771
772 let a_lo = state.get_reg(rn_lo).clone();
773 let a_hi = state.get_reg(rn_hi).clone();
774 let b_lo = state.get_reg(rm_lo).clone();
775 let b_hi = state.get_reg(rm_hi).clone();
776
777 // Low part: a_lo * b_lo (32x32→64, we need both parts)
778 // For SMT, we can use bvmul which gives 32-bit result (truncated)
779 let lo_lo = a_lo.bvmul(&b_lo);
780 state.set_reg(rd_lo, lo_lo.clone());
781
782 // For the high part, we need to handle overflow from a_lo * b_lo
783 // and add the cross products: a_hi * b_lo + a_lo * b_hi
784 //
785 // Simplified approach: use symbolic representation for now
786 // TODO: Implement full 64-bit multiplication with proper overflow handling
787 // This requires 64-bit bitvector intermediate computations
788
789 // Cross products (take low 32 bits of each)
790 let hi_lo = a_hi.bvmul(&b_lo); // a_hi * b_lo (low 32 bits)
791 let lo_hi = a_lo.bvmul(&b_hi); // a_lo * b_hi (low 32 bits)
792
793 // High part approximation (missing carry from a_lo * b_lo)
794 // result_hi ≈ hi_lo + lo_hi
795 let hi_sum = hi_lo.bvadd(&lo_hi);
796 state.set_reg(rd_hi, hi_sum);
797
798 // Note: This is a simplified implementation. A complete implementation
799 // would need to:
800 // 1. Extract high 32 bits of (a_lo * b_lo)
801 // 2. Add that to the cross products
802 // 3. Handle carries properly
803 }
804
805 // ========================================================================
806 // i64 Division and Remainder
807 // ========================================================================
808 // Note: ARM32 has no 64-bit divide instruction — the shipped
809 // lowering expands these pseudo-ops INLINE to a software
810 // long-division sequence with an internal 64-iteration runtime
811 // loop (arm_encoder.rs; no `__aeabi_*` library call is emitted).
812 // For verification, we model the results symbolically.
813 ArmOp::I64DivS { rdlo, rdhi, .. } => {
814 // Signed 64-bit division — the value the inline expansion
815 // must produce; modeled here as symbolic values
816 state.set_reg(rdlo, BV::new_const("i64_divs_lo", 32));
817 state.set_reg(rdhi, BV::new_const("i64_divs_hi", 32));
818 }
819
820 ArmOp::I64DivU { rdlo, rdhi, .. } => {
821 // Unsigned 64-bit division — same inline-expansion note as
822 // I64DivS; for verification, return symbolic values
823 state.set_reg(rdlo, BV::new_const("i64_divu_lo", 32));
824 state.set_reg(rdhi, BV::new_const("i64_divu_hi", 32));
825 }
826
827 ArmOp::I64RemS {
828 rdlo,
829 rdhi,
830 rnlo,
831 rnhi,
832 rmlo,
833 rmhi,
834 ..
835 } => {
836 // Signed 64-bit remainder (modulo). Same shape as I64RemU but
837 // the SIGNED remainder (`bvsrem`, SMT-LIB sign-of-dividend). The
838 // shipped lowering is an inline software long-division
839 // expansion (arm_encoder.rs, 64-iteration loop — not a library
840 // call); the value it must produce is exactly the native
841 // 64-bit signed remainder. The value VC (`verify_i64_rem_value_preservation`)
842 // asserts the R0:R1 pair equals it on the non-trapping path.
843 // rem_s traps ONLY on ÷0 (`rem_s(INT64_MIN,-1) == 0`, no
844 // overflow trap).
845 let n_lo = state.get_reg(rnlo).clone();
846 let n_hi = state.get_reg(rnhi).clone();
847 let m_lo = state.get_reg(rmlo).clone();
848 let m_hi = state.get_reg(rmhi).clone();
849
850 let dividend = n_hi.concat(&n_lo); // 64-bit: n_hi:n_lo
851 let divisor = m_hi.concat(&m_lo); // 64-bit: m_hi:m_lo
852 let rem = dividend.bvsrem(&divisor); // native signed rem, 64-bit
853
854 state.set_reg(rdlo, rem.extract(31, 0));
855 state.set_reg(rdhi, rem.extract(63, 32));
856 }
857
858 ArmOp::I64RemU {
859 rdlo,
860 rdhi,
861 rnlo,
862 rnhi,
863 rmlo,
864 rmhi,
865 ..
866 } => {
867 // Unsigned 64-bit remainder (modulo). ARM32 has no 64-bit
868 // divide instruction — the shipped lowering expands this
869 // pseudo-op INLINE to a software long-division loop
870 // (arm_encoder.rs, not a library call) — but for
871 // translation-validation the *value* the expansion must
872 // produce is exactly the native 64-bit unsigned remainder. Model it with
873 // the native `BvTerm::Urem` (ordeal 0.12, plumbed via
874 // `BV::bvurem`) instead of a HAVOC constant, so the value VC
875 // (`verify_i64_rem_value_preservation`) proves the register
876 // pair actually equals `dividend % divisor`.
877 //
878 // Compose the 64-bit operands from their register halves
879 // (`concat` puts self in the HIGH bits), take the 64-bit
880 // unsigned remainder, and split back to lo/hi. On a zero
881 // divisor SMT-LIB `bvurem` is total (returns the dividend),
882 // but WASM traps — the value clause is asserted only on the
883 // non-trapping path by the trap-guarded value VC, so this
884 // total model is sound.
885 let n_lo = state.get_reg(rnlo).clone();
886 let n_hi = state.get_reg(rnhi).clone();
887 let m_lo = state.get_reg(rmlo).clone();
888 let m_hi = state.get_reg(rmhi).clone();
889
890 let dividend = n_hi.concat(&n_lo); // 64-bit: n_hi:n_lo
891 let divisor = m_hi.concat(&m_lo); // 64-bit: m_hi:m_lo
892 let rem = dividend.bvurem(&divisor); // native bvurem, 64-bit
893
894 state.set_reg(rdlo, rem.extract(31, 0)); // low 32 bits
895 state.set_reg(rdhi, rem.extract(63, 32)); // high 32 bits
896 }
897
898 ArmOp::I64And {
899 rdlo,
900 rdhi,
901 rnlo,
902 rnhi,
903 rmlo,
904 rmhi,
905 } => {
906 let n_low = state.get_reg(rnlo).clone();
907 let m_low = state.get_reg(rmlo).clone();
908 state.set_reg(rdlo, n_low.bvand(&m_low));
909
910 let n_high = state.get_reg(rnhi).clone();
911 let m_high = state.get_reg(rmhi).clone();
912 state.set_reg(rdhi, n_high.bvand(&m_high));
913 }
914
915 ArmOp::I64Or {
916 rdlo,
917 rdhi,
918 rnlo,
919 rnhi,
920 rmlo,
921 rmhi,
922 } => {
923 let n_low = state.get_reg(rnlo).clone();
924 let m_low = state.get_reg(rmlo).clone();
925 state.set_reg(rdlo, n_low.bvor(&m_low));
926
927 let n_high = state.get_reg(rnhi).clone();
928 let m_high = state.get_reg(rmhi).clone();
929 state.set_reg(rdhi, n_high.bvor(&m_high));
930 }
931
932 ArmOp::I64Xor {
933 rdlo,
934 rdhi,
935 rnlo,
936 rnhi,
937 rmlo,
938 rmhi,
939 } => {
940 let n_low = state.get_reg(rnlo).clone();
941 let m_low = state.get_reg(rmlo).clone();
942 state.set_reg(rdlo, n_low.bvxor(&m_low));
943
944 let n_high = state.get_reg(rnhi).clone();
945 let m_high = state.get_reg(rmhi).clone();
946 state.set_reg(rdhi, n_high.bvxor(&m_high));
947 }
948
949 ArmOp::I64Eq {
950 rd,
951 rnlo,
952 rnhi,
953 rmlo,
954 rmhi,
955 } => {
956 let n_low = state.get_reg(rnlo).clone();
957 let m_low = state.get_reg(rmlo).clone();
958 let n_high = state.get_reg(rnhi).clone();
959 let m_high = state.get_reg(rmhi).clone();
960
961 let low_eq = n_low.eq(&m_low);
962 let high_eq = n_high.eq(&m_high);
963 let both_eq = Bool::and(&[&low_eq, &high_eq]);
964 let result = self.bool_to_bv32(&both_eq);
965 state.set_reg(rd, result);
966 }
967
968 ArmOp::I64LtS {
969 rd,
970 rnlo,
971 rnhi,
972 rmlo,
973 rmhi,
974 } => {
975 // Signed less than: n < m
976 // Compare high parts first (signed), tiebreak with low parts (unsigned)
977 let n_low = state.get_reg(rnlo).clone();
978 let m_low = state.get_reg(rmlo).clone();
979 let n_high = state.get_reg(rnhi).clone();
980 let m_high = state.get_reg(rmhi).clone();
981
982 // High parts comparison (signed)
983 let high_lt = n_high.bvslt(&m_high);
984 let high_eq = n_high.eq(&m_high);
985
986 // Low parts comparison (unsigned)
987 let low_lt = n_low.bvult(&m_low);
988
989 // Result: high_lt OR (high_eq AND low_lt)
990 let eq_and_low = Bool::and(&[&high_eq, &low_lt]);
991 let result_bool = Bool::or(&[&high_lt, &eq_and_low]);
992 let result = self.bool_to_bv32(&result_bool);
993 state.set_reg(rd, result);
994 }
995
996 ArmOp::I64LtU {
997 rd,
998 rnlo,
999 rnhi,
1000 rmlo,
1001 rmhi,
1002 } => {
1003 // Unsigned less than: n < m
1004 // Compare high parts first (unsigned), tiebreak with low parts (unsigned)
1005 let n_low = state.get_reg(rnlo).clone();
1006 let m_low = state.get_reg(rmlo).clone();
1007 let n_high = state.get_reg(rnhi).clone();
1008 let m_high = state.get_reg(rmhi).clone();
1009
1010 // High parts comparison (unsigned)
1011 let high_lt = n_high.bvult(&m_high);
1012 let high_eq = n_high.eq(&m_high);
1013
1014 // Low parts comparison (unsigned)
1015 let low_lt = n_low.bvult(&m_low);
1016
1017 // Result: high_lt OR (high_eq AND low_lt)
1018 let eq_and_low = Bool::and(&[&high_eq, &low_lt]);
1019 let result_bool = Bool::or(&[&high_lt, &eq_and_low]);
1020 let result = self.bool_to_bv32(&result_bool);
1021 state.set_reg(rd, result);
1022 }
1023
1024 ArmOp::I64Ne {
1025 rd,
1026 rnlo,
1027 rnhi,
1028 rmlo,
1029 rmhi,
1030 } => {
1031 // Not equal: !(n == m)
1032 let n_low = state.get_reg(rnlo).clone();
1033 let m_low = state.get_reg(rmlo).clone();
1034 let n_high = state.get_reg(rnhi).clone();
1035 let m_high = state.get_reg(rmhi).clone();
1036
1037 let low_eq = n_low.eq(&m_low);
1038 let high_eq = n_high.eq(&m_high);
1039 let both_eq = Bool::and(&[&low_eq, &high_eq]);
1040 let not_eq = both_eq.not();
1041 let result = self.bool_to_bv32(¬_eq);
1042 state.set_reg(rd, result);
1043 }
1044
1045 ArmOp::I64LeS {
1046 rd,
1047 rnlo,
1048 rnhi,
1049 rmlo,
1050 rmhi,
1051 } => {
1052 // Signed less than or equal: n <= m
1053 // Equivalent to: n < m OR n == m
1054 let n_low = state.get_reg(rnlo).clone();
1055 let m_low = state.get_reg(rmlo).clone();
1056 let n_high = state.get_reg(rnhi).clone();
1057 let m_high = state.get_reg(rmhi).clone();
1058
1059 let high_lt = n_high.bvslt(&m_high);
1060 let high_eq = n_high.eq(&m_high);
1061 let low_le = n_low.bvule(&m_low); // Low parts unsigned LE
1062
1063 let eq_and_le = Bool::and(&[&high_eq, &low_le]);
1064 let result_bool = Bool::or(&[&high_lt, &eq_and_le]);
1065 let result = self.bool_to_bv32(&result_bool);
1066 state.set_reg(rd, result);
1067 }
1068
1069 ArmOp::I64LeU {
1070 rd,
1071 rnlo,
1072 rnhi,
1073 rmlo,
1074 rmhi,
1075 } => {
1076 // Unsigned less than or equal: n <= m
1077 let n_low = state.get_reg(rnlo).clone();
1078 let m_low = state.get_reg(rmlo).clone();
1079 let n_high = state.get_reg(rnhi).clone();
1080 let m_high = state.get_reg(rmhi).clone();
1081
1082 let high_lt = n_high.bvult(&m_high);
1083 let high_eq = n_high.eq(&m_high);
1084 let low_le = n_low.bvule(&m_low);
1085
1086 let eq_and_le = Bool::and(&[&high_eq, &low_le]);
1087 let result_bool = Bool::or(&[&high_lt, &eq_and_le]);
1088 let result = self.bool_to_bv32(&result_bool);
1089 state.set_reg(rd, result);
1090 }
1091
1092 ArmOp::I64GtS {
1093 rd,
1094 rnlo,
1095 rnhi,
1096 rmlo,
1097 rmhi,
1098 } => {
1099 // Signed greater than: n > m
1100 // Equivalent to: m < n
1101 let n_low = state.get_reg(rnlo).clone();
1102 let m_low = state.get_reg(rmlo).clone();
1103 let n_high = state.get_reg(rnhi).clone();
1104 let m_high = state.get_reg(rmhi).clone();
1105
1106 let high_gt = n_high.bvsgt(&m_high);
1107 let high_eq = n_high.eq(&m_high);
1108 let low_gt = n_low.bvugt(&m_low); // Low parts unsigned GT
1109
1110 let eq_and_gt = Bool::and(&[&high_eq, &low_gt]);
1111 let result_bool = Bool::or(&[&high_gt, &eq_and_gt]);
1112 let result = self.bool_to_bv32(&result_bool);
1113 state.set_reg(rd, result);
1114 }
1115
1116 ArmOp::I64GtU {
1117 rd,
1118 rnlo,
1119 rnhi,
1120 rmlo,
1121 rmhi,
1122 } => {
1123 // Unsigned greater than: n > m
1124 let n_low = state.get_reg(rnlo).clone();
1125 let m_low = state.get_reg(rmlo).clone();
1126 let n_high = state.get_reg(rnhi).clone();
1127 let m_high = state.get_reg(rmhi).clone();
1128
1129 let high_gt = n_high.bvugt(&m_high);
1130 let high_eq = n_high.eq(&m_high);
1131 let low_gt = n_low.bvugt(&m_low);
1132
1133 let eq_and_gt = Bool::and(&[&high_eq, &low_gt]);
1134 let result_bool = Bool::or(&[&high_gt, &eq_and_gt]);
1135 let result = self.bool_to_bv32(&result_bool);
1136 state.set_reg(rd, result);
1137 }
1138
1139 ArmOp::I64GeS {
1140 rd,
1141 rnlo,
1142 rnhi,
1143 rmlo,
1144 rmhi,
1145 } => {
1146 // Signed greater than or equal: n >= m
1147 // Equivalent to: !(n < m)
1148 let n_low = state.get_reg(rnlo).clone();
1149 let m_low = state.get_reg(rmlo).clone();
1150 let n_high = state.get_reg(rnhi).clone();
1151 let m_high = state.get_reg(rmhi).clone();
1152
1153 let high_lt = n_high.bvslt(&m_high);
1154 let high_eq = n_high.eq(&m_high);
1155 let low_lt = n_low.bvult(&m_low);
1156
1157 let eq_and_lt = Bool::and(&[&high_eq, &low_lt]);
1158 let lt_bool = Bool::or(&[&high_lt, &eq_and_lt]);
1159 let result_bool = lt_bool.not(); // GE is !(LT)
1160 let result = self.bool_to_bv32(&result_bool);
1161 state.set_reg(rd, result);
1162 }
1163
1164 ArmOp::I64GeU {
1165 rd,
1166 rnlo,
1167 rnhi,
1168 rmlo,
1169 rmhi,
1170 } => {
1171 // Unsigned greater than or equal: n >= m
1172 // Equivalent to: !(n < m)
1173 let n_low = state.get_reg(rnlo).clone();
1174 let m_low = state.get_reg(rmlo).clone();
1175 let n_high = state.get_reg(rnhi).clone();
1176 let m_high = state.get_reg(rmhi).clone();
1177
1178 let high_lt = n_high.bvult(&m_high);
1179 let high_eq = n_high.eq(&m_high);
1180 let low_lt = n_low.bvult(&m_low);
1181
1182 let eq_and_lt = Bool::and(&[&high_eq, &low_lt]);
1183 let lt_bool = Bool::or(&[&high_lt, &eq_and_lt]);
1184 let result_bool = lt_bool.not(); // GE is !(LT)
1185 let result = self.bool_to_bv32(&result_bool);
1186 state.set_reg(rd, result);
1187 }
1188
1189 // ================================================================
1190 // i64 Shift Operations
1191 // ================================================================
1192 ArmOp::I64Shl {
1193 rd_lo,
1194 rd_hi,
1195 rn_lo,
1196 rn_hi,
1197 rm_lo,
1198 rm_hi: _,
1199 } => {
1200 // 64-bit left shift: (n_hi:n_lo) << shift
1201 // WASM spec: shift amount is modulo 64
1202 let n_lo = state.get_reg(rn_lo).clone();
1203 let n_hi = state.get_reg(rn_hi).clone();
1204 let shift_amt = state.get_reg(rm_lo).clone();
1205
1206 // Modulo 64: shift_amt = shift_amt & 63
1207 let shift_mod = shift_amt.bvand(BV::from_i64(63, 32));
1208
1209 // If shift < 32: normal shift with bits moving from low to high
1210 // If shift >= 32: low becomes 0, high gets shifted low part
1211 let shift_32 = BV::from_i64(32, 32);
1212 let is_large = shift_mod.bvuge(&shift_32); // shift >= 32
1213
1214 // Small shift (< 32):
1215 // result_lo = n_lo << shift
1216 // result_hi = (n_hi << shift) | (n_lo >> (32 - shift))
1217 let result_lo_small = n_lo.bvshl(&shift_mod);
1218 let shift_complement = shift_32.bvsub(&shift_mod);
1219 let bits_to_high = n_lo.bvlshr(&shift_complement);
1220 let result_hi_small = n_hi.bvshl(&shift_mod).bvor(&bits_to_high);
1221
1222 // Large shift (>= 32):
1223 // result_lo = 0
1224 // result_hi = n_lo << (shift - 32)
1225 let zero = BV::from_i64(0, 32);
1226 let shift_minus_32 = shift_mod.bvsub(&shift_32);
1227 let result_lo_large = zero.clone();
1228 let result_hi_large = n_lo.bvshl(&shift_minus_32);
1229
1230 // Select based on shift size
1231 let result_lo = is_large.ite(&result_lo_large, &result_lo_small);
1232 let result_hi = is_large.ite(&result_hi_large, &result_hi_small);
1233
1234 state.set_reg(rd_lo, result_lo);
1235 state.set_reg(rd_hi, result_hi);
1236 }
1237
1238 ArmOp::I64ShrU {
1239 rd_lo,
1240 rd_hi,
1241 rn_lo,
1242 rn_hi,
1243 rm_lo,
1244 rm_hi: _,
1245 } => {
1246 // 64-bit logical (unsigned) right shift
1247 let n_lo = state.get_reg(rn_lo).clone();
1248 let n_hi = state.get_reg(rn_hi).clone();
1249 let shift_amt = state.get_reg(rm_lo).clone();
1250
1251 let shift_mod = shift_amt.bvand(BV::from_i64(63, 32));
1252 let shift_32 = BV::from_i64(32, 32);
1253 let is_large = shift_mod.bvuge(&shift_32);
1254
1255 // Small shift (< 32):
1256 // result_hi = n_hi >> shift
1257 // result_lo = (n_lo >> shift) | (n_hi << (32 - shift))
1258 let result_hi_small = n_hi.bvlshr(&shift_mod);
1259 let shift_complement = shift_32.bvsub(&shift_mod);
1260 let bits_to_low = n_hi.bvshl(&shift_complement);
1261 let result_lo_small = n_lo.bvlshr(&shift_mod).bvor(&bits_to_low);
1262
1263 // Large shift (>= 32):
1264 // result_hi = 0
1265 // result_lo = n_hi >> (shift - 32)
1266 let zero = BV::from_i64(0, 32);
1267 let shift_minus_32 = shift_mod.bvsub(&shift_32);
1268 let result_hi_large = zero.clone();
1269 let result_lo_large = n_hi.bvlshr(&shift_minus_32);
1270
1271 let result_lo = is_large.ite(&result_lo_large, &result_lo_small);
1272 let result_hi = is_large.ite(&result_hi_large, &result_hi_small);
1273
1274 state.set_reg(rd_lo, result_lo);
1275 state.set_reg(rd_hi, result_hi);
1276 }
1277
1278 ArmOp::I64ShrS {
1279 rd_lo,
1280 rd_hi,
1281 rn_lo,
1282 rn_hi,
1283 rm_lo,
1284 rm_hi: _,
1285 } => {
1286 // 64-bit arithmetic (signed) right shift
1287 let n_lo = state.get_reg(rn_lo).clone();
1288 let n_hi = state.get_reg(rn_hi).clone();
1289 let shift_amt = state.get_reg(rm_lo).clone();
1290
1291 let shift_mod = shift_amt.bvand(BV::from_i64(63, 32));
1292 let shift_32 = BV::from_i64(32, 32);
1293 let is_large = shift_mod.bvuge(&shift_32);
1294
1295 // Small shift (< 32):
1296 // result_hi = n_hi >> shift (arithmetic)
1297 // result_lo = (n_lo >> shift) | (n_hi << (32 - shift))
1298 let result_hi_small = n_hi.bvashr(&shift_mod);
1299 let shift_complement = shift_32.bvsub(&shift_mod);
1300 let bits_to_low = n_hi.bvshl(&shift_complement);
1301 let result_lo_small = n_lo.bvlshr(&shift_mod).bvor(&bits_to_low);
1302
1303 // Large shift (>= 32):
1304 // result_hi = n_hi >> 31 (sign extension: all 0s or all 1s)
1305 // result_lo = n_hi >> (shift - 32) (arithmetic)
1306 let shift_31 = BV::from_i64(31, 32);
1307 let result_hi_large = n_hi.bvashr(&shift_31);
1308 let shift_minus_32 = shift_mod.bvsub(&shift_32);
1309 let result_lo_large = n_hi.bvashr(&shift_minus_32);
1310
1311 let result_lo = is_large.ite(&result_lo_large, &result_lo_small);
1312 let result_hi = is_large.ite(&result_hi_large, &result_hi_small);
1313
1314 state.set_reg(rd_lo, result_lo);
1315 state.set_reg(rd_hi, result_hi);
1316 }
1317
1318 // ========================================================================
1319 // i64 Rotation Operations
1320 // ========================================================================
1321 ArmOp::I64Rotl {
1322 rdlo,
1323 rdhi,
1324 rnlo,
1325 rnhi,
1326 shift,
1327 } => {
1328 // 64-bit rotate left: rotl(hi:lo, shift)
1329 // Result = (value << shift) | (value >> (64 - shift))
1330 let n_lo = state.get_reg(rnlo).clone();
1331 let n_hi = state.get_reg(rnhi).clone();
1332 let shift_amt = state.get_reg(shift).clone();
1333
1334 // Normalize shift to 0-63 range
1335 let shift_mod = shift_amt.bvand(BV::from_i64(63, 32));
1336 let shift_32 = BV::from_i64(32, 32);
1337 let is_large = shift_mod.bvuge(&shift_32); // shift >= 32
1338
1339 // For shift < 32:
1340 // result_lo = (n_lo << shift) | (n_hi >> (32 - shift))
1341 // result_hi = (n_hi << shift) | (n_lo >> (32 - shift))
1342 let shift_complement = shift_32.bvsub(&shift_mod);
1343
1344 let lo_shifted_left = n_lo.bvshl(&shift_mod);
1345 let hi_bits_to_lo = n_hi.bvlshr(&shift_complement);
1346 let result_lo_small = lo_shifted_left.bvor(&hi_bits_to_lo);
1347
1348 let hi_shifted_left = n_hi.bvshl(&shift_mod);
1349 let lo_bits_to_hi = n_lo.bvlshr(&shift_complement);
1350 let result_hi_small = hi_shifted_left.bvor(&lo_bits_to_hi);
1351
1352 // For shift >= 32:
1353 // Swap and rotate by (shift - 32)
1354 let shift_minus_32 = shift_mod.bvsub(&shift_32);
1355 let complement_large = shift_32.bvsub(&shift_minus_32);
1356
1357 let hi_shifted_left_large = n_hi.bvshl(&shift_minus_32);
1358 let lo_bits_to_hi_large = n_lo.bvlshr(&complement_large);
1359 let result_lo_large = hi_shifted_left_large.bvor(&lo_bits_to_hi_large);
1360
1361 let lo_shifted_left_large = n_lo.bvshl(&shift_minus_32);
1362 let hi_bits_to_lo_large = n_hi.bvlshr(&complement_large);
1363 let result_hi_large = lo_shifted_left_large.bvor(&hi_bits_to_lo_large);
1364
1365 // Select based on shift size
1366 let result_lo = is_large.ite(&result_lo_large, &result_lo_small);
1367 let result_hi = is_large.ite(&result_hi_large, &result_hi_small);
1368
1369 state.set_reg(rdlo, result_lo);
1370 state.set_reg(rdhi, result_hi);
1371 }
1372
1373 ArmOp::I64Rotr {
1374 rdlo,
1375 rdhi,
1376 rnlo,
1377 rnhi,
1378 shift,
1379 } => {
1380 // 64-bit rotate right: rotr(hi:lo, shift)
1381 // Result = (value >> shift) | (value << (64 - shift))
1382 let n_lo = state.get_reg(rnlo).clone();
1383 let n_hi = state.get_reg(rnhi).clone();
1384 let shift_amt = state.get_reg(shift).clone();
1385
1386 // Normalize shift to 0-63 range
1387 let shift_mod = shift_amt.bvand(BV::from_i64(63, 32));
1388 let shift_32 = BV::from_i64(32, 32);
1389 let is_large = shift_mod.bvuge(&shift_32); // shift >= 32
1390
1391 // For shift < 32:
1392 // result_lo = (n_lo >> shift) | (n_hi << (32 - shift))
1393 // result_hi = (n_hi >> shift) | (n_lo << (32 - shift))
1394 let shift_complement = shift_32.bvsub(&shift_mod);
1395
1396 let lo_shifted_right = n_lo.bvlshr(&shift_mod);
1397 let hi_bits_to_lo = n_hi.bvshl(&shift_complement);
1398 let result_lo_small = lo_shifted_right.bvor(&hi_bits_to_lo);
1399
1400 let hi_shifted_right = n_hi.bvlshr(&shift_mod);
1401 let lo_bits_to_hi = n_lo.bvshl(&shift_complement);
1402 let result_hi_small = hi_shifted_right.bvor(&lo_bits_to_hi);
1403
1404 // For shift >= 32:
1405 // Swap and rotate by (shift - 32)
1406 let shift_minus_32 = shift_mod.bvsub(&shift_32);
1407 let complement_large = shift_32.bvsub(&shift_minus_32);
1408
1409 let hi_shifted_right_large = n_hi.bvlshr(&shift_minus_32);
1410 let lo_bits_to_hi_large = n_lo.bvshl(&complement_large);
1411 let result_lo_large = hi_shifted_right_large.bvor(&lo_bits_to_hi_large);
1412
1413 let lo_shifted_right_large = n_lo.bvlshr(&shift_minus_32);
1414 let hi_bits_to_lo_large = n_hi.bvshl(&complement_large);
1415 let result_hi_large = lo_shifted_right_large.bvor(&hi_bits_to_lo_large);
1416
1417 // Select based on shift size
1418 let result_lo = is_large.ite(&result_lo_large, &result_lo_small);
1419 let result_hi = is_large.ite(&result_hi_large, &result_hi_small);
1420
1421 state.set_reg(rdlo, result_lo);
1422 state.set_reg(rdhi, result_hi);
1423 }
1424
1425 ArmOp::I64Clz { rd, rnlo, rnhi } => {
1426 // Count leading zeros for 64-bit value
1427 // If high part has zeros, result = clz(high) + clz(low)
1428 // If high part is zero, result = 32 + clz(low)
1429 let n_lo = state.get_reg(rnlo).clone();
1430 let n_hi = state.get_reg(rnhi).clone();
1431
1432 let hi_clz = self.encode_clz(&n_hi);
1433 let lo_clz = self.encode_clz(&n_lo);
1434
1435 // If high == 32 (all zeros), add low clz; else use high clz
1436 let thirty_two = BV::from_i64(32, 32);
1437 let hi_is_zero = hi_clz.eq(&thirty_two);
1438 let result = hi_is_zero.ite(
1439 thirty_two.bvadd(&lo_clz), // High is zero: 32 + clz(low)
1440 &hi_clz, // High has bits: clz(high)
1441 );
1442 state.set_reg(rd, result);
1443 }
1444
1445 ArmOp::I64Ctz { rd, rnlo, rnhi } => {
1446 // Count trailing zeros for 64-bit value
1447 // If low part is zero, result = 32 + ctz(high)
1448 // Else result = ctz(low)
1449 let n_lo = state.get_reg(rnlo).clone();
1450 let n_hi = state.get_reg(rnhi).clone();
1451
1452 let lo_ctz = self.encode_ctz(&n_lo);
1453 let hi_ctz = self.encode_ctz(&n_hi);
1454
1455 // If low == 32 (all zeros), add high ctz; else use low ctz
1456 let thirty_two = BV::from_i64(32, 32);
1457 let lo_is_zero = lo_ctz.eq(&thirty_two);
1458 let result = lo_is_zero.ite(
1459 thirty_two.bvadd(&hi_ctz), // Low is zero: 32 + ctz(high)
1460 &lo_ctz, // Low has bits: ctz(low)
1461 );
1462 state.set_reg(rd, result);
1463 }
1464
1465 ArmOp::I64Popcnt { rd, rnlo, rnhi } => {
1466 // Population count for 64-bit value
1467 // Result = popcnt(low) + popcnt(high)
1468 let n_lo = state.get_reg(rnlo).clone();
1469 let n_hi = state.get_reg(rnhi).clone();
1470
1471 let lo_popcnt = self.encode_popcnt(&n_lo);
1472 let hi_popcnt = self.encode_popcnt(&n_hi);
1473
1474 let result = lo_popcnt.bvadd(&hi_popcnt);
1475 state.set_reg(rd, result);
1476 }
1477
1478 // ========================================================================
1479 // i64 Memory Operations
1480 // ========================================================================
1481 ArmOp::I64Ldr { rdlo, rdhi, addr } => {
1482 // Load 64-bit value from memory
1483 // Simplified: return symbolic values for both registers
1484 // Real implementation would load from memory at [addr] and [addr+4]
1485 let result_lo = BV::new_const(format!("i64load_lo_{:?}", addr), 32);
1486 let result_hi = BV::new_const(format!("i64load_hi_{:?}", addr), 32);
1487 state.set_reg(rdlo, result_lo);
1488 state.set_reg(rdhi, result_hi);
1489 }
1490
1491 ArmOp::I64Str {
1492 rdlo: _,
1493 rdhi: _,
1494 addr: _,
1495 } => {
1496 // Store 64-bit value to memory
1497 // Simplified: memory updates not fully modeled yet
1498 // Real implementation would store rdlo to [addr] and rdhi to [addr+4]
1499 // No register changes - store operation has no output
1500 }
1501
1502 // ========================================================================
1503 // f32 Operations (Phase 2 - Floating Point)
1504 // ========================================================================
1505 // Note: f32 values are represented as 32-bit bitvectors (IEEE 754 format)
1506 // For verification, we use symbolic bitvector operations
1507 // A complete implementation would use Z3's FloatingPoint sort
1508
1509 // f32 Constants
1510 ArmOp::F32Const { sd, value } => {
1511 // Load f32 constant (represented as 32-bit bitvector)
1512 // Convert f32 to its IEEE 754 bit representation
1513 let bits = value.to_bits() as i64;
1514 let bv_val = BV::from_i64(bits, 32);
1515 state.set_vfp_reg(sd, bv_val);
1516 }
1517
1518 // f32 Arithmetic (symbolic for verification)
1519 ArmOp::F32Add { sd, sn, sm } => {
1520 // f32 addition: sd = sn + sm
1521 // For verification, return symbolic value
1522 // Full implementation would use Z3 FloatingPoint operations
1523 let result = BV::new_const(format!("f32_add_{:?}_{:?}", sn, sm), 32);
1524 state.set_vfp_reg(sd, result);
1525 }
1526
1527 ArmOp::F32Sub { sd, sn, sm } => {
1528 // f32 subtraction: sd = sn - sm
1529 let result = BV::new_const(format!("f32_sub_{:?}_{:?}", sn, sm), 32);
1530 state.set_vfp_reg(sd, result);
1531 }
1532
1533 ArmOp::F32Mul { sd, sn, sm } => {
1534 // f32 multiplication: sd = sn * sm
1535 let result = BV::new_const(format!("f32_mul_{:?}_{:?}", sn, sm), 32);
1536 state.set_vfp_reg(sd, result);
1537 }
1538
1539 ArmOp::F32Div { sd, sn, sm } => {
1540 // f32 division: sd = sn / sm
1541 let result = BV::new_const(format!("f32_div_{:?}_{:?}", sn, sm), 32);
1542 state.set_vfp_reg(sd, result);
1543 }
1544
1545 // f32 Simple Math
1546 ArmOp::F32Abs { sd, sm } => {
1547 // f32 absolute value: sd = |sm|
1548 // Clear the sign bit (bit 31)
1549 let val = state.get_vfp_reg(sm).clone();
1550 let mask = BV::from_u64(0x7FFFFFFF, 32); // Clear sign bit
1551 let result = val.bvand(&mask);
1552 state.set_vfp_reg(sd, result);
1553 }
1554
1555 ArmOp::F32Neg { sd, sm } => {
1556 // f32 negation: sd = -sm
1557 // Flip the sign bit (bit 31)
1558 let val = state.get_vfp_reg(sm).clone();
1559 let mask = BV::from_u64(0x80000000, 32); // Sign bit
1560 let result = val.bvxor(&mask);
1561 state.set_vfp_reg(sd, result);
1562 }
1563
1564 ArmOp::F32Sqrt { sd, sm } => {
1565 // f32 square root: sd = sqrt(sm)
1566 // Symbolic representation for verification
1567 let result = BV::new_const(format!("f32_sqrt_{:?}", sm), 32);
1568 state.set_vfp_reg(sd, result);
1569 }
1570
1571 ArmOp::F32Min { sd, sn, sm } => {
1572 // f32 minimum: sd = min(sn, sm)
1573 // IEEE 754 semantics: NaN propagation, -0.0 < +0.0
1574 // Symbolic representation for verification
1575 let result = BV::new_const(format!("f32_min_{:?}_{:?}", sn, sm), 32);
1576 state.set_vfp_reg(sd, result);
1577 }
1578
1579 ArmOp::F32Max { sd, sn, sm } => {
1580 // f32 maximum: sd = max(sn, sm)
1581 // IEEE 754 semantics: NaN propagation, +0.0 > -0.0
1582 // Symbolic representation for verification
1583 let result = BV::new_const(format!("f32_max_{:?}_{:?}", sn, sm), 32);
1584 state.set_vfp_reg(sd, result);
1585 }
1586
1587 ArmOp::F32Copysign { sd, sn, sm } => {
1588 // f32 copysign: sd = |sn| with sign of sm
1589 // Take magnitude of sn and sign bit from sm
1590 let val_n = state.get_vfp_reg(sn).clone();
1591 let val_m = state.get_vfp_reg(sm).clone();
1592
1593 // Extract magnitude from sn (clear sign bit)
1594 let mag_mask = BV::from_u64(0x7FFFFFFF, 32);
1595 let magnitude = val_n.bvand(&mag_mask);
1596
1597 // Extract sign from sm (bit 31 only)
1598 let sign_mask = BV::from_u64(0x80000000, 32);
1599 let sign = val_m.bvand(&sign_mask);
1600
1601 // Combine: magnitude | sign
1602 let result = magnitude.bvor(&sign);
1603 state.set_vfp_reg(sd, result);
1604 }
1605
1606 ArmOp::F32Load { sd, addr } => {
1607 // f32 load: sd = memory[addr]
1608 // Symbolic memory access for verification
1609 let result = BV::new_const(format!("f32_load_{:?}", addr), 32);
1610 state.set_vfp_reg(sd, result);
1611 }
1612
1613 // f32 Comparisons (result stored in integer register)
1614 ArmOp::F32Eq { rd, sn, sm } => {
1615 // f32 equal: rd = (sn == sm) ? 1 : 0
1616 // IEEE 754: NaN != NaN, so symbolic comparison needed
1617 let result = BV::new_const(format!("f32_eq_{:?}_{:?}", sn, sm), 32);
1618 state.set_reg(rd, result);
1619 }
1620
1621 ArmOp::F32Ne { rd, sn, sm } => {
1622 // f32 not equal: rd = (sn != sm) ? 1 : 0
1623 let result = BV::new_const(format!("f32_ne_{:?}_{:?}", sn, sm), 32);
1624 state.set_reg(rd, result);
1625 }
1626
1627 ArmOp::F32Lt { rd, sn, sm } => {
1628 // f32 less than: rd = (sn < sm) ? 1 : 0
1629 let result = BV::new_const(format!("f32_lt_{:?}_{:?}", sn, sm), 32);
1630 state.set_reg(rd, result);
1631 }
1632
1633 ArmOp::F32Le { rd, sn, sm } => {
1634 // f32 less than or equal: rd = (sn <= sm) ? 1 : 0
1635 let result = BV::new_const(format!("f32_le_{:?}_{:?}", sn, sm), 32);
1636 state.set_reg(rd, result);
1637 }
1638
1639 ArmOp::F32Gt { rd, sn, sm } => {
1640 // f32 greater than: rd = (sn > sm) ? 1 : 0
1641 let result = BV::new_const(format!("f32_gt_{:?}_{:?}", sn, sm), 32);
1642 state.set_reg(rd, result);
1643 }
1644
1645 ArmOp::F32Ge { rd, sn, sm } => {
1646 // f32 greater than or equal: rd = (sn >= sm) ? 1 : 0
1647 let result = BV::new_const(format!("f32_ge_{:?}_{:?}", sn, sm), 32);
1648 state.set_reg(rd, result);
1649 }
1650
1651 ArmOp::F32Store { sd, addr } => {
1652 // f32 store: memory[addr] = sd
1653 // Memory write - modeled symbolically for verification
1654 // In a full implementation, would update memory state
1655 // For now, this is a no-op as we model memory symbolically
1656 let _val = state.get_vfp_reg(sd);
1657 let _addr_str = format!("{:?}", addr);
1658 // TODO: Add memory state tracking when implementing full memory model
1659 }
1660
1661 // f32 Advanced Math Operations
1662 ArmOp::F32Ceil { sd, sm } => {
1663 // f32 ceil: sd = ceil(sm) - round toward +infinity
1664 // Symbolic representation for IEEE 754 rounding
1665 let result = BV::new_const(format!("f32_ceil_{:?}", sm), 32);
1666 state.set_vfp_reg(sd, result);
1667 }
1668
1669 ArmOp::F32Floor { sd, sm } => {
1670 // f32 floor: sd = floor(sm) - round toward -infinity
1671 // Symbolic representation for IEEE 754 rounding
1672 let result = BV::new_const(format!("f32_floor_{:?}", sm), 32);
1673 state.set_vfp_reg(sd, result);
1674 }
1675
1676 ArmOp::F32Trunc { sd, sm } => {
1677 // f32 trunc: sd = trunc(sm) - round toward zero
1678 // Symbolic representation for IEEE 754 rounding
1679 let result = BV::new_const(format!("f32_trunc_{:?}", sm), 32);
1680 state.set_vfp_reg(sd, result);
1681 }
1682
1683 ArmOp::F32Nearest { sd, sm } => {
1684 // f32 nearest: sd = nearest(sm) - round to nearest, ties to even
1685 // Symbolic representation for IEEE 754 rounding
1686 let result = BV::new_const(format!("f32_nearest_{:?}", sm), 32);
1687 state.set_vfp_reg(sd, result);
1688 }
1689
1690 // f32 Conversions from Integers
1691 ArmOp::F32ConvertI32S { sd, rm } => {
1692 // f32 convert from signed i32: sd = (f32)rm
1693 let int_val = state.get_reg(rm);
1694 let result = BV::new_const(format!("f32_convert_i32s_{:?}", int_val), 32);
1695 state.set_vfp_reg(sd, result);
1696 }
1697
1698 ArmOp::F32ConvertI32U { sd, rm } => {
1699 // f32 convert from unsigned i32: sd = (f32)(unsigned)rm
1700 let int_val = state.get_reg(rm);
1701 let result = BV::new_const(format!("f32_convert_i32u_{:?}", int_val), 32);
1702 state.set_vfp_reg(sd, result);
1703 }
1704
1705 ArmOp::F32ConvertI64S { sd, rmlo, rmhi } => {
1706 // f32 convert from signed i64: sd = (f32)r64
1707 let lo = state.get_reg(rmlo);
1708 let hi = state.get_reg(rmhi);
1709 let result = BV::new_const(format!("f32_convert_i64s_{:?}_{:?}", lo, hi), 32);
1710 state.set_vfp_reg(sd, result);
1711 }
1712
1713 ArmOp::F32ConvertI64U { sd, rmlo, rmhi } => {
1714 // f32 convert from unsigned i64: sd = (f32)(unsigned)r64
1715 let lo = state.get_reg(rmlo);
1716 let hi = state.get_reg(rmhi);
1717 let result = BV::new_const(format!("f32_convert_i64u_{:?}_{:?}", lo, hi), 32);
1718 state.set_vfp_reg(sd, result);
1719 }
1720
1721 // f32 Reinterpretations
1722 ArmOp::F32ReinterpretI32 { sd, rm } => {
1723 // f32 reinterpret i32: sd = reinterpret_cast<f32>(rm)
1724 // Bitwise copy without conversion
1725 let bits = state.get_reg(rm).clone();
1726 state.set_vfp_reg(sd, bits);
1727 }
1728
1729 ArmOp::I32ReinterpretF32 { rd, sm } => {
1730 // i32 reinterpret f32: rd = reinterpret_cast<i32>(sm)
1731 // Bitwise copy without conversion
1732 let bits = state.get_vfp_reg(sm).clone();
1733 state.set_reg(rd, bits);
1734 }
1735
1736 // ===================================================================
1737 // f64 Operations (Phase 2c - Double-Precision Floating Point)
1738 // ===================================================================
1739
1740 // f64 Arithmetic (symbolic for verification)
1741 ArmOp::F64Add { dd, dn, dm } => {
1742 // f64 addition: dd = dn + dm
1743 // For verification, return symbolic value
1744 // Full implementation would use Z3 FloatingPoint operations
1745 let result = BV::new_const(format!("f64_add_{:?}_{:?}", dn, dm), 64);
1746 state.set_vfp_reg(dd, result);
1747 }
1748
1749 ArmOp::F64Sub { dd, dn, dm } => {
1750 // f64 subtraction: dd = dn - dm
1751 let result = BV::new_const(format!("f64_sub_{:?}_{:?}", dn, dm), 64);
1752 state.set_vfp_reg(dd, result);
1753 }
1754
1755 ArmOp::F64Mul { dd, dn, dm } => {
1756 // f64 multiplication: dd = dn * dm
1757 let result = BV::new_const(format!("f64_mul_{:?}_{:?}", dn, dm), 64);
1758 state.set_vfp_reg(dd, result);
1759 }
1760
1761 ArmOp::F64Div { dd, dn, dm } => {
1762 // f64 division: dd = dn / dm
1763 let result = BV::new_const(format!("f64_div_{:?}_{:?}", dn, dm), 64);
1764 state.set_vfp_reg(dd, result);
1765 }
1766
1767 // f64 Simple Math
1768 ArmOp::F64Abs { dd, dm } => {
1769 // f64 absolute value: dd = |dm|
1770 // Clear the sign bit (bit 63)
1771 let val = state.get_vfp_reg(dm).clone();
1772 let mask = BV::from_u64(0x7FFFFFFFFFFFFFFF, 64); // Clear sign bit
1773 let result = val.bvand(&mask);
1774 state.set_vfp_reg(dd, result);
1775 }
1776
1777 ArmOp::F64Neg { dd, dm } => {
1778 // f64 negation: dd = -dm
1779 // Flip the sign bit (bit 63)
1780 let val = state.get_vfp_reg(dm).clone();
1781 let mask = BV::from_u64(0x8000000000000000, 64); // Sign bit
1782 let result = val.bvxor(&mask);
1783 state.set_vfp_reg(dd, result);
1784 }
1785
1786 ArmOp::F64Sqrt { dd, dm } => {
1787 // f64 square root: dd = sqrt(dm)
1788 // Symbolic representation for verification
1789 let result = BV::new_const(format!("f64_sqrt_{:?}", dm), 64);
1790 state.set_vfp_reg(dd, result);
1791 }
1792
1793 ArmOp::F64Min { dd, dn, dm } => {
1794 // f64 minimum: dd = min(dn, dm)
1795 // IEEE 754 semantics: NaN propagation, -0.0 < +0.0
1796 // Symbolic representation for verification
1797 let result = BV::new_const(format!("f64_min_{:?}_{:?}", dn, dm), 64);
1798 state.set_vfp_reg(dd, result);
1799 }
1800
1801 ArmOp::F64Max { dd, dn, dm } => {
1802 // f64 maximum: dd = max(dn, dm)
1803 // IEEE 754 semantics: NaN propagation, +0.0 > -0.0
1804 // Symbolic representation for verification
1805 let result = BV::new_const(format!("f64_max_{:?}_{:?}", dn, dm), 64);
1806 state.set_vfp_reg(dd, result);
1807 }
1808
1809 ArmOp::F64Copysign { dd, dn, dm } => {
1810 // f64 copysign: dd = |dn| with sign of dm
1811 // Take magnitude of dn and sign bit from dm
1812 let val_n = state.get_vfp_reg(dn).clone();
1813 let val_m = state.get_vfp_reg(dm).clone();
1814
1815 // Extract magnitude from dn (clear sign bit)
1816 let mag_mask = BV::from_u64(0x7FFFFFFFFFFFFFFF, 64);
1817 let magnitude = val_n.bvand(&mag_mask);
1818
1819 // Extract sign from dm (bit 63 only)
1820 let sign_mask = BV::from_u64(0x8000000000000000, 64);
1821 let sign = val_m.bvand(&sign_mask);
1822
1823 // Combine: magnitude | sign
1824 let result = magnitude.bvor(&sign);
1825 state.set_vfp_reg(dd, result);
1826 }
1827
1828 // f64 Rounding Operations (symbolic for verification)
1829 ArmOp::F64Ceil { dd, dm } => {
1830 // f64 ceil: dd = ceil(dm) - round toward +infinity
1831 let result = BV::new_const(format!("f64_ceil_{:?}", dm), 64);
1832 state.set_vfp_reg(dd, result);
1833 }
1834
1835 ArmOp::F64Floor { dd, dm } => {
1836 // f64 floor: dd = floor(dm) - round toward -infinity
1837 let result = BV::new_const(format!("f64_floor_{:?}", dm), 64);
1838 state.set_vfp_reg(dd, result);
1839 }
1840
1841 ArmOp::F64Trunc { dd, dm } => {
1842 // f64 trunc: dd = trunc(dm) - round toward zero
1843 let result = BV::new_const(format!("f64_trunc_{:?}", dm), 64);
1844 state.set_vfp_reg(dd, result);
1845 }
1846
1847 ArmOp::F64Nearest { dd, dm } => {
1848 // f64 nearest: dd = round(dm) - round to nearest, ties to even
1849 let result = BV::new_const(format!("f64_nearest_{:?}", dm), 64);
1850 state.set_vfp_reg(dd, result);
1851 }
1852
1853 // f64 Memory Operations
1854 ArmOp::F64Load { dd, addr } => {
1855 // f64 load: dd = memory[addr]
1856 // Symbolic memory access for verification
1857 let result = BV::new_const(format!("f64_load_{:?}", addr), 64);
1858 state.set_vfp_reg(dd, result);
1859 }
1860
1861 ArmOp::F64Store { dd: _, addr: _ } => {
1862 // f64 store: memory[addr] = dd
1863 // Store operations don't produce register values
1864 // No state change for symbolic execution
1865 }
1866
1867 ArmOp::F64Const { dd, value } => {
1868 // f64 constant: dd = value
1869 let bits = value.to_bits() as i64;
1870 let result = BV::from_i64(bits, 64);
1871 state.set_vfp_reg(dd, result);
1872 }
1873
1874 // f64 Comparisons (result stored in integer register)
1875 ArmOp::F64Eq { rd, dn, dm } => {
1876 // f64 equal: rd = (dn == dm) ? 1 : 0
1877 // IEEE 754: NaN != NaN, so symbolic comparison needed
1878 let result = BV::new_const(format!("f64_eq_{:?}_{:?}", dn, dm), 32);
1879 state.set_reg(rd, result);
1880 }
1881
1882 ArmOp::F64Ne { rd, dn, dm } => {
1883 // f64 not equal: rd = (dn != dm) ? 1 : 0
1884 let result = BV::new_const(format!("f64_ne_{:?}_{:?}", dn, dm), 32);
1885 state.set_reg(rd, result);
1886 }
1887
1888 ArmOp::F64Lt { rd, dn, dm } => {
1889 // f64 less than: rd = (dn < dm) ? 1 : 0
1890 let result = BV::new_const(format!("f64_lt_{:?}_{:?}", dn, dm), 32);
1891 state.set_reg(rd, result);
1892 }
1893
1894 ArmOp::F64Le { rd, dn, dm } => {
1895 // f64 less than or equal: rd = (dn <= dm) ? 1 : 0
1896 let result = BV::new_const(format!("f64_le_{:?}_{:?}", dn, dm), 32);
1897 state.set_reg(rd, result);
1898 }
1899
1900 ArmOp::F64Gt { rd, dn, dm } => {
1901 // f64 greater than: rd = (dn > dm) ? 1 : 0
1902 let result = BV::new_const(format!("f64_gt_{:?}_{:?}", dn, dm), 32);
1903 state.set_reg(rd, result);
1904 }
1905
1906 ArmOp::F64Ge { rd, dn, dm } => {
1907 // f64 greater than or equal: rd = (dn >= dm) ? 1 : 0
1908 let result = BV::new_const(format!("f64_ge_{:?}_{:?}", dn, dm), 32);
1909 state.set_reg(rd, result);
1910 }
1911
1912 // f64 Conversions
1913 ArmOp::F64ConvertI32S { dd, rm } => {
1914 // f64 convert i32 signed: dd = (f64)rm
1915 // Symbolic conversion
1916 let result = BV::new_const(format!("f64_convert_i32s_{:?}", rm), 64);
1917 state.set_vfp_reg(dd, result);
1918 }
1919
1920 ArmOp::F64ConvertI32U { dd, rm } => {
1921 // f64 convert i32 unsigned: dd = (f64)(unsigned)rm
1922 // Symbolic conversion
1923 let result = BV::new_const(format!("f64_convert_i32u_{:?}", rm), 64);
1924 state.set_vfp_reg(dd, result);
1925 }
1926
1927 ArmOp::F64ConvertI64S {
1928 dd,
1929 rmlo: _,
1930 rmhi: _,
1931 } => {
1932 // f64 convert i64 signed: dd = (f64)(rmhi:rmlo)
1933 // Symbolic conversion (complex operation)
1934 let result = BV::new_const("f64_convert_i64s_result", 64);
1935 state.set_vfp_reg(dd, result);
1936 }
1937
1938 ArmOp::F64ConvertI64U {
1939 dd,
1940 rmlo: _,
1941 rmhi: _,
1942 } => {
1943 // f64 convert i64 unsigned: dd = (f64)(unsigned)(rmhi:rmlo)
1944 // Symbolic conversion (complex operation)
1945 let result = BV::new_const("f64_convert_i64u_result", 64);
1946 state.set_vfp_reg(dd, result);
1947 }
1948
1949 ArmOp::F64PromoteF32 { dd, sm } => {
1950 // f64 promote f32: dd = (f64)sm
1951 // Promote from 32-bit to 64-bit (symbolic for verification)
1952 let result = BV::new_const(format!("f64_promote_f32_{:?}", sm), 64);
1953 state.set_vfp_reg(dd, result);
1954 }
1955
1956 ArmOp::F64ReinterpretI64 { dd, rmlo, rmhi } => {
1957 // f64 reinterpret i64: dd = reinterpret_cast<f64>(rmhi:rmlo)
1958 // Bitwise copy without conversion - combine two 32-bit registers
1959 let lo = state.get_reg(rmlo).clone();
1960 let hi = state.get_reg(rmhi).clone();
1961
1962 // Extend to 64 bits and combine: (hi << 32) | lo
1963 let lo_64 = lo.zero_ext(32); // Extend to 64 bits
1964 let hi_64 = hi.zero_ext(32);
1965 let shift_32 = BV::from_u64(32, 64);
1966 let hi_shifted = hi_64.bvshl(&shift_32);
1967 let result = hi_shifted.bvor(&lo_64);
1968
1969 state.set_vfp_reg(dd, result);
1970 }
1971
1972 ArmOp::I64ReinterpretF64 { rdlo, rdhi, dm } => {
1973 // i64 reinterpret f64: (rdhi:rdlo) = reinterpret_cast<i64>(dm)
1974 // Bitwise copy without conversion - split 64-bit into two 32-bit registers
1975 let bits = state.get_vfp_reg(dm).clone();
1976
1977 // Extract low 32 bits
1978 let lo = bits.extract(31, 0);
1979 state.set_reg(rdlo, lo);
1980
1981 // Extract high 32 bits
1982 let hi = bits.extract(63, 32);
1983 state.set_reg(rdhi, hi);
1984 }
1985
1986 ArmOp::I64TruncF64S {
1987 rdlo: _,
1988 rdhi: _,
1989 dm: _,
1990 } => {
1991 // i64 trunc f64 signed: (rdhi:rdlo) = (i64)dm
1992 // Symbolic conversion (complex operation)
1993 // Would require proper truncation with saturation
1994 }
1995
1996 ArmOp::I64TruncF64U {
1997 rdlo: _,
1998 rdhi: _,
1999 dm: _,
2000 } => {
2001 // i64 trunc f64 unsigned: (rdhi:rdlo) = (unsigned i64)dm
2002 // Symbolic conversion (complex operation)
2003 // Would require proper truncation with saturation
2004 }
2005
2006 ArmOp::I32TruncF64S { rd, dm } => {
2007 // i32 trunc f64 signed: rd = (i32)dm
2008 // Symbolic conversion
2009 let result = BV::new_const(format!("i32_trunc_f64s_{:?}", dm), 32);
2010 state.set_reg(rd, result);
2011 }
2012
2013 ArmOp::I32TruncF64U { rd, dm } => {
2014 // i32 trunc f64 unsigned: rd = (unsigned i32)dm
2015 // Symbolic conversion
2016 let result = BV::new_const(format!("i32_trunc_f64u_{:?}", dm), 32);
2017 state.set_reg(rd, result);
2018 }
2019
2020 // #923: the f32 twins of the two arms above. Both were already on
2021 // `exec_trap_subset_op`'s "delegate to encode_op" allowlist for the
2022 // SHIPPED `i32.trunc_f32_s/u` guard sequences, but had no arm here,
2023 // so the delegation silently no-oped and the destination register
2024 // kept whatever it held before the conversion. Uninterpreted, like
2025 // the f64 twins: the trunc trap VC derives its condition from the
2026 // guard's VCMP/branch structure, not from the converted value.
2027 ArmOp::I32TruncF32S { rd, sm } => {
2028 let result = BV::new_const(format!("i32_trunc_f32s_{:?}", sm), 32);
2029 state.set_reg(rd, result);
2030 }
2031
2032 ArmOp::I32TruncF32U { rd, sm } => {
2033 let result = BV::new_const(format!("i32_trunc_f32u_{:?}", sm), 32);
2034 state.set_reg(rd, result);
2035 }
2036
2037 // VCR-VER-002 (#166): UDF is the WASM trap sink — executing it
2038 // raises UsageFault. In the straight-line model (no path guards)
2039 // reaching a UDF means the sequence traps unconditionally; the
2040 // branch-taking executor [`Self::encode_sequence_br`] instead
2041 // conditions this on the guard the UDF is reached under.
2042 ArmOp::Udf { .. } => {
2043 state.may_trap = Bool::from_bool(true);
2044 }
2045
2046 // #923: an op with no semantics here is RECORDED, not ignored.
2047 // The state is still left unchanged (callers that only want a
2048 // best-effort register picture are unaffected), but the fact that
2049 // the model skipped an instruction is now observable, so a
2050 // consumer whose conclusion depends on the whole sequence having
2051 // been executed can decline loudly instead of concluding from a
2052 // partially-executed program. Only the FIRST such op is kept —
2053 // it is the one that first invalidates the state.
2054 other => {
2055 if state.unmodeled.is_none() {
2056 state.unmodeled = Some(op_variant_name(other));
2057 }
2058 }
2059 }
2060 }
2061
2062 /// The shift amount an ARMv7-M `<shift> (register)` form actually applies:
2063 /// `shift_n = UInt(R[m]<7:0>)`, zero-extended back to 32 bits so it can be
2064 /// handed to an SMT shift.
2065 ///
2066 /// Concretely: `Rm = 0x0000_0100` shifts by 0 (identity), `Rm =
2067 /// 0x0000_0120` shifts by 32 (LSL/LSR → 0). Neither is what the raw
2068 /// 32-bit register value would give, and neither is WASM's mod-32 rule.
2069 fn shift_amount_rm_7_0(rm: &BV) -> BV {
2070 rm.extract(7, 0).zero_ext(24)
2071 }
2072
2073 /// Evaluate an Operand2 value
2074 fn evaluate_operand2(&self, op2: &Operand2, state: &ArmState) -> BV {
2075 match op2 {
2076 Operand2::Imm(value) => BV::from_i64(*value as i64, 32),
2077 Operand2::Reg(reg) => state.get_reg(reg).clone(),
2078 Operand2::RegShift { rm, shift, amount } => {
2079 let reg_val = state.get_reg(rm).clone();
2080 let shift_amount = BV::from_i64(*amount as i64, 32);
2081
2082 match shift {
2083 synth_synthesis::ShiftType::LSL => reg_val.bvshl(&shift_amount),
2084 synth_synthesis::ShiftType::LSR => reg_val.bvlshr(&shift_amount),
2085 synth_synthesis::ShiftType::ASR => reg_val.bvashr(&shift_amount),
2086 synth_synthesis::ShiftType::ROR => reg_val.bvrotr(&shift_amount),
2087 }
2088 }
2089 }
2090 }
2091
2092 /// Extract the result value from a register after execution
2093 pub fn extract_result(&self, state: &ArmState, reg: &Reg) -> BV {
2094 state.get_reg(reg).clone()
2095 }
2096
2097 /// Encode ARM CLZ (Count Leading Zeros) instruction
2098 ///
2099 /// Implements the same algorithm as WASM i32.clz for equivalence verification.
2100 /// Uses binary search through bit positions.
2101 fn encode_clz(&self, input: &BV) -> BV {
2102 let zero = BV::from_i64(0, 32);
2103
2104 // Special case: if input is 0, return 32
2105 let all_zero = input.eq(&zero);
2106 let result_if_zero = BV::from_i64(32, 32);
2107
2108 // Binary search approach
2109 let mut count = BV::from_i64(0, 32);
2110 let mut remaining = input.clone();
2111
2112 // Check top 16 bits
2113 let mask_16 = BV::from_u64(0xFFFF0000, 32);
2114 let top_16 = remaining.bvand(&mask_16);
2115 let top_16_zero = top_16.eq(&zero);
2116
2117 count = top_16_zero.ite(count.bvadd(BV::from_i64(16, 32)), &count);
2118 remaining = top_16_zero.ite(remaining.bvshl(BV::from_i64(16, 32)), &remaining);
2119
2120 // Check top 8 bits
2121 let mask_8 = BV::from_u64(0xFF000000, 32);
2122 let top_8 = remaining.bvand(&mask_8);
2123 let top_8_zero = top_8.eq(&zero);
2124
2125 count = top_8_zero.ite(count.bvadd(BV::from_i64(8, 32)), &count);
2126 remaining = top_8_zero.ite(remaining.bvshl(BV::from_i64(8, 32)), &remaining);
2127
2128 // Check top 4 bits
2129 let mask_4 = BV::from_u64(0xF0000000, 32);
2130 let top_4 = remaining.bvand(&mask_4);
2131 let top_4_zero = top_4.eq(&zero);
2132
2133 count = top_4_zero.ite(count.bvadd(BV::from_i64(4, 32)), &count);
2134 remaining = top_4_zero.ite(remaining.bvshl(BV::from_i64(4, 32)), &remaining);
2135
2136 // Check top 2 bits
2137 let mask_2 = BV::from_u64(0xC0000000, 32);
2138 let top_2 = remaining.bvand(&mask_2);
2139 let top_2_zero = top_2.eq(&zero);
2140
2141 count = top_2_zero.ite(count.bvadd(BV::from_i64(2, 32)), &count);
2142 remaining = top_2_zero.ite(remaining.bvshl(BV::from_i64(2, 32)), &remaining);
2143
2144 // Check top bit
2145 let mask_1 = BV::from_u64(0x80000000, 32);
2146 let top_1 = remaining.bvand(&mask_1);
2147 let top_1_zero = top_1.eq(&zero);
2148
2149 count = top_1_zero.ite(count.bvadd(BV::from_i64(1, 32)), &count);
2150
2151 // Return 32 if all zeros, otherwise return count
2152 all_zero.ite(&result_if_zero, &count)
2153 }
2154
2155 /// Encode CTZ (Count Trailing Zeros) instruction
2156 ///
2157 /// Counts the number of trailing (low-order) zero bits.
2158 /// Implemented as: ctz(x) = clz(rbit(x))
2159 /// Returns 32 if input is 0.
2160 fn encode_ctz(&self, input: &BV) -> BV {
2161 // CTZ can be implemented by reversing bits and then counting leading zeros
2162 let reversed = self.encode_rbit(input);
2163 self.encode_clz(&reversed)
2164 }
2165
2166 /// Encode ARM RBIT (Reverse Bits) instruction
2167 ///
2168 /// Reverses the bit order in a 32-bit value.
2169 /// Used in combination with CLZ to implement CTZ.
2170 fn encode_rbit(&self, input: &BV) -> BV {
2171 // Reverse bits by swapping progressively smaller chunks
2172 let mut result = input.clone();
2173
2174 // Swap 16-bit halves
2175 let mask_16 = BV::from_u64(0xFFFF0000, 32);
2176 let top_16 = result.bvand(&mask_16).bvlshr(BV::from_i64(16, 32));
2177 let bottom_16 = result.bvshl(BV::from_i64(16, 32));
2178 result = top_16.bvor(&bottom_16);
2179
2180 // Swap 8-bit chunks
2181 let mask_8_top = BV::from_u64(0xFF00FF00, 32);
2182 let mask_8_bottom = BV::from_u64(0x00FF00FF, 32);
2183 let top_8 = result.bvand(&mask_8_top).bvlshr(BV::from_i64(8, 32));
2184 let bottom_8 = result.bvand(&mask_8_bottom).bvshl(BV::from_i64(8, 32));
2185 result = top_8.bvor(&bottom_8);
2186
2187 // Swap 4-bit chunks
2188 let mask_4_top = BV::from_u64(0xF0F0F0F0, 32);
2189 let mask_4_bottom = BV::from_u64(0x0F0F0F0F, 32);
2190 let top_4 = result.bvand(&mask_4_top).bvlshr(BV::from_i64(4, 32));
2191 let bottom_4 = result.bvand(&mask_4_bottom).bvshl(BV::from_i64(4, 32));
2192 result = top_4.bvor(&bottom_4);
2193
2194 // Swap 2-bit chunks
2195 let mask_2_top = BV::from_u64(0xCCCCCCCC, 32);
2196 let mask_2_bottom = BV::from_u64(0x33333333, 32);
2197 let top_2 = result.bvand(&mask_2_top).bvlshr(BV::from_i64(2, 32));
2198 let bottom_2 = result.bvand(&mask_2_bottom).bvshl(BV::from_i64(2, 32));
2199 result = top_2.bvor(&bottom_2);
2200
2201 // Swap 1-bit chunks (individual bits)
2202 let mask_1_top = BV::from_u64(0xAAAAAAAA, 32);
2203 let mask_1_bottom = BV::from_u64(0x55555555, 32);
2204 let top_1 = result.bvand(&mask_1_top).bvlshr(BV::from_i64(1, 32));
2205 let bottom_1 = result.bvand(&mask_1_bottom).bvshl(BV::from_i64(1, 32));
2206 result = top_1.bvor(&bottom_1);
2207
2208 result
2209 }
2210
2211 /// Update condition flags for subtraction (used by CMP, SUB, etc.)
2212 ///
2213 /// Computes all four ARM condition flags based on a subtraction:
2214 /// - N (Negative): Result is negative (bit 31 set)
2215 /// - Z (Zero): Result is zero
2216 /// - C (Carry): No borrow occurred (unsigned: a >= b)
2217 /// - V (Overflow): Signed overflow occurred
2218 ///
2219 /// For subtraction result = a - b:
2220 /// - C = 1 if a >= b (unsigned), 0 if borrow
2221 /// - V = 1 if signs of a and b differ AND sign of result differs from a
2222 fn update_flags_sub(&self, state: &mut ArmState, a: &BV, b: &BV, result: &BV) {
2223 let zero = BV::from_i64(0, 32);
2224
2225 // N flag: bit 31 of result (negative if set)
2226 let sign_bit = result.extract(31, 31);
2227 let one_bit = BV::from_i64(1, 1);
2228 state.flags.n = sign_bit.eq(&one_bit);
2229
2230 // Z flag: result == 0
2231 state.flags.z = result.eq(&zero);
2232
2233 // C flag: carry/borrow flag for subtraction
2234 // For SUB: C = 1 if no borrow (i.e., a >= b unsigned)
2235 // This is equivalent to: a >= b in unsigned arithmetic
2236 state.flags.c = a.bvuge(b);
2237
2238 // V flag: signed overflow
2239 // Overflow occurs when:
2240 // - Subtracting a positive from a negative gives positive
2241 // - Subtracting a negative from a positive gives negative
2242 // Formula: (a[31] != b[31]) && (a[31] != result[31])
2243 let a_sign = a.extract(31, 31);
2244 let b_sign = b.extract(31, 31);
2245 let r_sign = result.extract(31, 31);
2246
2247 let signs_differ = a_sign.eq(&b_sign).not(); // a and b have different signs
2248 let result_sign_wrong = a_sign.eq(&r_sign).not(); // result sign differs from a
2249 state.flags.v = Bool::and(&[&signs_differ, &result_sign_wrong]);
2250 }
2251
2252 /// Update condition flags for addition
2253 ///
2254 /// Similar to subtraction but with different carry logic:
2255 /// - C = 1 if unsigned overflow (result < a or result < b)
2256 /// - V = 1 if signed overflow
2257 #[allow(dead_code)]
2258 fn update_flags_add(&self, state: &mut ArmState, a: &BV, b: &BV, result: &BV) {
2259 let zero = BV::from_i64(0, 32);
2260
2261 // N flag: bit 31 of result
2262 let sign_bit = result.extract(31, 31);
2263 let one_bit = BV::from_i64(1, 1);
2264 state.flags.n = sign_bit.eq(&one_bit);
2265
2266 // Z flag: result == 0
2267 state.flags.z = result.eq(&zero);
2268
2269 // C flag: unsigned overflow
2270 // For ADD: C = 1 if carry out (unsigned overflow)
2271 // This occurs if result < a (wrapping occurred)
2272 state.flags.c = result.bvult(a);
2273
2274 // V flag: signed overflow
2275 // Overflow occurs when:
2276 // - Adding two positives gives negative
2277 // - Adding two negatives gives positive
2278 // Formula: (a[31] == b[31]) && (a[31] != result[31])
2279 let a_sign = a.extract(31, 31);
2280 let b_sign = b.extract(31, 31);
2281 let r_sign = result.extract(31, 31);
2282
2283 let signs_same = a_sign.eq(&b_sign); // a and b have same sign
2284 let result_sign_wrong = a_sign.eq(&r_sign).not(); // result sign differs
2285 state.flags.v = Bool::and(&[&signs_same, &result_sign_wrong]);
2286 }
2287
2288 /// Evaluate an ARM condition code based on NZCV flags
2289 ///
2290 /// This implements the standard ARM condition code logic:
2291 /// - EQ: Z == 1
2292 /// - NE: Z == 0
2293 /// - LT: N != V (signed less than)
2294 /// - LE: Z == 1 || N != V (signed less or equal)
2295 /// - GT: Z == 0 && N == V (signed greater than)
2296 /// - GE: N == V (signed greater or equal)
2297 /// - LO: C == 0 (unsigned less than)
2298 /// - LS: C == 0 || Z == 1 (unsigned less or equal)
2299 /// - HI: C == 1 && Z == 0 (unsigned greater than)
2300 /// - HS: C == 1 (unsigned greater or equal)
2301 fn evaluate_condition(
2302 &self,
2303 cond: &synth_synthesis::rules::Condition,
2304 flags: &ConditionFlags,
2305 ) -> Bool {
2306 use synth_synthesis::rules::Condition;
2307
2308 match cond {
2309 Condition::EQ => flags.z.clone(),
2310 Condition::NE => flags.z.not(),
2311 Condition::LT => {
2312 // N != V: negative flag differs from overflow flag
2313 flags.n.eq(&flags.v).not()
2314 }
2315 Condition::LE => {
2316 // Z == 1 || N != V
2317 let n_ne_v = flags.n.eq(&flags.v).not();
2318 Bool::or(&[&flags.z, &n_ne_v])
2319 }
2320 Condition::GT => {
2321 // Z == 0 && N == V
2322 let z_zero = flags.z.not();
2323 let n_eq_v = flags.n.eq(&flags.v);
2324 Bool::and(&[&z_zero, &n_eq_v])
2325 }
2326 Condition::GE => {
2327 // N == V
2328 flags.n.eq(&flags.v)
2329 }
2330 Condition::LO => {
2331 // C == 0 (no carry = less than unsigned)
2332 flags.c.not()
2333 }
2334 Condition::LS => {
2335 // C == 0 || Z == 1
2336 let c_zero = flags.c.not();
2337 Bool::or(&[&flags.z, &c_zero])
2338 }
2339 Condition::HI => {
2340 // C == 1 && Z == 0
2341 let z_zero = flags.z.not();
2342 Bool::and(&[&flags.c, &z_zero])
2343 }
2344 Condition::HS => {
2345 // C == 1 (carry = greater or equal unsigned)
2346 flags.c.clone()
2347 }
2348 }
2349 }
2350
2351 /// Convert a boolean to a 32-bit bitvector (0 or 1)
2352 fn bool_to_bv32(&self, cond: &Bool) -> BV {
2353 let zero = BV::from_i64(0, 32);
2354 let one = BV::from_i64(1, 32);
2355 cond.ite(&one, &zero)
2356 }
2357
2358 /// Encode ARM POPCNT (population count)
2359 ///
2360 /// Uses the Hamming weight algorithm (same as WASM implementation).
2361 /// This is a pseudo-instruction that would be expanded into actual ARM code.
2362 fn encode_popcnt(&self, input: &BV) -> BV {
2363 let mut x = input.clone();
2364
2365 // Step 1: Count bits in pairs
2366 let mask1 = BV::from_u64(0x55555555, 32);
2367 let masked = x.bvand(&mask1);
2368 let shifted = x.bvlshr(BV::from_i64(1, 32));
2369 let shifted_masked = shifted.bvand(&mask1);
2370 x = masked.bvadd(&shifted_masked);
2371
2372 // Step 2: Count pairs in nibbles
2373 let mask2 = BV::from_u64(0x33333333, 32);
2374 let masked = x.bvand(&mask2);
2375 let shifted = x.bvlshr(BV::from_i64(2, 32));
2376 let shifted_masked = shifted.bvand(&mask2);
2377 x = masked.bvadd(&shifted_masked);
2378
2379 // Step 3: Count nibbles in bytes
2380 let mask3 = BV::from_u64(0x0F0F0F0F, 32);
2381 let masked = x.bvand(&mask3);
2382 let shifted = x.bvlshr(BV::from_i64(4, 32));
2383 let shifted_masked = shifted.bvand(&mask3);
2384 x = masked.bvadd(&shifted_masked);
2385
2386 // Step 4: Sum all bytes
2387 let multiplier = BV::from_u64(0x01010101, 32);
2388 x = x.bvmul(&multiplier);
2389 x = x.bvlshr(BV::from_i64(24, 32));
2390
2391 x
2392 }
2393}
2394
2395// ===========================================================================
2396// VCR-VER-002 (#166): branch-taking guarded executor — DERIVES the ARM trap
2397// condition from the emitted guard/branch/UDF structure
2398// ===========================================================================
2399
2400/// Path guard: the condition under which an instruction executes. `Always`
2401/// keeps the straight-line common case free of `ite` merging.
2402#[derive(Clone)]
2403enum Guard {
2404 Always,
2405 Cond(Bool),
2406}
2407
2408impl Guard {
2409 fn and_cond(&self, c: &Bool) -> Guard {
2410 match self {
2411 Guard::Always => Guard::Cond(c.clone()),
2412 Guard::Cond(g) => Guard::Cond(Bool::and(&[g, c])),
2413 }
2414 }
2415}
2416
2417/// Merge an incoming edge guard into the guard map at `at`.
2418fn merge_guard(incoming: &mut HashMap<usize, Guard>, at: usize, g: Guard) {
2419 match (incoming.get(&at), g) {
2420 (Some(Guard::Always), _) => {}
2421 (_, Guard::Always) => {
2422 incoming.insert(at, Guard::Always);
2423 }
2424 (Some(Guard::Cond(a)), Guard::Cond(b)) => {
2425 let merged = Bool::or(&[a, &b]);
2426 incoming.insert(at, Guard::Cond(merged));
2427 }
2428 (None, g @ Guard::Cond(_)) => {
2429 incoming.insert(at, g);
2430 }
2431 }
2432}
2433
2434/// Boolean if-then-else (the term API only has BV ite).
2435fn bool_ite(c: &Bool, t: &Bool, e: &Bool) -> Bool {
2436 Bool::or(&[&Bool::and(&[c, t]), &Bool::and(&[&c.not(), e])])
2437}
2438
2439/// IEEE 754 single-precision NaN test over the raw bit pattern:
2440/// exponent all-ones with a non-zero fraction.
2441fn f32_is_nan(x: &BV) -> Bool {
2442 let exp_ones = x.extract(30, 23).eq(BV::from_u64(0xFF, 8));
2443 let frac_nonzero = x.extract(22, 0).eq(BV::from_u64(0, 23)).not();
2444 Bool::and(&[&exp_ones, &frac_nonzero])
2445}
2446
2447/// Ordered `a < b` over IEEE 754 single-precision BIT PATTERNS, assuming
2448/// neither operand is NaN (the callers conjoin the NaN exclusion). Uses the
2449/// sign/magnitude case split; `+0.0 == -0.0` (neither is less).
2450fn f32_ordered_lt(a: &BV, b: &BV) -> Bool {
2451 let a_neg = a.extract(31, 31).eq(BV::from_u64(1, 1));
2452 let b_neg = b.extract(31, 31).eq(BV::from_u64(1, 1));
2453 let a_mag = a.extract(30, 0);
2454 let b_mag = b.extract(30, 0);
2455 let zero31 = BV::from_u64(0, 31);
2456 let both_zero = Bool::and(&[&a_mag.eq(&zero31), &b_mag.eq(&zero31)]);
2457 // (neg, neg): larger magnitude is smaller; (neg, pos): a < b unless both
2458 // are zeros; (pos, neg): never; (pos, pos): magnitude order.
2459 let neg_neg = b_mag.bvult(&a_mag);
2460 let neg_pos = both_zero.not();
2461 let pos_pos = a_mag.bvult(&b_mag);
2462 bool_ite(
2463 &a_neg,
2464 &bool_ite(&b_neg, &neg_neg, &neg_pos),
2465 &bool_ite(&b_neg, &Bool::from_bool(false), &pos_pos),
2466 )
2467}
2468
2469/// The three ordered VFP comparison results the trunc guards use, as total
2470/// functions over the operands' bit patterns (result is 0 on any NaN — the
2471/// unordered case — exactly the ARM `VCMP`+`VMRS`+`IT` materialization the
2472/// `F32Lt`/`F32Gt`/`F32Ge` pseudo-ops stand for).
2473fn f32_cmp_result(kind: F32CmpKind, a: &BV, b: &BV) -> Bool {
2474 let ordered = Bool::and(&[&f32_is_nan(a).not(), &f32_is_nan(b).not()]);
2475 let rel = match kind {
2476 F32CmpKind::Lt => f32_ordered_lt(a, b),
2477 F32CmpKind::Gt => f32_ordered_lt(b, a),
2478 F32CmpKind::Ge => f32_ordered_lt(a, b).not(),
2479 };
2480 Bool::and(&[&ordered, &rel])
2481}
2482
2483#[derive(Clone, Copy)]
2484enum F32CmpKind {
2485 Lt,
2486 Gt,
2487 Ge,
2488}
2489
2490/// IEEE 754 double-precision NaN test over the raw bit pattern:
2491/// exponent all-ones (bits 62..52) with a non-zero fraction (bits 51..0).
2492/// The 64-bit twin of [`f32_is_nan`], for the #709/#756 f64→i32 trunc guards.
2493fn f64_is_nan(x: &BV) -> Bool {
2494 let exp_ones = x.extract(62, 52).eq(BV::from_u64(0x7FF, 11));
2495 let frac_nonzero = x.extract(51, 0).eq(BV::from_u64(0, 52)).not();
2496 Bool::and(&[&exp_ones, &frac_nonzero])
2497}
2498
2499/// Ordered `a < b` over IEEE 754 double-precision BIT PATTERNS, assuming
2500/// neither operand is NaN (the callers conjoin the NaN exclusion). The 64-bit
2501/// twin of [`f32_ordered_lt`]: sign bit 63, magnitude bits 62..0; `+0.0 == -0.0`
2502/// (neither is less).
2503fn f64_ordered_lt(a: &BV, b: &BV) -> Bool {
2504 let a_neg = a.extract(63, 63).eq(BV::from_u64(1, 1));
2505 let b_neg = b.extract(63, 63).eq(BV::from_u64(1, 1));
2506 let a_mag = a.extract(62, 0);
2507 let b_mag = b.extract(62, 0);
2508 let zero63 = BV::from_u64(0, 63);
2509 let both_zero = Bool::and(&[&a_mag.eq(&zero63), &b_mag.eq(&zero63)]);
2510 // (neg, neg): larger magnitude is smaller; (neg, pos): a < b unless both
2511 // are zeros; (pos, neg): never; (pos, pos): magnitude order.
2512 let neg_neg = b_mag.bvult(&a_mag);
2513 let neg_pos = both_zero.not();
2514 let pos_pos = a_mag.bvult(&b_mag);
2515 bool_ite(
2516 &a_neg,
2517 &bool_ite(&b_neg, &neg_neg, &neg_pos),
2518 &bool_ite(&b_neg, &Bool::from_bool(false), &pos_pos),
2519 )
2520}
2521
2522/// The three ordered VFP.F64 comparison results the f64 trunc guards use, as
2523/// total functions over the operands' bit patterns (result is 0 on any NaN —
2524/// the unordered case — exactly the ARM `VCMP.F64`+`VMRS`+`IT` materialization
2525/// the `F64Lt`/`F64Gt`/`F64Ge` pseudo-ops stand for). The 64-bit twin of
2526/// [`f32_cmp_result`].
2527fn f64_cmp_result(kind: F32CmpKind, a: &BV, b: &BV) -> Bool {
2528 let ordered = Bool::and(&[&f64_is_nan(a).not(), &f64_is_nan(b).not()]);
2529 let rel = match kind {
2530 F32CmpKind::Lt => f64_ordered_lt(a, b),
2531 F32CmpKind::Gt => f64_ordered_lt(b, a),
2532 F32CmpKind::Ge => f64_ordered_lt(a, b).not(),
2533 };
2534 Bool::and(&[&ordered, &rel])
2535}
2536
2537impl ArmSemantics {
2538 /// Branch-taking guarded symbolic execution of an ARM sequence,
2539 /// deriving `state.may_trap` from the emitted guard structure
2540 /// (VCR-VER-002, #166).
2541 ///
2542 /// Forward-branch DAG execution over the op list: every instruction
2543 /// carries the disjunction of the path conditions that reach it
2544 /// (if-conversion), `BCondOffset` routes guards forward, and a `Udf`
2545 /// accumulates its path guard into [`ArmState::may_trap`] — and does NOT
2546 /// fall through (a trap halts execution, so the code after a guarded
2547 /// `UDF` is reached only via the guard's skip branch). This makes the ARM
2548 /// trap condition a DERIVED term: a lowering whose guard was dropped,
2549 /// inverted, or aimed at the wrong register derives a trap condition that
2550 /// fails the preservation VC — unlike the previous structural
2551 /// `Udf`-presence proxy, which only saw that *some* trap existed.
2552 ///
2553 /// Branch targets are resolved in bytes via the shipped byte-size
2554 /// estimator (`synth_synthesis::optimizer_bridge::estimate_arm_byte_size`,
2555 /// the #511 estimator that CI pins against the encoder), matching the
2556 /// encoder's `target = branch + 4 + 2*offset` halfword rule. A target
2557 /// that lands mid-instruction, a backward branch (loop), an op outside
2558 /// the modeled subset, or any label/call control flow is a loud `Err` —
2559 /// never a silent accept.
2560 pub fn encode_sequence_br(
2561 &self,
2562 arm_ops: &[ArmOp],
2563 state: &mut ArmState,
2564 ) -> Result<(), String> {
2565 use synth_synthesis::optimizer_bridge::estimate_arm_byte_size;
2566
2567 // Byte offset of each op (the estimator is the pinned encoder mirror).
2568 let mut offsets = Vec::with_capacity(arm_ops.len());
2569 let mut off = 0usize;
2570 for op in arm_ops {
2571 offsets.push(off);
2572 off += estimate_arm_byte_size(op);
2573 }
2574 let total_len = off;
2575 let boundaries: std::collections::HashSet<usize> = offsets.iter().copied().collect();
2576
2577 let mut incoming: HashMap<usize, Guard> = HashMap::new();
2578 incoming.insert(0, Guard::Always);
2579
2580 for (i, op) in arm_ops.iter().enumerate() {
2581 let o = offsets[i];
2582 // Unreached instruction (e.g. dead code behind an unconditional
2583 // trap): no incoming edge, skip — it can never execute.
2584 let Some(g) = incoming.get(&o).cloned() else {
2585 continue;
2586 };
2587 let next = o + estimate_arm_byte_size(op);
2588
2589 match op {
2590 ArmOp::BCondOffset { cond, offset } => {
2591 if *offset < 0 {
2592 return Err(
2593 "backward branch (loop) outside the trap-derivation subset — held out"
2594 .to_string(),
2595 );
2596 }
2597 // Encoder rule: offset is the halfword displacement,
2598 // target = branch_addr + 4 + 2*offset.
2599 let target = o + 4 + 2 * (*offset as usize);
2600 if target != total_len && !boundaries.contains(&target) {
2601 return Err(format!(
2602 "BCondOffset target {target} lands mid-instruction \
2603 (sequence len {total_len}) — estimator/encoder drift or \
2604 malformed guard"
2605 ));
2606 }
2607 let c = self.evaluate_condition(cond, &state.flags);
2608 merge_guard(&mut incoming, target, g.and_cond(&c));
2609 merge_guard(&mut incoming, next, g.and_cond(&c.not()));
2610 }
2611
2612 ArmOp::Udf { .. } => {
2613 // The trap fires exactly under this path guard; execution
2614 // never continues past it (no fall-through edge).
2615 state.may_trap = match &g {
2616 Guard::Always => Bool::from_bool(true),
2617 Guard::Cond(gb) => Bool::or(&[&state.may_trap, gb]),
2618 };
2619 }
2620
2621 // Label/relative/indirect control flow has no derivable local
2622 // trap semantics here — loud decline, never a silent accept.
2623 ArmOp::B { .. }
2624 | ArmOp::BOffset { .. }
2625 | ArmOp::Bcc { .. }
2626 | ArmOp::Bhs { .. }
2627 | ArmOp::Blo { .. }
2628 | ArmOp::Bl { .. }
2629 | ArmOp::Blx { .. }
2630 | ArmOp::Bx { .. }
2631 | ArmOp::Label { .. }
2632 | ArmOp::Call { .. }
2633 | ArmOp::CallIndirect { .. }
2634 | ArmOp::BrTable { .. }
2635 | ArmOp::Push { .. }
2636 | ArmOp::Pop { .. } => {
2637 return Err(format!(
2638 "op {op:?} outside the trap-derivation subset — loud decline"
2639 ));
2640 }
2641
2642 _ => {
2643 match &g {
2644 Guard::Always => self.exec_trap_subset_op(op, state)?,
2645 Guard::Cond(gb) => {
2646 // Guarded (if-converted) execution: snapshot the
2647 // register/flag/VFP state, execute, ite-merge
2648 // under the guard. Sound because these ops touch
2649 // only registers/flags/VFP (the subset check in
2650 // exec_trap_subset_op rejects everything else).
2651 //
2652 // Only components the op actually CHANGED are
2653 // merged — `ite(g, x, x) ≡ x`, and wrapping every
2654 // untouched register on every guarded step nests
2655 // the SDIV/UDIV operands in ite chains, blowing
2656 // the div/rem trap VC off a CDCL cliff (observed:
2657 // the div_s double-guard query ran 45+ min / 5 GB
2658 // with the unconditional merge, sub-second
2659 // without).
2660 let regs_before = state.registers.clone();
2661 let vfp_before = state.vfp_registers.clone();
2662 let flags_before = ConditionFlags {
2663 n: state.flags.n.clone(),
2664 z: state.flags.z.clone(),
2665 c: state.flags.c.clone(),
2666 v: state.flags.v.clone(),
2667 };
2668 self.exec_trap_subset_op(op, state)?;
2669 for (r, before) in regs_before.iter().enumerate() {
2670 if !state.registers[r].same_term(before) {
2671 state.registers[r] = gb.ite(&state.registers[r], before);
2672 }
2673 }
2674 for (r, before) in vfp_before.iter().enumerate() {
2675 if !state.vfp_registers[r].same_term(before) {
2676 state.vfp_registers[r] =
2677 gb.ite(&state.vfp_registers[r], before);
2678 }
2679 }
2680 if !state.flags.n.same_term(&flags_before.n) {
2681 state.flags.n = bool_ite(gb, &state.flags.n, &flags_before.n);
2682 }
2683 if !state.flags.z.same_term(&flags_before.z) {
2684 state.flags.z = bool_ite(gb, &state.flags.z, &flags_before.z);
2685 }
2686 if !state.flags.c.same_term(&flags_before.c) {
2687 state.flags.c = bool_ite(gb, &state.flags.c, &flags_before.c);
2688 }
2689 if !state.flags.v.same_term(&flags_before.v) {
2690 state.flags.v = bool_ite(gb, &state.flags.v, &flags_before.v);
2691 }
2692 }
2693 }
2694 merge_guard(&mut incoming, next, g);
2695 }
2696 }
2697 }
2698
2699 Ok(())
2700 }
2701
2702 /// Whether the sequence's branch structure is VALUE-DEAD: every op inside
2703 /// a branch-skipped span writes no register/VFP state (`Udf`, `Cmp`,
2704 /// `Cmn`, nested `BCondOffset` only), and no op anywhere in the sequence
2705 /// turns flags into a register value (`SetCond`).
2706 ///
2707 /// Under this condition the final REGISTER state is path-independent —
2708 /// every register-writing op executes on every path, in program order —
2709 /// so the straight-line value pass
2710 /// [`Self::encode_sequence_value_straightline`] computes exactly the
2711 /// registers any non-trapping real path produces. The flag writes a taken
2712 /// branch skips (e.g. the div_s overflow guard's `CMN` behind `BNE +3`)
2713 /// can only influence which PATH is taken — the trap side, which
2714 /// [`Self::encode_sequence_br`] derives with full path sensitivity — and
2715 /// never a register value, because `SetCond` (the only flag→register op
2716 /// in the modeled subset) is excluded outright.
2717 ///
2718 /// This is what lets the div/rem trap VC keep its value clause
2719 /// STRUCTURALLY aligned with the WASM side (`bvsdiv`/`MLS` terms
2720 /// identical after canonicalization): an `ite(guard, …)` wrapper on an
2721 /// SDIV/MLS operand un-shares the 32×32 multiplier/divider circuits and
2722 /// sends the UNSAT proof off the CDCL cliff term.rs documents (observed:
2723 /// rem_s value clause 15+ min with the ite, sub-second without).
2724 pub fn branch_spans_are_value_dead(arm_ops: &[ArmOp]) -> bool {
2725 use synth_synthesis::optimizer_bridge::estimate_arm_byte_size;
2726
2727 let mut offsets = Vec::with_capacity(arm_ops.len());
2728 let mut off = 0usize;
2729 for op in arm_ops {
2730 offsets.push(off);
2731 off += estimate_arm_byte_size(op);
2732 }
2733
2734 // No flag→register materialization anywhere in the sequence.
2735 if arm_ops.iter().any(|op| matches!(op, ArmOp::SetCond { .. })) {
2736 return false;
2737 }
2738
2739 for (i, op) in arm_ops.iter().enumerate() {
2740 if let ArmOp::BCondOffset { offset, .. } = op {
2741 if *offset < 0 {
2742 return false; // backward branch — not this subset at all
2743 }
2744 // Fall-through = next instruction; encoder rule for the
2745 // target: branch_addr + 4 + 2*offset (same as
2746 // `encode_sequence_br`). The skipped span is [fall-through,
2747 // target).
2748 let span_start = offsets[i] + estimate_arm_byte_size(op);
2749 let span_end = offsets[i] + 4 + 2 * (*offset as usize);
2750 for (j, skipped) in arm_ops.iter().enumerate() {
2751 if offsets[j] >= span_start && offsets[j] < span_end {
2752 match skipped {
2753 ArmOp::Udf { .. }
2754 | ArmOp::Cmp { .. }
2755 | ArmOp::Cmn { .. }
2756 | ArmOp::BCondOffset { .. } => {}
2757 _ => return false, // a register/VFP write is skippable
2758 }
2759 }
2760 }
2761 }
2762 }
2763 true
2764 }
2765
2766 /// Straight-line VALUE execution of a trap-guarded sequence: branches and
2767 /// `UDF`s are register no-ops, every other op executes unconditionally
2768 /// via the same modeled subset as the branch-taking executor.
2769 ///
2770 /// ONLY sound when [`Self::branch_spans_are_value_dead`] holds (see its
2771 /// doc for the argument); callers must check it first. Produces ite-free
2772 /// register terms, keeping the trap VC's value clause structurally
2773 /// aligned with the WASM encoding.
2774 pub fn encode_sequence_value_straightline(
2775 &self,
2776 arm_ops: &[ArmOp],
2777 state: &mut ArmState,
2778 ) -> Result<(), String> {
2779 for op in arm_ops {
2780 match op {
2781 ArmOp::BCondOffset { .. } | ArmOp::Udf { .. } => {}
2782 _ => self.exec_trap_subset_op(op, state)?,
2783 }
2784 }
2785 Ok(())
2786 }
2787
2788 /// Execute one non-branch op of the trap-derivation subset. The ordered
2789 /// VFP compares get explicit semantics here (`encode_op` models them as
2790 /// uninterpreted symbols, which cannot drive a trap derivation); a
2791 /// WHITELIST of register-only value ops delegates to `encode_op`; anything
2792 /// else is a loud `Err` — `encode_op`'s `_ =>` default must never
2793 /// green-wash a trap derivation.
2794 ///
2795 /// #923 hardened that last sentence into a MECHANISM. It used to rest
2796 /// entirely on the allowlist below being an accurate mirror of
2797 /// `encode_op`'s match arms, and it had drifted: `Rsb`, `I32TruncF32S`
2798 /// and `I32TruncF32U` were allowlisted to delegate to a model that did not
2799 /// implement them, so the guard passed them straight through as no-ops.
2800 /// Every delegation now re-checks [`ArmState::unmodeled`] afterwards, so
2801 /// an allowlist entry `encode_op` cannot honour is a loud decline rather
2802 /// than a silent skip — and `Cmn`/`Movw`/`Movt`, which used to carry a
2803 /// duplicate model here, now delegate to the single one in `encode_op`.
2804 fn exec_trap_subset_op(&self, op: &ArmOp, state: &mut ArmState) -> Result<(), String> {
2805 match op {
2806 // Ordered VFP compares (the #709 trunc guards): real bit-pattern
2807 // semantics — result register is 1 iff the ordered relation
2808 // holds, 0 on NaN. encode_op models these as uninterpreted
2809 // symbols, which cannot drive a trap derivation.
2810 ArmOp::F32Lt { rd, sn, sm } => {
2811 let a = state.get_vfp_reg(sn).clone();
2812 let b = state.get_vfp_reg(sm).clone();
2813 let r = self.bool_to_bv32(&f32_cmp_result(F32CmpKind::Lt, &a, &b));
2814 state.set_reg(rd, r);
2815 Ok(())
2816 }
2817 ArmOp::F32Gt { rd, sn, sm } => {
2818 let a = state.get_vfp_reg(sn).clone();
2819 let b = state.get_vfp_reg(sm).clone();
2820 let r = self.bool_to_bv32(&f32_cmp_result(F32CmpKind::Gt, &a, &b));
2821 state.set_reg(rd, r);
2822 Ok(())
2823 }
2824 ArmOp::F32Ge { rd, sn, sm } => {
2825 let a = state.get_vfp_reg(sn).clone();
2826 let b = state.get_vfp_reg(sm).clone();
2827 let r = self.bool_to_bv32(&f32_cmp_result(F32CmpKind::Ge, &a, &b));
2828 state.set_reg(rd, r);
2829 Ok(())
2830 }
2831 // Ordered VFP.F64 compares (the #756 f64→i32 trunc guards): real
2832 // bit-pattern semantics over the 64-bit D-register operands — 1 iff
2833 // the ordered relation holds, 0 on NaN. encode_op models these as
2834 // uninterpreted symbols, which cannot drive a trap derivation.
2835 ArmOp::F64Lt { rd, dn, dm } => {
2836 let a = state.get_vfp_reg(dn).clone();
2837 let b = state.get_vfp_reg(dm).clone();
2838 let r = self.bool_to_bv32(&f64_cmp_result(F32CmpKind::Lt, &a, &b));
2839 state.set_reg(rd, r);
2840 Ok(())
2841 }
2842 ArmOp::F64Gt { rd, dn, dm } => {
2843 let a = state.get_vfp_reg(dn).clone();
2844 let b = state.get_vfp_reg(dm).clone();
2845 let r = self.bool_to_bv32(&f64_cmp_result(F32CmpKind::Gt, &a, &b));
2846 state.set_reg(rd, r);
2847 Ok(())
2848 }
2849 ArmOp::F64Ge { rd, dn, dm } => {
2850 let a = state.get_vfp_reg(dn).clone();
2851 let b = state.get_vfp_reg(dm).clone();
2852 let r = self.bool_to_bv32(&f64_cmp_result(F32CmpKind::Ge, &a, &b));
2853 state.set_reg(rd, r);
2854 Ok(())
2855 }
2856 // Register/flag-only value ops the covered lowerings use:
2857 // delegate to the existing encode_op semantics.
2858 ArmOp::Cmp { .. }
2859 | ArmOp::Cmn { .. }
2860 | ArmOp::Movw { .. }
2861 | ArmOp::Movt { .. }
2862 | ArmOp::Add { .. }
2863 | ArmOp::Sub { .. }
2864 | ArmOp::Rsb { .. }
2865 | ArmOp::Mov { .. }
2866 | ArmOp::And { .. }
2867 | ArmOp::Orr { .. }
2868 | ArmOp::Eor { .. }
2869 | ArmOp::Mul { .. }
2870 | ArmOp::Mls { .. }
2871 | ArmOp::Sdiv { .. }
2872 | ArmOp::Udiv { .. }
2873 | ArmOp::SetCond { .. }
2874 | ArmOp::Nop
2875 | ArmOp::F32Const { .. }
2876 | ArmOp::I32TruncF32S { .. }
2877 | ArmOp::I32TruncF32U { .. }
2878 // f64 trunc guards (#756): F64Const sets the D-reg to the real
2879 // 64-bit float bit pattern (load-bearing for the derived compare);
2880 // the saturating VCVT pseudo-ops write only the RESULT register,
2881 // which the trap derivation ignores.
2882 | ArmOp::F64Const { .. }
2883 | ArmOp::I32TruncF64S { .. }
2884 | ArmOp::I32TruncF64U { .. }
2885 | ArmOp::I64TruncF64S { .. }
2886 | ArmOp::I64TruncF64U { .. }
2887 // Ldr/Str: the value model treats loads as fresh symbols and
2888 // stores as no-ops (no memory-contents model) — fine for a trap
2889 // derivation, where only the guard's flags/registers matter.
2890 | ArmOp::Ldr { .. }
2891 | ArmOp::Str { .. } => self.delegate_to_encode_op(op, state),
2892 // Subword accesses (#752 gate coverage for the guarded
2893 // i32.load8/16 + i32.store8/16 shapes): same treatment as
2894 // Ldr/Str — a load writes a fresh symbol (no memory-contents
2895 // model), a store touches no register. Neither affects flags,
2896 // so the trap derivation is untouched; modeling them here just
2897 // lets guarded subword sequences through instead of a loud
2898 // decline.
2899 ArmOp::Ldrb { rd, .. }
2900 | ArmOp::Ldrsb { rd, .. }
2901 | ArmOp::Ldrh { rd, .. }
2902 | ArmOp::Ldrsh { rd, .. } => {
2903 let result = BV::new_const(format!("load_{rd:?}"), 32);
2904 state.set_reg(rd, result);
2905 Ok(())
2906 }
2907 ArmOp::Strb { .. } | ArmOp::Strh { .. } => Ok(()),
2908 // i64 rem_u/rem_s pseudo-ops (VCR-VER, #825/#836): register-only
2909 // (they set the `rd*` pair), so they belong in this subset — the
2910 // executor delegates to the general value model, which now builds a
2911 // real `BvTerm::Urem`/`bvsrem` term. The ÷0 TRAP is NOT derived
2912 // here (the bare pseudo-op carries no `UDF`); the VC reconstructs
2913 // it from the pseudo-op's `elide_zero_guard` field, exactly like
2914 // the i64 trap-only VC. div_u/div_s stay OUT (their 64-bit quotient
2915 // value model is havoc — no value VC consumes it).
2916 ArmOp::I64RemU { .. } | ArmOp::I64RemS { .. } => {
2917 self.delegate_to_encode_op(op, state)
2918 }
2919 other => Err(format!(
2920 "op {other:?} outside the trap-derivation subset — loud decline"
2921 )),
2922 }
2923 }
2924
2925 /// Run an allowlisted op through [`Self::encode_op`] and REFUSE if
2926 /// `encode_op` turns out not to model it (#923).
2927 ///
2928 /// The allowlist above says which ops belong to the trap-derivation
2929 /// subset; `encode_op`'s match arms say which ops actually have
2930 /// semantics. Those are two lists, and they had drifted apart (`Rsb`,
2931 /// `I32TruncF32S`, `I32TruncF32U`). This check makes the drift
2932 /// unrepresentable in the only direction that matters: an allowlisted op
2933 /// with no model is a loud decline, not a silent no-op that lets a trap
2934 /// derivation run on a partially-executed program.
2935 fn delegate_to_encode_op(&self, op: &ArmOp, state: &mut ArmState) -> Result<(), String> {
2936 let before = state.unmodeled.clone();
2937 self.encode_op(op, state);
2938 if state.unmodeled != before {
2939 return Err(format!(
2940 "op {op:?} is allowlisted for the trap-derivation subset but \
2941 `encode_op` has no semantics for it — loud decline (#923)"
2942 ));
2943 }
2944 Ok(())
2945 }
2946}
2947
2948#[cfg(test)]
2949mod tests {
2950 use super::*;
2951 use crate::with_verification_context;
2952
2953 #[test]
2954 fn test_arm_add_semantics() {
2955 with_verification_context(|| {
2956 let encoder = ArmSemantics::new();
2957 let mut state = ArmState::new_symbolic();
2958
2959 // Set up concrete values for testing
2960 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
2961 state.set_reg(&Reg::R2, BV::from_i64(20, 32));
2962
2963 // Execute: ADD R0, R1, R2
2964 let op = ArmOp::Add {
2965 rd: Reg::R0,
2966 rn: Reg::R1,
2967 op2: Operand2::Reg(Reg::R2),
2968 };
2969
2970 encoder.encode_op(&op, &mut state);
2971
2972 // Check result: R0 should be 30
2973 let result = state.get_reg(&Reg::R0).simplify();
2974 assert_eq!(result.as_i64(), Some(30));
2975 });
2976 }
2977
2978 #[test]
2979 fn test_arm_sub_semantics() {
2980 with_verification_context(|| {
2981 let encoder = ArmSemantics::new();
2982 let mut state = ArmState::new_symbolic();
2983
2984 state.set_reg(&Reg::R1, BV::from_i64(50, 32));
2985 state.set_reg(&Reg::R2, BV::from_i64(20, 32));
2986
2987 let op = ArmOp::Sub {
2988 rd: Reg::R0,
2989 rn: Reg::R1,
2990 op2: Operand2::Reg(Reg::R2),
2991 };
2992
2993 encoder.encode_op(&op, &mut state);
2994
2995 let result = state.get_reg(&Reg::R0);
2996 assert_eq!(result.simplify().as_i64(), Some(30));
2997 });
2998 }
2999
3000 #[test]
3001 fn test_arm_mov_immediate() {
3002 with_verification_context(|| {
3003 let encoder = ArmSemantics::new();
3004 let mut state = ArmState::new_symbolic();
3005
3006 let op = ArmOp::Mov {
3007 rd: Reg::R0,
3008 op2: Operand2::Imm(42),
3009 };
3010
3011 encoder.encode_op(&op, &mut state);
3012
3013 let result = state.get_reg(&Reg::R0);
3014 assert_eq!(result.simplify().as_i64(), Some(42));
3015 });
3016 }
3017
3018 #[test]
3019 fn test_arm_bitwise_ops() {
3020 with_verification_context(|| {
3021 let encoder = ArmSemantics::new();
3022 let mut state = ArmState::new_symbolic();
3023
3024 state.set_reg(&Reg::R1, BV::from_i64(0b1010, 32));
3025 state.set_reg(&Reg::R2, BV::from_i64(0b1100, 32));
3026
3027 // Test AND
3028 let and_op = ArmOp::And {
3029 rd: Reg::R0,
3030 rn: Reg::R1,
3031 op2: Operand2::Reg(Reg::R2),
3032 };
3033 encoder.encode_op(&and_op, &mut state);
3034 assert_eq!(state.get_reg(&Reg::R0).simplify().as_i64(), Some(0b1000));
3035
3036 // Test ORR
3037 let orr_op = ArmOp::Orr {
3038 rd: Reg::R0,
3039 rn: Reg::R1,
3040 op2: Operand2::Reg(Reg::R2),
3041 };
3042 encoder.encode_op(&orr_op, &mut state);
3043 assert_eq!(state.get_reg(&Reg::R0).simplify().as_i64(), Some(0b1110));
3044
3045 // Test EOR (XOR)
3046 let eor_op = ArmOp::Eor {
3047 rd: Reg::R0,
3048 rn: Reg::R1,
3049 op2: Operand2::Reg(Reg::R2),
3050 };
3051 encoder.encode_op(&eor_op, &mut state);
3052 assert_eq!(state.get_reg(&Reg::R0).simplify().as_i64(), Some(0b0110));
3053 });
3054 }
3055
3056 #[test]
3057 fn test_arm_mls() {
3058 // Test MLS (Multiply and Subtract): Rd = Ra - Rn * Rm
3059 // This is used for remainder: a % b = a - (a/b) * b
3060 with_verification_context(|| {
3061 let encoder = ArmSemantics::new();
3062 let mut state = ArmState::new_symbolic();
3063
3064 // Test: 17 % 5 = 17 - (17/5) * 5 = 17 - 3*5 = 17 - 15 = 2
3065 // Ra = 17, Rn = 3 (quotient), Rm = 5 (divisor)
3066 state.set_reg(&Reg::R0, BV::from_i64(17, 32)); // Ra (dividend)
3067 state.set_reg(&Reg::R1, BV::from_i64(3, 32)); // Rn (quotient)
3068 state.set_reg(&Reg::R2, BV::from_i64(5, 32)); // Rm (divisor)
3069
3070 let mls_op = ArmOp::Mls {
3071 rd: Reg::R3,
3072 rn: Reg::R1,
3073 rm: Reg::R2,
3074 ra: Reg::R0,
3075 };
3076 encoder.encode_op(&mls_op, &mut state);
3077 assert_eq!(
3078 state.get_reg(&Reg::R3).simplify().as_i64(),
3079 Some(2),
3080 "MLS: 17 - 3*5 = 2"
3081 );
3082
3083 // Test: 100 - 7 * 3 = 100 - 21 = 79
3084 state.set_reg(&Reg::R0, BV::from_i64(100, 32));
3085 state.set_reg(&Reg::R1, BV::from_i64(7, 32));
3086 state.set_reg(&Reg::R2, BV::from_i64(3, 32));
3087
3088 let mls_op2 = ArmOp::Mls {
3089 rd: Reg::R3,
3090 rn: Reg::R1,
3091 rm: Reg::R2,
3092 ra: Reg::R0,
3093 };
3094 encoder.encode_op(&mls_op2, &mut state);
3095 assert_eq!(
3096 state.get_reg(&Reg::R3).simplify().as_i64(),
3097 Some(79),
3098 "MLS: 100 - 7*3 = 79"
3099 );
3100
3101 // Test with negative numbers: (-17) - 3 * 5 = -17 - 15 = -32
3102 state.set_reg(&Reg::R0, BV::from_i64(-17, 32));
3103 state.set_reg(&Reg::R1, BV::from_i64(3, 32));
3104 state.set_reg(&Reg::R2, BV::from_i64(5, 32));
3105
3106 let mls_op3 = ArmOp::Mls {
3107 rd: Reg::R3,
3108 rn: Reg::R1,
3109 rm: Reg::R2,
3110 ra: Reg::R0,
3111 };
3112 encoder.encode_op(&mls_op3, &mut state);
3113 // Result is -32, but as_i64() returns unsigned, so we need to convert
3114 let result = state.get_reg(&Reg::R3).simplify().as_i64();
3115 let signed_result = result.map(|v| (v as i32) as i64);
3116 assert_eq!(signed_result, Some(-32), "MLS: -17 - 3*5 = -32");
3117 });
3118 }
3119
3120 #[test]
3121 fn test_arm_shift_ops() {
3122 with_verification_context(|| {
3123 let encoder = ArmSemantics::new();
3124 let mut state = ArmState::new_symbolic();
3125
3126 state.set_reg(&Reg::R1, BV::from_i64(8, 32));
3127
3128 // Test LSL (logical shift left) with immediate
3129 let lsl_op = ArmOp::Lsl {
3130 rd: Reg::R0,
3131 rn: Reg::R1,
3132 shift: 2,
3133 };
3134 encoder.encode_op(&lsl_op, &mut state);
3135 assert_eq!(state.get_reg(&Reg::R0).simplify().as_i64(), Some(32));
3136
3137 // Test LSR (logical shift right) with immediate
3138 let lsr_op = ArmOp::Lsr {
3139 rd: Reg::R0,
3140 rn: Reg::R1,
3141 shift: 2,
3142 };
3143 encoder.encode_op(&lsr_op, &mut state);
3144 assert_eq!(state.get_reg(&Reg::R0).simplify().as_i64(), Some(2));
3145 });
3146 }
3147
3148 #[test]
3149 fn test_arm_ror_comprehensive() {
3150 with_verification_context(|| {
3151 let encoder = ArmSemantics::new();
3152 let mut state = ArmState::new_symbolic();
3153
3154 // Test ROR with 0x12345678
3155 // ROR by 8 should rotate right by 8 bits
3156 state.set_reg(&Reg::R1, BV::from_u64(0x12345678, 32));
3157 let ror_op = ArmOp::Ror {
3158 rd: Reg::R0,
3159 rn: Reg::R1,
3160 shift: 8,
3161 };
3162 encoder.encode_op(&ror_op, &mut state);
3163 // 0x12345678 ROR 8 = 0x78123456
3164 assert_eq!(
3165 state.get_reg(&Reg::R0).simplify().as_i64(),
3166 Some(0x78123456),
3167 "ROR by 8"
3168 );
3169
3170 // Test ROR by 16 (swap halves)
3171 let ror_op_16 = ArmOp::Ror {
3172 rd: Reg::R0,
3173 rn: Reg::R1,
3174 shift: 16,
3175 };
3176 encoder.encode_op(&ror_op_16, &mut state);
3177 // 0x12345678 ROR 16 = 0x56781234
3178 assert_eq!(
3179 state.get_reg(&Reg::R0).simplify().as_i64(),
3180 Some(0x56781234),
3181 "ROR by 16"
3182 );
3183
3184 // Test ROR by 0 (no change)
3185 let ror_op_0 = ArmOp::Ror {
3186 rd: Reg::R0,
3187 rn: Reg::R1,
3188 shift: 0,
3189 };
3190 encoder.encode_op(&ror_op_0, &mut state);
3191 assert_eq!(
3192 state.get_reg(&Reg::R0).simplify().as_i64(),
3193 Some(0x12345678),
3194 "ROR by 0"
3195 );
3196
3197 // Test ROR by 32 (full rotation, back to original)
3198 let ror_op_32 = ArmOp::Ror {
3199 rd: Reg::R0,
3200 rn: Reg::R1,
3201 shift: 32,
3202 };
3203 encoder.encode_op(&ror_op_32, &mut state);
3204 assert_eq!(
3205 state.get_reg(&Reg::R0).simplify().as_i64(),
3206 Some(0x12345678),
3207 "ROR by 32"
3208 );
3209
3210 // Test ROR by 4 (nibble rotation)
3211 state.set_reg(&Reg::R1, BV::from_u64(0xABCDEF01, 32));
3212 let ror_op_4 = ArmOp::Ror {
3213 rd: Reg::R0,
3214 rn: Reg::R1,
3215 shift: 4,
3216 };
3217 encoder.encode_op(&ror_op_4, &mut state);
3218 // 0xABCDEF01 ROR 4 = 0x1ABCDEF0
3219 assert_eq!(
3220 state.get_reg(&Reg::R0).simplify().as_i64(),
3221 Some(0x1ABCDEF0),
3222 "ROR by 4"
3223 );
3224
3225 // Test ROR with 1-bit rotation
3226 state.set_reg(&Reg::R1, BV::from_u64(0x80000001, 32));
3227 let ror_op_1 = ArmOp::Ror {
3228 rd: Reg::R0,
3229 rn: Reg::R1,
3230 shift: 1,
3231 };
3232 encoder.encode_op(&ror_op_1, &mut state);
3233 // 0x80000001 ROR 1 = 0xC0000000
3234 let result = state.get_reg(&Reg::R0).simplify().as_i64();
3235 let signed_result = result.map(|v| (v as i32) as i64);
3236 assert_eq!(
3237 signed_result,
3238 Some(0xC0000000_u32 as i32 as i64),
3239 "ROR by 1"
3240 );
3241 });
3242 }
3243
3244 #[test]
3245 fn test_arm_clz_comprehensive() {
3246 with_verification_context(|| {
3247 let encoder = ArmSemantics::new();
3248 let mut state = ArmState::new_symbolic();
3249
3250 // Test CLZ(0) = 32
3251 state.set_reg(&Reg::R1, BV::from_i64(0, 32));
3252 let clz_op = ArmOp::Clz {
3253 rd: Reg::R0,
3254 rm: Reg::R1,
3255 };
3256 encoder.encode_op(&clz_op, &mut state);
3257 assert_eq!(
3258 state.get_reg(&Reg::R0).simplify().as_i64(),
3259 Some(32),
3260 "CLZ(0) should be 32"
3261 );
3262
3263 // Test CLZ(1) = 31
3264 state.set_reg(&Reg::R1, BV::from_i64(1, 32));
3265 encoder.encode_op(&clz_op, &mut state);
3266 assert_eq!(
3267 state.get_reg(&Reg::R0).simplify().as_i64(),
3268 Some(31),
3269 "CLZ(1) should be 31"
3270 );
3271
3272 // Test CLZ(0x80000000) = 0
3273 state.set_reg(&Reg::R1, BV::from_u64(0x80000000, 32));
3274 encoder.encode_op(&clz_op, &mut state);
3275 assert_eq!(
3276 state.get_reg(&Reg::R0).simplify().as_i64(),
3277 Some(0),
3278 "CLZ(0x80000000) should be 0"
3279 );
3280
3281 // Test CLZ(0x00FF0000) = 8
3282 state.set_reg(&Reg::R1, BV::from_u64(0x00FF0000, 32));
3283 encoder.encode_op(&clz_op, &mut state);
3284 assert_eq!(
3285 state.get_reg(&Reg::R0).simplify().as_i64(),
3286 Some(8),
3287 "CLZ(0x00FF0000) should be 8"
3288 );
3289
3290 // Test CLZ(0x00001000) = 19
3291 state.set_reg(&Reg::R1, BV::from_u64(0x00001000, 32));
3292 encoder.encode_op(&clz_op, &mut state);
3293 assert_eq!(
3294 state.get_reg(&Reg::R0).simplify().as_i64(),
3295 Some(19),
3296 "CLZ(0x00001000) should be 19"
3297 );
3298
3299 // Test CLZ(0xFFFFFFFF) = 0
3300 state.set_reg(&Reg::R1, BV::from_u64(0xFFFFFFFF, 32));
3301 encoder.encode_op(&clz_op, &mut state);
3302 assert_eq!(
3303 state.get_reg(&Reg::R0).simplify().as_i64(),
3304 Some(0),
3305 "CLZ(0xFFFFFFFF) should be 0"
3306 );
3307 });
3308 }
3309
3310 #[test]
3311 fn test_arm_rbit_comprehensive() {
3312 with_verification_context(|| {
3313 let encoder = ArmSemantics::new();
3314 let mut state = ArmState::new_symbolic();
3315
3316 let rbit_op = ArmOp::Rbit {
3317 rd: Reg::R0,
3318 rm: Reg::R1,
3319 };
3320
3321 // Test RBIT(0) = 0
3322 state.set_reg(&Reg::R1, BV::from_i64(0, 32));
3323 encoder.encode_op(&rbit_op, &mut state);
3324 assert_eq!(
3325 state.get_reg(&Reg::R0).simplify().as_i64(),
3326 Some(0),
3327 "RBIT(0) should be 0"
3328 );
3329
3330 // Test RBIT(1) = 0x80000000 (bit 0 → bit 31)
3331 state.set_reg(&Reg::R1, BV::from_i64(1, 32));
3332 encoder.encode_op(&rbit_op, &mut state);
3333 assert_eq!(
3334 state.get_reg(&Reg::R0).simplify().as_u64(),
3335 Some(0x80000000),
3336 "RBIT(1) should be 0x80000000"
3337 );
3338
3339 // Test RBIT(0x80000000) = 1 (bit 31 → bit 0)
3340 state.set_reg(&Reg::R1, BV::from_u64(0x80000000, 32));
3341 encoder.encode_op(&rbit_op, &mut state);
3342 assert_eq!(
3343 state.get_reg(&Reg::R0).simplify().as_i64(),
3344 Some(1),
3345 "RBIT(0x80000000) should be 1"
3346 );
3347
3348 // Test RBIT(0xFF000000) = 0x000000FF (top byte → bottom byte)
3349 state.set_reg(&Reg::R1, BV::from_u64(0xFF000000, 32));
3350 encoder.encode_op(&rbit_op, &mut state);
3351 assert_eq!(
3352 state.get_reg(&Reg::R0).simplify().as_u64(),
3353 Some(0x000000FF),
3354 "RBIT(0xFF000000) should be 0x000000FF"
3355 );
3356
3357 // Test RBIT(0x12345678) - specific pattern
3358 state.set_reg(&Reg::R1, BV::from_u64(0x12345678, 32));
3359 encoder.encode_op(&rbit_op, &mut state);
3360 // 0x12345678 reversed = 0x1E6A2C48
3361 assert_eq!(
3362 state.get_reg(&Reg::R0).simplify().as_u64(),
3363 Some(0x1E6A2C48),
3364 "RBIT(0x12345678) should be 0x1E6A2C48"
3365 );
3366
3367 // Test RBIT(0xFFFFFFFF) = 0xFFFFFFFF (all bits stay)
3368 state.set_reg(&Reg::R1, BV::from_u64(0xFFFFFFFF, 32));
3369 encoder.encode_op(&rbit_op, &mut state);
3370 assert_eq!(
3371 state.get_reg(&Reg::R0).simplify().as_u64(),
3372 Some(0xFFFFFFFF),
3373 "RBIT(0xFFFFFFFF) should be 0xFFFFFFFF"
3374 );
3375 });
3376 }
3377
3378 #[test]
3379 fn test_arm_cmp_flags() {
3380 // Test CMP instruction and condition flag updates
3381
3382 with_verification_context(|| {
3383 let encoder = ArmSemantics::new();
3384 let mut state = ArmState::new_symbolic();
3385
3386 // Test 1: CMP with equal values (10 - 10 = 0)
3387 // Should set: Z=1, N=0, C=1 (no borrow), V=0
3388 state.set_reg(&Reg::R0, BV::from_i64(10, 32));
3389 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
3390
3391 let cmp_op = ArmOp::Cmp {
3392 rn: Reg::R0,
3393 op2: Operand2::Reg(Reg::R1),
3394 };
3395 encoder.encode_op(&cmp_op, &mut state);
3396
3397 assert_eq!(
3398 state.flags.z.simplify().as_bool(),
3399 Some(true),
3400 "Z flag should be set (equal)"
3401 );
3402 assert_eq!(
3403 state.flags.n.simplify().as_bool(),
3404 Some(false),
3405 "N flag should be clear (non-negative)"
3406 );
3407 assert_eq!(
3408 state.flags.c.simplify().as_bool(),
3409 Some(true),
3410 "C flag should be set (no borrow)"
3411 );
3412 assert_eq!(
3413 state.flags.v.simplify().as_bool(),
3414 Some(false),
3415 "V flag should be clear (no overflow)"
3416 );
3417
3418 // Test 2: CMP with first > second (20 - 10 = 10)
3419 // Should set: Z=0, N=0, C=1 (no borrow), V=0
3420 state.set_reg(&Reg::R0, BV::from_i64(20, 32));
3421 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
3422 encoder.encode_op(&cmp_op, &mut state);
3423
3424 assert_eq!(
3425 state.flags.z.simplify().as_bool(),
3426 Some(false),
3427 "Z flag should be clear (not equal)"
3428 );
3429 assert_eq!(
3430 state.flags.n.simplify().as_bool(),
3431 Some(false),
3432 "N flag should be clear (positive result)"
3433 );
3434 assert_eq!(
3435 state.flags.c.simplify().as_bool(),
3436 Some(true),
3437 "C flag should be set (no borrow)"
3438 );
3439 assert_eq!(
3440 state.flags.v.simplify().as_bool(),
3441 Some(false),
3442 "V flag should be clear (no overflow)"
3443 );
3444
3445 // Test 3: CMP with first < second (unsigned: will wrap)
3446 // 10 - 20 = -10 (0xFFFFFFF6 in two's complement)
3447 // Should set: Z=0, N=1 (negative), C=0 (borrow), V=0
3448 state.set_reg(&Reg::R0, BV::from_i64(10, 32));
3449 state.set_reg(&Reg::R1, BV::from_i64(20, 32));
3450 encoder.encode_op(&cmp_op, &mut state);
3451
3452 assert_eq!(
3453 state.flags.z.simplify().as_bool(),
3454 Some(false),
3455 "Z flag should be clear"
3456 );
3457 assert_eq!(
3458 state.flags.n.simplify().as_bool(),
3459 Some(true),
3460 "N flag should be set (negative result)"
3461 );
3462 assert_eq!(
3463 state.flags.c.simplify().as_bool(),
3464 Some(false),
3465 "C flag should be clear (borrow occurred)"
3466 );
3467 assert_eq!(
3468 state.flags.v.simplify().as_bool(),
3469 Some(false),
3470 "V flag should be clear"
3471 );
3472
3473 // Test 4: Signed overflow case
3474 // Subtracting large negative from positive should overflow
3475 // 0x7FFFFFFF (max positive) - 0x80000000 (min negative)
3476 // Result wraps to negative, but mathematically should be huge positive
3477 state.set_reg(&Reg::R0, BV::from_i64(0x7FFFFFFF, 32));
3478 state.set_reg(&Reg::R1, BV::from_i64(-2147483648i64, 32)); // 0x80000000
3479 encoder.encode_op(&cmp_op, &mut state);
3480
3481 assert_eq!(
3482 state.flags.z.simplify().as_bool(),
3483 Some(false),
3484 "Z flag should be clear"
3485 );
3486 assert_eq!(
3487 state.flags.n.simplify().as_bool(),
3488 Some(true),
3489 "N flag should be set (wrapped result)"
3490 );
3491 assert_eq!(
3492 state.flags.c.simplify().as_bool(),
3493 Some(false),
3494 "C flag should be clear"
3495 );
3496 assert_eq!(
3497 state.flags.v.simplify().as_bool(),
3498 Some(true),
3499 "V flag should be set (overflow)"
3500 );
3501
3502 // Test 5: Zero comparison
3503 state.set_reg(&Reg::R0, BV::from_i64(0, 32));
3504 state.set_reg(&Reg::R1, BV::from_i64(0, 32));
3505 encoder.encode_op(&cmp_op, &mut state);
3506
3507 assert_eq!(
3508 state.flags.z.simplify().as_bool(),
3509 Some(true),
3510 "Z flag should be set (0 - 0 = 0)"
3511 );
3512 assert_eq!(
3513 state.flags.n.simplify().as_bool(),
3514 Some(false),
3515 "N flag should be clear"
3516 );
3517 assert_eq!(
3518 state.flags.c.simplify().as_bool(),
3519 Some(true),
3520 "C flag should be set"
3521 );
3522 assert_eq!(
3523 state.flags.v.simplify().as_bool(),
3524 Some(false),
3525 "V flag should be clear"
3526 );
3527 });
3528 }
3529
3530 #[test]
3531 fn test_arm_flags_all_combinations() {
3532 // Test that flags correctly distinguish all comparison outcomes
3533
3534 with_verification_context(|| {
3535 let encoder = ArmSemantics::new();
3536 let mut state = ArmState::new_symbolic();
3537
3538 let cmp_op = ArmOp::Cmp {
3539 rn: Reg::R0,
3540 op2: Operand2::Reg(Reg::R1),
3541 };
3542
3543 // Test signed comparisons using flags
3544 // For signed comparison A vs B (after CMP A, B):
3545 // - EQ (equal): Z=1
3546 // - NE (not equal): Z=0
3547 // - LT (less than): N != V
3548 // - LE (less or equal): Z=1 OR (N != V)
3549 // - GT (greater than): Z=0 AND (N == V)
3550 // - GE (greater or equal): N == V
3551
3552 // Case: 5 compared to 10 (5 < 10)
3553 state.set_reg(&Reg::R0, BV::from_i64(5, 32));
3554 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
3555 encoder.encode_op(&cmp_op, &mut state);
3556
3557 let n = state.flags.n.simplify().as_bool().unwrap();
3558 let z = state.flags.z.simplify().as_bool().unwrap();
3559 let v = state.flags.v.simplify().as_bool().unwrap();
3560
3561 assert!(!z, "Not equal");
3562 assert!(n != v, "5 < 10 signed (N != V)");
3563
3564 // Case: -5 compared to 10 (-5 < 10)
3565 state.set_reg(&Reg::R0, BV::from_i64(-5, 32));
3566 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
3567 encoder.encode_op(&cmp_op, &mut state);
3568
3569 let n = state.flags.n.simplify().as_bool().unwrap();
3570 let v = state.flags.v.simplify().as_bool().unwrap();
3571 assert!(n != v, "-5 < 10 signed (N != V)");
3572 });
3573 }
3574
3575 #[test]
3576 fn test_arm_setcond_eq() {
3577 with_verification_context(|| {
3578 let encoder = ArmSemantics::new();
3579 let mut state = ArmState::new_symbolic();
3580
3581 // Test EQ condition: 10 == 10
3582 state.set_reg(&Reg::R0, BV::from_i64(10, 32));
3583 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
3584
3585 // CMP R0, R1 (sets Z=1 since equal)
3586 let cmp_op = ArmOp::Cmp {
3587 rn: Reg::R0,
3588 op2: Operand2::Reg(Reg::R1),
3589 };
3590 encoder.encode_op(&cmp_op, &mut state);
3591
3592 // SetCond R0, EQ (should set R0 = 1)
3593 let setcond_op = ArmOp::SetCond {
3594 rd: Reg::R0,
3595 cond: synth_synthesis::Condition::EQ,
3596 };
3597 encoder.encode_op(&setcond_op, &mut state);
3598
3599 assert_eq!(
3600 state.get_reg(&Reg::R0).simplify().as_i64(),
3601 Some(1),
3602 "EQ condition (10 == 10) should return 1"
3603 );
3604
3605 // Test NE condition: 10 != 5
3606 state.set_reg(&Reg::R0, BV::from_i64(10, 32));
3607 state.set_reg(&Reg::R1, BV::from_i64(5, 32));
3608
3609 encoder.encode_op(&cmp_op, &mut state);
3610
3611 let setcond_ne = ArmOp::SetCond {
3612 rd: Reg::R0,
3613 cond: synth_synthesis::Condition::NE,
3614 };
3615 encoder.encode_op(&setcond_ne, &mut state);
3616
3617 assert_eq!(
3618 state.get_reg(&Reg::R0).simplify().as_i64(),
3619 Some(1),
3620 "NE condition (10 != 5) should return 1"
3621 );
3622 });
3623 }
3624
3625 #[test]
3626 fn test_arm_setcond_signed() {
3627 with_verification_context(|| {
3628 let encoder = ArmSemantics::new();
3629 let mut state = ArmState::new_symbolic();
3630
3631 // Test LT signed: 5 < 10
3632 state.set_reg(&Reg::R0, BV::from_i64(5, 32));
3633 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
3634
3635 let cmp_op = ArmOp::Cmp {
3636 rn: Reg::R0,
3637 op2: Operand2::Reg(Reg::R1),
3638 };
3639 encoder.encode_op(&cmp_op, &mut state);
3640
3641 let setcond_lt = ArmOp::SetCond {
3642 rd: Reg::R0,
3643 cond: synth_synthesis::Condition::LT,
3644 };
3645 encoder.encode_op(&setcond_lt, &mut state);
3646
3647 assert_eq!(
3648 state.get_reg(&Reg::R0).simplify().as_i64(),
3649 Some(1),
3650 "LT signed (5 < 10) should return 1"
3651 );
3652
3653 // Test GE signed: 10 >= 5
3654 state.set_reg(&Reg::R0, BV::from_i64(10, 32));
3655 state.set_reg(&Reg::R1, BV::from_i64(5, 32));
3656
3657 encoder.encode_op(&cmp_op, &mut state);
3658
3659 let setcond_ge = ArmOp::SetCond {
3660 rd: Reg::R0,
3661 cond: synth_synthesis::Condition::GE,
3662 };
3663 encoder.encode_op(&setcond_ge, &mut state);
3664
3665 assert_eq!(
3666 state.get_reg(&Reg::R0).simplify().as_i64(),
3667 Some(1),
3668 "GE signed (10 >= 5) should return 1"
3669 );
3670
3671 // Test GT signed: 10 > 5
3672 state.set_reg(&Reg::R0, BV::from_i64(10, 32));
3673 state.set_reg(&Reg::R1, BV::from_i64(5, 32));
3674
3675 encoder.encode_op(&cmp_op, &mut state);
3676
3677 let setcond_gt = ArmOp::SetCond {
3678 rd: Reg::R0,
3679 cond: synth_synthesis::Condition::GT,
3680 };
3681 encoder.encode_op(&setcond_gt, &mut state);
3682
3683 assert_eq!(
3684 state.get_reg(&Reg::R0).simplify().as_i64(),
3685 Some(1),
3686 "GT signed (10 > 5) should return 1"
3687 );
3688
3689 // Test LE signed: 5 <= 10
3690 state.set_reg(&Reg::R0, BV::from_i64(5, 32));
3691 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
3692
3693 encoder.encode_op(&cmp_op, &mut state);
3694
3695 let setcond_le = ArmOp::SetCond {
3696 rd: Reg::R0,
3697 cond: synth_synthesis::Condition::LE,
3698 };
3699 encoder.encode_op(&setcond_le, &mut state);
3700
3701 assert_eq!(
3702 state.get_reg(&Reg::R0).simplify().as_i64(),
3703 Some(1),
3704 "LE signed (5 <= 10) should return 1"
3705 );
3706 });
3707 }
3708
3709 #[test]
3710 fn test_arm_setcond_unsigned() {
3711 with_verification_context(|| {
3712 let encoder = ArmSemantics::new();
3713 let mut state = ArmState::new_symbolic();
3714
3715 // Test LO unsigned: 5 < 10
3716 state.set_reg(&Reg::R0, BV::from_i64(5, 32));
3717 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
3718
3719 let cmp_op = ArmOp::Cmp {
3720 rn: Reg::R0,
3721 op2: Operand2::Reg(Reg::R1),
3722 };
3723 encoder.encode_op(&cmp_op, &mut state);
3724
3725 let setcond_lo = ArmOp::SetCond {
3726 rd: Reg::R0,
3727 cond: synth_synthesis::Condition::LO,
3728 };
3729 encoder.encode_op(&setcond_lo, &mut state);
3730
3731 assert_eq!(
3732 state.get_reg(&Reg::R0).simplify().as_i64(),
3733 Some(1),
3734 "LO unsigned (5 < 10) should return 1"
3735 );
3736
3737 // Test HS unsigned: 10 >= 5
3738 state.set_reg(&Reg::R0, BV::from_i64(10, 32));
3739 state.set_reg(&Reg::R1, BV::from_i64(5, 32));
3740
3741 encoder.encode_op(&cmp_op, &mut state);
3742
3743 let setcond_hs = ArmOp::SetCond {
3744 rd: Reg::R0,
3745 cond: synth_synthesis::Condition::HS,
3746 };
3747 encoder.encode_op(&setcond_hs, &mut state);
3748
3749 assert_eq!(
3750 state.get_reg(&Reg::R0).simplify().as_i64(),
3751 Some(1),
3752 "HS unsigned (10 >= 5) should return 1"
3753 );
3754
3755 // Test HI unsigned: 10 > 5
3756 state.set_reg(&Reg::R0, BV::from_i64(10, 32));
3757 state.set_reg(&Reg::R1, BV::from_i64(5, 32));
3758
3759 encoder.encode_op(&cmp_op, &mut state);
3760
3761 let setcond_hi = ArmOp::SetCond {
3762 rd: Reg::R0,
3763 cond: synth_synthesis::Condition::HI,
3764 };
3765 encoder.encode_op(&setcond_hi, &mut state);
3766
3767 assert_eq!(
3768 state.get_reg(&Reg::R0).simplify().as_i64(),
3769 Some(1),
3770 "HI unsigned (10 > 5) should return 1"
3771 );
3772
3773 // Test LS unsigned: 5 <= 10
3774 state.set_reg(&Reg::R0, BV::from_i64(5, 32));
3775 state.set_reg(&Reg::R1, BV::from_i64(10, 32));
3776
3777 encoder.encode_op(&cmp_op, &mut state);
3778
3779 let setcond_ls = ArmOp::SetCond {
3780 rd: Reg::R0,
3781 cond: synth_synthesis::Condition::LS,
3782 };
3783 encoder.encode_op(&setcond_ls, &mut state);
3784
3785 assert_eq!(
3786 state.get_reg(&Reg::R0).simplify().as_i64(),
3787 Some(1),
3788 "LS unsigned (5 <= 10) should return 1"
3789 );
3790 });
3791 }
3792}