From 01bf9ca81237dc90e4707f16b1c43a553d15a151 Mon Sep 17 00:00:00 2001 From: Joran Honig Date: Mon, 6 Aug 2018 12:43:31 +0200 Subject: [PATCH] Add concretization --- mythril/laser/ethereum/instructions.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 86a485c3..7801a04c 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -1042,6 +1042,13 @@ class Instruction: return [global_state] + try: + memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, ExprRef) else memory_out_offset + memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, ExprRef) else memory_out_size + except AttributeError: + global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + return [global_state] + # Copy memory global_state.mstate.mem_extend(memory_out_offset, min(memory_out_size.as_long(), len(global_state.last_return_data))) for i in range(min(memory_out_size.as_long(), len(global_state.last_return_data))): @@ -1105,6 +1112,15 @@ class Instruction: return [global_state] + try: + memory_out_offset = util.get_concrete_int(memory_out_offset) if isinstance(memory_out_offset, + ExprRef) else memory_out_offset + memory_out_size = util.get_concrete_int(memory_out_size) if isinstance(memory_out_size, + ExprRef) else memory_out_size + except AttributeError: + global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256)) + return [global_state] + # Copy memory global_state.mstate.mem_extend(memory_out_offset, min(memory_out_size.as_long(), len(global_state.last_return_data)))