improved symbolic calldata indexing

mythril/analysis/solver.py

@@ -1,4 +1,4 @@
-from z3 import Solver, simplify, sat, unknown
+from z3 import Solver, simplify, sat, unknown, FuncInterp
 from mythril.exceptions import UnsatError
 import logging
 
@@ -21,6 +21,10 @@ def pretty_print_model(model):
     ret = ""
 
     for d in model.decls():
+        if type(model[d]) == FuncInterp:
+            condition = model[d].as_list()
+            ret += ("%s: %s\n" % (d.name(), condition))
+            continue
 
         try:
             condition = "0x%x" % model[d].as_long()

mythril/laser/ethereum/instructions.py

@@ -130,7 +130,6 @@ class Instruction:
             op1 = If(op1, BitVecVal(1, 256), BitVecVal(0, 256))
         if type(op2) == BoolRef:
             op2 = If(op2, BitVecVal(1, 256), BitVecVal(0, 256))
-
         stack.append(op1 & op2)
 
         return [global_state]
@@ -353,43 +352,7 @@ class Instruction:
         environment = global_state.environment
         op0 = state.stack.pop()
 
-        if environment.calldata_type == CalldataType.CONCRETE:
+        state.stack.append(environment.calldata.get_word_at(op0))
-            try:
-                offset = util.get_concrete_int(simplify(op0))
-                b = environment.calldata[offset]
-            except AttributeError:
-                logging.debug("CALLDATALOAD: Unsupported symbolic index")
-                state.stack.append(global_state.new_bitvec(
-                    "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
-                return [global_state]
-            except IndexError:
-                logging.debug("Calldata not set, using symbolic variable instead")
-                state.stack.append(global_state.new_bitvec(
-                    "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
-                return [global_state]
-
-            if type(b) == int:
-                val = b''
-
-                try:
-                    for i in range(offset, offset + 32):
-                        val += environment.calldata[i].to_bytes(1, byteorder='big')
-
-                    logging.debug("Final value: " + str(int.from_bytes(val, byteorder='big')))
-                    state.stack.append(BitVecVal(int.from_bytes(val, byteorder='big'), 256))
-                # FIXME: broad exception catch
-                except:
-                    state.stack.append(global_state.new_bitvec(
-                        "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
-        else:
-            # symbolic calldata
-            try:
-                state.stack.append(environment.calldata.get_word_at(util.get_concrete_int(op0)))
-            except AttributeError:
-                logging.debug("CALLDATALOAD: Unsupported symbolic index")
-                state.stack.append(global_state.new_bitvec(
-                    "calldata_" + str(environment.active_account.contract_name) + "[" + str(simplify(op0)) + "]", 256))
-
         return [global_state]
 
     @StateTransition()
@@ -420,7 +383,6 @@ class Instruction:
             dstart = util.get_concrete_int(op1)
             # FIXME: broad exception catch
         except:
-            logging.debug("Unsupported symbolic calldata offset in CALLDATACOPY")
             dstart = simplify(op1)
             dstart_sym = True
 
@@ -433,7 +395,7 @@ class Instruction:
             size = simplify(op2)
             size_sym = True
 
-        if dstart_sym or size_sym:
+        if size_sym:
             state.mem_extend(mstart, 1)
             state.memory[mstart] = global_state.new_bitvec(
                 "calldata_" + str(environment.active_account.contract_name) + "[" + str(dstart) + ": + " + str(
@@ -455,9 +417,13 @@ class Instruction:
             try:
                 i_data = dstart
 
+                new_memory = []
                 for i in range(mstart, mstart + size):
-                    state.memory[i] = environment.calldata[i_data]
+                    new_memory.append(environment.calldata[i_data])
-                    i_data += 1
+                    i_data = simplify(i_data + 1)
+
+                for i in range(0, len(new_memory), 32):
+                    state.memory[i+mstart] = simplify(Concat(new_memory[i:i+32]))
             except:
                 logging.debug("Exception copying calldata to memory")
 

mythril/laser/ethereum/state.py

@@ -1,4 +1,5 @@
-from z3 import BitVec, BitVecVal, Solver, ExprRef, Concat, sat, simplify
+from z3 import BitVec, BitVecVal, BitVecRef, BitVecNumRef, BitVecSort, Solver, ExprRef, Concat, sat, simplify, Array
+from z3.z3types import Z3Exception
 from mythril.disassembler.disassembly import Disassembly
 from copy import copy, deepcopy
 from enum import Enum
@@ -10,35 +11,46 @@ class CalldataType(Enum):
     CONCRETE = 1
     SYMBOLIC = 2
 
-class SymbolicCalldata:
+class Calldata:
     def __init__(self, tx_id: int, starting_calldata: bytes=None):
         self.tx_id = tx_id
-        self._calldata = {}
+        self._calldata = Array('{}_calldata'.format(self.tx_id), BitVecSort(256), BitVecSort(8))
 
         if starting_calldata:
             for i in range(len(starting_calldata)):
-                self._calldata[i] = BitVecVal(starting_calldata[i], 8)
+                self._calldata[BitVecVal(i, 256)] = BitVecVal(starting_calldata[i], 8)
 
     def get_word_at(self, index: int):
         return self[index:index+32]
 
+    def concretized(self, model):
+        concrete_calldata = model[self._calldata].as_list()
+        concrete_calldata.sort(key=lambda x: x[0].as_long() if type(x) == list else -1)
+        result = []
+        arr_index = 1
+        for i in range(0, concrete_calldata[len(concrete_calldata)-1][0].as_long()+1):
+            if concrete_calldata[arr_index][0].as_long() == i:
+                result.append(concrete_calldata[arr_index][1].as_long())
+                arr_index += 1
+            else:
+                # Default value
+                result.append(concrete_calldata[0].as_long())
+        return result
+
     def __getitem__(self, item: int):
         if isinstance(item, slice):
-            if item.step != None \
+            try:
-            or item.start > item.stop \
+                current_index = item.start if type(item.start) in [BitVecRef, BitVecNumRef] else BitVecVal(item.start, 256)
-            or item.start < 0 \
-            or item.stop < 0: raise IndexError("Invalid Calldata Slice")
-
                 dataparts = []
-            for i in range(item.start, item.stop):
+                while simplify(current_index != item.stop):
-                dataparts.append(self[i])
+                    dataparts.append(self[current_index])
+                    current_index = simplify(current_index + 1)
+            except Z3Exception:
+                raise IndexError("Invalid Calldata Slice")
+
             return simplify(Concat(dataparts))
         else:
-            try:
+            return self._calldata[item] if type(item) != BitVecVal else self._calldata[BitVecVal(item, 256)]
-                return self._calldata[item]
-            except KeyError:
-                self._calldata[item] = BitVec(str(self.tx_id)+'_calldata['+str(item)+']', 8)
-                return self._calldata[item]
 
 class Storage:
     """

mythril/laser/ethereum/transaction/concolic.py

@@ -1,6 +1,6 @@
 from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction, get_next_transaction_id
 from z3 import BitVec
-from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState, SymbolicCalldata
+from mythril.laser.ethereum.state import GlobalState, Environment, CalldataType, Account, WorldState, Calldata
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
 
@@ -10,14 +10,14 @@ def execute_message_call(laser_evm, callee_address, caller_address, origin_addre
     open_states = laser_evm.open_states[:]
     del laser_evm.open_states[:]
 
-    next_transaction_id = get_next_transaction_id()
     for open_world_state in open_states:
+        next_transaction_id = get_next_transaction_id()
         transaction = MessageCallTransaction(
             identifier=next_transaction_id,
             world_state=open_world_state,
             callee_account=open_world_state[callee_address],
             caller=caller_address,
-            call_data=SymbolicCalldata(next_transaction_id, data),
+            call_data=Calldata(next_transaction_id, data),
             gas_price=gas_price,
             call_value=value,
             origin=origin_address,

mythril/laser/ethereum/transaction/symbolic.py

@@ -3,7 +3,7 @@ from logging import debug
 
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.cfg import Node, Edge, JumpType
-from mythril.laser.ethereum.state import CalldataType, SymbolicCalldata
+from mythril.laser.ethereum.state import CalldataType, Calldata
 from mythril.laser.ethereum.transaction.transaction_models import MessageCallTransaction, ContractCreationTransaction,\
     get_next_transaction_id
 
@@ -23,7 +23,7 @@ def execute_message_call(laser_evm, callee_address):
             callee_account=open_world_state[callee_address],
             caller=BitVec("caller{}".format(next_transaction_id), 256),
             identifier=next_transaction_id,
-            call_data=SymbolicCalldata(next_transaction_id),
+            call_data=Calldata(next_transaction_id),
             gas_price=BitVec("gas_price{}".format(next_transaction_id), 256),
             call_value=BitVec("call_value{}".format(next_transaction_id), 256),
             origin=BitVec("origin{}".format(next_transaction_id), 256),