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: Union[mythril.laser.smt.bitvec.BitVec, str], code=None, contract_name=None, balances: mythril.laser.smt.array.Array = None, concrete_storage=False, dynamic_loader=None, nonce=0)

Bases: object

Account class representing ethereum accounts.

add_balance(balance: Union[int, mythril.laser.smt.bitvec.BitVec]) → None

Parameters:balance –

as_dict

Returns:

serialised_code()

set_balance(balance: Union[int, mythril.laser.smt.bitvec.BitVec]) → None

Parameters:balance –

set_storage(storage: Dict[KT, VT])

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: mythril.laser.ethereum.state.annotation.StateAnnotation

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

check_merge_annotation(annotation) → bool

merge_annotation(annotation)

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

Bases: mythril.laser.ethereum.state.annotation.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.

persist_over_calls

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

The default is set to False

persist_to_world_state

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

search_importance

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.

calldatasize

Returns:Calldata size for this calldata object

concrete(model: z3.z3.Model) → list

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

Parameters:model –

get_word_at(offset: int) → mythril.laser.smt.expression.Expression

Gets word at offset.

Parameters:offset – Returns:

size

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: mythril.laser.ethereum.state.calldata.BaseCalldata

A base class to represent concrete call data.

concrete(model: z3.z3.Model) → list

Parameters:model – Returns:

size

Returns:

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

Bases: mythril.laser.ethereum.state.calldata.BaseCalldata

A basic class representing symbolic call data.

concrete(model: z3.z3.Model) → list

Parameters:model – Returns:

size

Returns:

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

Bases: mythril.laser.ethereum.state.calldata.BaseCalldata

A concrete call data representation.

concrete(model: z3.z3.Model) → list

Parameters:model – Returns:

size

Returns:

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

Bases: mythril.laser.ethereum.state.calldata.BaseCalldata

A class for representing symbolic call data.

concrete(model: z3.z3.Model) → list

Parameters:model – Returns:

size

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: Optional[List[mythril.laser.smt.bool.Bool]] = 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: Union[bool, mythril.laser.smt.bool.Bool]) → None

Parameters:constraint – The constraint to be appended

as_list

Returns:returns the list of constraints

copy() → mythril.laser.ethereum.state.constraints.Constraints

Return a shallow copy of the list.

get_all_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: mythril.laser.ethereum.state.account.Account, sender: z3.z3.ExprRef, calldata: mythril.laser.ethereum.state.calldata.BaseCalldata, gasprice: z3.z3.ExprRef, callvalue: z3.z3.ExprRef, origin: z3.z3.ExprRef, basefee: z3.z3.ExprRef, code=None, static=False)

Bases: object

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

as_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: mythril.laser.ethereum.state.environment.Environment, node: mythril.laser.ethereum.cfg.Node, machine_state=None, transaction_stack=None, last_return_data=None, annotations=None)

Bases: object

GlobalState represents the current globalstate.

accounts

Returns:

add_annotations(annotations: List[mythril.laser.ethereum.state.annotation.StateAnnotation])

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

annotate(annotation: mythril.laser.ethereum.state.annotation.StateAnnotation) → None

Parameters:annotation –

annotations

Returns:

current_transaction

Returns:

get_annotations(annotation_type: type) → Iterable[mythril.laser.ethereum.state.annotation.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[KT, VT]

Gets the current instruction for this GlobalState.

Returns:

instruction

Returns:

new_bitvec(name: str, size=256, annotations=None) → z3.z3.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: Union[int, mythril.laser.smt.expression.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) → Union[int, mythril.laser.smt.expression.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: Optional[mythril.laser.ethereum.state.memory.Memory] = 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.

as_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: Union[int, mythril.laser.smt.bitvec.BitVec], size: Union[int, mythril.laser.smt.bitvec.BitVec]) → None

Extends the memory of this machine state.

Parameters:

• start – Start of memory extension
• size – Size of memory extension

memory_size

Returns:

memory_write(offset: int, data: List[Union[int, mythril.laser.smt.bitvec.BitVec]]) → None

Writes data to memory starting at offset.

Parameters:

• offset –
• data –

pop(amount=1) → Union[mythril.laser.smt.bitvec.BitVec, List[mythril.laser.smt.bitvec.BitVec]]

Pops amount elements from the stack.

Parameters:amount – Returns:

mythril.laser.ethereum.state.machine_state.ceil32(value: int, *, ceiling: int = 32) → int

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) → Union[int, mythril.laser.smt.bitvec.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: Union[int, mythril.laser.smt.bitvec.BitVec, bool, mythril.laser.smt.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: Union[int, mythril.laser.smt.bitvec.BitVec]) → mythril.laser.smt.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[mythril.laser.smt.bitvec.BitVec], return_data_size: mythril.laser.smt.bitvec.BitVec)

Bases: object

Base returndata class.

size

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[mythril.laser.ethereum.state.annotation.StateAnnotation] = None, constraints: mythril.laser.ethereum.state.constraints.Constraints = None)

Bases: object

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

accounts

accounts_exist_or_load(addr, dynamic_loader: mythril.support.loader.DynLoader) → mythril.laser.ethereum.state.account.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: mythril.laser.ethereum.state.annotation.StateAnnotation) → None

Parameters:annotation –

annotations

Returns:

create_account(balance=0, address=None, concrete_storage=False, dynamic_loader=None, creator=None, code=None, nonce=0) → mythril.laser.ethereum.state.account.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[mythril.laser.ethereum.state.annotation.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: mythril.laser.ethereum.state.account.Account) → None

Parameters:account –

Module contents