Merge branch 'develop'

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/analysis/report.py

@@ -231,7 +231,7 @@ class Report:
                 title = "Unspecified Security Issue"
             extra = {"discoveryTime": int(issue.discovery_time * 10 ** 9)}
             if issue.transaction_sequence_jsonv2:
-                extra["testCase"] = issue.transaction_sequence_jsonv2
+                extra["testCases"] = [issue.transaction_sequence_jsonv2]
 
             _issues.append(
                 {

mythril/analysis/symbolic.py

@@ -215,7 +215,7 @@ class SymExecWrapper:
                                     gas,
                                     value,
                                     state.mstate.memory[
-                                        meminstart.val : meminsz.val * 4
+                                        meminstart.val : meminsz.val + meminstart.val
                                     ],
                                 )
                             )

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,13 @@ class Instruction:
         """
         state = global_state.mstate
         offset, length = state.stack.pop(), state.stack.pop()
+        if length.symbolic:
             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")
+        else:
+            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 typing import cast, List, Union, overload
-
+from copy import copy
+from typing import cast, Dict, List, Union, overload
 from z3 import Z3Exception
 
 from mythril.laser.ethereum import util
@@ -15,31 +15,43 @@ 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)
+
+
+# No of iterations to perform when iteration size is symbolic
+APPROX_ITR = 100
+
+
 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 = {}  # type: Dict[BitVec, Union[int, BitVec]]
 
     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.
@@ -103,7 +115,7 @@ class Memory:
                 self[index + 31 - (i // 8)] = Extract(i + 7, i, value_to_write)
 
     @overload
-    def __getitem__(self, item: int) -> Union[int, BitVec]:
+    def __getitem__(self, item: BitVec) -> Union[int, BitVec]:
         ...
 
     @overload
@@ -111,7 +123,7 @@ class Memory:
         ...
 
     def __getitem__(
-        self, item: Union[int, slice]
+        self, item: Union[BitVec, slice]
     ) -> Union[BitVec, int, List[Union[int, BitVec]]]:
         """
 
@@ -126,16 +138,31 @@ 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)]
+            bvstart, bvstop, bvstep = (
+                convert_bv(start),
+                convert_bv(stop),
+                convert_bv(step),
+            )
+            ret_lis = []
+            symbolic_len = False
+            itr = symbol_factory.BitVecVal(0, 256)
+            if (bvstop - bvstart).symbolic:
+                symbolic_len = True
+
+            while simplify(bvstart + bvstep * itr != bvstop) and (
+                not symbolic_len or itr <= APPROX_ITR
+            ):
+                ret_lis.append(self[bvstart + bvstep * 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,
-        key: Union[int, slice],
+        key: Union[int, BitVec, slice],
         value: Union[BitVec, int, List[Union[int, BitVec]]],
     ):
         """
@@ -152,15 +179,32 @@ 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]
+            bvstart, bvstop, bvstep = (
+                convert_bv(start),
+                convert_bv(stop),
+                convert_bv(step),
+            )
+            symbolic_len = False
+            itr = symbol_factory.BitVecVal(0, 256)
+            if (bvstop - bvstart).symbolic:
+                symbolic_len = True
+            while simplify(bvstart + bvstep * itr != bvstop) and (
+                not symbolic_len or itr <= APPROX_ITR
+            ):
+                self[bvstart + itr * bvstep] = cast(List[Union[int, BitVec]], value)[
+                    itr.value
+                ]
+                itr += 1
 
         else:
-            if key >= len(self):
+            bv_key = simplify(convert_bv(key))
+            if bv_key >= len(self):
                 return
             if isinstance(value, int):
                 assert 0 <= value <= 0xFF
             if isinstance(value, BitVec):
                 assert value.size() == 8
-            self._memory[key] = cast(Union[int, BitVec], value)
+            self._memory[bv_key] = cast(Union[int, BitVec], value)

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)
 

mythril/laser/smt/bitvecfunc.py

@@ -140,56 +140,68 @@ class BitVecFunc(BitVec):
         """
         return _arithmetic_helper(self, other, operator.and_)
 
-    def __or__(self, other: "BitVec") -> "BitVecFunc":
+    def __or__(self, other: Union[int, "BitVec"]) -> "BitVecFunc":
         """Create an or expression.
 
         :param other: The int or BitVec to or with this BitVecFunc
         :return: The resulting BitVecFunc
         """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         return _arithmetic_helper(self, other, operator.or_)
 
-    def __xor__(self, other: "BitVec") -> "BitVecFunc":
+    def __xor__(self, other: Union[int, "BitVec"]) -> "BitVecFunc":
         """Create a xor expression.
 
         :param other: The int or BitVec to xor with this BitVecFunc
         :return: The resulting BitVecFunc
         """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         return _arithmetic_helper(self, other, operator.xor)
 
-    def __lt__(self, other: "BitVec") -> Bool:
+    def __lt__(self, other: Union[int, "BitVec"]) -> Bool:
         """Create a signed less than expression.
 
         :param other: The int or BitVec to compare to this BitVecFunc
         :return: The resulting Bool
         """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         return _comparison_helper(
             self, other, operator.lt, default_value=False, inputs_equal=False
         )
 
-    def __gt__(self, other: "BitVec") -> Bool:
+    def __gt__(self, other: Union[int, "BitVec"]) -> Bool:
         """Create a signed greater than expression.
 
         :param other: The int or BitVec to compare to this BitVecFunc
         :return: The resulting Bool
         """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         return _comparison_helper(
             self, other, operator.gt, default_value=False, inputs_equal=False
         )
 
-    def __le__(self, other: "BitVec") -> Bool:
+    def __le__(self, other: Union[int, "BitVec"]) -> Bool:
         """Create a signed less than or equal to expression.
 
         :param other: The int or BitVec to compare to this BitVecFunc
         :return: The resulting Bool
         """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         return Or(self < other, self == other)
 
-    def __ge__(self, other: "BitVec") -> Bool:
+    def __ge__(self, other: Union[int, "BitVec"]) -> Bool:
         """Create a signed greater than or equal to expression.
 
         :param other: The int or BitVec to compare to this BitVecFunc
         :return: The resulting Bool
         """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         return Or(self > other, self == other)
 
     # MYPY: fix complains about overriding __eq__
@@ -200,6 +212,9 @@ class BitVecFunc(BitVec):
         :return: The resulting Bool
         """
 
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
+
         return _comparison_helper(
             self, other, operator.eq, default_value=False, inputs_equal=True
         )
@@ -211,6 +226,8 @@ class BitVecFunc(BitVec):
         :param other: The int or BitVec to compare to this BitVecFunc
         :return: The resulting Bool
         """
+        if not isinstance(other, BitVec):
+            other = BitVec(z3.BitVecVal(other, self.size()))
         return _comparison_helper(
             self, other, operator.ne, default_value=True, inputs_equal=False
         )