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

Portyng symbolic name formating to the new svm and instructions file structure

Browse Source
pull/310/head
Konrad Weiss 6 years ago
parent 45b08081d3
commit b1d1127841
1 changed files with 27 additions and 20 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. 47
      mythril/laser/ethereum/instructions.py

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

@ -157,7 +157,7 @@ class Instruction:
result = Concat(BitVecVal(0, 248), Extract(offset + 7, offset, op1)) result = Concat(BitVecVal(0, 248), Extract(offset + 7, offset, op1))
except AttributeError: except AttributeError:
logging.debug("BYTE: Unsupported symbolic byte offset") logging.debug("BYTE: Unsupported symbolic byte offset")
result = BitVec(str(simplify(op1)) + "_" + str(simplify(op0)), 256) result = BitVec(str(simplify(op1)) + "[" + str(simplify(op0)) + "]", 256)
mstate.stack.append(simplify(result)) mstate.stack.append(simplify(result))
return [global_state] return [global_state]
@ -219,7 +219,7 @@ class Instruction:
base, exponent = util.pop_bitvec(state), util.pop_bitvec(state) base, exponent = util.pop_bitvec(state), util.pop_bitvec(state)
if (type(base) != BitVecNumRef) or (type(exponent) != BitVecNumRef): if (type(base) != BitVecNumRef) or (type(exponent) != BitVecNumRef):
state.stack.append(BitVec(str(base) + "_EXP_" + str(exponent), 256)) state.stack.append(BitVec("(" + str(simplify(base)) + ")^(" + str(simplify(exponent)) + ")", 256))
elif base.as_long() == 2: elif base.as_long() == 2:
if exponent.as_long() == 0: if exponent.as_long() == 0:
state.stack.append(BitVecVal(1, 256)) state.stack.append(BitVecVal(1, 256))
@ -330,13 +330,13 @@ class Instruction:
b = environment.calldata[offset] b = environment.calldata[offset]
except AttributeError: except AttributeError:
logging.debug("CALLDATALOAD: Unsupported symbolic index") logging.debug("CALLDATALOAD: Unsupported symbolic index")
state.stack.append( state.stack.append(BitVec(
BitVec("calldata_" + str(environment.active_account.contract_name) + "_" + str(op0), 256)) "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
return [global_state] return [global_state]
except IndexError: except IndexError:
logging.debug("Calldata not set, using symbolic variable instead") logging.debug("Calldata not set, using symbolic variable instead")
state.stack.append( state.stack.append(BitVec(
BitVec("calldata_" + str(environment.active_account.contract_name) + "_" + str(op0), 256)) "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
return [global_state] return [global_state]
if type(b) == int: if type(b) == int:
@ -350,12 +350,12 @@ class Instruction:
state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256)) state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256))
# FIXME: broad exception catch # FIXME: broad exception catch
except: except:
state.stack.append( state.stack.append(BitVec(
BitVec("calldata_" + str(environment.active_account.contract_name) + "_" + str(op0), 256)) "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
else: else:
# symbolic variable # symbolic variable
state.stack.append( state.stack.append(BitVec(
BitVec("calldata_" + str(environment.active_account.contract_name) + "_" + str(op0), 256)) "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
return [global_state] return [global_state]
@ -382,24 +382,29 @@ class Instruction:
logging.debug("Unsupported symbolic memory offset in CALLDATACOPY") logging.debug("Unsupported symbolic memory offset in CALLDATACOPY")
return [global_state] return [global_state]
dstart_sym = False
try: try:
dstart = util.get_concrete_int(op1) dstart = util.get_concrete_int(op1)
dstart_sym = True
# FIXME: broad exception catch # FIXME: broad exception catch
except: except:
logging.debug("Unsupported symbolic calldata offset in CALLDATACOPY") logging.debug("Unsupported symbolic calldata offset in CALLDATACOPY")
state.mem_extend(mstart, 1) dstart = simplify(op1)
state.memory[mstart] = BitVec("calldata_" + str(environment.active_account.contract_name) + "_cpy",
256)
return [global_state]
size_sym = False
try: try:
size = util.get_concrete_int(op2) size = util.get_concrete_int(op2)
size_sym = True
# FIXME: broad exception catch # FIXME: broad exception catch
except: except:
logging.debug("Unsupported symbolic size in CALLDATACOPY") logging.debug("Unsupported symbolic size in CALLDATACOPY")
size = simplify(op2)
if dstart_sym or size_sym:
state.mem_extend(mstart, 1) state.mem_extend(mstart, 1)
state.memory[mstart] = BitVec( state.memory[mstart] = BitVec(
"calldata_" + str(environment.active_account.contract_name) + "_" + str(dstart), 256) "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
size) + "]", 256)
return [global_state] return [global_state]
if size > 0: if size > 0:
@ -410,7 +415,8 @@ class Instruction:
logging.debug("Memory allocation error: mstart = " + str(mstart) + ", size = " + str(size)) logging.debug("Memory allocation error: mstart = " + str(mstart) + ", size = " + str(size))
state.mem_extend(mstart, 1) state.mem_extend(mstart, 1)
state.memory[mstart] = BitVec( state.memory[mstart] = BitVec(
"calldata_" + str(environment.active_account.contract_name) + "_" + str(dstart), 256) "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
size) + "]", 256)
return [global_state] return [global_state]
try: try:
@ -423,7 +429,8 @@ class Instruction:
logging.debug("Exception copying calldata to memory") logging.debug("Exception copying calldata to memory")
state.memory[mstart] = BitVec( state.memory[mstart] = BitVec(
"calldata_" + str(environment.active_account.contract_name) + "_" + str(dstart), 256) "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
size) + "]", 256)
return [global_state] return [global_state]
# Environment # Environment
@ -474,7 +481,7 @@ class Instruction:
# FIXME: broad exception catch # FIXME: broad exception catch
except: except:
# Can't access symbolic memory offsets # Can't access symbolic memory offsets
state.stack.append(BitVec("KECCAC_mem_" + str(op0) + ")", 256)) state.stack.append(BitVec("KECCAC_mem[" + str(simplify(op0)) + "]", 256))
return [global_state] return [global_state]
try: try:
@ -590,14 +597,14 @@ class Instruction:
offset = util.get_concrete_int(op0) offset = util.get_concrete_int(op0)
except AttributeError: except AttributeError:
logging.debug("Can't MLOAD from symbolic index") logging.debug("Can't MLOAD from symbolic index")
data = BitVec("mem_" + str(op0), 256) data = BitVec("mem[" + str(simplify(op0)) + "]", 256)
state.stack.append(data) state.stack.append(data)
return [global_state] return [global_state]
try: try:
data = util.concrete_int_from_bytes(state.memory, offset) data = util.concrete_int_from_bytes(state.memory, offset)
except IndexError: # Memory slot not allocated except IndexError: # Memory slot not allocated
data = BitVec("mem_" + str(offset), 256) data = BitVec("mem[" + str(offset) + "]", 256)
except TypeError: # Symbolic memory except TypeError: # Symbolic memory
data = state.memory[offset] data = state.memory[offset]

Write Preview
Loading…
Cancel
Save