In the current setting, an abstract state tracks values of PUSHk instructions. In order to track jump destinations we may only track push argument that are JUMPDESTs, otherwise they cannot be target of jumps.
Why is this important?
In #25 we want to make sure that two states that differ on stack values that are not JUMPDESTs are considered equivalent.
It is easier then to track JUMPDESTs and otherwise use a Random() value. If it is not a JUMPDEST it cannot eve a JUMP target so we can safely ignore it.
To do
There is already a function to collect the JUMPDESTs in the code, so this is a matter of making available to the NextState function. The PUSHk instructions should only be tracked if they push a JUMPDEST, otherwise, we can push a Random() value.
In the current setting, an abstract state tracks values of
PUSHkinstructions. In order to track jump destinations we may only track push argument that are JUMPDESTs, otherwise they cannot be target of jumps. Why is this important? In #25 we want to make sure that two states that differ on stack values that are not JUMPDESTs are considered equivalent. It is easier then to track JUMPDESTs and otherwise use aRandom()value. If it is not a JUMPDEST it cannot eve a JUMP target so we can safely ignore it.To do
There is already a function to collect the JUMPDESTs in the code, so this is a matter of making available to the
NextStatefunction. ThePUSHkinstructions should only be tracked if they push a JUMPDEST, otherwise, we can push aRandom()value.