Fix merge conflicts

README.md

@@ -6,16 +6,18 @@
 
 [![Discord](https://img.shields.io/discord/481002907366588416.svg)](https://discord.gg/E3YrVtG)
 [![PyPI](https://badge.fury.io/py/mythril.svg)](https://pypi.python.org/pypi/mythril)
+[![Read the Docs](https://readthedocs.org/projects/mythril-classic/badge/?version=master)](https://mythril-classic.readthedocs.io/en/master/)
 ![Master Build Status](https://img.shields.io/circleci/project/github/ConsenSys/mythril-classic/master.svg)
 [![Waffle.io - Columns and their card count](https://badge.waffle.io/ConsenSys/mythril-classic.svg?columns=In%20Progress)](https://waffle.io/ConsenSys/mythril-classic/)
 [![Sonarcloud - Maintainability](https://sonarcloud.io/api/project_badges/measure?project=mythril&metric=sqale_rating)](https://sonarcloud.io/dashboard?id=mythril)
 [![Downloads](https://pepy.tech/badge/mythril)](https://pepy.tech/project/mythril)
 
-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. 
+Mythril Classic is an open-source security analysis tool for Ethereum smart contracts. It uses symbolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities. It's also an experimental tool designed for security pros. If you a smart contract developer you might prefer smoother tools such as:
 
-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.
+- [Mythos](https://github.com/cleanunicorn/mythos)
+- [Truffle Security](https://github.com/ConsenSys/truffle-security)
 
-Oh and by the way, we're also building an [easy-to-use security analysis API called MythX](https://mythx.io) that integrates seamlessly with Truffle, Visual Studio Code, Github and other environments. If you're looking for tooling to plug into your SDLC you should check it out. 
+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.
 
 ## Installation and setup
 
@@ -40,7 +42,7 @@ Instructions for using Mythril Classic are found on the [Wiki](https://github.co
 For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
 
 ## Bulding the Documentation
-Mythril Classic's documentation is contained in the `docs` folder. It is based on Sphinx and can be built using the Makefile contained in the subdirectory:
+Mythril Classic's documentation is contained in the `docs` folder and is published to [Read the Docs](https://mythril-classic.readthedocs.io/en/master/). It is based on Sphinx and can be built using the Makefile contained in the subdirectory:
 
 ```
 cd docs

docs/source/about.rst

@@ -0,0 +1,6 @@
+What is Mythril Classic?
+========================
+
+Mythril Classic is a security analysis tool for Ethereum smart contracts. It was `introduced at HITBSecConf 2018 <https://github.com/b-mueller/smashing-smart-contracts/blob/master/smashing-smart-contracts-1of1.pdf>`_.
+
+Mythril Classic detects a range of security issues, including integer underflows, owner-overwrite-to-Ether-withdrawal, and others. Note that Mythril is targeted at finding common vulnerabilities, and is not able to discover issues in the business logic of an application. Furthermore, Mythril and symbolic executors are generally unsound, as they are often unable to explore all possible states of a program.

docs/source/analysis-modules.rst

@@ -0,0 +1,11 @@
+Analysis Modules
+================
+
+Mythril Classic's detection capabilities are written in modules in the `/analysis/modules <https://github.com/ConsenSys/mythril-classic/tree/master/mythril/analysis/modules>`_ directory.
+
+
+.. toctree::
+   :maxdepth: 2
+
+   module-list.rst
+   create-module.rst

docs/source/conf.py

@@ -81,7 +81,7 @@ pygments_style = None
 # The theme to use for HTML and HTML Help pages.  See the documentation for
 # a list of builtin themes.
 #
-html_theme = "alabaster"
+html_theme = "sphinx_rtd_theme"
 
 # Theme options are theme-specific and customize the look and feel of a theme
 # further.  For a list of options available for each theme, see the

docs/source/create-module.rst

@@ -0,0 +1,4 @@
+Creating a Module
+=================
+
+Create a module in the :code:`analysis/modules` directory, and create an instance of a class that inherits :code:`DetectionModule` named :code:`detector`. Take a look at the `suicide module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/suicide.py>`_ as an example.

docs/source/index.rst

@@ -2,16 +2,20 @@ Welcome to Mythril Classic's documentation!
 ===========================================
 
 .. toctree::
-   :maxdepth: 3
-   :caption: Package Contents:
+   :maxdepth: 1
+   :caption: Table of Contents:
 
+   about
+   installation
+   security-analysis
+   analysis-modules
    mythril
 
 
-
-Indices and tables
+Indices and Tables
 ==================
 
 * :ref:`genindex`
 * :ref:`modindex`
 * :ref:`search`
+

docs/source/installation.rst

@@ -0,0 +1,66 @@
+Installation and Setup
+======================
+
+Mythril can be setup using different methods.
+
+**************
+PyPI on Mac OS
+**************
+
+.. code-block:: bash
+
+   brew update
+   brew upgrade
+   brew tap ethereum/ethereum
+   brew install leveldb
+   brew install solidity
+   pip3 install mythril
+
+
+**************
+PyPI on Ubuntu
+**************
+
+.. code-block:: bash
+
+   # Update
+   sudo apt update
+
+   # Install solc
+   sudo apt install software-properties-common
+   sudo add-apt-repository ppa:ethereum/ethereum
+   sudo apt install solc
+
+   # Install libssl-dev, python3-dev, and python3-pip
+   sudo apt install libssl-dev python3-dev python3-pip
+
+   # Install mythril
+   pip3 install mythril
+   myth --version
+
+
+******
+Docker
+******
+
+All Mythril releases, starting from v0.18.3, are published to DockerHub as Docker images under the :code:`mythril/myth` name.
+
+After installing `Docker CE <https://docs.docker.com/install/>`_:
+
+   .. code-block:: bash
+
+      # Pull the latest release of mythril/myth
+      $ docker pull mythril/myth
+
+Use :code:`docker run mythril/myth` the same way you would use the :code:`myth` command
+
+   .. code-block:: bash
+
+      docker run mythril/myth --help
+      docker run mythril/myth -dc "0x6060"
+
+To pass a file from your host machine to the dockerized Mythril, you must mount its containing folder to the container properly. For :code:`contract.sol` in the current working directory, do:
+
+   .. code-block:: bash
+
+      docker run -v $(pwd):/tmp mythril/myth -x /tmp/contract.sol

docs/source/module-list.rst

@@ -0,0 +1,68 @@
+Modules
+=======
+
+***********************************
+Delegate Call To Untrusted Contract
+***********************************
+
+The `delegatecall module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/delegatecall.py>`_ detects `SWC-112 (DELEGATECALL to Untrusted Callee) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-112>`_.
+
+***********************************
+Dependence on Predictable Variables
+***********************************
+
+The `predictable variables module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/dependence_on_predictable_vars.py>`_ detects `SWC-120 (Weak Randomness) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-120>`_ and `SWC-116 (Timestamp Dependence) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-116>`_.
+
+******************
+Deprecated Opcodes
+******************
+
+The `deprecated opcodes module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/deprecated_ops.py>`_ detects `SWC-111 (Use of Deprecated Functions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-111>`_.
+
+***********
+Ether Thief
+***********
+
+The `Ether Thief module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/ether_thief.py>`_ detects `SWC-105 (Unprotected Ether Withdrawal) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-105>`_.
+
+**********
+Exceptions
+**********
+
+The `exceptions module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/exceptions.py>`_ detects `SWC-110 (Assert Violation) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-110>`_.
+
+**************
+External Calls
+**************
+
+The `external calls module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/external_calls.py>`_ detects `SWC-117 (Reentrancy) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-117>`_ by detecting state changes after calls to external contracts.
+
+*******
+Integer
+*******
+
+The `integer module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/integer.py>`_ detects `SWC-101 (Integer Overflow and Underflow) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-101>`_.
+
+**************
+Multiple Sends
+**************
+
+The `multiple sends module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/multiple_sends.py>`_ detects `SWC-113 (Denial of Service with Failed Call) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-113>`_ by checking for multiple calls or sends in a single transaction.
+
+*******
+Suicide
+*******
+
+The `suicide module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/suicide.py>`_ detects `SWC-106 (Unprotected SELFDESTRUCT) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-106>`_.
+
+****************************
+Transaction Order Dependence
+****************************
+
+The `transaction order dependence module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/transaction_order_dependence.py>`_ detects `SWC-114 (Transaction Order Dependence / Race Conditions) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-114>`_.
+
+****************
+Unchecked Retval
+****************
+
+The `unchecked retval module <https://github.com/ConsenSys/mythril-classic/blob/develop/mythril/analysis/modules/unchecked_retval.py>`_ detects `SWC-104 (Unchecked Call Return Value) <https://smartcontractsecurity.github.io/SWC-registry/docs/SWC-104>`_.

docs/source/modules.rst

@@ -1,7 +0,0 @@
-mythril
-=======
-
-.. toctree::
-   :maxdepth: 4
-
-   mythril

docs/source/mythril.rst

@@ -1,4 +1,4 @@
-mythril package
+Mythril Package
 ===============
 
 Subpackages

docs/source/security-analysis.rst

@@ -0,0 +1,90 @@
+Security Analysis
+=================
+
+Run :code:`myth -x` with one of the input options described below will run the analysis modules in the `/analysis/modules <https://github.com/ConsenSys/mythril-classic/tree/master/mythril/analysis/modules>`_ directory.
+
+***********************
+Analyzing Solidity Code
+***********************
+
+In order to work with Solidity source code files, the `solc command line compiler <https://solidity.readthedocs.io/en/develop/using-the-compiler.html>`_ needs to be installed and in PATH. You can then provide the source file(s) as positional arguments.
+
+.. code-block:: bash
+
+   $ myth -x ether_send.sol
+   ==== Unprotected Ether Withdrawal ====
+   SWC ID: 105
+   Severity: High
+   Contract: Crowdfunding
+   Function name: withdrawfunds()
+   PC address: 730
+   Estimated Gas Usage: 1132 - 1743
+   Anyone can withdraw ETH from the contract account.
+   Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.
+   --------------------
+   In file: tests/testdata/input_contracts/ether_send.sol:21
+
+   msg.sender.transfer(address(this).balance)
+
+   --------------------
+
+If an input file contains multiple contract definitions, Mythril analyzes the *last* bytecode output produced by solc. You can override this by specifying the contract name explicitly:
+
+.. code-block:: bash
+
+   myth -x OmiseGo.sol:OMGToken
+
+Specifying Solc Versions
+########################
+
+You can specify a version of the solidity compiler to be used with :code:`--solv <version number>`. Please be aware that this uses `py-solc <https://github.com/ethereum/py-solc>`_ and will only work on Linux and macOS. It will check the version of solc in your path, and if this is not what is specified, it will download binaries on Linux or try to compile from source on macOS.
+
+
+Output Formats
+##############
+
+By default, analysis results are printed to the terminal in text format. You can change the output format with the :code:`-o` argument:
+
+.. code-block:: bash
+
+   myth -xo jsonv2 underflow.sol
+
+Available formats are :code:`text`, :code:`markdown`, :code:`json`, and :code:`jsonv2`. For integration with other tools, :code:`jsonv2` is generally preferred over :code:`json` because it is consistent with other `MythX <https://mythx.io>`_ tools.
+
+****************************
+Analyzing On-Chain Contracts
+****************************
+
+When analyzing contracts on the blockchain, Mythril will by default attempt to query INFURA. You can use the built-in INFURA support or manually configure the RPC settings with the :code:`--rpc` argument.
+
++--------------------------------+-------------------------------------------------+
+| :code:`--rpc ganache`          | Connect to local Ganache                        |
++--------------------------------+-------------------------------------------------+
+| :code:`--rpc infura-[netname]` | Connect to mainnet, rinkeby, kovan, or ropsten. |
++--------------------------------+-------------------------------------------------+
+| :code:`--rpc host:port`        | Connect to custom rpc                           |
++--------------------------------+-------------------------------------------------+
+| :code:`--rpctls <True/False>`  | RPC connection over TLS (default: False)        |
++--------------------------------+-------------------------------------------------+
+
+To specify a contract address, use :code:`-a <address>`
+
+Analyze mainnet contract via INFURA:
+
+.. code-block:: bash
+
+   myth -x -a 0x5c436ff914c458983414019195e0f4ecbef9e6dd
+
+Adding the :code:`-l` flag will cause mythril to automatically retrieve dependencies, such as dynamically linked library contracts:
+
+.. code-block:: bash
+
+   myth -xla 0xEbFD99838cb0c132016B9E117563CB41f2B02264 -v4
+
+******************
+Speed vs. Coverage
+******************
+
+The execution timeout can be specified with the :code:`--execution-timeout <seconds>` argument. When the timeout is reached, mythril will stop analysis and print out all currently found issues.
+
+The maximum recursion depth for the symbolic execution engine can be controlled with the :code:`--max-depth` argument. The default value is 22. Lowering this value will decrease the number of explored states and analysis time, while increasing this number will increase the number of explored states and increase analysis time. For some contracts, it helps to fine tune this number to get the best analysis results.

mythril/analysis/modules/delegatecall.py

@@ -85,7 +85,7 @@ def _concrete_call(
         title="Delegatecall Proxy",
         severity="Low",
         description_head="The contract implements a delegatecall proxy.",
-        description_tail="The smart contract forwards the received calldata via delegatecall. Note that callers"
+        description_tail="The smart contract forwards the received calldata via delegatecall. Note that callers "
         "can execute arbitrary functions in the callee contract and that the callee contract "
         "can access the storage of the calling contract. "
         "Make sure that the callee contract is audited properly.",

mythril/analysis/modules/deprecated_ops.py

@@ -1,6 +1,6 @@
 """This module contains the detection code for deprecated op codes."""
 from mythril.analysis.report import Issue
-from mythril.analysis.swc_data import DEPRICATED_FUNCTIONS_USAGE
+from mythril.analysis.swc_data import DEPRECATED_FUNCTIONS_USAGE
 from mythril.analysis.modules.base import DetectionModule
 from mythril.laser.ethereum.state.global_state import GlobalState
 import logging
@@ -33,7 +33,7 @@ def _analyze_state(state):
                 node.function_name
             )
         )
-        swc_id = DEPRICATED_FUNCTIONS_USAGE
+        swc_id = DEPRECATED_FUNCTIONS_USAGE
 
     elif instruction["opcode"] == "CALLCODE":
         log.debug("CALLCODE in function " + node.function_name)
@@ -44,7 +44,7 @@ def _analyze_state(state):
             "Due to a bug in the implementation it does not persist sender and value over the call. It was "
             "therefore deprecated and may be removed in the future. Use the delegatecall method instead."
         )
-        swc_id = DEPRICATED_FUNCTIONS_USAGE
+        swc_id = DEPRECATED_FUNCTIONS_USAGE
 
     issue = Issue(
         contract=node.contract_name,
@@ -68,7 +68,7 @@ class DeprecatedOperationsModule(DetectionModule):
         """"""
         super().__init__(
             name="Deprecated Operations",
-            swc_id=DEPRICATED_FUNCTIONS_USAGE,
+            swc_id=DEPRECATED_FUNCTIONS_USAGE,
             description=DESCRIPTION,
             entrypoint="callback",
             pre_hooks=["ORIGIN", "CALLCODE"],

mythril/analysis/modules/external_calls.py

@@ -51,7 +51,7 @@ def _analyze_state(state):
             description_tail = (
                 "The callee address of an external message call can be set by "
                 "the caller. Note that the callee can contain arbitrary code and may re-enter any function "
-                "in this contract. Review the business logic carefully to prevent averse effects on the"
+                "in this contract. Review the business logic carefully to prevent averse effects on the "
                 "contract state."
             )
 

mythril/analysis/modules/integer.py

@@ -2,12 +2,16 @@
 underflows."""
 
 import json
-from typing import Dict
+
+from math import log2, ceil
+from typing import Dict, cast, List
 from mythril.analysis import solver
 from mythril.analysis.report import Issue
 from mythril.analysis.swc_data import INTEGER_OVERFLOW_AND_UNDERFLOW
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.util import get_concrete_int
+from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.analysis.modules.base import DetectionModule
 
 from mythril.laser.smt import (
@@ -18,6 +22,8 @@ from mythril.laser.smt import (
     symbol_factory,
     Not,
     Expression,
+    Bool,
+    And,
 )
 
 import logging
@@ -27,8 +33,21 @@ log = logging.getLogger(__name__)
 
 
 class OverUnderflowAnnotation:
+    """ Symbol Annotation used if a BitVector can overflow"""
+
     def __init__(
-        self, overflowing_state: GlobalState, operator: str, constraint
+        self, overflowing_state: GlobalState, operator: str, constraint: Bool
+    ) -> None:
+        self.overflowing_state = overflowing_state
+        self.operator = operator
+        self.constraint = constraint
+
+
+class OverUnderflowStateAnnotation(StateAnnotation):
+    """ State Annotation used if an overflow is both possible and used in the annotated path"""
+
+    def __init__(
+        self, overflowing_state: GlobalState, operator: str, constraint: Bool
     ) -> None:
         self.overflowing_state = overflowing_state
         self.operator = operator
@@ -49,7 +68,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 "there's a possible state where op1 + op0 > 2^32 - 1"
             ),
             entrypoint="callback",
-            pre_hooks=["ADD", "MUL", "SUB", "SSTORE", "JUMPI"],
+            pre_hooks=["ADD", "MUL", "EXP", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"],
         )
         self._overflow_cache = {}  # type: Dict[int, bool]
         self._underflow_cache = {}  # type: Dict[int, bool]
@@ -74,23 +93,30 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         has_underflow = self._underflow_cache.get(address, False)
         if has_overflow or has_underflow:
             return
-        if state.get_current_instruction()["opcode"] == "ADD":
-            self._handle_add(state)
-        elif state.get_current_instruction()["opcode"] == "MUL":
-            self._handle_mul(state)
-        elif state.get_current_instruction()["opcode"] == "SUB":
-            self._handle_sub(state)
-        elif state.get_current_instruction()["opcode"] == "SSTORE":
-            self._handle_sstore(state)
-        elif state.get_current_instruction()["opcode"] == "JUMPI":
-            self._handle_jumpi(state)
-
-    def _handle_add(self, state):
+        opcode = state.get_current_instruction()["opcode"]
+        funcs = {
+            "ADD": [self._handle_add],
+            "SUB": [self._handle_sub],
+            "MUL": [self._handle_mul],
+            "SSTORE": [self._handle_sstore],
+            "JUMPI": [self._handle_jumpi],
+            "RETURN": [self._handle_return, self._handle_transaction_end],
+            "STOP": [self._handle_transaction_end],
+            "EXP": [self._handle_exp],
+        }
+        for func in funcs[opcode]:
+            func(state)
+
+    def _get_args(self, state):
         stack = state.mstate.stack
         op0, op1 = (
             self._make_bitvec_if_not(stack, -1),
             self._make_bitvec_if_not(stack, -2),
         )
+        return op0, op1
+
+    def _handle_add(self, state):
+        op0, op1 = self._get_args(state)
         c = Not(BVAddNoOverflow(op0, op1, False))
 
         # Check satisfiable
@@ -102,12 +128,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         op0.annotate(annotation)
 
     def _handle_mul(self, state):
-        stack = state.mstate.stack
-        op0, op1 = (
-            self._make_bitvec_if_not(stack, -1),
-            self._make_bitvec_if_not(stack, -2),
-        )
-
+        op0, op1 = self._get_args(state)
         c = Not(BVMulNoOverflow(op0, op1, False))
 
         # Check satisfiable
@@ -119,11 +140,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         op0.annotate(annotation)
 
     def _handle_sub(self, state):
-        stack = state.mstate.stack
-        op0, op1 = (
-            self._make_bitvec_if_not(stack, -1),
-            self._make_bitvec_if_not(stack, -2),
-        )
+        op0, op1 = self._get_args(state)
         c = Not(BVSubNoUnderflow(op0, op1, False))
 
         # Check satisfiable
@@ -134,6 +151,33 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         annotation = OverUnderflowAnnotation(state, "subtraction", c)
         op0.annotate(annotation)
 
+    def _handle_exp(self, state):
+        op0, op1 = self._get_args(state)
+        if op0.symbolic and op1.symbolic:
+            constraint = And(
+                op1 > symbol_factory.BitVecVal(256, 256),
+                op0 > symbol_factory.BitVecVal(1, 256),
+            )
+        elif op1.symbolic:
+            if op0.value < 2:
+                return
+            constraint = op1 >= symbol_factory.BitVecVal(
+                ceil(256 / log2(op0.value)), 256
+            )
+        elif op0.symbolic:
+            if op1.value == 0:
+                return
+            constraint = op0 >= symbol_factory.BitVecVal(
+                2 ** ceil(256 / op1.value), 256
+            )
+        else:
+            constraint = op0.value ** op1.value >= 2 ** 256
+        model = self._try_constraints(state.node.constraints, [constraint])
+        if model is None:
+            return
+        annotation = OverUnderflowAnnotation(state, "exponentiation", constraint)
+        op0.annotate(annotation)
+
     @staticmethod
     def _make_bitvec_if_not(stack, index):
         value = stack[index]
@@ -165,70 +209,91 @@ class IntegerOverflowUnderflowModule(DetectionModule):
     def _get_title(_type):
         return "Integer {}".format(_type)
 
-    def _handle_sstore(self, state):
+    @staticmethod
+    def _handle_sstore(state: GlobalState) -> None:
         stack = state.mstate.stack
         value = stack[-2]
-
         if not isinstance(value, Expression):
             return
         for annotation in value.annotations:
             if not isinstance(annotation, OverUnderflowAnnotation):
                 continue
+            state.annotate(
+                OverUnderflowStateAnnotation(
+                    annotation.overflowing_state,
+                    annotation.operator,
+                    annotation.constraint,
+                )
+            )
 
-            _type = "Underflow" if annotation.operator == "subtraction" else "Overflow"
-            ostate = annotation.overflowing_state
-            node = ostate.node
+    @staticmethod
+    def _handle_jumpi(state):
+        stack = state.mstate.stack
+        value = stack[-2]
 
-            issue = Issue(
-                contract=node.contract_name,
-                function_name=node.function_name,
-                address=ostate.get_current_instruction()["address"],
-                swc_id=INTEGER_OVERFLOW_AND_UNDERFLOW,
-                bytecode=ostate.environment.code.bytecode,
-                title=self._get_title(_type),
-                severity="High",
-                description_head=self._get_description_head(annotation, _type),
-                description_tail=self._get_description_tail(annotation, _type),
-                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
+        for annotation in value.annotations:
+            if not isinstance(annotation, OverUnderflowAnnotation):
+                continue
+            state.annotate(
+                OverUnderflowStateAnnotation(
+                    annotation.overflowing_state,
+                    annotation.operator,
+                    annotation.constraint,
+                )
             )
 
+    @staticmethod
+    def _handle_return(state: GlobalState) -> None:
+        """
+        Adds all the annotations into the state which correspond to the
+        locations in the memory returned by RETURN opcode.
+        :param state: The Global State
+        """
+        stack = state.mstate.stack
+        try:
+            offset, length = get_concrete_int(stack[-1]), get_concrete_int(stack[-2])
+        except TypeError:
+            return
+        for element in state.mstate.memory[offset : offset + length]:
+            if not isinstance(element, Expression):
+                continue
+            for annotation in element.annotations:
+                if isinstance(annotation, OverUnderflowAnnotation):
+                    state.annotate(
+                        OverUnderflowStateAnnotation(
+                            annotation.overflowing_state,
+                            annotation.operator,
+                            annotation.constraint,
+                        )
+                    )
+
+    def _handle_transaction_end(self, state: GlobalState) -> None:
+        for annotation in cast(
+            List[OverUnderflowStateAnnotation],
+            state.get_annotations(OverUnderflowStateAnnotation),
+        ):
+
+            ostate = annotation.overflowing_state
             address = _get_address_from_state(ostate)
 
             if annotation.operator == "subtraction" and self._underflow_cache.get(
                 address, False
             ):
                 continue
+
             if annotation.operator != "subtraction" and self._overflow_cache.get(
                 address, False
             ):
                 continue
 
+            node = ostate.node
             try:
 
                 transaction_sequence = solver.get_transaction_sequence(
                     state, node.constraints + [annotation.constraint]
                 )
-
-                issue.debug = json.dumps(transaction_sequence, indent=4)
-
             except UnsatError:
                 continue
-            if annotation.operator == "subtraction":
-                self._underflow_cache[address] = True
-            else:
-                self._overflow_cache[address] = True
-
-            self._issues.append(issue)
-
-    def _handle_jumpi(self, state):
-        stack = state.mstate.stack
-        value = stack[-2]
-
-        for annotation in value.annotations:
-            if not isinstance(annotation, OverUnderflowAnnotation):
-                continue
-            ostate = annotation.overflowing_state
-            node = ostate.node
 
             _type = "Underflow" if annotation.operator == "subtraction" else "Overflow"
             issue = Issue(
@@ -244,29 +309,8 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
 
-            address = _get_address_from_state(ostate)
-
-            if annotation.operator == "subtraction" and self._underflow_cache.get(
-                address, False
-            ):
-                continue
-
-            if annotation.operator != "subtraction" and self._overflow_cache.get(
-                address, False
-            ):
-                continue
-
-            try:
-
-                transaction_sequence = solver.get_transaction_sequence(
-                    state, node.constraints + [annotation.constraint]
-                )
-
             issue.debug = json.dumps(transaction_sequence, indent=4)
 
-            except UnsatError:
-                continue
-
             if annotation.operator == "subtraction":
                 self._underflow_cache[address] = True
             else:

mythril/analysis/report.py

@@ -3,13 +3,15 @@ import logging
 import json
 import operator
 from jinja2 import PackageLoader, Environment
+from typing import Dict, List
 import _pysha3 as sha3
 import hashlib
 
 from mythril.solidity.soliditycontract import SolidityContract
 from mythril.analysis.swc_data import SWC_TO_TITLE
 from mythril.support.source_support import Source
-
+from mythril.support.start_time import StartTime
+from time import time
 
 log = logging.getLogger(__name__)
 
@@ -33,16 +35,17 @@ class Issue:
     ):
         """
 
-        :param contract:
-        :param function_name:
-        :param address:
-        :param swc_id:
-        :param title:
-        :param bytecode:
-        :param gas_used:
-        :param _type:
-        :param description:
-        :param debug:
+        :param contract: The contract
+        :param function_name: Function name where the issue is detected
+        :param address: The address of the issue
+        :param swc_id: Issue's corresponding swc-id
+        :param title: Title
+        :param bytecode: bytecode of the issue
+        :param gas_used: amount of gas used
+        :param severity: The severity of the issue
+        :param description_head: The top part of description
+        :param description_tail: The bottom part of the description
+        :param debug: The transaction sequence
         """
         self.title = title
         self.contract = contract
@@ -59,6 +62,7 @@ class Issue:
         self.code = None
         self.lineno = None
         self.source_mapping = None
+        self.discovery_time = time() - StartTime().global_start_time
 
         try:
             keccak = sha3.keccak_256()
@@ -103,6 +107,17 @@ class Issue:
 
         return issue
 
+    def _set_internal_compiler_error(self):
+        """
+        Adds the false positive to description and changes severity to low
+        """
+        self.severity = "Low"
+        self.description_tail += (
+            " This issue is reported for internal compiler generated code."
+        )
+        self.description = "%s\n%s" % (self.description_head, self.description_tail)
+        self.code = ""
+
     def add_code_info(self, contract):
         """
 
@@ -115,6 +130,8 @@ class Issue:
             self.filename = codeinfo.filename
             self.code = codeinfo.code
             self.lineno = codeinfo.lineno
+            if self.lineno is None:
+                self._set_internal_compiler_error()
             self.source_mapping = codeinfo.solc_mapping
         else:
             self.source_mapping = self.address
@@ -127,7 +144,7 @@ class Report:
         loader=PackageLoader("mythril.analysis"), trim_blocks=True
     )
 
-    def __init__(self, verbose=False, source=None):
+    def __init__(self, verbose=False, source=None, exceptions=None):
         """
 
         :param verbose:
@@ -137,6 +154,7 @@ class Report:
         self.solc_version = ""
         self.meta = {}
         self.source = source or Source()
+        self.exceptions = exceptions or []
 
     def sorted_issues(self):
         """
@@ -174,6 +192,14 @@ class Report:
         result = {"success": True, "error": None, "issues": self.sorted_issues()}
         return json.dumps(result, sort_keys=True)
 
+    def _get_exception_data(self) -> dict:
+        if not self.exceptions:
+            return {}
+        logs = []  # type: List[Dict]
+        for exception in self.exceptions:
+            logs += [{"level": "error", "hidden": "true", "error": exception}]
+        return {"logs": logs}
+
     def as_swc_standard_format(self):
         """Format defined for integration and correlation.
 
@@ -208,14 +234,14 @@ class Report:
                     "extra": {},
                 }
             )
-
+        meta_data = self._get_exception_data()
         result = [
             {
                 "issues": _issues,
                 "sourceType": "raw-bytecode",
                 "sourceFormat": "evm-byzantium-bytecode",
                 "sourceList": source_list,
-                "meta": {},
+                "meta": meta_data,
             }
         ]
 

mythril/analysis/security.py

@@ -1,7 +1,7 @@
 """This module contains functionality for hooking in detection modules and
 executing them."""
 from collections import defaultdict
-from ethereum.opcodes import opcodes
+from mythril.support.opcodes import opcodes
 from mythril.analysis import modules
 import pkgutil
 import importlib.util

mythril/analysis/swc_data.py

@@ -11,7 +11,7 @@ REENTRANCY = "107"
 DEFAULT_STATE_VARIABLE_VISIBILITY = "108"
 UNINITIALIZED_STORAGE_POINTER = "109"
 ASSERT_VIOLATION = "110"
-DEPRICATED_FUNCTIONS_USAGE = "111"
+DEPRECATED_FUNCTIONS_USAGE = "111"
 DELEGATECALL_TO_UNTRUSTED_CONTRACT = "112"
 MULTIPLE_SENDS = "113"
 TX_ORDER_DEPENDENCE = "114"

mythril/analysis/symbolic.py

@@ -193,7 +193,7 @@ class SymExecWrapper:
                         )
 
                 elif op == "SSTORE":
-                    stack = copy.deepcopy(state.mstate.stack)
+                    stack = copy.copy(state.mstate.stack)
                     address = state.environment.active_account.address
 
                     index, value = stack.pop(), stack.pop()

mythril/disassembler/asm.py

@@ -4,12 +4,12 @@ code disassembly."""
 import re
 from collections import Generator
 
-from ethereum.opcodes import opcodes
+from mythril.support.opcodes import opcodes
 
 regex_PUSH = re.compile(r"^PUSH(\d*)$")
 
 # Additional mnemonic to catch failed assertions
-opcodes[254] = ["ASSERT_FAIL", 0, 0, 0]
+opcodes[254] = ("ASSERT_FAIL", 0, 0, 0)
 
 
 class EvmInstruction:

mythril/interfaces/cli.py

@@ -12,6 +12,7 @@ import os
 import sys
 
 import coloredlogs
+import traceback
 
 import mythril.support.signatures as sigs
 from mythril.exceptions import AddressNotFoundError, CriticalError
@@ -28,17 +29,29 @@ from mythril.version import VERSION
 log = logging.getLogger(__name__)
 
 
-def exit_with_error(format_: str, message: str) -> None:
+def exit_with_error(format_, message):
     """
-
     :param format_:
     :param message:
     """
     if format_ == "text" or format_ == "markdown":
         log.error(message)
-    else:
+    elif format_ == "json":
         result = {"success": False, "error": str(message), "issues": []}
         print(json.dumps(result))
+    else:
+        result = [
+            {
+                "issues": [],
+                "sourceType": "",
+                "sourceFormat": "",
+                "sourceList": [],
+                "meta": {
+                    "logs": [{"level": "error", "hidden": "true", "error": message}]
+                },
+            }
+        ]
+        print(json.dumps(result))
     sys.exit()
 
 
@@ -55,10 +68,6 @@ def main() -> None:
     parse_args(parser=parser, args=args)
 
 
-if __name__ == "__main__":
-    main()
-
-
 def create_parser(parser: argparse.ArgumentParser) -> None:
     """
     Creates the parser by setting all the possible arguments
@@ -187,14 +196,14 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
     options.add_argument(
         "--max-depth",
         type=int,
-        default=22,
+        default=50,
         help="Maximum recursion depth for symbolic execution",
     )
 
     options.add_argument(
         "--strategy",
         choices=["dfs", "bfs", "naive-random", "weighted-random"],
-        default="dfs",
+        default="bfs",
         help="Symbolic execution strategy",
     )
     options.add_argument(
@@ -250,27 +259,7 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
     parser.add_argument("--epic", action="store_true", help=argparse.SUPPRESS)
 
 
-def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> None:
-    """
-    Parses the arguments
-    :param parser: The parser
-    :param args: The 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":
-            print(json.dumps({"version_str": VERSION}))
-        else:
-            print("Mythril version {}".format(VERSION))
-        sys.exit()
-
-    # Parse cmdline args
-
+def validate_args(parser: argparse.ArgumentParser, args: argparse.Namespace):
     if not (
         args.search
         or args.hash
@@ -323,21 +312,16 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non
                 "--enable-iprof must be used with one of -g, --graph, -x, --fire-lasers, -j and --statespace-json",
             )
 
-    # -- commands --
+
+def quick_commands(args: argparse.Namespace):
     if args.hash:
         print(MythrilDisassembler.hash_for_function_signature(args.hash))
         sys.exit()
 
-    try:
-        # the mythril object should be our main interface
-        # infura = None, rpc = None, rpctls = None
-        # solc_args = None, dynld = None, max_recursion_depth = 12):
+
+def set_config(args: argparse.Namespace):
     config = MythrilConfig()
-        if (
-            args.dynld
-            or not args.no_onchain_storage_access
-            and not (args.rpc or args.i)
-        ):
+    if args.dynld or not args.no_onchain_storage_access and not (args.rpc or args.i):
         config.set_api_from_config_path()
 
     if args.address:
@@ -348,7 +332,10 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non
         config.set_api_leveldb(
             config.leveldb_dir if not args.leveldb_dir else args.leveldb_dir
         )
+    return config
 
+
+def leveldb_search(config: MythrilConfig, args: argparse.Namespace):
     if args.search or args.contract_hash_to_address:
         leveldb_searcher = MythrilLevelDB(config.eth_db)
         if args.search:
@@ -358,44 +345,26 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non
         else:
             # search corresponding address
             try:
-                    leveldb_searcher.contract_hash_to_address(
-                        args.contract_hash_to_address
-                    )
+                leveldb_searcher.contract_hash_to_address(args.contract_hash_to_address)
             except AddressNotFoundError:
                 print("Address not found.")
 
         sys.exit()
 
-        dissasembler = MythrilDisassembler(
-            eth=config.eth,
-            solc_version=args.solv,
-            solc_args=args.solc_args,
-            enable_online_lookup=args.query_signature,
-        )
-        if args.truffle:
-            try:
-                # not really pythonic atm. needs refactoring
-                dissasembler.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."
-                )
-            sys.exit()
 
-        # Load / compile input contracts
+def get_code(disassembler: MythrilDisassembler, args: argparse.Namespace):
     address = None
-
     if args.code:
         # Load from bytecode
         code = args.code[2:] if args.code.startswith("0x") else args.code
-            address, _ = dissasembler.load_from_bytecode(code, args.bin_runtime)
+        address, _ = disassembler.load_from_bytecode(code, args.bin_runtime)
     elif args.codefile:
         bytecode = "".join([l.strip() for l in args.codefile if len(l.strip()) > 0])
         bytecode = bytecode[2:] if bytecode.startswith("0x") else bytecode
-            address, _ = dissasembler.load_from_bytecode(bytecode, args.bin_runtime)
+        address, _ = disassembler.load_from_bytecode(bytecode, args.bin_runtime)
     elif args.address:
         # Get bytecode from a contract address
-            address, _ = dissasembler.load_from_address(args.address)
+        address, _ = disassembler.load_from_address(args.address)
     elif args.solidity_file:
         # Compile Solidity source file(s)
         if args.graph and len(args.solidity_file) > 1:
@@ -403,7 +372,7 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non
                 args.outform,
                 "Cannot generate call graphs from multiple input files. Please do it one at a time.",
             )
-            address, _ = dissasembler.load_from_solidity(
+        address, _ = disassembler.load_from_solidity(
             args.solidity_file
         )  # list of files
     else:
@@ -411,18 +380,15 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non
             args.outform,
             "No input bytecode. Please provide EVM code via -c BYTECODE, -a ADDRESS, or -i SOLIDITY_FILES",
         )
+    return address
 
-        analyzer = MythrilAnalyzer(
-            strategy=args.strategy,
-            disassembler=dissasembler,
-            address=address,
-            max_depth=args.max_depth,
-            execution_timeout=args.execution_timeout,
-            create_timeout=args.create_timeout,
-            enable_iprof=args.enable_iprof,
-            onchain_storage_access=not args.no_onchain_storage_access,
-        )
-        # Commands
+
+def execute_command(
+    disassembler: MythrilDisassembler,
+    address: str,
+    parser: argparse.ArgumentParser,
+    args: argparse.Namespace,
+):
 
     if args.storage:
         if not args.address:
@@ -431,22 +397,33 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non
                 "To read storage, provide the address of a deployed contract with the -a option.",
             )
 
-            storage = dissasembler.get_state_variable_from_storage(
-                address=address,
-                params=[a.strip() for a in args.storage.strip().split(",")],
+        storage = disassembler.get_state_variable_from_storage(
+            address=address, params=[a.strip() for a in args.storage.strip().split(",")]
         )
         print(storage)
+        return
+
+    analyzer = MythrilAnalyzer(
+        strategy=args.strategy,
+        disassembler=disassembler,
+        address=address,
+        max_depth=args.max_depth,
+        execution_timeout=args.execution_timeout,
+        create_timeout=args.create_timeout,
+        enable_iprof=args.enable_iprof,
+        onchain_storage_access=not args.no_onchain_storage_access,
+    )
 
-        elif args.disassemble:
+    if args.disassemble:
         # or mythril.disassemble(mythril.contracts[0])
 
-            if dissasembler.contracts[0].code:
-                print("Runtime Disassembly: \n" + dissasembler.contracts[0].get_easm())
-            if dissasembler.contracts[0].creation_code:
-                print("Disassembly: \n" + dissasembler.contracts[0].get_creation_easm())
+        if disassembler.contracts[0].code:
+            print("Runtime Disassembly: \n" + disassembler.contracts[0].get_easm())
+        if disassembler.contracts[0].creation_code:
+            print("Disassembly: \n" + disassembler.contracts[0].get_creation_easm())
 
     elif args.graph or args.fire_lasers:
-            if not dissasembler.contracts:
+        if not disassembler.contracts:
             exit_with_error(
                 args.outform, "input files do not contain any valid contracts"
             )
@@ -503,5 +480,57 @@ def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> Non
     else:
         parser.print_help()
 
+
+def parse_args(parser: argparse.ArgumentParser, args: argparse.Namespace) -> None:
+    """
+    Parses the arguments
+    :param parser: The parser
+    :param args: The 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":
+            print(json.dumps({"version_str": VERSION}))
+        else:
+            print("Mythril version {}".format(VERSION))
+        sys.exit()
+
+    # Parse cmdline args
+    validate_args(parser, args)
+    try:
+        quick_commands(args)
+        config = set_config(args)
+        leveldb_search(config, args)
+        dissasembler = MythrilDisassembler(
+            eth=config.eth,
+            solc_version=args.solv,
+            solc_args=args.solc_args,
+            enable_online_lookup=args.query_signature,
+        )
+        if args.truffle:
+            try:
+                dissasembler.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."
+                )
+            sys.exit()
+
+        address = get_code(dissasembler, args)
+        execute_command(
+            disassembler=dissasembler, address=address, parser=parser, args=args
+        )
     except CriticalError as ce:
         exit_with_error(args.outform, str(ce))
+    except Exception:
+        exit_with_error(args.outform, traceback.format_exc())
+
+
+if __name__ == "__main__":
+    main()

mythril/laser/ethereum/gas.py

@@ -62,6 +62,9 @@ OPCODE_GAS = {
     "XOR": (3, 3),
     "NOT": (3, 3),
     "BYTE": (3, 3),
+    "SHL": (3, 3),
+    "SHR": (3, 3),
+    "SAR": (3, 3),
     "SHA3": (
         30,
         30 + 6 * 8,
@@ -80,6 +83,7 @@ OPCODE_GAS = {
     "GASPRICE": (2, 2),
     "EXTCODESIZE": (700, 700),
     "EXTCODECOPY": (700, 700 + 3 * 768),  # https://ethereum.stackexchange.com/a/47556
+    "EXTCODEHASH": (400, 400),
     "RETURNDATASIZE": (2, 2),
     "RETURNDATACOPY": (3, 3),
     "BLOCKHASH": (20, 20),
@@ -176,6 +180,10 @@ OPCODE_GAS = {
     "LOG3": (4 * 375, 4 * 375 + 8 * 32),
     "LOG4": (5 * 375, 5 * 375 + 8 * 32),
     "CREATE": (32000, 32000),
+    "CREATE2": (
+        32000,
+        32000,
+    ),  # TODO: The gas value is dynamic, to be done while implementing create2
     "CALL": (700, 700 + 9000 + 25000),
     "NATIVE_COST": calculate_native_gas,
     "CALLCODE": (700, 700 + 9000 + 25000),

mythril/laser/ethereum/instructions.py

@@ -6,7 +6,7 @@ import logging
 from copy import copy, deepcopy
 from typing import cast, Callable, List, Union, Tuple
 from datetime import datetime
-
+from math import ceil
 from ethereum import utils
 
 from mythril.laser.smt import (
@@ -26,6 +26,7 @@ from mythril.laser.smt import (
     Bool,
     Or,
     Not,
+    LShR,
 )
 from mythril.laser.smt import symbol_factory
 
@@ -464,6 +465,33 @@ class Instruction:
         global_state.mstate.stack.append(0 if s1 == 0 else URem(s0, s1))
         return [global_state]
 
+    @StateTransition()
+    def shl_(self, global_state: GlobalState) -> List[GlobalState]:
+        shift, value = (
+            util.pop_bitvec(global_state.mstate),
+            util.pop_bitvec(global_state.mstate),
+        )
+        global_state.mstate.stack.append(value << shift)
+        return [global_state]
+
+    @StateTransition()
+    def shr_(self, global_state: GlobalState) -> List[GlobalState]:
+        shift, value = (
+            util.pop_bitvec(global_state.mstate),
+            util.pop_bitvec(global_state.mstate),
+        )
+        global_state.mstate.stack.append(LShR(value, shift))
+        return [global_state]
+
+    @StateTransition()
+    def sar_(self, global_state: GlobalState) -> List[GlobalState]:
+        shift, value = (
+            util.pop_bitvec(global_state.mstate),
+            util.pop_bitvec(global_state.mstate),
+        )
+        global_state.mstate.stack.append(value >> shift)
+        return [global_state]
+
     @StateTransition()
     def smod_(self, global_state: GlobalState) -> List[GlobalState]:
         """
@@ -519,16 +547,22 @@ class Instruction:
         base, exponent = util.pop_bitvec(state), util.pop_bitvec(state)
 
         if base.symbolic or exponent.symbolic:
+
             state.stack.append(
                 global_state.new_bitvec(
                     "(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")",
                     256,
+                    base.annotations + exponent.annotations,
                 )
             )
         else:
 
             state.stack.append(
-                symbol_factory.BitVecVal(pow(base.value, exponent.value, 2 ** 256), 256)
+                symbol_factory.BitVecVal(
+                    pow(base.value, exponent.value, 2 ** 256),
+                    256,
+                    annotations=base.annotations + exponent.annotations,
+                )
             )
 
         return [global_state]
@@ -891,29 +925,35 @@ class Instruction:
         state.max_gas_used += max_gas
         StateTransition.check_gas_usage_limit(global_state)
 
-        try:
         state.mem_extend(index, length)
-            data = b"".join(
-                [
-                    util.get_concrete_int(i).to_bytes(1, byteorder="big")
-                    for i in state.memory[index : index + length]
+        data_list = [
+            b if isinstance(b, BitVec) else symbol_factory.BitVecVal(b, 8)
+            for b in state.memory[index : index + length]
         ]
-            )
+        if len(data_list) > 1:
+            data = simplify(Concat(data_list))
+        elif len(data_list) == 1:
+            data = data_list[0]
+        else:
+            # length is 0; this only matters for input of the BitVecFuncVal
+            data = symbol_factory.BitVecVal(0, 1)
 
-        except TypeError:
-            argument = str(state.memory[index]).replace(" ", "_")
+        if data.symbolic:
+            argument_str = str(state.memory[index]).replace(" ", "_")
+            result = symbol_factory.BitVecFuncSym(
+                "KECCAC[{}]".format(argument_str), "keccak256", 256, input_=data
+            )
+            log.debug("Created BitVecFunc hash.")
 
-            result = symbol_factory.BitVecSym("KECCAC[{}]".format(argument), 256)
             keccak_function_manager.add_keccak(result, state.memory[index])
-            state.stack.append(result)
-            return [global_state]
-
-        keccak = utils.sha3(utils.bytearray_to_bytestr(data))
+        else:
+            keccak = utils.sha3(data.value.to_bytes(length, byteorder="big"))
+            result = symbol_factory.BitVecFuncVal(
+                util.concrete_int_from_bytes(keccak, 0), "keccak256", 256, input_=data
+            )
             log.debug("Computed SHA3 Hash: " + str(binascii.hexlify(keccak)))
 
-        state.stack.append(
-            symbol_factory.BitVecVal(util.concrete_int_from_bytes(keccak, 0), 256)
-        )
+        state.stack.append(result)
         return [global_state]
 
     @StateTransition()
@@ -926,6 +966,34 @@ class Instruction:
         global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256))
         return [global_state]
 
+    @staticmethod
+    def _handle_symbolic_args(
+        global_state: GlobalState, concrete_memory_offset: int
+    ) -> None:
+        """
+        In contract creation transaction with dynamic arguments(like arrays, maps) solidity will try to
+        execute CODECOPY with code size as len(with_args) - len(without_args) which in our case
+        would be 0, hence we are writing 10 symbol words onto the memory on the assumption that
+        no one would use 10 array/map arguments for constructor.
+        :param global_state: The global state
+        :param concrete_memory_offset: The memory offset on which symbols should be written
+        """
+        no_of_words = ceil(
+            min(len(global_state.environment.code.bytecode) / 2, 320) / 32
+        )
+        global_state.mstate.mem_extend(concrete_memory_offset, 32 * no_of_words)
+        for i in range(no_of_words):
+            global_state.mstate.memory.write_word_at(
+                concrete_memory_offset + i * 32,
+                global_state.new_bitvec(
+                    "code_{}({})".format(
+                        concrete_memory_offset + i * 32,
+                        global_state.environment.active_account.contract_name,
+                    ),
+                    256,
+                ),
+            )
+
     @StateTransition()
     def codecopy_(self, global_state: GlobalState) -> List[GlobalState]:
         """
@@ -986,15 +1054,7 @@ class Instruction:
             global_state.current_transaction, ContractCreationTransaction
         ):
             if concrete_code_offset >= len(bytecode) // 2:
-                global_state.mstate.mem_extend(concrete_memory_offset, 1)
-                global_state.mstate.memory[
-                    concrete_memory_offset
-                ] = global_state.new_bitvec(
-                    "code({})".format(
-                        global_state.environment.active_account.contract_name
-                    ),
-                    8,
-                )
+                self._handle_symbolic_args(global_state, concrete_memory_offset)
                 return [global_state]
 
         for i in range(size):
@@ -1050,6 +1110,20 @@ class Instruction:
 
         return [global_state]
 
+    @StateTransition
+    def extcodehash_(self, global_state: GlobalState) -> List[GlobalState]:
+        """
+
+        :param global_state:
+        :return: List of global states possible, list of size 1 in this case
+        """
+        # TODO: To be implemented
+        address = global_state.mstate.stack.pop()
+        global_state.mstate.stack.append(
+            global_state.new_bitvec("extcodehash_{}".format(str(address)), 256)
+        )
+        return [global_state]
+
     @StateTransition()
     def extcodecopy_(self, global_state: GlobalState) -> List[GlobalState]:
         """
@@ -1270,7 +1344,7 @@ class Instruction:
 
         try:
             value_to_write = (
-                util.get_concrete_int(value) ^ 0xFF
+                util.get_concrete_int(value) % 256
             )  # type: Union[int, BitVec]
         except TypeError:  # BitVec
             value_to_write = Extract(7, 0, value)
@@ -1639,6 +1713,25 @@ class Instruction:
         state.stack.append(0)
         return [global_state]
 
+    @StateTransition()
+    def create2_(self, global_state: GlobalState) -> List[GlobalState]:
+        """
+
+        :param global_state:
+        :return:
+        """
+        # TODO: implement me
+        state = global_state.mstate
+        endowment, memory_start, memory_length, salt = (
+            state.stack.pop(),
+            state.stack.pop(),
+            state.stack.pop(),
+            state.stack.pop(),
+        )
+        # Not supported
+        state.stack.append(0)
+        return [global_state]
+
     @StateTransition()
     def return_(self, global_state: GlobalState):
         """

mythril/laser/ethereum/plugins/benchmark.py

@@ -0,0 +1,84 @@
+from mythril.laser.ethereum.svm import LaserEVM
+from time import time
+import matplotlib.pyplot as plt
+import logging
+
+log = logging.getLogger(__name__)
+
+
+class BenchmarkPlugin:
+    """Benchmark Plugin
+
+    This plugin aggregates the following information:
+    - duration
+    - code coverage over time
+    - final code coverage
+    - total number of executed instructions
+
+    """
+
+    def __init__(self, name=None):
+        """Creates BenchmarkPlugin
+
+        :param name: name of this benchmark, used for storing the results
+        """
+        self.nr_of_executed_insns = 0
+        self.begin = None
+        self.end = None
+        self.coverage = {}
+        self.name = name
+
+    def initialize(self, symbolic_vm: LaserEVM):
+        """Initializes the BenchmarkPlugin
+
+        Introduces hooks in symbolic_vm to track the desired values
+        :param symbolic_vm: Symbolic virtual machine to analyze
+        """
+        self._reset()
+
+        @symbolic_vm.laser_hook("execute_state")
+        def execute_state_hook(_):
+            current_time = time() - self.begin
+            self.nr_of_executed_insns += 1
+
+            for key, value in symbolic_vm.coverage.items():
+                try:
+                    self.coverage[key][current_time] = sum(value[1]) * 100 / value[0]
+                except KeyError:
+                    self.coverage[key] = {}
+                    self.coverage[key][current_time] = sum(value[1]) * 100 / value[0]
+
+        @symbolic_vm.laser_hook("start_sym_exec")
+        def start_sym_exec_hook():
+            self.begin = time()
+
+        @symbolic_vm.laser_hook("stop_sym_exec")
+        def stop_sym_exec_hook():
+            self.end = time()
+
+            self._write_to_graph()
+            self._store_report()
+
+    def _reset(self):
+        """Reset this plugin"""
+        self.nr_of_executed_insns = 0
+        self.begin = None
+        self.end = None
+        self.coverage = {}
+
+    def _store_report(self):
+        """Store the results of this plugin"""
+        pass
+
+    def _write_to_graph(self):
+        """Write the coverage results to a graph"""
+        traces = []
+        for byte_code, trace_data in self.coverage.items():
+            traces += [list(trace_data.keys()), list(trace_data.values()), "r--"]
+
+        plt.plot(*traces)
+        plt.axis([0, self.end - self.begin, 0, 100])
+        plt.xlabel("Duration (seconds)")
+        plt.ylabel("Coverage (percentage)")
+
+        plt.savefig("{}.png".format(self.name))

mythril/laser/ethereum/state/constraints.py

@@ -1,7 +1,7 @@
 """This module contains the class used to represent state-change constraints in
 the call graph."""
 
-from mythril.laser.smt import Solver, Bool
+from mythril.laser.smt import Solver, Bool, symbol_factory
 
 from typing import Iterable, List, Optional, Union
 from z3 import unsat
@@ -40,6 +40,11 @@ class Constraints(list):
         solver = Solver()
         solver.set_timeout(self._default_timeout)
         for constraint in self[:]:
+            constraint = (
+                symbol_factory.Bool(constraint)
+                if isinstance(constraint, bool)
+                else constraint
+            )
             solver.add(constraint)
         self._is_possible = solver.check() != unsat
         return self._is_possible

mythril/laser/ethereum/state/global_state.py

@@ -111,7 +111,7 @@ class GlobalState:
         """
         return self.get_current_instruction()
 
-    def new_bitvec(self, name: str, size=256) -> BitVec:
+    def new_bitvec(self, name: str, size=256, annotations=None) -> BitVec:
         """
 
         :param name:
@@ -119,7 +119,9 @@ class GlobalState:
         :return:
         """
         transaction_id = self.current_transaction.id
-        return symbol_factory.BitVecSym("{}_{}".format(transaction_id, name), size)
+        return symbol_factory.BitVecSym(
+            "{}_{}".format(transaction_id, name), size, annotations=annotations
+        )
 
     def annotate(self, annotation: StateAnnotation) -> None:
         """

mythril/laser/ethereum/state/memory.py

@@ -29,6 +29,11 @@ class Memory:
         """
         return len(self._memory)
 
+    def __copy__(self):
+        copy = Memory()
+        copy._memory = self._memory[:]
+        return copy
+
     def extend(self, size):
         """
 

mythril/laser/ethereum/state/world_state.py

@@ -117,7 +117,7 @@ class WorldState:
         :return:
         """
         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(40)])
             if address not in self.accounts.keys():
                 return address
 

mythril/laser/ethereum/svm.py

@@ -3,7 +3,6 @@ import logging
 from collections import defaultdict
 from copy import copy
 from datetime import datetime, timedelta
-from functools import reduce
 from typing import Callable, Dict, DefaultDict, List, Tuple, Union
 
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
@@ -15,7 +14,7 @@ from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
 from mythril.laser.ethereum.time_handler import time_handler
-from mythril.laser.ethereum.plugins.signals import PluginSignal, PluginSkipWorldState
+from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
 from mythril.laser.ethereum.transaction import (
     ContractCreationTransaction,
     TransactionEndSignal,
@@ -97,6 +96,10 @@ class LaserEVM:
         self.post_hooks = defaultdict(list)  # type: DefaultDict[str, List[Callable]]
 
         self._add_world_state_hooks = []  # type: List[Callable]
+        self._execute_state_hooks = []  # type: List[Callable]
+        self._start_sym_exec_hooks = []  # type: List[Callable]
+        self._stop_sym_exec_hooks = []  # type: List[Callable]
+
         self.iprof = InstructionProfiler() if enable_iprof else None
 
         log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
@@ -119,6 +122,8 @@ class LaserEVM:
         :param contract_name:
         """
         log.debug("Starting LASER execution")
+        for hook in self._start_sym_exec_hooks:
+            hook()
 
         time_handler.start_execution(self.execution_timeout)
         self.time = datetime.now()
@@ -161,6 +166,9 @@ class LaserEVM:
         if self.iprof is not None:
             log.info("Instruction Statistics:\n{}".format(self.iprof))
 
+        for hook in self._stop_sym_exec_hooks:
+            hook()
+
     def _execute_transactions(self, address):
         """This function executes multiple transactions on the address based on
         the coverage.
@@ -262,6 +270,10 @@ class LaserEVM:
         :param global_state:
         :return:
         """
+        # Execute hooks
+        for hook in self._execute_state_hooks:
+            hook(global_state)
+
         instructions = global_state.environment.code.instruction_list
 
         try:
@@ -509,6 +521,12 @@ class LaserEVM:
         """registers the hook with this Laser VM"""
         if hook_type == "add_world_state":
             self._add_world_state_hooks.append(hook)
+        elif hook_type == "execute_state":
+            self._execute_state_hooks.append(hook)
+        elif hook_type == "start_sym_exec":
+            self._start_sym_exec_hooks.append(hook)
+        elif hook_type == "stop_sym_exec":
+            self._stop_sym_exec_hooks.append(hook)
         else:
             raise ValueError(
                 "Invalid hook type %s. Must be one of {add_world_state}", hook_type

mythril/laser/ethereum/taint_analysis.py

@@ -449,5 +449,6 @@ class TaintRunner:
         "MSIZE": (0, 1),
         "GAS": (0, 1),
         "CREATE": (3, 1),
+        "CREATE2": (4, 1),
         "RETURN": (2, 0),
     }

mythril/laser/smt/__init__.py

@@ -13,11 +13,13 @@ from mythril.laser.smt.bitvec import (
     BVAddNoOverflow,
     BVMulNoOverflow,
     BVSubNoUnderflow,
+    LShR,
 )
+from mythril.laser.smt.bitvecfunc import BitVecFunc
 from mythril.laser.smt.expression import Expression, simplify
 from mythril.laser.smt.bool import Bool, is_true, is_false, Or, Not, And
 from mythril.laser.smt.array import K, Array, BaseArray
-from mythril.laser.smt.solver import Solver, Optimize
+from mythril.laser.smt.solver import Solver, Optimize, SolverStatistics
 from mythril.laser.smt.model import Model
 
 from typing import Union, Any, Optional, List, TypeVar, Generic
@@ -64,6 +66,44 @@ class SymbolFactory(Generic[T, U]):
         """
         raise NotImplementedError()
 
+    @staticmethod
+    def BitVecFuncVal(
+        value: int,
+        func_name: str,
+        size: int,
+        annotations: Annotations = None,
+        input_: Union[int, "BitVec"] = None,
+    ) -> BitVecFunc:
+        """Creates a new bit vector function with a symbolic value.
+
+        :param value: The concrete value to set the bit vector to
+        :param func_name: The name of the bit vector function
+        :param size: The size of the bit vector
+        :param annotations: The annotations to initialize the bit vector with
+        :param input_: The input to the bit vector function
+        :return: The freshly created bit vector function
+        """
+        raise NotImplementedError()
+
+    @staticmethod
+    def BitVecFuncSym(
+        name: str,
+        func_name: str,
+        size: int,
+        annotations: Annotations = None,
+        input_: Union[int, "BitVec"] = None,
+    ) -> BitVecFunc:
+        """Creates a new bit vector function with a symbolic value.
+
+        :param name: The name of the symbolic bit vector
+        :param func_name: The name of the bit vector function
+        :param size: The size of the bit vector
+        :param annotations: The annotations to initialize the bit vector with
+        :param input_: The input to the bit vector function
+        :return: The freshly created bit vector function
+        """
+        raise NotImplementedError()
+
 
 class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]):
     """
@@ -94,6 +134,30 @@ class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]):
         raw = z3.BitVec(name, size)
         return BitVec(raw, annotations)
 
+    @staticmethod
+    def BitVecFuncVal(
+        value: int,
+        func_name: str,
+        size: int,
+        annotations: Annotations = None,
+        input_: Union[int, "BitVec"] = None,
+    ) -> BitVecFunc:
+        """Creates a new bit vector function with a concrete value."""
+        raw = z3.BitVecVal(value, size)
+        return BitVecFunc(raw, func_name, input_, annotations)
+
+    @staticmethod
+    def BitVecFuncSym(
+        name: str,
+        func_name: str,
+        size: int,
+        annotations: Annotations = None,
+        input_: Union[int, "BitVec"] = None,
+    ) -> BitVecFunc:
+        """Creates a new bit vector function with a symbolic value."""
+        raw = z3.BitVec(name, size)
+        return BitVecFunc(raw, func_name, input_, annotations)
+
 
 class _Z3SymbolFactory(SymbolFactory[z3.BoolRef, z3.BitVecRef]):
     """

mythril/laser/smt/bitvec.py

@@ -1,10 +1,10 @@
 """This module provides classes for an SMT abstraction of bit vectors."""
 
-from typing import Union, overload, List, cast, Any, Optional
-
+from typing import Union, overload, List, cast, Any, Optional, Callable
+from operator import lshift, rshift
 import z3
 
-from mythril.laser.smt.bool import Bool
+from mythril.laser.smt.bool import Bool, And, Or
 from mythril.laser.smt.expression import Expression
 
 Annotations = List[Any]
@@ -15,7 +15,7 @@ Annotations = List[Any]
 class BitVec(Expression[z3.BitVecRef]):
     """A bit vector symbol."""
 
-    def __init__(self, raw: z3.BitVecRef, annotations: Optional[Annotations]=None):
+    def __init__(self, raw: z3.BitVecRef, annotations: Optional[Annotations] = None):
         """
 
         :param raw:
@@ -56,6 +56,8 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other + self
         if isinstance(other, int):
             return BitVec(self.raw + other, annotations=self.annotations)
 
@@ -68,7 +70,8 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
-
+        if isinstance(other, BitVecFunc):
+            return other - self
         if isinstance(other, int):
             return BitVec(self.raw - other, annotations=self.annotations)
 
@@ -81,6 +84,8 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other * self
         union = self.annotations + other.annotations
         return BitVec(self.raw * other.raw, annotations=union)
 
@@ -90,6 +95,8 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other / self
         union = self.annotations + other.annotations
         return BitVec(self.raw / other.raw, annotations=union)
 
@@ -99,8 +106,10 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other & self
         if not isinstance(other, BitVec):
-            other = BitVec(z3.BitVecVal(other, 256))
+            other = BitVec(z3.BitVecVal(other, self.size()))
         union = self.annotations + other.annotations
         return BitVec(self.raw & other.raw, annotations=union)
 
@@ -110,6 +119,8 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other | self
         union = self.annotations + other.annotations
         return BitVec(self.raw | other.raw, annotations=union)
 
@@ -119,6 +130,8 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other ^ self
         union = self.annotations + other.annotations
         return BitVec(self.raw ^ other.raw, annotations=union)
 
@@ -128,6 +141,8 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other > self
         union = self.annotations + other.annotations
         return Bool(self.raw < other.raw, annotations=union)
 
@@ -137,6 +152,8 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other < self
         union = self.annotations + other.annotations
         return Bool(self.raw > other.raw, annotations=union)
 
@@ -165,8 +182,12 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other == self
         if not isinstance(other, BitVec):
-            return Bool(cast(z3.BoolRef, self.raw == other), annotations=self.annotations)
+            return Bool(
+                cast(z3.BoolRef, self.raw == other), annotations=self.annotations
+            )
 
         union = self.annotations + other.annotations
         # MYPY: fix complaints due to z3 overriding __eq__
@@ -179,13 +200,95 @@ class BitVec(Expression[z3.BitVecRef]):
         :param other:
         :return:
         """
+        if isinstance(other, BitVecFunc):
+            return other != self
         if not isinstance(other, BitVec):
-            return Bool(cast(z3.BoolRef, self.raw != other), annotations=self.annotations)
+            return Bool(
+                cast(z3.BoolRef, self.raw != other), annotations=self.annotations
+            )
 
         union = self.annotations + other.annotations
         # MYPY: fix complaints due to z3 overriding __eq__
         return Bool(cast(z3.BoolRef, self.raw != other.raw), annotations=union)
 
+    def _handle_shift(self, other: Union[int, "BitVec"], operator: Callable) -> "BitVec":
+        """
+        Handles shift
+        :param other: The other BitVector
+        :param operator: The shift operator
+        :return: the resulting output
+        """
+        if isinstance(other, BitVecFunc):
+            return operator(other, self)
+        if not isinstance(other, BitVec):
+            return BitVec(
+                operator(self.raw, other), annotations=self.annotations
+            )
+        union = self.annotations + other.annotations
+        return BitVec(operator(self.raw, other.raw), annotations=union)
+
+    def __lshift__(self, other: Union[int, "BitVec"]) -> "BitVec":
+        """
+
+        :param other:
+        :return:
+        """
+        return self._handle_shift(other, lshift)
+
+    def __rshift__(self, other: Union[int, "BitVec"]) -> "BitVec":
+        """
+
+        :param other:
+        :return:
+        """
+        return self._handle_shift(other, rshift)
+
+
+def _comparison_helper(
+    a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool
+) -> Bool:
+    annotations = a.annotations + b.annotations
+    if isinstance(a, BitVecFunc):
+        if not a.symbolic and not b.symbolic:
+            return Bool(operation(a.raw, b.raw), annotations=annotations)
+
+        if (
+            not isinstance(b, BitVecFunc)
+            or not a.func_name
+            or not a.input_
+            or not a.func_name == b.func_name
+        ):
+            return Bool(z3.BoolVal(default_value), annotations=annotations)
+
+        return And(
+            Bool(operation(a.raw, b.raw), annotations=annotations),
+            a.input_ == b.input_ if inputs_equal else a.input_ != b.input_,
+        )
+
+    return Bool(operation(a.raw, b.raw), annotations)
+
+
+def _arithmetic_helper(a: BitVec, b: BitVec, operation: Callable) -> BitVec:
+    raw = operation(a.raw, b.raw)
+    union = a.annotations + b.annotations
+
+    if isinstance(a, BitVecFunc) and isinstance(b, BitVecFunc):
+        return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union)
+    elif isinstance(a, BitVecFunc):
+        return BitVecFunc(
+            raw=raw, func_name=a.func_name, input_=a.input_, annotations=union
+        )
+    elif isinstance(b, BitVecFunc):
+        return BitVecFunc(
+            raw=raw, func_name=b.func_name, input_=b.input_, annotations=union
+        )
+
+    return BitVec(raw, annotations=union)
+
+
+def LShR(a: BitVec, b: BitVec):
+    return _arithmetic_helper(a, b, z3.LShR)
+
 
 def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> BitVec:
     """Create an if-then-else expression.
@@ -195,6 +298,8 @@ def If(a: Union[Bool, bool], b: Union[BitVec, int], c: Union[BitVec, int]) -> Bi
     :param c:
     :return:
     """
+    # TODO: Handle BitVecFunc
+
     if not isinstance(a, Bool):
         a = Bool(z3.BoolVal(a))
     if not isinstance(b, BitVec):
@@ -212,19 +317,17 @@ def UGT(a: BitVec, b: BitVec) -> Bool:
     :param b:
     :return:
     """
-    annotations = a.annotations + b.annotations
-    return Bool(z3.UGT(a.raw, b.raw), annotations)
+    return _comparison_helper(a, b, z3.UGT, default_value=False, inputs_equal=False)
 
 
-def UGE(a: BitVec, b:BitVec) -> Bool:
+def UGE(a: BitVec, b: BitVec) -> Bool:
     """Create an unsigned greater or equals expression.
 
     :param a:
     :param b:
     :return:
     """
-    annotations = a.annotations + b.annotations
-    return Bool(z3.UGE(a.raw, b.raw), annotations)
+    return Or(UGT(a, b), a == b)
 
 
 def ULT(a: BitVec, b: BitVec) -> Bool:
@@ -234,8 +337,17 @@ def ULT(a: BitVec, b: BitVec) -> Bool:
     :param b:
     :return:
     """
-    annotations = a.annotations + b.annotations
-    return Bool(z3.ULT(a.raw, b.raw), annotations)
+    return _comparison_helper(a, b, z3.ULT, default_value=False, inputs_equal=False)
+
+
+def ULE(a: BitVec, b: BitVec) -> Bool:
+    """Create an unsigned less than expression.
+
+    :param a:
+    :param b:
+    :return:
+    """
+    return Or(ULT(a, b), a == b)
 
 
 @overload
@@ -252,7 +364,6 @@ def Concat(*args: Union[BitVec, List[BitVec]]) -> BitVec:
     :param args:
     :return:
     """
-
     # The following statement is used if a list is provided as an argument to concat
     if len(args) == 1 and isinstance(args[0], list):
         bvs = args[0]  # type: List[BitVec]
@@ -261,8 +372,18 @@ def Concat(*args: Union[BitVec, List[BitVec]]) -> BitVec:
 
     nraw = z3.Concat([a.raw for a in bvs])
     annotations = []  # type: Annotations
+    bitvecfunc = False
     for bv in bvs:
         annotations += bv.annotations
+        if isinstance(bv, BitVecFunc):
+            bitvecfunc = True
+
+    if bitvecfunc:
+        # Is there a better value to set func_name and input to in this case?
+        return BitVecFunc(
+            raw=nraw, func_name=None, input_=None, annotations=annotations
+        )
+
     return BitVec(nraw, annotations)
 
 
@@ -274,7 +395,14 @@ def Extract(high: int, low: int, bv: BitVec) -> BitVec:
     :param bv:
     :return:
     """
-    return BitVec(z3.Extract(high, low, bv.raw), annotations=bv.annotations)
+    raw = z3.Extract(high, low, bv.raw)
+    if isinstance(bv, BitVecFunc):
+        # Is there a better value to set func_name and input to in this case?
+        return BitVecFunc(
+            raw=raw, func_name=None, input_=None, annotations=bv.annotations
+        )
+
+    return BitVec(raw, annotations=bv.annotations)
 
 
 def URem(a: BitVec, b: BitVec) -> BitVec:
@@ -284,8 +412,7 @@ def URem(a: BitVec, b: BitVec) -> BitVec:
     :param b:
     :return:
     """
-    union = a.annotations + b.annotations
-    return BitVec(z3.URem(a.raw, b.raw), annotations=union)
+    return _arithmetic_helper(a, b, z3.URem)
 
 
 def SRem(a: BitVec, b: BitVec) -> BitVec:
@@ -295,8 +422,7 @@ def SRem(a: BitVec, b: BitVec) -> BitVec:
     :param b:
     :return:
     """
-    union = a.annotations + b.annotations
-    return BitVec(z3.SRem(a.raw, b.raw), annotations=union)
+    return _arithmetic_helper(a, b, z3.SRem)
 
 
 def UDiv(a: BitVec, b: BitVec) -> BitVec:
@@ -306,8 +432,7 @@ def UDiv(a: BitVec, b: BitVec) -> BitVec:
     :param b:
     :return:
     """
-    union = a.annotations + b.annotations
-    return BitVec(z3.UDiv(a.raw, b.raw), annotations=union)
+    return _arithmetic_helper(a, b, z3.UDiv)
 
 
 def Sum(*args: BitVec) -> BitVec:
@@ -315,11 +440,26 @@ def Sum(*args: BitVec) -> BitVec:
 
     :return:
     """
-    nraw = z3.Sum([a.raw for a in args])
+    raw = z3.Sum([a.raw for a in args])
     annotations = []  # type: Annotations
+    bitvecfuncs = []
+
     for bv in args:
         annotations += bv.annotations
-    return BitVec(nraw, annotations)
+        if isinstance(bv, BitVecFunc):
+            bitvecfuncs.append(bv)
+
+    if len(bitvecfuncs) >= 2:
+        return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=annotations)
+    elif len(bitvecfuncs) == 1:
+        return BitVecFunc(
+            raw=raw,
+            func_name=bitvecfuncs[0].func_name,
+            input_=bitvecfuncs[0].input_,
+            annotations=annotations,
+        )
+
+    return BitVec(raw, annotations)
 
 
 def BVAddNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
@@ -353,7 +493,9 @@ def BVMulNoOverflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool)
     return Bool(z3.BVMulNoOverflow(a.raw, b.raw, signed))
 
 
-def BVSubNoUnderflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool) -> Bool:
+def BVSubNoUnderflow(
+    a: Union[BitVec, int], b: Union[BitVec, int], signed: bool
+) -> Bool:
     """Creates predicate that verifies that the subtraction doesn't overflow.
 
     :param a:
@@ -367,3 +509,7 @@ def BVSubNoUnderflow(a: Union[BitVec, int], b: Union[BitVec, int], signed: bool)
         b = BitVec(z3.BitVecVal(b, 256))
 
     return Bool(z3.BVSubNoUnderflow(a.raw, b.raw, signed))
+
+
+# TODO: Fix circular import issues
+from mythril.laser.smt.bitvecfunc import BitVecFunc

mythril/laser/smt/bitvecfunc.py

@@ -0,0 +1,225 @@
+from typing import Optional, Union, cast, Callable
+
+import z3
+
+from mythril.laser.smt.bitvec import BitVec, Bool, And, Annotations
+from mythril.laser.smt.bool import Or
+
+import operator
+
+
+def _arithmetic_helper(
+    a: "BitVecFunc", b: Union[BitVec, int], operation: Callable
+) -> "BitVecFunc":
+    """
+    Helper function for arithmetic operations on BitVecFuncs.
+
+    :param a: The BitVecFunc to perform the operation on.
+    :param b: A BitVec or int to perform the operation on.
+    :param operation: The arithmetic operation to perform.
+    :return: The resulting BitVecFunc
+    """
+    if isinstance(b, int):
+        b = BitVec(z3.BitVecVal(b, a.size()))
+
+    raw = operation(a.raw, b.raw)
+    union = a.annotations + b.annotations
+
+    if isinstance(b, BitVecFunc):
+        # TODO: Find better value to set input and name to in this case?
+        return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union)
+
+    return BitVecFunc(
+        raw=raw, func_name=a.func_name, input_=a.input_, annotations=union
+    )
+
+
+def _comparison_helper(
+    a: "BitVecFunc",
+    b: Union[BitVec, int],
+    operation: Callable,
+    default_value: bool,
+    inputs_equal: bool,
+) -> Bool:
+    """
+    Helper function for comparison operations with BitVecFuncs.
+
+    :param a: The BitVecFunc to compare.
+    :param b: A BitVec or int to compare to.
+    :param operation: The comparison operation to perform.
+    :return: The resulting Bool
+    """
+    # Is there some hack for gt/lt comparisons?
+    if isinstance(b, int):
+        b = BitVec(z3.BitVecVal(b, a.size()))
+
+    union = a.annotations + b.annotations
+
+    if not a.symbolic and not b.symbolic:
+        return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union)
+
+    if (
+        not isinstance(b, BitVecFunc)
+        or not a.func_name
+        or not a.input_
+        or not a.func_name == b.func_name
+    ):
+        return Bool(z3.BoolVal(default_value), annotations=union)
+
+    return And(
+        Bool(cast(z3.BoolRef, operation(a.raw, b.raw)), annotations=union),
+        a.input_ == b.input_ if inputs_equal else a.input_ != b.input_,
+    )
+
+
+class BitVecFunc(BitVec):
+    """A bit vector function symbol. Used in place of functions like sha3."""
+
+    def __init__(
+        self,
+        raw: z3.BitVecRef,
+        func_name: Optional[str],
+        input_: Union[int, "BitVec"] = None,
+        annotations: Optional[Annotations] = None,
+    ):
+        """
+
+        :param raw: The raw bit vector symbol
+        :param func_name: The function name. e.g. sha3
+        :param input: The input to the functions
+        :param annotations: The annotations the BitVecFunc should start with
+        """
+
+        self.func_name = func_name
+        self.input_ = input_
+        super().__init__(raw, annotations)
+
+    def __add__(self, other: Union[int, "BitVec"]) -> "BitVecFunc":
+        """Create an addition expression.
+
+        :param other: The int or BitVec to add to this BitVecFunc
+        :return: The resulting BitVecFunc
+        """
+        return _arithmetic_helper(self, other, operator.add)
+
+    def __sub__(self, other: Union[int, "BitVec"]) -> "BitVecFunc":
+        """Create a subtraction expression.
+
+        :param other: The int or BitVec to subtract from this BitVecFunc
+        :return: The resulting BitVecFunc
+        """
+        return _arithmetic_helper(self, other, operator.sub)
+
+    def __mul__(self, other: "BitVec") -> "BitVecFunc":
+        """Create a multiplication expression.
+
+        :param other: The int or BitVec to multiply to this BitVecFunc
+        :return: The resulting BitVecFunc
+        """
+        return _arithmetic_helper(self, other, operator.mul)
+
+    def __truediv__(self, other: "BitVec") -> "BitVecFunc":
+        """Create a signed division expression.
+
+        :param other: The int or BitVec to divide this BitVecFunc by
+        :return: The resulting BitVecFunc
+        """
+        return _arithmetic_helper(self, other, operator.truediv)
+
+    def __and__(self, other: Union[int, "BitVec"]) -> "BitVecFunc":
+        """Create an and expression.
+
+        :param other: The int or BitVec to and with this BitVecFunc
+        :return: The resulting BitVecFunc
+        """
+        return _arithmetic_helper(self, other, operator.and_)
+
+    def __or__(self, other: "BitVec") -> "BitVecFunc":
+        """Create an or expression.
+
+        :param other: The int or BitVec to or with this BitVecFunc
+        :return: The resulting BitVecFunc
+        """
+        return _arithmetic_helper(self, other, operator.or_)
+
+    def __xor__(self, other: "BitVec") -> "BitVecFunc":
+        """Create a xor expression.
+
+        :param other: The int or BitVec to xor with this BitVecFunc
+        :return: The resulting BitVecFunc
+        """
+        return _arithmetic_helper(self, other, operator.xor)
+
+    def __lt__(self, other: "BitVec") -> Bool:
+        """Create a signed less than expression.
+
+        :param other: The int or BitVec to compare to this BitVecFunc
+        :return: The resulting Bool
+        """
+        return _comparison_helper(
+            self, other, operator.lt, default_value=False, inputs_equal=False
+        )
+
+    def __gt__(self, other: "BitVec") -> Bool:
+        """Create a signed greater than expression.
+
+        :param other: The int or BitVec to compare to this BitVecFunc
+        :return: The resulting Bool
+        """
+        return _comparison_helper(
+            self, other, operator.gt, default_value=False, inputs_equal=False
+        )
+
+    def __le__(self, other: "BitVec") -> Bool:
+        """Create a signed less than or equal to expression.
+
+        :param other: The int or BitVec to compare to this BitVecFunc
+        :return: The resulting Bool
+        """
+        return Or(self < other, self == other)
+
+    def __ge__(self, other: "BitVec") -> Bool:
+        """Create a signed greater than or equal to expression.
+
+        :param other: The int or BitVec to compare to this BitVecFunc
+        :return: The resulting Bool
+        """
+        return Or(self > other, self == other)
+
+    # MYPY: fix complains about overriding __eq__
+    def __eq__(self, other: Union[int, "BitVec"]) -> Bool:  # type: ignore
+        """Create an equality expression.
+
+        :param other: The int or BitVec to compare to this BitVecFunc
+        :return: The resulting Bool
+        """
+        return _comparison_helper(
+            self, other, operator.eq, default_value=False, inputs_equal=True
+        )
+
+    # MYPY: fix complains about overriding __ne__
+    def __ne__(self, other: Union[int, "BitVec"]) -> Bool:  # type: ignore
+        """Create an inequality expression.
+
+        :param other: The int or BitVec to compare to this BitVecFunc
+        :return: The resulting Bool
+        """
+        return _comparison_helper(
+            self, other, operator.eq, default_value=True, inputs_equal=False
+        )
+
+    def __lshift__(self, other: Union[int, "BitVec"]) -> "BitVec":
+        """
+        Left shift operation
+        :param other: The int or BitVec to shift on
+        :return The resulting left shifted output
+        """
+        return _arithmetic_helper(self, other, operator.lshift)
+
+    def __rshift__(self, other: Union[int, "BitVec"]) -> "BitVec":
+        """
+        Right shift operation
+        :param other: The int or BitVec to shift on
+        :return The resulting right shifted output:
+        """
+        return _arithmetic_helper(self, other, operator.rshift)

mythril/laser/smt/solver/__init__.py

@@ -0,0 +1,3 @@
+from mythril.laser.smt.solver.solver import Solver, Optimize, BaseSolver
+from mythril.laser.smt.solver.independence_solver import IndependenceSolver
+from mythril.laser.smt.solver.solver_statistics import SolverStatistics

mythril/laser/smt/solver/independence_solver.py

@@ -2,6 +2,8 @@ import z3
 
 from mythril.laser.smt.model import Model
 from mythril.laser.smt.bool import Bool
+from mythril.laser.smt.solver.solver_statistics import stat_smt_query
+
 from typing import Set, Tuple, Dict, List, cast
 
 
@@ -63,7 +65,7 @@ class DependenceMap:
             relevant_buckets.add(new_bucket)
             new_bucket = self._merge_buckets(relevant_buckets)
 
-        for variable in variables:
+        for variable in new_bucket.variables:
             self.variable_map[str(variable)] = new_bucket
 
     def _merge_buckets(self, bucket_list: Set[DependenceBucket]) -> DependenceBucket:
@@ -118,6 +120,7 @@ class IndependenceSolver:
         ]  # type: List[z3.BoolRef]
         self.constraints.extend(raw_constraints)
 
+    @stat_smt_query
     def check(self) -> z3.CheckSatResult:
         """Returns z3 smt check result. """
         dependence_map = DependenceMap()

mythril/laser/smt/solver/solver.py

@@ -1,11 +1,13 @@
 """This module contains an abstract SMT representation of an SMT solver."""
+import os
+import sys
 import z3
 from typing import Union, cast, TypeVar, Generic, List, Sequence
 
 from mythril.laser.smt.expression import Expression
 from mythril.laser.smt.model import Model
 from mythril.laser.smt.bool import Bool
-
+from mythril.laser.smt.solver.solver_statistics import stat_smt_query
 
 T = TypeVar("T", bound=Union[z3.Solver, z3.Optimize])
 
@@ -42,12 +44,17 @@ class BaseSolver(Generic[T]):
         """
         self.add(*constraints)
 
+    @stat_smt_query
     def check(self) -> z3.CheckSatResult:
         """Returns z3 smt check result.
-
-        :return:
+        Also suppresses the stdout when running z3 library's check() to avoid unnecessary output
+        :return: The evaluated result which is either of sat, unsat or unknown
         """
-        return self.raw.check()
+        old_stdout = sys.stdout
+        sys.stdout = open(os.devnull, "w")
+        evaluate = self.raw.check()
+        sys.stdout = old_stdout
+        return evaluate
 
     def model(self) -> Model:
         """Returns z3 model for a solution.

mythril/laser/smt/solver/solver_statistics.py

@@ -0,0 +1,43 @@
+from time import time
+
+from mythril.support.support_utils import Singleton
+
+from typing import Callable
+
+
+def stat_smt_query(func: Callable):
+    """Measures statistics for annotated smt query check function"""
+    stat_store = SolverStatistics()
+
+    def function_wrapper(*args, **kwargs):
+        if not stat_store.enabled:
+            return func(*args, **kwargs)
+
+        stat_store.query_count += 1
+        begin = time()
+
+        result = func(*args, **kwargs)
+
+        end = time()
+        stat_store.solver_time += end - begin
+
+        return result
+
+    return function_wrapper
+
+
+class SolverStatistics(object, metaclass=Singleton):
+    """ Solver Statistics Class
+
+    Keeps track of the important statistics around smt queries
+    """
+
+    def __init__(self):
+        self.enabled = False
+        self.query_count = 0
+        self.solver_time = 0
+
+    def __repr__(self):
+        return "Query count: {} \nSolver time: {}".format(
+            self.query_count, self.solver_time
+        )

mythril/mythril.py

@@ -0,0 +1,721 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+"""mythril.py: Bug hunting on the Ethereum blockchain
+
+   http://www.github.com/b-mueller/mythril
+"""
+
+import codecs
+import logging
+import os
+import platform
+import re
+import traceback
+from pathlib import Path
+from shutil import copyfile
+from configparser import ConfigParser
+
+import solc
+from ethereum import utils
+from solc.exceptions import SolcError
+
+from mythril.ethereum import util
+from mythril.ethereum.evmcontract import EVMContract
+from mythril.ethereum.interface.rpc.client import EthJsonRpc
+from mythril.ethereum.interface.rpc.exceptions import ConnectionError
+from mythril.solidity.soliditycontract import SolidityContract, get_contracts_from_file
+from mythril.support import signatures
+from mythril.support.source_support import Source
+from mythril.support.loader import DynLoader
+from mythril.exceptions import CompilerError, NoContractFoundError, CriticalError
+from mythril.analysis.symbolic import SymExecWrapper
+from mythril.analysis.callgraph import generate_graph
+from mythril.analysis.traceexplore import get_serializable_statespace
+from mythril.analysis.security import fire_lasers, retrieve_callback_issues
+from mythril.analysis.report import Report
+from mythril.support.truffle import analyze_truffle_project
+from mythril.ethereum.interface.leveldb.client import EthLevelDB
+from mythril.laser.smt import SolverStatistics
+from mythril.support.start_time import StartTime
+
+
+log = logging.getLogger(__name__)
+
+
+class Mythril(object):
+    """Mythril main interface class.
+
+    1. create mythril object
+    2. set rpc or leveldb interface if needed
+    3. load contracts (from solidity, bytecode, address)
+    4. fire_lasers
+
+    .. code-block:: python
+
+        mythril = Mythril()
+        mythril.set_api_rpc_infura()
+
+        # (optional) other API adapters
+        mythril.set_api_rpc(args)
+        mythril.set_api_rpc_localhost()
+        mythril.set_api_leveldb(path)
+
+        # (optional) other func
+        mythril.analyze_truffle_project(args)
+        mythril.search_db(args)
+
+        # load contract
+        mythril.load_from_bytecode(bytecode)
+        mythril.load_from_address(address)
+        mythril.load_from_solidity(solidity_file)
+
+        # analyze
+        print(mythril.fire_lasers(args).as_text())
+
+        # (optional) graph
+        for contract in mythril.contracts:
+            # prints html or save it to file
+            print(mythril.graph_html(args))
+
+        # (optional) other funcs
+        mythril.dump_statespaces(args)
+        mythril.disassemble(contract)
+        mythril.get_state_variable_from_storage(args)
+    """
+
+    def __init__(
+        self,
+        solv=None,
+        solc_args=None,
+        dynld=False,
+        enable_online_lookup=False,
+        onchain_storage_access=True,
+    ):
+
+        self.solv = solv
+        self.solc_args = solc_args
+        self.dynld = dynld
+        self.onchain_storage_access = onchain_storage_access
+        self.enable_online_lookup = enable_online_lookup
+
+        self.mythril_dir = self._init_mythril_dir()
+
+        # tries mythril_dir/signatures.db by default (provide path= arg to make this configurable)
+        self.sigs = signatures.SignatureDB(
+            enable_online_lookup=self.enable_online_lookup
+        )
+
+        self.solc_binary = self._init_solc_binary(solv)
+        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_db = None  # ethereum LevelDB client
+
+        self.contracts = []  # loaded contracts
+
+    @staticmethod
+    def _init_mythril_dir():
+        try:
+            mythril_dir = os.environ["MYTHRIL_DIR"]
+        except KeyError:
+            mythril_dir = os.path.join(os.path.expanduser("~"), ".mythril")
+
+        if not os.path.exists(mythril_dir):
+            # Initialize data directory
+            log.info("Creating mythril data directory")
+            os.mkdir(mythril_dir)
+
+        db_path = str(Path(mythril_dir) / "signatures.db")
+        if not os.path.exists(db_path):
+            # if the default mythril dir doesn't contain a signature DB
+            # initialize it with the default one from the project root
+            asset_dir = Path(__file__).parent / "support" / "assets"
+            copyfile(str(asset_dir / "signatures.db"), db_path)
+
+        return mythril_dir
+
+    def _init_config(self):
+        """If no config file exists, create it and add default options.
+
+        Default LevelDB path is specified based on OS
+        dynamic loading is set to infura by default in the file
+        Returns: leveldb directory
+        """
+
+        system = platform.system().lower()
+        leveldb_fallback_dir = os.path.expanduser("~")
+        if system.startswith("darwin"):
+            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"
+            )
+        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):
+            log.info("No config file found. Creating default: " + self.config_path)
+            open(self.config_path, "a").close()
+
+        config = ConfigParser(allow_no_value=True)
+        config.optionxform = str
+        config.read(self.config_path, "utf-8")
+        if "defaults" not in config.sections():
+            self._add_default_options(config)
+
+        if not config.has_option("defaults", "leveldb_dir"):
+            self._add_leveldb_option(config, leveldb_fallback_dir)
+
+        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:
+            config.write(fp)
+
+        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")
+
+    @staticmethod
+    def _add_leveldb_option(config, leveldb_fallback_dir):
+        config.set("defaults", "#Default chaindata locations:")
+        config.set("defaults", "#– Mac: ~/Library/Ethereum/geth/chaindata")
+        config.set("defaults", "#– Linux: ~/.ethereum/geth/chaindata")
+        config.set(
+            "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 Rpc use "
+            "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):
+        """
+
+        :param args:
+        :param kwargs:
+        :return:
+        """
+        return analyze_truffle_project(
+            self.sigs, *args, **kwargs
+        )  # just passthru by passing signatures for now
+
+    @staticmethod
+    def _init_solc_binary(version):
+        """Figure out solc binary and version.
+
+        Only proper versions are supported. No nightlies, commits etc (such as available in remix).
+        """
+
+        if not version:
+            return os.environ.get("SOLC") or "solc"
+
+        # tried converting input to semver, seemed not necessary so just slicing for now
+        main_version = solc.main.get_solc_version_string()
+        main_version_number = re.match(r"\d+.\d+.\d+", main_version)
+        if main_version is None:
+            raise CriticalError(
+                "Could not extract solc version from string {}".format(main_version)
+            )
+        if version == main_version_number:
+            log.info("Given version matches installed version")
+            solc_binary = os.environ.get("SOLC") or "solc"
+        else:
+            solc_binary = util.solc_exists(version)
+            if solc_binary:
+                log.info("Given version is already installed")
+            else:
+                try:
+                    solc.install_solc("v" + version)
+                    solc_binary = util.solc_exists(version)
+                    if not solc_binary:
+                        raise SolcError()
+                except SolcError:
+                    raise CriticalError(
+                        "There was an error when trying to install the specified solc version"
+                    )
+
+            log.info("Setting the compiler to %s", solc_binary)
+
+        return solc_binary
+
+    def set_api_leveldb(self, leveldb):
+        """
+
+        :param leveldb:
+        :return:
+        """
+        self.eth_db = EthLevelDB(leveldb)
+        self.eth = self.eth_db
+        return self.eth
+
+    def set_api_rpc_infura(self):
+        """Set the RPC mode to INFURA on mainnet."""
+        self.eth = EthJsonRpc("mainnet.infura.io", 443, True)
+        log.info("Using INFURA for RPC queries")
+
+    def set_api_rpc(self, rpc=None, rpctls=False):
+        """
+
+        :param rpc:
+        :param rpctls:
+        """
+        if rpc == "ganache":
+            rpcconfig = ("localhost", 8545, False)
+        else:
+            m = re.match(r"infura-(.*)", rpc)
+            if m and m.group(1) in ["mainnet", "rinkeby", "kovan", "ropsten"]:
+                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'"
+                    )
+
+        if rpcconfig:
+            self.eth = EthJsonRpc(rpcconfig[0], int(rpcconfig[1]), rpcconfig[2])
+            log.info("Using RPC settings: %s" % str(rpcconfig))
+        else:
+            raise CriticalError("Invalid RPC settings, check help for details.")
+
+    def set_api_rpc_localhost(self):
+        """Set the RPC mode to a local instance."""
+        self.eth = EthJsonRpc("localhost", 8545)
+        log.info("Using default RPC settings: http://localhost:8545")
+
+    def set_api_from_config_path(self):
+        """Set the RPC mode based on a given config file."""
+        config = ConfigParser(allow_no_value=False)
+        config.optionxform = str
+        config.read(self.config_path, "utf-8")
+        if config.has_option("defaults", "dynamic_loading"):
+            dynamic_loading = config.get("defaults", "dynamic_loading")
+        else:
+            dynamic_loading = "infura"
+        if dynamic_loading == "infura":
+            self.set_api_rpc_infura()
+        elif dynamic_loading == "localhost":
+            self.set_api_rpc_localhost()
+        else:
+            self.set_api_rpc(dynamic_loading)
+
+    def search_db(self, search):
+        """
+
+        :param search:
+        """
+
+        def search_callback(_, address, balance):
+            """
+
+            :param _:
+            :param address:
+            :param balance:
+            """
+            print("Address: " + address + ", balance: " + str(balance))
+
+        try:
+            self.eth_db.search(search, search_callback)
+
+        except SyntaxError:
+            raise CriticalError("Syntax error in search expression.")
+
+    def contract_hash_to_address(self, hash):
+        """
+
+        :param hash:
+        """
+        if not re.match(r"0x[a-fA-F0-9]{64}", hash):
+            raise CriticalError("Invalid address hash. Expected format is '0x...'.")
+
+        print(self.eth_db.contract_hash_to_address(hash))
+
+    def load_from_bytecode(self, code, bin_runtime=False, address=None):
+        """
+
+        :param code:
+        :param bin_runtime:
+        :param address:
+        :return:
+        """
+        if address is None:
+            address = util.get_indexed_address(0)
+        if bin_runtime:
+            self.contracts.append(
+                EVMContract(
+                    code=code,
+                    name="MAIN",
+                    enable_online_lookup=self.enable_online_lookup,
+                )
+            )
+        else:
+            self.contracts.append(
+                EVMContract(
+                    creation_code=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):
+        """
+
+        :param address:
+        :return:
+        """
+        if not re.match(r"0x[a-fA-F0-9]{40}", address):
+            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))
+        except ConnectionError:
+            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."
+                )
+            else:
+                self.contracts.append(
+                    EVMContract(
+                        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):
+        """
+
+        :param solidity_files:
+        :return:
+        """
+        address = util.get_indexed_address(0)
+        contracts = []
+        for file in solidity_files:
+            if ":" in file:
+                file, contract_name = file.split(":")
+            else:
+                contract_name = None
+
+            file = os.path.expanduser(file)
+
+            try:
+                # import signatures from solidity source
+                self.sigs.import_solidity_file(
+                    file, solc_binary=self.solc_binary, solc_args=self.solc_args
+                )
+                if contract_name is not None:
+                    contract = SolidityContract(
+                        input_file=file,
+                        name=contract_name,
+                        solc_args=self.solc_args,
+                        solc_binary=self.solc_binary,
+                    )
+                    self.contracts.append(contract)
+                    contracts.append(contract)
+                else:
+                    for contract in get_contracts_from_file(
+                        input_file=file,
+                        solc_args=self.solc_args,
+                        solc_binary=self.solc_binary,
+                    ):
+                        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:
+                log.error(
+                    "The file " + file + " does not contain a compilable contract."
+                )
+
+        return address, contracts
+
+    def dump_statespace(
+        self,
+        strategy,
+        contract,
+        address=None,
+        max_depth=None,
+        execution_timeout=None,
+        create_timeout=None,
+        enable_iprof=False,
+    ):
+        """
+
+        :param strategy:
+        :param contract:
+        :param address:
+        :param max_depth:
+        :param execution_timeout:
+        :param create_timeout:
+        :return:
+        """
+        sym = SymExecWrapper(
+            contract,
+            address,
+            strategy,
+            dynloader=DynLoader(
+                self.eth,
+                storage_loading=self.onchain_storage_access,
+                contract_loading=self.dynld,
+            ),
+            max_depth=max_depth,
+            execution_timeout=execution_timeout,
+            create_timeout=create_timeout,
+            enable_iprof=enable_iprof,
+        )
+
+        return get_serializable_statespace(sym)
+
+    def graph_html(
+        self,
+        strategy,
+        contract,
+        address,
+        max_depth=None,
+        enable_physics=False,
+        phrackify=False,
+        execution_timeout=None,
+        create_timeout=None,
+        enable_iprof=False,
+    ):
+        """
+
+        :param strategy:
+        :param contract:
+        :param address:
+        :param max_depth:
+        :param enable_physics:
+        :param phrackify:
+        :param execution_timeout:
+        :param create_timeout:
+        :return:
+        """
+        sym = SymExecWrapper(
+            contract,
+            address,
+            strategy,
+            dynloader=DynLoader(
+                self.eth,
+                storage_loading=self.onchain_storage_access,
+                contract_loading=self.dynld,
+            ),
+            max_depth=max_depth,
+            execution_timeout=execution_timeout,
+            create_timeout=create_timeout,
+            enable_iprof=enable_iprof,
+        )
+        return generate_graph(sym, physics=enable_physics, phrackify=phrackify)
+
+    def fire_lasers(
+        self,
+        strategy,
+        contracts=None,
+        address=None,
+        modules=None,
+        verbose_report=False,
+        max_depth=None,
+        execution_timeout=None,
+        create_timeout=None,
+        transaction_count=None,
+        enable_iprof=False,
+    ):
+        """
+
+        :param strategy:
+        :param contracts:
+        :param address:
+        :param modules:
+        :param verbose_report:
+        :param max_depth:
+        :param execution_timeout:
+        :param create_timeout:
+        :param transaction_count:
+        :return:
+        """
+        all_issues = []
+        SolverStatistics().enabled = True
+        exceptions = []
+        for contract in contracts or self.contracts:
+            StartTime()  # Reinitialize start time for new contracts
+            try:
+                sym = SymExecWrapper(
+                    contract,
+                    address,
+                    strategy,
+                    dynloader=DynLoader(
+                        self.eth,
+                        storage_loading=self.onchain_storage_access,
+                        contract_loading=self.dynld,
+                    ),
+                    max_depth=max_depth,
+                    execution_timeout=execution_timeout,
+                    create_timeout=create_timeout,
+                    transaction_count=transaction_count,
+                    modules=modules,
+                    compulsory_statespace=False,
+                    enable_iprof=enable_iprof,
+                )
+                issues = fire_lasers(sym, modules)
+            except KeyboardInterrupt:
+                log.critical("Keyboard Interrupt")
+                issues = retrieve_callback_issues(modules)
+            except Exception:
+                log.critical(
+                    "Exception occurred, aborting analysis. Please report this issue to the Mythril GitHub page.\n"
+                    + traceback.format_exc()
+                )
+                issues = retrieve_callback_issues(modules)
+                exceptions.append(traceback.format_exc())
+            for issue in issues:
+                issue.add_code_info(contract)
+
+            all_issues += issues
+            log.info("Solver statistics: \n{}".format(str(SolverStatistics())))
+
+        source_data = Source()
+        source_data.get_source_from_contracts_list(self.contracts)
+        # Finally, output the results
+        report = Report(verbose_report, source_data, exceptions=exceptions)
+        for issue in all_issues:
+            report.append_issue(issue)
+
+        return report
+
+    def get_state_variable_from_storage(self, address, params=None):
+        """
+
+        :param address:
+        :param params:
+        :return:
+        """
+        if params is None:
+            params = []
+        (position, length, mappings) = (0, 1, [])
+        try:
+            if params[0] == "mapping":
+                if len(params) < 3:
+                    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_formatted = utils.rzpad(key, 32)
+                    mappings.append(
+                        int.from_bytes(
+                            utils.sha3(key_formatted + position_formatted),
+                            byteorder="big",
+                        )
+                    )
+
+                length = len(mappings)
+                if length == 1:
+                    position = mappings[0]
+
+            else:
+                if len(params) >= 4:
+                    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 = int.from_bytes(
+                        utils.sha3(position_formatted), byteorder="big"
+                    )
+
+        except ValueError:
+            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)
+                    )
+                )
+            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),
+                            )
+                        )
+                else:
+                    for i in range(position, position + length):
+                        outtxt.append(
+                            "{}: {}".format(
+                                hex(i), self.eth.eth_getStorageAt(address, i)
+                            )
+                        )
+        except FileNotFoundError as 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."
+            )
+        return "\n".join(outtxt)
+
+    @staticmethod
+    def disassemble(contract):
+        """
+
+        :param contract:
+        :return:
+        """
+        return contract.get_easm()
+
+    @staticmethod
+    def hash_for_function_signature(sig):
+        """
+
+        :param sig:
+        :return:
+        """
+        return "0x%s" % utils.sha3(sig)[:4].hex()

mythril/mythril/mythril_analyzer.py

@@ -14,6 +14,8 @@ from mythril.analysis.traceexplore import get_serializable_statespace
 from mythril.analysis.security import fire_lasers, retrieve_callback_issues
 from mythril.analysis.report import Report, Issue
 from mythril.ethereum.evmcontract import EVMContract
+from mythril.laser.smt import SolverStatistics
+from mythril.support.start_time import StartTime
 
 log = logging.getLogger(__name__)
 
@@ -122,7 +124,10 @@ class MythrilAnalyzer:
         :return: The Report class which contains the all the issues/vulnerabilities
         """
         all_issues = []  # type: List[Issue]
+        SolverStatistics().enabled = True
+        exceptions = []
         for contract in self.contracts:
+            StartTime()  # Reinitialize start time for new contracts
             try:
                 sym = SymExecWrapper(
                     contract,
@@ -151,16 +156,17 @@ class MythrilAnalyzer:
                     + traceback.format_exc()
                 )
                 issues = retrieve_callback_issues(modules)
-
+                exceptions.append(traceback.format_exc())
             for issue in issues:
                 issue.add_code_info(contract)
 
             all_issues += issues
+            log.info("Solver statistics: \n{}".format(str(SolverStatistics())))
 
         source_data = Source()
         source_data.get_source_from_contracts_list(self.contracts)
         # Finally, output the results
-        report = Report(verbose_report, source_data)
+        report = Report(verbose_report, source_data, exceptions=exceptions)
         for issue in all_issues:
             report.append_issue(issue)
 

mythril/solidity/soliditycontract.py

@@ -161,6 +161,9 @@ class SolidityContract(EVMContract):
 
             if len(mapping) > 2 and len(mapping[2]) > 0:
                 idx = int(mapping[2])
+            if idx == -1:
+                lineno = None
+            else:
                 lineno = (
                     self.solidity_files[idx]
                     .data.encode("utf-8")[0:offset]

mythril/support/opcodes.py

@@ -0,0 +1,94 @@
+# This pyethereum opcodes file with added opcodes
+from typing import Dict, Tuple
+
+opcodes = {
+    0x00: ("STOP", 0, 0, 0),
+    0x01: ("ADD", 2, 1, 3),
+    0x02: ("MUL", 2, 1, 5),
+    0x03: ("SUB", 2, 1, 3),
+    0x04: ("DIV", 2, 1, 5),
+    0x05: ("SDIV", 2, 1, 5),
+    0x06: ("MOD", 2, 1, 5),
+    0x07: ("SMOD", 2, 1, 5),
+    0x08: ("ADDMOD", 3, 1, 8),
+    0x09: ("MULMOD", 3, 1, 8),
+    0x0A: ("EXP", 2, 1, 10),
+    0x0B: ("SIGNEXTEND", 2, 1, 5),
+    0x10: ("LT", 2, 1, 3),
+    0x11: ("GT", 2, 1, 3),
+    0x12: ("SLT", 2, 1, 3),
+    0x13: ("SGT", 2, 1, 3),
+    0x14: ("EQ", 2, 1, 3),
+    0x15: ("ISZERO", 1, 1, 3),
+    0x16: ("AND", 2, 1, 3),
+    0x17: ("OR", 2, 1, 3),
+    0x18: ("XOR", 2, 1, 3),
+    0x19: ("NOT", 1, 1, 3),
+    0x1A: ("BYTE", 2, 1, 3),
+    0x1B: ("SHL", 2, 1, 3),
+    0x1C: ("SHR", 2, 1, 3),
+    0x1D: ("SAR", 2, 1, 3),
+    0x20: ("SHA3", 2, 1, 30),
+    0x30: ("ADDRESS", 0, 1, 2),
+    0x31: ("BALANCE", 1, 1, 20),  # now 400
+    0x32: ("ORIGIN", 0, 1, 2),
+    0x33: ("CALLER", 0, 1, 2),
+    0x34: ("CALLVALUE", 0, 1, 2),
+    0x35: ("CALLDATALOAD", 1, 1, 3),
+    0x36: ("CALLDATASIZE", 0, 1, 2),
+    0x37: ("CALLDATACOPY", 3, 0, 3),
+    0x38: ("CODESIZE", 0, 1, 2),
+    0x39: ("CODECOPY", 3, 0, 3),
+    0x3A: ("GASPRICE", 0, 1, 2),
+    0x3B: ("EXTCODESIZE", 1, 1, 20),  # now 700
+    0x3C: ("EXTCODECOPY", 4, 0, 20),  # now 700
+    0x3D: ("RETURNDATASIZE", 0, 1, 2),
+    0x3E: ("RETURNDATACOPY", 3, 0, 3),
+    0x3F: ("EXTCODEHASH", 3, 0, 3),
+    0x40: ("BLOCKHASH", 1, 1, 20),
+    0x41: ("COINBASE", 0, 1, 2),
+    0x42: ("TIMESTAMP", 0, 1, 2),
+    0x43: ("NUMBER", 0, 1, 2),
+    0x44: ("DIFFICULTY", 0, 1, 2),
+    0x45: ("GASLIMIT", 0, 1, 2),
+    0x50: ("POP", 1, 0, 2),
+    0x51: ("MLOAD", 1, 1, 3),
+    0x52: ("MSTORE", 2, 0, 3),
+    0x53: ("MSTORE8", 2, 0, 3),
+    0x54: ("SLOAD", 1, 1, 50),  # 200 now
+    0x55: ("SSTORE", 2, 0, 0),
+    0x56: ("JUMP", 1, 0, 8),
+    0x57: ("JUMPI", 2, 0, 10),
+    0x58: ("PC", 0, 1, 2),
+    0x59: ("MSIZE", 0, 1, 2),
+    0x5A: ("GAS", 0, 1, 2),
+    0x5B: ("JUMPDEST", 0, 0, 1),
+    0xA0: ("LOG0", 2, 0, 375),
+    0xA1: ("LOG1", 3, 0, 750),
+    0xA2: ("LOG2", 4, 0, 1125),
+    0xA3: ("LOG3", 5, 0, 1500),
+    0xA4: ("LOG4", 6, 0, 1875),
+    0xF0: ("CREATE", 3, 1, 32000),
+    0xF1: ("CALL", 7, 1, 40),  # 700 now
+    0xF2: ("CALLCODE", 7, 1, 40),  # 700 now
+    0xF3: ("RETURN", 2, 0, 0),
+    0xF4: ("DELEGATECALL", 6, 1, 40),  # 700 now
+    0xF5: ("CREATE2", 3, 1, 32000),
+    0xFA: ("STATICCALL", 6, 1, 40),
+    0xFD: ("REVERT", 2, 0, 0),
+    0xFF: ("SUICIDE", 1, 0, 0),  # 5000 now
+}  # type: Dict[int, Tuple[str, int, int, int]]
+
+opcodesMetropolis = {0x3D, 0x3E, 0xFA, 0xFD}
+
+for i in range(1, 33):
+    opcodes[0x5F + i] = ("PUSH" + str(i), 0, 1, 3)
+
+for i in range(1, 17):
+    opcodes[0x7F + i] = ("DUP" + str(i), i, i + 1, 3)
+    opcodes[0x8F + i] = ("SWAP" + str(i), i + 1, i + 1, 3)
+
+reverse_opcodes = {}
+for o in opcodes:
+    vars()[opcodes[o][0]] = opcodes[o]
+    reverse_opcodes[opcodes[o][0]] = o

mythril/support/start_time.py

@@ -0,0 +1,9 @@
+from time import time
+from mythril.support.support_utils import Singleton
+
+
+class StartTime(metaclass=Singleton):
+    """Maintains the start time of the current contract in execution"""
+
+    def __init__(self):
+        self.global_start_time = time()

mythril/support/truffle.py

@@ -5,6 +5,7 @@ import logging
 import os
 import re
 import sys
+import warnings
 from pathlib import PurePath
 
 from ethereum.utils import sha3
@@ -20,12 +21,24 @@ from mythril.solidity.soliditycontract import SourceMapping
 log = logging.getLogger(__name__)
 
 
+def format_Warning(message, category, filename, lineno, line=""):
+    return "{}: {}\n\n".format(str(filename), str(message))
+
+
+warnings.formatwarning = format_Warning
+
+
 def analyze_truffle_project(sigs, args):
     """
 
     :param sigs:
     :param args:
     """
+    warnings.warn(
+        "The option --truffle is being deprecated, Please use the truffle-security plugin, https://github.com/ConsenSys/truffle-security",
+        FutureWarning,
+    )
+
     project_root = os.getcwd()
 
     build_dir = os.path.join(project_root, "build", "contracts")
@@ -181,6 +194,9 @@ def get_mappings(source, deployed_source_map):
         if len(mapping) > 2 and len(mapping[2]) > 0:
             idx = int(mapping[2])
 
+        if idx == -1:
+            lineno = None
+        else:
             lineno = source.encode("utf-8")[0:offset].count("\n".encode("utf-8")) + 1
         prev_item = item
 

mythril/version.py

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

solidity_examples/BECToken.sol

@@ -1,4 +1,3 @@
-pragma solidity 0.5.0;
 
 /**
  * @title SafeMath

solidity_examples/WalletLibrary.sol

@@ -212,7 +212,7 @@ contract WalletLibrary is WalletEvents {
   }
 
   // throw unless the contract is not yet initialized.
-  modifier only_uninitialized { require(m_numOwners > 0); _; }
+  modifier only_uninitialized { require(m_numOwners == 0); _; }
 
   // constructor - just pass on the owner array to the multiowned and
   // the limit to daylimit

solidity_examples/rubixi.sol

@@ -34,7 +34,7 @@ contract Rubixi {
 
     //Fee functions for creator
     function collectAllFees() public onlyowner {
-        require(collectedFees == 0);
+        require(collectedFees > 0);
         creator.transfer(collectedFees);
         collectedFees = 0;
     }
@@ -43,14 +43,14 @@ contract Rubixi {
         _amt *= 1 ether;
         if (_amt > collectedFees) collectAllFees();
 
-        require(collectedFees == 0);
+        require(collectedFees > 0);
 
         creator.transfer(_amt);
         collectedFees -= _amt;
     }
 
     function collectPercentOfFees(uint _pcent) public onlyowner {
-        require(collectedFees == 0 || _pcent > 100);
+        require(collectedFees > 0 && _pcent <= 100);
 
         uint feesToCollect = collectedFees / 100 * _pcent;
         creator.transfer(feesToCollect);
@@ -63,12 +63,12 @@ contract Rubixi {
     }
 
     function changeMultiplier(uint _mult) public onlyowner {
-        require(_mult > 300 || _mult < 120);
+        require(_mult <= 300 &&  _mult >= 120);
         pyramidMultiplier = _mult;
     }
 
     function changeFeePercentage(uint _fee) public onlyowner {
-        require(_fee > 10);
+        require(_fee <= 10);
         feePercent = _fee;
     }
 

tests/__init__.py

@@ -14,6 +14,9 @@ TESTDATA_OUTPUTS_CURRENT_LASER_RESULT = TESTDATA / "outputs_current_laser_result
 TESTDATA_OUTPUTS_EXPECTED_LASER_RESULT = TESTDATA / "outputs_expected_laser_result"
 MYTHRIL_DIR = TESTS_DIR / "mythril_dir"
 
+TESTDATA_OUTPUTS_CURRENT.mkdir(exist_ok=True)
+TESTDATA_OUTPUTS_CURRENT_LASER_RESULT.mkdir(exist_ok=True)
+
 
 class BaseTestCase(TestCase):
     def setUp(self):

tests/instructions/sar_test.py

@@ -0,0 +1,148 @@
+import pytest
+
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.machine_state import MachineState
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.instructions import Instruction
+from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
+from mythril.laser.smt import symbol_factory, simplify
+
+
+def get_state():
+    active_account = Account("0x0", code=Disassembly("60606040"))
+    environment = Environment(active_account, None, None, None, None, None)
+    state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
+    state.transaction_stack.append(
+        (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
+    )
+    return state
+
+
+BVV = symbol_factory.BitVecVal
+BV = symbol_factory.BitVecSym
+
+test_data = (
+    ([BVV(-1, 256), BVV(1, 256)], BVV(-1, 256)),
+    ([BVV(23, 256), BVV(257, 256)], BVV(0, 256)),
+    ([BVV(23, 256), BVV(30, 256)], BVV(23 >> 30, 256)),
+    ([BVV(-10, 256), BVV(10, 256)], BVV(-1, 256)),
+    ([BV("a", 256), BV("b", 256)], BV("a", 256) >> BV("b", 256)),
+)
+
+
+@pytest.mark.parametrize("inputs,output", test_data)
+def test_sar(inputs, output):
+    # Arrange
+    state = get_state()
+
+    state.mstate.stack = inputs
+    instruction = Instruction("sar", dynamic_loader=None)
+
+    # Act
+    new_state = instruction.evaluate(state)[0]
+
+    # Assert
+    assert simplify(new_state.mstate.stack[-1]) == output
+
+
+@pytest.mark.parametrize(
+    # Test cases from https://github.com/ethereum/EIPs/blob/master/EIPS/eip-145.md#sar-arithmetic-shift-right
+    "val1, val2, expected ",
+    (
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+            "0x00",
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+        ),
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+            "0x01",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+            "0x01",
+            "0xc000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+            "0xff",
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+            "0x0100",
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+            "0x0101",
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x00",
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x01",
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0xff",
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x0100",
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+            "0x01",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x4000000000000000000000000000000000000000000000000000000000000000",
+            "0xfe",
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+        ),
+        (
+            "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0xf8",
+            "0x000000000000000000000000000000000000000000000000000000000000007f",
+        ),
+        (
+            "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0xfe",
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+        ),
+        (
+            "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0xff",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x0100",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+    ),
+)
+def test_concrete_sar(val1, val2, expected):
+    # Arrange
+    state = get_state()
+    state.mstate.stack = [BVV(int(val1, 16), 256), BVV(int(val2, 16), 256)]
+    expected = BVV(int(expected, 16), 256)
+    instruction = Instruction("sar", dynamic_loader=None)
+
+    # Act
+    new_state = instruction.evaluate(state)[0]
+
+    # Assert
+    assert simplify(new_state.mstate.stack[-1]) == expected

tests/instructions/shl_test.py

@@ -0,0 +1,123 @@
+import pytest
+
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.machine_state import MachineState
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.instructions import Instruction
+from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
+from mythril.laser.smt import symbol_factory, simplify
+
+
+def get_state():
+    active_account = Account("0x0", code=Disassembly("60606040"))
+    environment = Environment(active_account, None, None, None, None, None)
+    state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
+    state.transaction_stack.append(
+        (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
+    )
+    return state
+
+
+BVV = symbol_factory.BitVecVal
+BV = symbol_factory.BitVecSym
+
+test_data = (
+    ([BVV(2, 256), BVV(2, 256)], BVV(8, 256)),
+    ([BVV(23, 256), BVV(257, 256)], BVV(0, 256)),
+    ([BVV(23, 256), BVV(30, 256)], BVV(23 * (1 << 30), 256)),
+    ([BV("a", 256), BVV(270, 256)], 0),
+    ([BV("a", 256), BV("b", 256)], BV("a", 256) << BV("b", 256)),
+)
+
+
+@pytest.mark.parametrize("inputs,output,", test_data)
+def test_shl(inputs, output):
+    # Arrange
+    state = get_state()
+
+    state.mstate.stack = inputs
+    instruction = Instruction("shl", dynamic_loader=None)
+
+    # Act
+    new_state = instruction.evaluate(state)[0]
+
+    # Assert
+    assert simplify(new_state.mstate.stack[-1]) == output
+
+
+@pytest.mark.parametrize(
+    # Testcases from https://github.com/ethereum/EIPs/blob/master/EIPS/eip-145.md#shl-shift-left
+    "val1, val2, expected",
+    (
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+            "0x00",
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+        ),
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+            "0x01",
+            "0x0000000000000000000000000000000000000000000000000000000000000002",
+        ),
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+            "0xff",
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+            "0x0100",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+            "0x0101",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x00",
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x01",
+            "0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0xff",
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x0100",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+            "0x01",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x01",
+            "0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe",
+        ),
+    ),
+)
+def test_concrete_shl(val1, val2, expected):
+    # Arrange
+    state = get_state()
+    state.mstate.stack = [BVV(int(val1, 16), 256), BVV(int(val2, 16), 256)]
+    expected = BVV(int(expected, 16), 256)
+    instruction = Instruction("shl", dynamic_loader=None)
+
+    # Act
+    new_state = instruction.evaluate(state)[0]
+
+    # Assert
+    assert simplify(new_state.mstate.stack[-1]) == expected

tests/instructions/shr_test.py

@@ -0,0 +1,125 @@
+import pytest
+
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.machine_state import MachineState
+from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.instructions import Instruction
+from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction
+from mythril.laser.smt import symbol_factory, simplify, LShR
+
+
+def get_state():
+    active_account = Account("0x0", code=Disassembly("60606040"))
+    environment = Environment(active_account, None, None, None, None, None)
+    state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
+    state.transaction_stack.append(
+        (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
+    )
+    return state
+
+
+BVV = symbol_factory.BitVecVal
+BV = symbol_factory.BitVecSym
+
+test_data = (
+    ([BVV(33, 256), BVV(4, 256)], BVV(2, 256)),
+    ([BVV(1 << 100, 256), BVV(257, 256)], BVV(0, 256)),
+    ([BVV(23233, 256), BVV(10, 256)], BVV(23233 // (1 << 10), 256)),
+    ([BV("a", 256), BVV(270, 256)], 0),
+    (
+        [BV("a", 256), BV("b", 256)],
+        LShR(BV("a", 256), BV("b", 256)),
+    ),  # Current approximate specs
+)
+
+
+@pytest.mark.parametrize("inputs,output,", test_data)
+def test_shr(inputs, output):
+    # Arrange
+    state = get_state()
+
+    state.mstate.stack = inputs
+    instruction = Instruction("shr", dynamic_loader=None)
+
+    # Act
+    new_state = instruction.evaluate(state)[0]
+
+    # Assert
+    assert simplify(new_state.mstate.stack[-1]) == output
+
+
+@pytest.mark.parametrize(
+    # Cases: https://github.com/ethereum/EIPs/blob/master/EIPS/eip-145.md#shr-logical-shift-right
+    "val1, val2, expected",
+    (
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+            "0x00",
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+        ),
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+            "0x01",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+            "0x01",
+            "0x4000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+            "0xff",
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+        ),
+        (
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+            "0x0100",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x8000000000000000000000000000000000000000000000000000000000000000",
+            "0x0101",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x00",
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x01",
+            "0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0xff",
+            "0x0000000000000000000000000000000000000000000000000000000000000001",
+        ),
+        (
+            "0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff",
+            "0x0100",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+        (
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+            "0x01",
+            "0x0000000000000000000000000000000000000000000000000000000000000000",
+        ),
+    ),
+)
+def test_concrete_shr(val1, val2, expected):
+    state = get_state()
+    state.mstate.stack = [BVV(int(val1, 16), 256), BVV(int(val2, 16), 256)]
+    expected = BVV(int(expected, 16), 256)
+    instruction = Instruction("shr", dynamic_loader=None)
+
+    # Act
+    new_state = instruction.evaluate(state)[0]
+
+    # Assert
+    assert simplify(new_state.mstate.stack[-1]) == expected

tests/laser/smt/bitvecfunc_test.py

@@ -0,0 +1,82 @@
+from mythril.laser.smt import Solver, symbol_factory, bitvec
+import z3
+import pytest
+
+import operator
+
+
+@pytest.mark.parametrize(
+    "operation,expected",
+    [
+        (operator.add, z3.unsat),
+        (operator.sub, z3.unsat),
+        (operator.and_, z3.sat),
+        (operator.or_, z3.sat),
+        (operator.xor, z3.unsat),
+    ],
+)
+def test_bitvecfunc_arithmetic(operation, expected):
+    # Arrange
+    s = Solver()
+
+    input_ = symbol_factory.BitVecVal(1, 8)
+    bvf = symbol_factory.BitVecFuncSym("bvf", "sha3", 256, input_=input_)
+
+    x = symbol_factory.BitVecSym("x", 256)
+    y = symbol_factory.BitVecSym("y", 256)
+
+    # Act
+    s.add(x != y)
+    s.add(operation(bvf, x) == operation(y, bvf))
+
+    # Assert
+    assert s.check() == expected
+
+
+@pytest.mark.parametrize(
+    "operation,expected",
+    [
+        (operator.eq, z3.sat),
+        (operator.ne, z3.unsat),
+        (operator.lt, z3.unsat),
+        (operator.le, z3.sat),
+        (operator.gt, z3.unsat),
+        (operator.ge, z3.sat),
+        (bitvec.UGT, z3.unsat),
+        (bitvec.UGE, z3.sat),
+        (bitvec.ULT, z3.unsat),
+        (bitvec.ULE, z3.sat),
+    ],
+)
+def test_bitvecfunc_bitvecfunc_comparison(operation, expected):
+    # Arrange
+    s = Solver()
+
+    input1 = symbol_factory.BitVecSym("input1", 256)
+    input2 = symbol_factory.BitVecSym("input2", 256)
+    bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
+    bvf2 = symbol_factory.BitVecFuncSym("bvf2", "sha3", 256, input_=input2)
+
+    # Act
+    s.add(operation(bvf1, bvf2))
+    s.add(input1 == input2)
+
+    # Assert
+    assert s.check() == expected
+
+
+def test_bitvecfunc_bitvecfuncval_comparison():
+    # Arrange
+    s = Solver()
+
+    input1 = symbol_factory.BitVecSym("input1", 256)
+    input2 = symbol_factory.BitVecVal(1337, 256)
+    bvf1 = symbol_factory.BitVecFuncSym("bvf1", "sha3", 256, input_=input1)
+    bvf2 = symbol_factory.BitVecFuncVal(12345678910, "sha3", 256, input_=input2)
+
+    # Act
+    s.add(bvf1 == bvf2)
+
+    # Assert
+    assert s.check() == z3.sat
+    assert s.model().eval(input2.raw) == 1337

tests/laser/smt/independece_solver_test.py

@@ -1,4 +1,4 @@
-from mythril.laser.smt.independence_solver import (
+from mythril.laser.smt.solver.independence_solver import (
     _get_expr_variables,
     DependenceBucket,
     DependenceMap,

tests/report_test.py

@@ -18,7 +18,7 @@ def _fix_debug_data(json_str):
     read_json = json.loads(json_str)
     for issue in read_json["issues"]:
         issue["debug"] = "<DEBUG-DATA>"
-    return json.dumps(read_json, sort_keys=True)
+    return json.dumps(read_json, sort_keys=True, indent=4)
 
 
 def _generate_report(input_file):

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

@@ -1 +1,110 @@
-{"error": null, "issues": [{"address": 661, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "thisisfine()", "max_gas_used": 1254, "min_gas_used": 643, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 661, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "thisisfine()", "max_gas_used": 35972, "min_gas_used": 1361, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 779, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "callstoredaddress()", "max_gas_used": 1298, "min_gas_used": 687, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 779, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "callstoredaddress()", "max_gas_used": 36016, "min_gas_used": 1405, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 858, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "reentrancy()", "max_gas_used": 1320, "min_gas_used": 709, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 858, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "reentrancy()", "max_gas_used": 61052, "min_gas_used": 6441, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 912, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.", "function": "calluseraddress(address)", "max_gas_used": 616, "min_gas_used": 335, "severity": "Medium", "sourceMap": null, "swc-id": "107", "title": "External Call To User-Supplied Address"}, {"address": 912, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "calluseraddress(address)", "max_gas_used": 35336, "min_gas_used": 1055, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}], "success": true}
+{
+    "error": null,
+    "issues": [
+        {
+            "address": 661,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "function": "thisisfine()",
+            "max_gas_used": 1254,
+            "min_gas_used": 643,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "107",
+            "title": "External Call To Fixed Address"
+        },
+        {
+            "address": 661,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
+            "function": "thisisfine()",
+            "max_gas_used": 35972,
+            "min_gas_used": 1361,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "104",
+            "title": "Unchecked Call Return Value"
+        },
+        {
+            "address": 779,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "function": "callstoredaddress()",
+            "max_gas_used": 1298,
+            "min_gas_used": 687,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "107",
+            "title": "External Call To Fixed Address"
+        },
+        {
+            "address": 779,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
+            "function": "callstoredaddress()",
+            "max_gas_used": 36016,
+            "min_gas_used": 1405,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "104",
+            "title": "Unchecked Call Return Value"
+        },
+        {
+            "address": 858,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "function": "reentrancy()",
+            "max_gas_used": 1320,
+            "min_gas_used": 709,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "107",
+            "title": "External Call To Fixed Address"
+        },
+        {
+            "address": 858,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
+            "function": "reentrancy()",
+            "max_gas_used": 61052,
+            "min_gas_used": 6441,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "104",
+            "title": "Unchecked Call Return Value"
+        },
+        {
+            "address": 912,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
+            "function": "calluseraddress(address)",
+            "max_gas_used": 616,
+            "min_gas_used": 335,
+            "severity": "Medium",
+            "sourceMap": null,
+            "swc-id": "107",
+            "title": "External Call To User-Supplied Address"
+        },
+        {
+            "address": 912,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
+            "function": "calluseraddress(address)",
+            "max_gas_used": 35336,
+            "min_gas_used": 1055,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "104",
+            "title": "Unchecked Call Return Value"
+        }
+    ],
+    "success": true
+}

tests/testdata/outputs_expected/calls.sol.o.jsonv2

@@ -1,132 +1 @@
-[
-    {
-        "issues": [
-            {
-                "description": {
-                    "head": "The contract executes an external message call.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "661:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-107",
-                "swcTitle": "Reentrancy"
-            },
-            {
-                "description": {
-                    "head": "The contract executes an external message call.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "779:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-107",
-                "swcTitle": "Reentrancy"
-            },
-            {
-                "description": {
-                    "head": "The contract executes an external message call.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "858:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-107",
-                "swcTitle": "Reentrancy"
-            },
-            {
-                "description": {
-                    "head": "A call to a user-supplied address is executed.",
-                    "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "912:1:0"
-                    }
-                ],
-                "severity": "Medium",
-                "swcID": "SWC-107",
-                "swcTitle": "Reentrancy"
-            },
-            {
-                "description": {
-                    "head": "The return value of a message call is not checked.",
-                    "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "661:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-104",
-                "swcTitle": "Unchecked Call Return Value"
-            },
-            {
-                "description": {
-                    "head": "The return value of a message call is not checked.",
-                    "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "779:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-104",
-                "swcTitle": "Unchecked Call Return Value"
-            },
-            {
-                "description": {
-                    "head": "The return value of a message call is not checked.",
-                    "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "858:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-104",
-                "swcTitle": "Unchecked Call Return Value"
-            },
-            {
-                "description": {
-                    "head": "The return value of a message call is not checked.",
-                    "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "912:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-104",
-                "swcTitle": "Unchecked Call Return Value"
-            }
-        ],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [
-            "0x7cbb77986c6b1bf6e945cd3fba06d3ea3d28cfc49cdfdc9571ec30703ac5862f"
-        ],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [{"description": {"head": "The contract executes an external message call.", "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."}, "extra": {}, "locations": [{"sourceMap": "661:1:0"}], "severity": "Low", "swcID": "SWC-107", "swcTitle": "Reentrancy"}, {"description": {"head": "The contract executes an external message call.", "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."}, "extra": {}, "locations": [{"sourceMap": "779:1:0"}], "severity": "Low", "swcID": "SWC-107", "swcTitle": "Reentrancy"}, {"description": {"head": "The contract executes an external message call.", "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."}, "extra": {}, "locations": [{"sourceMap": "858:1:0"}], "severity": "Low", "swcID": "SWC-107", "swcTitle": "Reentrancy"}, {"description": {"head": "A call to a user-supplied address is executed.", "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."}, "extra": {}, "locations": [{"sourceMap": "912:1:0"}], "severity": "Medium", "swcID": "SWC-107", "swcTitle": "Reentrancy"}, {"description": {"head": "The return value of a message call is not checked.", "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."}, "extra": {}, "locations": [{"sourceMap": "661:1:0"}], "severity": "Low", "swcID": "SWC-104", "swcTitle": "Unchecked Call Return Value"}, {"description": {"head": "The return value of a message call is not checked.", "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."}, "extra": {}, "locations": [{"sourceMap": "779:1:0"}], "severity": "Low", "swcID": "SWC-104", "swcTitle": "Unchecked Call Return Value"}, {"description": {"head": "The return value of a message call is not checked.", "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."}, "extra": {}, "locations": [{"sourceMap": "858:1:0"}], "severity": "Low", "swcID": "SWC-104", "swcTitle": "Unchecked Call Return Value"}, {"description": {"head": "The return value of a message call is not checked.", "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."}, "extra": {}, "locations": [{"sourceMap": "912:1:0"}], "severity": "Low", "swcID": "SWC-104", "swcTitle": "Unchecked Call Return Value"}], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": ["0x7cbb77986c6b1bf6e945cd3fba06d3ea3d28cfc49cdfdc9571ec30703ac5862f"], "sourceType": "raw-bytecode"}]

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

@@ -89,7 +89,7 @@ External calls return a boolean value. If the callee contract halts with an exce
 ### Description
 
 A call to a user-supplied address is executed.
-The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 
 ## Unchecked Call Return Value
 - SWC ID: 104

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

@@ -72,7 +72,7 @@ Function name: calluseraddress(address)
 PC address: 912
 Estimated Gas Usage: 335 - 616
 A call to a user-supplied address is executed.
-The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 --------------------
 
 ==== Unchecked Call Return Value ====

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

@@ -1 +1,5 @@
-{"error": null, "issues": [], "success": true}
+{
+    "error": null,
+    "issues": [],
+    "success": true
+}

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

@@ -1,9 +1 @@
-[
-    {
-        "issues": [],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": [], "sourceType": "raw-bytecode"}]

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

@@ -1 +1,58 @@
-{"error": null, "issues": [{"address": 446, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", "function": "assert3(uint256)", "max_gas_used": 301, "min_gas_used": 206, "severity": "Low", "sourceMap": null, "swc-id": "110", "title": "Exception State"}, {"address": 484, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", "function": "arrayaccess(uint256)", "max_gas_used": 351, "min_gas_used": 256, "severity": "Low", "sourceMap": null, "swc-id": "110", "title": "Exception State"}, {"address": 506, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", "function": "divisionby0(uint256)", "max_gas_used": 367, "min_gas_used": 272, "severity": "Low", "sourceMap": null, "swc-id": "110", "title": "Exception State"}, {"address": 531, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.", "function": "assert1()", "max_gas_used": 363, "min_gas_used": 268, "severity": "Low", "sourceMap": null, "swc-id": "110", "title": "Exception State"}], "success": true}
+{
+    "error": null,
+    "issues": [
+        {
+            "address": 446,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.",
+            "function": "assert3(uint256)",
+            "max_gas_used": 301,
+            "min_gas_used": 206,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "110",
+            "title": "Exception State"
+        },
+        {
+            "address": 484,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.",
+            "function": "arrayaccess(uint256)",
+            "max_gas_used": 351,
+            "min_gas_used": 256,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "110",
+            "title": "Exception State"
+        },
+        {
+            "address": 506,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.",
+            "function": "divisionby0(uint256)",
+            "max_gas_used": 367,
+            "min_gas_used": 272,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "110",
+            "title": "Exception State"
+        },
+        {
+            "address": 531,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "A reachable exception has been detected.\nIt is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking.",
+            "function": "assert1()",
+            "max_gas_used": 363,
+            "min_gas_used": 268,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "110",
+            "title": "Exception State"
+        }
+    ],
+    "success": true
+}

tests/testdata/outputs_expected/exceptions.sol.o.jsonv2

@@ -1,72 +1 @@
-[
-    {
-        "issues": [
-            {
-                "description": {
-                    "head": "A reachable exception has been detected.",
-                    "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "446:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-110",
-                "swcTitle": "Assert Violation"
-            },
-            {
-                "description": {
-                    "head": "A reachable exception has been detected.",
-                    "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "484:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-110",
-                "swcTitle": "Assert Violation"
-            },
-            {
-                "description": {
-                    "head": "A reachable exception has been detected.",
-                    "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "506:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-110",
-                "swcTitle": "Assert Violation"
-            },
-            {
-                "description": {
-                    "head": "A reachable exception has been detected.",
-                    "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "531:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-110",
-                "swcTitle": "Assert Violation"
-            }
-        ],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [
-            "0x4a773a86bc6fb269f88bf09bb3094de29b6073cf13b1760e9d01d957f50a9dfd"
-        ],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [{"description": {"head": "A reachable exception has been detected.", "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."}, "extra": {}, "locations": [{"sourceMap": "446:1:0"}], "severity": "Low", "swcID": "SWC-110", "swcTitle": "Assert Violation"}, {"description": {"head": "A reachable exception has been detected.", "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."}, "extra": {}, "locations": [{"sourceMap": "484:1:0"}], "severity": "Low", "swcID": "SWC-110", "swcTitle": "Assert Violation"}, {"description": {"head": "A reachable exception has been detected.", "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."}, "extra": {}, "locations": [{"sourceMap": "506:1:0"}], "severity": "Low", "swcID": "SWC-110", "swcTitle": "Assert Violation"}, {"description": {"head": "A reachable exception has been detected.", "tail": "It is possible to trigger an exception (opcode 0xfe). Exceptions can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. Note that explicit `assert()` should only be used to check invariants. Use `require()` for regular input checking."}, "extra": {}, "locations": [{"sourceMap": "531:1:0"}], "severity": "Low", "swcID": "SWC-110", "swcTitle": "Assert Violation"}], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": ["0x4a773a86bc6fb269f88bf09bb3094de29b6073cf13b1760e9d01d957f50a9dfd"], "sourceType": "raw-bytecode"}]

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

@@ -1 +1,71 @@
-{"error": null, "issues": [{"address": 618, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "_function_0x141f32ff", "max_gas_used": 35865, "min_gas_used": 1113, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 618, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "Use of callcode is deprecated.\nThe callcode method executes code of another contract in the context of the caller account. Due to a bug in the implementation it does not persist sender and value over the call. It was therefore deprecated and may be removed in the future. Use the delegatecall method instead.", "function": "_function_0x141f32ff", "max_gas_used": 1141, "min_gas_used": 389, "severity": "Medium", "sourceMap": null, "swc-id": "111", "title": "Use of callcode"}, {"address": 849, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "_function_0x9b58bc26", "max_gas_used": 35922, "min_gas_used": 1170, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}, {"address": 1038, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.", "function": "_function_0xeea4c864", "max_gas_used": 1223, "min_gas_used": 471, "severity": "Medium", "sourceMap": null, "swc-id": "107", "title": "External Call To User-Supplied Address"}, {"address": 1038, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "_function_0xeea4c864", "max_gas_used": 35947, "min_gas_used": 1195, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}], "success": true}
+{
+    "error": null,
+    "issues": [
+        {
+            "address": 618,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
+            "function": "_function_0x141f32ff",
+            "max_gas_used": 35865,
+            "min_gas_used": 1113,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "104",
+            "title": "Unchecked Call Return Value"
+        },
+        {
+            "address": 618,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "Use of callcode is deprecated.\nThe callcode method executes code of another contract in the context of the caller account. Due to a bug in the implementation it does not persist sender and value over the call. It was therefore deprecated and may be removed in the future. Use the delegatecall method instead.",
+            "function": "_function_0x141f32ff",
+            "max_gas_used": 1141,
+            "min_gas_used": 389,
+            "severity": "Medium",
+            "sourceMap": null,
+            "swc-id": "111",
+            "title": "Use of callcode"
+        },
+        {
+            "address": 849,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
+            "function": "_function_0x9b58bc26",
+            "max_gas_used": 35928,
+            "min_gas_used": 1176,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "104",
+            "title": "Unchecked Call Return Value"
+        },
+        {
+            "address": 1038,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "A call to a user-supplied address is executed.\nThe callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.",
+            "function": "_function_0xeea4c864",
+            "max_gas_used": 1229,
+            "min_gas_used": 477,
+            "severity": "Medium",
+            "sourceMap": null,
+            "swc-id": "107",
+            "title": "External Call To User-Supplied Address"
+        },
+        {
+            "address": 1038,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
+            "function": "_function_0xeea4c864",
+            "max_gas_used": 35953,
+            "min_gas_used": 1201,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "104",
+            "title": "Unchecked Call Return Value"
+        }
+    ],
+    "success": true
+}

tests/testdata/outputs_expected/kinds_of_calls.sol.o.jsonv2

@@ -1,87 +1 @@
-[
-    {
-        "issues": [
-            {
-                "description": {
-                    "head": "Use of callcode is deprecated.",
-                    "tail": "The callcode method executes code of another contract in the context of the caller account. Due to a bug in the implementation it does not persist sender and value over the call. It was therefore deprecated and may be removed in the future. Use the delegatecall method instead."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "618:1:0"
-                    }
-                ],
-                "severity": "Medium",
-                "swcID": "SWC-111",
-                "swcTitle": "Use of Deprecated Solidity Functions"
-            },
-            {
-                "description": {
-                    "head": "A call to a user-supplied address is executed.",
-                    "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "1038:1:0"
-                    }
-                ],
-                "severity": "Medium",
-                "swcID": "SWC-107",
-                "swcTitle": "Reentrancy"
-            },
-            {
-                "description": {
-                    "head": "The return value of a message call is not checked.",
-                    "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "618:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-104",
-                "swcTitle": "Unchecked Call Return Value"
-            },
-            {
-                "description": {
-                    "head": "The return value of a message call is not checked.",
-                    "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "849:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-104",
-                "swcTitle": "Unchecked Call Return Value"
-            },
-            {
-                "description": {
-                    "head": "The return value of a message call is not checked.",
-                    "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "1038:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-104",
-                "swcTitle": "Unchecked Call Return Value"
-            }
-        ],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [
-            "0x6daec61d05d8f1210661e7e7d1ed6d72bd6ade639398fac1e867aff50abfc1c1"
-        ],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [{"description": {"head": "Use of callcode is deprecated.", "tail": "The callcode method executes code of another contract in the context of the caller account. Due to a bug in the implementation it does not persist sender and value over the call. It was therefore deprecated and may be removed in the future. Use the delegatecall method instead."}, "extra": {}, "locations": [{"sourceMap": "618:1:0"}], "severity": "Medium", "swcID": "SWC-111", "swcTitle": "Use of Deprecated Solidity Functions"}, {"description": {"head": "A call to a user-supplied address is executed.", "tail": "The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state."}, "extra": {}, "locations": [{"sourceMap": "1038:1:0"}], "severity": "Medium", "swcID": "SWC-107", "swcTitle": "Reentrancy"}, {"description": {"head": "The return value of a message call is not checked.", "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."}, "extra": {}, "locations": [{"sourceMap": "618:1:0"}], "severity": "Low", "swcID": "SWC-104", "swcTitle": "Unchecked Call Return Value"}, {"description": {"head": "The return value of a message call is not checked.", "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."}, "extra": {}, "locations": [{"sourceMap": "849:1:0"}], "severity": "Low", "swcID": "SWC-104", "swcTitle": "Unchecked Call Return Value"}, {"description": {"head": "The return value of a message call is not checked.", "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."}, "extra": {}, "locations": [{"sourceMap": "1038:1:0"}], "severity": "Low", "swcID": "SWC-104", "swcTitle": "Unchecked Call Return Value"}], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": ["0x6daec61d05d8f1210661e7e7d1ed6d72bd6ade639398fac1e867aff50abfc1c1"], "sourceType": "raw-bytecode"}]

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

@@ -32,7 +32,7 @@ The callcode method executes code of another contract in the context of the call
 - Contract: Unknown
 - Function name: `_function_0x9b58bc26`
 - PC address: 849
-- Estimated Gas Usage: 1170 - 35922
+- Estimated Gas Usage: 1176 - 35928
 
 ### Description
 
@@ -45,12 +45,12 @@ External calls return a boolean value. If the callee contract halts with an exce
 - Contract: Unknown
 - Function name: `_function_0xeea4c864`
 - PC address: 1038
-- Estimated Gas Usage: 471 - 1223
+- Estimated Gas Usage: 477 - 1229
 
 ### Description
 
 A call to a user-supplied address is executed.
-The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 
 ## Unchecked Call Return Value
 - SWC ID: 104
@@ -58,7 +58,7 @@ The callee address of an external message call can be set by the caller. Note th
 - Contract: Unknown
 - Function name: `_function_0xeea4c864`
 - PC address: 1038
-- Estimated Gas Usage: 1195 - 35947
+- Estimated Gas Usage: 1201 - 35953
 
 ### Description
 

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

@@ -26,7 +26,7 @@ Severity: Low
 Contract: Unknown
 Function name: _function_0x9b58bc26
 PC address: 849
-Estimated Gas Usage: 1170 - 35922
+Estimated Gas Usage: 1176 - 35928
 The return value of a message call is not checked.
 External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.
 --------------------
@@ -37,9 +37,9 @@ Severity: Medium
 Contract: Unknown
 Function name: _function_0xeea4c864
 PC address: 1038
-Estimated Gas Usage: 471 - 1223
+Estimated Gas Usage: 477 - 1229
 A call to a user-supplied address is executed.
-The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on thecontract state.
+The callee address of an external message call can be set by the caller. Note that the callee can contain arbitrary code and may re-enter any function in this contract. Review the business logic carefully to prevent averse effects on the contract state.
 --------------------
 
 ==== Unchecked Call Return Value ====
@@ -48,7 +48,7 @@ Severity: Low
 Contract: Unknown
 Function name: _function_0xeea4c864
 PC address: 1038
-Estimated Gas Usage: 1195 - 35947
+Estimated Gas Usage: 1201 - 35953
 The return value of a message call is not checked.
 External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.
 --------------------

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

@@ -1 +1,5 @@
-{"error": null, "issues": [], "success": true}
+{
+    "error": null,
+    "issues": [],
+    "success": true
+}

tests/testdata/outputs_expected/metacoin.sol.o.jsonv2

@@ -1,9 +1 @@
-[
-    {
-        "issues": [],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": [], "sourceType": "raw-bytecode"}]

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

@@ -1 +1,19 @@
-{"error": null, "issues": [{"address": 142, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "Anyone can withdraw ETH from the contract account.\nArbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.", "function": "transfer()", "max_gas_used": 467, "min_gas_used": 186, "severity": "High", "sourceMap": null, "swc-id": "105", "title": "Unprotected Ether Withdrawal"}], "success": true}
+{
+    "error": null,
+    "issues": [
+        {
+            "address": 142,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "Anyone can withdraw ETH from the contract account.\nArbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability.",
+            "function": "transfer()",
+            "max_gas_used": 467,
+            "min_gas_used": 186,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "105",
+            "title": "Unprotected Ether Withdrawal"
+        }
+    ],
+    "success": true
+}

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

@@ -1,27 +1 @@
-[
-    {
-        "issues": [
-            {
-                "description": {
-                    "head": "Anyone can withdraw ETH from the contract account.",
-                    "tail": "Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "142:1:0"
-                    }
-                ],
-                "severity": "High",
-                "swcID": "SWC-105",
-                "swcTitle": "Unprotected Ether Withdrawal"
-            }
-        ],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [
-            "0xbc9c3d9db56d20cf4ca3b6fd88ff9215cf728a092cca1ed8edb83272b933ff5b"
-        ],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [{"description": {"head": "Anyone can withdraw ETH from the contract account.", "tail": "Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability."}, "extra": {}, "locations": [{"sourceMap": "142:1:0"}], "severity": "High", "swcID": "SWC-105", "swcTitle": "Unprotected Ether Withdrawal"}], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": ["0xbc9c3d9db56d20cf4ca3b6fd88ff9215cf728a092cca1ed8edb83272b933ff5b"], "sourceType": "raw-bytecode"}]

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

@@ -1 +1,5 @@
-{"error": null, "issues": [], "success": true}
+{
+    "error": null,
+    "issues": [],
+    "success": true
+}

tests/testdata/outputs_expected/nonascii.sol.o.jsonv2

@@ -1,9 +1 @@
-[
-    {
-        "issues": [],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": [], "sourceType": "raw-bytecode"}]

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

@@ -1 +1,19 @@
-{"error": null, "issues": [{"address": 317, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "Use of tx.origin is deprecated.\nThe smart contract retrieves the transaction origin (tx.origin) using msg.origin. Use of msg.origin is deprecated and the instruction may be removed in the  future. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin", "function": "transferOwnership(address)", "max_gas_used": 1051, "min_gas_used": 626, "severity": "Medium", "sourceMap": null, "swc-id": "111", "title": "Use of tx.origin"}], "success": true}
+{
+    "error": null,
+    "issues": [
+        {
+            "address": 317,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "Use of tx.origin is deprecated.\nThe smart contract retrieves the transaction origin (tx.origin) using msg.origin. Use of msg.origin is deprecated and the instruction may be removed in the  future. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin",
+            "function": "transferOwnership(address)",
+            "max_gas_used": 1051,
+            "min_gas_used": 626,
+            "severity": "Medium",
+            "sourceMap": null,
+            "swc-id": "111",
+            "title": "Use of tx.origin"
+        }
+    ],
+    "success": true
+}

tests/testdata/outputs_expected/origin.sol.o.jsonv2

@@ -1,27 +1 @@
-[
-    {
-        "issues": [
-            {
-                "description": {
-                    "head": "Use of tx.origin is deprecated.",
-                    "tail": "The smart contract retrieves the transaction origin (tx.origin) using msg.origin. Use of msg.origin is deprecated and the instruction may be removed in the  future. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin"
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "317:1:0"
-                    }
-                ],
-                "severity": "Medium",
-                "swcID": "SWC-111",
-                "swcTitle": "Use of Deprecated Solidity Functions"
-            }
-        ],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [
-            "0x25b20ef097dfc0aa56a932c4e09f06ee02a69c005767df86877f48c6c2412f03"
-        ],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [{"description": {"head": "Use of tx.origin is deprecated.", "tail": "The smart contract retrieves the transaction origin (tx.origin) using msg.origin. Use of msg.origin is deprecated and the instruction may be removed in the  future. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin"}, "extra": {}, "locations": [{"sourceMap": "317:1:0"}], "severity": "Medium", "swcID": "SWC-111", "swcTitle": "Use of Deprecated Solidity Functions"}], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": ["0x25b20ef097dfc0aa56a932c4e09f06ee02a69c005767df86877f48c6c2412f03"], "sourceType": "raw-bytecode"}]

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

@@ -1,29 +1,32 @@
 {
     "error": null,
-	"issues": [{
+    "issues": [
+        {
             "address": 567,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
             "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
-		"max_gas_used": 1053,
-		"min_gas_used": 768,
+            "max_gas_used": 78155,
+            "min_gas_used": 17019,
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
             "title": "Integer Underflow"
-	}, {
+        },
+        {
             "address": 649,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
             "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
-		"max_gas_used": 1774,
-		"min_gas_used": 1299,
+            "max_gas_used": 78155,
+            "min_gas_used": 17019,
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
             "title": "Integer Underflow"
-	}],
+        }
+    ],
     "success": true
 }

tests/testdata/outputs_expected/overflow.sol.o.jsonv2

@@ -1,42 +1 @@
-[
-    {
-        "issues": [
-            {
-                "description": {
-                    "head": "The binary subtraction can underflow.",
-                    "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "567:1:0"
-                    }
-                ],
-                "severity": "High",
-                "swcID": "SWC-101",
-                "swcTitle": "Integer Overflow and Underflow"
-            },
-            {
-                "description": {
-                    "head": "The binary subtraction can underflow.",
-                    "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "649:1:0"
-                    }
-                ],
-                "severity": "High",
-                "swcID": "SWC-101",
-                "swcTitle": "Integer Overflow and Underflow"
-            }
-        ],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [
-            "0xf230bec502569e8b7e7737616d0ad0f200c436624e3c223e5398c0615cd2d6b9"
-        ],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [{"description": {"head": "The binary subtraction can underflow.", "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."}, "extra": {}, "locations": [{"sourceMap": "567:1:0"}], "severity": "High", "swcID": "SWC-101", "swcTitle": "Integer Overflow and Underflow"}, {"description": {"head": "The binary subtraction can underflow.", "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."}, "extra": {}, "locations": [{"sourceMap": "649:1:0"}], "severity": "High", "swcID": "SWC-101", "swcTitle": "Integer Overflow and Underflow"}], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": ["0xf230bec502569e8b7e7737616d0ad0f200c436624e3c223e5398c0615cd2d6b9"], "sourceType": "raw-bytecode"}]

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

@@ -6,7 +6,7 @@
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 567
-- Estimated Gas Usage: 768 - 1053
+- Estimated Gas Usage: 17019 - 78155
 
 ### Description
 
@@ -19,7 +19,7 @@ The operands of the subtraction operation are not sufficiently constrained. The
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 649
-- Estimated Gas Usage: 1299 - 1774
+- Estimated Gas Usage: 17019 - 78155
 
 ### Description
 

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

@@ -4,7 +4,7 @@ Severity: High
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 567
-Estimated Gas Usage: 768 - 1053
+Estimated Gas Usage: 17019 - 78155
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------
@@ -15,7 +15,7 @@ Severity: High
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 649
-Estimated Gas Usage: 1299 - 1774
+Estimated Gas Usage: 17019 - 78155
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------

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

@@ -1 +1,45 @@
-{"error": null, "issues": [{"address": 196, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "callchecked()", "max_gas_used": 1210, "min_gas_used": 599, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 285, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.", "function": "callnotchecked()", "max_gas_used": 1232, "min_gas_used": 621, "severity": "Low", "sourceMap": null, "swc-id": "107", "title": "External Call To Fixed Address"}, {"address": 285, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.", "function": "callnotchecked()", "max_gas_used": 35950, "min_gas_used": 1339, "severity": "Low", "sourceMap": null, "swc-id": "104", "title": "Unchecked Call Return Value"}], "success": true}
+{
+    "error": null,
+    "issues": [
+        {
+            "address": 196,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "function": "callchecked()",
+            "max_gas_used": 1210,
+            "min_gas_used": 599,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "107",
+            "title": "External Call To Fixed Address"
+        },
+        {
+            "address": 285,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The contract executes an external message call.\nAn external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully.",
+            "function": "callnotchecked()",
+            "max_gas_used": 1232,
+            "min_gas_used": 621,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "107",
+            "title": "External Call To Fixed Address"
+        },
+        {
+            "address": 285,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The return value of a message call is not checked.\nExternal calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states.",
+            "function": "callnotchecked()",
+            "max_gas_used": 35950,
+            "min_gas_used": 1339,
+            "severity": "Low",
+            "sourceMap": null,
+            "swc-id": "104",
+            "title": "Unchecked Call Return Value"
+        }
+    ],
+    "success": true
+}

tests/testdata/outputs_expected/returnvalue.sol.o.jsonv2

@@ -1,57 +1 @@
-[
-    {
-        "issues": [
-            {
-                "description": {
-                    "head": "The contract executes an external message call.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "196:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-107",
-                "swcTitle": "Reentrancy"
-            },
-            {
-                "description": {
-                    "head": "The contract executes an external message call.",
-                    "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "285:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-107",
-                "swcTitle": "Reentrancy"
-            },
-            {
-                "description": {
-                    "head": "The return value of a message call is not checked.",
-                    "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "285:1:0"
-                    }
-                ],
-                "severity": "Low",
-                "swcID": "SWC-104",
-                "swcTitle": "Unchecked Call Return Value"
-            }
-        ],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [
-            "0xb191cf6cc0d8cc37a91c9d88019cc011b932169fb5776df616e2bb9cd93b4039"
-        ],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [{"description": {"head": "The contract executes an external message call.", "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."}, "extra": {}, "locations": [{"sourceMap": "196:1:0"}], "severity": "Low", "swcID": "SWC-107", "swcTitle": "Reentrancy"}, {"description": {"head": "The contract executes an external message call.", "tail": "An external function call to a fixed contract address is executed. Make sure that the callee contract has been reviewed carefully."}, "extra": {}, "locations": [{"sourceMap": "285:1:0"}], "severity": "Low", "swcID": "SWC-107", "swcTitle": "Reentrancy"}, {"description": {"head": "The return value of a message call is not checked.", "tail": "External calls return a boolean value. If the callee contract halts with an exception, 'false' is returned and execution continues in the caller. It is usually recommended to wrap external calls into a require statement to prevent unexpected states."}, "extra": {}, "locations": [{"sourceMap": "285:1:0"}], "severity": "Low", "swcID": "SWC-104", "swcTitle": "Unchecked Call Return Value"}], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": ["0xb191cf6cc0d8cc37a91c9d88019cc011b932169fb5776df616e2bb9cd93b4039"], "sourceType": "raw-bytecode"}]

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

@@ -1,19 +1,19 @@
 {
-   "error" : null,
-   "issues" : [
+    "error": null,
+    "issues": [
         {
-         "title" : "Unprotected Selfdestruct",
-         "swc-id" : "106",
-         "severity" : "High",
-         "contract" : "Unknown",
-         "description" : "The contract can be killed by anyone.\nAnyone can kill this contract and withdraw its balance to an arbitrary address.",
-         "function" : "kill(address)",
-         "min_gas_used" : 168,
-         "max_gas_used" : 263,
-         "debug" : "<DEBUG-DATA>",
-         "sourceMap" : null,
-         "address" : 146
+            "address": 146,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The contract can be killed by anyone.\nAnyone can kill this contract and withdraw its balance to an arbitrary address.",
+            "function": "kill(address)",
+            "max_gas_used": 263,
+            "min_gas_used": 168,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "106",
+            "title": "Unprotected Selfdestruct"
         }
     ],
-   "success" : true
+    "success": true
 }

tests/testdata/outputs_expected/suicide.sol.o.jsonv2

@@ -1,27 +1 @@
-[
-   {
-      "issues" : [
-         {
-            "swcTitle" : "Unprotected SELFDESTRUCT Instruction",
-            "locations" : [
-               {
-                  "sourceMap" : "146:1:0"
-               }
-            ],
-            "extra" : {},
-            "description" : {
-               "tail" : "Anyone can kill this contract and withdraw its balance to an arbitrary address.",
-               "head" : "The contract can be killed by anyone."
-            },
-            "severity" : "High",
-            "swcID" : "SWC-106"
-         }
-      ],
-      "sourceFormat" : "evm-byzantium-bytecode",
-      "meta" : {},
-      "sourceType" : "raw-bytecode",
-      "sourceList" : [
-         "0x2fb801366b61a05b30550481a1c8f7d5f20de0b93d9f2f2ce2b28c4e322033c9"
-      ]
-   }
-]
+[{"issues": [{"description": {"head": "The contract can be killed by anyone.", "tail": "Anyone can kill this contract and withdraw its balance to an arbitrary address."}, "extra": {}, "locations": [{"sourceMap": "146:1:0"}], "severity": "High", "swcID": "SWC-106", "swcTitle": "Unprotected SELFDESTRUCT Instruction"}], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": ["0x2fb801366b61a05b30550481a1c8f7d5f20de0b93d9f2f2ce2b28c4e322033c9"], "sourceType": "raw-bytecode"}]

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

@@ -1,29 +1,32 @@
 {
     "error": null,
-	"issues": [{
+    "issues": [
+        {
             "address": 567,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
             "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
-		"max_gas_used": 1053,
-		"min_gas_used": 768,
+            "max_gas_used": 52861,
+            "min_gas_used": 11915,
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
             "title": "Integer Underflow"
-	}, {
+        },
+        {
             "address": 649,
             "contract": "Unknown",
             "debug": "<DEBUG-DATA>",
             "description": "The binary subtraction can underflow.\nThe operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.",
             "function": "sendeth(address,uint256)",
-		"max_gas_used": 1774,
-		"min_gas_used": 1299,
+            "max_gas_used": 52861,
+            "min_gas_used": 11915,
             "severity": "High",
             "sourceMap": null,
             "swc-id": "101",
             "title": "Integer Underflow"
-	}],
+        }
+    ],
     "success": true
 }

tests/testdata/outputs_expected/underflow.sol.o.jsonv2

@@ -1,42 +1 @@
-[
-    {
-        "issues": [
-            {
-                "description": {
-                    "head": "The binary subtraction can underflow.",
-                    "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "567:1:0"
-                    }
-                ],
-                "severity": "High",
-                "swcID": "SWC-101",
-                "swcTitle": "Integer Overflow and Underflow"
-            },
-            {
-                "description": {
-                    "head": "The binary subtraction can underflow.",
-                    "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."
-                },
-                "extra": {},
-                "locations": [
-                    {
-                        "sourceMap": "649:1:0"
-                    }
-                ],
-                "severity": "High",
-                "swcID": "SWC-101",
-                "swcTitle": "Integer Overflow and Underflow"
-            }
-        ],
-        "meta": {},
-        "sourceFormat": "evm-byzantium-bytecode",
-        "sourceList": [
-            "0xabef56740bf7795a9f8732e4781ebd27f2977f8a4997e3ff11cee79a4ba6c0ce"
-        ],
-        "sourceType": "raw-bytecode"
-    }
-]
+[{"issues": [{"description": {"head": "The binary subtraction can underflow.", "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."}, "extra": {}, "locations": [{"sourceMap": "567:1:0"}], "severity": "High", "swcID": "SWC-101", "swcTitle": "Integer Overflow and Underflow"}, {"description": {"head": "The binary subtraction can underflow.", "tail": "The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion."}, "extra": {}, "locations": [{"sourceMap": "649:1:0"}], "severity": "High", "swcID": "SWC-101", "swcTitle": "Integer Overflow and Underflow"}], "meta": {}, "sourceFormat": "evm-byzantium-bytecode", "sourceList": ["0xabef56740bf7795a9f8732e4781ebd27f2977f8a4997e3ff11cee79a4ba6c0ce"], "sourceType": "raw-bytecode"}]

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

@@ -6,7 +6,7 @@
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 567
-- Estimated Gas Usage: 768 - 1053
+- Estimated Gas Usage: 11915 - 52861
 
 ### Description
 
@@ -19,7 +19,7 @@ The operands of the subtraction operation are not sufficiently constrained. The
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 649
-- Estimated Gas Usage: 1299 - 1774
+- Estimated Gas Usage: 11915 - 52861
 
 ### Description
 

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

@@ -4,7 +4,7 @@ Severity: High
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 567
-Estimated Gas Usage: 768 - 1053
+Estimated Gas Usage: 11915 - 52861
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------
@@ -15,7 +15,7 @@ Severity: High
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 649
-Estimated Gas Usage: 1299 - 1774
+Estimated Gas Usage: 11915 - 52861
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------