Merge branch 'develop' into analyze-with-mythx

myth

@@ -11,7 +11,7 @@ import warnings
 
 
 def format_Warning(message, category, filename, lineno, line=""):
-    return "Deprecated Warning: {}\n\n".format(str(message))
+    return "Deprecation warning: {}\n\n".format(str(message))
 
 
 warnings.formatwarning = format_Warning
@@ -21,6 +21,10 @@ if __name__ == "__main__":
         if arg in COMMAND_LIST:
             mythril.interfaces.cli.main()
             exit()
+    if "--help" in argv or "-h" in argv:
+        mythril.interfaces.cli.main()
+        exit()
+
     warnings.warn("The old cli arguments are deprecated, Please use 'myth -h' to view the new command line interface")
     mythril.interfaces.old_cli.main()
 

mythril/__version__.py

@@ -4,4 +4,4 @@ This file is suitable for sourcing inside POSIX shell, e.g. bash as well
 as for importing into Python.
 """
 
-__version__ = "v0.21.3"
+__version__ = "v0.21.4"

mythril/analysis/modules/dos.py

@@ -9,17 +9,24 @@ from mythril.analysis.modules.base import DetectionModule
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.state.annotation import StateAnnotation
 from mythril.laser.ethereum import util
+from copy import copy
 
 log = logging.getLogger(__name__)
 
 
-class LoopAnnotation(StateAnnotation):
-    def __init__(self, loop_start: int, loop_end: int) -> None:
-        self.loop_start = loop_start
-        self.loop_end = loop_end
+class VisitsAnnotation(StateAnnotation):
+    """State annotation that stores the addresses of state-modifying operations"""
 
-    def contains(self, address: int) -> bool:
-        return self.loop_start < address < self.loop_end
+    def __init__(self) -> None:
+        self.loop_start = None
+        self.jump_targets = []  # type: List[int]
+
+    def __copy__(self):
+        result = VisitsAnnotation()
+
+        result.loop_start = self.loop_start
+        result.jump_targets = copy(self.jump_targets)
+        return result
 
 
 class DOS(DetectionModule):
@@ -37,12 +44,9 @@ class DOS(DetectionModule):
             swc_id=DOS_WITH_BLOCK_GAS_LIMIT,
             description="Check for DOS",
             entrypoint="callback",
-            pre_hooks=["JUMPI", "CALL", "SSTORE"],
+            pre_hooks=["JUMP", "JUMPI", "CALL", "SSTORE"],
         )
 
-        """Keeps track of how often jump destinations are reached."""
-        self._jumpdest_count = {}  # type: Dict[object, dict]
-
     def _execute(self, state: GlobalState) -> None:
 
         """
@@ -61,65 +65,53 @@ class DOS(DetectionModule):
         opcode = state.get_current_instruction()["opcode"]
         address = state.get_current_instruction()["address"]
 
-        if opcode == "JUMPI":
-
-            target = util.get_concrete_int(state.mstate.stack[-1])
+        annotations = cast(
+            List[VisitsAnnotation], list(state.get_annotations(VisitsAnnotation))
+        )
 
-            transaction = state.current_transaction
-            if state.current_transaction in self._jumpdest_count:
+        if len(annotations) == 0:
+            annotation = VisitsAnnotation()
+            state.annotate(annotation)
+        else:
+            annotation = annotations[0]
 
-                try:
-                    self._jumpdest_count[transaction][target] += 1
-                    if self._jumpdest_count[transaction][target] == 3:
+        if opcode in ["JUMP", "JUMPI"]:
+            target = util.get_concrete_int(state.mstate.stack[-1])
 
-                        annotation = (
-                            LoopAnnotation(address, target)
-                            if target > address
-                            else LoopAnnotation(target, address)
-                        )
+            if annotation.loop_start is None:
+                if target in annotation.jump_targets:
+                    annotation.loop_start = address
+                else:
+                    annotation.jump_targets.append(target)
 
-                        state.annotate(annotation)
-                except KeyError:
-                    self._jumpdest_count[transaction][target] = 0
+        elif annotation.loop_start is not None:
 
+            if opcode == "CALL":
+                operation = "A message call"
             else:
-                self._jumpdest_count[transaction] = {}
-                self._jumpdest_count[transaction][target] = 0
+                operation = "A storage modification"
 
-        else:
+            description_head = (
+                "Potential denial-of-service if block gas limit is reached."
+            )
+            description_tail = "{} is executed in a loop. Be aware that the transaction may fail to execute if the loop is unbounded and the necessary gas exceeds the block gas limit.".format(
+                operation
+            )
 
-            annotations = cast(
-                List[LoopAnnotation], list(state.get_annotations(LoopAnnotation))
+            issue = Issue(
+                contract=state.environment.active_account.contract_name,
+                function_name=state.environment.active_function_name,
+                address=annotation.loop_start,
+                swc_id=DOS_WITH_BLOCK_GAS_LIMIT,
+                bytecode=state.environment.code.bytecode,
+                title="Potential denial-of-service if block gas limit is reached",
+                severity="Low",
+                description_head=description_head,
+                description_tail=description_tail,
+                gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
             )
 
-            for annotation in annotations:
-
-                if annotation.contains(address):
-
-                    operation = (
-                        "A storage modification"
-                        if opcode == "SSTORE"
-                        else "An external call"
-                    )
-
-                    description_head = (
-                        "Potential denial-of-service if block gas limit is reached."
-                    )
-                    description_tail = "{} is executed in a loop.".format(operation)
-
-                    issue = Issue(
-                        contract=state.environment.active_account.contract_name,
-                        function_name=state.environment.active_function_name,
-                        address=annotation.loop_start,
-                        swc_id=DOS_WITH_BLOCK_GAS_LIMIT,
-                        bytecode=state.environment.code.bytecode,
-                        title="Potential denial-of-service if block gas limit is reached",
-                        severity="Low",
-                        description_head=description_head,
-                        description_tail=description_tail,
-                        gas_used=(state.mstate.min_gas_used, state.mstate.max_gas_used),
-                    )
-                    return [issue]
+            return [issue]
 
         return []
 

mythril/analysis/modules/integer.py

@@ -75,7 +75,17 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 "there's a possible state where op1 + op0 > 2^32 - 1"
             ),
             entrypoint="callback",
-            pre_hooks=["ADD", "MUL", "EXP", "SUB", "SSTORE", "JUMPI", "STOP", "RETURN"],
+            pre_hooks=[
+                "ADD",
+                "MUL",
+                "EXP",
+                "SUB",
+                "SSTORE",
+                "JUMPI",
+                "STOP",
+                "RETURN",
+                "CALL",
+            ],
         )
 
         """
@@ -121,6 +131,7 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             "MUL": [self._handle_mul],
             "SSTORE": [self._handle_sstore],
             "JUMPI": [self._handle_jumpi],
+            "CALL": [self._handle_call],
             "RETURN": [self._handle_return, self._handle_transaction_end],
             "STOP": [self._handle_transaction_end],
             "EXP": [self._handle_exp],
@@ -230,7 +241,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 or annotation.overflowing_state in state_annotation.ostates_seen
             ):
                 continue
-
             state_annotation.overflowing_state_annotations.append(annotation)
             state_annotation.ostates_seen.add(annotation.overflowing_state)
 
@@ -248,7 +258,23 @@ class IntegerOverflowUnderflowModule(DetectionModule):
                 or annotation.overflowing_state in state_annotation.ostates_seen
             ):
                 continue
+            state_annotation.overflowing_state_annotations.append(annotation)
+            state_annotation.ostates_seen.add(annotation.overflowing_state)
+
+    @staticmethod
+    def _handle_call(state):
+
+        stack = state.mstate.stack
+        value = stack[-3]
+
+        state_annotation = _get_overflowunderflow_state_annotation(state)
 
+        for annotation in value.annotations:
+            if (
+                not isinstance(annotation, OverUnderflowAnnotation)
+                or annotation.overflowing_state in state_annotation.ostates_seen
+            ):
+                continue
             state_annotation.overflowing_state_annotations.append(annotation)
             state_annotation.ostates_seen.add(annotation.overflowing_state)
 
@@ -311,7 +337,6 @@ class IntegerOverflowUnderflowModule(DetectionModule):
             try:
 
                 constraints = state.mstate.constraints + [annotation.constraint]
-
                 transaction_sequence = solver.get_transaction_sequence(
                     state, constraints
                 )

mythril/analysis/ops.py

@@ -91,11 +91,3 @@ class Call(Op):
         self.type = _type
         self.value = value
         self.data = data
-
-
-class SStore(Op):
-    """The respresentation of an SSTORE operation."""
-
-    def __init__(self, node, state, state_index, value):
-        super().__init__(node, state, state_index)
-        self.value = value

mythril/analysis/report.py

@@ -67,19 +67,12 @@ class Issue:
 
     @property
     def transaction_sequence_users(self):
-        """ Returns the transaction sequence in json without pre-generated block data"""
-        return (
-            json.dumps(self.transaction_sequence, indent=4)
-            if self.transaction_sequence
-            else None
-        )
+        """ Returns the transaction sequence without pre-generated block data"""
+        return self.transaction_sequence
 
     @property
     def transaction_sequence_jsonv2(self):
-        """
-        Returns the transaction sequence with pre-generated block data.
-        Jsonv2 tx sequence isn't formatted for user readability.
-        """
+        """ Returns the transaction sequence as a json string with pre-generated block data"""
         return (
             self.add_block_data(self.transaction_sequence)
             if self.transaction_sequence
@@ -105,6 +98,7 @@ class Issue:
 
         :return:
         """
+
         issue = {
             "title": self.title,
             "swc-id": self.swc_id,
@@ -113,7 +107,7 @@ class Issue:
             "function": self.function,
             "severity": self.severity,
             "address": self.address,
-            "tx_sequence": self.transaction_sequence_users,
+            "tx_sequence": self.transaction_sequence,
             "min_gas_used": self.min_gas_used,
             "max_gas_used": self.max_gas_used,
             "sourceMap": self.source_mapping,
@@ -165,13 +159,13 @@ class Report:
         loader=PackageLoader("mythril.analysis"), trim_blocks=True
     )
 
-    def __init__(self, verbose=False, contracts=None, exceptions=None):
+    def __init__(self, contracts=None, exceptions=None):
         """
 
-        :param verbose:
+        :param contracts:
+        :param exceptions:
         """
         self.issues = {}
-        self.verbose = verbose
         self.solc_version = ""
         self.meta = {}
         self.source = Source()
@@ -203,9 +197,7 @@ class Report:
         name = self._file_name()
         template = Report.environment.get_template("report_as_text.jinja2")
 
-        return template.render(
-            filename=name, issues=self.sorted_issues(), verbose=self.verbose
-        )
+        return template.render(filename=name, issues=self.sorted_issues())
 
     def as_json(self):
         """
@@ -274,9 +266,7 @@ class Report:
         """
         filename = self._file_name()
         template = Report.environment.get_template("report_as_markdown.jinja2")
-        return template.render(
-            filename=filename, issues=self.sorted_issues(), verbose=self.verbose
-        )
+        return template.render(filename=filename, issues=self.sorted_issues())
 
     def _file_name(self):
         """

mythril/analysis/symbolic.py

@@ -1,12 +1,9 @@
 """This module contains a wrapper around LASER for extended analysis
 purposes."""
 
-import copy
 
 from mythril.analysis.security import get_detection_module_hooks, get_detection_modules
 from mythril.laser.ethereum import svm
-from mythril.laser.ethereum.plugins.plugin_factory import PluginFactory
-from mythril.laser.ethereum.plugins.plugin_loader import LaserPluginLoader
 from mythril.laser.ethereum.state.account import Account
 from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.strategy.basic import (
@@ -30,9 +27,9 @@ from mythril.laser.ethereum.strategy.extensions.bounded_loops import (
     BoundedLoopsStrategy,
 )
 from mythril.laser.smt import symbol_factory, BitVec
-from typing import Union, List, Dict, Type
+from typing import Union, List, Type
 from mythril.solidity.soliditycontract import EVMContract, SolidityContract
-from .ops import Call, SStore, VarType, get_variable
+from .ops import Call, VarType, get_variable
 
 
 class SymExecWrapper:
@@ -50,7 +47,7 @@ class SymExecWrapper:
         dynloader=None,
         max_depth=22,
         execution_timeout=None,
-        loop_bound=4,
+        loop_bound=2,
         create_timeout=None,
         transaction_count=2,
         modules=(),
@@ -158,7 +155,9 @@ class SymExecWrapper:
                 contract.disassembly,
                 dynamic_loader=dynloader,
                 contract_name=contract.name,
-                concrete_storage=False,
+                concrete_storage=True
+                if (dynloader is not None and dynloader.storage_loading)
+                else False,
             )
             world_state.put_account(account)
             self.laser.sym_exec(world_state=world_state, target_address=address.value)
@@ -169,10 +168,9 @@ class SymExecWrapper:
         self.nodes = self.laser.nodes
         self.edges = self.laser.edges
 
-        # Generate lists of interesting operations
+        # Parse calls to make them easily accessible
 
         self.calls = []  # type: List[Call]
-        self.sstors = {}  # type: Dict[int, Dict[str, List[SStore]]]
 
         for key in self.nodes:
 
@@ -247,50 +245,4 @@ class SymExecWrapper:
                             Call(self.nodes[key], state, state_index, op, to, gas)
                         )
 
-                elif op == "SSTORE":
-                    stack = copy.copy(state.mstate.stack)
-                    address = state.environment.active_account.address.value
-
-                    index, value = stack.pop(), stack.pop()
-
-                    try:
-                        self.sstors[address]
-                    except KeyError:
-                        self.sstors[address] = {}
-
-                    try:
-                        self.sstors[address][str(index)].append(
-                            SStore(self.nodes[key], state, state_index, value)
-                        )
-                    except KeyError:
-                        self.sstors[address][str(index)] = [
-                            SStore(self.nodes[key], state, state_index, value)
-                        ]
-
                 state_index += 1
-
-    def find_storage_write(self, address, index):
-        """
-
-        :param address:
-        :param index:
-        :return:
-        """
-        # Find an SSTOR not constrained by caller that writes to storage index "index"
-
-        try:
-            for s in self.sstors[address][index]:
-
-                taint = True
-
-                for constraint in s.node.constraints:
-                    if "caller" in str(constraint):
-                        taint = False
-                        break
-
-                if taint:
-                    return s.node.function_name
-
-            return None
-        except KeyError:
-            return None

mythril/analysis/templates/report_as_markdown.jinja2

@@ -30,15 +30,20 @@ In file: {{ issue.filename }}
 {{ issue.code }}
 ```
 {% endif %}
-{% if verbose and issue.tx_sequence %}
---------------------
-### Debugging Information:
+{% if issue.tx_sequence %}
 
-{{ issue.tx_sequence }}
+### Transaction Sequence
 
+{% for step in issue.tx_sequence.steps %}
+{% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
+Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
+{% else %}
+Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, data: {{ step.input }}, value: {{ step.value }}
 {% endif %}
 {% endfor %}
-{% else %}
+{% endif %}
 
+{% endfor %}
+{% else %}
 The analysis was completed successfully. No issues were detected.
 {% endif %}

mythril/analysis/templates/report_as_text.jinja2

@@ -22,11 +22,16 @@ In file: {{ issue.filename }}:{{ issue.lineno }}
 
 --------------------
 {% endif %}
-{% if verbose and issue.tx_sequence %}
---------------------
+{% if issue.tx_sequence %}
 Transaction Sequence:
 
-{{ issue.tx_sequence }}
+{% for step in issue.tx_sequence.steps %}
+{% if step == issue.tx_sequence.steps[0] and step.input != "0x" and step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}
+Caller: [CREATOR], data: [CONTRACT CREATION], value: {{ step.value }}
+{% else %}
+Caller: {% if step.origin == "0xaffeaffeaffeaffeaffeaffeaffeaffeaffeaffe" %}[CREATOR]{% elif step.origin == "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" %}[ATTACKER]{% else %}[SOMEGUY]{% endif %}, data: {{ step.input }}, value: {{ step.value }}
+{% endif %}
+{% endfor %}
 {% endif %}
 
 {% endfor %}

mythril/interfaces/cli.py

@@ -133,11 +133,6 @@ def get_output_parser() -> ArgumentParser:
         help="report output format",
         metavar="<text/markdown/json/jsonv2>",
     )
-    parser.add_argument(
-        "--verbose-report",
-        action="store_true",
-        help="Include debugging information in report",
-    )
     return parser
 
 
@@ -382,7 +377,7 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
         "-b",
         "--loop-bound",
         type=int,
-        default=4,
+        default=2,
         help="Bound loops at n iterations",
         metavar="N",
     )
@@ -658,7 +653,6 @@ def execute_command(
                     modules=[m.strip() for m in args.modules.strip().split(",")]
                     if args.modules
                     else [],
-                    verbose_report=args.verbose_report,
                     transaction_count=args.transaction_count,
                 )
                 outputs = {

mythril/interfaces/old_cli.py

@@ -148,11 +148,6 @@ def create_parser(parser: argparse.ArgumentParser) -> None:
         help="report output format",
         metavar="<text/markdown/json/jsonv2>",
     )
-    outputs.add_argument(
-        "--verbose-report",
-        action="store_true",
-        help="Include debugging information in report",
-    )
 
     database = parser.add_argument_group("local contracts database")
     database.add_argument(
@@ -460,7 +455,6 @@ def execute_command(
                     modules=[m.strip() for m in args.modules.strip().split(",")]
                     if args.modules
                     else [],
-                    verbose_report=args.verbose_report,
                     transaction_count=args.transaction_count,
                 )
                 outputs = {

mythril/laser/ethereum/instructions.py

@@ -18,13 +18,11 @@ from mythril.laser.smt import (
     ULT,
     UGT,
     BitVec,
-    is_true,
     is_false,
     URem,
     SRem,
     If,
     Bool,
-    Or,
     Not,
     LShR,
 )
@@ -41,7 +39,6 @@ from mythril.laser.ethereum.evm_exceptions import (
     OutOfGasException,
 )
 from mythril.laser.ethereum.gas import OPCODE_GAS
-from mythril.laser.ethereum.keccak import KeccakFunctionManager
 from mythril.laser.ethereum.state.global_state import GlobalState
 from mythril.laser.ethereum.transaction import (
     MessageCallTransaction,
@@ -56,8 +53,6 @@ log = logging.getLogger(__name__)
 TT256 = 2 ** 256
 TT256M1 = 2 ** 256 - 1
 
-keccak_function_manager = KeccakFunctionManager()
-
 
 class StateTransition(object):
     """Decorator that handles global state copy and original return.
@@ -193,7 +188,6 @@ class Instruction:
             if not post
             else getattr(self, op + "_" + "post", None)
         )
-
         if instruction_mutator is None:
             raise NotImplementedError
 
@@ -417,6 +411,7 @@ class Instruction:
                 * helper.pop_bitvec(global_state.mstate)
             )
         )
+
         return [global_state]
 
     @StateTransition()
@@ -552,11 +547,15 @@ class Instruction:
 
             state.stack.append(
                 global_state.new_bitvec(
-                    "(" + str(simplify(base)) + ")**(" + str(simplify(exponent)) + ")",
+                    "invhash("
+                    + str(hash(simplify(base)))
+                    + ")**invhash("
+                    + str(hash(simplify(exponent)))
+                    + ")",
                     256,
                     base.annotations + exponent.annotations,
                 )
-            )
+            )  # Hash is used because str(symbol) takes a long time to be converted to a string
         else:
 
             state.stack.append(
@@ -774,13 +773,8 @@ class Instruction:
         if size > 0:
             try:
                 state.mem_extend(mstart, size)
-            except TypeError:
-                log.debug(
-                    "Memory allocation error: mstart = "
-                    + str(mstart)
-                    + ", size = "
-                    + str(size)
-                )
+            except TypeError as e:
+                log.debug("Memory allocation error: {}".format(e))
                 state.mem_extend(mstart, 1)
                 state.memory[mstart] = global_state.new_bitvec(
                     "calldata_"
@@ -893,7 +887,6 @@ class Instruction:
         :param global_state:
         :return:
         """
-        global keccak_function_manager
 
         state = global_state.mstate
         op0, op1 = state.stack.pop(), state.stack.pop()
@@ -936,7 +929,7 @@ class Instruction:
 
             for b in state.memory[index : index + length]:
                 if isinstance(b, BitVec):
-                    annotations.append(b.annotations)
+                    annotations += b.annotations
 
             argument_str = str(state.memory[index]).replace(" ", "_")
             result = symbol_factory.BitVecFuncSym(
@@ -948,7 +941,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(
@@ -1318,21 +1310,19 @@ class Instruction:
         state = global_state.mstate
         op0 = state.stack.pop()
 
-        log.debug("MLOAD[" + str(op0) + "]")
-
         try:
             offset = util.get_concrete_int(op0)
         except TypeError:
             log.debug("Can't MLOAD from symbolic index")
-            data = global_state.new_bitvec("mem[" + str(simplify(op0)) + "]", 256)
+            data = global_state.new_bitvec(
+                "mem[invhash(" + str(hash(simplify(op0))) + ")]", 256
+            )
             state.stack.append(data)
             return [global_state]
 
         state.mem_extend(offset, 32)
         data = state.memory.get_word_at(offset)
 
-        log.debug("Load from memory[" + str(offset) + "]: " + str(data))
-
         state.stack.append(data)
         return [global_state]
 
@@ -1355,9 +1345,7 @@ class Instruction:
         try:
             state.mem_extend(mstart, 32)
         except Exception:
-            log.debug("Error extending memory, mstart = " + str(mstart) + ", size = 32")
-
-        log.debug("MSTORE to mem[" + str(mstart) + "]: " + str(value))
+            log.debug("Error extending memory")
 
         state.memory.write_word_at(mstart, value)
 
@@ -1387,7 +1375,6 @@ class Instruction:
             )  # type: Union[int, BitVec]
         except TypeError:  # BitVec
             value_to_write = Extract(7, 0, value)
-        log.debug("MSTORE8 to mem[" + str(offset) + "]: " + str(value_to_write))
 
         state.memory[offset] = value_to_write
 
@@ -1400,86 +1387,13 @@ class Instruction:
         :param global_state:
         :return:
         """
-        global keccak_function_manager
 
         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))
-
-    @staticmethod
-    def _sload_helper(
-        global_state: GlobalState, index: Union[str, int], constraints=None
-    ):
-        """
-
-        :param global_state:
-        :param index:
-        :param constraints:
-        :return:
-        """
-        try:
-            data = global_state.environment.active_account.storage[index]
-        except KeyError:
-            data = global_state.new_bitvec("storage_" + str(index), 256)
-            global_state.environment.active_account.storage[index] = data
 
-        if constraints is not None:
-            global_state.mstate.constraints += constraints
-
-        global_state.mstate.stack.append(data)
+        state.stack.append(global_state.environment.active_account.storage[index])
         return [global_state]
 
-    @staticmethod
-    def _get_constraints(keccak_keys, this_key, argument):
-        """
-
-        :param keccak_keys:
-        :param this_key:
-        :param argument:
-        """
-        global keccak_function_manager
-        for keccak_key in keccak_keys:
-            if keccak_key == this_key:
-                continue
-            keccak_argument = keccak_function_manager.get_argument(keccak_key)
-            yield keccak_argument != argument
-
     @StateTransition()
     def sstore_(self, global_state: GlobalState) -> List[GlobalState]:
         """
@@ -1487,90 +1401,10 @@ class Instruction:
         :param global_state:
         :return:
         """
-        global keccak_function_manager
         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)
-            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)
-
-    @staticmethod
-    def _sstore_helper(global_state, index, value, constraint=None):
-        """
-
-        :param global_state:
-        :param index:
-        :param value:
-        :param constraint:
-        :return:
-        """
-        try:
-            global_state.environment.active_account = deepcopy(
-                global_state.environment.active_account
-            )
-            global_state.accounts[
-                global_state.environment.active_account.address.value
-            ] = global_state.environment.active_account
-
-            global_state.environment.active_account.storage[index] = (
-                value if not isinstance(value, Expression) else simplify(value)
-            )
-        except KeyError:
-            log.debug("Error writing to storage: Invalid index")
-
-        if constraint is not None:
-            global_state.mstate.constraints.append(constraint)
 
+        global_state.environment.active_account.storage[index] = value
         return [global_state]
 
     @StateTransition(increment_pc=False, enable_gas=False)

mythril/laser/ethereum/keccak.py

@@ -1,38 +0,0 @@
-"""This module contains a function manager to deal with symbolic Keccak
-values."""
-from mythril.laser.smt import Expression
-
-
-class KeccakFunctionManager:
-    """A keccak function manager for symbolic expressions."""
-
-    def __init__(self):
-        """"""
-        self.keccak_expression_mapping = {}
-
-    def is_keccak(self, expression: Expression) -> bool:
-        """
-
-        :param expression:
-        :return:
-        """
-        return str(expression) in self.keccak_expression_mapping.keys()
-
-    def get_argument(self, expression: Expression) -> Expression:
-        """
-
-        :param expression:
-        :return:
-        """
-        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)

mythril/laser/ethereum/state/account.py

@@ -2,12 +2,20 @@
 
 This includes classes representing accounts and their storage.
 """
-from copy import deepcopy, copy
-from typing import Any, Dict, KeysView, Union
-
-from z3 import ExprRef
-
-from mythril.laser.smt import Array, symbol_factory, BitVec
+from copy import copy, deepcopy
+from typing import Any, Dict, Union, Tuple, cast
+
+
+from mythril.laser.smt import (
+    Array,
+    K,
+    BitVec,
+    simplify,
+    BitVecFunc,
+    Extract,
+    BaseArray,
+    Concat,
+)
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.smt import symbol_factory
 
@@ -20,62 +28,105 @@ class 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)  # type: BaseArray
+        else:
+            self._standard_storage = Array("Storage", 256, 256)
+        self._map_storage = {}  # type: Dict[BitVec, BaseArray]
+
+        self.printable_storage = {}  # type: Dict[BitVec, BitVec]
+
         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=hex(self.address.value),
-                                index=int(item),
-                            ),
-                            16,
+    @staticmethod
+    def _sanitize(input_: BitVec) -> BitVec:
+        if input_.size() == 512:
+            return input_
+        if input_.size() > 512:
+            return Extract(511, 0, input_)
+        else:
+            return Concat(symbol_factory.BitVecVal(0, 512 - input_.size()), input_)
+
+    def __getitem__(self, item: BitVec) -> BitVec:
+        storage, is_keccak_storage = self._get_corresponding_storage(item)
+        if is_keccak_storage:
+            item = self._sanitize(cast(BitVecFunc, item).input_)
+        value = storage[item]
+        if (
+            value.value == 0
+            and self.address
+            and item.symbolic is False
+            and self.address.value != 0
+            and (self.dynld and self.dynld.storage_loading)
+        ):
+            try:
+                storage[item] = symbol_factory.BitVecVal(
+                    int(
+                        self.dynld.read_storage(
+                            contract_address=hex(self.address.value),
+                            index=int(item.value),
                         ),
-                        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:
-        """
-
-        :return:
-        """
-        return self._storage.keys()
+                        16,
+                    ),
+                    256,
+                )
+                self.printable_storage[item] = storage[item]
+                return storage[item]
+            except ValueError:
+                pass
+
+        return simplify(storage[item])
+
+    @staticmethod
+    def get_map_index(key: BitVec) -> BitVec:
+        if (
+            not isinstance(key, BitVecFunc)
+            or key.func_name != "keccak256"
+            or key.input_ is None
+        ):
+            return None
+        index = Extract(255, 0, key.input_)
+        return simplify(index)
+
+    def _get_corresponding_storage(self, key: BitVec) -> Tuple[BaseArray, bool]:
+        index = self.get_map_index(key)
+        if index is None:
+            storage = self._standard_storage
+            is_keccak_storage = False
+        else:
+            storage_map = self._map_storage
+            try:
+                storage = storage_map[index]
+            except KeyError:
+                if isinstance(self._standard_storage, Array):
+                    storage_map[index] = Array("Storage", 512, 256)
+                else:
+                    storage_map[index] = K(512, 256, 0)
+                storage = storage_map[index]
+            is_keccak_storage = True
+        return storage, is_keccak_storage
+
+    def __setitem__(self, key, value: Any) -> None:
+        storage, is_keccak_storage = self._get_corresponding_storage(key)
+        self.printable_storage[key] = value
+        if is_keccak_storage:
+            key = self._sanitize(key.input_)
+        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
         )
-        storage._storage = copy(self._storage)
+        storage._standard_storage = deepcopy(self._standard_storage)
+        storage._map_storage = deepcopy(self._map_storage)
+        storage.print_storage = copy(self.printable_storage)
         return storage
 
-    def __str__(self):
-        return str(self._storage)
+    def __str__(self) -> str:
+        # TODO: Do something better here
+        return str(self.printable_storage)
 
 
 class Account:
@@ -159,7 +210,7 @@ class Account:
             "storage": self.storage,
         }
 
-    def __deepcopy__(self, memodict={}):
+    def __copy__(self, memodict={}):
         new_account = Account(
             address=self.address,
             code=self.code,

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/ethereum/strategy/extensions/bounded_loops.py

@@ -14,11 +14,11 @@ class JumpdestCountAnnotation(StateAnnotation):
     """State annotation that counts the number of jumps per destination."""
 
     def __init__(self) -> None:
-        self._jumpdest_count = {}  # type: Dict[int, int]
+        self._reached_count = {}  # type: Dict[int, int]
 
     def __copy__(self):
         result = JumpdestCountAnnotation()
-        result._jumpdest_count = copy(self._jumpdest_count)
+        result._reached_count = copy(self._reached_count)
         return result
 
 
@@ -31,11 +31,11 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
         """"""
 
         self.super_strategy = super_strategy
-        self.jumpdest_limit = args[0][0]
+        self.bound = args[0][0]
 
         log.info(
             "Loaded search strategy extension: Loop bounds (limit = {})".format(
-                self.jumpdest_limit
+                self.bound
             )
         )
 
@@ -44,17 +44,14 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
         )
 
     def get_strategic_global_state(self) -> GlobalState:
-        """
-        :return:
+        """ Returns the next state
+
+        :return: Global state
         """
 
         while True:
 
             state = self.super_strategy.get_strategic_global_state()
-            opcode = state.get_current_instruction()["opcode"]
-
-            if opcode != "JUMPI":
-                return state
 
             annotations = cast(
                 List[JumpdestCountAnnotation],
@@ -67,18 +64,15 @@ class BoundedLoopsStrategy(BasicSearchStrategy):
             else:
                 annotation = annotations[0]
 
-            try:
-                target = util.get_concrete_int(state.mstate.stack[-1])
-            except TypeError:
-                return state
+            address = state.get_current_instruction()["address"]
 
-            try:
-                annotation._jumpdest_count[target] += 1
-            except KeyError:
-                annotation._jumpdest_count[target] = 1
+            if address in annotation._reached_count:
+                annotation._reached_count[address] += 1
+            else:
+                annotation._reached_count[address] = 1
 
-            if annotation._jumpdest_count[target] > self.jumpdest_limit:
-                log.debug("JUMPDEST limit reached, skipping JUMPI")
+            if annotation._reached_count[address] > self.bound:
+                log.debug("Loop bound reached, skipping state")
                 continue
 
             return state

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_: "BitVec" = 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_: "BitVec" = 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_: "BitVec" = 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_: "BitVec" = None,
     ) -> BitVecFunc:
         """Creates a new bit vector function with a symbolic value."""
         raw = z3.BitVec(name, size)

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

@@ -79,7 +79,7 @@ class BitVecFunc(BitVec):
         self,
         raw: z3.BitVecRef,
         func_name: Optional[str],
-        input_: Union[int, "BitVec"] = None,
+        input_: "BitVec" = None,
         annotations: Optional[Annotations] = None,
     ):
         """
@@ -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,16 +80,26 @@ 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."""
-    union = []
+    union = []    # type: List
     args_list = [arg if isinstance(arg, Bool) else Bool(arg) for arg in args]
     for arg in args_list:
-        union.append(arg.annotations)
+        union += arg.annotations
     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.
 
@@ -98,7 +108,9 @@ def Or(*args: Union[Bool, bool]) -> Bool:
     :return:
     """
     args_list = [arg if isinstance(arg, Bool) else Bool(arg) for arg in args]
-    union = [arg.annotations for arg in args_list]
+    union = []  # type: List
+    for arg in args_list:
+        union += arg.annotations
     return Bool(z3.Or([a.raw for a in args_list]), annotations=union)
 
 

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)
 

mythril/mythril/mythril_analyzer.py

@@ -122,12 +122,10 @@ class MythrilAnalyzer:
     def fire_lasers(
         self,
         modules: Optional[List[str]] = None,
-        verbose_report: bool = False,
         transaction_count: Optional[int] = None,
     ) -> Report:
         """
         :param modules: The analysis modules which should be executed
-        :param verbose_report: Gives out the transaction sequence of the vulnerability
         :param transaction_count: The amount of transactions to be executed
         :return: The Report class which contains the all the issues/vulnerabilities
         """
@@ -177,7 +175,7 @@ class MythrilAnalyzer:
         source_data = Source()
         source_data.get_source_from_contracts_list(self.contracts)
         # Finally, output the results
-        report = Report(verbose_report, contracts=self.contracts, exceptions=exceptions)
+        report = Report(contracts=self.contracts, exceptions=exceptions)
         for issue in all_issues:
             report.append_issue(issue)
 

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,7 +1,10 @@
 import pytest
+from mythril.laser.smt import symbol_factory
 from mythril.laser.ethereum.state.account import Storage
 from mythril.laser.smt import Expression
 
+BVV = symbol_factory.BitVecVal
+
 storage_uninitialized_test_data = [({}, 1), ({1: 5}, 2), ({1: 5, 3: 10}, 2)]
 
 
@@ -9,10 +12,11 @@ storage_uninitialized_test_data = [({}, 1), ({1: 5}, 2), ({1: 5, 3: 10}, 2)]
 def test_concrete_storage_uninitialized_index(initial_storage, key):
     # Arrange
     storage = Storage(concrete=True)
-    storage._storage = initial_storage
+    for k, val in initial_storage.items():
+        storage[BVV(k, 256)] = BVV(val, 256)
 
     # Act
-    value = storage[key]
+    value = storage[BVV(key, 256)]
 
     # Assert
     assert value == 0
@@ -22,10 +26,11 @@ def test_concrete_storage_uninitialized_index(initial_storage, key):
 def test_symbolic_storage_uninitialized_index(initial_storage, key):
     # Arrange
     storage = Storage(concrete=False)
-    storage._storage = initial_storage
+    for k, val in initial_storage.items():
+        storage[BVV(k, 256)] = BVV(val, 256)
 
     # Act
-    value = storage[key]
+    value = storage[BVV(key, 256)]
 
     # Assert
     assert isinstance(value, Expression)
@@ -36,18 +41,18 @@ def test_storage_set_item():
     storage = Storage()
 
     # Act
-    storage[1] = 13
+    storage[BVV(1, 256)] = BVV(13, 256)
 
     # Assert
-    assert storage[1] == 13
+    assert storage[BVV(1, 256)] == BVV(13, 256)
 
 
 def test_storage_change_item():
     # Arrange
     storage = Storage()
-    storage._storage = {1: 12}
+    storage[BVV(1, 256)] = BVV(12, 256)
     # Act
-    storage[1] = 14
+    storage[BVV(1, 256)] = BVV(14, 256)
 
     # Assert
-    assert storage[1] == 14
+    assert storage[BVV(1, 256)] == BVV(14, 256)