mythril.concolic package

Submodules

mythril.concolic.concolic_execution module

mythril.concolic.concolic_execution.concolic_execution(concrete_data: mythril.concolic.concrete_data.ConcreteData, jump_addresses: List[T], solver_timeout=100000) → List[Dict[str, Dict[str, Any]]][source]

Executes codes and prints input required to cover the branch flips :param input_file: Input file :param jump_addresses: Jump addresses to flip :param solver_timeout: Solver timeout

mythril.concolic.concolic_execution.flip_branches(init_state: mythril.laser.ethereum.state.world_state.WorldState, concrete_data: mythril.concolic.concrete_data.ConcreteData, jump_addresses: List[str], trace: List[T]) → List[Dict[str, Dict[str, Any]]][source]

Flips branches and prints the input required for branch flip

Parameters:
  • concrete_data – Concrete data
  • jump_addresses – Jump addresses to flip
  • trace – trace to follow

mythril.concolic.concrete_data module

class mythril.concolic.concrete_data.AccountData[source]

Bases: dict

class mythril.concolic.concrete_data.ConcreteData[source]

Bases: dict

class mythril.concolic.concrete_data.InitialState[source]

Bases: dict

class mythril.concolic.concrete_data.TransactionData[source]

Bases: dict

mythril.concolic.find_trace module

mythril.concolic.find_trace.concrete_execution(concrete_data: mythril.concolic.concrete_data.ConcreteData) → Tuple[mythril.laser.ethereum.state.world_state.WorldState, List[T]][source]

Executes code concretely to find the path to be followed by concolic executor :param concrete_data: Concrete data :return: path trace

mythril.concolic.find_trace.setup_concrete_initial_state(concrete_data: mythril.concolic.concrete_data.ConcreteData) → mythril.laser.ethereum.state.world_state.WorldState[source]

Sets up concrete initial state :param concrete_data: Concrete data :return: initialised world state

Module contents