mythril.concolic package

Submodules

mythril.concolic.concolic_execution module

mythril.concolic.concolic_execution.concolic_execution(concrete_data: ConcreteData, jump_addresses: List, 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: WorldState, concrete_data: ConcreteData, jump_addresses: List[str], trace: List) → 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: TypedDict

balance: str
code: str
nonce: int
storage: dict
class mythril.concolic.concrete_data.ConcreteData[source]

Bases: TypedDict

initialState: InitialState
steps: List[TransactionData]
class mythril.concolic.concrete_data.InitialState[source]

Bases: TypedDict

accounts: Dict[str, AccountData]
class mythril.concolic.concrete_data.TransactionData[source]

Bases: TypedDict

address: str
blockCoinbase: str
blockDifficulty: str
blockGasLimit: str
blockNumber: str
blockTime: str
calldata: str
gasLimit: str
gasPrice: str
input: str
name: str
origin: str
value: str

mythril.concolic.find_trace module

mythril.concolic.find_trace.concrete_execution(concrete_data: ConcreteData) → Tuple[WorldState, List][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: ConcreteData) → WorldState[source]

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

Module contents