Fix hashes (#1389)

Co-authored-by: Nikhil Parasaram <nikhilparasaram@Nikhils-MacBook-Pro.local>

mythril/laser/ethereum/instructions.py

@@ -4,9 +4,8 @@ import binascii
 import logging
 
 from copy import copy, deepcopy
-from typing import cast, Callable, List, Set, Union, Tuple, Any
+from typing import cast, Callable, List, Union
 from datetime import datetime
-from ethereum import utils
 
 from mythril.laser.smt import (
     Extract,
@@ -1003,22 +1002,14 @@ class Instruction:
         """
 
         state = global_state.mstate
-        op0, op1 = state.stack.pop(), state.stack.pop()
+        index, op1 = state.stack.pop(), state.stack.pop()
 
         try:
-            index, length = util.get_concrete_int(op0), util.get_concrete_int(op1)
+            length = util.get_concrete_int(op1)
         except TypeError:
             # Can't access symbolic memory offsets
-            if isinstance(op0, Expression):
-                op0 = simplify(op0)
-            state.stack.append(
-                symbol_factory.BitVecSym("KECCAC_mem[{}]".format(hash(op0)), 256)
-            )
-            gas_tuple = get_opcode_gas("SHA3")
-            state.min_gas_used += gas_tuple[0]
-            state.max_gas_used += gas_tuple[1]
-            return [global_state]
-
+            length = 64
+            global_state.world_state.constraints.append(op1 == length)
         Instruction._sha3_gas_helper(global_state, length)
 
         state.mem_extend(index, length)

mythril/laser/ethereum/keccak_function_manager.py

@@ -12,10 +12,13 @@ from mythril.laser.smt import (
 )
 from typing import Dict, Tuple, List, Optional
 
+import logging
+
 TOTAL_PARTS = 10 ** 40
 PART = (2 ** 256 - 1) // TOTAL_PARTS
 INTERVAL_DIFFERENCE = 10 ** 30
 hash_matcher = "fffffff"  # This is usually the prefix for the hash in the output
+log = logging.getLogger(__name__)
 
 
 class KeccakFunctionManager: