Merge branch 'develop' into arbitrary_storage

.circleci/config.yml

@@ -108,6 +108,7 @@ jobs:
                 -e CIRCLE_BUILD_NUM=$CIRCLE_BUILD_NUM \
                 -e CIRCLE_BUILD_URL=$CIRCLE_BUILD_URL \
                 -e CIRCLE_WEBHOOK_URL=$CIRCLE_WEBHOOK_URL \
+                -e MONGO_URL=$MONGO_URL \
                 --rm edelweiss-mythril:latest \
                 --timeout 90 \
                 --output-dir /opt/edelweiss \

README.md

@@ -32,7 +32,7 @@ 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
 
@@ -75,7 +75,7 @@ Caller: [ATTACKER], function: commencekilling(), txdata: 0x7c11da20, value: 0x0
 ```
 
 
-Instructions for using Mythril are found on the [Wiki](https://github.com/ConsenSys/mythril/wiki). 
+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).
 

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/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.issues = []  # type: List[Issue]
-        self._cache = set()  # type: Set[int]
+        self.cache = set()  # type: Set[int]
-
-    @property
-    def issues(self):
-        """
-        Returns the issues
-        """
-        return self._issues
 
     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,78 +1,24 @@
 """This module contains the detection code for insecure delegate call usage."""
 import logging
-from copy import copy
+from typing import List
-from typing import List, cast, Dict
 
-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."""
 
@@ -83,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:
@@ -92,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)
+        potential_issues = self._analyze_state(state)
-        for issue in issues:
-            self._cache.add(issue.address)
-        self._issues.extend(issues)
 
-    @staticmethod
+        annotation = get_potential_issues_annotation(state)
-    def _analyze_state(state: GlobalState) -> List[Issue]:
+        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(
+            address = state.get_current_instruction()["address"]
-                        state,
+
-                        state.mstate.constraints
+            logging.debug(
-                        + annotation.constraints
+                "[DELEGATECALL] Detected potential delegatecall to a user-supplied address : {}".format(
-                        + [annotation.return_value == 1],
+                    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.cache.add(issue.address)
-        self._issues.extend(issues)
+        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.potential_issues import (
-from mythril.analysis.solver import get_transaction_sequence, UnsatError
+    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,16 +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:
+        annotation = get_potential_issues_annotation(state)
-            self._cache.add(issue.address)
+        annotation.potential_issues.extend(issues)
-        self._issues.extend(issues)
 
-    @staticmethod
+    def _analyze_state(self, state):
-    def _analyze_state(state):
         """
 
         :param state:
@@ -76,26 +76,21 @@ class DeprecatedOperationsModule(DetectionModule):
             swc_id = DEPRECATED_FUNCTIONS_USAGE
         else:
             return []
-        try:
+
-            transaction_sequence = get_transaction_sequence(
+        potential_issue = PotentialIssue(
-                state, state.mstate.constraints
-            )
-        except UnsatError:
-            return []
-        issue = Issue(
             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),
+            constraints=[],
-            transaction_sequence=transaction_sequence,
         )
-        return [issue]
+        return [potential_issue]
 
 
 detector = DeprecatedOperationsModule()

mythril/analysis/modules/dos.py

@@ -56,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]:
         """

mythril/analysis/modules/ether_thief.py

@@ -1,21 +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, If
+from mythril.laser.ethereum.transaction import ContractCreationTransaction
+
+from mythril.laser.smt import UGT, symbol_factory, UGE
 
 log = logging.getLogger(__name__)
 
@@ -60,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)
+        potential_issues = self._analyze_state(state)
-        for issue in issues:
+
-            self._cache.add(issue.address)
+        annotation = get_potential_issues_annotation(state)
-        self._issues.extend(issues)
+        annotation.potential_issues.extend(potential_issues)
 
-    @staticmethod
+    def _analyze_state(self, state):
-    def _analyze_state(state):
         """
 
         :param state:
         :return:
         """
+        state = copy(state)
         instruction = state.get_current_instruction()
 
-        if instruction["opcode"] != "CALL":
-            return []
-
         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
+        Require that the current transaction is sent by the attacker and
-            transactions. This prevents false positives caused by legitimate refund functions.
+        that the Ether sent to the attacker's address is greater than the
-            Also constrain the addition from overflowing (otherwise the solver produces solutions with
+        amount of Ether the attacker sent.
-            ridiculously high call values).
         """
-            constraints += [
+        for tx in state.world_state.transaction_sequence:
-                BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, signed=False)
-            ]
-            eth_sent_by_attacker = Sum(
-                eth_sent_by_attacker,
-                tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0),
-            )
-
             """
             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]
 
-        """
+        attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256)
-        Require that the current transaction is sent by the attacker and
-        that the Ether is sent to the attacker's address.
-        """
 
         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:
+        potential_issue = PotentialIssue(
-
-            transaction_sequence = solver.get_transaction_sequence(state, constraints)
-
-            issue = Issue(
             contract=state.environment.active_account.contract_name,
             function_name=state.environment.active_function_name,
             address=instruction["address"],
@@ -136,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,
+            detector=self,
-                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+            constraints=constraints,
         )
-        except UnsatError:
-            log.debug("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.cache.add(issue.address)
-        self._issues.extend(issues)
+        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)
+        potential_issues = self._analyze_state(state)
-        for issue in issues:
+
-            self._cache.add(issue.address)
+        annotation = get_potential_issues_annotation(state)
-        self._issues.extend(issues)
+        annotation.potential_issues.extend(potential_issues)
 
-    @staticmethod
+    def _analyze_state(self, state: GlobalState):
-    def _analyze_state(state):
         """
 
         :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,
+                    constraints=constraints,
-                    gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                    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,
+                    constraints=constraints,
-                    gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+                    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.cache.add(address)
-            self._issues.append(issue)
+            self.issues.append(issue)
 
 
 detector = IntegerOverflowUnderflowModule()

mythril/analysis/modules/multiple_sends.py

@@ -46,12 +46,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.cache.add(issue.address)
-        self._issues.extend(issues)
+        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)
+        annotation = get_potential_issues_annotation(state)
-        self._issues.extend(issues)
+        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(self, global_state: GlobalState) -> List[PotentialIssue]:
-    def _analyze_state(global_state: GlobalState) -> List[Issue]:
 
         annotations = cast(
             List[StateChangeCallsAnnotation],
@@ -171,7 +178,7 @@ class StateChange(DetectionModule):
         for annotation in annotations:
             if not annotation.state_change_states:
                 continue
-            issue = annotation.get_issue(global_state)
+            issue = annotation.get_issue(global_state, self)
             if issue:
                 vulnerabilities.append(issue)
         return vulnerabilities

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.cache.add(issue.address)
-        self._issues.extend(issues)
+        self.issues.extend(issues)
 
     @staticmethod
     def _analyze_state(state):
@@ -60,9 +60,7 @@ class SuicideModule(DetectionModule):
 
         to = state.mstate.stack[-1]
 
-        log.debug(
+        log.debug("SUICIDE in function %s", state.environment.active_function_name)
-            "[SUICIDE] SUICIDE in function " + 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.cache.add(issue.address)
-        self._issues.extend(issues)
+        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]
+            return_value = state.mstate.stack[-1]
-            # Use Typed Dict after release of mypy 0.670 and remove type ignore
             retvals.append(
-                {  # type: ignore
+                {"address": state.instruction["address"] - 1, "retval": return_value}
-                    "address": state.instruction["address"] - 1,
-                    "retval": retval,
-                }
             )
 
         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/solver.py

@@ -95,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:
@@ -103,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"]
+    min_price_dict = {}  # type: Dict[str, int]
-        value = int(concrete_transaction["value"], 16)
+    for address in initial_accounts.keys():
-        min_price_dict[caller] = min_price_dict.get(caller, 0) + value
+        min_price_dict[address] = model.eval(
-
+            initial_world_state.starting_balances[
-    if isinstance(transaction_sequence[0], ContractCreationTransaction):
+                symbol_factory.BitVecVal(address, 256)
-        initial_accounts = transaction_sequence[0].prev_world_state.accounts
+            ].raw,
-    else:
+            model_completion=True,
-        initial_accounts = transaction_sequence[0].world_state.accounts
+        ).as_long()
 
     concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict)
 
@@ -133,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}
@@ -148,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
+        input_ += transaction.code.bytecode
-    else:
+
-        input_ = "".join(
+    input_ += "".join(
         [
             hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:]
             for b in transaction.call_data.concrete(model)
@@ -171,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
 
@@ -193,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,
@@ -212,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 %}
 
@@ -36,7 +42,7 @@ Account: {% if key == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{%
 
 {% 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 %}
@@ -29,7 +33,7 @@ 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, "--optimize", "--standard-json", "--allow-paths", "."]
-    cmd = [solc_binary, "--combined-json", "bin,bin-runtime,srcmap,srcmap-runtime,ast"]
+
-
+    settings = json.loads(solc_settings_json) if solc_settings_json else {}
-    if solc_args:
+    settings.update(
-        cmd.extend(solc_args.split())
+        {
-    if not "--allow-paths" in cmd:
+            "outputSelection": {
-        cmd.extend(["--allow-paths", "."])
+                "*": {
-    else:
+                    "": ["ast"],
-        for i, arg in enumerate(cmd):
+                    "*": [
-            if arg == "--allow-paths":
+                        "metadata",
-                cmd[i + 1] += ",."
+                        "evm.bytecode",
-
+                        "evm.deployedBytecode",
-    cmd.append(file)
+                        "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):
+    result = json.loads(out)
-        raise CompilerError("Compilation failed.")
+
+    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"):
+    else:
-        # Temporary fix to support v0.5.x with Ubuntu PPA setup
+        # we are using solc-x for the the 0.5 and higher
-        solc_binaries.append("/usr/bin/solc")
+        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": {
+                "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]},
-                    "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(
@@ -427,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:
@@ -511,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(
@@ -551,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())
@@ -681,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": {
+                "meta": {"logs": [{"level": "error", "hidden": True, "msg": message}]},
-                    "logs": [{"level": "error", "hidden": "true", "msg": message}]
-                },
             }
         ]
         print(json.dumps(result))
@@ -231,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"
     )
@@ -524,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

@@ -10,13 +10,14 @@ 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,12 +89,11 @@ def get_callee_address(
     except TypeError:
         log.debug("Symbolic call encountered")
 
-        # TODO: This is broken. Now it should be Storage[(\d+)].
+        match = re.search(r"Storage\[(\d+)\]", str(simplify(symbolic_to_address)))
-        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,9 +104,8 @@ def get_callee_address(
                 "0x{:040X}".format(environment.active_account.address.value), index
             )
         # TODO: verify whether this happens or not
-        except Exception:
+        except:
-            log.debug("Error accessing contract storage.")
+            return symbolic_to_address
-            raise ValueError
 
         # testrpc simply returns the address, geth response is more elaborate.
         if not re.match(r"^0x[0-9a-f]{40}$", callee_address):
@@ -112,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.
 
@@ -121,7 +126,11 @@ def get_callee_account(
     :param dynamic_loader: dynamic loader to use
     :return: Account belonging to callee
     """
-    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)]
@@ -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],
 ) -> Optional[List[GlobalState]]:
-    if not 0 < int(callee_address, 16) < 5:
+
+    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

@@ -37,7 +37,7 @@ class OutOfGasException(VmException):
     pass
 
 
-class ProgramCounterException(VmException):
+class WriteProtection(VmException):
-    """A VM exception denoting an invalid PC value (No stop instruction is reached)."""
+    """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": (
+    "CREATE2": (32000, 32000),  # TODO: Make the gas values dynamic
-        32000,
-        32000,
-    ),  # TODO: The gas value is dynamic, to be done while implementing create2
     "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
@@ -173,6 +216,7 @@ class Instruction:
         """
         # Generalize some ops
         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"
@@ -575,23 +619,29 @@ class Instruction:
         :param global_state:
         :return:
         """
-        state = global_state.mstate
+        mstate = global_state.mstate
-        s0, s1 = state.stack.pop(), state.stack.pop()
+        s0, s1 = mstate.stack.pop(), mstate.stack.pop()
 
         try:
             s0 = util.get_concrete_int(s0)
             s1 = util.get_concrete_int(s1)
         except TypeError:
-            return []
+            log.debug("Unsupported symbolic argument for SIGNEXTEND")
+            mstate.stack.append(
+                global_state.new_bitvec(
+                    "SIGNEXTEND({},{})".format(hash(s0), hash(s1)), 256
+                )
+            )
+            return [global_state]
 
         if s0 <= 31:
             testbit = s0 * 8 + 7
             if s1 & (1 << testbit):
-                state.stack.append(s1 | (TT256 - (1 << testbit)))
+                mstate.stack.append(s1 | (TT256 - (1 << testbit)))
             else:
-                state.stack.append(s1 & ((1 << testbit) - 1))
+                mstate.stack.append(s1 & ((1 << testbit) - 1))
         else:
-            state.stack.append(s1)
+            mstate.stack.append(s1)
 
         return [global_state]
 
@@ -732,51 +782,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()
+        return [global_state]
-    def calldatacopy_(self, global_state: GlobalState) -> List[GlobalState]:
-        """
 
-        :param global_state:
+    @staticmethod
-        :return:
+    def _calldata_copy_helper(global_state, mstate, mstart, dstart, size):
-        """
-        state = global_state.mstate
         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)
+                mstate.mem_extend(mstart, 1)
-                state.memory[mstart] = global_state.new_bitvec(
+                mstate.memory[mstart] = global_state.new_bitvec(
                     "calldata_"
                     + str(environment.active_account.contract_name)
                     + "["
@@ -801,12 +845,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 +862,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 +900,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 +941,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 +991,7 @@ class Instruction:
             state.max_gas_used += gas_tuple[1]
             return [global_state]
 
-        min_gas, max_gas = cast(Callable, OPCODE_GAS["SHA3_FUNC"])(length)
+        Instruction._sha3_gas_helper(global_state, length)
-        state.min_gas_used += min_gas
-        state.max_gas_used += max_gas
-        StateTransition.check_gas_usage_limit(global_state)
 
         state.mem_extend(index, length)
         data_list = [
@@ -961,34 +1044,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 +1056,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 +1153,9 @@ class Instruction:
     @staticmethod
     def _code_copy_helper(
         code: str,
-        memory_offset: BitVec,
+        memory_offset: Union[int, BitVec],
-        code_offset: BitVec,
+        code_offset: Union[int, BitVec],
-        size: BitVec,
+        size: Union[int, BitVec],
         op: str,
         global_state: GlobalState,
     ) -> List[GlobalState]:
@@ -1089,13 +1201,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 +1260,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
+        world_state = global_state.world_state
-        address = global_state.mstate.stack.pop()
+        stack = global_state.mstate.stack
-        global_state.mstate.stack.append(
+        address = Extract(159, 0, stack.pop())
-            global_state.new_bitvec("extcodehash_{}".format(str(address)), 256)
+
-        )
+        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 +1481,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 +1493,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 +1651,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 +1666,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
+        call_value, mem_offset, mem_size = global_state.mstate.pop(3)
-        state = global_state.mstate
+
-        state.stack.pop(), state.stack.pop(), state.stack.pop()
+        return self._create_transaction_helper(
-        # Not supported
+            global_state, call_value, mem_offset, mem_size
-        state.stack.append(0)
+        )
-        return [global_state]
 
     @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
+        call_value, mem_offset, mem_size, salt = global_state.mstate.pop(4)
-        state = global_state.mstate
+
-        endowment, memory_start, memory_length, salt = (
+        return self._create_transaction_helper(
-            state.stack.pop(),
+            global_state, call_value, mem_offset, mem_size, salt
-            state.stack.pop(),
-            state.stack.pop(),
-            state.stack.pop(),
         )
-        # 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 +1791,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 +1801,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 +1875,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 +1896,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 +1925,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 +2020,6 @@ class Instruction:
             )
             global_state.mstate.stack.append(return_value)
             global_state.mstate.constraints.append(return_value == 0)
-
             return [global_state]
 
         try:
@@ -1787,11 +2052,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 +2066,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 +2097,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 +2116,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 +2171,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 +2179,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 +2206,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,
+            caller=environment.address,
-            callee_account=environment.active_account,
+            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:
+    def post_handler(self, global_state, function_name: str):
-        :return:
-        """
         instr = global_state.get_current_instruction()
 
         try:
-            callee_address, _, _, value, _, memory_out_offset, memory_out_size = get_call_parameters(
+            with_value = function_name is not "staticcall"
-                global_state, self.dynamic_loader
+            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(
+                "Could not determine required parameters for {}, putting fresh symbol on the stack. \n{}".format(
-                    e
+                    function_name, e
                 )
             )
             global_state.mstate.stack.append(
@@ -1993,39 +2288,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 mythril.laser.ethereum.util import extract_copy, extract32
-from ethereum.utils import sha3
+from ethereum.utils import (
-from mythril.laser.smt import Concat, simplify
+    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)
+        bytes_data = bytearray(data)
-        v = extract32(byte_data, 32)
+        v = extract32(bytes_data, 32)
-        r = extract32(byte_data, 64)
+        r = extract32(bytes_data, 64)
-        s = extract32(byte_data, 96)
+        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

@@ -4,7 +4,7 @@ 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 (
@@ -60,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
@@ -74,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_)
+            sanitized_item = self._sanitize(cast(BitVecFunc, item).input_)
-        value = storage[item]
+        else:
+            sanitized_item = item
         if (
-            (value.value == 0 or value.value is None)  # 0 for Array, None for K
+            self.address
-            and self.address
-            and item.symbolic is False
             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),
@@ -94,12 +96,12 @@ class Storage:
                     ),
                     256,
                 )
-                self.printable_storage[item] = storage[item]
+                self.storage_keys_loaded.add(int(item.value))
-                return storage[item]
+                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:
@@ -136,6 +138,8 @@ 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=dict()):
         concrete = isinstance(self._standard_storage, K)
@@ -144,7 +148,8 @@ class Storage:
         )
         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

@@ -9,7 +9,6 @@ from mythril.laser.ethereum.cfg import Node
 from mythril.laser.ethereum.state.environment import Environment
 from mythril.laser.ethereum.state.machine_state import MachineState
 from mythril.laser.ethereum.state.annotation import StateAnnotation
-from mythril.laser.ethereum.evm_exceptions import ProgramCounterException
 
 if TYPE_CHECKING:
     from mythril.laser.ethereum.state.world_state import WorldState
@@ -53,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":
         """
 
@@ -87,13 +94,11 @@ class GlobalState:
 
         :return:
         """
-
         instructions = self.environment.code.instruction_list
-        if self.mstate.pc >= len(instructions):
+        try:
-            raise ProgramCounterException(
-                "PC: {} can not be reached.".format(self.mstate.pc)
-            )
             return instructions[self.mstate.pc]
+        except KeyError:
+            return {"address": self.mstate.pc, "opcode": "STOP"}
 
     @property
     def current_transaction(

mythril/laser/ethereum/state/machine_state.py

@@ -95,6 +95,7 @@ class MachineState:
         depth=0,
         max_gas_used=0,
         min_gas_used=0,
+        prev_pc=-1,
     ) -> None:
         """Constructor for machineState.
 
@@ -106,8 +107,9 @@ class MachineState:
         :param depth:
         :param max_gas_used:
         :param min_gas_used:
+        :param prev_pc:
         """
-        self.pc = pc
+        self._pc = pc
         self.stack = MachineStack(stack)
         self.memory = memory or Memory()
         self.gas_limit = gas_limit
@@ -115,6 +117,7 @@ class MachineState:
         self.max_gas_used = max_gas_used  # upper gas usage bound
         self.constraints = constraints or Constraints()
         self.depth = depth
+        self.prev_pc = prev_pc  # holds context of current pc
 
     def calculate_extension_size(self, start: int, size: int) -> int:
         """
@@ -210,11 +213,12 @@ class MachineState:
             gas_limit=self.gas_limit,
             max_gas_used=self.max_gas_used,
             min_gas_used=self.min_gas_used,
-            pc=self.pc,
+            pc=self._pc,
             stack=copy(self.stack),
             memory=copy(self.memory),
             constraints=copy(self.constraints),
             depth=self.depth,
+            prev_pc=self.prev_pc,
         )
 
     def __str__(self):
@@ -224,6 +228,19 @@ class MachineState:
         """
         return str(self.as_dict)
 
+    @property
+    def pc(self) -> int:
+        """
+
+        :return:
+        """
+        return self._pc
+
+    @pc.setter
+    def pc(self, value):
+        self.prev_pc = self._pc
+        self._pc = value
+
     @property
     def memory_size(self) -> int:
         """
@@ -239,11 +256,12 @@ class MachineState:
         :return:
         """
         return dict(
-            pc=self.pc,
+            pc=self._pc,
             stack=self.stack,
             memory=self.memory,
             memsize=self.memory_size,
             gas=self.gas_limit,
             max_gas_used=self.max_gas_used,
             min_gas_used=self.min_gas_used,
+            prev_pc=self.prev_pc,
         )

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/strategy/extensions/bounded_loops.py

@@ -3,7 +3,6 @@ from mythril.laser.ethereum.strategy.basic import BasicSearchStrategy
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum.transaction import ContractCreationTransaction
 from typing import Dict, cast, List
-from copy import copy
 import logging
 
 
@@ -14,12 +13,10 @@ class JumpdestCountAnnotation(StateAnnotation):
     """State annotation that counts the number of jumps per destination."""
 
     def __init__(self) -> None:
-        self._reached_count = {}  # type: Dict[int, int]
+        self._reached_count = {}  # type: Dict[str, int]
 
     def __copy__(self):
-        result = JumpdestCountAnnotation()
+        return self
-        result._reached_count = copy(self._reached_count)
-        return result
 
 
 class BoundedLoopsStrategy(BasicSearchStrategy):
@@ -48,7 +45,6 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
 
         :return: Global state
         """
-
         while True:
 
             state = self.super_strategy.get_strategic_global_state()
@@ -60,26 +56,35 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
 
             if len(annotations) == 0:
                 annotation = JumpdestCountAnnotation()
+                log.debug("Adding JumpdestCountAnnotation to GlobalState")
                 state.annotate(annotation)
             else:
                 annotation = annotations[0]
 
-            address = state.get_current_instruction()["address"]
+            cur_instr = state.get_current_instruction()
+
+            if cur_instr["opcode"].upper() != "JUMPDEST":
+                return state
+
+            # create unique instruction identifier
+            key = "{};{};{}".format(
+                cur_instr["opcode"], cur_instr["address"], state.mstate.prev_pc
+            )
 
-            if address in annotation._reached_count:
+            if key in annotation._reached_count:
-                annotation._reached_count[address] += 1
+                annotation._reached_count[key] += 1
             else:
-                annotation._reached_count[address] = 1
+                annotation._reached_count[key] = 1
 
             # The creation transaction gets a higher loop bound to give it a better chance of success.
             # TODO: There's probably a nicer way to do this
 
             if isinstance(
                 state.current_transaction, ContractCreationTransaction
-            ) and annotation._reached_count[address] < max(8, self.bound):
+            ) and annotation._reached_count[key] < max(8, self.bound):
                 return state
 
-            elif annotation._reached_count[address] > self.bound:
+            elif annotation._reached_count[key] > self.bound:
                 log.debug("Loop bound reached, skipping state")
                 continue
 

mythril/laser/ethereum/svm.py

@@ -5,12 +5,16 @@ from copy import copy
 from datetime import datetime, timedelta
 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
@@ -257,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)
@@ -323,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
 
@@ -332,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 = []
@@ -344,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,
@@ -384,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(

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, UGE, BitVec
-from mythril.laser.smt import symbol_factory
+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
+        callee_account.contract_name = contract_name or callee_account.contract_name
-        # TODO: set correct balance for new account
+        # 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/bitvecfunc.py

@@ -3,7 +3,7 @@ from itertools import product
 from typing import Optional, Union, cast, Callable, List
 import z3
 
-from mythril.laser.smt.bitvec import BitVec, Annotations
+from mythril.laser.smt.bitvec import BitVec, Annotations, _padded_operation
 from mythril.laser.smt.bool import Or, Bool, And
 
 
@@ -113,7 +113,10 @@ def _comparison_helper(
             )
 
     return And(
-        Bool(cast(z3.BoolRef, operation(a.raw, b.raw)), annotations=union),
+        Bool(
+            cast(z3.BoolRef, _padded_operation(a.raw, b.raw, operation)),
+            annotations=union,
+        ),
         Bool(condition) if b.nested_functions else Bool(True),
         a.input_ == b.input_ if inputs_equal else a.input_ != b.input_,
     )

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()
+                        raise solc.exceptions.SolcError()
-                except 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():
+        for contract_name in data["contracts"][input_file].keys():
-            filename, name = key.split(":")
+            if len(
-            if filename == input_file and len(contract["bin-runtime"]):
+                data["contracts"][input_file][contract_name]["evm"]["deployedBytecode"][
+                    "object"
+                ]
+            ):
                 yield SolidityContract(
                     input_file=input_file,
-                    name=name,
+                    name=contract_name,
-                    solc_args=solc_args,
+                    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"):
+    def __init__(
-        data = get_solc_json(input_file, solc_args=solc_args, solc_binary=solc_binary)
+        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()):
+            contract = data["contracts"][input_file][name]
-                filename, _name = key.split(":")
+            if len(contract["evm"]["deployedBytecode"]["object"]):
-
+                code = contract["evm"]["deployedBytecode"]["object"]
-                if (
+                creation_code = contract["evm"]["bytecode"]["object"]
-                    filename == input_file
+                srcmap = contract["evm"]["deployedBytecode"]["sourceMap"].split(";")
-                    and name == _name
+                srcmap_constructor = contract["evm"]["bytecode"]["sourceMap"].split(";")
-                    and len(contract["bin-runtime"])
-                ):
-                    code = contract["bin-runtime"]
-                    creation_code = contract["bin"]
-                    srcmap = contract["srcmap-runtime"].split(";")
-                    srcmap_constructor = contract["srcmap"].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()):
+            for contract_name, contract in sorted(
-                filename, name = key.split(":")
+                data["contracts"][input_file].items()
-
+            ):
-                if filename == input_file and len(contract["bin-runtime"]):
+                if len(contract["evm"]["deployedBytecode"]["object"]):
-                    code = contract["bin-runtime"]
+                    name = contract_name
-                    creation_code = contract["bin"]
+                    code = contract["evm"]["deployedBytecode"]["object"]
-                    srcmap = contract["srcmap-runtime"].split(";")
+                    creation_code = contract["evm"]["bytecode"]["object"]
-                    srcmap_constructor = contract["srcmap"].split(";")
+                    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"]:
+        for child in ast["nodes"]:
-            if "contractKind" in child["attributes"]:
+            if child.get("contractKind"):
                 source_maps.add(child["src"])
         return source_maps
 

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]
+        solc_json = get_solc_json(file_path, solc_binary, solc_settings_json)
-        if solc_args:
-            cmd.extend(solc_args.split())
 
-        try:
+        for contract in solc_json["contracts"][file_path].values():
-            p = Popen(cmd, stdout=PIPE, stderr=PIPE)
+            for name, hash in contract["evm"]["methodIdentifiers"].items():
-            stdout, stderr = p.communicate()
+                self.add("0x" + hash, name)
-            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)
 
     @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
@@ -17,13 +17,16 @@ 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,11 +25,13 @@ 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-account>=0.1.0a2,<=0.3.0",
@@ -49,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/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 =