mythril.laser.plugin package

Subpackages

• mythril.laser.plugin.plugins package
  • Subpackages
    • mythril.laser.plugin.plugins.coverage package
      • Submodules
      • mythril.laser.plugin.plugins.coverage.coverage_plugin module
      • mythril.laser.plugin.plugins.coverage.coverage_strategy module
      • Module contents
    • mythril.laser.plugin.plugins.summary_backup package
      • Module contents
  • Submodules
  • mythril.laser.plugin.plugins.benchmark module
    • BenchmarkPlugin
      • BenchmarkPlugin.initialize()
    • BenchmarkPluginBuilder
      • BenchmarkPluginBuilder.name
  • mythril.laser.plugin.plugins.call_depth_limiter module
    • CallDepthLimit
      • CallDepthLimit.initialize()
    • CallDepthLimitBuilder
      • CallDepthLimitBuilder.name
  • mythril.laser.plugin.plugins.dependency_pruner module
    • DependencyPruner
      • DependencyPruner.initialize()
      • DependencyPruner.update_calls()
      • DependencyPruner.update_sloads()
      • DependencyPruner.update_sstores()
      • DependencyPruner.wanna_execute()
    • DependencyPrunerBuilder
      • DependencyPrunerBuilder.name
    • get_dependency_annotation()
    • get_ftn_seq_annotation_from_ws()
    • get_writes_annotation_from_ws()
    • get_ws_dependency_annotation()
  • mythril.laser.plugin.plugins.instruction_profiler module
    • InstructionProfiler
      • InstructionProfiler.initialize()
    • InstructionProfilerBuilder
      • InstructionProfilerBuilder.name
  • mythril.laser.plugin.plugins.mutation_pruner module
    • MutationPruner
      • MutationPruner.initialize()
    • MutationPrunerBuilder
      • MutationPrunerBuilder.name
  • mythril.laser.plugin.plugins.plugin_annotations module
    • DependencyAnnotation
      • DependencyAnnotation.check_merge_annotation()
      • DependencyAnnotation.extend_storage_write_cache()
      • DependencyAnnotation.get_storage_write_cache()
      • DependencyAnnotation.merge_annotation()
    • MutationAnnotation
      • MutationAnnotation.persist_over_calls
    • WSDependencyAnnotation
      • WSDependencyAnnotation.check_merge_annotation()
      • WSDependencyAnnotation.merge_annotation()
  • Module contents

Submodules

mythril.laser.plugin.builder module

class mythril.laser.plugin.builder.PluginBuilder

Bases: ABC

The plugin builder interface enables construction of Laser plugins

name = 'Default Plugin Name'

mythril.laser.plugin.interface module

class mythril.laser.plugin.interface.LaserPlugin

Bases: object

Base class for laser plugins

Functionality in laser that the symbolic execution process does not need to depend on can be implemented in the form of a laser plugin.

Laser plugins implement the function initialize(symbolic_vm) which is called with the laser virtual machine when they are loaded. Regularly a plugin will introduce several hooks into laser in this function

Plugins can direct actions by raising Signals defined in mythril.laser.ethereum.plugins.signals For example, a pruning plugin might raise the PluginSkipWorldState signal.

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

mythril.laser.plugin.loader module

class mythril.laser.plugin.loader.LaserPluginLoader(*args, **kwargs)

Bases: object

The LaserPluginLoader is used to abstract the logic relating to plugins. Components outside of laser thus don’t have to be aware of the interface that plugins provide

add_args(plugin_name, **kwargs)

enable(plugin_name: str)

instrument_virtual_machine(symbolic_vm: LaserEVM, with_plugins: List[str] | None)

Load enabled plugins into the passed symbolic virtual machine :param symbolic_vm: The virtual machine to instrument the plugins with :param with_plugins: Override the globally enabled/disabled builders and load all plugins in the list

is_enabled(plugin_name: str) → bool

Returns whether the plugin is loaded in the symbolic_vm

Parameters:

plugin_name – Name of the plugin to check

load(plugin_builder: PluginBuilder) → None

Enables a Laser Plugin

Parameters:

plugin_builder – Builder that constructs the plugin

mythril.laser.plugin.signals module

exception mythril.laser.plugin.signals.PluginSignal

Bases: Exception

Base plugin signal

These signals are used by the laser plugins to create intent for certain actions in the symbolic virtual machine

exception mythril.laser.plugin.signals.PluginSkipState

Bases: PluginSignal

Plugin to skip world state

Plugins that raise this signal while the add_world_state hook is being executed will force laser to abandon that world state.

exception mythril.laser.plugin.signals.PluginSkipWorldState

Bases: PluginSignal

Plugin to skip world state

Plugins that raise this signal while the add_world_state hook is being executed will force laser to abandon that world state.

Module contents

Laser plugins

This module contains everything to do with laser plugins

Laser plugins are a way of extending laser’s functionality without complicating the core business logic. Different features that have been implemented in the form of plugins are: - benchmarking - path pruning

Plugins also provide a way to implement optimisations outside of the mythril code base and to inject them. The api that laser currently provides is still unstable and will probably change to suit our needs as more plugins get developed.

For the implementation of plugins the following modules are of interest: - laser.plugins.plugin - laser.plugins.signals - laser.svm

Which show the basic interfaces with which plugins are able to interact