Merge pull request #859 from ConsenSys/enhance/statespace

Stores the entire statespace only when necessary

mythril/analysis/modules/base.py

@@ -35,7 +35,8 @@ class DetectionModule:
             "DetectionModule "
             "name={0.name} "
             "swc_id={0.swc_id} "
-            "hooks={0.hooks} "
+            "pre_hooks={0.pre_hooks} "
+            "post_hooks={0.post_hooks} "
             "description={0.description}"
             ">"
         ).format(self)

mythril/analysis/symbolic.py

@@ -1,4 +1,4 @@
-from mythril.analysis.security import get_detection_module_hooks
+from mythril.analysis.security import get_detection_module_hooks, get_detection_modules
 from mythril.laser.ethereum import svm
 from mythril.laser.ethereum.state.account import Account
 from mythril.solidity.soliditycontract import SolidityContract, EVMContract
@@ -29,6 +29,7 @@ class SymExecWrapper:
         create_timeout=None,
         transaction_count=2,
         modules=(),
+        compulsory_statespace=True,
     ):
 
         if strategy == "dfs":
@@ -48,7 +49,9 @@ class SymExecWrapper:
             dynamic_loader=dynloader,
             contract_name=contract.name,
         )
-
+        requires_statespace = (
+            compulsory_statespace or len(get_detection_modules("post", modules)) > 0
+        )
         self.accounts = {address: account}
 
         self.laser = svm.LaserEVM(
@@ -59,6 +62,7 @@ class SymExecWrapper:
             strategy=s_strategy,
             create_timeout=create_timeout,
             transaction_count=transaction_count,
+            requires_statespace=requires_statespace,
         )
         self.laser.register_hooks(
             hook_type="pre",
@@ -80,6 +84,9 @@ class SymExecWrapper:
         else:
             self.laser.sym_exec(address)
 
+        if not requires_statespace:
+            return
+
         self.nodes = self.laser.nodes
         self.edges = self.laser.edges
 

mythril/laser/ethereum/svm.py

@@ -49,6 +49,7 @@ class LaserEVM:
         create_timeout=10,
         strategy=DepthFirstSearchStrategy,
         transaction_count=2,
+        requires_statespace=True,
     ):
         world_state = WorldState()
         world_state.accounts = accounts
@@ -56,8 +57,6 @@ class LaserEVM:
         self.world_state = world_state
         self.open_states = [world_state]
 
-        self.nodes = {}
-        self.edges = []
         self.coverage = {}
 
         self.total_states = 0
@@ -71,6 +70,11 @@ class LaserEVM:
         self.execution_timeout = execution_timeout
         self.create_timeout = create_timeout
 
+        self.requires_statespace = requires_statespace
+        if self.requires_statespace:
+            self.nodes = {}
+            self.edges = []
+
         self.time = None
 
         self.pre_hooks = defaultdict(list)
@@ -124,12 +128,13 @@ class LaserEVM:
             self._execute_transactions(created_account.address)
 
         log.info("Finished symbolic execution")
-        log.info(
-            "%d nodes, %d edges, %d total states",
-            len(self.nodes),
-            len(self.edges),
-            self.total_states,
-        )
+        if self.requires_statespace:
+            log.info(
+                "%d nodes, %d edges, %d total states",
+                len(self.nodes),
+                len(self.edges),
+                self.total_states,
+            )
         for code, coverage in self.coverage.items():
             cov = (
                 reduce(lambda sum_, val: sum_ + 1 if val else sum_, coverage[1])
@@ -362,10 +367,13 @@ class LaserEVM:
         old_node = state.node
         state.node = new_node
         new_node.constraints = state.mstate.constraints
-        self.nodes[new_node.uid] = new_node
-        self.edges.append(
-            Edge(old_node.uid, new_node.uid, edge_type=edge_type, condition=condition)
-        )
+        if self.requires_statespace:
+            self.nodes[new_node.uid] = new_node
+            self.edges.append(
+                Edge(
+                    old_node.uid, new_node.uid, edge_type=edge_type, condition=condition
+                )
+            )
 
         if edge_type == JumpType.RETURN:
             new_node.flags |= NodeFlags.CALL_RETURN

mythril/laser/ethereum/transaction/concolic.py

@@ -58,8 +58,9 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
         function_name=global_state.environment.active_function_name,
     )
 
-    laser_evm.nodes[new_node.uid] = new_node
-    if transaction.world_state.node:
+    if laser_evm.requires_statespace:
+        laser_evm.nodes[new_node.uid] = new_node
+    if transaction.world_state.node and laser_evm.requires_statespace:
         laser_evm.edges.append(
             Edge(
                 transaction.world_state.node.uid,
@@ -68,6 +69,7 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
                 condition=None,
             )
         )
+
     global_state.node = new_node
     new_node.states.append(global_state)
     laser_evm.work_list.append(global_state)

mythril/laser/ethereum/transaction/symbolic.py

@@ -102,17 +102,19 @@ def _setup_global_state_for_execution(laser_evm, transaction) -> None:
         global_state.environment.active_account.contract_name,
         function_name=global_state.environment.active_function_name,
     )
+    if laser_evm.requires_statespace:
+        laser_evm.nodes[new_node.uid] = new_node
 
-    laser_evm.nodes[new_node.uid] = new_node
     if transaction.world_state.node:
-        laser_evm.edges.append(
-            Edge(
-                transaction.world_state.node.uid,
-                new_node.uid,
-                edge_type=JumpType.Transaction,
-                condition=None,
+        if laser_evm.requires_statespace:
+            laser_evm.edges.append(
+                Edge(
+                    transaction.world_state.node.uid,
+                    new_node.uid,
+                    edge_type=JumpType.Transaction,
+                    condition=None,
+                )
             )
-        )
 
         global_state.mstate.constraints += transaction.world_state.node.constraints
         new_node.constraints = global_state.mstate.constraints

mythril/mythril.py

@@ -496,6 +496,7 @@ class Mythril(object):
                     create_timeout=create_timeout,
                     transaction_count=transaction_count,
                     modules=modules,
+                    compulsory_statespace=False,
                 )
                 issues = fire_lasers(sym, modules)
             except KeyboardInterrupt:

mythril/support/truffle.py

@@ -56,6 +56,8 @@ def analyze_truffle_project(sigs, args):
                 create_timeout=args.create_timeout,
                 execution_timeout=args.execution_timeout,
                 transaction_count=args.transaction_count,
+                modules=args.modules or [],
+                compulsory_statespace=False,
             )
             issues = fire_lasers(sym)