Merge branch 'develop' into feature/import-custom-modules

mythril/analysis/modules/ether_thief.py

@@ -79,8 +79,6 @@ class EtherThief(DetectionModule):
         if instruction["opcode"] != "CALL":
             return []
 
-        address = instruction["address"]
-
         value = state.mstate.stack[-3]
         target = state.mstate.stack[-2]
 
@@ -95,7 +93,9 @@ class EtherThief(DetectionModule):
             Also constrain the addition from overflowing (otherwise the solver produces solutions with
             ridiculously high call values).
             """
-            constraints += [BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, False)]
+            constraints += [
+                BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, signed=False)
+            ]
             eth_sent_by_attacker = Sum(
                 eth_sent_by_attacker,
                 tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0),
@@ -140,7 +140,7 @@ class EtherThief(DetectionModule):
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
         except UnsatError:
-            log.debug("[ETHER_THIEF] no model found")
+            log.debug("No model found")
             return []
 
         return [issue]

mythril/laser/ethereum/call.py

@@ -4,7 +4,7 @@ parameters for the new global state."""
 
 import logging
 import re
-from typing import Union, List, cast, Callable
+from typing import Union, List, cast, Callable, Optional
 
 import mythril.laser.ethereum.util as util
 from mythril.laser.ethereum import natives
@@ -84,6 +84,7 @@ def get_callee_address(
     except TypeError:
         log.debug("Symbolic call encountered")
 
+        # TODO: This is broken. Now it should be Storage[(\d+)].
         match = re.search(r"storage_(\d+)", str(simplify(symbolic_to_address)))
         log.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
@@ -99,7 +100,7 @@ def get_callee_address(
                 "0x{:040X}".format(environment.active_account.address.value), index
             )
         # TODO: verify whether this happens or not
-        except:
+        except Exception:
             log.debug("Error accessing contract storage.")
             raise ValueError
 
@@ -120,28 +121,27 @@ def get_callee_account(
     :param dynamic_loader: dynamic loader to use
     :return: Account belonging to callee
     """
-    environment = global_state.environment
     accounts = global_state.accounts
 
     try:
         return global_state.accounts[int(callee_address, 16)]
     except KeyError:
         # We have a valid call address, but contract is not in the modules list
-        log.debug("Module with address " + callee_address + " not loaded.")
+        log.debug("Module with address %s not loaded.", callee_address)
 
     if dynamic_loader is None:
-        raise ValueError()
+        raise ValueError("dynamic_loader is None")
 
     log.debug("Attempting to load dependency")
 
     try:
         code = dynamic_loader.dynld(callee_address)
     except ValueError as error:
-        log.debug("Unable to execute dynamic loader because: {}".format(str(error)))
+        log.debug("Unable to execute dynamic loader because: %s", error)
         raise error
     if code is None:
         log.debug("No code returned, not a contract account?")
-        raise ValueError()
+        raise ValueError("No code returned")
     log.debug("Dependency loaded: " + callee_address)
 
     callee_account = Account(
@@ -213,7 +213,7 @@ def native_call(
     call_data: BaseCalldata,
     memory_out_offset: Union[int, Expression],
     memory_out_size: Union[int, Expression],
-) -> Union[List[GlobalState], None]:
+) -> Optional[List[GlobalState]]:
     if not 0 < int(callee_address, 16) < 5:
         return None
 

mythril/laser/ethereum/instructions.py

@@ -172,7 +172,7 @@ class Instruction:
         :return:
         """
         # Generalize some ops
-        log.debug("Evaluating {}".format(self.op_code))
+        log.debug("Evaluating %s at %i", self.op_code, global_state.mstate.pc)
         op = self.op_code.lower()
         if self.op_code.startswith("PUSH"):
             op = "push"

mythril/laser/ethereum/state/account.py

@@ -2,6 +2,7 @@
 
 This includes classes representing accounts and their storage.
 """
+import logging
 from copy import copy, deepcopy
 from typing import Any, Dict, Union, Tuple, cast
 
@@ -19,6 +20,8 @@ from mythril.laser.smt import (
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.smt import symbol_factory
 
+log = logging.getLogger(__name__)
+
 
 class StorageRegion:
     def __getitem__(self, item):
@@ -74,7 +77,7 @@ class Storage:
             item = self._sanitize(cast(BitVecFunc, item).input_)
         value = storage[item]
         if (
-            value.value == 0
+            (value.value == 0 or value.value is None)  # 0 for Array, None for K
             and self.address
             and item.symbolic is False
             and self.address.value != 0
@@ -93,8 +96,8 @@ class Storage:
                 )
                 self.printable_storage[item] = storage[item]
                 return storage[item]
-            except ValueError:
+            except ValueError as e:
-                pass
+                log.debug("Couldn't read storage at %s: %s", item, e)
 
         return simplify(storage[item])
 

mythril/laser/ethereum/svm.py

@@ -3,7 +3,7 @@ import logging
 from collections import defaultdict
 from copy import copy
 from datetime import datetime, timedelta
-from typing import Callable, Dict, DefaultDict, List, Tuple, Union
+from typing import Callable, Dict, DefaultDict, List, Tuple, Optional
 
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
 from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
@@ -75,6 +75,7 @@ class LaserEVM:
         self.total_states = 0
         self.dynamic_loader = dynamic_loader
 
+        # TODO: What about using a deque here?
         self.work_list = []  # type: List[GlobalState]
         self.strategy = strategy(self.work_list, max_depth)
         self.max_depth = max_depth
@@ -209,7 +210,7 @@ class LaserEVM:
             for hook in self._stop_sym_trans_hooks:
                 hook()
 
-    def exec(self, create=False, track_gas=False) -> Union[List[GlobalState], None]:
+    def exec(self, create=False, track_gas=False) -> Optional[List[GlobalState]]:
         """
 
         :param create:
@@ -223,6 +224,7 @@ class LaserEVM:
                 and create
                 and self.time + timedelta(seconds=self.create_timeout) <= datetime.now()
             ):
+                log.debug("Hit create timeout, returning.")
                 return final_states + [global_state] if track_gas else None
 
             if (
@@ -231,6 +233,7 @@ class LaserEVM:
                 <= datetime.now()
                 and not create
             ):
+                log.debug("Hit execution timeout, returning.")
                 return final_states + [global_state] if track_gas else None
 
             try:
@@ -243,8 +246,7 @@ class LaserEVM:
                 state for state in new_states if state.mstate.constraints.is_possible
             ]
 
-            self.manage_cfg(op_code, new_states)
+            self.manage_cfg(op_code, new_states)  # TODO: What about op_code is None?
-
             if new_states:
                 self.work_list += new_states
             elif track_gas:
@@ -265,11 +267,11 @@ class LaserEVM:
 
     def execute_state(
         self, global_state: GlobalState
-    ) -> Tuple[List[GlobalState], Union[str, None]]:
+    ) -> Tuple[List[GlobalState], Optional[str]]:
-        """
+        """Execute a single instruction in global_state.
 
         :param global_state:
-        :return:
+        :return: A list of successor states.
         """
         # Execute hooks
         for hook in self._execute_state_hooks:
@@ -405,6 +407,7 @@ class LaserEVM:
             for state in new_states:
                 self._new_node_state(state)
         elif opcode == "JUMPI":
+            assert len(new_states) <= 2
             for state in new_states:
                 self._new_node_state(
                     state, JumpType.CONDITIONAL, state.mstate.constraints[-1]