Merge pull request #1129 from ConsenSys/develop

Merge changes to dependency pruning

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
                     )
                 )