diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 8528a51f..1626607e 100644 --- a/mythril/analysis/symbolic.py +++ b/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, ): """ @@ -111,6 +112,7 @@ class SymExecWrapper: transaction_count=transaction_count, requires_statespace=requires_statespace, enable_iprof=enable_iprof, + enable_coverage_strategy=enable_coverage_strategy, ) if loop_bound is not None: diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index f18aa254..fce9428a 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -391,6 +391,9 @@ 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 +564,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: diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index 9755fc33..cb804a7f 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -55,6 +55,7 @@ class LaserEVM: transaction_count=2, requires_statespace=True, enable_iprof=False, + enable_coverage_strategy=False, ) -> None: """ Initializes the laser evm object @@ -102,6 +103,13 @@ class LaserEVM: self.iprof = InstructionProfiler() if enable_iprof else None + if enable_coverage_strategy: + from mythril.laser.ethereum.plugins.implementations.coverage.coverage_plugin import InstructionCoveragePlugin + from mythril.laser.ethereum.plugins.implementations.coverage.coverage_strategy import CoverageStrategy + instruction = InstructionCoveragePlugin() + instruction.initialize(self) + self.strategy = CoverageStrategy(self.strategy, instruction) + log.info("LASER EVM initialized with dynamic loader: " + str(dynamic_loader)) def extend_strategy(self, extension: ABCMeta, *args) -> None: diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py index 497c4c33..deb86281 100644 --- a/mythril/mythril/mythril_analyzer.py +++ b/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)