diff --git a/.gitignore b/.gitignore index 7985ddd..cdee14e 100644 --- a/.gitignore +++ b/.gitignore @@ -8,6 +8,7 @@ __pycache__/ venv/ env .env +myenv/ # IDE-specific files .vscode/ diff --git a/seewasm/arch/wasm/instructions/ArithmeticInstructions.py b/seewasm/arch/wasm/instructions/ArithmeticInstructions.py index 6c84f73..66c1f35 100644 --- a/seewasm/arch/wasm/instructions/ArithmeticInstructions.py +++ b/seewasm/arch/wasm/instructions/ArithmeticInstructions.py @@ -7,13 +7,15 @@ UDiv, URem, fpAbs, fpAdd, fpDiv, fpMax, fpMin, fpMul, fpNeg, fpRoundToIntegral, fpSqrt, fpSub, is_bool, simplify) +# Helper map for the bit sizes of different WebAssembly data types helper_map = { - 'i32': 32, - 'i64': 64, - 'f32': [8, 24], - 'f64': [11, 53] + 'i32': 32, # 32-bit integer + 'i64': 64, # 64-bit integer + 'f32': [8, 24], # 32-bit float (8 exponent bits, 24 significand bit) + 'f64': [11, 53] # 64-bit float (11 exponent bits, 53 significand bit) } +# Maps WebAssembly float types to Z3's floating-point representations float_helper_map = { 'f32': Float32, 'f64': Float64 @@ -21,15 +23,32 @@ class ArithmeticInstructions: + """ + This class is responsible for emulating arithmetic instructions for WebAssembly + in a symbolic execution environment. It handles both integer and floating-point + instructions by processing the symbolic stack in the given state. + """ def __init__(self, instr_name, instr_operand, _): + # Initialize with the instruction name, its operands self.instr_name = instr_name self.instr_operand = instr_operand def emulate(self, state): + """ + This method selects the correct arithmetic operation (integer or floating-point) + based on the instruction name and emulates it by manipulating the symbolic stack + in the given state. + """ def do_emulate_arithmetic_int_instruction(state): - instr_type = self.instr_name[:3] + """ + Handles integer arithmetic instructions such as addition, subtraction, multiplication, + division, and reamainder. It pops two operands from the stack, performs the operation, + and pushes the result back onto the stack. + """ + instr_type = self.instr_name[:3] # Extract instruction type (e.g. i32, i64, f32, f64) if '.clz' in self.instr_name or '.ctz' in self.instr_name: + # Specail cases: count leading zero (clz), count trailing zero (ctz) # wasm documentation says: # This instruction is fully defined when all bits are zero; # it returns the number of bits in the operand type. @@ -37,6 +56,7 @@ def do_emulate_arithmetic_int_instruction(state): state.symbolic_stack.append( BitVecVal(helper_map[instr_type], helper_map[instr_type])) elif '.popcnt' in self.instr_name: + # Popcount counts the number of '1' bits; in case of all bits zero, return 0 # wasm documentation says: # This instruction is fully defined when all bits are zero; # it returns 0. @@ -84,24 +104,30 @@ def do_emulate_arithmetic_int_instruction(state): return [state] def do_emulate_arithmetic_float_instruction(state): + """ + Handles floating-point arithmetic instructions such as addition, subtraction, + multiplication, division, square root, etc. It pops the appropriate number of + operands from the stack, applies the operation, and pushes the result back to the stack. + """ # TODO need to be clarified # wasm default rounding rules - rm = RNE() + rm = RNE() # Default rounding mode: Round to Nearest, ties to Even - instr_type = self.instr_name[:3] + instr_type = self.instr_name[:3] # Extract instruction type (e.g., 'f32', 'f64') + # Define instruction sets that require one or two arguments two_arguments_instrs = ['add', 'sub', 'mul', 'div', 'min', 'max', 'copysign'] one_argument_instrs = ['sqrt', 'floor', 'ceil', 'trunc', 'nearest', 'abs', 'neg'] - # add instr_type before each instr + # Add instruction type prefix to each instruction (e.g., 'f32.add', 'f64.mul') two_arguments_instrs = [str(instr_type + '.' + i) for i in two_arguments_instrs] one_argument_instrs = [str(instr_type + '.' + i) for i in one_argument_instrs] - # pop two elements + # Handling instructions that require two operands (e.g., f32.add) if self.instr_name in two_arguments_instrs: arg1, arg2 = state.symbolic_stack.pop(), state.symbolic_stack.pop() @@ -127,12 +153,15 @@ def do_emulate_arithmetic_float_instruction(state): if arg2.isPositive() ^ arg1.isPositive(): result = fpNeg(arg1) # pop one element + # Handling instructions that require one operand (e.g., f32.sqrt) elif self.instr_name in one_argument_instrs: arg1 = state.symbolic_stack.pop() + # Ensure the argument has the correct bit size assert arg1.ebits() == helper_map[instr_type][0] and arg1.sbits( ) == helper_map[instr_type][1], 'In do_emulate_arithmetic_float_instruction, arg1 type mismatch' + # Perform the appropriate floating-point operation if '.sqrt' in self.instr_name: result = fpSqrt(rm, arg1) elif '.floor' in self.instr_name: diff --git a/seewasm/arch/wasm/instructions/BitwiseInstructions.py b/seewasm/arch/wasm/instructions/BitwiseInstructions.py index 7d54e6c..2d45027 100644 --- a/seewasm/arch/wasm/instructions/BitwiseInstructions.py +++ b/seewasm/arch/wasm/instructions/BitwiseInstructions.py @@ -6,23 +6,41 @@ from z3 import (BitVec, BitVecVal, LShR, RotateLeft, RotateRight, is_bool, is_bv, is_false, is_true, simplify) +# Helper map for the bit sizes of different WebAssembly data types helper_map = { - 'i32': 32, - 'i64': 64, + 'i32': 32, # 32-bit integer + 'i64': 64, # 64-bit integer } class BitwiseInstructions: + """ + Class to emulate bitwise operations for WebAssembly instructions using Z3 symbolic execution. + """ def __init__(self, instr_name, instr_operand, _): + """ + Initialize the instruction with its name and operand. + + :param instr_name: The WebAssembly instruction name (e.g., "i32.and") + :param instr_operand: Operand for the instruction (not used in this implementation) + """ self.instr_name = instr_name self.instr_operand = instr_operand # TODO overflow check in this function? def emulate(self, state): + """ + Emulate the bitwise instruction by performing symbolic operations on two arguments + from the symbolic stack, and push the result back onto the stack. + + :param state: The current execution state, including the symbolic stack. + :return: The modified state after emulation. + """ + arg1, arg2 = state.symbolic_stack.pop(), state.symbolic_stack.pop() instr_type = self.instr_name[:3] - # arg1 and arg2 could be BitVecRef, BitVecValRef and BoolRef + # Handle the case where the arguments are BoolRef types (Boolean), converting them to BitVec if is_bool(arg1): arg1 = BitVec(str(arg1), helper_map[instr_type]) logging.warning( @@ -32,30 +50,33 @@ def emulate(self, state): logging.warning( f"[!] In `BitwiseInstructions.py`, arg2 is BoolRef, translated to BitVec which may lead to some information loss") + # Ensure that both arguments match the expected size for the WebAssembly type (i32 or i64) assert arg1.size( ) == helper_map[instr_type], f'arg1 size is {arg1.size()} instead of {helper_map[instr_type]} in do_emulate_bitwise_instruction' assert arg2.size( ) == helper_map[instr_type], f'arg2 size is {arg2.size()} instead of {helper_map[instr_type]} in do_emulate_bitwise_instruction' + # Determine the bitwise operation to perform based on the instruction name if '.and' in self.instr_name: - result = simplify(arg1 & arg2) + result = simplify(arg1 & arg2) # Bitwise AND operation elif '.or' in self.instr_name: - result = simplify(arg1 | arg2) + result = simplify(arg1 | arg2) # Bitwise OR operation elif '.xor' in self.instr_name: - result = simplify(arg1 ^ arg2) + result = simplify(arg1 ^ arg2) # Bitwise XOR operation elif '.shr_s' in self.instr_name: - result = simplify(arg2 >> arg1) + result = simplify(arg2 >> arg1) # Signed right shift (arithmetic shift) elif '.shr_u' in self.instr_name: - result = simplify(LShR(arg2, arg1)) + result = simplify(LShR(arg2, arg1)) # Unsigned right shift (logical shift) elif '.shl' in self.instr_name: - result = simplify(arg2 << arg1) + result = simplify(arg2 << arg1) # Left shift elif '.rotl' in self.instr_name: - result = simplify(RotateLeft(arg2, arg1)) + result = simplify(RotateLeft(arg2, arg1)) # Rotate left elif '.rotr' in self.instr_name: - result = simplify(RotateRight(arg2, arg1)) + result = simplify(RotateRight(arg2, arg1)) # Rotate right else: raise UnsupportInstructionError + # Handle the case where the result is a boolean value if is_bool(result): if is_true(result): result = BitVecVal(1, 32)