Storage Refactor

mythril/laser/ethereum/instructions.py

@@ -945,7 +945,6 @@ class Instruction:
             )
             log.debug("Created BitVecFunc hash.")
 
-            keccak_function_manager.add_keccak(result, state.memory[index])
         else:
             keccak = utils.sha3(data.value.to_bytes(length, byteorder="big"))
             result = symbol_factory.BitVecFuncVal(
@@ -1366,42 +1365,37 @@ class Instruction:
         state = global_state.mstate
         index = state.stack.pop()
         log.debug("Storage access at index " + str(index))
+        index = simplify(index)
 
-        try:
-            index = util.get_concrete_int(index)
+        if not keccak_function_manager.is_keccak(index):
             return self._sload_helper(global_state, index)
 
-        except TypeError:
-            if not keccak_function_manager.is_keccak(index):
-                return self._sload_helper(global_state, str(index))
+        storage_keys = global_state.environment.active_account.storage.keys()
+        keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys))
 
-            storage_keys = global_state.environment.active_account.storage.keys()
-            keccak_keys = list(filter(keccak_function_manager.is_keccak, storage_keys))
+        results = []  # type: List[GlobalState]
+        constraints = []
 
-            results = []  # type: List[GlobalState]
-            constraints = []
+        for keccak_key in keccak_keys:
+            key_argument = keccak_function_manager.get_argument(keccak_key)
+            index_argument = keccak_function_manager.get_argument(index)
+            if key_argument.size() != index_argument.size():
+                continue
+            constraints.append((keccak_key, key_argument == index_argument))
 
-            for keccak_key in keccak_keys:
-                key_argument = keccak_function_manager.get_argument(keccak_key)
-                index_argument = keccak_function_manager.get_argument(index)
-                constraints.append((keccak_key, key_argument == index_argument))
+        for (keccak_key, constraint) in constraints:
+            if constraint in state.constraints:
+                results += self._sload_helper(global_state, keccak_key, [constraint])
+        if len(results) > 0:
+            return results
 
-            for (keccak_key, constraint) in constraints:
-                if constraint in state.constraints:
-                    results += self._sload_helper(
-                        global_state, keccak_key, [constraint]
-                    )
-            if len(results) > 0:
-                return results
+        for (keccak_key, constraint) in constraints:
+            results += self._sload_helper(copy(global_state), keccak_key, [constraint])
 
-            for (keccak_key, constraint) in constraints:
-                results += self._sload_helper(
-                    copy(global_state), keccak_key, [constraint]
-                )
-            if len(results) > 0:
-                return results
+        if len(results) > 0:
+            return results
 
-            return self._sload_helper(global_state, str(index))
+        return self._sload_helper(global_state, index)
 
     @staticmethod
     def _sload_helper(
@@ -1422,6 +1416,8 @@ class Instruction:
 
         if constraints is not None:
             global_state.mstate.constraints += constraints
+            if global_state.mstate.constraints.is_possible is False:
+                return []
 
         global_state.mstate.stack.append(data)
         return [global_state]
@@ -1452,58 +1448,40 @@ class Instruction:
         state = global_state.mstate
         index, value = state.stack.pop(), state.stack.pop()
         log.debug("Write to storage[" + str(index) + "]")
-
-        try:
-            index = util.get_concrete_int(index)
+        index = simplify(index)
+        is_keccak = keccak_function_manager.is_keccak(index)
+        if not is_keccak:
             return self._sstore_helper(global_state, index, value)
-        except TypeError:
-            is_keccak = keccak_function_manager.is_keccak(index)
-            if not is_keccak:
-                return self._sstore_helper(global_state, str(index), value)
-
-            storage_keys = global_state.environment.active_account.storage.keys()
-            keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys)
-
-            results = []  # type: List[GlobalState]
-            new = symbol_factory.Bool(False)
-
-            for keccak_key in keccak_keys:
-                key_argument = keccak_function_manager.get_argument(
-                    keccak_key
-                )  # type: Expression
-                index_argument = keccak_function_manager.get_argument(
-                    index
-                )  # type: Expression
-                condition = key_argument == index_argument
-                condition = (
-                    condition
-                    if type(condition) == bool
-                    else is_true(simplify(cast(Bool, condition)))
-                )
-                if condition:
-                    return self._sstore_helper(
-                        copy(global_state),
-                        keccak_key,
-                        value,
-                        key_argument == index_argument,
-                    )
 
-                results += self._sstore_helper(
-                    copy(global_state),
-                    keccak_key,
-                    value,
-                    key_argument == index_argument,
-                )
+        storage_keys = global_state.environment.active_account.storage.keys()
 
-                new = Or(new, cast(Bool, key_argument != index_argument))
+        keccak_keys = filter(keccak_function_manager.is_keccak, storage_keys)
 
-            if len(results) > 0:
-                results += self._sstore_helper(
-                    copy(global_state), str(index), value, new
-                )
-                return results
+        results = []  # type: List[GlobalState]
+        new = symbol_factory.Bool(False)
+
+        for keccak_key in keccak_keys:
+            key_argument = keccak_function_manager.get_argument(
+                keccak_key
+            )  # type: Expression
+            index_argument = keccak_function_manager.get_argument(
+                index
+            )  # type: Expression
+            if key_argument.size() != index_argument.size():
+                continue
+
+            result = self._sstore_helper(
+                copy(global_state), keccak_key, value, key_argument == index_argument
+            )
+            if len(result) > 0:
+                return result
 
-            return self._sstore_helper(global_state, str(index), value)
+            new = Or(new, cast(Bool, key_argument != index_argument))
+        results += self._sstore_helper(copy(global_state), index, value, new)
+        if len(results) > 0:
+            return results
+        # results += self._sstore_helper(copy(global_state), index, value)
+        return self._sstore_helper(copy(global_state), index, value)
 
     @staticmethod
     def _sstore_helper(global_state, index, value, constraint=None):
@@ -1531,6 +1509,8 @@ class Instruction:
 
         if constraint is not None:
             global_state.mstate.constraints.append(constraint)
+            if global_state.mstate.constraints.is_possible is False:
+                return []
 
         return [global_state]
 

mythril/laser/ethereum/keccak.py

@@ -1,6 +1,7 @@
 """This module contains a function manager to deal with symbolic Keccak
 values."""
-from mythril.laser.smt import Expression
+from mythril.laser.smt import Expression, BitVecFunc, BitVec
+from typing import cast, Union
 
 
 class KeccakFunctionManager:
@@ -16,7 +17,9 @@ class KeccakFunctionManager:
         :param expression:
         :return:
         """
-        return str(expression) in self.keccak_expression_mapping.keys()
+        if not isinstance(expression, BitVecFunc):
+            return False
+        return expression.func_name == "keccak256"
 
     def get_argument(self, expression: Expression) -> Expression:
         """
@@ -26,13 +29,4 @@ class KeccakFunctionManager:
         """
         if not self.is_keccak(expression):
             raise ValueError("Expression is not a recognized keccac result")
-        return self.keccak_expression_mapping[str(expression)][1]
-
-    def add_keccak(self, expression: Expression, argument: Expression) -> None:
-        """
-
-        :param expression:
-        :param argument:
-        """
-        index = str(expression)
-        self.keccak_expression_mapping[index] = (expression, argument)
+        return cast(BitVecFunc, expression).input_

mythril/laser/ethereum/transaction/symbolic.py

@@ -73,7 +73,7 @@ def execute_contract_creation(
     del laser_evm.open_states[:]
 
     new_account = laser_evm.world_state.create_account(
-        0, concrete_storage=True, dynamic_loader=None, creator=CREATOR_ADDRESS
+        0, concrete_storage=False, dynamic_loader=None, creator=CREATOR_ADDRESS
     )
     if contract_name:
         new_account.contract_name = contract_name

mythril/laser/ethereum/transaction/transaction_models.py

@@ -154,7 +154,7 @@ class ContractCreationTransaction(BaseTransaction):
         super().__init__(*args, **kwargs, init_call_data=False)  # type: ignore
         # TODO: set correct balance for new account
         self.callee_account = self.callee_account or self.world_state.create_account(
-            0, concrete_storage=True
+            0, concrete_storage=False
         )
 
     def initial_global_state(self) -> GlobalState:

mythril/laser/smt/__init__.py

@@ -72,7 +72,7 @@ class SymbolFactory(Generic[T, U]):
         func_name: str,
         size: int,
         annotations: Annotations = None,
-        input_: Union[int, "BitVec"] = None,
+        input_: Expression = None,
     ) -> BitVecFunc:
         """Creates a new bit vector function with a symbolic value.
 
@@ -91,7 +91,7 @@ class SymbolFactory(Generic[T, U]):
         func_name: str,
         size: int,
         annotations: Annotations = None,
-        input_: Union[int, "BitVec"] = None,
+        input_: Expression = None,
     ) -> BitVecFunc:
         """Creates a new bit vector function with a symbolic value.
 
@@ -140,7 +140,7 @@ class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]):
         func_name: str,
         size: int,
         annotations: Annotations = None,
-        input_: Union[int, "BitVec"] = None,
+        input_: Expression = None,
     ) -> BitVecFunc:
         """Creates a new bit vector function with a concrete value."""
         raw = z3.BitVecVal(value, size)
@@ -152,7 +152,7 @@ class _SmtSymbolFactory(SymbolFactory[bool.Bool, BitVec]):
         func_name: str,
         size: int,
         annotations: Annotations = None,
-        input_: Union[int, "BitVec"] = None,
+        input_: Expression = None,
     ) -> BitVecFunc:
         """Creates a new bit vector function with a symbolic value."""
         raw = z3.BitVec(name, size)

mythril/laser/smt/bitvec.py

@@ -243,6 +243,9 @@ class BitVec(Expression[z3.BitVecRef]):
         """
         return self._handle_shift(other, rshift)
 
+    def __hash__(self):
+        return self.raw.__hash__()
+
 
 def _comparison_helper(
     a: BitVec, b: BitVec, operation: Callable, default_value: bool, inputs_equal: bool

mythril/laser/smt/bitvecfunc.py

@@ -2,6 +2,7 @@ from typing import Optional, Union, cast, Callable
 
 import z3
 
+from mythril.laser.smt.expression import Expression
 from mythril.laser.smt.bitvec import BitVec, Bool, And, Annotations
 from mythril.laser.smt.bool import Or
 
@@ -26,6 +27,7 @@ def _arithmetic_helper(
     union = a.annotations + b.annotations
 
     if isinstance(b, BitVecFunc):
+
         # TODO: Find better value to set input and name to in this case?
         return BitVecFunc(raw=raw, func_name=None, input_=None, annotations=union)
 
@@ -79,7 +81,7 @@ class BitVecFunc(BitVec):
         self,
         raw: z3.BitVecRef,
         func_name: Optional[str],
-        input_: Union[int, "BitVec"] = None,
+        input_: Expression = None,
         annotations: Optional[Annotations] = None,
     ):
         """
@@ -223,3 +225,6 @@ class BitVecFunc(BitVec):
         :return The resulting right shifted output:
         """
         return _arithmetic_helper(self, other, operator.rshift)
+
+    def __hash__(self) -> int:
+        return self.raw.__hash__()

mythril/laser/smt/bool.py

@@ -80,6 +80,9 @@ class Bool(Expression[z3.BoolRef]):
         else:
             return False
 
+    def __hash__(self) -> int:
+        return self.raw.__hash__()
+
 
 def And(*args: Union[Bool, bool]) -> Bool:
     """Create an And expression."""

mythril/laser/smt/expression.py

@@ -45,6 +45,12 @@ class Expression(Generic[T]):
     def __repr__(self) -> str:
         return repr(self.raw)
 
+    def size(self):
+        return self.raw.size()
+
+    def __hash__(self) -> int:
+        return self.raw.__hash__()
+
 
 G = TypeVar("G", bound=Expression)
 

tests/laser/evm_testsuite/evm_test.py

@@ -2,7 +2,7 @@ from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.state.account import Account
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.transaction.concolic import execute_message_call
-from mythril.laser.smt import Expression, BitVec
+from mythril.laser.smt import Expression, BitVec, symbol_factory
 from mythril.analysis.solver import get_model
 from datetime import datetime
 
@@ -139,7 +139,7 @@ def test_vmtest(
 
             for index, value in details["storage"].items():
                 expected = int(value, 16)
-                actual = account.storage[int(index, 16)]
+                actual = account.storage[symbol_factory.BitVecVal(int(index, 16), 256)]
                 if isinstance(actual, Expression):
                     actual = actual.value
                     actual = 1 if actual is True else 0 if actual is False else actual

tests/testdata/outputs_expected/overflow.sol.o.json

@@ -26,6 +26,19 @@
             "sourceMap": null,
             "swc-id": "101",
             "title": "Integer Underflow"
+        },
+        {
+            "address": 725,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
+            "function": "sendeth(address,uint256)",
+            "max_gas_used": 78155,
+            "min_gas_used": 17019,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "101",
+            "title": "Integer Overflow"
         }
     ],
     "success": true

tests/testdata/outputs_expected/overflow.sol.o.jsonv2

@@ -34,6 +34,23 @@
                 "severity": "High",
                 "swcID": "SWC-101",
                 "swcTitle": "Integer Overflow and Underflow"
+            },
+            {
+                "description": {
+                    "head": "The binary addition can overflow.",
+                    "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
+                },
+                "extra": {
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                },
+                "locations": [
+                    {
+                        "sourceMap": "725:1:0"
+                    }
+                ],
+                "severity": "High",
+                "swcID": "SWC-101",
+                "swcTitle": "Integer Overflow and Underflow"
             }
         ],
         "meta": {},

tests/testdata/outputs_expected/overflow.sol.o.markdown

@@ -25,3 +25,16 @@ The operands of the subtraction operation are not sufficiently constrained. The
 
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
+
+## Integer Overflow
+- SWC ID: 101
+- Severity: High
+- Contract: Unknown
+- Function name: `sendeth(address,uint256)`
+- PC address: 725
+- Estimated Gas Usage: 17019 - 78155
+
+### Description
+
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.

tests/testdata/outputs_expected/overflow.sol.o.text

@@ -20,3 +20,14 @@ The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------
 
+==== Integer Overflow ====
+SWC ID: 101
+Severity: High
+Contract: Unknown
+Function name: sendeth(address,uint256)
+PC address: 725
+Estimated Gas Usage: 17019 - 78155
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.
+--------------------
+

tests/testdata/outputs_expected/underflow.sol.o.json

@@ -26,6 +26,19 @@
             "sourceMap": null,
             "swc-id": "101",
             "title": "Integer Underflow"
+        },
+        {
+            "address": 725,
+            "contract": "Unknown",
+            "debug": "<DEBUG-DATA>",
+            "description": "The binary addition can overflow.\nThe operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.",
+            "function": "sendeth(address,uint256)",
+            "max_gas_used": 52861,
+            "min_gas_used": 11915,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "101",
+            "title": "Integer Overflow"
         }
     ],
     "success": true

tests/testdata/outputs_expected/underflow.sol.o.jsonv2

@@ -34,6 +34,23 @@
                 "severity": "High",
                 "swcID": "SWC-101",
                 "swcTitle": "Integer Overflow and Underflow"
+            },
+            {
+                "description": {
+                    "head": "The binary addition can overflow.",
+                    "tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
+                },
+                "extra": {
+                    "discoveryTime": "<DISCOVERY-TIME-DATA>"
+                },
+                "locations": [
+                    {
+                        "sourceMap": "725:1:0"
+                    }
+                ],
+                "severity": "High",
+                "swcID": "SWC-101",
+                "swcTitle": "Integer Overflow and Underflow"
             }
         ],
         "meta": {},

tests/testdata/outputs_expected/underflow.sol.o.markdown

@@ -25,3 +25,16 @@ The operands of the subtraction operation are not sufficiently constrained. The
 
 The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
+
+## Integer Overflow
+- SWC ID: 101
+- Severity: High
+- Contract: Unknown
+- Function name: `sendeth(address,uint256)`
+- PC address: 725
+- Estimated Gas Usage: 11915 - 52861
+
+### Description
+
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.

tests/testdata/outputs_expected/underflow.sol.o.text

@@ -20,3 +20,14 @@ The binary subtraction can underflow.
 The operands of the subtraction operation are not sufficiently constrained. The subtraction could therefore result in an integer underflow. Prevent the underflow by checking inputs or ensure sure that the underflow is caught by an assertion.
 --------------------
 
+==== Integer Overflow ====
+SWC ID: 101
+Severity: High
+Contract: Unknown
+Function name: sendeth(address,uint256)
+PC address: 725
+Estimated Gas Usage: 11915 - 52861
+The binary addition can overflow.
+The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion.
+--------------------
+