From b84a55b81369b43dc99309084a944349253d7fd5 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 26 Jun 2019 11:01:38 +0200 Subject: [PATCH 1/3] Simplify bounded loops extensions --- .../strategy/extensions/bounded_loops.py | 57 +++++++++---------- 1 file changed, 26 insertions(+), 31 deletions(-) diff --git a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py index 48f77383..88f68cae 100644 --- a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py +++ b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py @@ -14,11 +14,11 @@ class JumpdestCountAnnotation(StateAnnotation): """State annotation that counts the number of jumps per destination.""" def __init__(self) -> None: - self._jumpdest_count = {} # type: Dict[int, int] + self._reached_count = {} # type: Dict[int, int] def __copy__(self): result = JumpdestCountAnnotation() - result._jumpdest_count = copy(self._jumpdest_count) + result._reached_count = copy(self._reached_count) return result @@ -31,11 +31,11 @@ class BoundedLoopsStrategy(BasicSearchStrategy): """""" self.super_strategy = super_strategy - self.jumpdest_limit = args[0][0] + self.bound = args[0][0] log.info( "Loaded search strategy extension: Loop bounds (limit = {})".format( - self.jumpdest_limit + self.bound ) ) @@ -44,41 +44,36 @@ class BoundedLoopsStrategy(BasicSearchStrategy): ) def get_strategic_global_state(self) -> GlobalState: - """ - :return: + """ Returns the next state + + :return: Global state """ - while True: + state = self.super_strategy.get_strategic_global_state() - state = self.super_strategy.get_strategic_global_state() - opcode = state.get_current_instruction()["opcode"] + annotations = cast( + List[JumpdestCountAnnotation], + list(state.get_annotations(JumpdestCountAnnotation)), + ) - if opcode != "JUMPI": - return state + if len(annotations) == 0: + annotation = JumpdestCountAnnotation() + state.annotate(annotation) + else: + annotation = annotations[0] - annotations = cast( - List[JumpdestCountAnnotation], - list(state.get_annotations(JumpdestCountAnnotation)), - ) - - if len(annotations) == 0: - annotation = JumpdestCountAnnotation() - state.annotate(annotation) - else: - annotation = annotations[0] + while True: - try: - target = util.get_concrete_int(state.mstate.stack[-1]) - except TypeError: - return state + address = state.get_current_instruction()["address"] - try: - annotation._jumpdest_count[target] += 1 - except KeyError: - annotation._jumpdest_count[target] = 1 + if address in annotation._reached_count: + annotation._reached_count[address] += 1 + else: + annotation._reached_count[address] = 1 - if annotation._jumpdest_count[target] > self.jumpdest_limit: - log.debug("JUMPDEST limit reached, skipping JUMPI") + if annotation._reached_count[address] > self.bound: + log.info("Loop bound reached, skipping state") + state = self.super_strategy.get_strategic_global_state() continue return state From a146a9a8cddcb49fa9ed44f7f4a34be1b39db4f6 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 26 Jun 2019 11:05:44 +0200 Subject: [PATCH 2/3] Refactor --- .../strategy/extensions/bounded_loops.py | 23 +++++++++---------- 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py index 88f68cae..f312516c 100644 --- a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py +++ b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py @@ -49,20 +49,20 @@ class BoundedLoopsStrategy(BasicSearchStrategy): :return: Global state """ - state = self.super_strategy.get_strategic_global_state() + while True: - annotations = cast( - List[JumpdestCountAnnotation], - list(state.get_annotations(JumpdestCountAnnotation)), - ) + state = self.super_strategy.get_strategic_global_state() - if len(annotations) == 0: - annotation = JumpdestCountAnnotation() - state.annotate(annotation) - else: - annotation = annotations[0] + annotations = cast( + List[JumpdestCountAnnotation], + list(state.get_annotations(JumpdestCountAnnotation)), + ) - while True: + if len(annotations) == 0: + annotation = JumpdestCountAnnotation() + state.annotate(annotation) + else: + annotation = annotations[0] address = state.get_current_instruction()["address"] @@ -73,7 +73,6 @@ class BoundedLoopsStrategy(BasicSearchStrategy): if annotation._reached_count[address] > self.bound: log.info("Loop bound reached, skipping state") - state = self.super_strategy.get_strategic_global_state() continue return state From 42f2a5dede79d1223b2512e45d6ec1ecffa73968 Mon Sep 17 00:00:00 2001 From: Bernhard Mueller Date: Wed, 26 Jun 2019 11:10:55 +0200 Subject: [PATCH 3/3] Change log level of debug msg --- mythril/laser/ethereum/strategy/extensions/bounded_loops.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py index f312516c..74762c2a 100644 --- a/mythril/laser/ethereum/strategy/extensions/bounded_loops.py +++ b/mythril/laser/ethereum/strategy/extensions/bounded_loops.py @@ -72,7 +72,7 @@ class BoundedLoopsStrategy(BasicSearchStrategy): annotation._reached_count[address] = 1 if annotation._reached_count[address] > self.bound: - log.info("Loop bound reached, skipping state") + log.debug("Loop bound reached, skipping state") continue return state