|
|
|
@ -175,7 +175,7 @@ class Instruction: |
|
|
|
|
result = simplify(Concat(BitVecVal(0, 248), Extract(offset + 7, offset, op1))) |
|
|
|
|
else: |
|
|
|
|
result = 0 |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("BYTE: Unsupported symbolic byte offset") |
|
|
|
|
result = global_state.new_bitvec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256) |
|
|
|
|
|
|
|
|
@ -265,6 +265,8 @@ class Instruction: |
|
|
|
|
try: |
|
|
|
|
s0 = util.get_concrete_int(s0) |
|
|
|
|
s1 = util.get_concrete_int(s1) |
|
|
|
|
except TypeError: |
|
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
if s0 <= 31: |
|
|
|
|
testbit = s0 * 8 + 7 |
|
|
|
@ -274,9 +276,6 @@ class Instruction: |
|
|
|
|
state.stack.append(s1 & ((1 << testbit) - 1)) |
|
|
|
|
else: |
|
|
|
|
state.stack.append(s1) |
|
|
|
|
# TODO: broad exception handler |
|
|
|
|
except: |
|
|
|
|
return [] |
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
@ -356,7 +355,7 @@ class Instruction: |
|
|
|
|
try: |
|
|
|
|
offset = util.get_concrete_int(simplify(op0)) |
|
|
|
|
b = environment.calldata[offset] |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("CALLDATALOAD: Unsupported symbolic index") |
|
|
|
|
state.stack.append(global_state.new_bitvec( |
|
|
|
|
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256)) |
|
|
|
@ -368,16 +367,15 @@ class Instruction: |
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
if type(b) == int: |
|
|
|
|
val = b'' |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
for i in range(offset, offset + 32): |
|
|
|
|
val += environment.calldata[i].to_bytes(1, byteorder='big') |
|
|
|
|
val = b''.join([calldata.to_bytes(1, byteorder='big') for calldata in |
|
|
|
|
environment.calldata[offset:offset+32]]) |
|
|
|
|
|
|
|
|
|
logging.debug("Final value: " + str(int.from_bytes(val, byteorder='big'))) |
|
|
|
|
state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256)) |
|
|
|
|
# FIXME: broad exception catch |
|
|
|
|
except: |
|
|
|
|
|
|
|
|
|
except (TypeError, AttributeError): |
|
|
|
|
state.stack.append(global_state.new_bitvec( |
|
|
|
|
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256)) |
|
|
|
|
else: |
|
|
|
@ -405,16 +403,14 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
mstart = util.get_concrete_int(op0) |
|
|
|
|
# FIXME: broad exception catch |
|
|
|
|
except: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Unsupported symbolic memory offset in CALLDATACOPY") |
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
dstart_sym = False |
|
|
|
|
try: |
|
|
|
|
dstart = util.get_concrete_int(op1) |
|
|
|
|
# FIXME: broad exception catch |
|
|
|
|
except: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Unsupported symbolic calldata offset in CALLDATACOPY") |
|
|
|
|
dstart = simplify(op1) |
|
|
|
|
dstart_sym = True |
|
|
|
@ -422,8 +418,7 @@ class Instruction: |
|
|
|
|
size_sym = False |
|
|
|
|
try: |
|
|
|
|
size = util.get_concrete_int(op2) |
|
|
|
|
# FIXME: broad exception catch |
|
|
|
|
except: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Unsupported symbolic size in CALLDATACOPY") |
|
|
|
|
size = simplify(op2) |
|
|
|
|
size_sym = True |
|
|
|
@ -438,8 +433,7 @@ class Instruction: |
|
|
|
|
if size > 0: |
|
|
|
|
try: |
|
|
|
|
state.mem_extend(mstart, size) |
|
|
|
|
# FIXME: broad exception catch |
|
|
|
|
except: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Memory allocation error: mstart = " + str(mstart) + ", size = " + str(size)) |
|
|
|
|
state.mem_extend(mstart, 1) |
|
|
|
|
state.memory[mstart] = global_state.new_bitvec( |
|
|
|
@ -453,7 +447,7 @@ class Instruction: |
|
|
|
|
for i in range(mstart, mstart + size): |
|
|
|
|
state.memory[i] = environment.calldata[i_data] |
|
|
|
|
i_data += 1 |
|
|
|
|
except: |
|
|
|
|
except IndexError: |
|
|
|
|
logging.debug("Exception copying calldata to memory") |
|
|
|
|
|
|
|
|
|
state.memory[mstart] = global_state.new_bitvec( |
|
|
|
@ -508,8 +502,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
index, length = util.get_concrete_int(op0), util.get_concrete_int(op1) |
|
|
|
|
# FIXME: broad exception catch |
|
|
|
|
except: |
|
|
|
|
except TypeError: |
|
|
|
|
# Can't access symbolic memory offsets |
|
|
|
|
if is_expr(op0): |
|
|
|
|
op0 = simplify(op0) |
|
|
|
@ -521,7 +514,7 @@ class Instruction: |
|
|
|
|
data = b''.join([util.get_concrete_int(i).to_bytes(1, byteorder='big') |
|
|
|
|
for i in state.memory[index: index + length]]) |
|
|
|
|
|
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
argument = str(state.memory[index]).replace(" ", "_") |
|
|
|
|
|
|
|
|
|
result = BitVec("KECCAC[{}]".format(argument), 256) |
|
|
|
@ -546,14 +539,14 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
concrete_memory_offset = helper.get_concrete_int(memory_offset) |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Unsupported symbolic memory offset in CODECOPY") |
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
concrete_size = helper.get_concrete_int(size) |
|
|
|
|
global_state.mstate.mem_extend(concrete_memory_offset, concrete_size) |
|
|
|
|
except: |
|
|
|
|
except TypeError: |
|
|
|
|
# except both attribute error and Exception |
|
|
|
|
global_state.mstate.mem_extend(concrete_memory_offset, 1) |
|
|
|
|
global_state.mstate.memory[concrete_memory_offset] = \ |
|
|
|
@ -562,7 +555,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
concrete_code_offset = helper.get_concrete_int(code_offset) |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Unsupported symbolic code offset in CODECOPY") |
|
|
|
|
global_state.mstate.mem_extend(concrete_memory_offset, concrete_size) |
|
|
|
|
for i in range(concrete_size): |
|
|
|
@ -596,7 +589,7 @@ class Instruction: |
|
|
|
|
environment = global_state.environment |
|
|
|
|
try: |
|
|
|
|
addr = hex(helper.get_concrete_int(addr)) |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.info("unsupported symbolic address for EXTCODESIZE") |
|
|
|
|
state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256)) |
|
|
|
|
return [global_state] |
|
|
|
@ -670,7 +663,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
offset = util.get_concrete_int(op0) |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Can't MLOAD from symbolic index") |
|
|
|
|
data = global_state.new_bitvec("mem[" + str(simplify(op0)) + "]", 256) |
|
|
|
|
state.stack.append(data) |
|
|
|
@ -695,7 +688,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
mstart = util.get_concrete_int(op0) |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("MSTORE to symbolic index. Not supported") |
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
@ -708,17 +701,15 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
# Attempt to concretize value |
|
|
|
|
|
|
|
|
|
_bytes = util.concrete_int_to_bytes(value) |
|
|
|
|
|
|
|
|
|
i = 0 |
|
|
|
|
state.memory[mstart:mstart+len(_bytes)] = _bytes |
|
|
|
|
|
|
|
|
|
for b in _bytes: |
|
|
|
|
state.memory[mstart + i] = _bytes[i] |
|
|
|
|
i += 1 |
|
|
|
|
except: |
|
|
|
|
except (AttributeError, TypeError): |
|
|
|
|
try: |
|
|
|
|
state.memory[mstart] = value |
|
|
|
|
except: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Invalid memory access") |
|
|
|
|
|
|
|
|
|
return [global_state] |
|
|
|
@ -730,7 +721,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
offset = util.get_concrete_int(op0) |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("MSTORE to symbolic index. Not supported") |
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
@ -751,7 +742,7 @@ class Instruction: |
|
|
|
|
index = util.get_concrete_int(index) |
|
|
|
|
return self._sload_helper(global_state, index) |
|
|
|
|
|
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
if not keccak_function_manager.is_keccak(index): |
|
|
|
|
return self._sload_helper(global_state, str(index)) |
|
|
|
|
|
|
|
|
@ -813,7 +804,7 @@ class Instruction: |
|
|
|
|
try: |
|
|
|
|
index = util.get_concrete_int(index) |
|
|
|
|
return self._sstore_helper(global_state, index, value) |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
is_keccak = keccak_function_manager.is_keccak(index) |
|
|
|
|
if not is_keccak: |
|
|
|
|
return self._sstore_helper(global_state, str(index), value) |
|
|
|
@ -867,7 +858,7 @@ class Instruction: |
|
|
|
|
disassembly = global_state.environment.code |
|
|
|
|
try: |
|
|
|
|
jump_addr = util.get_concrete_int(state.stack.pop()) |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
raise InvalidJumpDestination("Invalid jump argument (symbolic address)") |
|
|
|
|
except IndexError: |
|
|
|
|
raise StackUnderflowException() |
|
|
|
@ -897,8 +888,7 @@ class Instruction: |
|
|
|
|
|
|
|
|
|
try: |
|
|
|
|
jump_addr = util.get_concrete_int(op0) |
|
|
|
|
# FIXME: to broad exception handler |
|
|
|
|
except: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Skipping JUMPI to invalid destination.") |
|
|
|
|
global_state.mstate.pc += 1 |
|
|
|
|
return [global_state] |
|
|
|
@ -978,7 +968,7 @@ class Instruction: |
|
|
|
|
return_data = [global_state.new_bitvec("return_data", 256)] |
|
|
|
|
try: |
|
|
|
|
return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)] |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Return with symbolic length or offset. Not supported") |
|
|
|
|
global_state.current_transaction.end(global_state, return_data) |
|
|
|
|
|
|
|
|
@ -1008,7 +998,7 @@ class Instruction: |
|
|
|
|
return_data = [global_state.new_bitvec("return_data", 256)] |
|
|
|
|
try: |
|
|
|
|
return_data = state.memory[util.get_concrete_int(offset):util.get_concrete_int(offset + length)] |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("Return with symbolic length or offset. Not supported") |
|
|
|
|
global_state.current_transaction.end(global_state, return_data=return_data, revert=True) |
|
|
|
|
|
|
|
|
@ -1052,7 +1042,7 @@ class Instruction: |
|
|
|
|
try: |
|
|
|
|
mem_out_start = helper.get_concrete_int(memory_out_offset) |
|
|
|
|
mem_out_sz = memory_out_size.as_long() |
|
|
|
|
except AttributeError: |
|
|
|
|
except TypeError: |
|
|
|
|
logging.debug("CALL with symbolic start or offset not supported") |
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
@ -1109,7 +1099,7 @@ class Instruction: |
|
|
|
|
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: |
|
|
|
|
except TypeError: |
|
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) |
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
@ -1177,7 +1167,7 @@ class Instruction: |
|
|
|
|
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: |
|
|
|
|
except TypeError: |
|
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) |
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
@ -1249,7 +1239,7 @@ class Instruction: |
|
|
|
|
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: |
|
|
|
|
except TypeError: |
|
|
|
|
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256)) |
|
|
|
|
return [global_state] |
|
|
|
|
|
|
|
|
|