mythril.laser.plugin.plugins package

Subpackages

• mythril.laser.plugin.plugins.coverage package
  • Submodules
  • mythril.laser.plugin.plugins.coverage.coverage_plugin module
    • CoveragePluginBuilder
      • CoveragePluginBuilder.name
    • InstructionCoveragePlugin
      • InstructionCoveragePlugin.initialize()
      • InstructionCoveragePlugin.is_instruction_covered()
  • mythril.laser.plugin.plugins.coverage.coverage_strategy module
    • CoverageStrategy
      • CoverageStrategy.get_strategic_global_state()
  • Module contents
• mythril.laser.plugin.plugins.summary_backup package
  • Module contents

Submodules

mythril.laser.plugin.plugins.benchmark module

class mythril.laser.plugin.plugins.benchmark.BenchmarkPlugin(name=None)

Bases: LaserPlugin

Benchmark Plugin

This plugin aggregates the following information: - duration - code coverage over time - final code coverage - total number of executed instructions

initialize(symbolic_vm: LaserEVM)

Initializes the BenchmarkPlugin

Introduces hooks in symbolic_vm to track the desired values :param symbolic_vm: Symbolic virtual machine to analyze

class mythril.laser.plugin.plugins.benchmark.BenchmarkPluginBuilder

Bases: PluginBuilder

name = 'benchmark'

mythril.laser.plugin.plugins.call_depth_limiter module

class mythril.laser.plugin.plugins.call_depth_limiter.CallDepthLimit(call_depth_limit: int)

Bases: LaserPlugin

initialize(symbolic_vm: LaserEVM)

Initializes the mutation pruner

Introduces hooks for SSTORE operations :param symbolic_vm: :return:

class mythril.laser.plugin.plugins.call_depth_limiter.CallDepthLimitBuilder

Bases: PluginBuilder

name = 'call-depth-limit'

mythril.laser.plugin.plugins.dependency_pruner module

class mythril.laser.plugin.plugins.dependency_pruner.DependencyPruner

Bases: LaserPlugin

Dependency Pruner Plugin

For every basic block, this plugin keeps a list of storage locations that are accessed (read) in the execution path containing that block. This map is built up over the whole symbolic execution run.

After the initial build up of the map in the first transaction, blocks are executed only if any of the storage locations written to in the previous transaction can have an effect on that block or any of its successors.

initialize(symbolic_vm: LaserEVM) → None

Initializes the DependencyPruner

:param symbolic_vm

update_calls(path: List[int]) → None

Update the dependency map for the block offsets on the given path.

:param path :param target_location

update_sloads(path: List[int], target_location: object) → None

Update the dependency map for the block offsets on the given path.

:param path :param target_location

update_sstores(path: List[int], target_location: object) → None

Update the dependency map for the block offsets on the given path.

:param path :param target_location

wanna_execute(address: int, annotation: DependencyAnnotation) → bool

Decide whether the basic block starting at ‘address’ should be executed.

:param address :param storage_write_cache

class mythril.laser.plugin.plugins.dependency_pruner.DependencyPrunerBuilder

Bases: PluginBuilder

name = 'dependency-pruner'

mythril.laser.plugin.plugins.dependency_pruner.get_dependency_annotation(state: GlobalState) → DependencyAnnotation

Returns a dependency annotation

Parameters:

state – A global state object

mythril.laser.plugin.plugins.dependency_pruner.get_ftn_seq_annotation_from_ws(state: WorldState) → list

Returns the global state annotation

Parameters:

state – A world state object

mythril.laser.plugin.plugins.dependency_pruner.get_writes_annotation_from_ws(state: WorldState) → list

Returns the global state annotation

Parameters:

state – A world state object

mythril.laser.plugin.plugins.dependency_pruner.get_ws_dependency_annotation(state: GlobalState) → WSDependencyAnnotation

Returns the world state annotation

Parameters:

state – A global state object

mythril.laser.plugin.plugins.instruction_profiler module

class mythril.laser.plugin.plugins.instruction_profiler.InstructionProfiler

Bases: LaserPlugin

Performance profile for the execution of each instruction.

initialize(symbolic_vm: LaserEVM) → None

Initializes this plugin on the symbolic virtual machine

Parameters:

symbolic_vm – symbolic virtual machine to initialize the laser plugin on

class mythril.laser.plugin.plugins.instruction_profiler.InstructionProfilerBuilder

Bases: PluginBuilder

name = 'instruction-profiler'

mythril.laser.plugin.plugins.mutation_pruner module

class mythril.laser.plugin.plugins.mutation_pruner.MutationPruner

Bases: LaserPlugin

Mutation pruner plugin

Let S be a world state from which T is a symbolic transaction, and S’ is the resulting world state. In a situation where T does not execute any mutating instructions we can safely abandon further analysis on top of state S’. This is for the reason that we already performed analysis on S, which is equivalent.

This optimization inhibits path explosion caused by “clean” behaviour

The basic operation of this plugin is as follows:

• Hook all mutating operations and introduce a MutationAnnotation to the global state on execution of the hook

• Hook the svm EndTransaction on execution filter the states that do not have a mutation annotation

initialize(symbolic_vm: LaserEVM)

Initializes the mutation pruner

Introduces hooks for SSTORE operations :param symbolic_vm: :return:

class mythril.laser.plugin.plugins.mutation_pruner.MutationPrunerBuilder

Bases: PluginBuilder

name = 'mutation-pruner'

mythril.laser.plugin.plugins.plugin_annotations module

class mythril.laser.plugin.plugins.plugin_annotations.DependencyAnnotation

Bases: MergeableStateAnnotation

Dependency Annotation

This annotation tracks read and write access to the state during each transaction.

check_merge_annotation(other: DependencyAnnotation)

extend_storage_write_cache(iteration: int, value: object)

get_storage_write_cache(iteration: int)

merge_annotation(other: DependencyAnnotation)

class mythril.laser.plugin.plugins.plugin_annotations.MutationAnnotation

Bases: StateAnnotation

Mutation Annotation

This is the annotation used by the MutationPruner plugin to record mutations

property persist_over_calls: bool

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

The default is set to False

class mythril.laser.plugin.plugins.plugin_annotations.WSDependencyAnnotation

Bases: MergeableStateAnnotation

Dependency Annotation for World state

This world state annotation maintains a stack of state annotations. It is used to transfer individual state annotations from one transaction to the next.

check_merge_annotation(annotation: WSDependencyAnnotation) → bool

merge_annotation(annotation: WSDependencyAnnotation) → WSDependencyAnnotation

Module contents

Plugin implementations

This module contains the implementation of some features

• benchmarking

• pruning