Clean up leftover code

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 (
+from mythril.laser.ethereum.transaction.symbolic import ATTACKER_ADDRESS
-    ATTACKER_ADDRESS,
-    CREATOR_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 (
+from mythril.laser.smt import UGT, symbol_factory, UGE
-    UGT,
-    Sum,
-    symbol_factory,
-    BVAddNoOverflow,
-    If,
-    simplify,
-    UGE,
-)
 
 log = logging.getLogger(__name__)
 

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))

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 = (
+                transfer_ether(sender, receiver, 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)
@@ -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 = (
+                transfer_ether(sender, receiver, 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)
@@ -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 = (
+                transfer_ether(sender, receiver, 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)
@@ -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 = (
+                transfer_ether(sender, receiver, 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)

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