Store a BitVec when an exception occurs

mythril/laser/ethereum/instructions.py

@@ -1,11 +1,11 @@
 import binascii
-import logging
+import logging,sys
 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, \
-    is_false
+    is_false, BitVecRef
 from z3 import BitVecVal, If, BoolRef
 
 import mythril.laser.ethereum.util as helper
@@ -899,11 +899,15 @@ class Instruction:
                 return [global_state]
 
             global_state.mstate.mem_extend(mem_out_start, mem_out_sz)
-            try:
-                for i in range(min(len(data), mem_out_sz)):  # If more data is used then it's chopped off
-                    global_state.mstate.memory[mem_out_start + i] = data[i]
-            except:
-                global_state.mstate.memory[mem_out_start] = BitVec(data, 256)
+            if type(data) == BitVecRef:
+                global_state.mstate.memory[mem_out_start] = data
+            else:
+                try:
+                    for i in range(min(len(data), mem_out_sz)):  # If more data is used then it's chopped off
+                        global_state.mstate.memory[mem_out_start + i] = data[i]
+                except:
+                    sys.stderr.write(str(data))
+                    global_state.mstate.memory[mem_out_start] = BitVec(data, 256)
 
             # TODO: maybe use BitVec here constrained to 1
             global_state.mstate.stack.append(BitVec("retval_" + str(instr['address']), 256))

mythril/laser/ethereum/natives.py

@@ -2,14 +2,16 @@
 
 import copy
 import hashlib
+import logging
 
 import coincurve
+from z3 import BitVec
 
 from py_ecc.secp256k1 import N as secp256k1n
 from mythril.laser.ethereum.util import ALL_BYTES, bytearray_to_int, concrete_int_to_bytes, sha3, zpad
 
 
-def int_to_32bytes(i):   #used because int can't fit as bytes function's input
+def int_to_32bytes(i):   # used because int can't fit as bytes function's input
     o = [0] * 32
     for x in range(32):
         o[31 - x] = i & 0xff
@@ -44,7 +46,7 @@ def ecrecover(data):
     try:
         data = bytearray(data)
     except TypeError:
-        return "ecrecover_"+str(data)
+        return BitVec("ecrecover_"+str(data), 256)
     message = b''.join(map(lambda x: ALL_BYTES[x], data[0:32]))
     v = extract32(data, 32)
     r = extract32(data, 64)
@@ -54,6 +56,7 @@ def ecrecover(data):
     try:
         pub = ecrecover_to_pub(message, v, r, s)
     except Exception as e:
+        logging.info("An error has been encountered while extracting public key: " + str(e))
         return []
     o = [0] * 12 + [x for x in sha3(pub)[-20:]]
     return o
@@ -63,7 +66,7 @@ def sha256(data):
     try:
         data = bytes(data)
     except TypeError:
-        return "sha256_"+str(data)
+        return BitVec("sha256_"+str(data), 256)
     return hashlib.sha256(data).digest()
 
 
@@ -71,7 +74,7 @@ def ripemd160(data):
     try:
         data = bytes(data)
     except TypeError:
-        return "ripemd160_"+str(data)
+        return BitVec("ripemd160_"+str(data), 256)
     return 12*[0]+[i for i in hashlib.new('ripemd160', data).digest()]