Merge branch 'develop' into edelweiss/2.0

.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 \

README.md

@@ -32,11 +32,50 @@ Install from Pypi:
 $ pip3 install mythril
 ```
 
-See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup) for more detailed instructions. 
+See the [docs](https://mythril-classic.readthedocs.io/en/master/installation.html) for more detailed instructions. 
 
 ## Usage
 
-Instructions for using Mythril are found on the [Wiki](https://github.com/ConsenSys/mythril/wiki). 
+Run:
+
+```
+$ myth analyze <solidity-file>
+```
+
+Or:
+
+```
+$ myth analyze -a <contract-address>
+```
+
+Specify the maximum number of transaction to explore with `-t <number>`. You can also set a timeout with `--execution-timeout <seconds>`. Example ([source code](https://gist.github.com/b-mueller/2b251297ce88aa7628680f50f177a81a#file-killbilly-sol)):
+
+```
+==== Unprotected Selfdestruct ====
+SWC ID: 106
+Severity: High
+Contract: KillBilly
+Function name: commencekilling()
+PC address: 354
+Estimated Gas Usage: 574 - 999
+The contract can be killed by anyone.
+Anyone can kill this contract and withdraw its balance to an arbitrary address.
+--------------------
+In file: killbilly.sol:22
+
+selfdestruct(msg.sender)
+
+--------------------
+Transaction Sequence:
+
+Caller: [CREATOR], data: [CONTRACT CREATION], value: 0x0
+Caller: [ATTACKER], function: killerize(address), txdata: 0x9fa299ccbebebebebebebebebebebebedeadbeefdeadbeefdeadbeefdeadbeefdeadbeef, value: 0x0
+Caller: [ATTACKER], function: activatekillability(), txdata: 0x84057065, value: 0x0
+Caller: [ATTACKER], function: commencekilling(), txdata: 0x7c11da20, value: 0x0
+```
+
+
+Instructions for using Mythril are found on the [docs](https://mythril-classic.readthedocs.io/en/master/). 
 
 For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
 

all_tests.sh

@@ -7,22 +7,6 @@ assert sys.version_info[0:2] >= (3,5), \
 """Please make sure you are using Python 3.5 or later.
 You ran with {}""".format(sys.version)' || exit $?
 
-echo "Checking solc version..."
-out=$(solc --version) || {
-    echo 2>&1 "Please make sure you have solc installed, version 0.4.21 or greater"
-
-    }
-case $out in
-    *Version:\ 0.4.2[1-9]* )
-	echo $out
-	;;
-    * )
-	echo $out
-	echo "Please make sure your solc version is at least 0.4.21"
-	exit 1
-	;;
-esac
-
 echo "Checking that truffle is installed..."
 if ! which truffle ; then
     echo "Please make sure you have etherum truffle installed (npm install -g truffle)"

docs/source/index.rst

@@ -9,6 +9,7 @@ Welcome to Mythril's documentation!
    installation
    security-analysis
    analysis-modules
+   mythx-analysis
    mythril
 
 

docs/source/module-list.rst

@@ -67,3 +67,9 @@ Unchecked Retval
 ****************
 
 The `unchecked retval module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.
+
+****************
+Unchecked Retval
+****************
+
+The `user supplied assertion module <https://github.com/ConsenSys/mythril/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_ for user-supplied assertions. User supplied assertions should be log messages of the form: :code:`emit AssertionFailed(string)`.

docs/source/mythx-analysis.rst

@@ -0,0 +1,63 @@
+MythX Analysis
+=================
+
+Run :code:`myth pro` with one of the input options described below will run a `MythX analysis <https://mythx.io>`_ on the desired input. This includes a run of Mythril, the fuzzer Harvey, and the static analysis engine Maru and has some false-positive filtering only possible by combining the tool capabilities.
+
+**************
+Authentication
+**************
+
+In order to authenticate with the MythX API, set the environment variables ``MYTHX_PASSWORD`` and ``MYTHX_ETH_ADDRESS``.
+
+.. code-block:: bash
+
+   $ export MYTHX_ETH_ADDRESS='0x0000000000000000000000000000000000000000'
+   $ export MYTHX_PASSWORD='password'
+
+***********************
+Analyzing Solidity Code
+***********************
+
+The input format is the same as a regular Mythril analysis.
+
+.. code-block:: bash
+
+   $ myth pro ether_send.sol
+   ==== Unprotected Ether Withdrawal ====
+   SWC ID: 105
+   Severity: High
+   Contract: Crowdfunding
+   Function name: withdrawfunds()
+   PC address: 730
+   Anyone can withdraw ETH from the contract account.
+   Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.
+   --------------------
+   In file: tests/testdata/input_contracts/ether_send.sol:21
+
+   msg.sender.transfer(address(this).balance)
+
+   --------------------
+
+If an input file contains multiple contract definitions, Mythril analyzes the *last* bytecode output produced by solc. You can override this by specifying the contract name explicitly:
+
+.. code-block:: bash
+
+   myth pro OmiseGo.sol:OMGToken
+
+To specify a contract address, use :code:`-a <address>`
+
+****************************
+Analyzing On-Chain Contracts
+****************************
+
+Analyzing a mainnet contract via INFURA:
+
+.. code-block:: bash
+
+   myth pro -a 0x5c436ff914c458983414019195e0f4ecbef9e6dd
+
+Adding the :code:`-l` flag will cause mythril to automatically retrieve dependencies, such as dynamically linked library contracts:
+
+.. code-block:: bash
+
+   myth -v4 pro -l -a 0xEbFD99838cb0c132016B9E117563CB41f2B02264

docs/source/security-analysis.rst

@@ -1,7 +1,7 @@
 Security Analysis
 =================
 
-Run :code:`myth -x` with one of the input options described below will run the analysis modules in the `/analysis/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/modules>`_ directory.
+Run :code:`myth analyze` with one of the input options described below will run the analysis modules in the `/analysis/modules <https://github.com/ConsenSys/mythril/tree/master/mythril/analysis/modules>`_ directory.
 
 ***********************
 Analyzing Solidity Code

mythril/__version__.py

@@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
 as for importing into Python.
 """
 
-__version__ = "v0.21.12"
+__version__ = "v0.21.17"

mythril/analysis/analysis_args.py

@@ -0,0 +1,30 @@
+from mythril.support.support_utils import Singleton
+
+
+class AnalysisArgs(object, metaclass=Singleton):
+    """
+    This module helps in preventing args being sent through multiple of classes to reach analysis modules
+    """
+
+    def __init__(self):
+        self._loop_bound = 3
+        self._solver_timeout = 10000
+
+    def set_loop_bound(self, loop_bound: int):
+        if loop_bound is not None:
+            self._loop_bound = loop_bound
+
+    def set_solver_timeout(self, solver_timeout: int):
+        if solver_timeout is not None:
+            self._solver_timeout = solver_timeout
+
+    @property
+    def loop_bound(self):
+        return self._loop_bound
+
+    @property
+    def solver_timeout(self):
+        return self._solver_timeout
+
+
+analysis_args = AnalysisArgs()

mythril/analysis/call_helpers.py

@@ -4,6 +4,7 @@ from typing import Union
 
 from mythril.analysis.ops import VarType, Call, get_variable
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 
 
 def get_call_from_state(state: GlobalState) -> Union[Call, None]:
@@ -17,7 +18,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]:
     op = instruction["opcode"]
     stack = state.mstate.stack
 
-    if op in ("CALL", "CALLCODE", "STATICCALL"):
+    if op in ("CALL", "CALLCODE"):
         gas, to, value, meminstart, meminsz, memoutstart, memoutsz = (
             get_variable(stack[-1]),
             get_variable(stack[-2]),
@@ -28,7 +29,7 @@ def get_call_from_state(state: GlobalState) -> Union[Call, None]:
             get_variable(stack[-7]),
         )
 
-        if to.type == VarType.CONCRETE and 0 < to.val < 5:
+        if to.type == VarType.CONCRETE and 0 < to.val <= PRECOMPILE_COUNT:
             return None
 
         if meminstart.type == VarType.CONCRETE and meminsz.type == VarType.CONCRETE:

mythril/analysis/modules/base.py

@@ -3,6 +3,7 @@ modules."""
 
 import logging
 from typing import List, Set
+
 from mythril.analysis.report import Issue
 
 log = logging.getLogger(__name__)
@@ -34,21 +35,14 @@ class DetectionModule:
                 self.name,
             )
         self.entrypoint = entrypoint
-        self._issues = []  # type: List[Issue]
-        self._cache = set()  # type: Set[int]
-
-    @property
-    def issues(self):
-        """
-        Returns the issues
-        """
-        return self._issues
+        self.issues = []  # type: List[Issue]
+        self.cache = set()  # type: Set[int]
 
     def reset_module(self):
         """
         Resets issues
         """
-        self._issues = []
+        self.issues = []
 
     def execute(self, statespace) -> None:
         """The entry point for execution, which is being called by Mythril.

mythril/analysis/modules/delegatecall.py

@@ -1,79 +1,24 @@
 """This module contains the detection code for insecure delegate call usage."""
-import json
 import logging
-from copy import copy
-from typing import List, cast, Dict
+from typing import List
 
-from mythril.analysis import solver
+from mythril.analysis.potential_issues import (
+    get_potential_issues_annotation,
+    PotentialIssue,
+)
 from mythril.analysis.swc_data import DELEGATECALL_TO_UNTRUSTED_CONTRACT
 from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
-from mythril.analysis.report import Issue
 from mythril.analysis.modules.base import DetectionModule
 from mythril.exceptions import UnsatError
-from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.smt import symbol_factory, UGT
 
 log = logging.getLogger(__name__)
 
 
-class DelegateCallAnnotation(StateAnnotation):
-    def __init__(self, call_state: GlobalState, constraints: List) -> None:
-        """
-        Initialize DelegateCall Annotation
-        :param call_state: Call state
-        """
-        self.call_state = call_state
-        self.constraints = constraints
-        self.return_value = call_state.new_bitvec(
-            "retval_{}".format(call_state.get_current_instruction()["address"]), 256
-        )
-
-    def _copy__(self):
-        return DelegateCallAnnotation(self.call_state, copy(self.constraints))
-
-    def get_issue(self, global_state: GlobalState, transaction_sequence: Dict) -> Issue:
-        """
-        Returns Issue for the annotation
-        :param global_state: Global State
-        :param transaction_sequence: Transaction sequence
-        :return: Issue
-        """
-
-        address = self.call_state.get_current_instruction()["address"]
-        logging.debug(
-            "[DELEGATECALL] Detected delegatecall to a user-supplied address : {}".format(
-                address
-            )
-        )
-        description_head = "The contract delegates execution to another contract with a user-supplied address."
-        description_tail = (
-            "The smart contract delegates execution to a user-supplied address. Note that callers "
-            "can execute arbitrary contracts and that the callee contract "
-            "can access the storage of the calling contract. "
-        )
-
-        return Issue(
-            contract=self.call_state.environment.active_account.contract_name,
-            function_name=self.call_state.environment.active_function_name,
-            address=address,
-            swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT,
-            title="Delegatecall Proxy To User-Supplied Address",
-            bytecode=global_state.environment.code.bytecode,
-            severity="Medium",
-            description_head=description_head,
-            description_tail=description_tail,
-            transaction_sequence=transaction_sequence,
-            gas_used=(
-                global_state.mstate.min_gas_used,
-                global_state.mstate.max_gas_used,
-            ),
-        )
-
-
 class DelegateCallModule(DetectionModule):
     """This module detects calldata being forwarded using DELEGATECALL."""
 
@@ -84,7 +29,7 @@ class DelegateCallModule(DetectionModule):
             swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT,
             description="Check for invocations of delegatecall(msg.data) in the fallback function.",
             entrypoint="callback",
-            pre_hooks=["DELEGATECALL", "RETURN", "STOP"],
+            pre_hooks=["DELEGATECALL"],
         )
 
     def _execute(self, state: GlobalState) -> None:
@@ -93,63 +38,68 @@ class DelegateCallModule(DetectionModule):
         :param state:
         :return:
         """
-        if state.get_current_instruction()["address"] in self._cache:
+        if state.get_current_instruction()["address"] in self.cache:
             return
-        issues = self._analyze_state(state)
-        for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
+        potential_issues = self._analyze_state(state)
 
-    @staticmethod
-    def _analyze_state(state: GlobalState) -> List[Issue]:
+        annotation = get_potential_issues_annotation(state)
+        annotation.potential_issues.extend(potential_issues)
+
+    def _analyze_state(self, state: GlobalState) -> List[PotentialIssue]:
         """
         :param state: the current state
         :return: returns the issues for that corresponding state
         """
-        issues = []
-        op_code = state.get_current_instruction()["opcode"]
-        annotations = cast(
-            List[DelegateCallAnnotation],
-            list(state.get_annotations(DelegateCallAnnotation)),
-        )
-
-        if len(annotations) == 0 and op_code in ("RETURN", "STOP"):
-            return []
-
-        if op_code == "DELEGATECALL":
         gas = state.mstate.stack[-1]
         to = state.mstate.stack[-2]
 
         constraints = [
             to == ATTACKER_ADDRESS,
             UGT(gas, symbol_factory.BitVecVal(2300, 256)),
+            state.new_bitvec(
+                "retval_{}".format(state.get_current_instruction()["address"]), 256
+            )
+            == 1,
         ]
 
         for tx in state.world_state.transaction_sequence:
             if not isinstance(tx, ContractCreationTransaction):
                 constraints.append(tx.caller == ATTACKER_ADDRESS)
 
-            state.annotate(DelegateCallAnnotation(state, constraints))
-
-            return []
-        else:
-            for annotation in annotations:
         try:
-                    transaction_sequence = solver.get_transaction_sequence(
-                        state,
-                        state.mstate.constraints
-                        + annotation.constraints
-                        + [annotation.return_value == 1],
+            address = state.get_current_instruction()["address"]
+
+            logging.debug(
+                "[DELEGATECALL] Detected potential delegatecall to a user-supplied address : {}".format(
+                    address
                 )
-                    issues.append(
-                        annotation.get_issue(
-                            state, transaction_sequence=transaction_sequence
             )
+
+            description_head = "The contract delegates execution to another contract with a user-supplied address."
+            description_tail = (
+                "The smart contract delegates execution to a user-supplied address. Note that callers "
+                "can execute arbitrary contracts and that the callee contract "
+                "can access the storage of the calling contract. "
             )
-                except UnsatError:
-                    continue
 
-            return issues
+            return [
+                PotentialIssue(
+                    contract=state.environment.active_account.contract_name,
+                    function_name=state.environment.active_function_name,
+                    address=address,
+                    swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT,
+                    bytecode=state.environment.code.bytecode,
+                    title="Delegatecall Proxy To User-Supplied Address",
+                    severity="Medium",
+                    description_head=description_head,
+                    description_tail=description_tail,
+                    constraints=constraints,
+                    detector=self,
+                )
+            ]
+
+        except UnsatError:
+            return []
 
 
 detector = DelegateCallModule()

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -74,12 +74,12 @@ class PredictableDependenceModule(DetectionModule):
         :param state:
         :return:
         """
-        if state.get_current_instruction()["address"] in self._cache:
+        if state.get_current_instruction()["address"] in self.cache:
             return
         issues = self._analyze_state(state)
         for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
+            self.cache.add(issue.address)
+        self.issues.extend(issues)
 
     @staticmethod
     def _analyze_state(state: GlobalState) -> list:

mythril/analysis/modules/deprecated_ops.py

@@ -1,6 +1,8 @@
 """This module contains the detection code for deprecated op codes."""
-from mythril.analysis.report import Issue
-from mythril.analysis.solver import get_transaction_sequence, UnsatError
+from mythril.analysis.potential_issues import (
+    PotentialIssue,
+    get_potential_issues_annotation,
+)
 from mythril.analysis.swc_data import DEPRECATED_FUNCTIONS_USAGE
 from mythril.analysis.modules.base import DetectionModule
 from mythril.laser.ethereum.state.global_state import GlobalState
@@ -32,15 +34,14 @@ class DeprecatedOperationsModule(DetectionModule):
         :param state:
         :return:
         """
-        if state.get_current_instruction()["address"] in self._cache:
+        if state.get_current_instruction()["address"] in self.cache:
             return
         issues = self._analyze_state(state)
-        for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
 
-    @staticmethod
-    def _analyze_state(state):
+        annotation = get_potential_issues_annotation(state)
+        annotation.potential_issues.extend(issues)
+
+    def _analyze_state(self, state):
         """
 
         :param state:
@@ -74,27 +75,22 @@ class DeprecatedOperationsModule(DetectionModule):
             )
             swc_id = DEPRECATED_FUNCTIONS_USAGE
         else:
-            return
-        try:
-            transaction_sequence = get_transaction_sequence(
-                state, state.mstate.constraints
-            )
-        except UnsatError:
-            return
-        issue = Issue(
+            return []
+
+        potential_issue = PotentialIssue(
             contract=state.environment.active_account.contract_name,
             function_name=state.environment.active_function_name,
             address=instruction["address"],
             title=title,
             bytecode=state.environment.code.bytecode,
+            detector=self,
             swc_id=swc_id,
             severity="Medium",
             description_head=description_head,
             description_tail=description_tail,
-            gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
-            transaction_sequence=transaction_sequence,
+            constraints=[],
         )
-        return [issue]
+        return [potential_issue]
 
 
 detector = DeprecatedOperationsModule()

mythril/analysis/modules/dos.py

@@ -7,6 +7,7 @@ from mythril.analysis.swc_data import DOS_WITH_BLOCK_GAS_LIMIT
 from mythril.analysis.report import Issue
 from mythril.analysis.modules.base import DetectionModule
 from mythril.analysis.solver import get_transaction_sequence, UnsatError
+from mythril.analysis.analysis_args import analysis_args
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum import util
@@ -55,7 +56,7 @@ class DosModule(DetectionModule):
         :return:
         """
         issues = self._analyze_state(state)
-        self._issues.extend(issues)
+        self.issues.extend(issues)
 
     def _analyze_state(self, state: GlobalState) -> List[Issue]:
         """
@@ -90,7 +91,7 @@ class DosModule(DetectionModule):
             else:
                 annotation.jump_targets[target] = 1
 
-            if annotation.jump_targets[target] > 2:
+            if annotation.jump_targets[target] > min(2, analysis_args.loop_bound - 1):
                 annotation.loop_start = address
 
         elif annotation.loop_start is not None:

mythril/analysis/modules/ether_thief.py

@@ -1,22 +1,22 @@
 """This module contains the detection code for unauthorized ether
 withdrawal."""
 import logging
-import json
 from copy import copy
 
-from mythril.analysis import solver
 from mythril.analysis.modules.base import DetectionModule
-from mythril.analysis.report import Issue
+from mythril.analysis.potential_issues import (
+    get_potential_issues_annotation,
+    PotentialIssue,
+)
 from mythril.laser.ethereum.transaction.symbolic import (
     ATTACKER_ADDRESS,
     CREATOR_ADDRESS,
 )
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
-from mythril.exceptions import UnsatError
-from mythril.laser.ethereum.transaction import ContractCreationTransaction
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import UGT, Sum, symbol_factory, BVAddNoOverflow
-from mythril.laser.smt.bitvec import If
+from mythril.laser.ethereum.transaction import ContractCreationTransaction
+
+from mythril.laser.smt import UGT, symbol_factory, UGE
 
 log = logging.getLogger(__name__)
 
@@ -61,71 +61,61 @@ class EtherThief(DetectionModule):
         :param state:
         :return:
         """
-        if state.get_current_instruction()["address"] in self._cache:
+        if state.get_current_instruction()["address"] in self.cache:
             return
-        issues = self._analyze_state(state)
-        for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
+        potential_issues = self._analyze_state(state)
+
+        annotation = get_potential_issues_annotation(state)
+        annotation.potential_issues.extend(potential_issues)
 
-    @staticmethod
-    def _analyze_state(state):
+    def _analyze_state(self, state):
         """
 
         :param state:
         :return:
         """
+        state = copy(state)
         instruction = state.get_current_instruction()
 
-        if instruction["opcode"] != "CALL":
-            return []
-
-        address = instruction["address"]
-
         value = state.mstate.stack[-3]
         target = state.mstate.stack[-2]
 
-        eth_sent_by_attacker = symbol_factory.BitVecVal(0, 256)
-
         constraints = copy(state.mstate.constraints)
 
-        for tx in state.world_state.transaction_sequence:
         """
-            Constraint: The call value must be greater than the sum of Ether sent by the attacker over all
-            transactions. This prevents false positives caused by legitimate refund functions.
-            Also constrain the addition from overflowing (otherwise the solver produces solutions with 
-            ridiculously high call values).
+        Require that the current transaction is sent by the attacker and
+        that the Ether sent to the attacker's address is greater than the
+        amount of Ether the attacker sent.
         """
-            constraints += [BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, False)]
-            eth_sent_by_attacker = Sum(
-                eth_sent_by_attacker,
-                tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0),
-            )
-
+        for tx in state.world_state.transaction_sequence:
             """
             Constraint: All transactions must originate from regular users (not the creator/owner).
             This prevents false positives where the owner willingly transfers ownership to another address.
             """
-
             if not isinstance(tx, ContractCreationTransaction):
                 constraints += [tx.caller != CREATOR_ADDRESS]
 
-        """
-        Require that the current transaction is sent by the attacker and
-        that the Ether is sent to the attacker's address.
-        """
+        attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256)
 
         constraints += [
-            UGT(value, eth_sent_by_attacker),
+            UGE(
+                state.world_state.balances[state.environment.active_account.address],
+                value,
+            )
+        ]
+        state.world_state.balances[attacker_address_bitvec] += value
+        state.world_state.balances[state.environment.active_account.address] -= value
+
+        constraints += [
+            UGT(
+                state.world_state.balances[attacker_address_bitvec],
+                state.world_state.starting_balances[attacker_address_bitvec],
+            ),
             target == ATTACKER_ADDRESS,
             state.current_transaction.caller == ATTACKER_ADDRESS,
         ]
 
-        try:
-
-            transaction_sequence = solver.get_transaction_sequence(state, constraints)
-
-            issue = Issue(
+        potential_issue = PotentialIssue(
             contract=state.environment.active_account.contract_name,
             function_name=state.environment.active_function_name,
             address=instruction["address"],
@@ -137,14 +127,11 @@ class EtherThief(DetectionModule):
             description_tail="Arbitrary senders other than the contract creator can withdraw ETH from the contract"
             + " account without previously having sent an equivalent amount of ETH to it. This is likely to be"
             + " a vulnerability.",
-                transaction_sequence=transaction_sequence,
-                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+            detector=self,
+            constraints=constraints,
         )
-        except UnsatError:
-            log.debug("[ETHER_THIEF] no model found")
-            return []
 
-        return [issue]
+        return [potential_issue]
 
 
 detector = EtherThief()

mythril/analysis/modules/exceptions.py

@@ -33,8 +33,8 @@ class ReachableExceptionsModule(DetectionModule):
         """
         issues = self._analyze_state(state)
         for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
+            self.cache.add(issue.address)
+        self.issues.extend(issues)
 
     @staticmethod
     def _analyze_state(state) -> list:

mythril/analysis/modules/external_calls.py

@@ -2,19 +2,23 @@
 calls."""
 
 from mythril.analysis import solver
+from mythril.analysis.potential_issues import (
+    PotentialIssue,
+    get_potential_issues_annotation,
+)
 from mythril.analysis.swc_data import REENTRANCY
+from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
 from mythril.analysis.modules.base import DetectionModule
-from mythril.analysis.report import Issue
 from mythril.laser.smt import UGT, symbol_factory, Or, BitVec
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.exceptions import UnsatError
 from copy import copy
 import logging
-import json
 
 log = logging.getLogger(__name__)
 
@@ -33,7 +37,7 @@ def _is_precompile_call(global_state: GlobalState):
     constraints += [
         Or(
             to < symbol_factory.BitVecVal(1, 256),
-            to > symbol_factory.BitVecVal(16, 256),
+            to > symbol_factory.BitVecVal(PRECOMPILE_COUNT, 256),
         )
     ]
 
@@ -64,13 +68,12 @@ class ExternalCalls(DetectionModule):
         :param state:
         :return:
         """
-        issues = self._analyze_state(state)
-        for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
+        potential_issues = self._analyze_state(state)
+
+        annotation = get_potential_issues_annotation(state)
+        annotation.potential_issues.extend(potential_issues)
 
-    @staticmethod
-    def _analyze_state(state):
+    def _analyze_state(self, state: GlobalState):
         """
 
         :param state:
@@ -82,10 +85,10 @@ class ExternalCalls(DetectionModule):
         address = state.get_current_instruction()["address"]
 
         try:
-            constraints = copy(state.mstate.constraints)
+            constraints = Constraints([UGT(gas, symbol_factory.BitVecVal(2300, 256))])
 
             transaction_sequence = solver.get_transaction_sequence(
-                state, constraints + [UGT(gas, symbol_factory.BitVecVal(2300, 256))]
+                state, constraints + state.mstate.constraints
             )
 
             # Check whether we can also set the callee address
@@ -98,7 +101,7 @@ class ExternalCalls(DetectionModule):
                         constraints.append(tx.caller == ATTACKER_ADDRESS)
 
                 transaction_sequence = solver.get_transaction_sequence(
-                    state, constraints
+                    state, constraints + state.mstate.constraints
                 )
 
                 description_head = "A call to a user-supplied address is executed."
@@ -109,7 +112,7 @@ class ExternalCalls(DetectionModule):
                     "contract state."
                 )
 
-                issue = Issue(
+                issue = PotentialIssue(
                     contract=state.environment.active_account.contract_name,
                     function_name=state.environment.active_function_name,
                     address=address,
@@ -119,8 +122,8 @@ class ExternalCalls(DetectionModule):
                     severity="Medium",
                     description_head=description_head,
                     description_tail=description_tail,
-                    transaction_sequence=transaction_sequence,
-                    gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                    constraints=constraints,
+                    detector=self,
                 )
 
             except UnsatError:
@@ -137,7 +140,7 @@ class ExternalCalls(DetectionModule):
                     "that the callee contract has been reviewed carefully."
                 )
 
-                issue = Issue(
+                issue = PotentialIssue(
                     contract=state.environment.active_account.contract_name,
                     function_name=state.environment.active_function_name,
                     address=address,
@@ -147,8 +150,8 @@ class ExternalCalls(DetectionModule):
                     severity="Low",
                     description_head=description_head,
                     description_tail=description_tail,
-                    transaction_sequence=transaction_sequence,
-                    gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                    constraints=constraints,
+                    detector=self,
                 )
 
         except UnsatError:

mythril/analysis/modules/integer.py

@@ -113,7 +113,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
 
         address = _get_address_from_state(state)
 
-        if address in self._cache:
+        if address in self.cache:
             return
 
         opcode = state.get_current_instruction()["opcode"]
@@ -331,8 +331,8 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             )
 
             address = _get_address_from_state(ostate)
-            self._cache.add(address)
-            self._issues.append(issue)
+            self.cache.add(address)
+            self.issues.append(issue)
 
 
 detector = IntegerOverflowUnderflowModule()

mythril/analysis/modules/multiple_sends.py

@@ -45,12 +45,12 @@ class MultipleSendsModule(DetectionModule):
         )
 
     def _execute(self, state: GlobalState) -> None:
-        if state.get_current_instruction()["address"] in self._cache:
+        if state.get_current_instruction()["address"] in self.cache:
             return
         issues = self._analyze_state(state)
         for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
+            self.cache.add(issue.address)
+        self.issues.extend(issues)
 
     @staticmethod
     def _analyze_state(state: GlobalState):

mythril/analysis/modules/state_change_external_calls.py

@@ -1,6 +1,10 @@
+from mythril.analysis.potential_issues import (
+    PotentialIssue,
+    get_potential_issues_annotation,
+)
 from mythril.analysis.swc_data import REENTRANCY
 from mythril.analysis.modules.base import DetectionModule
-from mythril.analysis.report import Issue
+from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.smt import symbol_factory, UGT, BitVec, Or
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.annotation import StateAnnotation
@@ -32,10 +36,12 @@ class StateChangeCallsAnnotation(StateAnnotation):
         new_annotation.state_change_states = self.state_change_states[:]
         return new_annotation
 
-    def get_issue(self, global_state: GlobalState) -> Optional[Issue]:
+    def get_issue(
+        self, global_state: GlobalState, detector: DetectionModule
+    ) -> Optional[PotentialIssue]:
         if not self.state_change_states:
             return None
-        constraints = copy(global_state.mstate.constraints)
+        constraints = Constraints()
         gas = self.call_state.mstate.stack[-1]
         to = self.call_state.mstate.stack[-2]
         constraints += [
@@ -50,10 +56,11 @@ class StateChangeCallsAnnotation(StateAnnotation):
 
         try:
             transaction_sequence = solver.get_transaction_sequence(
-                global_state, constraints
+                global_state, constraints + global_state.mstate.constraints
             )
         except UnsatError:
             return None
+
         severity = "Medium" if self.user_defined_address else "Low"
         address = global_state.get_current_instruction()["address"]
         logging.debug(
@@ -67,7 +74,7 @@ class StateChangeCallsAnnotation(StateAnnotation):
             "state change takes place. This can lead to business logic vulnerabilities."
         )
 
-        return Issue(
+        return PotentialIssue(
             contract=global_state.environment.active_account.contract_name,
             function_name=global_state.environment.active_function_name,
             address=address,
@@ -77,7 +84,8 @@ class StateChangeCallsAnnotation(StateAnnotation):
             description_tail=description_tail,
             swc_id=REENTRANCY,
             bytecode=global_state.environment.code.bytecode,
-            transaction_sequence=transaction_sequence,
+            constraints=constraints,
+            detector=detector,
         )
 
 
@@ -104,12 +112,12 @@ class StateChange(DetectionModule):
         )
 
     def _execute(self, state: GlobalState) -> None:
-        if state.get_current_instruction()["address"] in self._cache:
+        if state.get_current_instruction()["address"] in self.cache:
             return
         issues = self._analyze_state(state)
-        for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
+
+        annotation = get_potential_issues_annotation(state)
+        annotation.potential_issues.extend(issues)
 
     @staticmethod
     def _add_external_call(global_state: GlobalState) -> None:
@@ -139,8 +147,7 @@ class StateChange(DetectionModule):
         except UnsatError:
             pass
 
-    @staticmethod
-    def _analyze_state(global_state: GlobalState) -> List[Issue]:
+    def _analyze_state(self, global_state: GlobalState) -> List[PotentialIssue]:
 
         annotations = cast(
             List[StateChangeCallsAnnotation],
@@ -171,7 +178,9 @@ class StateChange(DetectionModule):
         for annotation in annotations:
             if not annotation.state_change_states:
                 continue
-            vulnerabilities.append(annotation.get_issue(global_state))
+            issue = annotation.get_issue(global_state, self)
+            if issue:
+                vulnerabilities.append(issue)
         return vulnerabilities
 
     @staticmethod

mythril/analysis/modules/suicide.py

@@ -46,12 +46,12 @@ class SuicideModule(DetectionModule):
         :param state:
         :return:
         """
-        if state.get_current_instruction()["address"] in self._cache:
+        if state.get_current_instruction()["address"] in self.cache:
             return
         issues = self._analyze_state(state)
         for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
+            self.cache.add(issue.address)
+        self.issues.extend(issues)
 
     @staticmethod
     def _analyze_state(state):
@@ -60,9 +60,7 @@ class SuicideModule(DetectionModule):
 
         to = state.mstate.stack[-1]
 
-        log.debug(
-            "[SUICIDE] SUICIDE in function " + state.environment.active_function_name
-        )
+        log.debug("SUICIDE in function %s", state.environment.active_function_name)
 
         description_head = "The contract can be killed by anyone."
 
@@ -103,7 +101,7 @@ class SuicideModule(DetectionModule):
             )
             return [issue]
         except UnsatError:
-            log.info("[UNCHECKED_SUICIDE] no model found")
+            log.debug("No model found")
 
         return []
 

mythril/analysis/modules/unchecked_retval.py

@@ -55,12 +55,12 @@ class UncheckedRetvalModule(DetectionModule):
         :param state:
         :return:
         """
-        if state.get_current_instruction()["address"] in self._cache:
+        if state.get_current_instruction()["address"] in self.cache:
             return
         issues = self._analyze_state(state)
         for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
+            self.cache.add(issue.address)
+        self.issues.extend(issues)
 
     def _analyze_state(self, state: GlobalState) -> list:
         instruction = state.get_current_instruction()
@@ -116,13 +116,9 @@ class UncheckedRetvalModule(DetectionModule):
             assert state.environment.code.instruction_list[state.mstate.pc - 1][
                 "opcode"
             ] in ["CALL", "DELEGATECALL", "STATICCALL", "CALLCODE"]
-            retval = state.mstate.stack[-1]
-            # Use Typed Dict after release of mypy 0.670 and remove type ignore
+            return_value = state.mstate.stack[-1]
             retvals.append(
-                {  # type: ignore
-                    "address": state.instruction["address"] - 1,
-                    "retval": retval,
-                }
+                {"address": state.instruction["address"] - 1, "retval": return_value}
             )
 
         return []

mythril/analysis/modules/user_assertions.py

@@ -0,0 +1,100 @@
+"""This module contains the detection code for potentially insecure low-level
+calls."""
+
+from mythril.analysis.potential_issues import (
+    PotentialIssue,
+    get_potential_issues_annotation,
+)
+from mythril.analysis.swc_data import ASSERT_VIOLATION
+from mythril.analysis.modules.base import DetectionModule
+from mythril.laser.ethereum.state.global_state import GlobalState
+import logging
+import eth_abi
+
+log = logging.getLogger(__name__)
+
+DESCRIPTION = """
+
+Search for reachable user-supplied exceptions.
+Report a warning if an log message is emitted: 'emit AssertionFailed(string)'
+
+"""
+
+assertion_failed_hash = (
+    0xB42604CB105A16C8F6DB8A41E6B00C0C1B4826465E8BC504B3EB3E88B3E6A4A0
+)
+
+
+class UserAssertions(DetectionModule):
+    """This module searches for user supplied exceptions: emit AssertionFailed("Error")."""
+
+    def __init__(self):
+        """"""
+        super().__init__(
+            name="External calls",
+            swc_id=ASSERT_VIOLATION,
+            description=DESCRIPTION,
+            entrypoint="callback",
+            pre_hooks=["LOG1"],
+        )
+
+    def _execute(self, state: GlobalState) -> None:
+        """
+
+        :param state:
+        :return:
+        """
+        potential_issues = self._analyze_state(state)
+
+        annotation = get_potential_issues_annotation(state)
+        annotation.potential_issues.extend(potential_issues)
+
+    def _analyze_state(self, state: GlobalState):
+        """
+
+        :param state:
+        :return:
+        """
+        topic, size, mem_start = state.mstate.stack[-3:]
+
+        if topic.symbolic or topic.value != assertion_failed_hash:
+            return []
+
+        message = None
+        if not mem_start.symbolic and not size.symbolic:
+            message = eth_abi.decode_single(
+                "string",
+                bytes(
+                    state.mstate.memory[
+                        mem_start.value + 32 : mem_start.value + size.value
+                    ]
+                ),
+            ).decode("utf8")
+
+        description_head = "A user-provided assertion failed."
+        if message:
+            description_tail = "A user-provided assertion failed with message '{}'. Make sure the user-provided assertion is correct.".format(
+                message
+            )
+        else:
+            description_tail = "A user-provided assertion failed. Make sure the user-provided assertion is correct."
+
+        address = state.get_current_instruction()["address"]
+        issue = PotentialIssue(
+            contract=state.environment.active_account.contract_name,
+            function_name=state.environment.active_function_name,
+            address=address,
+            swc_id=ASSERT_VIOLATION,
+            title="Assertion Failed",
+            bytecode=state.environment.code.bytecode,
+            severity="Medium",
+            description_head=description_head,
+            description_tail=description_tail,
+            constraints=[],
+            detector=self,
+        )
+
+        return [issue]
+
+
+detector = UserAssertions()

mythril/analysis/potential_issues.py

@@ -0,0 +1,108 @@
+from mythril.analysis.report import Issue
+from mythril.analysis.solver import get_transaction_sequence
+from mythril.exceptions import UnsatError
+from mythril.laser.ethereum.state.annotation import StateAnnotation
+from mythril.laser.ethereum.state.global_state import GlobalState
+
+
+class PotentialIssue:
+    """Representation of a potential issue"""
+
+    def __init__(
+        self,
+        contract,
+        function_name,
+        address,
+        swc_id,
+        title,
+        bytecode,
+        detector,
+        severity=None,
+        description_head="",
+        description_tail="",
+        constraints=None,
+    ):
+        """
+
+        :param contract: The contract
+        :param function_name: Function name where the issue is detected
+        :param address: The address of the issue
+        :param swc_id: Issue's corresponding swc-id
+        :param title: Title
+        :param bytecode: bytecode of the issue
+        :param detector: The detector the potential issue belongs to
+        :param gas_used: amount of gas used
+        :param severity: The severity of the issue
+        :param description_head: The top part of description
+        :param description_tail: The bottom part of the description
+        :param constraints: The non-path related constraints for the potential issue
+        """
+        self.title = title
+        self.contract = contract
+        self.function_name = function_name
+        self.address = address
+        self.description_head = description_head
+        self.description_tail = description_tail
+        self.severity = severity
+        self.swc_id = swc_id
+        self.bytecode = bytecode
+        self.constraints = constraints or []
+        self.detector = detector
+
+
+class PotentialIssuesAnnotation(StateAnnotation):
+    def __init__(self):
+        self.potential_issues = []
+
+
+def get_potential_issues_annotation(state: GlobalState) -> PotentialIssuesAnnotation:
+    """
+    Returns the potential issues annotation of the given global state, and creates one if
+    one does not already exist.
+
+    :param state: The global state
+    :return:
+    """
+    for annotation in state.annotations:
+        if isinstance(annotation, PotentialIssuesAnnotation):
+            return annotation
+
+    annotation = PotentialIssuesAnnotation()
+    state.annotate(annotation)
+    return annotation
+
+
+def check_potential_issues(state: GlobalState) -> None:
+    """
+    Called at the end of a transaction, checks potential issues, and
+    adds valid issues to the detector.
+
+    :param state: The final global state of a transaction
+    :return:
+    """
+    annotation = get_potential_issues_annotation(state)
+    for potential_issue in annotation.potential_issues:
+        try:
+            transaction_sequence = get_transaction_sequence(
+                state, state.mstate.constraints + potential_issue.constraints
+            )
+        except UnsatError:
+            continue
+
+        annotation.potential_issues.remove(potential_issue)
+        potential_issue.detector.cache.add(potential_issue.address)
+        potential_issue.detector.issues.append(
+            Issue(
+                contract=potential_issue.contract,
+                function_name=potential_issue.function_name,
+                address=potential_issue.address,
+                title=potential_issue.title,
+                bytecode=potential_issue.bytecode,
+                swc_id=potential_issue.swc_id,
+                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                severity=potential_issue.severity,
+                description_head=potential_issue.description_head,
+                description_tail=potential_issue.description_tail,
+                transaction_sequence=transaction_sequence,
+            )
+        )

mythril/analysis/report.py

@@ -238,7 +238,7 @@ class Report:
             return {}
         logs = []  # type: List[Dict]
         for exception in self.exceptions:
-            logs += [{"level": "error", "hidden": "true", "msg": exception}]
+            logs += [{"level": "error", "hidden": True, "msg": exception}]
         return {"logs": logs}
 
     def as_swc_standard_format(self):

mythril/analysis/security.py

@@ -6,22 +6,28 @@ from mythril.analysis import modules
 import pkgutil
 import importlib.util
 import logging
+import os
+import sys
 
 log = logging.getLogger(__name__)
 
 OPCODE_LIST = [c[0] for _, c in opcodes.items()]
 
 
-def reset_callback_modules():
+def reset_callback_modules(module_names=(), custom_modules_directory=""):
     """Clean the issue records of every callback-based module."""
-    modules = get_detection_modules("callback")
+    modules = get_detection_modules("callback", module_names, custom_modules_directory)
     for module in modules:
         module.detector.reset_module()
 
 
-def get_detection_module_hooks(modules, hook_type="pre"):
+def get_detection_module_hooks(modules, hook_type="pre", custom_modules_directory=""):
     hook_dict = defaultdict(list)
-    _modules = get_detection_modules(entrypoint="callback", include_modules=modules)
+    _modules = get_detection_modules(
+        entrypoint="callback",
+        include_modules=modules,
+        custom_modules_directory=custom_modules_directory,
+    )
     for module in _modules:
         hooks = (
             module.detector.pre_hooks
@@ -45,14 +51,13 @@ def get_detection_module_hooks(modules, hook_type="pre"):
     return dict(hook_dict)
 
 
-def get_detection_modules(entrypoint, include_modules=()):
+def get_detection_modules(entrypoint, include_modules=(), custom_modules_directory=""):
     """
 
     :param entrypoint:
     :param include_modules:
     :return:
     """
-
     module = importlib.import_module("mythril.analysis.modules.base")
     module.log.setLevel(log.level)
 
@@ -60,27 +65,35 @@ def get_detection_modules(entrypoint, include_modules=()):
 
     _modules = []
 
-    if not include_modules:
     for loader, module_name, _ in pkgutil.walk_packages(modules.__path__):
+        if include_modules and module_name not in include_modules:
+            continue
+
         if module_name != "base":
-                module = importlib.import_module(
-                    "mythril.analysis.modules." + module_name
-                )
+            module = importlib.import_module("mythril.analysis.modules." + module_name)
             module.log.setLevel(log.level)
             if module.detector.entrypoint == entrypoint:
                 _modules.append(module)
-    else:
-        for module_name in include_modules:
-            module = importlib.import_module("mythril.analysis.modules." + module_name)
-            if module.__name__ != "base" and module.detector.entrypoint == entrypoint:
+    if custom_modules_directory:
+        custom_modules_path = os.path.abspath(custom_modules_directory)
+        if custom_modules_path not in sys.path:
+            sys.path.append(custom_modules_path)
+
+        for loader, module_name, _ in pkgutil.walk_packages([custom_modules_path]):
+            if include_modules and module_name not in include_modules:
+                continue
+
+            if module_name != "base":
+                module = importlib.import_module(module_name, custom_modules_path)
                 module.log.setLevel(log.level)
+                if module.detector.entrypoint == entrypoint:
                     _modules.append(module)
 
     log.info("Found %s detection modules", len(_modules))
     return _modules
 
 
-def fire_lasers(statespace, module_names=()):
+def fire_lasers(statespace, module_names=(), custom_modules_directory=""):
     """
 
     :param statespace:
@@ -91,22 +104,28 @@ def fire_lasers(statespace, module_names=()):
 
     issues = []
     for module in get_detection_modules(
-        entrypoint="post", include_modules=module_names
+        entrypoint="post",
+        include_modules=module_names,
+        custom_modules_directory=custom_modules_directory,
     ):
         log.info("Executing " + module.detector.name)
         issues += module.detector.execute(statespace)
 
-    issues += retrieve_callback_issues(module_names)
+    issues += retrieve_callback_issues(module_names, custom_modules_directory)
     return issues
 
 
-def retrieve_callback_issues(module_names=()):
+def retrieve_callback_issues(module_names=(), custom_modules_directory=""):
     issues = []
     for module in get_detection_modules(
-        entrypoint="callback", include_modules=module_names
+        entrypoint="callback",
+        include_modules=module_names,
+        custom_modules_directory=custom_modules_directory,
     ):
         log.debug("Retrieving results for " + module.detector.name)
         issues += module.detector.issues
 
-    reset_callback_modules()
+    reset_callback_modules(
+        module_names=module_names, custom_modules_directory=custom_modules_directory
+    )
     return issues

mythril/analysis/solver.py

@@ -4,6 +4,7 @@ from typing import Dict, Tuple, Union
 from z3 import sat, unknown, FuncInterp
 import z3
 
+from mythril.analysis.analysis_args import analysis_args
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.ethereum.transaction import BaseTransaction
@@ -29,7 +30,7 @@ def get_model(constraints, minimize=(), maximize=(), enforce_execution_time=True
     :return:
     """
     s = Optimize()
-    timeout = 100000
+    timeout = analysis_args.solver_timeout
     if enforce_execution_time:
         timeout = min(timeout, time_handler.time_remaining() - 500)
         if timeout <= 0:
@@ -94,7 +95,7 @@ def get_transaction_sequence(
     concrete_transactions = []
 
     tx_constraints, minimize = _set_minimisation_constraints(
-        transaction_sequence, constraints.copy(), [], 5000
+        transaction_sequence, constraints.copy(), [], 5000, global_state.world_state
     )
 
     try:
@@ -102,19 +103,23 @@ def get_transaction_sequence(
     except UnsatError:
         raise UnsatError
 
-    min_price_dict = {}  # type: Dict[str, int]
+    # Include creation account in initial state
+    # Note: This contains the code, which should not exist until after the first tx
+    initial_world_state = transaction_sequence[0].world_state
+    initial_accounts = initial_world_state.accounts
+
     for transaction in transaction_sequence:
         concrete_transaction = _get_concrete_transaction(model, transaction)
         concrete_transactions.append(concrete_transaction)
 
-        caller = concrete_transaction["origin"]
-        value = int(concrete_transaction["value"], 16)
-        min_price_dict[caller] = min_price_dict.get(caller, 0) + value
-
-    if isinstance(transaction_sequence[0], ContractCreationTransaction):
-        initial_accounts = transaction_sequence[0].prev_world_state.accounts
-    else:
-        initial_accounts = transaction_sequence[0].world_state.accounts
+    min_price_dict = {}  # type: Dict[str, int]
+    for address in initial_accounts.keys():
+        min_price_dict[address] = model.eval(
+            initial_world_state.starting_balances[
+                symbol_factory.BitVecVal(address, 256)
+            ].raw,
+            model_completion=True,
+        ).as_long()
 
     concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict)
 
@@ -132,7 +137,7 @@ def _get_concrete_state(initial_accounts: Dict, min_price_dict: Dict[str, int]):
         data = dict()  # type: Dict[str, Union[int, str]]
         data["nonce"] = account.nonce
         data["code"] = account.code.bytecode
-        data["storage"] = account.storage.printable_storage
+        data["storage"] = str(account.storage)
         data["balance"] = hex(min_price_dict.get(address, 0))
         accounts[hex(address)] = data
     return {"accounts": accounts}
@@ -147,11 +152,12 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
         "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long()
     ).zfill(40)
 
+    input_ = ""
     if isinstance(transaction, ContractCreationTransaction):
         address = ""
-        input_ = transaction.code.bytecode
-    else:
-        input_ = "".join(
+        input_ += transaction.code.bytecode
+
+    input_ += "".join(
         [
             hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:]
             for b in transaction.call_data.concrete(model)
@@ -170,7 +176,7 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
 
 
 def _set_minimisation_constraints(
-    transaction_sequence, constraints, minimize, max_size
+    transaction_sequence, constraints, minimize, max_size, world_state
 ) -> Tuple[Constraints, tuple]:
     """ Set constraints that minimise key transaction values
 
@@ -192,5 +198,21 @@ def _set_minimisation_constraints(
         # Minimize
         minimize.append(transaction.call_data.calldatasize)
         minimize.append(transaction.call_value)
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(1000000000000000000000, 256),
+                world_state.starting_balances[transaction.caller],
+            )
+        )
+
+    for account in world_state.accounts.values():
+        # Lazy way to prevent overflows and to ensure "reasonable" balances
+        # Each account starts with less than 100 ETH
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(100000000000000000000, 256),
+                world_state.starting_balances[account.address],
+            )
+        )
 
     return constraints, tuple(minimize)

mythril/analysis/symbolic.py

@@ -14,6 +14,7 @@ from mythril.laser.ethereum.strategy.basic import (
     BasicSearchStrategy,
 )
 
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 from mythril.laser.ethereum.transaction.symbolic import (
     ATTACKER_ADDRESS,
     CREATOR_ADDRESS,
@@ -47,7 +48,7 @@ class SymExecWrapper:
         dynloader=None,
         max_depth=22,
         execution_timeout=None,
-        loop_bound=2,
+        loop_bound=3,
         create_timeout=None,
         transaction_count=2,
         modules=(),
@@ -55,6 +56,8 @@ class SymExecWrapper:
         enable_iprof=False,
         disable_dependency_pruning=False,
         run_analysis_modules=True,
+        enable_coverage_strategy=False,
+        custom_modules_directory="",
     ):
         """
 
@@ -92,7 +95,8 @@ class SymExecWrapper:
         )
 
         requires_statespace = (
-            compulsory_statespace or len(get_detection_modules("post", modules)) > 0
+            compulsory_statespace
+            or len(get_detection_modules("post", modules, custom_modules_directory)) > 0
         )
         if not contract.creation_code:
             self.accounts = {hex(ATTACKER_ADDRESS): attacker_account}
@@ -102,6 +106,8 @@ class SymExecWrapper:
                 hex(ATTACKER_ADDRESS): attacker_account,
             }
 
+        instruction_laser_plugin = PluginFactory.build_instruction_coverage_plugin()
+
         self.laser = svm.LaserEVM(
             dynamic_loader=dynloader,
             max_depth=max_depth,
@@ -111,6 +117,8 @@ class SymExecWrapper:
             transaction_count=transaction_count,
             requires_statespace=requires_statespace,
             enable_iprof=enable_iprof,
+            enable_coverage_strategy=enable_coverage_strategy,
+            instruction_laser_plugin=instruction_laser_plugin,
         )
 
         if loop_bound is not None:
@@ -118,7 +126,7 @@ class SymExecWrapper:
 
         plugin_loader = LaserPluginLoader(self.laser)
         plugin_loader.load(PluginFactory.build_mutation_pruner_plugin())
-        plugin_loader.load(PluginFactory.build_instruction_coverage_plugin())
+        plugin_loader.load(instruction_laser_plugin)
 
         if not disable_dependency_pruning:
             plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())
@@ -130,11 +138,19 @@ class SymExecWrapper:
         if run_analysis_modules:
             self.laser.register_hooks(
                 hook_type="pre",
-                hook_dict=get_detection_module_hooks(modules, hook_type="pre"),
+                hook_dict=get_detection_module_hooks(
+                    modules,
+                    hook_type="pre",
+                    custom_modules_directory=custom_modules_directory,
+                ),
             )
             self.laser.register_hooks(
                 hook_type="post",
-                hook_dict=get_detection_module_hooks(modules, hook_type="post"),
+                hook_dict=get_detection_module_hooks(
+                    modules,
+                    hook_type="post",
+                    custom_modules_directory=custom_modules_directory,
+                ),
             )
 
         if isinstance(contract, SolidityContract):
@@ -197,7 +213,10 @@ class SymExecWrapper:
                             get_variable(stack[-7]),
                         )
 
-                        if to.type == VarType.CONCRETE and to.val < 5:
+                        if (
+                            to.type == VarType.CONCRETE
+                            and 0 < to.val <= PRECOMPILE_COUNT
+                        ):
                             # ignore prebuilts
                             continue
 

mythril/analysis/templates/report_as_markdown.jinja2

@@ -6,15 +6,21 @@
 - SWC ID: {{ issue['swc-id'] }}
 - Severity: {{ issue.severity }}
 - Contract: {{ issue.contract | default("Unknown") }}
+{% if issue.function %}
 - Function name: `{{ issue.function }}`
+{% endif %}
 - PC address: {{ issue.address }}
+{% if issue.min_gas_used or issue.max_gas_used %}
 - Estimated Gas Usage: {{ issue.min_gas_used }} - {{ issue.max_gas_used }}
+{% endif %}
 
 ### Description
 
 {{ issue.description.rstrip() }}
 {% if issue.filename and issue.lineno %}
 In file: {{ issue.filename }}:{{ issue.lineno }}
+{% elif issue.filename %}
+In file: {{ issue.filename }}
 {% endif %}
 {% if issue.code %}
 
@@ -26,11 +32,17 @@ 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 %}
 {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
-Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
+Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }}
 {% else %}
 Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }}
 {% endif %}

mythril/analysis/templates/report_as_text.jinja2

@@ -4,9 +4,13 @@
 SWC ID: {{ issue['swc-id'] }}
 Severity: {{ issue.severity }}
 Contract: {{ issue.contract | default("Unknown") }}
+{% if issue.function %}
 Function name: {{ issue.function }}
+{% endif %}
 PC address: {{ issue.address }}
+{% if issue.min_gas_used or issue.max_gas_used %}
 Estimated Gas Usage: {{ issue.min_gas_used }} - {{ issue.max_gas_used }}
+{% endif %}
 {{ issue.description }}
 --------------------
 {% if issue.filename and issue.lineno %}
@@ -19,11 +23,17 @@ 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 %}
 {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
-Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
+Caller: [CREATOR], data: {{ step.input }}, value: {{ step.value }}
 {% else %}
 Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, function: {{ step.name }}, txdata: {{ step.input }}, value: {{ step.value }}
 {% endif %}

mythril/ethereum/util.py

@@ -3,6 +3,7 @@ solc integration."""
 import binascii
 import json
 import os
+import solcx
 from pathlib import Path
 from subprocess import PIPE, Popen
 
@@ -24,39 +25,44 @@ def safe_decode(hex_encoded_string):
         return bytes.fromhex(hex_encoded_string)
 
 
-def get_solc_json(file, solc_binary="solc", solc_args=None):
+def get_solc_json(file, solc_binary="solc", solc_settings_json=None):
     """
 
     :param file:
     :param solc_binary:
-    :param solc_args:
+    :param solc_settings_json:
     :return:
     """
-
-    cmd = [solc_binary, "--combined-json", "bin,bin-runtime,srcmap,srcmap-runtime,ast"]
-
-    if solc_args:
-        cmd.extend(solc_args.split())
-    if not "--allow-paths" in cmd:
-        cmd.extend(["--allow-paths", "."])
-    else:
-        for i, arg in enumerate(cmd):
-            if arg == "--allow-paths":
-                cmd[i + 1] += ",."
-
-    cmd.append(file)
+    cmd = [solc_binary, "--standard-json", "--allow-paths", "."]
+
+    settings = json.loads(solc_settings_json) if solc_settings_json else {}
+    settings.update(
+        {
+            "outputSelection": {
+                "*": {
+                    "": ["ast"],
+                    "*": [
+                        "metadata",
+                        "evm.bytecode",
+                        "evm.deployedBytecode",
+                        "evm.methodIdentifiers",
+                    ],
+                }
+            }
+        }
+    )
+    input_json = json.dumps(
+        {
+            "language": "Solidity",
+            "sources": {file: {"urls": [file]}},
+            "settings": settings,
+        }
+    )
 
     try:
-        p = Popen(cmd, stdout=PIPE, stderr=PIPE)
+        p = Popen(cmd, stdin=PIPE, stdout=PIPE, stderr=PIPE)
+        stdout, stderr = p.communicate(bytes(input_json, "utf8"))
 
-        stdout, stderr = p.communicate()
-        ret = p.returncode
-
-        if ret != 0:
-            raise CompilerError(
-                "Solc experienced a fatal error (code %d).\n\n%s"
-                % (ret, stderr.decode("UTF-8"))
-            )
     except FileNotFoundError:
         raise CompilerError(
             "Compiler not found. Make sure that solc is installed and in PATH, or set the SOLC environment variable."
@@ -64,10 +70,15 @@ def get_solc_json(file, solc_binary="solc", solc_args=None):
 
     out = stdout.decode("UTF-8")
 
-    if not len(out):
-        raise CompilerError("Compilation failed.")
+    result = json.loads(out)
+
+    for error in result.get("errors", []):
+        if error["severity"] == "error":
+            raise CompilerError(
+                "Solc experienced a fatal error.\n\n%s" % error["formattedMessage"]
+            )
 
-    return json.loads(out)
+    return result
 
 
 def encode_calldata(func_name, arg_types, args):
@@ -107,6 +118,9 @@ def solc_exists(version):
     :param version:
     :return:
     """
+
+    solc_binaries = []
+    if version.startswith("0.4"):
         solc_binaries = [
             os.path.join(
                 os.environ.get("HOME", str(Path.home())),
@@ -114,9 +128,15 @@ def solc_exists(version):
                 "bin/solc",
             )  # py-solc setup
         ]
-    if version.startswith("0.5"):
-        # Temporary fix to support v0.5.x with Ubuntu PPA setup
-        solc_binaries.append("/usr/bin/solc")
+    else:
+        # we are using solc-x for the the 0.5 and higher
+        solc_binaries = [os.path.join(solcx.__path__[0], "bin", "solc-v" + version)]
+
     for solc_path in solc_binaries:
         if os.path.exists(solc_path):
             return solc_path
+
+    # Last resort is to use the system installation
+    default_binary = "/usr/bin/solc"
+    if os.path.exists(default_binary):
+        return default_binary

mythril/interfaces/cli.py

@@ -15,7 +15,8 @@ import coloredlogs
 import traceback
 
 import mythril.support.signatures as sigs
-from argparse import ArgumentParser, Namespace
+from argparse import ArgumentParser, Namespace, RawTextHelpFormatter
+from mythril import mythx
 from mythril.exceptions import AddressNotFoundError, CriticalError
 from mythril.mythril import (
     MythrilAnalyzer,
@@ -27,12 +28,14 @@ from mythril.__version__ import __version__ as VERSION
 
 ANALYZE_LIST = ("analyze", "a")
 DISASSEMBLE_LIST = ("disassemble", "d")
+PRO_LIST = ("pro", "p")
 
 log = logging.getLogger(__name__)
 
 COMMAND_LIST = (
     ANALYZE_LIST
     + DISASSEMBLE_LIST
+    + PRO_LIST
     + (
         "read-storage",
         "leveldb-search",
@@ -41,6 +44,7 @@ COMMAND_LIST = (
         "version",
         "truffle",
         "help",
+        "pro",
     )
 )
 
@@ -63,16 +67,34 @@ def exit_with_error(format_, message):
                 "sourceType": "",
                 "sourceFormat": "",
                 "sourceList": [],
-                "meta": {
-                    "logs": [{"level": "error", "hidden": "true", "msg": message}]
-                },
+                "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]},
             }
         ]
         print(json.dumps(result))
     sys.exit()
 
 
-def get_input_parser() -> ArgumentParser:
+def get_runtime_input_parser() -> ArgumentParser:
+    """
+    Returns Parser which handles input
+    :return: Parser which handles input
+    """
+    parser = ArgumentParser(add_help=False)
+    parser.add_argument(
+        "-a",
+        "--address",
+        help="pull contract from the blockchain",
+        metavar="CONTRACT_ADDRESS",
+    )
+    parser.add_argument(
+        "--bin-runtime",
+        action="store_true",
+        help="Only when -c or -f is used. Consider the input bytecode as binary runtime code, default being the contract creation bytecode.",
+    )
+    return parser
+
+
+def get_creation_input_parser() -> ArgumentParser:
     """
     Returns Parser which handles input
     :return: Parser which handles input
@@ -91,17 +113,6 @@ def get_input_parser() -> ArgumentParser:
         metavar="BYTECODEFILE",
         type=argparse.FileType("r"),
     )
-    parser.add_argument(
-        "-a",
-        "--address",
-        help="pull contract from the blockchain",
-        metavar="CONTRACT_ADDRESS",
-    )
-    parser.add_argument(
-        "--bin-runtime",
-        action="store_true",
-        help="Only when -c or -f is used. Consider the input bytecode as binary runtime code, default being the contract creation bytecode.",
-    )
     return parser
 
 
@@ -146,7 +157,10 @@ def get_utilities_parser() -> ArgumentParser:
     :return: Parser which handles utility flags
     """
     parser = argparse.ArgumentParser(add_help=False)
-    parser.add_argument("--solc-args", help="Extra arguments for solc")
+    parser.add_argument(
+        "--solc-json",
+        help="Json for the optional 'settings' parameter of solc's standard-json input",
+    )
     parser.add_argument(
         "--solv",
         help="specify solidity compiler version. If not present, will try to install it (Experimental)",
@@ -160,7 +174,8 @@ def main() -> None:
 
     rpc_parser = get_rpc_parser()
     utilities_parser = get_utilities_parser()
-    input_parser = get_input_parser()
+    runtime_input_parser = get_runtime_input_parser()
+    creation_input_parser = get_creation_input_parser()
     output_parser = get_output_parser()
     parser = argparse.ArgumentParser(
         description="Security analysis of Ethereum smart contracts"
@@ -174,8 +189,15 @@ def main() -> None:
     analyzer_parser = subparsers.add_parser(
         ANALYZE_LIST[0],
         help="Triggers the analysis of the smart contract",
-        parents=[rpc_parser, utilities_parser, input_parser, output_parser],
+        parents=[
+            rpc_parser,
+            utilities_parser,
+            creation_input_parser,
+            runtime_input_parser,
+            output_parser,
+        ],
         aliases=ANALYZE_LIST[1:],
+        formatter_class=RawTextHelpFormatter,
     )
     create_analyzer_parser(analyzer_parser)
 
@@ -183,10 +205,25 @@ def main() -> None:
         DISASSEMBLE_LIST[0],
         help="Disassembles the smart contract",
         aliases=DISASSEMBLE_LIST[1:],
-        parents=[rpc_parser, utilities_parser, input_parser],
+        parents=[
+            rpc_parser,
+            utilities_parser,
+            creation_input_parser,
+            runtime_input_parser,
+        ],
+        formatter_class=RawTextHelpFormatter,
     )
     create_disassemble_parser(disassemble_parser)
 
+    pro_parser = subparsers.add_parser(
+        PRO_LIST[0],
+        help="Analyzes input with the MythX API (https://mythx.io)",
+        aliases=PRO_LIST[1:],
+        parents=[utilities_parser, creation_input_parser, output_parser],
+        formatter_class=RawTextHelpFormatter,
+    )
+    create_pro_parser(pro_parser)
+
     read_storage_parser = subparsers.add_parser(
         "read-storage",
         help="Retrieves storage slots from a given address through rpc",
@@ -225,7 +262,32 @@ def create_disassemble_parser(parser: ArgumentParser):
     :param parser:
     :return:
     """
-    parser.add_argument("solidity_file", nargs="*")
+    # Using nargs=* would the implementation below for getting code for both disassemble and analyze
+    parser.add_argument(
+        "solidity_files",
+        nargs="*",
+        help="Inputs file name and contract name. Currently supports a single contract\n"
+        "usage: file1.sol:OptionalContractName",
+    )
+
+
+def create_pro_parser(parser: ArgumentParser):
+    """
+    Modify parser to handle mythx analysis
+    :param parser:
+    :return:
+    """
+    parser.add_argument(
+        "solidity_files",
+        nargs="*",
+        help="Inputs file name and contract name. \n"
+        "usage: file1.sol:OptionalContractName file2.sol file3.sol:OptionalContractName",
+    )
+    parser.add_argument(
+        "--full",
+        help="Run a full analysis. Default: quick analysis",
+        action="store_true",
+    )
 
 
 def create_read_storage_parser(read_storage_parser: ArgumentParser):
@@ -292,7 +354,12 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
     :param analyzer_parser:
     :return:
     """
-    analyzer_parser.add_argument("solidity_file", nargs="*")
+    analyzer_parser.add_argument(
+        "solidity_files",
+        nargs="*",
+        help="Inputs file name and contract name. \n"
+        "usage: file1.sol:OptionalContractName file2.sol file3.sol:OptionalContractName",
+    )
     commands = analyzer_parser.add_argument_group("commands")
     commands.add_argument("-g", "--graph", help="generate a control flow graph")
     commands.add_argument(
@@ -346,11 +413,17 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
         default=86400,
         help="The amount of seconds to spend on symbolic execution",
     )
+    options.add_argument(
+        "--solver-timeout",
+        type=int,
+        default=10000,
+        help="The maximum amount of time(in milli seconds) the solver spends for queries from analysis modules",
+    )
     options.add_argument(
         "--create-timeout",
         type=int,
         default=10,
-        help="The amount of seconds to spend on " "the initial contract creation",
+        help="The amount of seconds to spend on the initial contract creation",
     )
     options.add_argument(
         "-l",
@@ -360,8 +433,9 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
     )
     options.add_argument(
         "--no-onchain-storage-access",
+        "--no-onchain-access",
         action="store_true",
-        help="turns off getting the data from onchain contracts",
+        help="turns off getting the data from onchain contracts (both loading storage and contract code)",
     )
 
     options.add_argument(
@@ -384,6 +458,16 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
         action="store_true",
         help="Deactivate dependency-based pruning",
     )
+    options.add_argument(
+        "--enable-coverage-strategy",
+        action="store_true",
+        help="enable coverage based search strategy",
+    )
+    options.add_argument(
+        "--custom-modules-directory",
+        help="designates a separate directory to search for custom analysis modules",
+        metavar="CUSTOM_MODULES_DIRECTORY",
+    )
 
 
 def validate_args(args: Namespace):
@@ -410,6 +494,8 @@ def validate_args(args: Namespace):
             exit_with_error(
                 args.outform, "Invalid -v value, you can find valid values in usage"
             )
+    if args.command in DISASSEMBLE_LIST and len(args.solidity_files) > 1:
+        exit_with_error("text", "Only a single arg is supported for using disassemble")
 
     if args.command in ANALYZE_LIST:
         if args.query_signature and sigs.ethereum_input_decoder is None:
@@ -494,15 +580,15 @@ def load_code(disassembler: MythrilDisassembler, args: Namespace):
     elif args.__dict__.get("address", False):
         # Get bytecode from a contract address
         address, _ = disassembler.load_from_address(args.address)
-    elif args.__dict__.get("solidity_file", False):
+    elif args.__dict__.get("solidity_files", False):
         # Compile Solidity source file(s)
-        if args.command in ANALYZE_LIST and args.graph and len(args.solidity_file) > 1:
+        if args.command in ANALYZE_LIST and args.graph and len(args.solidity_files) > 1:
             exit_with_error(
                 args.outform,
                 "Cannot generate call graphs from multiple input files. Please do it one at a time.",
             )
         address, _ = disassembler.load_from_solidity(
-            args.solidity_file
+            args.solidity_files
         )  # list of files
     else:
         exit_with_error(
@@ -534,6 +620,17 @@ def execute_command(
         )
         print(storage)
 
+    elif args.command in PRO_LIST:
+        mode = "full" if args.full else "quick"
+        report = mythx.analyze(disassembler.contracts, mode)
+        outputs = {
+            "json": report.as_json(),
+            "jsonv2": report.as_swc_standard_format(),
+            "text": report.as_text(),
+            "markdown": report.as_markdown(),
+        }
+        print(outputs[args.outform])
+
     elif args.command in DISASSEMBLE_LIST:
         if disassembler.contracts[0].code:
             print("Runtime Disassembly: \n" + disassembler.contracts[0].get_easm())
@@ -552,6 +649,12 @@ def execute_command(
             enable_iprof=args.enable_iprof,
             disable_dependency_pruning=args.disable_dependency_pruning,
             onchain_storage_access=not args.no_onchain_storage_access,
+            solver_timeout=args.solver_timeout,
+            requires_dynld=not args.no_onchain_storage_access,
+            enable_coverage_strategy=args.enable_coverage_strategy,
+            custom_modules_directory=args.custom_modules_directory
+            if args.custom_modules_directory
+            else "",
         )
 
         if not disassembler.contracts:
@@ -658,12 +761,12 @@ def parse_args_and_execute(parser: ArgumentParser, args: Namespace) -> None:
         config = set_config(args)
         leveldb_search(config, args)
         query_signature = args.__dict__.get("query_signature", None)
-        solc_args = args.__dict__.get("solc_args", None)
+        solc_json = args.__dict__.get("solc_json", None)
         solv = args.__dict__.get("solv", None)
         disassembler = MythrilDisassembler(
             eth=config.eth,
             solc_version=solv,
-            solc_args=solc_args,
+            solc_settings_json=solc_json,
             enable_online_lookup=query_signature,
         )
         if args.command == "truffle":

mythril/interfaces/old_cli.py

@@ -44,9 +44,7 @@ def exit_with_error(format_, message):
                 "sourceType": "",
                 "sourceFormat": "",
                 "sourceList": [],
-                "meta": {
-                    "logs": [{"level": "error", "hidden": "true", "msg": message}]
-                },
+                "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]},
             }
         ]
         print(json.dumps(result))
@@ -213,6 +211,12 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
         default=2,
         help="Maximum number of transactions issued by laser",
     )
+    options.add_argument(
+        "--solver-timeout",
+        type=int,
+        default=10000,
+        help="The maximum amount of time(in milli seconds) the solver spends for queries from analysis modules",
+    )
     options.add_argument(
         "--execution-timeout",
         type=int,
@@ -225,7 +229,10 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
         default=10,
         help="The amount of seconds to spend on " "the initial contract creation",
     )
-    options.add_argument("--solc-args", help="Extra arguments for solc")
+    options.add_argument(
+        "--solc-json",
+        help="Json for the optional 'settings' parameter of solc's standard-json input",
+    )
     options.add_argument(
         "--phrack", action="store_true", help="Phrack-style call graph"
     )
@@ -419,6 +426,7 @@ def execute_command(
         enable_iprof=args.enable_iprof,
         disable_dependency_pruning=args.disable_dependency_pruning,
         onchain_storage_access=not args.no_onchain_storage_access,
+        solver_timeout=args.solver_timeout,
     )
 
     if args.disassemble:
@@ -517,7 +525,7 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non
         disassembler = MythrilDisassembler(
             eth=config.eth,
             solc_version=args.solv,
-            solc_args=args.solc_args,
+            solc_settings_json=args.solc_json,
             enable_online_lookup=args.query_signature,
         )
         if args.truffle:

mythril/laser/ethereum/call.py

@@ -4,19 +4,20 @@ 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
 from mythril.laser.ethereum.gas import OPCODE_GAS
 from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.natives import PRECOMPILE_COUNT
 from mythril.laser.ethereum.state.calldata import (
     BaseCalldata,
     SymbolicCalldata,
     ConcreteCalldata,
 )
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import BitVec
+from mythril.laser.smt import BitVec, is_true
 from mythril.laser.smt import simplify, Expression, symbol_factory
 from mythril.support.loader import DynLoader
 
@@ -49,7 +50,11 @@ def get_call_parameters(
 
     callee_account = None
     call_data = get_call_data(global_state, memory_input_offset, memory_input_size)
-    if int(callee_address, 16) >= 5 or int(callee_address, 16) == 0:
+    if (
+        isinstance(callee_address, BitVec)
+        or int(callee_address, 16) > PRECOMPILE_COUNT
+        or int(callee_address, 16) == 0
+    ):
         callee_account = get_callee_account(
             global_state, callee_address, dynamic_loader
         )
@@ -84,11 +89,11 @@ def get_callee_address(
     except TypeError:
         log.debug("Symbolic call encountered")
 
-        match = re.search(r"storage_(\d+)", str(simplify(symbolic_to_address)))
+        match = re.search(r"Storage\[(\d+)\]", str(simplify(symbolic_to_address)))
         log.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
         if match is None or dynamic_loader is None:
-            raise ValueError()
+            return symbolic_to_address
 
         index = int(match.group(1))
         log.debug("Dynamic contract address at storage index {}".format(index))
@@ -100,8 +105,7 @@ def get_callee_address(
             )
         # TODO: verify whether this happens or not
         except:
-            log.debug("Error accessing contract storage.")
-            raise ValueError
+            return symbolic_to_address
 
         # testrpc simply returns the address, geth response is more elaborate.
         if not re.match(r"^0x[0-9a-f]{40}$", callee_address):
@@ -111,7 +115,9 @@ def get_callee_address(
 
 
 def get_callee_account(
-    global_state: GlobalState, callee_address: str, dynamic_loader: DynLoader
+    global_state: GlobalState,
+    callee_address: Union[str, BitVec],
+    dynamic_loader: DynLoader,
 ):
     """Gets the callees account from the global_state.
 
@@ -120,28 +126,31 @@ 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):
+        if callee_address.symbolic:
+            return Account(callee_address, balances=global_state.world_state.balances)
+        else:
+            callee_address = hex(callee_address.value)[2:]
 
     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(
@@ -151,7 +160,7 @@ def get_callee_account(
         dynamic_loader=dynamic_loader,
         balances=global_state.world_state.balances,
     )
-    accounts[callee_address] = callee_account
+    global_state.accounts[int(callee_address, 16)] = callee_account
 
     return callee_account
 
@@ -189,10 +198,10 @@ def get_call_data(
     )
 
     uses_entire_calldata = simplify(
-        memory_size - global_state.environment.calldata.calldatasize == 0
+        memory_size == global_state.environment.calldata.calldatasize
     )
 
-    if uses_entire_calldata is True:
+    if is_true(uses_entire_calldata):
         return global_state.environment.calldata
 
     try:
@@ -203,18 +212,24 @@ def get_call_data(
         ]
         return ConcreteCalldata(transaction_id, calldata_from_mem)
     except TypeError:
-        log.debug("Unsupported symbolic calldata offset")
+        log.debug(
+            "Unsupported symbolic calldata offset %s size %s", memory_start, memory_size
+        )
         return SymbolicCalldata(transaction_id)
 
 
 def native_call(
     global_state: GlobalState,
-    callee_address: str,
+    callee_address: Union[str, BitVec],
     call_data: BaseCalldata,
     memory_out_offset: Union[int, Expression],
     memory_out_size: Union[int, Expression],
-) -> Union[List[GlobalState], None]:
-    if not 0 < int(callee_address, 16) < 5:
+) -> Optional[List[GlobalState]]:
+
+    if (
+        isinstance(callee_address, BitVec)
+        or not 0 < int(callee_address, 16) <= PRECOMPILE_COUNT
+    ):
         return None
 
     log.debug("Native contract called: " + callee_address)

mythril/laser/ethereum/evm_exceptions.py

@@ -35,3 +35,9 @@ class OutOfGasException(VmException):
     """A VM exception denoting the current execution has run out of gas."""
 
     pass
+
+
+class WriteProtection(VmException):
+    """A VM exception denoting that a write operation is executed on a write protected environment"""
+
+    pass

mythril/laser/ethereum/gas.py

@@ -180,10 +180,7 @@ OPCODE_GAS = {
     "LOG3": (4 * 375, 4 * 375 + 8 * 32),
     "LOG4": (5 * 375, 5 * 375 + 8 * 32),
     "CREATE": (32000, 32000),
-    "CREATE2": (
-        32000,
-        32000,
-    ),  # TODO: The gas value is dynamic, to be done while implementing create2
+    "CREATE2": (32000, 32000),  # TODO: Make the gas values dynamic
     "CALL": (700, 700 + 9000 + 25000),
     "NATIVE_COST": calculate_native_gas,
     "CALLCODE": (700, 700 + 9000 + 25000),

mythril/laser/ethereum/instructions.py

@@ -6,7 +6,6 @@ import logging
 from copy import copy, deepcopy
 from typing import cast, Callable, List, Set, Union, Tuple, Any
 from datetime import datetime
-from math import ceil
 from ethereum import utils
 
 from mythril.laser.smt import (
@@ -25,18 +24,24 @@ from mythril.laser.smt import (
     Bool,
     Not,
     LShR,
+    UGE,
 )
 from mythril.laser.smt import symbol_factory
 
+from mythril.disassembler.disassembly import Disassembly
+
+from mythril.laser.ethereum.state.calldata import ConcreteCalldata, SymbolicCalldata
+
 import mythril.laser.ethereum.util as helper
 from mythril.laser.ethereum import util
-from mythril.laser.ethereum.call import get_call_parameters, native_call
+from mythril.laser.ethereum.call import get_call_parameters, native_call, get_call_data
 from mythril.laser.ethereum.evm_exceptions import (
     VmException,
     StackUnderflowException,
     InvalidJumpDestination,
     InvalidInstruction,
     OutOfGasException,
+    WriteProtection,
 )
 from mythril.laser.ethereum.gas import OPCODE_GAS
 from mythril.laser.ethereum.state.global_state import GlobalState
@@ -44,8 +49,11 @@ from mythril.laser.ethereum.transaction import (
     MessageCallTransaction,
     TransactionStartSignal,
     ContractCreationTransaction,
+    get_next_transaction_id,
 )
 
+from mythril.support.support_utils import get_code_hash
+
 from mythril.support.loader import DynLoader
 
 log = logging.getLogger(__name__)
@@ -54,6 +62,30 @@ TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
 
 
+def transfer_ether(
+    global_state: GlobalState,
+    sender: BitVec,
+    receiver: BitVec,
+    value: Union[int, BitVec],
+):
+    """
+    Perform an Ether transfer between two accounts
+
+    :param global_state: The global state in which the Ether transfer occurs
+    :param sender: The sender of the Ether
+    :param receiver: The recipient of the Ether
+    :param value: The amount of Ether to send
+    :return:
+    """
+    value = value if isinstance(value, BitVec) else symbol_factory.BitVecVal(value, 256)
+
+    global_state.mstate.constraints.append(
+        UGE(global_state.world_state.balances[sender], value)
+    )
+    global_state.world_state.balances[receiver] += value
+    global_state.world_state.balances[sender] -= value
+
+
 class StateTransition(object):
     """Decorator that handles global state copy and original return.
 
@@ -63,14 +95,18 @@ class StateTransition(object):
     if `increment_pc=True`.
     """
 
-    def __init__(self, increment_pc=True, enable_gas=True):
+    def __init__(
+        self, increment_pc=True, enable_gas=True, is_state_mutation_instruction=False
+    ):
         """
 
         :param increment_pc:
         :param enable_gas:
+        :param is_state_mutation_instruction: The function mutates state
         """
         self.increment_pc = increment_pc
         self.enable_gas = enable_gas
+        self.is_state_mutation_instruction = is_state_mutation_instruction
 
     @staticmethod
     def call_on_state_copy(func: Callable, func_obj: "Instruction", state: GlobalState):
@@ -140,6 +176,13 @@ class StateTransition(object):
             :param global_state:
             :return:
             """
+            if self.is_state_mutation_instruction and global_state.environment.static:
+                raise WriteProtection(
+                    "The function {} cannot be executed in a static call".format(
+                        func.__name__[:-1]
+                    )
+                )
+
             new_global_states = self.call_on_state_copy(func, func_obj, global_state)
             new_global_states = [
                 self.accumulate_gas(state) for state in new_global_states
@@ -172,7 +215,8 @@ 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"
@@ -732,51 +776,45 @@ class Instruction:
         """
         state = global_state.mstate
         environment = global_state.environment
+
+        if isinstance(global_state.current_transaction, ContractCreationTransaction):
+            log.debug("Attempt to use CALLDATASIZE in creation transaction")
+            state.stack.append(0)
+        else:
             state.stack.append(environment.calldata.calldatasize)
-        return [global_state]
 
-    @StateTransition()
-    def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]:
-        """
+        return [global_state]
 
-        :param global_state:
-        :return:
-        """
-        state = global_state.mstate
+    @staticmethod
+    def _calldata_copy_helper(global_state, mstate, mstart, dstart, size):
         environment = global_state.environment
-        op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop()
 
         try:
-            mstart = util.get_concrete_int(op0)
+            mstart = util.get_concrete_int(mstart)
         except TypeError:
             log.debug("Unsupported symbolic memory offset in CALLDATACOPY")
             return [global_state]
 
         try:
-            dstart = util.get_concrete_int(op1)  # type: Union[int, BitVec]
+            dstart = util.get_concrete_int(dstart)  # type: Union[int, BitVec]
         except TypeError:
             log.debug("Unsupported symbolic calldata offset in CALLDATACOPY")
-            dstart = simplify(op1)
+            dstart = simplify(dstart)
 
-        size_sym = False
         try:
-            size = util.get_concrete_int(op2)  # type: Union[int, BitVec]
+            size = util.get_concrete_int(size)  # type: Union[int, BitVec]
         except TypeError:
             log.debug("Unsupported symbolic size in CALLDATACOPY")
-            size = simplify(op2)
-            size_sym = True
-
-        if size_sym:
             size = 320  # The excess size will get overwritten
 
         size = cast(int, size)
         if size > 0:
             try:
-                state.mem_extend(mstart, size)
+                mstate.mem_extend(mstart, size)
             except TypeError as e:
                 log.debug("Memory allocation error: {}".format(e))
-                state.mem_extend(mstart, 1)
-                state.memory[mstart] = global_state.new_bitvec(
+                mstate.mem_extend(mstart, 1)
+                mstate.memory[mstart] = global_state.new_bitvec(
                     "calldata_"
                     + str(environment.active_account.contract_name)
                     + "["
@@ -801,12 +839,12 @@ class Instruction:
                         else simplify(cast(BitVec, i_data) + 1)
                     )
                 for i in range(len(new_memory)):
-                    state.memory[i + mstart] = new_memory[i]
+                    mstate.memory[i + mstart] = new_memory[i]
 
             except IndexError:
                 log.debug("Exception copying calldata to memory")
 
-                state.memory[mstart] = global_state.new_bitvec(
+                mstate.memory[mstart] = global_state.new_bitvec(
                     "calldata_"
                     + str(environment.active_account.contract_name)
                     + "["
@@ -818,6 +856,22 @@ class Instruction:
                 )
         return [global_state]
 
+    @StateTransition()
+    def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]:
+        """
+
+        :param global_state:
+        :return:
+        """
+        state = global_state.mstate
+        op0, op1, op2 = state.stack.pop(), state.stack.pop(), state.stack.pop()
+
+        if isinstance(global_state.current_transaction, ContractCreationTransaction):
+            log.debug("Attempt to use CALLDATACOPY in creation transaction")
+            return [global_state]
+
+        return self._calldata_copy_helper(global_state, state, op0, op1, op2)
+
     # Environment
     @StateTransition()
     def address_(self, global_state: GlobalState) -> List[GlobalState]:
@@ -840,7 +894,11 @@ class Instruction:
         """
         state = global_state.mstate
         address = state.stack.pop()
-        state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
+
+        balance = global_state.world_state.balances[
+            global_state.environment.active_account.address
+        ]
+        state.stack.append(balance)
         return [global_state]
 
     @StateTransition()
@@ -877,9 +935,31 @@ class Instruction:
         state = global_state.mstate
         environment = global_state.environment
         disassembly = environment.code
-        state.stack.append(len(disassembly.bytecode) // 2)
+        calldata = global_state.environment.calldata
+        if isinstance(global_state.current_transaction, ContractCreationTransaction):
+            # Hacky way to ensure constructor arguments work - Pick some reasonably large size.
+            no_of_bytes = len(disassembly.bytecode) // 2
+            if isinstance(calldata, ConcreteCalldata):
+                no_of_bytes += calldata.size
+            else:
+                no_of_bytes += 0x200  # space for 16 32-byte arguments
+                global_state.mstate.constraints.append(
+                    global_state.environment.calldata.size == no_of_bytes
+                )
+
+        else:
+            no_of_bytes = len(disassembly.bytecode) // 2
+        state.stack.append(no_of_bytes)
         return [global_state]
 
+    @staticmethod
+    def _sha3_gas_helper(global_state, length):
+        min_gas, max_gas = cast(Callable, OPCODE_GAS["SHA3_FUNC"])(length)
+        global_state.mstate.min_gas_used += min_gas
+        global_state.mstate.max_gas_used += max_gas
+        StateTransition.check_gas_usage_limit(global_state)
+        return global_state
+
     @StateTransition(enable_gas=False)
     def sha3_(self, global_state: GlobalState) -> List[GlobalState]:
         """
@@ -905,10 +985,7 @@ class Instruction:
             state.max_gas_used += gas_tuple[1]
             return [global_state]
 
-        min_gas, max_gas = cast(Callable, OPCODE_GAS["SHA3_FUNC"])(length)
-        state.min_gas_used += min_gas
-        state.max_gas_used += max_gas
-        StateTransition.check_gas_usage_limit(global_state)
+        Instruction._sha3_gas_helper(global_state, length)
 
         state.mem_extend(index, length)
         data_list = [
@@ -961,34 +1038,6 @@ class Instruction:
         global_state.mstate.stack.append(global_state.environment.gasprice)
         return [global_state]
 
-    @staticmethod
-    def _handle_symbolic_args(
-        global_state: GlobalState, concrete_memory_offset: int
-    ) -> None:
-        """
-        In contract creation transaction with dynamic arguments(like arrays, maps) solidity will try to
-        execute CODECOPY with code size as len(with_args) - len(without_args) which in our case
-        would be 0, hence we are writing 10 symbol words onto the memory on the assumption that
-        no one would use 10 array/map arguments for constructor.
-        :param global_state: The global state
-        :param concrete_memory_offset: The memory offset on which symbols should be written
-        """
-        no_of_words = ceil(
-            min(len(global_state.environment.code.bytecode) / 2, 320) / 32
-        )
-        global_state.mstate.mem_extend(concrete_memory_offset, 32 * no_of_words)
-        for i in range(no_of_words):
-            global_state.mstate.memory.write_word_at(
-                concrete_memory_offset + i * 32,
-                global_state.new_bitvec(
-                    "code_{}({})".format(
-                        concrete_memory_offset + i * 32,
-                        global_state.environment.active_account.contract_name,
-                    ),
-                    256,
-                ),
-            )
-
     @StateTransition()
     def codecopy_(self, global_state: GlobalState) -> List[GlobalState]:
         """
@@ -1001,6 +1050,63 @@ class Instruction:
             global_state.mstate.stack.pop(),
             global_state.mstate.stack.pop(),
         )
+        code = global_state.environment.code.bytecode
+        if code[0:2] == "0x":
+            code = code[2:]
+        code_size = len(code) // 2
+
+        if isinstance(global_state.current_transaction, ContractCreationTransaction):
+            # Treat creation code after the expected disassembly as calldata.
+            # This is a slightly hacky way to ensure that symbolic constructor
+            # arguments work correctly.
+            mstate = global_state.mstate
+            offset = code_offset - code_size
+            log.debug("Copying from code offset: {} with size: {}".format(offset, size))
+
+            if isinstance(global_state.environment.calldata, SymbolicCalldata):
+                if code_offset >= code_size:
+                    return self._calldata_copy_helper(
+                        global_state, mstate, memory_offset, offset, size
+                    )
+            else:
+                # Copy from both code and calldata appropriately.
+                concrete_code_offset = helper.get_concrete_int(code_offset)
+                concrete_size = helper.get_concrete_int(size)
+
+                code_copy_offset = concrete_code_offset
+                code_copy_size = (
+                    concrete_size
+                    if concrete_code_offset + concrete_size <= code_size
+                    else code_size - concrete_code_offset
+                )
+                code_copy_size = code_copy_size if code_copy_size >= 0 else 0
+
+                calldata_copy_offset = (
+                    concrete_code_offset - code_size
+                    if concrete_code_offset - code_size > 0
+                    else 0
+                )
+                calldata_copy_size = concrete_code_offset + concrete_size - code_size
+                calldata_copy_size = (
+                    calldata_copy_size if calldata_copy_size >= 0 else 0
+                )
+
+                [global_state] = self._code_copy_helper(
+                    code=global_state.environment.code.bytecode,
+                    memory_offset=memory_offset,
+                    code_offset=code_copy_offset,
+                    size=code_copy_size,
+                    op="CODECOPY",
+                    global_state=global_state,
+                )
+                return self._calldata_copy_helper(
+                    global_state=global_state,
+                    mstate=mstate,
+                    mstart=memory_offset + code_copy_size,
+                    dstart=calldata_copy_offset,
+                    size=calldata_copy_size,
+                )
+
         return self._code_copy_helper(
             code=global_state.environment.code.bytecode,
             memory_offset=memory_offset,
@@ -1041,9 +1147,9 @@ class Instruction:
     @staticmethod
     def _code_copy_helper(
         code: str,
-        memory_offset: BitVec,
-        code_offset: BitVec,
-        size: BitVec,
+        memory_offset: Union[int, BitVec],
+        code_offset: Union[int, BitVec],
+        size: Union[int, BitVec],
         op: str,
         global_state: GlobalState,
     ) -> List[GlobalState]:
@@ -1089,13 +1195,6 @@ class Instruction:
         if code[0:2] == "0x":
             code = code[2:]
 
-        if concrete_size == 0 and isinstance(
-            global_state.current_transaction, ContractCreationTransaction
-        ):
-            if concrete_code_offset >= len(code) // 2:
-                Instruction._handle_symbolic_args(global_state, concrete_memory_offset)
-                return [global_state]
-
         for i in range(concrete_size):
             if 2 * (concrete_code_offset + i + 1) <= len(code):
                 global_state.mstate.memory[concrete_memory_offset + i] = int(
@@ -1155,18 +1254,26 @@ class Instruction:
             global_state=global_state,
         )
 
-    @StateTransition
+    @StateTransition()
     def extcodehash_(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
         :param global_state:
         :return: List of global states possible, list of size 1 in this case
         """
-        # TODO: To be implemented
-        address = global_state.mstate.stack.pop()
-        global_state.mstate.stack.append(
-            global_state.new_bitvec("extcodehash_{}".format(str(address)), 256)
-        )
+        world_state = global_state.world_state
+        stack = global_state.mstate.stack
+        address = Extract(159, 0, stack.pop())
+
+        if address.symbolic:
+            code_hash = symbol_factory.BitVecVal(int(get_code_hash(""), 16), 256)
+        elif address.value not in world_state.accounts:
+            code_hash = symbol_factory.BitVecVal(0, 256)
+        else:
+            addr = "0" * (40 - len(hex(address.value)[2:])) + hex(address.value)[2:]
+            code = world_state.accounts_exist_or_load(addr, self.dynamic_loader)
+            code_hash = symbol_factory.BitVecVal(int(get_code_hash(code), 16), 256)
+        stack.append(code_hash)
         return [global_state]
 
     @StateTransition()
@@ -1368,11 +1475,10 @@ class Instruction:
 
         state = global_state.mstate
         index = state.stack.pop()
-
         state.stack.append(global_state.environment.active_account.storage[index])
         return [global_state]
 
-    @StateTransition()
+    @StateTransition(is_state_mutation_instruction=True)
     def sstore_(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
@@ -1381,7 +1487,6 @@ class Instruction:
         """
         state = global_state.mstate
         index, value = state.stack.pop(), state.stack.pop()
-
         global_state.environment.active_account.storage[index] = value
         return [global_state]
 
@@ -1540,7 +1645,7 @@ class Instruction:
         global_state.mstate.stack.append(global_state.new_bitvec("gas", 256))
         return [global_state]
 
-    @StateTransition()
+    @StateTransition(is_state_mutation_instruction=True)
     def log_(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
@@ -1555,37 +1660,112 @@ class Instruction:
         # Not supported
         return [global_state]
 
-    @StateTransition()
+    def _create_transaction_helper(
+        self, global_state, call_value, mem_offset, mem_size, create2_salt=None
+    ):
+        mstate = global_state.mstate
+        environment = global_state.environment
+        world_state = global_state.world_state
+
+        call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size)
+
+        code_raw = []
+        code_end = call_data.size
+        for i in range(call_data.size):
+            if call_data[i].symbolic:
+                code_end = i
+                break
+            code_raw.append(call_data[i].value)
+
+        code_str = bytes.hex(bytes(code_raw))
+
+        next_transaction_id = get_next_transaction_id()
+        constructor_arguments = ConcreteCalldata(
+            next_transaction_id, call_data[code_end:]
+        )
+        code = Disassembly(code_str)
+
+        caller = environment.active_account.address
+        gas_price = environment.gasprice
+        origin = environment.origin
+
+        contract_address = None
+        if create2_salt:
+            salt = hex(create2_salt)[2:]
+            salt = "0" * (64 - len(salt)) + salt
+
+            addr = hex(caller.value)[2:]
+            addr = "0" * (40 - len(addr)) + addr
+
+            Instruction._sha3_gas_helper(global_state, len(code_str[2:] // 2))
+
+            contract_address = int(
+                get_code_hash("0xff" + addr + salt + get_code_hash(code_str)[2:])[26:],
+                16,
+            )
+        transaction = ContractCreationTransaction(
+            world_state=world_state,
+            caller=caller,
+            code=code,
+            call_data=constructor_arguments,
+            gas_price=gas_price,
+            gas_limit=mstate.gas_limit,
+            origin=origin,
+            call_value=call_value,
+            contract_address=contract_address,
+        )
+        raise TransactionStartSignal(transaction, self.op_code, global_state)
+
+    @StateTransition(is_state_mutation_instruction=True)
     def create_(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
         :param global_state:
         :return:
         """
-        # TODO: implement me
-        state = global_state.mstate
-        state.stack.pop(), state.stack.pop(), state.stack.pop()
-        # Not supported
-        state.stack.append(0)
-        return [global_state]
+        call_value, mem_offset, mem_size = global_state.mstate.pop(3)
+
+        return self._create_transaction_helper(
+            global_state, call_value, mem_offset, mem_size
+        )
 
     @StateTransition()
+    def create_post(self, global_state: GlobalState) -> List[GlobalState]:
+        call_value, mem_offset, mem_size = global_state.mstate.pop(3)
+        call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size)
+        if global_state.last_return_data:
+            return_val = symbol_factory.BitVecVal(
+                int(global_state.last_return_data, 16), 256
+            )
+        else:
+            return_val = symbol_factory.BitVecVal(0, 256)
+        global_state.mstate.stack.append(return_val)
+        return [global_state]
+
+    @StateTransition(is_state_mutation_instruction=True)
     def create2_(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
         :param global_state:
         :return:
         """
-        # TODO: implement me
-        state = global_state.mstate
-        endowment, memory_start, memory_length, salt = (
-            state.stack.pop(),
-            state.stack.pop(),
-            state.stack.pop(),
-            state.stack.pop(),
+        call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4)
+
+        return self._create_transaction_helper(
+            global_state, call_value, mem_offset, mem_size, salt
         )
-        # Not supported
-        state.stack.append(0)
+
+    @StateTransition()
+    def create2_post(self, global_state: GlobalState) -> List[GlobalState]:
+        call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4)
+        call_data = get_call_data(global_state, mem_offset, mem_offset + mem_size)
+        if global_state.last_return_data:
+            return_val = symbol_factory.BitVecVal(
+                int(global_state.last_return_data), 256
+            )
+        else:
+            return_val = symbol_factory.BitVecVal(0, 256)
+        global_state.mstate.stack.append(return_val)
         return [global_state]
 
     @StateTransition()
@@ -1605,7 +1785,7 @@ class Instruction:
             return_data = state.memory[offset : offset + length]
         global_state.current_transaction.end(global_state, return_data)
 
-    @StateTransition()
+    @StateTransition(is_state_mutation_instruction=True)
     def suicide_(self, global_state: GlobalState):
         """
 
@@ -1615,7 +1795,7 @@ class Instruction:
         transfer_amount = global_state.environment.active_account.balance()
         # Often the target of the suicide instruction will be symbolic
         # If it isn't then we'll transfer the balance to the indicated contract
-        global_state.world_state[target].add_balance(transfer_amount)
+        global_state.world_state.balances[target] += transfer_amount
 
         global_state.environment.active_account = deepcopy(
             global_state.environment.active_account
@@ -1689,6 +1869,10 @@ class Instruction:
 
             if callee_account is not None and callee_account.code.bytecode == "":
                 log.debug("The call is related to ether transfer between accounts")
+                sender = environment.active_account.address
+                receiver = callee_account.address
+                transfer_ether(global_state, sender, receiver, value)
+
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
                 )
@@ -1706,6 +1890,21 @@ class Instruction:
             )
             return [global_state]
 
+        if environment.static:
+            if isinstance(value, int) and value > 0:
+                raise WriteProtection(
+                    "Cannot call with non zero value in a static call"
+                )
+            if isinstance(value, BitVec):
+                if value.symbolic:
+                    global_state.mstate.constraints.append(
+                        value == symbol_factory.BitVecVal(0, 256)
+                    )
+                elif value.value > 0:
+                    raise WriteProtection(
+                        "Cannot call with non zero value in a static call"
+                    )
+
         native_result = native_call(
             global_state, callee_address, call_data, memory_out_offset, memory_out_size
         )
@@ -1720,20 +1919,81 @@ class Instruction:
             callee_account=callee_account,
             call_data=call_data,
             call_value=value,
+            static=environment.static,
         )
-        raise TransactionStartSignal(transaction, self.op_code)
+        raise TransactionStartSignal(transaction, self.op_code, global_state)
 
     @StateTransition()
     def call_post(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
+        :param global_state:
+        :return:
+        """
+
+        return self.post_handler(global_state, function_name="call")
+
+    @StateTransition()
+    def callcode_(self, global_state: GlobalState) -> List[GlobalState]:
+        """
+
         :param global_state:
         :return:
         """
         instr = global_state.get_current_instruction()
+        environment = global_state.environment
 
         try:
-            callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
+            callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters(
+                global_state, self.dynamic_loader, True
+            )
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = global_state.environment.active_account.address
+                receiver = callee_account.address
+                transfer_ether(global_state, sender, receiver, value)
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
+        except ValueError as e:
+            log.debug(
+                "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
+                    e
+                )
+            )
+            global_state.mstate.stack.append(
+                global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+            )
+            return [global_state]
+
+        transaction = MessageCallTransaction(
+            world_state=global_state.world_state,
+            gas_price=environment.gasprice,
+            gas_limit=gas,
+            origin=environment.origin,
+            code=callee_account.code,
+            caller=environment.address,
+            callee_account=environment.active_account,
+            call_data=call_data,
+            call_value=value,
+            static=environment.static,
+        )
+        raise TransactionStartSignal(transaction, self.op_code, global_state)
+
+    @StateTransition()
+    def callcode_post(self, global_state: GlobalState) -> List[GlobalState]:
+        """
+
+        :param global_state:
+        :return:
+        """
+        instr = global_state.get_current_instruction()
+
+        try:
+            callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters(
                 global_state, self.dynamic_loader, True
             )
         except ValueError as e:
@@ -1754,7 +2014,6 @@ class Instruction:
             )
             global_state.mstate.stack.append(return_value)
             global_state.mstate.constraints.append(return_value == 0)
-
             return [global_state]
 
         try:
@@ -1787,11 +2046,10 @@ class Instruction:
         return_value = global_state.new_bitvec("retval_" + str(instr["address"]), 256)
         global_state.mstate.stack.append(return_value)
         global_state.mstate.constraints.append(return_value == 1)
-
         return [global_state]
 
     @StateTransition()
-    def callcode_(self, global_state: GlobalState) -> List[GlobalState]:
+    def delegatecall_(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
         :param global_state:
@@ -1802,8 +2060,20 @@ class Instruction:
 
         try:
             callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters(
-                global_state, self.dynamic_loader, True
+                global_state, self.dynamic_loader
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = global_state.environment.active_account.address
+                receiver = callee_account.address
+                transfer_ether(global_state, sender, receiver, value)
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@@ -1821,15 +2091,16 @@ class Instruction:
             gas_limit=gas,
             origin=environment.origin,
             code=callee_account.code,
-            caller=environment.address,
+            caller=environment.sender,
             callee_account=environment.active_account,
             call_data=call_data,
-            call_value=value,
+            call_value=environment.callvalue,
+            static=environment.static,
         )
-        raise TransactionStartSignal(transaction, self.op_code)
+        raise TransactionStartSignal(transaction, self.op_code, global_state)
 
     @StateTransition()
-    def callcode_post(self, global_state: GlobalState) -> List[GlobalState]:
+    def delegatecall_post(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
         :param global_state:
@@ -1839,7 +2110,7 @@ class Instruction:
 
         try:
             callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters(
-                global_state, self.dynamic_loader, True
+                global_state, self.dynamic_loader
             )
         except ValueError as e:
             log.debug(
@@ -1894,7 +2165,7 @@ class Instruction:
         return [global_state]
 
     @StateTransition()
-    def delegatecall_(self, global_state: GlobalState) -> List[GlobalState]:
+    def staticcall_(self, global_state: GlobalState) -> List[GlobalState]:
         """
 
         :param global_state:
@@ -1902,11 +2173,22 @@ class Instruction:
         """
         instr = global_state.get_current_instruction()
         environment = global_state.environment
-
         try:
-            callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters(
+            callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
                 global_state, self.dynamic_loader
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = environment.active_account.address
+                receiver = callee_account.address
+                transfer_ether(global_state, sender, receiver, value)
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@@ -1918,36 +2200,43 @@ class Instruction:
             )
             return [global_state]
 
+        native_result = native_call(
+            global_state, callee_address, call_data, memory_out_offset, memory_out_size
+        )
+
+        if native_result:
+            return native_result
+
         transaction = MessageCallTransaction(
             world_state=global_state.world_state,
             gas_price=environment.gasprice,
             gas_limit=gas,
             origin=environment.origin,
             code=callee_account.code,
-            caller=environment.sender,
-            callee_account=environment.active_account,
+            caller=environment.address,
+            callee_account=callee_account,
             call_data=call_data,
-            call_value=environment.callvalue,
+            call_value=value,
+            static=True,
         )
-        raise TransactionStartSignal(transaction, self.op_code)
+        raise TransactionStartSignal(transaction, self.op_code, global_state)
 
     @StateTransition()
-    def delegatecall_post(self, global_state: GlobalState) -> List[GlobalState]:
-        """
+    def staticcall_post(self, global_state: GlobalState) -> List[GlobalState]:
+        return self.post_handler(global_state, function_name="staticcall")
 
-        :param global_state:
-        :return:
-        """
+    def post_handler(self, global_state, function_name: str):
         instr = global_state.get_current_instruction()
 
         try:
-            callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters(
-                global_state, self.dynamic_loader
+            with_value = function_name is not "staticcall"
+            callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
+                global_state, self.dynamic_loader, with_value
             )
         except ValueError as e:
             log.debug(
-                "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
-                    e
+                "Could not determine required parameters for {}, putting fresh symbol on the stack. \n{}".format(
+                    function_name, e
                 )
             )
             global_state.mstate.stack.append(
@@ -1993,39 +2282,5 @@ class Instruction:
         return_value = global_state.new_bitvec("retval_" + str(instr["address"]), 256)
         global_state.mstate.stack.append(return_value)
         global_state.mstate.constraints.append(return_value == 1)
-        return [global_state]
-
-    @StateTransition()
-    def staticcall_(self, global_state: GlobalState) -> List[GlobalState]:
-        """
-
-        :param global_state:
-        :return:
-        """
-        # TODO: implement me
-        instr = global_state.get_current_instruction()
-        try:
-            callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
-                global_state, self.dynamic_loader
-            )
-        except ValueError as e:
-            log.debug(
-                "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
-                    e
-                )
-            )
-            global_state.mstate.stack.append(
-                global_state.new_bitvec("retval_" + str(instr["address"]), 256)
-            )
-            return [global_state]
 
-        native_result = native_call(
-            global_state, callee_address, call_data, memory_out_offset, memory_out_size
-        )
-        if native_result:
-            return native_result
-
-        global_state.mstate.stack.append(
-            global_state.new_bitvec("retval_" + str(instr["address"]), 256)
-        )
         return [global_state]

mythril/laser/ethereum/natives.py

@@ -6,12 +6,20 @@ from typing import List, Union
 
 from ethereum.utils import ecrecover_to_pub
 from py_ecc.secp256k1 import N as secp256k1n
+import py_ecc.optimized_bn128 as bn128
 from rlp.utils import ALL_BYTES
 
 from mythril.laser.ethereum.state.calldata import BaseCalldata, ConcreteCalldata
-from mythril.laser.ethereum.util import bytearray_to_int
-from ethereum.utils import sha3
-from mythril.laser.smt import Concat, simplify
+from mythril.laser.ethereum.util import extract_copy, extract32
+from ethereum.utils import (
+    sha3,
+    big_endian_to_int,
+    safe_ord,
+    zpad,
+    int_to_big_endian,
+    encode_int32,
+)
+from ethereum.specials import validate_point
 
 log = logging.getLogger(__name__)
 
@@ -22,35 +30,6 @@ class NativeContractException(Exception):
     pass
 
 
-def int_to_32bytes(
-    i: int
-) -> bytes:  # used because int can't fit as bytes function's input
-    """
-
-    :param i:
-    :return:
-    """
-    o = [0] * 32
-    for x in range(32):
-        o[31 - x] = i & 0xFF
-        i >>= 8
-    return bytes(o)
-
-
-def extract32(data: bytearray, i: int) -> int:
-    """
-
-    :param data:
-    :param i:
-    :return:
-    """
-    if i >= len(data):
-        return 0
-    o = data[i : min(i + 32, len(data))]
-    o.extend(bytearray(32 - len(o)))
-    return bytearray_to_int(o)
-
-
 def ecrecover(data: List[int]) -> List[int]:
     """
 
@@ -59,14 +38,14 @@ def ecrecover(data: List[int]) -> List[int]:
     """
     # TODO: Add type hints
     try:
-        byte_data = bytearray(data)
-        v = extract32(byte_data, 32)
-        r = extract32(byte_data, 64)
-        s = extract32(byte_data, 96)
+        bytes_data = bytearray(data)
+        v = extract32(bytes_data, 32)
+        r = extract32(bytes_data, 64)
+        s = extract32(bytes_data, 96)
     except TypeError:
         raise NativeContractException
 
-    message = b"".join([ALL_BYTES[x] for x in byte_data[0:32]])
+    message = b"".join([ALL_BYTES[x] for x in bytes_data[0:32]])
     if r >= secp256k1n or s >= secp256k1n or v < 27 or v > 28:
         return []
     try:
@@ -85,10 +64,10 @@ def sha256(data: List[int]) -> List[int]:
     :return:
     """
     try:
-        byte_data = bytes(data)
+        bytes_data = bytes(data)
     except TypeError:
         raise NativeContractException
-    return list(bytearray(hashlib.sha256(byte_data).digest()))
+    return list(bytearray(hashlib.sha256(bytes_data).digest()))
 
 
 def ripemd160(data: List[int]) -> List[int]:
@@ -120,6 +99,114 @@ def identity(data: List[int]) -> List[int]:
     return data
 
 
+def mod_exp(data: List[int]) -> List[int]:
+    """
+    TODO: Some symbolic parts can be handled here
+    Modular Exponentiation
+    :param data: Data with <length_of_BASE> <length_of_EXPONENT> <length_of_MODULUS> <BASE> <EXPONENT> <MODULUS>
+    :return: modular exponentiation
+    """
+    bytes_data = bytearray(data)
+    baselen = extract32(bytes_data, 0)
+    explen = extract32(bytes_data, 32)
+    modlen = extract32(bytes_data, 64)
+    if baselen == 0:
+        return [0] * modlen
+    if modlen == 0:
+        return []
+
+    first_exp_bytes = extract32(bytes_data, 96 + baselen) >> (8 * max(32 - explen, 0))
+    bitlength = -1
+    while first_exp_bytes:
+        bitlength += 1
+        first_exp_bytes >>= 1
+
+    base = bytearray(baselen)
+    extract_copy(bytes_data, base, 0, 96, baselen)
+    exp = bytearray(explen)
+    extract_copy(bytes_data, exp, 0, 96 + baselen, explen)
+    mod = bytearray(modlen)
+    extract_copy(bytes_data, mod, 0, 96 + baselen + explen, modlen)
+    if big_endian_to_int(mod) == 0:
+        return [0] * modlen
+    o = pow(big_endian_to_int(base), big_endian_to_int(exp), big_endian_to_int(mod))
+    return [safe_ord(x) for x in zpad(int_to_big_endian(o), modlen)]
+
+
+def ec_add(data: List[int]) -> List[int]:
+    bytes_data = bytearray(data)
+    x1 = extract32(bytes_data, 0)
+    y1 = extract32(bytes_data, 32)
+    x2 = extract32(bytes_data, 64)
+    y2 = extract32(bytes_data, 96)
+    p1 = validate_point(x1, y1)
+    p2 = validate_point(x2, y2)
+    if p1 is False or p2 is False:
+        return []
+    o = bn128.normalize(bn128.add(p1, p2))
+    return [safe_ord(x) for x in (encode_int32(o[0].n) + encode_int32(o[1].n))]
+
+
+def ec_mul(data: List[int]) -> List[int]:
+    bytes_data = bytearray(data)
+    x = extract32(bytes_data, 0)
+    y = extract32(bytes_data, 32)
+    m = extract32(bytes_data, 64)
+    p = validate_point(x, y)
+    if p is False:
+        return []
+    o = bn128.normalize(bn128.multiply(p, m))
+    return [safe_ord(c) for c in (encode_int32(o[0].n) + encode_int32(o[1].n))]
+
+
+def ec_pair(data: List[int]) -> List[int]:
+    if len(data) % 192:
+        return []
+
+    zero = (bn128.FQ2.one(), bn128.FQ2.one(), bn128.FQ2.zero())
+    exponent = bn128.FQ12.one()
+    bytes_data = bytearray(data)
+    for i in range(0, len(bytes_data), 192):
+        x1 = extract32(bytes_data, i)
+        y1 = extract32(bytes_data, i + 32)
+        x2_i = extract32(bytes_data, i + 64)
+        x2_r = extract32(bytes_data, i + 96)
+        y2_i = extract32(bytes_data, i + 128)
+        y2_r = extract32(bytes_data, i + 160)
+        p1 = validate_point(x1, y1)
+        if p1 is False:
+            return []
+        for v in (x2_i, x2_r, y2_i, y2_r):
+            if v >= bn128.field_modulus:
+                return []
+        fq2_x = bn128.FQ2([x2_r, x2_i])
+        fq2_y = bn128.FQ2([y2_r, y2_i])
+        if (fq2_x, fq2_y) != (bn128.FQ2.zero(), bn128.FQ2.zero()):
+            p2 = (fq2_x, fq2_y, bn128.FQ2.one())
+            if not bn128.is_on_curve(p2, bn128.b2):
+                return []
+        else:
+            p2 = zero
+        if bn128.multiply(p2, bn128.curve_order)[-1] != bn128.FQ2.zero():
+            return []
+        exponent *= bn128.pairing(p2, p1, final_exponentiate=False)
+    result = bn128.final_exponentiate(exponent) == bn128.FQ12.one()
+    return [0] * 31 + [1 if result else 0]
+
+
+PRECOMPILE_FUNCTIONS = (
+    ecrecover,
+    sha256,
+    ripemd160,
+    identity,
+    mod_exp,
+    ec_add,
+    ec_mul,
+    ec_pair,
+)
+PRECOMPILE_COUNT = len(PRECOMPILE_FUNCTIONS)
+
+
 def native_contracts(address: int, data: BaseCalldata) -> List[int]:
     """Takes integer address 1, 2, 3, 4.
 
@@ -127,11 +214,10 @@ def native_contracts(address: int, data: BaseCalldata) -> List[int]:
     :param data:
     :return:
     """
-    functions = (ecrecover, sha256, ripemd160, identity)
 
     if isinstance(data, ConcreteCalldata):
         concrete_data = data.concrete(None)
     else:
         raise NativeContractException()
 
-    return functions[address - 1](concrete_data)
+    return PRECOMPILE_FUNCTIONS[address - 1](concrete_data)

mythril/laser/ethereum/plugins/implementations/dependency_pruner.py

@@ -1,7 +1,10 @@
 from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.plugins.plugin import LaserPlugin
 from mythril.laser.ethereum.plugins.signals import PluginSkipState
-from mythril.laser.ethereum.state.annotation import StateAnnotation
+from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
+    DependencyAnnotation,
+    WSDependencyAnnotation,
+)
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
@@ -9,62 +12,12 @@ from mythril.laser.ethereum.transaction.transaction_models import (
 from mythril.exceptions import UnsatError
 from mythril.analysis import solver
 from typing import cast, List, Dict, Set
-from copy import copy
 import logging
 
 
 log = logging.getLogger(__name__)
 
 
-class DependencyAnnotation(StateAnnotation):
-    """Dependency Annotation
-
-    This annotation tracks read and write access to the state during each transaction.
-    """
-
-    def __init__(self):
-        self.storage_loaded = []  # type: List
-        self.storage_written = {}  # type: Dict[int, List]
-        self.path = [0]  # type: List
-        self.blocks_seen = set()  # type: Set[int]
-
-    def __copy__(self):
-        result = DependencyAnnotation()
-        result.storage_loaded = copy(self.storage_loaded)
-        result.storage_written = copy(self.storage_written)
-        result.path = copy(self.path)
-        result.blocks_seen = copy(self.blocks_seen)
-        return result
-
-    def get_storage_write_cache(self, iteration: int):
-        if iteration not in self.storage_written:
-            self.storage_written[iteration] = []
-
-        return self.storage_written[iteration]
-
-    def extend_storage_write_cache(self, iteration: int, value: object):
-        if iteration not in self.storage_written:
-            self.storage_written[iteration] = [value]
-        elif value not in self.storage_written[iteration]:
-            self.storage_written[iteration].append(value)
-
-
-class WSDependencyAnnotation(StateAnnotation):
-    """Dependency Annotation for World state
-
-    This  world state annotation maintains a stack of state annotations.
-    It is used to transfer individual state annotations from one transaction to the next.
-    """
-
-    def __init__(self):
-        self.annotations_stack = []
-
-    def __copy__(self):
-        result = WSDependencyAnnotation()
-        result.annotations_stack = copy(self.annotations_stack)
-        return result
-
-
 def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation:
     """ Returns a dependency annotation
 
@@ -134,6 +87,7 @@ class DependencyPruner(LaserPlugin):
 
     def _reset(self):
         self.iteration = 0
+        self.calls_on_path = {}  # type: Dict[int, bool]
         self.sloads_on_path = {}  # type: Dict[int, List[object]]
         self.sstores_on_path = {}  # type: Dict[int, List[object]]
         self.storage_accessed_global = set()  # type: Set
@@ -166,6 +120,17 @@ class DependencyPruner(LaserPlugin):
             else:
                 self.sstores_on_path[address] = [target_location]
 
+    def update_calls(self, path: List[int]) -> None:
+        """Update the dependency map for the block offsets on the given path.
+
+        :param path
+        :param target_location
+        """
+
+        for address in path:
+            if address in self.sstores_on_path:
+                self.calls_on_path[address] = True
+
     def wanna_execute(self, address: int, annotation: DependencyAnnotation) -> bool:
         """Decide whether the basic block starting at 'address' should be executed.
 
@@ -175,6 +140,9 @@ class DependencyPruner(LaserPlugin):
 
         storage_write_cache = annotation.get_storage_write_cache(self.iteration - 1)
 
+        if address in self.calls_on_path:
+            return True
+
         # Skip "pure" paths that don't have any dependencies.
 
         if address not in self.sloads_on_path:
@@ -270,6 +238,13 @@ class DependencyPruner(LaserPlugin):
             self.update_sloads(annotation.path, location)
             self.storage_accessed_global.add(location)
 
+        @symbolic_vm.pre_hook("CALL")
+        def call_hook(state: GlobalState):
+            annotation = get_dependency_annotation(state)
+
+            self.update_calls(annotation.path)
+            annotation.has_call = True
+
         @symbolic_vm.pre_hook("STOP")
         def stop_hook(state: GlobalState):
             _transaction_end(state)
@@ -293,11 +268,14 @@ class DependencyPruner(LaserPlugin):
             for index in annotation.storage_written:
                 self.update_sstores(annotation.path, index)
 
+            if annotation.has_call:
+                self.update_calls(annotation.path)
+
         def _check_basic_block(address: int, annotation: DependencyAnnotation):
             """This method is where the actual pruning happens.
 
              :param address: Start address (bytecode offset) of the block
-             :param annotation
+             :param annotation:
              """
 
             # Don't skip any blocks in the contract creation transaction
@@ -338,13 +316,3 @@ class DependencyPruner(LaserPlugin):
             annotation.storage_loaded = []
 
             world_state_annotation.annotations_stack.append(annotation)
-
-            log.debug(
-                "Iteration {}: Adding world state at address {}, end of function {}.\nDependency map: {}\nStorage written: {}".format(
-                    self.iteration,
-                    state.get_current_instruction()["address"],
-                    state.node.function_name,
-                    self.sloads_on_path,
-                    annotation.storage_written[self.iteration],
-                )
-            )

mythril/laser/ethereum/plugins/implementations/mutation_pruner.py

@@ -1,23 +1,16 @@
-from mythril.laser.ethereum.state.annotation import StateAnnotation
-from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
 from mythril.laser.ethereum.plugins.plugin import LaserPlugin
+from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
+    MutationAnnotation,
+)
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
 )
 from mythril.laser.smt import And, symbol_factory
 
 
-class MutationAnnotation(StateAnnotation):
-    """Mutation Annotation
-
-    This is the annotation used by the MutationPruner plugin to record mutations
-    """
-
-    pass
-
-
 class MutationPruner(LaserPlugin):
     """Mutation pruner plugin
 
@@ -42,7 +35,11 @@ class MutationPruner(LaserPlugin):
         """
 
         @symbolic_vm.pre_hook("SSTORE")
-        def mutator_hook(global_state: GlobalState):
+        def sstore_mutator_hook(global_state: GlobalState):
+            global_state.annotate(MutationAnnotation())
+
+        @symbolic_vm.pre_hook("CALL")
+        def call_mutator_hook(global_state: GlobalState):
             global_state.annotate(MutationAnnotation())
 
         @symbolic_vm.laser_hook("add_world_state")

mythril/laser/ethereum/plugins/implementations/plugin_annotations.py

@@ -0,0 +1,65 @@
+from mythril.laser.ethereum.state.annotation import StateAnnotation
+
+from copy import copy
+from typing import Dict, List, Set
+
+
+class MutationAnnotation(StateAnnotation):
+    """Mutation Annotation
+
+    This is the annotation used by the MutationPruner plugin to record mutations
+    """
+
+    def __init__(self):
+        pass
+
+
+class DependencyAnnotation(StateAnnotation):
+    """Dependency Annotation
+
+    This annotation tracks read and write access to the state during each transaction.
+    """
+
+    def __init__(self):
+        self.storage_loaded = []  # type: List
+        self.storage_written = {}  # type: Dict[int, List]
+        self.has_call = False  # type: bool
+        self.path = [0]  # type: List
+        self.blocks_seen = set()  # type: Set[int]
+
+    def __copy__(self):
+        result = DependencyAnnotation()
+        result.storage_loaded = copy(self.storage_loaded)
+        result.storage_written = copy(self.storage_written)
+        result.has_call = self.has_call
+        result.path = copy(self.path)
+        result.blocks_seen = copy(self.blocks_seen)
+        return result
+
+    def get_storage_write_cache(self, iteration: int):
+        if iteration not in self.storage_written:
+            self.storage_written[iteration] = []
+
+        return self.storage_written[iteration]
+
+    def extend_storage_write_cache(self, iteration: int, value: object):
+        if iteration not in self.storage_written:
+            self.storage_written[iteration] = [value]
+        elif value not in self.storage_written[iteration]:
+            self.storage_written[iteration].append(value)
+
+
+class WSDependencyAnnotation(StateAnnotation):
+    """Dependency Annotation for World state
+
+    This  world state annotation maintains a stack of state annotations.
+    It is used to transfer individual state annotations from one transaction to the next.
+    """
+
+    def __init__(self):
+        self.annotations_stack = []
+
+    def __copy__(self):
+        result = WSDependencyAnnotation()
+        result.annotations_stack = copy(self.annotations_stack)
+        return result

mythril/laser/ethereum/state/account.py

@@ -2,8 +2,9 @@
 
 This includes classes representing accounts and their storage.
 """
+import logging
 from copy import copy, deepcopy
-from typing import Any, Dict, Union, Tuple, cast
+from typing import Any, Dict, Union, Tuple, Set, cast
 
 
 from mythril.laser.smt import (
@@ -19,6 +20,28 @@ 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):
+        raise NotImplementedError
+
+    def __setitem__(self, key, value):
+        raise NotImplementedError
+
+
+class ArrayStorageRegion(StorageRegion):
+    """ An ArrayStorageRegion is a storage region that leverages smt array theory to resolve expressions"""
+
+    pass
+
+
+class IteStorageRegion(StorageRegion):
+    """ An IteStorageRegion is a storage region that uses Ite statements to implement a storage"""
+
+    pass
+
 
 class Storage:
     """Storage class represents the storage of an Account."""
@@ -37,6 +60,7 @@ class Storage:
         self.printable_storage = {}  # type: Dict[BitVec, BitVec]
 
         self.dynld = dynamic_loader
+        self.storage_keys_loaded = set()  # type: Set[int]
         self.address = address
 
     @staticmethod
@@ -51,17 +75,18 @@ class Storage:
     def __getitem__(self, item: BitVec) -> BitVec:
         storage, is_keccak_storage = self._get_corresponding_storage(item)
         if is_keccak_storage:
-            item = self._sanitize(cast(BitVecFunc, item).input_)
-        value = storage[item]
+            sanitized_item = self._sanitize(cast(BitVecFunc, item).input_)
+        else:
+            sanitized_item = item
         if (
-            value.value == 0
-            and self.address
-            and item.symbolic is False
+            self.address
             and self.address.value != 0
+            and item.symbolic is False
+            and int(item.value) not in self.storage_keys_loaded
             and (self.dynld and self.dynld.storage_loading)
         ):
             try:
-                storage[item] = symbol_factory.BitVecVal(
+                storage[sanitized_item] = symbol_factory.BitVecVal(
                     int(
                         self.dynld.read_storage(
                             contract_address="0x{:040X}".format(self.address.value),
@@ -71,12 +96,12 @@ class Storage:
                     ),
                     256,
                 )
-                self.printable_storage[item] = storage[item]
-                return storage[item]
-            except ValueError:
-                pass
+                self.storage_keys_loaded.add(int(item.value))
+                self.printable_storage[item] = storage[sanitized_item]
+            except ValueError as e:
+                log.debug("Couldn't read storage at %s: %s", item, e)
 
-        return simplify(storage[item])
+        return simplify(storage[sanitized_item])
 
     @staticmethod
     def get_map_index(key: BitVec) -> BitVec:
@@ -113,15 +138,18 @@ class Storage:
         if is_keccak_storage:
             key = self._sanitize(key.input_)
         storage[key] = value
+        if key.symbolic is False:
+            self.storage_keys_loaded.add(int(key.value))
 
-    def __deepcopy__(self, memodict={}):
+    def __deepcopy__(self, memodict=dict()):
         concrete = isinstance(self._standard_storage, K)
         storage = Storage(
             concrete=concrete, address=self.address, dynamic_loader=self.dynld
         )
         storage._standard_storage = deepcopy(self._standard_storage)
         storage._map_storage = deepcopy(self._map_storage)
-        storage.print_storage = copy(self.printable_storage)
+        storage.printable_storage = copy(self.printable_storage)
+        storage.storage_keys_loaded = copy(self.storage_keys_loaded)
         return storage
 
     def __str__(self) -> str:

mythril/laser/ethereum/state/annotation.py

@@ -12,6 +12,8 @@ class StateAnnotation:
     traverse the state space themselves.
     """
 
+    # TODO: Remove this? It seems to be used only in the MutationPruner, and
+    # we could simply use world state annotations if we want them to be persisted.
     @property
     def persist_to_world_state(self) -> bool:
         """If this function returns true then laser will also annotate the

mythril/laser/ethereum/state/calldata.py

@@ -70,7 +70,7 @@ class BaseCalldata:
             try:
                 current_index = (
                     start
-                    if isinstance(start, Expression)
+                    if isinstance(start, BitVec)
                     else symbol_factory.BitVecVal(start, 256)
                 )
                 parts = []

mythril/laser/ethereum/state/environment.py

@@ -22,6 +22,7 @@ class Environment:
         callvalue: ExprRef,
         origin: ExprRef,
         code=None,
+        static=False,
     ) -> None:
         """
 
@@ -32,7 +33,7 @@ class Environment:
         :param callvalue:
         :param origin:
         :param code:
-        :param calldata_type:
+        :param static: Makes the environment static.
         """
         # Metadata
 
@@ -50,6 +51,7 @@ class Environment:
         self.gasprice = gasprice
         self.origin = origin
         self.callvalue = callvalue
+        self.static = static
 
     def __str__(self) -> str:
         """

mythril/laser/ethereum/state/global_state.py

@@ -52,6 +52,14 @@ class GlobalState:
         self.last_return_data = last_return_data
         self._annotations = annotations or []
 
+    def add_annotations(self, annotations: List[StateAnnotation]):
+        """
+        Function used to add annotations to global state
+        :param annotations:
+        :return:
+        """
+        self._annotations += annotations
+
     def __copy__(self) -> "GlobalState":
         """
 
@@ -86,9 +94,12 @@ class GlobalState:
 
         :return:
         """
-
         instructions = self.environment.code.instruction_list
+        try:
             return instructions[self.mstate.pc]
+        except KeyError:
+            new_instruction = {"address": self.mstate.pc, "opcode": "STOP"}
+            return new_instruction
 
     @property
     def current_transaction(

mythril/laser/ethereum/state/world_state.py

@@ -27,6 +27,7 @@ class WorldState:
         """
         self._accounts = {}  # type: Dict[int, Account]
         self.balances = Array("balance", 256, 256)
+        self.starting_balances = copy(self.balances)
 
         self.node = None  # type: Optional['Node']
         self.transaction_sequence = transaction_sequence or []
@@ -60,6 +61,7 @@ class WorldState:
             annotations=new_annotations,
         )
         new_world_state.balances = copy(self.balances)
+        new_world_state.starting_balances = copy(self.starting_balances)
         for account in self._accounts.values():
             new_world_state.put_account(copy(account))
         new_world_state.node = self.node
@@ -115,7 +117,7 @@ class WorldState:
             concrete_storage=concrete_storage,
         )
         if balance:
-            new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
+            new_account.add_balance(symbol_factory.BitVecVal(balance, 256))
 
         self.put_account(new_account)
         return new_account

mythril/laser/ethereum/svm.py

@@ -3,14 +3,18 @@ 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.analysis.potential_issues import check_potential_issues
 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
 from mythril.laser.ethereum.instructions import Instruction
 from mythril.laser.ethereum.iprof import InstructionProfiler
 from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState
+from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
+    MutationAnnotation,
+)
 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
@@ -55,6 +59,8 @@ class LaserEVM:
         transaction_count=2,
         requires_statespace=True,
         enable_iprof=False,
+        enable_coverage_strategy=False,
+        instruction_laser_plugin=None,
     ) -> None:
         """
         Initializes the laser evm object
@@ -73,6 +79,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
@@ -102,6 +109,13 @@ class LaserEVM:
 
         self.iprof = InstructionProfiler() if enable_iprof else None
 
+        if enable_coverage_strategy:
+            from mythril.laser.ethereum.plugins.implementations.coverage.coverage_strategy import (
+                CoverageStrategy,
+            )
+
+            self.strategy = CoverageStrategy(self.strategy, instruction_laser_plugin)
+
         log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
 
     def extend_strategy(self, extension: ABCMeta, *args) -> None:
@@ -200,7 +214,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:
@@ -214,6 +228,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 (
@@ -222,6 +237,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:
@@ -234,8 +250,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:
@@ -246,6 +261,7 @@ class LaserEVM:
 
     def _add_world_state(self, global_state: GlobalState):
         """ Stores the world_state of the passed global state in the open states"""
+
         for hook in self._add_world_state_hooks:
             try:
                 hook(global_state)
@@ -256,11 +272,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:
@@ -312,7 +328,11 @@ class LaserEVM:
                 global_state.transaction_stack
             ) + [(start_signal.transaction, global_state)]
             new_global_state.node = global_state.node
-            new_global_state.mstate.constraints = global_state.mstate.constraints
+            new_global_state.mstate.constraints = (
+                start_signal.global_state.mstate.constraints
+            )
+
+            log.debug("Starting new transaction %s", start_signal.transaction)
 
             return [new_global_state], op_code
 
@@ -321,11 +341,15 @@ class LaserEVM:
                 -1
             ]
 
+            log.debug("Ending transaction %s.", transaction)
+
             if return_global_state is None:
                 if (
                     not isinstance(transaction, ContractCreationTransaction)
                     or transaction.return_data
                 ) and not end_signal.revert:
+                    check_potential_issues(global_state)
+
                     end_signal.global_state.world_state.node = global_state.node
                     self._add_world_state(end_signal.global_state)
                 new_global_states = []
@@ -333,6 +357,19 @@ class LaserEVM:
                 # First execute the post hook for the transaction ending instruction
                 self._execute_post_hook(op_code, [end_signal.global_state])
 
+                # Propogate codecall based annotations
+                if return_global_state.get_current_instruction()["opcode"] in (
+                    "DELEGATECALL",
+                    "CALLCODE",
+                ):
+                    new_annotations = [
+                        annotation
+                        for annotation in global_state.get_annotations(
+                            MutationAnnotation
+                        )
+                    ]
+                    return_global_state.add_annotations(new_annotations)
+
                 new_global_states = self._end_message_call(
                     copy(return_global_state),
                     global_state,
@@ -373,6 +410,15 @@ class LaserEVM:
             return_global_state.environment.active_account = global_state.accounts[
                 return_global_state.environment.active_account.address.value
             ]
+            if isinstance(
+                global_state.current_transaction, ContractCreationTransaction
+            ):
+                return_global_state.mstate.min_gas_used += (
+                    global_state.mstate.min_gas_used
+                )
+                return_global_state.mstate.max_gas_used += (
+                    global_state.mstate.max_gas_used
+                )
 
         # Execute the post instruction handler
         new_global_states = Instruction(
@@ -396,6 +442,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]

mythril/laser/ethereum/transaction/symbolic.py

@@ -23,7 +23,7 @@ ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
 ACTOR_ADDRESSES = [
     symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256),
     symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256),
-    symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEE, 256),
+    symbol_factory.BitVecVal(0xAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA, 256),
 ]
 
 
@@ -85,6 +85,8 @@ def execute_contract_creation(
     new_account = None
     for open_world_state in open_states:
         next_transaction_id = get_next_transaction_id()
+        # call_data "should" be '[]', but it is easier to model the calldata symbolically
+        # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly"
         transaction = ContractCreationTransaction(
             world_state=open_world_state,
             identifier=next_transaction_id,
@@ -98,7 +100,7 @@ def execute_contract_creation(
             code=Disassembly(contract_initialization_code),
             caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256),
             contract_name=contract_name,
-            call_data=[],
+            call_data=None,
             call_value=symbol_factory.BitVecSym(
                 "call_value{}".format(next_transaction_id), 256
             ),

mythril/laser/ethereum/transaction/transaction_models.py

@@ -4,7 +4,7 @@ execution."""
 import array
 from copy import deepcopy
 from z3 import ExprRef
-from typing import Union, Optional, cast
+from typing import Union, Optional
 
 from mythril.laser.ethereum.state.calldata import ConcreteCalldata
 from mythril.laser.ethereum.state.account import Account
@@ -12,8 +12,10 @@ from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata
 from mythril.laser.ethereum.state.environment import Environment
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
-from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.smt import symbol_factory
+from mythril.laser.smt import symbol_factory, UGE, BitVec
+import logging
+
+log = logging.getLogger(__name__)
 
 _next_transaction_id = 0
 
@@ -43,9 +45,11 @@ class TransactionStartSignal(Exception):
         self,
         transaction: Union["MessageCallTransaction", "ContractCreationTransaction"],
         op_code: str,
+        global_state: GlobalState,
     ) -> None:
         self.transaction = transaction
         self.op_code = op_code
+        self.global_state = global_state
 
 
 class BaseTransaction:
@@ -64,6 +68,7 @@ class BaseTransaction:
         code=None,
         call_value=None,
         init_call_data=True,
+        static=False,
     ) -> None:
         assert isinstance(world_state, WorldState)
         self.world_state = world_state
@@ -99,7 +104,7 @@ class BaseTransaction:
             if call_value is not None
             else symbol_factory.BitVecSym("callvalue{}".format(identifier), 256)
         )
-
+        self.static = static
         self.return_data = None  # type: str
 
     def initial_global_state_from_environment(self, environment, active_function):
@@ -115,16 +120,31 @@ class BaseTransaction:
 
         sender = environment.sender
         receiver = environment.active_account.address
-        value = environment.callvalue
+        value = (
+            environment.callvalue
+            if isinstance(environment.callvalue, BitVec)
+            else symbol_factory.BitVecVal(environment.callvalue, 256)
+        )
 
-        global_state.world_state.balances[sender] -= value
+        global_state.mstate.constraints.append(
+            UGE(global_state.world_state.balances[sender], value)
+        )
         global_state.world_state.balances[receiver] += value
+        global_state.world_state.balances[sender] -= value
 
         return global_state
 
     def initial_global_state(self) -> GlobalState:
         raise NotImplementedError
 
+    def __str__(self) -> str:
+        return "{} {} from {} to {:#42x}".format(
+            self.__class__.__name__,
+            self.id,
+            self.caller,
+            int(str(self.callee_account.address)) if self.callee_account else -1,
+        )
+
 
 class MessageCallTransaction(BaseTransaction):
     """Transaction object models an transaction."""
@@ -142,6 +162,7 @@ class MessageCallTransaction(BaseTransaction):
             self.call_value,
             self.origin,
             code=self.code or self.callee_account.code,
+            static=self.static,
         )
         return super().initial_global_state_from_environment(
             environment, active_function="fallback"
@@ -174,13 +195,18 @@ class ContractCreationTransaction(BaseTransaction):
         code=None,
         call_value=None,
         contract_name=None,
+        contract_address=None,
     ) -> None:
         self.prev_world_state = deepcopy(world_state)
+        contract_address = (
+            contract_address if isinstance(contract_address, int) else None
+        )
         callee_account = world_state.create_account(
-            0, concrete_storage=True, creator=caller.value
+            0, concrete_storage=True, creator=caller.value, address=contract_address
         )
-        callee_account.contract_name = contract_name
-        # TODO: set correct balance for new account
+        callee_account.contract_name = contract_name or callee_account.contract_name
+        # init_call_data "should" be false, but it is easier to model the calldata symbolically
+        # and add logic in codecopy/codesize/calldatacopy/calldatasize than to model code "correctly"
         super().__init__(
             world_state=world_state,
             callee_account=callee_account,
@@ -192,7 +218,7 @@ class ContractCreationTransaction(BaseTransaction):
             origin=origin,
             code=code,
             call_value=call_value,
-            init_call_data=False,
+            init_call_data=True,
         )
 
     def initial_global_state(self) -> GlobalState:

mythril/laser/ethereum/util.py

@@ -45,7 +45,7 @@ def get_instruction_index(
     """
     index = 0
     for instr in instruction_list:
-        if instr["address"] == address:
+        if instr["address"] >= address:
             return index
         index += 1
     return None
@@ -150,3 +150,27 @@ def bytearray_to_int(arr):
     for a in arr:
         o = (o << 8) + a
     return o
+
+
+def extract_copy(
+    data: bytearray, mem: bytearray, memstart: int, datastart: int, size: int
+):
+    for i in range(size):
+        if datastart + i < len(data):
+            mem[memstart + i] = data[datastart + i]
+        else:
+            mem[memstart + i] = 0
+
+
+def extract32(data: bytearray, i: int) -> int:
+    """
+
+    :param data:
+    :param i:
+    :return:
+    """
+    if i >= len(data):
+        return 0
+    o = data[i : min(i + 32, len(data))]
+    o.extend(bytearray(32 - len(o)))
+    return bytearray_to_int(o)

mythril/laser/smt/__init__.py

@@ -1,8 +1,10 @@
-from mythril.laser.smt.bitvec import (
-    BitVec,
+from mythril.laser.smt.bitvec import BitVec
+
+from mythril.laser.smt.bitvec_helper import (
     If,
     UGT,
     ULT,
+    ULE,
     Concat,
     Extract,
     URem,
@@ -15,6 +17,7 @@ from mythril.laser.smt.bitvec import (
     BVSubNoUnderflow,
     LShR,
 )
+
 from mythril.laser.smt.bitvecfunc import BitVecFunc
 from mythril.laser.smt.expression import Expression, simplify
 from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not, And

mythril/laser/smt/array.py

@@ -8,7 +8,8 @@ default values over a certain range.
 from typing import cast
 import z3
 
-from mythril.laser.smt.bitvec import BitVec, If
+from mythril.laser.smt.bitvec import BitVec
+from mythril.laser.smt.bitvec_helper import If
 from mythril.laser.smt.bool import Bool
 
 

mythril/laser/smt/bitvec.py

@@ -1,10 +1,11 @@
 """This module provides classes for an SMT abstraction of bit vectors."""
 
-from typing import Union, overload, List, Set, cast, Any, Optional, Callable
 from operator import lshift, rshift, ne, eq
+from typing import Union, Set, cast, Any, Optional, Callable
+
 import z3
 
-from mythril.laser.smt.bool import Bool, And, Or
+from mythril.laser.smt.bool import Bool
 from mythril.laser.smt.expression import Expression
 
 Annotations = Set[Any]
@@ -276,276 +277,5 @@ class BitVec(Expression[z3.BitVecRef]):
         return self.raw.__hash__()
 
 
-def _comparison_helper(
-    a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool
-) -> Bool:
-    annotations = a.annotations.union(b.annotations)
-    if isinstance(a, BitVecFunc):
-        if not a.symbolic and not b.symbolic:
-            return Bool(operation(a.raw, b.raw), annotations=annotations)
-
-        if (
-            not isinstance(b, BitVecFunc)
-            or not a.func_name
-            or not a.input_
-            or not a.func_name == b.func_name
-        ):
-            return Bool(z3.BoolVal(default_value), annotations=annotations)
-
-        return And(
-            Bool(operation(a.raw, b.raw), annotations=annotations),
-            a.input_ == b.input_ if inputs_equal else a.input_ != b.input_,
-        )
-
-    return Bool(operation(a.raw, b.raw), annotations)
-
-
-def _arithmetic_helper(a: BitVec, b: BitVec, operation: Callable) -> BitVec:
-    raw = operation(a.raw, b.raw)
-    union = a.annotations.union(b.annotations)
-
-    if isinstance(a, BitVecFunc) and isinstance(b, BitVecFunc):
-        return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union)
-    elif isinstance(a, BitVecFunc):
-        return BitVecFunc(
-            raw=raw, func_name=a.func_name, input_=a.input_, annotations=union
-        )
-    elif isinstance(b, BitVecFunc):
-        return BitVecFunc(
-            raw=raw, func_name=b.func_name, input_=b.input_, annotations=union
-        )
-
-    return BitVec(raw, annotations=union)
-
-
-def LShR(a: BitVec, b: BitVec):
-    return _arithmetic_helper(a, b, z3.LShR)
-
-
-def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> BitVec:
-    """Create an if-then-else expression.
-
-    :param a:
-    :param b:
-    :param c:
-    :return:
-    """
-    # TODO: Handle BitVecFunc
-
-    if not isinstance(a, Bool):
-        a = Bool(z3.BoolVal(a))
-    if not isinstance(b, BitVec):
-        b = BitVec(z3.BitVecVal(b, 256))
-    if not isinstance(c, BitVec):
-        c = BitVec(z3.BitVecVal(c, 256))
-    union = a.annotations.union(b.annotations).union(c.annotations)
-    return BitVec(z3.If(a.raw, b.raw, c.raw), union)
-
-
-def UGT(a: BitVec, b: BitVec) -> Bool:
-    """Create an unsigned greater than expression.
-
-    :param a:
-    :param b:
-    :return:
-    """
-    return _comparison_helper(a, b, z3.UGT, default_value=False, inputs_equal=False)
-
-
-def UGE(a: BitVec, b: BitVec) -> Bool:
-    """Create an unsigned greater or equals expression.
-
-    :param a:
-    :param b:
-    :return:
-    """
-    return Or(UGT(a, b), a == b)
-
-
-def ULT(a: BitVec, b: BitVec) -> Bool:
-    """Create an unsigned less than expression.
-
-    :param a:
-    :param b:
-    :return:
-    """
-    return _comparison_helper(a, b, z3.ULT, default_value=False, inputs_equal=False)
-
-
-def ULE(a: BitVec, b: BitVec) -> Bool:
-    """Create an unsigned less than expression.
-
-    :param a:
-    :param b:
-    :return:
-    """
-    return Or(ULT(a, b), a == b)
-
-
-@overload
-def Concat(*args: List[BitVec]) -> BitVec:    ...
-
-
-@overload
-def Concat(*args: BitVec) -> BitVec:    ...
-
-
-def Concat(*args: Union[BitVec, List[BitVec]]) -> BitVec:
-    """Create a concatenation expression.
-
-    :param args:
-    :return:
-    """
-    # The following statement is used if a list is provided as an argument to concat
-    if len(args) == 1 and isinstance(args[0], list):
-        bvs = args[0]  # type: List[BitVec]
-    else:
-        bvs = cast(List[BitVec], args)
-
-    nraw = z3.Concat([a.raw for a in bvs])
-    annotations = set()  # type: Annotations
-    bitvecfunc = False
-    for bv in bvs:
-        annotations = annotations.union(bv.annotations)
-        if isinstance(bv, BitVecFunc):
-            bitvecfunc = True
-
-    if bitvecfunc:
-        # Added this not so good and misleading NOTATION to help with this
-        str_hash = ",".join(["hashed({})".format(hash(bv)) for bv in bvs])
-        input_string = "MisleadingNotationConcat({})".format(str_hash)
-
-        return BitVecFunc(
-            raw=nraw, func_name="Hybrid", input_=BitVec(z3.BitVec(input_string, 256), annotations=annotations)
-        )
-
-    return BitVec(nraw, annotations)
-
-
-def Extract(high: int, low: int, bv: BitVec) -> BitVec:
-    """Create an extract expression.
-
-    :param high:
-    :param low:
-    :param bv:
-    :return:
-    """
-    raw = z3.Extract(high, low, bv.raw)
-    if isinstance(bv, BitVecFunc):
-        input_string = "MisleadingNotationExtract({}, {}, hashed({}))".format(high, low, hash(bv))
-        # Is there a better value to set func_name and input to in this case?
-        return BitVecFunc(
-            raw=raw, func_name="Hybrid", input_=BitVec(z3.BitVec(input_string, 256), annotations=bv.annotations)
-        )
-
-    return BitVec(raw, annotations=bv.annotations)
-
-
-def URem(a: BitVec, b: BitVec) -> BitVec:
-    """Create an unsigned remainder expression.
-
-    :param a:
-    :param b:
-    :return:
-    """
-    return _arithmetic_helper(a, b, z3.URem)
-
-
-def SRem(a: BitVec, b: BitVec) -> BitVec:
-    """Create a signed remainder expression.
-
-    :param a:
-    :param b:
-    :return:
-    """
-    return _arithmetic_helper(a, b, z3.SRem)
-
-
-def UDiv(a: BitVec, b: BitVec) -> BitVec:
-    """Create an unsigned division expression.
-
-    :param a:
-    :param b:
-    :return:
-    """
-    return _arithmetic_helper(a, b, z3.UDiv)
-
-
-def Sum(*args: BitVec) -> BitVec:
-    """Create sum expression.
-
-    :return:
-    """
-    raw = z3.Sum([a.raw for a in args])
-    annotations = set()  # type: Annotations
-    bitvecfuncs = []
-
-    for bv in args:
-        annotations = annotations.union(bv.annotations)
-        if isinstance(bv, BitVecFunc):
-            bitvecfuncs.append(bv)
-
-    if len(bitvecfuncs) >= 2:
-        return BitVecFunc(raw=raw, func_name="Hybrid", input_=None, annotations=annotations)
-    elif len(bitvecfuncs) == 1:
-        return BitVecFunc(
-            raw=raw,
-            func_name=bitvecfuncs[0].func_name,
-            input_=bitvecfuncs[0].input_,
-            annotations=annotations,
-        )
-
-    return BitVec(raw, annotations)
-
-
-def BVAddNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
-    """Creates predicate that verifies that the addition doesn't overflow.
-
-    :param a:
-    :param b:
-    :param signed:
-    :return:
-    """
-    if not isinstance(a, BitVec):
-        a = BitVec(z3.BitVecVal(a, 256))
-    if not isinstance(b, BitVec):
-        b = BitVec(z3.BitVecVal(b, 256))
-    return Bool(z3.BVAddNoOverflow(a.raw, b.raw, signed))
-
-
-def BVMulNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
-    """Creates predicate that verifies that the multiplication doesn't
-    overflow.
-
-    :param a:
-    :param b:
-    :param signed:
-    :return:
-    """
-    if not isinstance(a, BitVec):
-        a = BitVec(z3.BitVecVal(a, 256))
-    if not isinstance(b, BitVec):
-        b = BitVec(z3.BitVecVal(b, 256))
-    return Bool(z3.BVMulNoOverflow(a.raw, b.raw, signed))
-
-
-def BVSubNoUnderflow(
-    a: Union[BitVec, int], b: Union[BitVec, int], signed: bool
-) -> Bool:
-    """Creates predicate that verifies that the subtraction doesn't overflow.
-
-    :param a:
-    :param b:
-    :param signed:
-    :return:
-    """
-    if not isinstance(a, BitVec):
-        a = BitVec(z3.BitVecVal(a, 256))
-    if not isinstance(b, BitVec):
-        b = BitVec(z3.BitVecVal(b, 256))
-
-    return Bool(z3.BVSubNoUnderflow(a.raw, b.raw, signed))
-
-
 # TODO: Fix circular import issues
 from mythril.laser.smt.bitvecfunc import BitVecFunc

mythril/laser/smt/bitvec_helper.py

@@ -0,0 +1,291 @@
+from typing import Union, overload, List, Set, cast, Any, Optional, Callable
+from operator import lshift, rshift, ne, eq
+import z3
+
+from mythril.laser.smt.bool import Bool, And, Or
+from mythril.laser.smt.bitvec import BitVec
+from mythril.laser.smt.bitvecfunc import BitVecFunc
+from mythril.laser.smt.bitvecfunc import _arithmetic_helper as _func_arithmetic_helper
+from mythril.laser.smt.bitvecfunc import _comparison_helper as _func_comparison_helper
+
+Annotations = Set[Any]
+
+
+def _comparison_helper(
+    a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool
+) -> Bool:
+    annotations = a.annotations.union(b.annotations)
+    if isinstance(a, BitVecFunc):
+        return _func_comparison_helper(a, b, operation, default_value, inputs_equal)
+    return Bool(operation(a.raw, b.raw), annotations)
+
+
+def _arithmetic_helper(a: BitVec, b: BitVec, operation: Callable) -> BitVec:
+    raw = operation(a.raw, b.raw)
+    union = a.annotations.union(b.annotations)
+
+    if isinstance(a, BitVecFunc):
+        return _func_arithmetic_helper(a, b, operation)
+    elif isinstance(b, BitVecFunc):
+        return _func_arithmetic_helper(b, a, operation)
+
+    return BitVec(raw, annotations=union)
+
+
+def LShR(a: BitVec, b: BitVec):
+    return _arithmetic_helper(a, b, z3.LShR)
+
+
+def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> BitVec:
+    """Create an if-then-else expression.
+
+    :param a:
+    :param b:
+    :param c:
+    :return:
+    """
+    # TODO: Handle BitVecFunc
+
+    if not isinstance(a, Bool):
+        a = Bool(z3.BoolVal(a))
+    if not isinstance(b, BitVec):
+        b = BitVec(z3.BitVecVal(b, 256))
+    if not isinstance(c, BitVec):
+        c = BitVec(z3.BitVecVal(c, 256))
+    union = a.annotations.union(b.annotations).union(c.annotations)
+
+    bvf = []  # type: List[BitVecFunc]
+    if isinstance(a, BitVecFunc):
+        bvf += [a]
+    if isinstance(b, BitVecFunc):
+        bvf += [b]
+    if isinstance(c, BitVecFunc):
+        bvf += [c]
+    if bvf:
+        raw = z3.If(a.raw, b.raw, c.raw)
+        nested_functions = [nf for func in bvf for nf in func.nested_functions] + bvf
+        return BitVecFunc(raw, func_name="Hybrid", nested_functions=nested_functions)
+
+    return BitVec(z3.If(a.raw, b.raw, c.raw), union)
+
+
+def UGT(a: BitVec, b: BitVec) -> Bool:
+    """Create an unsigned greater than expression.
+
+    :param a:
+    :param b:
+    :return:
+    """
+    return _comparison_helper(a, b, z3.UGT, default_value=False, inputs_equal=False)
+
+
+def UGE(a: BitVec, b: BitVec) -> Bool:
+    """Create an unsigned greater or equals expression.
+
+    :param a:
+    :param b:
+    :return:
+    """
+    return Or(UGT(a, b), a == b)
+
+
+def ULT(a: BitVec, b: BitVec) -> Bool:
+    """Create an unsigned less than expression.
+
+    :param a:
+    :param b:
+    :return:
+    """
+    return _comparison_helper(a, b, z3.ULT, default_value=False, inputs_equal=False)
+
+
+def ULE(a: BitVec, b: BitVec) -> Bool:
+    """Create an unsigned less than expression.
+
+    :param a:
+    :param b:
+    :return:
+    """
+    return Or(ULT(a, b), a == b)
+
+
+@overload
+def Concat(*args: List[BitVec]) -> BitVec:
+    ...
+
+
+@overload
+def Concat(*args: BitVec) -> BitVec:
+    ...
+
+
+def Concat(*args: Union[BitVec, List[BitVec]]) -> BitVec:
+    """Create a concatenation expression.
+
+    :param args:
+    :return:
+    """
+    # The following statement is used if a list is provided as an argument to concat
+    if len(args) == 1 and isinstance(args[0], list):
+        bvs = args[0]  # type: List[BitVec]
+    else:
+        bvs = cast(List[BitVec], args)
+
+    nraw = z3.Concat([a.raw for a in bvs])
+    annotations = set()  # type: Annotations
+
+    nested_functions = []  # type: List[BitVecFunc]
+    for bv in bvs:
+        annotations = annotations.union(bv.annotations)
+        if isinstance(bv, BitVecFunc):
+            nested_functions += bv.nested_functions
+            nested_functions += [bv]
+
+    if nested_functions:
+        return BitVecFunc(
+            raw=nraw,
+            func_name="Hybrid",
+            input_=BitVec(z3.BitVec("", 256), annotations=annotations),
+            nested_functions=nested_functions,
+        )
+
+    return BitVec(nraw, annotations)
+
+
+def Extract(high: int, low: int, bv: BitVec) -> BitVec:
+    """Create an extract expression.
+
+    :param high:
+    :param low:
+    :param bv:
+    :return:
+    """
+    raw = z3.Extract(high, low, bv.raw)
+    if isinstance(bv, BitVecFunc):
+        input_string = ""
+        # Is there a better value to set func_name and input to in this case?
+        return BitVecFunc(
+            raw=raw,
+            func_name="Hybrid",
+            input_=BitVec(z3.BitVec(input_string, 256), annotations=bv.annotations),
+            nested_functions=bv.nested_functions + [bv],
+        )
+
+    return BitVec(raw, annotations=bv.annotations)
+
+
+def URem(a: BitVec, b: BitVec) -> BitVec:
+    """Create an unsigned remainder expression.
+
+    :param a:
+    :param b:
+    :return:
+    """
+    return _arithmetic_helper(a, b, z3.URem)
+
+
+def SRem(a: BitVec, b: BitVec) -> BitVec:
+    """Create a signed remainder expression.
+
+    :param a:
+    :param b:
+    :return:
+    """
+    return _arithmetic_helper(a, b, z3.SRem)
+
+
+def UDiv(a: BitVec, b: BitVec) -> BitVec:
+    """Create an unsigned division expression.
+
+    :param a:
+    :param b:
+    :return:
+    """
+    return _arithmetic_helper(a, b, z3.UDiv)
+
+
+def Sum(*args: BitVec) -> BitVec:
+    """Create sum expression.
+
+    :return:
+    """
+    raw = z3.Sum([a.raw for a in args])
+    annotations = set()  # type: Annotations
+    bitvecfuncs = []
+
+    for bv in args:
+        annotations = annotations.union(bv.annotations)
+        if isinstance(bv, BitVecFunc):
+            bitvecfuncs.append(bv)
+
+    nested_functions = [
+        nf for func in bitvecfuncs for nf in func.nested_functions
+    ] + bitvecfuncs
+
+    if len(bitvecfuncs) >= 2:
+        return BitVecFunc(
+            raw=raw,
+            func_name="Hybrid",
+            input_=None,
+            annotations=annotations,
+            nested_functions=nested_functions,
+        )
+    elif len(bitvecfuncs) == 1:
+        return BitVecFunc(
+            raw=raw,
+            func_name=bitvecfuncs[0].func_name,
+            input_=bitvecfuncs[0].input_,
+            annotations=annotations,
+            nested_functions=nested_functions,
+        )
+
+    return BitVec(raw, annotations)
+
+
+def BVAddNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
+    """Creates predicate that verifies that the addition doesn't overflow.
+
+    :param a:
+    :param b:
+    :param signed:
+    :return:
+    """
+    if not isinstance(a, BitVec):
+        a = BitVec(z3.BitVecVal(a, 256))
+    if not isinstance(b, BitVec):
+        b = BitVec(z3.BitVecVal(b, 256))
+    return Bool(z3.BVAddNoOverflow(a.raw, b.raw, signed))
+
+
+def BVMulNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
+    """Creates predicate that verifies that the multiplication doesn't
+    overflow.
+
+    :param a:
+    :param b:
+    :param signed:
+    :return:
+    """
+    if not isinstance(a, BitVec):
+        a = BitVec(z3.BitVecVal(a, 256))
+    if not isinstance(b, BitVec):
+        b = BitVec(z3.BitVecVal(b, 256))
+    return Bool(z3.BVMulNoOverflow(a.raw, b.raw, signed))
+
+
+def BVSubNoUnderflow(
+    a: Union[BitVec, int], b: Union[BitVec, int], signed: bool
+) -> Bool:
+    """Creates predicate that verifies that the subtraction doesn't overflow.
+
+    :param a:
+    :param b:
+    :param signed:
+    :return:
+    """
+    if not isinstance(a, BitVec):
+        a = BitVec(z3.BitVecVal(a, 256))
+    if not isinstance(b, BitVec):
+        b = BitVec(z3.BitVecVal(b, 256))
+
+    return Bool(z3.BVSubNoUnderflow(a.raw, b.raw, signed))

mythril/laser/smt/bitvecfunc.py

@@ -1,11 +1,10 @@
-from typing import Optional, Union, cast, Callable
-
+import operator
+from itertools import product
+from typing import Optional, Union, cast, Callable, List
 import z3
 
-from mythril.laser.smt.bitvec import BitVec, Bool, And, Annotations
-from mythril.laser.smt.bool import Or
-
-import operator
+from mythril.laser.smt.bitvec import BitVec, Annotations
+from mythril.laser.smt.bool import Or, Bool, And
 
 
 def _arithmetic_helper(
@@ -26,18 +25,19 @@ def _arithmetic_helper(
     union = a.annotations.union(b.annotations)
 
     if isinstance(b, BitVecFunc):
-        # TODO: Find better value to set input and name to in this case?
-        input_string = "MisleadingNotationop(invhash({}) {} invhash({})".format(
-            hash(a), operation, hash(b)
-        )
         return BitVecFunc(
             raw=raw,
             func_name="Hybrid",
-            input_=BitVec(z3.BitVec(input_string, 256), annotations=union),
+            input_=BitVec(z3.BitVec("", 256), annotations=union),
+            nested_functions=a.nested_functions + b.nested_functions + [a, b],
         )
 
     return BitVecFunc(
-        raw=raw, func_name=a.func_name, input_=a.input_, annotations=union
+        raw=raw,
+        func_name=a.func_name,
+        input_=a.input_,
+        annotations=union,
+        nested_functions=a.nested_functions + [a],
     )
 
 
@@ -62,23 +62,58 @@ def _comparison_helper(
     union = a.annotations.union(b.annotations)
 
     if not a.symbolic and not b.symbolic:
+        if operation == z3.UGT:
+            operation = operator.gt
+        if operation == z3.ULT:
+            operation = operator.lt
         return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union)
-
     if (
         not isinstance(b, BitVecFunc)
         or not a.func_name
         or not a.input_
         or not a.func_name == b.func_name
+        or str(operation) not in ("<built-in function eq>", "<built-in function ne>")
     ):
         return Bool(z3.BoolVal(default_value), annotations=union)
 
+    condition = True
+    for a_nest, b_nest in product(a.nested_functions, b.nested_functions):
+        if a_nest.func_name != b_nest.func_name:
+            continue
+        if a_nest.func_name == "Hybrid":
+            continue
+        # a.input (eq/neq) b.input ==> a == b
+        if inputs_equal:
+            condition = z3.And(
+                condition,
+                z3.Or(
+                    z3.Not((a_nest.input_ == b_nest.input_).raw),
+                    (a_nest.raw == b_nest.raw),
+                ),
+                z3.Or(
+                    z3.Not((a_nest.raw == b_nest.raw)),
+                    (a_nest.input_ == b_nest.input_).raw,
+                ),
+            )
+        else:
+            condition = z3.And(
+                condition,
+                z3.Or(
+                    z3.Not((a_nest.input_ != b_nest.input_).raw),
+                    (a_nest.raw == b_nest.raw),
+                ),
+                z3.Or(
+                    z3.Not((a_nest.raw == b_nest.raw)),
+                    (a_nest.input_ != b_nest.input_).raw,
+                ),
+            )
+
     return And(
         Bool(cast(z3.BoolRef, operation(a.raw, b.raw)), annotations=union),
+        Bool(condition) if b.nested_functions else Bool(True),
         a.input_ == b.input_ if inputs_equal else a.input_ != b.input_,
     )
 
-    return a.input_ == b.input_
-
 
 class BitVecFunc(BitVec):
     """A bit vector function symbol. Used in place of functions like sha3."""
@@ -89,6 +124,7 @@ class BitVecFunc(BitVec):
         func_name: Optional[str],
         input_: "BitVec" = None,
         annotations: Optional[Annotations] = None,
+        nested_functions: Optional[List["BitVecFunc"]] = None,
     ):
         """
 
@@ -100,6 +136,10 @@ class BitVecFunc(BitVec):
 
         self.func_name = func_name
         self.input_ = input_
+        self.nested_functions = nested_functions or []
+        self.nested_functions = list(dict.fromkeys(self.nested_functions))
+        if isinstance(input_, BitVecFunc):
+            self.nested_functions.extend(input_.nested_functions)
         super().__init__(raw, annotations)
 
     def __add__(self, other: Union[int, "BitVec"]) -> "BitVecFunc":

mythril/mythril/mythril_analyzer.py

@@ -10,6 +10,7 @@ from mythril.support.source_support import Source
 from mythril.support.loader import DynLoader
 from mythril.analysis.symbolic import SymExecWrapper
 from mythril.analysis.callgraph import generate_graph
+from mythril.analysis.analysis_args import analysis_args
 from mythril.analysis.traceexplore import get_serializable_statespace
 from mythril.analysis.security import fire_lasers, retrieve_callback_issues
 from mythril.analysis.report import Report, Issue
@@ -39,6 +40,9 @@ class MythrilAnalyzer:
         create_timeout: Optional[int] = None,
         enable_iprof: bool = False,
         disable_dependency_pruning: bool = False,
+        solver_timeout: Optional[int] = None,
+        enable_coverage_strategy: bool = False,
+        custom_modules_directory: str = "",
     ):
         """
 
@@ -59,6 +63,11 @@ class MythrilAnalyzer:
         self.create_timeout = create_timeout
         self.enable_iprof = enable_iprof
         self.disable_dependency_pruning = disable_dependency_pruning
+        self.enable_coverage_strategy = enable_coverage_strategy
+        self.custom_modules_directory = custom_modules_directory
+
+        analysis_args.set_loop_bound(loop_bound)
+        analysis_args.set_solver_timeout(solver_timeout)
 
     def dump_statespace(self, contract: EVMContract = None) -> str:
         """
@@ -81,6 +90,8 @@ class MythrilAnalyzer:
             enable_iprof=self.enable_iprof,
             disable_dependency_pruning=self.disable_dependency_pruning,
             run_analysis_modules=False,
+            enable_coverage_strategy=self.enable_coverage_strategy,
+            custom_modules_directory=self.custom_modules_directory,
         )
 
         return get_serializable_statespace(sym)
@@ -116,6 +127,8 @@ class MythrilAnalyzer:
             enable_iprof=self.enable_iprof,
             disable_dependency_pruning=self.disable_dependency_pruning,
             run_analysis_modules=False,
+            enable_coverage_strategy=self.enable_coverage_strategy,
+            custom_modules_directory=self.custom_modules_directory,
         )
         return generate_graph(sym, physics=enable_physics, phrackify=phrackify)
 
@@ -153,18 +166,23 @@ class MythrilAnalyzer:
                     compulsory_statespace=False,
                     enable_iprof=self.enable_iprof,
                     disable_dependency_pruning=self.disable_dependency_pruning,
+                    enable_coverage_strategy=self.enable_coverage_strategy,
+                    custom_modules_directory=self.custom_modules_directory,
                 )
-
-                issues = fire_lasers(sym, modules)
+                issues = fire_lasers(sym, modules, self.custom_modules_directory)
             except KeyboardInterrupt:
                 log.critical("Keyboard Interrupt")
-                issues = retrieve_callback_issues(modules)
+                issues = retrieve_callback_issues(
+                    modules, self.custom_modules_directory
+                )
             except Exception:
                 log.critical(
                     "Exception occurred, aborting analysis. Please report this issue to the Mythril GitHub page.\n"
                     + traceback.format_exc()
                 )
-                issues = retrieve_callback_issues(modules)
+                issues = retrieve_callback_issues(
+                    modules, self.custom_modules_directory
+                )
                 exceptions.append(traceback.format_exc())
             for issue in issues:
                 issue.add_code_info(contract)

mythril/mythril/mythril_disassembler.py

@@ -1,10 +1,10 @@
 import logging
 import re
 import solc
+import solcx
 import os
 
 from ethereum import utils
-from solc.exceptions import SolcError
 from typing import List, Tuple, Optional
 from mythril.ethereum import util
 from mythril.ethereum.interface.rpc.client import EthJsonRpc
@@ -30,11 +30,11 @@ class MythrilDisassembler:
         self,
         eth: Optional[EthJsonRpc] = None,
         solc_version: str = None,
-        solc_args: str = None,
+        solc_settings_json: str = None,
         enable_online_lookup: bool = False,
     ) -> None:
         self.solc_binary = self._init_solc_binary(solc_version)
-        self.solc_args = solc_args
+        self.solc_settings_json = solc_settings_json
         self.eth = eth
         self.enable_online_lookup = enable_online_lookup
         self.sigs = signatures.SignatureDB(enable_online_lookup=enable_online_lookup)
@@ -63,15 +63,24 @@ class MythrilDisassembler:
             solc_binary = os.environ.get("SOLC") or "solc"
         else:
             solc_binary = util.solc_exists(version)
-            if solc_binary:
+            if solc_binary and solc_binary != util.solc_exists(
+                "default_ubuntu_version"
+            ):
                 log.info("Given version is already installed")
             else:
                 try:
+                    if version.startswith("0.4"):
                         solc.install_solc("v" + version)
+                    else:
+                        solcx.install_solc("v" + version)
                     solc_binary = util.solc_exists(version)
                     if not solc_binary:
-                        raise SolcError()
-                except SolcError:
+                        raise solc.exceptions.SolcError()
+                except solc.exceptions.SolcError:
+                    raise CriticalError(
+                        "There was an error when trying to install the specified solc version"
+                    )
+                except solcx.exceptions.SolcError:
                     raise CriticalError(
                         "There was an error when trying to install the specified solc version"
                     )
@@ -163,13 +172,15 @@ class MythrilDisassembler:
             try:
                 # import signatures from solidity source
                 self.sigs.import_solidity_file(
-                    file, solc_binary=self.solc_binary, solc_args=self.solc_args
+                    file,
+                    solc_binary=self.solc_binary,
+                    solc_settings_json=self.solc_settings_json,
                 )
                 if contract_name is not None:
                     contract = SolidityContract(
                         input_file=file,
                         name=contract_name,
-                        solc_args=self.solc_args,
+                        solc_settings_json=self.solc_settings_json,
                         solc_binary=self.solc_binary,
                     )
                     self.contracts.append(contract)
@@ -177,7 +188,7 @@ class MythrilDisassembler:
                 else:
                     for contract in get_contracts_from_file(
                         input_file=file,
-                        solc_args=self.solc_args,
+                        solc_settings_json=self.solc_settings_json,
                         solc_binary=self.solc_binary,
                     ):
                         self.contracts.append(contract)

mythril/mythx/__init__.py

@@ -0,0 +1,111 @@
+import sys
+
+import os
+import time
+
+from mythx_models.exceptions import MythXAPIError
+from typing import List, Dict, Any
+
+from mythril.analysis.report import Issue, Report
+from mythril.solidity.soliditycontract import SolidityContract
+
+from pythx import Client
+
+import logging
+
+log = logging.getLogger(__name__)
+
+TRIAL_ETH_ADDRESS = "0x0000000000000000000000000000000000000000"
+TRIAL_PASSWORD = "trial"
+
+
+def analyze(contracts: List[SolidityContract], analysis_mode: str = "quick") -> Report:
+    """
+    Analyze contracts via the MythX API.
+
+    :param contracts: List of solidity contracts to analyze
+    :param analysis_mode: The mode to submit the analysis request with. "quick" or "full" (default: "quick")
+    :return: Report with analyzed contracts
+    """
+    assert analysis_mode in ("quick", "full"), "analysis_mode must be 'quick' or 'full'"
+
+    c = Client(
+        eth_address=os.environ.get("MYTHX_ETH_ADDRESS", TRIAL_ETH_ADDRESS),
+        password=os.environ.get("MYTHX_PASSWORD", TRIAL_PASSWORD),
+    )
+
+    if c.eth_address == TRIAL_ETH_ADDRESS:
+        print(
+            "You are currently running MythX in Trial mode. This mode reports only a partial analysis of your smart contracts, limited to three vulnerabilities. To get a more complete analysis, sign up for a free account at https://mythx.io."
+        )
+
+    issues = []  # type: List[Issue]
+
+    # TODO: Analyze multiple contracts asynchronously.
+    for contract in contracts:
+        source_codes = {}
+        source_list = []
+        sources = {}  # type: Dict[str, Any]
+        main_source = None
+
+        try:
+            main_source = contract.input_file
+            for solidity_file in contract.solidity_files:
+                source_codes[solidity_file.filename] = solidity_file.data
+            for filename in contract.solc_json["sources"].keys():
+                sources[filename] = {}
+                if source_codes[filename]:
+                    sources[filename]["source"] = source_codes[filename]
+                sources[filename]["ast"] = contract.solc_json["sources"][filename][
+                    "ast"
+                ]
+
+                source_list.append(filename)
+
+            source_list.sort(
+                key=lambda fname: contract.solc_json["sources"][fname]["id"]
+            )
+        except AttributeError:
+            # No solidity file
+            pass
+
+        assert contract.creation_code, "Creation bytecode must exist."
+        try:
+            resp = c.analyze(
+                contract_name=contract.name,
+                analysis_mode=analysis_mode,
+                bytecode=contract.creation_code or None,
+                deployed_bytecode=contract.code or None,
+                sources=sources or None,
+                main_source=main_source,
+                source_list=source_list or None,
+            )
+        except MythXAPIError as e:
+            log.critical(e)
+
+        while not c.analysis_ready(resp.uuid):
+            log.info(c.status(resp.uuid).analysis)
+            time.sleep(5)
+
+        for issue in c.report(resp.uuid):
+            issue = Issue(
+                contract=contract.name,
+                function_name=None,
+                address=issue.locations[0].source_map.components[0].offset
+                if issue.locations
+                else -1,
+                swc_id=issue.swc_id[4:] or "None",  # remove 'SWC-' prefix
+                title=issue.swc_title,
+                bytecode=contract.creation_code,
+                severity=issue.severity.capitalize(),
+                description_head=issue.description_short,
+                description_tail=issue.description_long,
+            )
+            issue.add_code_info(contract)
+            issues.append(issue)
+
+    report = Report(contracts=contracts)
+    for issue in issues:
+        report.append_issue(issue)
+
+    return report

mythril/solidity/soliditycontract.py

@@ -44,23 +44,28 @@ class SourceCodeInfo:
         self.solc_mapping = mapping
 
 
-def get_contracts_from_file(input_file, solc_args=None, solc_binary="solc"):
+def get_contracts_from_file(input_file, solc_settings_json=None, solc_binary="solc"):
     """
 
     :param input_file:
-    :param solc_args:
+    :param solc_settings_json:
     :param solc_binary:
     """
-    data = get_solc_json(input_file, solc_args=solc_args, solc_binary=solc_binary)
+    data = get_solc_json(
+        input_file, solc_settings_json=solc_settings_json, solc_binary=solc_binary
+    )
 
     try:
-        for key, contract in data["contracts"].items():
-            filename, name = key.split(":")
-            if filename == input_file and len(contract["bin-runtime"]):
+        for contract_name in data["contracts"][input_file].keys():
+            if len(
+                data["contracts"][input_file][contract_name]["evm"]["deployedBytecode"][
+                    "object"
+                ]
+            ):
                 yield SolidityContract(
                     input_file=input_file,
-                    name=name,
-                    solc_args=solc_args,
+                    name=contract_name,
+                    solc_settings_json=solc_settings_json,
                     solc_binary=solc_binary,
                 )
     except KeyError:
@@ -70,16 +75,22 @@ def get_contracts_from_file(input_file, solc_args=None, solc_binary="solc"):
 class SolidityContract(EVMContract):
     """Representation of a Solidity contract."""
 
-    def __init__(self, input_file, name=None, solc_args=None, solc_binary="solc"):
-        data = get_solc_json(input_file, solc_args=solc_args, solc_binary=solc_binary)
+    def __init__(
+        self, input_file, name=None, solc_settings_json=None, solc_binary="solc"
+    ):
+        data = get_solc_json(
+            input_file, solc_settings_json=solc_settings_json, solc_binary=solc_binary
+        )
 
         self.solidity_files = []
+        self.solc_json = data
+        self.input_file = input_file
 
-        for filename in data["sourceList"]:
+        for filename, contract in data["sources"].items():
             with open(filename, "r", encoding="utf-8") as file:
                 code = file.read()
                 full_contract_src_maps = self.get_full_contract_src_maps(
-                    data["sources"][filename]["AST"]
+                    contract["ast"]
                 )
                 self.solidity_files.append(
                     SolidityFile(filename, code, full_contract_src_maps)
@@ -91,32 +102,28 @@ class SolidityContract(EVMContract):
         srcmap_constructor = []
         srcmap = []
         if name:
-            for key, contract in sorted(data["contracts"].items()):
-                filename, _name = key.split(":")
-
-                if (
-                    filename == input_file
-                    and name == _name
-                    and len(contract["bin-runtime"])
-                ):
-                    code = contract["bin-runtime"]
-                    creation_code = contract["bin"]
-                    srcmap = contract["srcmap-runtime"].split(";")
-                    srcmap_constructor = contract["srcmap"].split(";")
+            contract = data["contracts"][input_file][name]
+            if len(contract["evm"]["deployedBytecode"]["object"]):
+                code = contract["evm"]["deployedBytecode"]["object"]
+                creation_code = contract["evm"]["bytecode"]["object"]
+                srcmap = contract["evm"]["deployedBytecode"]["sourceMap"].split(";")
+                srcmap_constructor = contract["evm"]["bytecode"]["sourceMap"].split(";")
                 has_contract = True
-                    break
 
         # If no contract name is specified, get the last bytecode entry for the input file
 
         else:
-            for key, contract in sorted(data["contracts"].items()):
-                filename, name = key.split(":")
-
-                if filename == input_file and len(contract["bin-runtime"]):
-                    code = contract["bin-runtime"]
-                    creation_code = contract["bin"]
-                    srcmap = contract["srcmap-runtime"].split(";")
-                    srcmap_constructor = contract["srcmap"].split(";")
+            for contract_name, contract in sorted(
+                data["contracts"][input_file].items()
+            ):
+                if len(contract["evm"]["deployedBytecode"]["object"]):
+                    name = contract_name
+                    code = contract["evm"]["deployedBytecode"]["object"]
+                    creation_code = contract["evm"]["bytecode"]["object"]
+                    srcmap = contract["evm"]["deployedBytecode"]["sourceMap"].split(";")
+                    srcmap_constructor = contract["evm"]["bytecode"]["sourceMap"].split(
+                        ";"
+                    )
                     has_contract = True
 
         if not has_contract:
@@ -139,8 +146,8 @@ class SolidityContract(EVMContract):
         :return: The source maps
         """
         source_maps = set()
-        for child in ast["children"]:
-            if "contractKind" in child["attributes"]:
+        for child in ast["nodes"]:
+            if child.get("contractKind"):
                 source_maps.add(child["src"])
         return source_maps
 

mythril/support/loader.py

@@ -3,6 +3,11 @@ and dependencies."""
 from mythril.disassembler.disassembly import Disassembly
 import logging
 import re
+import functools
+from mythril.ethereum.interface.rpc.client import EthJsonRpc
+from typing import Optional
+
+LRU_CACHE_SIZE = 4096
 
 log = logging.getLogger(__name__)
 
@@ -10,7 +15,9 @@ log = logging.getLogger(__name__)
 class DynLoader:
     """The dynamic loader class."""
 
-    def __init__(self, eth, contract_loading=True, storage_loading=True):
+    def __init__(
+        self, eth: Optional[EthJsonRpc], contract_loading=True, storage_loading=True
+    ):
         """
 
         :param eth:
@@ -18,11 +25,11 @@ class DynLoader:
         :param storage_loading:
         """
         self.eth = eth
-        self.storage_cache = {}
         self.contract_loading = contract_loading
         self.storage_loading = storage_loading
 
-    def read_storage(self, contract_address: str, index: int):
+    @functools.lru_cache(LRU_CACHE_SIZE)
+    def read_storage(self, contract_address: str, index: int) -> str:
         """
 
         :param contract_address:
@@ -30,43 +37,28 @@ class DynLoader:
         :return:
         """
         if not self.storage_loading:
-            raise Exception(
+            raise ValueError(
                 "Cannot load from the storage when the storage_loading flag is false"
             )
+        if not self.eth:
+            raise ValueError("Cannot load from the storage when eth is None")
 
-        try:
-            contract_ref = self.storage_cache[contract_address]
-            data = contract_ref[index]
-
-        except KeyError:
-
-            self.storage_cache[contract_address] = {}
-
-            data = self.eth.eth_getStorageAt(
+        return self.eth.eth_getStorageAt(
             contract_address, position=index, block="latest"
         )
 
-            self.storage_cache[contract_address][index] = data
-
-        except IndexError:
-
-            data = self.eth.eth_getStorageAt(
-                contract_address, position=index, block="latest"
-            )
-
-            self.storage_cache[contract_address][index] = data
-
-        return data
-
-    def dynld(self, dependency_address):
+    @functools.lru_cache(LRU_CACHE_SIZE)
+    def dynld(self, dependency_address: str) -> Optional[Disassembly]:
         """
         :param dependency_address:
         :return:
         """
         if not self.contract_loading:
             raise ValueError("Cannot load contract when contract_loading flag is false")
+        if not self.eth:
+            raise ValueError("Cannot load from the storage when eth is None")
 
-        log.debug("Dynld at contract " + dependency_address)
+        log.debug("Dynld at contract %s", dependency_address)
 
         # Ensure that dependency_address is the correct length, with 0s prepended as needed.
         dependency_address = (
@@ -81,7 +73,7 @@ class DynLoader:
         else:
             return None
 
-        log.debug("Dependency address: " + dependency_address)
+        log.debug("Dependency address: %s", dependency_address)
 
         code = self.eth.eth_getCode(dependency_address)
 

mythril/support/signatures.py

@@ -1,5 +1,6 @@
 """The Mythril function signature database."""
 import functools
+import json
 import logging
 import multiprocessing
 import os
@@ -9,6 +10,7 @@ from collections import defaultdict
 from subprocess import PIPE, Popen
 from typing import List, Set, DefaultDict, Dict
 
+from mythril.ethereum.util import get_solc_json
 from mythril.exceptions import CompilerError
 
 log = logging.getLogger(__name__)
@@ -231,53 +233,20 @@ class SignatureDB(object, metaclass=Singleton):
             return []
 
     def import_solidity_file(
-        self, file_path: str, solc_binary: str = "solc", solc_args: str = None
+        self, file_path: str, solc_binary: str = "solc", solc_settings_json: str = None
     ):
         """Import Function Signatures from solidity source files.
 
         :param solc_binary:
-        :param solc_args:
+        :param solc_settings_json:
         :param file_path: solidity source code file path
         :return:
         """
-        cmd = [solc_binary, "--hashes", file_path]
-        if solc_args:
-            cmd.extend(solc_args.split())
+        solc_json = get_solc_json(file_path, solc_binary, solc_settings_json)
 
-        try:
-            p = Popen(cmd, stdout=PIPE, stderr=PIPE)
-            stdout, stderr = p.communicate()
-            ret = p.returncode
-
-            if ret != 0:
-                raise CompilerError(
-                    "Solc has experienced a fatal error (code {}).\n\n{}".format(
-                        ret, stderr.decode("utf-8")
-                    )
-                )
-        except FileNotFoundError:
-            raise CompilerError(
-                (
-                    "Compiler not found. Make sure that solc is installed and in PATH, "
-                    "or the SOLC environment variable is set."
-                )
-            )
-
-        stdout = stdout.decode("unicode_escape").split("\n")
-        for line in stdout:
-            # the ':' need not be checked but just to be sure
-            if all(map(lambda x: x in line, ["(", ")", ":"])):
-                solc_bytes = "0x" + line.split(":")[0]
-                solc_text = line.split(":")[1].strip()
-                self.solidity_sigs[solc_bytes].append(solc_text)
-        log.debug(
-            "Signatures: found %d signatures after parsing" % len(self.solidity_sigs)
-        )
-
-        # update DB with what we've found
-        for byte_sig, text_sigs in self.solidity_sigs.items():
-            for text_sig in text_sigs:
-                self.add(byte_sig, text_sig)
+        for contract in solc_json["contracts"][file_path].values():
+            for name, hash in contract["evm"]["methodIdentifiers"].items():
+                self.add("0x" + hash, name)
 
     @staticmethod
     def lookup_online(byte_sig: str, timeout: int, proxies=None) -> List[str]:

requirements.txt

@@ -1,7 +1,7 @@
 coloredlogs>=10.0
 configparser>=3.5.0
 coverage
-py_ecc==1.4.2
+py_ecc==1.6.0
 eth_abi==1.3.0
 eth-account>=0.1.0a2,<=0.3.0
 ethereum>=2.3.2
@@ -12,19 +12,21 @@ eth-keys>=0.2.0b3,<0.3.0
 eth-rlp>=0.1.0
 eth-tester==0.1.0b32
 eth-typing>=2.0.0
-eth-utils>=1.0.1
 jinja2>=2.9
 mock
 persistent>=4.2.0
 plyvel
 py-flags
+py-solc-x==0.6.0
 py-solc
 pytest>=3.6.0
 pytest-cov
 pytest_mock
-requests
+requests>=2.22.0
 rlp>=1.0.1
+semantic_version==2.8.1
 transaction>=2.2.1
 z3-solver>=4.8.5.0
 pysha3
 matplotlib
+pythx

setup.py

@@ -25,14 +25,15 @@ REQUIRES_PYTHON = ">=3.5.0"
 # What packages are required for this module to be executed?
 REQUIRED = [
     "coloredlogs>=10.0",
-    "py_ecc==1.4.2",
+    "py_ecc==1.6.0",
     "ethereum>=2.3.2",
     "z3-solver>=4.8.5.0",
-    "requests",
+    "requests>=2.22.0",
     "py-solc",
+    "py-solc-x==0.6.0",
+    "semantic_version==2.8.1",
     "plyvel",
     "eth_abi==1.3.0",
-    "eth-utils>=1.0.1",
     "eth-account>=0.1.0a2,<=0.3.0",
     "eth-hash>=0.1.0",
     "eth-keyfile>=0.5.1",
@@ -50,6 +51,7 @@ REQUIRED = [
     "persistent>=4.2.0",
     "ethereum-input-decoder>=0.2.2",
     "matplotlib",
+    "pythx",
 ]
 
 TESTS_REQUIRE = ["mypy", "pytest>=3.6.0", "pytest_mock", "pytest-cov"]

tests/instructions/create_test.py

@@ -0,0 +1,72 @@
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.machine_state import MachineState
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.instructions import Instruction
+from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
+from mythril.laser.ethereum.state.calldata import ConcreteCalldata
+from mythril.laser.ethereum.svm import LaserEVM
+from mythril.laser.smt import symbol_factory
+
+# contract A {
+#    uint256 public val = 10;
+# }
+contract_init_code = "6080604052600a600055348015601457600080fd5b506084806100236000396000f3fe6080604052348015600f57600080fd5b506004361060285760003560e01c80633c6bb43614602d575b600080fd5b60336049565b6040518082815260200191505060405180910390f35b6000548156fea265627a7a72315820d3cfe7a909450a953cbd7e47d8c17477f2609baa5208d043e965efec69d1ed9864736f6c634300050b0032"
+contract_runtime_code = "6080604052348015600f57600080fd5b506004361060285760003560e01c80633c6bb43614602d575b600080fd5b60336049565b6040518082815260200191505060405180910390f35b6000548156fea265627a7a72315820d3cfe7a909450a953cbd7e47d8c17477f2609baa5208d043e965efec69d1ed9864736f6c634300050b0032"
+
+last_state = None
+created_contract_account = None
+
+
+def execute_create():
+    global last_state
+    global created_contract_account
+    if not last_state and not created_contract_account:
+        code_raw = []
+        for i in range(len(contract_init_code) // 2):
+            code_raw.append(int(contract_init_code[2 * i : 2 * (i + 1)], 16))
+        calldata = ConcreteCalldata(0, code_raw)
+
+        world_state = WorldState()
+        account = world_state.create_account(balance=1000000, address=101)
+        account.code = Disassembly("60a760006000f000")
+        environment = Environment(account, None, calldata, None, None, None)
+        og_state = GlobalState(
+            world_state, environment, None, MachineState(gas_limit=8000000)
+        )
+        og_state.transaction_stack.append(
+            (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
+        )
+
+        laser = LaserEVM()
+        states = [og_state]
+        last_state = og_state
+        for state in states:
+            new_states, op_code = laser.execute_state(state)
+            last_state = state
+            if op_code == "STOP":
+                break
+            states.extend(new_states)
+
+        created_contract_address = last_state.mstate.stack[-1].value
+        created_contract_account = last_state.world_state.accounts[
+            created_contract_address
+        ]
+
+    return last_state, created_contract_account
+
+
+def test_create_has_code():
+    last_state, created_contract_account = execute_create()
+    assert created_contract_account.code.bytecode == contract_runtime_code
+
+
+def test_create_has_storage():
+    last_state, created_contract_account = execute_create()
+    storage = created_contract_account.storage
+    # From contract, val = 10.
+    assert storage[symbol_factory.BitVecVal(0, 256)] == symbol_factory.BitVecVal(
+        10, 256
+    )

tests/instructions/extcodehash_test.py

@@ -0,0 +1,48 @@
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.machine_state import MachineState
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.instructions import Instruction
+from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
+
+from mythril.support.support_utils import get_code_hash
+
+from mythril.laser.smt import symbol_factory
+
+# Arrange
+world_state = WorldState()
+account = world_state.create_account(balance=10, address=101)
+account.code = Disassembly("60606040")
+world_state.create_account(balance=10, address=1000)
+environment = Environment(account, None, None, None, None, None)
+og_state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000))
+og_state.transaction_stack.append(
+    (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
+)
+
+instruction = Instruction("extcodehash", dynamic_loader=None)
+
+
+def test_extcodehash_no_account():
+
+    # If account does not exist, return 0
+    og_state.mstate.stack = [symbol_factory.BitVecVal(1, 256)]
+    new_state = instruction.evaluate(og_state)[0]
+    assert new_state.mstate.stack[-1] == 0
+
+
+def test_extcodehash_no_code():
+
+    # If account code does not exist, return hash of empty set.
+    og_state.mstate.stack = [symbol_factory.BitVecVal(1000, 256)]
+    new_state = instruction.evaluate(og_state)[0]
+    assert hex(new_state.mstate.stack[-1].value) == get_code_hash("")
+
+
+def test_extcodehash_return_hash():
+    # If account code exists, return hash of the code.
+    og_state.mstate.stack = [symbol_factory.BitVecVal(101, 256)]
+    new_state = instruction.evaluate(og_state)[0]
+    assert hex(new_state.mstate.stack[-1].value) == get_code_hash("60606040")

tests/instructions/static_call_test.py

@@ -0,0 +1,124 @@
+import pytest
+from mock import patch
+
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.smt import symbol_factory
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.machine_state import MachineState
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.instructions import Instruction
+from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
+from mythril.laser.ethereum.call import SymbolicCalldata
+from mythril.laser.ethereum.transaction import TransactionStartSignal
+
+from mythril.laser.ethereum.evm_exceptions import WriteProtection
+
+
+def get_global_state():
+    active_account = Account("0x0", code=Disassembly("60606040"))
+    environment = Environment(
+        active_account, None, SymbolicCalldata("2"), None, None, None
+    )
+    world_state = WorldState()
+    world_state.put_account(active_account)
+    state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000))
+    state.transaction_stack.append(
+        (MessageCallTransaction(world_state=world_state, gas_limit=8000000), None)
+    )
+    return state
+
+
+@patch(
+    "mythril.laser.ethereum.instructions.get_call_parameters",
+    return_value=(
+        "0",
+        Account(code=Disassembly(code="0x00"), address="0x19"),
+        0,
+        0,
+        0,
+        0,
+        0,
+    ),
+)
+def test_staticcall(f1):
+    # Arrange
+    state = get_global_state()
+    state.mstate.stack = [10, 10, 10, 10, 10, 10, 10, 10, 0]
+    instruction = Instruction("staticcall", dynamic_loader=None)
+
+    # Act and Assert
+    with pytest.raises(TransactionStartSignal) as ts:
+        instruction.evaluate(state)
+    assert ts.value.transaction.static
+    assert ts.value.transaction.initial_global_state().environment.static
+
+
+test_data = (
+    "suicide",
+    "create",
+    "create2",
+    "log0",
+    "log1",
+    "log2",
+    "log3",
+    "log4",
+    "sstore",
+)
+
+
+@pytest.mark.parametrize("input", test_data)
+def test_staticness(input):
+    # Arrange
+    state = get_global_state()
+    state.environment.static = True
+    state.mstate.stack = []
+    instruction = Instruction(input, dynamic_loader=None)
+
+    # Act and Assert
+    with pytest.raises(WriteProtection):
+        instruction.evaluate(state)
+
+
+test_data_call = ((0, True), (100, False))
+
+
+@pytest.mark.parametrize("input, success", test_data_call)
+@patch("mythril.laser.ethereum.instructions.get_call_parameters")
+def test_staticness_call_concrete(f1, input, success):
+    # Arrange
+    state = get_global_state()
+    state.environment.static = True
+    state.mstate.stack = []
+    code = Disassembly(code="616263")
+    f1.return_value = ("0", Account(code=code, address="0x19"), 0, input, 0, 0, 0)
+    instruction = Instruction("call", dynamic_loader=None)
+
+    # Act and Assert
+    if success:
+        with pytest.raises(TransactionStartSignal) as ts:
+            instruction.evaluate(state)
+        assert ts.value.transaction.static
+    else:
+        with pytest.raises(WriteProtection):
+            instruction.evaluate(state)
+
+
+@patch("mythril.laser.ethereum.instructions.get_call_parameters")
+def test_staticness_call_symbolic(f1):
+    # Arrange
+    state = get_global_state()
+    state.environment.static = True
+    state.mstate.stack = []
+    call_value = symbol_factory.BitVecSym("x", 256)
+    code = Disassembly(code="616263")
+    f1.return_value = ("0", Account(code=code, address="0x19"), 0, call_value, 0, 0, 0)
+    instruction = Instruction("call", dynamic_loader=None)
+
+    # Act and Assert
+    with pytest.raises(TransactionStartSignal) as ts:
+        instruction.evaluate(state)
+
+    assert ts.value.transaction.static
+    assert ts.value.global_state.mstate.constraints[-1] == (call_value == 0)

tests/laser/Precompiles/test_ec_add.py

@@ -0,0 +1,27 @@
+from mock import patch
+from eth_utils import decode_hex
+from mythril.laser.ethereum.natives import ec_add
+from py_ecc.optimized_bn128 import FQ
+
+VECTOR_A = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+
+def test_ec_add_sanity():
+    assert ec_add(VECTOR_A) == []
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.add", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.normalize")
+def test_ec_add(f1, f2, f3):
+    FQ.fielf_modulus = 128
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    assert ec_add(VECTOR_A) == ([0] * 31 + [1]) * 2

tests/laser/Precompiles/test_elliptic_curves.py

@@ -0,0 +1,35 @@
+from mock import patch
+from mythril.laser.ethereum.natives import ec_pair
+from py_ecc.optimized_bn128 import FQ
+
+
+def test_ec_pair_192_check():
+    vec_c = [0] * 100
+    assert ec_pair(vec_c) == []
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.is_on_curve", return_value=True)
+@patch("mythril.laser.ethereum.natives.bn128.pairing", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.normalize")
+def test_ec_pair(f1, f2, f3, f4):
+    FQ.fielf_modulus = 100
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    vec_c = [0] * 192
+    assert ec_pair(vec_c) == [0] * 31 + [1]
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=False)
+def test_ec_pair_point_validation_failure(f1):
+    vec_c = [0] * 192
+    assert ec_pair(vec_c) == []
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+def test_ec_pair_field_exceed_mod(f1):
+    FQ.fielf_modulus = 100
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    vec_c = [10] * 192
+    assert ec_pair(vec_c) == []

tests/laser/Precompiles/test_elliptic_mul.py

@@ -0,0 +1,27 @@
+from mock import patch
+from eth_utils import decode_hex
+from mythril.laser.ethereum.natives import ec_mul
+from py_ecc.optimized_bn128 import FQ
+
+VECTOR_A = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+
+@patch("mythril.laser.ethereum.natives.validate_point", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.multiply", return_value=1)
+@patch("mythril.laser.ethereum.natives.bn128.normalize")
+def test_ec_mul(f1, f2, f3):
+    FQ.fielf_modulus = 128
+    a = FQ(val=1)
+    f1.return_value = (a, a)
+    assert ec_mul(VECTOR_A) == ([0] * 31 + [1]) * 2
+
+
+def test_ec_mul_validation_failure():
+    assert ec_mul(VECTOR_A) == []

tests/laser/Precompiles/test_mod_exp.py

@@ -0,0 +1,61 @@
+import pytest
+from eth_utils import decode_hex
+from mythril.laser.ethereum.natives import mod_exp
+from ethereum.utils import big_endian_to_int
+
+
+EIP198_VECTOR_A = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+EIP198_VECTOR_B = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000000"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2e"
+    "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc2f"
+)
+
+EIP198_VECTOR_C = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000002"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "ffff"
+    "8000000000000000000000000000000000000000000000000000000000000000"
+    "07"
+)
+
+EIP198_VECTOR_D = decode_hex(
+    "0000000000000000000000000000000000000000000000000000000000000001"
+    "0000000000000000000000000000000000000000000000000000000000000002"
+    "0000000000000000000000000000000000000000000000000000000000000020"
+    "03"
+    "ffff"
+    "80"
+)
+
+
+@pytest.mark.parametrize(
+    "data,expected",
+    (
+        (EIP198_VECTOR_A, 1),
+        (EIP198_VECTOR_B, 0),
+        (
+            EIP198_VECTOR_C,
+            26689440342447178617115869845918039756797228267049433585260346420242739014315,
+        ),
+        (
+            EIP198_VECTOR_D,
+            26689440342447178617115869845918039756797228267049433585260346420242739014315,
+        ),
+    ),
+)
+def test_modexp_result(data, expected):
+    actual = mod_exp(data)
+    assert big_endian_to_int(actual) == expected

tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json

@@ -47,7 +47,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {

tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json

@@ -54,7 +54,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {

tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json

@@ -47,7 +47,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {

tests/laser/smt/bitvecfunc_test.py

@@ -1,4 +1,4 @@
-from mythril.laser.smt import Solver, symbol_factory, bitvec
+from mythril.laser.smt import Solver, symbol_factory, UGT, UGE, ULT, ULE
 import z3
 import pytest
 
@@ -42,10 +42,10 @@ def test_bitvecfunc_arithmetic(operation, expected):
         (operator.le, z3.sat),
         (operator.gt, z3.unsat),
         (operator.ge, z3.sat),
-        (bitvec.UGT, z3.unsat),
-        (bitvec.UGE, z3.sat),
-        (bitvec.ULT, z3.unsat),
-        (bitvec.ULE, z3.sat),
+        (UGT, z3.unsat),
+        (UGE, z3.sat),
+        (ULT, z3.unsat),
+        (ULE, z3.sat),
     ],
 )
 def test_bitvecfunc_bitvecfunc_comparison(operation, expected):
@@ -80,3 +80,158 @@ def test_bitvecfunc_bitvecfuncval_comparison():
     # Assert
     assert s.check() == z3.sat
     assert s.model().eval(input2.raw) == 1337
+
+
+def test_bitvecfunc_nested_comparison():
+    # arrange
+    s = Solver()
+
+    input1 = symbol_factory.BitVecSym("input1", 256)
+    input2 = symbol_factory.BitVecSym("input2", 256)
+
+    bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
+    bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1)
+
+    bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
+    bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3)
+
+    # Act
+    s.add(input1 == input2)
+    s.add(bvf2 == bvf4)
+
+    # Assert
+    assert s.check() == z3.sat
+
+
+def test_bitvecfunc_unequal_nested_comparison():
+    # arrange
+    s = Solver()
+
+    input1 = symbol_factory.BitVecSym("input1", 256)
+    input2 = symbol_factory.BitVecSym("input2", 256)
+
+    bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
+    bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1)
+
+    bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
+    bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3)
+
+    # Act
+    s.add(input1 != input2)
+    s.add(bvf2 == bvf4)
+
+    # Assert
+    assert s.check() == z3.unsat
+
+
+def test_bitvecfunc_ext_nested_comparison():
+    # arrange
+    s = Solver()
+
+    input1 = symbol_factory.BitVecSym("input1", 256)
+    input2 = symbol_factory.BitVecSym("input2", 256)
+    input3 = symbol_factory.BitVecSym("input3", 256)
+    input4 = symbol_factory.BitVecSym("input4", 256)
+
+    bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
+    bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1 + input3)
+
+    bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
+    bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3 + input4)
+
+    # Act
+    s.add(input1 == input2)
+    s.add(input3 == input4)
+    s.add(bvf2 == bvf4)
+
+    # Assert
+    assert s.check() == z3.sat
+
+
+def test_bitvecfunc_ext_unequal_nested_comparison():
+    # Arrange
+    s = Solver()
+
+    input1 = symbol_factory.BitVecSym("input1", 256)
+    input2 = symbol_factory.BitVecSym("input2", 256)
+    input3 = symbol_factory.BitVecSym("input3", 256)
+    input4 = symbol_factory.BitVecSym("input4", 256)
+
+    bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
+    bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1 + input3)
+
+    bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
+    bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3 + input4)
+
+    # Act
+    s.add(input1 == input2)
+    s.add(input3 != input4)
+    s.add(bvf2 == bvf4)
+
+    # Assert
+    assert s.check() == z3.unsat
+
+
+def test_bitvecfunc_ext_unequal_nested_comparison_f():
+    # Arrange
+    s = Solver()
+
+    input1 = symbol_factory.BitVecSym("input1", 256)
+    input2 = symbol_factory.BitVecSym("input2", 256)
+    input3 = symbol_factory.BitVecSym("input3", 256)
+    input4 = symbol_factory.BitVecSym("input4", 256)
+
+    bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
+    bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1 + input3)
+
+    bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
+    bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3 + input4)
+
+    # Act
+    s.add(input1 != input2)
+    s.add(input3 == input4)
+    s.add(bvf2 == bvf4)
+
+    # Assert
+    assert s.check() == z3.unsat
+
+
+def test_bitvecfunc_find_input():
+    # Arrange
+    s = Solver()
+
+    input1 = symbol_factory.BitVecSym("input1", 256)
+    input2 = symbol_factory.BitVecSym("input2", 256)
+
+    bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
+    bvf2 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
+
+    # Act
+    s.add(input1 == symbol_factory.BitVecVal(1, 256))
+    s.add(bvf1 == bvf2)
+
+    # Assert
+    assert s.check() == z3.sat
+    assert s.model()[input2.raw] == 1
+
+
+def test_bitvecfunc_nested_find_input():
+    # Arrange
+    s = Solver()
+
+    input1 = symbol_factory.BitVecSym("input1", 256)
+    input2 = symbol_factory.BitVecSym("input2", 256)
+
+    bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
+    bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=bvf1)
+
+    bvf3 = symbol_factory.BitVecFuncSym("bvf3", "sha3", 256, input_=input2)
+    bvf4 = symbol_factory.BitVecFuncSym("bvf4", "sha3", 256, input_=bvf3)
+
+    # Act
+    s.add(input1 == symbol_factory.BitVecVal(123, 256))
+    s.add(bvf2 == bvf4)
+
+    # Assert
+    assert s.check() == z3.sat
+    assert s.model()[input2.raw] == 123

tests/laser/transaction/create_transaction_test.py

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

tests/native_test.py

@@ -76,6 +76,8 @@ class NativeTests(BaseTestCase):
     @staticmethod
     def runTest():
         """"""
+        # The solidity version (0.5.3 at the moment) should be kept in sync with
+        # pragma in ./tests/native_tests.sol
         disassembly = SolidityContract(
             "./tests/native_tests.sol",
             solc_binary=MythrilDisassembler._init_solc_binary("0.5.3"),

tests/native_tests.sol

@@ -1,4 +1,4 @@
-pragma solidity 0.5.0;
+pragma solidity ^0.5.0;
 
 
 contract Caller {

tox.ini

@@ -1,5 +1,5 @@
 [tox]
-envlist = py35,py36
+envlist = py36
 
 [testenv]
 deps =