Adding first working transacation application purely working on the stack and not considering the combination of constraints

mythril/analysis/modules/build_traces.py

@@ -1,4 +1,6 @@
 from mythril.analysis.report import Issue
+from mythril.solidnotary.transactiontrace import TransactionTrace
+from mythril.solidnotary.solidnotary import SolidNotary
 import logging
 
 
@@ -19,4 +21,10 @@ def execute(statespace):
 
     traces = []
 
+    traces = SolidNotary().get_transaction_traces(statespace)
+
+    print("==== Second level traces ====")
+    for trace in traces:
+        print(trace.apply_traces_parallel(traces))
+
     return []

mythril/analysis/modules/dummy.py

@@ -9,7 +9,8 @@ import logging
 def print_obj(obj):
     print()
     print(obj)
-    # print(dir(obj))
+    print(type(obj))
+    print(dir(obj))
     print()
 
 
@@ -27,7 +28,8 @@ def execute(statespace):
             instruction = state.get_current_instruction()
 
             if(instruction['opcode'] == "STOP"):
-                print_obj(state.environment.active_account.storage)
+                for k,v in state.environment.active_account.storage.items():
+                    print_obj(v)
                 # print("opc: {}, add: {} {}".format(instruction['opcode'], instruction['address'], instruction['argument'] if 'argument' in instruction else ""))
 
     return issues

mythril/solidnotary/solidnotary.py

@@ -13,7 +13,7 @@ class SolidNotary:
         # Todo Find how they are storing results
         pass
 
-    def get_transaction_traces(statespace):
+    def get_transaction_traces(self, statespace):
         logging.debug("Executing module: Transaction End")
 
         traces = []
@@ -24,4 +24,4 @@ class SolidNotary:
                 instruction = state.get_current_instruction()
                 if instruction['opcode'] == "STOP":
                     traces.append(TransactionTrace(state.environment.active_account.storage))
-            return traces
+        return traces

mythril/solidnotary/transactiontrace.py

@@ -1,16 +1,45 @@
+from z3 import *
+
 class TransactionTrace:
 
     def __init__(self, storage):
         self.storage = storage
+        # Todo the constraints of a trace are probably also important here and have to be somehow aggregated
         # Todo Identifiy addional trace information such as blocknumber and more
 
+    """
+          Either do only deep checing here and use the proper trace or storage_slot reduction in the apply function. Or do
+          both here.
+      """
+
+    def deep_equals(trace_lvl1, trace_lvl2):
+        return set(trace_lvl1) == set(trace_lvl2) # Todo Impelement an ACTUAL deep comparison
+
+    def simplify_storage(self):
+        for k,v in self.storage.items():
+            # Todo explore the arguments of this storage simplification in z3 to find ways to further simplify and to
+            # sort this expressions for equality comparison
+            self.storage[k] = simplify(v)
+
     """
         Applies the new trace tt on a possibly even changed trace self.
     """
     def apply_trace(self, tt):
         if tt is None:
             return self
-        # Todo implement application of a trace on a existing trace.
+        subs_map = list(map(lambda x: (BitVec("storage_" + str(x[0]), 256), x[1]), tt.storage.items()))
+        print("_________")
+        print(subs_map)
+        print(self.storage)
+        print("+++++++++")
+        for k,v in self.storage.items():
+            self.storage[k] = substitute(v, subs_map)
+        # Todo Add combination of constraints, this might by tricky if we cannot identify which entrancy constraints of
+        # self can be omitted (e.g. when related storage locations were overwritten)
+        print(self.storage)
+        print("=========")
+        self.simplify_storage()
+        print(self.storage)
         return None
 
     def apply_traces_parallel(self, traces):
@@ -27,7 +56,7 @@ class TransactionTrace:
             trace_lvl_np1 = []
             for trace in trace_lvl_n:
                 trace_lvl_np1.append(trace.apply_traces_parallel(traces))
-            if deep_equals(trace_lvl_np1, trace_lvl_n): # Fixpoint detected, function needs to ignore lists, dicts and objects.
+            if TransactionTrace.deep_equals(trace_lvl_np1, trace_lvl_n): # Fixpoint detected, function needs to ignore lists, dicts and objects.
                 return trace_lvl_n
             trace_lvl_n = trace_lvl_np1
         return trace_lvl_n
@@ -40,15 +69,10 @@ class TransactionTrace:
                 trace_lvl_np1.append(trace.apply_traces_parallel(traces))
             for trace_lvl_i in traces_up_to:
                 # the following might be faster to check when using a content representing hash
-                if deep_equals(trace_lvl_np1, trace_lvl_i): # cycle in the traces of trace chains detected: levels
+                if TransactionTrace.deep_equals(trace_lvl_np1, trace_lvl_i): # cycle in the traces of trace chains detected: levels
                     # while repeat themselves, function needs to ignore lists, dicts and objects.
                     return traces_up_to
             traces_up_to.append(trace_lvl_np1)
         return traces_up_to
 
-    """
+
-        Either do only deep checing here and use the proper trace or storage_slot reduction in the apply function. Or do
-        both here.
-    """
-    def deep_equals(trace_lvl1, trace_lvl2):
-        pass