Merge pull request #711 from ConsenSys/develop

Merge changes from develop

CONTRIBUTING.md

@@ -5,12 +5,12 @@ Hi, if you are reading this that means that you probably want to contribute to M
 If you have found a problem with Mythril or want to propose a new feature then you can do this using GitHub issues. 
 We already created some templates to make this process easier, but if your issue/feature request does not fit within the template then feel free to deviate.
 
-If you have a small question or aren't sure if you should create an issue for your problem/suggestion then you can always hop by on our [Gitter channel](https://gitter.im/ConsenSys/mythril).
+If you have a small question or aren't sure if you should create an issue for your problem/suggestion then you can always hop by on our [Discord server](https://discord.gg/FGMkcU2).
 
 # Coding
 If you want to help out with the development of Mythril then you can take a look at our issues or [Waffle board](https://waffle.io/ConsenSys/mythril).
 
-Before you start working on an issue pkease stop by on Gitter to message a collaborator, this way we can assign you to the issue making sure nobody does double work. We can also provide you with support through Gitter if there are any questions during the development process.
+Before you start working on an issue pkease stop by on Discord to message a collaborator, this way we can assign you to the issue making sure nobody does double work. We can also provide you with support through Discord if there are any questions during the development process.
 
 ## New ideas
 Before you start working on a new idea, it's useful to create an issue on GitHub, that way we know what you want to implement and that you are working on it. Additionally, it might happen that your feature does not fit with our roadmap, in which case it would be unfortunate if you have already spent some time working on it.

mythril/analysis/analysis_utils.py

@@ -2,7 +2,7 @@ import re
 from typing import List
 from z3 import *
 from mythril.laser.ethereum.transaction import ContractCreationTransaction
-from mythril.laser.ethereum.state import GlobalState
+from mythril.laser.ethereum.state.global_state import GlobalState
 
 
 def get_non_creator_constraints(state: GlobalState) -> (List, bool):

mythril/analysis/modules/delegatecall.py

@@ -52,6 +52,7 @@ def _concrete_call(call, state, address, meminstart):
         bytecode=state.environment.code.bytecode,
         title="Call data forwarded with delegatecall()",
         _type="Informational",
+        gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
     )
 
     issue.description = (
@@ -74,6 +75,7 @@ def _symbolic_call(call, state, address, statespace):
         swc_id=DELEGATECALL_TO_UNTRUSTED_CONTRACT,
         bytecode=state.environment.code.bytecode,
         title=call.type + " to a user-supplied address",
+        gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
     )
 
     if "calldata" in str(call.to):

mythril/analysis/modules/dependence_on_predictable_vars.py

@@ -70,6 +70,10 @@ def execute(statespace):
                     title="Dependence on predictable environment variable",
                     _type="Warning",
                     description=description,
+                    gas_used=(
+                        call.state.mstate.min_gas_used,
+                        call.state.mstate.max_gas_used,
+                    ),
                 )
                 issues.append(issue)
 
@@ -119,6 +123,10 @@ def execute(statespace):
                             _type="Warning",
                             description=description,
                             swc_id=PREDICTABLE_VARS_DEPENDENCE,
+                            gas_used=(
+                                call.state.mstate.min_gas_used,
+                                call.state.mstate.max_gas_used,
+                            ),
                         )
                         issues.append(issue)
                         break
@@ -149,6 +157,10 @@ def execute(statespace):
                                 _type="Informational",
                                 description=description,
                                 swc_id=PREDICTABLE_VARS_DEPENDENCE,
+                                gas_used=(
+                                    call.state.mstate.min_gas_used,
+                                    call.state.mstate.max_gas_used,
+                                ),
                             )
                             issues.append(issue)
                             break

mythril/analysis/modules/deprecated_ops.py

@@ -41,6 +41,7 @@ def execute(statespace):
                     _type="Warning",
                     swc_id=TX_ORIGIN_USAGE,
                     description=description,
+                    gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                 )
                 issues.append(issue)
 

mythril/analysis/modules/ether_thief.py

@@ -85,6 +85,7 @@ def _analyze_state(state, node):
             description="Users other than the contract creator can withdraw ETH from the contract account"
             + " without previously having sent any ETH to it. This is likely to be vulnerability.",
             debug=debug,
+            gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
         )
         issues.append(issue)
     except UnsatError:

mythril/analysis/modules/exceptions.py

@@ -55,6 +55,10 @@ def execute(statespace):
                             description=description,
                             bytecode=state.environment.code.bytecode,
                             debug=debug,
+                            gas_used=(
+                                state.mstate.min_gas_used,
+                                state.mstate.max_gas_used,
+                            ),
                         )
                     )
 

mythril/analysis/modules/external_calls.py

@@ -126,6 +126,7 @@ def execute(statespace):
                         description=description,
                         bytecode=state.environment.code.bytecode,
                         swc_id=REENTRANCY,
+                        gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                     )
 
                 else:
@@ -141,6 +142,7 @@ def execute(statespace):
                         description=description,
                         bytecode=state.environment.code.bytecode,
                         swc_id=REENTRANCY,
+                        gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                     )
 
                 issues.append(issue)
@@ -186,6 +188,10 @@ def execute(statespace):
                                 description=description,
                                 bytecode=state.environment.code.bytecode,
                                 swc_id=REENTRANCY,
+                                gas_used=(
+                                    state.mstate.min_gas_used,
+                                    state.mstate.max_gas_used,
+                                ),
                             )
                             issues.append(issue)
 

mythril/analysis/modules/integer.py

@@ -74,13 +74,12 @@ def _check_integer_overflow(statespace, state, node):
     if instruction["opcode"] == "ADD":
         operator = "add"
         expr = op0 + op1
-        # constraint = Not(BVAddNoOverflow(op0, op1, signed=False))
+        constraint = Not(BVAddNoOverflow(op0, op1, signed=False))
     else:
         operator = "multiply"
         expr = op1 * op0
-        # constraint = Not(BVMulNoOverflow(op0, op1, signed=False))
+        constraint = Not(BVMulNoOverflow(op0, op1, signed=False))
 
-    constraint = Or(And(ULT(expr, op0), op1 != 0), And(ULT(expr, op1), op0 != 0))
     # Check satisfiable
     model = _try_constraints(node.constraints, [constraint])
 
@@ -102,6 +101,7 @@ def _check_integer_overflow(statespace, state, node):
         bytecode=state.environment.code.bytecode,
         title="Integer Overflow",
         _type="Warning",
+        gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
     )
 
     issue.description = "This binary {} operation can result in integer overflow.\n".format(
@@ -215,6 +215,7 @@ def _check_integer_underflow(statespace, state, node):
                     bytecode=state.environment.code.bytecode,
                     title="Integer Underflow",
                     _type="Warning",
+                    gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                 )
 
                 issue.description = (

mythril/analysis/modules/multiple_sends.py

@@ -30,6 +30,10 @@ def execute(statespace):
                 bytecode=call.state.environment.code.bytecode,
                 title="Multiple Calls",
                 _type="Informational",
+                gas_used=(
+                    call.state.mstate.min_gas_used,
+                    call.state.mstate.max_gas_used,
+                ),
             )
 
             issue.description = (

mythril/analysis/modules/suicide.py

@@ -78,6 +78,7 @@ def _analyze_state(state, node):
             _type="Warning",
             description=description,
             debug=debug,
+            gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
         )
         issues.append(issue)
     except UnsatError:

mythril/analysis/modules/transaction_order_dependence.py

@@ -41,6 +41,10 @@ def execute(statespace):
                 bytecode=call.state.environment.code.bytecode,
                 swc_id=TX_ORDER_DEPENDENCE,
                 _type="Warning",
+                gas_used=(
+                    call.state.mstate.min_gas_used,
+                    call.state.mstate.max_gas_used,
+                ),
             )
 
             issue.description = (

mythril/analysis/modules/unchecked_retval.py

@@ -59,6 +59,7 @@ def execute(statespace):
                     bytecode=state.environment.code.bytecode,
                     title="Unchecked CALL return value",
                     swc_id=UNCHECKED_RET_VAL,
+                    gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
                 )
 
                 issue.description = (
@@ -108,6 +109,10 @@ def execute(statespace):
                             address=address,
                             title="Unchecked CALL return value",
                             swc_id=UNCHECKED_RET_VAL,
+                            gas_used=(
+                                state.mstate.min_gas_used,
+                                state.mstate.max_gas_used,
+                            ),
                         )
 
                         issue.description = (

mythril/analysis/report.py

@@ -15,6 +15,7 @@ class Issue:
         swc_id,
         title,
         bytecode,
+        gas_used=(None, None),
         _type="Informational",
         description="",
         debug="",
@@ -28,6 +29,7 @@ class Issue:
         self.type = _type
         self.debug = debug
         self.swc_id = swc_id
+        self.min_gas_used, self.max_gas_used = gas_used
         self.filename = None
         self.code = None
         self.lineno = None
@@ -54,6 +56,8 @@ class Issue:
             "type": self.type,
             "address": self.address,
             "debug": self.debug,
+            "min_gas_used": self.min_gas_used,
+            "max_gas_used": self.max_gas_used,
         }
 
         if self.filename and self.lineno:

mythril/analysis/symbolic.py

@@ -1,5 +1,5 @@
 from mythril.laser.ethereum import svm
-from mythril.laser.ethereum.state import Account
+from mythril.laser.ethereum.state.account import Account
 from mythril.ether.soliditycontract import SolidityContract, ETHContract
 import copy
 import logging

mythril/analysis/templates/report_as_markdown.jinja2

@@ -8,6 +8,7 @@
 - Contract: {{ issue.contract | default("Unknown") }}
 - Function name: `{{ issue.function }}`
 - PC address: {{ issue.address }}
+- Estimated Gas Usage: {{ issue.min_gas_used }} - {{ issue.max_gas_used }}
 
 ### Description
 

mythril/analysis/templates/report_as_text.jinja2

@@ -6,6 +6,7 @@ Type: {{ issue.type }}
 Contract: {{ issue.contract | default("Unknown") }}
 Function name: {{ issue.function }}
 PC address: {{ issue.address }}
+Estimated Gas Usage: {{ issue.min_gas_used }} - {{ issue.max_gas_used }}
 {{ issue.description }}
 --------------------
 {% if issue.filename and issue.lineno %}

mythril/laser/ethereum/call.py

@@ -2,7 +2,9 @@ import logging
 from typing import Union
 from z3 import simplify, ExprRef, Extract
 import mythril.laser.ethereum.util as util
-from mythril.laser.ethereum.state import Account, CalldataType, GlobalState, Calldata
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.calldata import CalldataType, Calldata
+from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.support.loader import DynLoader
 import re
 

mythril/laser/ethereum/evm_exceptions.py

@@ -16,3 +16,7 @@ class InvalidJumpDestination(VmException):
 
 class InvalidInstruction(VmException):
     pass
+
+
+class OutOfGasException(VmException):
+    pass

mythril/laser/ethereum/gas.py

@@ -0,0 +1,175 @@
+from ethereum import opcodes
+from ethereum.utils import ceil32
+
+
+def calculate_native_gas(size: int, contract: str):
+    gas_value = None
+    word_num = ceil32(size) // 32
+    if contract == "ecrecover":
+        gas_value = opcodes.GECRECOVER
+    elif contract == "sha256":
+        gas_value = opcodes.GSHA256BASE + word_num * opcodes.GSHA256WORD
+    elif contract == "ripemd160":
+        gas_value = opcodes.GRIPEMD160BASE + word_num * opcodes.GRIPEMD160WORD
+    elif contract == "identity":
+        gas_value = opcodes.GIDENTITYBASE + word_num * opcodes.GIDENTITYWORD
+    else:
+        raise ValueError("Unknown contract type {}".format(contract))
+    return gas_value, gas_value
+
+
+def calculate_sha3_gas(length: int):
+    gas_val = 30 + opcodes.GSHA3WORD * (ceil32(length) // 32)
+    return gas_val, gas_val
+
+
+# opcode -> (min_gas, max_gas)
+OPCODE_GAS = {
+    "STOP": (0, 0),
+    "ADD": (3, 3),
+    "MUL": (5, 5),
+    "SUB": (3, 3),
+    "DIV": (5, 5),
+    "SDIV": (5, 5),
+    "MOD": (5, 5),
+    "SMOD": (5, 5),
+    "ADDMOD": (8, 8),
+    "MULMOD": (8, 8),
+    "EXP": (10, 340),  # exponent max 2^32
+    "SIGNEXTEND": (5, 5),
+    "LT": (3, 3),
+    "GT": (3, 3),
+    "SLT": (3, 3),
+    "SGT": (3, 3),
+    "EQ": (3, 3),
+    "ISZERO": (3, 3),
+    "AND": (3, 3),
+    "OR": (3, 3),
+    "XOR": (3, 3),
+    "NOT": (3, 3),
+    "BYTE": (3, 3),
+    "SHA3": (
+        30,
+        30 + 6 * 8,
+    ),  # max can be larger, but usually storage location with 8 words
+    "SHA3_FUNC": calculate_sha3_gas,
+    "ADDRESS": (2, 2),
+    "BALANCE": (400, 400),
+    "ORIGIN": (2, 2),
+    "CALLER": (2, 2),
+    "CALLVALUE": (2, 2),
+    "CALLDATALOAD": (3, 3),
+    "CALLDATASIZE": (2, 2),
+    "CALLDATACOPY": (2, 2 + 3 * 768),  # https://ethereum.stackexchange.com/a/47556
+    "CODESIZE": (2, 2),
+    "CODECOPY": (2, 2 + 3 * 768),  # https://ethereum.stackexchange.com/a/47556,
+    "GASPRICE": (2, 2),
+    "EXTCODESIZE": (700, 700),
+    "EXTCODECOPY": (700, 700 + 3 * 768),  # https://ethereum.stackexchange.com/a/47556
+    "RETURNDATASIZE": (2, 2),
+    "RETURNDATACOPY": (3, 3),
+    "BLOCKHASH": (20, 20),
+    "COINBASE": (2, 2),
+    "TIMESTAMP": (2, 2),
+    "NUMBER": (2, 2),
+    "DIFFICULTY": (2, 2),
+    "GASLIMIT": (2, 2),
+    "POP": (2, 2),
+    # assume 1KB memory r/w cost as upper bound
+    "MLOAD": (3, 96),
+    "MSTORE": (3, 98),
+    "MSTORE8": (3, 98),
+    # assume 64 byte r/w cost as upper bound
+    "SLOAD": (400, 400),
+    "SSTORE": (5000, 25000),
+    "JUMP": (8, 8),
+    "JUMPI": (10, 10),
+    "PC": (2, 2),
+    "MSIZE": (2, 2),
+    "GAS": (2, 2),
+    "JUMPDEST": (1, 1),
+    "PUSH1": (3, 3),
+    "PUSH2": (3, 3),
+    "PUSH3": (3, 3),
+    "PUSH4": (3, 3),
+    "PUSH5": (3, 3),
+    "PUSH6": (3, 3),
+    "PUSH7": (3, 3),
+    "PUSH8": (3, 3),
+    "PUSH9": (3, 3),
+    "PUSH10": (3, 3),
+    "PUSH11": (3, 3),
+    "PUSH12": (3, 3),
+    "PUSH13": (3, 3),
+    "PUSH14": (3, 3),
+    "PUSH15": (3, 3),
+    "PUSH16": (3, 3),
+    "PUSH17": (3, 3),
+    "PUSH18": (3, 3),
+    "PUSH19": (3, 3),
+    "PUSH20": (3, 3),
+    "PUSH21": (3, 3),
+    "PUSH22": (3, 3),
+    "PUSH23": (3, 3),
+    "PUSH24": (3, 3),
+    "PUSH25": (3, 3),
+    "PUSH26": (3, 3),
+    "PUSH27": (3, 3),
+    "PUSH28": (3, 3),
+    "PUSH29": (3, 3),
+    "PUSH30": (3, 3),
+    "PUSH31": (3, 3),
+    "PUSH32": (3, 3),
+    "DUP1": (3, 3),
+    "DUP2": (3, 3),
+    "DUP3": (3, 3),
+    "DUP4": (3, 3),
+    "DUP5": (3, 3),
+    "DUP6": (3, 3),
+    "DUP7": (3, 3),
+    "DUP8": (3, 3),
+    "DUP9": (3, 3),
+    "DUP10": (3, 3),
+    "DUP11": (3, 3),
+    "DUP12": (3, 3),
+    "DUP13": (3, 3),
+    "DUP14": (3, 3),
+    "DUP15": (3, 3),
+    "DUP16": (3, 3),
+    "SWAP1": (3, 3),
+    "SWAP2": (3, 3),
+    "SWAP3": (3, 3),
+    "SWAP4": (3, 3),
+    "SWAP5": (3, 3),
+    "SWAP6": (3, 3),
+    "SWAP7": (3, 3),
+    "SWAP8": (3, 3),
+    "SWAP9": (3, 3),
+    "SWAP10": (3, 3),
+    "SWAP11": (3, 3),
+    "SWAP12": (3, 3),
+    "SWAP13": (3, 3),
+    "SWAP14": (3, 3),
+    "SWAP15": (3, 3),
+    "SWAP16": (3, 3),
+    # apparently Solidity only allows byte32 as input to the log
+    # function. Virtually it could be as large as the block gas limit
+    # allows, but let's stick to the reasonable standard here.
+    # https://ethereum.stackexchange.com/a/1691
+    "LOG0": (375, 375 + 8 * 32),
+    "LOG1": (2 * 375, 2 * 375 + 8 * 32),
+    "LOG2": (3 * 375, 3 * 375 + 8 * 32),
+    "LOG3": (4 * 375, 4 * 375 + 8 * 32),
+    "LOG4": (5 * 375, 5 * 375 + 8 * 32),
+    "CREATE": (32000, 32000),
+    "CALL": (700, 700 + 9000 + 25000),
+    "NATIVE_COST": calculate_native_gas,
+    "CALLCODE": (700, 700 + 9000 + 25000),
+    "RETURN": (0, 0),
+    "DELEGATECALL": (700, 700 + 9000 + 25000),
+    "STATICCALL": (700, 700 + 9000 + 25000),
+    "REVERT": (0, 0),
+    "SUICIDE": (5000, 30000),
+    "ASSERT_FAIL": (0, 0),
+    "INVALID": (0, 0),
+}

mythril/laser/ethereum/instructions.py

@@ -37,9 +37,12 @@ from mythril.laser.ethereum.evm_exceptions import (
     StackUnderflowException,
     InvalidJumpDestination,
     InvalidInstruction,
+    OutOfGasException,
 )
+from mythril.laser.ethereum.gas import OPCODE_GAS
 from mythril.laser.ethereum.keccak import KeccakFunctionManager
-from mythril.laser.ethereum.state import GlobalState, CalldataType, Calldata
+from mythril.laser.ethereum.state.calldata import CalldataType, Calldata
+from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction import (
     MessageCallTransaction,
     TransactionStartSignal,
@@ -62,8 +65,9 @@ class StateTransition(object):
     incremented if `increment_pc=True`.
     """
 
-    def __init__(self, increment_pc=True):
+    def __init__(self, increment_pc=True, enable_gas=True):
         self.increment_pc = increment_pc
+        self.enable_gas = enable_gas
 
     @staticmethod
     def call_on_state_copy(func: Callable, func_obj: "Instruction", state: GlobalState):
@@ -76,11 +80,32 @@ class StateTransition(object):
                 state.mstate.pc += 1
         return states
 
+    @staticmethod
+    def check_gas_usage_limit(global_state: GlobalState):
+        global_state.mstate.check_gas()
+        if (
+            global_state.mstate.min_gas_used
+            >= global_state.current_transaction.gas_limit
+        ):
+            raise OutOfGasException()
+
+    def accumulate_gas(self, global_state: GlobalState):
+        if not self.enable_gas:
+            return global_state
+        opcode = global_state.instruction["opcode"]
+        min_gas, max_gas = OPCODE_GAS[opcode]
+        global_state.mstate.min_gas_used += min_gas
+        global_state.mstate.max_gas_used += max_gas
+        return global_state
+
     def __call__(self, func: Callable) -> Callable:
         def wrapper(
             func_obj: "Instruction", global_state: GlobalState
         ) -> List[GlobalState]:
             new_global_states = self.call_on_state_copy(func, func_obj, global_state)
+            new_global_states = [
+                self.accumulate_gas(state) for state in new_global_states
+            ]
             return self.increment_states_pc(new_global_states)
 
         return wrapper
@@ -93,7 +118,7 @@ class Instruction:
 
     def __init__(self, op_code: str, dynamic_loader: DynLoader):
         self.dynamic_loader = dynamic_loader
-        self.op_code = op_code
+        self.op_code = op_code.upper()
 
     def evaluate(self, global_state: GlobalState, post=False) -> List[GlobalState]:
         """ Performs the mutation for this instruction """
@@ -325,6 +350,7 @@ class Instruction:
                 )
             )
         else:
+
             state.stack.append(pow(base.as_long(), exponent.as_long(), 2 ** 256))
 
         return [global_state]
@@ -569,7 +595,7 @@ class Instruction:
         state.stack.append(len(disassembly.bytecode) // 2)
         return [global_state]
 
-    @StateTransition()
+    @StateTransition(enable_gas=False)
     def sha3_(self, global_state: GlobalState) -> List[GlobalState]:
         global keccak_function_manager
 
@@ -583,8 +609,15 @@ class Instruction:
             if is_expr(op0):
                 op0 = simplify(op0)
             state.stack.append(BitVec("KECCAC_mem[" + str(op0) + "]", 256))
+            state.min_gas_used += OPCODE_GAS["SHA3"][0]
+            state.max_gas_used += OPCODE_GAS["SHA3"][1]
             return [global_state]
 
+        min_gas, max_gas = OPCODE_GAS["SHA3_FUNC"](length)
+        state.min_gas_used += min_gas
+        state.max_gas_used += max_gas
+        StateTransition.check_gas_usage_limit(global_state)
+
         try:
             state.mem_extend(index, length)
             data = b"".join(
@@ -628,8 +661,9 @@ class Instruction:
             return [global_state]
 
         try:
-            concrete_size = helper.get_concrete_int(size)
+            size = helper.get_concrete_int(size)
-            global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
+            global_state.mstate.mem_extend(concrete_memory_offset, size)
+
         except TypeError:
             # except both attribute error and Exception
             global_state.mstate.mem_extend(concrete_memory_offset, 1)
@@ -647,8 +681,8 @@ class Instruction:
             concrete_code_offset = helper.get_concrete_int(code_offset)
         except TypeError:
             logging.debug("Unsupported symbolic code offset in CODECOPY")
-            global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
+            global_state.mstate.mem_extend(concrete_memory_offset, size)
-            for i in range(concrete_size):
+            for i in range(size):
                 global_state.mstate.memory[
                     concrete_memory_offset + i
                 ] = global_state.new_bitvec(
@@ -661,7 +695,7 @@ class Instruction:
 
         bytecode = global_state.environment.code.bytecode
 
-        if concrete_size == 0 and isinstance(
+        if size == 0 and isinstance(
             global_state.current_transaction, ContractCreationTransaction
         ):
             if concrete_code_offset >= len(global_state.environment.code.bytecode) // 2:
@@ -676,7 +710,7 @@ class Instruction:
                 )
                 return [global_state]
 
-        for i in range(concrete_size):
+        for i in range(size):
             if 2 * (concrete_code_offset + i + 1) <= len(bytecode):
                 global_state.mstate.memory[concrete_memory_offset + i] = int(
                     bytecode[
@@ -730,6 +764,7 @@ class Instruction:
         state = global_state.mstate
         addr = state.stack.pop()
         start, s2, size = state.stack.pop(), state.stack.pop(), state.stack.pop()
+
         return [global_state]
 
     @StateTransition()
@@ -770,7 +805,7 @@ class Instruction:
 
     @StateTransition()
     def gaslimit_(self, global_state: GlobalState) -> List[GlobalState]:
-        global_state.mstate.stack.append(global_state.new_bitvec("block_gaslimit", 256))
+        global_state.mstate.stack.append(global_state.mstate.gas_limit)
         return [global_state]
 
     # Memory operations
@@ -989,7 +1024,7 @@ class Instruction:
 
         return [global_state]
 
-    @StateTransition(increment_pc=False)
+    @StateTransition(increment_pc=False, enable_gas=False)
     def jump_(self, global_state: GlobalState) -> List[GlobalState]:
         state = global_state.mstate
         disassembly = global_state.environment.code
@@ -1012,15 +1047,22 @@ class Instruction:
             )
 
         new_state = copy(global_state)
+        # add JUMP gas cost
+        min_gas, max_gas = OPCODE_GAS["JUMP"]
+        new_state.mstate.min_gas_used += min_gas
+        new_state.mstate.max_gas_used += max_gas
+
+        # manually set PC to destination
         new_state.mstate.pc = index
         new_state.mstate.depth += 1
 
         return [new_state]
 
-    @StateTransition(increment_pc=False)
+    @StateTransition(increment_pc=False, enable_gas=False)
     def jumpi_(self, global_state: GlobalState) -> List[GlobalState]:
         state = global_state.mstate
         disassembly = global_state.environment.code
+        min_gas, max_gas = OPCODE_GAS["JUMPI"]
         states = []
 
         op0, condition = state.stack.pop(), state.stack.pop()
@@ -1030,6 +1072,8 @@ class Instruction:
         except TypeError:
             logging.debug("Skipping JUMPI to invalid destination.")
             global_state.mstate.pc += 1
+            global_state.mstate.min_gas_used += min_gas
+            global_state.mstate.max_gas_used += max_gas
             return [global_state]
 
         # False case
@@ -1041,6 +1085,11 @@ class Instruction:
             type(negated) == BoolRef and not is_false(negated)
         ):
             new_state = copy(global_state)
+            # add JUMPI gas cost
+            new_state.mstate.min_gas_used += min_gas
+            new_state.mstate.max_gas_used += max_gas
+
+            # manually increment PC
             new_state.mstate.depth += 1
             new_state.mstate.pc += 1
             new_state.mstate.constraints.append(negated)
@@ -1064,6 +1113,11 @@ class Instruction:
                 type(condi) == BoolRef and not is_false(condi)
             ):
                 new_state = copy(global_state)
+                # add JUMPI gas cost
+                new_state.mstate.min_gas_used += min_gas
+                new_state.mstate.max_gas_used += max_gas
+
+                # manually set PC to destination
                 new_state.mstate.pc = index
                 new_state.mstate.depth += 1
                 new_state.mstate.constraints.append(condi)
@@ -1094,7 +1148,7 @@ class Instruction:
         state = global_state.mstate
         dpth = int(self.op_code[3:])
         state.stack.pop(), state.stack.pop()
-        [state.stack.pop() for _ in range(dpth)]
+        log_data = [state.stack.pop() for _ in range(dpth)]
         # Not supported
         return [global_state]
 
@@ -1123,7 +1177,7 @@ class Instruction:
     @StateTransition()
     def suicide_(self, global_state: GlobalState):
         target = global_state.mstate.stack.pop()
-
+        account_created = False
         # Often the target of the suicide instruction will be symbolic
         # If it isn't then well transfer the balance to the indicated contract
         if isinstance(target, BitVecNumRef):
@@ -1138,10 +1192,17 @@ class Instruction:
                     address=target,
                     balance=global_state.environment.active_account.balance,
                 )
+                account_created = True
+
+        global_state.environment.active_account = deepcopy(
+            global_state.environment.active_account
+        )
+        global_state.accounts[
+            global_state.environment.active_account.address
+        ] = global_state.environment.active_account
 
         global_state.environment.active_account.balance = 0
         global_state.environment.active_account.deleted = True
-
         global_state.current_transaction.end(global_state)
 
     @StateTransition()
@@ -1210,12 +1271,18 @@ class Instruction:
                 logging.debug("CALL with symbolic start or offset not supported")
                 return [global_state]
 
-            global_state.mstate.mem_extend(mem_out_start, mem_out_sz)
+            contract_list = ["ecrecover", "sha256", "ripemd160", "identity"]
             call_address_int = int(callee_address, 16)
+            native_gas_min, native_gas_max = OPCODE_GAS["NATIVE_COST"](
+                global_state.mstate.calculate_extension_size(mem_out_start, mem_out_sz),
+                contract_list[call_address_int - 1],
+            )
+            global_state.mstate.min_gas_used += native_gas_min
+            global_state.mstate.max_gas_used += native_gas_max
+            global_state.mstate.mem_extend(mem_out_start, mem_out_sz)
             try:
                 data = natives.native_contracts(call_address_int, call_data)
             except natives.NativeContractException:
-                contract_list = ["ecerecover", "sha256", "ripemd160", "identity"]
                 for i in range(mem_out_sz):
                     global_state.mstate.memory[
                         mem_out_start + i
@@ -1226,7 +1293,6 @@ class Instruction:
                         + ")",
                         256,
                     )
-
                 return [global_state]
 
             for i in range(
@@ -1238,14 +1304,15 @@ class Instruction:
             return [global_state]
 
         transaction = MessageCallTransaction(
-            global_state.world_state,
+            world_state=global_state.world_state,
-            callee_account,
-            BitVecVal(int(environment.active_account.address, 16), 256),
-            call_data=call_data,
             gas_price=environment.gasprice,
-            call_value=value,
+            gas_limit=gas,
             origin=environment.origin,
+            caller=BitVecVal(int(environment.active_account.address, 16), 256),
+            callee_account=callee_account,
+            call_data=call_data,
             call_data_type=call_data_type,
+            call_value=value,
         )
         raise TransactionStartSignal(transaction, self.op_code)
 
@@ -1254,7 +1321,7 @@ class Instruction:
         instr = global_state.get_current_instruction()
 
         try:
-            _, _, _, _, _, _, memory_out_offset, memory_out_size = get_call_parameters(
+            callee_address, _, _, value, _, _, memory_out_offset, memory_out_size = get_call_parameters(
                 global_state, self.dynamic_loader, True
             )
         except ValueError as e:
@@ -1332,15 +1399,16 @@ class Instruction:
             return [global_state]
 
         transaction = MessageCallTransaction(
-            global_state.world_state,
+            world_state=global_state.world_state,
-            environment.active_account,
-            environment.address,
-            call_data=call_data,
             gas_price=environment.gasprice,
-            call_value=value,
+            gas_limit=gas,
             origin=environment.origin,
-            call_data_type=call_data_type,
             code=callee_account.code,
+            caller=environment.address,
+            callee_account=environment.active_account,
+            call_data=call_data,
+            call_data_type=call_data_type,
+            call_value=value,
         )
         raise TransactionStartSignal(transaction, self.op_code)
 
@@ -1349,7 +1417,7 @@ class Instruction:
         instr = global_state.get_current_instruction()
 
         try:
-            _, _, _, _, _, _, memory_out_offset, memory_out_size = get_call_parameters(
+            callee_address, _, _, value, _, _, memory_out_offset, memory_out_size = get_call_parameters(
                 global_state, self.dynamic_loader, True
             )
         except ValueError as e:
@@ -1370,7 +1438,6 @@ class Instruction:
             )
             global_state.mstate.stack.append(return_value)
             global_state.mstate.constraints.append(return_value == 0)
-
             return [global_state]
 
         try:
@@ -1403,7 +1470,6 @@ class Instruction:
         return_value = global_state.new_bitvec("retval_" + str(instr["address"]), 256)
         global_state.mstate.stack.append(return_value)
         global_state.mstate.constraints.append(return_value == 1)
-
         return [global_state]
 
     @StateTransition()
@@ -1412,7 +1478,7 @@ class Instruction:
         environment = global_state.environment
 
         try:
-            callee_address, callee_account, call_data, _, call_data_type, gas, _, _ = get_call_parameters(
+            callee_address, callee_account, call_data, value, call_data_type, gas, _, _ = get_call_parameters(
                 global_state, self.dynamic_loader
             )
         except ValueError as e:
@@ -1427,15 +1493,16 @@ class Instruction:
             return [global_state]
 
         transaction = MessageCallTransaction(
-            global_state.world_state,
+            world_state=global_state.world_state,
-            environment.active_account,
-            environment.sender,
-            call_data,
             gas_price=environment.gasprice,
-            call_value=environment.callvalue,
+            gas_limit=gas,
             origin=environment.origin,
-            call_data_type=call_data_type,
             code=callee_account.code,
+            caller=environment.sender,
+            callee_account=environment.active_account,
+            call_data=call_data,
+            call_data_type=call_data_type,
+            call_value=environment.callvalue,
         )
         raise TransactionStartSignal(transaction, self.op_code)
 
@@ -1444,7 +1511,7 @@ class Instruction:
         instr = global_state.get_current_instruction()
 
         try:
-            _, _, _, _, _, _, memory_out_offset, memory_out_size = get_call_parameters(
+            callee_address, _, _, value, _, _, memory_out_offset, memory_out_size = get_call_parameters(
                 global_state, self.dynamic_loader
             )
         except ValueError as e:
@@ -1465,7 +1532,6 @@ class Instruction:
             )
             global_state.mstate.stack.append(return_value)
             global_state.mstate.constraints.append(return_value == 0)
-
             return [global_state]
 
         try:
@@ -1498,7 +1564,6 @@ class Instruction:
         return_value = global_state.new_bitvec("retval_" + str(instr["address"]), 256)
         global_state.mstate.stack.append(return_value)
         global_state.mstate.constraints.append(return_value == 1)
-
         return [global_state]
 
     @StateTransition()

mythril/laser/ethereum/natives.py

@@ -8,7 +8,7 @@ from ethereum.utils import ecrecover_to_pub
 from py_ecc.secp256k1 import N as secp256k1n
 from rlp.utils import ALL_BYTES
 
-from mythril.laser.ethereum.state import Calldata
+from mythril.laser.ethereum.state.calldata import Calldata
 from mythril.laser.ethereum.util import bytearray_to_int, sha3, get_concrete_int
 from z3 import Concat, simplify
 

mythril/laser/ethereum/state.py

@@ -1,571 +0,0 @@
-import struct
-from z3 import (
-    BitVec,
-    BitVecVal,
-    BitVecRef,
-    BitVecSort,
-    ExprRef,
-    Concat,
-    sat,
-    simplify,
-    Array,
-    ForAll,
-    Implies,
-    UGE,
-    UGT,
-)
-from z3.z3types import Z3Exception
-from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.ethereum.cfg import Node
-from copy import copy, deepcopy
-from enum import Enum
-from random import randint
-from typing import KeysView, Dict, List, Union, Any, Sequence
-from mythril.laser.ethereum.util import get_concrete_int
-
-from mythril.laser.ethereum.evm_exceptions import (
-    StackOverflowException,
-    StackUnderflowException,
-)
-
-
-class CalldataType(Enum):
-    CONCRETE = 1
-    SYMBOLIC = 2
-
-
-class Calldata:
-    """
-    Calldata class representing the calldata of a transaction
-    """
-
-    def __init__(self, tx_id, starting_calldata=None):
-        """
-        Constructor for Calldata
-        :param tx_id: unique value representing the transaction the calldata is for
-        :param starting_calldata: byte array representing the concrete calldata of a transaction
-        """
-        self.tx_id = tx_id
-        if starting_calldata is not None:
-            self._calldata = []
-            self.calldatasize = BitVecVal(len(starting_calldata), 256)
-            self.concrete = True
-        else:
-            self._calldata = Array(
-                "{}_calldata".format(self.tx_id), BitVecSort(256), BitVecSort(8)
-            )
-            self.calldatasize = BitVec("{}_calldatasize".format(self.tx_id), 256)
-            self.concrete = False
-
-        if self.concrete:
-            for calldata_byte in starting_calldata:
-                if type(calldata_byte) == int:
-                    self._calldata.append(BitVecVal(calldata_byte, 8))
-                else:
-                    self._calldata.append(calldata_byte)
-
-    def concretized(self, model):
-        result = []
-        for i in range(
-            get_concrete_int(model.eval(self.calldatasize, model_completion=True))
-        ):
-            result.append(
-                get_concrete_int(model.eval(self._calldata[i], model_completion=True))
-            )
-
-        return result
-
-    def get_word_at(self, index: int):
-        return self[index : index + 32]
-
-    def __getitem__(self, item: Union[int, slice]) -> Any:
-        if isinstance(item, slice):
-            start, step, stop = item.start, item.step, item.stop
-            try:
-                if start is None:
-                    start = 0
-                if step is None:
-                    step = 1
-                if stop is None:
-                    stop = self.calldatasize
-                current_index = (
-                    start if isinstance(start, BitVecRef) else BitVecVal(start, 256)
-                )
-                dataparts = []
-                while simplify(current_index != stop):
-                    dataparts.append(self[current_index])
-                    current_index = simplify(current_index + step)
-            except Z3Exception:
-                raise IndexError("Invalid Calldata Slice")
-
-            values, constraints = zip(*dataparts)
-            result_constraints = []
-            for c in constraints:
-                result_constraints.extend(c)
-            return simplify(Concat(values)), result_constraints
-
-        if self.concrete:
-            try:
-                return self._calldata[get_concrete_int(item)], ()
-            except IndexError:
-                return BitVecVal(0, 8), ()
-        else:
-            constraints = [
-                Implies(self._calldata[item] != 0, UGT(self.calldatasize, item))
-            ]
-
-            return self._calldata[item], constraints
-
-
-class Storage:
-    """
-    Storage class represents the storage of an Account
-    """
-
-    def __init__(self, concrete=False, address=None, dynamic_loader=None):
-        """
-        Constructor for Storage
-        :param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic
-        """
-        self._storage = {}
-        self.concrete = concrete
-        self.dynld = dynamic_loader
-        self.address = address
-
-    def __getitem__(self, item: Union[int, slice]) -> Any:
-        try:
-            return self._storage[item]
-        except KeyError:
-            if (
-                self.address
-                and int(self.address[2:], 16) != 0
-                and (self.dynld and self.dynld.storage_loading)
-            ):
-                try:
-                    self._storage[item] = int(
-                        self.dynld.read_storage(
-                            contract_address=self.address, index=int(item)
-                        ),
-                        16,
-                    )
-                    return self._storage[item]
-                except ValueError:
-                    pass
-        if self.concrete:
-            return 0
-        self._storage[item] = BitVec("storage_" + str(item), 256)
-        return self._storage[item]
-
-    def __setitem__(self, key: str, value: ExprRef) -> None:
-        self._storage[key] = value
-
-    def keys(self) -> KeysView:
-        return self._storage.keys()
-
-
-class Account:
-    """
-    Account class representing ethereum accounts
-    """
-
-    def __init__(
-        self,
-        address: str,
-        code=None,
-        contract_name="unknown",
-        balance=None,
-        concrete_storage=False,
-        dynamic_loader=None,
-    ):
-        """
-        Constructor for account
-        :param address: Address of the account
-        :param code: The contract code of the account
-        :param contract_name: The name associated with the account
-        :param balance: The balance for the account
-        :param concrete_storage: Interpret storage as concrete
-        """
-        self.nonce = 0
-        self.code = code or Disassembly("")
-        self.balance = balance if balance else BitVec("balance", 256)
-        self.storage = Storage(
-            concrete_storage, address=address, dynamic_loader=dynamic_loader
-        )
-
-        # Metadata
-        self.address = address
-        self.contract_name = contract_name
-
-        self.deleted = False
-
-    def __str__(self) -> str:
-        return str(self.as_dict)
-
-    def set_balance(self, balance: ExprRef) -> None:
-        self.balance = balance
-
-    def add_balance(self, balance: ExprRef) -> None:
-        self.balance += balance
-
-    @property
-    def as_dict(self) -> Dict:
-        return {
-            "nonce": self.nonce,
-            "code": self.code,
-            "balance": self.balance,
-            "storage": self.storage,
-        }
-
-
-class Environment:
-    """
-    The environment class represents the current execution environment for the symbolic executor
-    """
-
-    def __init__(
-        self,
-        active_account: Account,
-        sender: ExprRef,
-        calldata: Calldata,
-        gasprice: ExprRef,
-        callvalue: ExprRef,
-        origin: ExprRef,
-        code=None,
-        calldata_type=CalldataType.SYMBOLIC,
-    ):
-        # Metadata
-
-        self.active_account = active_account
-        self.active_function_name = ""
-
-        self.address = BitVecVal(int(active_account.address, 16), 256)
-
-        # Ib
-        self.code = active_account.code if code is None else code
-
-        self.sender = sender
-        self.calldata = calldata
-        self.calldata_type = calldata_type
-        self.gasprice = gasprice
-        self.origin = origin
-        self.callvalue = callvalue
-
-    def __str__(self) -> str:
-        return str(self.as_dict)
-
-    @property
-    def as_dict(self) -> Dict:
-        return dict(
-            active_account=self.active_account,
-            sender=self.sender,
-            calldata=self.calldata,
-            gasprice=self.gasprice,
-            callvalue=self.callvalue,
-            origin=self.origin,
-            calldata_type=self.calldata_type,
-        )
-
-
-class Constraints(list):
-    """
-    This class should maintain a solver and it's constraints, This class tries to make the Constraints() object
-    as a simple list of constraints with some background processing.
-    TODO: add the solver to this class after callback refactor
-    """
-
-    def __init__(self, constraint_list=None, solver=None, possibility=None):
-        super(Constraints, self).__init__(constraint_list or [])
-        self.solver = solver
-        self.__possibility = possibility
-
-    def check_possibility(self):
-        return True
-
-    def append(self, constraint):
-        super(Constraints, self).append(constraint)
-
-    def pop(self, index=-1):
-        raise NotImplementedError
-
-    def __copy__(self):
-        constraint_list = super(Constraints, self).copy()
-        return Constraints(constraint_list)
-
-    def __deepcopy__(self, memodict=None):
-        return self.__copy__()
-
-    def __add__(self, constraints):
-        constraints_list = super(Constraints, self).__add__(constraints)
-        return Constraints(constraint_list=constraints_list)
-
-    def __iadd__(self, constraints):
-        super(Constraints, self).__iadd__(constraints)
-        return self
-
-
-class MachineStack(list):
-    """
-    Defines EVM stack, overrides the default list to handle overflows
-    """
-
-    STACK_LIMIT = 1024
-
-    def __init__(self, default_list=None):
-        if default_list is None:
-            default_list = []
-        super(MachineStack, self).__init__(default_list)
-
-    def append(self, element: BitVec) -> None:
-        """
-        :param element: element to be appended to the list
-        :function: appends the element to list if the size is less than STACK_LIMIT, else throws an error
-        """
-        if super(MachineStack, self).__len__() >= self.STACK_LIMIT:
-            raise StackOverflowException(
-                "Reached the EVM stack limit of {}, you can't append more "
-                "elements".format(self.STACK_LIMIT)
-            )
-        super(MachineStack, self).append(element)
-
-    def pop(self, index=-1) -> BitVec:
-        """
-        :param index:index to be popped, same as the list() class.
-        :returns popped value
-        :function: same as list() class but throws StackUnderflowException for popping from an empty list
-        """
-
-        try:
-            return super(MachineStack, self).pop(index)
-        except IndexError:
-            raise StackUnderflowException("Trying to pop from an empty stack")
-
-    def __getitem__(self, item: Union[int, slice]) -> Any:
-        try:
-            return super(MachineStack, self).__getitem__(item)
-        except IndexError:
-            raise StackUnderflowException(
-                "Trying to access a stack element which doesn't exist"
-            )
-
-    def __add__(self, other):
-        """
-        Implement list concatenation if needed
-        """
-        raise NotImplementedError("Implement this if needed")
-
-    def __iadd__(self, other):
-        """
-        Implement list concatenation if needed
-        """
-        raise NotImplementedError("Implement this if needed")
-
-
-class MachineState:
-    """
-    MachineState represents current machine state also referenced to as \mu
-    """
-
-    def __init__(
-        self, gas: int, pc=0, stack=None, memory=None, constraints=None, depth=0
-    ):
-        """ Constructor for machineState """
-        self.pc = pc
-        self.stack = MachineStack(stack)
-        self.memory = memory or []
-        self.gas = gas
-        self.constraints = constraints or Constraints()
-        self.depth = depth
-
-    def mem_extend(self, start: int, size: int) -> None:
-        """
-        Extends the memory of this machine state
-        :param start: Start of memory extension
-        :param size: Size of memory extension
-        """
-        if self.memory_size > start + size:
-            return
-        m_extend = start + size - self.memory_size
-        self.memory.extend(bytearray(m_extend))
-
-    def memory_write(self, offset: int, data: List[int]) -> None:
-        """ Writes data to memory starting at offset """
-        self.mem_extend(offset, len(data))
-        self.memory[offset : offset + len(data)] = data
-
-    def pop(self, amount=1) -> Union[BitVec, List[BitVec]]:
-        """ Pops amount elements from the stack"""
-        if amount > len(self.stack):
-            raise StackUnderflowException
-        values = self.stack[-amount:][::-1]
-        del self.stack[-amount:]
-
-        return values[0] if amount == 1 else values
-
-    def __deepcopy__(self, memodict=None):
-        memodict = {} if memodict is None else memodict
-        return MachineState(
-            gas=self.gas,
-            pc=self.pc,
-            stack=copy(self.stack),
-            memory=copy(self.memory),
-            constraints=copy(self.constraints),
-            depth=self.depth,
-        )
-
-    def __str__(self):
-        return str(self.as_dict)
-
-    @property
-    def memory_size(self) -> int:
-        return len(self.memory)
-
-    @property
-    def as_dict(self) -> Dict:
-        return dict(
-            pc=self.pc,
-            stack=self.stack,
-            memory=self.memory,
-            memsize=self.memory_size,
-            gas=self.gas,
-        )
-
-
-class GlobalState:
-    """
-    GlobalState represents the current globalstate
-    """
-
-    def __init__(
-        self,
-        world_state: "WorldState",
-        environment: Environment,
-        node: Node,
-        machine_state=None,
-        transaction_stack=None,
-        last_return_data=None,
-    ):
-        """ Constructor for GlobalState"""
-        self.node = node
-        self.world_state = world_state
-        self.environment = environment
-        self.mstate = machine_state if machine_state else MachineState(gas=10000000)
-        self.transaction_stack = transaction_stack if transaction_stack else []
-        self.op_code = ""
-        self.last_return_data = last_return_data
-
-    def __copy__(self) -> "GlobalState":
-        world_state = copy(self.world_state)
-        environment = copy(self.environment)
-        mstate = deepcopy(self.mstate)
-        transaction_stack = copy(self.transaction_stack)
-        return GlobalState(
-            world_state,
-            environment,
-            self.node,
-            mstate,
-            transaction_stack=transaction_stack,
-            last_return_data=self.last_return_data,
-        )
-
-    @property
-    def accounts(self) -> Dict:
-        return self.world_state.accounts
-
-    # TODO: remove this, as two instructions are confusing
-    def get_current_instruction(self) -> Dict:
-        """ Gets the current instruction for this GlobalState"""
-
-        instructions = self.environment.code.instruction_list
-        return instructions[self.mstate.pc]
-
-    @property
-    def current_transaction(
-        self
-    ) -> Union["MessageCallTransaction", "ContractCreationTransaction", None]:
-        # TODO: Remove circular to transaction package to import Transaction classes
-        try:
-            return self.transaction_stack[-1][0]
-        except IndexError:
-            return None
-
-    @property
-    def instruction(self) -> Dict:
-        return self.get_current_instruction()
-
-    def new_bitvec(self, name: str, size=256) -> BitVec:
-        transaction_id = self.current_transaction.id
-        return BitVec("{}_{}".format(transaction_id, name), size)
-
-
-class WorldState:
-    """
-    The WorldState class represents the world state as described in the yellow paper
-    """
-
-    def __init__(self, transaction_sequence=None):
-        """
-        Constructor for the world state. Initializes the accounts record
-        """
-        self.accounts = {}
-        self.node = None
-        self.transaction_sequence = transaction_sequence or []
-
-    def __getitem__(self, item: str) -> Account:
-        """
-        Gets an account from the worldstate using item as key
-        :param item: Address of the account to get
-        :return: Account associated with the address
-        """
-        return self.accounts[item]
-
-    def __copy__(self) -> "WorldState":
-        new_world_state = WorldState(transaction_sequence=self.transaction_sequence[:])
-        new_world_state.accounts = copy(self.accounts)
-        new_world_state.node = self.node
-        return new_world_state
-
-    def create_account(
-        self, balance=0, address=None, concrete_storage=False, dynamic_loader=None
-    ) -> Account:
-        """
-        Create non-contract account
-        :param address: The account's address
-        :param balance: Initial balance for the account
-        :param concrete_storage: Interpret account storage as concrete
-        :param dynamic_loader: used for dynamically loading storage from the block chain
-        :return: The new account
-        """
-        address = address if address else self._generate_new_address()
-        new_account = Account(
-            address,
-            balance=balance,
-            dynamic_loader=dynamic_loader,
-            concrete_storage=concrete_storage,
-        )
-        self._put_account(new_account)
-        return new_account
-
-    def create_initialized_contract_account(self, contract_code, storage) -> None:
-        """
-        Creates a new contract account, based on the contract code and storage provided
-        The contract code only includes the runtime contract bytecode
-        :param contract_code: Runtime bytecode for the contract
-        :param storage: Initial storage for the contract
-        :return: The new account
-        """
-        # TODO: Add type hints
-        new_account = Account(
-            self._generate_new_address(), code=contract_code, balance=0
-        )
-        new_account.storage = storage
-        self._put_account(new_account)
-
-    def _generate_new_address(self) -> str:
-        """ Generates a new address for the global state"""
-        while True:
-            address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(20)])
-            if address not in self.accounts.keys():
-                return address
-
-    def _put_account(self, account: Account) -> None:
-        self.accounts[account.address] = account

mythril/laser/ethereum/state/__init__.py

@@ -0,0 +1 @@
+# Hello!

mythril/laser/ethereum/state/account.py

@@ -0,0 +1,105 @@
+from typing import Dict, Union, Any, KeysView
+
+from z3 import BitVec, ExprRef
+
+from mythril.disassembler.disassembly import Disassembly
+
+
+class Storage:
+    """
+    Storage class represents the storage of an Account
+    """
+
+    def __init__(self, concrete=False, address=None, dynamic_loader=None):
+        """
+        Constructor for Storage
+        :param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic
+        """
+        self._storage = {}
+        self.concrete = concrete
+        self.dynld = dynamic_loader
+        self.address = address
+
+    def __getitem__(self, item: Union[int, slice]) -> Any:
+        try:
+            return self._storage[item]
+        except KeyError:
+            if (
+                self.address
+                and int(self.address[2:], 16) != 0
+                and (self.dynld and self.dynld.storage_loading)
+            ):
+                try:
+                    self._storage[item] = int(
+                        self.dynld.read_storage(
+                            contract_address=self.address, index=int(item)
+                        ),
+                        16,
+                    )
+                    return self._storage[item]
+                except ValueError:
+                    pass
+        if self.concrete:
+            return 0
+        self._storage[item] = BitVec("storage_" + str(item), 256)
+        return self._storage[item]
+
+    def __setitem__(self, key: str, value: ExprRef) -> None:
+        self._storage[key] = value
+
+    def keys(self) -> KeysView:
+        return self._storage.keys()
+
+
+class Account:
+    """
+    Account class representing ethereum accounts
+    """
+
+    def __init__(
+        self,
+        address: str,
+        code=None,
+        contract_name="unknown",
+        balance=None,
+        concrete_storage=False,
+        dynamic_loader=None,
+    ):
+        """
+        Constructor for account
+        :param address: Address of the account
+        :param code: The contract code of the account
+        :param contract_name: The name associated with the account
+        :param balance: The balance for the account
+        :param concrete_storage: Interpret storage as concrete
+        """
+        self.nonce = 0
+        self.code = code or Disassembly("")
+        self.balance = balance if balance else BitVec("balance", 256)
+        self.storage = Storage(
+            concrete_storage, address=address, dynamic_loader=dynamic_loader
+        )
+
+        # Metadata
+        self.address = address
+        self.contract_name = contract_name
+
+        self.deleted = False
+
+    def __str__(self) -> str:
+        return str(self.as_dict)
+
+    def set_balance(self, balance: ExprRef) -> None:
+        self.balance = balance
+
+    def add_balance(self, balance: ExprRef) -> None:
+        self.balance += balance
+
+    @property
+    def as_dict(self) -> Dict:
+        return {
+            "nonce": self.nonce,
+            "code": self.code,
+            "balance": self.balance,
+            "storage": self.storage,
+        }

mythril/laser/ethereum/state/calldata.py

@@ -0,0 +1,104 @@
+from enum import Enum
+from typing import Union, Any
+from z3 import (
+    BitVecVal,
+    BitVecRef,
+    BitVecSort,
+    BitVec,
+    Implies,
+    simplify,
+    Concat,
+    UGT,
+    Array,
+)
+from z3.z3types import Z3Exception
+
+from mythril.laser.ethereum.util import get_concrete_int
+
+
+class CalldataType(Enum):
+    CONCRETE = 1
+    SYMBOLIC = 2
+
+
+class Calldata:
+    """
+    Calldata class representing the calldata of a transaction
+    """
+
+    def __init__(self, tx_id, starting_calldata=None):
+        """
+        Constructor for Calldata
+        :param tx_id: unique value representing the transaction the calldata is for
+        :param starting_calldata: byte array representing the concrete calldata of a transaction
+        """
+        self.tx_id = tx_id
+        if starting_calldata is not None:
+            self._calldata = []
+            self.calldatasize = BitVecVal(len(starting_calldata), 256)
+            self.concrete = True
+        else:
+            self._calldata = Array(
+                "{}_calldata".format(self.tx_id), BitVecSort(256), BitVecSort(8)
+            )
+            self.calldatasize = BitVec("{}_calldatasize".format(self.tx_id), 256)
+            self.concrete = False
+
+        if self.concrete:
+            for calldata_byte in starting_calldata:
+                if type(calldata_byte) == int:
+                    self._calldata.append(BitVecVal(calldata_byte, 8))
+                else:
+                    self._calldata.append(calldata_byte)
+
+    def concretized(self, model):
+        result = []
+        for i in range(
+            get_concrete_int(model.eval(self.calldatasize, model_completion=True))
+        ):
+            result.append(
+                get_concrete_int(model.eval(self._calldata[i], model_completion=True))
+            )
+
+        return result
+
+    def get_word_at(self, index: int):
+        return self[index : index + 32]
+
+    def __getitem__(self, item: Union[int, slice]) -> Any:
+        if isinstance(item, slice):
+            start, step, stop = item.start, item.step, item.stop
+            try:
+                if start is None:
+                    start = 0
+                if step is None:
+                    step = 1
+                if stop is None:
+                    stop = self.calldatasize
+                current_index = (
+                    start if isinstance(start, BitVecRef) else BitVecVal(start, 256)
+                )
+                dataparts = []
+                while simplify(current_index != stop):
+                    dataparts.append(self[current_index])
+                    current_index = simplify(current_index + step)
+            except Z3Exception:
+                raise IndexError("Invalid Calldata Slice")
+
+            values, constraints = zip(*dataparts)
+            result_constraints = []
+            for c in constraints:
+                result_constraints.extend(c)
+            return simplify(Concat(values)), result_constraints
+
+        if self.concrete:
+            try:
+                return self._calldata[get_concrete_int(item)], ()
+            except IndexError:
+                return BitVecVal(0, 8), ()
+        else:
+            constraints = [
+                Implies(self._calldata[item] != 0, UGT(self.calldatasize, item))
+            ]
+
+            return self._calldata[item], constraints

mythril/laser/ethereum/state/constraints.py

@@ -0,0 +1,35 @@
+class Constraints(list):
+    """
+    This class should maintain a solver and it's constraints, This class tries to make the Constraints() object
+    as a simple list of constraints with some background processing.
+    TODO: add the solver to this class after callback refactor
+    """
+
+    def __init__(self, constraint_list=None, solver=None, possibility=None):
+        super(Constraints, self).__init__(constraint_list or [])
+        self.solver = solver
+        self.__possibility = possibility
+
+    def check_possibility(self):
+        return True
+
+    def append(self, constraint):
+        super(Constraints, self).append(constraint)
+
+    def pop(self, index=-1):
+        raise NotImplementedError
+
+    def __copy__(self):
+        constraint_list = super(Constraints, self).copy()
+        return Constraints(constraint_list)
+
+    def __deepcopy__(self, memodict=None):
+        return self.__copy__()
+
+    def __add__(self, constraints):
+        constraints_list = super(Constraints, self).__add__(constraints)
+        return Constraints(constraint_list=constraints_list)
+
+    def __iadd__(self, constraints):
+        super(Constraints, self).__iadd__(constraints)
+        return self

mythril/laser/ethereum/state/environment.py

@@ -0,0 +1,55 @@
+from typing import Dict
+
+from z3 import ExprRef, BitVecVal
+
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.calldata import Calldata, CalldataType
+
+
+class Environment:
+    """
+    The environment class represents the current execution environment for the symbolic executor
+    """
+
+    def __init__(
+        self,
+        active_account: Account,
+        sender: ExprRef,
+        calldata: Calldata,
+        gasprice: ExprRef,
+        callvalue: ExprRef,
+        origin: ExprRef,
+        code=None,
+        calldata_type=CalldataType.SYMBOLIC,
+    ):
+        # Metadata
+
+        self.active_account = active_account
+        self.active_function_name = ""
+
+        self.address = BitVecVal(int(active_account.address, 16), 256)
+
+        # Ib
+        self.code = active_account.code if code is None else code
+
+        self.sender = sender
+        self.calldata = calldata
+        self.calldata_type = calldata_type
+        self.gasprice = gasprice
+        self.origin = origin
+        self.callvalue = callvalue
+
+    def __str__(self) -> str:
+        return str(self.as_dict)
+
+    @property
+    def as_dict(self) -> Dict:
+        return dict(
+            active_account=self.active_account,
+            sender=self.sender,
+            calldata=self.calldata,
+            gasprice=self.gasprice,
+            callvalue=self.callvalue,
+            origin=self.origin,
+            calldata_type=self.calldata_type,
+        )

mythril/laser/ethereum/state/global_state.py

@@ -0,0 +1,77 @@
+from typing import Dict, Union
+
+from copy import copy, deepcopy
+from z3 import BitVec
+
+from mythril.laser.ethereum.cfg import Node
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.machine_state import MachineState
+
+
+class GlobalState:
+    """
+    GlobalState represents the current globalstate
+    """
+
+    def __init__(
+        self,
+        world_state: "WorldState",
+        environment: Environment,
+        node: Node,
+        machine_state=None,
+        transaction_stack=None,
+        last_return_data=None,
+    ):
+        """ Constructor for GlobalState"""
+        self.node = node
+        self.world_state = world_state
+        self.environment = environment
+        self.mstate = (
+            machine_state if machine_state else MachineState(gas_limit=1000000000)
+        )
+        self.transaction_stack = transaction_stack if transaction_stack else []
+        self.op_code = ""
+        self.last_return_data = last_return_data
+
+    def __copy__(self) -> "GlobalState":
+        world_state = copy(self.world_state)
+        environment = copy(self.environment)
+        mstate = deepcopy(self.mstate)
+        transaction_stack = copy(self.transaction_stack)
+        return GlobalState(
+            world_state,
+            environment,
+            self.node,
+            mstate,
+            transaction_stack=transaction_stack,
+            last_return_data=self.last_return_data,
+        )
+
+    @property
+    def accounts(self) -> Dict:
+        return self.world_state.accounts
+
+    # TODO: remove this, as two instructions are confusing
+    def get_current_instruction(self) -> Dict:
+        """ Gets the current instruction for this GlobalState"""
+
+        instructions = self.environment.code.instruction_list
+        return instructions[self.mstate.pc]
+
+    @property
+    def current_transaction(
+        self
+    ) -> Union["MessageCallTransaction", "ContractCreationTransaction", None]:
+        # TODO: Remove circular to transaction package to import Transaction classes
+        try:
+            return self.transaction_stack[-1][0]
+        except IndexError:
+            return None
+
+    @property
+    def instruction(self) -> Dict:
+        return self.get_current_instruction()
+
+    def new_bitvec(self, name: str, size=256) -> BitVec:
+        transaction_id = self.current_transaction.id
+        return BitVec("{}_{}".format(transaction_id, name), size)

mythril/laser/ethereum/state/machine_state.py

@@ -0,0 +1,177 @@
+from copy import copy
+from typing import Union, Any, List, Dict
+
+from z3 import BitVec
+
+from ethereum import opcodes, utils
+from mythril.laser.ethereum.evm_exceptions import (
+    StackOverflowException,
+    StackUnderflowException,
+    OutOfGasException,
+)
+from mythril.laser.ethereum.state.constraints import Constraints
+
+
+class MachineStack(list):
+    """
+    Defines EVM stack, overrides the default list to handle overflows
+    """
+
+    STACK_LIMIT = 1024
+
+    def __init__(self, default_list=None):
+        if default_list is None:
+            default_list = []
+        super(MachineStack, self).__init__(default_list)
+
+    def append(self, element: BitVec) -> None:
+        """
+        :param element: element to be appended to the list
+        :function: appends the element to list if the size is less than STACK_LIMIT, else throws an error
+        """
+        if super(MachineStack, self).__len__() >= self.STACK_LIMIT:
+            raise StackOverflowException(
+                "Reached the EVM stack limit of {}, you can't append more "
+                "elements".format(self.STACK_LIMIT)
+            )
+        super(MachineStack, self).append(element)
+
+    def pop(self, index=-1) -> BitVec:
+        """
+        :param index:index to be popped, same as the list() class.
+        :returns popped value
+        :function: same as list() class but throws StackUnderflowException for popping from an empty list
+        """
+
+        try:
+            return super(MachineStack, self).pop(index)
+        except IndexError:
+            raise StackUnderflowException("Trying to pop from an empty stack")
+
+    def __getitem__(self, item: Union[int, slice]) -> Any:
+        try:
+            return super(MachineStack, self).__getitem__(item)
+        except IndexError:
+            raise StackUnderflowException(
+                "Trying to access a stack element which doesn't exist"
+            )
+
+    def __add__(self, other):
+        """
+        Implement list concatenation if needed
+        """
+        raise NotImplementedError("Implement this if needed")
+
+    def __iadd__(self, other):
+        """
+        Implement list concatenation if needed
+        """
+        raise NotImplementedError("Implement this if needed")
+
+
+class MachineState:
+    """
+    MachineState represents current machine state also referenced to as \mu
+    """
+
+    def __init__(
+        self,
+        gas_limit: int,
+        pc=0,
+        stack=None,
+        memory=None,
+        constraints=None,
+        depth=0,
+        max_gas_used=0,
+        min_gas_used=0,
+    ):
+        """ Constructor for machineState """
+        self.pc = pc
+        self.stack = MachineStack(stack)
+        self.memory = memory or []
+        self.gas_limit = gas_limit
+        self.min_gas_used = min_gas_used  # lower gas usage bound
+        self.max_gas_used = max_gas_used  # upper gas usage bound
+        self.constraints = constraints or Constraints()
+        self.depth = depth
+
+    def calculate_extension_size(self, start: int, size: int) -> int:
+        if self.memory_size > start + size:
+            return 0
+        return start + size - self.memory_size
+
+    def calculate_memory_gas(self, start: int, size: int):
+        # https://github.com/ethereum/pyethereum/blob/develop/ethereum/vm.py#L148
+        oldsize = self.memory_size // 32
+        old_totalfee = (
+            oldsize * opcodes.GMEMORY + oldsize ** 2 // opcodes.GQUADRATICMEMDENOM
+        )
+        newsize = utils.ceil32(start + size) // 32
+        new_totalfee = (
+            newsize * opcodes.GMEMORY + newsize ** 2 // opcodes.GQUADRATICMEMDENOM
+        )
+        return new_totalfee - old_totalfee
+
+    def check_gas(self):
+        if self.min_gas_used > self.gas_limit:
+            raise OutOfGasException()
+
+    def mem_extend(self, start: int, size: int) -> None:
+        """
+        Extends the memory of this machine state
+        :param start: Start of memory extension
+        :param size: Size of memory extension
+        """
+        m_extend = self.calculate_extension_size(start, size)
+        if m_extend:
+            extend_gas = self.calculate_memory_gas(start, size)
+            self.min_gas_used += extend_gas
+            self.max_gas_used += extend_gas
+            self.check_gas()
+            self.memory.extend(bytearray(m_extend))
+
+    def memory_write(self, offset: int, data: List[int]) -> None:
+        """ Writes data to memory starting at offset """
+        self.mem_extend(offset, len(data))
+        self.memory[offset : offset + len(data)] = data
+
+    def pop(self, amount=1) -> Union[BitVec, List[BitVec]]:
+        """ Pops amount elements from the stack"""
+        if amount > len(self.stack):
+            raise StackUnderflowException
+        values = self.stack[-amount:][::-1]
+        del self.stack[-amount:]
+
+        return values[0] if amount == 1 else values
+
+    def __deepcopy__(self, memodict=None):
+        memodict = {} if memodict is None else memodict
+        return MachineState(
+            gas_limit=self.gas_limit,
+            max_gas_used=self.max_gas_used,
+            min_gas_used=self.min_gas_used,
+            pc=self.pc,
+            stack=copy(self.stack),
+            memory=copy(self.memory),
+            constraints=copy(self.constraints),
+            depth=self.depth,
+        )
+
+    def __str__(self):
+        return str(self.as_dict)
+
+    @property
+    def memory_size(self) -> int:
+        return len(self.memory)
+
+    @property
+    def as_dict(self) -> Dict:
+        return dict(
+            pc=self.pc,
+            stack=self.stack,
+            memory=self.memory,
+            memsize=self.memory_size,
+            gas=self.gas_limit,
+            max_gas_used=self.max_gas_used,
+            min_gas_used=self.min_gas_used,
+        )

mythril/laser/ethereum/state/world_state.py

@@ -0,0 +1,78 @@
+from copy import copy
+from random import randint
+
+from mythril.laser.ethereum.state.account import Account
+
+
+class WorldState:
+    """
+    The WorldState class represents the world state as described in the yellow paper
+    """
+
+    def __init__(self, transaction_sequence=None):
+        """
+        Constructor for the world state. Initializes the accounts record
+        """
+        self.accounts = {}
+        self.node = None
+        self.transaction_sequence = transaction_sequence or []
+
+    def __getitem__(self, item: str) -> Account:
+        """
+        Gets an account from the worldstate using item as key
+        :param item: Address of the account to get
+        :return: Account associated with the address
+        """
+        return self.accounts[item]
+
+    def __copy__(self) -> "WorldState":
+        new_world_state = WorldState(transaction_sequence=self.transaction_sequence[:])
+        new_world_state.accounts = copy(self.accounts)
+        new_world_state.node = self.node
+        return new_world_state
+
+    def create_account(
+        self, balance=0, address=None, concrete_storage=False, dynamic_loader=None
+    ) -> Account:
+        """
+        Create non-contract account
+        :param address: The account's address
+        :param balance: Initial balance for the account
+        :param concrete_storage: Interpret account storage as concrete
+        :param dynamic_loader: used for dynamically loading storage from the block chain
+        :return: The new account
+        """
+        address = address if address else self._generate_new_address()
+        new_account = Account(
+            address,
+            balance=balance,
+            dynamic_loader=dynamic_loader,
+            concrete_storage=concrete_storage,
+        )
+        self._put_account(new_account)
+        return new_account
+
+    def create_initialized_contract_account(self, contract_code, storage) -> None:
+        """
+        Creates a new contract account, based on the contract code and storage provided
+        The contract code only includes the runtime contract bytecode
+        :param contract_code: Runtime bytecode for the contract
+        :param storage: Initial storage for the contract
+        :return: The new account
+        """
+        # TODO: Add type hints
+        new_account = Account(
+            self._generate_new_address(), code=contract_code, balance=0
+        )
+        new_account.storage = storage
+        self._put_account(new_account)
+
+    def _generate_new_address(self) -> str:
+        """ Generates a new address for the global state"""
+        while True:
+            address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(20)])
+            if address not in self.accounts.keys():
+                return address
+
+    def _put_account(self, account: Account) -> None:
+        self.accounts[account.address] = account

mythril/laser/ethereum/strategy/basic.py

@@ -1,7 +1,7 @@
 """
 This module implements basic symbolic execution search strategies
 """
-from ..state import GlobalState
+from mythril.laser.ethereum.state.global_state import GlobalState
 from typing import List
 from random import randrange
 from . import BasicSearchStrategy

mythril/laser/ethereum/svm.py

@@ -1,7 +1,9 @@
 import logging
 from typing import List, Tuple, Union, Callable, Dict
 from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.ethereum.state import WorldState, GlobalState
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction import (
     TransactionStartSignal,
     TransactionEndSignal,
@@ -10,7 +12,6 @@ from mythril.laser.ethereum.transaction import (
 from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
 from mythril.laser.ethereum.instructions import Instruction
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
-from mythril.laser.ethereum.state import Account
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
 from datetime import datetime, timedelta
 from copy import copy
@@ -154,17 +155,18 @@ class LaserEVM:
             )
         return total_covered_instructions
 
-    def exec(self, create=False) -> None:
+    def exec(self, create=False, track_gas=False) -> Union[List[GlobalState], None]:
+        final_states = []
         for global_state in self.strategy:
             if self.execution_timeout and not create:
                 if (
                     self.time + timedelta(seconds=self.execution_timeout)
                     <= datetime.now()
                 ):
-                    return
+                    return final_states + [global_state] if track_gas else None
             elif self.create_timeout and create:
                 if self.time + timedelta(seconds=self.create_timeout) <= datetime.now():
-                    return
+                    return final_states + [global_state] if track_gas else None
 
             try:
                 new_states, op_code = self.execute_state(global_state)
@@ -173,8 +175,12 @@ class LaserEVM:
                 continue
             self.manage_cfg(op_code, new_states)
 
-            self.work_list += new_states
+            if new_states:
+                self.work_list += new_states
+            elif track_gas:
+                final_states.append(global_state)
             self.total_states += len(new_states)
+        return final_states if track_gas else None
 
     def execute_state(
         self, global_state: GlobalState

mythril/laser/ethereum/taint_analysis.py

@@ -4,7 +4,8 @@ from typing import Union, List, Tuple
 from z3 import ExprRef
 import mythril.laser.ethereum.util as helper
 from mythril.laser.ethereum.cfg import JumpType, Node
-from mythril.laser.ethereum.state import GlobalState, Environment
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.analysis.symbolic import SymExecWrapper
 
 

mythril/laser/ethereum/transaction/concolic.py

@@ -1,17 +1,15 @@
+from typing import List, Union
 from mythril.laser.ethereum.transaction.transaction_models import (
     MessageCallTransaction,
     ContractCreationTransaction,
     get_next_transaction_id,
 )
 from z3 import BitVec
-from mythril.laser.ethereum.state import (
+from mythril.laser.ethereum.state.environment import Environment
-    GlobalState,
+from mythril.laser.ethereum.state.calldata import Calldata, CalldataType
-    Environment,
+from mythril.laser.ethereum.state.account import Account
-    CalldataType,
+from mythril.laser.ethereum.state.world_state import WorldState
-    Account,
+from mythril.laser.ethereum.state.global_state import GlobalState
-    WorldState,
-    Calldata,
-)
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 
@@ -23,10 +21,11 @@ def execute_message_call(
     origin_address,
     code,
     data,
-    gas,
+    gas_limit,
     gas_price,
     value,
-) -> None:
+    track_gas=False,
+) -> Union[None, List[GlobalState]]:
     """ Executes a message call transaction from all open states """
     # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
     open_states = laser_evm.open_states[:]
@@ -35,21 +34,22 @@ def execute_message_call(
     for open_world_state in open_states:
         next_transaction_id = get_next_transaction_id()
         transaction = MessageCallTransaction(
-            identifier=next_transaction_id,
             world_state=open_world_state,
-            callee_account=open_world_state[callee_address],
+            identifier=next_transaction_id,
-            caller=caller_address,
-            call_data=Calldata(next_transaction_id, data),
             gas_price=gas_price,
-            call_value=value,
+            gas_limit=gas_limit,
             origin=origin_address,
-            call_data_type=CalldataType.SYMBOLIC,
             code=Disassembly(code),
+            caller=caller_address,
+            callee_account=open_world_state[callee_address],
+            call_data=Calldata(next_transaction_id, data),
+            call_data_type=CalldataType.SYMBOLIC,
+            call_value=value,
         )
 
         _setup_global_state_for_execution(laser_evm, transaction)
 
-    laser_evm.exec()
+    return laser_evm.exec(track_gas=track_gas)
 
 
 def _setup_global_state_for_execution(laser_evm, transaction) -> None:

mythril/laser/ethereum/transaction/symbolic.py

@@ -3,7 +3,8 @@ from logging import debug
 
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
-from mythril.laser.ethereum.state import CalldataType, Account, Calldata
+from mythril.laser.ethereum.state.calldata import CalldataType, Calldata
+from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.transaction.transaction_models import (
     MessageCallTransaction,
     ContractCreationTransaction,
@@ -25,14 +26,15 @@ def execute_message_call(laser_evm, callee_address: str) -> None:
         next_transaction_id = get_next_transaction_id()
         transaction = MessageCallTransaction(
             world_state=open_world_state,
-            callee_account=open_world_state[callee_address],
-            caller=BitVec("caller{}".format(next_transaction_id), 256),
             identifier=next_transaction_id,
-            call_data=Calldata(next_transaction_id),
             gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
-            call_value=BitVec("call_value{}".format(next_transaction_id), 256),
+            gas_limit=8000000,  # block gas limit
             origin=BitVec("origin{}".format(next_transaction_id), 256),
+            caller=BitVec("caller{}".format(next_transaction_id), 256),
+            callee_account=open_world_state[callee_address],
+            call_data=Calldata(next_transaction_id),
             call_data_type=CalldataType.SYMBOLIC,
+            call_value=BitVec("call_value{}".format(next_transaction_id), 256),
         )
         _setup_global_state_for_execution(laser_evm, transaction)
 
@@ -56,16 +58,17 @@ def execute_contract_creation(
     for open_world_state in open_states:
         next_transaction_id = get_next_transaction_id()
         transaction = ContractCreationTransaction(
-            open_world_state,
+            world_state=open_world_state,
-            BitVec("creator{}".format(next_transaction_id), 256),
+            identifier=next_transaction_id,
-            next_transaction_id,
+            gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
-            new_account,
+            gas_limit=8000000,  # block gas limit
-            Disassembly(contract_initialization_code),
+            origin=BitVec("origin{}".format(next_transaction_id), 256),
-            [],
+            code=Disassembly(contract_initialization_code),
-            BitVec("gas_price{}".format(next_transaction_id), 256),
+            caller=BitVec("creator{}".format(next_transaction_id), 256),
-            BitVec("call_value{}".format(next_transaction_id), 256),
+            callee_account=new_account,
-            BitVec("origin{}".format(next_transaction_id), 256),
+            call_data=[],
-            CalldataType.SYMBOLIC,
+            call_data_type=CalldataType.SYMBOLIC,
+            call_value=BitVec("call_value{}".format(next_transaction_id), 256),
         )
         _setup_global_state_for_execution(laser_evm, transaction)
     laser_evm.exec(True)

mythril/laser/ethereum/transaction/transaction_models.py

@@ -1,13 +1,11 @@
 import logging
 from typing import Union
 from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.ethereum.state import (
+from mythril.laser.ethereum.state.environment import Environment
-    GlobalState,
+from mythril.laser.ethereum.state.calldata import Calldata
-    Environment,
+from mythril.laser.ethereum.state.account import Account
-    WorldState,
+from mythril.laser.ethereum.state.world_state import WorldState
-    Account,
+from mythril.laser.ethereum.state.global_state import GlobalState
-    Calldata,
-)
 from z3 import BitVec, ExprRef
 import array
 
@@ -40,53 +38,72 @@ class TransactionStartSignal(Exception):
         self.op_code = op_code
 
 
-class MessageCallTransaction:
+class BaseTransaction:
-    """ Transaction object models an transaction"""
+    """Basic transaction class holding common data."""
 
     def __init__(
         self,
         world_state: WorldState,
-        callee_account: Account,
+        callee_account: Account = None,
-        caller: ExprRef,
+        caller: ExprRef = None,
         call_data=None,
         identifier=None,
         gas_price=None,
-        call_value=None,
+        gas_limit=None,
         origin=None,
-        call_data_type=None,
         code=None,
+        call_data_type=None,
+        call_value=None,
+        init_call_data=True,
     ):
         assert isinstance(world_state, WorldState)
-        self.id = identifier or get_next_transaction_id()
         self.world_state = world_state
-        self.callee_account = callee_account
+        self.id = identifier or get_next_transaction_id()
-        self.caller = caller
+
-        self.call_data = (
-            Calldata(self.id, call_data)
-            if not isinstance(call_data, Calldata)
-            else call_data
-        )
         self.gas_price = (
-            BitVec("gasprice{}".format(identifier), 256)
+            gas_price
-            if gas_price is None
+            if gas_price is not None
-            else gas_price
+            else BitVec("gasprice{}".format(identifier), 256)
-        )
-        self.call_value = (
-            BitVec("callvalue{}".format(identifier), 256)
-            if call_value is None
-            else call_value
         )
+        self.gas_limit = gas_limit
+
         self.origin = (
-            BitVec("origin{}".format(identifier), 256) if origin is None else origin
+            origin if origin is not None else BitVec("origin{}".format(identifier), 256)
         )
+        self.code = code
+
+        self.caller = caller
+        self.callee_account = callee_account
+        if call_data is None and init_call_data:
+            self.call_data = Calldata(self.id, call_data)
+        else:
+            self.call_data = call_data if isinstance(call_data, Calldata) else None
         self.call_data_type = (
-            BitVec("call_data_type{}".format(identifier), 256)
+            call_data_type
-            if call_data_type is None
+            if call_data_type is not None
-            else call_data_type
+            else BitVec("call_data_type{}".format(identifier), 256)
         )
-        self.code = code
+        self.call_value = (
+            call_value
+            if call_value is not None
+            else BitVec("callvalue{}".format(identifier), 256)
+        )
+
         self.return_data = None
 
+    def initial_global_state_from_environment(self, environment, active_function):
+        # Initialize the execution environment
+        global_state = GlobalState(self.world_state, environment, None)
+        global_state.environment.active_function_name = active_function
+        return global_state
+
+
+class MessageCallTransaction(BaseTransaction):
+    """ Transaction object models an transaction"""
+
+    def __init__(self, *args, **kwargs):
+        super().__init__(*args, **kwargs)
+
     def initial_global_state(self) -> GlobalState:
         """Initialize the execution environment"""
         environment = Environment(
@@ -99,73 +116,25 @@ class MessageCallTransaction:
             code=self.code or self.callee_account.code,
             calldata_type=self.call_data_type,
         )
-
+        return super().initial_global_state_from_environment(
-        global_state = GlobalState(self.world_state, environment, None)
+            environment, active_function="fallback"
-        global_state.environment.active_function_name = "fallback"
+        )
-
-        return global_state
 
     def end(self, global_state: GlobalState, return_data=None, revert=False) -> None:
         self.return_data = return_data
         raise TransactionEndSignal(global_state, revert)
 
 
-class ContractCreationTransaction:
+class ContractCreationTransaction(BaseTransaction):
     """ Transaction object models an transaction"""
 
-    def __init__(
+    def __init__(self, *args, **kwargs):
-        self,
+        super().__init__(*args, **kwargs, init_call_data=False)
-        world_state: WorldState,
-        caller: ExprRef,
-        identifier=None,
-        callee_account=None,
-        code=None,
-        call_data=None,
-        gas_price=None,
-        call_value=None,
-        origin=None,
-        call_data_type=None,
-    ):
-        assert isinstance(world_state, WorldState)
-        self.id = identifier or get_next_transaction_id()
-        self.world_state = world_state
         # TODO: set correct balance for new account
-        self.callee_account = (
+        self.callee_account = self.callee_account or self.world_state.create_account(
-            callee_account
+            0, concrete_storage=True
-            if callee_account
-            else world_state.create_account(0, concrete_storage=True)
-        )
-
-        self.caller = caller
-
-        self.gas_price = (
-            BitVec("gasprice{}".format(identifier), 256)
-            if gas_price is None
-            else gas_price
-        )
-        self.call_value = (
-            BitVec("callvalue{}".format(identifier), 256)
-            if call_value is None
-            else call_value
-        )
-        self.origin = (
-            BitVec("origin{}".format(identifier), 256) if origin is None else origin
-        )
-        self.call_data_type = (
-            BitVec("call_data_type{}".format(identifier), 256)
-            if call_data_type is None
-            else call_data_type
         )
 
-        self.call_data = (
-            Calldata(self.id, call_data)
-            if not isinstance(call_data, Calldata)
-            else call_data
-        )
-        self.origin = origin
-        self.code = code
-        self.return_data = None
-
     def initial_global_state(self) -> GlobalState:
         """Initialize the execution environment"""
         environment = Environment(
@@ -178,11 +147,9 @@ class ContractCreationTransaction:
             self.code,
             calldata_type=self.call_data_type,
         )
-
+        return super().initial_global_state_from_environment(
-        global_state = GlobalState(self.world_state, environment, None)
+            environment, active_function="constructor"
-        global_state.environment.active_function_name = "constructor"
+        )
-
-        return global_state
 
     def end(self, global_state: GlobalState, return_data=None, revert=False):
 

tests/analysis/test_delegatecall.py

@@ -6,7 +6,9 @@ from mythril.analysis.modules.delegatecall import (
 from mythril.analysis.ops import Call, Variable, VarType
 from mythril.analysis.symbolic import SymExecWrapper
 from mythril.laser.ethereum.cfg import Node
-from mythril.laser.ethereum.state import GlobalState, Environment, Account
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.global_state import GlobalState
 import pytest
 from unittest.mock import MagicMock, patch
 import pytest_mock
@@ -181,7 +183,7 @@ def test_symbolic_call_calldata_to(mocker):
     )
 
 
-@patch("mythril.laser.ethereum.state.GlobalState.get_current_instruction")
+@patch("mythril.laser.ethereum.state.global_state.GlobalState.get_current_instruction")
 @patch("mythril.analysis.modules.delegatecall._concrete_call")
 @patch("mythril.analysis.modules.delegatecall._symbolic_call")
 def test_delegate_call(sym_mock, concrete_mock, curr_instruction):

tests/instructions/codecopy_test.py

@@ -1,13 +1,21 @@
 from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.ethereum.state import MachineState, GlobalState, Environment, Account
+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
 
 
 def test_codecopy_concrete():
     # Arrange
     active_account = Account("0x0", code=Disassembly("60606040"))
     environment = Environment(active_account, None, None, None, None, None)
-    og_state = GlobalState(None, environment, None, MachineState(gas=10000000))
+    og_state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
+    og_state.transaction_stack.append(
+        (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
+    )
 
     og_state.mstate.stack = [2, 2, 2]
     instruction = Instruction("codecopy", dynamic_loader=None)

tests/laser/evm_testsuite/VMTests/vmEnvironmentalInfo/calldatacopyUnderFlowerror.json

@@ -1,5 +1,5 @@
 {
-    "calldatacopyUnderFlow" : {
+    "calldatacopyUnderFlowerror" : {
         "_info" : {
             "comment" : "",
             "filledwith" : "testeth 1.5.0.dev2-52+commit.d419e0a2",

tests/laser/evm_testsuite/VMTests/vmSha3Test/sha3_3oog.json

@@ -1,5 +1,5 @@
 {
-    "sha3_3" : {
+    "sha3_3oog" : {
         "_info" : {
             "comment" : "",
             "filledwith" : "cpp-1.3.0+commit.6e0ce939.Linux.g++",

tests/laser/evm_testsuite/VMTests/vmSha3Test/sha3_4oog.json

@@ -1,5 +1,5 @@
 {
-    "sha3_4" : {
+    "sha3_4oog" : {
         "_info" : {
             "comment" : "",
             "filledwith" : "cpp-1.3.0+commit.6e0ce939.Linux.g++",

tests/laser/evm_testsuite/VMTests/vmSha3Test/sha3_5oog.json

@@ -1,5 +1,5 @@
 {
-    "sha3_5" : {
+    "sha3_5oog" : {
         "_info" : {
             "comment" : "",
             "filledwith" : "cpp-1.3.0+commit.6e0ce939.Linux.g++",

tests/laser/evm_testsuite/VMTests/vmSha3Test/sha3_6oog.json

@@ -1,5 +1,5 @@
 {
-    "sha3_6" : {
+    "sha3_6oog" : {
         "_info" : {
             "comment" : "",
             "filledwith" : "cpp-1.3.0+commit.6e0ce939.Linux.g++",

tests/laser/evm_testsuite/VMTests/vmSha3Test/sha3_bigOffsetoog.json

@@ -1,5 +1,5 @@
 {
-    "sha3_bigOffset" : {
+    "sha3_bigOffsetoog" : {
         "_info" : {
             "comment" : "",
             "filledwith" : "cpp-1.3.0+commit.6e0ce939.Linux.g++",

tests/laser/evm_testsuite/VMTests/vmSha3Test/sha3_bigSizeoog.json

@@ -1,5 +1,5 @@
 {
-    "sha3_bigSize" : {
+    "sha3_bigSizeoog" : {
         "_info" : {
             "comment" : "",
             "filledwith" : "cpp-1.3.0+commit.6e0ce939.Linux.g++",

tests/laser/evm_testsuite/evm_test.py

@@ -1,5 +1,5 @@
 from mythril.laser.ethereum.svm import LaserEVM
-from mythril.laser.ethereum.state import Account
+from mythril.laser.ethereum.state.account import Account
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.transaction.concolic import execute_message_call
 from mythril.analysis.solver import get_model
@@ -18,8 +18,8 @@ test_types = [
     "vmBitwiseLogicOperation",
     "vmEnvironmentalInfo",
     "vmPushDupSwapTest",
-    "vmSha3Test",
     "vmTests",
+    "vmSha3Test",
 ]
 
 
@@ -35,21 +35,42 @@ def load_test_data(designations):
                     pre_condition = data["pre"]
 
                     action = data["exec"]
+                    gas_before = int(action["gas"], 16)
+                    gas_after = data.get("gas")
+                    gas_used = (
+                        gas_before - int(gas_after, 16)
+                        if gas_after is not None
+                        else None
+                    )
 
                     post_condition = data.get("post", {})
+                    environment = data.get("env")
 
                     return_data.append(
-                        (test_name, pre_condition, action, post_condition)
+                        (
+                            test_name,
+                            environment,
+                            pre_condition,
+                            action,
+                            gas_used,
+                            post_condition,
+                        )
                     )
 
     return return_data
 
 
 @pytest.mark.parametrize(
-    "test_name, pre_condition, action, post_condition", load_test_data(test_types)
+    "test_name, environment, pre_condition, action, gas_used, post_condition",
+    load_test_data(test_types),
 )
 def test_vmtest(
-    test_name: str, pre_condition: dict, action: dict, post_condition: dict
+    test_name: str,
+    environment: dict,
+    pre_condition: dict,
+    action: dict,
+    gas_used: int,
+    post_condition: dict,
 ) -> None:
     # Arrange
     if test_name == "gasprice":
@@ -68,46 +89,57 @@ def test_vmtest(
     # Act
     laser_evm.time = datetime.now()
 
-    # TODO: move this line below and check for VmExceptions when gas has been implemented
+    final_states = execute_message_call(
-    if post_condition == {}:
-        return
-
-    execute_message_call(
         laser_evm,
         callee_address=action["address"],
         caller_address=action["caller"],
         origin_address=binascii.a2b_hex(action["origin"][2:]),
         code=action["code"][2:],
-        gas=action["gas"],
+        gas_limit=int(action["gas"], 16),
         data=binascii.a2b_hex(action["data"][2:]),
         gas_price=int(action["gasPrice"], 16),
         value=int(action["value"], 16),
+        track_gas=True,
     )
 
     # Assert
-
+    if gas_used is not None and gas_used < int(environment["currentGasLimit"], 16):
-    assert len(laser_evm.open_states) == 1
+        # avoid gas usage larger than block gas limit
-
+        # this currently exceeds our estimations
-    world_state = laser_evm.open_states[0]
+        gas_min_max = [
-    model = get_model(next(iter(laser_evm.nodes.values())).states[0].mstate.constraints)
+            (s.mstate.min_gas_used, s.mstate.max_gas_used) for s in final_states
-
+        ]
-    for address, details in post_condition.items():
+        gas_ranges = [g[0] <= gas_used for g in gas_min_max]
-        account = world_state[address]
+        assert all(map(lambda g: g[0] <= g[1], gas_min_max))
-
+        assert any(gas_ranges)
-        assert account.nonce == int(details["nonce"], 16)
+
-        assert account.code.bytecode == details["code"][2:]
+    if any((v in test_name for v in ["error", "oog"])) and post_condition == {}:
-
+        # no more work to do if error happens or out of gas
-        for index, value in details["storage"].items():
+        assert len(laser_evm.open_states) == 0
-            expected = int(value, 16)
+    else:
-            actual = account.storage[int(index, 16)]
+        assert len(laser_evm.open_states) == 1
-            if isinstance(actual, ExprRef):
+        world_state = laser_evm.open_states[0]
-                actual = model.eval(actual)
+        model = get_model(
-                actual = (
+            next(iter(laser_evm.nodes.values())).states[0].mstate.constraints
-                    1 if actual == True else 0 if actual == False else actual
+        )
-                )  # Comparisons should be done with == than 'is' here as actual can be a BoolRef
+
-            else:
+        for address, details in post_condition.items():
-                if type(actual) == bytes:
+            account = world_state[address]
-                    actual = int(binascii.b2a_hex(actual), 16)
+
-                elif type(actual) == str:
+            assert account.nonce == int(details["nonce"], 16)
-                    actual = int(actual, 16)
+            assert account.code.bytecode == details["code"][2:]
-            assert actual == expected
+
+            for index, value in details["storage"].items():
+                expected = int(value, 16)
+                actual = account.storage[int(index, 16)]
+                if isinstance(actual, ExprRef):
+                    actual = model.eval(actual)
+                    actual = (
+                        1 if actual == True else 0 if actual == False else actual
+                    )  # Comparisons should be done with == than 'is' here as actual can be a BoolRef
+                else:
+                    if type(actual) == bytes:
+                        actual = int(binascii.b2a_hex(actual), 16)
+                    elif type(actual) == str:
+                        actual = int(actual, 16)
+                assert actual == expected

tests/laser/state/calldata_test.py

@@ -1,5 +1,5 @@
 import pytest
-from mythril.laser.ethereum.state import Calldata
+from mythril.laser.ethereum.state.calldata import Calldata
 from z3 import Solver, simplify
 from z3.z3types import Z3Exception
 from mock import MagicMock

tests/laser/state/mstack_test.py

@@ -1,6 +1,6 @@
 import pytest
 
-from mythril.laser.ethereum.state import MachineStack
+from mythril.laser.ethereum.state.machine_state import MachineStack
 from mythril.laser.ethereum.evm_exceptions import *
 from tests import BaseTestCase
 

tests/laser/state/mstate_test.py

@@ -1,5 +1,5 @@
 import pytest
-from mythril.laser.ethereum.state import MachineState
+from mythril.laser.ethereum.state.machine_state import MachineState
 from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
 
 memory_extension_test_data = [(0, 0, 10), (0, 30, 10), (100, 22, 8)]
@@ -10,7 +10,7 @@ memory_extension_test_data = [(0, 0, 10), (0, 30, 10), (100, 22, 8)]
 )
 def test_memory_extension(initial_size, start, extension_size):
     # Arrange
-    machine_state = MachineState(0)
+    machine_state = MachineState(gas_limit=8000000)
     machine_state.memory = [0] * initial_size
 
     # Act
@@ -27,7 +27,7 @@ stack_pop_too_many_test_data = [(0, 1), (0, 2), (5, 1), (5, 10)]
 @pytest.mark.parametrize("initial_size,overflow", stack_pop_too_many_test_data)
 def test_stack_pop_too_many(initial_size, overflow):
     # Arrange
-    machine_state = MachineState(0)
+    machine_state = MachineState(8000000)
     machine_state.stack = [42] * initial_size
 
     # Act + Assert
@@ -44,7 +44,7 @@ stack_pop_test_data = [
 @pytest.mark.parametrize("initial_stack,amount,expected", stack_pop_test_data)
 def test_stack_multiple_pop(initial_stack, amount, expected):
     # Arrange
-    machine_state = MachineState(0)
+    machine_state = MachineState(8000000)
     machine_state.stack = initial_stack[:]
 
     # Act
@@ -58,7 +58,7 @@ def test_stack_multiple_pop(initial_stack, amount, expected):
 
 def test_stack_multiple_pop_():
     # Arrange
-    machine_state = MachineState(0)
+    machine_state = MachineState(8000000)
     machine_state.stack = [1, 2, 3]
 
     # Act
@@ -71,7 +71,7 @@ def test_stack_multiple_pop_():
 
 def test_stack_single_pop():
     # Arrange
-    machine_state = MachineState(0)
+    machine_state = MachineState(8000000)
     machine_state.stack = [1, 2, 3]
 
     # Act
@@ -87,7 +87,7 @@ memory_write_test_data = [(5, 10, [1, 2, 3]), (0, 0, [3, 4]), (20, 1, [2, 4, 10]
 @pytest.mark.parametrize("initial_size, memory_offset, data", memory_write_test_data)
 def test_memory_write(initial_size, memory_offset, data):
     # Arrange
-    machine_state = MachineState(0)
+    machine_state = MachineState(8000000)
     machine_state.memory = [0] * initial_size
 
     # Act

tests/laser/state/storage_test.py

@@ -1,5 +1,5 @@
 import pytest
-from mythril.laser.ethereum.state import Storage
+from mythril.laser.ethereum.state.account import Storage
 from z3 import ExprRef
 
 storage_uninitialized_test_data = [({}, 1), ({1: 5}, 2), ({1: 5, 3: 10}, 2)]

tests/laser/test_transaction.py

@@ -1,6 +1,6 @@
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum import svm
-from mythril.laser.ethereum.state import Account
+from mythril.laser.ethereum.state.account import Account
 import mythril.laser.ethereum.cfg as cfg
 
 

tests/laser/transaction/symbolic_test.py

@@ -7,7 +7,8 @@ from mythril.laser.ethereum.transaction import (
     ContractCreationTransaction,
 )
 from mythril.laser.ethereum.svm import LaserEVM
-from mythril.laser.ethereum.state import WorldState, Account
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.world_state import WorldState
 import unittest.mock as mock
 from unittest.mock import MagicMock
 

tests/native_test.py

@@ -1,7 +1,9 @@
 import json
 from mythril.ether.soliditycontract import SolidityContract
 
-from mythril.laser.ethereum.state import GlobalState, MachineState, Account
+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 import svm
 from tests import *
 

tests/svm_test.py

@@ -4,7 +4,9 @@ from mythril.analysis.callgraph import generate_graph
 from mythril.ether.ethcontract import ETHContract
 from mythril.ether.soliditycontract import SolidityContract
 
-from mythril.laser.ethereum.state import GlobalState, MachineState, Account
+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 import svm
 from tests import *
 

tests/taint_result_test.py

@@ -1,5 +1,5 @@
 from mythril.laser.ethereum.taint_analysis import *
-from mythril.laser.ethereum.state import GlobalState
+from mythril.laser.ethereum.state.global_state import GlobalState
 
 
 def test_result_state():

tests/taint_runner_test.py

@@ -3,7 +3,10 @@ import pytest
 from pytest_mock import mocker
 from mythril.laser.ethereum.taint_analysis import *
 from mythril.laser.ethereum.cfg import Node, Edge
-from mythril.laser.ethereum.state import MachineState, Account, Environment, GlobalState
+from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.machine_state import MachineState
+from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.svm import LaserEVM
 
 
@@ -58,12 +61,12 @@ def test_execute_node(mocker):
 def test_execute(mocker):
     active_account = Account("0x00")
     environment = Environment(active_account, None, None, None, None, None)
-    state_1 = GlobalState(None, environment, None, MachineState(gas=10000000))
+    state_1 = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
     state_1.mstate.stack = [1, 2]
     mocker.patch.object(state_1, "get_current_instruction")
     state_1.get_current_instruction.return_value = {"opcode": "PUSH"}
 
-    state_2 = GlobalState(None, environment, None, MachineState(gas=10000000))
+    state_2 = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
     state_2.mstate.stack = [1, 2, 3]
     mocker.patch.object(state_2, "get_current_instruction")
     state_2.get_current_instruction.return_value = {"opcode": "ADD"}
@@ -71,7 +74,7 @@ def test_execute(mocker):
     node_1 = Node("Test contract")
     node_1.states = [state_1, state_2]
 
-    state_3 = GlobalState(None, environment, None, MachineState(gas=10000000))
+    state_3 = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
     state_3.mstate.stack = [1, 2]
     mocker.patch.object(state_3, "get_current_instruction")
     state_3.get_current_instruction.return_value = {"opcode": "ADD"}

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

@@ -1 +1,126 @@
-{"error": null, "issues": [{"address": 661, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.", "function": "_function_0x5a6814ec", "swc-id": "107", "title": "Message call to external contract", "type": "Informational"}, {"address": 666, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "_function_0x5a6814ec", "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}, {"address": 779, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This contract executes a message call to an address found at storage slot 1. This storage slot can be written to by calling the function `_function_0x2776b163`. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.", "function": "_function_0xd24b08cc", "swc-id": "107", "title": "Message call to external contract", "type": "Warning"}, {"address": 779, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "Possible transaction order dependence vulnerability: The value or direction of the call statement is determined from a tainted storage location", "function": "_function_0xd24b08cc", "swc-id": "114", "title": "Transaction order dependence", "type": "Warning"}, {"address": 784, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "_function_0xd24b08cc", "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}, {"address": 858, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.", "function": "_function_0xe11f493e", "swc-id": "107", "title": "Message call to external contract", "type": "Informational"}, {"address": 869, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The contract account state is changed after an external call. Consider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities.", "function": "_function_0xe11f493e", "swc-id": "107", "title": "State change after external call", "type": "Warning"}, {"address": 871, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "_function_0xe11f493e", "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}, {"address": 912, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.", "function": "_function_0xe1d10f79", "swc-id": "107", "title": "Message call to external contract", "type": "Warning"}, {"address": 918, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "_function_0xe1d10f79", "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 661,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.",
+      "function": "_function_0x5a6814ec",
+      "swc-id": "107",
+      "min_gas_used": 643,
+      "max_gas_used": 1254,
+      "title": "Message call to external contract",
+      "type": "Informational"
+    },
+    {
+      "address": 666,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "function": "_function_0x5a6814ec",
+      "swc-id": "104",
+      "min_gas_used": 1352,
+      "max_gas_used": 35963,
+      "title": "Unchecked CALL return value",
+      "type": "Informational"
+    },
+    {
+      "address": 779,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This contract executes a message call to an address found at storage slot 1. This storage slot can be written to by calling the function `_function_0x2776b163`. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.",
+      "function": "_function_0xd24b08cc",
+      "swc-id": "107",
+      "min_gas_used": 687,
+      "max_gas_used": 1298,
+      "title": "Message call to external contract",
+      "type": "Warning"
+    },
+    {
+      "address": 779,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "Possible transaction order dependence vulnerability: The value or direction of the call statement is determined from a tainted storage location",
+      "function": "_function_0xd24b08cc",
+      "swc-id": "114",
+      "min_gas_used": 687,
+      "max_gas_used": 1298,
+      "title": "Transaction order dependence",
+      "type": "Warning"
+    },
+    {
+      "address": 784,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "function": "_function_0xd24b08cc",
+      "swc-id": "104",
+      "min_gas_used": 1396,
+      "max_gas_used": 36007,
+      "title": "Unchecked CALL return value",
+      "type": "Informational"
+    },
+    {
+      "address": 858,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.",
+      "function": "_function_0xe11f493e",
+      "swc-id": "107",
+      "min_gas_used": 709,
+      "max_gas_used": 1320,
+      "title": "Message call to external contract",
+      "type": "Informational"
+    },
+    {
+      "address": 869,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The contract account state is changed after an external call. Consider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities.",
+      "function": "_function_0xe11f493e",
+      "swc-id": "107",
+      "min_gas_used": 709,
+      "max_gas_used": 1320,
+      "title": "State change after external call",
+      "type": "Warning"
+    },
+    {
+      "address": 871,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "function": "_function_0xe11f493e",
+      "swc-id": "104",
+      "min_gas_used": 6432,
+      "max_gas_used": 61043,
+      "title": "Unchecked CALL return value",
+      "type": "Informational"
+    },
+    {
+      "address": 912,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.",
+      "function": "_function_0xe1d10f79",
+      "swc-id": "107",
+      "min_gas_used": 335,
+      "max_gas_used": 616,
+      "title": "Message call to external contract",
+      "type": "Warning"
+    },
+    {
+      "address": 918,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "function": "_function_0xe1d10f79",
+      "swc-id": "104",
+      "min_gas_used": 1046,
+      "max_gas_used": 35327,
+      "title": "Unchecked CALL return value",
+      "type": "Informational"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `_function_0x5a6814ec`
 - PC address: 661
+- Estimated Gas Usage: 643 - 1254
 
 ### Description
 
@@ -17,6 +18,7 @@ This contract executes a message call to to another contract. Make sure that the
 - Contract: Unknown
 - Function name: `_function_0x5a6814ec`
 - PC address: 666
+- Estimated Gas Usage: 1352 - 35963
 
 ### Description
 
@@ -28,6 +30,7 @@ The return value of an external call is not checked. Note that execution continu
 - Contract: Unknown
 - Function name: `_function_0xd24b08cc`
 - PC address: 779
+- Estimated Gas Usage: 687 - 1298
 
 ### Description
 
@@ -39,6 +42,7 @@ This contract executes a message call to an address found at storage slot 1. Thi
 - Contract: Unknown
 - Function name: `_function_0xd24b08cc`
 - PC address: 779
+- Estimated Gas Usage: 687 - 1298
 
 ### Description
 
@@ -50,6 +54,7 @@ Possible transaction order dependence vulnerability: The value or direction of t
 - Contract: Unknown
 - Function name: `_function_0xd24b08cc`
 - PC address: 784
+- Estimated Gas Usage: 1396 - 36007
 
 ### Description
 
@@ -61,6 +66,7 @@ The return value of an external call is not checked. Note that execution continu
 - Contract: Unknown
 - Function name: `_function_0xe11f493e`
 - PC address: 858
+- Estimated Gas Usage: 709 - 1320
 
 ### Description
 
@@ -72,6 +78,7 @@ This contract executes a message call to to another contract. Make sure that the
 - Contract: Unknown
 - Function name: `_function_0xe11f493e`
 - PC address: 869
+- Estimated Gas Usage: 709 - 1320
 
 ### Description
 
@@ -83,6 +90,7 @@ The contract account state is changed after an external call. Consider that the
 - Contract: Unknown
 - Function name: `_function_0xe11f493e`
 - PC address: 871
+- Estimated Gas Usage: 6432 - 61043
 
 ### Description
 
@@ -94,6 +102,7 @@ The return value of an external call is not checked. Note that execution continu
 - Contract: Unknown
 - Function name: `_function_0xe1d10f79`
 - PC address: 912
+- Estimated Gas Usage: 335 - 616
 
 ### Description
 
@@ -105,6 +114,7 @@ This contract executes a message call to an address provided as a function argum
 - Contract: Unknown
 - Function name: `_function_0xe1d10f79`
 - PC address: 918
+- Estimated Gas Usage: 1046 - 35327
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0x5a6814ec
 PC address: 661
+Estimated Gas Usage: 643 - 1254
 This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
 --------------------
 
@@ -13,6 +14,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0x5a6814ec
 PC address: 666
+Estimated Gas Usage: 1352 - 35963
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 
@@ -22,6 +24,7 @@ Type: Warning
 Contract: Unknown
 Function name: _function_0xd24b08cc
 PC address: 779
+Estimated Gas Usage: 687 - 1298
 This contract executes a message call to an address found at storage slot 1. This storage slot can be written to by calling the function `_function_0x2776b163`. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
 --------------------
 
@@ -31,6 +34,7 @@ Type: Warning
 Contract: Unknown
 Function name: _function_0xd24b08cc
 PC address: 779
+Estimated Gas Usage: 687 - 1298
 Possible transaction order dependence vulnerability: The value or direction of the call statement is determined from a tainted storage location
 --------------------
 
@@ -40,6 +44,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0xd24b08cc
 PC address: 784
+Estimated Gas Usage: 1396 - 36007
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 
@@ -49,6 +54,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0xe11f493e
 PC address: 858
+Estimated Gas Usage: 709 - 1320
 This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
 --------------------
 
@@ -58,6 +64,7 @@ Type: Warning
 Contract: Unknown
 Function name: _function_0xe11f493e
 PC address: 869
+Estimated Gas Usage: 709 - 1320
 The contract account state is changed after an external call. Consider that the called contract could re-enter the function before this state change takes place. This can lead to business logic vulnerabilities.
 --------------------
 
@@ -67,6 +74,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0xe11f493e
 PC address: 871
+Estimated Gas Usage: 6432 - 61043
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 
@@ -76,6 +84,7 @@ Type: Warning
 Contract: Unknown
 Function name: _function_0xe1d10f79
 PC address: 912
+Estimated Gas Usage: 335 - 616
 This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
 --------------------
 
@@ -85,6 +94,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0xe1d10f79
 PC address: 918
+Estimated Gas Usage: 1046 - 35327
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 

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

@@ -1 +1,36 @@
-{"error": null, "issues": [{"address": 158, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "_function_0x83f12fec", "swc-id": "101", "title": "Integer Overflow", "type": "Warning"}, {"address": 278, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The arithmetic operation can result in integer overflow.\n", "function": "_function_0x83f12fec", "swc-id": "101", "title": "Integer Overflow", "type": "Warning"}, {"address": 378, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The substraction can result in an integer underflow.\n", "function": "_function_0x83f12fec", "swc-id": "101", "title": "Integer Underflow", "type": "Warning"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 158,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The arithmetic operation can result in integer overflow.\n",
+      "function": "_function_0x83f12fec",
+      "swc-id": "101",
+      "title": "Integer Overflow",
+      "type": "Warning"
+    },
+    {
+      "address": 278,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The arithmetic operation can result in integer overflow.\n",
+      "function": "_function_0x83f12fec",
+      "swc-id": "101",
+      "title": "Integer Overflow",
+      "type": "Warning"
+    },
+    {
+      "address": 378,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The substraction can result in an integer underflow.\n",
+      "function": "_function_0x83f12fec",
+      "swc-id": "101",
+      "title": "Integer Underflow",
+      "type": "Warning"
+    }
+  ],
+  "success": true
+}

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

@@ -1 +1,30 @@
-{"error": null, "issues": [{"address": 722, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.", "function": "withdrawfunds()", "swc-id": "105", "title": "Ether thief", "type": "Warning"}, {"address": 883, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This binary add operation can result in integer overflow.\n", "function": "invest()", "swc-id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 722,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.",
+      "function": "withdrawfunds()",
+      "swc-id": "105",
+      "min_gas_used": 1138,
+      "max_gas_used": 1749,
+      "title": "Ether thief",
+      "type": "Warning"
+    },
+    {
+      "address": 883,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This binary add operation can result in integer overflow.\n",
+      "function": "invest()",
+      "swc-id": "101",
+      "min_gas_used": 1571,
+      "max_gas_used": 1856,
+      "title": "Integer Overflow",
+      "type": "Warning"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `withdrawfunds()`
 - PC address: 722
+- Estimated Gas Usage: 1138 - 1749
 
 ### Description
 
@@ -17,6 +18,7 @@ Users other than the contract creator can withdraw ETH from the contract account
 - Contract: Unknown
 - Function name: `invest()`
 - PC address: 883
+- Estimated Gas Usage: 1571 - 1856
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Warning
 Contract: Unknown
 Function name: withdrawfunds()
 PC address: 722
+Estimated Gas Usage: 1138 - 1749
 Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.
 --------------------
 
@@ -13,6 +14,7 @@ Type: Warning
 Contract: Unknown
 Function name: invest()
 PC address: 883
+Estimated Gas Usage: 1571 - 1856
 This binary add operation can result in integer overflow.
 
 --------------------

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

@@ -1 +1,54 @@
-{"error": null, "issues": [{"address": 446, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A reachable exception (opcode 0xfe) has been detected. This 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": "_function_0x546455b5", "swc-id": "110", "title": "Exception state", "type": "Informational"}, {"address": 484, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A reachable exception (opcode 0xfe) has been detected. This 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": "_function_0x92dd38ea", "swc-id": "110", "title": "Exception state", "type": "Informational"}, {"address": 506, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A reachable exception (opcode 0xfe) has been detected. This 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": "_function_0xa08299f1", "swc-id": "110", "title": "Exception state", "type": "Informational"}, {"address": 531, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A reachable exception (opcode 0xfe) has been detected. This 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": "_function_0xb34c3610", "swc-id": "110", "title": "Exception state", "type": "Informational"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 446,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "A reachable exception (opcode 0xfe) has been detected. This 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": "_function_0x546455b5",
+      "swc-id": "110",
+      "min_gas_used": 206,
+      "max_gas_used": 301,
+      "title": "Exception state",
+      "type": "Informational"
+    },
+    {
+      "address": 484,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "A reachable exception (opcode 0xfe) has been detected. This 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": "_function_0x92dd38ea",
+      "swc-id": "110",
+      "min_gas_used": 256,
+      "max_gas_used": 351,
+      "title": "Exception state",
+      "type": "Informational"
+    },
+    {
+      "address": 506,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "A reachable exception (opcode 0xfe) has been detected. This 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": "_function_0xa08299f1",
+      "swc-id": "110",
+      "min_gas_used": 272,
+      "max_gas_used": 367,
+      "title": "Exception state",
+      "type": "Informational"
+    },
+    {
+      "address": 531,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "A reachable exception (opcode 0xfe) has been detected. This 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": "_function_0xb34c3610",
+      "swc-id": "110",
+      "min_gas_used": 268,
+      "max_gas_used": 363,
+      "title": "Exception state",
+      "type": "Informational"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `_function_0x546455b5`
 - PC address: 446
+- Estimated Gas Usage: 206 - 301
 
 ### Description
 
@@ -17,6 +18,7 @@ A reachable exception (opcode 0xfe) has been detected. This can be caused by typ
 - Contract: Unknown
 - Function name: `_function_0x92dd38ea`
 - PC address: 484
+- Estimated Gas Usage: 256 - 351
 
 ### Description
 
@@ -28,6 +30,7 @@ A reachable exception (opcode 0xfe) has been detected. This can be caused by typ
 - Contract: Unknown
 - Function name: `_function_0xa08299f1`
 - PC address: 506
+- Estimated Gas Usage: 272 - 367
 
 ### Description
 
@@ -39,6 +42,7 @@ A reachable exception (opcode 0xfe) has been detected. This can be caused by typ
 - Contract: Unknown
 - Function name: `_function_0xb34c3610`
 - PC address: 531
+- Estimated Gas Usage: 268 - 363
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0x546455b5
 PC address: 446
+Estimated Gas Usage: 206 - 301
 A reachable exception (opcode 0xfe) has been detected. This 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. 
 --------------------
 
@@ -13,6 +14,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0x92dd38ea
 PC address: 484
+Estimated Gas Usage: 256 - 351
 A reachable exception (opcode 0xfe) has been detected. This 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. 
 --------------------
 
@@ -22,6 +24,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0xa08299f1
 PC address: 506
+Estimated Gas Usage: 272 - 367
 A reachable exception (opcode 0xfe) has been detected. This 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. 
 --------------------
 
@@ -31,6 +34,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0xb34c3610
 PC address: 531
+Estimated Gas Usage: 268 - 363
 A reachable exception (opcode 0xfe) has been detected. This 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. 
 --------------------
 

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

@@ -1 +1,54 @@
-{"error": null, "issues": [{"address": 626, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "_function_0x141f32ff", "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}, {"address": 857, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "_function_0x9b58bc26", "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}, {"address": 1038, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.", "function": "_function_0xeea4c864", "swc-id": "107", "title": "Message call to external contract", "type": "Warning"}, {"address": 1046, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "_function_0xeea4c864", "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 626,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "function": "_function_0x141f32ff",
+      "swc-id": "104",
+      "min_gas_used": 1104,
+      "max_gas_used": 35856,
+      "title": "Unchecked CALL return value",
+      "type": "Informational"
+    },
+    {
+      "address": 857,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "function": "_function_0x9b58bc26",
+      "swc-id": "104",
+      "min_gas_used": 1167,
+      "max_gas_used": 35919,
+      "title": "Unchecked CALL return value",
+      "type": "Informational"
+    },
+    {
+      "address": 1038,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.",
+      "function": "_function_0xeea4c864",
+      "swc-id": "107",
+      "min_gas_used": 477,
+      "max_gas_used": 1229,
+      "title": "Message call to external contract",
+      "type": "Warning"
+    },
+    {
+      "address": 1046,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "function": "_function_0xeea4c864",
+      "swc-id": "104",
+      "min_gas_used": 1192,
+      "max_gas_used": 35944,
+      "title": "Unchecked CALL return value",
+      "type": "Informational"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `_function_0x141f32ff`
 - PC address: 626
+- Estimated Gas Usage: 1104 - 35856
 
 ### Description
 
@@ -17,6 +18,7 @@ The return value of an external call is not checked. Note that execution continu
 - Contract: Unknown
 - Function name: `_function_0x9b58bc26`
 - PC address: 857
+- Estimated Gas Usage: 1167 - 35919
 
 ### Description
 
@@ -28,6 +30,7 @@ The return value of an external call is not checked. Note that execution continu
 - Contract: Unknown
 - Function name: `_function_0xeea4c864`
 - PC address: 1038
+- Estimated Gas Usage: 477 - 1229
 
 ### Description
 
@@ -39,6 +42,7 @@ This contract executes a message call to an address provided as a function argum
 - Contract: Unknown
 - Function name: `_function_0xeea4c864`
 - PC address: 1046
+- Estimated Gas Usage: 1192 - 35944
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0x141f32ff
 PC address: 626
+Estimated Gas Usage: 1104 - 35856
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 
@@ -13,6 +14,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0x9b58bc26
 PC address: 857
+Estimated Gas Usage: 1167 - 35919
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 
@@ -22,6 +24,7 @@ Type: Warning
 Contract: Unknown
 Function name: _function_0xeea4c864
 PC address: 1038
+Estimated Gas Usage: 477 - 1229
 This contract executes a message call to an address provided as a function argument. Generally, it is not recommended to call user-supplied addresses using Solidity's call() construct. Note that attackers might leverage reentrancy attacks to exploit race conditions or manipulate this contract's state.
 --------------------
 
@@ -31,6 +34,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0xeea4c864
 PC address: 1046
+Estimated Gas Usage: 1192 - 35944
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 

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/multi_contracts.sol.o.json

@@ -1 +1,18 @@
-{"error": null, "issues": [{"address": 142, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.", "function": "_function_0x8a4068dd", "swc-id": "105", "title": "Ether thief", "type": "Warning"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 142,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.",
+      "function": "_function_0x8a4068dd",
+      "swc-id": "105",
+      "min_gas_used": 186,
+      "max_gas_used": 467,
+      "title": "Ether thief",
+      "type": "Warning"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `_function_0x8a4068dd`
 - PC address: 142
+- Estimated Gas Usage: 186 - 467
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Warning
 Contract: Unknown
 Function name: _function_0x8a4068dd
 PC address: 142
+Estimated Gas Usage: 186 - 467
 Users other than the contract creator can withdraw ETH from the contract account without previously having sent any ETH to it. This is likely to be vulnerability.
 --------------------
 

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/origin.sol.o.json

@@ -1 +1,18 @@
-{"error": null, "issues": [{"address": 317, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The function `transferOwnership(address)` retrieves the transaction origin (tx.origin) using the ORIGIN opcode. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin", "function": "transferOwnership(address)", "swc-id": "115", "title": "Use of tx.origin", "type": "Warning"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 317,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The function `transferOwnership(address)` retrieves the transaction origin (tx.origin) using the ORIGIN opcode. Use msg.sender instead.\nSee also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin",
+      "function": "transferOwnership(address)",
+      "swc-id": "115",
+      "min_gas_used": 626,
+      "max_gas_used": 1051,
+      "title": "Use of tx.origin",
+      "type": "Warning"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `transferOwnership(address)`
 - PC address: 317
+- Estimated Gas Usage: 626 - 1051
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Warning
 Contract: Unknown
 Function name: transferOwnership(address)
 PC address: 317
+Estimated Gas Usage: 626 - 1051
 The function `transferOwnership(address)` retrieves the transaction origin (tx.origin) using the ORIGIN opcode. Use msg.sender instead.
 See also: https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin
 --------------------

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

@@ -1 +1,42 @@
-{"error":null,"issues":[{"address":567,"contract":"Unknown","debug":"<DEBUG-DATA>","description":"The subtraction can result in an integer underflow.\n","function":"sendeth(address,uint256)","swc-id":"101","title":"Integer Underflow","type":"Warning"},{"address":649,"contract":"Unknown","debug":"<DEBUG-DATA>","description":"The subtraction can result in an integer underflow.\n","function":"sendeth(address,uint256)","swc-id":"101","title":"Integer Underflow","type":"Warning"},{"address":725,"contract":"Unknown","debug":"<DEBUG-DATA>","description":"This binary add operation can result in integer overflow.\n","function":"sendeth(address,uint256)","swc-id":"101","title":"Integer Overflow","type":"Warning"}],"success":true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 567,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The subtraction can result in an integer underflow.\n",
+      "function": "sendeth(address,uint256)",
+      "swc-id": "101",
+      "min_gas_used": 750,
+      "max_gas_used": 1035,
+      "title": "Integer Underflow",
+      "type": "Warning"
+    },
+    {
+      "address": 649,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The subtraction can result in an integer underflow.\n",
+      "function": "sendeth(address,uint256)",
+      "swc-id": "101",
+      "min_gas_used": 1283,
+      "max_gas_used": 1758,
+      "title": "Integer Underflow",
+      "type": "Warning"
+    },
+    {
+      "address": 725,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This binary add operation can result in integer overflow.\n",
+      "function": "sendeth(address,uint256)",
+      "swc-id": "101",
+      "min_gas_used": 6806,
+      "max_gas_used": 27471,
+      "title": "Integer Overflow",
+      "type": "Warning"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 567
+- Estimated Gas Usage: 750 - 1035
 
 ### Description
 
@@ -17,6 +18,7 @@ The subtraction can result in an integer underflow.
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 649
+- Estimated Gas Usage: 1283 - 1758
 
 ### Description
 
@@ -28,6 +30,7 @@ The subtraction can result in an integer underflow.
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 725
+- Estimated Gas Usage: 6806 - 27471
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 567
+Estimated Gas Usage: 750 - 1035
 The subtraction can result in an integer underflow.
 
 --------------------
@@ -14,6 +15,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 649
+Estimated Gas Usage: 1283 - 1758
 The subtraction can result in an integer underflow.
 
 --------------------
@@ -24,6 +26,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 725
+Estimated Gas Usage: 6806 - 27471
 This binary add operation can result in integer overflow.
 
 --------------------

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

@@ -1 +1,42 @@
-{"error": null, "issues": [{"address": 196, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.", "function": "_function_0x633ab5e0", "swc-id": "107", "title": "Message call to external contract", "type": "Informational"}, {"address": 285, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.", "function": "_function_0xe3bea282", "swc-id": "107", "title": "Message call to external contract", "type": "Informational"}, {"address": 290, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.", "function": "_function_0xe3bea282", "swc-id": "104", "title": "Unchecked CALL return value", "type": "Informational"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 196,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.",
+      "function": "_function_0x633ab5e0",
+      "swc-id": "107",
+      "min_gas_used": 599,
+      "max_gas_used": 1210,
+      "title": "Message call to external contract",
+      "type": "Informational"
+    },
+    {
+      "address": 285,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.",
+      "function": "_function_0xe3bea282",
+      "swc-id": "107",
+      "min_gas_used": 621,
+      "max_gas_used": 1232,
+      "title": "Message call to external contract",
+      "type": "Informational"
+    },
+    {
+      "address": 290,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "function": "_function_0xe3bea282",
+      "swc-id": "104",
+      "min_gas_used": 1330,
+      "max_gas_used": 35941,
+      "title": "Unchecked CALL return value",
+      "type": "Informational"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `_function_0x633ab5e0`
 - PC address: 196
+- Estimated Gas Usage: 599 - 1210
 
 ### Description
 
@@ -17,6 +18,7 @@ This contract executes a message call to to another contract. Make sure that the
 - Contract: Unknown
 - Function name: `_function_0xe3bea282`
 - PC address: 285
+- Estimated Gas Usage: 621 - 1232
 
 ### Description
 
@@ -28,6 +30,7 @@ This contract executes a message call to to another contract. Make sure that the
 - Contract: Unknown
 - Function name: `_function_0xe3bea282`
 - PC address: 290
+- Estimated Gas Usage: 1330 - 35941
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0x633ab5e0
 PC address: 196
+Estimated Gas Usage: 599 - 1210
 This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
 --------------------
 
@@ -13,6 +14,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0xe3bea282
 PC address: 285
+Estimated Gas Usage: 621 - 1232
 This contract executes a message call to to another contract. Make sure that the called contract is trusted and does not execute user-supplied code.
 --------------------
 
@@ -22,6 +24,7 @@ Type: Informational
 Contract: Unknown
 Function name: _function_0xe3bea282
 PC address: 290
+Estimated Gas Usage: 1330 - 35941
 The return value of an external call is not checked. Note that execution continue even if the called contract throws.
 --------------------
 

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

@@ -1,166 +1,166 @@
 {
-    "success": true,
+  "success": true,
-    "error": null,
+  "error": null,
-    "issues": [
+  "issues": [
-        {
+    {
-            "title": "Ether send",
+      "title": "Ether send",
-            "description": "In the function `_function_0x4229616d` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+      "description": "In the function `_function_0x4229616d` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
-            "function": "_function_0x4229616d",
+      "function": "_function_0x4229616d",
-            "type": "Warning",
+      "type": "Warning",
-            "address": 1599,
+      "address": 1599,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Ether send",
+      "title": "Ether send",
-            "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+      "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
-            "function": "_function_0xb4022950",
+      "function": "_function_0xb4022950",
-            "type": "Warning",
+      "type": "Warning",
-            "address": 1940,
+      "address": 1940,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Ether send",
+      "title": "Ether send",
-            "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+      "description": "In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\n\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
-            "function": "_function_0xb4022950",
+      "function": "_function_0xb4022950",
-            "type": "Warning",
+      "type": "Warning",
-            "address": 2582,
+      "address": 2582,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Exception state",
+      "title": "Exception state",
-            "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
+      "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
-            "function": "_function_0x57d4021b",
+      "function": "_function_0x57d4021b",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 1653,
+      "address": 1653,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Exception state",
+      "title": "Exception state",
-            "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
+      "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
-            "function": "_function_0x9dbc4f9b",
+      "function": "_function_0x9dbc4f9b",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 2085,
+      "address": 2085,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "fallback",
+      "function": "fallback",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 3111,
+      "address": 3111,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "fallback",
+      "function": "fallback",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 3140,
+      "address": 3140,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "fallback",
+      "function": "fallback",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 2950,
+      "address": 2950,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "fallback",
+      "function": "fallback",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 1268,
+      "address": 1268,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x09dfdc71",
+      "function": "_function_0x09dfdc71",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 310,
+      "address": 310,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x09dfdc71",
+      "function": "_function_0x09dfdc71",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 1316,
+      "address": 1316,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x253459e3",
+      "function": "_function_0x253459e3",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 1375,
+      "address": 1375,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x4229616d",
+      "function": "_function_0x4229616d",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 1511,
+      "address": 1511,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x57d4021b",
+      "function": "_function_0x57d4021b",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 1679,
+      "address": 1679,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x6fbaaa1e",
+      "function": "_function_0x6fbaaa1e",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 618,
+      "address": 618,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x8a5fb3ca",
+      "function": "_function_0x8a5fb3ca",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 805,
+      "address": 805,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Invariant branch condition",
+      "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
+      "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x9dbc4f9b",
+      "function": "_function_0x9dbc4f9b",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 2187,
+      "address": 2187,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Unchecked CALL return value",
+      "title": "Unchecked CALL return value",
-            "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-            "function": "_function_0x4229616d",
+      "function": "_function_0x4229616d",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 1599,
+      "address": 1599,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Unchecked CALL return value",
+      "title": "Unchecked CALL return value",
-            "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-            "function": "_function_0xb4022950",
+      "function": "_function_0xb4022950",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 1940,
+      "address": 1940,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Unchecked CALL return value",
+      "title": "Unchecked CALL return value",
-            "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
+      "description": "The return value of an external call is not checked. Note that execution continue even if the called contract throws.",
-            "function": "_function_0xb4022950",
+      "function": "_function_0xb4022950",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 2582,
+      "address": 2582,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        }
+    }
-    ]
+  ]
 }

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

@@ -1 +1,18 @@
-{"error": null, "issues": [{"address": 146, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "A reachable SUICIDE instruction was detected. The remaining Ether is sent to an address provided as a function argument.\n", "function": "_function_0xcbf0b0c0", "swc-id": "106", "title": "Unchecked SUICIDE", "type": "Warning"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 146,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "A reachable SUICIDE instruction was detected. The remaining Ether is sent to an address provided as a function argument.\n",
+      "function": "_function_0xcbf0b0c0",
+      "swc-id": "106",
+      "min_gas_used": 168,
+      "max_gas_used": 263,
+      "title": "Unchecked SUICIDE",
+      "type": "Warning"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `_function_0xcbf0b0c0`
 - PC address: 146
+- Estimated Gas Usage: 168 - 263
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Warning
 Contract: Unknown
 Function name: _function_0xcbf0b0c0
 PC address: 146
+Estimated Gas Usage: 168 - 263
 A reachable SUICIDE instruction was detected. The remaining Ether is sent to an address provided as a function argument.
 
 --------------------

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

@@ -1 +1,42 @@
-{"error": null, "issues": [{"address": 567, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc-id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 649, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "The subtraction can result in an integer underflow.\n", "function": "sendeth(address,uint256)", "swc-id": "101", "title": "Integer Underflow", "type": "Warning"}, {"address": 725, "contract": "Unknown", "debug": "<DEBUG-DATA>", "description": "This binary add operation can result in integer overflow.\n", "function": "sendeth(address,uint256)", "swc-id": "101", "title": "Integer Overflow", "type": "Warning"}], "success": true}
+{
+  "error": null,
+  "issues": [
+    {
+      "address": 567,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The subtraction can result in an integer underflow.\n",
+      "function": "sendeth(address,uint256)",
+      "swc-id": "101",
+      "min_gas_used": 750,
+      "max_gas_used": 1035,
+      "title": "Integer Underflow",
+      "type": "Warning"
+    },
+    {
+      "address": 649,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "The subtraction can result in an integer underflow.\n",
+      "function": "sendeth(address,uint256)",
+      "swc-id": "101",
+      "min_gas_used": 1283,
+      "max_gas_used": 1758,
+      "title": "Integer Underflow",
+      "type": "Warning"
+    },
+    {
+      "address": 725,
+      "contract": "Unknown",
+      "debug": "<DEBUG-DATA>",
+      "description": "This binary add operation can result in integer overflow.\n",
+      "function": "sendeth(address,uint256)",
+      "swc-id": "101",
+      "min_gas_used": 6806,
+      "max_gas_used": 27471,
+      "title": "Integer Overflow",
+      "type": "Warning"
+    }
+  ],
+  "success": true
+}

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

@@ -6,6 +6,7 @@
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 567
+- Estimated Gas Usage: 750 - 1035
 
 ### Description
 
@@ -17,6 +18,7 @@ The subtraction can result in an integer underflow.
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 649
+- Estimated Gas Usage: 1283 - 1758
 
 ### Description
 
@@ -28,6 +30,7 @@ The subtraction can result in an integer underflow.
 - Contract: Unknown
 - Function name: `sendeth(address,uint256)`
 - PC address: 725
+- Estimated Gas Usage: 6806 - 27471
 
 ### Description
 

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

@@ -4,6 +4,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 567
+Estimated Gas Usage: 750 - 1035
 The subtraction can result in an integer underflow.
 
 --------------------
@@ -14,6 +15,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 649
+Estimated Gas Usage: 1283 - 1758
 The subtraction can result in an integer underflow.
 
 --------------------
@@ -24,6 +26,7 @@ Type: Warning
 Contract: Unknown
 Function name: sendeth(address,uint256)
 PC address: 725
+Estimated Gas Usage: 6806 - 27471
 This binary add operation can result in integer overflow.
 
 --------------------

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

@@ -1,46 +1,46 @@
 {
-    "success": true,
+  "success": true,
-    "error": null,
+  "error": null,
-    "issues": [
+  "issues": [
-        {
+    {
-            "title": "Dependence on predictable environment variable",
+      "title": "Dependence on predictable environment variable",
-            "description": "In the function `_function_0xe9874106` the following predictable state variables are used to determine Ether recipient:\n- block.coinbase\n",
+      "description": "In the function `_function_0xe9874106` the following predictable state variables are used to determine Ether recipient:\n- block.coinbase\n",
-            "function": "_function_0xe9874106",
+      "function": "_function_0xe9874106",
-            "type": "Warning",
+      "type": "Warning",
-            "address": 1285,
+      "address": 1285,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Ether send",
+      "title": "Ether send",
-            "description": "In the function `_function_0xe9874106` a non-zero amount of Ether is sent to an address taken from storage slot 0.\nThere is a check on storage index 0. This storage slot can be written to by calling the function `fallback`.\n\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
+      "description": "In the function `_function_0xe9874106` a non-zero amount of Ether is sent to an address taken from storage slot 0.\nThere is a check on storage index 0. This storage slot can be written to by calling the function `fallback`.\n\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.\nThere is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.",
-            "function": "_function_0xe9874106",
+      "function": "_function_0xe9874106",
-            "type": "Warning",
+      "type": "Warning",
-            "address": 1285,
+      "address": 1285,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Exception state",
+      "title": "Exception state",
-            "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
+      "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
-            "function": "fallback",
+      "function": "fallback",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 356,
+      "address": 356,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Exception state",
+      "title": "Exception state",
-            "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
+      "description": "A reachable exception (opcode 0xfe) has been detected. This can be caused by type errors, division by zero, out-of-bounds array access, or assert violations. This is acceptable in most situations. Note however that `assert()` should only be used to check invariants. Use `require()` for regular input checking. ",
-            "function": "_function_0xe9874106",
+      "function": "_function_0xe9874106",
-            "type": "Informational",
+      "type": "Informational",
-            "address": 146,
+      "address": 146,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        },
+    },
-        {
+    {
-            "title": "Transaction order dependence",
+      "title": "Transaction order dependence",
-            "description": "A possible transaction order independence vulnerability exists in function _function_0xe9874106. The value or direction of the call statement is determined from a tainted storage location",
+      "description": "A possible transaction order independence vulnerability exists in function _function_0xe9874106. The value or direction of the call statement is determined from a tainted storage location",
-            "function": "_function_0xe9874106",
+      "function": "_function_0xe9874106",
-            "type": "Warning",
+      "type": "Warning",
-            "address": 1285,
+      "address": 1285,
-            "debug": "<DEBUG-DATA>"
+      "debug": "<DEBUG-DATA>"
-        }
+    }
-    ]
+  ]
 }