diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index 86755610..fa6aef58 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -15,7 +15,10 @@ class MutationAnnotation(StateAnnotation): This is the annotation used by the MutationPruner plugin to record mutations """ - pass + @property + def persist_to_world_state(self): + # This should persist among calls, and be but as a world state annotation. + return True class MutationPruner(LaserPlugin): @@ -44,10 +47,16 @@ class MutationPruner(LaserPlugin): @symbolic_vm.pre_hook("SSTORE") def sstore_mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) + assert len( + list(global_state.world_state.get_annotations(MutationAnnotation)) + ) @symbolic_vm.pre_hook("CALL") def call_mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) + assert len( + list(global_state.world_state.get_annotations(MutationAnnotation)) + ) @symbolic_vm.laser_hook("add_world_state") def world_state_filter_hook(global_state: GlobalState): @@ -63,5 +72,8 @@ class MutationPruner(LaserPlugin): global_state.current_transaction, ContractCreationTransaction ): return - if len(list(global_state.get_annotations(MutationAnnotation))) == 0: + if ( + len(list(global_state.world_state.get_annotations(MutationAnnotation))) + == 0 + ): raise PluginSkipWorldState diff --git a/mythril/laser/ethereum/state/annotation.py b/mythril/laser/ethereum/state/annotation.py index 6a321776..0f25a311 100644 --- a/mythril/laser/ethereum/state/annotation.py +++ b/mythril/laser/ethereum/state/annotation.py @@ -12,6 +12,8 @@ class StateAnnotation: traverse the state space themselves. """ + # TODO: Remove this? It seems to be used only in the MutationPruner, and + # we could simply use world state annotations if we want them to be persisted. @property def persist_to_world_state(self) -> bool: """If this function returns true then laser will also annotate the