diff --git a/mythril/laser/ethereum/instructions.py b/mythril/laser/ethereum/instructions.py index 19c54d1d..55ea9b3f 100644 --- a/mythril/laser/ethereum/instructions.py +++ b/mythril/laser/ethereum/instructions.py @@ -547,11 +547,15 @@ class Instruction: state.stack.append( global_state.new_bitvec( - "(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")", + "invhash(" + + str(hash(simplify(base))) + + ")**invhash(" + + str(hash(simplify(exponent))) + + ")", 256, base.annotations + exponent.annotations, ) - ) + ) # Hash is used because str(symbol) takes a long time to be converted to a string else: state.stack.append( @@ -1311,21 +1315,19 @@ class Instruction: state = global_state.mstate op0 = state.stack.pop() - log.debug("MLOAD[" + str(op0) + "]") - try: offset = util.get_concrete_int(op0) except TypeError: log.debug("Can't MLOAD from symbolic index") - data = global_state.new_bitvec("mem[" + str(simplify(op0)) + "]", 256) + data = global_state.new_bitvec( + "mem[invhash(" + str(hash(simplify(op0))) + ")]", 256 + ) state.stack.append(data) return [global_state] state.mem_extend(offset, 32) data = state.memory.get_word_at(offset) - log.debug("Load from memory[" + str(offset) + "]: " + str(data)) - state.stack.append(data) return [global_state] @@ -1348,9 +1350,7 @@ class Instruction: try: state.mem_extend(mstart, 32) except Exception: - log.debug("Error extending memory, mstart = " + str(mstart) + ", size = 32") - - log.debug("MSTORE to mem[" + str(mstart) + "]: " + str(value)) + log.debug("Error extending memory") state.memory.write_word_at(mstart, value)