Fix the account transfer and add initial state

mythril/analysis/solver.py

@@ -1,5 +1,5 @@
 """This module contains analysis module helpers to solve path constraints."""
-from typing import Dict, List
+from typing import Collection, Dict, List
 from z3 import sat, unknown, FuncInterp
 import z3
 
@@ -77,7 +77,9 @@ def pretty_print_model(model):
     return ret
 
 
-def get_transaction_sequence(global_state: GlobalState, constraints) -> Dict[str, List[Dict[str, str]]]:
+def get_transaction_sequence(
+    global_state: GlobalState, constraints
+) -> Dict[str, Collection]:
     """Generate concrete transaction sequence.
 
     :param global_state: GlobalState to generate transaction sequence for
@@ -97,7 +99,7 @@ def get_transaction_sequence(global_state: GlobalState, constraints) -> Dict[str
         "blockDifficulty": "<ARBITRARY_DIFFICULTY>",
         "blockGasLimit": "<ARBITRARY_GAS_LIMIT>",
         "blockNumber": "<ARBITRARY_BLOCKNUMBER>",
-        "blockTime": "<ARBITRARY_BLOCKTIME>"
+        "blockTime": "<ARBITRARY_BLOCKTIME>",
     }  # type: Dict[str, str]
 
     concrete_transactions = []
@@ -105,7 +107,7 @@ def get_transaction_sequence(global_state: GlobalState, constraints) -> Dict[str
     tx_constraints = constraints.copy()
     minimize = []
 
-    transactions = []   # type: List[BaseTransaction]
+    transactions = []  # type: List[BaseTransaction]
     for transaction in transaction_sequence:
         tx_id = str(transaction.id)
         if not isinstance(transaction, ContractCreationTransaction):
@@ -141,13 +143,11 @@ def get_transaction_sequence(global_state: GlobalState, constraints) -> Dict[str
         concrete_transaction["origin"] = "0x" + (
             "%x" % model.eval(transaction.caller.raw, model_completion=True).as_long()
         ).zfill(40)
-        concrete_transaction["address"] = (
-            "%s" % transaction.callee_account.address
-        )
+        concrete_transaction["address"] = "%s" % transaction.callee_account.address
         concrete_transactions.append(concrete_transaction)
-
     steps = {
-        "steps": concrete_transactions
+        "initialState": global_state.world_state.initial_state_account,
+        "steps": concrete_transactions,
     }
 
     return steps

mythril/analysis/symbolic.py

@@ -12,7 +12,10 @@ from mythril.laser.ethereum.strategy.basic import (
     ReturnRandomNaivelyStrategy,
     ReturnWeightedRandomStrategy,
 )
-from mythril.laser.ethereum.transaction.symbolic import CREATOR_ADDRESS
+from mythril.laser.ethereum.transaction.symbolic import (
+    ATTACKER_ADDRESS,
+    CREATOR_ADDRESS,
+)
 
 
 from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory
@@ -72,10 +75,21 @@ class SymExecWrapper:
             dynamic_loader=dynloader,
             contract_name=contract.name,
         )
+        creator_account = Account(
+            hex(CREATOR_ADDRESS), "", dynamic_loader=dynloader, contract_name=None
+        )
+        attacker_account = Account(
+            hex(ATTACKER_ADDRESS), "", dynamic_loader=dynloader, contract_name=None
+        )
+
         requires_statespace = (
             compulsory_statespace or len(get_detection_modules("post", modules)) > 0
         )
-        self.accounts = {address: account}
+        self.accounts = {
+            address: account,
+            hex(CREATOR_ADDRESS): creator_account,
+            hex(ATTACKER_ADDRESS): attacker_account,
+        }
 
         self.laser = svm.LaserEVM(
             self.accounts,

mythril/laser/ethereum/instructions.py

@@ -1842,6 +1842,14 @@ class Instruction:
             callee_address, callee_account, call_data, value, gas, memory_out_offset, memory_out_size = 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")
+                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(
@@ -1859,7 +1867,6 @@ class Instruction:
         )
         if native_result:
             return native_result
-
         transaction = MessageCallTransaction(
             world_state=global_state.world_state,
             gas_price=environment.gasprice,

mythril/laser/ethereum/state/world_state.py

@@ -26,6 +26,7 @@ class WorldState:
         self.node = None  # type: Optional['Node']
         self.transaction_sequence = transaction_sequence or []
         self._annotations = annotations or []
+        self.initial_state_account = {}  # type: Dict
 
     def __getitem__(self, item: str) -> Account:
         """Gets an account from the worldstate using item as key.
@@ -47,6 +48,7 @@ class WorldState:
         )
         new_world_state.accounts = copy(self.accounts)
         new_world_state.node = self.node
+        new_world_state.initial_state_account = self.initial_state_account
         return new_world_state
 
     def create_account(

mythril/laser/ethereum/svm.py

@@ -1,9 +1,9 @@
 """This module implements the main symbolic execution engine."""
 import logging
 from collections import defaultdict
-from copy import copy
+from copy import copy, deepcopy
 from datetime import datetime, timedelta
-from typing import Callable, Dict, DefaultDict, List, Tuple, Union
+from typing import Any, Callable, Dict, DefaultDict, List, Tuple, Union
 
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
 from mythril.laser.ethereum.evm_exceptions import StackUnderflowException
@@ -68,6 +68,8 @@ class LaserEVM:
         """
         world_state = WorldState()
         world_state.accounts = accounts
+        world_state.initial_state_account = self.get_standard_initial_state(accounts)
+
         # this sets the initial world state
         self.world_state = world_state
         self.open_states = [world_state]
@@ -114,6 +116,18 @@ class LaserEVM:
         """
         return self.world_state.accounts
 
+    @staticmethod
+    def get_standard_initial_state(accounts: Dict[str, Account]) -> Dict:
+        template = {"accounts": {}}  # type: Dict[str, Dict[str, Any]]
+        for address, account in accounts.items():
+            template["accounts"][address] = {
+                "nounce": account.nonce,
+                "balance": "<ARBITRARY_BALANCE>",
+                "code": account.code.bytecode,
+                "storage": {},
+            }
+        return template
+
     def sym_exec(
         self, main_address=None, creation_code=None, contract_name=None
     ) -> None: