From 074d5a74be2c022d3c2bf419e729621d2696eb1b Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Mon, 22 Jul 2019 09:33:52 -0700
Subject: [PATCH 1/9] WIP uselsess commit

---
 mythril/analysis/modules/ether_thief.py        | 12 +++++++++---
 .../analysis/templates/report_as_text.jinja2   |  2 ++
 mythril/laser/ethereum/call.py                 | 18 ++++++++++++++++--
 mythril/laser/ethereum/instructions.py         | 17 ++++++++++++++---
 mythril/laser/ethereum/state/account.py        |  2 ++
 mythril/laser/ethereum/state/world_state.py    |  5 ++++-
 .../ethereum/transaction/transaction_models.py |  5 +++--
 7 files changed, 50 insertions(+), 11 deletions(-)

diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py
index 76952a54..b5dc8c02 100644
--- a/mythril/analysis/modules/ether_thief.py
+++ b/mythril/analysis/modules/ether_thief.py
@@ -114,15 +114,21 @@ class EtherThief(DetectionModule):
         Require that the current transaction is sent by the attacker and
         that the Ether is sent to the attacker's address.
         """
-
+        attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256)
+        eth_recieved_by_attacker = (
+            value
+            + state.world_state.balances[attacker_address_bitvec]
+            - state.world_state.starting_balances[attacker_address_bitvec]
+        )
+        eth_recieved_by_attacker.simplify()
+        print(eth_recieved_by_attacker)
         constraints += [
-            UGT(value, eth_sent_by_attacker),
+            UGT(eth_recieved_by_attacker, eth_sent_by_attacker),
             target == ATTACKER_ADDRESS,
             state.current_transaction.caller == ATTACKER_ADDRESS,
         ]
 
         try:
-
             transaction_sequence = solver.get_transaction_sequence(state, constraints)
 
             issue = Issue(
diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2
index dd70bb45..776b661d 100644
--- a/mythril/analysis/templates/report_as_text.jinja2
+++ b/mythril/analysis/templates/report_as_text.jinja2
@@ -21,6 +21,8 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
 {% if issue.tx_sequence %}
 Transaction Sequence:
 
+{{ issue.tx_sequence.initialState }}
+
 {% for step in issue.tx_sequence.steps %}
 {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
 Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py
index 918c1d3f..7cb084b0 100644
--- a/mythril/laser/ethereum/call.py
+++ b/mythril/laser/ethereum/call.py
@@ -49,7 +49,11 @@ def get_call_parameters(
 
     callee_account = None
     call_data = get_call_data(global_state, memory_input_offset, memory_input_size)
-    if int(callee_address, 16) >= 5 or int(callee_address, 16) == 0:
+    if (
+        isinstance(callee_address, BitVec)
+        or int(callee_address, 16) >= 5
+        or int(callee_address, 16) == 0
+    ):
         callee_account = get_callee_account(
             global_state, callee_address, dynamic_loader
         )
@@ -88,6 +92,8 @@ def get_callee_address(
         log.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
         if match is None or dynamic_loader is None:
+            # TODO: Fix types
+            return symbolic_to_address
             raise ValueError()
 
         index = int(match.group(1))
@@ -111,7 +117,9 @@ def get_callee_address(
 
 
 def get_callee_account(
-    global_state: GlobalState, callee_address: str, dynamic_loader: DynLoader
+    global_state: GlobalState,
+    callee_address: Union[str, BitVec],
+    dynamic_loader: DynLoader,
 ):
     """Gets the callees account from the global_state.
 
@@ -123,6 +131,12 @@ def get_callee_account(
     environment = global_state.environment
     accounts = global_state.accounts
 
+    if isinstance(callee_address, BitVec):
+        if callee_address.symbolic:
+            return Account(callee_address, balances=global_state.world_state.balances)
+        else:
+            callee_address = callee_address.value
+
     try:
         return global_state.accounts[int(callee_address, 16)]
     except KeyError:
diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index b3e3eaa6..79c00945 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -25,7 +25,7 @@ from mythril.laser.smt import (
     Bool,
     Not,
     LShR,
-)
+    BVSubNoUnderflow, UGE)
 from mythril.laser.smt import symbol_factory
 
 import mythril.laser.ethereum.util as helper
@@ -840,7 +840,11 @@ class Instruction:
         """
         state = global_state.mstate
         address = state.stack.pop()
-        state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
+
+        balance = global_state.world_state.balances[
+            global_state.environment.active_account.address
+        ]
+        state.stack.append(balance)
         return [global_state]
 
     @StateTransition()
@@ -1688,7 +1692,14 @@ class Instruction:
             )
 
             if callee_account is not None and callee_account.code.bytecode == "":
-                log.debug("The call is related to ether transfer between accounts")
+                log.warning(
+                    "The call is related to ether transfer between accounts"
+                )  # TODO: was debug
+
+                global_state.mstate.constraints.append(UGE(global_state.world_state.balances[environment.active_account.address], value))
+                #global_state.world_state.balances[environment.active_account.address] -= value
+                global_state.world_state.balances[callee_account.address] += value
+
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
                 )
diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index f5196287..9e83f63a 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -169,6 +169,8 @@ class Account:
         self._balances = balances
         self.balance = lambda: self._balances[self.address]
 
+        # TODO: Add initial balance
+
     def __str__(self) -> str:
         return str(self.as_dict)
 
diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py
index 236da526..d5851533 100644
--- a/mythril/laser/ethereum/state/world_state.py
+++ b/mythril/laser/ethereum/state/world_state.py
@@ -27,6 +27,7 @@ class WorldState:
         """
         self._accounts = {}  # type: Dict[int, Account]
         self.balances = Array("balance", 256, 256)
+        self.starting_balances = copy(self.balances)
 
         self.node = None  # type: Optional['Node']
         self.transaction_sequence = transaction_sequence or []
@@ -60,6 +61,7 @@ class WorldState:
             annotations=new_annotations,
         )
         new_world_state.balances = copy(self.balances)
+        new_world_state.starting_balances = copy(self.starting_balances)
         for account in self._accounts.values():
             new_world_state.put_account(copy(account))
         new_world_state.node = self.node
@@ -115,7 +117,7 @@ class WorldState:
             concrete_storage=concrete_storage,
         )
         if balance:
-            new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
+            new_account.add_balance(symbol_factory.BitVecVal(balance, 256))
 
         self.put_account(new_account)
         return new_account
@@ -180,5 +182,6 @@ class WorldState:
 
         :param account:
         """
+        assert not account.address.symbolic # ???
         self._accounts[account.address.value] = account
         account._balances = self.balances
diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py
index 93cc7e3b..2f5c34cf 100644
--- a/mythril/laser/ethereum/transaction/transaction_models.py
+++ b/mythril/laser/ethereum/transaction/transaction_models.py
@@ -13,7 +13,7 @@ from mythril.laser.ethereum.state.environment import Environment
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.smt import symbol_factory
+from mythril.laser.smt import symbol_factory, BVSubNoUnderflow, UGE
 
 _next_transaction_id = 0
 
@@ -117,7 +117,8 @@ class BaseTransaction:
         receiver = environment.active_account.address
         value = environment.callvalue
 
-        global_state.world_state.balances[sender] -= value
+        global_state.mstate.constraints.append(UGE(global_state.world_state.balances[sender], value))
+        #global_state.world_state.balances[sender] -= value
         global_state.world_state.balances[receiver] += value
 
         return global_state

From 584bdf13d68b4ebf674168ce150ae5b8127b9d31 Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 24 Jul 2019 15:51:38 -0700
Subject: [PATCH 2/9] First draft of ether balance modeling

---
 mythril/analysis/modules/ether_thief.py       | 64 ++++++-------
 mythril/analysis/solver.py                    | 37 +++++---
 .../analysis/templates/report_as_text.jinja2  |  2 -
 mythril/laser/ethereum/call.py                | 12 +--
 mythril/laser/ethereum/instructions.py        | 91 +++++++++++++++++--
 mythril/laser/ethereum/state/account.py       |  2 -
 mythril/laser/ethereum/state/world_state.py   |  2 +-
 .../transaction/transaction_models.py         | 20 ++--
 tests/laser/evm_testsuite/evm_test.py         |  4 +-
 9 files changed, 156 insertions(+), 78 deletions(-)

diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py
index 95fbe2fb..cf668b25 100644
--- a/mythril/analysis/modules/ether_thief.py
+++ b/mythril/analysis/modules/ether_thief.py
@@ -15,7 +15,15 @@ from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction import ContractCreationTransaction
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import UGT, Sum, symbol_factory, BVAddNoOverflow, If
+from mythril.laser.smt import (
+    UGT,
+    Sum,
+    symbol_factory,
+    BVAddNoOverflow,
+    If,
+    simplify,
+    UGE,
+)
 
 log = logging.getLogger(__name__)
 
@@ -74,55 +82,35 @@ class EtherThief(DetectionModule):
         :param state:
         :return:
         """
+        state = copy(state)
         instruction = state.get_current_instruction()
 
-        if instruction["opcode"] != "CALL":
-            return []
-
-        address = instruction["address"]
-
         value = state.mstate.stack[-3]
         target = state.mstate.stack[-2]
 
-        eth_sent_by_attacker = symbol_factory.BitVecVal(0, 256)
-
         constraints = copy(state.mstate.constraints)
 
-        for tx in state.world_state.transaction_sequence:
-            """
-            Constraint: The call value must be greater than the sum of Ether sent by the attacker over all
-            transactions. This prevents false positives caused by legitimate refund functions.
-            Also constrain the addition from overflowing (otherwise the solver produces solutions with 
-            ridiculously high call values).
-            """
-            constraints += [BVAddNoOverflow(eth_sent_by_attacker, tx.call_value, False)]
-            eth_sent_by_attacker = Sum(
-                eth_sent_by_attacker,
-                tx.call_value * If(tx.caller == ATTACKER_ADDRESS, 1, 0),
-            )
-
-            """
-            Constraint: All transactions must originate from regular users (not the creator/owner).
-            This prevents false positives where the owner willingly transfers ownership to another address.
-            """
-
-            if not isinstance(tx, ContractCreationTransaction):
-                constraints += [tx.caller != CREATOR_ADDRESS]
-
         """
         Require that the current transaction is sent by the attacker and
-        that the Ether is sent to the attacker's address.
+        that the Ether sent to the attacker's address is greater than the
+        amount of Ether the attacker sent.
         """
         attacker_address_bitvec = symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256)
-        eth_recieved_by_attacker = (
-            value
-            + state.world_state.balances[attacker_address_bitvec]
-            - state.world_state.starting_balances[attacker_address_bitvec]
-        )
-        eth_recieved_by_attacker.simplify()
-        print(eth_recieved_by_attacker)
+
+        constraints += [
+            UGE(
+                state.world_state.balances[state.environment.active_account.address],
+                value,
+            )
+        ]
+        state.world_state.balances[attacker_address_bitvec] += value
+        state.world_state.balances[state.environment.active_account.address] -= value
+
         constraints += [
-            UGT(eth_recieved_by_attacker, eth_sent_by_attacker),
+            UGT(
+                state.world_state.balances[attacker_address_bitvec],
+                state.world_state.starting_balances[attacker_address_bitvec],
+            ),
             target == ATTACKER_ADDRESS,
             state.current_transaction.caller == ATTACKER_ADDRESS,
         ]
diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 6a14fb68..547e5d11 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -95,7 +95,7 @@ def get_transaction_sequence(
     concrete_transactions = []
 
     tx_constraints, minimize = _set_minimisation_constraints(
-        transaction_sequence, constraints.copy(), [], 5000
+        transaction_sequence, constraints.copy(), [], 5000, global_state.world_state
     )
 
     try:
@@ -103,19 +103,23 @@ def get_transaction_sequence(
     except UnsatError:
         raise UnsatError
 
-    min_price_dict = {}  # type: Dict[str, int]
+    # Include creation account in initial state
+    # Note: This contains the code, which should not exist until after the first tx
+    initial_world_state = transaction_sequence[0].world_state
+    initial_accounts = initial_world_state.accounts
+
     for transaction in transaction_sequence:
         concrete_transaction = _get_concrete_transaction(model, transaction)
         concrete_transactions.append(concrete_transaction)
 
-        caller = concrete_transaction["origin"]
-        value = int(concrete_transaction["value"], 16)
-        min_price_dict[caller] = min_price_dict.get(caller, 0) + value
-
-    if isinstance(transaction_sequence[0], ContractCreationTransaction):
-        initial_accounts = transaction_sequence[0].prev_world_state.accounts
-    else:
-        initial_accounts = transaction_sequence[0].world_state.accounts
+    min_price_dict = {}  # type: Dict[str, int]
+    for address in initial_accounts.keys():
+        min_price_dict[address] = model.eval(
+            initial_world_state.starting_balances[
+                symbol_factory.BitVecVal(address, 256)
+            ].raw,
+            model_completion=True,
+        ).as_long()
 
     concrete_initial_state = _get_concrete_state(initial_accounts, min_price_dict)
 
@@ -171,7 +175,7 @@ def _get_concrete_transaction(model: z3.Model, transaction: BaseTransaction):
 
 
 def _set_minimisation_constraints(
-    transaction_sequence, constraints, minimize, max_size
+    transaction_sequence, constraints, minimize, max_size, world_state
 ) -> Tuple[Constraints, tuple]:
     """ Set constraints that minimise key transaction values
 
@@ -192,6 +196,15 @@ def _set_minimisation_constraints(
 
         # Minimize
         minimize.append(transaction.call_data.calldatasize)
-        minimize.append(transaction.call_value)
+
+    for account in world_state.accounts.values():
+        # Lazy way to prevent overflows and to ensure "reasonable" balances
+        # Each account starts with less than 100 ETH
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(100000000000000000000, 256),
+                world_state.starting_balances[account.address],
+            )
+        )
 
     return constraints, tuple(minimize)
diff --git a/mythril/analysis/templates/report_as_text.jinja2 b/mythril/analysis/templates/report_as_text.jinja2
index 8fa2454a..d7b84355 100644
--- a/mythril/analysis/templates/report_as_text.jinja2
+++ b/mythril/analysis/templates/report_as_text.jinja2
@@ -21,8 +21,6 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
 {% if issue.tx_sequence %}
 Transaction Sequence:
 
-{{ issue.tx_sequence.initialState }}
-
 {% for step in issue.tx_sequence.steps %}
 {% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
 Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py
index 7cb084b0..f29c34bf 100644
--- a/mythril/laser/ethereum/call.py
+++ b/mythril/laser/ethereum/call.py
@@ -88,13 +88,12 @@ def get_callee_address(
     except TypeError:
         log.debug("Symbolic call encountered")
 
-        match = re.search(r"storage_(\d+)", str(simplify(symbolic_to_address)))
+        match = re.search(r"Storage\[(\d+)\]", str(simplify(symbolic_to_address)))
         log.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
         if match is None or dynamic_loader is None:
             # TODO: Fix types
             return symbolic_to_address
-            raise ValueError()
 
         index = int(match.group(1))
         log.debug("Dynamic contract address at storage index {}".format(index))
@@ -106,8 +105,7 @@ def get_callee_address(
             )
         # TODO: verify whether this happens or not
         except:
-            log.debug("Error accessing contract storage.")
-            raise ValueError
+            return symbolic_to_address
 
         # testrpc simply returns the address, geth response is more elaborate.
         if not re.match(r"^0x[0-9a-f]{40}$", callee_address):
@@ -135,7 +133,7 @@ def get_callee_account(
         if callee_address.symbolic:
             return Account(callee_address, balances=global_state.world_state.balances)
         else:
-            callee_address = callee_address.value
+            callee_address = hex(callee_address.value)[2:]
 
     try:
         return global_state.accounts[int(callee_address, 16)]
@@ -223,12 +221,12 @@ def get_call_data(
 
 def native_call(
     global_state: GlobalState,
-    callee_address: str,
+    callee_address: Union[str, BitVec],
     call_data: BaseCalldata,
     memory_out_offset: Union[int, Expression],
     memory_out_size: Union[int, Expression],
 ) -> Union[List[GlobalState], None]:
-    if not 0 < int(callee_address, 16) < 5:
+    if isinstance(callee_address, BitVec) or not 0 < int(callee_address, 16) < 5:
         return None
 
     log.debug("Native contract called: " + callee_address)
diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 79c00945..eda8a037 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -25,7 +25,9 @@ from mythril.laser.smt import (
     Bool,
     Not,
     LShR,
-    BVSubNoUnderflow, UGE)
+    BVSubNoUnderflow,
+    UGE,
+)
 from mythril.laser.smt import symbol_factory
 
 import mythril.laser.ethereum.util as helper
@@ -1619,7 +1621,7 @@ class Instruction:
         transfer_amount = global_state.environment.active_account.balance()
         # Often the target of the suicide instruction will be symbolic
         # If it isn't then we'll transfer the balance to the indicated contract
-        global_state.world_state[target].add_balance(transfer_amount)
+        global_state.world_state.balances[target] += transfer_amount
 
         global_state.environment.active_account = deepcopy(
             global_state.environment.active_account
@@ -1692,13 +1694,20 @@ class Instruction:
             )
 
             if callee_account is not None and callee_account.code.bytecode == "":
-                log.warning(
-                    "The call is related to ether transfer between accounts"
-                )  # TODO: was debug
+                log.debug("The call is related to ether transfer between accounts")
+                sender = environment.active_account.address
+                receiver = callee_account.address
+                value = (
+                    value
+                    if isinstance(value, BitVec)
+                    else symbol_factory.BitVecVal(value, 256)
+                )
 
-                global_state.mstate.constraints.append(UGE(global_state.world_state.balances[environment.active_account.address], value))
-                #global_state.world_state.balances[environment.active_account.address] -= value
-                global_state.world_state.balances[callee_account.address] += value
+                global_state.mstate.constraints.append(
+                    UGE(global_state.world_state.balances[sender], value)
+                )
+                global_state.world_state.balances[receiver] += value
+                global_state.world_state.balances[sender] -= value
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1815,6 +1824,28 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters(
                 global_state, self.dynamic_loader, True
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = global_state.environment.active_account.address
+                receiver = callee_account.address
+                value = (
+                    value
+                    if isinstance(value, BitVec)
+                    else symbol_factory.BitVecVal(value, 256)
+                )
+
+                global_state.mstate.constraints.append(
+                    UGE(global_state.world_state.balances[sender], value)
+                )
+                global_state.world_state.balances[receiver] += value
+                global_state.world_state.balances[sender] -= value
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@@ -1918,6 +1949,28 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, _, _ = get_call_parameters(
                 global_state, self.dynamic_loader
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = environment.active_account.address
+                receiver = callee_account.address
+                value = (
+                    value
+                    if isinstance(value, BitVec)
+                    else symbol_factory.BitVecVal(value, 256)
+                )
+
+                global_state.mstate.constraints.append(
+                    UGE(global_state.world_state.balances[sender], value)
+                )
+                global_state.world_state.balances[receiver] += value
+                global_state.world_state.balances[sender] -= value
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
@@ -2019,6 +2072,28 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = get_call_parameters(
                 global_state, self.dynamic_loader
             )
+
+            if callee_account is not None and callee_account.code.bytecode == "":
+                log.debug("The call is related to ether transfer between accounts")
+                sender = global_state.environment.active_account.address
+                receiver = callee_account.address
+                value = (
+                    value
+                    if isinstance(value, BitVec)
+                    else symbol_factory.BitVecVal(value, 256)
+                )
+
+                global_state.mstate.constraints.append(
+                    UGE(global_state.world_state.balances[sender], value)
+                )
+                global_state.world_state.balances[receiver] += value
+                global_state.world_state.balances[sender] -= value
+
+                global_state.mstate.stack.append(
+                    global_state.new_bitvec("retval_" + str(instr["address"]), 256)
+                )
+                return [global_state]
+
         except ValueError as e:
             log.debug(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(
diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index 51d61d27..1a32ad37 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -189,8 +189,6 @@ class Account:
         self._balances = balances
         self.balance = lambda: self._balances[self.address]
 
-        # TODO: Add initial balance
-
     def __str__(self) -> str:
         return str(self.as_dict)
 
diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py
index d5851533..5227099e 100644
--- a/mythril/laser/ethereum/state/world_state.py
+++ b/mythril/laser/ethereum/state/world_state.py
@@ -182,6 +182,6 @@ class WorldState:
 
         :param account:
         """
-        assert not account.address.symbolic # ???
+        assert not account.address.symbolic  # ???
         self._accounts[account.address.value] = account
         account._balances = self.balances
diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py
index 2f5c34cf..f29e9236 100644
--- a/mythril/laser/ethereum/transaction/transaction_models.py
+++ b/mythril/laser/ethereum/transaction/transaction_models.py
@@ -4,7 +4,7 @@ execution."""
 import array
 from copy import deepcopy
 from z3 import ExprRef
-from typing import Union, Optional, cast
+from typing import Union, Optional
 
 from mythril.laser.ethereum.state.calldata import ConcreteCalldata
 from mythril.laser.ethereum.state.account import Account
@@ -12,8 +12,10 @@ from mythril.laser.ethereum.state.calldata import BaseCalldata, SymbolicCalldata
 from mythril.laser.ethereum.state.environment import Environment
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.world_state import WorldState
-from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.smt import symbol_factory, BVSubNoUnderflow, UGE
+from mythril.laser.smt import symbol_factory, UGE, BitVec
+import logging
+
+log = logging.getLogger(__name__)
 
 _next_transaction_id = 0
 
@@ -115,11 +117,17 @@ class BaseTransaction:
 
         sender = environment.sender
         receiver = environment.active_account.address
-        value = environment.callvalue
+        value = (
+            environment.callvalue
+            if isinstance(environment.callvalue, BitVec)
+            else symbol_factory.BitVecVal(environment.callvalue, 256)
+        )
 
-        global_state.mstate.constraints.append(UGE(global_state.world_state.balances[sender], value))
-        #global_state.world_state.balances[sender] -= value
+        global_state.mstate.constraints.append(
+            UGE(global_state.world_state.balances[sender], value)
+        )
         global_state.world_state.balances[receiver] += value
+        global_state.world_state.balances[sender] -= value
 
         return global_state
 
diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py
index 244b5844..e5d1727d 100644
--- a/tests/laser/evm_testsuite/evm_test.py
+++ b/tests/laser/evm_testsuite/evm_test.py
@@ -165,8 +165,8 @@ def test_vmtest(
         # no more work to do if error happens or out of gas
         assert len(laser_evm.open_states) == 0
     else:
-        assert len(laser_evm.open_states) == 1
-        world_state = laser_evm.open_states[0]
+        assert len(final_states) == 1
+        world_state = final_states[0].world_state
 
         for address, details in post_condition.items():
             account = world_state[symbol_factory.BitVecVal(int(address, 16), 256)]

From a288da7bb5c42a3e443eccb82a73ea48a03b6dda Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 24 Jul 2019 16:28:03 -0700
Subject: [PATCH 3/9] Clean up leftover code

---
 mythril/analysis/modules/ether_thief.py     | 17 +----
 mythril/laser/ethereum/call.py              |  1 -
 mythril/laser/ethereum/instructions.py      | 73 ++++++++-------------
 mythril/laser/ethereum/state/world_state.py |  1 -
 4 files changed, 30 insertions(+), 62 deletions(-)

diff --git a/mythril/analysis/modules/ether_thief.py b/mythril/analysis/modules/ether_thief.py
index cf668b25..948e9c89 100644
--- a/mythril/analysis/modules/ether_thief.py
+++ b/mythril/analysis/modules/ether_thief.py
@@ -1,29 +1,16 @@
 """This module contains the detection code for unauthorized ether
 withdrawal."""
 import logging
-import json
 from copy import copy
 
 from mythril.analysis import solver
 from mythril.analysis.modules.base import DetectionModule
 from mythril.analysis.report import Issue
-from mythril.laser.ethereum.transaction.symbolic import (
-    ATTACKER_ADDRESS,
-    CREATOR_ADDRESS,
-)
+from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
 from mythril.analysis.swc_data import UNPROTECTED_ETHER_WITHDRAWAL
 from mythril.exceptions import UnsatError
-from mythril.laser.ethereum.transaction import ContractCreationTransaction
 from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.laser.smt import (
-    UGT,
-    Sum,
-    symbol_factory,
-    BVAddNoOverflow,
-    If,
-    simplify,
-    UGE,
-)
+from mythril.laser.smt import UGT, symbol_factory, UGE
 
 log = logging.getLogger(__name__)
 
diff --git a/mythril/laser/ethereum/call.py b/mythril/laser/ethereum/call.py
index f29c34bf..e31f0474 100644
--- a/mythril/laser/ethereum/call.py
+++ b/mythril/laser/ethereum/call.py
@@ -92,7 +92,6 @@ def get_callee_address(
         log.debug("CALL to: " + str(simplify(symbolic_to_address)))
 
         if match is None or dynamic_loader is None:
-            # TODO: Fix types
             return symbolic_to_address
 
         index = int(match.group(1))
diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index eda8a037..80dcd840 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -25,7 +25,6 @@ from mythril.laser.smt import (
     Bool,
     Not,
     LShR,
-    BVSubNoUnderflow,
     UGE,
 )
 from mythril.laser.smt import symbol_factory
@@ -56,6 +55,30 @@ TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
 
 
+def transfer_ether(
+    global_state: GlobalState,
+    sender: BitVec,
+    receiver: BitVec,
+    value: Union[int, BitVec],
+):
+    """
+    Perform an Ether transfer between two accounts
+
+    :param global_state: The global state in which the Ether transfer occurs
+    :param sender: The sender of the Ether
+    :param receiver: The recipient of the Ether
+    :param value: The amount of Ether to send
+    :return:
+    """
+    value = value if isinstance(value, BitVec) else symbol_factory.BitVecVal(value, 256)
+
+    global_state.mstate.constraints.append(
+        UGE(global_state.world_state.balances[sender], value)
+    )
+    global_state.world_state.balances[receiver] += value
+    global_state.world_state.balances[sender] -= value
+
+
 class StateTransition(object):
     """Decorator that handles global state copy and original return.
 
@@ -1697,17 +1720,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = environment.active_account.address
                 receiver = callee_account.address
-                value = (
-                    value
-                    if isinstance(value, BitVec)
-                    else symbol_factory.BitVecVal(value, 256)
-                )
-
-                global_state.mstate.constraints.append(
-                    UGE(global_state.world_state.balances[sender], value)
-                )
-                global_state.world_state.balances[receiver] += value
-                global_state.world_state.balances[sender] -= value
+                transfer_ether(sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1829,17 +1842,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
-                value = (
-                    value
-                    if isinstance(value, BitVec)
-                    else symbol_factory.BitVecVal(value, 256)
-                )
-
-                global_state.mstate.constraints.append(
-                    UGE(global_state.world_state.balances[sender], value)
-                )
-                global_state.world_state.balances[receiver] += value
-                global_state.world_state.balances[sender] -= value
+                transfer_ether(sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1954,17 +1957,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = environment.active_account.address
                 receiver = callee_account.address
-                value = (
-                    value
-                    if isinstance(value, BitVec)
-                    else symbol_factory.BitVecVal(value, 256)
-                )
-
-                global_state.mstate.constraints.append(
-                    UGE(global_state.world_state.balances[sender], value)
-                )
-                global_state.world_state.balances[receiver] += value
-                global_state.world_state.balances[sender] -= value
+                transfer_ether(sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -2077,17 +2070,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
-                value = (
-                    value
-                    if isinstance(value, BitVec)
-                    else symbol_factory.BitVecVal(value, 256)
-                )
-
-                global_state.mstate.constraints.append(
-                    UGE(global_state.world_state.balances[sender], value)
-                )
-                global_state.world_state.balances[receiver] += value
-                global_state.world_state.balances[sender] -= value
+                transfer_ether(sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
diff --git a/mythril/laser/ethereum/state/world_state.py b/mythril/laser/ethereum/state/world_state.py
index 5227099e..20628877 100644
--- a/mythril/laser/ethereum/state/world_state.py
+++ b/mythril/laser/ethereum/state/world_state.py
@@ -182,6 +182,5 @@ class WorldState:
 
         :param account:
         """
-        assert not account.address.symbolic  # ???
         self._accounts[account.address.value] = account
         account._balances = self.balances

From 267fbf06ebf05105777d3c02127de558cc154863 Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 24 Jul 2019 22:44:04 -0700
Subject: [PATCH 4/9] Fix missing argument to function

---
 mythril/laser/ethereum/instructions.py | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py
index 80dcd840..e5347f2f 100644
--- a/mythril/laser/ethereum/instructions.py
+++ b/mythril/laser/ethereum/instructions.py
@@ -1720,7 +1720,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = environment.active_account.address
                 receiver = callee_account.address
-                transfer_ether(sender, receiver, value)
+                transfer_ether(global_state, sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1842,7 +1842,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
-                transfer_ether(sender, receiver, value)
+                transfer_ether(global_state, sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -1957,7 +1957,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = environment.active_account.address
                 receiver = callee_account.address
-                transfer_ether(sender, receiver, value)
+                transfer_ether(global_state, sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)
@@ -2070,7 +2070,7 @@ class Instruction:
                 log.debug("The call is related to ether transfer between accounts")
                 sender = global_state.environment.active_account.address
                 receiver = callee_account.address
-                transfer_ether(sender, receiver, value)
+                transfer_ether(global_state, sender, receiver, value)
 
                 global_state.mstate.stack.append(
                     global_state.new_bitvec("retval_" + str(instr["address"]), 256)

From 2aa0d39646f767c32d28772645911c91c9377ceb Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Thu, 25 Jul 2019 12:03:06 -0700
Subject: [PATCH 5/9] Only add constraint to symbolic Ether balances

---
 mythril/analysis/solver.py                            | 11 ++++++-----
 .../laser/ethereum/transaction/transaction_models.py  |  1 -
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 547e5d11..82e3f2ee 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -200,11 +200,12 @@ def _set_minimisation_constraints(
     for account in world_state.accounts.values():
         # Lazy way to prevent overflows and to ensure "reasonable" balances
         # Each account starts with less than 100 ETH
-        constraints.append(
-            UGE(
-                symbol_factory.BitVecVal(100000000000000000000, 256),
-                world_state.starting_balances[account.address],
+        if account.address.symbolic:
+            constraints.append(
+                UGE(
+                    symbol_factory.BitVecVal(100000000000000000000, 256),
+                    world_state.starting_balances[account.address],
+                )
             )
-        )
 
     return constraints, tuple(minimize)
diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py
index f29e9236..bccdf7aa 100644
--- a/mythril/laser/ethereum/transaction/transaction_models.py
+++ b/mythril/laser/ethereum/transaction/transaction_models.py
@@ -189,7 +189,6 @@ class ContractCreationTransaction(BaseTransaction):
             0, concrete_storage=True, creator=caller.value
         )
         callee_account.contract_name = contract_name
-        # TODO: set correct balance for new account
         super().__init__(
             world_state=world_state,
             callee_account=callee_account,

From 518e33b45b1de974e94eb0779c9c91d8d1f2f6ee Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Mon, 29 Jul 2019 09:25:04 -0700
Subject: [PATCH 6/9] Fix incorrect values in some suicide evm tests

---
 .../evm_testsuite/VMTests/vmSystemOperations/suicide0.json    | 4 ++--
 .../VMTests/vmSystemOperations/suicideNotExistingAccount.json | 4 ++--
 .../VMTests/vmSystemOperations/suicideSendEtherToMe.json      | 4 ++--
 tests/laser/evm_testsuite/evm_test.py                         | 4 ++--
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json
index ae80e8f6..456a7c16 100644
--- a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json
+++ b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicide0.json
@@ -47,7 +47,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {
@@ -55,4 +55,4 @@
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json
index ecf5d3bc..b72d6bcc 100644
--- a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json
+++ b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideNotExistingAccount.json
@@ -54,7 +54,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {
@@ -62,4 +62,4 @@
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json
index 7a8f19b8..f27557ed 100644
--- a/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json
+++ b/tests/laser/evm_testsuite/VMTests/vmSystemOperations/suicideSendEtherToMe.json
@@ -47,7 +47,7 @@
                 }
             },
             "0xcd1722f3947def4cf144679da39c4c32bdc35681" : {
-                "balance" : "0x17",
+                "balance" : "0x0186a0",
                 "code" : "0x6000355415600957005b60203560003555",
                 "nonce" : "0x00",
                 "storage" : {
@@ -55,4 +55,4 @@
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/tests/laser/evm_testsuite/evm_test.py b/tests/laser/evm_testsuite/evm_test.py
index e5d1727d..244b5844 100644
--- a/tests/laser/evm_testsuite/evm_test.py
+++ b/tests/laser/evm_testsuite/evm_test.py
@@ -165,8 +165,8 @@ def test_vmtest(
         # no more work to do if error happens or out of gas
         assert len(laser_evm.open_states) == 0
     else:
-        assert len(final_states) == 1
-        world_state = final_states[0].world_state
+        assert len(laser_evm.open_states) == 1
+        world_state = laser_evm.open_states[0]
 
         for address, details in post_condition.items():
             account = world_state[symbol_factory.BitVecVal(int(address, 16), 256)]

From 73d11a6405284e5db3666959d7b4a5aa56315c4b Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Tue, 6 Aug 2019 09:08:02 -0700
Subject: [PATCH 7/9] Update wiki links to Read the Docs links

---
 README.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index 4eee32a3..df3ad81c 100644
--- a/README.md
+++ b/README.md
@@ -32,7 +32,7 @@ Install from Pypi:
 $ pip3 install mythril
 ```
 
-See the [Wiki](https://github.com/ConsenSys/mythril/wiki/Installation-and-Setup) for more detailed instructions. 
+See the [docs](https://mythril-classic.readthedocs.io/en/master/installation.html) for more detailed instructions. 
 
 ## Usage
 
@@ -75,7 +75,7 @@ Caller: [ATTACKER], function: commencekilling(), txdata: 0x7c11da20, value: 0x0
 ```
 
 
-Instructions for using Mythril are found on the [Wiki](https://github.com/ConsenSys/mythril/wiki). 
+Instructions for using Mythril are found on the [docs](https://mythril-classic.readthedocs.io/en/master/). 
 
 For support or general discussions please join the Mythril community on [Discord](https://discord.gg/E3YrVtG).
 

From b08a9d9d84d8159dd3a3665498bb4ec098a12db4 Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 7 Aug 2019 12:00:18 -0700
Subject: [PATCH 8/9] Constrain all transaction callers to have <= 1000 ETH

---
 mythril/analysis/solver.py | 20 +++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 82e3f2ee..8755c6c5 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -8,7 +8,7 @@ from mythril.analysis.analysis_args import analysis_args
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.ethereum.transaction import BaseTransaction
-from mythril.laser.smt import UGE, Optimize, symbol_factory
+from mythril.laser.smt import UGE, Optimize, symbol_factory, simplify
 from mythril.laser.ethereum.time_handler import time_handler
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (
@@ -197,15 +197,21 @@ def _set_minimisation_constraints(
         # Minimize
         minimize.append(transaction.call_data.calldatasize)
 
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(1000000000000000000000, 256),
+                world_state.starting_balances[transaction.caller],
+            )
+        )
+
     for account in world_state.accounts.values():
         # Lazy way to prevent overflows and to ensure "reasonable" balances
         # Each account starts with less than 100 ETH
-        if account.address.symbolic:
-            constraints.append(
-                UGE(
-                    symbol_factory.BitVecVal(100000000000000000000, 256),
-                    world_state.starting_balances[account.address],
-                )
+        constraints.append(
+            UGE(
+                symbol_factory.BitVecVal(100000000000000000000, 256),
+                world_state.starting_balances[account.address],
             )
+        )
 
     return constraints, tuple(minimize)

From 4bfaadea98bed96a7b4b9385614c99eb74f66261 Mon Sep 17 00:00:00 2001
From: Nathan <nbanmp@gmail.com>
Date: Wed, 7 Aug 2019 12:03:17 -0700
Subject: [PATCH 9/9] Remove unneeded import

---
 mythril/analysis/solver.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py
index 8755c6c5..3358d537 100644
--- a/mythril/analysis/solver.py
+++ b/mythril/analysis/solver.py
@@ -8,7 +8,7 @@ from mythril.analysis.analysis_args import analysis_args
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.constraints import Constraints
 from mythril.laser.ethereum.transaction import BaseTransaction
-from mythril.laser.smt import UGE, Optimize, symbol_factory, simplify
+from mythril.laser.smt import UGE, Optimize, symbol_factory
 from mythril.laser.ethereum.time_handler import time_handler
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (