Merge branch 'develop' of github.com:ConsenSys/mythril into mypy_branch

mythril/analysis/solver.py

@@ -3,6 +3,7 @@
 import z3
 
 from mythril.laser.smt import simplify, UGE, Optimize, symbol_factory
+from mythril.laser.ethereum.time_handler import time_handler
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
@@ -21,8 +22,10 @@ def get_model(constraints, minimize=(), maximize=()):
     :return:
     """
     s = Optimize()
-    s.set_timeout(100000)
-
+    timeout = min(100000, time_handler.time_remaining() - 500)
+    if timeout <= 0:
+        raise UnsatError
+    s.set_timeout(timeout)
     for constraint in constraints:
         if type(constraint) == bool and not constraint:
             raise UnsatError

mythril/analysis/traceexplore.py

@@ -97,7 +97,7 @@ def get_state_accounts(node_state):
                 account["balance"] = str(account["balance"])
 
                 storage = {}
-                for storage_key in account["storage"]:
+                for storage_key in account["storage"].keys():
                     storage[str(storage_key)] = str(account["storage"][storage_key])
 
                 state_accounts.append({"address": key, "storage": storage})
@@ -110,7 +110,10 @@ def get_state_accounts(node_state):
 
         for state in states:
             state["machine"]["stack"] = [str(s) for s in state["machine"]["stack"]]
-            state["machine"]["memory"] = [str(m) for m in state["machine"]["memory"]]
+            state["machine"]["memory"] = [
+                str(m)
+                for m in state["machine"]["memory"][: len(state["machine"]["memory"])]
+            ]
 
         truncated_code = truncated_code.replace("\\n", "\n")
         code = code.replace("\\n", "\n")

mythril/exceptions.py

@@ -7,10 +7,6 @@ class MythrilBaseException(Exception):
     pass
 
 
-class OutOfTimeError(MythrilBaseException):
-    pass
-
-
 class CompilerError(MythrilBaseException):
     """A Mythril exception denoting an error during code compilation."""
 

mythril/laser/ethereum/svm.py

@@ -6,8 +6,6 @@
 from functools import reduce
 from typing import Callable, Dict, DefaultDict, List, Tuple, Union
 
-from mythril import alarm
-from mythril.exceptions import OutOfTimeError
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
 from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
 from mythril.laser.ethereum.evm_exceptions import VmException
@@ -16,6 +14,7 @@
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
+from mythril.laser.ethereum.time_handler import time_handler
 from mythril.laser.ethereum.plugins.signals import PluginSignal, PluginSkipWorldState
 from mythril.laser.ethereum.transaction import (
     ContractCreationTransaction,
@@ -121,36 +120,30 @@ def sym_exec(
         """
         log.debug("Starting LASER execution")
 
-        try:
-            alarm.start_timeout(self.execution_timeout)
-            self.time = datetime.now()
+        time_handler.start_execution(self.execution_timeout)
+        self.time = datetime.now()
 
-            if main_address:
-                log.info("Starting message call transaction to {}".format(main_address))
-                self._execute_transactions(main_address)
+        if main_address:
+            log.info("Starting message call transaction to {}".format(main_address))
+            self._execute_transactions(main_address)
 
-            elif creation_code:
-                log.info("Starting contract creation transaction")
-                created_account = execute_contract_creation(
-                    self, creation_code, contract_name
+        elif creation_code:
+            log.info("Starting contract creation transaction")
+            created_account = execute_contract_creation(
+                self, creation_code, contract_name
+            )
+            log.info(
+                "Finished contract creation, found {} open states".format(
+                    len(self.open_states)
                 )
-                log.info(
-                    "Finished contract creation, found {} open states".format(
-                        len(self.open_states)
-                    )
+            )
+            if len(self.open_states) == 0:
+                log.warning(
+                    "No contract was created during the execution of contract creation "
+                    "Increase the resources for creation execution (--max-depth or --create-timeout)"
                 )
-                if len(self.open_states) == 0:
-                    log.warning(
-                        "No contract was created during the execution of contract creation "
-                        "Increase the resources for creation execution (--max-depth or --create-timeout)"
-                    )
-
-                self._execute_transactions(created_account.address)
-
-        except OutOfTimeError:
-            log.warning("Timeout occurred, ending symbolic execution")
-        finally:
-            alarm.disable_timeout()
+
+            self._execute_transactions(created_account.address)
 
         log.info("Finished symbolic execution")
         if self.requires_statespace:

mythril/laser/ethereum/time_handler.py

@@ -0,0 +1,18 @@
+import time
+from mythril.support.support_utils import Singleton
+
+
+class TimeHandler(object, metaclass=Singleton):
+    def __init__(self):
+        self._start_time = None
+        self._execution_time = None
+
+    def start_execution(self, execution_time):
+        self._start_time = int(time.time() * 1000)
+        self._execution_time = execution_time * 1000
+
+    def time_remaining(self):
+        return self._execution_time - (int(time.time() * 1000) - self._start_time)
+
+
+time_handler = TimeHandler()

mythril/laser/smt/bool.py

@@ -84,6 +84,7 @@ def __bool__(self) -> bool:
 def And(*args: Bool) -> Bool:
     """Create an And expression."""
     union = []
+    args = [arg if isinstance(arg, Bool) else Bool(arg) for arg in args]
     for arg in args:
         union.append(arg.annotations)
     return Bool(z3.And([a.raw for a in args]), union)

mythril/laser/smt/solver.py

@@ -20,6 +20,7 @@ def set_timeout(self, timeout: int) -> None:
 
         :param timeout:
         """
+        assert timeout > 0  # timeout <= 0 isn't supported by z3
         self.raw.set(timeout=timeout)
 
     def add(self, constraints: Union[Bool, List[Bool]]) -> None:

mythril/mythril.py

@@ -19,17 +19,10 @@
 from ethereum import utils
 from solc.exceptions import SolcError
 
-from mythril.analysis.callgraph import generate_graph
-from mythril.analysis.report import Report
-from mythril.analysis.security import fire_lasers
-from mythril.analysis.symbolic import SymExecWrapper
-from mythril.analysis.traceexplore import get_serializable_statespace
 from mythril.ethereum import util
 from mythril.ethereum.evmcontract import EVMContract
-from mythril.ethereum.interface.leveldb.client import EthLevelDB
 from mythril.ethereum.interface.rpc.client import EthJsonRpc
 from mythril.ethereum.interface.rpc.exceptions import ConnectionError
-from mythril.exceptions import CompilerError, CriticalError, NoContractFoundError
 from mythril.solidity.soliditycontract import SolidityContract, get_contracts_from_file
 from mythril.support import signatures
 from mythril.support.source_support import Source

mythril/support/support_utils.py

@@ -1 +1,21 @@
 """This module contains utility functions for the Mythril support package."""
+
+
+class Singleton(type):
+    """A metaclass type implementing the singleton pattern."""
+
+    _instances = {}
+
+    def __call__(cls, *args, **kwargs):
+        """Delegate the call to an existing resource or a a new one.
+
+        This is not thread- or process-safe by default. It must be protected with
+        a lock.
+
+        :param args:
+        :param kwargs:
+        :return:
+        """
+        if cls not in cls._instances:
+            cls._instances[cls] = super(Singleton, cls).__call__(*args, **kwargs)
+        return cls._instances[cls]

requirements.txt

@@ -25,5 +25,5 @@ pytest_mock
 requests
 rlp>=1.0.1
 transaction>=2.2.1
-z3-solver>=4.8.0.0
+z3-solver-mythril>=4.8.4.1
 pysha3

setup.py

@@ -75,7 +75,7 @@ def read_file(fname):
         "coloredlogs>=10.0",
         "py_ecc==1.4.2",
         "ethereum>=2.3.2",
-        "z3-solver>=4.8.0.0",
+        "z3-solver-mythril>=4.8.4.1",
         "requests",
         "py-solc",
         "plyvel",

tests/laser/transaction/create_transaction_test.py

@@ -41,7 +41,10 @@ def test_sym_exec():
     )
 
     sym = SymExecWrapper(
-        contract, address=(util.get_indexed_address(0)), strategy="dfs"
+        contract,
+        address=(util.get_indexed_address(0)),
+        strategy="dfs",
+        execution_timeout=10,
     )
     issues = fire_lasers(sym)