TheDude
/
mythril
mirror of https://github.com/ConsenSys/mythril
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Use global_state.new_bitvec vs directly initializing the bitvector

Browse Source
pull/485/head
Joran Honig 6 years ago
parent c62067ba30
commit bcc90a27f2
1 changed files with 56 additions and 55 deletions
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Show Stats Download Patch File Download Diff File
  1. 111
      mythril/laser/ethereum/instructions.py

111
mythril/laser/ethereum/instructions.py
Unescape View File

@ -4,7 +4,7 @@ from copy import copy, deepcopy
import ethereum.opcodes as opcodes
from ethereum import utils
from z3 import BitVec, Extract, UDiv, simplify, Concat, ULT, UGT, BitVecNumRef, Not, \
from z3 import Extract, UDiv, simplify, Concat, ULT, UGT, BitVecNumRef, Not, \
is_false, is_expr, ExprRef, URem, SRem
from z3 import BitVecVal, If, BoolRef
@ -159,7 +159,7 @@ class Instruction:
result = Concat(BitVecVal(0, 248), Extract(offset + 7, offset, op1))
except AttributeError:
logging.debug("BYTE: Unsupported symbolic byte offset")
result = BitVec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256)
result = global_state.new_bitvec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256)
mstate.stack.append(simplify(result))
return [global_state]
@ -233,7 +233,7 @@ class Instruction:
base, exponent = util.pop_bitvec(state), util.pop_bitvec(state)
if (type(base) != BitVecNumRef) or (type(exponent) != BitVecNumRef):
state.stack.append(BitVec("(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", 256))
state.stack.append(global_state.new_bitvec("(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", 256))
else:
state.stack.append(pow(base.as_long(), exponent.as_long(), 2**256))
@ -340,13 +340,13 @@ class Instruction:
b = environment.calldata[offset]
except AttributeError:
logging.debug("CALLDATALOAD: Unsupported symbolic index")
state.stack.append(BitVec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
state.stack.append(global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + str(len(global_state.current_transaction.caller)) +"[" + str(simplify(op0)) + "]", 256))
return [global_state]
except IndexError:
logging.debug("Calldata not set, using symbolic variable instead")
state.stack.append(BitVec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
state.stack.append(global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) +str(global_state.current_transaction.caller)+ "[" + str(simplify(op0)) + "]", 256))
return [global_state]
if type(b) == int:
@ -360,11 +360,11 @@ class Instruction:
state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256))
# FIXME: broad exception catch
except:
state.stack.append(BitVec(
state.stack.append(global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
else:
# symbolic variable
state.stack.append(BitVec(
state.stack.append(global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
return [global_state]
@ -374,7 +374,7 @@ class Instruction:
state = global_state.mstate
environment = global_state.environment
if environment.calldata_type == CalldataType.SYMBOLIC:
state.stack.append(BitVec("calldatasize_" + environment.active_account.contract_name, 256))
state.stack.append(global_state.new_bitvec("calldatasize_" + environment.active_account.contract_name, 256))
else:
state.stack.append(BitVecVal(len(environment.calldata), 256))
return [global_state]
@ -412,7 +412,7 @@ class Instruction:
if dstart_sym or size_sym:
state.mem_extend(mstart, 1)
state.memory[mstart] = BitVec(
state.memory[mstart] = global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
size) + "]", 256)
return [global_state]
@ -424,7 +424,7 @@ class Instruction:
except:
logging.debug("Memory allocation error: mstart = " + str(mstart) + ", size = " + str(size))
state.mem_extend(mstart, 1)
state.memory[mstart] = BitVec(
state.memory[mstart] = global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
size) + "]", 256)
return [global_state]
@ -438,7 +438,7 @@ class Instruction:
except:
logging.debug("Exception copying calldata to memory")
state.memory[mstart] = BitVec(
state.memory[mstart] = global_state.new_bitvec(
"calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
size) + "]", 256)
return [global_state]
@ -455,7 +455,7 @@ class Instruction:
def balance_(self, global_state):
state = global_state.mstate
address = state.stack.pop()
state.stack.append(BitVec("balance_at_" + str(address), 256))
state.stack.append(global_state.new_bitvec("balance_at_" + str(address), 256))
return [global_state]
@instruction
@ -493,7 +493,7 @@ class Instruction:
# Can't access symbolic memory offsets
if is_expr(op0):
op0 = simplify(op0)
state.stack.append(BitVec("KECCAC_mem[" + str(op0) + "]", 256))
state.stack.append(global_state.new_bitvec("KECCAC_mem[" + str(op0) + "]", 256))
return [global_state]
try:
@ -509,7 +509,7 @@ class Instruction:
svar = svar.replace(" ", "_")
state.stack.append(BitVec("keccac_" + svar, 256))
state.stack.append(global_state.new_bitvec("keccac_" + svar, 256))
return [global_state]
keccac = utils.sha3(utils.bytearray_to_bytestr(data))
@ -520,7 +520,7 @@ class Instruction:
@instruction
def gasprice_(self, global_state):
global_state.mstate.stack.append(BitVec("gasprice", 256))
global_state.mstate.stack.append(global_state.new_bitvec("gasprice", 256))
return [global_state]
@instruction
@ -540,7 +540,7 @@ class Instruction:
# except both attribute error and Exception
global_state.mstate.mem_extend(concrete_memory_offset, 1)
global_state.mstate.memory[concrete_memory_offset] = \
BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
return [global_state]
try:
@ -550,7 +550,7 @@ class Instruction:
global_state.mstate.mem_extend(concrete_memory_offset, concrete_size)
for i in range(concrete_size):
global_state.mstate.memory[concrete_memory_offset + i] = \
BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
return [global_state]
bytecode = global_state.environment.code.bytecode
@ -559,7 +559,7 @@ class Instruction:
if concrete_code_offset >= len(global_state.environment.code.bytecode) // 2:
global_state.mstate.mem_extend(concrete_memory_offset, 1)
global_state.mstate.memory[concrete_memory_offset] = \
BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
return [global_state]
for i in range(concrete_size):
@ -568,7 +568,7 @@ class Instruction:
int(bytecode[2*(concrete_code_offset + i): 2*(concrete_code_offset + i + 1)], 16)
else:
global_state.mstate.memory[concrete_memory_offset + i] = \
BitVec("code({})".format(global_state.environment.active_account.contract_name), 256)
global_state.new_bitvec("code({})".format(global_state.environment.active_account.contract_name), 256)
return [global_state]
@ -581,14 +581,14 @@ class Instruction:
addr = hex(helper.get_concrete_int(addr))
except AttributeError:
logging.info("unsupported symbolic address for EXTCODESIZE")
state.stack.append(BitVec("extcodesize_" + str(addr), 256))
state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
return [global_state]
try:
code = self.dynamic_loader.dynld(environment.active_account.address, addr)
except Exception as e:
logging.info("error accessing contract storage due to: " + str(e))
state.stack.append(BitVec("extcodesize_" + str(addr), 256))
state.stack.append(global_state.new_bitvec("extcodesize_" + str(addr), 256))
return [global_state]
if code is None:
@ -608,39 +608,39 @@ class Instruction:
@instruction
def returndatasize_(self, global_state):
global_state.mstate.stack.append(BitVec("returndatasize", 256))
global_state.mstate.stack.append(global_state.new_bitvec("returndatasize", 256))
return [global_state]
@instruction
def blockhash_(self, global_state):
state = global_state.mstate
blocknumber = state.stack.pop()
state.stack.append(BitVec("blockhash_block_" + str(blocknumber), 256))
state.stack.append(global_state.new_bitvec("blockhash_block_" + str(blocknumber), 256))
return [global_state]
@instruction
def coinbase_(self, global_state):
global_state.mstate.stack.append(BitVec("coinbase", 256))
global_state.mstate.stack.append(global_state.new_bitvec("coinbase", 256))
return [global_state]
@instruction
def timestamp_(self, global_state):
global_state.mstate.stack.append(BitVec("timestamp", 256))
global_state.mstate.stack.append(global_state.new_bitvec("timestamp", 256))
return [global_state]
@instruction
def number_(self, global_state):
global_state.mstate.stack.append(BitVec("block_number", 256))
global_state.mstate.stack.append(global_state.new_bitvec("block_number", 256))
return [global_state]
@instruction
def difficulty_(self, global_state):
global_state.mstate.stack.append(BitVec("block_difficulty", 256))
global_state.mstate.stack.append(global_state.new_bitvec("block_difficulty", 256))
return [global_state]
@instruction
def gaslimit_(self, global_state):
global_state.mstate.stack.append(BitVec("block_gaslimit", 256))
global_state.mstate.stack.append(global_state.new_bitvec("block_gaslimit", 256))
return [global_state]
# Memory operations
@ -655,14 +655,14 @@ class Instruction:
offset = util.get_concrete_int(op0)
except AttributeError:
logging.debug("Can't MLOAD from symbolic index")
data = BitVec("mem[" + str(simplify(op0)) + "]", 256)
data = global_state.new_bitvec("mem[" + str(simplify(op0)) + "]", 256)
state.stack.append(data)
return [global_state]
try:
data = util.concrete_int_from_bytes(state.memory, offset)
except IndexError: # Memory slot not allocated
data = BitVec("mem[" + str(offset) + "]", 256)
data = global_state.new_bitvec("mem[" + str(offset) + "]", 256)
except TypeError: # Symbolic memory
data = state.memory[offset]
@ -739,7 +739,7 @@ class Instruction:
try:
data = global_state.environment.active_account.storage[index]
except KeyError:
data = BitVec("storage_" + str(index), 256)
data = global_state.new_bitvec("storage_" + str(index), 256)
global_state.environment.active_account.storage[index] = data
state.stack.append(data)
@ -762,7 +762,7 @@ class Instruction:
global_state.accounts[
global_state.environment.active_account.address] = global_state.environment.active_account
global_state.environment.active_account.storage[index] = value
global_state.environment.active_account.storage[index] = simplify(value)
except KeyError:
logging.debug("Error writing to storage: Invalid index")
return [global_state]
@ -853,12 +853,12 @@ class Instruction:
@instruction
def msize_(self, global_state):
global_state.mstate.stack.append(BitVec("msize", 256))
global_state.mstate.stack.append(global_state.new_bitvec("msize", 256))
return [global_state]
@instruction
def gas_(self, global_state):
global_state.mstate.stack.append(BitVec("gas", 256))
global_state.mstate.stack.append(global_state.new_bitvec("gas", 256))
return [global_state]
@instruction
@ -884,7 +884,7 @@ class Instruction:
def return_(self, global_state):
state = global_state.mstate
offset, length = state.stack.pop(), state.stack.pop()
return_data = [BitVec("return_data", 256)]
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:
@ -924,9 +924,9 @@ class Instruction:
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
# TODO: decide what to do in this case
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
if 0 < int(callee_address, 16) < 5:
logging.info("Native contract called: " + callee_address)
@ -948,7 +948,7 @@ class Instruction:
except natives.NativeContractException:
contract_list = ['ecerecover', 'sha256', 'ripemd160', 'identity']
for i in range(mem_out_sz):
global_state.mstate.memory[mem_out_start + i] = BitVec(contract_list[call_address_int - 1] +
global_state.mstate.memory[mem_out_start + i] = global_state.new_bitvec(contract_list[call_address_int - 1] +
"(" + str(call_data) + ")", 256)
return [global_state]
@ -980,12 +980,12 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
if global_state.last_return_data is None:
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 0)
@ -995,7 +995,7 @@ class Instruction:
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))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
# Copy memory
@ -1004,7 +1004,7 @@ class Instruction:
global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i]
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 1)
@ -1022,7 +1022,7 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
transaction = MessageCallTransaction(global_state.world_state,
@ -1048,12 +1048,12 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
if global_state.last_return_data is None:
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 0)
@ -1063,7 +1063,7 @@ class Instruction:
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))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
# Copy memory
@ -1072,7 +1072,7 @@ class Instruction:
global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i]
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 1)
@ -1091,7 +1091,7 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
transaction = MessageCallTransaction(global_state.world_state,
@ -1118,12 +1118,12 @@ class Instruction:
logging.info(
"Could not determine required parameters for call, putting fresh symbol on the stack. \n{}".format(e)
)
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
if global_state.last_return_data is None:
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 0)
@ -1135,7 +1135,7 @@ class Instruction:
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))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]
# Copy memory
@ -1145,7 +1145,7 @@ class Instruction:
global_state.mstate.memory[i + memory_out_offset] = global_state.last_return_data[i]
# Put return value on stack
return_value = BitVec("retval_" + str(instr['address']), 256)
return_value = global_state.new_bitvec("retval_" + str(instr['address']), 256)
global_state.mstate.stack.append(return_value)
global_state.mstate.constraints.append(return_value == 1)
@ -1155,5 +1155,6 @@ class Instruction:
def staticcall_(self, global_state):
# TODO: implement me
instr = global_state.get_current_instruction()
global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))
global_state.mstate.stack.append(global_state.new_bitvec("retval_" + str(instr['address']), 256))
return [global_state]

Write Preview
Loading…
Cancel
Save