From ae28fd0d52fbc392651d65a4e871856ee6725708 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 10 Dec 2018 16:18:35 +0100 Subject: [PATCH] mythril/laser/ethereum/transaction: use symbol factory --- .../laser/ethereum/transaction/concolic.py | 14 ++++------- .../laser/ethereum/transaction/symbolic.py | 23 +++++++++---------- .../transaction/transaction_models.py | 12 ++++++---- 3 files changed, 23 insertions(+), 26 deletions(-) diff --git a/mythril/laser/ethereum/transaction/concolic.py b/mythril/laser/ethereum/transaction/concolic.py index 6c7a406d..27c9de1a 100644 --- a/mythril/laser/ethereum/transaction/concolic.py +++ b/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( diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 55593005..3e0c8102 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/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) diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index 35861290..2600db3d 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/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