Fix propagation of JumpdestCountAnnotation

fix/boundedloops
Nathan 5 years ago
parent a223219ab6
commit c465e14fb7
  1. 9
      mythril/laser/ethereum/strategy/extensions/bounded_loops.py

@ -3,7 +3,6 @@ from mythril.laser.ethereum.strategy.basic import BasicSearchStrategy
from mythril.laser.ethereum.state.annotation import StateAnnotation from mythril.laser.ethereum.state.annotation import StateAnnotation
from mythril.laser.ethereum.transaction import ContractCreationTransaction from mythril.laser.ethereum.transaction import ContractCreationTransaction
from typing import Dict, cast, List from typing import Dict, cast, List
from copy import copy
import logging import logging
@ -17,9 +16,7 @@ class JumpdestCountAnnotation(StateAnnotation):
self._reached_count = {} # type: Dict[str, int] self._reached_count = {} # type: Dict[str, int]
def __copy__(self): def __copy__(self):
result = JumpdestCountAnnotation() return self
result._reached_count = copy(self._reached_count)
return result
class BoundedLoopsStrategy(BasicSearchStrategy): class BoundedLoopsStrategy(BasicSearchStrategy):
@ -48,7 +45,6 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
:return: Global state :return: Global state
""" """
while True: while True:
state = self.super_strategy.get_strategic_global_state() state = self.super_strategy.get_strategic_global_state()
@ -60,6 +56,7 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
if len(annotations) == 0: if len(annotations) == 0:
annotation = JumpdestCountAnnotation() annotation = JumpdestCountAnnotation()
log.debug("Adding JumpdestCountAnnotation to GlobalState")
state.annotate(annotation) state.annotate(annotation)
else: else:
annotation = annotations[0] annotation = annotations[0]
@ -74,7 +71,7 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
cur_instr["opcode"], cur_instr["address"], state.mstate.prev_pc cur_instr["opcode"], cur_instr["address"], state.mstate.prev_pc
) )
if key in annotation._reached_count: if key in annotation._reached_count.keys():
annotation._reached_count[key] += 1 annotation._reached_count[key] += 1
else: else:
annotation._reached_count[key] = 1 annotation._reached_count[key] = 1

Loading…
Cancel
Save