init transactions

mythril/laser/ethereum/instructions.py

@@ -13,6 +13,7 @@ from mythril.laser.ethereum import util
 from mythril.laser.ethereum.call import get_call_parameters
 from mythril.laser.ethereum.state import GlobalState, MachineState, Environment, CalldataType
 import mythril.laser.ethereum.natives as natives
+from mythril.laser.ethereum.transaction import CallTransaction, TransactionEndSignal, TransactionStartSignal
 
 TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
@@ -35,8 +36,8 @@ def instruction(func):
         for state in new_global_states:
             state.mstate.pc += 1
         return new_global_states
-    return wrapper
 
+    return wrapper
 
 class Instruction:
     """
@@ -47,7 +48,7 @@ class Instruction:
         self.dynamic_loader = dynamic_loader
         self.op_code = op_code
 
-    def evaluate(self, global_state):
+    def evaluate(self, global_state, post=False):
         """ Performs the mutation for this instruction """
         # Generalize some ops
         logging.debug("Evaluating {}".format(self.op_code))
@@ -61,7 +62,7 @@ class Instruction:
         elif self.op_code.startswith("LOG"):
             op = "log"
 
-        instruction_mutator = getattr(self, op + '_', None)
+        instruction_mutator = getattr(self, op + '_', None) if not post else getattr(self, op + '_' + 'post', None)
 
         if instruction_mutator is None:
             raise NotImplementedError
@@ -708,7 +709,8 @@ class Instruction:
 
         try:
             global_state.environment.active_account = deepcopy(global_state.environment.active_account)
-            global_state.accounts[global_state.environment.active_account.address] = global_state.environment.active_account
+            global_state.accounts[
+                global_state.environment.active_account.address] = global_state.environment.active_account
 
             global_state.environment.active_account.storage[index] = value
         except KeyError:
@@ -828,24 +830,15 @@ class Instruction:
 
     @instruction
     def return_(self, global_state):
-        # TODO: memory
         state = global_state.mstate
         offset, length = state.stack.pop(), state.stack.pop()
         try:
-            _ = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)]
+            return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)]
         except AttributeError:
             logging.debug("Return with symbolic length or offset. Not supported")
+            global_state.transaction_stack[-1][0].end(global_state, [BitVec("return_data")])
 
-        return_value = BitVec("retval_" + global_state.environment.active_function_name, 256)
+        global_state.transaction_stack[-1][0].end(global_state, return_data)
-
-        if not global_state.call_stack:
-            return []
-
-        new_global_state = deepcopy(global_state.call_stack.pop())
-        new_global_state.node = global_state.node
-        # TODO: copy memory
-
-        return [new_global_state]
 
     @instruction
     def suicide_(self, global_state):
@@ -865,11 +858,7 @@ class Instruction:
 
     @instruction
     def stop_(self, global_state):
-        if len(global_state.call_stack) is 0:
         return []
-        new_global_state = deepcopy(global_state.call_stack.pop())
-        new_global_state.node = global_state.node
-        return [new_global_state]
 
     @instruction
     def call_(self, global_state):
@@ -877,7 +866,8 @@ class Instruction:
         environment = global_state.environment
 
         try:
-            callee_address, callee_account, call_data, value, call_data_type, gas, memory_out_offset, memory_out_size = get_call_parameters(global_state, self.dynamic_loader, True)
+            callee_address, callee_account, call_data, value, call_data_type, gas, memory_out_offset, memory_out_size = get_call_parameters(
+                global_state, self.dynamic_loader, True)
         except ValueError as e:
             logging.info(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
@@ -907,7 +897,7 @@ class Instruction:
             except natives.NativeContractException:
                 contract_list = ['ecerecover', 'sha256', 'ripemd160', 'identity']
                 for i in range(mem_out_sz):
-                    global_state.mstate.memory[mem_out_start+i] = BitVec(contract_list[call_address_int - 1]+
+                    global_state.mstate.memory[mem_out_start + i] = BitVec(contract_list[call_address_int - 1] +
                                                                            "(" + str(call_data) + ")", 256)
 
                 return [global_state]
@@ -918,19 +908,15 @@ class Instruction:
             # TODO: maybe use BitVec here constrained to 1
             return [global_state]
 
-        callee_environment = Environment(callee_account,
+        transaction = CallTransaction(global_state.accounts,
+                                      callee_account,
                                       BitVecVal(int(environment.active_account.address, 16), 256),
                                       call_data,
                                       environment.gasprice,
                                       value,
                                       environment.origin,
-                                         calldata_type=call_data_type)
+                                      call_data_type)
-        new_global_state = GlobalState(global_state.accounts, callee_environment, global_state.node, MachineState(gas))
+        raise TransactionStartSignal(transaction, self.op_code)
-        new_global_state.call_stack.append(global_state)
-        new_global_state.mstate.pc = -1
-        new_global_state.mstate.depth = global_state.mstate.depth + 1
-        new_global_state.mstate.constraints = copy(global_state.mstate.constraints)
-        return [new_global_state]
 
     @instruction
     def callcode_(self, global_state):
@@ -938,7 +924,8 @@ class Instruction:
         environment = global_state.environment
 
         try:
-            callee_address, callee_account, call_data, value, call_data_type, gas, _, _ = get_call_parameters(global_state, self.dynamic_loader, True)
+            callee_address, callee_account, call_data, value, call_data_type, gas, _, _ = get_call_parameters(
+                global_state, self.dynamic_loader, True)
         except ValueError as e:
             logging.info(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
@@ -968,7 +955,8 @@ class Instruction:
         environment = global_state.environment
 
         try:
-            callee_address, callee_account, call_data, _, call_data_type, gas, _, _ = get_call_parameters(global_state, self.dynamic_loader)
+            callee_address, callee_account, call_data, _, call_data_type, gas, _, _ = get_call_parameters(global_state,
+                                                                                                          self.dynamic_loader)
         except ValueError as e:
             logging.info(
                 "Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
@@ -991,7 +979,6 @@ class Instruction:
 
         return [new_global_state]
 
-
     @instruction
     def staticcall_(self, global_state):
         # TODO: implement me

mythril/laser/ethereum/state.py

@@ -144,22 +144,21 @@ class GlobalState:
     """
     GlobalState represents the current globalstate
     """
-    def __init__(self, accounts, environment, node, machine_state=None, call_stack=None):
+    def __init__(self, accounts, environment, node, machine_state=None, transaction_stack=None):
         """ Constructor for GlobalState"""
         self.node = node
         self.accounts = accounts
         self.environment = environment
         self.mstate = machine_state if machine_state else MachineState(gas=10000000)
-        self.call_stack = call_stack if call_stack else []
+        self.transaction_stack = transaction_stack if transaction_stack else []
         self.op_code = ""
 
-
     def __copy__(self):
         accounts = copy(self.accounts)
         environment = copy(self.environment)
         mstate = deepcopy(self.mstate)
-        call_stack = copy(self.call_stack)
+        transaction_stack = deepcopy(self.transaction_stack)
-        return GlobalState(accounts, environment, self.node, mstate, call_stack=call_stack)
+        return GlobalState(accounts, environment, self.node, mstate, transaction_stack=transaction_stack)
 
     #TODO: remove this, as two instructions are confusing
     def get_current_instruction(self):

mythril/laser/ethereum/svm.py

@@ -1,7 +1,7 @@
 from z3 import BitVec
 import logging
 from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState
-from mythril.laser.ethereum.transaction import MessageCall
+from mythril.laser.ethereum.transaction import MessageCall, TransactionStartSignal, TransactionEndSignal
 from mythril.laser.ethereum.instructions import Instruction
 from mythril.laser.ethereum.cfg import NodeFlags, Node, Edge, JumpType
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
@@ -70,31 +70,34 @@ class LaserEVM:
             try:
                 new_states, op_code = self.execute_state(global_state)
             except NotImplementedError:
-                logging.info("Encountered unimplemented instruction: {}".format(op_code))
+                logging.info("Encountered unimplemented instruction")
                 continue
-
+            except TransactionStartSignal as e:
-            if len(new_states) == 0:
+                new_global_state = transaction.initial_global_state()
-                # TODO: let global state use worldstate
+                new_global_state.transaction_stack.append(e.transaction, global_state)
-                open_world_state = WorldState()
+                new_states, op_code = [e.transaction.initial_global_state()], e.op_code
-                open_world_state.accounts = global_state.accounts
+            except TransactionEndSignal as e:
-                open_world_state.node = global_state.node
+                transaction, return_global_state = e.global_state.transaction_stack.pop()
-                self.open_states.append(open_world_state)
+                if return_global_state is None:
+                    self.open_states.append(e.global_state)
+                    continue
+                new_states, op_code = self.execute_state(return_global_state, post=True)
 
             self.manage_cfg(op_code, new_states)
 
             self.work_list += new_states
             self.total_states += len(new_states)
 
-    def execute_state(self, global_state):
+    def execute_state(self, global_state, post=False):
         instructions = global_state.environment.code.instruction_list
         op_code = instructions[global_state.mstate.pc]['opcode']
 
         # Only count coverage for the main contract
-        if len(global_state.call_stack) == 0:
+        if len(global_state.transaction_stack) == 0:
             self.instructions_covered[global_state.mstate.pc] = True
 
         self._execute_pre_hook(op_code, global_state)
-        new_global_states = Instruction(op_code, self.dynamic_loader).evaluate(global_state)
+        new_global_states = Instruction(op_code, self.dynamic_loader).evaluate(global_state, post)
         self._execute_post_hook(op_code, new_global_states)
 
         return new_global_states, op_code
@@ -189,3 +192,16 @@ class LaserEVM:
             return function
 
         return hook_decorator
+
+    # def start_transaction(self, type, world_state, account, caller,
+    #                       call_data, gas_price, call_value, origin, call_data_type):
+    #     environment = Environment(
+    #         account,
+    #         caller,
+    #         call_data,
+    #         gas_price,
+    #         call_value,
+    #         origin,
+    #         call_data_type,
+    #     )
+    #     new_node = Node(environment.active_account.contract_name)

mythril/laser/ethereum/transaction.py

@@ -5,6 +5,63 @@ from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 from z3 import BitVec
 
 
+class TransactionEndSignal(IndexError):
+    def __init__(self, global_state):
+        self.global_state = global_state
+
+
+class TransactionStartSignal(Exception):
+
+    def __init__(self, transaction, op_code):
+        self.transaction = transaction
+        self.op_code = op_code
+
+
+class CallTransaction:
+    def __init__(self,
+                 world_state,
+                 callee_account,
+                 caller,
+                 call_data=(),
+                 gas_price=BitVec("gasprice", 256),
+                 call_value=BitVec("callvalue", 256),
+                 origin=BitVec("origin", 256),
+                 call_data_type=BitVec("call_data_type", 256)
+                 ):
+        self.world_state = world_state
+        self.callee_account = callee_account
+        self.caller = caller
+        self.call_data = call_data
+        self.gas_price = gas_price
+        self.call_value = call_value
+        self.origin = origin
+        self.call_data_type = call_data_type
+
+        self.return_data = None
+
+    def initial_global_state(self):
+        # Initialize the execution environment
+        environment = Environment(
+            self.callee_account,
+            self.caller,
+            self.call_data,
+            self.gas_price,
+            self.call_value,
+            self.origin,
+            code=self.callee_account.code,
+            calldata_type=self.call_data_type,
+        )
+
+        global_state = GlobalState(self.world_state.accounts, environment, None)
+        global_state.environment.active_function_name = 'fallback'
+
+        return global_state
+
+    def end(self, global_state, return_data=None):
+        self.return_data = return_data
+        raise TransactionEndSignal(global_state)
+
+
 class Transaction:
     def __init__(self):
         self.open_states = None
@@ -40,27 +97,27 @@ class MessageCall(Transaction):
 
         for open_world_state in open_states:
 
-            # Initialize the execution environment
+            transaction = CallTransaction(
-            environment = Environment(
+                open_world_state,
                 open_world_state[self.callee_address],
                 self.caller,
                 [],
                 self.gas_price,
                 self.call_value,
                 self.origin,
-                calldata_type=CalldataType.SYMBOLIC,
+                CalldataType.SYMBOLIC,
             )
-            new_node = Node(environment.active_account.contract_name)
+            global_state = transaction.initial_global_state()
-            evm.instructions_covered = [False for _ in environment.code.instruction_list]
+            global_state.transaction_stack.append((transaction, None))
+
+            new_node = Node(global_state.environment.active_account.contract_name)
+            evm.instructions_covered = [False for _ in global_state.environment.code.instruction_list]
 
             evm.nodes[new_node.uid] = new_node
             if open_world_state.node:
                 evm.edges.append(Edge(open_world_state.node.uid, new_node.uid, edge_type=JumpType.Transaction, condition=None))
-
+            global_state.node = new_node
-            global_state = GlobalState(open_world_state.accounts, environment, new_node)
-            global_state.environment.active_function_name = 'fallback()'
             new_node.states.append(global_state)
-
             evm.work_list.append(global_state)
 
         evm.exec()