mythril/laser/ethereum/transaction: use symbol factory

mythril/laser/ethereum/transaction/concolic.py

@@ -1,17 +1,13 @@
 from typing import List, Union
+
+from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.ethereum.cfg import Node, Edge, JumpType
+from mythril.laser.ethereum.state.calldata import CalldataType, ConcreteCalldata
+from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction.transaction_models import (
     MessageCallTransaction,
-    ContractCreationTransaction,
     get_next_transaction_id,
 )
-from z3 import BitVec
-from mythril.laser.ethereum.state.environment import Environment
-from mythril.laser.ethereum.state.calldata import CalldataType, ConcreteCalldata
-from mythril.laser.ethereum.state.account import Account
-from mythril.laser.ethereum.state.world_state import WorldState
-from mythril.laser.ethereum.state.global_state import GlobalState
-from mythril.disassembler.disassembly import Disassembly
-from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 
 
 def execute_message_call(

mythril/laser/ethereum/transaction/symbolic.py

@@ -1,21 +1,20 @@
-from z3 import BitVec, BitVecVal
 from logging import debug
 
+
+from mythril.laser.smt import symbol_factory
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
+from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.calldata import (
     CalldataType,
-    BaseCalldata,
     SymbolicCalldata,
 )
-from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.transaction.transaction_models import (
     MessageCallTransaction,
     ContractCreationTransaction,
     get_next_transaction_id,
 )
 
-
 CREATOR_ADDRESS = 0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE
 ATTACKER_ADDRESS = 0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF
 
@@ -35,14 +34,14 @@ def execute_message_call(laser_evm, callee_address: str) -> None:
         transaction = MessageCallTransaction(
             world_state=open_world_state,
             identifier=next_transaction_id,
-            gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
+            gas_price=symbol_factory.BitVecSym("gas_price{}".format(next_transaction_id), 256),
             gas_limit=8000000,  # block gas limit
-            origin=BitVec("origin{}".format(next_transaction_id), 256),
-            caller=BitVecVal(ATTACKER_ADDRESS, 256),
+            origin=symbol_factory.BitVecSym("origin{}".format(next_transaction_id), 256),
+            caller=symbol_factory.BitVecVal(ATTACKER_ADDRESS, 256),
             callee_account=open_world_state[callee_address],
             call_data=SymbolicCalldata(next_transaction_id),
             call_data_type=CalldataType.SYMBOLIC,
-            call_value=BitVec("call_value{}".format(next_transaction_id), 256),
+            call_value=symbol_factory.BitVecSym("call_value{}".format(next_transaction_id), 256),
         )
         _setup_global_state_for_execution(laser_evm, transaction)
 
@@ -68,15 +67,15 @@ def execute_contract_creation(
         transaction = ContractCreationTransaction(
             world_state=open_world_state,
             identifier=next_transaction_id,
-            gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
+            gas_price=symbol_factory.BitVecSym("gas_price{}".format(next_transaction_id), 256),
             gas_limit=8000000,  # block gas limit
-            origin=BitVec("origin{}".format(next_transaction_id), 256),
+            origin=symbol_factory.BitVecSym("origin{}".format(next_transaction_id), 256),
             code=Disassembly(contract_initialization_code),
-            caller=BitVecVal(CREATOR_ADDRESS, 256),
+            caller=symbol_factory.BitVecVal(CREATOR_ADDRESS, 256),
             callee_account=new_account,
             call_data=[],
             call_data_type=CalldataType.SYMBOLIC,
-            call_value=BitVec("call_value{}".format(next_transaction_id), 256),
+            call_value=symbol_factory.BitVecSym("call_value{}".format(next_transaction_id), 256),
         )
         _setup_global_state_for_execution(laser_evm, transaction)
     laser_evm.exec(True)

mythril/laser/ethereum/transaction/transaction_models.py

@@ -1,6 +1,8 @@
 import logging
 from typing import Union
 from mythril.disassembler.disassembly import Disassembly
+from mythril.laser.smt import symbol_factory
+
 from mythril.laser.ethereum.state.environment import Environment
 from mythril.laser.ethereum.state.calldata import (
     BaseCalldata,
@@ -10,7 +12,7 @@ from mythril.laser.ethereum.state.calldata import (
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.state.global_state import GlobalState
-from z3 import BitVec, ExprRef
+from z3 import ExprRef
 import array
 
 _next_transaction_id = 0
@@ -67,12 +69,12 @@ class BaseTransaction:
         self.gas_price = (
             gas_price
             if gas_price is not None
-            else BitVec("gasprice{}".format(identifier), 256)
+            else symbol_factory.BitVecSym("gasprice{}".format(identifier), 256)
         )
         self.gas_limit = gas_limit
 
         self.origin = (
-            origin if origin is not None else BitVec("origin{}".format(identifier), 256)
+            origin if origin is not None else symbol_factory.BitVecSym("origin{}".format(identifier), 256)
         )
         self.code = code
 
@@ -86,12 +88,12 @@ class BaseTransaction:
         self.call_data_type = (
             call_data_type
             if call_data_type is not None
-            else BitVec("call_data_type{}".format(identifier), 256)
+            else symbol_factory.BitVecSym("call_data_type{}".format(identifier), 256)
         )
         self.call_value = (
             call_value
             if call_value is not None
-            else BitVec("callvalue{}".format(identifier), 256)
+            else symbol_factory.BitVecSym("callvalue{}".format(identifier), 256)
         )
 
         self.return_data = None