mythril.laser.ethereum.state package

Submodules

mythril.laser.ethereum.state.account module

This module contains account-related functionality.

This includes classes representing accounts and their storage.

class mythril.laser.ethereum.state.account.Account(address: BitVec | str, code=None, contract_name=None, balances: Array | None = None, concrete_storage=False, dynamic_loader=None, nonce=0)

Bases: object

Account class representing ethereum accounts.

add_balance(balance: int | BitVec) → None

Parameters:

balance

property as_dict: Dict

Returns:

serialised_code()

set_balance(balance: int | BitVec) → None

Parameters:

balance

set_storage(storage: Dict)

Sets concrete storage

class mythril.laser.ethereum.state.account.Storage(concrete=False, address=None, dynamic_loader=None)

Bases: object

Storage class represents the storage of an Account.

mythril.laser.ethereum.state.annotation module

This module includes classes used for annotating trace information.

This includes the base StateAnnotation class, as well as an adaption, which will not be copied on every new state.

class mythril.laser.ethereum.state.annotation.MergeableStateAnnotation

Bases: StateAnnotation

This class allows a base annotation class for annotations that can be merged.

abstract check_merge_annotation(annotation) → bool

abstract merge_annotation(annotation)

class mythril.laser.ethereum.state.annotation.NoCopyAnnotation

Bases: StateAnnotation

This class provides a base annotation class for annotations that shouldn’t be copied on every new state.

Rather the same object should be propagated. This is very useful if you are looking to analyze a property over multiple substates

class mythril.laser.ethereum.state.annotation.StateAnnotation

Bases: object

The StateAnnotation class is used to persist information over traces.

This allows modules to reason about traces without the need to traverse the state space themselves.

property persist_over_calls: bool

If this function returns true then laser will propagate the annotation between calls

The default is set to False

property persist_to_world_state: bool

If this function returns true then laser will also annotate the world state.

If you want annotations to persist through different user initiated message call transactions then this should be enabled.

The default is set to False

property search_importance: int

Used in estimating the priority of a state annotated with the corresponding annotation. Default is 1

mythril.laser.ethereum.state.calldata module

This module declares classes to represent call data.

class mythril.laser.ethereum.state.calldata.BaseCalldata(tx_id: str)

Bases: object

Base calldata class This represents the calldata provided when sending a transaction to a contract.

property calldatasize: BitVec

Returns:

Calldata size for this calldata object

concrete(model: Model) → list

Returns a concrete version of the calldata using the provided model.

Parameters:

model

get_word_at(offset: int) → Expression

Gets word at offset.

Parameters:

offset

Returns:

property size: BitVec | int

Returns the exact size of this calldata, this is not normalized.

Returns:

unnormalized call data size

class mythril.laser.ethereum.state.calldata.BasicConcreteCalldata(tx_id: str, calldata: list)

Bases: BaseCalldata

A base class to represent concrete call data.

concrete(model: Model) → list

Parameters:

model

Returns:

property size: int

Returns:

class mythril.laser.ethereum.state.calldata.BasicSymbolicCalldata(tx_id: str)

Bases: BaseCalldata

A basic class representing symbolic call data.

concrete(model: Model) → list

Parameters:

model

Returns:

property size: BitVec

Returns:

class mythril.laser.ethereum.state.calldata.ConcreteCalldata(tx_id: str, calldata: list)

Bases: BaseCalldata

A concrete call data representation.

concrete(model: Model) → list

Parameters:

model

Returns:

property size: int

Returns:

class mythril.laser.ethereum.state.calldata.SymbolicCalldata(tx_id: str)

Bases: BaseCalldata

A class for representing symbolic call data.

concrete(model: Model) → list

Parameters:

model

Returns:

property size: BitVec

Returns:

mythril.laser.ethereum.state.constraints module

This module contains the class used to represent state-change constraints in the call graph.

class mythril.laser.ethereum.state.constraints.Constraints(constraint_list: List[Bool] | None = None)

Bases: list

This class should maintain a solver and it’s constraints, This class tries to make the Constraints() object as a simple list of constraints with some background processing.

append(constraint: bool | Bool) → None

Parameters:

constraint – The constraint to be appended

property as_list: List[Bool]

Returns:

returns the list of constraints

copy() → Constraints

Return a shallow copy of the list.

get_all_constraints()

get_model(solver_timeout=None) → bool

Parameters:

solver_timeout – The default timeout uses analysis timeout from args.solver_timeout

Returns:

True/False based on the existence of solution of constraints

is_possible(solver_timeout=None) → bool

Parameters:

solver_timeout – The default timeout uses analysis timeout from args.solver_timeout

Returns:

True/False based on the existence of solution of constraints

mythril.laser.ethereum.state.environment module

This module contains the representation for an execution state’s environment.

class mythril.laser.ethereum.state.environment.Environment(active_account: Account, sender: ExprRef, calldata: BaseCalldata, gasprice: ExprRef, callvalue: ExprRef, origin: ExprRef, basefee: ExprRef, code=None, static=False)

Bases: object

The environment class represents the current execution environment for the symbolic executor.

property as_dict: Dict

Returns:

mythril.laser.ethereum.state.global_state module

This module contains a representation of the global execution state.

class mythril.laser.ethereum.state.global_state.GlobalState(world_state: WorldState, environment: Environment, node: Node, machine_state=None, transaction_stack=None, last_return_data=None, annotations=None)

Bases: object

GlobalState represents the current globalstate.

property accounts: Dict

Returns:

add_annotations(annotations: List[StateAnnotation])

Function used to add annotations to global state :param annotations: :return:

annotate(annotation: StateAnnotation) → None

Parameters:

annotation

property annotations: List[StateAnnotation]

Returns:

property current_transaction: MessageCallTransaction | ContractCreationTransaction | None

Returns:

get_annotations(annotation_type: type) → Iterable[StateAnnotation]

Filters annotations for the queried annotation type. Designed particularly for modules with annotations: globalstate.get_annotations(MySpecificModuleAnnotation)

Parameters:

annotation_type – The type to filter annotations for

Returns:

filter of matching annotations

get_current_instruction() → Dict

Gets the current instruction for this GlobalState.

Returns:

property instruction: Dict

Returns:

new_bitvec(name: str, size=256, annotations=None) → BitVec

Parameters:

• name

• size

Returns:

mythril.laser.ethereum.state.machine_state module

This module contains a representation of the EVM’s machine state and its stack.

class mythril.laser.ethereum.state.machine_state.MachineStack(default_list=None)

Bases: list

Defines EVM stack, overrides the default list to handle overflows.

STACK_LIMIT = 1024

append(element: int | Expression) → None

This function ensures the following properties when appending to a list:

• Element appended to this list should be a BitVec

• Ensures stack overflow bound

Parameters:

element – element to be appended to the list

Function:

appends the element to list if the size is less than STACK_LIMIT, else throws an error

pop(index=-1) → int | Expression

This function ensures stack underflow bound :param index:index to be popped, same as the list() class. :returns popped value :function: same as list() class but throws StackUnderflowException for popping from an empty list

class mythril.laser.ethereum.state.machine_state.MachineState(gas_limit: int, pc=0, stack=None, subroutine_stack=None, memory: Memory | None = None, constraints=None, depth=0, max_gas_used=0, min_gas_used=0)

Bases: object

MachineState represents current machine state also referenced to as mu.

property as_dict: Dict

Returns:

calculate_extension_size(start: int, size: int) → int

Parameters:

• start

• size

Returns:

calculate_memory_gas(start: int, size: int)

Parameters:

• start

• size

Returns:

check_gas()

Check whether the machine is out of gas.

mem_extend(start: int | BitVec, size: int | BitVec) → None

Extends the memory of this machine state.

Parameters:

• start – Start of memory extension

• size – Size of memory extension

property memory_size: int

Returns:

memory_write(offset: int, data: List[int | BitVec]) → None

Writes data to memory starting at offset.

Parameters:

• offset

• data

pop(amount=1) → BitVec | List[BitVec]

Pops amount elements from the stack.

Parameters:

amount

Returns:

mythril.laser.ethereum.state.memory module

This module contains a representation of a smart contract’s memory.

class mythril.laser.ethereum.state.memory.Memory

Bases: object

A class representing contract memory with random access.

extend(size: int)

Parameters:

size

get_word_at(index: int) → int | BitVec

Access a word from a specified memory index.

Parameters:

index – integer representing the index to access

Returns:

32 byte word at the specified index

write_word_at(index: int, value: int | BitVec | bool | Bool) → None

Writes a 32 byte word to memory at the specified index`

Parameters:

• index – index to write to

• value – the value to write to memory

mythril.laser.ethereum.state.memory.convert_bv(val: int | BitVec) → BitVec

mythril.laser.ethereum.state.return_data module

This module declares classes to represent call data.

class mythril.laser.ethereum.state.return_data.ReturnData(return_data: List[BitVec], return_data_size: BitVec)

Bases: object

Base returndata class.

property size: BitVec

Returns:

Calldata size for this calldata object

mythril.laser.ethereum.state.world_state module

This module contains a representation of the EVM’s world state.

class mythril.laser.ethereum.state.world_state.WorldState(transaction_sequence=None, annotations: List[StateAnnotation] | None = None, constraints: Constraints | None = None)

Bases: object

The WorldState class represents the world state as described in the yellow paper.

property accounts

accounts_exist_or_load(addr, dynamic_loader: DynLoader) → Account

returns account if it exists, else it loads from the dynamic loader :param addr: address :param dynamic_loader: Dynamic Loader :return: The code

annotate(annotation: StateAnnotation) → None

Parameters:

annotation

property annotations: List[StateAnnotation]

Returns:

create_account(balance=0, address=None, concrete_storage=False, dynamic_loader=None, creator=None, code=None, nonce=0) → Account

Create non-contract account.

Parameters:

• address – The account’s address

• balance – Initial balance for the account

• concrete_storage – Interpret account storage as concrete

• dynamic_loader – used for dynamically loading storage from the block chain

• creator – The address of the creator of the contract if it’s a contract

• code – The code of the contract, if it’s a contract

• nonce – Nonce of the account

Returns:

The new account

create_initialized_contract_account(contract_code, storage) → None

Creates a new contract account, based on the contract code and storage provided The contract code only includes the runtime contract bytecode.

Parameters:

• contract_code – Runtime bytecode for the contract

• storage – Initial storage for the contract

Returns:

The new account

get_annotations(annotation_type: type) → Iterator[StateAnnotation]

Filters annotations for the queried annotation type. Designed particularly for modules with annotations: worldstate.get_annotations(MySpecificModuleAnnotation)

Parameters:

annotation_type – The type to filter annotations for

Returns:

filter of matching annotations

put_account(account: Account) → None

Parameters:

account

Module contents