WIP uselsess commit

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(

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

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:

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

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)
 

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

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