Use combined storage

mythril/analysis/modules/exceptions.py

@@ -43,6 +43,7 @@ class ReachableExceptionsModule(DetectionModule):
         :param state:
         :return:
         """
+        print("SHIT ASSERT")
         log.debug("ASSERT_FAIL in function " + state.environment.active_function_name)
 
         try:
@@ -76,6 +77,7 @@ class ReachableExceptionsModule(DetectionModule):
             return [issue]
 
         except UnsatError:
+            print("SHIT NO Model", state.mstate.constraints)
             log.debug("no model found")
 
         return []

mythril/laser/ethereum/instructions.py

@@ -1370,8 +1370,7 @@ class Instruction:
         index = state.stack.pop()
 
         state.stack.append(global_state.environment.active_account.storage[index])
-        if global_state.get_current_instruction()["address"] == 418:
-            print(state.stack[-1])
+
         return [global_state]
 
     @StateTransition()
@@ -1439,6 +1438,7 @@ class Instruction:
         states = []
 
         op0, condition = state.stack.pop(), state.stack.pop()
+
         try:
             jump_addr = util.get_concrete_int(op0)
         except TypeError:
@@ -1503,6 +1503,7 @@ class Instruction:
                 states.append(new_state)
             else:
                 log.debug("Pruned unreachable states.")
+
         return states
 
     @StateTransition()

mythril/laser/ethereum/state/account.py

@@ -190,10 +190,9 @@ class Storage:
         )
 
     def __getitem__(self, key: BitVec) -> BitVec:
-        if self._array_condition(key):
-            return self._array_region[key]
-
-        return self._ite_region[cast(BitVecFunc, key)]
+        ite_get = self._ite_region[cast(BitVecFunc, key)]
+        array_get = self._array_region[key]
+        return If(ite_get, ite_get, array_get)
 
     def __setitem__(self, key: BitVec, value: Any) -> None:
         self._printable_storage[key] = value
@@ -214,20 +213,14 @@ class Storage:
         # TODO: Do something better here
         return str(self._printable_storage)
 
-    def concretize(self, model):
-        constraints = []
+    def concretize(self, models):
         for key, value in self._ite_region.itelist:
             if simplify(Extract(255, 0, key.input_)).symbolic or not isinstance(
                 key.input_, BitVecFunc
             ):
                 continue
-            new_constraints, key_concrete = self._traverse_concretise(key, model)
+            key_concrete = self._traverse_concretise(key, models)
             key.potential_value = key_concrete
-            constraints += new_constraints
-            self._array_region[key] = value
-        self._ite_region.itelist = []
-
-        return constraints
 
     def calc_sha3(self, val, size):
         try:
@@ -239,6 +232,8 @@ class Storage:
         return symbol_factory.BitVecVal(val, 256)
 
     def _find_value(self, symbol, model):
+        if model is None:
+            return
         modify = symbol
         size = min(symbol.size(), 256)
         if symbol.size() > 256:
@@ -258,47 +253,57 @@ class Storage:
         assert modify.size() == symbol.size()
         return modify
 
-    def _traverse_concretise(self, key, model):
+    def _traverse_concretise(self, key, models):
         """
         Breadth first Search
         :param key:
         :param model:
         :return:
         """
-        constraints = []
         if not isinstance(key, BitVecFunc):
-            concrete_value = self._find_value(key, model)
-            key.potential_value = concrete_value
-            return constraints, concrete_value
+            concrete_values = [self._find_value(key, model) for model in models]
+            key.potential_values = concrete_values
+            return concrete_values
         if key.size() == 512:
             val = simplify(Extract(511, 256, key))
-            new_const, concrete_val = self._traverse_concretise(val, model)
-            constraints += new_const
-            new_const, val2 = self._traverse_concretise(Extract(255, 0, key), model)
-            key.potential_value = Concat(concrete_val, val2)
-            constraints += new_const
+            concrete_vals = self._traverse_concretise(val, models)
+            vals2 = self._traverse_concretise(Extract(255, 0, key), models)
+            key.potential_value = []
+            for val1, val2 in zip(concrete_vals, vals2):
+                if val2 and val1:
+                    key.potential_value.append(Concat(val1, val2))
+                else:
+                    key.potential_value.append(None)
 
         if isinstance(key.input_, BitVec) or (
             isinstance(key.input_, BitVecFunc) and key.input_.func_name == "sha3"
         ):
-            new_const, _ = self._traverse_concretise(key.input_, model)
-            constraints += new_const
+            value = self._traverse_concretise(key.input_, models)
+            key.input_.potential_value = value
 
         if isinstance(key, BitVecFunc):
             if key.size() == 512:
                 p1 = Extract(511, 256, key)
-                p1 = self.calc_sha3(p1.input_.potential_value, p1.input_.size())
-                key.potential_value = Concat(p1, Extract(255, 0, key))
-                if str(key.raw) != "":
-                    constraints += [key.raw == key.potential_value.value]
+                p1 = [self.calc_sha3(val, p1.input_.size()) for val in p1.input_.potential_value]
+                key.potential_value = [Concat(p, Extract(255, 0, key)) for p in p1]
+                key.potential_value = []
+                for val in p1:
+                    if val:
+                        key.potential_value.append(Concat(val, Extract(255, 0, key)))
+                    else:
+                        key.potential_value.append(None)
             else:
-                key.potential_value = self.calc_sha3(
-                    key.input_.potential_value, key.input_.size()
-                )
-                if str(key.raw) != "":
-                    constraints += [key.raw == key.potential_value.value]
-        assert key.size() == key.potential_value.size()
-        return constraints, key.potential_value
+                key.potential_value = []
+                for val in key.input_.potential_value:
+                    if val:
+                        key.potential_value.append(self.calc_sha3(
+                            val, key.input_.size()
+                        ))
+                    else:
+                        key.potential_value.append(None)
+        if key.potential_value[0] is not None:
+            assert key.size() == key.potential_value[0].size()
+        return key.potential_value
 
 
 class Account:

mythril/laser/ethereum/state/constraints.py

@@ -35,6 +35,7 @@ class Constraints(list):
         """
         :return: True/False based on the existence of solution of constraints
         """
+        return True
         if self._is_possible is not None:
             return self._is_possible
         solver = Solver()

mythril/laser/ethereum/svm.py

@@ -16,8 +16,8 @@ from mythril.laser.ethereum.state.world_state import WorldState
 from mythril.laser.ethereum.strategy.basic import DepthFirstSearchStrategy
 from abc import ABCMeta
 from mythril.laser.ethereum.time_handler import time_handler
-from mythril.laser.smt import Solver
-from z3 import unsat
+from mythril.analysis.solver import get_model, UnsatError
+
 from mythril.laser.ethereum.transaction import (
     ContractCreationTransaction,
     TransactionEndSignal,
@@ -27,6 +27,12 @@ from mythril.laser.ethereum.transaction import (
 )
 from mythril.laser.smt import symbol_factory
 
+ACTOR_ADDRESSES = [
+    symbol_factory.BitVecVal(0xAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFEAFFE, 256),
+    symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEF, 256),
+    symbol_factory.BitVecVal(0xDEADBEEFDEADBEEFDEADBEEFDEADBEEFDEADBEEE, 256),
+]
+
 log = logging.getLogger(__name__)
 
 
@@ -347,15 +353,17 @@ class LaserEVM:
         return new_global_states, op_code
 
     def concretize_ite_storage(self, global_state):
-        solver = Solver()
-        for constraint in global_state.mstate.constraints:
-            solver.add(constraint)
+        sender = global_state.environment.sender
+        models = []
+
+        for actor in ACTOR_ADDRESSES:
+            try:
+                models.append(get_model(constraints=global_state.mstate.constraints + [sender == actor]))
+            except UnsatError:
+                models.append(None)
 
-        if solver.check() == unsat:
-            return []
-        model = solver.model()
         for account in global_state.world_state.accounts.values():
-            global_state.mstate.constraints += account.storage.concretize(model)
+            account.storage.concretize(models)
 
     def _end_message_call(
         self,

mythril/laser/smt/bitvecfunc.py

@@ -113,6 +113,10 @@ def _comparison_helper(
         Bool(condition) if b.nested_functions else Bool(True),
         a.input_ == b.input_ if inputs_equal else a.input_ != b.input_,
     )
+    if a.potential_value:
+        for i, val in enumerate(a.potential_value):
+            comparision = Or(comparision, val == b)
+
     return comparision