From 1cf4df9b596df2c3076d1636e00a88da8cd34960 Mon Sep 17 00:00:00 2001
From: Nikhil Parasaram <nikhilparasaram@gmail.com>
Date: Mon, 13 Apr 2020 12:58:54 +0100
Subject: [PATCH] Unconstrained storage (#1366)

* Add unconstrained storage flag

* Dont take from onchain
---
 mythril/interfaces/cli.py               | 7 +++++++
 mythril/laser/ethereum/state/account.py | 4 +++-
 mythril/mythril/mythril_analyzer.py     | 2 ++
 mythril/support/support_args.py         | 1 +
 4 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/mythril/interfaces/cli.py b/mythril/interfaces/cli.py
index aa4055cb..b46b00ff 100644
--- a/mythril/interfaces/cli.py
+++ b/mythril/interfaces/cli.py
@@ -455,6 +455,12 @@ def create_analyzer_parser(analyzer_parser: ArgumentParser):
         action="store_true",
         help="Checks for reachability after the end of tx. Recommended for short execution timeouts < 1 min",
     )
+    options.add_argument(
+        "--unconstrained-storage",
+        action="store_true",
+        help="Default storage value is symbolic, turns off the on-chain storage loading",
+    )
+
     options.add_argument(
         "--phrack", action="store_true", help="Phrack-style call graph"
     )
@@ -683,6 +689,7 @@ def execute_command(
             if args.custom_modules_directory
             else "",
             sparse_pruning=args.sparse_pruning,
+            unconstrained_storage=args.unconstrained_storage,
         )
 
         if not disassembler.contracts:
diff --git a/mythril/laser/ethereum/state/account.py b/mythril/laser/ethereum/state/account.py
index d8d877e9..cc92e285 100644
--- a/mythril/laser/ethereum/state/account.py
+++ b/mythril/laser/ethereum/state/account.py
@@ -10,6 +10,7 @@ from typing import Any, Dict, Union, Set
 from mythril.laser.smt import Array, K, BitVec, simplify, BaseArray
 from mythril.disassembler.disassembly import Disassembly
 from mythril.laser.smt import symbol_factory
+from mythril.support.support_args import args
 
 log = logging.getLogger(__name__)
 
@@ -22,7 +23,7 @@ class Storage:
 
         :param concrete: bool indicating whether to interpret uninitialized storage as concrete versus symbolic
         """
-        if concrete:
+        if concrete and args.unconstrained_storage is False:
             self._standard_storage = K(256, 256, 0)  # type: BaseArray
         else:
             self._standard_storage = Array("Storage", 256, 256)
@@ -41,6 +42,7 @@ class Storage:
             and item.symbolic is False
             and int(item.value) not in self.storage_keys_loaded
             and (self.dynld and self.dynld.active)
+            and args.unconstrained_storage is False
         ):
             try:
                 storage[item] = symbol_factory.BitVecVal(
diff --git a/mythril/mythril/mythril_analyzer.py b/mythril/mythril/mythril_analyzer.py
index 8b239c8d..ab383f1f 100644
--- a/mythril/mythril/mythril_analyzer.py
+++ b/mythril/mythril/mythril_analyzer.py
@@ -46,6 +46,7 @@ class MythrilAnalyzer:
         enable_coverage_strategy: bool = False,
         custom_modules_directory: str = "",
         sparse_pruning: bool = False,
+        unconstrained_storage: bool = False,
     ):
         """
 
@@ -69,6 +70,7 @@ class MythrilAnalyzer:
         self.custom_modules_directory = custom_modules_directory
         args.sparse_pruning = sparse_pruning
         args.solver_timeout = solver_timeout
+        args.unconstrained_storage = unconstrained_storage
 
     def dump_statespace(self, contract: EVMContract = None) -> str:
         """
diff --git a/mythril/support/support_args.py b/mythril/support/support_args.py
index b44691de..c5f30b87 100644
--- a/mythril/support/support_args.py
+++ b/mythril/support/support_args.py
@@ -7,6 +7,7 @@ class Args:
     def __init__(self):
         self.solver_timeout = 10000
         self.sparse_pruning = True
+        self.unconstrained_storage = False
 
 
 args = Args()