diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 0abc2d51..c50c08fe 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -284,13 +284,16 @@ class Instruction: :return: """ push_instruction = global_state.get_current_instruction() - push_value = push_instruction["argument"] + push_value = push_instruction.get("argument", 0) + try: length_of_value = 2 * int(push_instruction["opcode"][4:]) except ValueError: raise VmException("Invalid Push instruction") - if type(push_value) == tuple: + if length_of_value == 0: + global_state.mstate.stack.append(symbol_factory.BitVecVal(0, 256)) + elif type(push_value) == tuple: if type(push_value[0]) == int: new_value = symbol_factory.BitVecVal(push_value[0], 8) else: diff --git a/mythril/support/opcodes.py b/mythril/support/opcodes.py index 99b45283..c927b582 100644 --- a/mythril/support/opcodes.py +++ b/mythril/support/opcodes.py @@ -77,9 +77,9 @@ OPCODES: Dict = { STACK: (4, 0), ADDRESS: 0x3C, }, - "EXTCODEHASH": {GAS: (700, 700), STACK: UN_OPERATOR_TUPLE, ADDRESS: 0x3F}, "RETURNDATASIZE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE, ADDRESS: 0x3D}, "RETURNDATACOPY": {GAS: (3, 3), STACK: (3, 0), ADDRESS: 0x3E}, + "EXTCODEHASH": {GAS: (700, 700), STACK: UN_OPERATOR_TUPLE, ADDRESS: 0x3F}, "BLOCKHASH": {GAS: (20, 20), STACK: UN_OPERATOR_TUPLE, ADDRESS: 0x40}, "COINBASE": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE, ADDRESS: 0x41}, "TIMESTAMP": {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE, ADDRESS: 0x42}, @@ -131,6 +131,7 @@ OPCODES: Dict = { "INVALID": {GAS: (0, 0), STACK: (0, 0), ADDRESS: 0xFE}, } +OPCODES["PUSH0"] = {GAS: (2, 2), STACK: Z_OPERATOR_TUPLE, ADDRESS: 0x5F} for i in range(1, 33): OPCODES[f"PUSH{i}"] = {GAS: (3, 3), STACK: Z_OPERATOR_TUPLE, ADDRESS: 0x5F + i} diff --git a/tests/instructions/push_test.py b/tests/instructions/push_test.py new file mode 100644 index 00000000..13f26648 --- /dev/null +++ b/tests/instructions/push_test.py @@ -0,0 +1,50 @@ +import pytest + +from mythril.disassembler.disassembly import Disassembly +from mythril.laser.ethereum.state.environment import Environment +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.state.account import Account +from mythril.laser.ethereum.state.machine_state import MachineState +from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.state.world_state import WorldState +from mythril.laser.ethereum.instructions import Instruction +from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction +from mythril.laser.smt import symbol_factory, simplify + + +def get_state(input): + world_state = WorldState() + account = world_state.create_account(balance=10, address=101) + account.code = Disassembly(input) + environment = Environment(account, None, None, None, None, None, None) + state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000)) + state.transaction_stack.append( + (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None) + ) + return state + + +BVV = symbol_factory.BitVecVal +BV = symbol_factory.BitVecSym + +test_data = [ + ("5F", 0), # Successful execution, stack consists of a single item, set to zero + ( + "5F" * 1024, + 0, + ), # Successful execution, stack consists of 1024 items, all set to zero +] + + +@pytest.mark.parametrize("inputs,output", test_data) +def test_push0(inputs, output): + # Arrange + state = get_state(inputs) + + instruction = Instruction("push", dynamic_loader=None) + + # Act + new_state = instruction.evaluate(state)[0] + + # Assert + assert simplify(new_state.mstate.stack[-1]) == output