diff --git a/mythril/analysis/solver.py b/mythril/analysis/solver.py index d949dd57..9504c71a 100644 --- a/mythril/analysis/solver.py +++ b/mythril/analysis/solver.py @@ -204,6 +204,14 @@ def _set_minimisation_constraints( ) ) + # FIXME: This shouldn't be needed. + constraints.append( + UGE( + symbol_factory.BitVecVal(1000000000000000000000, 256), + transaction.call_value, + ) + ) + for account in world_state.accounts.values(): # Lazy way to prevent overflows and to ensure "reasonable" balances # Each account starts with less than 100 ETH diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index bb78fdd8..b2b1ee16 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -25,6 +25,7 @@ class DependencyAnnotation(StateAnnotation): 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] @@ -32,6 +33,7 @@ class DependencyAnnotation(StateAnnotation): 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 @@ -134,6 +136,7 @@ class DependencyPruner(LaserPlugin): def _reset(self): self.iteration = 0 + self.calls_on_path = {} # type: Dict[int, bool] self.sloads_on_path = {} # type: Dict[int, List[object]] self.sstores_on_path = {} # type: Dict[int, List[object]] self.storage_accessed_global = set() # type: Set @@ -166,6 +169,17 @@ class DependencyPruner(LaserPlugin): else: self.sstores_on_path[address] = [target_location] + def update_calls(self, path: List[int]) -> None: + """Update the dependency map for the block offsets on the given path. + + :param path + :param target_location + """ + + for address in path: + if address in self.sstores_on_path: + self.calls_on_path[address] = True + def wanna_execute(self, address: int, annotation: DependencyAnnotation) -> bool: """Decide whether the basic block starting at 'address' should be executed. @@ -175,6 +189,9 @@ class DependencyPruner(LaserPlugin): storage_write_cache = annotation.get_storage_write_cache(self.iteration - 1) + if address in self.calls_on_path: + return True + # Skip "pure" paths that don't have any dependencies. if address not in self.sloads_on_path: @@ -270,6 +287,13 @@ class DependencyPruner(LaserPlugin): self.update_sloads(annotation.path, location) self.storage_accessed_global.add(location) + @symbolic_vm.pre_hook("CALL") + def stop_hook(state: GlobalState): + annotation = get_dependency_annotation(state) + + self.update_calls(annotation.path) + annotation.has_call = True + @symbolic_vm.pre_hook("STOP") def stop_hook(state: GlobalState): _transaction_end(state) @@ -293,11 +317,14 @@ class DependencyPruner(LaserPlugin): for index in annotation.storage_written: self.update_sstores(annotation.path, index) + if annotation.has_call: + self.update_calls(annotation.path) + def _check_basic_block(address: int, annotation: DependencyAnnotation): """This method is where the actual pruning happens. :param address: Start address (bytecode offset) of the block - :param annotation + :param annotation: """ # Don't skip any blocks in the contract creation transaction @@ -338,13 +365,3 @@ class DependencyPruner(LaserPlugin): annotation.storage_loaded = [] world_state_annotation.annotations_stack.append(annotation) - - log.debug( - "Iteration {}: Adding world state at address {}, end of function {}.\nDependency map: {}\nStorage written: {}".format( - self.iteration, - state.get_current_instruction()["address"], - state.node.function_name, - self.sloads_on_path, - annotation.storage_written[self.iteration], - ) - ) diff --git a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py index 8a6fc9d6..8b19b292 100644 --- a/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/mutation_pruner.py @@ -45,6 +45,10 @@ class MutationPruner(LaserPlugin): def mutator_hook(global_state: GlobalState): global_state.annotate(MutationAnnotation()) + @symbolic_vm.pre_hook("CALL") + def mutator_hook(global_state: GlobalState): + global_state.annotate(MutationAnnotation()) + @symbolic_vm.laser_hook("add_world_state") def world_state_filter_hook(global_state: GlobalState): if And(