From 9dc1007a152eac16b3216298b4bd3f9a6ec68974 Mon Sep 17 00:00:00 2001
From: e-ngo <eric.ngo@consensys.net>
Date: Wed, 7 Aug 2019 13:26:24 -0700
Subject: [PATCH] Implemented extcodehash

---
 mythril/laser/ethereum/instructions.py | 26 ++++++++++++----
 tests/instructions/extcodehash_test.py | 43 ++++++++++++++++++++++++++
 2 files changed, 63 insertions(+), 6 deletions(-)
 create mode 100644 tests/instructions/extcodehash_test.py

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 16cb4d38..531aaf03 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -46,6 +46,8 @@ from mythril.laser.ethereum.transaction import (
     ContractCreationTransaction,
 )
 
+from mythril.support.support_utils import get_code_hash
+
 from mythril.support.loader import DynLoader
 
 log = logging.getLogger(__name__)
@@ -1155,18 +1157,30 @@ class Instruction:
             global_state=global_state,
         )
 
-    @StateTransition
+    @StateTransition()
     def extcodehash_(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
         :param global_state:
         :return: List of global states possible, list of size 1 in this case
         """
-        # TODO: To be implemented
-        address = global_state.mstate.stack.pop()
-        global_state.mstate.stack.append(
-            global_state.new_bitvec("extcodehash_{}".format(str(address)), 256)
-        )
+        world_state = global_state.world_state
+        stack = global_state.mstate.stack
+        address = stack.pop()
+        if address.symbolic:
+            log.debug("unsupported symbolic address for EXTCODEHASH")
+            stack.append(global_state.new_bitvec("extcodehash_" + str(address), 256))
+            return [global_state]
+        address = address.value
+            
+        mask = int((symbol_factory.BitVecVal(TT256M1, 256) >> 96).value)
+        address = address & mask
+        if address not in world_state.accounts:
+            code_hash = symbol_factory.BitVecVal(0, 256)
+        else:
+            code = world_state.accounts_exist_or_load(hex(address), self.dynamic_loader)
+            code_hash = get_code_hash(code)
+        stack.append(code_hash)
         return [global_state]
 
     @StateTransition()
diff --git a/tests/instructions/extcodehash_test.py b/tests/instructions/extcodehash_test.py
new file mode 100644
index 00000000..e4586285
--- /dev/null
+++ b/tests/instructions/extcodehash_test.py
@@ -0,0 +1,43 @@
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.ethereum.state.environment import Environment
+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.support.support_utils import get_code_hash
+
+from mythril.laser.smt import symbol_factory
+
+def test_extcodehash_concrete():
+    # Arrange
+    world_state = WorldState()
+    account = world_state.create_account(balance=10, address=101)
+    account.code = Disassembly("60606040")
+    world_state.create_account(balance = 10, address = 1000)
+    environment = Environment(account, None, None, None, None, None)
+    og_state = GlobalState(
+        world_state, environment, None, MachineState(gas_limit=8000000)
+    )
+    og_state.transaction_stack.append(
+        (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
+    )
+    
+    instruction = Instruction("extcodehash", dynamic_loader=None)
+    
+    # If account does not exist, return 0
+    og_state.mstate.stack = [symbol_factory.BitVecVal(1, 256)]
+    new_state = instruction.evaluate(og_state)[0]
+    assert new_state.mstate.stack[-1] == 0
+
+    # If account code does not exist, return hash of empty set.
+    og_state.mstate.stack = [symbol_factory.BitVecVal(1000, 256)]
+    new_state = instruction.evaluate(og_state)[0]
+    assert new_state.mstate.stack[-1] == '0xc5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a470'
+
+    # If account code exists, return hash of the code.
+    og_state.mstate.stack = [symbol_factory.BitVecVal(101, 256)]
+    new_state = instruction.evaluate(og_state)[0]
+    assert new_state.mstate.stack[-1] == get_code_hash("60606040")
\ No newline at end of file