|
|
@ -36,9 +36,9 @@ def instruction(func): |
|
|
|
for state in new_global_states: |
|
|
|
for state in new_global_states: |
|
|
|
state.mstate.pc += 1 |
|
|
|
state.mstate.pc += 1 |
|
|
|
return new_global_states |
|
|
|
return new_global_states |
|
|
|
|
|
|
|
|
|
|
|
return wrapper |
|
|
|
return wrapper |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
class Instruction: |
|
|
|
class Instruction: |
|
|
|
""" |
|
|
|
""" |
|
|
|
Instruction class is used to mutate a state according to the current instruction |
|
|
|
Instruction class is used to mutate a state according to the current instruction |
|
|
@ -830,17 +830,13 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
|
|
@instruction |
|
|
|
@instruction |
|
|
|
def return_(self, global_state): |
|
|
|
def return_(self, global_state): |
|
|
|
# return [] |
|
|
|
|
|
|
|
state = global_state.mstate |
|
|
|
state = global_state.mstate |
|
|
|
offset, length = state.stack.pop(), state.stack.pop() |
|
|
|
offset, length = state.stack.pop(), state.stack.pop() |
|
|
|
return_data = None |
|
|
|
return_data = [BitVec("return_data", 256)] |
|
|
|
|
|
|
|
|
|
|
|
try: |
|
|
|
try: |
|
|
|
return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)] |
|
|
|
return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)] |
|
|
|
except AttributeError: |
|
|
|
except AttributeError: |
|
|
|
logging.debug("Return with symbolic length or offset. Not supported") |
|
|
|
logging.debug("Return with symbolic length or offset. Not supported") |
|
|
|
global_state.current_transaction.end(global_state, [BitVec("return_data", 256)]) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
global_state.current_transaction.end(global_state, return_data) |
|
|
|
global_state.current_transaction.end(global_state, return_data) |
|
|
|
|
|
|
|
|
|
|
|
@instruction |
|
|
|
@instruction |
|
|
@ -937,7 +933,7 @@ class Instruction: |
|
|
|
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
|
|
if global_state.last_return_data is None: |
|
|
|
if global_state.last_return_data is None or True: |
|
|
|
# TODO: set to 0 |
|
|
|
# TODO: set to 0 |
|
|
|
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) |
|
|
|
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) |
|
|
|
return [global_state] |
|
|
|
return [global_state] |
|
|
|