Merge pull request #1347 from ConsenSys/ether_transfer

Ether transfer

mythril/analysis/symbolic.py

@@ -171,6 +171,7 @@ class SymExecWrapper:
                 world_state=world_state,
             )
         else:
+
             account = Account(
                 address,
                 contract.disassembly,
@@ -181,6 +182,34 @@ class SymExecWrapper:
                 if (dynloader is not None and dynloader.active)
                 else False,
             )
+
+            if dynloader is not None:
+                if isinstance(address, int):
+                    try:
+                        _balance = dynloader.read_balance(
+                            "{0:#0{1}x}".format(address, 42)
+                        )
+                        account.set_balance(_balance)
+                    except:
+                        # Initial balance will be a symbolic variable
+                        pass
+                elif isinstance(address, str):
+                    try:
+                        _balance = dynloader.read_balance(address)
+                        account.set_balance(_balance)
+                    except:
+                        # Initial balance will be a symbolic variable
+                        pass
+                elif isinstance(address, BitVec):
+                    try:
+                        _balance = dynloader.read_balance(
+                            "{0:#0{1}x}".format(address.value, 42)
+                        )
+                        account.set_balance(_balance)
+                    except:
+                        # Initial balance will be a symbolic variable
+                        pass
+
             world_state.put_account(account)
             self.laser.sym_exec(world_state=world_state, target_address=address.value)
 

mythril/laser/ethereum/instructions.py

@@ -901,7 +901,11 @@ class Instruction:
         state = global_state.mstate
         address = state.stack.pop()
 
-        balance = global_state.world_state.balances[address]
+        account = global_state.world_state.accounts_exist_or_load(
+            address.value, self.dynamic_loader
+        )
+
+        balance = account.balance()
         state.stack.append(balance)
         return [global_state]
 

mythril/laser/ethereum/plugins/implementations/dependency_pruner.py

@@ -245,6 +245,13 @@ class DependencyPruner(LaserPlugin):
             self.update_calls(annotation.path)
             annotation.has_call = True
 
+        @symbolic_vm.pre_hook("STATICCALL")
+        def staticcall_hook(state: GlobalState):
+            annotation = get_dependency_annotation(state)
+
+            self.update_calls(annotation.path)
+            annotation.has_call = True
+
         @symbolic_vm.pre_hook("STOP")
         def stop_hook(state: GlobalState):
             _transaction_end(state)

mythril/laser/ethereum/plugins/implementations/mutation_pruner.py

@@ -42,6 +42,10 @@ class MutationPruner(LaserPlugin):
         def call_mutator_hook(global_state: GlobalState):
             global_state.annotate(MutationAnnotation())
 
+        @symbolic_vm.pre_hook("STATICCALL")
+        def staticcall_mutator_hook(global_state: GlobalState):
+            global_state.annotate(MutationAnnotation())
+
         @symbolic_vm.laser_hook("add_world_state")
         def world_state_filter_hook(global_state: GlobalState):
             if And(

mythril/laser/ethereum/state/account.py

@@ -127,16 +127,6 @@ class Account:
         self._balances = balances
         self.balance = lambda: self._balances[self.address]
 
-        if not self.address.symbolic and dynamic_loader is not None:
-            try:
-                _balance = dynamic_loader.read_balance(
-                    "{0:#0{1}x}".format(self.address.value, 42)
-                )
-                self.set_balance(_balance)
-            except:
-                # Initial balance will be a symbolic variable
-                pass
-
     def __str__(self) -> str:
         return str(self.as_dict)
 

mythril/laser/ethereum/state/world_state.py

@@ -73,21 +73,51 @@ class WorldState:
         new_world_state.constraints = copy(self.constraints)
         return new_world_state
 
-    def accounts_exist_or_load(self, addr: str, dynamic_loader: DynLoader) -> Account:
+    def accounts_exist_or_load(self, addr, dynamic_loader: DynLoader) -> Account:
         """
         returns account if it exists, else it loads from the dynamic loader
         :param addr: address
         :param dynamic_loader: Dynamic Loader
         :return: The code
         """
-        addr_bitvec = symbol_factory.BitVecVal(int(addr, 16), 256)
+
+        if isinstance(addr, str):
+            addr_bitvec = symbol_factory.BitVecVal(int(addr, 16), 256)
+        elif isinstance(addr, int):
+            addr_bitvec = symbol_factory.BitVecVal(addr, 256)
+        elif not isinstance(addr, BitVec):
+            addr_bitvec = symbol_factory.BitVecVal(int(addr, 16), 256)
 
         if addr_bitvec.value in self.accounts:
             return self.accounts[addr_bitvec.value]
         if dynamic_loader is None:
             raise ValueError("dynamic_loader is None")
+
+        if isinstance(addr, int):
+            try:
+                balance = dynamic_loader.read_balance("{0:#0{1}x}".format(addr, 42))
+                return self.create_account(
+                    balance=balance,
+                    address=addr_bitvec.value,
+                    dynamic_loader=dynamic_loader,
+                    code=dynamic_loader.dynld(addr),
+                )
+            except:
+                # Initial balance will be a symbolic variable
+                pass
+        elif isinstance(addr, str):
+            try:
+                balance = dynamic_loader.read_balance(addr)
+                return self.create_account(
+                    balance=balance,
+                    address=addr_bitvec.value,
+                    dynamic_loader=dynamic_loader,
+                    code=dynamic_loader.dynld(addr),
+                )
+            except:
+                pass
+
         return self.create_account(
-            balance=0,
             address=addr_bitvec.value,
             dynamic_loader=dynamic_loader,
             code=dynamic_loader.dynld(addr),
@@ -126,8 +156,8 @@ class WorldState:
         )
         if code:
             new_account.code = code
-        if balance:
-            new_account.add_balance(symbol_factory.BitVecVal(balance, 256))
+
+        new_account.set_balance(symbol_factory.BitVecVal(balance, 256))
 
         self.put_account(new_account)
         return new_account

mythril/laser/ethereum/svm.py

@@ -9,7 +9,7 @@ from mythril.analysis.potential_issues import check_potential_issues
 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.instructions import Instruction, transfer_ether
 from mythril.laser.ethereum.instruction_data import get_required_stack_elements
 from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState
 from mythril.laser.ethereum.plugins.implementations.plugin_annotations import (
@@ -351,6 +351,13 @@ class LaserEVM:
                 start_signal.global_state.world_state.constraints
             )
 
+            transfer_ether(
+                new_global_state,
+                start_signal.transaction.caller,
+                start_signal.transaction.callee_account.address,
+                start_signal.transaction.call_value,
+            )
+
             log.debug("Starting new transaction %s", start_signal.transaction)
 
             return [new_global_state], op_code

mythril/support/loader.py

@@ -69,9 +69,13 @@ class DynLoader:
         log.debug("Dynld at contract %s", dependency_address)
 
         # Ensure that dependency_address is the correct length, with 0s prepended as needed.
-        dependency_address = (
-            "0x" + "0" * (42 - len(dependency_address)) + dependency_address[2:]
-        )
+
+        if isinstance(dependency_address, int):
+            dependency_address = "0x{:040X}".format(dependency_address)
+        else:
+            dependency_address = (
+                "0x" + "0" * (42 - len(dependency_address)) + dependency_address[2:]
+            )
 
         m = re.match(r"^(0x[0-9a-fA-F]{40})$", dependency_address)