Added 'context' to loop annotations.

bug/invalid-loop-pruning
Eric Ngo 5 years ago
parent a8a76b3da5
commit 6f21b92796
  1. 24
      mythril/laser/ethereum/state/machine_state.py
  2. 20
      mythril/laser/ethereum/strategy/extensions/bounded_loops.py

@ -95,6 +95,7 @@ class MachineState:
depth=0, depth=0,
max_gas_used=0, max_gas_used=0,
min_gas_used=0, min_gas_used=0,
prev_pc=-1,
) -> None: ) -> None:
"""Constructor for machineState. """Constructor for machineState.
@ -106,8 +107,9 @@ class MachineState:
:param depth: :param depth:
:param max_gas_used: :param max_gas_used:
:param min_gas_used: :param min_gas_used:
:param prev_pc:
""" """
self.pc = pc self._pc = pc
self.stack = MachineStack(stack) self.stack = MachineStack(stack)
self.memory = memory or Memory() self.memory = memory or Memory()
self.gas_limit = gas_limit self.gas_limit = gas_limit
@ -115,6 +117,7 @@ class MachineState:
self.max_gas_used = max_gas_used # upper gas usage bound self.max_gas_used = max_gas_used # upper gas usage bound
self.constraints = constraints or Constraints() self.constraints = constraints or Constraints()
self.depth = depth self.depth = depth
self.prev_pc = prev_pc # holds context of current pc
def calculate_extension_size(self, start: int, size: int) -> int: def calculate_extension_size(self, start: int, size: int) -> int:
""" """
@ -210,11 +213,12 @@ class MachineState:
gas_limit=self.gas_limit, gas_limit=self.gas_limit,
max_gas_used=self.max_gas_used, max_gas_used=self.max_gas_used,
min_gas_used=self.min_gas_used, min_gas_used=self.min_gas_used,
pc=self.pc, pc=self._pc,
stack=copy(self.stack), stack=copy(self.stack),
memory=copy(self.memory), memory=copy(self.memory),
constraints=copy(self.constraints), constraints=copy(self.constraints),
depth=self.depth, depth=self.depth,
prev_pc=self.prev_pc,
) )
def __str__(self): def __str__(self):
@ -224,6 +228,19 @@ class MachineState:
""" """
return str(self.as_dict) return str(self.as_dict)
@property
def pc(self) -> int:
"""
:return:
"""
return self._pc
@pc.setter
def pc(self, value):
self.prev_pc = self._pc
self._pc = value
@property @property
def memory_size(self) -> int: def memory_size(self) -> int:
""" """
@ -239,11 +256,12 @@ class MachineState:
:return: :return:
""" """
return dict( return dict(
pc=self.pc, pc=self._pc,
stack=self.stack, stack=self.stack,
memory=self.memory, memory=self.memory,
memsize=self.memory_size, memsize=self.memory_size,
gas=self.gas_limit, gas=self.gas_limit,
max_gas_used=self.max_gas_used, max_gas_used=self.max_gas_used,
min_gas_used=self.min_gas_used, min_gas_used=self.min_gas_used,
prev_pc=self.prev_pc,
) )

@ -64,22 +64,30 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
else: else:
annotation = annotations[0] annotation = annotations[0]
address = state.get_current_instruction()["address"] cur_instr = state.get_current_instruction()
if address in annotation._reached_count: if cur_instr["opcode"].upper() != "JUMPDEST":
annotation._reached_count[address] += 1 return state
# create unique instruction identifier
key = "{}{}{}".format(
cur_instr["opcode"], cur_instr["address"], state.mstate.prev_pc
)
if key in annotation._reached_count:
annotation._reached_count[key] += 1
else: else:
annotation._reached_count[address] = 1 annotation._reached_count[key] = 1
# The creation transaction gets a higher loop bound to give it a better chance of success. # The creation transaction gets a higher loop bound to give it a better chance of success.
# TODO: There's probably a nicer way to do this # TODO: There's probably a nicer way to do this
if isinstance( if isinstance(
state.current_transaction, ContractCreationTransaction state.current_transaction, ContractCreationTransaction
) and annotation._reached_count[address] < max(8, self.bound): ) and annotation._reached_count[key] < max(8, self.bound):
return state return state
elif annotation._reached_count[address] > self.bound: elif annotation._reached_count[key] > self.bound:
log.debug("Loop bound reached, skipping state") log.debug("Loop bound reached, skipping state")
continue continue

Loading…
Cancel
Save