Merge branch 'develop' into model-balances

.circleci/config.yml

@@ -103,6 +103,8 @@ jobs:
           name: Run Edelweiss
           command: |
               docker run \
+                -e CIRCLE_BRANCH=$CIRCLE_BRANCH \
+                -e CIRCLE_SHA1=$CIRCLE_SHA1 \
                 -e CIRCLE_BUILD_NUM=$CIRCLE_BUILD_NUM \
                 -e CIRCLE_BUILD_URL=$CIRCLE_BUILD_URL \
                 -e CIRCLE_WEBHOOK_URL=$CIRCLE_WEBHOOK_URL \

mythril/analysis/modules/ether_thief.py

@@ -16,7 +16,7 @@ log = logging.getLogger(__name__)
 
 DESCRIPTION = """
 
-Search for cases where Ether can be withdrawn to a user-specified address. 
+Search for cases where Ether can be withdrawn to a user-specified address.
 
 An issue is reported if:
 
@@ -121,7 +121,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/analysis/templates/report_as_markdown.jinja2

@@ -26,6 +26,12 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
 {% endif %}
 {% if issue.tx_sequence %}
 
+### Initial State:
+
+{% for key, value in issue.tx_sequence.initialState.accounts.items() %}
+Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif key == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, balance: {{value.balance}}, nonce:{{value.nonce}}, storage:{{value.storage}}
+{% endfor %}
+
 ### Transaction Sequence
 
 {% for step in issue.tx_sequence.steps %}

mythril/analysis/templates/report_as_text.jinja2

@@ -19,6 +19,12 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
 --------------------
 {% endif %}
 {% if issue.tx_sequence %}
+Initial State:
+
+{% for key, value in issue.tx_sequence.initialState.accounts.items() %}
+Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif key == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, balance: {{value.balance}}, nonce:{{value.nonce}}, storage:{{value.storage}}
+{% endfor %}
+
 Transaction Sequence:
 
 {% for step in issue.tx_sequence.steps %}

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
@@ -125,7 +125,6 @@ def get_callee_account(
     :param dynamic_loader: dynamic loader to use
     :return: Account belonging to callee
     """
-    environment = global_state.environment
     accounts = global_state.accounts
 
     if isinstance(callee_address, BitVec):
@@ -138,21 +137,21 @@ def get_callee_account(
         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(

mythril/laser/ethereum/instructions.py

@@ -197,7 +197,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:
-                pass
+            except ValueError as e:
+                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]