mythril.laser.plugin.plugins package¶
Subpackages¶
Submodules¶
mythril.laser.plugin.plugins.benchmark module¶
-
class
mythril.laser.plugin.plugins.benchmark.
BenchmarkPlugin
(name=None)[source]¶ Bases:
mythril.laser.plugin.interface.LaserPlugin
Benchmark Plugin
This plugin aggregates the following information: - duration - code coverage over time - final code coverage - total number of executed instructions
-
class
mythril.laser.plugin.plugins.benchmark.
BenchmarkPluginBuilder
[source]¶ Bases:
mythril.laser.plugin.builder.PluginBuilder
-
name
= 'benchmark'¶
-
mythril.laser.plugin.plugins.call_depth_limiter module¶
-
class
mythril.laser.plugin.plugins.call_depth_limiter.
CallDepthLimit
(call_depth_limit: int)[source]¶
-
class
mythril.laser.plugin.plugins.call_depth_limiter.
CallDepthLimitBuilder
[source]¶ Bases:
mythril.laser.plugin.builder.PluginBuilder
-
name
= 'call-depth-limit'¶
-
mythril.laser.plugin.plugins.dependency_pruner module¶
-
class
mythril.laser.plugin.plugins.dependency_pruner.
DependencyPruner
[source]¶ Bases:
mythril.laser.plugin.interface.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: mythril.laser.ethereum.svm.LaserEVM) → None[source]¶ Initializes the DependencyPruner
:param symbolic_vm
-
update_calls
(path: List[int]) → None[source]¶ 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[source]¶ Update the dependency map for the block offsets on the given path.
:param path :param target_location
-
-
class
mythril.laser.plugin.plugins.dependency_pruner.
DependencyPrunerBuilder
[source]¶ Bases:
mythril.laser.plugin.builder.PluginBuilder
-
name
= 'dependency-pruner'¶
-
mythril.laser.plugin.plugins.instruction_profiler module¶
-
class
mythril.laser.plugin.plugins.instruction_profiler.
InstructionProfiler
[source]¶ Bases:
mythril.laser.plugin.interface.LaserPlugin
Performance profile for the execution of each instruction.
-
class
mythril.laser.plugin.plugins.instruction_profiler.
InstructionProfilerBuilder
[source]¶ Bases:
mythril.laser.plugin.builder.PluginBuilder
-
name
= 'instruction-profiler'¶
-
mythril.laser.plugin.plugins.mutation_pruner module¶
-
class
mythril.laser.plugin.plugins.mutation_pruner.
MutationPruner
[source]¶ Bases:
mythril.laser.plugin.interface.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
-
class
mythril.laser.plugin.plugins.mutation_pruner.
MutationPrunerBuilder
[source]¶ Bases:
mythril.laser.plugin.builder.PluginBuilder
-
name
= 'mutation-pruner'¶
-
mythril.laser.plugin.plugins.plugin_annotations module¶
-
class
mythril.laser.plugin.plugins.plugin_annotations.
DependencyAnnotation
[source]¶ Bases:
mythril.laser.ethereum.state.annotation.MergeableStateAnnotation
Dependency Annotation
This annotation tracks read and write access to the state during each transaction.
-
class
mythril.laser.plugin.plugins.plugin_annotations.
MutationAnnotation
[source]¶ Bases:
mythril.laser.ethereum.state.annotation.StateAnnotation
Mutation Annotation
This is the annotation used by the MutationPruner plugin to record mutations
-
persist_over_calls
¶ 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
[source]¶ Bases:
mythril.laser.ethereum.state.annotation.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.
Module contents¶
Plugin implementations
This module contains the implementation of some features
- benchmarking
- pruning