diff --git a/mythril/analysis/symbolic.py b/mythril/analysis/symbolic.py index 8064d8fe..d5315b3f 100644 --- a/mythril/analysis/symbolic.py +++ b/mythril/analysis/symbolic.py @@ -56,6 +56,7 @@ class SymExecWrapper: run_analysis_modules: bool = True, enable_coverage_strategy: bool = False, custom_modules_directory: str = "", + enable_state_merging: bool = False ): """ @@ -74,6 +75,7 @@ class SymExecWrapper: :param run_analysis_modules: Boolean indicating whether analysis modules should be executed :param enable_coverage_strategy: Boolean indicating whether the coverage strategy should be enabled :param custom_modules_directory: The directory to read custom analysis modules from + :param enable_state_merging: Enables state merging """ if isinstance(address, str): address = symbol_factory.BitVecVal(int(address, 16), 256) @@ -130,8 +132,9 @@ class SymExecWrapper: plugin_loader = LaserPluginLoader(self.laser) plugin_loader.load(PluginFactory.build_mutation_pruner_plugin()) - plugin_loader.load(PluginFactory.build_state_merge_plugin()) plugin_loader.load(instruction_laser_plugin) + if enable_state_merging: + plugin_loader.load(PluginFactory.build_state_merge_plugin()) if not disable_dependency_pruning: plugin_loader.load(PluginFactory.build_dependency_pruner_plugin()) diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py index 96731a10..0ff8121c 100644 --- a/mythril/interfaces/cli.py +++ b/mythril/interfaces/cli.py @@ -464,6 +464,11 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser): action="store_true", help="enable coverage based search strategy", ) + options.add_argument( + "--enable-state-merging", + action="store_true", + help="enables state merging", + ) options.add_argument( "--custom-modules-directory", help="designates a separate directory to search for custom analysis modules", @@ -666,6 +671,7 @@ def execute_command( custom_modules_directory=args.custom_modules_directory if args.custom_modules_directory else "", + enable_state_merging=args.enable_state_merging, ) if not disassembler.contracts: diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py index a7920d57..5407570c 100644 --- a/mythril/mythril/mythril_analyzer.py +++ b/mythril/mythril/mythril_analyzer.py @@ -44,6 +44,7 @@ class MythrilAnalyzer: solver_timeout: Optional[int] = None, enable_coverage_strategy: bool = False, custom_modules_directory: str = "", + enable_state_merging: bool = False, ): """ @@ -66,7 +67,7 @@ class MythrilAnalyzer: self.disable_dependency_pruning = disable_dependency_pruning self.enable_coverage_strategy = enable_coverage_strategy self.custom_modules_directory = custom_modules_directory - + self.enable_state_merging = enable_state_merging analysis_args.set_loop_bound(loop_bound) analysis_args.set_solver_timeout(solver_timeout) @@ -170,6 +171,7 @@ class MythrilAnalyzer: disable_dependency_pruning=self.disable_dependency_pruning, enable_coverage_strategy=self.enable_coverage_strategy, custom_modules_directory=self.custom_modules_directory, + enable_state_merging=self.enable_state_merging ) issues = fire_lasers(sym, modules, self.custom_modules_directory) except KeyboardInterrupt: