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

Merge pull request #310 from LoCorVin/feature/reformatsymindices

Browse Source 
Modifies the symbolic suffixes enclosing them into brackets and sympl…
pull/339/head
Nikhil Parasaram 6 years ago committed by GitHub
parent e57ef0d361 704307890a
commit b9414cafcd
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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)
# 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", dstart_sym = True
256)
return [global_state]
size_sym = False
try: try:
size = util.get_concrete_int(op2) size = util.get_concrete_int(op2)
# 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)
size_sym = True
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:
@ -594,14 +601,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