Use dictionary for memory

mythril/analysis/modules/integer.py

@@ -265,10 +265,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
         """
 
         stack = state.mstate.stack
-        try:
-            offset, length = get_concrete_int(stack[-1]), get_concrete_int(stack[-2])
-        except TypeError:
-            return
+        offset, length = stack[-1], stack[-2]
 
         state_annotation = _get_overflowunderflow_state_annotation(state)
 

mythril/laser/ethereum/instructions.py

@@ -1308,17 +1308,7 @@ class Instruction:
         :return:
         """
         state = global_state.mstate
-        op0 = state.stack.pop()
-
-        try:
-            offset = util.get_concrete_int(op0)
-        except TypeError:
-            log.debug("Can't MLOAD from symbolic index")
-            data = global_state.new_bitvec(
-                "mem[invhash(" + str(hash(simplify(op0))) + ")]", 256
-            )
-            state.stack.append(data)
-            return [global_state]
+        offset = state.stack.pop()
 
         state.mem_extend(offset, 32)
         data = state.memory.get_word_at(offset)
@@ -1334,13 +1324,7 @@ class Instruction:
         :return:
         """
         state = global_state.mstate
-        op0, value = state.stack.pop(), state.stack.pop()
-
-        try:
-            mstart = util.get_concrete_int(op0)
-        except TypeError:
-            log.debug("MSTORE to symbolic index. Not supported")
-            return [global_state]
+        mstart, value = state.stack.pop(), state.stack.pop()
 
         try:
             state.mem_extend(mstart, 32)
@@ -1359,13 +1343,7 @@ class Instruction:
         :return:
         """
         state = global_state.mstate
-        op0, value = state.stack.pop(), state.stack.pop()
-
-        try:
-            offset = util.get_concrete_int(op0)
-        except TypeError:
-            log.debug("MSTORE to symbolic index. Not supported")
-            return [global_state]
+        offset, value = state.stack.pop(), state.stack.pop()
 
         state.mem_extend(offset, 1)
 
@@ -1618,17 +1596,9 @@ class Instruction:
         """
         state = global_state.mstate
         offset, length = state.stack.pop(), state.stack.pop()
-        return_data = [global_state.new_bitvec("return_data", 8)]
-        try:
-            concrete_offset = util.get_concrete_int(offset)
-            concrete_length = util.get_concrete_int(length)
-            state.mem_extend(concrete_offset, concrete_length)
-            StateTransition.check_gas_usage_limit(global_state)
-            return_data = state.memory[
-                concrete_offset : concrete_offset + concrete_length
-            ]
-        except TypeError:
-            log.debug("Return with symbolic length or offset. Not supported")
+        state.mem_extend(offset, length)
+        StateTransition.check_gas_usage_limit(global_state)
+        return_data = state.memory[offset : offset + length]
         global_state.current_transaction.end(global_state, return_data)
 
     @StateTransition()

mythril/laser/ethereum/state/machine_state.py

@@ -155,12 +155,20 @@ class MachineState:
         if self.min_gas_used > self.gas_limit:
             raise OutOfGasException()
 
-    def mem_extend(self, start: int, size: int) -> None:
+    def mem_extend(self, start: Union[int, BitVec], size: Union[int, BitVec]) -> None:
         """Extends the memory of this machine state.
 
         :param start: Start of memory extension
         :param size: Size of memory extension
         """
+        if (isinstance(start, BitVec) and start.symbolic) or (
+            isinstance(size, BitVec) and size.symbolic
+        ):
+            return
+        if isinstance(start, BitVec):
+            start = start.value
+        if isinstance(size, BitVec):
+            size = size.value
         m_extend = self.calculate_extension_size(start, size)
         if m_extend:
             extend_gas = self.calculate_memory_gas(start, size)

mythril/laser/ethereum/state/memory.py

@@ -1,6 +1,6 @@
 """This module contains a representation of a smart contract's memory."""
+from copy import copy
 from typing import cast, List, Union, overload
-
 from z3 import Z3Exception
 
 from mythril.laser.ethereum import util
@@ -15,31 +15,39 @@ from mythril.laser.smt import (
 )
 
 
+def convert_bv(val: Union[int, BitVec]) -> BitVec:
+    if isinstance(val, BitVec):
+        return val
+    return symbol_factory.BitVecVal(val, 256)
+
+
 class Memory:
     """A class representing contract memory with random access."""
 
     def __init__(self):
         """"""
-        self._memory = []  # type: List[Union[int, BitVec]]
+        self._msize = 0
+        self._memory = {}
 
     def __len__(self):
         """
 
         :return:
         """
-        return len(self._memory)
+        return self._msize
 
     def __copy__(self):
-        copy = Memory()
-        copy._memory = self._memory[:]
-        return copy
+        new_memory = Memory()
+        new_memory._memory = copy(self._memory)
+        new_memory._msize = self._msize
+        return new_memory
 
-    def extend(self, size):
+    def extend(self, size: int):
         """
 
         :param size:
         """
-        self._memory.extend(bytearray(size))
+        self._msize += size
 
     def get_word_at(self, index: int) -> Union[int, BitVec]:
         """Access a word from a specified memory index.
@@ -126,12 +134,17 @@ class Memory:
                 raise IndexError("Invalid Memory Slice")
             if step is None:
                 step = 1
-            return [cast(Union[int, BitVec], self[i]) for i in range(start, stop, step)]
+            start, stop, step = convert_bv(start), convert_bv(stop), convert_bv(step)
+            ret_lis = []
+            itr = symbol_factory.BitVecVal(0, 256)
+            while simplify(start + itr != stop) and itr <= 10000000:
+                ret_lis.append(self[start + step * itr])
+                itr += 1
 
-        try:
-            return self._memory[item]
-        except IndexError:
-            return 0
+            return ret_lis
+
+        item = simplify(convert_bv(item))
+        return self._memory.get(item, 0)
 
     def __setitem__(
         self,
@@ -152,11 +165,17 @@ class Memory:
                 raise IndexError("Invalid Memory Slice")
             if step is None:
                 step = 1
+            else:
+                assert False, "Currently mentioning step size is not supported"
             assert type(value) == list
-            for i in range(0, stop - start, step):
-                self[start + i] = cast(List[Union[int, BitVec]], value)[i]
+            start, stop, step = convert_bv(start), convert_bv(stop), convert_bv(step)
+            itr = symbol_factory.BitVecVal(0, 256)
+            while simplify(start + itr != stop) and itr <= 10000000:
+                self[start + itr] = value[itr.value]
+                itr += 1
 
         else:
+            key = simplify(convert_bv(key))
             if key >= len(self):
                 return
             if isinstance(value, int):

mythril/laser/smt/bitvec.py

@@ -113,7 +113,7 @@ class BitVec(Expression[z3.BitVecRef]):
         union = self.annotations.union(other.annotations)
         return BitVec(self.raw & other.raw, annotations=union)
 
-    def __or__(self, other: "BitVec") -> "BitVec":
+    def __or__(self, other: Union[int, "BitVec"]) -> "BitVec":
         """Create an or expression.
 
         :param other:
@@ -121,10 +121,12 @@ class BitVec(Expression[z3.BitVecRef]):
         """
         if isinstance(other, BitVecFunc):
             return other | self
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         union = self.annotations.union(other.annotations)
         return BitVec(self.raw | other.raw, annotations=union)
 
-    def __xor__(self, other: "BitVec") -> "BitVec":
+    def __xor__(self, other: Union[int, "BitVec"]) -> "BitVec":
         """Create a xor expression.
 
         :param other:
@@ -132,10 +134,12 @@ class BitVec(Expression[z3.BitVecRef]):
         """
         if isinstance(other, BitVecFunc):
             return other ^ self
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         union = self.annotations.union(other.annotations)
         return BitVec(self.raw ^ other.raw, annotations=union)
 
-    def __lt__(self, other: "BitVec") -> Bool:
+    def __lt__(self, other: Union[int, "BitVec"]) -> Bool:
         """Create a signed less than expression.
 
         :param other:
@@ -143,10 +147,12 @@ class BitVec(Expression[z3.BitVecRef]):
         """
         if isinstance(other, BitVecFunc):
             return other > self
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         union = self.annotations.union(other.annotations)
         return Bool(self.raw < other.raw, annotations=union)
 
-    def __gt__(self, other: "BitVec") -> Bool:
+    def __gt__(self, other: Union[int, "BitVec"]) -> Bool:
         """Create a signed greater than expression.
 
         :param other:
@@ -154,24 +160,30 @@ class BitVec(Expression[z3.BitVecRef]):
         """
         if isinstance(other, BitVecFunc):
             return other < self
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         union = self.annotations.union(other.annotations)
         return Bool(self.raw > other.raw, annotations=union)
 
-    def __le__(self, other: "BitVec") -> Bool:
+    def __le__(self, other: Union[int, "BitVec"]) -> Bool:
         """Create a signed less than expression.
 
         :param other:
         :return:
         """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         union = self.annotations.union(other.annotations)
         return Bool(self.raw <= other.raw, annotations=union)
 
-    def __ge__(self, other: "BitVec") -> Bool:
+    def __ge__(self, other: Union[int, "BitVec"]) -> Bool:
         """Create a signed greater than expression.
 
         :param other:
         :return:
         """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         union = self.annotations.union(other.annotations)
         return Bool(self.raw >= other.raw, annotations=union)