mythril.laser.ethereum.transaction package

Submodules

mythril.laser.ethereum.transaction.concolic module

This module contains functions to set up and execute concolic message calls.

mythril.laser.ethereum.transaction.concolic.execute_contract_creation(laser_evm, callee_address, caller_address, origin_address, data, gas_limit, gas_price, value, code=None, track_gas=False, contract_name=None)

Executes a contract creation transaction concretely.

Parameters:

• laser_evm –
• callee_address –
• caller_address –
• origin_address –
• code –
• data –
• gas_limit –
• gas_price –
• value –
• track_gas –

Returns:

mythril.laser.ethereum.transaction.concolic.execute_message_call(laser_evm, callee_address, caller_address, origin_address, data, gas_limit, gas_price, value, code=None, track_gas=False) → Union[None, List[mythril.laser.ethereum.state.global_state.GlobalState]]

Execute a message call transaction from all open states.

Parameters:

• laser_evm –
• callee_address –
• caller_address –
• origin_address –
• code –
• data –
• gas_limit –
• gas_price –
• value –
• track_gas –

Returns:

mythril.laser.ethereum.transaction.concolic.execute_transaction(*args, **kwargs) → Union[None, List[mythril.laser.ethereum.state.global_state.GlobalState]]

Chooses the transaction type based on callee address and executes the transaction

mythril.laser.ethereum.transaction.symbolic module

This module contains functions setting up and executing transactions with symbolic values.

class mythril.laser.ethereum.transaction.symbolic.Actors(creator=1004753105490295263244812946565948198177742958590, attacker=1271270613000041655817448348132275889066893754095, someguy=974334424887268612135789888477522013103955028650)

Bases: object

attacker

creator

mythril.laser.ethereum.transaction.symbolic.execute_contract_creation(laser_evm, contract_initialization_code, contract_name=None, world_state=None, origin=1004753105490295263244812946565948198177742958590, caller=1004753105490295263244812946565948198177742958590) → mythril.laser.ethereum.state.account.Account

Executes a contract creation transaction from all open states.

Parameters:

• laser_evm –
• contract_initialization_code –
• contract_name –

Returns:

mythril.laser.ethereum.transaction.symbolic.execute_message_call(laser_evm, callee_address: mythril.laser.smt.bitvec.BitVec, func_hashes: List[List[int]] = None) → None

Executes a message call transaction from all open states.

Parameters:

• laser_evm –
• callee_address –

mythril.laser.ethereum.transaction.symbolic.execute_transaction(*args, **kwargs)

Chooses the transaction type based on callee address and executes the transaction

mythril.laser.ethereum.transaction.symbolic.generate_function_constraints(calldata: mythril.laser.ethereum.state.calldata.SymbolicCalldata, func_hashes: List[List[int]]) → List[mythril.laser.smt.bool.Bool]

This will generate constraints for fixing the function call part of calldata :param calldata: Calldata :param func_hashes: The list of function hashes allowed for this transaction :return: Constraints List

mythril.laser.ethereum.transaction.transaction_models module

This module contians the transaction models used throughout LASER’s symbolic execution.

class mythril.laser.ethereum.transaction.transaction_models.BaseTransaction(world_state: mythril.laser.ethereum.state.world_state.WorldState, callee_account: mythril.laser.ethereum.state.account.Account = None, caller: z3.z3.ExprRef = None, call_data=None, identifier: Optional[str] = None, gas_price=None, gas_limit=None, origin=None, code=None, call_value=None, init_call_data=True, static=False, base_fee=None)

Bases: object

Basic transaction class holding common data.

initial_global_state() → mythril.laser.ethereum.state.global_state.GlobalState

initial_global_state_from_environment(environment, active_function)

Parameters:

• environment –
• active_function –

Returns:

class mythril.laser.ethereum.transaction.transaction_models.ContractCreationTransaction(world_state: mythril.laser.ethereum.state.world_state.WorldState, caller: z3.z3.ExprRef = None, call_data=None, identifier: Optional[str] = None, gas_price=None, gas_limit=None, origin=None, code=None, call_value=None, contract_name=None, contract_address=None, base_fee=None)

Bases: mythril.laser.ethereum.transaction.transaction_models.BaseTransaction

Transaction object models an transaction.

end(global_state: mythril.laser.ethereum.state.global_state.GlobalState, return_data=None, revert=False)

Parameters:

• global_state –
• return_data –
• revert –

initial_global_state() → mythril.laser.ethereum.state.global_state.GlobalState

Initialize the execution environment.

class mythril.laser.ethereum.transaction.transaction_models.MessageCallTransaction(*args, **kwargs)

Bases: mythril.laser.ethereum.transaction.transaction_models.BaseTransaction

Transaction object models an transaction.

end(global_state: mythril.laser.ethereum.state.global_state.GlobalState, return_data=None, revert=False) → None

Parameters:

• global_state –
• return_data –
• revert –

initial_global_state() → mythril.laser.ethereum.state.global_state.GlobalState

Initialize the execution environment.

exception mythril.laser.ethereum.transaction.transaction_models.TransactionEndSignal(global_state: mythril.laser.ethereum.state.global_state.GlobalState, revert=False)

Bases: Exception

Exception raised when a transaction is finalized.

exception mythril.laser.ethereum.transaction.transaction_models.TransactionStartSignal(transaction: Union[MessageCallTransaction, ContractCreationTransaction], op_code: str, global_state: mythril.laser.ethereum.state.global_state.GlobalState)

Bases: Exception

Exception raised when a new transaction is started.

class mythril.laser.ethereum.transaction.transaction_models.TxIdManager

Bases: object

get_next_tx_id()

restart_counter()

Module contents