From 2855b34a97943f5bb66ec074796bc8262443d00a Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Sun, 25 Jun 2023 19:38:05 +0530
Subject: [PATCH] Add push0 and push tests (#1781)

* Add push0 and push tests

* Fix issue with args

* Add missing files
---
 mythril/laser/ethereum/instructions.py |  7 ++--
 mythril/support/opcodes.py             |  3 +-
 tests/instructions/push_test.py        | 50 ++++++++++++++++++++++++++
 3 files changed, 57 insertions(+), 3 deletions(-)
 create mode 100644 tests/instructions/push_test.py

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