mythril.laser.ethereum.strategy package

Subpackages

• mythril.laser.ethereum.strategy.extensions package
  • Submodules
  • mythril.laser.ethereum.strategy.extensions.bounded_loops module
  • Module contents

Submodules

mythril.laser.ethereum.strategy.basic module

This module implements basic symbolic execution search strategies.

class mythril.laser.ethereum.strategy.basic.BreadthFirstSearchStrategy(work_list, max_depth, **kwargs)

Bases: mythril.laser.ethereum.strategy.BasicSearchStrategy

Implements a breadth first search strategy I.E.

Execute all states of a “level” before continuing

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

Returns:

class mythril.laser.ethereum.strategy.basic.DepthFirstSearchStrategy(work_list, max_depth, **kwargs)

Bases: mythril.laser.ethereum.strategy.BasicSearchStrategy

Implements a depth first search strategy I.E.

Follow one path to a leaf, and then continue to the next one

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

Returns:

class mythril.laser.ethereum.strategy.basic.ReturnRandomNaivelyStrategy(work_list, max_depth, **kwargs)

Bases: mythril.laser.ethereum.strategy.BasicSearchStrategy

chooses a random state from the worklist with equal likelihood.

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

Returns:

class mythril.laser.ethereum.strategy.basic.ReturnWeightedRandomStrategy(work_list, max_depth, **kwargs)

Bases: mythril.laser.ethereum.strategy.BasicSearchStrategy

chooses a random state from the worklist with likelihood based on inverse proportion to depth.

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

Returns:

mythril.laser.ethereum.strategy.beam module

class mythril.laser.ethereum.strategy.beam.BeamSearch(work_list, max_depth, beam_width, **kwargs)

Bases: mythril.laser.ethereum.strategy.BasicSearchStrategy

chooses a random state from the worklist with equal likelihood.

static beam_priority(state)

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

Returns:

sort_and_eliminate_states()

mythril.laser.ethereum.strategy.concolic module

class mythril.laser.ethereum.strategy.concolic.ConcolicStrategy(work_list: List[mythril.laser.ethereum.state.global_state.GlobalState], max_depth: int, trace: List[List[Tuple[int, str]]], flip_branch_addresses: List[str])

Bases: mythril.laser.ethereum.strategy.CriterionSearchStrategy

Executes program concolically using the input trace till a specific branch

check_completion_criterion()

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

This function does the following:- 1) Choose the states by following the concolic trace. 2) In case we have an executed JUMPI that is in flip_branch_addresses, flip that branch. :return:

class mythril.laser.ethereum.strategy.concolic.TraceAnnotation(trace=None)

Bases: mythril.laser.ethereum.state.annotation.StateAnnotation

This is the annotation used by the ConcolicStrategy to store concolic traces.

persist_over_calls

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

The default is set to False

Module contents

class mythril.laser.ethereum.strategy.BasicSearchStrategy(work_list, max_depth, **kwargs)

Bases: abc.ABC

A basic search strategy which halts based on depth

get_strategic_global_state()

class mythril.laser.ethereum.strategy.CriterionSearchStrategy(work_list, max_depth, **kwargs)

Bases: mythril.laser.ethereum.strategy.BasicSearchStrategy

If a criterion is satisfied, the search halts

get_strategic_global_state()

set_criterion_satisfied()