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

Modifies the symbolic suffixes enclosing them into brackets and symplifying them with the z3 simplification algorithm

Browse Source
pull/310/head
Konrad Weiss 6 years ago
parent dc0e93566a
commit 06ddeb13dc
1 changed files with 20 additions and 15 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. 35
      mythril/laser/ethereum/svm.py

35
mythril/laser/ethereum/svm.py
Unescape View File

@ -396,7 +396,7 @@ class LaserEVM:
result = Concat(BitVecVal(0, 248), Extract(oft + 7, oft, s1)) result = Concat(BitVecVal(0, 248), Extract(oft + 7, oft, s1))
except AttributeError: except AttributeError:
logging.debug("BYTE: Unsupported symbolic byte offset") logging.debug("BYTE: Unsupported symbolic byte offset")
result = BitVec(str(simplify(s1)) + "_" + str(simplify(s0)), 256) result = BitVec(str(simplify(s1)) + "[" + str(simplify(s0)) + "]", 256)
state.stack.append(simplify(result)) state.stack.append(simplify(result))
@ -442,7 +442,7 @@ class LaserEVM:
base, exponent = helper.pop_bitvec(state), helper.pop_bitvec(state) base, exponent = helper.pop_bitvec(state), helper.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))
@ -535,11 +535,11 @@ class LaserEVM:
except AttributeError: except AttributeError:
logging.debug("CALLDATALOAD: Unsupported symbolic index") logging.debug("CALLDATALOAD: Unsupported symbolic index")
state.stack.append(BitVec("calldata_" + str(environment.active_account.contract_name) + "_" + str(op0), 256)) state.stack.append(BitVec("calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
continue continue
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(BitVec("calldata_" + str(environment.active_account.contract_name) + "_" + str(op0), 256)) state.stack.append(BitVec("calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
continue continue
if type(b) == int: if type(b) == int:
@ -554,10 +554,10 @@ class LaserEVM:
state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256)) state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256))
except: except:
state.stack.append(BitVec("calldata_" + str(environment.active_account.contract_name) + "_" + str(op0), 256)) state.stack.append(BitVec("calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
else: else:
# symbolic variable # symbolic variable
state.stack.append(BitVec("calldata_" + str(environment.active_account.contract_name) + "_" + str(op0), 256)) state.stack.append(BitVec("calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
elif op == 'CALLDATASIZE': elif op == 'CALLDATASIZE':
@ -575,20 +575,25 @@ class LaserEVM:
logging.debug("Unsupported symbolic memory offset in CALLDATACOPY") logging.debug("Unsupported symbolic memory offset in CALLDATACOPY")
continue continue
dstart_sym = False
try: try:
dstart = helper.get_concrete_int(op1) dstart = helper.get_concrete_int(op1)
dstart_sym = True
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)
continue
size_sym = False
try: try:
size = helper.get_concrete_int(op2) size = helper.get_concrete_int(op2)
size_sym = True
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("calldata_" + str(environment.active_account.contract_name) + "_" + str(dstart), 256) state.memory[mstart] = BitVec("calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(size) + "]", 256)
continue continue
if size > 0: if size > 0:
@ -598,7 +603,7 @@ class LaserEVM:
except: except:
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("calldata_" + str(environment.active_account.contract_name) + "_" + str(dstart), 256) state.memory[mstart] = BitVec("calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(size) + "]", 256)
continue continue
try: try:
@ -610,7 +615,7 @@ class LaserEVM:
except: except:
logging.debug("Exception copying calldata to memory") logging.debug("Exception copying calldata to memory")
state.memory[mstart] = BitVec("calldata_" + str(environment.active_account.contract_name) + "_" + str(dstart), 256) state.memory[mstart] = BitVec("calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(size) + "]", 256)
elif op == 'STOP': elif op == 'STOP':
if len(self.call_stack): if len(self.call_stack):
@ -645,7 +650,7 @@ class LaserEVM:
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))
continue continue
try: try:
@ -717,14 +722,14 @@ class LaserEVM:
offset = helper.get_concrete_int(op0) offset = helper.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)
continue continue
try: try:
data = helper.concrete_int_from_bytes(state.memory, offset) data = helper.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