diff --git a/mythril/laser/ethereum/svm.py b/mythril/laser/ethereum/svm.py index cdf85484..08f35ba4 100644 --- a/mythril/laser/ethereum/svm.py +++ b/mythril/laser/ethereum/svm.py @@ -60,7 +60,7 @@ class LaserEVM: def accounts(self): return self.world_state.accounts - def sym_exec(self, main_address=None, creation_code=None, contract_name=None): + def sym_exec(self, main_address=None, creation_code=None, contract_name=None, max_transactions=3): logging.debug("Starting LASER execution") self.time = datetime.now() @@ -77,12 +77,16 @@ class LaserEVM: # Reset code coverage self.coverage = {} - self.time = datetime.now() - logging.info("Starting message call transaction") - execute_message_call(self, created_account.address) + for i in range(max_transactions): + initial_coverage = self._get_covered_instructions() - self.time = datetime.now() - execute_message_call(self, created_account.address) + self.time = datetime.now() + logging.info("Starting message call transaction, iteration: {}".format(i)) + execute_message_call(self, created_account.address) + + end_coverage = self._get_covered_instructions() + if end_coverage == initial_coverage: + break logging.info("Finished symbolic execution") logging.info("%d nodes, %d edges, %d total states", len(self.nodes), len(self.edges), self.total_states) @@ -90,6 +94,13 @@ class LaserEVM: cov = reduce(lambda sum_, val: sum_ + 1 if val else sum_, coverage[1]) / float(coverage[0]) * 100 logging.info("Achieved {} coverage for code: {}".format(cov, code)) + def _get_covered_instructions(self) -> int: + """ Gets the total number of covered instructions for all accounts in the svm""" + total_covered_instructions = 0 + for _, cv in self.coverage.items(): + total_covered_instructions += reduce(lambda sum_, val: sum_ + 1 if val else sum_, cv[1]) + return total_covered_instructions + def exec(self, create=False): for global_state in self.strategy: if self.execution_timeout and not create: