Merge branch 'model-balances' of github.com:ConsenSys/mythril-classic into model-balances

mythril/analysis/symbolic.py

@@ -55,6 +55,7 @@ class SymExecWrapper:
         enable_iprof=False,
         disable_dependency_pruning=False,
         run_analysis_modules=True,
+        enable_coverage_strategy=False,
     ):
         """
 
@@ -102,6 +103,8 @@ class SymExecWrapper:
                 hex(ATTACKER_ADDRESS): attacker_account,
             }
 
+        instruction_laser_plugin = PluginFactory.build_instruction_coverage_plugin()
+
         self.laser = svm.LaserEVM(
             dynamic_loader=dynloader,
             max_depth=max_depth,
@@ -111,6 +114,8 @@ class SymExecWrapper:
             transaction_count=transaction_count,
             requires_statespace=requires_statespace,
             enable_iprof=enable_iprof,
+            enable_coverage_strategy=enable_coverage_strategy,
+            instruction_laser_plugin=instruction_laser_plugin,
         )
 
         if loop_bound is not None:
@@ -118,7 +123,7 @@ class SymExecWrapper:
 
         plugin_loader = LaserPluginLoader(self.laser)
         plugin_loader.load(PluginFactory.build_mutation_pruner_plugin())
-        plugin_loader.load(PluginFactory.build_instruction_coverage_plugin())
+        plugin_loader.load(instruction_laser_plugin)
 
         if not disable_dependency_pruning:
             plugin_loader.load(PluginFactory.build_dependency_pruner_plugin())

mythril/interfaces/cli.py

@@ -391,6 +391,11 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
         action="store_true",
         help="Deactivate dependency-based pruning",
     )
+    options.add_argument(
+        "--enable-coverage-strategy",
+        action="store_true",
+        help="enable coverage based search strategy",
+    )
 
 
 def validate_args(args: Namespace):
@@ -561,6 +566,7 @@ def execute_command(
             onchain_storage_access=not args.no_onchain_storage_access,
             solver_timeout=args.solver_timeout,
             requires_dynld=not args.no_onchain_storage_access,
+            enable_coverage_strategy=args.enable_coverage_strategy,
         )
 
         if not disassembler.contracts:

mythril/laser/ethereum/svm.py

@@ -55,6 +55,8 @@ class LaserEVM:
         transaction_count=2,
         requires_statespace=True,
         enable_iprof=False,
+        enable_coverage_strategy=False,
+        instruction_laser_plugin=None,
     ) -> None:
         """
         Initializes the laser evm object
@@ -102,6 +104,13 @@ class LaserEVM:
 
         self.iprof = InstructionProfiler() if enable_iprof else None
 
+        if enable_coverage_strategy:
+            from mythril.laser.ethereum.plugins.implementations.coverage.coverage_strategy import (
+                CoverageStrategy,
+            )
+
+            self.strategy = CoverageStrategy(self.strategy, instruction_laser_plugin)
+
         log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader))
 
     def extend_strategy(self, extension: ABCMeta, *args) -> None:

mythril/mythril/mythril_analyzer.py

@@ -41,6 +41,7 @@ class MythrilAnalyzer:
         enable_iprof: bool = False,
         disable_dependency_pruning: bool = False,
         solver_timeout: Optional[int] = None,
+        enable_coverage_strategy: bool = False,
     ):
         """
 
@@ -61,6 +62,7 @@ class MythrilAnalyzer:
         self.create_timeout = create_timeout
         self.enable_iprof = enable_iprof
         self.disable_dependency_pruning = disable_dependency_pruning
+        self.enable_coverage_strategy = enable_coverage_strategy
 
         analysis_args.set_loop_bound(loop_bound)
         analysis_args.set_solver_timeout(solver_timeout)
@@ -86,6 +88,7 @@ class MythrilAnalyzer:
             enable_iprof=self.enable_iprof,
             disable_dependency_pruning=self.disable_dependency_pruning,
             run_analysis_modules=False,
+            enable_coverage_strategy=self.enable_coverage_strategy,
         )
 
         return get_serializable_statespace(sym)
@@ -121,6 +124,7 @@ class MythrilAnalyzer:
             enable_iprof=self.enable_iprof,
             disable_dependency_pruning=self.disable_dependency_pruning,
             run_analysis_modules=False,
+            enable_coverage_strategy=self.enable_coverage_strategy,
         )
         return generate_graph(sym, physics=enable_physics, phrackify=phrackify)
 
@@ -158,6 +162,7 @@ class MythrilAnalyzer:
                     compulsory_statespace=False,
                     enable_iprof=self.enable_iprof,
                     disable_dependency_pruning=self.disable_dependency_pruning,
+                    enable_coverage_strategy=self.enable_coverage_strategy,
                 )
 
                 issues = fire_lasers(sym, modules)