Fix storage

mythril/laser/ethereum/instructions.py

@@ -19,6 +19,8 @@ from mythril.laser.smt import (
     UGT,
     BitVec,
     is_true,
+    Bool,
+    BitVecFunc,
     is_false,
     URem,
     SRem,
@@ -1369,42 +1371,20 @@ class Instruction:
         state = global_state.mstate
         index = state.stack.pop()
         log.debug("Storage access at index " + str(index))
-
-        try:
-            index = util.get_concrete_int(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))
-
-            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)
-                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:
-                results += self._sload_helper(
-                    copy(global_state), keccak_key, [constraint]
-                )
-            if len(results) > 0:
-                return results
-
-            return self._sload_helper(global_state, str(index))
+        """
+        if index not in global_state.environment.active_account.storage.keys():
+            for key in global_state.environment.active_account.storage.keys():
+                if not isinstance(index, BitVecFunc) or not isinstance(key, BitVecFunc):
+                    global_state.mstate.constraints.append(Bool(key.raw != index.raw))
+                    continue
+                key_map = Extract(255, 0, key.input_)
+                index_map = Extract(255, 0, index.input_)
+                if simplify(key_map == index_map):
+                    continue
+                global_state.mstate.constraints.append(key != index)
+        """
+        state.stack.append(global_state.environment.active_account.storage[index])
+        return [global_state]
 
     @staticmethod
     def _sload_helper(
@@ -1454,59 +1434,21 @@ class Instruction:
         global keccak_function_manager
         state = global_state.mstate
         index, value = state.stack.pop(), state.stack.pop()
+        """
+        if index not in global_state.environment.active_account.storage.keys():
+            for key in global_state.environment.active_account.storage.keys():
+                if not isinstance(index, BitVecFunc) or not isinstance(key, BitVecFunc):
+                    global_state.mstate.constraints.append(Bool(key.raw != index.raw))
+                    continue
+                key_map = Extract(255, 0, key.input_)
+                index_map = Extract(255, 0, index.input_)
+                if simplify(key_map == index_map):
+                    continue
+                global_state.mstate.constraints.append(key != index)
+        """
         log.debug("Write to storage[" + str(index) + "]")
-
-        try:
-            index = util.get_concrete_int(index)
-            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,
-                )
-
-                new = Or(new, cast(Bool, key_argument != index_argument))
-
-            if len(results) > 0:
-                results += self._sstore_helper(
-                    copy(global_state), str(index), value, new
-                )
-                return results
-
-            return self._sstore_helper(global_state, str(index), value)
+        global_state.environment.active_account.storage[index] = value
+        return [global_state]
 
     @staticmethod
     def _sstore_helper(global_state, index, value, constraint=None):

mythril/laser/ethereum/state/account.py

@@ -3,11 +3,10 @@
 This includes classes representing accounts and their storage.
 """
 from copy import deepcopy, copy
-from typing import Any, Dict, KeysView, Union
+from typing import Any, Dict, Union
 
-from z3 import ExprRef
 
-from mythril.laser.smt import Array, symbol_factory, BitVec
+from mythril.laser.smt import Array, K, BitVec, simplify, BitVecFunc, Extract
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.smt import symbol_factory
 
@@ -15,66 +14,74 @@ from mythril.laser.smt import symbol_factory
 class Storage:
     """Storage class represents the storage of an Account."""
 
-    def __init__(self, concrete=False, address=None, dynamic_loader=None) -> None:
+    def __init__(
+        self, concrete=False, address=None, dynamic_loader=None, keys=None
+    ) -> None:
         """Constructor for Storage.
 
         :param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic
         """
-        self._storage = {}  # type: Dict[Union[int, str], Any]
-        self.concrete = concrete
+        if concrete:
+            self._standard_storage = K(256, 256, 0)
+            self._map_storage = {}
+        else:
+            self._standard_storage = Array("Storage", 256, 256)
+            self._map_storage = {}
+
+        self._keys = keys or set()
         self.dynld = dynamic_loader
         self.address = address
 
     def __getitem__(self, item: Union[str, int]) -> Any:
-        try:
-            return self._storage[item]
-        except KeyError:
-            if (
-                self.address
-                and self.address.value != 0
-                and (self.dynld and self.dynld.storage_loading)
-            ):
-                try:
-                    self._storage[item] = symbol_factory.BitVecVal(
-                        int(
-                            self.dynld.read_storage(
-                                contract_address=self.address, index=int(item)
-                            ),
-                            16,
-                        ),
-                        256,
-                    )
-                    return self._storage[item]
-                except ValueError:
-                    pass
-
-        if self.concrete:
-            return symbol_factory.BitVecVal(0, 256)
-
-        self._storage[item] = symbol_factory.BitVecSym(
-            "storage_{}_{}".format(str(item), str(self.address)), 256
-        )
-        return self._storage[item]
-
-    def __setitem__(self, key: Union[int, str], value: Any) -> None:
-        self._storage[key] = value
-
-    def keys(self) -> KeysView:
-        """
+        self._keys.add(item)
+        storage = self._get_corresponding_storage(item)
+        return simplify(storage[item])
+
+    @staticmethod
+    def get_map_index(key):
+        if not isinstance(key, BitVecFunc) or key.func_name != "keccak256":
+            return None
+        index = Extract(255, 0, key.input_)
+        print(simplify(index), key.input_)
+        return simplify(index)
+
+    def _get_corresponding_storage(self, key):
+        index = self.get_map_index(key)
+        if index is None:
+            storage = self._standard_storage
+        else:
+            try:
+                storage = self._map_storage[index]
+            except KeyError:
+                if isinstance(self._standard_storage, Array):
+                    self._map_storage[index] = Array("Storage", 256, 256)
+                else:
+                    self._map_storage[index] = K(256, 256, 0)
+                storage = self._map_storage[index]
+        return storage
 
-        :return:
-        """
-        return self._storage.keys()
+    def __setitem__(self, key, value: Any) -> None:
+        self._keys.add(key)
+        storage = self._get_corresponding_storage(key)
+        storage[key] = value
 
     def __deepcopy__(self, memodict={}):
+        concrete = isinstance(self._standard_storage, K)
         storage = Storage(
-            concrete=self.concrete, address=self.address, dynamic_loader=self.dynld
+            concrete=concrete,
+            address=self.address,
+            dynamic_loader=self.dynld,
+            keys=deepcopy(self._keys),
         )
-        storage._storage = copy(self._storage)
+        storage._standard_storage = deepcopy(self._standard_storage)
+        storage._map_storage = deepcopy(self._map_storage)
         return storage
 
     def __str__(self):
-        return str(self._storage)
+        return str(self._standard_storage)
+
+    def keys(self):
+        return self._keys
 
 
 class Account:
@@ -158,13 +165,13 @@ class Account:
             "storage": self.storage,
         }
 
-    def __deepcopy__(self, memodict={}):
+    def __copy__(self, memodict={}):
         new_account = Account(
             address=self.address,
             code=self.code,
             contract_name=self.contract_name,
             balances=self._balances,
         )
-        new_account.storage = deepcopy(self.storage)
+        new_account.storage = copy(self.storage)
         new_account.code = self.code
         return new_account

mythril/laser/ethereum/state/constraints.py

@@ -1,7 +1,7 @@
 """This module contains the class used to represent state-change constraints in
 the call graph."""
 
-from mythril.laser.smt import Solver, Bool, symbol_factory
+from mythril.laser.smt import Solver, Bool, symbol_factory, simplify
 
 from typing import Iterable, List, Optional, Union
 from z3 import unsat
@@ -54,7 +54,9 @@ class Constraints(list):
 
         :param constraint: The constraint to be appended
         """
-        constraint = constraint if isinstance(constraint, Bool) else Bool(constraint)
+        constraint = (
+            simplify(constraint) if isinstance(constraint, Bool) else Bool(constraint)
+        )
         super(Constraints, self).append(constraint)
         self._is_possible = None
 

mythril/laser/ethereum/state/global_state.py

@@ -61,6 +61,7 @@ class GlobalState:
         environment = copy(self.environment)
         mstate = deepcopy(self.mstate)
         transaction_stack = copy(self.transaction_stack)
+        environment.active_account = world_state[environment.active_account.address]
         return GlobalState(
             world_state,
             environment,

mythril/laser/smt/array.py

@@ -8,7 +8,8 @@ default values over a certain range.
 from typing import cast
 import z3
 
-from mythril.laser.smt.bitvec import BitVec
+from mythril.laser.smt.bitvec import BitVec, If
+from mythril.laser.smt.bool import Bool
 
 
 class BaseArray:
@@ -24,6 +25,9 @@ class BaseArray:
 
     def __setitem__(self, key: BitVec, value: BitVec) -> None:
         """Sets an item in the array, key can be symbolic."""
+        if isinstance(value, Bool):
+            value = If(value, 1, 0)
+
         self.raw = z3.Store(self.raw, key.raw, value.raw)  # type: ignore
 
 

mythril/laser/smt/bitvecfunc.py

@@ -205,7 +205,7 @@ class BitVecFunc(BitVec):
         :return: The resulting Bool
         """
         return _comparison_helper(
-            self, other, operator.eq, default_value=True, inputs_equal=False
+            self, other, operator.ne, default_value=True, inputs_equal=False
         )
 
     def __lshift__(self, other: Union[int, "BitVec"]) -> "BitVec":
@@ -223,3 +223,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."""
@@ -90,6 +93,13 @@ def And(*args: Union[Bool, bool]) -> Bool:
     return Bool(z3.And([a.raw for a in args_list]), union)
 
 
+def Xor(a: Bool, b: Bool) -> Bool:
+    """Create an And expression."""
+
+    union = a.annotations + b.annotations
+    return Bool(z3.Xor(a.raw, b.raw), union)
+
+
 def Or(*args: Union[Bool, bool]) -> Bool:
     """Create an or 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/instructions/codecopy_test.py

@@ -10,9 +10,13 @@ from mythril.laser.ethereum.transaction.transaction_models import MessageCallTra
 
 def test_codecopy_concrete():
     # Arrange
-    active_account = Account("0x0", code=Disassembly("60606040"))
-    environment = Environment(active_account, None, None, None, None, None)
-    og_state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
+    world_state = WorldState()
+    account = world_state.create_account(balance=10, address=101)
+    account.code = Disassembly("60606040")
+    environment = Environment(account, None, None, None, None, None)
+    og_state = GlobalState(
+        world_state, environment, None, MachineState(gas_limit=8000000)
+    )
     og_state.transaction_stack.append(
         (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
     )

tests/instructions/sar_test.py

@@ -2,6 +2,7 @@ import pytest
 
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.ethereum.state.environment import Environment
+from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.machine_state import MachineState
 from mythril.laser.ethereum.state.global_state import GlobalState
@@ -12,9 +13,11 @@ from mythril.laser.smt import symbol_factory, simplify
 
 
 def get_state():
-    active_account = Account("0x0", code=Disassembly("60606040"))
-    environment = Environment(active_account, None, None, None, None, None)
-    state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
+    world_state = WorldState()
+    account = world_state.create_account(balance=10, address=101)
+    account.code = Disassembly("60606040")
+    environment = Environment(account, None, None, None, None, None)
+    state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000))
     state.transaction_stack.append(
         (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
     )

tests/instructions/shl_test.py

@@ -12,9 +12,11 @@ from mythril.laser.smt import symbol_factory, simplify
 
 
 def get_state():
-    active_account = Account("0x0", code=Disassembly("60606040"))
-    environment = Environment(active_account, None, None, None, None, None)
-    state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
+    world_state = WorldState()
+    account = world_state.create_account(balance=10, address=101)
+    account.code = Disassembly("60606040")
+    environment = Environment(account, None, None, None, None, None)
+    state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000))
     state.transaction_stack.append(
         (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
     )

tests/instructions/shr_test.py

@@ -12,9 +12,11 @@ from mythril.laser.smt import symbol_factory, simplify, LShR
 
 
 def get_state():
-    active_account = Account("0x0", code=Disassembly("60606040"))
-    environment = Environment(active_account, None, None, None, None, None)
-    state = GlobalState(None, environment, None, MachineState(gas_limit=8000000))
+    world_state = WorldState()
+    account = world_state.create_account(balance=10, address=101)
+    account.code = Disassembly("60606040")
+    environment = Environment(account, None, None, None, None, None)
+    state = GlobalState(world_state, environment, None, MachineState(gas_limit=8000000))
     state.transaction_stack.append(
         (MessageCallTransaction(world_state=WorldState(), gas_limit=8000000), None)
     )

tests/laser/evm_testsuite/evm_test.py

@@ -125,7 +125,8 @@ def test_vmtest(
         account.code = Disassembly(details["code"][2:])
         account.nonce = int(details["nonce"], 16)
         for key, value in details["storage"].items():
-            account.storage[int(key, 16)] = int(value, 16)
+            key_bitvec = symbol_factory.BitVecVal(int(key, 16), 256)
+            account.storage[key_bitvec] = symbol_factory.BitVecVal(int(value, 16), 256)
 
         world_state.put_account(account)
         account.set_balance(int(details["balance"], 16))
@@ -175,8 +176,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/laser/state/storage_test.py

@@ -1,53 +0,0 @@
-import pytest
-from mythril.laser.ethereum.state.account import Storage
-from mythril.laser.smt import Expression
-
-storage_uninitialized_test_data = [({}, 1), ({1: 5}, 2), ({1: 5, 3: 10}, 2)]
-
-
-@pytest.mark.parametrize("initial_storage,key", storage_uninitialized_test_data)
-def test_concrete_storage_uninitialized_index(initial_storage, key):
-    # Arrange
-    storage = Storage(concrete=True)
-    storage._storage = initial_storage
-
-    # Act
-    value = storage[key]
-
-    # Assert
-    assert value == 0
-
-
-@pytest.mark.parametrize("initial_storage,key", storage_uninitialized_test_data)
-def test_symbolic_storage_uninitialized_index(initial_storage, key):
-    # Arrange
-    storage = Storage(concrete=False)
-    storage._storage = initial_storage
-
-    # Act
-    value = storage[key]
-
-    # Assert
-    assert isinstance(value, Expression)
-
-
-def test_storage_set_item():
-    # Arrange
-    storage = Storage()
-
-    # Act
-    storage[1] = 13
-
-    # Assert
-    assert storage[1] == 13
-
-
-def test_storage_change_item():
-    # Arrange
-    storage = Storage()
-    storage._storage = {1: 12}
-    # Act
-    storage[1] = 14
-
-    # Assert
-    assert storage[1] == 14

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

@@ -1,5 +1,19 @@
 {
     "error": null,
-    "issues": [],
+    "issues": [
+        {
+            "address": 498,
+            "contract": "Unknown",
+            "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": "sendToken(address,uint256)",
+            "max_gas_used": 52806,
+            "min_gas_used": 11860,
+            "severity": "High",
+            "sourceMap": null,
+            "swc-id": "101",
+            "title": "Integer Overflow",
+            "tx_sequence": "<TX-DATA>"
+        }
+    ],
     "success": true
 }

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

@@ -1,6 +1,25 @@
 [
     {
-        "issues": [],
+        "issues": [
+            {
+                "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>",
+                    "testCase": "<TEST-CASE>"
+                },
+                "locations": [
+                    {
+                        "sourceMap": "498:1:0"
+                    }
+                ],
+                "severity": "High",
+                "swcID": "SWC-101",
+                "swcTitle": "Integer Overflow and Underflow"
+            }
+        ],
         "meta": {},
         "sourceFormat": "evm-byzantium-bytecode",
         "sourceList": [

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

@@ -1,3 +1,14 @@
-# Analysis results for None
+# Analysis results for test-filename.sol
 
-The analysis was completed successfully. No issues were detected.
+## Integer Overflow
+- SWC ID: 101
+- Severity: High
+- Contract: Unknown
+- Function name: `sendToken(address,uint256)`
+- PC address: 498
+- Estimated Gas Usage: 11860 - 52806
+
+### 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/metacoin.sol.o.text

@@ -1 +1,11 @@
-The analysis was completed successfully. No issues were detected.
+==== Integer Overflow ====
+SWC ID: 101
+Severity: High
+Contract: Unknown
+Function name: sendToken(address,uint256)
+PC address: 498
+Estimated Gas Usage: 11860 - 52806
+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.
+--------------------
+