Add transaction ids

mythril/laser/ethereum/transaction/symbolic.py

@@ -1,25 +1,30 @@
-from z3 import BitVec
+from z3 import BitVec, Extract, Not
 
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 from mythril.laser.ethereum.state import CalldataType
 from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction
 
+next_transaction_id = 0
+
 
 def execute_message_call(laser_evm, callee_address):
     """ Executes a message call transaction from all open states """
+    global next_transaction_id
     open_states = laser_evm.open_states[:]
     del laser_evm.open_states[:]
 
     for open_world_state in open_states:
+        next_transaction_id += 1
         transaction = MessageCallTransaction(
+            next_transaction_id,
             open_world_state,
             open_world_state[callee_address],
-            BitVec("caller", 256),
+            BitVec("caller{}".format(next_transaction_id), 256),
             [],
-            BitVec("gas_price", 256),
+            BitVec("gas_price{}".format(next_transaction_id), 256),
-            BitVec("call_value", 256),
+            BitVec("call_value{}".format(next_transaction_id), 256),
-            BitVec("origin", 256),
+            BitVec("origin{}".format(next_transaction_id), 256),
             CalldataType.SYMBOLIC,
         )
         _setup_global_state_for_execution(laser_evm, transaction)
@@ -29,6 +34,7 @@ def execute_message_call(laser_evm, callee_address):
 
 def execute_contract_creation(laser_evm, contract_initialization_code, contract_name=None):
     """ Executes a contract creation transaction from all open states"""
+    global next_transaction_id
     open_states = laser_evm.open_states[:]
     del laser_evm.open_states[:]
 
@@ -37,18 +43,19 @@ def execute_contract_creation(laser_evm, contract_initialization_code, contract_
         new_account.contract_name = contract_name
 
     for open_world_state in open_states:
+        next_transaction_id += 1
         transaction = ContractCreationTransaction(
+            next_transaction_id,
             open_world_state,
-            BitVec("creator", 256),
+            BitVec("creator{}".format(next_transaction_id), 256),
             new_account,
             Disassembly(contract_initialization_code),
             [],
-            BitVec("gas_price", 256),
+            BitVec("gas_price{}".format(next_transaction_id), 256),
-            BitVec("call_value", 256),
+            BitVec("call_value{}".format(next_transaction_id), 256),
-            BitVec("origin", 256),
+            BitVec("origin{}".format(next_transaction_id), 256),
             CalldataType.SYMBOLIC
         )
-
         _setup_global_state_for_execution(laser_evm, transaction)
     laser_evm.exec(True)
 

mythril/laser/ethereum/transaction/transaction_models.py

@@ -21,25 +21,27 @@ class TransactionStartSignal(Exception):
 class MessageCallTransaction:
     """ Transaction object models an transaction"""
     def __init__(self,
+                 identifier,
                  world_state,
                  callee_account,
                  caller,
                  call_data=(),
-                 gas_price=BitVec("gasprice", 256),
+                 gas_price=None,
-                 call_value=BitVec("callvalue", 256),
+                 call_value=None,
-                 origin=BitVec("origin", 256),
+                 origin=None,
-                 call_data_type=BitVec("call_data_type", 256),
+                 call_data_type=None,
                  code=None
                  ):
         assert isinstance(world_state, WorldState)
+        self.id = identifier
         self.world_state = world_state
         self.callee_account = callee_account
         self.caller = caller
         self.call_data = call_data
-        self.gas_price = gas_price
+        self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price
-        self.call_value = call_value
+        self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value
-        self.origin = origin
+        self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin
-        self.call_data_type = call_data_type
+        self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type
         self.code = code
         self.return_data = None
 
@@ -69,29 +71,32 @@ class MessageCallTransaction:
 class ContractCreationTransaction:
     """ Transaction object models an transaction"""
     def __init__(self,
+                 identifier,
                  world_state,
                  caller,
                  callee_account=None,
                  code=None,
                  call_data=(),
-                 gas_price=BitVec("gasprice", 256),
+                 gas_price=None,
-                 call_value=BitVec("callvalue", 256),
+                 call_value=None,
-                 origin=BitVec("origin", 256),
+                 origin=None,
-                 call_data_type=BitVec("call_data_type", 256),
+                 call_data_type=None,
                  ):
         assert isinstance(world_state, WorldState)
-
+        self.id = identifier
         self.world_state = world_state
         # TODO: set correct balance for new account
         self.callee_account = callee_account if callee_account else world_state.create_account(0, concrete_storage=True)
 
         self.caller = caller
-        self.call_data = call_data
-        self.gas_price = gas_price
-        self.call_value = call_value
 
+        self.gas_price = BitVec("gasprice{}".format(identifier), 256) if gas_price is None else gas_price
+        self.call_value = BitVec("callvalue{}".format(identifier), 256) if call_value is None else call_value
+        self.origin = BitVec("origin{}".format(identifier), 256) if origin is None else origin
+        self.call_data_type = BitVec("call_data_type{}".format(identifier), 256) if call_data_type is None else call_data_type
+
+        self.call_data = call_data
         self.origin = origin
-        self.call_data_type = call_data_type
         self.code = code
         self.return_data = None