Merge branch 'develop'

.circleci/config.yml

@@ -33,6 +33,12 @@ jobs:
             - .tox/py*
             - /root/.cache/pip/wheels/
 
+      - run:
+          name: Black style check
+          command: |
+            pip3 install --user black
+            python3 -m black --check /home/mythril/
+
       - run:
           background: true
           name: Launch of background geth instance
@@ -61,10 +67,10 @@ jobs:
           name: Sonar analysis
           command: if [ -z "$CIRCLE_PR_NUMBER" ]; then if [ -z "$CIRCLE_TAG" ]; then sonar-scanner -Dsonar.projectKey=$SONAR_PROJECT_KEY -Dsonar.organization=$SONAR_ORGANIZATION -Dsonar.branch.name=$CIRCLE_BRANCH -Dsonar.projectBaseDir=/home/mythril -Dsonar.sources=mythril -Dsonar.host.url=$SONAR_HOST_URL -Dsonar.tests=/home/mythril/tests -Dsonar.login=$SONAR_LOGIN; fi; fi
 
-      - run:
+      # - run:
-          name: Integration tests
+      #     name: Integration tests
-          command: if [ -z "$CIRCLE_PR_NUMBER" ]; then ./run-integration-tests.sh; fi
+      #     command: if [ -z "$CIRCLE_PR_NUMBER" ]; then ./run-integration-tests.sh; fi
-          working_directory: /home
+      #     working_directory: /home
 
   pypi_release:
     <<: *defaults
@@ -84,6 +90,8 @@ jobs:
           command: twine upload dist/*
           working_directory: /home/mythril
 
+  # Release of the mainstream (current stable) version as mythril/myth
+  # container.
   dockerhub_release:
     docker:
       - image: docker:stable
@@ -92,7 +100,18 @@ jobs:
       - setup_remote_docker
       - run:
           name: Building Docker Image
-          command: ./docker_build_and_deploy.sh
+          command: ./docker_build_and_deploy.sh mythril/myth
+
+  # Release of the latest development version as mythril/myth-dev container.
+  dockerhub_dev_release:
+    docker:
+      - image: docker:stable
+    steps:
+      - checkout
+      - setup_remote_docker
+      - run:
+          name: Building Docker Image
+          command: ./docker_build_and_deploy.sh mythril/myth-dev
 
 workflows:
   version: 2
@@ -110,6 +129,12 @@ workflows:
               only: /v[0-9]+(\.[0-9]+)*/
           requires:
             - test
+      - dockerhub_dev_release:
+          filters:
+            branches:
+              only: develop
+          # requires:
+          #  - test
       - dockerhub_release:
           filters:
             branches:

README.md

@@ -13,12 +13,10 @@
 
 Mythril Classic is an open-source security analysis tool for Ethereum smart contracts. It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. 
 
-Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/E3YrVtG) will serve your needs!
+Whether you want to contribute, need support, or want to learn what we have cooking for the future, our [Discord server](https://discord.gg/E3YrVtG) will serve your needs.
 
 Oh and by the way, we're also building an easy-to-use security analysis platform (a.k.a. "the INFURA for smart contract security") that anybody can use to create purpose-built security tools. It's called [Mythril Platform](https://mythril.ai) and you should definitely [check it out](https://media.consensys.net/mythril-platform-api-is-upping-the-smart-contract-security-game-eee1d2642488).
 
-
-
 ## Installation and setup
 
 Get it with [Docker](https://www.docker.com):
@@ -37,21 +35,10 @@ See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup)
 
 ## Usage
 
-Instructions for using the 'myth' tool are found on the [Wiki](https://github.com/ConsenSys/mythril-classic/wiki). 
+Instructions for using Mythril Classic are found on the [Wiki](https://github.com/ConsenSys/mythril-classic/wiki). 
 
 For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
 
 ## Vulnerability Remediation
 
 Visit the [Smart Contract Vulnerability Classification Registry](https://smartcontractsecurity.github.io/SWC-registry/) to find detailed information and remediation guidance for the vulnerabilities reported.
-
-## Presentations, papers and articles
-
-- [Analyzing Ethereum Smart Contracts for Vulnerabilities](https://hackernoon.com/scanning-ethereum-smart-contracts-for-vulnerabilities-b5caefd995df)
-- [What Caused the Parity SUICIDE Vulnerability & How to Detect Similar Bugs](https://hackernoon.com/what-caused-the-latest-100-million-ethereum-bug-and-a-detection-tool-for-similar-bugs-7b80f8ab7279)
-- [Detecting Integer Overflows in Ethereum Smart Contracts](https://media.consensys.net/detecting-batchoverflow-and-similar-flaws-in-ethereum-smart-contracts-93cf5a5aaac8)
-- [How Formal Verification Can Ensure Flawless Smart Contracts](https://media.consensys.net/how-formal-verification-can-ensure-flawless-smart-contracts-cbda8ad99bd1)
-- [Smashing Smart Contracts for Fun and Real Profit](https://hackernoon.com/hitb2018ams-smashing-smart-contracts-for-fun-and-real-profit-720f5e3ac777)
-- [HITBSecConf 2018 - Presentation video](https://www.youtube.com/watch?v=iqf6epACgds)
-- [EDCon Toronto 2018 - Mythril: Find bugs and verify security properties in your contracts](https://www.youtube.com/watch?v=NJ9StJThxZY&feature=youtu.be&t=3h3m18s)
-

docker_build_and_deploy.sh

@@ -1,9 +1,17 @@
 #!/bin/sh
+
 set -eo pipefail
 
-NAME=mythril/myth
+NAME=$1
+
+if [ ! -z $CIRCLE_TAG ];
+then
+  VERSION=${CIRCLE_TAG#?}
+else
+  VERSION=${CIRCLE_SHA1}
+fi
 
-VERSION_TAG=${NAME}:${CIRCLE_TAG#?}
+VERSION_TAG=${NAME}:${VERSION}
 LATEST_TAG=${NAME}:latest
 
 docker build -t ${VERSION_TAG} .

mythril/__init__.py

@@ -1,6 +1,6 @@
 # We use RsT document formatting in docstring. For example :param to mark parameters.
 # See PEP 287
-__docformat__ = 'restructuredtext'
+__docformat__ = "restructuredtext"
 
 # Accept mythril.VERSION to get mythril's current version number
 from .version import VERSION  # NOQA

mythril/analysis/callgraph.py

@@ -5,87 +5,119 @@ from mythril.laser.ethereum.svm import NodeFlags
 import z3
 
 default_opts = {
-    'autoResize': True,
+    "autoResize": True,
-    'height': '100%',
+    "height": "100%",
-    'width': '100%',
+    "width": "100%",
-    'manipulation': False,
+    "manipulation": False,
-    'layout': {
+    "layout": {
-        'improvedLayout': True,
+        "improvedLayout": True,
-        'hierarchical': {
+        "hierarchical": {
-            'enabled': True,
+            "enabled": True,
-            'levelSeparation': 450,
+            "levelSeparation": 450,
-            'nodeSpacing': 200,
+            "nodeSpacing": 200,
-            'treeSpacing': 100,
+            "treeSpacing": 100,
-            'blockShifting': True,
+            "blockShifting": True,
-            'edgeMinimization': True,
+            "edgeMinimization": True,
-            'parentCentralization': False,
+            "parentCentralization": False,
-            'direction': 'LR',
+            "direction": "LR",
-            'sortMethod': 'directed'
+            "sortMethod": "directed",
-        }
+        },
     },
-    'nodes': {
+    "nodes": {
-        'color': '#000000',
+        "color": "#000000",
-        'borderWidth': 1,
+        "borderWidth": 1,
-        'borderWidthSelected': 2,
+        "borderWidthSelected": 2,
-        'chosen': True,
+        "chosen": True,
-        'shape': 'box',
+        "shape": "box",
-        'font': {'align': 'left', 'color': '#FFFFFF'},
+        "font": {"align": "left", "color": "#FFFFFF"},
     },
-    'edges': {
+    "edges": {
-        'font': {
+        "font": {
-            'color': '#FFFFFF',
+            "color": "#FFFFFF",
-            'face': 'arial',
+            "face": "arial",
-            'background': 'none',
+            "background": "none",
-            'strokeWidth': 0,
+            "strokeWidth": 0,
-            'strokeColor': '#ffffff',
+            "strokeColor": "#ffffff",
-            'align': 'horizontal',
+            "align": "horizontal",
-            'multi': False,
+            "multi": False,
-            'vadjust': 0,
+            "vadjust": 0,
         }
     },
-    'physics': {'enabled': False}
+    "physics": {"enabled": False},
 }
 
 phrack_opts = {
-    'nodes': {
+    "nodes": {
-        'color': '#000000',
+        "color": "#000000",
-        'borderWidth': 1,
+        "borderWidth": 1,
-        'borderWidthSelected': 1,
+        "borderWidthSelected": 1,
-        'shapeProperties': {
+        "shapeProperties": {"borderDashes": False, "borderRadius": 0},
-            'borderDashes': False,
+        "chosen": True,
-            'borderRadius': 0,
+        "shape": "box",
-        },
+        "font": {"face": "courier new", "align": "left", "color": "#000000"},
-        'chosen': True,
-        'shape': 'box',
-        'font': {'face': 'courier new', 'align': 'left', 'color': '#000000'},
     },
-    'edges': {
+    "edges": {
-        'font': {
+        "font": {
-            'color': '#000000',
+            "color": "#000000",
-            'face': 'courier new',
+            "face": "courier new",
-            'background': 'none',
+            "background": "none",
-            'strokeWidth': 0,
+            "strokeWidth": 0,
-            'strokeColor': '#ffffff',
+            "strokeColor": "#ffffff",
-            'align': 'horizontal',
+            "align": "horizontal",
-            'multi': False,
+            "multi": False,
-            'vadjust': 0,
+            "vadjust": 0,
         }
-    }
+    },
 }
 
 default_colors = [
-    {'border': '#26996f', 'background': '#2f7e5b', 'highlight': {'border': '#26996f', 'background': '#28a16f'}},
+    {
-    {'border': '#9e42b3', 'background': '#842899', 'highlight': {'border': '#9e42b3', 'background': '#933da6'}},
+        "border": "#26996f",
-    {'border': '#b82323', 'background': '#991d1d', 'highlight': {'border': '#b82323', 'background': '#a61f1f'}},
+        "background": "#2f7e5b",
-    {'border': '#4753bf', 'background': '#3b46a1', 'highlight': {'border': '#4753bf', 'background': '#424db3'}},
+        "highlight": {"border": "#26996f", "background": "#28a16f"},
-    {'border': '#26996f', 'background': '#2f7e5b', 'highlight': {'border': '#26996f', 'background': '#28a16f'}},
+    },
-    {'border': '#9e42b3', 'background': '#842899', 'highlight': {'border': '#9e42b3', 'background': '#933da6'}},
+    {
-    {'border': '#b82323', 'background': '#991d1d', 'highlight': {'border': '#b82323', 'background': '#a61f1f'}},
+        "border": "#9e42b3",
-    {'border': '#4753bf', 'background': '#3b46a1', 'highlight': {'border': '#4753bf', 'background': '#424db3'}},
+        "background": "#842899",
+        "highlight": {"border": "#9e42b3", "background": "#933da6"},
+    },
+    {
+        "border": "#b82323",
+        "background": "#991d1d",
+        "highlight": {"border": "#b82323", "background": "#a61f1f"},
+    },
+    {
+        "border": "#4753bf",
+        "background": "#3b46a1",
+        "highlight": {"border": "#4753bf", "background": "#424db3"},
+    },
+    {
+        "border": "#26996f",
+        "background": "#2f7e5b",
+        "highlight": {"border": "#26996f", "background": "#28a16f"},
+    },
+    {
+        "border": "#9e42b3",
+        "background": "#842899",
+        "highlight": {"border": "#9e42b3", "background": "#933da6"},
+    },
+    {
+        "border": "#b82323",
+        "background": "#991d1d",
+        "highlight": {"border": "#b82323", "background": "#a61f1f"},
+    },
+    {
+        "border": "#4753bf",
+        "background": "#3b46a1",
+        "highlight": {"border": "#4753bf", "background": "#424db3"},
+    },
 ]
 
-phrack_color = {'border': '#000000', 'background': '#ffffff',
+phrack_color = {
-                'highlight': {'border': '#000000', 'background': '#ffffff'}}
+    "border": "#000000",
+    "background": "#ffffff",
+    "highlight": {"border": "#000000", "background": "#ffffff"},
+}
 
 
 def extract_nodes(statespace, color_map):
@@ -95,28 +127,43 @@ def extract_nodes(statespace, color_map):
         instructions = [state.get_current_instruction() for state in node.states]
         code_split = []
         for instruction in instructions:
-            if instruction['opcode'].startswith("PUSH"):
+            if instruction["opcode"].startswith("PUSH"):
-                code_line = "%d %s %s" % (instruction['address'], instruction['opcode'], instruction['argument'])
+                code_line = "%d %s %s" % (
-            elif instruction['opcode'].startswith("JUMPDEST") and NodeFlags.FUNC_ENTRY in node.flags and instruction['address'] == node.start_addr:
+                    instruction["address"],
+                    instruction["opcode"],
+                    instruction["argument"],
+                )
+            elif (
+                instruction["opcode"].startswith("JUMPDEST")
+                and NodeFlags.FUNC_ENTRY in node.flags
+                and instruction["address"] == node.start_addr
+            ):
                 code_line = node.function_name
             else:
-                code_line = "%d %s" % (instruction['address'], instruction['opcode'])
+                code_line = "%d %s" % (instruction["address"], instruction["opcode"])
 
-            code_line = re.sub("([0-9a-f]{8})[0-9a-f]+", lambda m: m.group(1) + "(...)", code_line)
+            code_line = re.sub(
+                "([0-9a-f]{8})[0-9a-f]+", lambda m: m.group(1) + "(...)", code_line
+            )
             code_split.append(code_line)
 
-        truncated_code = '\n'.join(code_split) if (len(code_split) < 7) \
+        truncated_code = (
-            else '\n'.join(code_split[:6]) + "\n(click to expand +)"
+            "\n".join(code_split)
-
+            if (len(code_split) < 7)
-        nodes.append({
+            else "\n".join(code_split[:6]) + "\n(click to expand +)"
-            'id': str(node_key),
+        )
-            'color': color_map[node.get_cfg_dict()['contract_name']],
+
-            'size': 150,
+        nodes.append(
-            'fullLabel': '\n'.join(code_split),
+            {
-            'label': truncated_code,
+                "id": str(node_key),
-            'truncLabel': truncated_code,
+                "color": color_map[node.get_cfg_dict()["contract_name"]],
-            'isExpanded': False
+                "size": 150,
-        })
+                "fullLabel": "\n".join(code_split),
+                "label": truncated_code,
+                "truncLabel": truncated_code,
+                "isExpanded": False,
+            }
+        )
     return nodes
 
 
@@ -131,21 +178,33 @@ def extract_edges(statespace):
             except z3.Z3Exception:
                 label = str(edge.condition).replace("\n", "")
 
-        label = re.sub(r'([^_])([\d]{2}\d+)', lambda m: m.group(1) + hex(int(m.group(2))), label)
+        label = re.sub(
-
+            r"([^_])([\d]{2}\d+)", lambda m: m.group(1) + hex(int(m.group(2))), label
-        edges.append({
+        )
-            'from': str(edge.as_dict['from']),
+
-            'to': str(edge.as_dict['to']),
+        edges.append(
-            'arrows': 'to',
+            {
-            'label': label,
+                "from": str(edge.as_dict["from"]),
-            'smooth': {'type': 'cubicBezier'}
+                "to": str(edge.as_dict["to"]),
-        })
+                "arrows": "to",
+                "label": label,
+                "smooth": {"type": "cubicBezier"},
+            }
+        )
     return edges
 
 
-def generate_graph(statespace, title="Mythril / Ethereum LASER Symbolic VM", physics=False, phrackify=False):
+def generate_graph(
-    env = Environment(loader=PackageLoader('mythril.analysis'), autoescape=select_autoescape(['html', 'xml']))
+    statespace,
-    template = env.get_template('callgraph.html')
+    title="Mythril / Ethereum LASER Symbolic VM",
+    physics=False,
+    phrackify=False,
+):
+    env = Environment(
+        loader=PackageLoader("mythril.analysis"),
+        autoescape=select_autoescape(["html", "xml"]),
+    )
+    template = env.get_template("callgraph.html")
 
     graph_opts = default_opts
     accounts = statespace.accounts
@@ -154,13 +213,17 @@ def generate_graph(statespace, title="Mythril / Ethereum LASER Symbolic VM", phy
         color_map = {accounts[k].contract_name: phrack_color for k in accounts}
         graph_opts.update(phrack_opts)
     else:
-        color_map = {accounts[k].contract_name: default_colors[i % len(default_colors)] for i, k in enumerate(accounts)}
+        color_map = {
+            accounts[k].contract_name: default_colors[i % len(default_colors)]
+            for i, k in enumerate(accounts)
+        }
 
-    graph_opts['physics']['enabled'] = physics
+    graph_opts["physics"]["enabled"] = physics
 
-    return template.render(title=title,
+    return template.render(
-                           nodes=extract_nodes(statespace, color_map),
+        title=title,
-                           edges=extract_edges(statespace),
+        nodes=extract_nodes(statespace, color_map),
-                           phrackify=phrackify,
+        edges=extract_edges(statespace),
-                           opts=graph_opts
+        phrackify=phrackify,
-                           )
+        opts=graph_opts,
+    )

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -159,12 +159,11 @@ def solve(call):
     try:
         model = solver.get_model(call.node.constraints)
         logging.debug("[DEPENDENCE_ON_PREDICTABLE_VARS] MODEL: " + str(model))
+        pretty_model = solver.pretty_print_model(model)
 
-        for decl in model.decls():
+        logging.debug(
-            logging.debug(
+            "[DEPENDENCE_ON_PREDICTABLE_VARS] main model: \n%s" % pretty_model
-                "[DEPENDENCE_ON_PREDICTABLE_VARS] main model: %s = 0x%x"
+        )
-                % (decl.name(), model[decl].as_long())
-            )
         return True
 
     except UnsatError:

mythril/analysis/modules/ether_send.py

@@ -1,10 +1,8 @@
-from z3 import *
 from mythril.analysis.ops import *
 from mythril.analysis import solver
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.exceptions import UnsatError
-import re
 import logging
 
 
@@ -17,148 +15,68 @@ to that index).
 """
 
 
-def execute(statespace):
+def execute(state_space):
 
     logging.debug("Executing module: ETHER_SEND")
 
     issues = []
 
-    for call in statespace.calls:
+    for k in state_space.nodes:
+        node = state_space.nodes[k]
 
-        state = call.state
+        for state in node.states:
-        address = state.get_current_instruction()["address"]
+            issues += _analyze_state(state, node)
 
-        if "callvalue" in str(call.value):
+    return issues
-            logging.debug("[ETHER_SEND] Skipping refund function")
-            continue
-
-        # We're only interested in calls that send Ether
-
-        if call.value.type == VarType.CONCRETE and call.value.val == 0:
-            continue
-
-        interesting = False
-
-        description = "A non-zero amount of Ether is sent to a user-supplied address."
-
-        if re.search(r"caller", str(call.to)):
-            description += " The target address is msg.sender.\n"
-            interesting = True
-
-        elif re.search(r"calldata", str(call.to)):
-            description += " The target address is taken from function arguments.\n"
-            interesting = True
-
-        else:
-            m = re.search(r"storage_([a-z0-9_&^]+)", str(call.to))
-
-            if m:
-                idx = m.group(1)
-
-                description += (
-                    " The target address is taken from storage slot "
-                    + str(idx)
-                    + ".\n"
-                )
-
-                func = statespace.find_storage_write(
-                    state.environment.active_account.address, idx
-                )
-
-                if func:
-                    description += (
-                        "There is a check on storage index "
-                        + str(idx)
-                        + ". This storage slot can be written to by calling the function `"
-                        + func
-                        + "`.\n"
-                    )
-                    interesting = True
-                else:
-                    logging.debug("[ETHER_SEND] No storage writes to index " + str(idx))
-
-        if interesting:
-
-            node = call.node
-
-            can_solve = True
-            constrained = False
-
-            index = 0
-
-            while can_solve and index < len(node.constraints):
-
-                constraint = node.constraints[index]
-                index += 1
-                logging.debug("[ETHER_SEND] Constraint: " + str(constraint))
-
-                m = re.search(r"storage_([a-z0-9_&^]+)", str(constraint))
-
-                if m:
-
-                    constrained = True
-                    idx = m.group(1)
-
-                    func = statespace.find_storage_write(
-                        state.environment.active_account.address, idx
-                    )
-
-                    if func:
-                        description += (
-                            "\nThere is a check on storage index "
-                            + str(idx)
-                            + ". This storage slot can be written to by calling the function `"
-                            + func
-                            + "`."
-                        )
-                    else:
-                        logging.debug(
-                            "[ETHER_SEND] No storage writes to index " + str(idx)
-                        )
-                        can_solve = False
-                        break
 
-                # CALLER may also be constrained to hardcoded address. I.e. 'caller' and some integer
 
-                elif re.search(r"caller", str(constraint)) and re.search(
+def _analyze_state(state, node):
-                    r"[0-9]{20}", str(constraint)
+    issues = []
-                ):
+    instruction = state.get_current_instruction()
-                    constrained = True
+
-                    can_solve = False
+    if instruction["opcode"] != "CALL":
-                    break
+        return []
-
+
-            if not constrained:
+    call_value = state.mstate.stack[-3]
-                description += (
+    target = state.mstate.stack[-2]
-                    "It seems that this function can be called without restrictions."
+
-                )
+    not_creator_constraints = []
-
+    if len(state.world_state.transaction_sequence) > 1:
-            if can_solve:
+        creator = state.world_state.transaction_sequence[0].caller
-
+        for transaction in state.world_state.transaction_sequence[1:]:
-                try:
+            not_creator_constraints.append(
-                    model = solver.get_model(node.constraints)
+                Not(Extract(159, 0, transaction.caller) == Extract(159, 0, creator))
-
+            )
-                    for decl in model.decls():
+            not_creator_constraints.append(
-                        logging.debug(
+                Not(Extract(159, 0, transaction.caller) == 0)
-                            "[ETHER_SEND] main model: %s = 0x%x"
+            )
-                            % (decl.name(), model[decl].as_long())
+
-                        )
+    try:
-
+        model = solver.get_model(
-                    debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model)
+            node.constraints + not_creator_constraints + [call_value > 0]
-
+        )
-                    issue = Issue(
+
-                        contract=call.node.contract_name,
+        debug = "Transaction Sequence: " + str(
-                        function_name=call.node.function_name,
+            solver.get_transaction_sequence(
-                        address=address,
+                state, node.constraints + not_creator_constraints + [call_value > 0]
-                        title="Ether send",
+            )
-                        _type="Warning",
+        )
-                        swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
+
-                        description=description,
+        issue = Issue(
-                        bytecode=state.environment.code.bytecode,
+            contract=node.contract_name,
-                        debug=debug,
+            function_name=node.function_name,
-                    )
+            address=instruction["address"],
-                    issues.append(issue)
+            swc_id=UNPROTECTED_ETHER_WITHDRAWAL,
-
+            title="Ether send",
-                except UnsatError:
+            _type="Warning",
-                    logging.debug("[ETHER_SEND] no model found")
+            bytecode=state.environment.code.bytecode,
+            description="It seems that an attacker is able to execute an call instruction,"
+            " this can mean that the attacker is able to extract funds "
+            "out of the contract.".format(target),
+            debug=debug,
+        )
+        issues.append(issue)
+    except UnsatError:
+        logging.debug("[UNCHECKED_SUICIDE] no model found")
 
     return issues

mythril/analysis/modules/exceptions.py

@@ -36,16 +36,14 @@ def execute(statespace):
                         "out-of-bounds array access, or assert violations. "
                     )
                     description += (
-                        "Note that explicit `assert()` should only be used to check invariants. " 
+                        "Note that explicit `assert()` should only be used to check invariants. "
                         "Use `require()` for regular input checking. "
                     )
 
-                    debug = (
+                    debug = "Transaction Sequence: " + str(
-                        "The exception is triggered under the following conditions:\n\n"
+                        solver.get_transaction_sequence(state, node.constraints)
                     )
 
-                    debug += solver.pretty_print_model(model)
-
                     issues.append(
                         Issue(
                             contract=node.contract_name,

mythril/analysis/modules/external_calls.py

@@ -5,7 +5,7 @@ from mythril.analysis import solver
 from mythril.analysis.swc_data import REENTRANCY
 import re
 import logging
-
+from mythril.laser.ethereum.cfg import JumpType
 
 """
 MODULE DESCRIPTION:
@@ -16,7 +16,9 @@ Check for call.value()() to external addresses
 MAX_SEARCH_DEPTH = 64
 
 
-def search_children(statespace, node, start_index=0, depth=0, results=None):
+def search_children(
+    statespace, node, transaction_id, start_index=0, depth=0, results=None
+):
     if results is None:
         results = []
     logging.debug("SEARCHING NODE %d", node.uid)
@@ -28,19 +30,21 @@ def search_children(statespace, node, start_index=0, depth=0, results=None):
         if n_states > start_index:
 
             for j in range(start_index, n_states):
-                if node.states[j].get_current_instruction()["opcode"] == "SSTORE":
+                if (
+                    node.states[j].get_current_instruction()["opcode"] == "SSTORE"
+                    and node.states[j].current_transaction.id == transaction_id
+                ):
                     results.append(node.states[j].get_current_instruction()["address"])
-
         children = []
 
         for edge in statespace.edges:
-            if edge.node_from == node.uid:
+            if edge.node_from == node.uid and edge.type != JumpType.Transaction:
                 children.append(statespace.nodes[edge.node_to])
 
         if len(children):
             for node in children:
-                return search_children(
+                results += search_children(
-                    statespace, node, depth=depth + 1, results=results
+                    statespace, node, transaction_id, depth=depth + 1, results=results
                 )
 
     return results
@@ -152,7 +156,12 @@ def execute(statespace):
                     # Check for SSTORE in remaining instructions in current node & nodes down the CFG
 
                     state_change_addresses = search_children(
-                        statespace, call.node, call.state_index + 1, depth=0, results=[]
+                        statespace,
+                        call.node,
+                        call.state.current_transaction.id,
+                        call.state_index + 1,
+                        depth=0,
+                        results=[],
                     )
 
                     logging.debug(

mythril/analysis/modules/integer.py

@@ -100,7 +100,9 @@ def _check_integer_overflow(statespace, state, node):
     )
 
     issue.description = "The arithmetic operation can result in integer overflow.\n"
-    issue.debug = solver.pretty_print_model(model)
+    issue.debug = "Transaction Sequence: " + str(
+        solver.get_transaction_sequence(state, node.constraints)
+    )
     issues.append(issue)
 
     return issues
@@ -211,7 +213,9 @@ def _check_integer_underflow(statespace, state, node):
                     "The substraction can result in an integer underflow.\n"
                 )
 
-                issue.debug = solver.pretty_print_model(model)
+                issue.debug = "Transaction Sequence: " + str(
+                    solver.get_transaction_sequence(state, node.constraints)
+                )
                 issues.append(issue)
 
             except UnsatError:
@@ -292,8 +296,6 @@ def _search_children(
             element = _check_usage(current_state, taint_result)
             if len(element) < 1:
                 continue
-            if _check_requires(element[0], node, statespace, constraint):
-                continue
             results += element
 
     # Recursively search children
@@ -315,24 +317,3 @@ def _search_children(
         )
 
     return results
-
-
-def _check_requires(state, node, statespace, constraint):
-    """Checks if usage of overflowed statement results in a revert statement"""
-    instruction = state.get_current_instruction()
-    if instruction["opcode"] is not "JUMPI":
-        return False
-    children = [
-        statespace.nodes[edge.node_to]
-        for edge in statespace.edges
-        if edge.node_from == node.uid
-    ]
-
-    for child in children:
-        opcodes = [s.get_current_instruction()["opcode"] for s in child.states]
-        if "REVERT" in opcodes or "ASSERT_FAIL" in opcodes:
-            return True
-    # I added the following case, bc of false positives if the max depth is not high enough
-    if len(children) == 0:
-        return True
-    return False

mythril/analysis/modules/multiple_sends.py

@@ -33,7 +33,8 @@ def execute(statespace):
             )
 
             issue.description = (
-                "Multiple sends are executed in a single transaction. Try to isolate each external call into its own transaction," 
+                "Multiple sends are executed in a single transaction. "
+                "Try to isolate each external call into its own transaction,"
                 " as external calls can fail accidentally or deliberately.\nConsecutive calls: \n"
             )
 

mythril/analysis/modules/suicide.py

@@ -67,7 +67,11 @@ def _analyze_state(state, node):
     try:
         model = solver.get_model(node.constraints + not_creator_constraints)
 
-        debug = "SOLVER OUTPUT:\n" + solver.pretty_print_model(model)
+        debug = "Transaction Sequence: " + str(
+            solver.get_transaction_sequence(
+                state, node.constraints + not_creator_constraints
+            )
+        )
 
         issue = Issue(
             contract=node.contract_name,

mythril/analysis/modules/transaction_order_dependence.py

@@ -43,7 +43,7 @@ def execute(statespace):
             )
 
             issue.description = (
-                "Possible transaction order dependence vulnerability: The value or " 
+                "Possible transaction order dependence vulnerability: The value or "
                 "direction of the call statement is determined from a tainted storage location"
             )
             issues.append(issue)

mythril/analysis/ops.py

@@ -9,7 +9,6 @@ class VarType(Enum):
 
 
 class Variable:
-
     def __init__(self, val, _type):
         self.val = val
         self.type = _type
@@ -26,7 +25,6 @@ def get_variable(i):
 
 
 class Op:
-
     def __init__(self, node, state, state_index):
         self.node = node
         self.state = state
@@ -34,8 +32,17 @@ class Op:
 
 
 class Call(Op):
-
+    def __init__(
-    def __init__(self, node, state, state_index, _type, to, gas, value=Variable(0, VarType.CONCRETE), data=None):
+        self,
+        node,
+        state,
+        state_index,
+        _type,
+        to,
+        gas,
+        value=Variable(0, VarType.CONCRETE),
+        data=None,
+    ):
 
         super().__init__(node, state, state_index)
         self.to = to
@@ -46,7 +53,6 @@ class Call(Op):
 
 
 class SStore(Op):
-
     def __init__(self, node, state, state_index, value):
         super().__init__(node, state, state_index)
         self.value = value

mythril/analysis/report.py

@@ -2,9 +2,10 @@ import logging
 import json
 import operator
 from jinja2 import PackageLoader, Environment
-import sha3
+import _pysha3 as sha3
 import hashlib
 
+
 class Issue:
     def __init__(
         self,
@@ -36,7 +37,9 @@ class Issue:
             keccak.update(bytes.fromhex(bytecode))
             self.bytecode_hash = "0x" + keccak.hexdigest()
         except ValueError:
-            logging.debug("Unable to change the bytecode to bytes. Bytecode: {}".format(bytecode))
+            logging.debug(
+                "Unable to change the bytecode to bytes. Bytecode: {}".format(bytecode)
+            )
             self.bytecode_hash = ""
 
     @property

mythril/analysis/solver.py

@@ -1,7 +1,11 @@
-from z3 import Solver, simplify, sat, unknown
+from z3 import Solver, simplify, sat, unknown, FuncInterp, UGE
 from mythril.exceptions import UnsatError
+from mythril.laser.ethereum.transaction.transaction_models import (
+    ContractCreationTransaction,
+)
 import logging
 
+
 def get_model(constraints):
     s = Solver()
     s.set("timeout", 100000)
@@ -21,12 +25,88 @@ def pretty_print_model(model):
     ret = ""
 
     for d in model.decls():
+        if type(model[d]) == FuncInterp:
+            condition = model[d].as_list()
+            ret += "%s: %s\n" % (d.name(), condition)
+            continue
 
         try:
             condition = "0x%x" % model[d].as_long()
         except:
             condition = str(simplify(model[d]))
 
-        ret += ("%s: %s\n" % (d.name(), condition))
+        ret += "%s: %s\n" % (d.name(), condition)
 
     return ret
+
+
+def get_transaction_sequence(global_state, constraints):
+    """
+    Generate concrete transaction sequence
+
+    :param global_state: GlobalState to generate transaction sequence for
+    :param constraints: list of constraints used to generate transaction sequence
+    :param caller: address of caller
+    :param max_callvalue: maximum callvalue for a transaction
+    """
+
+    transaction_sequence = global_state.world_state.transaction_sequence
+
+    # gaslimit & gasprice don't exist yet
+    tx_template = {
+        "calldata": None,
+        "call_value": None,
+        "caller": "0xCA11EDEADBEEF37E636E6CA11EDEADBEEFCA11ED",
+    }
+
+    txs = {}
+    creation_tx_ids = []
+    tx_constraints = constraints.copy()
+
+    for transaction in transaction_sequence:
+        tx_id = str(transaction.id)
+        if not isinstance(transaction, ContractCreationTransaction):
+
+            # Constrain calldatasize
+            max_calldatasize = 5000
+            if max_calldatasize != None:
+                tx_constraints.append(
+                    UGE(max_calldatasize, transaction.call_data.calldatasize)
+                )
+
+            txs[tx_id] = tx_template.copy()
+
+        else:
+            creation_tx_ids.append(tx_id)
+
+    model = get_model(tx_constraints)
+
+    for transaction in transaction_sequence:
+        if not isinstance(transaction, ContractCreationTransaction):
+            tx_id = str(transaction.id)
+
+            txs[tx_id]["calldata"] = "0x" + "".join(
+                [
+                    hex(b)[2:] if len(hex(b)) % 2 == 0 else "0" + hex(b)[2:]
+                    for b in transaction.call_data.concretized(model)
+                ]
+            )
+
+    for d in model.decls():
+        name = d.name()
+
+        if "call_value" in name:
+            tx_id = name.replace("call_value", "")
+            if not tx_id in creation_tx_ids:
+                call_value = "0x%x" % model[d].as_long()
+
+                txs[tx_id]["call_value"] = call_value
+
+        if "caller" in name:
+            # caller is 'creator' for creation transactions
+            tx_id = name.replace("caller", "")
+            caller = "0x" + ("%x" % model[d].as_long()).zfill(64)
+
+            txs[tx_id]["caller"] = caller
+
+    return txs

mythril/analysis/swc_data.py

@@ -1,25 +1,27 @@
-DEFAULT_FUNCTION_VISIBILITY = '100'
+DEFAULT_FUNCTION_VISIBILITY = "100"
-INTEGER_OVERFLOW_AND_UNDERFLOW = '101'
+INTEGER_OVERFLOW_AND_UNDERFLOW = "101"
-OUTDATED_COMPILER_VERSION = '102'
+OUTDATED_COMPILER_VERSION = "102"
-FLOATING_PRAGMA = '103'
+FLOATING_PRAGMA = "103"
-UNCHECKED_RET_VAL = '104'
+UNCHECKED_RET_VAL = "104"
-UNPROTECTED_ETHER_WITHDRAWAL = '105'
+UNPROTECTED_ETHER_WITHDRAWAL = "105"
-UNPROTECTED_SELFDESTRUCT = '106'
+UNPROTECTED_SELFDESTRUCT = "106"
-REENTRANCY = '107'
+REENTRANCY = "107"
-DEFAULT_STATE_VARIABLE_VISIBILITY = '108'
+DEFAULT_STATE_VARIABLE_VISIBILITY = "108"
-UNINITIALIZED_STORAGE_POINTER = '109'
+UNINITIALIZED_STORAGE_POINTER = "109"
-ASSERT_VIOLATION = '110'
+ASSERT_VIOLATION = "110"
-DEPRICATED_FUNCTIONS_USAGE = '111'
+DEPRICATED_FUNCTIONS_USAGE = "111"
-DELEGATECALL_TO_UNTRUSTED_CONTRACT = '112'
+DELEGATECALL_TO_UNTRUSTED_CONTRACT = "112"
-MULTIPLE_SENDS = '113'
+MULTIPLE_SENDS = "113"
-TX_ORDER_DEPENDENCE = '114'
+TX_ORDER_DEPENDENCE = "114"
-TX_ORIGIN_USAGE = '115'
+TX_ORIGIN_USAGE = "115"
-TIMESTAMP_DEPENDENCE = '116'
+TIMESTAMP_DEPENDENCE = "116"
 # TODO: SWC ID 116 is missing, Add it if it's added to the https://github.com/SmartContractSecurity/SWC-registry
-INCORRECT_CONSTRUCTOR_NAME = '118'
+INCORRECT_CONSTRUCTOR_NAME = "118"
-SHADOWING_STATE_VARIABLES = '119'
+SHADOWING_STATE_VARIABLES = "119"
-WEAK_RANDOMNESS = '120'
+WEAK_RANDOMNESS = "120"
-SIGNATURE_REPLAY = '121'
+SIGNATURE_REPLAY = "121"
-IMPROPER_VERIFICATION_BASED_ON_MSG_SENDER = '122'
+IMPROPER_VERIFICATION_BASED_ON_MSG_SENDER = "122"
 
-PREDICTABLE_VARS_DEPENDENCE = 'N/A'    # TODO: Add the swc id when this is added to the SWC Registry
+PREDICTABLE_VARS_DEPENDENCE = (
+    "N/A"
+)  # TODO: Add the swc id when this is added to the SWC Registry

mythril/analysis/symbolic.py

@@ -4,8 +4,12 @@ from mythril.ether.soliditycontract import SolidityContract
 import copy
 import logging
 from .ops import get_variable, SStore, Call, VarType
-from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy, BreadthFirstSearchStrategy, \
+from mythril.laser.ethereum.strategy.basic import (
-    ReturnRandomNaivelyStrategy, ReturnWeightedRandomStrategy
+    DepthFirstSearchStrategy,
+    BreadthFirstSearchStrategy,
+    ReturnRandomNaivelyStrategy,
+    ReturnWeightedRandomStrategy,
+)
 
 
 class SymExecWrapper:
@@ -14,31 +18,52 @@ class SymExecWrapper:
     Wrapper class for the LASER Symbolic virtual machine. Symbolically executes the code and does a bit of pre-analysis for convenience.
     """
 
-    def __init__(self, contract, address, strategy, dynloader=None, max_depth=22,
+    def __init__(
-                 execution_timeout=None, create_timeout=None, max_transaction_count=3):
+        self,
-
+        contract,
-        if strategy == 'dfs':
+        address,
+        strategy,
+        dynloader=None,
+        max_depth=22,
+        execution_timeout=None,
+        create_timeout=None,
+        max_transaction_count=3,
+    ):
+
+        if strategy == "dfs":
             s_strategy = DepthFirstSearchStrategy
-        elif strategy == 'bfs':
+        elif strategy == "bfs":
             s_strategy = BreadthFirstSearchStrategy
-        elif strategy == 'naive-random':
+        elif strategy == "naive-random":
             s_strategy = ReturnRandomNaivelyStrategy
-        elif strategy == 'weighted-random':
+        elif strategy == "weighted-random":
             s_strategy = ReturnWeightedRandomStrategy
         else:
             raise ValueError("Invalid strategy argument supplied")
 
-        account = Account(address, contract.disassembly, dynamic_loader=dynloader, contract_name=contract.name)
+        account = Account(
+            address,
+            contract.disassembly,
+            dynamic_loader=dynloader,
+            contract_name=contract.name,
+        )
 
         self.accounts = {address: account}
 
-        self.laser = svm.LaserEVM(self.accounts, dynamic_loader=dynloader, max_depth=max_depth,
+        self.laser = svm.LaserEVM(
-                                  execution_timeout=execution_timeout, strategy=s_strategy,
+            self.accounts,
-                                  create_timeout=create_timeout,
+            dynamic_loader=dynloader,
-                                  max_transaction_count=max_transaction_count)
+            max_depth=max_depth,
+            execution_timeout=execution_timeout,
+            strategy=s_strategy,
+            create_timeout=create_timeout,
+            max_transaction_count=max_transaction_count,
+        )
 
         if isinstance(contract, SolidityContract):
-            self.laser.sym_exec(creation_code=contract.creation_code, contract_name=contract.name)
+            self.laser.sym_exec(
+                creation_code=contract.creation_code, contract_name=contract.name
+            )
         else:
             self.laser.sym_exec(address)
 
@@ -58,31 +83,72 @@ class SymExecWrapper:
 
                 instruction = state.get_current_instruction()
 
-                op = instruction['opcode']
+                op = instruction["opcode"]
 
-                if op in ('CALL', 'CALLCODE', 'DELEGATECALL', 'STATICCALL'):
+                if op in ("CALL", "CALLCODE", "DELEGATECALL", "STATICCALL"):
 
                     stack = state.mstate.stack
 
-                    if op in ('CALL', 'CALLCODE'):
+                    if op in ("CALL", "CALLCODE"):
-                        gas, to, value, meminstart, meminsz, memoutstart, memoutsz = \
+                        gas, to, value, meminstart, meminsz, memoutstart, memoutsz = (
-                            get_variable(stack[-1]), get_variable(stack[-2]), get_variable(stack[-3]), get_variable(stack[-4]), get_variable(stack[-5]), get_variable(stack[-6]), get_variable(stack[-7])
+                            get_variable(stack[-1]),
+                            get_variable(stack[-2]),
+                            get_variable(stack[-3]),
+                            get_variable(stack[-4]),
+                            get_variable(stack[-5]),
+                            get_variable(stack[-6]),
+                            get_variable(stack[-7]),
+                        )
 
                         if to.type == VarType.CONCRETE and to.val < 5:
-                                # ignore prebuilts
+                            # ignore prebuilts
-                                continue
+                            continue
-
+
-                        if meminstart.type == VarType.CONCRETE and meminsz.type == VarType.CONCRETE:
+                        if (
-                            self.calls.append(Call(self.nodes[key], state, state_index, op, to, gas, value, state.mstate.memory[meminstart.val:meminsz.val * 4]))
+                            meminstart.type == VarType.CONCRETE
+                            and meminsz.type == VarType.CONCRETE
+                        ):
+                            self.calls.append(
+                                Call(
+                                    self.nodes[key],
+                                    state,
+                                    state_index,
+                                    op,
+                                    to,
+                                    gas,
+                                    value,
+                                    state.mstate.memory[
+                                        meminstart.val : meminsz.val * 4
+                                    ],
+                                )
+                            )
                         else:
-                            self.calls.append(Call(self.nodes[key], state, state_index, op, to, gas, value))
+                            self.calls.append(
+                                Call(
+                                    self.nodes[key],
+                                    state,
+                                    state_index,
+                                    op,
+                                    to,
+                                    gas,
+                                    value,
+                                )
+                            )
                     else:
-                        gas, to, meminstart, meminsz, memoutstart, memoutsz = \
+                        gas, to, meminstart, meminsz, memoutstart, memoutsz = (
-                            get_variable(stack[-1]), get_variable(stack[-2]), get_variable(stack[-3]), get_variable(stack[-4]), get_variable(stack[-5]), get_variable(stack[-6])
+                            get_variable(stack[-1]),
-
+                            get_variable(stack[-2]),
-                        self.calls.append(Call(self.nodes[key], state, state_index, op, to, gas))
+                            get_variable(stack[-3]),
-
+                            get_variable(stack[-4]),
-                elif op == 'SSTORE':
+                            get_variable(stack[-5]),
+                            get_variable(stack[-6]),
+                        )
+
+                        self.calls.append(
+                            Call(self.nodes[key], state, state_index, op, to, gas)
+                        )
+
+                elif op == "SSTORE":
                     stack = copy.deepcopy(state.mstate.stack)
                     address = state.environment.active_account.address
 
@@ -94,9 +160,13 @@ class SymExecWrapper:
                         self.sstors[address] = {}
 
                     try:
-                        self.sstors[address][str(index)].append(SStore(self.nodes[key], state, state_index, value))
+                        self.sstors[address][str(index)].append(
+                            SStore(self.nodes[key], state, state_index, value)
+                        )
                     except KeyError:
-                        self.sstors[address][str(index)] = [SStore(self.nodes[key], state, state_index, value)]
+                        self.sstors[address][str(index)] = [
+                            SStore(self.nodes[key], state, state_index, value)
+                        ]
 
                 state_index += 1
 

mythril/analysis/traceexplore.py

@@ -3,32 +3,64 @@ from mythril.laser.ethereum.svm import NodeFlags
 import re
 
 colors = [
-    {'border': '#26996f', 'background': '#2f7e5b', 'highlight': {'border': '#fff', 'background': '#28a16f'}},
+    {
-    {'border': '#9e42b3', 'background': '#842899', 'highlight': {'border': '#fff', 'background': '#933da6'}},
+        "border": "#26996f",
-    {'border': '#b82323', 'background': '#991d1d', 'highlight': {'border': '#fff', 'background': '#a61f1f'}},
+        "background": "#2f7e5b",
-    {'border': '#4753bf', 'background': '#3b46a1', 'highlight': {'border': '#fff', 'background': '#424db3'}},
+        "highlight": {"border": "#fff", "background": "#28a16f"},
-    {'border': '#26996f', 'background': '#2f7e5b', 'highlight': {'border': '#fff', 'background': '#28a16f'}},
+    },
-    {'border': '#9e42b3', 'background': '#842899', 'highlight': {'border': '#fff', 'background': '#933da6'}},
+    {
-    {'border': '#b82323', 'background': '#991d1d', 'highlight': {'border': '#fff', 'background': '#a61f1f'}},
+        "border": "#9e42b3",
-    {'border': '#4753bf', 'background': '#3b46a1', 'highlight': {'border': '#fff', 'background': '#424db3'}},
+        "background": "#842899",
+        "highlight": {"border": "#fff", "background": "#933da6"},
+    },
+    {
+        "border": "#b82323",
+        "background": "#991d1d",
+        "highlight": {"border": "#fff", "background": "#a61f1f"},
+    },
+    {
+        "border": "#4753bf",
+        "background": "#3b46a1",
+        "highlight": {"border": "#fff", "background": "#424db3"},
+    },
+    {
+        "border": "#26996f",
+        "background": "#2f7e5b",
+        "highlight": {"border": "#fff", "background": "#28a16f"},
+    },
+    {
+        "border": "#9e42b3",
+        "background": "#842899",
+        "highlight": {"border": "#fff", "background": "#933da6"},
+    },
+    {
+        "border": "#b82323",
+        "background": "#991d1d",
+        "highlight": {"border": "#fff", "background": "#a61f1f"},
+    },
+    {
+        "border": "#4753bf",
+        "background": "#3b46a1",
+        "highlight": {"border": "#fff", "background": "#424db3"},
+    },
 ]
 
 
 def get_serializable_statespace(statespace):
     nodes = []
     edges = []
-    
+
     color_map = {}
     i = 0
     for k in statespace.accounts:
         color_map[statespace.accounts[k].contract_name] = colors[i]
         i += 1
-    
+
     for node_key in statespace.nodes:
 
         node = statespace.nodes[node_key]
 
-        code = node.get_cfg_dict()['code']
+        code = node.get_cfg_dict()["code"]
         code = re.sub("([0-9a-f]{8})[0-9a-f]+", lambda m: m.group(1) + "(...)", code)
 
         if NodeFlags.FUNC_ENTRY in node.flags:
@@ -36,47 +68,51 @@ def get_serializable_statespace(statespace):
 
         code_split = code.split("\\n")
 
-        truncated_code = code if (len(code_split) < 7) else "\\n".join(code_split[:6]) + "\\n(click to expand +)"
+        truncated_code = (
+            code
+            if (len(code_split) < 7)
+            else "\\n".join(code_split[:6]) + "\\n(click to expand +)"
+        )
+
+        color = color_map[node.get_cfg_dict()["contract_name"]]
 
-        color = color_map[node.get_cfg_dict()['contract_name']]
-                
         def get_state_accounts(node_state):
             state_accounts = []
             for key in node_state.accounts:
                 account = node_state.accounts[key].as_dict
-                account.pop('code', None)
+                account.pop("code", None)
-                account['balance'] = str(account['balance'])
+                account["balance"] = str(account["balance"])
-                
+
                 storage = {}
-                for storage_key in account['storage']:
+                for storage_key in account["storage"]:
-                    storage[str(storage_key)] = str(account['storage'][storage_key])
+                    storage[str(storage_key)] = str(account["storage"][storage_key])
-            
+
-                state_accounts.append({
+                state_accounts.append({"address": key, "storage": storage})
-                    'address': key,
+            return state_accounts
-                    'storage': storage
+
-                })  
+        states = [
-            return state_accounts          
+            {"machine": x.mstate.as_dict, "accounts": get_state_accounts(x)}
-                
+            for x in node.states
-        states = [{'machine': x.mstate.as_dict, 'accounts': get_state_accounts(x)} for x in node.states]
+        ]
-        
+
         for state in states:
-            state['machine']['stack'] = [str(s) for s in state['machine']['stack']]
+            state["machine"]["stack"] = [str(s) for s in state["machine"]["stack"]]
-            state['machine']['memory'] = [str(m) for m in state['machine']['memory']]
+            state["machine"]["memory"] = [str(m) for m in state["machine"]["memory"]]
-        
+
-        truncated_code = truncated_code.replace('\\n', '\n')
+        truncated_code = truncated_code.replace("\\n", "\n")
-        code = code.replace('\\n', '\n')
+        code = code.replace("\\n", "\n")
-        
+
         s_node = {
-            'id': str(node_key),
+            "id": str(node_key),
-            'func': str(node.function_name),
+            "func": str(node.function_name),
-            'label': truncated_code,
+            "label": truncated_code,
-            'code': code,
+            "code": code,
-            'truncated': truncated_code,
+            "truncated": truncated_code,
-            'states': states,
+            "states": states,
-            'color': color,
+            "color": color,
-            'instructions': code.split('\n')
+            "instructions": code.split("\n"),
         }
-        
+
         nodes.append(s_node)
 
     for edge in statespace.edges:
@@ -90,20 +126,19 @@ def get_serializable_statespace(statespace):
             except Z3Exception:
                 label = str(edge.condition).replace("\n", "")
 
-        label = re.sub("([^_])([\d]{2}\d+)", lambda m: m.group(1) + hex(int(m.group(2))), label)
+        label = re.sub(
+            "([^_])([\d]{2}\d+)", lambda m: m.group(1) + hex(int(m.group(2))), label
+        )
         code = re.sub("([0-9a-f]{8})[0-9a-f]+", lambda m: m.group(1) + "(...)", code)
 
         s_edge = {
-            'from': str(edge.as_dict['from']),
+            "from": str(edge.as_dict["from"]),
-            'to': str(edge.as_dict['to']),
+            "to": str(edge.as_dict["to"]),
-            'arrows': 'to',
+            "arrows": "to",
-            'label': label,
+            "label": label,
-            'smooth': { 'type': "cubicBezier" }
+            "smooth": {"type": "cubicBezier"},
         }
-        
+
         edges.append(s_edge)
 
-    return {
+    return {"edges": edges, "nodes": nodes}
-        'edges': edges,
-        'nodes': nodes
-    }

mythril/disassembler/asm.py

@@ -11,6 +11,7 @@ opcodes[254] = ["ASSERT_FAIL", 0, 0, 0]
 
 class EvmInstruction:
     """ Model to hold the information of the disassembly """
+
     def __init__(self, address, op_code, argument=None):
         self.address = address
         self.op_code = op_code
@@ -23,7 +24,7 @@ class EvmInstruction:
         return result
 
 
-def instruction_list_to_easm(instruction_list: dict) -> str:
+def instruction_list_to_easm(instruction_list: list) -> str:
     result = ""
 
     for instruction in instruction_list:
@@ -66,7 +67,7 @@ def is_sequence_match(pattern: list, instruction_list: list, index: int) -> bool
     """
     for index, pattern_slot in enumerate(pattern, start=index):
         try:
-            if not instruction_list[index]['opcode'] in pattern_slot:
+            if not instruction_list[index]["opcode"] in pattern_slot:
                 return False
         except IndexError:
             return False
@@ -95,7 +96,7 @@ def disassemble(bytecode: str) -> list:
 
         match = re.search(regex_PUSH, op_code_name)
         if match:
-            argument_bytes = bytecode[address + 1: address + 1 + int(match.group(1))]
+            argument_bytes = bytecode[address + 1 : address + 1 + int(match.group(1))]
             current_instruction.argument = "0x" + argument_bytes.hex()
             address += int(match.group(1))
 

mythril/disassembler/disassembly.py

@@ -5,57 +5,92 @@ import logging
 
 
 class Disassembly(object):
+    """
+    Disassembly class
 
-    def __init__(self, code, enable_online_lookup=False):
+    Stores bytecode, and its disassembly.
+    Additionally it will gather the following information on the existing functions in the disassembled code:
+     - function hashes
+     - function name to entry point mapping
+     - function entry point to function name mapping
+    """
+
+    def __init__(self, code: str, enable_online_lookup: bool = False):
+        self.bytecode = code
         self.instruction_list = asm.disassemble(util.safe_decode(code))
+
         self.func_hashes = []
-        self.func_to_addr = {}
+        self.function_name_to_address = {}
-        self.addr_to_func = {}
+        self.address_to_function_name = {}
-        self.bytecode = code
 
-        signatures = SignatureDb(enable_online_lookup=enable_online_lookup)  # control if you want to have online sighash lookups
+        signatures = SignatureDb(
+            enable_online_lookup=enable_online_lookup
+        )  # control if you want to have online signature hash lookups
         try:
             signatures.open()  # open from default locations
         except FileNotFoundError:
-            logging.info("Missing function signature file. Resolving of function names from signature file disabled.")
+            logging.info(
-
+                "Missing function signature file. Resolving of function names from signature file disabled."
-        # Parse jump table & resolve function names
+            )
 
         # Need to take from PUSH1 to PUSH4 because solc seems to remove excess 0s at the beginning for optimizing
-        jmptable_indices = asm.find_op_code_sequence([("PUSH1", "PUSH2", "PUSH3", "PUSH4"), ("EQ",)],
+        jump_table_indices = asm.find_op_code_sequence(
-                                                    self.instruction_list)
+            [("PUSH1", "PUSH2", "PUSH3", "PUSH4"), ("EQ",)], self.instruction_list
-
+        )
-        for i in jmptable_indices:
+
-            func_hash = self.instruction_list[i]['argument']
+        for index in jump_table_indices:
-
+            function_hash, jump_target, function_name = get_function_info(
-            # Append with missing 0s at the beginning
+                index, self.instruction_list, signatures
-            func_hash = "0x" + func_hash[2:].rjust(8, "0")
+            )
-
+            self.func_hashes.append(function_hash)
-            self.func_hashes.append(func_hash)
+
-            try:
+            if jump_target is not None and function_name is not None:
-                # tries local cache, file and optional online lookup
+                self.function_name_to_address[function_name] = jump_target
-                # may return more than one function signature. since we cannot probe for the correct one we'll use the first
+                self.address_to_function_name[jump_target] = function_name
-                func_names = signatures.get(func_hash)
-                if len(func_names) > 1:
-                    # ambigious result
-                    func_name = "**ambiguous** %s" % func_names[0]  # return first hit but note that result was ambiguous
-                else:
-                    # only one item
-                    func_name = func_names[0]
-            except KeyError:
-                func_name = "_function_" + func_hash
-
-            try:
-                offset = self.instruction_list[i + 2]['argument']
-                jump_target = int(offset, 16)
-
-                self.func_to_addr[func_name] = jump_target
-                self.addr_to_func[jump_target] = func_name
-            except:
-                continue
 
         signatures.write()  # store resolved signatures (potentially resolved online)
 
     def get_easm(self):
-        # todo: tintinweb - print funcsig resolved data from self.addr_to_func?
         return asm.instruction_list_to_easm(self.instruction_list)
+
+
+def get_function_info(
+    index: int, instruction_list: list, signature_database: SignatureDb
+) -> (str, int, str):
+    """
+    Finds the function information for a call table entry
+    Solidity uses the first 4 bytes of the calldata to indicate which function the message call should execute
+    The generated code that directs execution to the correct function looks like this:
+    - PUSH function_hash
+    - EQ
+    - PUSH entry_point
+    - JUMPI
+
+    This function takes an index that points to the first instruction, and from that finds out the function hash,
+    function entry and the function name.
+
+    :param index: Start of the entry pattern
+    :param instruction_list: Instruction list for the contract that is being analyzed
+    :param signature_database: Database used to map function hashes to their respective function names
+    :return: function hash, function entry point, function name
+    """
+
+    # Append with missing 0s at the beginning
+    function_hash = "0x" + instruction_list[index]["argument"][2:].rjust(8, "0")
+
+    function_names = signature_database.get(function_hash)
+    if len(function_names) > 1:
+        # In this case there was an ambiguous result
+        function_name = "**ambiguous** {}".format(function_names[0])
+    elif len(function_names) == 1:
+        function_name = function_names[0]
+    else:
+        function_name = "_function_" + function_hash
+
+    try:
+        offset = instruction_list[index + 2]["argument"]
+        entry_point = int(offset, 16)
+    except (KeyError, IndexError):
+        return function_hash, None, None
+
+    return function_hash, entry_point, function_name

mythril/ether/ethcontract.py

@@ -5,30 +5,33 @@ import re
 
 
 class ETHContract(persistent.Persistent):
+    def __init__(
+        self, code, creation_code="", name="Unknown", enable_online_lookup=False
+    ):
 
-    def __init__(self, code, creation_code="", name="Unknown", enable_online_lookup=False):
-        
         # Workaround: We currently do not support compile-time linking.
         # Dynamic contract addresses of the format __[contract-name]_____________ are replaced with a generic address
         # Apply this for creation_code & code
 
-        creation_code = re.sub(r'(_{2}.{38})', 'aa' * 20, creation_code)
+        creation_code = re.sub(r"(_{2}.{38})", "aa" * 20, creation_code)
-        code = re.sub(r'(_{2}.{38})', 'aa' * 20, code)
+        code = re.sub(r"(_{2}.{38})", "aa" * 20, code)
 
         self.creation_code = creation_code
         self.name = name
         self.code = code
         self.disassembly = Disassembly(code, enable_online_lookup=enable_online_lookup)
-        self.creation_disassembly = Disassembly(creation_code, enable_online_lookup=enable_online_lookup)
+        self.creation_disassembly = Disassembly(
+            creation_code, enable_online_lookup=enable_online_lookup
+        )
 
     def as_dict(self):
 
         return {
-            'address': self.address,
+            "address": self.address,
-            'name': self.name,
+            "name": self.name,
-            'code': self.code,
+            "code": self.code,
-            'creation_code': self.creation_code,
+            "creation_code": self.creation_code,
-            'disassembly': self.disassembly
+            "disassembly": self.disassembly,
         }
 
     def get_easm(self):
@@ -37,7 +40,7 @@ class ETHContract(persistent.Persistent):
 
     def matches_expression(self, expression):
 
-        str_eval = ''
+        str_eval = ""
         easm_code = None
 
         tokens = re.split("\s+(and|or|not)\s+", expression, re.IGNORECASE)
@@ -48,23 +51,23 @@ class ETHContract(persistent.Persistent):
                 str_eval += " " + token + " "
                 continue
 
-            m = re.match(r'^code#([a-zA-Z0-9\s,\[\]]+)#', token)
+            m = re.match(r"^code#([a-zA-Z0-9\s,\[\]]+)#", token)
 
             if m:
                 if easm_code is None:
                     easm_code = self.get_easm()
 
                 code = m.group(1).replace(",", "\\n")
-                str_eval += "\"" + code + "\" in easm_code"
+                str_eval += '"' + code + '" in easm_code'
                 continue
 
-            m = re.match(r'^func#([a-zA-Z0-9\s_,(\\)\[\]]+)#$', token)
+            m = re.match(r"^func#([a-zA-Z0-9\s_,(\\)\[\]]+)#$", token)
 
             if m:
 
                 sign_hash = "0x" + utils.sha3(m.group(1))[:4].hex()
 
-                str_eval += "\"" + sign_hash + "\" in self.disassembly.func_hashes"
+                str_eval += '"' + sign_hash + '" in self.disassembly.func_hashes'
 
                 continue
 

mythril/ether/evm.py

@@ -8,7 +8,12 @@ import re
 
 
 def trace(code, calldata=""):
-    log_handlers = ['eth.vm.op', 'eth.vm.op.stack', 'eth.vm.op.memory', 'eth.vm.op.storage']
+    log_handlers = [
+        "eth.vm.op",
+        "eth.vm.op.stack",
+        "eth.vm.op.memory",
+        "eth.vm.op.storage",
+    ]
     output = StringIO()
     stream_handler = StreamHandler(output)
 
@@ -17,7 +22,7 @@ def trace(code, calldata=""):
         log_vm_op.setLevel("TRACE")
         log_vm_op.addHandler(stream_handler)
 
-    addr = bytes.fromhex('0123456789ABCDEF0123456789ABCDEF01234567')
+    addr = bytes.fromhex("0123456789ABCDEF0123456789ABCDEF01234567")
     state = State()
 
     ext = messages.VMExt(state, transactions.Transaction(0, 0, 21000, addr, 0, addr))
@@ -29,14 +34,14 @@ def trace(code, calldata=""):
 
     state_trace = []
     for line in lines:
-        m = re.search(r'pc=b\'(\d+)\'.*op=([A-Z0-9]+)', line)
+        m = re.search(r"pc=b\'(\d+)\'.*op=([A-Z0-9]+)", line)
         if m:
             pc = m.group(1)
             op = m.group(2)
-            m = re.match(r'.*stack=(\[.*?\])', line)
+            m = re.match(r".*stack=(\[.*?\])", line)
 
             if m:
-                stackitems = re.findall(r'b\'(\d+)\'', m.group(1))
+                stackitems = re.findall(r"b\'(\d+)\'", m.group(1))
                 stack = "["
 
                 if len(stackitems):
@@ -48,11 +53,13 @@ def trace(code, calldata=""):
             else:
                 stack = "[]"
 
-            if re.match(r'^PUSH.*', op):
+            if re.match(r"^PUSH.*", op):
-                val = re.search(r'pushvalue=(\d+)', line).group(1)
+                val = re.search(r"pushvalue=(\d+)", line).group(1)
                 pushvalue = hex(int(val))
-                state_trace.append({'pc': pc, 'op': op, 'stack': stack, 'pushvalue': pushvalue})
+                state_trace.append(
+                    {"pc": pc, "op": op, "stack": stack, "pushvalue": pushvalue}
+                )
             else:
-                state_trace.append({'pc': pc, 'op': op, 'stack': stack})
+                state_trace.append({"pc": pc, "op": op, "stack": stack})
 
     return state_trace

mythril/ether/soliditycontract.py

@@ -5,7 +5,6 @@ from mythril.exceptions import NoContractFoundError
 
 
 class SourceMapping:
-
     def __init__(self, solidity_file_idx, offset, length, lineno):
         self.solidity_file_idx = solidity_file_idx
         self.offset = offset
@@ -14,14 +13,12 @@ class SourceMapping:
 
 
 class SolidityFile:
-
     def __init__(self, filename, data):
         self.filename = filename
         self.data = data
 
 
 class SourceCodeInfo:
-
     def __init__(self, filename, lineno, code):
         self.filename = filename
         self.lineno = lineno
@@ -30,22 +27,21 @@ class SourceCodeInfo:
 
 def get_contracts_from_file(input_file, solc_args=None):
     data = get_solc_json(input_file, solc_args=solc_args)
-    for key, contract in data['contracts'].items():
+    for key, contract in data["contracts"].items():
         filename, name = key.split(":")
-        if filename == input_file and len(contract['bin-runtime']):
+        if filename == input_file and len(contract["bin-runtime"]):
             yield SolidityContract(input_file, name, solc_args)
 
 
 class SolidityContract(ETHContract):
-
     def __init__(self, input_file, name=None, solc_args=None):
 
         data = get_solc_json(input_file, solc_args=solc_args)
 
         self.solidity_files = []
 
-        for filename in data['sourceList']:
+        for filename in data["sourceList"]:
-            with open(filename, 'r', encoding='utf-8') as file:
+            with open(filename, "r", encoding="utf-8") as file:
                 code = file.read()
                 self.solidity_files.append(SolidityFile(filename, code))
 
@@ -55,28 +51,32 @@ class SolidityContract(ETHContract):
         srcmap_constructor = []
         srcmap = []
         if name:
-            for key, contract in sorted(data['contracts'].items()):
+            for key, contract in sorted(data["contracts"].items()):
                 filename, _name = key.split(":")
 
-                if filename == input_file and name == _name and len(contract['bin-runtime']):
+                if (
-                    code = contract['bin-runtime']
+                    filename == input_file
-                    creation_code = contract['bin']
+                    and name == _name
-                    srcmap = contract['srcmap-runtime'].split(";")
+                    and len(contract["bin-runtime"])
-                    srcmap_constructor = contract['srcmap'].split(";")
+                ):
+                    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 key, contract in sorted(data["contracts"].items()):
                 filename, name = key.split(":")
 
-                if filename == input_file and len(contract['bin-runtime']):
+                if filename == input_file and len(contract["bin-runtime"]):
-                    code = contract['bin-runtime']
+                    code = contract["bin-runtime"]
-                    creation_code = contract['bin']
+                    creation_code = contract["bin"]
-                    srcmap = contract['srcmap-runtime'].split(";")
+                    srcmap = contract["srcmap-runtime"].split(";")
-                    srcmap_constructor = contract['srcmap'].split(";")
+                    srcmap_constructor = contract["srcmap"].split(";")
                     has_contract = True
 
         if not has_contract:
@@ -102,7 +102,9 @@ class SolidityContract(ETHContract):
         offset = mappings[index].offset
         length = mappings[index].length
 
-        code = solidity_file.data.encode('utf-8')[offset:offset + length].decode('utf-8', errors="ignore")
+        code = solidity_file.data.encode("utf-8")[offset : offset + length].decode(
+            "utf-8", errors="ignore"
+        )
         lineno = mappings[index].lineno
 
         return SourceCodeInfo(filename, lineno, code)
@@ -120,6 +122,11 @@ class SolidityContract(ETHContract):
 
             if len(mapping) > 2 and len(mapping[2]) > 0:
                 idx = int(mapping[2])
-            lineno = self.solidity_files[idx].data.encode('utf-8')[0:offset].count('\n'.encode('utf-8')) + 1
+            lineno = (
+                self.solidity_files[idx]
+                .data.encode("utf-8")[0:offset]
+                .count("\n".encode("utf-8"))
+                + 1
+            )
 
             mappings.append(SourceMapping(idx, offset, length, lineno))

mythril/ether/util.py

@@ -39,9 +39,14 @@ def get_solc_json(file, solc_binary="solc", solc_args=None):
         ret = p.returncode
 
         if ret != 0:
-            raise CompilerError("Solc experienced a fatal error (code %d).\n\n%s" % (ret, stderr.decode('UTF-8')))
+            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.")
+        raise CompilerError(
+            "Compiler not found. Make sure that solc is installed and in PATH, or set the SOLC environment variable."
+        )
 
     out = stdout.decode("UTF-8")
 
@@ -59,7 +64,7 @@ def encode_calldata(func_name, arg_types, args):
 
 
 def get_random_address():
-    return binascii.b2a_hex(os.urandom(20)).decode('UTF-8')
+    return binascii.b2a_hex(os.urandom(20)).decode("UTF-8")
 
 
 def get_indexed_address(index):
@@ -67,7 +72,9 @@ def get_indexed_address(index):
 
 
 def solc_exists(version):
-    solc_binary = os.path.join(os.environ['HOME'], ".py-solc/solc-v" + version, "bin/solc")
+    solc_binary = os.path.join(
+        os.environ["HOME"], ".py-solc/solc-v" + version, "bin/solc"
+    )
     if os.path.exists(solc_binary):
         return True
     else:

mythril/ethereum/interface/leveldb/accountindexing.py

@@ -39,13 +39,13 @@ class ReceiptForStorage(rlp.Serializable):
     """
 
     fields = [
-        ('state_root', binary),
+        ("state_root", binary),
-        ('cumulative_gas_used', big_endian_int),
+        ("cumulative_gas_used", big_endian_int),
-        ('bloom', int256),
+        ("bloom", int256),
-        ('tx_hash', hash32),
+        ("tx_hash", hash32),
-        ('contractAddress', address),
+        ("contractAddress", address),
-        ('logs', CountableList(Log)),
+        ("logs", CountableList(Log)),
-        ('gas_used', big_endian_int)
+        ("gas_used", big_endian_int),
     ]
 
 
@@ -76,7 +76,9 @@ class AccountIndexer(object):
         """
         Processesing method
         """
-        logging.debug("Processing blocks %d to %d" % (startblock, startblock + BATCH_SIZE))
+        logging.debug(
+            "Processing blocks %d to %d" % (startblock, startblock + BATCH_SIZE)
+        )
 
         addresses = []
 
@@ -86,7 +88,9 @@ class AccountIndexer(object):
                 receipts = self.db.reader._get_block_receipts(block_hash, blockNum)
 
                 for receipt in receipts:
-                    if receipt.contractAddress is not None and not all(b == 0 for b in receipt.contractAddress):
+                    if receipt.contractAddress is not None and not all(
+                        b == 0 for b in receipt.contractAddress
+                    ):
                         addresses.append(receipt.contractAddress)
             else:
                 if len(addresses) == 0:
@@ -112,15 +116,21 @@ class AccountIndexer(object):
 
         # in fast sync head block is at 0 (e.g. in fastSync), we can't use it to determine length
         if self.lastBlock is not None and self.lastBlock == 0:
-            self.lastBlock = 2e+9
+            self.lastBlock = 2e9
 
-        if self.lastBlock is None or (self.lastProcessedBlock is not None and self.lastBlock <= self.lastProcessedBlock):
+        if self.lastBlock is None or (
+            self.lastProcessedBlock is not None
+            and self.lastBlock <= self.lastProcessedBlock
+        ):
             return
 
         blockNum = 0
         if self.lastProcessedBlock is not None:
             blockNum = self.lastProcessedBlock + 1
-            print("Updating hash-to-address index from block " + str(self.lastProcessedBlock))
+            print(
+                "Updating hash-to-address index from block "
+                + str(self.lastProcessedBlock)
+            )
         else:
             print("Starting hash-to-address index")
 
@@ -147,7 +157,10 @@ class AccountIndexer(object):
             blockNum = min(blockNum + BATCH_SIZE, self.lastBlock + 1)
 
             cost_time = time.time() - ether.start_time
-            print("%d blocks processed (in %d seconds), %d unique addresses found, next block: %d" % (processed, cost_time, count, min(self.lastBlock, blockNum)))
+            print(
+                "%d blocks processed (in %d seconds), %d unique addresses found, next block: %d"
+                % (processed, cost_time, count, min(self.lastBlock, blockNum))
+            )
 
             self.lastProcessedBlock = blockNum - 1
             self.db.writer._set_last_indexed_number(self.lastProcessedBlock)

mythril/ethereum/interface/leveldb/client.py

@@ -1,7 +1,10 @@
 import binascii
 import rlp
 from mythril.ethereum.interface.leveldb.accountindexing import CountableList
-from mythril.ethereum.interface.leveldb.accountindexing import ReceiptForStorage, AccountIndexer
+from mythril.ethereum.interface.leveldb.accountindexing import (
+    ReceiptForStorage,
+    AccountIndexer,
+)
 import logging
 from ethereum import utils
 from ethereum.block import BlockHeader, Block
@@ -12,17 +15,19 @@ from mythril.exceptions import AddressNotFoundError
 
 # Per https://github.com/ethereum/go-ethereum/blob/master/core/rawdb/schema.go
 # prefixes and suffixes for keys in geth
-header_prefix = b'h'         # header_prefix + num (uint64 big endian) + hash -> header
+header_prefix = b"h"  # header_prefix + num (uint64 big endian) + hash -> header
-body_prefix = b'b'           # body_prefix + num (uint64 big endian) + hash -> block body
+body_prefix = b"b"  # body_prefix + num (uint64 big endian) + hash -> block body
-num_suffix = b'n'            # header_prefix + num (uint64 big endian) + num_suffix -> hash
+num_suffix = b"n"  # header_prefix + num (uint64 big endian) + num_suffix -> hash
-block_hash_prefix = b'H'      # block_hash_prefix + hash -> num (uint64 big endian)
+block_hash_prefix = b"H"  # block_hash_prefix + hash -> num (uint64 big endian)
-block_receipts_prefix = b'r'  # block_receipts_prefix + num (uint64 big endian) + hash -> block receipts
+block_receipts_prefix = (
+    b"r"
+)  # block_receipts_prefix + num (uint64 big endian) + hash -> block receipts
 # known geth keys
-head_header_key = b'LastBlock'  # head (latest) header hash
+head_header_key = b"LastBlock"  # head (latest) header hash
 # custom prefixes
-address_prefix = b'AM'       # address_prefix + hash -> address
+address_prefix = b"AM"  # address_prefix + hash -> address
 # custom keys
-address_mapping_head_key = b'accountMapping'  # head (latest) number of indexed block
+address_mapping_head_key = b"accountMapping"  # head (latest) number of indexed block
 
 
 def _format_block_number(number):
@@ -36,7 +41,7 @@ def _encode_hex(v):
     """
     encodes hash as hex
     """
-    return '0x' + utils.encode_hex(v)
+    return "0x" + utils.encode_hex(v)
 
 
 class LevelDBReader(object):
@@ -83,7 +88,10 @@ class LevelDBReader(object):
             num = self._get_block_number(block_hash)
             self.head_block_header = self._get_block_header(block_hash, num)
             # find header with valid state
-            while not self.db.get(self.head_block_header.state_root) and self.head_block_header.prevhash is not None:
+            while (
+                not self.db.get(self.head_block_header.state_root)
+                and self.head_block_header.prevhash is not None
+            ):
                 block_hash = self.head_block_header.prevhash
                 num = self._get_block_number(block_hash)
                 self.head_block_header = self._get_block_header(block_hash, num)
@@ -192,11 +200,11 @@ class EthLevelDB(object):
                 try:
                     address = _encode_hex(indexer.get_contract_by_hash(address_hash))
                 except AddressNotFoundError:
-                    '''
+                    """
                     The hash->address mapping does not exist in our index. If the index is up-to-date, this likely means
                     that the contract was created by an internal transaction. Skip this contract as right now we don't
                     have a good solution for this.
-                    '''
+                    """
 
                     continue
 
@@ -253,4 +261,6 @@ class EthLevelDB(object):
         gets account storage data at position
         """
         account = self.reader._get_account(address)
-        return _encode_hex(utils.zpad(utils.encode_int(account.get_storage_data(position)), 32))
+        return _encode_hex(
+            utils.zpad(utils.encode_int(account.get_storage_data(position)), 32)
+        )

mythril/ethereum/interface/leveldb/state.py

@@ -1,24 +1,39 @@
 import rlp
 import binascii
-from ethereum.utils import normalize_address, hash32, trie_root, \
+from ethereum.utils import (
-    big_endian_int, address, int256, encode_hex, encode_int, \
+    normalize_address,
-    big_endian_to_int, int_to_addr, zpad, parse_as_bin, parse_as_int, \
+    hash32,
-    decode_hex, sha3, is_string, is_numeric
+    trie_root,
+    big_endian_int,
+    address,
+    int256,
+    encode_hex,
+    encode_int,
+    big_endian_to_int,
+    int_to_addr,
+    zpad,
+    parse_as_bin,
+    parse_as_int,
+    decode_hex,
+    sha3,
+    is_string,
+    is_numeric,
+)
 from rlp.sedes import big_endian_int, Binary, binary, CountableList
 from ethereum import utils
 from ethereum import trie
 from ethereum.trie import Trie
 from ethereum.securetrie import SecureTrie
 
-BLANK_HASH = utils.sha3(b'')
+BLANK_HASH = utils.sha3(b"")
-BLANK_ROOT = utils.sha3rlp(b'')
+BLANK_ROOT = utils.sha3rlp(b"")
 
 STATE_DEFAULTS = {
     "txindex": 0,
     "gas_used": 0,
     "gas_limit": 3141592,
     "block_number": 0,
-    "block_coinbase": '\x00' * 20,
+    "block_coinbase": "\x00" * 20,
     "block_difficulty": 1,
     "timestamp": 0,
     "logs": [],
@@ -37,10 +52,10 @@ class Account(rlp.Serializable):
     """
 
     fields = [
-        ('nonce', big_endian_int),
+        ("nonce", big_endian_int),
-        ('balance', big_endian_int),
+        ("balance", big_endian_int),
-        ('storage', trie_root),
+        ("storage", trie_root),
-        ('code_hash', hash32)
+        ("code_hash", hash32),
     ]
 
     def __init__(self, nonce, balance, storage, code_hash, db, addr):
@@ -69,7 +84,8 @@ class Account(rlp.Serializable):
         if key not in self.storage_cache:
             v = self.storage_trie.get(utils.encode_int32(key))
             self.storage_cache[key] = utils.big_endian_to_int(
-                rlp.decode(v) if v else b'')
+                rlp.decode(v) if v else b""
+            )
         return self.storage_cache[key]
 
     @classmethod
@@ -77,7 +93,7 @@ class Account(rlp.Serializable):
         """
         creates a blank account
         """
-        db.put(BLANK_HASH, b'')
+        db.put(BLANK_HASH, b"")
         o = cls(initial_nonce, 0, trie.BLANK_ROOT, BLANK_HASH, db, addr)
         o.existent_at_start = False
         return o
@@ -88,6 +104,7 @@ class Account(rlp.Serializable):
         """
         return self.nonce == 0 and self.balance == 0 and self.code_hash == BLANK_HASH
 
+
 class State:
     """
     adjusted state from ethereum.state
@@ -106,14 +123,15 @@ class State:
         if addr in self.cache:
             return self.cache[addr]
         rlpdata = self.secure_trie.get(addr)
-        if rlpdata == trie.BLANK_NODE and len(addr) == 32: # support for hashed addresses
+        if (
+            rlpdata == trie.BLANK_NODE and len(addr) == 32
+        ):  # support for hashed addresses
             rlpdata = self.trie.get(addr)
 
         if rlpdata != trie.BLANK_NODE:
             o = rlp.decode(rlpdata, Account, db=self.db, address=addr)
         else:
-            o = Account.blank_account(
+            o = Account.blank_account(self.db, addr, 0)
-                self.db, addr, 0)
         self.cache[addr] = o
         o._mutable = True
         o._cached_rlp = None

mythril/ethereum/interface/rpc/base_client.py

@@ -1,4 +1,4 @@
-from abc import (abstractmethod)
+from abc import abstractmethod
 
 from .constants import BLOCK_TAGS, BLOCK_TAG_LATEST
 from .utils import hex_to_dec, validate_block
@@ -8,13 +8,14 @@ ETH_DEFAULT_RPC_PORT = 8545
 PARITY_DEFAULT_RPC_PORT = 8545
 PYETHAPP_DEFAULT_RPC_PORT = 4000
 MAX_RETRIES = 3
-JSON_MEDIA_TYPE = 'application/json'
+JSON_MEDIA_TYPE = "application/json"
 
-'''
+"""
 This code is adapted from: https://github.com/ConsenSys/ethjsonrpc
-'''
+"""
-class BaseClient(object):
+
 
+class BaseClient(object):
     @abstractmethod
     def _call(self, method, params=None, _id=1):
         pass
@@ -25,7 +26,7 @@ class BaseClient(object):
 
         TESTED
         """
-        return self._call('eth_coinbase')
+        return self._call("eth_coinbase")
 
     def eth_blockNumber(self):
         """
@@ -33,7 +34,7 @@ class BaseClient(object):
 
         TESTED
         """
-        return hex_to_dec(self._call('eth_blockNumber'))
+        return hex_to_dec(self._call("eth_blockNumber"))
 
     def eth_getBalance(self, address=None, block=BLOCK_TAG_LATEST):
         """
@@ -43,7 +44,7 @@ class BaseClient(object):
         """
         address = address or self.eth_coinbase()
         block = validate_block(block)
-        return hex_to_dec(self._call('eth_getBalance', [address, block]))
+        return hex_to_dec(self._call("eth_getBalance", [address, block]))
 
     def eth_getStorageAt(self, address=None, position=0, block=BLOCK_TAG_LATEST):
         """
@@ -52,7 +53,7 @@ class BaseClient(object):
         TESTED
         """
         block = validate_block(block)
-        return self._call('eth_getStorageAt', [address, hex(position), block])
+        return self._call("eth_getStorageAt", [address, hex(position), block])
 
     def eth_getCode(self, address, default_block=BLOCK_TAG_LATEST):
         """
@@ -63,7 +64,7 @@ class BaseClient(object):
         if isinstance(default_block, str):
             if default_block not in BLOCK_TAGS:
                 raise ValueError
-        return self._call('eth_getCode', [address, default_block])
+        return self._call("eth_getCode", [address, default_block])
 
     def eth_getBlockByNumber(self, block=BLOCK_TAG_LATEST, tx_objects=True):
         """
@@ -72,7 +73,7 @@ class BaseClient(object):
         TESTED
         """
         block = validate_block(block)
-        return self._call('eth_getBlockByNumber', [block, tx_objects])
+        return self._call("eth_getBlockByNumber", [block, tx_objects])
 
     def eth_getTransactionReceipt(self, tx_hash):
         """
@@ -80,4 +81,4 @@ class BaseClient(object):
 
         TESTED
         """
-        return self._call('eth_getTransactionReceipt', [tx_hash])
+        return self._call("eth_getTransactionReceipt", [tx_hash])

mythril/ethereum/interface/rpc/client.py

@@ -3,7 +3,12 @@ import logging
 import requests
 from requests.adapters import HTTPAdapter
 from requests.exceptions import ConnectionError as RequestsConnectionError
-from .exceptions import (ConnectionError, BadStatusCodeError, BadJsonError, BadResponseError)
+from .exceptions import (
+    ConnectionError,
+    BadStatusCodeError,
+    BadJsonError,
+    BadResponseError,
+)
 from .base_client import BaseClient
 
 GETH_DEFAULT_RPC_PORT = 8545
@@ -11,17 +16,19 @@ ETH_DEFAULT_RPC_PORT = 8545
 PARITY_DEFAULT_RPC_PORT = 8545
 PYETHAPP_DEFAULT_RPC_PORT = 4000
 MAX_RETRIES = 3
-JSON_MEDIA_TYPE = 'application/json'
+JSON_MEDIA_TYPE = "application/json"
 
-'''
+"""
 This code is adapted from: https://github.com/ConsenSys/ethjsonrpc
-'''
+"""
+
+
 class EthJsonRpc(BaseClient):
     """
     Ethereum JSON-RPC client class
     """
 
-    def __init__(self, host='localhost', port=GETH_DEFAULT_RPC_PORT, tls=False):
+    def __init__(self, host="localhost", port=GETH_DEFAULT_RPC_PORT, tls=False):
         self.host = host
         self.port = port
         self.tls = tls
@@ -31,17 +38,12 @@ class EthJsonRpc(BaseClient):
     def _call(self, method, params=None, _id=1):
 
         params = params or []
-        data = {
+        data = {"jsonrpc": "2.0", "method": method, "params": params, "id": _id}
-            'jsonrpc': '2.0',
+        scheme = "http"
-            'method': method,
-            'params': params,
-            'id': _id,
-        }
-        scheme = 'http'
         if self.tls:
-            scheme += 's'
+            scheme += "s"
-        url = '{}://{}:{}'.format(scheme, self.host, self.port)
+        url = "{}://{}:{}".format(scheme, self.host, self.port)
-        headers = {'Content-Type': JSON_MEDIA_TYPE}
+        headers = {"Content-Type": JSON_MEDIA_TYPE}
         logging.debug("rpc send: %s" % json.dumps(data))
         try:
             r = self.session.post(url, headers=headers, data=json.dumps(data))
@@ -55,7 +57,7 @@ class EthJsonRpc(BaseClient):
         except ValueError:
             raise BadJsonError(r.text)
         try:
-            return response['result']
+            return response["result"]
         except KeyError:
             raise BadResponseError(response)
 

mythril/ethereum/interface/rpc/constants.py

@@ -1,8 +1,4 @@
-BLOCK_TAG_EARLIEST = 'earliest'
+BLOCK_TAG_EARLIEST = "earliest"
-BLOCK_TAG_LATEST   = 'latest'
+BLOCK_TAG_LATEST = "latest"
-BLOCK_TAG_PENDING  = 'pending'
+BLOCK_TAG_PENDING = "pending"
-BLOCK_TAGS = (
+BLOCK_TAGS = (BLOCK_TAG_EARLIEST, BLOCK_TAG_LATEST, BLOCK_TAG_PENDING)
-    BLOCK_TAG_EARLIEST,
-    BLOCK_TAG_LATEST,
-    BLOCK_TAG_PENDING,
-)

mythril/ethereum/interface/rpc/utils.py

@@ -13,12 +13,13 @@ def clean_hex(d):
     Convert decimal to hex and remove the "L" suffix that is appended to large
     numbers
     """
-    return hex(d).rstrip('L')
+    return hex(d).rstrip("L")
+
 
 def validate_block(block):
     if isinstance(block, str):
         if block not in BLOCK_TAGS:
-            raise ValueError('invalid block tag')
+            raise ValueError("invalid block tag")
     if isinstance(block, int):
         block = hex(block)
     return block
@@ -28,11 +29,11 @@ def wei_to_ether(wei):
     """
     Convert wei to ether
     """
-    return 1.0 * wei / 10**18
+    return 1.0 * wei / 10 ** 18
 
 
 def ether_to_wei(ether):
     """
     Convert ether to wei
     """
-    return ether * 10**18
+    return ether * 10 ** 18

mythril/interfaces/cli.py

@@ -7,6 +7,7 @@
 
 import logging, coloredlogs
 import json
+import os
 import sys
 import argparse
 
@@ -19,107 +20,240 @@ import mythril.support.signatures as sigs
 
 
 def exit_with_error(format_, message):
-    if format_ == 'text' or format_ == 'markdown':
+    if format_ == "text" or format_ == "markdown":
         print(message)
     else:
-        result = {'success': False, 'error': str(message), 'issues': []}
+        result = {"success": False, "error": str(message), "issues": []}
         print(json.dumps(result))
     sys.exit()
 
 
 def main():
-    parser = argparse.ArgumentParser(description='Security analysis of Ethereum smart contracts')
+    parser = argparse.ArgumentParser(
-    parser.add_argument("solidity_file", nargs='*')
+        description="Security analysis of Ethereum smart contracts"
-
+    )
-    commands = parser.add_argument_group('commands')
+    parser.add_argument("solidity_file", nargs="*")
-    commands.add_argument('-g', '--graph', help='generate a control flow graph')
+
-    commands.add_argument('-V', '--version', action='store_true',
+    commands = parser.add_argument_group("commands")
-                          help='print the Mythril version number and exit')
+    commands.add_argument("-g", "--graph", help="generate a control flow graph")
-    commands.add_argument('-x', '--fire-lasers', action='store_true',
+    commands.add_argument(
-                          help='detect vulnerabilities, use with -c, -a or solidity file(s)')
+        "-V",
-    commands.add_argument('-t', '--truffle', action='store_true',
+        "--version",
-                          help='analyze a truffle project (run from project dir)')
+        action="store_true",
-    commands.add_argument('-d', '--disassemble', action='store_true', help='print disassembly')
+        help="print the Mythril version number and exit",
-    commands.add_argument('-j', '--statespace-json', help='dumps the statespace json', metavar='OUTPUT_FILE')
+    )
-
+    commands.add_argument(
-    inputs = parser.add_argument_group('input arguments')
+        "-x",
-    inputs.add_argument('-c', '--code', help='hex-encoded bytecode string ("6060604052...")', metavar='BYTECODE')
+        "--fire-lasers",
-    inputs.add_argument('-f', '--codefile', help='file containing hex-encoded bytecode string', 
+        action="store_true",
-            metavar='BYTECODEFILE', type=argparse.FileType('r'))
+        help="detect vulnerabilities, use with -c, -a or solidity file(s)",
-    inputs.add_argument('-a', '--address', help='pull contract from the blockchain', metavar='CONTRACT_ADDRESS')
+    )
-    inputs.add_argument('-l', '--dynld', action='store_true', help='auto-load dependencies from the blockchain')
+    commands.add_argument(
-
+        "-t",
-    outputs = parser.add_argument_group('output formats')
+        "--truffle",
-    outputs.add_argument('-o', '--outform', choices=['text', 'markdown', 'json', 'swc-standard'], default='text',
+        action="store_true",
-                         help='report output format', metavar='<text/markdown/json>')
+        help="analyze a truffle project (run from project dir)",
-    outputs.add_argument('--verbose-report', action='store_true', help='Include debugging information in report')
+    )
-
+    commands.add_argument(
-    database = parser.add_argument_group('local contracts database')
+        "-d", "--disassemble", action="store_true", help="print disassembly"
-    database.add_argument('-s', '--search', help='search the contract database', metavar='EXPRESSION')
+    )
-    database.add_argument('--leveldb-dir', help='specify leveldb directory for search or direct access operations', metavar='LEVELDB_PATH')
+    commands.add_argument(
-
+        "-j",
-    utilities = parser.add_argument_group('utilities')
+        "--statespace-json",
-    utilities.add_argument('--hash', help='calculate function signature hash', metavar='SIGNATURE')
+        help="dumps the statespace json",
-    utilities.add_argument('--storage', help='read state variables from storage index, use with -a',
+        metavar="OUTPUT_FILE",
-                           metavar='INDEX,NUM_SLOTS,[array] / mapping,INDEX,[KEY1, KEY2...]')
+    )
-    utilities.add_argument('--solv',
+
-                           help='specify solidity compiler version. If not present, will try to install it (Experimental)',
+    inputs = parser.add_argument_group("input arguments")
-                           metavar='SOLV')
+    inputs.add_argument(
-    utilities.add_argument('--contract-hash-to-address', help='returns corresponding address for a contract address hash', metavar='SHA3_TO_LOOK_FOR')
+        "-c",
-
+        "--code",
-    options = parser.add_argument_group('options')
+        help='hex-encoded bytecode string ("6060604052...")',
-    options.add_argument('-m', '--modules', help='Comma-separated list of security analysis modules', metavar='MODULES')
+        metavar="BYTECODE",
-    options.add_argument('--max-depth', type=int, default=22, help='Maximum recursion depth for symbolic execution')
+    )
-
+    inputs.add_argument(
-    options.add_argument('--strategy', choices=['dfs', 'bfs', 'naive-random', 'weighted-random'],
+        "-f",
-                         default='dfs', help='Symbolic execution strategy')
+        "--codefile",
-    options.add_argument('--max-transaction-count', type=int, default=3, help='Maximum number of transactions issued by laser')
+        help="file containing hex-encoded bytecode string",
-
+        metavar="BYTECODEFILE",
-    options.add_argument('--execution-timeout', type=int, default=600, help="The amount of seconds to spend on symbolic execution")
+        type=argparse.FileType("r"),
-    options.add_argument('--create-timeout', type=int, default=10, help="The amount of seconds to spend on "
+    )
-                                                                        "the initial contract creation")
+    inputs.add_argument(
-    options.add_argument('--solc-args', help='Extra arguments for solc')
+        "-a",
-    options.add_argument('--phrack', action='store_true', help='Phrack-style call graph')
+        "--address",
-    options.add_argument('--enable-physics', action='store_true', help='enable graph physics simulation')
+        help="pull contract from the blockchain",
-    options.add_argument('-v', type=int, help='log level (0-2)', metavar='LOG_LEVEL')
+        metavar="CONTRACT_ADDRESS",
-    options.add_argument('-q', '--query-signature', action='store_true', help='Lookup function signatures through www.4byte.directory')
+    )
-
+    inputs.add_argument(
-    rpc = parser.add_argument_group('RPC options')
+        "-l",
-    rpc.add_argument('-i', action='store_true', help='Preset: Infura Node service (Mainnet)')
+        "--dynld",
-    rpc.add_argument('--rpc', help='custom RPC settings', metavar='HOST:PORT / ganache / infura-[network_name]')
+        action="store_true",
-    rpc.add_argument('--rpctls', type=bool, default=False, help='RPC connection over TLS')
+        help="auto-load dependencies from the blockchain",
+    )
+
+    outputs = parser.add_argument_group("output formats")
+    outputs.add_argument(
+        "-o",
+        "--outform",
+        choices=["text", "markdown", "json"],
+        default="text",
+        help="report output format",
+        metavar="<text/markdown/json>",
+    )
+    outputs.add_argument(
+        "--verbose-report",
+        action="store_true",
+        help="Include debugging information in report",
+    )
+
+    database = parser.add_argument_group("local contracts database")
+    database.add_argument(
+        "-s", "--search", help="search the contract database", metavar="EXPRESSION"
+    )
+    database.add_argument(
+        "--leveldb-dir",
+        help="specify leveldb directory for search or direct access operations",
+        metavar="LEVELDB_PATH",
+    )
+
+    utilities = parser.add_argument_group("utilities")
+    utilities.add_argument(
+        "--hash", help="calculate function signature hash", metavar="SIGNATURE"
+    )
+    utilities.add_argument(
+        "--storage",
+        help="read state variables from storage index, use with -a",
+        metavar="INDEX,NUM_SLOTS,[array] / mapping,INDEX,[KEY1, KEY2...]",
+    )
+    utilities.add_argument(
+        "--solv",
+        help="specify solidity compiler version. If not present, will try to install it (Experimental)",
+        metavar="SOLV",
+    )
+    utilities.add_argument(
+        "--contract-hash-to-address",
+        help="returns corresponding address for a contract address hash",
+        metavar="SHA3_TO_LOOK_FOR",
+    )
+
+    options = parser.add_argument_group("options")
+    options.add_argument(
+        "-m",
+        "--modules",
+        help="Comma-separated list of security analysis modules",
+        metavar="MODULES",
+    )
+    options.add_argument(
+        "--max-depth",
+        type=int,
+        default=22,
+        help="Maximum recursion depth for symbolic execution",
+    )
+
+    options.add_argument(
+        "--strategy",
+        choices=["dfs", "bfs", "naive-random", "weighted-random"],
+        default="dfs",
+        help="Symbolic execution strategy",
+    )
+    options.add_argument(
+        "--max-transaction-count",
+        type=int,
+        default=1,
+        help="Maximum number of transactions issued by laser",
+    )
+
+    options.add_argument(
+        "--execution-timeout",
+        type=int,
+        default=600,
+        help="The amount of seconds to spend on symbolic execution",
+    )
+    options.add_argument(
+        "--create-timeout",
+        type=int,
+        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(
+        "--phrack", action="store_true", help="Phrack-style call graph"
+    )
+    options.add_argument(
+        "--enable-physics", action="store_true", help="enable graph physics simulation"
+    )
+    options.add_argument("-v", type=int, help="log level (0-2)", metavar="LOG_LEVEL")
+    options.add_argument(
+        "-q",
+        "--query-signature",
+        action="store_true",
+        help="Lookup function signatures through www.4byte.directory",
+    )
+
+    rpc = parser.add_argument_group("RPC options")
+    rpc.add_argument(
+        "-i", action="store_true", help="Preset: Infura Node service (Mainnet)"
+    )
+    rpc.add_argument(
+        "--rpc",
+        help="custom RPC settings",
+        metavar="HOST:PORT / ganache / infura-[network_name]",
+    )
+    rpc.add_argument(
+        "--rpctls", type=bool, default=False, help="RPC connection over TLS"
+    )
+    parser.add_argument("--epic", action="store_true", help=argparse.SUPPRESS)
 
     # Get config values
 
     args = parser.parse_args()
 
+    if args.epic:
+        path = os.path.dirname(os.path.realpath(__file__))
+        sys.argv.remove("--epic")
+        os.system(" ".join(sys.argv) + " | python3 " + path + "/epic.py")
+        sys.exit()
+
     if args.version:
-        if args.outform == 'json':
+        if args.outform == "json":
-            print(json.dumps({'version_str': VERSION}))
+            print(json.dumps({"version_str": VERSION}))
         else:
             print("Mythril version {}".format(VERSION))
         sys.exit()
 
     # Parse cmdline args
 
-    if not (args.search or args.hash or args.disassemble or args.graph or args.fire_lasers
+    if not (
-            or args.storage or args.truffle or args.statespace_json or args.contract_hash_to_address):
+        args.search
+        or args.hash
+        or args.disassemble
+        or args.graph
+        or args.fire_lasers
+        or args.storage
+        or args.truffle
+        or args.statespace_json
+        or args.contract_hash_to_address
+    ):
         parser.print_help()
         sys.exit()
 
-
     if args.v:
         if 0 <= args.v < 3:
             coloredlogs.install(
-                fmt='%(name)s[%(process)d] %(levelname)s %(message)s',
+                fmt="%(name)s[%(process)d] %(levelname)s %(message)s",
-                level=[logging.NOTSET, logging.INFO, logging.DEBUG][args.v]
+                level=[logging.NOTSET, logging.INFO, logging.DEBUG][args.v],
             )
         else:
-            exit_with_error(args.outform, "Invalid -v value, you can find valid values in usage")
+            exit_with_error(
+                args.outform, "Invalid -v value, you can find valid values in usage"
+            )
 
     if args.query_signature:
         if sigs.ethereum_input_decoder == None:
-            exit_with_error(args.outform, "The --query-signature function requires the python package ethereum-input-decoder")
+            exit_with_error(
+                args.outform,
+                "The --query-signature function requires the python package ethereum-input-decoder",
+            )
 
     # -- commands --
     if args.hash:
@@ -131,9 +265,12 @@ def main():
         # infura = None, rpc = None, rpctls = None
         # solc_args = None, dynld = None, max_recursion_depth = 12):
 
-        mythril = Mythril(solv=args.solv, dynld=args.dynld,
+        mythril = Mythril(
-                          solc_args=args.solc_args,
+            solv=args.solv,
-                          enable_online_lookup=args.query_signature)
+            dynld=args.dynld,
+            solc_args=args.solc_args,
+            enable_online_lookup=args.query_signature,
+        )
         if args.dynld and not (args.rpc or args.i):
             mythril.set_api_from_config_path()
 
@@ -147,7 +284,9 @@ def main():
                 mythril.set_api_rpc_localhost()
         elif args.search or args.contract_hash_to_address:
             # Open LevelDB if necessary
-            mythril.set_api_leveldb(mythril.leveldb_dir if not args.leveldb_dir else args.leveldb_dir)
+            mythril.set_api_leveldb(
+                mythril.leveldb_dir if not args.leveldb_dir else args.leveldb_dir
+            )
 
         if args.search:
             # Database search ops
@@ -169,7 +308,8 @@ def main():
                 mythril.analyze_truffle_project(args)
             except FileNotFoundError:
                 print(
-                    "Build directory not found. Make sure that you start the analysis from the project root, and that 'truffle compile' has executed successfully.")
+                    "Build directory not found. Make sure that you start the analysis from the project root, and that 'truffle compile' has executed successfully."
+                )
             sys.exit()
 
         # Load / compile input contracts
@@ -179,7 +319,7 @@ def main():
             # Load from bytecode
             address, _ = mythril.load_from_bytecode(args.code)
         elif args.codefile:
-            bytecode = ''.join([l.strip() for l in args.codefile if len(l.strip()) > 0])
+            bytecode = "".join([l.strip() for l in args.codefile if len(l.strip()) > 0])
             address, _ = mythril.load_from_bytecode(bytecode)
         elif args.address:
             # Get bytecode from a contract address
@@ -187,37 +327,55 @@ def main():
         elif args.solidity_file:
             # Compile Solidity source file(s)
             if args.graph and len(args.solidity_file) > 1:
-                exit_with_error(args.outform,
+                exit_with_error(
-                                "Cannot generate call graphs from multiple input files. Please do it one at a time.")
+                    args.outform,
+                    "Cannot generate call graphs from multiple input files. Please do it one at a time.",
+                )
             address, _ = mythril.load_from_solidity(args.solidity_file)  # list of files
         else:
-            exit_with_error(args.outform,
+            exit_with_error(
-                            "No input bytecode. Please provide EVM code via -c BYTECODE, -a ADDRESS, or -i SOLIDITY_FILES")
+                args.outform,
+                "No input bytecode. Please provide EVM code via -c BYTECODE, -a ADDRESS, or -i SOLIDITY_FILES",
+            )
 
         # Commands
 
         if args.storage:
             if not args.address:
-                exit_with_error(args.outform,
+                exit_with_error(
-                                "To read storage, provide the address of a deployed contract with the -a option.")
+                    args.outform,
-
+                    "To read storage, provide the address of a deployed contract with the -a option.",
-            storage = mythril.get_state_variable_from_storage(address=address,
+                )
-                                                              params=[a.strip() for a in args.storage.strip().split(",")])
+
+            storage = mythril.get_state_variable_from_storage(
+                address=address,
+                params=[a.strip() for a in args.storage.strip().split(",")],
+            )
             print(storage)
 
         elif args.disassemble:
-            easm_text = mythril.contracts[0].get_easm() # or mythril.disassemble(mythril.contracts[0])
+            easm_text = mythril.contracts[
+                0
+            ].get_easm()  # or mythril.disassemble(mythril.contracts[0])
             sys.stdout.write(easm_text)
 
         elif args.graph or args.fire_lasers:
             if not mythril.contracts:
-                exit_with_error(args.outform, "input files do not contain any valid contracts")
+                exit_with_error(
+                    args.outform, "input files do not contain any valid contracts"
+                )
 
             if args.graph:
-                html = mythril.graph_html(strategy=args.strategy, contract=mythril.contracts[0], address=address,
+                html = mythril.graph_html(
-                                          enable_physics=args.enable_physics, phrackify=args.phrack,
+                    strategy=args.strategy,
-                                          max_depth=args.max_depth, execution_timeout=args.execution_timeout,
+                    contract=mythril.contracts[0],
-                                          create_timeout=args.create_timeout)
+                    address=address,
+                    enable_physics=args.enable_physics,
+                    phrackify=args.phrack,
+                    max_depth=args.max_depth,
+                    execution_timeout=args.execution_timeout,
+                    create_timeout=args.create_timeout,
+                )
 
                 try:
                     with open(args.graph, "w") as f:
@@ -226,28 +384,40 @@ def main():
                     exit_with_error(args.outform, "Error saving graph: " + str(e))
 
             else:
-                report = mythril.fire_lasers(strategy=args.strategy, address=address,
+                report = mythril.fire_lasers(
-                                             modules=[m.strip() for m in args.modules.strip().split(",")] if args.modules else [],
+                    strategy=args.strategy,
-                                             verbose_report=args.verbose_report,
+                    address=address,
-                                             max_depth=args.max_depth, execution_timeout=args.execution_timeout,
+                    modules=[m.strip() for m in args.modules.strip().split(",")]
-                                             create_timeout=args.create_timeout,
+                    if args.modules
-                                             max_transaction_count=args.max_transaction_count)
+                    else [],
+                    verbose_report=args.verbose_report,
+                    max_depth=args.max_depth,
+                    execution_timeout=args.execution_timeout,
+                    create_timeout=args.create_timeout,
+                    max_transaction_count=args.max_transaction_count,
+                )
                 outputs = {
-                    'swc-standard': report.as_swc_standard_format(),
+                    "json": report.as_json(),
-                    'json': report.as_json(),
+                    "text": report.as_text(),
-                    'text': report.as_text(),
+                    "markdown": report.as_markdown(),
-                    'markdown': report.as_markdown()
                 }
                 print(outputs[args.outform])
 
         elif args.statespace_json:
 
             if not mythril.contracts:
-                exit_with_error(args.outform, "input files do not contain any valid contracts")
+                exit_with_error(
-
+                    args.outform, "input files do not contain any valid contracts"
-            statespace = mythril.dump_statespace(strategy=args.strategy, contract=mythril.contracts[0], address=address,
+                )
-                                                 max_depth=args.max_depth, execution_timeout=args.execution_timeout,
+
-                                                 create_timeout=args.create_timeout)
+            statespace = mythril.dump_statespace(
+                strategy=args.strategy,
+                contract=mythril.contracts[0],
+                address=address,
+                max_depth=args.max_depth,
+                execution_timeout=args.execution_timeout,
+                create_timeout=args.create_timeout,
+            )
 
             try:
                 with open(args.statespace_json, "w") as f:

mythril/interfaces/epic.py

@@ -0,0 +1,249 @@
+#!/usr/bin/env python
+#
+# "THE BEER-WARE LICENSE" (Revision 43~maze)
+#
+# <maze@pyth0n.org> wrote these files. As long as you retain this notice you
+# can do whatever you want with this stuff. If we meet some day, and you think
+# this stuff is worth it, you can buy me a beer in return.
+
+# https://github.com/tehmaze/lolcat
+
+import atexit
+import math
+import os
+import random
+import re
+import sys
+import time
+
+PY3 = sys.version_info >= (3,)
+
+# Reset terminal colors at exit
+def reset():
+    sys.stdout.write("\x1b[0m")
+    sys.stdout.flush()
+
+
+atexit.register(reset)
+
+
+STRIP_ANSI = re.compile(r"\x1b\[(\d+)(;\d+)?(;\d+)?[m|K]")
+COLOR_ANSI = (
+    (0x00, 0x00, 0x00),
+    (0xCD, 0x00, 0x00),
+    (0x00, 0xCD, 0x00),
+    (0xCD, 0xCD, 0x00),
+    (0x00, 0x00, 0xEE),
+    (0xCD, 0x00, 0xCD),
+    (0x00, 0xCD, 0xCD),
+    (0xE5, 0xE5, 0xE5),
+    (0x7F, 0x7F, 0x7F),
+    (0xFF, 0x00, 0x00),
+    (0x00, 0xFF, 0x00),
+    (0xFF, 0xFF, 0x00),
+    (0x5C, 0x5C, 0xFF),
+    (0xFF, 0x00, 0xFF),
+    (0x00, 0xFF, 0xFF),
+    (0xFF, 0xFF, 0xFF),
+)
+
+
+class LolCat(object):
+    def __init__(self, mode=256, output=sys.stdout):
+        self.mode = mode
+        self.output = output
+
+    def _distance(self, rgb1, rgb2):
+        return sum(map(lambda c: (c[0] - c[1]) ** 2, zip(rgb1, rgb2)))
+
+    def ansi(self, rgb):
+        r, g, b = rgb
+
+        if self.mode in (8, 16):
+            colors = COLOR_ANSI[: self.mode]
+            matches = [
+                (self._distance(c, map(int, rgb)), i) for i, c in enumerate(colors)
+            ]
+            matches.sort()
+            color = matches[0][1]
+
+            return "3%d" % (color,)
+        else:
+            gray_possible = True
+            sep = 2.5
+
+            while gray_possible:
+                if r < sep or g < sep or b < sep:
+                    gray = r < sep and g < sep and b < sep
+                    gray_possible = False
+
+                sep += 42.5
+
+            if gray:
+                color = 232 + int(float(sum(rgb) / 33.0))
+            else:
+                color = sum(
+                    [16]
+                    + [
+                        int(6 * float(val) / 256) * mod
+                        for val, mod in zip(rgb, [36, 6, 1])
+                    ]
+                )
+
+            return "38;5;%d" % (color,)
+
+    def wrap(self, *codes):
+        return "\x1b[%sm" % ("".join(codes),)
+
+    def rainbow(self, freq, i):
+        r = math.sin(freq * i) * 127 + 128
+        g = math.sin(freq * i + 2 * math.pi / 3) * 127 + 128
+        b = math.sin(freq * i + 4 * math.pi / 3) * 127 + 128
+        return [r, g, b]
+
+    def cat(self, fd, options):
+        if options.animate:
+            self.output.write("\x1b[?25l")
+
+        for line in fd:
+            options.os += 1
+            self.println(line, options)
+
+        if options.animate:
+            self.output.write("\x1b[?25h")
+
+    def println(self, s, options):
+        s = s.rstrip()
+        if options.force or self.output.isatty():
+            s = STRIP_ANSI.sub("", s)
+
+        if options.animate:
+            self.println_ani(s, options)
+        else:
+            self.println_plain(s, options)
+
+        self.output.write("\n")
+        self.output.flush()
+
+    def println_ani(self, s, options):
+        if not s:
+            return
+
+        for i in range(1, options.duration):
+            self.output.write("\x1b[%dD" % (len(s),))
+            self.output.flush()
+            options.os += options.spread
+            self.println_plain(s, options)
+            time.sleep(1.0 / options.speed)
+
+    def println_plain(self, s, options):
+        for i, c in enumerate(s if PY3 else s.decode(options.charset_py2, "replace")):
+            rgb = self.rainbow(options.freq, options.os + i / options.spread)
+            self.output.write(
+                "".join(
+                    [
+                        self.wrap(self.ansi(rgb)),
+                        c if PY3 else c.encode(options.charset_py2, "replace"),
+                    ]
+                )
+            )
+
+
+def detect_mode(term_hint="xterm-256color"):
+    """
+    Poor-mans color mode detection.
+    """
+    if "ANSICON" in os.environ:
+        return 16
+    elif os.environ.get("ConEmuANSI", "OFF") == "ON":
+        return 256
+    else:
+        term = os.environ.get("TERM", term_hint)
+        if term.endswith("-256color") or term in ("xterm", "screen"):
+            return 256
+        elif term.endswith("-color") or term in ("rxvt",):
+            return 16
+        else:
+            return 256  # optimistic default
+
+
+def run():
+    """Main entry point."""
+    import optparse
+
+    parser = optparse.OptionParser(usage=r"%prog [<options>] [file ...]")
+    parser.add_option(
+        "-p", "--spread", type="float", default=3.0, help="Rainbow spread"
+    )
+    parser.add_option(
+        "-F", "--freq", type="float", default=0.1, help="Rainbow frequency"
+    )
+    parser.add_option("-S", "--seed", type="int", default=0, help="Rainbow seed")
+    parser.add_option(
+        "-a",
+        "--animate",
+        action="store_true",
+        default=False,
+        help="Enable psychedelics",
+    )
+    parser.add_option(
+        "-d", "--duration", type="int", default=12, help="Animation duration"
+    )
+    parser.add_option(
+        "-s", "--speed", type="float", default=20.0, help="Animation speed"
+    )
+    parser.add_option(
+        "-f",
+        "--force",
+        action="store_true",
+        default=False,
+        help="Force colour even when stdout is not a tty",
+    )
+
+    parser.add_option(
+        "-3", action="store_const", dest="mode", const=8, help="Force 3 bit colour mode"
+    )
+    parser.add_option(
+        "-4",
+        action="store_const",
+        dest="mode",
+        const=16,
+        help="Force 4 bit colour mode",
+    )
+    parser.add_option(
+        "-8",
+        action="store_const",
+        dest="mode",
+        const=256,
+        help="Force 8 bit colour mode",
+    )
+
+    parser.add_option(
+        "-c",
+        "--charset-py2",
+        default="utf-8",
+        help="Manually set a charset to convert from, for python 2.7",
+    )
+
+    options, args = parser.parse_args()
+    options.os = random.randint(0, 256) if options.seed == 0 else options.seed
+    options.mode = options.mode or detect_mode()
+
+    lolcat = LolCat(mode=options.mode)
+
+    if not args:
+        args = ["-"]
+
+    for filename in args:
+        if filename == "-":
+            lolcat.cat(sys.stdin, options)
+        else:
+            try:
+                with open(filename, "r") as handle:
+                    lolcat.cat(handle, options)
+            except IOError as error:
+                sys.stderr.write(str(error) + "\n")
+
+
+if __name__ == "__main__":
+    sys.exit(run())

mythril/laser/ethereum/call.py

@@ -1,7 +1,7 @@
 import logging
-from z3 import simplify
+from z3 import simplify, Extract
 import mythril.laser.ethereum.util as util
-from mythril.laser.ethereum.state import Account, CalldataType, GlobalState
+from mythril.laser.ethereum.state import Account, CalldataType, GlobalState, Calldata
 from mythril.support.loader import DynLoader
 import re
 
@@ -11,7 +11,9 @@ to get the necessary elements from the stack and determine the parameters for th
 """
 
 
-def get_call_parameters(global_state: GlobalState, dynamic_loader: DynLoader, with_value=False):
+def get_call_parameters(
+    global_state: GlobalState, dynamic_loader: DynLoader, with_value=False
+):
     """
     Gets call parameters from global state
     Pops the values from the stack and determines output parameters
@@ -22,21 +24,40 @@ def get_call_parameters(global_state: GlobalState, dynamic_loader: DynLoader, wi
     """
     gas, to = global_state.mstate.pop(2)
     value = global_state.mstate.pop() if with_value else 0
-    memory_input_offset, memory_input_size, memory_out_offset, memory_out_size = global_state.mstate.pop(4)
+    memory_input_offset, memory_input_size, memory_out_offset, memory_out_size = global_state.mstate.pop(
+        4
+    )
 
     callee_address = get_callee_address(global_state, dynamic_loader, to)
 
     callee_account = None
-    call_data, call_data_type = get_call_data(global_state, memory_input_offset, memory_input_size, False)
+    call_data, call_data_type = get_call_data(
+        global_state, memory_input_offset, memory_input_size, False
+    )
 
     if int(callee_address, 16) >= 5 or int(callee_address, 16) == 0:
-        call_data, call_data_type = get_call_data(global_state, memory_input_offset, memory_input_size)
+        call_data, call_data_type = get_call_data(
-        callee_account = get_callee_account(global_state, callee_address, dynamic_loader)
+            global_state, memory_input_offset, memory_input_size
-
+        )
-    return callee_address, callee_account, call_data, value, call_data_type, gas, memory_out_offset, memory_out_size
+        callee_account = get_callee_account(
-
+            global_state, callee_address, dynamic_loader
-
+        )
-def get_callee_address(global_state:GlobalState, dynamic_loader: DynLoader, symbolic_to_address):
+
+    return (
+        callee_address,
+        callee_account,
+        call_data,
+        value,
+        call_data_type,
+        gas,
+        memory_out_offset,
+        memory_out_size,
+    )
+
+
+def get_callee_address(
+    global_state: GlobalState, dynamic_loader: DynLoader, symbolic_to_address
+):
     """
     Gets the address of the callee
     :param global_state: state to look in
@@ -51,7 +72,7 @@ def get_callee_address(global_state:GlobalState, dynamic_loader: DynLoader, symb
     except TypeError:
         logging.debug("Symbolic call encountered")
 
-        match = re.search(r'storage_(\d+)', str(simplify(symbolic_to_address)))
+        match = re.search(r"storage_(\d+)", str(simplify(symbolic_to_address)))
         logging.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
         if match is None or dynamic_loader is None:
@@ -62,7 +83,9 @@ def get_callee_address(global_state:GlobalState, dynamic_loader: DynLoader, symb
 
         # attempt to read the contract address from instance storage
         try:
-            callee_address = dynamic_loader.read_storage(environment.active_account.address, index)
+            callee_address = dynamic_loader.read_storage(
+                environment.active_account.address, index
+            )
         # TODO: verify whether this happens or not
         except:
             logging.debug("Error accessing contract storage.")
@@ -107,7 +130,9 @@ def get_callee_account(global_state, callee_address, dynamic_loader):
         raise ValueError()
     logging.debug("Dependency loaded: " + callee_address)
 
-    callee_account = Account(callee_address, code, callee_address, dynamic_loader=dynamic_loader)
+    callee_account = Account(
+        callee_address, code, callee_address, dynamic_loader=dynamic_loader
+    )
     accounts[callee_address] = callee_account
 
     return callee_account
@@ -122,17 +147,33 @@ def get_call_data(global_state, memory_start, memory_size, pad=True):
     :return: Tuple containing: call_data array from memory or empty array if symbolic, type found
     """
     state = global_state.mstate
+    transaction_id = "{}_internalcall".format(global_state.current_transaction.id)
     try:
         # TODO: This only allows for either fully concrete or fully symbolic calldata.
         # Improve management of memory and callata to support a mix between both types.
-        call_data = state.memory[util.get_concrete_int(memory_start):util.get_concrete_int(memory_start + memory_size)]
+        calldata_from_mem = state.memory[
-        if len(call_data) < 32 and pad:
+            util.get_concrete_int(memory_start) : util.get_concrete_int(
-            call_data += [0] * (32 - len(call_data))
+                memory_start + memory_size
+            )
+        ]
+        i = 0
+        starting_calldata = []
+        while i < len(calldata_from_mem):
+            elem = calldata_from_mem[i]
+            if isinstance(elem, int):
+                starting_calldata.append(elem)
+                i += 1
+            else:  # BitVec
+                for j in range(0, elem.size(), 8):
+                    starting_calldata.append(Extract(j + 7, j, elem))
+                    i += 1
+
+        call_data = Calldata(transaction_id, starting_calldata)
         call_data_type = CalldataType.CONCRETE
         logging.debug("Calldata: " + str(call_data))
     except TypeError:
         logging.info("Unsupported symbolic calldata offset")
         call_data_type = CalldataType.SYMBOLIC
-        call_data = []
+        call_data = Calldata("{}_internalcall".format(transaction_id))
 
     return call_data, call_data_type

mythril/laser/ethereum/cfg.py

@@ -3,6 +3,7 @@ from enum import Enum
 
 gbl_next_uid = 0  # node counter
 
+
 class JumpType(Enum):
     CONDITIONAL = 1
     UNCONDITIONAL = 2
@@ -41,18 +42,24 @@ class Node:
 
             instruction = state.get_current_instruction()
 
-            code += str(instruction['address']) + " " + instruction['opcode']
+            code += str(instruction["address"]) + " " + instruction["opcode"]
-            if instruction['opcode'].startswith("PUSH"):
+            if instruction["opcode"].startswith("PUSH"):
-                code += " " + instruction['argument']
+                code += " " + instruction["argument"]
 
             code += "\\n"
 
-        return dict(contract_name=self.contract_name, start_addr=self.start_addr, function_name=self.function_name,
+        return dict(
-                    code=code)
+            contract_name=self.contract_name,
+            start_addr=self.start_addr,
+            function_name=self.function_name,
+            code=code,
+        )
 
 
 class Edge:
-    def __init__(self, node_from, node_to, edge_type=JumpType.UNCONDITIONAL, condition=None):
+    def __init__(
+        self, node_from, node_to, edge_type=JumpType.UNCONDITIONAL, condition=None
+    ):
         self.node_from = node_from
         self.node_to = node_to
         self.type = edge_type
@@ -63,4 +70,4 @@ class Edge:
 
     @property
     def as_dict(self):
-        return {"from": self.node_from, 'to': self.node_to}
+        return {"from": self.node_from, "to": self.node_to}

mythril/laser/ethereum/keccak.py

@@ -1,5 +1,6 @@
 from z3 import ExprRef
 
+
 class KeccakFunctionManager:
     def __init__(self):
         self.keccak_expression_mapping = {}

mythril/laser/ethereum/natives.py

@@ -15,10 +15,10 @@ class NativeContractException(Exception):
     pass
 
 
-def int_to_32bytes(i):   # used because int can't fit as bytes function's input
+def int_to_32bytes(i):  # used because int can't fit as bytes function's input
     o = [0] * 32
     for x in range(32):
-        o[31 - x] = i & 0xff
+        o[31 - x] = i & 0xFF
         i >>= 8
     return bytes(o)
 
@@ -26,7 +26,7 @@ def int_to_32bytes(i):   # used because int can't fit as bytes function's input
 def extract32(data, i):
     if i >= len(data):
         return 0
-    o = data[i: min(i + 32, len(data))]
+    o = data[i : min(i + 32, len(data))]
     o.extend(bytearray(32 - len(o)))
     return bytearray_to_int(o)
 
@@ -41,13 +41,13 @@ def ecrecover(data):
     except TypeError:
         raise NativeContractException
 
-    message = b''.join([ALL_BYTES[x] for x in data[0:32]])
+    message = b"".join([ALL_BYTES[x] for x in data[0:32]])
     if r >= secp256k1n or s >= secp256k1n or v < 27 or v > 28:
         return []
     try:
         pub = ecrecover_to_pub(message, v, r, s)
     except Exception as e:
-        logging.info("An error has occured while extracting public key: "+e)
+        logging.info("An error has occured while extracting public key: " + e)
         return []
     o = [0] * 12 + [x for x in sha3(pub)[-20:]]
     return o
@@ -66,7 +66,7 @@ def ripemd160(data):
         data = bytes(data)
     except TypeError:
         raise NativeContractException
-    return 12*[0]+[i for i in hashlib.new('ripemd160', data).digest()]
+    return 12 * [0] + [i for i in hashlib.new("ripemd160", data).digest()]
 
 
 def identity(data):
@@ -79,4 +79,4 @@ def native_contracts(address, data):
     """
 
     functions = (ecrecover, sha256, ripemd160, identity)
-    return functions[address-1](data)
+    return functions[address - 1](data.starting_calldata)

mythril/laser/ethereum/state.py

@@ -1,10 +1,31 @@
-from z3 import BitVec, BitVecVal, Solver, ExprRef, sat
+from z3 import (
+    BitVec,
+    BitVecVal,
+    BitVecRef,
+    BitVecNumRef,
+    BitVecSort,
+    Solver,
+    ExprRef,
+    Concat,
+    sat,
+    simplify,
+    Array,
+    ForAll,
+    Solver,
+    UGT,
+    Implies,
+)
+from z3.z3types import Z3Exception
 from mythril.disassembler.disassembly import Disassembly
 from copy import copy, deepcopy
 from enum import Enum
 from random import randint
+from mythril.laser.ethereum.util import get_concrete_int
 
-from mythril.laser.ethereum.evm_exceptions import StackOverflowException, StackUnderflowException
+from mythril.laser.ethereum.evm_exceptions import (
+    StackOverflowException,
+    StackUnderflowException,
+)
 
 
 class CalldataType(Enum):
@@ -12,10 +33,92 @@ class CalldataType(Enum):
     SYMBOLIC = 2
 
 
+class Calldata:
+    """
+    Calldata class representing the calldata of a transaction
+    """
+
+    def __init__(self, tx_id, starting_calldata=None):
+        """
+        Constructor for Calldata
+        :param tx_id: unique value representing the transaction the calldata is for
+        :param starting_calldata: byte array representing the concrete calldata of a transaction
+        """
+        self.tx_id = tx_id
+        if starting_calldata:
+            self._calldata = []
+            self.calldatasize = BitVecVal(len(starting_calldata), 256)
+            self.concrete = True
+        else:
+            self._calldata = Array(
+                "{}_calldata".format(self.tx_id), BitVecSort(256), BitVecSort(8)
+            )
+            self.calldatasize = BitVec("{}_calldatasize".format(self.tx_id), 256)
+            self.concrete = False
+
+        self.starting_calldata = starting_calldata or []
+
+    @property
+    def constraints(self):
+        constraints = []
+        if self.concrete:
+            for calldata_byte in self.starting_calldata:
+                if type(calldata_byte) == int:
+                    self._calldata.append(BitVecVal(calldata_byte, 8))
+                else:
+                    self._calldata.append(calldata_byte)
+            constraints.append(self.calldatasize == len(self.starting_calldata))
+        else:
+            x = BitVec("x", 256)
+            constraints.append(
+                ForAll(x, Implies(self[x] != 0, UGT(self.calldatasize, x)))
+            )
+        return constraints
+
+    def concretized(self, model):
+        result = []
+
+        for i in range(
+            get_concrete_int(model.eval(self.calldatasize, model_completion=True))
+        ):
+            result.append(get_concrete_int(model.eval(self[i], model_completion=True)))
+
+        return result
+
+    def get_word_at(self, index: int):
+        return self[index : index + 32]
+
+    def __getitem__(self, item):
+        if isinstance(item, slice):
+            try:
+                current_index = (
+                    item.start
+                    if isinstance(item.start, BitVecRef)
+                    else BitVecVal(item.start, 256)
+                )
+                dataparts = []
+                while simplify(current_index != item.stop):
+                    dataparts.append(self[current_index])
+                    current_index = simplify(current_index + 1)
+            except Z3Exception:
+                raise IndexError("Invalid Calldata Slice")
+
+            return simplify(Concat(dataparts))
+
+        if self.concrete:
+            try:
+                return self._calldata[get_concrete_int(item)]
+            except IndexError:
+                return BitVecVal(0, 8)
+        else:
+            return self._calldata[item]
+
+
 class Storage:
     """
     Storage class represents the storage of an Account
     """
+
     def __init__(self, concrete=False, address=None, dynamic_loader=None):
         """
         Constructor for Storage
@@ -32,7 +135,12 @@ class Storage:
         except KeyError:
             if self.address and int(self.address[2:], 16) != 0 and self.dynld:
                 try:
-                    self._storage[item] = int(self.dynld.read_storage(contract_address=self.address, index=int(item)), 16)
+                    self._storage[item] = int(
+                        self.dynld.read_storage(
+                            contract_address=self.address, index=int(item)
+                        ),
+                        16,
+                    )
                     return self._storage[item]
                 except ValueError:
                     pass
@@ -47,12 +155,21 @@ class Storage:
     def keys(self):
         return self._storage.keys()
 
+
 class Account:
     """
     Account class representing ethereum accounts
     """
-    def __init__(self, address, code=None, contract_name="unknown", balance=None, concrete_storage=False,
+
-                 dynamic_loader=None):
+    def __init__(
+        self,
+        address,
+        code=None,
+        contract_name="unknown",
+        balance=None,
+        concrete_storage=False,
+        dynamic_loader=None,
+    ):
         """
         Constructor for account
         :param address: Address of the account
@@ -64,7 +181,9 @@ class Account:
         self.nonce = 0
         self.code = code or Disassembly("")
         self.balance = balance if balance else BitVec("balance", 256)
-        self.storage = Storage(concrete_storage, address=address, dynamic_loader=dynamic_loader)
+        self.storage = Storage(
+            concrete_storage, address=address, dynamic_loader=dynamic_loader
+        )
 
         # Metadata
         self.address = address
@@ -83,13 +202,19 @@ class Account:
 
     @property
     def as_dict(self):
-        return {'nonce': self.nonce, 'code': self.code, 'balance': self.balance, 'storage': self.storage}
+        return {
+            "nonce": self.nonce,
+            "code": self.code,
+            "balance": self.balance,
+            "storage": self.storage,
+        }
 
 
 class Environment:
     """
     The environment class represents the current execution environment for the symbolic executor
     """
+
     def __init__(
         self,
         active_account,
@@ -121,18 +246,24 @@ class Environment:
     def __str__(self):
         return str(self.as_dict)
 
-
     @property
     def as_dict(self):
-        return dict(active_account=self.active_account, sender=self.sender, calldata=self.calldata,
+        return dict(
-                    gasprice=self.gasprice, callvalue=self.callvalue, origin=self.origin,
+            active_account=self.active_account,
-                    calldata_type=self.calldata_type)
+            sender=self.sender,
+            calldata=self.calldata,
+            gasprice=self.gasprice,
+            callvalue=self.callvalue,
+            origin=self.origin,
+            calldata_type=self.calldata_type,
+        )
 
 
 class MachineStack(list):
     """
     Defines EVM stack, overrides the default list to handle overflows
     """
+
     STACK_LIMIT = 1024
 
     def __init__(self, default_list=None):
@@ -146,8 +277,10 @@ class MachineStack(list):
         :function: appends the element to list if the size is less than STACK_LIMIT, else throws an error
         """
         if super(MachineStack, self).__len__() >= self.STACK_LIMIT:
-            raise StackOverflowException("Reached the EVM stack limit of {}, you can't append more "
+            raise StackOverflowException(
-                                         "elements".format(self.STACK_LIMIT))
+                "Reached the EVM stack limit of {}, you can't append more "
+                "elements".format(self.STACK_LIMIT)
+            )
         super(MachineStack, self).append(element)
 
     def pop(self, index=-1):
@@ -166,25 +299,28 @@ class MachineStack(list):
         try:
             return super(MachineStack, self).__getitem__(item)
         except IndexError:
-            raise StackUnderflowException("Trying to access a stack element which doesn't exist")
+            raise StackUnderflowException(
+                "Trying to access a stack element which doesn't exist"
+            )
 
     def __add__(self, other):
         """
         Implement list concatenation if needed
         """
-        raise NotImplementedError('Implement this if needed')
+        raise NotImplementedError("Implement this if needed")
 
     def __iadd__(self, other):
         """
         Implement list concatenation if needed
         """
-        raise NotImplementedError('Implement this if needed')
+        raise NotImplementedError("Implement this if needed")
 
 
 class MachineState:
     """
     MachineState represents current machine state also referenced to as \mu
     """
+
     def __init__(self, gas):
         """ Constructor for machineState """
         self.pc = 0
@@ -202,13 +338,13 @@ class MachineState:
         """
         if self.memory_size > start + size:
             return
-        m_extend = (start + size - self.memory_size)
+        m_extend = start + size - self.memory_size
         self.memory.extend(bytearray(m_extend))
 
     def memory_write(self, offset, data):
         """ Writes data to memory starting at offset """
         self.mem_extend(offset, len(data))
-        self.memory[offset:offset+len(data)] = data
+        self.memory[offset : offset + len(data)] = data
 
     def pop(self, amount=1):
         """ Pops amount elements from the stack"""
@@ -228,14 +364,29 @@ class MachineState:
 
     @property
     def as_dict(self):
-        return dict(pc=self.pc, stack=self.stack, memory=self.memory, memsize=self.memory_size, gas=self.gas)
+        return dict(
+            pc=self.pc,
+            stack=self.stack,
+            memory=self.memory,
+            memsize=self.memory_size,
+            gas=self.gas,
+        )
 
 
 class GlobalState:
     """
     GlobalState represents the current globalstate
     """
-    def __init__(self, world_state, environment, node, machine_state=None, transaction_stack=None, last_return_data=None):
+
+    def __init__(
+        self,
+        world_state,
+        environment,
+        node,
+        machine_state=None,
+        transaction_stack=None,
+        last_return_data=None,
+    ):
         """ Constructor for GlobalState"""
         self.node = node
         self.world_state = world_state
@@ -250,8 +401,14 @@ class GlobalState:
         environment = copy(self.environment)
         mstate = deepcopy(self.mstate)
         transaction_stack = copy(self.transaction_stack)
-        return GlobalState(world_state, environment, self.node, mstate, transaction_stack=transaction_stack,
+        return GlobalState(
-                           last_return_data=self.last_return_data)
+            world_state,
+            environment,
+            self.node,
+            mstate,
+            transaction_stack=transaction_stack,
+            last_return_data=self.last_return_data,
+        )
 
     @property
     def accounts(self):
@@ -261,7 +418,6 @@ class GlobalState:
     def get_current_instruction(self):
         """ Gets the current instruction for this GlobalState"""
 
-
         instructions = self.environment.code.instruction_list
         return instructions[self.mstate.pc]
 
@@ -286,6 +442,7 @@ class WorldState:
     """
     The WorldState class represents the world state as described in the yellow paper
     """
+
     def __init__(self, transaction_sequence=None):
         """
         Constructor for the world state. Initializes the accounts record
@@ -308,7 +465,9 @@ class WorldState:
         new_world_state.node = self.node
         return new_world_state
 
-    def create_account(self, balance=0, address=None, concrete_storage=False, dynamic_loader=None):
+    def create_account(
+        self, balance=0, address=None, concrete_storage=False, dynamic_loader=None
+    ):
         """
         Create non-contract account
         :param address: The account's address
@@ -318,7 +477,12 @@ class WorldState:
         :return: The new account
         """
         address = address if address else self._generate_new_address()
-        new_account = Account(address, balance=balance, dynamic_loader=dynamic_loader, concrete_storage=concrete_storage)
+        new_account = Account(
+            address,
+            balance=balance,
+            dynamic_loader=dynamic_loader,
+            concrete_storage=concrete_storage,
+        )
         self._put_account(new_account)
         return new_account
 
@@ -330,14 +494,16 @@ class WorldState:
         :param storage: Initial storage for the contract
         :return: The new account
         """
-        new_account = Account(self._generate_new_address(), code=contract_code, balance=0)
+        new_account = Account(
+            self._generate_new_address(), code=contract_code, balance=0
+        )
         new_account.storage = storage
         self._put_account(new_account)
 
     def _generate_new_address(self):
         """ Generates a new address for the global state"""
         while True:
-            address = '0x' + ''.join([str(hex(randint(0, 16)))[-1] for _ in range(20)])
+            address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(20)])
             if address not in self.accounts.keys():
                 return address
 

mythril/laser/ethereum/strategy/__init__.py

@@ -2,7 +2,7 @@ from abc import ABC, abstractmethod
 
 
 class BasicSearchStrategy(ABC):
-    __slots__ = 'work_list', 'max_depth'
+    __slots__ = "work_list", "max_depth"
 
     def __init__(self, work_list, max_depth):
         self.work_list = work_list

mythril/laser/ethereum/strategy/basic.py

@@ -22,7 +22,11 @@ except ImportError:
         if weights is None:
             return [population[int(random() * len(population))]]
         cum_weights = accumulate(weights)
-        return [population[bisect(cum_weights, random()*cum_weights[-1], 0, len(population)-1)]]
+        return [
+            population[
+                bisect(cum_weights, random() * cum_weights[-1], 0, len(population) - 1)
+            ]
+        ]
 
 
 class DepthFirstSearchStrategy(BasicSearchStrategy):
@@ -49,6 +53,7 @@ class ReturnRandomNaivelyStrategy(BasicSearchStrategy):
     """
     chooses a random state from the worklist with equal likelihood
     """
+
     def get_strategic_global_state(self):
         if len(self.work_list) > 0:
             return self.work_list.pop(randrange(len(self.work_list)))
@@ -62,6 +67,9 @@ class ReturnWeightedRandomStrategy(BasicSearchStrategy):
     """
 
     def get_strategic_global_state(self):
-        probability_distribution = [1/(global_state.mstate.depth+1) for global_state in self.work_list]
+        probability_distribution = [
-        return self.work_list.pop(choices(range(len(self.work_list)), probability_distribution)[0])
+            1 / (global_state.mstate.depth + 1) for global_state in self.work_list
-
+        ]
+        return self.work_list.pop(
+            choices(range(len(self.work_list)), probability_distribution)[0]
+        )

mythril/laser/ethereum/svm.py

@@ -1,14 +1,21 @@
 import logging
+from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.state import WorldState
-from mythril.laser.ethereum.transaction import TransactionStartSignal, TransactionEndSignal, \
+from mythril.laser.ethereum.transaction import (
-    ContractCreationTransaction
+    TransactionStartSignal,
+    TransactionEndSignal,
+    ContractCreationTransaction,
+)
 from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
 from mythril.laser.ethereum.instructions import Instruction
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
 from datetime import datetime, timedelta
 from copy import copy
-from mythril.laser.ethereum.transaction import execute_contract_creation, execute_message_call
+from mythril.laser.ethereum.transaction import (
+    execute_contract_creation,
+    execute_message_call,
+)
 from functools import reduce
 from mythril.laser.ethereum.evm_exceptions import VmException
 
@@ -17,9 +24,9 @@ class SVMError(Exception):
     pass
 
 
-'''
+"""
 Main symbolic execution engine.
-'''
+"""
 
 
 class LaserEVM:
@@ -27,8 +34,16 @@ class LaserEVM:
     Laser EVM class
     """
 
-    def __init__(self, accounts, dynamic_loader=None, max_depth=float('inf'), execution_timeout=60, create_timeout=10,
+    def __init__(
-                 strategy=DepthFirstSearchStrategy, max_transaction_count=3):
+        self,
+        accounts,
+        dynamic_loader=None,
+        max_depth=float("inf"),
+        execution_timeout=60,
+        create_timeout=10,
+        strategy=DepthFirstSearchStrategy,
+        max_transaction_count=3,
+    ):
         world_state = WorldState()
         world_state.accounts = accounts
         # this sets the initial world state
@@ -55,7 +70,9 @@ class LaserEVM:
         self.pre_hooks = {}
         self.post_hooks = {}
 
-        logging.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
+        logging.info(
+            "LASER EVM initialized with dynamic loader: " + str(dynamic_loader)
+        )
 
     @property
     def accounts(self):
@@ -70,11 +87,19 @@ class LaserEVM:
             execute_message_call(self, main_address)
         elif creation_code:
             logging.info("Starting contract creation transaction")
-            created_account = execute_contract_creation(self, creation_code, contract_name)
+            created_account = execute_contract_creation(
-            logging.info("Finished contract creation, found {} open states".format(len(self.open_states)))
+                self, creation_code, contract_name
+            )
+            logging.info(
+                "Finished contract creation, found {} open states".format(
+                    len(self.open_states)
+                )
+            )
             if len(self.open_states) == 0:
-                logging.warning("No contract was created during the execution of contract creation "
+                logging.warning(
-                                "Increase the resources for creation execution (--max-depth or --create-timeout)")
+                    "No contract was created during the execution of contract creation "
+                    "Increase the resources for creation execution (--max-depth or --create-timeout)"
+                )
 
             # Reset code coverage
             self.coverage = {}
@@ -82,7 +107,9 @@ class LaserEVM:
                 initial_coverage = self._get_covered_instructions()
 
                 self.time = datetime.now()
-                logging.info("Starting message call transaction, iteration: {}".format(i))
+                logging.info(
+                    "Starting message call transaction, iteration: {}".format(i)
+                )
                 execute_message_call(self, created_account.address)
 
                 end_coverage = self._get_covered_instructions()
@@ -90,22 +117,36 @@ class LaserEVM:
                     break
 
         logging.info("Finished symbolic execution")
-        logging.info("%d nodes, %d edges, %d total states", len(self.nodes), len(self.edges), self.total_states)
+        logging.info(
+            "%d nodes, %d edges, %d total states",
+            len(self.nodes),
+            len(self.edges),
+            self.total_states,
+        )
         for code, coverage in self.coverage.items():
-            cov = reduce(lambda sum_, val: sum_ + 1 if val else sum_, coverage[1]) / float(coverage[0]) * 100
+            cov = (
+                reduce(lambda sum_, val: sum_ + 1 if val else sum_, coverage[1])
+                / float(coverage[0])
+                * 100
+            )
             logging.info("Achieved {} coverage for code: {}".format(cov, code))
 
     def _get_covered_instructions(self) -> int:
         """ Gets the total number of covered instructions for all accounts in the svm"""
         total_covered_instructions = 0
         for _, cv in self.coverage.items():
-            total_covered_instructions += reduce(lambda sum_, val: sum_ + 1 if val else sum_, cv[1])
+            total_covered_instructions += reduce(
+                lambda sum_, val: sum_ + 1 if val else sum_, cv[1]
+            )
         return total_covered_instructions
 
     def exec(self, create=False):
         for global_state in self.strategy:
             if self.execution_timeout and not create:
-                if self.time + timedelta(seconds=self.execution_timeout) <= datetime.now():
+                if (
+                    self.time + timedelta(seconds=self.execution_timeout)
+                    <= datetime.now()
+                ):
                     return
             elif self.create_timeout and create:
                 if self.time + timedelta(seconds=self.create_timeout) <= datetime.now():
@@ -125,7 +166,7 @@ class LaserEVM:
     def execute_state(self, global_state):
         instructions = global_state.environment.code.instruction_list
         try:
-            op_code = instructions[global_state.mstate.pc]['opcode']
+            op_code = instructions[global_state.mstate.pc]["opcode"]
         except IndexError:
             self.open_states.append(global_state.world_state)
             return [], None
@@ -133,7 +174,9 @@ class LaserEVM:
         self._execute_pre_hook(op_code, global_state)
         try:
             self._measure_coverage(global_state)
-            new_global_states = Instruction(op_code, self.dynamic_loader).evaluate(global_state)
+            new_global_states = Instruction(op_code, self.dynamic_loader).evaluate(
+                global_state
+            )
 
         except VmException as e:
             transaction, return_global_state = global_state.transaction_stack.pop()
@@ -142,29 +185,42 @@ class LaserEVM:
                 # In this case we don't put an unmodified world state in the open_states list Since in the case of an
                 #  exceptional halt all changes should be discarded, and this world state would not provide us with a
                 #  previously unseen world state
-                logging.debug("Encountered a VmException, ending path: `{}`".format(str(e)))
+                logging.debug(
+                    "Encountered a VmException, ending path: `{}`".format(str(e))
+                )
                 new_global_states = []
             else:
                 # First execute the post hook for the transaction ending instruction
                 self._execute_post_hook(op_code, [global_state])
-                new_global_states = self._end_message_call(return_global_state, global_state,
+                new_global_states = self._end_message_call(
-                                                           revert_changes=True, return_data=None)
+                    return_global_state,
+                    global_state,
+                    revert_changes=True,
+                    return_data=None,
+                )
 
         except TransactionStartSignal as start_signal:
             # Setup new global state
             new_global_state = start_signal.transaction.initial_global_state()
 
-            new_global_state.transaction_stack = copy(global_state.transaction_stack) + [(start_signal.transaction, global_state)]
+            new_global_state.transaction_stack = copy(
+                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
 
             return [new_global_state], op_code
 
         except TransactionEndSignal as end_signal:
-            transaction, return_global_state = end_signal.global_state.transaction_stack.pop()
+            transaction, return_global_state = (
+                end_signal.global_state.transaction_stack.pop()
+            )
 
             if return_global_state is None:
-                if (not isinstance(transaction, ContractCreationTransaction) or transaction.return_data) and not end_signal.revert:
+                if (
+                    not isinstance(transaction, ContractCreationTransaction)
+                    or transaction.return_data
+                ) and not end_signal.revert:
                     end_signal.global_state.world_state.node = global_state.node
                     self.open_states.append(end_signal.global_state.world_state)
                 new_global_states = []
@@ -172,27 +228,37 @@ class LaserEVM:
                 # First execute the post hook for the transaction ending instruction
                 self._execute_post_hook(op_code, [end_signal.global_state])
 
-                new_global_states = self._end_message_call(return_global_state, global_state,
+                new_global_states = self._end_message_call(
-                                                           revert_changes=False or end_signal.revert,
+                    return_global_state,
-                                                           return_data=transaction.return_data)
+                    global_state,
+                    revert_changes=False or end_signal.revert,
+                    return_data=transaction.return_data,
+                )
 
         self._execute_post_hook(op_code, new_global_states)
 
         return new_global_states, op_code
 
-    def _end_message_call(self, return_global_state, global_state, revert_changes=False, return_data=None):
+    def _end_message_call(
+        self, return_global_state, global_state, revert_changes=False, return_data=None
+    ):
         # Resume execution of the transaction initializing instruction
-        op_code = return_global_state.environment.code.instruction_list[return_global_state.mstate.pc]['opcode']
+        op_code = return_global_state.environment.code.instruction_list[
+            return_global_state.mstate.pc
+        ]["opcode"]
 
         # Set execution result in the return_state
         return_global_state.last_return_data = return_data
         if not revert_changes:
             return_global_state.world_state = copy(global_state.world_state)
-            return_global_state.environment.active_account = \
+            return_global_state.environment.active_account = global_state.accounts[
-                global_state.accounts[return_global_state.environment.active_account.address]
+                return_global_state.environment.active_account.address
+            ]
 
         # Execute the post instruction handler
-        new_global_states = Instruction(op_code, self.dynamic_loader).evaluate(return_global_state, True)
+        new_global_states = Instruction(op_code, self.dynamic_loader).evaluate(
+            return_global_state, True
+        )
 
         # In order to get a nice call graph we need to set the nodes here
         for state in new_global_states:
@@ -206,7 +272,10 @@ class LaserEVM:
         instruction_index = global_state.mstate.pc
 
         if code not in self.coverage.keys():
-            self.coverage[code] = [number_of_instructions, [False]*number_of_instructions]
+            self.coverage[code] = [
+                number_of_instructions,
+                [False] * number_of_instructions,
+            ]
 
         self.coverage[code][1][instruction_index] = True
 
@@ -217,19 +286,27 @@ class LaserEVM:
                 self._new_node_state(state)
         elif opcode == "JUMPI":
             for state in new_states:
-                self._new_node_state(state, JumpType.CONDITIONAL, state.mstate.constraints[-1])
+                self._new_node_state(
+                    state, JumpType.CONDITIONAL, state.mstate.constraints[-1]
+                )
         elif opcode in ("SLOAD", "SSTORE") and len(new_states) > 1:
             for state in new_states:
-                self._new_node_state(state, JumpType.CONDITIONAL, state.mstate.constraints[-1])
+                self._new_node_state(
+                    state, JumpType.CONDITIONAL, state.mstate.constraints[-1]
+                )
 
-        elif opcode in ("CALL", 'CALLCODE', 'DELEGATECALL', 'STATICCALL'):
+        elif opcode in ("CALL", "CALLCODE", "DELEGATECALL", "STATICCALL"):
             assert len(new_states) <= 1
             for state in new_states:
                 self._new_node_state(state, JumpType.CALL)
                 # Keep track of added contracts so the graph can be generated properly
-                if state.environment.active_account.contract_name not in self.world_state.accounts.keys():
+                if (
+                    state.environment.active_account.contract_name
+                    not in self.world_state.accounts.keys()
+                ):
                     self.world_state.accounts[
-                        state.environment.active_account.address] = state.environment.active_account
+                        state.environment.active_account.address
+                    ] = state.environment.active_account
         elif opcode == "RETURN":
             for state in new_states:
                 self._new_node_state(state, JumpType.RETURN)
@@ -243,30 +320,37 @@ class LaserEVM:
         state.node = new_node
         new_node.constraints = state.mstate.constraints
         self.nodes[new_node.uid] = new_node
-        self.edges.append(Edge(old_node.uid, new_node.uid, edge_type=edge_type, condition=condition))
+        self.edges.append(
+            Edge(old_node.uid, new_node.uid, edge_type=edge_type, condition=condition)
+        )
 
         if edge_type == JumpType.RETURN:
             new_node.flags |= NodeFlags.CALL_RETURN
         elif edge_type == JumpType.CALL:
             try:
-                if 'retval' in str(state.mstate.stack[-1]):
+                if "retval" in str(state.mstate.stack[-1]):
                     new_node.flags |= NodeFlags.CALL_RETURN
                 else:
                     new_node.flags |= NodeFlags.FUNC_ENTRY
             except StackUnderflowException:
                 new_node.flags |= NodeFlags.FUNC_ENTRY
-        address = state.environment.code.instruction_list[state.mstate.pc]['address']
+        address = state.environment.code.instruction_list[state.mstate.pc]["address"]
 
         environment = state.environment
         disassembly = environment.code
-        if address in state.environment.code.addr_to_func:
+        if address in disassembly.address_to_function_name:
             # Enter a new function
-
+            environment.active_function_name = disassembly.address_to_function_name[
-            environment.active_function_name = disassembly.addr_to_func[address]
+                address
+            ]
             new_node.flags |= NodeFlags.FUNC_ENTRY
 
             logging.debug(
-                "- Entering function " + environment.active_account.contract_name + ":" + new_node.function_name)
+                "- Entering function "
+                + environment.active_account.contract_name
+                + ":"
+                + new_node.function_name
+            )
         elif address == 0:
             environment.active_function_name = "fallback"
 

mythril/laser/ethereum/taint_analysis.py

@@ -2,6 +2,7 @@ import logging, copy
 import mythril.laser.ethereum.util as helper
 from mythril.laser.ethereum.cfg import JumpType
 
+
 class TaintRecord:
     """
     TaintRecord contains tainting information for a specific (state, node)
@@ -109,22 +110,36 @@ class TaintRunner:
             records = TaintRunner.execute_node(node, record, index)
 
             result.add_records(records)
-            if len(records) == 0:          # continue if there is no record to work on
+            if len(records) == 0:  # continue if there is no record to work on
                 continue
-            children = TaintRunner.children(node, statespace, environment, transaction_stack_length)
+            children = TaintRunner.children(
+                node, statespace, environment, transaction_stack_length
+            )
             for child in children:
                 current_nodes.append((child, records[-1], 0))
         return result
 
     @staticmethod
     def children(node, statespace, environment, transaction_stack_length):
-        direct_children = [statespace.nodes[edge.node_to] for edge in statespace.edges if edge.node_from == node.uid and edge.type != JumpType.Transaction]
+        direct_children = [
+            statespace.nodes[edge.node_to]
+            for edge in statespace.edges
+            if edge.node_from == node.uid and edge.type != JumpType.Transaction
+        ]
         children = []
         for child in direct_children:
-            if all(len(state.transaction_stack) == transaction_stack_length for state in child.states):
+            if all(
+                len(state.transaction_stack) == transaction_stack_length
+                for state in child.states
+            ):
                 children.append(child)
-            elif all(len(state.transaction_stack) > transaction_stack_length for state in child.states):
+            elif all(
-                children += TaintRunner.children(child, statespace, environment, transaction_stack_length)
+                len(state.transaction_stack) > transaction_stack_length
+                for state in child.states
+            ):
+                children += TaintRunner.children(
+                    child, statespace, environment, transaction_stack_length
+                )
         return children
 
     @staticmethod
@@ -150,7 +165,7 @@ class TaintRunner:
         new_record = record.clone()
 
         # Apply Change
-        op = state.get_current_instruction()['opcode']
+        op = state.get_current_instruction()["opcode"]
 
         if op in TaintRunner.stack_taint_table.keys():
             mutator = TaintRunner.stack_taint_table[op]
@@ -171,7 +186,7 @@ class TaintRunner:
             TaintRunner.mutate_sstore(new_record, state.mstate.stack[-1])
         elif op.startswith("LOG"):
             TaintRunner.mutate_log(new_record, op)
-        elif op in ('CALL', 'CALLCODE', 'DELEGATECALL', 'STATICCALL'):
+        elif op in ("CALL", "CALLCODE", "DELEGATECALL", "STATICCALL"):
             TaintRunner.mutate_call(new_record, op)
         else:
             logging.debug("Unknown operation encountered: {}".format(op))
@@ -263,7 +278,7 @@ class TaintRunner:
     @staticmethod
     def mutate_call(record, op):
         pops = 6
-        if op in ('CALL', 'CALLCODE'):
+        if op in ("CALL", "CALLCODE"):
             pops += 1
         for _ in range(pops):
             record.stack.pop()
@@ -272,55 +287,55 @@ class TaintRunner:
 
     stack_taint_table = {
         # instruction: (taint source, taint target)
-        'POP': (1, 0),
+        "POP": (1, 0),
-        'ADD': (2, 1),
+        "ADD": (2, 1),
-        'MUL': (2, 1),
+        "MUL": (2, 1),
-        'SUB': (2, 1),
+        "SUB": (2, 1),
-        'AND': (2, 1),
+        "AND": (2, 1),
-        'OR':  (2, 1),
+        "OR": (2, 1),
-        'XOR': (2, 1),
+        "XOR": (2, 1),
-        'NOT': (1, 1),
+        "NOT": (1, 1),
-        'BYTE': (2, 1),
+        "BYTE": (2, 1),
-        'DIV': (2, 1),
+        "DIV": (2, 1),
-        'MOD': (2, 1),
+        "MOD": (2, 1),
-        'SDIV': (2, 1),
+        "SDIV": (2, 1),
-        'SMOD': (2, 1),
+        "SMOD": (2, 1),
-        'ADDMOD': (3, 1),
+        "ADDMOD": (3, 1),
-        'MULMOD': (3, 1),
+        "MULMOD": (3, 1),
-        'EXP': (2, 1),
+        "EXP": (2, 1),
-        'SIGNEXTEND': (2, 1),
+        "SIGNEXTEND": (2, 1),
-        'LT': (2, 1),
+        "LT": (2, 1),
-        'GT': (2, 1),
+        "GT": (2, 1),
-        'SLT': (2, 1),
+        "SLT": (2, 1),
-        'SGT': (2, 1),
+        "SGT": (2, 1),
-        'EQ': (2, 1),
+        "EQ": (2, 1),
-        'ISZERO': (1, 1),
+        "ISZERO": (1, 1),
-        'CALLVALUE': (0, 1),
+        "CALLVALUE": (0, 1),
-        'CALLDATALOAD': (1, 1),
+        "CALLDATALOAD": (1, 1),
-        'CALLDATACOPY': (3, 0), #todo
+        "CALLDATACOPY": (3, 0),  # todo
-        'CALLDATASIZE': (0, 1),
+        "CALLDATASIZE": (0, 1),
-        'ADDRESS': (0, 1),
+        "ADDRESS": (0, 1),
-        'BALANCE': (1, 1),
+        "BALANCE": (1, 1),
-        'ORIGIN': (0, 1),
+        "ORIGIN": (0, 1),
-        'CALLER': (0, 1),
+        "CALLER": (0, 1),
-        'CODESIZE': (0, 1),
+        "CODESIZE": (0, 1),
-        'SHA3': (2, 1),
+        "SHA3": (2, 1),
-        'GASPRICE': (0, 1),
+        "GASPRICE": (0, 1),
-        'CODECOPY': (3, 0),
+        "CODECOPY": (3, 0),
-        'EXTCODESIZE': (1, 1),
+        "EXTCODESIZE": (1, 1),
-        'EXTCODECOPY': (4, 0),
+        "EXTCODECOPY": (4, 0),
-        'RETURNDATASIZE': (0, 1),
+        "RETURNDATASIZE": (0, 1),
-        'BLOCKHASH': (1, 1),
+        "BLOCKHASH": (1, 1),
-        'COINBASE': (0, 1),
+        "COINBASE": (0, 1),
-        'TIMESTAMP': (0, 1),
+        "TIMESTAMP": (0, 1),
-        'NUMBER': (0, 1),
+        "NUMBER": (0, 1),
-        'DIFFICULTY': (0, 1),
+        "DIFFICULTY": (0, 1),
-        'GASLIMIT': (0, 1),
+        "GASLIMIT": (0, 1),
-        'JUMP': (1, 0),
+        "JUMP": (1, 0),
-        'JUMPI': (2, 0),
+        "JUMPI": (2, 0),
-        'PC': (0, 1),
+        "PC": (0, 1),
-        'MSIZE': (0, 1),
+        "MSIZE": (0, 1),
-        'GAS': (0, 1),
+        "GAS": (0, 1),
-        'CREATE': (3, 1),
+        "CREATE": (3, 1),
-        'RETURN': (2, 0)
+        "RETURN": (2, 0),
     }

mythril/laser/ethereum/transaction/__init__.py

@@ -1,2 +1,5 @@
 from mythril.laser.ethereum.transaction.transaction_models import *
-from mythril.laser.ethereum.transaction.symbolic import execute_message_call,  execute_contract_creation
+from mythril.laser.ethereum.transaction.symbolic import (
+    execute_message_call,
+    execute_contract_creation,
+)

mythril/laser/ethereum/transaction/concolic.py

@@ -1,27 +1,49 @@
-from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction, get_next_transaction_id
+from mythril.laser.ethereum.transaction.transaction_models import (
+    MessageCallTransaction,
+    ContractCreationTransaction,
+    get_next_transaction_id,
+)
 from z3 import BitVec
-from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState
+from mythril.laser.ethereum.state import (
+    GlobalState,
+    Environment,
+    CalldataType,
+    Account,
+    WorldState,
+    Calldata,
+)
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 
 
-def execute_message_call(laser_evm, callee_address, caller_address, origin_address, code, data, gas, gas_price, value):
+def execute_message_call(
+    laser_evm,
+    callee_address,
+    caller_address,
+    origin_address,
+    code,
+    data,
+    gas,
+    gas_price,
+    value,
+):
     """ Executes a message call transaction from all open states """
     open_states = laser_evm.open_states[:]
     del laser_evm.open_states[:]
 
     for open_world_state in open_states:
+        next_transaction_id = get_next_transaction_id()
         transaction = MessageCallTransaction(
-            identifier=get_next_transaction_id(),
+            identifier=next_transaction_id,
             world_state=open_world_state,
             callee_account=open_world_state[callee_address],
             caller=caller_address,
-            call_data=data,
+            call_data=Calldata(next_transaction_id, data),
             gas_price=gas_price,
             call_value=value,
             origin=origin_address,
             call_data_type=CalldataType.SYMBOLIC,
-            code=Disassembly(code)
+            code=Disassembly(code),
         )
 
         _setup_global_state_for_execution(laser_evm, transaction)
@@ -38,8 +60,14 @@ def _setup_global_state_for_execution(laser_evm, transaction):
 
     laser_evm.nodes[new_node.uid] = new_node
     if transaction.world_state.node:
-        laser_evm.edges.append(Edge(transaction.world_state.node.uid, new_node.uid, edge_type=JumpType.Transaction,
+        laser_evm.edges.append(
-                               condition=None))
+            Edge(
+                transaction.world_state.node.uid,
+                new_node.uid,
+                edge_type=JumpType.Transaction,
+                condition=None,
+            )
+        )
     global_state.node = new_node
     new_node.states.append(global_state)
     laser_evm.work_list.append(global_state)

mythril/laser/ethereum/transaction/symbolic.py

@@ -3,9 +3,13 @@ from logging import debug
 
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
-from mythril.laser.ethereum.state import CalldataType
+from mythril.laser.ethereum.state import CalldataType, Calldata
-from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction,\
+from mythril.laser.ethereum.transaction.transaction_models import (
-    get_next_transaction_id
+    MessageCallTransaction,
+    ContractCreationTransaction,
+    get_next_transaction_id,
+)
+
 
 def execute_message_call(laser_evm, callee_address):
     """ Executes a message call transaction from all open states """
@@ -23,7 +27,7 @@ def execute_message_call(laser_evm, callee_address):
             callee_account=open_world_state[callee_address],
             caller=BitVec("caller{}".format(next_transaction_id), 256),
             identifier=next_transaction_id,
-            call_data=[],
+            call_data=Calldata(next_transaction_id),
             gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
             call_value=BitVec("call_value{}".format(next_transaction_id), 256),
             origin=BitVec("origin{}".format(next_transaction_id), 256),
@@ -34,12 +38,16 @@ def execute_message_call(laser_evm, callee_address):
     laser_evm.exec()
 
 
-def execute_contract_creation(laser_evm, contract_initialization_code, contract_name=None):
+def execute_contract_creation(
+    laser_evm, contract_initialization_code, contract_name=None
+):
     """ Executes a contract creation transaction from all open states"""
     open_states = laser_evm.open_states[:]
     del laser_evm.open_states[:]
 
-    new_account = laser_evm.world_state.create_account(0, concrete_storage=True, dynamic_loader=None)
+    new_account = laser_evm.world_state.create_account(
+        0, concrete_storage=True, dynamic_loader=None
+    )
     if contract_name:
         new_account.contract_name = contract_name
 
@@ -55,7 +63,7 @@ def execute_contract_creation(laser_evm, contract_initialization_code, contract_
             BitVec("gas_price{}".format(next_transaction_id), 256),
             BitVec("call_value{}".format(next_transaction_id), 256),
             BitVec("origin{}".format(next_transaction_id), 256),
-            CalldataType.SYMBOLIC
+            CalldataType.SYMBOLIC,
         )
         _setup_global_state_for_execution(laser_evm, transaction)
     laser_evm.exec(True)
@@ -72,10 +80,16 @@ def _setup_global_state_for_execution(laser_evm, transaction):
 
     laser_evm.nodes[new_node.uid] = new_node
     if transaction.world_state.node:
-        laser_evm.edges.append(Edge(transaction.world_state.node.uid, new_node.uid, edge_type=JumpType.Transaction,
+        laser_evm.edges.append(
-                               condition=None))
+            Edge(
+                transaction.world_state.node.uid,
+                new_node.uid,
+                edge_type=JumpType.Transaction,
+                condition=None,
+            )
+        )
 
-        global_state.mstate.constraints = transaction.world_state.node.constraints
+        global_state.mstate.constraints += transaction.world_state.node.constraints
         new_node.constraints = global_state.mstate.constraints
 
     global_state.world_state.transaction_sequence.append(transaction)

mythril/laser/ethereum/transaction/transaction_models.py

@@ -1,6 +1,6 @@
 import logging
 from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.ethereum.state import GlobalState, Environment, WorldState
+from mythril.laser.ethereum.state import GlobalState, Environment, WorldState, Calldata
 from z3 import BitVec
 import array
 
@@ -15,6 +15,7 @@ def get_next_transaction_id():
 
 class TransactionEndSignal(Exception):
     """ Exception raised when a transaction is finalized"""
+
     def __init__(self, global_state, revert=False):
         self.global_state = global_state
         self.revert = revert
@@ -22,6 +23,7 @@ class TransactionEndSignal(Exception):
 
 class TransactionStartSignal(Exception):
     """ Exception raised when a new transaction is started"""
+
     def __init__(self, transaction, op_code):
         self.transaction = transaction
         self.op_code = op_code
@@ -29,28 +31,48 @@ class TransactionStartSignal(Exception):
 
 class MessageCallTransaction:
     """ Transaction object models an transaction"""
-    def __init__(self,
+
-                 world_state,
+    def __init__(
-                 callee_account,
+        self,
-                 caller,
+        world_state,
-                 call_data=(),
+        callee_account,
-                 identifier=None,
+        caller,
-                 gas_price=None,
+        call_data=None,
-                 call_value=None,
+        identifier=None,
-                 origin=None,
+        gas_price=None,
-                 call_data_type=None,
+        call_value=None,
-                 code=None
+        origin=None,
-                 ):
+        call_data_type=None,
+        code=None,
+    ):
         assert isinstance(world_state, WorldState)
         self.id = identifier or get_next_transaction_id()
         self.world_state = world_state
         self.callee_account = callee_account
         self.caller = caller
-        self.call_data = call_data
+        self.call_data = (
-        self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price
+            Calldata(self.id, call_data)
-        self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value
+            if not isinstance(call_data, Calldata)
-        self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin
+            else call_data
-        self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type
+        )
+        self.gas_price = (
+            BitVec("gasprice{}".format(identifier), 256)
+            if gas_price is None
+            else gas_price
+        )
+        self.call_value = (
+            BitVec("callvalue{}".format(identifier), 256)
+            if call_value is None
+            else call_value
+        )
+        self.origin = (
+            BitVec("origin{}".format(identifier), 256) if origin is None else origin
+        )
+        self.call_data_type = (
+            BitVec("call_data_type{}".format(identifier), 256)
+            if call_data_type is None
+            else call_data_type
+        )
         self.code = code
         self.return_data = None
 
@@ -68,7 +90,10 @@ class MessageCallTransaction:
         )
 
         global_state = GlobalState(self.world_state, environment, None)
-        global_state.environment.active_function_name = 'fallback'
+        global_state.environment.active_function_name = "fallback"
+        global_state.mstate.constraints.extend(
+            global_state.environment.calldata.constraints
+        )
 
         return global_state
 
@@ -79,32 +104,56 @@ class MessageCallTransaction:
 
 class ContractCreationTransaction:
     """ Transaction object models an transaction"""
-    def __init__(self,
+
-                 world_state,
+    def __init__(
-                 caller,
+        self,
-                 identifier=None,
+        world_state,
-                 callee_account=None,
+        caller,
-                 code=None,
+        identifier=None,
-                 call_data=(),
+        callee_account=None,
-                 gas_price=None,
+        code=None,
-                 call_value=None,
+        call_data=None,
-                 origin=None,
+        gas_price=None,
-                 call_data_type=None,
+        call_value=None,
-                 ):
+        origin=None,
+        call_data_type=None,
+    ):
         assert isinstance(world_state, WorldState)
         self.id = identifier or get_next_transaction_id()
         self.world_state = world_state
         # TODO: set correct balance for new account
-        self.callee_account = callee_account if callee_account else world_state.create_account(0, concrete_storage=True)
+        self.callee_account = (
+            callee_account
+            if callee_account
+            else world_state.create_account(0, concrete_storage=True)
+        )
 
         self.caller = caller
 
-        self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price
+        self.gas_price = (
-        self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value
+            BitVec("gasprice{}".format(identifier), 256)
-        self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin
+            if gas_price is None
-        self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type
+            else gas_price
+        )
+        self.call_value = (
+            BitVec("callvalue{}".format(identifier), 256)
+            if call_value is None
+            else call_value
+        )
+        self.origin = (
+            BitVec("origin{}".format(identifier), 256) if origin is None else origin
+        )
+        self.call_data_type = (
+            BitVec("call_data_type{}".format(identifier), 256)
+            if call_data_type is None
+            else call_data_type
+        )
 
-        self.call_data = call_data
+        self.call_data = (
+            Calldata(self.id, call_data)
+            if not isinstance(call_data, Calldata)
+            else call_data
+        )
         self.origin = origin
         self.code = code
         self.return_data = None
@@ -123,22 +172,26 @@ class ContractCreationTransaction:
         )
 
         global_state = GlobalState(self.world_state, environment, None)
-        global_state.environment.active_function_name = 'constructor'
+        global_state.environment.active_function_name = "constructor"
+        global_state.mstate.constraints.extend(
+            global_state.environment.calldata.constraints
+        )
 
         return global_state
 
     def end(self, global_state, return_data=None, revert=False):
 
-        if not all([isinstance(element, int) for element in return_data]) or len(return_data) == 0:
+        if (
+            not all([isinstance(element, int) for element in return_data])
+            or len(return_data) == 0
+        ):
             self.return_data = None
             raise TransactionEndSignal(global_state)
 
-        contract_code = bytes.hex(array.array('B', return_data).tostring())
+        contract_code = bytes.hex(array.array("B", return_data).tostring())
 
         global_state.environment.active_account.code = Disassembly(contract_code)
         self.return_data = global_state.environment.active_account.address
         assert global_state.environment.active_account.code.instruction_list != []
 
         raise TransactionEndSignal(global_state, revert=revert)
-
-

mythril/laser/ethereum/util.py

@@ -10,8 +10,6 @@ TT256M1 = 2 ** 256 - 1
 TT255 = 2 ** 255
 
 
-
-
 def sha3(seed):
     return _sha3.keccak_256(bytes(seed)).digest()
 
@@ -33,7 +31,7 @@ def get_instruction_index(instruction_list, address):
     index = 0
 
     for instr in instruction_list:
-        if instr['address'] == address:
+        if instr["address"] == address:
             return index
 
         index += 1
@@ -48,7 +46,7 @@ def get_trace_line(instr, state):
     # stack = re.sub("(\d+)",   lambda m: hex(int(m.group(1))), stack)
     stack = re.sub("\n", "", stack)
 
-    return str(instr['address']) + " " + instr['opcode'] + "\tSTACK: " + stack
+    return str(instr["address"]) + " " + instr["opcode"] + "\tSTACK: " + stack
 
 
 def pop_bitvec(state):
@@ -93,9 +91,9 @@ def get_concrete_int(item):
 def concrete_int_from_bytes(_bytes, start_index):
 
     # logging.debug("-- concrete_int_from_bytes: " + str(_bytes[start_index:start_index+32]))
-    b = _bytes[start_index:start_index+32]
+    b = _bytes[start_index : start_index + 32]
 
-    val = int.from_bytes(b, byteorder='big')
+    val = int.from_bytes(b, byteorder="big")
 
     return val
 
@@ -105,9 +103,9 @@ def concrete_int_to_bytes(val):
     # logging.debug("concrete_int_to_bytes " + str(val))
 
     if type(val) == int:
-        return val.to_bytes(32, byteorder='big')
+        return val.to_bytes(32, byteorder="big")
 
-    return (simplify(val).as_long()).to_bytes(32, byteorder='big')
+    return (simplify(val).as_long()).to_bytes(32, byteorder="big")
 
 
 def bytearray_to_int(arr):
@@ -115,4 +113,3 @@ def bytearray_to_int(arr):
     for a in arr:
         o = (o << 8) + a
     return o
-

mythril/mythril.py

@@ -35,6 +35,7 @@ from mythril.ethereum.interface.leveldb.client import EthLevelDB
 
 # logging.basicConfig(level=logging.DEBUG)
 
+
 class Mythril(object):
     """
     Mythril main interface class.
@@ -75,9 +76,10 @@ class Mythril(object):
         mythril.get_state_variable_from_storage(args)
 
     """
-    def __init__(self, solv=None,
+
-                 solc_args=None, dynld=False, 
+    def __init__(
-                 enable_online_lookup=False):
+        self, solv=None, solc_args=None, dynld=False, enable_online_lookup=False
+    ):
 
         self.solv = solv
         self.solc_args = solc_args
@@ -86,31 +88,41 @@ class Mythril(object):
 
         self.mythril_dir = self._init_mythril_dir()
 
-        self.sigs = signatures.SignatureDb(enable_online_lookup=self.enable_online_lookup)
+        self.sigs = signatures.SignatureDb(
+            enable_online_lookup=self.enable_online_lookup
+        )
         try:
             self.sigs.open()  # tries mythril_dir/signatures.json by default (provide path= arg to make this configurable)
         except FileNotFoundError:
             logging.info(
-                "No signature database found. Creating database if sigs are loaded in: " + self.sigs.signatures_file + "\n" +
+                "No signature database found. Creating database if sigs are loaded in: "
-                "Consider replacing it with the pre-initialized database at https://raw.githubusercontent.com/ConsenSys/mythril/master/signatures.json")
+                + self.sigs.signatures_file
+                + "\n"
+                + "Consider replacing it with the pre-initialized database at https://raw.githubusercontent.com/ConsenSys/mythril/master/signatures.json"
+            )
         except json.JSONDecodeError as jde:
-            raise CriticalError("Invalid JSON in signatures file " + self.sigs.signatures_file + "\n" + str(jde))
+            raise CriticalError(
+                "Invalid JSON in signatures file "
+                + self.sigs.signatures_file
+                + "\n"
+                + str(jde)
+            )
 
         self.solc_binary = self._init_solc_binary(solv)
-        self.config_path = os.path.join(self.mythril_dir, 'config.ini')
+        self.config_path = os.path.join(self.mythril_dir, "config.ini")
         self.leveldb_dir = self._init_config()
 
-        self.eth = None # ethereum API client
+        self.eth = None  # ethereum API client
-        self.eth_db = None # ethereum LevelDB client
+        self.eth_db = None  # ethereum LevelDB client
 
         self.contracts = []  # loaded contracts
 
     @staticmethod
     def _init_mythril_dir():
         try:
-            mythril_dir = os.environ['MYTHRIL_DIR']
+            mythril_dir = os.environ["MYTHRIL_DIR"]
         except KeyError:
-            mythril_dir = os.path.join(os.path.expanduser('~'), ".mythril")
+            mythril_dir = os.path.join(os.path.expanduser("~"), ".mythril")
 
             # Initialize data directory and signature database
 
@@ -128,59 +140,75 @@ class Mythril(object):
         """
 
         system = platform.system().lower()
-        leveldb_fallback_dir = os.path.expanduser('~')
+        leveldb_fallback_dir = os.path.expanduser("~")
         if system.startswith("darwin"):
-            leveldb_fallback_dir = os.path.join(leveldb_fallback_dir, "Library", "Ethereum")
+            leveldb_fallback_dir = os.path.join(
+                leveldb_fallback_dir, "Library", "Ethereum"
+            )
         elif system.startswith("windows"):
-            leveldb_fallback_dir = os.path.join(leveldb_fallback_dir, "AppData", "Roaming", "Ethereum")
+            leveldb_fallback_dir = os.path.join(
+                leveldb_fallback_dir, "AppData", "Roaming", "Ethereum"
+            )
         else:
             leveldb_fallback_dir = os.path.join(leveldb_fallback_dir, ".ethereum")
         leveldb_fallback_dir = os.path.join(leveldb_fallback_dir, "geth", "chaindata")
 
         if not os.path.exists(self.config_path):
             logging.info("No config file found. Creating default: " + self.config_path)
-            open(self.config_path, 'a').close()
+            open(self.config_path, "a").close()
 
         config = ConfigParser(allow_no_value=True)
         config.optionxform = str
-        config.read(self.config_path, 'utf-8')
+        config.read(self.config_path, "utf-8")
-        if 'defaults' not in config.sections():
+        if "defaults" not in config.sections():
             self._add_default_options(config)
 
-        if not config.has_option('defaults', 'leveldb_dir'):
+        if not config.has_option("defaults", "leveldb_dir"):
             self._add_leveldb_option(config, leveldb_fallback_dir)
 
-        if not config.has_option('defaults', 'dynamic_loading'):
+        if not config.has_option("defaults", "dynamic_loading"):
             self._add_dynamic_loading_option(config)
 
-        with codecs.open(self.config_path, 'w', 'utf-8') as fp:
+        with codecs.open(self.config_path, "w", "utf-8") as fp:
             config.write(fp)
 
-        leveldb_dir = config.get('defaults', 'leveldb_dir', fallback=leveldb_fallback_dir)
+        leveldb_dir = config.get(
+            "defaults", "leveldb_dir", fallback=leveldb_fallback_dir
+        )
         return os.path.expanduser(leveldb_dir)
 
     @staticmethod
     def _add_default_options(config):
-        config.add_section('defaults')
+        config.add_section("defaults")
 
     @staticmethod
     def _add_leveldb_option(config, leveldb_fallback_dir):
-        config.set('defaults', "#Default chaindata locations:")
+        config.set("defaults", "#Default chaindata locations:")
-        config.set('defaults', "#– Mac: ~/Library/Ethereum/geth/chaindata")
+        config.set("defaults", "#– Mac: ~/Library/Ethereum/geth/chaindata")
-        config.set('defaults', "#– Linux: ~/.ethereum/geth/chaindata")
+        config.set("defaults", "#– Linux: ~/.ethereum/geth/chaindata")
-        config.set('defaults', "#– Windows: %USERPROFILE%\\AppData\\Roaming\\Ethereum\\geth\\chaindata")
+        config.set(
-        config.set('defaults', 'leveldb_dir', leveldb_fallback_dir)
+            "defaults",
+            "#– Windows: %USERPROFILE%\\AppData\\Roaming\\Ethereum\\geth\\chaindata",
+        )
+        config.set("defaults", "leveldb_dir", leveldb_fallback_dir)
 
     @staticmethod
     def _add_dynamic_loading_option(config):
-        config.set('defaults', '#– To connect to Infura use dynamic_loading: infura')
+        config.set("defaults", "#– To connect to Infura use dynamic_loading: infura")
-        config.set('defaults', '#– To connect to Rpc use '
+        config.set(
-                               'dynamic_loading: HOST:PORT / ganache / infura-[network_name]')
+            "defaults",
-        config.set('defaults', '#– To connect to local host use dynamic_loading: localhost')
+            "#– To connect to Rpc use "
-        config.set('defaults', 'dynamic_loading', 'infura')
+            "dynamic_loading: HOST:PORT / ganache / infura-[network_name]",
+        )
+        config.set(
+            "defaults", "#– To connect to local host use dynamic_loading: localhost"
+        )
+        config.set("defaults", "dynamic_loading", "infura")
 
     def analyze_truffle_project(self, *args, **kwargs):
-        return analyze_truffle_project(self.sigs, *args, **kwargs)  # just passthru by passing signatures for now
+        return analyze_truffle_project(
+            self.sigs, *args, **kwargs
+        )  # just passthru by passing signatures for now
 
     @staticmethod
     def _init_solc_binary(version):
@@ -190,27 +218,31 @@ class Mythril(object):
         if version:
             # tried converting input to semver, seemed not necessary so just slicing for now
             if version == str(solc.main.get_solc_version())[:6]:
-                logging.info('Given version matches installed version')
+                logging.info("Given version matches installed version")
                 try:
-                    solc_binary = os.environ['SOLC']
+                    solc_binary = os.environ["SOLC"]
                 except KeyError:
-                    solc_binary = 'solc'
+                    solc_binary = "solc"
             else:
                 if util.solc_exists(version):
-                    logging.info('Given version is already installed')
+                    logging.info("Given version is already installed")
                 else:
                     try:
-                        solc.install_solc('v' + version)
+                        solc.install_solc("v" + version)
                     except SolcError:
-                        raise CriticalError("There was an error when trying to install the specified solc version")
+                        raise CriticalError(
+                            "There was an error when trying to install the specified solc version"
+                        )
 
-                solc_binary = os.path.join(os.environ['HOME'], ".py-solc/solc-v" + version, "bin/solc")
+                solc_binary = os.path.join(
+                    os.environ["HOME"], ".py-solc/solc-v" + version, "bin/solc"
+                )
                 logging.info("Setting the compiler to " + str(solc_binary))
         else:
             try:
-                solc_binary = os.environ['SOLC']
+                solc_binary = os.environ["SOLC"]
             except KeyError:
-                solc_binary = 'solc'
+                solc_binary = "solc"
         return solc_binary
 
     def set_api_leveldb(self, leveldb):
@@ -219,22 +251,24 @@ class Mythril(object):
         return self.eth
 
     def set_api_rpc_infura(self):
-        self.eth = EthJsonRpc('mainnet.infura.io', 443, True)
+        self.eth = EthJsonRpc("mainnet.infura.io", 443, True)
         logging.info("Using INFURA for RPC queries")
 
     def set_api_rpc(self, rpc=None, rpctls=False):
-        if rpc == 'ganache':
+        if rpc == "ganache":
-            rpcconfig = ('localhost', 8545, False)
+            rpcconfig = ("localhost", 8545, False)
         else:
-            m = re.match(r'infura-(.*)', rpc)
+            m = re.match(r"infura-(.*)", rpc)
-            if m and m.group(1) in ['mainnet', 'rinkeby', 'kovan', 'ropsten']:
+            if m and m.group(1) in ["mainnet", "rinkeby", "kovan", "ropsten"]:
-                rpcconfig = (m.group(1) + '.infura.io', 443, True)
+                rpcconfig = (m.group(1) + ".infura.io", 443, True)
             else:
                 try:
                     host, port = rpc.split(":")
                     rpcconfig = (host, int(port), rpctls)
                 except ValueError:
-                    raise CriticalError("Invalid RPC argument, use 'ganache', 'infura-[network]' or 'HOST:PORT'")
+                    raise CriticalError(
+                        "Invalid RPC argument, use 'ganache', 'infura-[network]' or 'HOST:PORT'"
+                    )
 
         if rpcconfig:
             self.eth = EthJsonRpc(rpcconfig[0], int(rpcconfig[1]), rpcconfig[2])
@@ -243,26 +277,25 @@ class Mythril(object):
             raise CriticalError("Invalid RPC settings, check help for details.")
 
     def set_api_rpc_localhost(self):
-        self.eth = EthJsonRpc('localhost', 8545)
+        self.eth = EthJsonRpc("localhost", 8545)
         logging.info("Using default RPC settings: http://localhost:8545")
 
     def set_api_from_config_path(self):
         config = ConfigParser(allow_no_value=False)
         config.optionxform = str
-        config.read(self.config_path, 'utf-8')
+        config.read(self.config_path, "utf-8")
-        if config.has_option('defaults', 'dynamic_loading'):
+        if config.has_option("defaults", "dynamic_loading"):
-            dynamic_loading = config.get('defaults', 'dynamic_loading')
+            dynamic_loading = config.get("defaults", "dynamic_loading")
         else:
-            dynamic_loading = 'infura'
+            dynamic_loading = "infura"
-        if dynamic_loading == 'infura':
+        if dynamic_loading == "infura":
             self.set_api_rpc_infura()
-        elif dynamic_loading == 'localhost':
+        elif dynamic_loading == "localhost":
             self.set_api_rpc_localhost()
         else:
             self.set_api_rpc(dynamic_loading)
 
     def search_db(self, search):
-
         def search_callback(_, address, balance):
             print("Address: " + address + ", balance: " + str(balance))
 
@@ -273,33 +306,47 @@ class Mythril(object):
             raise CriticalError("Syntax error in search expression.")
 
     def contract_hash_to_address(self, hash):
-        if not re.match(r'0x[a-fA-F0-9]{64}', hash):
+        if not re.match(r"0x[a-fA-F0-9]{64}", hash):
-             raise CriticalError("Invalid address hash. Expected format is '0x...'.")
+            raise CriticalError("Invalid address hash. Expected format is '0x...'.")
 
         print(self.eth_db.contract_hash_to_address(hash))
 
     def load_from_bytecode(self, code):
         address = util.get_indexed_address(0)
-        self.contracts.append(ETHContract(code, name="MAIN", enable_online_lookup=self.enable_online_lookup))
+        self.contracts.append(
+            ETHContract(
+                code, name="MAIN", enable_online_lookup=self.enable_online_lookup
+            )
+        )
         return address, self.contracts[-1]  # return address and contract object
 
     def load_from_address(self, address):
-        if not re.match(r'0x[a-fA-F0-9]{40}', address):
+        if not re.match(r"0x[a-fA-F0-9]{40}", address):
-             raise CriticalError("Invalid contract address. Expected format is '0x...'.")
+            raise CriticalError("Invalid contract address. Expected format is '0x...'.")
 
         try:
             code = self.eth.eth_getCode(address)
         except FileNotFoundError as e:
-             raise CriticalError("IPC error: " + str(e))
+            raise CriticalError("IPC error: " + str(e))
         except ConnectionError:
-            raise CriticalError("Could not connect to RPC server. Make sure that your node is running and that RPC parameters are set correctly.")
+            raise CriticalError(
+                "Could not connect to RPC server. Make sure that your node is running and that RPC parameters are set correctly."
+            )
         except Exception as e:
             raise CriticalError("IPC / RPC error: " + str(e))
         else:
             if code == "0x" or code == "0x0":
-                 raise CriticalError("Received an empty response from eth_getCode. Check the contract address and verify that you are on the correct chain.")
+                raise CriticalError(
+                    "Received an empty response from eth_getCode. Check the contract address and verify that you are on the correct chain."
+                )
             else:
-                self.contracts.append(ETHContract(code, name=address, enable_online_lookup=self.enable_online_lookup))
+                self.contracts.append(
+                    ETHContract(
+                        code,
+                        name=address,
+                        enable_online_lookup=self.enable_online_lookup,
+                    )
+                )
         return address, self.contracts[-1]  # return address and contract object
 
     def load_from_solidity(self, solidity_files):
@@ -320,57 +367,105 @@ class Mythril(object):
 
             try:
                 # import signatures from solidity source
-                self.sigs.import_from_solidity_source(file, solc_binary=self.solc_binary, solc_args=self.solc_args)
+                self.sigs.import_from_solidity_source(
+                    file, solc_binary=self.solc_binary, solc_args=self.solc_args
+                )
                 # Save updated function signatures
                 self.sigs.write()  # dump signatures to disk (previously opened file or default location)
 
                 if contract_name is not None:
-                    contract = SolidityContract(file, contract_name, solc_args=self.solc_args)
+                    contract = SolidityContract(
+                        file, contract_name, solc_args=self.solc_args
+                    )
                     self.contracts.append(contract)
                     contracts.append(contract)
                 else:
-                    for contract in get_contracts_from_file(file, solc_args=self.solc_args):
+                    for contract in get_contracts_from_file(
+                        file, solc_args=self.solc_args
+                    ):
                         self.contracts.append(contract)
                         contracts.append(contract)
 
-
             except FileNotFoundError:
                 raise CriticalError("Input file not found: " + file)
             except CompilerError as e:
                 raise CriticalError(e)
             except NoContractFoundError:
-                logging.info("The file " + file + " does not contain a compilable contract.")
+                logging.info(
-
+                    "The file " + file + " does not contain a compilable contract."
+                )
 
         return address, contracts
 
-    def dump_statespace(self, strategy, contract, address=None, max_depth=None,
+    def dump_statespace(
-                        execution_timeout=None, create_timeout=None):
+        self,
-
+        strategy,
-        sym = SymExecWrapper(contract, address, strategy,
+        contract,
-                             dynloader=DynLoader(self.eth) if self.dynld else None,
+        address=None,
-                             max_depth=max_depth, execution_timeout=execution_timeout, create_timeout=create_timeout)
+        max_depth=None,
+        execution_timeout=None,
+        create_timeout=None,
+    ):
+
+        sym = SymExecWrapper(
+            contract,
+            address,
+            strategy,
+            dynloader=DynLoader(self.eth) if self.dynld else None,
+            max_depth=max_depth,
+            execution_timeout=execution_timeout,
+            create_timeout=create_timeout,
+        )
 
         return get_serializable_statespace(sym)
 
-    def graph_html(self, strategy, contract, address, max_depth=None, enable_physics=False,
+    def graph_html(
-                   phrackify=False, execution_timeout=None, create_timeout=None):
+        self,
-        sym = SymExecWrapper(contract, address, strategy,
+        strategy,
-                             dynloader=DynLoader(self.eth) if self.dynld else None,
+        contract,
-                             max_depth=max_depth, execution_timeout=execution_timeout, create_timeout=create_timeout)
+        address,
+        max_depth=None,
+        enable_physics=False,
+        phrackify=False,
+        execution_timeout=None,
+        create_timeout=None,
+    ):
+        sym = SymExecWrapper(
+            contract,
+            address,
+            strategy,
+            dynloader=DynLoader(self.eth) if self.dynld else None,
+            max_depth=max_depth,
+            execution_timeout=execution_timeout,
+            create_timeout=create_timeout,
+        )
         return generate_graph(sym, physics=enable_physics, phrackify=phrackify)
 
-    def fire_lasers(self, strategy, contracts=None, address=None,
+    def fire_lasers(
-                    modules=None, verbose_report=False, max_depth=None, execution_timeout=None, create_timeout=None,
+        self,
-                    max_transaction_count=None):
+        strategy,
+        contracts=None,
+        address=None,
+        modules=None,
+        verbose_report=False,
+        max_depth=None,
+        execution_timeout=None,
+        create_timeout=None,
+        max_transaction_count=None,
+    ):
 
         all_issues = []
-        for contract in (contracts or self.contracts):
+        for contract in contracts or self.contracts:
-            sym = SymExecWrapper(contract, address, strategy,
+            sym = SymExecWrapper(
-                                 dynloader=DynLoader(self.eth) if self.dynld else None,
+                contract,
-                                 max_depth=max_depth, execution_timeout=execution_timeout,
+                address,
-                                 create_timeout=create_timeout,
+                strategy,
-                                 max_transaction_count=max_transaction_count)
+                dynloader=DynLoader(self.eth) if self.dynld else None,
+                max_depth=max_depth,
+                execution_timeout=execution_timeout,
+                create_timeout=create_timeout,
+                max_transaction_count=max_transaction_count,
+            )
 
             issues = fire_lasers(sym, modules)
 
@@ -394,13 +489,18 @@ class Mythril(object):
         try:
             if params[0] == "mapping":
                 if len(params) < 3:
-                     raise CriticalError("Invalid number of parameters.")
+                    raise CriticalError("Invalid number of parameters.")
                 position = int(params[1])
                 position_formatted = utils.zpad(utils.int_to_big_endian(position), 32)
                 for i in range(2, len(params)):
-                    key = bytes(params[i], 'utf8')
+                    key = bytes(params[i], "utf8")
                     key_formatted = utils.rzpad(key, 32)
-                    mappings.append(int.from_bytes(utils.sha3(key_formatted + position_formatted), byteorder='big'))
+                    mappings.append(
+                        int.from_bytes(
+                            utils.sha3(key_formatted + position_formatted),
+                            byteorder="big",
+                        )
+                    )
 
                 length = len(mappings)
                 if length == 1:
@@ -408,37 +508,58 @@ class Mythril(object):
 
             else:
                 if len(params) >= 4:
-                     raise CriticalError("Invalid number of parameters.")
+                    raise CriticalError("Invalid number of parameters.")
 
                 if len(params) >= 1:
                     position = int(params[0])
                 if len(params) >= 2:
                     length = int(params[1])
                 if len(params) == 3 and params[2] == "array":
-                    position_formatted = utils.zpad(utils.int_to_big_endian(position), 32)
+                    position_formatted = utils.zpad(
-                    position = int.from_bytes(utils.sha3(position_formatted), byteorder='big')
+                        utils.int_to_big_endian(position), 32
+                    )
+                    position = int.from_bytes(
+                        utils.sha3(position_formatted), byteorder="big"
+                    )
 
         except ValueError:
-             raise CriticalError("Invalid storage index. Please provide a numeric value.")
+            raise CriticalError(
+                "Invalid storage index. Please provide a numeric value."
+            )
 
         outtxt = []
 
         try:
             if length == 1:
-                outtxt.append("{}: {}".format(position, self.eth.eth_getStorageAt(address, position)))
+                outtxt.append(
+                    "{}: {}".format(
+                        position, self.eth.eth_getStorageAt(address, position)
+                    )
+                )
             else:
                 if len(mappings) > 0:
                     for i in range(0, len(mappings)):
                         position = mappings[i]
-                        outtxt.append("{}: {}".format(hex(position), self.eth.eth_getStorageAt(address, position)))
+                        outtxt.append(
+                            "{}: {}".format(
+                                hex(position),
+                                self.eth.eth_getStorageAt(address, position),
+                            )
+                        )
                 else:
                     for i in range(position, position + length):
-                        outtxt.append("{}: {}".format(hex(i), self.eth.eth_getStorageAt(address, i)))
+                        outtxt.append(
+                            "{}: {}".format(
+                                hex(i), self.eth.eth_getStorageAt(address, i)
+                            )
+                        )
         except FileNotFoundError as e:
-             raise CriticalError("IPC error: " + str(e))
+            raise CriticalError("IPC error: " + str(e))
         except ConnectionError:
-            raise CriticalError("Could not connect to RPC server. Make sure that your node is running and that RPC parameters are set correctly.")
+            raise CriticalError(
-        return '\n'.join(outtxt)
+                "Could not connect to RPC server. Make sure that your node is running and that RPC parameters are set correctly."
+            )
+        return "\n".join(outtxt)
 
     @staticmethod
     def disassemble(contract):

mythril/support/loader.py

@@ -4,7 +4,6 @@ import re
 
 
 class DynLoader:
-
     def __init__(self, eth):
         self.eth = eth
         self.storage_cache = {}
@@ -19,13 +18,17 @@ class DynLoader:
 
             self.storage_cache[contract_address] = {}
 
-            data = self.eth.eth_getStorageAt(contract_address, position=index, block='latest')
+            data = self.eth.eth_getStorageAt(
+                contract_address, position=index, block="latest"
+            )
 
             self.storage_cache[contract_address][index] = data
 
         except IndexError:
 
-            data = self.eth.eth_getStorageAt(contract_address, position=index, block='latest')
+            data = self.eth.eth_getStorageAt(
+                contract_address, position=index, block="latest"
+            )
 
             self.storage_cache[contract_address][index] = data
 
@@ -33,9 +36,11 @@ class DynLoader:
 
     def dynld(self, contract_address, dependency_address):
 
-        logging.info("Dynld at contract " + contract_address + ": " + dependency_address)
+        logging.info(
+            "Dynld at contract " + contract_address + ": " + dependency_address
+        )
 
-        m = re.match(r'^(0x[0-9a-fA-F]{40})$', dependency_address)
+        m = re.match(r"^(0x[0-9a-fA-F]{40})$", dependency_address)
 
         if m:
             dependency_address = m.group(1)

mythril/support/signatures.py

@@ -26,14 +26,15 @@ try:
     import fcntl
 
     def lock_file(f, exclusive=False):
-        if f.mode == 'r' and exclusive:
+        if f.mode == "r" and exclusive:
-            raise Exception('Please use non exclusive mode for reading')
+            raise Exception("Please use non exclusive mode for reading")
         flag = fcntl.LOCK_EX if exclusive else fcntl.LOCK_SH
         fcntl.lockf(f, flag)
 
     def unlock_file(f):
         return
 
+
 except ImportError:
     # Windows file locking
     # TODO: confirm the existence or non existence of shared locks in windows msvcrt and make changes based on that
@@ -43,8 +44,8 @@ except ImportError:
         return os.path.getsize(os.path.realpath(f.name))
 
     def lock_file(f, exclusive=False):
-        if f.mode == 'r' and exclusive:
+        if f.mode == "r" and exclusive:
-            raise Exception('Please use non exclusive mode for reading')
+            raise Exception("Please use non exclusive mode for reading")
         msvcrt.locking(f.fileno(), msvcrt.LK_RLCK, file_size(f))
 
     def unlock_file(f):
@@ -52,7 +53,6 @@ except ImportError:
 
 
 class SignatureDb(object):
-
     def __init__(self, enable_online_lookup=False):
         """
         Constr
@@ -60,9 +60,15 @@ class SignatureDb(object):
         """
         self.signatures = {}  # signatures in-mem cache
         self.signatures_file = None
-        self.enable_online_lookup = enable_online_lookup  # enable online funcsig resolving
+        self.enable_online_lookup = (
-        self.online_lookup_miss = set()  # temporarily track misses from onlinedb to avoid requesting the same non-existent sighash multiple times
+            enable_online_lookup
-        self.online_directory_unavailable_until = 0  # flag the online directory as unavailable for some time
+        )  # enable online funcsig resolving
+        self.online_lookup_miss = (
+            set()
+        )  # temporarily track misses from onlinedb to avoid requesting the same non-existent sighash multiple times
+        self.online_directory_unavailable_until = (
+            0
+        )  # flag the online directory as unavailable for some time
 
     def open(self, path=None):
         """
@@ -74,15 +80,19 @@ class SignatureDb(object):
         if not path:
             #  try default locations
             try:
-                mythril_dir = os.environ['MYTHRIL_DIR']
+                mythril_dir = os.environ["MYTHRIL_DIR"]
             except KeyError:
-                mythril_dir = os.path.join(os.path.expanduser('~'), ".mythril")
+                mythril_dir = os.path.join(os.path.expanduser("~"), ".mythril")
-            path = os.path.join(mythril_dir, 'signatures.json')
+            path = os.path.join(mythril_dir, "signatures.json")
 
-        self.signatures_file = path  # store early to allow error handling to access the place we tried to load the file
+        self.signatures_file = (
+            path
+        )  # store early to allow error handling to access the place we tried to load the file
         if not os.path.exists(path):
             logging.debug("Signatures: file not found: %s" % path)
-            raise FileNotFoundError("Missing function signature file. Resolving of function names disabled.")
+            raise FileNotFoundError(
+                "Missing function signature file. Resolving of function names disabled."
+            )
 
         with open(path, "r") as f:
             lock_file(f)
@@ -121,16 +131,18 @@ class SignatureDb(object):
                 finally:
                     unlock_file(f)
 
-            sigs.update(self.signatures)  # reload file and merge cached sigs into what we load from file
+            sigs.update(
+                self.signatures
+            )  # reload file and merge cached sigs into what we load from file
             self.signatures = sigs
 
         if directory and not os.path.exists(directory):
-            os.makedirs(directory)         # create folder structure if not existS
+            os.makedirs(directory)  # create folder structure if not existS
 
-        if not os.path.exists(path):       # creates signatures.json file if it doesn't exist
+        if not os.path.exists(path):  # creates signatures.json file if it doesn't exist
             open(path, "w").close()
 
-        with open(path, "r+") as f:        # placing 'w+' here will result in race conditions
+        with open(path, "r+") as f:  # placing 'w+' here will result in race conditions
             lock_file(f, exclusive=True)
             try:
                 json.dump(self.signatures, f)
@@ -150,11 +162,20 @@ class SignatureDb(object):
         """
         if not sighash.startswith("0x"):
             sighash = "0x%s" % sighash  # normalize sighash format
-        if self.enable_online_lookup and not self.signatures.get(sighash) and sighash not in self.online_lookup_miss and time.time() > self.online_directory_unavailable_until:
+        if (
+            self.enable_online_lookup
+            and not self.signatures.get(sighash)
+            and sighash not in self.online_lookup_miss
+            and time.time() > self.online_directory_unavailable_until
+        ):
             # online lookup enabled, and signature not in cache, sighash was not a miss earlier, and online directory not down
-            logging.debug("Signatures: performing online lookup for sighash %r" % sighash)
+            logging.debug(
+                "Signatures: performing online lookup for sighash %r" % sighash
+            )
             try:
-                funcsigs = SignatureDb.lookup_online(sighash, timeout=timeout)  # might return multiple sigs
+                funcsigs = SignatureDb.lookup_online(
+                    sighash, timeout=timeout
+                )  # might return multiple sigs
                 if funcsigs:
                     # only store if we get at least one result
                     self.signatures[sighash] = funcsigs
@@ -162,11 +183,19 @@ class SignatureDb(object):
                     # miss
                     self.online_lookup_miss.add(sighash)
             except FourByteDirectoryOnlineLookupError as fbdole:
-                self.online_directory_unavailable_until = time.time() + 2 * 60  # wait at least 2 mins to try again
+                self.online_directory_unavailable_until = (
-                logging.warning("online function signature lookup not available. will not try to lookup hash for the next 2 minutes. exception: %r" % fbdole)
+                    time.time() + 2 * 60
+                )  # wait at least 2 mins to try again
+                logging.warning(
+                    "online function signature lookup not available. will not try to lookup hash for the next 2 minutes. exception: %r"
+                    % fbdole
+                )
+
+        if sighash not in self.signatures:
+            return []
         if type(self.signatures[sighash]) != list:
             return [self.signatures[sighash]]
-        return self.signatures[sighash]  # raise keyerror
+        return self.signatures[sighash]
 
     def __getitem__(self, item):
         """
@@ -176,13 +205,19 @@ class SignatureDb(object):
         """
         return self.get(sighash=item)
 
-    def import_from_solidity_source(self, file_path, solc_binary="solc", solc_args=None):
+    def import_from_solidity_source(
+        self, file_path, solc_binary="solc", solc_args=None
+    ):
         """
         Import Function Signatures from solidity source files
         :param file_path: solidity source code file path
         :return: self
         """
-        self.signatures.update(SignatureDb.get_sigs_from_file(file_path, solc_binary=solc_binary, solc_args=solc_args))
+        self.signatures.update(
+            SignatureDb.get_sigs_from_file(
+                file_path, solc_binary=solc_binary, solc_args=solc_args
+            )
+        )
         return self
 
     @staticmethod
@@ -200,9 +235,11 @@ class SignatureDb(object):
         """
         if not ethereum_input_decoder:
             return None
-        return list(ethereum_input_decoder.decoder.FourByteDirectory.lookup_signatures(sighash,
+        return list(
-                                                                                       timeout=timeout,
+            ethereum_input_decoder.decoder.FourByteDirectory.lookup_signatures(
-                                                                                       proxies=proxies))
+                sighash, timeout=timeout, proxies=proxies
+            )
+        )
 
     @staticmethod
     def get_sigs_from_file(file_name, solc_binary="solc", solc_args=None):
@@ -220,13 +257,19 @@ class SignatureDb(object):
             ret = p.returncode
 
             if ret != 0:
-                raise CompilerError("Solc experienced a fatal error (code %d).\n\n%s" % (ret, stderr.decode('UTF-8')))
+                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.")
+                "Compiler not found. Make sure that solc is installed and in PATH, or set the SOLC environment variable."
-        stdout = stdout.decode('unicode_escape').split('\n')
+            )
+        stdout = stdout.decode("unicode_escape").split("\n")
         for line in stdout:
-            if '(' in line and ')' in line and ":" in line:        # the ':' need not be checked but just to be sure
+            if (
-                sigs["0x"+line.split(':')[0]] = [line.split(":")[1].strip()]
+                "(" in line and ")" in line and ":" in line
+            ):  # the ':' need not be checked but just to be sure
+                sigs["0x" + line.split(":")[0]] = [line.split(":")[1].strip()]
         logging.debug("Signatures: found %d signatures after parsing" % len(sigs))
         return sigs

mythril/support/truffle.py

@@ -25,36 +25,49 @@ def analyze_truffle_project(sigs, args):
 
     for filename in files:
 
-        if re.match(r'.*\.json$', filename) and filename != "Migrations.json":
+        if re.match(r".*\.json$", filename) and filename != "Migrations.json":
 
             with open(os.path.join(build_dir, filename)) as cf:
                 contractdata = json.load(cf)
 
             try:
-                name = contractdata['contractName']
+                name = contractdata["contractName"]
-                bytecode = contractdata['deployedBytecode']
+                bytecode = contractdata["deployedBytecode"]
-                filename = PurePath(contractdata['sourcePath']).name
+                filename = PurePath(contractdata["sourcePath"]).name
             except KeyError:
-                print("Unable to parse contract data. Please use Truffle 4 to compile your project.")
+                print(
+                    "Unable to parse contract data. Please use Truffle 4 to compile your project."
+                )
                 sys.exit()
             if len(bytecode) < 4:
                 continue
 
-            sigs.import_from_solidity_source(contractdata['sourcePath'], solc_args=args.solc_args)
+            sigs.import_from_solidity_source(
+                contractdata["sourcePath"], solc_args=args.solc_args
+            )
             sigs.write()
 
             ethcontract = ETHContract(bytecode, name=name)
 
             address = util.get_indexed_address(0)
-            sym = SymExecWrapper(ethcontract, address, args.strategy, max_depth=args.max_depth,
+            sym = SymExecWrapper(
-                                 create_timeout=args.create_timeout, execution_timeout=args.execution_timeout)
+                ethcontract,
+                address,
+                args.strategy,
+                max_depth=args.max_depth,
+                create_timeout=args.create_timeout,
+                execution_timeout=args.execution_timeout,
+            )
             issues = fire_lasers(sym)
 
             if not len(issues):
-                if args.outform == 'text' or args.outform == 'markdown':
+                if args.outform == "text" or args.outform == "markdown":
                     print("# Analysis result for " + name + "\n\nNo issues found.")
                 else:
-                    result = {'contract': name, 'result': {'success': True, 'error': None, 'issues': []}}
+                    result = {
+                        "contract": name,
+                        "result": {"success": True, "error": None, "issues": []},
+                    }
                     print(json.dumps(result))
             else:
 
@@ -62,9 +75,9 @@ def analyze_truffle_project(sigs, args):
                 # augment with source code
 
                 disassembly = ethcontract.disassembly
-                source = contractdata['source']
+                source = contractdata["source"]
 
-                deployed_source_map = contractdata['deployedSourceMap'].split(";")
+                deployed_source_map = contractdata["deployedSourceMap"].split(";")
 
                 mappings = []
 
@@ -80,34 +93,49 @@ def analyze_truffle_project(sigs, args):
                     if len(mapping) > 2 and len(mapping[2]) > 0:
                         idx = int(mapping[2])
 
-                    lineno = source.encode('utf-8')[0:offset].count('\n'.encode('utf-8')) + 1
+                    lineno = (
+                        source.encode("utf-8")[0:offset].count("\n".encode("utf-8")) + 1
+                    )
 
                     mappings.append(SourceMapping(idx, offset, length, lineno))
 
                 for issue in issues:
 
-                    index = get_instruction_index(disassembly.instruction_list, issue.address)
+                    index = get_instruction_index(
+                        disassembly.instruction_list, issue.address
+                    )
 
                     if index:
-                            try:
+                        try:
-                                offset = mappings[index].offset
+                            offset = mappings[index].offset
-                                length = mappings[index].length
+                            length = mappings[index].length
-
+
-                                issue.filename = filename
+                            issue.filename = filename
-                                issue.code = source.encode('utf-8')[offset:offset + length].decode('utf-8')
+                            issue.code = source.encode("utf-8")[
-                                issue.lineno = mappings[index].lineno
+                                offset : offset + length
-                            except IndexError:
+                            ].decode("utf-8")
-                                logging.debug("No code mapping at index %d", index)
+                            issue.lineno = mappings[index].lineno
+                        except IndexError:
+                            logging.debug("No code mapping at index %d", index)
 
                     report.append_issue(issue)
 
-                if args.outform == 'json':
+                if args.outform == "json":
 
-                    result = {'contract': name, 'result': {'success': True, 'error': None, 'issues': list(map(lambda x: x.as_dict, issues))}}
+                    result = {
+                        "contract": name,
+                        "result": {
+                            "success": True,
+                            "error": None,
+                            "issues": list(map(lambda x: x.as_dict, issues)),
+                        },
+                    }
                     print(json.dumps(result))
 
                 else:
-                    if args.outform == 'text':
+                    if args.outform == "text":
-                        print("# Analysis result for " + name + ":\n\n" + report.as_text())
+                        print(
-                    elif args.outform == 'markdown':
+                            "# Analysis result for " + name + ":\n\n" + report.as_text()
+                        )
+                    elif args.outform == "markdown":
                         print(report.as_markdown())

mythril/version.py

@@ -1,3 +1,3 @@
 # This file is suitable for sourcing inside POSIX shell, e.g. bash as
 # well as for importing into Python
-VERSION="v0.18.13"  # NOQA
+VERSION = "v0.18.13"  # NOQA

requirements.txt

@@ -25,3 +25,4 @@ requests
 rlp>=1.0.1
 transaction>=2.2.1
 z3-solver>=4.5
+pysha3

setup.py

@@ -22,19 +22,22 @@ VERSION = None
 # Package version (vX.Y.Z). It must match git tag being used for CircleCI
 # deployment; otherwise the build will failed.
 
-version_path = (Path(__file__).parent / 'mythril' / 'version.py').absolute()
+version_path = (Path(__file__).parent / "mythril" / "version.py").absolute()
-exec(open(str(version_path), 'r').read())
+exec(open(str(version_path), "r").read())
 
 
 class VerifyVersionCommand(install):
     """Custom command to verify that the git tag matches our version"""
-    description = 'verify that the git tag matches our version'
+
+    description = "verify that the git tag matches our version"
 
     def run(self):
-        tag = os.getenv('CIRCLE_TAG')
+        tag = os.getenv("CIRCLE_TAG")
 
         if tag != VERSION:
-            info = "Git tag: {0} does not match the version of this app: {1}".format(tag, VERSION)
+            info = "Git tag: {0} does not match the version of this app: {1}".format(
+                tag, VERSION
+            )
             sys.exit(info)
 
 
@@ -44,92 +47,62 @@ def read_file(fname):
     :param fname: path relative to setup.py
     :return: file contents
     """
-    with open(os.path.join(os.path.dirname(__file__), fname), 'r') as fd:
+    with open(os.path.join(os.path.dirname(__file__), fname), "r") as fd:
         return fd.read()
 
 
 setup(
-    name='mythril',
+    name="mythril",
-
     version=VERSION[1:],
-
+    description="Security analysis tool for Ethereum smart contracts",
-    description='Security analysis tool for Ethereum smart contracts',
     long_description=read_file("README.md") if os.path.isfile("README.md") else "",
-    long_description_content_type='text/markdown',  # requires twine and recent setuptools
+    long_description_content_type="text/markdown",  # requires twine and recent setuptools
-
+    url="https://github.com/b-mueller/mythril",
-    url='https://github.com/b-mueller/mythril',
+    author="Bernhard Mueller",
-
+    author_email="bernhard.mueller11@gmail.com",
-    author='Bernhard Mueller',
+    license="MIT",
-    author_email='bernhard.mueller11@gmail.com',
-
-    license='MIT',
-
     classifiers=[
-        'Development Status :: 3 - Alpha',
+        "Development Status :: 3 - Alpha",
-
+        "Intended Audience :: Science/Research",
-        'Intended Audience :: Science/Research',
+        "Topic :: Software Development :: Disassemblers",
-        'Topic :: Software Development :: Disassemblers',
+        "License :: OSI Approved :: MIT License",
-
+        "Programming Language :: Python :: 3.5",
-        'License :: OSI Approved :: MIT License',
+        "Programming Language :: Python :: 3.6",
-
+        "Programming Language :: Python :: 3.7",
-        'Programming Language :: Python :: 3.5',
-        'Programming Language :: Python :: 3.6',
-        'Programming Language :: Python :: 3.7',
     ],
-
+    keywords="hacking disassembler security ethereum",
-    keywords='hacking disassembler security ethereum',
+    packages=find_packages(exclude=["contrib", "docs", "tests"]),
-
-    packages=find_packages(exclude=['contrib', 'docs', 'tests']),
-
     install_requires=[
-        'coloredlogs>=10.0',
+        "coloredlogs>=10.0",
-        'ethereum>=2.3.2',
+        "ethereum>=2.3.2",
-        'z3-solver>=4.5',
+        "z3-solver>=4.5",
-        'requests',
+        "requests",
-        'py-solc',
+        "py-solc",
-        'plyvel',
+        "plyvel",
-        'eth_abi>=1.0.0',
+        "eth_abi>=1.0.0",
-        'eth-utils>=1.0.1',
+        "eth-utils>=1.0.1",
-        'eth-account>=0.1.0a2',
+        "eth-account>=0.1.0a2",
-        'eth-hash>=0.1.0',
+        "eth-hash>=0.1.0",
-        'eth-keyfile>=0.5.1',
+        "eth-keyfile>=0.5.1",
-        'eth-keys>=0.2.0b3',
+        "eth-keys>=0.2.0b3",
-        'eth-rlp>=0.1.0',
+        "eth-rlp>=0.1.0",
-        'eth-tester>=0.1.0b21',
+        "eth-tester>=0.1.0b21",
-        'eth-typing>=1.3.0,<2.0.0',
+        "eth-typing>=1.3.0,<2.0.0",
-        'coverage',
+        "coverage",
-        'jinja2>=2.9',
+        "jinja2>=2.9",
-        'rlp>=1.0.1',
+        "rlp>=1.0.1",
-        'transaction>=2.2.1',
+        "transaction>=2.2.1",
-        'py-flags',
+        "py-flags",
-        'mock',
+        "mock",
-        'configparser>=3.5.0',
+        "configparser>=3.5.0",
-        'persistent>=4.2.0',
+        "persistent>=4.2.0",
-        'ethereum-input-decoder>=0.2.2'
+        "ethereum-input-decoder>=0.2.2",
     ],
-
+    tests_require=["pytest>=3.6.0", "pytest_mock", "pytest-cov"],
-    tests_require=[
+    python_requires=">=3.5",
-        'pytest>=3.6.0',
+    extras_require={},
-        'pytest_mock',
+    package_data={"mythril.analysis.templates": ["*"]},
-        'pytest-cov'
-    ],
-
-    python_requires='>=3.5',
-
-    extras_require={
-    },
-
-    package_data={
-        'mythril.analysis.templates': ['*']
-    },
-
     include_package_data=True,
-
+    entry_points={"console_scripts": ["myth=mythril.interfaces.cli:main"]},
-    entry_points={
+    cmdclass={"verify": VerifyVersionCommand},
-        'console_scripts': ["myth=mythril.interfaces.cli:main"],
-    },
-
-    cmdclass={
-        'verify': VerifyVersionCommand,
-    }
 )

tests/__init__.py

@@ -16,15 +16,17 @@ MYTHRIL_DIR = TESTS_DIR / "mythril_dir"
 
 
 class BaseTestCase(TestCase):
-
     def setUp(self):
         self.changed_files = []
-        self.ori_mythril_dir = getattr(os.environ, 'MYTHRIL_DIR', '')
+        self.ori_mythril_dir = getattr(os.environ, "MYTHRIL_DIR", "")
-        os.environ['MYTHRIL_DIR'] = str(MYTHRIL_DIR)
+        os.environ["MYTHRIL_DIR"] = str(MYTHRIL_DIR)
-        shutil.copyfile(str(MYTHRIL_DIR / "signatures.json.example"), str(MYTHRIL_DIR / "signatures.json"))
+        shutil.copyfile(
+            str(MYTHRIL_DIR / "signatures.json.example"),
+            str(MYTHRIL_DIR / "signatures.json"),
+        )
 
     def tearDown(self):
-        os.environ['MYTHRIL_DIR'] = self.ori_mythril_dir
+        os.environ["MYTHRIL_DIR"] = self.ori_mythril_dir
         os.remove(str(MYTHRIL_DIR / "signatures.json"))
 
     def compare_files_error_message(self):
@@ -41,4 +43,6 @@ class BaseTestCase(TestCase):
         self.changed_files.append((input_file, output_expected, output_current))
 
     def assert_and_show_changed_files(self):
-        self.assertEqual(0, len(self.changed_files), msg=self.compare_files_error_message())
+        self.assertEqual(
+            0, len(self.changed_files), msg=self.compare_files_error_message()
+        )

tests/analysis/test_delegatecall.py

@@ -1,12 +1,16 @@
-from mythril.analysis.modules.delegatecall import execute, _concrete_call, _symbolic_call
+from mythril.analysis.modules.delegatecall import (
+    execute,
+    _concrete_call,
+    _symbolic_call,
+)
 from mythril.analysis.ops import Call, Variable, VarType
 from mythril.analysis.symbolic import SymExecWrapper
-from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node
 from mythril.laser.ethereum.state import GlobalState, Environment, Account
 import pytest
 from unittest.mock import MagicMock, patch
 import pytest_mock
+from mythril.disassembler.disassembly import Disassembly
 
 
 def test_concrete_call():
@@ -36,11 +40,14 @@ def test_concrete_call():
     assert issue.contract == node.contract_name
     assert issue.function == node.function_name
     assert issue.title == "Call data forwarded with delegatecall()"
-    assert issue.type == 'Informational'
+    assert issue.type == "Informational"
-    assert issue.description == "This contract forwards its call data via DELEGATECALL in its fallback function." \
+    assert (
-                                " This means that any function in the called contract can be executed." \
+        issue.description
-                                " Note that the callee contract will have access to the storage of the " \
+        == "This contract forwards its call data via DELEGATECALL in its fallback function."
-                                "calling contract.\n DELEGATECALL target: 0x1"
+        " This means that any function in the called contract can be executed."
+        " Note that the callee contract will have access to the storage of the "
+        "calling contract.\n DELEGATECALL target: 0x1"
+    )
 
 
 def test_concrete_call_symbolic_to():
@@ -70,11 +77,14 @@ def test_concrete_call_symbolic_to():
     assert issue.contract == node.contract_name
     assert issue.function == node.function_name
     assert issue.title == "Call data forwarded with delegatecall()"
-    assert issue.type == 'Informational'
+    assert issue.type == "Informational"
-    assert issue.description == "This contract forwards its call data via DELEGATECALL in its fallback function." \
+    assert (
-                                " This means that any function in the called contract can be executed." \
+        issue.description
-                                " Note that the callee contract will have access to the storage of the " \
+        == "This contract forwards its call data via DELEGATECALL in its fallback function."
-                                "calling contract.\n DELEGATECALL target: calldata_3"
+        " This means that any function in the called contract can be executed."
+        " Note that the callee contract will have access to the storage of the "
+        "calling contract.\n DELEGATECALL target: calldata_3"
+    )
 
 
 def test_concrete_call_not_calldata():
@@ -100,7 +110,6 @@ def test_symbolic_call_storage_to(mocker):
     state = GlobalState(None, environment, None)
     state.mstate.memory = ["placeholder", "calldata_bling_0"]
 
-
     node = Node("example")
     node.contract_name = "the contract name"
     node.function_name = "the function name"
@@ -108,14 +117,12 @@ def test_symbolic_call_storage_to(mocker):
     to = Variable("storage_1", VarType.SYMBOLIC)
     call = Call(node, state, None, "Type: ", to, None)
 
-
     mocker.patch.object(SymExecWrapper, "__init__", lambda x, y: None)
     statespace = SymExecWrapper(1)
 
-    mocker.patch.object(statespace, 'find_storage_write')
+    mocker.patch.object(statespace, "find_storage_write")
     statespace.find_storage_write.return_value = "Function name"
 
-
     # act
     issues = _symbolic_call(call, state, address, statespace)
 
@@ -124,11 +131,14 @@ def test_symbolic_call_storage_to(mocker):
     assert issue.address == address
     assert issue.contract == node.contract_name
     assert issue.function == node.function_name
-    assert issue.title == 'Type:  to a user-supplied address'
+    assert issue.title == "Type:  to a user-supplied address"
-    assert issue.type == 'Informational'
+    assert issue.type == "Informational"
-    assert issue.description == 'This contract delegates execution to a contract address in storage slot 1.' \
+    assert (
-                                ' This storage slot can be written to by calling the function `Function name`. ' \
+        issue.description
-                                'Be aware that the called contract gets unrestricted access to this contract\'s state.'
+        == "This contract delegates execution to a contract address in storage slot 1."
+        " This storage slot can be written to by calling the function `Function name`. "
+        "Be aware that the called contract gets unrestricted access to this contract's state."
+    )
 
 
 def test_symbolic_call_calldata_to(mocker):
@@ -141,7 +151,6 @@ def test_symbolic_call_calldata_to(mocker):
     state = GlobalState(None, environment, None)
     state.mstate.memory = ["placeholder", "calldata_bling_0"]
 
-
     node = Node("example")
     node.contract_name = "the contract name"
     node.function_name = "the function name"
@@ -149,14 +158,12 @@ def test_symbolic_call_calldata_to(mocker):
     to = Variable("calldata", VarType.SYMBOLIC)
     call = Call(node, state, None, "Type: ", to, None)
 
-
     mocker.patch.object(SymExecWrapper, "__init__", lambda x, y: None)
     statespace = SymExecWrapper(1)
 
-    mocker.patch.object(statespace, 'find_storage_write')
+    mocker.patch.object(statespace, "find_storage_write")
     statespace.find_storage_write.return_value = "Function name"
 
-
     # act
     issues = _symbolic_call(call, state, address, statespace)
 
@@ -165,31 +172,34 @@ def test_symbolic_call_calldata_to(mocker):
     assert issue.address == address
     assert issue.contract == node.contract_name
     assert issue.function == node.function_name
-    assert issue.title == 'Type:  to a user-supplied address'
+    assert issue.title == "Type:  to a user-supplied address"
-    assert issue.type == 'Informational'
+    assert issue.type == "Informational"
-    assert issue.description == 'This contract delegates execution to a contract address obtained from calldata. ' \
+    assert (
-                                'Be aware that the called contract gets unrestricted access to this contract\'s state.'
+        issue.description
-
+        == "This contract delegates execution to a contract address obtained from calldata. "
-
+        "Be aware that the called contract gets unrestricted access to this contract's state."
-@patch('mythril.laser.ethereum.state.GlobalState.get_current_instruction')
+    )
-@patch('mythril.analysis.modules.delegatecall._concrete_call')
+
-@patch('mythril.analysis.modules.delegatecall._symbolic_call')
+
+@patch("mythril.laser.ethereum.state.GlobalState.get_current_instruction")
+@patch("mythril.analysis.modules.delegatecall._concrete_call")
+@patch("mythril.analysis.modules.delegatecall._symbolic_call")
 def test_delegate_call(sym_mock, concrete_mock, curr_instruction):
     # arrange
     # sym_mock = mocker.patch.object(delegatecall, "_symbolic_call")
     # concrete_mock = mocker.patch.object(delegatecall, "_concrete_call")
     sym_mock.return_value = []
     concrete_mock.return_value = []
-    curr_instruction.return_value = {'address': '0x10'}
+    curr_instruction.return_value = {"address": "0x10"}
 
-    active_account = Account('0x10')
+    active_account = Account("0x10")
     active_account.code = Disassembly("00")
 
     environment = Environment(active_account, None, None, None, None, None)
     state = GlobalState(None, environment, Node)
     state.mstate.memory = ["placeholder", "calldata_bling_0"]
     state.mstate.stack = [1, 2, 3]
-    assert state.get_current_instruction() == {'address': '0x10'}
+    assert state.get_current_instruction() == {"address": "0x10"}
 
     node = Node("example")
     node.contract_name = "the contract name"
@@ -209,8 +219,8 @@ def test_delegate_call(sym_mock, concrete_mock, curr_instruction):
     assert sym_mock.call_count == 1
 
 
-@patch('mythril.analysis.modules.delegatecall._concrete_call')
+@patch("mythril.analysis.modules.delegatecall._concrete_call")
-@patch('mythril.analysis.modules.delegatecall._symbolic_call')
+@patch("mythril.analysis.modules.delegatecall._symbolic_call")
 def test_delegate_call_not_delegate(sym_mock, concrete_mock):
     # arrange
     # sym_mock = mocker.patch.object(delegatecall, "_symbolic_call")
@@ -236,8 +246,8 @@ def test_delegate_call_not_delegate(sym_mock, concrete_mock):
     assert sym_mock.call_count == 0
 
 
-@patch('mythril.analysis.modules.delegatecall._concrete_call')
+@patch("mythril.analysis.modules.delegatecall._concrete_call")
-@patch('mythril.analysis.modules.delegatecall._symbolic_call')
+@patch("mythril.analysis.modules.delegatecall._symbolic_call")
 def test_delegate_call_not_fallback(sym_mock, concrete_mock):
     # arrange
     # sym_mock = mocker.patch.object(delegatecall, "_symbolic_call")

tests/cmd_line_test.py

@@ -3,51 +3,61 @@ from tests import *
 
 MYTH = str(PROJECT_DIR / "myth")
 
+
 def output_of(command):
     return check_output(command, shell=True).decode("UTF-8")
 
-class CommandLineToolTestCase(BaseTestCase):
 
+class CommandLineToolTestCase(BaseTestCase):
     def test_disassemble_code_correctly(self):
         command = "python3 {} MYTH -d -c 0x5050".format(MYTH)
-        self.assertEqual('0 POP\n1 POP\n', output_of(command))
+        self.assertEqual("0 POP\n1 POP\n", output_of(command))
 
     def test_disassemble_solidity_file_correctly(self):
-        solidity_file = str(TESTDATA / 'input_contracts'/ 'metacoin.sol')
+        solidity_file = str(TESTDATA / "input_contracts" / "metacoin.sol")
         command = "python3 {} -d {}".format(MYTH, solidity_file)
-        self.assertIn('2 PUSH1 0x40\n4 MSTORE', output_of(command))
+        self.assertIn("2 PUSH1 0x40\n4 MSTORE", output_of(command))
 
     def test_hash_a_function_correctly(self):
         command = "python3 {} --hash 'setOwner(address)'".format(MYTH)
-        self.assertEqual('0x13af4035\n', output_of(command))
+        self.assertEqual("0x13af4035\n", output_of(command))
 
-class TruffleTestCase(BaseTestCase):
 
+class TruffleTestCase(BaseTestCase):
     def test_analysis_truffle_project(self):
         truffle_project_root = str(TESTS_DIR / "truffle_project")
-        command = "cd {}; truffle compile; python3 {} --truffle".format(truffle_project_root, MYTH)
+        command = "cd {}; truffle compile; python3 {} --truffle".format(
-        self.assertIn("A non-zero amount of Ether is sent to a user-supplied address. The target address is msg.sender."
+            truffle_project_root, MYTH
-                      , output_of(command))
+        )
+        self.assertIn("=== Ether send ====", output_of(command))
 
-class InfuraTestCase(BaseTestCase):
 
+class InfuraTestCase(BaseTestCase):
     def test_infura_mainnet(self):
-        command = "python3 {} --rpc infura-mainnet -d -a 0x2a0c0dbecc7e4d658f48e01e3fa353f44050c208".format(MYTH)
+        command = "python3 {} --rpc infura-mainnet -d -a 0x2a0c0dbecc7e4d658f48e01e3fa353f44050c208".format(
+            MYTH
+        )
         output = output_of(command)
         self.assertIn("0 PUSH1 0x60\n2 PUSH1 0x40\n4 MSTORE", output)
         self.assertIn("7278 POP\n7279 POP\n7280 JUMP\n7281 STOP", output)
 
     def test_infura_rinkeby(self):
-        command = "python3 {} --rpc infura-rinkeby -d -a 0xB6f2bFED892a662bBF26258ceDD443f50Fa307F5".format(MYTH)
+        command = "python3 {} --rpc infura-rinkeby -d -a 0xB6f2bFED892a662bBF26258ceDD443f50Fa307F5".format(
+            MYTH
+        )
         output = output_of(command)
         self.assertIn("34 JUMPDEST\n35 CALLVALUE", output)
 
     def test_infura_kovan(self):
-        command = "python3 {} --rpc infura-kovan -d -a 0xE6bBF9B5A3451242F82f8cd458675092617a1235".format(MYTH)
+        command = "python3 {} --rpc infura-kovan -d -a 0xE6bBF9B5A3451242F82f8cd458675092617a1235".format(
+            MYTH
+        )
         output = output_of(command)
         self.assertIn("9999 PUSH1 0x00\n10001 NOT\n10002 AND\n10003 PUSH1 0x00", output)
 
     def test_infura_ropsten(self):
-        command = "python3 {} --rpc infura-ropsten -d -a 0x6e0E0e02377Bc1d90E8a7c21f12BA385C2C35f78".format(MYTH)
+        command = "python3 {} --rpc infura-ropsten -d -a 0x6e0E0e02377Bc1d90E8a7c21f12BA385C2C35f78".format(
+            MYTH
+        )
         output = output_of(command)
         self.assertIn("1821 PUSH1 0x01\n1823 PUSH2 0x070c", output)

tests/disassembler/asm.py

@@ -1,7 +1,7 @@
 from mythril.disassembler.asm import *
 import pytest
 
-valid_names = [("PUSH1", 0x60), ("STOP", 0x0), ("RETURN", 0xf3)]
+valid_names = [("PUSH1", 0x60), ("STOP", 0x0), ("RETURN", 0xF3)]
 
 
 @pytest.mark.parametrize("operation_name, hex_value", valid_names)
@@ -22,36 +22,90 @@ def test_get_unknown_opcode():
 
 sequence_match_test_data = [
     # Normal no match
-    ((["PUSH1"], ["EQ"]), [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}], 1, False),
+    (
+        (["PUSH1"], ["EQ"]),
+        [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}],
+        1,
+        False,
+    ),
     # Normal match
-    ((["PUSH1"], ["EQ"]), [{"opcode": "PUSH1"}, {"opcode": "PUSH1"}, {"opcode": "EQ"}], 1, True),
+    (
+        (["PUSH1"], ["EQ"]),
+        [{"opcode": "PUSH1"}, {"opcode": "PUSH1"}, {"opcode": "EQ"}],
+        1,
+        True,
+    ),
     # Out of bounds pattern
-    ((["PUSH1"], ["EQ"]), [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}], 3, False),
+    (
-    ((["PUSH1"], ["EQ"]), [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}], 2, False),
+        (["PUSH1"], ["EQ"]),
+        [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}],
+        3,
+        False,
+    ),
+    (
+        (["PUSH1"], ["EQ"]),
+        [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}],
+        2,
+        False,
+    ),
     # Double option match
-    ((["PUSH1", "PUSH3"], ["EQ"]), [{"opcode": "PUSH1"}, {"opcode": "PUSH1"}, {"opcode": "EQ"}], 1, True),
+    (
-    ((["PUSH1", "PUSH3"], ["EQ"]), [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}], 1, True),
+        (["PUSH1", "PUSH3"], ["EQ"]),
+        [{"opcode": "PUSH1"}, {"opcode": "PUSH1"}, {"opcode": "EQ"}],
+        1,
+        True,
+    ),
+    (
+        (["PUSH1", "PUSH3"], ["EQ"]),
+        [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}],
+        1,
+        True,
+    ),
     # Double option no match
-    ((["PUSH1", "PUSH3"], ["EQ"]), [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}], 0, False),
+    (
+        (["PUSH1", "PUSH3"], ["EQ"]),
+        [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}],
+        0,
+        False,
+    ),
 ]
 
 
-@pytest.mark.parametrize("pattern, instruction_list, index,  expected_result", sequence_match_test_data)
+@pytest.mark.parametrize(
+    "pattern, instruction_list, index,  expected_result", sequence_match_test_data
+)
 def test_is_sequence_match(pattern, instruction_list, index, expected_result):
     # Act
     return_value = is_sequence_match(pattern, instruction_list, index)
     # Assert
     assert return_value == expected_result
 
+
 find_sequence_match_test_data = [
     # Normal no match
-    ((["PUSH1"], ["EQ"]), [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}], []),
+    (
+        (["PUSH1"], ["EQ"]),
+        [{"opcode": "PUSH1"}, {"opcode": "PUSH3"}, {"opcode": "EQ"}],
+        [],
+    ),
     # Normal match
-    ((["PUSH1"], ["EQ"]), [{"opcode": "PUSH1"}, {"opcode": "PUSH1"}, {"opcode": "EQ"}, {"opcode": "PUSH1"}, {"opcode": "EQ"}], [1, 3]),
+    (
+        (["PUSH1"], ["EQ"]),
+        [
+            {"opcode": "PUSH1"},
+            {"opcode": "PUSH1"},
+            {"opcode": "EQ"},
+            {"opcode": "PUSH1"},
+            {"opcode": "EQ"},
+        ],
+        [1, 3],
+    ),
 ]
 
 
-@pytest.mark.parametrize("pattern, instruction_list, expected_result", find_sequence_match_test_data)
+@pytest.mark.parametrize(
+    "pattern, instruction_list, expected_result", find_sequence_match_test_data
+)
 def test_find_op_code_sequence(pattern, instruction_list, expected_result):
     # Act
     return_value = list(find_op_code_sequence(pattern, instruction_list))

tests/disassembler/disassembly.py

@@ -0,0 +1,61 @@
+from mythril.disassembler.disassembly import *
+
+instruction_list = [
+    {"opcode": "PUSH4", "argument": "0x10203040"},
+    {"opcode": "EQ"},
+    {"opcode": "PUSH4", "argument": "0x40302010"},
+    {"opcode": "JUMPI"},
+]
+
+
+def test_get_function_info(mocker):
+    # Arrange
+    global instruction_list
+
+    signature_database_mock = SignatureDb()
+    mocker.patch.object(signature_database_mock, "get")
+    signature_database_mock.get.return_value = ["function_name"]
+
+    # Act
+    function_hash, entry_point, function_name = get_function_info(
+        0, instruction_list, signature_database_mock
+    )
+
+    # Assert
+    assert function_hash == "0x10203040"
+    assert entry_point == 0x40302010
+    assert function_name == "function_name"
+
+
+def test_get_function_info_multiple_names(mocker):
+    # Arrange
+    global instruction_list
+
+    signature_database_mock = SignatureDb()
+    mocker.patch.object(signature_database_mock, "get")
+    signature_database_mock.get.return_value = ["function_name", "another_name"]
+
+    # Act
+    function_hash, entry_point, function_name = get_function_info(
+        0, instruction_list, signature_database_mock
+    )
+
+    # Assert
+    assert function_name == "**ambiguous** function_name"
+
+
+def test_get_function_info_no_names(mocker):
+    # Arrange
+    global instruction_list
+
+    signature_database_mock = SignatureDb()
+    mocker.patch.object(signature_database_mock, "get")
+    signature_database_mock.get.return_value = []
+
+    # Act
+    function_hash, entry_point, function_name = get_function_info(
+        0, instruction_list, signature_database_mock
+    )
+
+    # Assert
+    assert function_name == "_function_0x10203040"

tests/ethcontract_test.py

@@ -3,33 +3,45 @@ from mythril.ether.ethcontract import ETHContract
 
 
 class ETHContractTestCase(unittest.TestCase):
-
     def setUp(self):
         self.code = "0x60606040525b603c5b60006010603e565b9050593681016040523660008237602060003683856040603f5a0204f41560545760206000f35bfe5b50565b005b73c3b2ae46792547a96b9f84405e36d0e07edcd05c5b905600a165627a7a7230582062a884f947232ada573f95940cce9c8bfb7e4e14e21df5af4e884941afb55e590029"
         self.creation_code = "0x60606040525b603c5b60006010603e565b9050593681016040523660008237602060003683856040603f5a0204f41560545760206000f35bfe5b50565b005b73c3b2ae46792547a96b9f84405e36d0e07edcd05c5b905600a165627a7a7230582062a884f947232ada573f95940cce9c8bfb7e4e14e21df5af4e884941afb55e590029"
 
-class Getinstruction_listTestCase(ETHContractTestCase):
 
+class Getinstruction_listTestCase(ETHContractTestCase):
     def runTest(self):
         contract = ETHContract(self.code, self.creation_code)
 
         disassembly = contract.disassembly
 
-        self.assertEqual(len(disassembly.instruction_list), 53, 'Error disassembling code using ETHContract.get_instruction_list()')
+        self.assertEqual(
+            len(disassembly.instruction_list),
+            53,
+            "Error disassembling code using ETHContract.get_instruction_list()",
+        )
 
-class GetEASMTestCase(ETHContractTestCase):
 
+class GetEASMTestCase(ETHContractTestCase):
     def runTest(self):
         contract = ETHContract(self.code)
 
         instruction_list = contract.get_easm()
 
-        self.assertTrue("PUSH1 0x60" in instruction_list, 'Error obtaining EASM code through ETHContract.get_easm()')
+        self.assertTrue(
+            "PUSH1 0x60" in instruction_list,
+            "Error obtaining EASM code through ETHContract.get_easm()",
+        )
 
-class MatchesExpressionTestCase(ETHContractTestCase):
 
+class MatchesExpressionTestCase(ETHContractTestCase):
     def runTest(self):
         contract = ETHContract(self.code)
 
-        self.assertTrue(contract.matches_expression("code#PUSH1# or code#PUSH1#"), 'Unexpected result in expression matching')
+        self.assertTrue(
-        self.assertFalse(contract.matches_expression("func#abcdef#"), 'Unexpected result in expression matching')
+            contract.matches_expression("code#PUSH1# or code#PUSH1#"),
+            "Unexpected result in expression matching",
+        )
+        self.assertFalse(
+            contract.matches_expression("func#abcdef#"),
+            "Unexpected result in expression matching",
+        )

tests/graph_test.py

@@ -5,23 +5,31 @@ from mythril.ether.soliditycontract import ETHContract
 from tests import *
 import re
 
-class GraphTest(BaseTestCase):
 
+class GraphTest(BaseTestCase):
     def test_generate_graph(self):
 
         for input_file in TESTDATA_INPUTS.iterdir():
-            output_expected = TESTDATA_OUTPUTS_EXPECTED / (input_file.name + ".graph.html")
+            output_expected = TESTDATA_OUTPUTS_EXPECTED / (
-            output_current = TESTDATA_OUTPUTS_CURRENT / (input_file.name + ".graph.html")
+                input_file.name + ".graph.html"
+            )
+            output_current = TESTDATA_OUTPUTS_CURRENT / (
+                input_file.name + ".graph.html"
+            )
 
             contract = ETHContract(input_file.read_text())
 
-            sym = SymExecWrapper(contract, address=(util.get_indexed_address(0)), strategy="dfs")
+            sym = SymExecWrapper(
+                contract, address=(util.get_indexed_address(0)), strategy="dfs"
+            )
 
             html = generate_graph(sym)
             output_current.write_text(html)
 
-            lines_expected = re.findall(r"'label': '.*'", str(output_current.read_text()))
+            lines_expected = re.findall(
-            lines_found    = re.findall(r"'label': '.*'", str(output_current.read_text()))
+                r"'label': '.*'", str(output_current.read_text())
+            )
+            lines_found = re.findall(r"'label': '.*'", str(output_current.read_text()))
             if not (lines_expected == lines_found):
                 self.found_changed_files(input_file, output_expected, output_current)
 

tests/instructions/codecopy_test.py

@@ -5,7 +5,7 @@ from mythril.laser.ethereum.instructions import Instruction
 
 def test_codecopy_concrete():
     # Arrange
-    active_account = Account("0x0", code= Disassembly("60606040"))
+    active_account = Account("0x0", code=Disassembly("60606040"))
     environment = Environment(active_account, None, None, None, None, None)
     og_state = GlobalState(None, environment, None, MachineState(gas=10000000))
 

tests/laser/evm_testsuite/evm_test.py

@@ -3,16 +3,21 @@ from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.state import Account
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.transaction.concolic import execute_message_call
+from mythril.analysis.solver import get_model
 from datetime import datetime
-from mythril.laser.ethereum.util import get_concrete_int
 import binascii
 import json
 from pathlib import Path
 import pytest
 
-evm_test_dir = Path(__file__).parent / 'VMTests'
+evm_test_dir = Path(__file__).parent / "VMTests"
 
-test_types = ['vmArithmeticTest', 'vmBitwiseLogicOperation', 'vmPushDupSwapTest', 'vmTests', 'vmSha3Test']
+test_types = [
+    "vmArithmeticTest",
+    "vmBitwiseLogicOperation",
+    "vmPushDupSwapTest",
+    "vmTests",
+]
 
 
 def load_test_data(designations):
@@ -24,27 +29,33 @@ def load_test_data(designations):
                 top_level = json.load(file)
 
                 for test_name, data in top_level.items():
-                    pre_condition = data['pre']
+                    pre_condition = data["pre"]
 
-                    action = data['exec']
+                    action = data["exec"]
 
-                    post_condition = data.get('post', {})
+                    post_condition = data.get("post", {})
 
-                    return_data.append((test_name, pre_condition, action, post_condition))
+                    return_data.append(
+                        (test_name, pre_condition, action, post_condition)
+                    )
 
     return return_data
 
 
-@pytest.mark.parametrize("test_name, pre_condition, action, post_condition", load_test_data(test_types))
+@pytest.mark.parametrize(
-def test_vmtest(test_name: str, pre_condition: dict, action: dict, post_condition: dict) -> None:
+    "test_name, pre_condition, action, post_condition", load_test_data(test_types)
+)
+def test_vmtest(
+    test_name: str, pre_condition: dict, action: dict, post_condition: dict
+) -> None:
     # Arrange
 
     accounts = {}
     for address, details in pre_condition.items():
         account = Account(address)
-        account.code = Disassembly(details['code'][2:])
+        account.code = Disassembly(details["code"][2:])
-        account.balance = int(details['balance'], 16)
+        account.balance = int(details["balance"], 16)
-        account.nonce = int(details['nonce'], 16)
+        account.nonce = int(details["nonce"], 16)
 
         accounts[address] = account
 
@@ -59,14 +70,14 @@ def test_vmtest(test_name: str, pre_condition: dict, action: dict, post_conditio
 
     execute_message_call(
         laser_evm,
-        callee_address=action['address'],
+        callee_address=action["address"],
-        caller_address=action['caller'],
+        caller_address=action["caller"],
-        origin_address=action['origin'],
+        origin_address=action["origin"],
-        code=action['code'][2:],
+        code=action["code"][2:],
-        gas=action['gas'],
+        gas=action["gas"],
-        data=binascii.a2b_hex(action['data'][2:]),
+        data=binascii.a2b_hex(action["data"][2:]),
-        gas_price=int(action['gasPrice'], 16),
+        gas_price=int(action["gasPrice"], 16),
-        value=int(action['value'], 16)
+        value=int(action["value"], 16),
     )
 
     # Assert
@@ -74,14 +85,19 @@ def test_vmtest(test_name: str, pre_condition: dict, action: dict, post_conditio
     assert len(laser_evm.open_states) == 1
 
     world_state = laser_evm.open_states[0]
+    model = get_model(next(iter(laser_evm.nodes.values())).states[0].mstate.constraints)
 
     for address, details in post_condition.items():
         account = world_state[address]
 
-        assert account.nonce == int(details['nonce'], 16)
+        assert account.nonce == int(details["nonce"], 16)
-        assert account.code.bytecode == details['code'][2:]
+        assert account.code.bytecode == details["code"][2:]
 
-        for index, value in details['storage'].items():
+        for index, value in details["storage"].items():
             expected = int(value, 16)
-            actual = get_concrete_int(account.storage[int(index, 16)])
+            if type(account.storage[int(index, 16)]) != int:
+                actual = model.eval(account.storage[int(index, 16)])
+                actual = 1 if actual == True else 0 if actual == False else actual
+            else:
+                actual = account.storage[int(index, 16)]
             assert actual == expected

tests/laser/state/calldata_test.py

@@ -0,0 +1,102 @@
+import pytest
+from mythril.laser.ethereum.state import Calldata
+from z3 import Solver, simplify
+from z3.z3types import Z3Exception
+
+
+uninitialized_test_data = [
+    ([]),  # Empty concrete calldata
+    ([1, 4, 5, 3, 4, 72, 230, 53]),  # Concrete calldata
+]
+
+
+@pytest.mark.parametrize("starting_calldata", uninitialized_test_data)
+def test_concrete_calldata_uninitialized_index(starting_calldata):
+    # Arrange
+    calldata = Calldata(0, starting_calldata)
+    solver = Solver()
+
+    # Act
+    value = calldata[100]
+    value2 = calldata.get_word_at(200)
+
+    solver.add(calldata.constraints)
+    solver.check()
+    model = solver.model()
+
+    value = model.eval(value)
+    value2 = model.eval(value2)
+
+    # Assert
+    assert value == 0
+    assert value2 == 0
+
+
+def test_concrete_calldata_calldatasize():
+    # Arrange
+    calldata = Calldata(0, [1, 4, 7, 3, 7, 2, 9])
+    solver = Solver()
+
+    # Act
+    solver.add(calldata.constraints)
+    solver.check()
+    model = solver.model()
+
+    result = model.eval(calldata.calldatasize)
+
+    # Assert
+    assert result == 7
+
+
+def test_symbolic_calldata_constrain_index():
+    # Arrange
+    calldata = Calldata(0)
+    solver = Solver()
+
+    # Act
+    constraint = calldata[100] == 50
+
+    value = calldata[100]
+
+    solver.add(calldata.constraints + [constraint])
+    solver.check()
+    model = solver.model()
+
+    value = model.eval(value)
+    calldatasize = model.eval(calldata.calldatasize)
+
+    # Assert
+    assert value == 50
+    assert simplify(calldatasize >= 100)
+
+
+def test_concrete_calldata_constrain_index():
+    # Arrange
+    calldata = Calldata(0, [1, 4, 7, 3, 7, 2, 9])
+    solver = Solver()
+
+    # Act
+    constraint = calldata[2] == 3
+
+    solver.add(calldata.constraints + [constraint])
+    result = solver.check()
+
+    # Assert
+    assert str(result) == "unsat"
+
+
+def test_concrete_calldata_constrain_index():
+    # Arrange
+    calldata = Calldata(0)
+    solver = Solver()
+
+    # Act
+    constraints = []
+    constraints.append(calldata[51] == 1)
+    constraints.append(calldata.calldatasize == 50)
+
+    solver.add(calldata.constraints + constraints)
+    result = solver.check()
+
+    # Assert
+    assert str(result) == "unsat"

tests/laser/state/mstack_test.py

@@ -6,11 +6,10 @@ from tests import BaseTestCase
 
 
 class MachineStackTest(BaseTestCase):
-
     @staticmethod
     def test_mstack_constructor():
         mstack = MachineStack([1, 2])
-        assert(mstack == [1, 2])
+        assert mstack == [1, 2]
 
     @staticmethod
     def test_mstack_append_single_element():
@@ -18,7 +17,7 @@ class MachineStackTest(BaseTestCase):
 
         mstack.append(0)
 
-        assert(mstack == [0])
+        assert mstack == [0]
 
     @staticmethod
     def test_mstack_append_multiple_elements():
@@ -53,4 +52,3 @@ class MachineStackTest(BaseTestCase):
 
         with pytest.raises(NotImplementedError):
             mstack += mstack
-

tests/laser/state/mstate_test.py

@@ -2,14 +2,12 @@ import pytest
 from mythril.laser.ethereum.state import MachineState
 from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
 
-memory_extension_test_data = [
+memory_extension_test_data = [(0, 0, 10), (0, 30, 10), (100, 22, 8)]
-    (0, 0, 10),
-    (0, 30, 10),
-    (100, 22, 8)
-]
 
 
-@pytest.mark.parametrize("initial_size,start,extension_size", memory_extension_test_data)
+@pytest.mark.parametrize(
+    "initial_size,start,extension_size", memory_extension_test_data
+)
 def test_memory_extension(initial_size, start, extension_size):
     # Arrange
     machine_state = MachineState(0)
@@ -23,12 +21,7 @@ def test_memory_extension(initial_size, start, extension_size):
     assert machine_state.memory_size == max(initial_size, start + extension_size)
 
 
-stack_pop_too_many_test_data = [
+stack_pop_too_many_test_data = [(0, 1), (0, 2), (5, 1), (5, 10)]
-    (0, 1),
-    (0, 2),
-    (5, 1),
-    (5, 10)
-]
 
 
 @pytest.mark.parametrize("initial_size,overflow", stack_pop_too_many_test_data)
@@ -44,7 +37,7 @@ def test_stack_pop_too_many(initial_size, overflow):
 
 stack_pop_test_data = [
     ([1, 2, 3], 2, [3, 2]),
-    ([1, 3, 4, 7, 7, 1, 2], 5, [2, 1, 7, 7, 4])
+    ([1, 3, 4, 7, 7, 1, 2], 5, [2, 1, 7, 7, 4]),
 ]
 
 
@@ -79,7 +72,7 @@ def test_stack_multiple_pop_():
 def test_stack_single_pop():
     # Arrange
     machine_state = MachineState(0)
-    machine_state.stack = [1,2,3]
+    machine_state.stack = [1, 2, 3]
 
     # Act
     result = machine_state.pop()
@@ -88,22 +81,18 @@ def test_stack_single_pop():
     assert isinstance(result, int)
 
 
-memory_write_test_data = [
+memory_write_test_data = [(5, 10, [1, 2, 3]), (0, 0, [3, 4]), (20, 1, [2, 4, 10])]
-    (5, 10, [1, 2, 3]),
-    (0, 0, [3, 4]),
-    (20, 1, [2, 4, 10])
-]
 
 
 @pytest.mark.parametrize("initial_size, memory_offset, data", memory_write_test_data)
 def test_memory_write(initial_size, memory_offset, data):
     # Arrange
     machine_state = MachineState(0)
-    machine_state.memory = [0]*initial_size
+    machine_state.memory = [0] * initial_size
 
     # Act
     machine_state.memory_write(memory_offset, data)
 
     # Assert
-    assert len(machine_state.memory) == max(initial_size, memory_offset+len(data))
+    assert len(machine_state.memory) == max(initial_size, memory_offset + len(data))
-    assert machine_state.memory[memory_offset:memory_offset+len(data)] == data
+    assert machine_state.memory[memory_offset : memory_offset + len(data)] == data

tests/laser/state/storage_test.py

@@ -2,11 +2,7 @@ import pytest
 from mythril.laser.ethereum.state import Storage
 from z3 import ExprRef
 
-storage_uninitialized_test_data = [
+storage_uninitialized_test_data = [({}, 1), ({1: 5}, 2), ({1: 5, 3: 10}, 2)]
-    ({}, 1),
-    ({1: 5}, 2),
-    ({1: 5, 3: 10}, 2)
-]
 
 
 @pytest.mark.parametrize("initial_storage,key", storage_uninitialized_test_data)

tests/laser/test_transaction.py

@@ -8,19 +8,20 @@ def test_intercontract_call():
     # Arrange
     cfg.gbl_next_uid = 0
 
-    caller_code = Disassembly("6080604052348015600f57600080fd5b5073deadbeefdeadbeefdeadbeefdeadbeefdeadbeef73ffffffffffffffffffffffffffffffffffffffff166389627e13336040518263ffffffff167c0100000000000000000000000000000000000000000000000000000000028152600401808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001915050602060405180830381600087803b15801560be57600080fd5b505af115801560d1573d6000803e3d6000fd5b505050506040513d602081101560e657600080fd5b8101908080519060200190929190505050500000a165627a7a72305820fdb1e90f0d9775c94820e516970e0d41380a94624fa963c556145e8fb645d4c90029")
+    caller_code = Disassembly(
+        "6080604052348015600f57600080fd5b5073deadbeefdeadbeefdeadbeefdeadbeefdeadbeef73ffffffffffffffffffffffffffffffffffffffff166389627e13336040518263ffffffff167c0100000000000000000000000000000000000000000000000000000000028152600401808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001915050602060405180830381600087803b15801560be57600080fd5b505af115801560d1573d6000803e3d6000fd5b505050506040513d602081101560e657600080fd5b8101908080519060200190929190505050500000a165627a7a72305820fdb1e90f0d9775c94820e516970e0d41380a94624fa963c556145e8fb645d4c90029"
+    )
     caller_address = "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe"
 
-    callee_code = Disassembly("608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806389627e13146044575b600080fd5b348015604f57600080fd5b506082600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506084565b005b8073ffffffffffffffffffffffffffffffffffffffff166108fc3073ffffffffffffffffffffffffffffffffffffffff16319081150290604051600060405180830381858888f1935050505015801560e0573d6000803e3d6000fd5b50505600a165627a7a72305820a6b1335d6f994632bc9a7092d0eaa425de3dea05e015af8a94ad70b3969e117a0029")
+    callee_code = Disassembly(
+        "608060405260043610603f576000357c0100000000000000000000000000000000000000000000000000000000900463ffffffff16806389627e13146044575b600080fd5b348015604f57600080fd5b506082600480360381019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506084565b005b8073ffffffffffffffffffffffffffffffffffffffff166108fc3073ffffffffffffffffffffffffffffffffffffffff16319081150290604051600060405180830381858888f1935050505015801560e0573d6000803e3d6000fd5b50505600a165627a7a72305820a6b1335d6f994632bc9a7092d0eaa425de3dea05e015af8a94ad70b3969e117a0029"
+    )
     callee_address = "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
 
     caller_account = Account(caller_address, caller_code, contract_name="Caller")
     callee_account = Account(callee_address, callee_code, contract_name="Callee")
 
-    accounts = {
+    accounts = {caller_address: caller_account, callee_address: callee_account}
-        caller_address: caller_account,
-        callee_address: callee_account
-    }
 
     laser = svm.LaserEVM(accounts)
 
@@ -30,11 +31,11 @@ def test_intercontract_call():
     # Assert
     # Initial node starts in contract caller
     assert len(laser.nodes.keys()) > 0
-    assert laser.nodes[0].contract_name == 'Caller'
+    assert laser.nodes[0].contract_name == "Caller"
 
     # At one point we call into contract callee
     for node in laser.nodes.values():
-        if node.contract_name == 'Callee':
+        if node.contract_name == "Callee":
             assert len(node.states[0].transaction_stack) > 1
             return
 

tests/laser/transaction/create_transaction_test.py

@@ -10,7 +10,7 @@ from mythril.analysis.symbolic import SymExecWrapper
 
 
 def test_create():
-    contract = SolidityContract(str(tests.TESTDATA_INPUTS_CONTRACTS / 'calls.sol'))
+    contract = SolidityContract(str(tests.TESTDATA_INPUTS_CONTRACTS / "calls.sol"))
 
     laser_evm = svm.LaserEVM({})
 
@@ -27,12 +27,15 @@ def test_create():
             found_instruction = created_account_code.instruction_list[i]
             actual_instruction = actual_code.instruction_list[i]
 
-            assert found_instruction['opcode'] == actual_instruction['opcode']
+            assert found_instruction["opcode"] == actual_instruction["opcode"]
+
 
 def test_sym_exec():
-    contract = SolidityContract(str(tests.TESTDATA_INPUTS_CONTRACTS / 'calls.sol'))
+    contract = SolidityContract(str(tests.TESTDATA_INPUTS_CONTRACTS / "calls.sol"))
 
-    sym = SymExecWrapper(contract, address=(util.get_indexed_address(0)), strategy="dfs")
+    sym = SymExecWrapper(
+        contract, address=(util.get_indexed_address(0)), strategy="dfs"
+    )
     issues = fire_lasers(sym)
 
     assert len(issues) != 0

tests/laser/transaction/symbolic_test.py

@@ -1,9 +1,18 @@
-from mythril.laser.ethereum.transaction.symbolic import execute_message_call, execute_contract_creation
+from mythril.laser.ethereum.transaction.symbolic import (
-from mythril.laser.ethereum.transaction import MessageCallTransaction, ContractCreationTransaction
+    execute_message_call,
+    execute_contract_creation,
+)
+from mythril.laser.ethereum.transaction import (
+    MessageCallTransaction,
+    ContractCreationTransaction,
+)
 from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.state import WorldState, Account
 import unittest.mock as mock
 from unittest.mock import MagicMock
+from mythril.laser.ethereum.transaction.symbolic import (
+    _setup_global_state_for_execution,
+)
 
 
 def _is_message_call(_, transaction):
@@ -14,7 +23,9 @@ def _is_contract_creation(_, transaction):
     assert isinstance(transaction, ContractCreationTransaction)
 
 
-@mock.patch("mythril.laser.ethereum.transaction.symbolic._setup_global_state_for_execution")
+@mock.patch(
+    "mythril.laser.ethereum.transaction.symbolic._setup_global_state_for_execution"
+)
 def test_execute_message_call(mocked_setup: MagicMock):
     # Arrange
     laser_evm = LaserEVM({})
@@ -39,7 +50,9 @@ def test_execute_message_call(mocked_setup: MagicMock):
     assert len(laser_evm.open_states) == 0
 
 
-@mock.patch("mythril.laser.ethereum.transaction.symbolic._setup_global_state_for_execution")
+@mock.patch(
+    "mythril.laser.ethereum.transaction.symbolic._setup_global_state_for_execution"
+)
 def test_execute_contract_creation(mocked_setup: MagicMock):
     # Arrange
     laser_evm = LaserEVM({})
@@ -58,3 +71,24 @@ def test_execute_contract_creation(mocked_setup: MagicMock):
     assert laser_evm.exec.call_count == 1
     assert len(laser_evm.open_states) == 0
 
+
+def test_calldata_constraints_in_transaction():
+    # Arrange
+    laser_evm = LaserEVM({})
+    world_state = WorldState()
+
+    correct_constraints = [MagicMock(), MagicMock(), MagicMock()]
+
+    transaction = MessageCallTransaction(
+        world_state, Account("ca11ee"), Account("ca114")
+    )
+    transaction.call_data = MagicMock()
+    transaction.call_data.constraints = correct_constraints
+
+    # Act
+    _setup_global_state_for_execution(laser_evm, transaction)
+
+    # Assert
+    state = laser_evm.work_list[0]
+    for constraint in correct_constraints:
+        assert constraint in state.environment.calldata.constraints

tests/native_test.py

@@ -14,7 +14,10 @@ ECRECOVER_TEST = [(0, False) for _ in range(9)]
 
 IDENTITY_TEST = [(0, False) for _ in range(4)]
 
-SHA256_TEST[0] = (5555555555555555, True)     #These are Random numbers to check whether the 'if condition' is entered or not(True means entered)
+SHA256_TEST[0] = (
+    5555555555555555,
+    True,
+)  # These are Random numbers to check whether the 'if condition' is entered or not(True means entered)
 SHA256_TEST[1] = (323232325445454546, True)
 SHA256_TEST[2] = (34756834765834658, False)
 SHA256_TEST[3] = (8756476956956795876987, True)
@@ -45,12 +48,13 @@ IDENTITY_TEST[1] = (476934798798347, False)
 IDENTITY_TEST[2] = (7346948379483769, True)
 IDENTITY_TEST[3] = (83269476937987, False)
 
+
 def _all_info(laser):
     accounts = {}
     for address, _account in laser.world_state.accounts.items():
         account = _account.as_dict
         account["code"] = account["code"].instruction_list
-        account['balance'] = str(account['balance'])
+        account["balance"] = str(account["balance"])
         accounts[address] = account
 
     nodes = {}
@@ -62,56 +66,58 @@ def _all_info(laser):
             elif isinstance(state, GlobalState):
                 environment = state.environment.as_dict
                 environment["active_account"] = environment["active_account"].address
-                states.append({
+                states.append(
-                    'accounts': state.accounts.keys(),
+                    {
-                    'environment': environment,
+                        "accounts": state.accounts.keys(),
-                    'mstate': state.mstate.as_dict
+                        "environment": environment,
-                })
+                        "mstate": state.mstate.as_dict,
+                    }
+                )
 
         nodes[uid] = {
-            'uid': node.uid,
+            "uid": node.uid,
-            'contract_name': node.contract_name,
+            "contract_name": node.contract_name,
-            'start_addr': node.start_addr,
+            "start_addr": node.start_addr,
-            'states': states,
+            "states": states,
-            'constraints': node.constraints,
+            "constraints": node.constraints,
-            'function_name': node.function_name,
+            "function_name": node.function_name,
-            'flags': str(node.flags)
+            "flags": str(node.flags),
         }
 
     edges = [edge.as_dict for edge in laser.edges]
 
     return {
-        'accounts': accounts,
+        "accounts": accounts,
-        'nodes': nodes,
+        "nodes": nodes,
-        'edges': edges,
+        "edges": edges,
-        'total_states': laser.total_states,
+        "total_states": laser.total_states,
-        'max_depth': laser.max_depth
+        "max_depth": laser.max_depth,
     }
 
+
 def _test_natives(laser_info, test_list, test_name):
     success = 0
     for i, j in test_list:
         if (str(i) in laser_info) == j:
             success += 1
         else:
-            print("Failed: "+str(i)+" "+str(j))
+            print("Failed: " + str(i) + " " + str(j))
-    assert(success == len(test_list))
+    assert success == len(test_list)
 
 
 class NativeTests(BaseTestCase):
     @staticmethod
     def runTest():
-        disassembly = SolidityContract('./tests/native_tests.sol').disassembly
+        disassembly = SolidityContract("./tests/native_tests.sol").disassembly
         account = Account("0x0000000000000000000000000000000000000000", disassembly)
         accounts = {account.address: account}
 
-        laser = svm.LaserEVM(accounts, max_depth = 100)
+        laser = svm.LaserEVM(accounts, max_depth=100)
         laser.sym_exec(account.address)
         laser_info = str(_all_info(laser))
-        print('\n')
+        print("\n")
-
-        _test_natives(laser_info, SHA256_TEST, 'SHA256')
-        _test_natives(laser_info, RIPEMD160_TEST, 'RIPEMD160')
-        _test_natives(laser_info, ECRECOVER_TEST, 'ECRECOVER')
-        _test_natives(laser_info, IDENTITY_TEST, 'IDENTITY')
 
+        _test_natives(laser_info, SHA256_TEST, "SHA256")
+        _test_natives(laser_info, RIPEMD160_TEST, "RIPEMD160")
+        _test_natives(laser_info, ECRECOVER_TEST, "ECRECOVER")
+        _test_natives(laser_info, IDENTITY_TEST, "IDENTITY")

tests/report_test.py

@@ -24,7 +24,12 @@ def _fix_debug_data(json_str):
 
 def _generate_report(input_file):
     contract = ETHContract(input_file.read_text(), enable_online_lookup=False)
-    sym = SymExecWrapper(contract, address=(util.get_indexed_address(0)), strategy="dfs", execution_timeout=30)
+    sym = SymExecWrapper(
+        contract,
+        address=(util.get_indexed_address(0)),
+        strategy="dfs",
+        execution_timeout=30,
+    )
     issues = fire_lasers(sym)
 
     report = Report()
@@ -34,11 +39,13 @@ def _generate_report(input_file):
     return report, input_file
 
 
-@pytest.fixture(scope='module')
+@pytest.fixture(scope="module")
 def reports():
     """ Fixture that analyses all reports"""
     pool = Pool(cpu_count())
-    input_files = sorted([f for f in TESTDATA_INPUTS.iterdir()])
+    input_files = sorted(
+        [f for f in TESTDATA_INPUTS.iterdir() if f.name != "environments.sol.o"]
+    )
     results = pool.map(_generate_report, input_files)
 
     return results
@@ -48,14 +55,25 @@ def _assert_empty(changed_files, postfix):
     """ Asserts there are no changed files and otherwise builds error message"""
     message = ""
     for input_file in changed_files:
-        output_expected = (TESTDATA_OUTPUTS_EXPECTED / (input_file.name + postfix)).read_text().splitlines(1)
+        output_expected = (
-        output_current = (TESTDATA_OUTPUTS_CURRENT / (input_file.name + postfix)).read_text().splitlines(1)
+            (TESTDATA_OUTPUTS_EXPECTED / (input_file.name + postfix))
-
+            .read_text()
-        difference = ''.join(difflib.unified_diff(output_expected, output_current))
+            .splitlines(1)
-        message += "Found differing file for input: {} \n Difference: \n {} \n".format(str(input_file), str(difference))
+        )
+        output_current = (
+            (TESTDATA_OUTPUTS_CURRENT / (input_file.name + postfix))
+            .read_text()
+            .splitlines(1)
+        )
+
+        difference = "".join(difflib.unified_diff(output_expected, output_current))
+        message += "Found differing file for input: {} \n Difference: \n {} \n".format(
+            str(input_file), str(difference)
+        )
 
     assert message == "", message
 
+
 def _assert_empty_json(changed_files):
     """ Asserts there are no changed files and otherwise builds error message"""
     postfix = ".json"
@@ -71,15 +89,20 @@ def _assert_empty_json(changed_files):
             return obj
 
     for input_file in changed_files:
-        output_expected = json.loads((TESTDATA_OUTPUTS_EXPECTED / (input_file.name + postfix)).read_text())
+        output_expected = json.loads(
-        output_current = json.loads((TESTDATA_OUTPUTS_CURRENT / (input_file.name + postfix)).read_text())
+            (TESTDATA_OUTPUTS_EXPECTED / (input_file.name + postfix)).read_text()
-
+        )
-        if not ordered(output_expected.items()) == ordered(output_current.items()): 
+        output_current = json.loads(
+            (TESTDATA_OUTPUTS_CURRENT / (input_file.name + postfix)).read_text()
+        )
+
+        if not ordered(output_expected.items()) == ordered(output_current.items()):
             expected.append(output_expected)
             actual.append(output_current)
 
     assert expected == actual
 
+
 def _get_changed_files(postfix, report_builder, reports):
     """
     Returns a generator for all unexpected changes in generated reports
@@ -99,6 +122,7 @@ def _get_changed_files(postfix, report_builder, reports):
 
 def _get_changed_files_json(report_builder, reports):
     postfix = ".json"
+
     def ordered(obj):
         if isinstance(obj, dict):
             return sorted((k, ordered(v)) for k, v in obj.items())
@@ -112,17 +136,33 @@ def _get_changed_files_json(report_builder, reports):
         output_current = TESTDATA_OUTPUTS_CURRENT / (input_file.name + postfix)
         output_current.write_text(report_builder(report))
 
-        if not ordered(json.loads(output_expected.read_text())) == ordered(json.loads(output_current.read_text())):
+        if not ordered(json.loads(output_expected.read_text())) == ordered(
+            json.loads(output_current.read_text())
+        ):
             yield input_file
 
 
 def test_json_report(reports):
-    _assert_empty_json(_get_changed_files_json(lambda report: _fix_path(_fix_debug_data(report.as_json())).strip(), reports))
+    _assert_empty_json(
+        _get_changed_files_json(
+            lambda report: _fix_path(_fix_debug_data(report.as_json())).strip(), reports
+        )
+    )
 
 
 def test_markdown_report(reports):
-    _assert_empty(_get_changed_files('.markdown', lambda report: _fix_path(report.as_markdown()), reports), '.markdown')
+    _assert_empty(
+        _get_changed_files(
+            ".markdown", lambda report: _fix_path(report.as_markdown()), reports
+        ),
+        ".markdown",
+    )
 
 
 def test_text_report(reports):
-    _assert_empty(_get_changed_files('.text', lambda report: _fix_path(report.as_text()), reports), '.text')
+    _assert_empty(
+        _get_changed_files(
+            ".text", lambda report: _fix_path(report.as_text()), reports
+        ),
+        ".text",
+    )

tests/rpc_test.py

@@ -2,6 +2,7 @@ from unittest import TestCase
 
 from mythril.ethereum.interface.rpc.client import EthJsonRpc
 
+
 class RpcTest(TestCase):
     client = None
 
@@ -18,26 +19,49 @@ class RpcTest(TestCase):
 
     def test_eth_blockNumber(self):
         block_number = self.client.eth_blockNumber()
-        self.assertGreater(block_number, 0, "we have made sure the blockNumber is > 0 for testing")
+        self.assertGreater(
+            block_number, 0, "we have made sure the blockNumber is > 0 for testing"
+        )
 
     def test_eth_getBalance(self):
-        balance = self.client.eth_getBalance(address="0x0000000000000000000000000000000000000000")
+        balance = self.client.eth_getBalance(
-        self.assertGreater(balance, 10000000, "specified address should have a lot of balance")
+            address="0x0000000000000000000000000000000000000000"
+        )
+        self.assertGreater(
+            balance, 10000000, "specified address should have a lot of balance"
+        )
 
     def test_eth_getStorageAt(self):
-        storage = self.client.eth_getStorageAt(address="0x0000000000000000000000000000000000000000")
+        storage = self.client.eth_getStorageAt(
-        self.assertEqual(storage, '0x0000000000000000000000000000000000000000000000000000000000000000')
+            address="0x0000000000000000000000000000000000000000"
+        )
+        self.assertEqual(
+            storage,
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        )
 
     def test_eth_getBlockByNumber(self):
         block = self.client.eth_getBlockByNumber(0)
-        self.assertEqual(block["extraData"], "0x11bbe8db4e347b4e8c937c1c8370e4b5ed33adb3db69cbdb7a38e1e50b1b82fa", "the data of the first block should be right")
+        self.assertEqual(
+            block["extraData"],
+            "0x11bbe8db4e347b4e8c937c1c8370e4b5ed33adb3db69cbdb7a38e1e50b1b82fa",
+            "the data of the first block should be right",
+        )
 
     def test_eth_getCode(self):
         # TODO: can't find a proper address for getting code
-        code = self.client.eth_getCode(address="0x0000000000000000000000000000000000000001")
+        code = self.client.eth_getCode(
+            address="0x0000000000000000000000000000000000000001"
+        )
         self.assertEqual(code, "0x")
 
     def test_eth_getTransactionReceipt(self):
-        transaction = self.client.eth_getTransactionReceipt(tx_hash="0xe363505adc6b2996111f8bd774f8653a61d244cc6567b5372c2e781c6c63b737")
+        transaction = self.client.eth_getTransactionReceipt(
-        self.assertEqual(transaction["from"], "0x22f2dcff5ad78c3eb6850b5cb951127b659522e6")
+            tx_hash="0xe363505adc6b2996111f8bd774f8653a61d244cc6567b5372c2e781c6c63b737"
-        self.assertEqual(transaction["to"], "0x0000000000000000000000000000000000000000")
+        )
+        self.assertEqual(
+            transaction["from"], "0x22f2dcff5ad78c3eb6850b5cb951127b659522e6"
+        )
+        self.assertEqual(
+            transaction["to"], "0x0000000000000000000000000000000000000000"
+        )

tests/solidity_contract_test.py

@@ -5,8 +5,8 @@ from tests import BaseTestCase
 
 TEST_FILES = Path(__file__).parent / "testdata/input_contracts"
 
-class SolidityContractTest(BaseTestCase):
 
+class SolidityContractTest(BaseTestCase):
     def test_get_source_info_without_name_gets_latest_contract_info(self):
         input_file = TEST_FILES / "multi_contracts.sol"
         contract = SolidityContract(str(input_file))
@@ -36,4 +36,3 @@ class SolidityContractTest(BaseTestCase):
         self.assertEqual(code_info.filename, str(input_file))
         self.assertEqual(code_info.lineno, 6)
         self.assertEqual(code_info.code, "assert(var1>0)")
-

tests/svm_test.py

@@ -21,7 +21,7 @@ def _all_info(laser):
     for address, _account in laser.world_state.accounts.items():
         account = _account.as_dict
         account["code"] = account["code"].instruction_list
-        account['balance'] = str(account['balance'])
+        account["balance"] = str(account["balance"])
         accounts[address] = account
 
     nodes = {}
@@ -33,45 +33,50 @@ def _all_info(laser):
             elif isinstance(state, GlobalState):
                 environment = state.environment.as_dict
                 environment["active_account"] = environment["active_account"].address
-                states.append({
+                states.append(
-                    'accounts': state.accounts.keys(),
+                    {
-                    'environment': environment,
+                        "accounts": state.accounts.keys(),
-                    'mstate': state.mstate.as_dict
+                        "environment": environment,
-                })
+                        "mstate": state.mstate.as_dict,
+                    }
+                )
 
         nodes[uid] = {
-            'uid': node.uid,
+            "uid": node.uid,
-            'contract_name': node.contract_name,
+            "contract_name": node.contract_name,
-            'start_addr': node.start_addr,
+            "start_addr": node.start_addr,
-            'states': states,
+            "states": states,
-            'constraints': node.constraints,
+            "constraints": node.constraints,
-            'function_name': node.function_name,
+            "function_name": node.function_name,
-            'flags': str(node.flags)
+            "flags": str(node.flags),
         }
 
     edges = [edge.as_dict for edge in laser.edges]
 
     return {
-        'accounts': accounts,
+        "accounts": accounts,
-        'nodes': nodes,
+        "nodes": nodes,
-        'edges': edges,
+        "edges": edges,
-        'total_states': laser.total_states,
+        "total_states": laser.total_states,
-        'max_depth': laser.max_depth
+        "max_depth": laser.max_depth,
     }
 
 
 class SVMTestCase(BaseTestCase):
-
     def setUp(self):
         super(SVMTestCase, self).setUp()
         svm.gbl_next_uid = 0
 
     def test_laser_result(self):
         for input_file in TESTDATA_INPUTS_CONTRACTS.iterdir():
-            if input_file.name == "weak_random.sol":
+            if input_file.name in ["weak_random.sol", "environments.sol"]:
                 continue
-            output_expected = TESTDATA_OUTPUTS_EXPECTED_LASER_RESULT / (input_file.name + ".json")
+            output_expected = TESTDATA_OUTPUTS_EXPECTED_LASER_RESULT / (
-            output_current = TESTDATA_OUTPUTS_CURRENT_LASER_RESULT / (input_file.name + ".json")
+                input_file.name + ".json"
+            )
+            output_current = TESTDATA_OUTPUTS_CURRENT_LASER_RESULT / (
+                input_file.name + ".json"
+            )
 
             disassembly = SolidityContract(str(input_file)).disassembly
             account = Account("0x0000000000000000000000000000000000000000", disassembly)
@@ -81,7 +86,9 @@ class SVMTestCase(BaseTestCase):
             laser.sym_exec(account.address)
             laser_info = _all_info(laser)
 
-            output_current.write_text(json.dumps(laser_info, cls=LaserEncoder, indent=4))
+            output_current.write_text(
+                json.dumps(laser_info, cls=LaserEncoder, indent=4)
+            )
 
             if not (output_expected.read_text() == output_expected.read_text()):
                 self.found_changed_files(input_file, output_expected, output_current)

tests/taint_mutate_stack_test.py

@@ -1,12 +1,13 @@
 from mythril.laser.ethereum.taint_analysis import *
 
+
 def test_mutate_not_tainted():
     # Arrange
     record = TaintRecord()
 
     record.stack = [True, False, False]
     # Act
-    TaintRunner.mutate_stack(record, (2,1))
+    TaintRunner.mutate_stack(record, (2, 1))
 
     # Assert
     assert record.stack_tainted(0)

tests/taint_result_test.py

@@ -7,7 +7,7 @@ def test_result_state():
     taint_result = TaintResult()
     record = TaintRecord()
     state = GlobalState(2, None, None)
-    state.mstate.stack = [1,2,3]
+    state.mstate.stack = [1, 2, 3]
     record.add_state(state)
     record.stack = [False, False, False]
     # act
@@ -24,8 +24,7 @@ def test_result_no_state():
     taint_result = TaintResult()
     record = TaintRecord()
     state = GlobalState(2, None, None)
-    state.mstate.stack = [1,2,3]
+    state.mstate.stack = [1, 2, 3]
-
 
     # act
     taint_result.add_records([record])

tests/taint_runner_test.py

@@ -13,7 +13,7 @@ def test_execute_state(mocker):
 
     state = GlobalState(None, None, None)
     state.mstate.stack = [1, 2, 3]
-    mocker.patch.object(state, 'get_current_instruction')
+    mocker.patch.object(state, "get_current_instruction")
     state.get_current_instruction.return_value = {"opcode": "ADD"}
 
     # Act
@@ -31,12 +31,12 @@ def test_execute_node(mocker):
     state_1 = GlobalState(None, None, None)
     state_1.mstate.stack = [1, 2, 3, 1]
     state_1.mstate.pc = 1
-    mocker.patch.object(state_1, 'get_current_instruction')
+    mocker.patch.object(state_1, "get_current_instruction")
     state_1.get_current_instruction.return_value = {"opcode": "SWAP1"}
 
     state_2 = GlobalState(None, 1, None)
     state_2.mstate.stack = [1, 2, 4, 1]
-    mocker.patch.object(state_2, 'get_current_instruction')
+    mocker.patch.object(state_2, "get_current_instruction")
     state_2.get_current_instruction.return_value = {"opcode": "ADD"}
 
     node = Node("Test contract")
@@ -56,16 +56,16 @@ def test_execute_node(mocker):
 
 
 def test_execute(mocker):
-    active_account = Account('0x00')
+    active_account = Account("0x00")
     environment = Environment(active_account, None, None, None, None, None)
     state_1 = GlobalState(None, environment, None, MachineState(gas=10000000))
     state_1.mstate.stack = [1, 2]
-    mocker.patch.object(state_1, 'get_current_instruction')
+    mocker.patch.object(state_1, "get_current_instruction")
     state_1.get_current_instruction.return_value = {"opcode": "PUSH"}
 
     state_2 = GlobalState(None, environment, None, MachineState(gas=10000000))
     state_2.mstate.stack = [1, 2, 3]
-    mocker.patch.object(state_2, 'get_current_instruction')
+    mocker.patch.object(state_2, "get_current_instruction")
     state_2.get_current_instruction.return_value = {"opcode": "ADD"}
 
     node_1 = Node("Test contract")
@@ -73,7 +73,7 @@ def test_execute(mocker):
 
     state_3 = GlobalState(None, environment, None, MachineState(gas=10000000))
     state_3.mstate.stack = [1, 2]
-    mocker.patch.object(state_3, 'get_current_instruction')
+    mocker.patch.object(state_3, "get_current_instruction")
     state_3.get_current_instruction.return_value = {"opcode": "ADD"}
 
     node_2 = Node("Test contract")

tests/test_cli_opts.py

@@ -4,22 +4,23 @@ import json
 
 import sys
 
+
 def test_version_opt(capsys):
     # Check that "myth --version" returns a string with the word
     # "version" in it
-    sys.argv = ['mythril', '--version']
+    sys.argv = ["mythril", "--version"]
     with pytest.raises(SystemExit) as pytest_wrapped_e:
         main()
     assert pytest_wrapped_e.type == SystemExit
     captured = capsys.readouterr()
-    assert captured.out.find(' version ') >= 1
+    assert captured.out.find(" version ") >= 1
 
     # Check that "myth --version -o json" returns a JSON object
-    sys.argv = ['mythril', '--version', '-o', 'json']
+    sys.argv = ["mythril", "--version", "-o", "json"]
     with pytest.raises(SystemExit) as pytest_wrapped_e:
         main()
     assert pytest_wrapped_e.type == SystemExit
     captured = capsys.readouterr()
     d = json.loads(captured.out)
     assert isinstance(d, dict)
-    assert d['version_str']
+    assert d["version_str"]

tests/testdata/compile.py

@@ -4,12 +4,12 @@ from mythril.ether.soliditycontract import SolidityContract
 
 # Recompiles all the to be tested contracts
 root = Path(__file__).parent
-input = root / 'input_contracts'
+input = root / "input_contracts"
-output = root / 'inputs'
+output = root / "inputs"
 
 for contract in input.iterdir():
     sol = SolidityContract(str(contract))
     code = sol.code
 
-    output_file = (output / "{}.o".format(contract.name))
+    output_file = output / "{}.o".format(contract.name)
     output_file.write_text(code)

tests/testdata/outputs_expected/ether_send.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 722, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A non-zero amount of Ether is sent to a user-supplied address. The target address is msg.sender.\n\nThere is a check on storage index 1. This storage slot can be written to by calling the function `crowdfunding()`.", "function": "withdrawfunds()", "swc_id": "105", "title": "Ether send", "type": "Warning"}, {"address": 883, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "invest()", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{"error": null, "issues": [{"address": 722, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.", "function": "withdrawfunds()", "swc_id": "105", "title": "Ether send", "type": "Warning"}, {"address": 883, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "invest()", "swc_id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/ether_send.sol.o.markdown

@@ -9,9 +9,7 @@
 
 ### Description
 
-A non-zero amount of Ether is sent to a user-supplied address. The target address is msg.sender.
+It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.
-
-There is a check on storage index 1. This storage slot can be written to by calling the function `crowdfunding()`.
 
 ## Integer Overflow
 - SWC ID: 101

tests/testdata/outputs_expected/ether_send.sol.o.text

@@ -4,9 +4,7 @@ Type: Warning
 Contract: Unknown
 Function name: withdrawfunds()
 PC address: 722
-A non-zero amount of Ether is sent to a user-supplied address. The target address is msg.sender.
+It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.
-
-There is a check on storage index 1. This storage slot can be written to by calling the function `crowdfunding()`.
 --------------------
 
 ==== Integer Overflow ====

tests/testdata/outputs_expected/multi_contracts.sol.o.json

@@ -1 +1 @@
-{"error": null, "issues": [{"address": 142, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A non-zero amount of Ether is sent to a user-supplied address. The target address is msg.sender.\nIt seems that this function can be called without restrictions.", "function": "_function_0x8a4068dd", "swc_id": "105", "title": "Ether send", "type": "Warning"}], "success": true}
+{"error": null, "issues": [{"address": 142, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.", "function": "_function_0x8a4068dd", "swc_id": "105", "title": "Ether send", "type": "Warning"}], "success": true}

tests/testdata/outputs_expected/multi_contracts.sol.o.markdown

@@ -9,5 +9,4 @@
 
 ### Description
 
-A non-zero amount of Ether is sent to a user-supplied address. The target address is msg.sender.
+It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.
-It seems that this function can be called without restrictions.

tests/testdata/outputs_expected/multi_contracts.sol.o.text

@@ -4,7 +4,6 @@ Type: Warning
 Contract: Unknown
 Function name: _function_0x8a4068dd
 PC address: 142
-A non-zero amount of Ether is sent to a user-supplied address. The target address is msg.sender.
+It seems that an attacker is able to execute an call instruction, this can mean that the attacker is able to extract funds out of the contract.
-It seems that this function can be called without restrictions.
 --------------------
 

tests/testdata/outputs_expected/outputs_current/calls.sol.o.easm

@@ -1,400 +0,0 @@
-0 PUSH1 0x60
-2 PUSH1 0x40
-4 MSTORE
-5 PUSH1 0x04
-7 CALLDATASIZE
-8 LT
-9 PUSH2 0x0083
-12 JUMPI
-13 PUSH1 0x00
-15 CALLDATALOAD
-16 PUSH29 0x0100000000000000000000000000000000000000000000000000000000
-46 SWAP1
-47 DIV
-48 PUSH4 0xffffffff
-53 AND
-54 DUP1
-55 PUSH4 0x2776b163
-60 EQ
-61 PUSH2 0x0088
-64 JUMPI
-65 DUP1
-66 PUSH4 0x379bf63c
-71 EQ
-72 PUSH2 0x00c1
-75 JUMPI
-76 DUP1
-77 PUSH4 0x5a6814ec
-82 EQ
-83 PUSH2 0x0116
-86 JUMPI
-87 DUP1
-88 PUSH4 0xb5d02c8a
-93 EQ
-94 PUSH2 0x012b
-97 JUMPI
-98 DUP1
-99 PUSH4 0xd24b08cc
-104 EQ
-105 PUSH2 0x0180
-108 JUMPI
-109 DUP1
-110 PUSH4 0xe11f493e
-115 EQ
-116 PUSH2 0x0195
-119 JUMPI
-120 DUP1
-121 PUSH4 0xe1d10f79
-126 EQ
-127 PUSH2 0x01aa
-130 JUMPI
-131 JUMPDEST
-132 PUSH1 0x00
-134 DUP1
-135 REVERT
-136 JUMPDEST
-137 CALLVALUE
-138 ISZERO
-139 PUSH2 0x0093
-142 JUMPI
-143 PUSH1 0x00
-145 DUP1
-146 REVERT
-147 JUMPDEST
-148 PUSH2 0x00bf
-151 PUSH1 0x04
-153 DUP1
-154 DUP1
-155 CALLDATALOAD
-156 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-177 AND
-178 SWAP1
-179 PUSH1 0x20
-181 ADD
-182 SWAP1
-183 SWAP2
-184 SWAP1
-185 POP
-186 POP
-187 PUSH2 0x01e3
-190 JUMP
-191 JUMPDEST
-192 STOP
-193 JUMPDEST
-194 CALLVALUE
-195 ISZERO
-196 PUSH2 0x00cc
-199 JUMPI
-200 PUSH1 0x00
-202 DUP1
-203 REVERT
-204 JUMPDEST
-205 PUSH2 0x00d4
-208 PUSH2 0x0227
-211 JUMP
-212 JUMPDEST
-213 PUSH1 0x40
-215 MLOAD
-216 DUP1
-217 DUP3
-218 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-239 AND
-240 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-261 AND
-262 DUP2
-263 MSTORE
-264 PUSH1 0x20
-266 ADD
-267 SWAP2
-268 POP
-269 POP
-270 PUSH1 0x40
-272 MLOAD
-273 DUP1
-274 SWAP2
-275 SUB
-276 SWAP1
-277 RETURN
-278 JUMPDEST
-279 CALLVALUE
-280 ISZERO
-281 PUSH2 0x0121
-284 JUMPI
-285 PUSH1 0x00
-287 DUP1
-288 REVERT
-289 JUMPDEST
-290 PUSH2 0x0129
-293 PUSH2 0x024c
-296 JUMP
-297 JUMPDEST
-298 STOP
-299 JUMPDEST
-300 CALLVALUE
-301 ISZERO
-302 PUSH2 0x0136
-305 JUMPI
-306 PUSH1 0x00
-308 DUP1
-309 REVERT
-310 JUMPDEST
-311 PUSH2 0x013e
-314 PUSH2 0x029b
-317 JUMP
-318 JUMPDEST
-319 PUSH1 0x40
-321 MLOAD
-322 DUP1
-323 DUP3
-324 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-345 AND
-346 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-367 AND
-368 DUP2
-369 MSTORE
-370 PUSH1 0x20
-372 ADD
-373 SWAP2
-374 POP
-375 POP
-376 PUSH1 0x40
-378 MLOAD
-379 DUP1
-380 SWAP2
-381 SUB
-382 SWAP1
-383 RETURN
-384 JUMPDEST
-385 CALLVALUE
-386 ISZERO
-387 PUSH2 0x018b
-390 JUMPI
-391 PUSH1 0x00
-393 DUP1
-394 REVERT
-395 JUMPDEST
-396 PUSH2 0x0193
-399 PUSH2 0x02c1
-402 JUMP
-403 JUMPDEST
-404 STOP
-405 JUMPDEST
-406 CALLVALUE
-407 ISZERO
-408 PUSH2 0x01a0
-411 JUMPI
-412 PUSH1 0x00
-414 DUP1
-415 REVERT
-416 JUMPDEST
-417 PUSH2 0x01a8
-420 PUSH2 0x0311
-423 JUMP
-424 JUMPDEST
-425 STOP
-426 JUMPDEST
-427 CALLVALUE
-428 ISZERO
-429 PUSH2 0x01b5
-432 JUMPI
-433 PUSH1 0x00
-435 DUP1
-436 REVERT
-437 JUMPDEST
-438 PUSH2 0x01e1
-441 PUSH1 0x04
-443 DUP1
-444 DUP1
-445 CALLDATALOAD
-446 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-467 AND
-468 SWAP1
-469 PUSH1 0x20
-471 ADD
-472 SWAP1
-473 SWAP2
-474 SWAP1
-475 POP
-476 POP
-477 PUSH2 0x0368
-480 JUMP
-481 JUMPDEST
-482 STOP
-483 JUMPDEST
-484 DUP1
-485 PUSH1 0x01
-487 PUSH1 0x00
-489 PUSH2 0x0100
-492 EXP
-493 DUP2
-494 SLOAD
-495 DUP2
-496 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-517 MUL
-518 NOT
-519 AND
-520 SWAP1
-521 DUP4
-522 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-543 AND
-544 MUL
-545 OR
-546 SWAP1
-547 SSTORE
-548 POP
-549 POP
-550 JUMP
-551 JUMPDEST
-552 PUSH1 0x00
-554 DUP1
-555 SWAP1
-556 SLOAD
-557 SWAP1
-558 PUSH2 0x0100
-561 EXP
-562 SWAP1
-563 DIV
-564 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-585 AND
-586 DUP2
-587 JUMP
-588 JUMPDEST
-589 PUSH1 0x00
-591 DUP1
-592 SWAP1
-593 SLOAD
-594 SWAP1
-595 PUSH2 0x0100
-598 EXP
-599 SWAP1
-600 DIV
-601 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-622 AND
-623 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-644 AND
-645 PUSH1 0x40
-647 MLOAD
-648 PUSH1 0x00
-650 PUSH1 0x40
-652 MLOAD
-653 DUP1
-654 DUP4
-655 SUB
-656 DUP2
-657 PUSH1 0x00
-659 DUP7
-660 GAS
-661 CALL
-662 SWAP2
-663 POP
-664 POP
-665 POP
-666 JUMP
-667 JUMPDEST
-668 PUSH1 0x01
-670 PUSH1 0x00
-672 SWAP1
-673 SLOAD
-674 SWAP1
-675 PUSH2 0x0100
-678 EXP
-679 SWAP1
-680 DIV
-681 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-702 AND
-703 DUP2
-704 JUMP
-705 JUMPDEST
-706 PUSH1 0x01
-708 PUSH1 0x00
-710 SWAP1
-711 SLOAD
-712 SWAP1
-713 PUSH2 0x0100
-716 EXP
-717 SWAP1
-718 DIV
-719 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-740 AND
-741 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-762 AND
-763 PUSH1 0x40
-765 MLOAD
-766 PUSH1 0x00
-768 PUSH1 0x40
-770 MLOAD
-771 DUP1
-772 DUP4
-773 SUB
-774 DUP2
-775 PUSH1 0x00
-777 DUP7
-778 GAS
-779 CALL
-780 SWAP2
-781 POP
-782 POP
-783 POP
-784 JUMP
-785 JUMPDEST
-786 PUSH1 0x00
-788 DUP1
-789 SWAP1
-790 SLOAD
-791 SWAP1
-792 PUSH2 0x0100
-795 EXP
-796 SWAP1
-797 DIV
-798 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-819 AND
-820 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-841 AND
-842 PUSH1 0x40
-844 MLOAD
-845 PUSH1 0x00
-847 PUSH1 0x40
-849 MLOAD
-850 DUP1
-851 DUP4
-852 SUB
-853 DUP2
-854 PUSH1 0x00
-856 DUP7
-857 GAS
-858 CALL
-859 SWAP2
-860 POP
-861 POP
-862 POP
-863 PUSH1 0x00
-865 PUSH1 0x02
-867 DUP2
-868 SWAP1
-869 SSTORE
-870 POP
-871 JUMP
-872 JUMPDEST
-873 DUP1
-874 PUSH20 0xffffffffffffffffffffffffffffffffffffffff
-895 AND
-896 PUSH1 0x40
-898 MLOAD
-899 PUSH1 0x00
-901 PUSH1 0x40
-903 MLOAD
-904 DUP1
-905 DUP4
-906 SUB
-907 DUP2
-908 PUSH1 0x00
-910 DUP7
-911 GAS
-912 CALL
-913 SWAP2
-914 POP
-915 POP
-916 POP
-917 POP
-918 JUMP
-919 STOP