diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index 21034850..7c1c0f83 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -150,6 +150,12 @@ class DependencyPruner(LaserPlugin): :param target_location """ + log.debug( + "Updating dependency map for path: {} with location: {}".format( + path, target_location + ) + ) + try: for address in path: if address in self.dependency_map: @@ -170,13 +176,17 @@ class DependencyPruner(LaserPlugin): for address in path: self.protected_addresses.add(address) - def wanna_execute(self, address: int, storage_write_cache) -> bool: + def wanna_execute(self, address: int, annotation: DependencyAnnotation) -> bool: """Decide whether the basic block starting at 'address' should be executed. :param address :param storage_write_cache """ + storage_write_cache = annotation.get_storage_write_cache(self.iteration - 1) + + # Execute the block if it's marked as "protected" or doesn't yet have an entry in the dependency map. + if address in self.protected_addresses or address not in self.dependency_map: return True @@ -187,6 +197,18 @@ class DependencyPruner(LaserPlugin): for location in storage_write_cache: for dependency in dependencies: + # Is there a known read operation along this path that matches a write in the previous transaction? + + try: + solver.get_model((location == dependency,)) + return True + + except UnsatError: + continue + + # Has the *currently executed* path been influenced by a write operation in the previous transaction? + + for dependency in annotation.storage_loaded: try: solver.get_model((location == dependency,)) return True @@ -216,27 +238,25 @@ class DependencyPruner(LaserPlugin): @symbolic_vm.post_hook("JUMP") def jump_hook(state: GlobalState): address = state.get_current_instruction()["address"] - annotation = get_dependency_annotation(state) - - _check_basic_block(address, annotation) - @symbolic_vm.pre_hook("JUMPDEST") - def jumpdest_hook(state: GlobalState): - address = state.get_current_instruction()["address"] annotation = get_dependency_annotation(state) + annotation.path.append(address) _check_basic_block(address, annotation) @symbolic_vm.post_hook("JUMPI") def jumpi_hook(state: GlobalState): address = state.get_current_instruction()["address"] + annotation = get_dependency_annotation(state) + annotation.path.append(address) _check_basic_block(address, annotation) @symbolic_vm.pre_hook("SSTORE") def sstore_hook(state: GlobalState): annotation = get_dependency_annotation(state) + annotation.extend_storage_write_cache( self.iteration, state.mstate.stack[-1] ) @@ -288,15 +308,11 @@ class DependencyPruner(LaserPlugin): if self.iteration < 2: return - annotation.path.append(address) - - if self.wanna_execute( - address, annotation.get_storage_write_cache(self.iteration - 1) - ): + if self.wanna_execute(address, annotation): return else: log.debug( - "Skipping state: Storage slots {} not read in block at address {}".format( + "Skipping state: Storage slots {} not read in block at address {}, function".format( annotation.get_storage_write_cache(self.iteration - 1), address ) )