Balance modelling and symbolic sender variables (#1025)

* add actor address to symbolic

This will allow us to simulate semi-symbolic transaction senders

* add value transfer to transaction global state creation

* add proper balance tracking to world state and account

* use address value vs string

* disable actor address variable

* use address directly

* allow balance functions with int types

* use value as getters since bitvecs aren't hashable

* implement correct value transfer for suicide

* use actor from actor pool

* allow use of Or with *arg pattern

* use bitvec instead of strings

* add dynamic balance implementation to state datamodels

* cleanup svm interface

* use balance lambda in suicide op implementation

* use bitvec instead of string address

* update world state and account creation in symbolic

* update tests to include overflow results

* apply style rules

* ignore previous open states for now

* update native test to conform to new laser interface

* fix incorrect types in the symbolic virtual machine

* allow multiple types as input for address in account

* fix type hint in symbolic.py

* get int out of string in call

* fix type in call op implementation

* adapt test_transaction to conform to new laser interface

* use static address to keep contracts from trying to enter themselves
and make address type more dynamic

* update evm test to conform to new laser interface

* implement suicide to uncreated account

* apply style rules

* dynamically create colormap

This removes the need for a globally maintained accountlist

* get value out of address

* add accounts getter

* change symbolic test call to be valid with respect to the world
state and account apis

* remove dependency on globally recorded accounts

* fix typing issues

* fix type annotations in symbolic.py

* fix remaining mypy warnings

* simplify assertion check

* execute lambda to get balance

* make variable name plural

* add documentation to svm constructor

* use list comprehension to make code cleaner

* remove comment

* change variable name to plural

* remove commented code

* change variable name to conform to changed interface

mythril/analysis/callgraph.py

@@ -125,7 +125,7 @@ phrack_color = {
 }
 
 
-def extract_nodes(statespace, color_map):
+def extract_nodes(statespace):
     """
 
     :param statespace:
@@ -133,6 +133,7 @@ def extract_nodes(statespace, color_map):
     :return:
     """
     nodes = []
+    color_map = {}
     for node_key in statespace.nodes:
         node = statespace.nodes[node_key]
         instructions = [state.get_current_instruction() for state in node.states]
@@ -164,10 +165,16 @@ def extract_nodes(statespace, color_map):
             else "\n".join(code_split[:6]) + "\n(click to expand +)"
         )
 
+        if node.get_cfg_dict()["contract_name"] not in color_map.keys():
+            color = default_colors[len(color_map) % len(default_colors)]
+            color_map[node.get_cfg_dict()["contract_name"]] = color
+
         nodes.append(
             {
                 "id": str(node_key),
-                "color": color_map[node.get_cfg_dict()["contract_name"]],
+                "color": color_map.get(
+                    node.get_cfg_dict()["contract_name"], default_colors[0]
+                ),
                 "size": 150,
                 "fullLabel": "\n".join(code_split),
                 "label": truncated_code,
@@ -231,22 +238,12 @@ def generate_graph(
     template = env.get_template("callgraph.html")
 
     graph_opts = default_opts
-    accounts = statespace.accounts
-
-    if phrackify:
-        color_map = {accounts[k].contract_name: phrack_color for k in accounts}
-        graph_opts.update(phrack_opts)
-    else:
-        color_map = {
-            accounts[k].contract_name: default_colors[i % len(default_colors)]
-            for i, k in enumerate(accounts)
-        }
 
     graph_opts["physics"]["enabled"] = physics
 
     return template.render(
         title=title,
-        nodes=extract_nodes(statespace, color_map),
+        nodes=extract_nodes(statespace),
         edges=extract_edges(statespace),
         phrackify=phrackify,
         opts=graph_opts,

mythril/analysis/symbolic.py

@@ -2,22 +2,22 @@
 purposes."""
 
 import copy
-from ethereum.utils import mk_contract_address
+
 from mythril.analysis.security import get_detection_module_hooks, get_detection_modules
 from mythril.laser.ethereum import svm
+from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory
+from mythril.laser.ethereum.plugins.plugin_loader import LaserPluginLoader
 from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.strategy.basic import (
     BreadthFirstSearchStrategy,
     DepthFirstSearchStrategy,
     ReturnRandomNaivelyStrategy,
     ReturnWeightedRandomStrategy,
+    BasicSearchStrategy,
 )
-from mythril.laser.ethereum.transaction.symbolic import CREATOR_ADDRESS
+from mythril.laser.smt import symbol_factory, BitVec
-
+from typing import Union, List, Dict, Type
-
-from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory
-from mythril.laser.ethereum.plugins.plugin_loader import LaserPluginLoader
-
 from mythril.solidity.soliditycontract import EVMContract, SolidityContract
 from .ops import Call, SStore, VarType, get_variable
 
@@ -32,7 +32,7 @@ class SymExecWrapper:
     def __init__(
         self,
         contract,
-        address,
+        address: Union[int, str, BitVec],
         strategy,
         dynloader=None,
         max_depth=22,
@@ -55,8 +55,13 @@ class SymExecWrapper:
         :param transaction_count:
         :param modules:
         """
+        if isinstance(address, str):
+            address = symbol_factory.BitVecVal(int(address, 16), 256)
+        if isinstance(address, int):
+            address = symbol_factory.BitVecVal(address, 256)
+
         if strategy == "dfs":
-            s_strategy = DepthFirstSearchStrategy
+            s_strategy = DepthFirstSearchStrategy  # type: Type[BasicSearchStrategy]
         elif strategy == "bfs":
             s_strategy = BreadthFirstSearchStrategy
         elif strategy == "naive-random":
@@ -66,19 +71,11 @@ class SymExecWrapper:
         else:
             raise ValueError("Invalid strategy argument supplied")
 
-        account = Account(
-            address,
-            contract.disassembly,
-            dynamic_loader=dynloader,
-            contract_name=contract.name,
-        )
         requires_statespace = (
             compulsory_statespace or len(get_detection_modules("post", modules)) > 0
         )
-        self.accounts = {address: account}
 
         self.laser = svm.LaserEVM(
-            self.accounts,
             dynamic_loader=dynloader,
             max_depth=max_depth,
             execution_timeout=execution_timeout,
@@ -111,12 +108,16 @@ class SymExecWrapper:
                 creation_code=contract.creation_code, contract_name=contract.name
             )
         else:
-            self.laser.sym_exec(address)
+            account = Account(
-        created_address = "0x" + str(mk_contract_address(CREATOR_ADDRESS, 0).hex())
+                address,
-        for key, value in self.laser.world_state.accounts.items():
+                contract.disassembly,
-            if created_address == value.address:
+                dynamic_loader=dynloader,
-                contract.code = value.code.bytecode
+                contract_name=contract.name,
-                break
+                concrete_storage=False,
+            )
+            world_state = WorldState()
+            world_state.put_account(account)
+            self.laser.sym_exec(world_state=world_state, target_address=address.value)
 
         if not requires_statespace:
             return
@@ -126,8 +127,8 @@ class SymExecWrapper:
 
         # Generate lists of interesting operations
 
-        self.calls = []
+        self.calls = []  # type: List[Call]
-        self.sstors = {}
+        self.sstors = {}  # type: Dict[int, Dict[str, List[SStore]]]
 
         for key in self.nodes:
 
@@ -204,7 +205,7 @@ class SymExecWrapper:
 
                 elif op == "SSTORE":
                     stack = copy.copy(state.mstate.stack)
-                    address = state.environment.active_account.address
+                    address = state.environment.active_account.address.value
 
                     index, value = stack.pop(), stack.pop()
 

mythril/laser/ethereum/call.py

@@ -3,13 +3,12 @@ instructions.py to get the necessary elements from the stack and determine the
 parameters for the new global state."""
 
 import logging
+import re
 from typing import Union, List, cast, Callable
-from z3 import Z3Exception
+
-from mythril.laser.smt import BitVec
+import mythril.laser.ethereum.util as util
 from mythril.laser.ethereum import natives
 from mythril.laser.ethereum.gas import OPCODE_GAS
-from mythril.laser.smt import simplify, Expression, symbol_factory
-import mythril.laser.ethereum.util as util
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.calldata import (
     BaseCalldata,
@@ -17,8 +16,9 @@ from mythril.laser.ethereum.state.calldata import (
     ConcreteCalldata,
 )
 from mythril.laser.ethereum.state.global_state import GlobalState
+from mythril.laser.smt import BitVec
+from mythril.laser.smt import simplify, Expression, symbol_factory
 from mythril.support.loader import DynLoader
-import re
 
 """
 This module contains the business logic used by Instruction in instructions.py
@@ -96,7 +96,7 @@ def get_callee_address(
         # attempt to read the contract address from instance storage
         try:
             callee_address = dynamic_loader.read_storage(
-                environment.active_account.address, index
+                str(hex(environment.active_account.address.value)), index
             )
         # TODO: verify whether this happens or not
         except:
@@ -124,7 +124,7 @@ def get_callee_account(
     accounts = global_state.accounts
 
     try:
-        return global_state.accounts[callee_address]
+        return global_state.accounts[int(callee_address, 16)]
     except KeyError:
         # We have a valid call address, but contract is not in the modules list
         log.debug("Module with address " + callee_address + " not loaded.")
@@ -145,7 +145,11 @@ def get_callee_account(
     log.debug("Dependency loaded: " + callee_address)
 
     callee_account = Account(
-        callee_address, code, callee_address, dynamic_loader=dynamic_loader
+        symbol_factory.BitVecVal(int(callee_address, 16), 256),
+        code,
+        callee_address,
+        dynamic_loader=dynamic_loader,
+        balances=global_state.world_state.balances,
     )
     accounts[callee_address] = callee_account
 

mythril/laser/ethereum/instructions.py

@@ -1520,7 +1520,7 @@ class Instruction:
                 global_state.environment.active_account
             )
             global_state.accounts[
-                global_state.environment.active_account.address
+                global_state.environment.active_account.address.value
             ] = global_state.environment.active_account
 
             global_state.environment.active_account.storage[index] = (
@@ -1756,31 +1756,19 @@ class Instruction:
         :param global_state:
         """
         target = global_state.mstate.stack.pop()
-        account_created = False
+        transfer_amount = global_state.environment.active_account.balance()
         # Often the target of the suicide instruction will be symbolic
-        # If it isn't then well transfer the balance to the indicated contract
+        # If it isn't then we'll transfer the balance to the indicated contract
-        if isinstance(target, BitVec) and not target.symbolic:
+        global_state.world_state[target].add_balance(transfer_amount)
-            target = "0x" + hex(target.value)[-40:]
-        if isinstance(target, str):
-            try:
-                global_state.world_state[
-                    target
-                ].balance += global_state.environment.active_account.balance
-            except KeyError:
-                global_state.world_state.create_account(
-                    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.address.value
         ] = global_state.environment.active_account
 
-        global_state.environment.active_account.balance = 0
+        global_state.environment.active_account.set_balance(0)
         global_state.environment.active_account.deleted = True
         global_state.current_transaction.end(global_state)
 
@@ -1865,9 +1853,7 @@ class Instruction:
             gas_price=environment.gasprice,
             gas_limit=gas,
             origin=environment.origin,
-            caller=symbol_factory.BitVecVal(
+            caller=environment.active_account.address,
-                int(environment.active_account.address, 16), 256
-            ),
             callee_account=callee_account,
             call_data=call_data,
             call_value=value,

mythril/laser/ethereum/state/account.py

@@ -7,6 +7,7 @@ from typing import Any, Dict, KeysView, Union
 
 from z3 import ExprRef
 
+from mythril.laser.smt import Array, symbol_factory, BitVec
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.smt import symbol_factory
 
@@ -30,7 +31,7 @@ class Storage:
         except KeyError:
             if (
                 self.address
-                and int(self.address[2:], 16) != 0
+                and self.address.value != 0
                 and (self.dynld and self.dynld.storage_loading)
             ):
                 try:
@@ -74,10 +75,10 @@ class Account:
 
     def __init__(
         self,
-        address: str,
+        address: Union[BitVec, str],
         code=None,
         contract_name="unknown",
-        balance=None,
+        balances: Array = None,
         concrete_storage=False,
         dynamic_loader=None,
     ) -> None:
@@ -91,36 +92,51 @@ class Account:
         """
         self.nonce = 0
         self.code = code or Disassembly("")
-        self.balance = (
+        self.address = (
-            balance
+            address
-            if balance
+            if isinstance(address, BitVec)
-            else symbol_factory.BitVecSym("{}_balance".format(address), 256)
+            else symbol_factory.BitVecVal(int(address, 16), 256)
         )
+
         self.storage = Storage(
-            concrete_storage, address=address, dynamic_loader=dynamic_loader
+            concrete_storage, address=self.address, dynamic_loader=dynamic_loader
         )
+
         # Metadata
-        self.address = address
         self.contract_name = contract_name
 
         self.deleted = False
 
+        self._balances = balances
+        self.balance = lambda: self._balances[self.address]
+
     def __str__(self) -> str:
         return str(self.as_dict)
 
-    def set_balance(self, balance: ExprRef) -> None:
+    def set_balance(self, balance: Union[int, BitVec]) -> None:
         """
 
         :param balance:
         """
-        self.balance = balance
+        balance = (
+            symbol_factory.BitVecVal(balance, 256)
+            if isinstance(balance, int)
+            else balance
+        )
+        assert self._balances is not None
+        self._balances[self.address] = balance
 
-    def add_balance(self, balance: ExprRef) -> None:
+    def add_balance(self, balance: Union[int, BitVec]) -> None:
         """
 
         :param balance:
         """
-        self.balance += balance
+        balance = (
+            symbol_factory.BitVecVal(balance, 256)
+            if isinstance(balance, int)
+            else balance
+        )
+        self._balances[self.address] += balance
 
     @property
     def as_dict(self) -> Dict:
@@ -131,7 +147,7 @@ class Account:
         return {
             "nonce": self.nonce,
             "code": self.code,
-            "balance": self.balance,
+            "balance": self.balance(),
             "storage": self.storage,
         }
 
@@ -139,8 +155,8 @@ class Account:
         new_account = Account(
             address=self.address,
             code=self.code,
-            balance=self.balance,
             contract_name=self.contract_name,
+            balances=self._balances,
         )
         new_account.storage = deepcopy(self.storage)
         new_account.code = self.code

mythril/laser/ethereum/state/environment.py

@@ -39,7 +39,7 @@ class Environment:
         self.active_account = active_account
         self.active_function_name = ""
 
-        self.address = symbol_factory.BitVecVal(int(active_account.address, 16), 256)
+        self.address = active_account.address
 
         # Ib
         self.code = active_account.code if code is None else code

mythril/laser/ethereum/state/global_state.py

@@ -77,7 +77,7 @@ class GlobalState:
 
         :return:
         """
-        return self.world_state.accounts
+        return self.world_state._accounts
 
     # TODO: remove this, as two instructions are confusing
     def get_current_instruction(self) -> Dict:

mythril/laser/ethereum/state/world_state.py

@@ -2,6 +2,8 @@
 from copy import copy
 from random import randint
 from typing import Dict, List, Iterator, Optional, TYPE_CHECKING
+
+from mythril.laser.smt import symbol_factory, Array, BitVec
 from ethereum.utils import mk_contract_address
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.annotation import StateAnnotation
@@ -22,18 +24,29 @@ class WorldState:
         :param transaction_sequence:
         :param annotations:
         """
-        self.accounts = {}  # type: Dict[str, Account]
+        self._accounts = {}  # type: Dict[int, Account]
+        self.balances = Array("balance", 256, 256)
+
         self.node = None  # type: Optional['Node']
         self.transaction_sequence = transaction_sequence or []
         self._annotations = annotations or []
 
-    def __getitem__(self, item: str) -> Account:
+    @property
+    def accounts(self):
+        return self._accounts
+
+    def __getitem__(self, item: BitVec) -> 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]
+        try:
+            return self._accounts[item.value]
+        except KeyError:
+            new_account = Account(address=item, code=None, balances=self.balances)
+            self._accounts[item.value] = new_account
+            return new_account
 
     def __copy__(self) -> "WorldState":
         """
@@ -45,7 +58,9 @@ class WorldState:
             transaction_sequence=self.transaction_sequence[:],
             annotations=new_annotations,
         )
-        new_world_state.accounts = copy(self.accounts)
+        new_world_state.balances = copy(self.balances)
+        for account in self._accounts.values():
+            new_world_state.put_account(copy(account))
         new_world_state.node = self.node
         return new_world_state
 
@@ -65,14 +80,22 @@ class WorldState:
         :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(creator)
+        address = (
+            symbol_factory.BitVecVal(address, 256)
+            if address
+            else self._generate_new_address(creator)
+        )
+
         new_account = Account(
-            address,
+            address=address,
-            balance=balance,
+            balances=self.balances,
             dynamic_loader=dynamic_loader,
             concrete_storage=concrete_storage,
         )
-        self._put_account(new_account)
+        if balance:
+            new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
+
+        self.put_account(new_account)
         return new_account
 
     def create_initialized_contract_account(self, contract_code, storage) -> None:
@@ -86,10 +109,10 @@ class WorldState:
         """
         # TODO: Add type hints
         new_account = Account(
-            self._generate_new_address(), code=contract_code, balance=0
+            self._generate_new_address(), code=contract_code, balances=self.balances
         )
         new_account.storage = storage
-        self._put_account(new_account)
+        self.put_account(new_account)
 
     def annotate(self, annotation: StateAnnotation) -> None:
         """
@@ -116,22 +139,24 @@ class WorldState:
         """
         return filter(lambda x: isinstance(x, annotation_type), self.annotations)
 
-    def _generate_new_address(self, creator=None) -> str:
+    def _generate_new_address(self, creator=None) -> BitVec:
         """Generates a new address for the global state.
 
         :return:
         """
         if creator:
             # TODO: Use nounce
-            return "0x" + str(mk_contract_address(creator, 0).hex())
+            address = "0x" + str(mk_contract_address(creator, 0).hex())
+            return symbol_factory.BitVecVal(int(address, 16), 256)
         while True:
             address = "0x" + "".join([str(hex(randint(0, 16)))[-1] for _ in range(40)])
-            if address not in self.accounts.keys():
+            if address not in self._accounts.keys():
-                return address
+                return symbol_factory.BitVecVal(int(address, 16), 256)
 
-    def _put_account(self, account: Account) -> None:
+    def put_account(self, account: Account) -> None:
         """
 
         :param account:
         """
-        self.accounts[account.address] = account
+        self._accounts[account.address.value] = account
+        account._balances = self.balances

mythril/laser/ethereum/svm.py

@@ -9,12 +9,12 @@ from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
 from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
 from mythril.laser.ethereum.evm_exceptions import VmException
 from mythril.laser.ethereum.instructions import Instruction
-from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.iprof import InstructionProfiler
+from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
 from mythril.laser.ethereum.time_handler import time_handler
-from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState
 from mythril.laser.ethereum.transaction import (
     ContractCreationTransaction,
     TransactionEndSignal,
@@ -22,7 +22,7 @@ from mythril.laser.ethereum.transaction import (
     execute_contract_creation,
     execute_message_call,
 )
-from mythril.laser.ethereum.iprof import InstructionProfiler
+from mythril.laser.smt import symbol_factory
 
 log = logging.getLogger(__name__)
 
@@ -46,7 +46,6 @@ class LaserEVM:
 
     def __init__(
         self,
-        accounts: Dict[str, Account],
         dynamic_loader=None,
         max_depth=float("inf"),
         execution_timeout=60,
@@ -57,21 +56,18 @@ class LaserEVM:
         enable_iprof=False,
     ) -> None:
         """
+        Initializes the laser evm object
 
-        :param accounts:
+        :param dynamic_loader: Loads data from chain
-        :param dynamic_loader:
+        :param max_depth: Maximum execution depth this vm should execute
-        :param max_depth:
+        :param execution_timeout: Time to take for execution
-        :param execution_timeout:
+        :param create_timeout: Time to take for contract creation
-        :param create_timeout:
+        :param strategy: Execution search strategy
-        :param strategy:
+        :param transaction_count: The amount of transactions to execute
-        :param transaction_count:
+        :param requires_statespace: Variable indicating whether the statespace should be recorded
+        :param enable_iprof: Variable indicating whether instruction profiling should be turned on
         """
-        world_state = WorldState()
+        self.open_states = []  # type: List[WorldState]
-        world_state.accounts = accounts
-        # this sets the initial world state
-        self.world_state = world_state
-        self.open_states = [world_state]
-
         self.total_states = 0
         self.dynamic_loader = dynamic_loader
 
@@ -106,23 +102,30 @@ class LaserEVM:
 
         log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
 
-    @property
-    def accounts(self) -> Dict[str, Account]:
-        """
-
-        :return:
-        """
-        return self.world_state.accounts
-
     def sym_exec(
-        self, main_address=None, creation_code=None, contract_name=None
+        self,
+        world_state: WorldState = None,
+        target_address: int = None,
+        creation_code: str = None,
+        contract_name: str = None,
     ) -> None:
-        """
+        """ Starts symbolic execution
+        There are two modes of execution.
+        Either we analyze a preconfigured configuration, in which case the world_state and target_address variables
+        must be supplied.
+        Or we execute the creation code of a contract, in which case the creation code and desired name of that
+        contract should be provided.
+
+        :param world_state The world state configuration from which to perform analysis
+        :param target_address The address of the contract account in the world state which analysis should target
+        :param creation_code The creation code to create the target contract in the symbolic environment
+        :param contract_name The name that the created account should be associated with
+        """
+        pre_configuration_mode = world_state is not None and target_address is not None
+        scratch_mode = creation_code is not None and contract_name is not None
+        if pre_configuration_mode == scratch_mode:
+            raise ValueError("Symbolic execution started with invalid parameters")
 
-        :param main_address:
-        :param creation_code:
-        :param contract_name:
-        """
         log.debug("Starting LASER execution")
         for hook in self._start_sym_exec_hooks:
             hook()
@@ -130,11 +133,12 @@ class LaserEVM:
         time_handler.start_execution(self.execution_timeout)
         self.time = datetime.now()
 
-        if main_address:
+        if pre_configuration_mode:
-            log.info("Starting message call transaction to {}".format(main_address))
+            self.open_states = [world_state]
-            self._execute_transactions(main_address)
+            log.info("Starting message call transaction to {}".format(target_address))
+            self._execute_transactions(symbol_factory.BitVecVal(target_address, 256))
 
-        elif creation_code:
+        elif scratch_mode:
             log.info("Starting contract creation transaction")
             created_account = execute_contract_creation(
                 self, creation_code, contract_name
@@ -355,7 +359,7 @@ class LaserEVM:
         if not revert_changes:
             return_global_state.world_state = copy(global_state.world_state)
             return_global_state.environment.active_account = global_state.accounts[
-                return_global_state.environment.active_account.address
+                return_global_state.environment.active_account.address.value
             ]
 
         # Execute the post instruction handler
@@ -389,19 +393,6 @@ class LaserEVM:
                 self._new_node_state(
                     state, JumpType.CONDITIONAL, state.mstate.constraints[-1]
                 )
-
-        elif opcode in ("CALL", "CALLCODE", "DELEGATECALL", "STATICCALL"):
-            assert len(new_states) <= 1
-            for state in new_states:
-                self._new_node_state(state, JumpType.CALL)
-                # Keep track of added contracts so the graph can be generated properly
-                if (
-                    state.environment.active_account.contract_name
-                    not in self.world_state.accounts.keys()
-                ):
-                    self.world_state.accounts[
-                        state.environment.active_account.address
-                    ] = state.environment.active_account
         elif opcode == "RETURN":
             for state in new_states:
                 self._new_node_state(state, JumpType.RETURN)

mythril/laser/ethereum/transaction/symbolic.py

@@ -2,25 +2,32 @@
 symbolic values."""
 import logging
 
-
-from mythril.laser.smt import symbol_factory
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
-from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata
 from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.calldata import SymbolicCalldata
+from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.transaction.transaction_models import (
     MessageCallTransaction,
     ContractCreationTransaction,
     get_next_transaction_id,
+    BaseTransaction,
 )
+from mythril.laser.smt import symbol_factory, Or, BitVec
 
 log = logging.getLogger(__name__)
 
 CREATOR_ADDRESS = 0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE
 ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
 
+ACTOR_ADDRESSES = [
+    symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256),
+    symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256),
+    symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEE, 256),
+]
+
 
-def execute_message_call(laser_evm, callee_address: str) -> None:
+def execute_message_call(laser_evm, callee_address: BitVec) -> None:
     """Executes a message call transaction from all open states.
 
     :param laser_evm:
@@ -46,7 +53,9 @@ def execute_message_call(laser_evm, callee_address: str) -> None:
             origin=symbol_factory.BitVecSym(
                 "origin{}".format(next_transaction_id), 256
             ),
-            caller=symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256),
+            caller=symbol_factory.BitVecSym(
+                "sender_{}".format(next_transaction_id), 256
+            ),
             callee_account=open_world_state[callee_address],
             call_data=SymbolicCalldata(next_transaction_id),
             call_value=symbol_factory.BitVecSym(
@@ -69,12 +78,14 @@ def execute_contract_creation(
     :return:
     """
     # TODO: Resolve circular import between .transaction and ..svm to import LaserEVM here
-    open_states = laser_evm.open_states[:]
     del laser_evm.open_states[:]
 
-    new_account = laser_evm.world_state.create_account(
+    world_state = WorldState()
+    open_states = [world_state]
+    new_account = world_state.create_account(
         0, concrete_storage=True, dynamic_loader=None, creator=CREATOR_ADDRESS
     )
+
     if contract_name:
         new_account.contract_name = contract_name
 
@@ -104,7 +115,7 @@ def execute_contract_creation(
     return new_account
 
 
-def _setup_global_state_for_execution(laser_evm, transaction) -> None:
+def _setup_global_state_for_execution(laser_evm, transaction: BaseTransaction) -> None:
     """Sets up global state and cfg for a transactions execution.
 
     :param laser_evm:
@@ -114,6 +125,10 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
     global_state = transaction.initial_global_state()
     global_state.transaction_stack.append((transaction, None))
 
+    global_state.mstate.constraints.append(
+        Or(*[transaction.caller == actor for actor in ACTOR_ADDRESSES])
+    )
+
     new_node = Node(
         global_state.environment.active_account.contract_name,
         function_name=global_state.environment.active_function_name,

mythril/laser/ethereum/transaction/transaction_models.py

@@ -111,8 +111,19 @@ class BaseTransaction:
         # Initialize the execution environment
         global_state = GlobalState(self.world_state, environment, None)
         global_state.environment.active_function_name = active_function
+
+        sender = environment.sender
+        receiver = environment.active_account.address
+        value = environment.callvalue
+
+        global_state.world_state.balances[sender] -= value
+        global_state.world_state.balances[receiver] += value
+
         return global_state
 
+    def initial_global_state(self) -> GlobalState:
+        raise NotImplementedError
+
 
 class MessageCallTransaction(BaseTransaction):
     """Transaction object models an transaction."""
@@ -143,6 +154,7 @@ class MessageCallTransaction(BaseTransaction):
         :param revert:
         """
         self.return_data = return_data
+
         raise TransactionEndSignal(global_state, revert)
 
 
@@ -190,7 +202,9 @@ class ContractCreationTransaction(BaseTransaction):
         contract_code = bytes.hex(array.array("B", return_data).tostring())
 
         global_state.environment.active_account.code.assign_bytecode(contract_code)
-        self.return_data = global_state.environment.active_account.address
+        self.return_data = str(
+            hex(global_state.environment.active_account.address.value)
+        )
         assert global_state.environment.active_account.code.instruction_list != []
 
         raise TransactionEndSignal(global_state, revert=revert)

mythril/laser/smt/bool.py

@@ -90,15 +90,16 @@ def And(*args: Union[Bool, bool]) -> Bool:
     return Bool(z3.And([a.raw for a in args_list]), union)
 
 
-def Or(a: Bool, b: Bool) -> Bool:
+def Or(*args: Union[Bool, bool]) -> Bool:
     """Create an or expression.
 
     :param a:
     :param b:
     :return:
     """
-    union = a.annotations + b.annotations
+    args_list = [arg if isinstance(arg, Bool) else Bool(arg) for arg in args]
-    return Bool(z3.Or(a.raw, b.raw), annotations=union)
+    union = [arg.annotations for arg in args_list]
+    return Bool(z3.Or([a.raw for a in args_list]), annotations=union)
 
 
 def Not(a: Bool) -> Bool:

tests/laser/evm_testsuite/evm_test.py

@@ -1,8 +1,9 @@
 from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.transaction.concolic import execute_message_call
-from mythril.laser.smt import Expression, BitVec
+from mythril.laser.smt import Expression, BitVec, symbol_factory
 from mythril.analysis.solver import get_model
 from datetime import datetime
 
@@ -82,25 +83,27 @@ def test_vmtest(
     # Arrange
     if test_name == "gasprice":
         return
-    accounts = {}
+
+    world_state = WorldState()
+
     for address, details in pre_condition.items():
         account = Account(address)
         account.code = Disassembly(details["code"][2:])
-        account.balance = int(details["balance"], 16)
         account.nonce = int(details["nonce"], 16)
+        world_state.put_account(account)
+        account.set_balance(int(details["balance"], 16))
 
-        accounts[address] = account
+    laser_evm = LaserEVM()
-
+    laser_evm.open_states = [world_state]
-    laser_evm = LaserEVM(accounts)
 
     # Act
     laser_evm.time = datetime.now()
 
     final_states = execute_message_call(
         laser_evm,
-        callee_address=action["address"],
+        callee_address=symbol_factory.BitVecVal(int(action["address"], 16), 256),
-        caller_address=action["caller"],
+        caller_address=symbol_factory.BitVecVal(int(action["caller"], 16), 256),
-        origin_address=binascii.a2b_hex(action["origin"][2:]),
+        origin_address=symbol_factory.BitVecVal(int(action["origin"], 16), 256),
         code=action["code"][2:],
         gas_limit=int(action["gas"], 16),
         data=binascii.a2b_hex(action["data"][2:]),
@@ -132,7 +135,7 @@ def test_vmtest(
         )
 
         for address, details in post_condition.items():
-            account = world_state[address]
+            account = world_state[symbol_factory.BitVecVal(int(address, 16), 256)]
 
             assert account.nonce == int(details["nonce"], 16)
             assert account.code.bytecode == details["code"][2:]

tests/laser/test_transaction.py

@@ -1,6 +1,8 @@
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum import svm
 from mythril.laser.ethereum.state.account import Account
+from mythril.laser.ethereum.state.world_state import WorldState
+
 import mythril.laser.ethereum.cfg as cfg
 
 
@@ -18,15 +20,17 @@ def test_intercontract_call():
     )
     callee_address = "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef"
 
+    world_state = WorldState()
+
     caller_account = Account(caller_address, caller_code, contract_name="Caller")
     callee_account = Account(callee_address, callee_code, contract_name="Callee")
+    world_state.put_account(callee_account)
+    world_state.put_account(caller_account)
 
-    accounts = {caller_address: caller_account, callee_address: callee_account}
+    laser = svm.LaserEVM()
-
-    laser = svm.LaserEVM(accounts)
 
     # Act
-    laser.sym_exec(caller_address)
+    laser.sym_exec(world_state=world_state, target_address=int(caller_address, 16))
 
     # Assert
     # Initial node starts in contract caller

tests/laser/transaction/symbolic_test.py

@@ -9,6 +9,8 @@ from mythril.laser.ethereum.transaction import (
 from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.world_state import WorldState
+from mythril.laser.smt import symbol_factory
+
 import unittest.mock as mock
 from unittest.mock import MagicMock
 
@@ -29,7 +31,7 @@ def test_execute_message_call(mocked_setup: MagicMock):
     laser_evm = LaserEVM({})
 
     world_state = WorldState()
-    world_state.accounts["address"] = Account("address")
+    world_state.put_account(Account("0x0"))
 
     laser_evm.open_states = [world_state]
     laser_evm.exec = MagicMock()
@@ -37,7 +39,7 @@ def test_execute_message_call(mocked_setup: MagicMock):
     mocked_setup.side_effect = _is_message_call
 
     # Act
-    execute_message_call(laser_evm, "address")
+    execute_message_call(laser_evm, symbol_factory.BitVecVal(0, 256))
 
     # Assert
     # laser_evm.exec.assert_called_once()

tests/native_test.py

@@ -3,6 +3,7 @@ from mythril.mythril import MythrilDisassembler
 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 import svm
 from tests import BaseTestCase
 
@@ -29,13 +30,6 @@ IDENTITY_TEST[1] = (hex(476934798798347), False)
 
 
 def _all_info(laser):
-    accounts = {}
-    for address, _account in laser.world_state.accounts.items():
-        account = _account.as_dict
-        account["code"] = account["code"].instruction_list
-        account["balance"] = str(account["balance"])
-        accounts[address] = account
-
     nodes = {}
     for uid, node in laser.nodes.items():
         states = []
@@ -66,7 +60,6 @@ def _all_info(laser):
     edges = [edge.as_dict for edge in laser.edges]
 
     return {
-        "accounts": accounts,
         "nodes": nodes,
         "edges": edges,
         "total_states": laser.total_states,
@@ -85,13 +78,13 @@ class NativeTests(BaseTestCase):
         """"""
         disassembly = SolidityContract(
             "./tests/native_tests.sol",
-            solc_binary=MythrilDisassembler._init_solc_binary("0.5.0"),
+            solc_binary=MythrilDisassembler._init_solc_binary("0.5.3"),
         ).disassembly
         account = Account("0x0000000000000000000000000000000000000000", disassembly)
-        accounts = {account.address: account}
+        world_state = WorldState()
-
+        world_state.put_account(account)
-        laser = svm.LaserEVM(accounts, max_depth=100, transaction_count=1)
+        laser = svm.LaserEVM(max_depth=100, transaction_count=1)
-        laser.sym_exec(account.address)
+        laser.sym_exec(world_state=world_state, target_address=account.address.value)
 
         laser_info = str(_all_info(laser))
 

tests/report_test.py

@@ -32,7 +32,7 @@ def _generate_report(input_file):
     contract = EVMContract(input_file.read_text(), enable_online_lookup=False)
     sym = SymExecWrapper(
         contract,
-        address=(util.get_indexed_address(0)),
+        address=0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE,
         strategy="dfs",
         execution_timeout=30,
         transaction_count=1,

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

@@ -1,36 +0,0 @@
-{
-    "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/environments.sol.o.markdown

@@ -1,34 +0,0 @@
-# Analysis results for test-filename.sol
-
-## Integer Overflow
-- SWC ID: 101
-- Type: Warning
-- Contract: Unknown
-- Function name: `_function_0x83f12fec`
-- PC address: 158
-
-### Description
-
-The arithmetic operation can result in integer overflow.
-
-## Integer Overflow
-- SWC ID: 101
-- Type: Warning
-- Contract: Unknown
-- Function name: `_function_0x83f12fec`
-- PC address: 278
-
-### Description
-
-The arithmetic operation can result in integer overflow.
-
-## Integer Underflow
-- SWC ID: 101
-- Type: Warning
-- Contract: Unknown
-- Function name: `_function_0x83f12fec`
-- PC address: 378
-
-### Description
-
-The substraction can result in an integer underflow.

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

@@ -1,30 +0,0 @@
-==== Integer Overflow ====
-SWC ID: 101
-Type: Warning
-Contract: Unknown
-Function name: _function_0x83f12fec
-PC address: 158
-The arithmetic operation can result in integer overflow.
-
---------------------
-
-==== Integer Overflow ====
-SWC ID: 101
-Type: Warning
-Contract: Unknown
-Function name: _function_0x83f12fec
-PC address: 278
-The arithmetic operation can result in integer overflow.
-
---------------------
-
-==== Integer Underflow ====
-SWC ID: 101
-Type: Warning
-Contract: Unknown
-Function name: _function_0x83f12fec
-PC address: 378
-The substraction can result in an integer underflow.
-
---------------------
-

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

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

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

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

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

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

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

@@ -26,6 +26,19 @@
             "sourceMap": null,
             "swc-id": "101",
             "title": "Integer Underflow"
+        },
+        {
+            "address": 725,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
+            "function": "sendeth(address,uint256)",
+            "max_gas_used": 78155,
+            "min_gas_used": 17019,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "101",
+            "title": "Integer Overflow"
         }
     ],
     "success": true

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

@@ -34,6 +34,23 @@
                 "severity": "High",
                 "swcID": "SWC-101",
                 "swcTitle": "Integer Overflow and Underflow"
+            },
+            {
+                "description": {
+                    "head": "The binary addition can overflow.",
+                    "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
+                },
+                "extra": {
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                },
+                "locations": [
+                    {
+                        "sourceMap": "725:1:0"
+                    }
+                ],
+                "severity": "High",
+                "swcID": "SWC-101",
+                "swcTitle": "Integer Overflow and Underflow"
             }
         ],
         "meta": {},

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

@@ -25,3 +25,16 @@ The operands of the subtraction operation are not sufficiently constrained. The
 
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
+
+## Integer Overflow
+- SWC ID: 101
+- Severity: High
+- Contract: Unknown
+- Function name: `sendeth(address,uint256)`
+- PC address: 725
+- Estimated Gas Usage: 17019 - 78155
+
+### Description
+
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.

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

@@ -20,3 +20,14 @@ The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------
 
+==== Integer Overflow ====
+SWC ID: 101
+Severity: High
+Contract: Unknown
+Function name: sendeth(address,uint256)
+PC address: 725
+Estimated Gas Usage: 17019 - 78155
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.
+--------------------
+

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

@@ -1,166 +0,0 @@
-{
-    "success": true,
-    "error": null,
-    "issues": [
-        {
-            "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`.",
-            "function": "_function_0x4229616d",
-            "type": "Warning",
-            "address": 1599,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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`.",
-            "function": "_function_0xb4022950",
-            "type": "Warning",
-            "address": 1940,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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`.",
-            "function": "_function_0xb4022950",
-            "type": "Warning",
-            "address": 2582,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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. ",
-            "function": "_function_0x57d4021b",
-            "type": "Informational",
-            "address": 1653,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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. ",
-            "function": "_function_0x9dbc4f9b",
-            "type": "Informational",
-            "address": 2085,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "fallback",
-            "type": "Informational",
-            "address": 3111,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "fallback",
-            "type": "Informational",
-            "address": 3140,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "fallback",
-            "type": "Informational",
-            "address": 2950,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "fallback",
-            "type": "Informational",
-            "address": 1268,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x09dfdc71",
-            "type": "Informational",
-            "address": 310,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x09dfdc71",
-            "type": "Informational",
-            "address": 1316,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x253459e3",
-            "type": "Informational",
-            "address": 1375,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x4229616d",
-            "type": "Informational",
-            "address": 1511,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x57d4021b",
-            "type": "Informational",
-            "address": 1679,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x6fbaaa1e",
-            "type": "Informational",
-            "address": 618,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x8a5fb3ca",
-            "type": "Informational",
-            "address": 805,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "title": "Invariant branch condition",
-            "description": "Found a conditional jump which always follows the same branch",
-            "function": "_function_0x9dbc4f9b",
-            "type": "Informational",
-            "address": 2187,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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.",
-            "function": "_function_0x4229616d",
-            "type": "Informational",
-            "address": 1599,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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.",
-            "function": "_function_0xb4022950",
-            "type": "Informational",
-            "address": 1940,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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.",
-            "function": "_function_0xb4022950",
-            "type": "Informational",
-            "address": 2582,
-            "debug": "<DEBUG-DATA>"
-        }
-    ]
-}

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

@@ -1,238 +0,0 @@
-# Analysis results for test-filename.sol
-
-## Ether send
-
-- Type: Warning
-- Contract: Unknown
-- Function name: `_function_0x4229616d`
-- PC address: 1599
-
-### Description
-
-In the function `_function_0x4229616d` a non-zero amount of Ether is sent to an address taken from storage slot 5.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-
-## Ether send
-
-- Type: Warning
-- Contract: Unknown
-- Function name: `_function_0xb4022950`
-- PC address: 1940
-
-### Description
-
-In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-
-## Ether send
-
-- Type: Warning
-- Contract: Unknown
-- Function name: `_function_0xb4022950`
-- PC address: 2582
-
-### Description
-
-In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-
-## Exception state
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x57d4021b`
-- PC address: 1653
-
-### 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. 
-
-## Exception state
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x9dbc4f9b`
-- PC address: 2085
-
-### 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. 
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `fallback`
-- PC address: 3111
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: True
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `fallback`
-- PC address: 3140
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: True
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `fallback`
-- PC address: 2950
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: True
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `fallback`
-- PC address: 1268
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: True
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x09dfdc71`
-- PC address: 310
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: False
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x09dfdc71`
-- PC address: 1316
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: True
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x253459e3`
-- PC address: 1375
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: True
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x4229616d`
-- PC address: 1511
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: True
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x57d4021b`
-- PC address: 1679
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: True
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x6fbaaa1e`
-- PC address: 618
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: False
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x8a5fb3ca`
-- PC address: 805
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: False
-
-## Tautology
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x9dbc4f9b`
-- PC address: 2187
-
-### Description
-
-Found a conditional jump which always follows the same branch, value: True
-
-## Unchecked CALL return value
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0x4229616d`
-- PC address: 1599
-
-### Description
-
-The return value of an external call is not checked. Note that execution continue even if the called contract throws.
-
-## Unchecked CALL return value
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0xb4022950`
-- PC address: 1940
-
-### Description
-
-The return value of an external call is not checked. Note that execution continue even if the called contract throws.
-
-## Unchecked CALL return value
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0xb4022950`
-- PC address: 2582
-
-### Description
-
-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.text

@@ -1,177 +0,0 @@
-==== Ether send ====
-Type: Warning
-Contract: Unknown
-Function name: _function_0x4229616d
-PC address: 1599
-In the function `_function_0x4229616d` a non-zero amount of Ether is sent to an address taken from storage slot 5.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
---------------------
-
-==== Ether send ====
-Type: Warning
-Contract: Unknown
-Function name: _function_0xb4022950
-PC address: 1940
-In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
---------------------
-
-==== Ether send ====
-Type: Warning
-Contract: Unknown
-Function name: _function_0xb4022950
-PC address: 2582
-In the function `_function_0xb4022950` a non-zero amount of Ether is sent to an address taken from storage slot 5.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-There is a check on storage index 5. This storage slot can be written to by calling the function `_function_0x67f809e9`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
---------------------
-
-==== Exception state ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x57d4021b
-PC address: 1653
-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. 
---------------------
-
-==== Exception state ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x9dbc4f9b
-PC address: 2085
-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. 
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: fallback
-PC address: 3111
-Found a conditional jump which always follows the same branch, value: True
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: fallback
-PC address: 3140
-Found a conditional jump which always follows the same branch, value: True
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: fallback
-PC address: 2950
-Found a conditional jump which always follows the same branch, value: True
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: fallback
-PC address: 1268
-Found a conditional jump which always follows the same branch, value: True
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x09dfdc71
-PC address: 310
-Found a conditional jump which always follows the same branch, value: False
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x09dfdc71
-PC address: 1316
-Found a conditional jump which always follows the same branch, value: True
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x253459e3
-PC address: 1375
-Found a conditional jump which always follows the same branch, value: True
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x4229616d
-PC address: 1511
-Found a conditional jump which always follows the same branch, value: True
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x57d4021b
-PC address: 1679
-Found a conditional jump which always follows the same branch, value: True
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x6fbaaa1e
-PC address: 618
-Found a conditional jump which always follows the same branch, value: False
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x8a5fb3ca
-PC address: 805
-Found a conditional jump which always follows the same branch, value: False
---------------------
-
-==== Tautology ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x9dbc4f9b
-PC address: 2187
-Found a conditional jump which always follows the same branch, value: True
---------------------
-
-==== Unchecked CALL return value ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0x4229616d
-PC address: 1599
-The return value of an external call is not checked. Note that execution continue even if the called contract throws.
---------------------
-
-==== Unchecked CALL return value ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0xb4022950
-PC address: 1940
-The return value of an external call is not checked. Note that execution continue even if the called contract throws.
---------------------
-
-==== Unchecked CALL return value ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0xb4022950
-PC address: 2582
-The return value of an external call is not checked. Note that execution continue even if the called contract throws.
---------------------
-

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

@@ -26,6 +26,19 @@
             "sourceMap": null,
             "swc-id": "101",
             "title": "Integer Underflow"
+        },
+        {
+            "address": 725,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
+            "function": "sendeth(address,uint256)",
+            "max_gas_used": 52861,
+            "min_gas_used": 11915,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "101",
+            "title": "Integer Overflow"
         }
     ],
     "success": true

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

@@ -34,6 +34,23 @@
                 "severity": "High",
                 "swcID": "SWC-101",
                 "swcTitle": "Integer Overflow and Underflow"
+            },
+            {
+                "description": {
+                    "head": "The binary addition can overflow.",
+                    "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
+                },
+                "extra": {
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                },
+                "locations": [
+                    {
+                        "sourceMap": "725:1:0"
+                    }
+                ],
+                "severity": "High",
+                "swcID": "SWC-101",
+                "swcTitle": "Integer Overflow and Underflow"
             }
         ],
         "meta": {},

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

@@ -25,3 +25,16 @@ The operands of the subtraction operation are not sufficiently constrained. The
 
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
+
+## Integer Overflow
+- SWC ID: 101
+- Severity: High
+- Contract: Unknown
+- Function name: `sendeth(address,uint256)`
+- PC address: 725
+- Estimated Gas Usage: 11915 - 52861
+
+### Description
+
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.

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

@@ -20,3 +20,14 @@ The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------
 
+==== Integer Overflow ====
+SWC ID: 101
+Severity: High
+Contract: Unknown
+Function name: sendeth(address,uint256)
+PC address: 725
+Estimated Gas Usage: 11915 - 52861
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.
+--------------------
+

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

@@ -1,46 +0,0 @@
-{
-    "success": true,
-    "error": null,
-    "issues": [
-        {
-            "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",
-            "function": "_function_0xe9874106",
-            "type": "Warning",
-            "address": 1285,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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`.",
-            "function": "_function_0xe9874106",
-            "type": "Warning",
-            "address": 1285,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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. ",
-            "function": "fallback",
-            "type": "Informational",
-            "address": 356,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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. ",
-            "function": "_function_0xe9874106",
-            "type": "Informational",
-            "address": 146,
-            "debug": "<DEBUG-DATA>"
-        },
-        {
-            "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",
-            "function": "_function_0xe9874106",
-            "type": "Warning",
-            "address": 1285,
-            "debug": "<DEBUG-DATA>"
-        }
-    ]
-}

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

@@ -1,62 +0,0 @@
-# Analysis results for test-filename.sol
-
-## Dependence on predictable environment variable
-
-- Type: Warning
-- Contract: Unknown
-- Function name: `_function_0xe9874106`
-- PC address: 1285
-
-### Description
-
-In the function `_function_0xe9874106` the following predictable state variables are used to determine Ether recipient:
-- block.coinbase
-
-
-## Ether send
-
-- Type: Warning
-- Contract: Unknown
-- Function name: `_function_0xe9874106`
-- PC address: 1285
-
-### Description
-
-In the function `_function_0xe9874106` a non-zero amount of Ether is sent to an address taken from storage slot 0.
-There is a check on storage index 0. This storage slot can be written to by calling the function `fallback`.
-
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-
-## Exception state
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `fallback`
-- PC address: 356
-
-### 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. 
-
-## Exception state
-
-- Type: Informational
-- Contract: Unknown
-- Function name: `_function_0xe9874106`
-- PC address: 146
-
-### 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. 
-
-## Transaction order dependence
-
-- Type: Warning
-- Contract: Unknown
-- Function name: `_function_0xe9874106`
-- PC address: 1285
-
-### 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

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

@@ -1,46 +0,0 @@
-==== Dependence on predictable environment variable ====
-Type: Warning
-Contract: Unknown
-Function name: _function_0xe9874106
-PC address: 1285
-In the function `_function_0xe9874106` the following predictable state variables are used to determine Ether recipient:
-- block.coinbase
-
---------------------
-
-==== Ether send ====
-Type: Warning
-Contract: Unknown
-Function name: _function_0xe9874106
-PC address: 1285
-In the function `_function_0xe9874106` a non-zero amount of Ether is sent to an address taken from storage slot 0.
-There is a check on storage index 0. This storage slot can be written to by calling the function `fallback`.
-
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
-There is a check on storage index 1. This storage slot can be written to by calling the function `fallback`.
---------------------
-
-==== Exception state ====
-Type: Informational
-Contract: Unknown
-Function name: fallback
-PC address: 356
-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. 
---------------------
-
-==== Exception state ====
-Type: Informational
-Contract: Unknown
-Function name: _function_0xe9874106
-PC address: 146
-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. 
---------------------
-
-==== Transaction order dependence ====
-Type: Warning
-Contract: Unknown
-Function name: _function_0xe9874106
-PC address: 1285
-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
---------------------
-