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            WasmOp::I32TruncF64S => {
935                assert_eq!(inputs.len(), 1, "I32TruncF64S requires 1 input");
936                // Truncate f64 to signed i32
937                BV::new_const("i32_trunc_f64s_result", 32)
938            }
939
940            WasmOp::I32TruncF64U => {
941                assert_eq!(inputs.len(), 1, "I32TruncF64U requires 1 input");
942                // Truncate f64 to unsigned i32
943                BV::new_const("i32_trunc_f64u_result", 32)
944            }
945
946            // Not yet supported operations
947            _ => {
948                // For unsupported operations, return a symbolic constant
949                // This allows partial verification of supported operations
950                BV::new_const(format!("unsupported_{:?}", op), 32)
951            }
952        }
953    }
954
955    /// Convert boolean to 32-bit bitvector (0 or 1)
956    fn bool_to_bv32(&self, b: &Bool) -> BV {
957        let zero = BV::from_i64(0, 32);
958        let one = BV::from_i64(1, 32);
959        b.ite(&one, &zero)
960    }
961
962    /// Encode count leading zeros (CLZ)
963    ///
964    /// Implements full binary search algorithm for counting leading zeros.
965    /// This provides precise semantics that can be verified against ARM's CLZ instruction.
966    ///
967    /// Algorithm: Binary search through bit positions
968    /// - Check top 16 bits, then 8, 4, 2, 1
969    /// - O(log n) complexity for n-bit integers
970    fn encode_clz(&self, input: &BV) -> BV {
971        let zero = BV::from_i64(0, 32);
972
973        // Special case: if input is 0, return 32
974        let all_zero = input.eq(&zero);
975        let result_if_zero = BV::from_i64(32, 32);
976
977        // Binary search approach
978        let mut count = BV::from_i64(0, 32);
979        let mut remaining = input.clone();
980
981        // Check top 16 bits
982        let mask_16 = BV::from_u64(0xFFFF0000, 32);
983        let top_16 = remaining.bvand(&mask_16);
984        let top_16_zero = top_16.eq(&zero);
985
986        // If top 16 are zero, add 16 to count and shift focus to bottom 16
987        count = top_16_zero.ite(count.bvadd(BV::from_i64(16, 32)), &count);
988        remaining = top_16_zero.ite(remaining.bvshl(BV::from_i64(16, 32)), &remaining);
989
990        // Check top 8 bits (of the 16 we're examining)
991        let mask_8 = BV::from_u64(0xFF000000, 32);
992        let top_8 = remaining.bvand(&mask_8);
993        let top_8_zero = top_8.eq(&zero);
994
995        count = top_8_zero.ite(count.bvadd(BV::from_i64(8, 32)), &count);
996        remaining = top_8_zero.ite(remaining.bvshl(BV::from_i64(8, 32)), &remaining);
997
998        // Check top 4 bits
999        let mask_4 = BV::from_u64(0xF0000000, 32);
1000        let top_4 = remaining.bvand(&mask_4);
1001        let top_4_zero = top_4.eq(&zero);
1002
1003        count = top_4_zero.ite(count.bvadd(BV::from_i64(4, 32)), &count);
1004        remaining = top_4_zero.ite(remaining.bvshl(BV::from_i64(4, 32)), &remaining);
1005
1006        // Check top 2 bits
1007        let mask_2 = BV::from_u64(0xC0000000, 32);
1008        let top_2 = remaining.bvand(&mask_2);
1009        let top_2_zero = top_2.eq(&zero);
1010
1011        count = top_2_zero.ite(count.bvadd(BV::from_i64(2, 32)), &count);
1012        remaining = top_2_zero.ite(remaining.bvshl(BV::from_i64(2, 32)), &remaining);
1013
1014        // Check top bit
1015        let mask_1 = BV::from_u64(0x80000000, 32);
1016        let top_1 = remaining.bvand(&mask_1);
1017        let top_1_zero = top_1.eq(&zero);
1018
1019        count = top_1_zero.ite(count.bvadd(BV::from_i64(1, 32)), &count);
1020
1021        // Return 32 if all zeros, otherwise return count
1022        all_zero.ite(&result_if_zero, &count)
1023    }
1024
1025    /// Encode count trailing zeros (CTZ)
1026    ///
1027    /// Implements binary search from the low end.
1028    /// CTZ counts zeros from the least significant bit up.
1029    fn encode_ctz(&self, input: &BV) -> BV {
1030        let zero = BV::from_i64(0, 32);
1031
1032        // Special case: if input is 0, return 32
1033        let all_zero = input.eq(&zero);
1034        let result_if_zero = BV::from_i64(32, 32);
1035
1036        // Binary search approach from low end
1037        let mut count = BV::from_i64(0, 32);
1038        let mut remaining = input.clone();
1039
1040        // Check bottom 16 bits
1041        let mask_16 = BV::from_u64(0x0000FFFF, 32);
1042        let bottom_16 = remaining.bvand(&mask_16);
1043        let bottom_16_zero = bottom_16.eq(&zero);
1044
1045        count = bottom_16_zero.ite(count.bvadd(BV::from_i64(16, 32)), &count);
1046        remaining = bottom_16_zero.ite(remaining.bvlshr(BV::from_i64(16, 32)), &remaining);
1047
1048        // Check bottom 8 bits
1049        let mask_8 = BV::from_u64(0x000000FF, 32);
1050        let bottom_8 = remaining.bvand(&mask_8);
1051        let bottom_8_zero = bottom_8.eq(&zero);
1052
1053        count = bottom_8_zero.ite(count.bvadd(BV::from_i64(8, 32)), &count);
1054        remaining = bottom_8_zero.ite(remaining.bvlshr(BV::from_i64(8, 32)), &remaining);
1055
1056        // Check bottom 4 bits
1057        let mask_4 = BV::from_u64(0x0000000F, 32);
1058        let bottom_4 = remaining.bvand(&mask_4);
1059        let bottom_4_zero = bottom_4.eq(&zero);
1060
1061        count = bottom_4_zero.ite(count.bvadd(BV::from_i64(4, 32)), &count);
1062        remaining = bottom_4_zero.ite(remaining.bvlshr(BV::from_i64(4, 32)), &remaining);
1063
1064        // Check bottom 2 bits
1065        let mask_2 = BV::from_u64(0x00000003, 32);
1066        let bottom_2 = remaining.bvand(&mask_2);
1067        let bottom_2_zero = bottom_2.eq(&zero);
1068
1069        count = bottom_2_zero.ite(count.bvadd(BV::from_i64(2, 32)), &count);
1070        remaining = bottom_2_zero.ite(remaining.bvlshr(BV::from_i64(2, 32)), &remaining);
1071
1072        // Check bottom bit
1073        let mask_1 = BV::from_u64(0x00000001, 32);
1074        let bottom_1 = remaining.bvand(&mask_1);
1075        let bottom_1_zero = bottom_1.eq(&zero);
1076
1077        count = bottom_1_zero.ite(count.bvadd(BV::from_i64(1, 32)), &count);
1078
1079        // Return 32 if all zeros, otherwise return count
1080        all_zero.ite(&result_if_zero, &count)
1081    }
1082
1083    /// Encode population count (count number of 1 bits)
1084    ///
1085    /// Uses the Hamming weight algorithm (parallel bit counting).
1086    /// This is efficient for SMT solving compared to bit-by-bit iteration.
1087    ///
1088    /// Algorithm:
1089    /// 1. Count bits in pairs: each 2-bit group contains count of its 1 bits
1090    /// 2. Count pairs in nibbles: each 4-bit group contains count
1091    /// 3. Count nibbles in bytes: each 8-bit group contains count
1092    /// 4. Sum all bytes to get final count
1093    fn encode_popcnt(&self, input: &BV) -> BV {
1094        let mut x = input.clone();
1095
1096        // Step 1: Count bits in pairs
1097        // x = (x & 0x55555555) + ((x >> 1) & 0x55555555)
1098        // Pattern: 01010101... (alternating bits)
1099        let mask1 = BV::from_u64(0x55555555, 32);
1100        let masked = x.bvand(&mask1);
1101        let shifted = x.bvlshr(BV::from_i64(1, 32));
1102        let shifted_masked = shifted.bvand(&mask1);
1103        x = masked.bvadd(&shifted_masked);
1104
1105        // Step 2: Count pairs in nibbles
1106        // x = (x & 0x33333333) + ((x >> 2) & 0x33333333)
1107        // Pattern: 00110011... (pairs of bits)
1108        let mask2 = BV::from_u64(0x33333333, 32);
1109        let masked = x.bvand(&mask2);
1110        let shifted = x.bvlshr(BV::from_i64(2, 32));
1111        let shifted_masked = shifted.bvand(&mask2);
1112        x = masked.bvadd(&shifted_masked);
1113
1114        // Step 3: Count nibbles in bytes
1115        // x = (x & 0x0F0F0F0F) + ((x >> 4) & 0x0F0F0F0F)
1116        // Pattern: 00001111... (nibbles)
1117        let mask3 = BV::from_u64(0x0F0F0F0F, 32);
1118        let masked = x.bvand(&mask3);
1119        let shifted = x.bvlshr(BV::from_i64(4, 32));
1120        let shifted_masked = shifted.bvand(&mask3);
1121        x = masked.bvadd(&shifted_masked);
1122
1123        // Step 4: Sum all bytes
1124        // x = (x * 0x01010101) >> 24
1125        // Multiply effectively sums all bytes, then we extract top byte
1126        let multiplier = BV::from_u64(0x01010101, 32);
1127        x = x.bvmul(&multiplier);
1128        x = x.bvlshr(BV::from_i64(24, 32));
1129
1130        x
1131    }
1132}
1133
1134#[cfg(test)]
1135mod tests {
1136    use super::*;
1137    use crate::with_verification_context;
1138
1139    #[test]
1140    fn test_wasm_add_encoding() {
1141        with_verification_context(|| {
1142            let encoder = WasmSemantics::new();
1143            let a = BV::new_const("a", 32);
1144            let b = BV::new_const("b", 32);
1145            let result = encoder.encode_op(&WasmOp::I32Add, &[a, b]);
1146            assert!(result.to_string().contains("bvadd"));
1147        });
1148    }
1149
1150    #[test]
1151    fn test_wasm_sub_encoding() {
1152        with_verification_context(|| {
1153            let encoder = WasmSemantics::new();
1154            let a = BV::new_const("a", 32);
1155            let b = BV::new_const("b", 32);
1156            let result = encoder.encode_op(&WasmOp::I32Sub, &[a, b]);
1157            assert!(result.to_string().contains("bvsub"));
1158        });
1159    }
1160
1161    #[test]
1162    fn test_wasm_const_encoding() {
1163        with_verification_context(|| {
1164            let encoder = WasmSemantics::new();
1165            let result = encoder.encode_op(&WasmOp::I32Const(42), &[]);
1166            assert_eq!(result.simplify().as_i64(), Some(42));
1167        });
1168    }
1169
1170    #[test]
1171    fn test_wasm_comparison() {
1172        with_verification_context(|| {
1173            let encoder = WasmSemantics::new();
1174            let a = BV::from_i64(5, 32);
1175            let b = BV::from_i64(10, 32);
1176            let result = encoder.encode_op(&WasmOp::I32LtS, &[a, b]);
1177            assert_eq!(result.simplify().as_i64(), Some(1));
1178        });
1179    }
1180
1181    #[test]
1182    fn test_wasm_bitwise_ops() {
1183        with_verification_context(|| {
1184            let encoder = WasmSemantics::new();
1185            let a = BV::from_i64(0b1010, 32);
1186            let b = BV::from_i64(0b1100, 32);
1187
1188            let and_result = encoder.encode_op(&WasmOp::I32And, &[a.clone(), b.clone()]);
1189            assert_eq!(and_result.simplify().as_i64(), Some(0b1000));
1190
1191            let or_result = encoder.encode_op(&WasmOp::I32Or, &[a.clone(), b.clone()]);
1192            assert_eq!(or_result.simplify().as_i64(), Some(0b1110));
1193
1194            let xor_result = encoder.encode_op(&WasmOp::I32Xor, &[a, b]);
1195            assert_eq!(xor_result.simplify().as_i64(), Some(0b0110));
1196        });
1197    }
1198
1199    #[test]
1200    fn test_wasm_shift_ops() {
1201        with_verification_context(|| {
1202            let encoder = WasmSemantics::new();
1203            let value = BV::from_i64(8, 32);
1204            let shift = BV::from_i64(2, 32);
1205
1206            let shl_result = encoder.encode_op(&WasmOp::I32Shl, &[value.clone(), shift.clone()]);
1207            assert_eq!(shl_result.simplify().as_i64(), Some(32));
1208
1209            let shr_result = encoder.encode_op(&WasmOp::I32ShrU, &[value, shift]);
1210            assert_eq!(shr_result.simplify().as_i64(), Some(2));
1211        });
1212    }
1213
1214    #[test]
1215    fn test_wasm_shift_modulo() {
1216        with_verification_context(|| {
1217            let encoder = WasmSemantics::new();
1218            let value = BV::from_i64(0xFF, 32);
1219            let shift = BV::from_i64(33, 32);
1220            let shl_result = encoder.encode_op(&WasmOp::I32Shl, &[value.clone(), shift.clone()]);
1221            assert_eq!(shl_result.simplify().as_i64(), Some(0x1FE));
1222        });
1223    }
1224
1225    #[test]
1226    fn test_wasm_rem_ops() {
1227        with_verification_context(|| {
1228            let encoder = WasmSemantics::new();
1229            let a = BV::from_i64(17, 32);
1230            let b = BV::from_i64(5, 32);
1231
1232            let rem_s = encoder.encode_op(&WasmOp::I32RemS, &[a.clone(), b.clone()]);
1233            assert_eq!(rem_s.simplify().as_i64(), Some(2));
1234
1235            let rem_u = encoder.encode_op(&WasmOp::I32RemU, &[a, b]);
1236            assert_eq!(rem_u.simplify().as_i64(), Some(2));
1237        });
1238    }
1239
1240    #[test]
1241    fn test_wasm_rotation_ops() {
1242        with_verification_context(|| {
1243            let encoder = WasmSemantics::new();
1244            let value = BV::from_i64(0x12345678, 32);
1245            let rotate = BV::from_i64(8, 32);
1246
1247            let rotr_result = encoder.encode_op(&WasmOp::I32Rotr, &[value.clone(), rotate.clone()]);
1248            assert_eq!(rotr_result.simplify().as_i64(), Some(0x78123456));
1249
1250            let rotl_result = encoder.encode_op(&WasmOp::I32Rotl, &[value, rotate]);
1251            assert_eq!(rotl_result.simplify().as_i64(), Some(0x34567812));
1252        });
1253    }
1254
1255    #[test]
1256    fn test_wasm_clz_comprehensive() {
1257        with_verification_context(|| {
1258            let encoder = WasmSemantics::new();
1259
1260            let zero = BV::from_i64(0, 32);
1261            assert_eq!(
1262                encoder
1263                    .encode_op(&WasmOp::I32Clz, &[zero])
1264                    .simplify()
1265                    .as_i64(),
1266                Some(32)
1267            );
1268
1269            let one = BV::from_i64(1, 32);
1270            assert_eq!(
1271                encoder
1272                    .encode_op(&WasmOp::I32Clz, &[one])
1273                    .simplify()
1274                    .as_i64(),
1275                Some(31)
1276            );
1277
1278            let msb_set = BV::from_u64(0x80000000, 32);
1279            assert_eq!(
1280                encoder
1281                    .encode_op(&WasmOp::I32Clz, &[msb_set])
1282                    .simplify()
1283                    .as_i64(),
1284                Some(0)
1285            );
1286
1287            let val1 = BV::from_u64(0x00FF0000, 32);
1288            assert_eq!(
1289                encoder
1290                    .encode_op(&WasmOp::I32Clz, &[val1])
1291                    .simplify()
1292                    .as_i64(),
1293                Some(8)
1294            );
1295
1296            let val2 = BV::from_u64(0x00001000, 32);
1297            assert_eq!(
1298                encoder
1299                    .encode_op(&WasmOp::I32Clz, &[val2])
1300                    .simplify()
1301                    .as_i64(),
1302                Some(19)
1303            );
1304
1305            let all_ones = BV::from_u64(0xFFFFFFFF, 32);
1306            assert_eq!(
1307                encoder
1308                    .encode_op(&WasmOp::I32Clz, &[all_ones])
1309                    .simplify()
1310                    .as_i64(),
1311                Some(0)
1312            );
1313
1314            let val3 = BV::from_u64(0x00000100, 32);
1315            assert_eq!(
1316                encoder
1317                    .encode_op(&WasmOp::I32Clz, &[val3])
1318                    .simplify()
1319                    .as_i64(),
1320                Some(23)
1321            );
1322        });
1323    }
1324
1325    #[test]
1326    fn test_wasm_ctz_comprehensive() {
1327        with_verification_context(|| {
1328            let encoder = WasmSemantics::new();
1329
1330            assert_eq!(
1331                encoder
1332                    .encode_op(&WasmOp::I32Ctz, &[BV::from_i64(0, 32)])
1333                    .simplify()
1334                    .as_i64(),
1335                Some(32)
1336            );
1337            assert_eq!(
1338                encoder
1339                    .encode_op(&WasmOp::I32Ctz, &[BV::from_i64(1, 32)])
1340                    .simplify()
1341                    .as_i64(),
1342                Some(0)
1343            );
1344            assert_eq!(
1345                encoder
1346                    .encode_op(&WasmOp::I32Ctz, &[BV::from_i64(2, 32)])
1347                    .simplify()
1348                    .as_i64(),
1349                Some(1)
1350            );
1351            assert_eq!(
1352                encoder
1353                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0x80000000, 32)])
1354                    .simplify()
1355                    .as_i64(),
1356                Some(31)
1357            );
1358            assert_eq!(
1359                encoder
1360                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0x00FF0000, 32)])
1361                    .simplify()
1362                    .as_i64(),
1363                Some(16)
1364            );
1365            assert_eq!(
1366                encoder
1367                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0x00001000, 32)])
1368                    .simplify()
1369                    .as_i64(),
1370                Some(12)
1371            );
1372            assert_eq!(
1373                encoder
1374                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0xFFFFFFFF, 32)])
1375                    .simplify()
1376                    .as_i64(),
1377                Some(0)
1378            );
1379            assert_eq!(
1380                encoder
1381                    .encode_op(&WasmOp::I32Ctz, &[BV::from_u64(0x00000100, 32)])
1382                    .simplify()
1383                    .as_i64(),
1384                Some(8)
1385            );
1386            assert_eq!(
1387                encoder
1388                    .encode_op(&WasmOp::I32Ctz, &[BV::from_i64(12, 32)])
1389                    .simplify()
1390                    .as_i64(),
1391                Some(2)
1392            );
1393        });
1394    }
1395
1396    #[test]
1397    fn test_wasm_popcnt() {
1398        with_verification_context(|| {
1399            let encoder = WasmSemantics::new();
1400
1401            assert_eq!(
1402                encoder
1403                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_i64(0, 32)])
1404                    .simplify()
1405                    .as_i64(),
1406                Some(0)
1407            );
1408            assert_eq!(
1409                encoder
1410                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_i64(1, 32)])
1411                    .simplify()
1412                    .as_i64(),
1413                Some(1)
1414            );
1415            assert_eq!(
1416                encoder
1417                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_u64(0xFFFFFFFF, 32)])
1418                    .simplify()
1419                    .as_i64(),
1420                Some(32)
1421            );
1422            assert_eq!(
1423                encoder
1424                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_u64(0x0F0F0F0F, 32)])
1425                    .simplify()
1426                    .as_i64(),
1427                Some(16)
1428            );
1429            assert_eq!(
1430                encoder
1431                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_i64(7, 32)])
1432                    .simplify()
1433                    .as_i64(),
1434                Some(3)
1435            );
1436            assert_eq!(
1437                encoder
1438                    .encode_op(&WasmOp::I32Popcnt, &[BV::from_u64(0xAAAAAAAA, 32)])
1439                    .simplify()
1440                    .as_i64(),
1441                Some(16)
1442            );
1443        });
1444    }
1445
1446    #[test]
1447    fn test_wasm_select() {
1448        with_verification_context(|| {
1449            let encoder = WasmSemantics::new();
1450
1451            let val1 = BV::from_i64(10, 32);
1452            let val2 = BV::from_i64(20, 32);
1453            let cond_true = BV::from_i64(1, 32);
1454            let result =
1455                encoder.encode_op(&WasmOp::Select, &[val1.clone(), val2.clone(), cond_true]);
1456            assert_eq!(result.simplify().as_i64(), Some(10));
1457
1458            let cond_false = BV::from_i64(0, 32);
1459            let result =
1460                encoder.encode_op(&WasmOp::Select, &[val1.clone(), val2.clone(), cond_false]);
1461            assert_eq!(result.simplify().as_i64(), Some(20));
1462
1463            let val3 = BV::from_i64(42, 32);
1464            let val4 = BV::from_i64(99, 32);
1465            let cond_neg = BV::from_i64(-1, 32);
1466            let result = encoder.encode_op(&WasmOp::Select, &[val3, val4, cond_neg]);
1467            assert_eq!(result.simplify().as_i64(), Some(42));
1468        });
1469    }
1470}
synth_verify/wasm_semantics.rs

synth_verify/
wasm_semantics.rs
