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

mythril/alarm.py

@@ -1,25 +0,0 @@
-import signal
-from types import FrameType
-from mythril.exceptions import OutOfTimeError
-
-
-def sigalrm_handler(signum: int, frame: FrameType) -> None:
-    raise OutOfTimeError
-
-
-def start_timeout(timeout: int) -> None:
-    """
-    Starts a timeout
-    :param timeout: Time in seconds to set the timeout for
-    :return: None
-    """
-    signal.signal(signal.SIGALRM, sigalrm_handler)
-    signal.alarm(timeout)
-
-
-def disable_timeout() -> None:
-    """
-    Ensures that the timeout is disabled
-    :return: None
-    """
-    signal.alarm(0)

mythril/analysis/solver.py

@@ -3,6 +3,7 @@ from z3 import sat, unknown, FuncInterp
 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_serializable_statespace(statespace):
                 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_serializable_statespace(statespace):
 
         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 datetime import datetime, timedelta
 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.account import Account
 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,8 +120,7 @@ class LaserEVM:
         """
         log.debug("Starting LASER execution")
 
-        try:
-            alarm.start_timeout(self.execution_timeout)
+        time_handler.start_execution(self.execution_timeout)
         self.time = datetime.now()
 
         if main_address:
@@ -147,11 +145,6 @@ class LaserEVM:
 
             self._execute_transactions(created_account.address)
 
-        except OutOfTimeError:
-            log.warning("Timeout occurred, ending symbolic execution")
-        finally:
-            alarm.disable_timeout()
-
         log.info("Finished symbolic execution")
         if self.requires_statespace:
             log.info(

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 @@ class Bool(Expression[z3.BoolRef]):
 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 @@ class BaseSolver(Generic[T]):
 
         :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 @@ import solc
 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 @@ setup(
         "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)