Added returning global state to SIGNEXTEND opcode. (#1227)

* Added returning global state to SIGNEXTEND opcode.

* Add TODO statement.

* added new symbol instead

* hash s0
bug/invalid-loop-pruning
e-ngo 5 years ago committed by Nikhil Parasaram
parent b0e57b2768
commit a8a76b3da5
  1. 18
      mythril/laser/ethereum/instructions.py

@ -619,23 +619,29 @@ class Instruction:
:param global_state:
:return:
"""
state = global_state.mstate
s0, s1 = state.stack.pop(), state.stack.pop()
mstate = global_state.mstate
s0, s1 = mstate.stack.pop(), mstate.stack.pop()
try:
s0 = util.get_concrete_int(s0)
s1 = util.get_concrete_int(s1)
except TypeError:
return []
log.debug("Unsupported symbolic argument for SIGNEXTEND")
mstate.stack.append(
global_state.new_bitvec(
"SIGNEXTEND({},{})".format(hash(s0), hash(s1)), 256
)
)
return [global_state]
if s0 <= 31:
testbit = s0 * 8 + 7
if s1 & (1 << testbit):
state.stack.append(s1 | (TT256 - (1 << testbit)))
mstate.stack.append(s1 | (TT256 - (1 << testbit)))
else:
state.stack.append(s1 & ((1 << testbit) - 1))
mstate.stack.append(s1 & ((1 << testbit) - 1))
else:
state.stack.append(s1)
mstate.stack.append(s1)
return [global_state]

Loading…
Cancel
Save