From 73e2c1d204e3551b3b1cd0df0ca7bf440d8ff5e7 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Fri, 28 Jun 2019 10:33:40 +0200 Subject: [PATCH] Catch Z3Exceptions in DependecyPruner --- .../implementations/dependency_pruner.py | 27 +++++++++++++------ 1 file changed, 19 insertions(+), 8 deletions(-) diff --git a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py index 267abb99..154a7184 100644 --- a/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py +++ b/mythril/laser/ethereum/plugins/implementations/dependency_pruner.py @@ -38,17 +38,28 @@ class DependencyAnnotation(StateAnnotation): return result def get_storage_write_cache(self, iteration: int): - if iteration not in self.storage_written: - self.storage_written[iteration] = [] + try: + if iteration not in self.storage_written: + self.storage_written[iteration] = [] - return self.storage_written[iteration] + return self.storage_written[iteration] + except Z3Exception: + return def extend_storage_write_cache(self, iteration: int, value: object): - if iteration not in self.storage_written: - self.storage_written[iteration] = [value] - else: - if value not in self.storage_written[iteration]: - self.storage_written[iteration].append(value) + """ + FIXME: Catching Z3Exceptions here because laser returns BitVec512 symbols on rare occasions. + This shouldn't actually happen. + """ + + try: + if iteration not in self.storage_written: + self.storage_written[iteration] = [value] + else: + if value not in self.storage_written[iteration]: + self.storage_written[iteration].append(value) + except Z3Exception: + return class WSDependencyAnnotation(StateAnnotation):