diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index bfff2c4d..dacc6bd8 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -1,7 +1,10 @@ from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.plugins.plugin import LaserPlugin from mythril.laser.ethereum.plugins.signals import PluginSkipState -from mythril.laser.ethereum.state.annotation import StateAnnotation +from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( + DependencyAnnotation, + WSDependencyAnnotation, +) from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, @@ -9,64 +12,12 @@ from mythril.laser.ethereum.transaction.transaction_models import ( from mythril.exceptions import UnsatError from mythril.analysis import solver from typing import cast, List, Dict, Set -from copy import copy import logging log = logging.getLogger(__name__) -class DependencyAnnotation(StateAnnotation): - """Dependency Annotation - - This annotation tracks read and write access to the state during each transaction. - """ - - def __init__(self): - self.storage_loaded = [] # type: List - self.storage_written = {} # type: Dict[int, List] - self.has_call = False # type: bool - self.path = [0] # type: List - self.blocks_seen = set() # type: Set[int] - - def __copy__(self): - result = DependencyAnnotation() - result.storage_loaded = copy(self.storage_loaded) - result.storage_written = copy(self.storage_written) - result.has_call = self.has_call - result.path = copy(self.path) - result.blocks_seen = copy(self.blocks_seen) - return result - - def get_storage_write_cache(self, iteration: int): - if iteration not in self.storage_written: - self.storage_written[iteration] = [] - - return self.storage_written[iteration] - - def extend_storage_write_cache(self, iteration: int, value: object): - if iteration not in self.storage_written: - self.storage_written[iteration] = [value] - elif value not in self.storage_written[iteration]: - self.storage_written[iteration].append(value) - - -class WSDependencyAnnotation(StateAnnotation): - """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. - """ - - def __init__(self): - self.annotations_stack = [] - - def __copy__(self): - result = WSDependencyAnnotation() - result.annotations_stack = copy(self.annotations_stack) - return result - - def get_dependency_annotation(state: GlobalState) -> DependencyAnnotation: """ Returns a dependency annotation diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index fa6aef58..6bc13d9e 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -1,26 +1,16 @@ -from mythril.laser.ethereum.state.annotation import StateAnnotation -from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState from mythril.laser.ethereum.plugins.plugin import LaserPlugin +from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( + MutationAnnotation, +) from mythril.laser.ethereum.state.global_state import GlobalState +from mythril.laser.ethereum.svm import LaserEVM from mythril.laser.ethereum.transaction.transaction_models import ( ContractCreationTransaction, ) from mythril.laser.smt import And, symbol_factory -class MutationAnnotation(StateAnnotation): - """Mutation Annotation - - This is the annotation used by the MutationPruner plugin to record mutations - """ - - @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): """Mutation pruner plugin @@ -47,16 +37,10 @@ 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): @@ -72,8 +56,5 @@ class MutationPruner(LaserPlugin): global_state.current_transaction, ContractCreationTransaction ): return - if ( - len(list(global_state.world_state.get_annotations(MutationAnnotation))) - == 0 - ): + if len(list(global_state.get_annotations(MutationAnnotation))) == 0: raise PluginSkipWorldState diff --git a/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py b/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py new file mode 100644 index 00000000..209e562e --- /dev/null +++ b/mythril/laser/ethereum/plugins/implementations/plugin_annotations.py @@ -0,0 +1,65 @@ +from mythril.laser.ethereum.state.annotation import StateAnnotation + +from copy import copy +from typing import Dict, List, Set + + +class MutationAnnotation(StateAnnotation): + """Mutation Annotation + + This is the annotation used by the MutationPruner plugin to record mutations + """ + + def __init__(self): + pass + + +class DependencyAnnotation(StateAnnotation): + """Dependency Annotation + + This annotation tracks read and write access to the state during each transaction. + """ + + def __init__(self): + self.storage_loaded = [] # type: List + self.storage_written = {} # type: Dict[int, List] + self.has_call = False # type: bool + self.path = [0] # type: List + self.blocks_seen = set() # type: Set[int] + + def __copy__(self): + result = DependencyAnnotation() + result.storage_loaded = copy(self.storage_loaded) + result.storage_written = copy(self.storage_written) + result.has_call = self.has_call + result.path = copy(self.path) + result.blocks_seen = copy(self.blocks_seen) + return result + + def get_storage_write_cache(self, iteration: int): + if iteration not in self.storage_written: + self.storage_written[iteration] = [] + + return self.storage_written[iteration] + + def extend_storage_write_cache(self, iteration: int, value: object): + if iteration not in self.storage_written: + self.storage_written[iteration] = [value] + elif value not in self.storage_written[iteration]: + self.storage_written[iteration].append(value) + + +class WSDependencyAnnotation(StateAnnotation): + """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. + """ + + def __init__(self): + self.annotations_stack = [] + + def __copy__(self): + result = WSDependencyAnnotation() + result.annotations_stack = copy(self.annotations_stack) + return result diff --git a/mythril/laser/ethereum/state/global_state.py b/mythril/laser/ethereum/state/global_state.py index 0c43980b..5096516e 100644 --- a/mythril/laser/ethereum/state/global_state.py +++ b/mythril/laser/ethereum/state/global_state.py @@ -53,6 +53,14 @@ class GlobalState: self.last_return_data = last_return_data self._annotations = annotations or [] + def add_annotations(self, annotations: List[StateAnnotation]): + """ + Function used to add annotations to global state + :param annotations: + :return: + """ + self._annotations += annotations + def __copy__(self) -> "GlobalState": """ diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 0c554c7c..822d1c55 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -12,6 +12,9 @@ from mythril.laser.ethereum.evm_exceptions import VmException from mythril.laser.ethereum.instructions import Instruction from mythril.laser.ethereum.iprof import InstructionProfiler from mythril.laser.ethereum.plugins.signals import PluginSkipWorldState, PluginSkipState +from mythril.laser.ethereum.plugins.implementations.plugin_annotations import ( + MutationAnnotation, +) from mythril.laser.ethereum.state.global_state import GlobalState from mythril.laser.ethereum.state.world_state import WorldState from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy @@ -354,6 +357,19 @@ class LaserEVM: # First execute the post hook for the transaction ending instruction self._execute_post_hook(op_code, [end_signal.global_state]) + # Propogate codecall based annotations + if return_global_state.get_current_instruction()["opcode"] in ( + "DELEGATECALL", + "CALLCODE", + ): + new_annotations = [ + annotation + for annotation in global_state.get_annotations( + MutationAnnotation + ) + ] + return_global_state.add_annotations(new_annotations) + new_global_states = self._end_message_call( copy(return_global_state), global_state,