synth_verify/
wasm_semantics.rs

1//! WASM Semantics Encoding to SMT
2//!
3//! Encodes WebAssembly operation semantics as SMT bitvector formulas.
4//! Each WASM operation is translated to a mathematical formula that precisely
5//! captures its behavior.
6
7use crate::term::{BV, Bool};
8use synth_core::WasmOp;
9
10/// WASM semantics encoder
11///
12/// Z3 0.19 uses thread-local context -- no lifetime parameters needed.
13pub struct WasmSemantics {
14    /// Memory model: maps addresses to 32-bit values
15    /// For bounded verification, we use a limited memory space
16    #[allow(dead_code)]
17    memory: Vec<BV>,
18}
19
20impl Default for WasmSemantics {
21    fn default() -> Self {
22        Self::new()
23    }
24}
25
26impl WasmSemantics {
27    /// Create a new WASM semantics encoder
28    pub fn new() -> Self {
29        // Initialize bounded memory (256 32-bit words)
30        let memory = (0..256)
31            .map(|i| BV::new_const(format!("mem_{}", i), 32))
32            .collect();
33
34        Self { memory }
35    }
36
37    /// Create encoder with mutable memory for load/store operations
38    pub fn new_with_memory(memory: Vec<BV>) -> Self {
39        Self { memory }
40    }
41
42    /// Encode a WASM operation as an SMT formula
43    ///
44    /// Returns a bitvector representing the result of the operation.
45    /// For operations with multiple operands, inputs are provided as a slice.
46    pub fn encode_op(&self, op: &WasmOp, inputs: &[BV]) -> BV {
47        match op {
48            // Arithmetic operations
49            WasmOp::I32Add => {
50                assert_eq!(inputs.len(), 2, "I32Add requires 2 inputs");
51                inputs[0].bvadd(&inputs[1])
52            }
53
54            WasmOp::I32Sub => {
55                assert_eq!(inputs.len(), 2, "I32Sub requires 2 inputs");
56                inputs[0].bvsub(&inputs[1])
57            }
58
59            WasmOp::I32Mul => {
60                assert_eq!(inputs.len(), 2, "I32Mul requires 2 inputs");
61                inputs[0].bvmul(&inputs[1])
62            }
63
64            WasmOp::I32DivS => {
65                assert_eq!(inputs.len(), 2, "I32DivS requires 2 inputs");
66                inputs[0].bvsdiv(&inputs[1])
67            }
68
69            WasmOp::I32DivU => {
70                assert_eq!(inputs.len(), 2, "I32DivU requires 2 inputs");
71                inputs[0].bvudiv(&inputs[1])
72            }
73
74            WasmOp::I32RemS => {
75                assert_eq!(inputs.len(), 2, "I32RemS requires 2 inputs");
76                inputs[0].bvsrem(&inputs[1])
77            }
78
79            WasmOp::I32RemU => {
80                assert_eq!(inputs.len(), 2, "I32RemU requires 2 inputs");
81                inputs[0].bvurem(&inputs[1])
82            }
83
84            // Bitwise operations
85            WasmOp::I32And => {
86                assert_eq!(inputs.len(), 2, "I32And requires 2 inputs");
87                inputs[0].bvand(&inputs[1])
88            }
89
90            WasmOp::I32Or => {
91                assert_eq!(inputs.len(), 2, "I32Or requires 2 inputs");
92                inputs[0].bvor(&inputs[1])
93            }
94
95            WasmOp::I32Xor => {
96                assert_eq!(inputs.len(), 2, "I32Xor requires 2 inputs");
97                inputs[0].bvxor(&inputs[1])
98            }
99
100            WasmOp::I32Shl => {
101                assert_eq!(inputs.len(), 2, "I32Shl requires 2 inputs");
102                // WASM spec: shift amount is modulo 32
103                let shift_mod = inputs[1].bvurem(BV::from_i64(32, 32));
104                inputs[0].bvshl(&shift_mod)
105            }
106
107            WasmOp::I32ShrS => {
108                assert_eq!(inputs.len(), 2, "I32ShrS requires 2 inputs");
109                // WASM spec: shift amount is modulo 32
110                let shift_mod = inputs[1].bvurem(BV::from_i64(32, 32));
111                inputs[0].bvashr(&shift_mod)
112            }
113
114            WasmOp::I32ShrU => {
115                assert_eq!(inputs.len(), 2, "I32ShrU requires 2 inputs");
116                // WASM spec: shift amount is modulo 32
117                let shift_mod = inputs[1].bvurem(BV::from_i64(32, 32));
118                inputs[0].bvlshr(&shift_mod)
119            }
120
121            WasmOp::I32Rotl => {
122                assert_eq!(inputs.len(), 2, "I32Rotl requires 2 inputs");
123                // WASM spec: rotation amount is modulo 32
124                let shift_mod = inputs[1].bvurem(BV::from_i64(32, 32));
125                inputs[0].bvrotl(&shift_mod)
126            }
127
128            WasmOp::I32Rotr => {
129                assert_eq!(inputs.len(), 2, "I32Rotr requires 2 inputs");
130                // WASM spec: rotation amount is modulo 32
131                let shift_mod = inputs[1].bvurem(BV::from_i64(32, 32));
132                inputs[0].bvrotr(&shift_mod)
133            }
134
135            WasmOp::I32Clz => {
136                assert_eq!(inputs.len(), 1, "I32Clz requires 1 input");
137                // Count leading zeros - use bit tricks
138                self.encode_clz(&inputs[0])
139            }
140
141            WasmOp::I32Ctz => {
142                assert_eq!(inputs.len(), 1, "I32Ctz requires 1 input");
143                // Count trailing zeros - use bit tricks
144                self.encode_ctz(&inputs[0])
145            }
146
147            WasmOp::I32Popcnt => {
148                assert_eq!(inputs.len(), 1, "I32Popcnt requires 1 input");
149                // Population count - count 1 bits
150                self.encode_popcnt(&inputs[0])
151            }
152
153            // Constants
154            WasmOp::I32Const(value) => {
155                assert_eq!(inputs.len(), 0, "I32Const requires 0 inputs");
156                BV::from_i64(*value as i64, 32)
157            }
158
159            // Comparison operations (return i32: 0 or 1)
160            WasmOp::I32Eqz => {
161                assert_eq!(inputs.len(), 1, "I32Eqz requires 1 input");
162                let zero = BV::from_i64(0, 32);
163                let cond = inputs[0].eq(&zero);
164                self.bool_to_bv32(&cond)
165            }
166
167            WasmOp::I32Eq => {
168                assert_eq!(inputs.len(), 2, "I32Eq requires 2 inputs");
169                let cond = inputs[0].eq(&inputs[1]);
170                self.bool_to_bv32(&cond)
171            }
172
173            WasmOp::I32Ne => {
174                assert_eq!(inputs.len(), 2, "I32Ne requires 2 inputs");
175                let cond = inputs[0].eq(&inputs[1]).not();
176                self.bool_to_bv32(&cond)
177            }
178
179            WasmOp::I32LtS => {
180                assert_eq!(inputs.len(), 2, "I32LtS requires 2 inputs");
181                let cond = inputs[0].bvslt(&inputs[1]);
182                self.bool_to_bv32(&cond)
183            }
184
185            WasmOp::I32LtU => {
186                assert_eq!(inputs.len(), 2, "I32LtU requires 2 inputs");
187                let cond = inputs[0].bvult(&inputs[1]);
188                self.bool_to_bv32(&cond)
189            }
190
191            WasmOp::I32LeS => {
192                assert_eq!(inputs.len(), 2, "I32LeS requires 2 inputs");
193                let cond = inputs[0].bvsle(&inputs[1]);
194                self.bool_to_bv32(&cond)
195            }
196
197            WasmOp::I32LeU => {
198                assert_eq!(inputs.len(), 2, "I32LeU requires 2 inputs");
199                let cond = inputs[0].bvule(&inputs[1]);
200                self.bool_to_bv32(&cond)
201            }
202
203            WasmOp::I32GtS => {
204                assert_eq!(inputs.len(), 2, "I32GtS requires 2 inputs");
205                let cond = inputs[0].bvsgt(&inputs[1]);
206                self.bool_to_bv32(&cond)
207            }
208
209            WasmOp::I32GtU => {
210                assert_eq!(inputs.len(), 2, "I32GtU requires 2 inputs");
211                let cond = inputs[0].bvugt(&inputs[1]);
212                self.bool_to_bv32(&cond)
213            }
214
215            WasmOp::I32GeS => {
216                assert_eq!(inputs.len(), 2, "I32GeS requires 2 inputs");
217                let cond = inputs[0].bvsge(&inputs[1]);
218                self.bool_to_bv32(&cond)
219            }
220
221            WasmOp::I32GeU => {
222                assert_eq!(inputs.len(), 2, "I32GeU requires 2 inputs");
223                let cond = inputs[0].bvuge(&inputs[1]);
224                self.bool_to_bv32(&cond)
225            }
226
227            // Control flow operations
228            WasmOp::Select => {
229                assert_eq!(inputs.len(), 3, "Select requires 3 inputs");
230                // Select returns inputs[0] if inputs[2] != 0, else inputs[1]
231                // WASM spec: select(val1, val2, cond) = cond ? val1 : val2
232                let zero = BV::from_i64(0, 32);
233                let cond = inputs[2].eq(&zero).not(); // cond != 0
234                cond.ite(&inputs[0], &inputs[1])
235            }
236
237            WasmOp::Drop => {
238                assert_eq!(inputs.len(), 1, "Drop requires 1 input");
239                // Drop discards the value - for verification, we return a dummy value
240                // In actual compilation, this operation doesn't produce a value
241                BV::from_i64(0, 32)
242            }
243
244            // Memory operations
245            WasmOp::I32Load { offset, .. } => {
246                assert_eq!(inputs.len(), 1, "I32Load requires 1 input (address)");
247                // Load from memory: mem[address + offset]
248                // For bounded verification, we model memory as array of symbolic values
249                let address = inputs[0].clone();
250                let offset_bv = BV::from_u64(*offset as u64, 32);
251                let _effective_addr = address.bvadd(&offset_bv);
252
253                // For simplicity, return symbolic value based on address
254                // A complete model would index into memory array
255                BV::new_const(format!("load_{}_{}", offset, address), 32)
256            }
257
258            WasmOp::I32Store { offset, .. } => {
259                assert_eq!(
260                    inputs.len(),
261                    2,
262                    "I32Store requires 2 inputs (address, value)"
263                );
264                // Store to memory: mem[address + offset] = value
265                // For verification, we model the effect without mutating state
266                let _address = inputs[0].clone();
267                let value = inputs[1].clone();
268                let _offset_bv = BV::from_u64(*offset as u64, 32);
269
270                // Store returns no value in WASM, but we return the stored value for verification
271                value
272            }
273
274            // Local/Global variable operations
275            WasmOp::LocalGet(index) => {
276                assert_eq!(inputs.len(), 0, "LocalGet requires 0 inputs");
277                // Return symbolic value representing local variable
278                BV::new_const(format!("local_{}", index), 32)
279            }
280
281            WasmOp::LocalSet(_index) => {
282                assert_eq!(inputs.len(), 1, "LocalSet requires 1 input");
283                // Set local variable (modeled as assignment)
284                // Return the value for verification purposes
285                inputs[0].clone()
286            }
287
288            WasmOp::LocalTee(_index) => {
289                assert_eq!(inputs.len(), 1, "LocalTee requires 1 input");
290                // Tee sets local and returns the value
291                inputs[0].clone()
292            }
293
294            WasmOp::GlobalGet(index) => {
295                assert_eq!(inputs.len(), 0, "GlobalGet requires 0 inputs");
296                // Return symbolic value representing global variable
297                BV::new_const(format!("global_{}", index), 32)
298            }
299
300            WasmOp::GlobalSet(_index) => {
301                assert_eq!(inputs.len(), 1, "GlobalSet requires 1 input");
302                // Set global variable (modeled as assignment)
303                // Return the value for verification purposes
304                inputs[0].clone()
305            }
306
307            // No-op operations
308            WasmOp::Nop => {
309                assert_eq!(inputs.len(), 0, "Nop requires 0 inputs");
310                // No operation - return zero
311                BV::from_i64(0, 32)
312            }
313
314            WasmOp::Unreachable => {
315                assert_eq!(inputs.len(), 0, "Unreachable requires 0 inputs");
316                // Unreachable - return symbolic value representing trap
317                BV::new_const("unreachable_trap", 32)
318            }
319
320            // Control flow operations
321            WasmOp::Block => {
322                assert_eq!(inputs.len(), 0, "Block requires 0 inputs");
323                // Block is a structure marker - return zero
324                BV::from_i64(0, 32)
325            }
326
327            WasmOp::Loop => {
328                assert_eq!(inputs.len(), 0, "Loop requires 0 inputs");
329                // Loop is a structure marker - return zero
330                BV::from_i64(0, 32)
331            }
332
333            WasmOp::End => {
334                assert_eq!(inputs.len(), 0, "End requires 0 inputs");
335                // End is a structure marker - return zero
336                BV::from_i64(0, 32)
337            }
338
339            WasmOp::Br(label) => {
340                assert_eq!(inputs.len(), 0, "Br requires 0 inputs");
341                // Branch to label - return symbolic control flow value
342                BV::new_const(format!("br_{}", label), 32)
343            }
344
345            WasmOp::BrIf(label) => {
346                assert_eq!(inputs.len(), 1, "BrIf requires 1 input (condition)");
347                // Conditional branch - return symbolic control flow value
348                // The condition determines whether branch is taken
349                let _cond = inputs[0].clone();
350                BV::new_const(format!("br_if_{}", label), 32)
351            }
352
353            WasmOp::Return => {
354                assert_eq!(inputs.len(), 0, "Return requires 0 inputs");
355                // Return from function - return symbolic control flow value
356                BV::new_const("return", 32)
357            }
358
359            WasmOp::If => {
360                // If is a structure marker with condition check
361                // For verification purposes, may be called without inputs
362                if !inputs.is_empty() {
363                    let _cond = inputs[0].clone();
364                }
365                BV::from_i64(0, 32)
366            }
367
368            WasmOp::Else => {
369                assert_eq!(inputs.len(), 0, "Else requires 0 inputs");
370                // Else is a structure marker
371                BV::from_i64(0, 32)
372            }
373
374            WasmOp::BrTable { targets, default } => {
375                // Multi-way branch based on index
376                // For verification purposes, may be called without inputs
377                // If index < len(targets), branch to targets[index]
378                // Otherwise, branch to default
379                if inputs.is_empty() {
380                    // Verification mode - return placeholder
381                    return BV::from_i64(0, 32);
382                }
383                let _index = inputs[0].clone();
384
385                // For verification, we model this as symbolic control flow
386                // A complete model would use nested ITEs to select the target
387                BV::new_const(format!("br_table_{}_{}", targets.len(), default), 32)
388            }
389
390            WasmOp::Call(func_idx) => {
391                // Function call - for verification, we model the call result symbolically
392                // A complete model would require analyzing the called function
393                // For now, we represent the result as a symbolic value
394                BV::new_const(format!("call_{}", func_idx), 32)
395            }
396
397            WasmOp::CallIndirect { type_index, .. } => {
398                // CallIndirect is a structural operation
399                // For verification purposes, may be called without inputs
400                if inputs.is_empty() {
401                    // Verification mode - return placeholder
402                    return BV::from_i64(0, 32);
403                }
404                // Indirect function call through table
405                // For verification, we model the call result symbolically
406                let _table_index = inputs[0].clone();
407                BV::new_const(format!("call_indirect_{}", type_index), 32)
408            }
409
410            // ================================================================
411            // i64 Operations (Phase 2) - Basic implementation
412            // ================================================================
413            // Note: These return 64-bit bitvectors, but current architecture
414            // expects 32-bit. For now, we truncate to 32-bit for compatibility.
415            // Full 64-bit support requires architectural changes.
416            WasmOp::I64Const(value) => {
417                assert_eq!(inputs.len(), 0, "I64Const requires 0 inputs");
418                // For now, truncate to 32-bit (low part)
419                // TODO: Full 64-bit support with register pairs
420                let low32 = (*value as i32) as i64;
421                BV::from_i64(low32, 32)
422            }
423
424            WasmOp::I64Add => {
425                assert_eq!(inputs.len(), 2, "I64Add requires 2 inputs");
426                // Simplified: treat as 32-bit for now
427                // TODO: Implement full 64-bit addition with carry
428                inputs[0].bvadd(&inputs[1])
429            }
430
431            WasmOp::I64Eqz => {
432                assert_eq!(inputs.len(), 1, "I64Eqz requires 1 input");
433                // Check if value is zero
434                // Simplified: 32-bit check for now
435                let zero = BV::from_i64(0, 32);
436                let cond = inputs[0].eq(&zero);
437                self.bool_to_bv32(&cond)
438            }
439
440            WasmOp::I32WrapI64 => {
441                assert_eq!(inputs.len(), 1, "I32WrapI64 requires 1 input");
442                // Wrap 64-bit to 32-bit (truncate)
443                // Already 32-bit in our simplified model
444                inputs[0].clone()
445            }
446
447            WasmOp::I64ExtendI32S => {
448                assert_eq!(inputs.len(), 1, "I64ExtendI32S requires 1 input");
449                // Sign-extend 32-bit to 64-bit
450                // In our simplified model, already 32-bit
451                // Full implementation would sign-extend to 64-bit
452                inputs[0].clone()
453            }
454
455            WasmOp::I64ExtendI32U => {
456                assert_eq!(inputs.len(), 1, "I64ExtendI32U requires 1 input");
457                // Zero-extend 32-bit to 64-bit
458                // In our simplified model, already 32-bit
459                inputs[0].clone()
460            }
461
462            // i64 Memory operations
463            WasmOp::I64Load { offset, .. } => {
464                assert_eq!(inputs.len(), 1, "I64Load requires 1 input (address)");
465                // Load 64-bit value from memory: mem[address + offset]
466                // In our simplified 32-bit model, return symbolic 32-bit value (low part)
467                // Full implementation would return 64-bit value
468                let address = inputs[0].clone();
469                let offset_bv = BV::from_u64(*offset as u64, 32);
470                let _effective_addr = address.bvadd(&offset_bv);
471
472                // Return symbolic value representing the low 32 bits of the loaded i64
473                BV::new_const(format!("i64load_{}_{}", offset, address), 32)
474            }
475
476            WasmOp::I64Store { offset, .. } => {
477                assert_eq!(
478                    inputs.len(),
479                    2,
480                    "I64Store requires 2 inputs (address, value)"
481                );
482                // Store 64-bit value to memory: mem[address + offset] = value
483                // In our simplified 32-bit model, store the 32-bit value
484                let _address = inputs[0].clone();
485                let value = inputs[1].clone();
486                let _offset_bv = BV::from_u64(*offset as u64, 32);
487
488                // Store returns no value in WASM, but we return the stored value for verification
489                value
490            }
491
492            // ========================================================================
493            // f32 Operations (Phase 2 - Floating Point)
494            // ========================================================================
495            // Note: f32 values represented as 32-bit bitvectors (IEEE 754 format)
496            WasmOp::F32Const(value) => {
497                // f32 constant value
498                // Convert f32 to IEEE 754 bit representation
499                let bits = value.to_bits() as i64;
500                BV::from_i64(bits, 32)
501            }
502
503            WasmOp::F32Add => {
504                assert_eq!(inputs.len(), 2, "F32Add requires 2 inputs");
505                // f32 addition (symbolic for verification)
506                BV::new_const("f32_add_result", 32)
507            }
508
509            WasmOp::F32Sub => {
510                assert_eq!(inputs.len(), 2, "F32Sub requires 2 inputs");
511                // f32 subtraction (symbolic for verification)
512                BV::new_const("f32_sub_result", 32)
513            }
514
515            WasmOp::F32Mul => {
516                assert_eq!(inputs.len(), 2, "F32Mul requires 2 inputs");
517                // f32 multiplication (symbolic for verification)
518                BV::new_const("f32_mul_result", 32)
519            }
520
521            WasmOp::F32Div => {
522                assert_eq!(inputs.len(), 2, "F32Div requires 2 inputs");
523                // f32 division (symbolic for verification)
524                BV::new_const("f32_div_result", 32)
525            }
526
527            WasmOp::F32Abs => {
528                assert_eq!(inputs.len(), 1, "F32Abs requires 1 input");
529                // f32 absolute value: clear sign bit
530                let val = inputs[0].clone();
531                let mask = BV::from_u64(0x7FFFFFFF, 32);
532                val.bvand(&mask)
533            }
534
535            WasmOp::F32Neg => {
536                assert_eq!(inputs.len(), 1, "F32Neg requires 1 input");
537                // f32 negation: flip sign bit
538                let val = inputs[0].clone();
539                let mask = BV::from_u64(0x80000000, 32);
540                val.bvxor(&mask)
541            }
542
543            WasmOp::F32Sqrt => {
544                assert_eq!(inputs.len(), 1, "F32Sqrt requires 1 input");
545                // f32 square root (symbolic for verification)
546                BV::new_const("f32_sqrt_result", 32)
547            }
548
549            WasmOp::F32Min => {
550                assert_eq!(inputs.len(), 2, "F32Min requires 2 inputs");
551                // f32 minimum with IEEE 754 semantics
552                BV::new_const("f32_min_result", 32)
553            }
554
555            WasmOp::F32Max => {
556                assert_eq!(inputs.len(), 2, "F32Max requires 2 inputs");
557                // f32 maximum with IEEE 754 semantics
558                BV::new_const("f32_max_result", 32)
559            }
560
561            WasmOp::F32Copysign => {
562                assert_eq!(inputs.len(), 2, "F32Copysign requires 2 inputs");
563                // f32 copysign: |input[0]| with sign of input[1]
564                let val_n = inputs[0].clone();
565                let val_m = inputs[1].clone();
566
567                // Extract magnitude from first input
568                let mag_mask = BV::from_u64(0x7FFFFFFF, 32);
569                let magnitude = val_n.bvand(&mag_mask);
570
571                // Extract sign from second input
572                let sign_mask = BV::from_u64(0x80000000, 32);
573                let sign = val_m.bvand(&sign_mask);
574
575                // Combine magnitude and sign
576                magnitude.bvor(&sign)
577            }
578
579            WasmOp::F32Load {
580                offset: _,
581                align: _,
582            } => {
583                assert_eq!(inputs.len(), 1, "F32Load requires 1 input (address)");
584                // f32 load from memory (symbolic)
585                BV::new_const("f32_load_result", 32)
586            }
587
588            // f32 Comparisons (return i32: 0 or 1)
589            WasmOp::F32Eq => {
590                assert_eq!(inputs.len(), 2, "F32Eq requires 2 inputs");
591                // f32 equal: IEEE 754 semantics (NaN != NaN)
592                BV::new_const("f32_eq_result", 32)
593            }
594
595            WasmOp::F32Ne => {
596                assert_eq!(inputs.len(), 2, "F32Ne requires 2 inputs");
597                // f32 not equal
598                BV::new_const("f32_ne_result", 32)
599            }
600
601            WasmOp::F32Lt => {
602                assert_eq!(inputs.len(), 2, "F32Lt requires 2 inputs");
603                // f32 less than
604                BV::new_const("f32_lt_result", 32)
605            }
606
607            WasmOp::F32Le => {
608                assert_eq!(inputs.len(), 2, "F32Le requires 2 inputs");
609                // f32 less than or equal
610                BV::new_const("f32_le_result", 32)
611            }
612
613            WasmOp::F32Gt => {
614                assert_eq!(inputs.len(), 2, "F32Gt requires 2 inputs");
615                // f32 greater than
616                BV::new_const("f32_gt_result", 32)
617            }
618
619            WasmOp::F32Ge => {
620                assert_eq!(inputs.len(), 2, "F32Ge requires 2 inputs");
621                // f32 greater than or equal
622                BV::new_const("f32_ge_result", 32)
623            }
624
625            WasmOp::F32Store {
626                offset: _,
627                align: _,
628            } => {
629                assert_eq!(
630                    inputs.len(),
631                    2,
632                    "F32Store requires 2 inputs (address, value)"
633                );
634                // f32 store to memory - returns void (modeled as zero)
635                // In verification, memory effects are tracked symbolically
636                BV::from_i64(0, 32)
637            }
638
639            // f32 Advanced Math Operations
640            WasmOp::F32Ceil => {
641                assert_eq!(inputs.len(), 1, "F32Ceil requires 1 input");
642                // f32 ceil: round toward +infinity
643                BV::new_const("f32_ceil_result", 32)
644            }
645
646            WasmOp::F32Floor => {
647                assert_eq!(inputs.len(), 1, "F32Floor requires 1 input");
648                // f32 floor: round toward -infinity
649                BV::new_const("f32_floor_result", 32)
650            }
651
652            WasmOp::F32Trunc => {
653                assert_eq!(inputs.len(), 1, "F32Trunc requires 1 input");
654                // f32 trunc: round toward zero
655                BV::new_const("f32_trunc_result", 32)
656            }
657
658            WasmOp::F32Nearest => {
659                assert_eq!(inputs.len(), 1, "F32Nearest requires 1 input");
660                // f32 nearest: round to nearest, ties to even
661                BV::new_const("f32_nearest_result", 32)
662            }
663
664            // f32 Conversions from Integers
665            WasmOp::F32ConvertI32S => {
666                assert_eq!(inputs.len(), 1, "F32ConvertI32S requires 1 input");
667                // Convert signed i32 to f32
668                BV::new_const("f32_convert_i32s_result", 32)
669            }
670
671            WasmOp::F32ConvertI32U => {
672                assert_eq!(inputs.len(), 1, "F32ConvertI32U requires 1 input");
673                // Convert unsigned i32 to f32
674                BV::new_const("f32_convert_i32u_result", 32)
675            }
676
677            WasmOp::F32ConvertI64S => {
678                assert_eq!(inputs.len(), 1, "F32ConvertI64S requires 1 input");
679                // Convert signed i64 to f32
680                BV::new_const("f32_convert_i64s_result", 32)
681            }
682
683            WasmOp::F32ConvertI64U => {
684                assert_eq!(inputs.len(), 1, "F32ConvertI64U requires 1 input");
685                // Convert unsigned i64 to f32
686                BV::new_const("f32_convert_i64u_result", 32)
687            }
688
689            // f32 Type Conversions
690            WasmOp::F32DemoteF64 => {
691                assert_eq!(inputs.len(), 1, "F32DemoteF64 requires 1 input");
692                // Convert f64 to f32 (lose precision)
693                BV::new_const("f32_demote_f64_result", 32)
694            }
695
696            // f32 Reinterpretations
697            WasmOp::F32ReinterpretI32 => {
698                assert_eq!(inputs.len(), 1, "F32ReinterpretI32 requires 1 input");
699                // Reinterpret i32 bits as f32 (bitcast)
700                inputs[0].clone()
701            }
702
703            WasmOp::I32ReinterpretF32 => {
704                assert_eq!(inputs.len(), 1, "I32ReinterpretF32 requires 1 input");
705                // Reinterpret f32 bits as i32 (bitcast)
706                inputs[0].clone()
707            }
708
709            // ===================================================================
710            // f64 Operations (Phase 2c - Double-Precision Floating Point)
711            // ===================================================================
712            WasmOp::F64Const(value) => {
713                // f64 constant value (64-bit)
714                // For verification, we model as 64-bit bitvector
715                let bits = value.to_bits() as i64;
716                BV::from_i64(bits, 64)
717            }
718
719            WasmOp::F64Add => {
720                assert_eq!(inputs.len(), 2, "F64Add requires 2 inputs");
721                // f64 addition (symbolic for verification)
722                BV::new_const("f64_add_result", 64)
723            }
724
725            WasmOp::F64Sub => {
726                assert_eq!(inputs.len(), 2, "F64Sub requires 2 inputs");
727                // f64 subtraction (symbolic for verification)
728                BV::new_const("f64_sub_result", 64)
729            }
730
731            WasmOp::F64Mul => {
732                assert_eq!(inputs.len(), 2, "F64Mul requires 2 inputs");
733                // f64 multiplication (symbolic for verification)
734                BV::new_const("f64_mul_result", 64)
735            }
736
737            WasmOp::F64Div => {
738                assert_eq!(inputs.len(), 2, "F64Div requires 2 inputs");
739                // f64 division (symbolic for verification)
740                BV::new_const("f64_div_result", 64)
741            }
742
743            WasmOp::F64Abs => {
744                assert_eq!(inputs.len(), 1, "F64Abs requires 1 input");
745                // f64 absolute value: clear sign bit
746                let val = inputs[0].clone();
747                let sign_mask = BV::from_u64(0x7FFF_FFFF_FFFF_FFFF, 64);
748                val.bvand(&sign_mask)
749            }
750
751            WasmOp::F64Neg => {
752                assert_eq!(inputs.len(), 1, "F64Neg requires 1 input");
753                // f64 negation: flip sign bit
754                let val = inputs[0].clone();
755                let sign_bit = BV::from_u64(0x8000_0000_0000_0000, 64);
756                val.bvxor(&sign_bit)
757            }
758
759            WasmOp::F64Sqrt => {
760                assert_eq!(inputs.len(), 1, "F64Sqrt requires 1 input");
761                // f64 square root (symbolic for verification)
762                BV::new_const("f64_sqrt_result", 64)
763            }
764
765            WasmOp::F64Min => {
766                assert_eq!(inputs.len(), 2, "F64Min requires 2 inputs");
767                // f64 minimum with IEEE 754 semantics
768                BV::new_const("f64_min_result", 64)
769            }
770
771            WasmOp::F64Max => {
772                assert_eq!(inputs.len(), 2, "F64Max requires 2 inputs");
773                // f64 maximum with IEEE 754 semantics
774                BV::new_const("f64_max_result", 64)
775            }
776
777            WasmOp::F64Copysign => {
778                assert_eq!(inputs.len(), 2, "F64Copysign requires 2 inputs");
779                // f64 copysign: |input[0]| with sign of input[1]
780                let val_n = inputs[0].clone();
781                let val_m = inputs[1].clone();
782
783                // Clear sign bit from input[0]
784                let magnitude_mask = BV::from_u64(0x7FFF_FFFF_FFFF_FFFF, 64);
785                let magnitude = val_n.bvand(&magnitude_mask);
786
787                // Extract sign bit from input[1]
788                let sign_mask = BV::from_u64(0x8000_0000_0000_0000, 64);
789                let sign = val_m.bvand(&sign_mask);
790
791                // Combine magnitude with sign
792                magnitude.bvor(&sign)
793            }
794
795            WasmOp::F64Load {
796                offset: _,
797                align: _,
798            } => {
799                // f64 load from memory (symbolic for verification)
800                assert_eq!(inputs.len(), 1, "F64Load requires 1 input (address)");
801                BV::new_const("f64_load_result", 64)
802            }
803
804            WasmOp::F64Eq => {
805                assert_eq!(inputs.len(), 2, "F64Eq requires 2 inputs");
806                // f64 equal: IEEE 754 semantics (NaN != NaN)
807                BV::new_const("f64_eq_result", 32)
808            }
809
810            WasmOp::F64Ne => {
811                assert_eq!(inputs.len(), 2, "F64Ne requires 2 inputs");
812                // f64 not equal
813                BV::new_const("f64_ne_result", 32)
814            }
815
816            WasmOp::F64Lt => {
817                assert_eq!(inputs.len(), 2, "F64Lt requires 2 inputs");
818                // f64 less than
819                BV::new_const("f64_lt_result", 32)
820            }
821
822            WasmOp::F64Le => {
823                assert_eq!(inputs.len(), 2, "F64Le requires 2 inputs");
824                // f64 less than or equal
825                BV::new_const("f64_le_result", 32)
826            }
827
828            WasmOp::F64Gt => {
829                assert_eq!(inputs.len(), 2, "F64Gt requires 2 inputs");
830                // f64 greater than
831                BV::new_const("f64_gt_result", 32)
832            }
833
834            WasmOp::F64Ge => {
835                assert_eq!(inputs.len(), 2, "F64Ge requires 2 inputs");
836                // f64 greater than or equal
837                BV::new_const("f64_ge_result", 32)
838            }
839
840            WasmOp::F64Store {
841                offset: _,
842                align: _,
843            } => {
844                // f64 store to memory (symbolic for verification)
845                assert_eq!(
846                    inputs.len(),
847                    2,
848                    "F64Store requires 2 inputs (value, address)"
849                );
850                // Store operations don't produce a value
851                BV::from_i64(0, 32)
852            }
853
854            WasmOp::F64Ceil => {
855                assert_eq!(inputs.len(), 1, "F64Ceil requires 1 input");
856                // f64 ceil: round toward +infinity
857                BV::new_const("f64_ceil_result", 64)
858            }
859
860            WasmOp::F64Floor => {
861                assert_eq!(inputs.len(), 1, "F64Floor requires 1 input");
862                // f64 floor: round toward -infinity
863                BV::new_const("f64_floor_result", 64)
864            }
865
866            WasmOp::F64Trunc => {
867                assert_eq!(inputs.len(), 1, "F64Trunc requires 1 input");
868                // f64 trunc: round toward zero
869                BV::new_const("f64_trunc_result", 64)
870            }
871
872            WasmOp::F64Nearest => {
873                assert_eq!(inputs.len(), 1, "F64Nearest requires 1 input");
874                // f64 nearest: round to nearest, ties to even
875                BV::new_const("f64_nearest_result", 64)
876            }
877
878            // f64 Conversions
879            WasmOp::F64ConvertI32S => {
880                assert_eq!(inputs.len(), 1, "F64ConvertI32S requires 1 input");
881                // Convert signed i32 to f64
882                BV::new_const("f64_convert_i32s_result", 64)
883            }
884
885            WasmOp::F64ConvertI32U => {
886                assert_eq!(inputs.len(), 1, "F64ConvertI32U requires 1 input");
887                // Convert unsigned i32 to f64
888                BV::new_const("f64_convert_i32u_result", 64)
889            }
890
891            WasmOp::F64ConvertI64S => {
892                assert_eq!(inputs.len(), 1, "F64ConvertI64S requires 1 input");
893                // Convert signed i64 to f64
894                BV::new_const("f64_convert_i64s_result", 64)
895            }
896
897            WasmOp::F64ConvertI64U => {
898                assert_eq!(inputs.len(), 1, "F64ConvertI64U requires 1 input");
899                // Convert unsigned i64 to f64
900                BV::new_const("f64_convert_i64u_result", 64)
901            }
902
903            WasmOp::F64PromoteF32 => {
904                assert_eq!(inputs.len(), 1, "F64PromoteF32 requires 1 input");
905                // Convert f32 to f64 (gain precision)
906                // For now, symbolic - proper implementation would zero-extend
907                BV::new_const("f64_promote_f32_result", 64)
908            }
909
910            WasmOp::F64ReinterpretI64 => {
911                assert_eq!(inputs.len(), 1, "F64ReinterpretI64 requires 1 input");
912                // Reinterpret i64 bits as f64 (bitcast)
913                inputs[0].clone()
914            }
915
916            WasmOp::I64ReinterpretF64 => {
917                assert_eq!(inputs.len(), 1, "I64ReinterpretF64 requires 1 input");
918                // Reinterpret f64 bits as i64 (bitcast)
919                inputs[0].clone()
920            }
921
922            WasmOp::I64TruncF64S => {
923                assert_eq!(inputs.len(), 1, "I64TruncF64S requires 1 input");
924                // Truncate f64 to signed i64
925                BV::new_const("i64_trunc_f64s_result", 64)
926            }
927
928            WasmOp::I64TruncF64U => {
929                assert_eq!(inputs.len(), 1, "I64TruncF64U requires 1 input");
930                // Truncate f64 to unsigned i64
931                BV::new_const("i64_trunc_f64u_result", 64)
932            }
933
934            // #869: the f32-source i64-target trapping truncations — modeled
935            // like their f64 twins (uninterpreted 64-bit result; the TRAP
936            // side is carried by `trap::trunc_op` + `trap_trunc`). Without
937            // these arms the wildcard would hand back a 32-BIT symbolic const
938            // for a 64-bit-typed op.
939            WasmOp::I64TruncF32S => {
940                assert_eq!(inputs.len(), 1, "I64TruncF32S requires 1 input");
941                BV::new_const("i64_trunc_f32s_result", 64)
942            }
943
944            WasmOp::I64TruncF32U => {
945                assert_eq!(inputs.len(), 1, "I64TruncF32U requires 1 input");
946                BV::new_const("i64_trunc_f32u_result", 64)
947            }
948
949            WasmOp::I32TruncF64S => {
950                assert_eq!(inputs.len(), 1, "I32TruncF64S requires 1 input");
951                // Truncate f64 to signed i32
952                BV::new_const("i32_trunc_f64s_result", 32)
953            }
954
955            WasmOp::I32TruncF64U => {
956                assert_eq!(inputs.len(), 1, "I32TruncF64U requires 1 input");
957                // Truncate f64 to unsigned i32
958                BV::new_const("i32_trunc_f64u_result", 32)
959            }
960
961            // Not yet supported operations
962            _ => {
963                // For unsupported operations, return a symbolic constant
964                // This allows partial verification of supported operations
965                BV::new_const(format!("unsupported_{:?}", op), 32)
966            }
967        }
968    }
969
970    /// Convert boolean to 32-bit bitvector (0 or 1)
971    fn bool_to_bv32(&self, b: &Bool) -> BV {
972        let zero = BV::from_i64(0, 32);
973        let one = BV::from_i64(1, 32);
974        b.ite(&one, &zero)
975    }
976
977    /// Encode count leading zeros (CLZ)
978    ///
979    /// Implements full binary search algorithm for counting leading zeros.
980    /// This provides precise semantics that can be verified against ARM's CLZ instruction.
981    ///
982    /// Algorithm: Binary search through bit positions
983    /// - Check top 16 bits, then 8, 4, 2, 1
984    /// - O(log n) complexity for n-bit integers
985    fn encode_clz(&self, input: &BV) -> BV {
986        let zero = BV::from_i64(0, 32);
987
988        // Special case: if input is 0, return 32
989        let all_zero = input.eq(&zero);
990        let result_if_zero = BV::from_i64(32, 32);
991
992        // Binary search approach
993        let mut count = BV::from_i64(0, 32);
994        let mut remaining = input.clone();
995
996        // Check top 16 bits
997        let mask_16 = BV::from_u64(0xFFFF0000, 32);
998        let top_16 = remaining.bvand(&mask_16);
999        let top_16_zero = top_16.eq(&zero);
1000
1001        // If top 16 are zero, add 16 to count and shift focus to bottom 16
1002        count = top_16_zero.ite(count.bvadd(BV::from_i64(16, 32)), &count);
1003        remaining = top_16_zero.ite(remaining.bvshl(BV::from_i64(16, 32)), &remaining);
1004
1005        // Check top 8 bits (of the 16 we're examining)
1006        let mask_8 = BV::from_u64(0xFF000000, 32);
1007        let top_8 = remaining.bvand(&mask_8);
1008        let top_8_zero = top_8.eq(&zero);
1009
1010        count = top_8_zero.ite(count.bvadd(BV::from_i64(8, 32)), &count);
1011        remaining = top_8_zero.ite(remaining.bvshl(BV::from_i64(8, 32)), &remaining);
1012
1013        // Check top 4 bits
1014        let mask_4 = BV::from_u64(0xF0000000, 32);
1015        let top_4 = remaining.bvand(&mask_4);
1016        let top_4_zero = top_4.eq(&zero);
1017
1018        count = top_4_zero.ite(count.bvadd(BV::from_i64(4, 32)), &count);
1019        remaining = top_4_zero.ite(remaining.bvshl(BV::from_i64(4, 32)), &remaining);
1020
1021        // Check top 2 bits
1022        let mask_2 = BV::from_u64(0xC0000000, 32);
1023        let top_2 = remaining.bvand(&mask_2);
1024        let top_2_zero = top_2.eq(&zero);
1025
1026        count = top_2_zero.ite(count.bvadd(BV::from_i64(2, 32)), &count);
1027        remaining = top_2_zero.ite(remaining.bvshl(BV::from_i64(2, 32)), &remaining);
1028
1029        // Check top bit
1030        let mask_1 = BV::from_u64(0x80000000, 32);
1031        let top_1 = remaining.bvand(&mask_1);
1032        let top_1_zero = top_1.eq(&zero);
1033
1034        count = top_1_zero.ite(count.bvadd(BV::from_i64(1, 32)), &count);
1035
1036        // Return 32 if all zeros, otherwise return count
1037        all_zero.ite(&result_if_zero, &count)
1038    }
1039
1040    /// Encode count trailing zeros (CTZ)
1041    ///
1042    /// Implements binary search from the low end.
1043    /// CTZ counts zeros from the least significant bit up.
1044    fn encode_ctz(&self, input: &BV) -> BV {
1045        let zero = BV::from_i64(0, 32);
1046
1047        // Special case: if input is 0, return 32
1048        let all_zero = input.eq(&zero);
1049        let result_if_zero = BV::from_i64(32, 32);
1050
1051        // Binary search approach from low end
1052        let mut count = BV::from_i64(0, 32);
1053        let mut remaining = input.clone();
1054
1055        // Check bottom 16 bits
1056        let mask_16 = BV::from_u64(0x0000FFFF, 32);
1057        let bottom_16 = remaining.bvand(&mask_16);
1058        let bottom_16_zero = bottom_16.eq(&zero);
1059
1060        count = bottom_16_zero.ite(count.bvadd(BV::from_i64(16, 32)), &count);
1061        remaining = bottom_16_zero.ite(remaining.bvlshr(BV::from_i64(16, 32)), &remaining);
1062
1063        // Check bottom 8 bits
1064        let mask_8 = BV::from_u64(0x000000FF, 32);
1065        let bottom_8 = remaining.bvand(&mask_8);
1066        let bottom_8_zero = bottom_8.eq(&zero);
1067
1068        count = bottom_8_zero.ite(count.bvadd(BV::from_i64(8, 32)), &count);
1069        remaining = bottom_8_zero.ite(remaining.bvlshr(BV::from_i64(8, 32)), &remaining);
1070
1071        // Check bottom 4 bits
1072        let mask_4 = BV::from_u64(0x0000000F, 32);
1073        let bottom_4 = remaining.bvand(&mask_4);
1074        let bottom_4_zero = bottom_4.eq(&zero);
1075
1076        count = bottom_4_zero.ite(count.bvadd(BV::from_i64(4, 32)), &count);
1077        remaining = bottom_4_zero.ite(remaining.bvlshr(BV::from_i64(4, 32)), &remaining);
1078
1079        // Check bottom 2 bits
1080        let mask_2 = BV::from_u64(0x00000003, 32);
1081        let bottom_2 = remaining.bvand(&mask_2);
1082        let bottom_2_zero = bottom_2.eq(&zero);
1083
1084        count = bottom_2_zero.ite(count.bvadd(BV::from_i64(2, 32)), &count);
1085        remaining = bottom_2_zero.ite(remaining.bvlshr(BV::from_i64(2, 32)), &remaining);
1086
1087        // Check bottom bit
1088        let mask_1 = BV::from_u64(0x00000001, 32);
1089        let bottom_1 = remaining.bvand(&mask_1);
1090        let bottom_1_zero = bottom_1.eq(&zero);
1091
1092        count = bottom_1_zero.ite(count.bvadd(BV::from_i64(1, 32)), &count);
1093
1094        // Return 32 if all zeros, otherwise return count
1095        all_zero.ite(&result_if_zero, &count)
1096    }
1097
1098    /// Encode population count (count number of 1 bits)
1099    ///
1100    /// Uses the Hamming weight algorithm (parallel bit counting).
1101    /// This is efficient for SMT solving compared to bit-by-bit iteration.
1102    ///
1103    /// Algorithm:
1104    /// 1. Count bits in pairs: each 2-bit group contains count of its 1 bits
1105    /// 2. Count pairs in nibbles: each 4-bit group contains count
1106    /// 3. Count nibbles in bytes: each 8-bit group contains count
1107    /// 4. Sum all bytes to get final count
1108    fn encode_popcnt(&self, input: &BV) -> BV {
1109        let mut x = input.clone();
1110
1111        // Step 1: Count bits in pairs
1112        // x = (x & 0x55555555) + ((x >> 1) & 0x55555555)
1113        // Pattern: 01010101... (alternating bits)
1114        let mask1 = BV::from_u64(0x55555555, 32);
1115        let masked = x.bvand(&mask1);
1116        let shifted = x.bvlshr(BV::from_i64(1, 32));
1117        let shifted_masked = shifted.bvand(&mask1);
1118        x = masked.bvadd(&shifted_masked);
1119
1120        // Step 2: Count pairs in nibbles
1121        // x = (x & 0x33333333) + ((x >> 2) & 0x33333333)
1122        // Pattern: 00110011... (pairs of bits)
1123        let mask2 = BV::from_u64(0x33333333, 32);
1124        let masked = x.bvand(&mask2);
1125        let shifted = x.bvlshr(BV::from_i64(2, 32));
1126        let shifted_masked = shifted.bvand(&mask2);
1127        x = masked.bvadd(&shifted_masked);
1128
1129        // Step 3: Count nibbles in bytes
1130        // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F)
1131        // Pattern: 00001111... (nibbles)
1132        let mask3 = BV::from_u64(0x0F0F0F0F, 32);
1133        let masked = x.bvand(&mask3);
1134        let shifted = x.bvlshr(BV::from_i64(4, 32));
1135        let shifted_masked = shifted.bvand(&mask3);
1136        x = masked.bvadd(&shifted_masked);
1137
1138        // Step 4: Sum all bytes
1139        // x = (x * 0x01010101) >> 24
1140        // Multiply effectively sums all bytes, then we extract top byte
1141        let multiplier = BV::from_u64(0x01010101, 32);
1142        x = x.bvmul(&multiplier);
1143        x = x.bvlshr(BV::from_i64(24, 32));
1144
1145        x
1146    }
1147}
1148
1149#[cfg(test)]
1150mod tests {
1151    use super::*;
1152    use crate::with_verification_context;
1153
1154    #[test]
1155    fn test_wasm_add_encoding() {
1156        with_verification_context(|| {
1157            let encoder = WasmSemantics::new();
1158            let a = BV::new_const("a", 32);
1159            let b = BV::new_const("b", 32);
1160            let result = encoder.encode_op(&WasmOp::I32Add, &[a, b]);
1161            assert!(result.to_string().contains("bvadd"));
1162        });
1163    }
1164
1165    #[test]
1166    fn test_wasm_sub_encoding() {
1167        with_verification_context(|| {
1168            let encoder = WasmSemantics::new();
1169            let a = BV::new_const("a", 32);
1170            let b = BV::new_const("b", 32);
1171            let result = encoder.encode_op(&WasmOp::I32Sub, &[a, b]);
1172            assert!(result.to_string().contains("bvsub"));
1173        });
1174    }
1175
1176    #[test]
1177    fn test_wasm_const_encoding() {
1178        with_verification_context(|| {
1179            let encoder = WasmSemantics::new();
1180            let result = encoder.encode_op(&WasmOp::I32Const(42), &[]);
1181            assert_eq!(result.simplify().as_i64(), Some(42));
1182        });
1183    }
1184
1185    #[test]
1186    fn test_wasm_comparison() {
1187        with_verification_context(|| {
1188            let encoder = WasmSemantics::new();
1189            let a = BV::from_i64(5, 32);
1190            let b = BV::from_i64(10, 32);
1191            let result = encoder.encode_op(&WasmOp::I32LtS, &[a, b]);
1192            assert_eq!(result.simplify().as_i64(), Some(1));
1193        });
1194    }
1195
1196    #[test]
1197    fn test_wasm_bitwise_ops() {
1198        with_verification_context(|| {
1199            let encoder = WasmSemantics::new();
1200            let a = BV::from_i64(0b1010, 32);
1201            let b = BV::from_i64(0b1100, 32);
1202
1203            let and_result = encoder.encode_op(&WasmOp::I32And, &[a.clone(), b.clone()]);
1204            assert_eq!(and_result.simplify().as_i64(), Some(0b1000));
1205
1206            let or_result = encoder.encode_op(&WasmOp::I32Or, &[a.clone(), b.clone()]);
1207            assert_eq!(or_result.simplify().as_i64(), Some(0b1110));
1208
1209            let xor_result = encoder.encode_op(&WasmOp::I32Xor, &[a, b]);
1210            assert_eq!(xor_result.simplify().as_i64(), Some(0b0110));
1211        });
1212    }
1213
1214    #[test]
1215    fn test_wasm_shift_ops() {
1216        with_verification_context(|| {
1217            let encoder = WasmSemantics::new();
1218            let value = BV::from_i64(8, 32);
1219            let shift = BV::from_i64(2, 32);
1220
1221            let shl_result = encoder.encode_op(&WasmOp::I32Shl, &[value.clone(), shift.clone()]);
1222            assert_eq!(shl_result.simplify().as_i64(), Some(32));
1223
1224            let shr_result = encoder.encode_op(&WasmOp::I32ShrU, &[value, shift]);
1225            assert_eq!(shr_result.simplify().as_i64(), Some(2));
1226        });
1227    }
1228
1229    #[test]
1230    fn test_wasm_shift_modulo() {
1231        with_verification_context(|| {
1232            let encoder = WasmSemantics::new();
1233            let value = BV::from_i64(0xFF, 32);
1234            let shift = BV::from_i64(33, 32);
1235            let shl_result = encoder.encode_op(&WasmOp::I32Shl, &[value.clone(), shift.clone()]);
1236            assert_eq!(shl_result.simplify().as_i64(), Some(0x1FE));
1237        });
1238    }
1239
1240    #[test]
1241    fn test_wasm_rem_ops() {
1242        with_verification_context(|| {
1243            let encoder = WasmSemantics::new();
1244            let a = BV::from_i64(17, 32);
1245            let b = BV::from_i64(5, 32);
1246
1247            let rem_s = encoder.encode_op(&WasmOp::I32RemS, &[a.clone(), b.clone()]);
1248            assert_eq!(rem_s.simplify().as_i64(), Some(2));
1249
1250            let rem_u = encoder.encode_op(&WasmOp::I32RemU, &[a, b]);
1251            assert_eq!(rem_u.simplify().as_i64(), Some(2));
1252        });
1253    }
1254
1255    #[test]
1256    fn test_wasm_rotation_ops() {
1257        with_verification_context(|| {
1258            let encoder = WasmSemantics::new();
1259            let value = BV::from_i64(0x12345678, 32);
1260            let rotate = BV::from_i64(8, 32);
1261
1262            let rotr_result = encoder.encode_op(&WasmOp::I32Rotr, &[value.clone(), rotate.clone()]);
1263            assert_eq!(rotr_result.simplify().as_i64(), Some(0x78123456));
1264
1265            let rotl_result = encoder.encode_op(&WasmOp::I32Rotl, &[value, rotate]);
1266            assert_eq!(rotl_result.simplify().as_i64(), Some(0x34567812));
1267        });
1268    }
1269
1270    #[test]
1271    fn test_wasm_clz_comprehensive() {
1272        with_verification_context(|| {
1273            let encoder = WasmSemantics::new();
1274
1275            let zero = BV::from_i64(0, 32);
1276            assert_eq!(
1277                encoder
1278                    .encode_op(&WasmOp::I32Clz, &[zero])
1279                    .simplify()
1280                    .as_i64(),
1281                Some(32)
1282            );
1283
1284            let one = BV::from_i64(1, 32);
1285            assert_eq!(
1286                encoder
1287                    .encode_op(&WasmOp::I32Clz, &[one])
1288                    .simplify()
1289                    .as_i64(),
1290                Some(31)
1291            );
1292
1293            let msb_set = BV::from_u64(0x80000000, 32);
1294            assert_eq!(
1295                encoder
1296                    .encode_op(&WasmOp::I32Clz, &[msb_set])
1297                    .simplify()
1298                    .as_i64(),
1299                Some(0)
1300            );
1301
1302            let val1 = BV::from_u64(0x00FF0000, 32);
1303            assert_eq!(
1304                encoder
1305                    .encode_op(&WasmOp::I32Clz, &[val1])
1306                    .simplify()
1307                    .as_i64(),
1308                Some(8)
1309            );
1310
1311            let val2 = BV::from_u64(0x00001000, 32);
1312            assert_eq!(
1313                encoder
1314                    .encode_op(&WasmOp::I32Clz, &[val2])
1315                    .simplify()
1316                    .as_i64(),
1317                Some(19)
1318            );
1319
1320            let all_ones = BV::from_u64(0xFFFFFFFF, 32);
1321            assert_eq!(
1322                encoder
1323                    .encode_op(&WasmOp::I32Clz, &[all_ones])
1324                    .simplify()
1325                    .as_i64(),
1326                Some(0)
1327            );
1328
1329            let val3 = BV::from_u64(0x00000100, 32);
1330            assert_eq!(
1331                encoder
1332                    .encode_op(&WasmOp::I32Clz, &[val3])
1333                    .simplify()
1334                    .as_i64(),
1335                Some(23)
1336            );
1337        });
1338    }
1339
1340    #[test]
1341    fn test_wasm_ctz_comprehensive() {
1342        with_verification_context(|| {
1343            let encoder = WasmSemantics::new();
1344
1345            assert_eq!(
1346                encoder
1347                    .encode_op(&WasmOp::I32Ctz, &[BV::from_i64(0, 32)])
1348                    .simplify()
1349                    .as_i64(),
1350                Some(32)
1351            );
1352            assert_eq!(
1353                encoder
1354                    .encode_op(&WasmOp::I32Ctz, &[BV::from_i64(1, 32)])
1355                    .simplify()
1356                    .as_i64(),
1357                Some(0)
1358            );
1359            assert_eq!(
1360                encoder
1361                    .encode_op(&WasmOp::I32Ctz, &[BV::from_i64(2, 32)])
1362                    .simplify()
1363                    .as_i64(),
1364                Some(1)
1365            );
1366            assert_eq!(
1367                encoder
1368                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0x80000000, 32)])
1369                    .simplify()
1370                    .as_i64(),
1371                Some(31)
1372            );
1373            assert_eq!(
1374                encoder
1375                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0x00FF0000, 32)])
1376                    .simplify()
1377                    .as_i64(),
1378                Some(16)
1379            );
1380            assert_eq!(
1381                encoder
1382                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0x00001000, 32)])
1383                    .simplify()
1384                    .as_i64(),
1385                Some(12)
1386            );
1387            assert_eq!(
1388                encoder
1389                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0xFFFFFFFF, 32)])
1390                    .simplify()
1391                    .as_i64(),
1392                Some(0)
1393            );
1394            assert_eq!(
1395                encoder
1396                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0x00000100, 32)])
1397                    .simplify()
1398                    .as_i64(),
1399                Some(8)
1400            );
1401            assert_eq!(
1402                encoder
1403                    .encode_op(&WasmOp::I32Ctz, &[BV::from_i64(12, 32)])
1404                    .simplify()
1405                    .as_i64(),
1406                Some(2)
1407            );
1408        });
1409    }
1410
1411    #[test]
1412    fn test_wasm_popcnt() {
1413        with_verification_context(|| {
1414            let encoder = WasmSemantics::new();
1415
1416            assert_eq!(
1417                encoder
1418                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_i64(0, 32)])
1419                    .simplify()
1420                    .as_i64(),
1421                Some(0)
1422            );
1423            assert_eq!(
1424                encoder
1425                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_i64(1, 32)])
1426                    .simplify()
1427                    .as_i64(),
1428                Some(1)
1429            );
1430            assert_eq!(
1431                encoder
1432                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_u64(0xFFFFFFFF, 32)])
1433                    .simplify()
1434                    .as_i64(),
1435                Some(32)
1436            );
1437            assert_eq!(
1438                encoder
1439                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_u64(0x0F0F0F0F, 32)])
1440                    .simplify()
1441                    .as_i64(),
1442                Some(16)
1443            );
1444            assert_eq!(
1445                encoder
1446                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_i64(7, 32)])
1447                    .simplify()
1448                    .as_i64(),
1449                Some(3)
1450            );
1451            assert_eq!(
1452                encoder
1453                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_u64(0xAAAAAAAA, 32)])
1454                    .simplify()
1455                    .as_i64(),
1456                Some(16)
1457            );
1458        });
1459    }
1460
1461    #[test]
1462    fn test_wasm_select() {
1463        with_verification_context(|| {
1464            let encoder = WasmSemantics::new();
1465
1466            let val1 = BV::from_i64(10, 32);
1467            let val2 = BV::from_i64(20, 32);
1468            let cond_true = BV::from_i64(1, 32);
1469            let result =
1470                encoder.encode_op(&WasmOp::Select, &[val1.clone(), val2.clone(), cond_true]);
1471            assert_eq!(result.simplify().as_i64(), Some(10));
1472
1473            let cond_false = BV::from_i64(0, 32);
1474            let result =
1475                encoder.encode_op(&WasmOp::Select, &[val1.clone(), val2.clone(), cond_false]);
1476            assert_eq!(result.simplify().as_i64(), Some(20));
1477
1478            let val3 = BV::from_i64(42, 32);
1479            let val4 = BV::from_i64(99, 32);
1480            let cond_neg = BV::from_i64(-1, 32);
1481            let result = encoder.encode_op(&WasmOp::Select, &[val3, val4, cond_neg]);
1482            assert_eq!(result.simplify().as_i64(), Some(42));
1483        });
1484    }
1485}
synth_verify/wasm_semantics.rs

synth_verify/
wasm_semantics.rs
