bring transaction sequence generation to a working state

mythril/analysis/solver.py

@@ -1,4 +1,4 @@
-from z3 import Solver, simplify, sat, unknown, FuncInterp, Extract
+from z3 import Solver, simplify, sat, unknown, FuncInterp, Extract, UGE
 from mythril.exceptions import UnsatError
 from mythril.laser.ethereum.transaction.transaction_models import (
     ContractCreationTransaction,
@@ -58,14 +58,16 @@ def get_transaction_sequence(
     transaction_sequence = global_state.world_state.transaction_sequence
 
     # gaslimit & gasprice don't exist yet
-    tx_template = {"calldata": [], "call_value": None, "caller": caller}
+    tx_template = {"calldata": None, "call_value": None, "caller": caller}
 
     txs = {}
     creation_tx_ids = []
     tx_constraints = constraints.copy()
 
     for transaction in transaction_sequence:
+        tx_id = str(transaction.id)
         if not isinstance(transaction, ContractCreationTransaction):
+
             # Constrain caller
             tx_constraints.append(
                 (Extract(159, 0, transaction.caller) == int(caller[2:], 16))
@@ -75,16 +77,27 @@ def get_transaction_sequence(
             if max_callvalue != None:
                 tx_constraints.append(UGE(max_callvalue, transaction.call_value))
 
-            txs[str(transaction.id)] = tx_template
+            # Constrain callvalue
+            max_calldatasize = 5000
+            if max_calldatasize != None:
+                tx_constraints.append(UGE(max_calldatasize, transaction.call_data.calldatasize))
+
+            txs[tx_id] = tx_template.copy()
+
         else:
-            creation_tx_ids.append(str(transaction.id))
+            creation_tx_ids.append(tx_id)
 
     model = get_model(tx_constraints)
 
+    for transaction in transaction_sequence:
+        if not isinstance(transaction, ContractCreationTransaction):
+            tx_id = str(transaction.id)
+
+            txs[tx_id]["calldata"] = '0x'+''.join([hex(b)[2:] if len(hex(b)) % 2 == 0 else '0'+hex(b)[2:] for b in transaction.call_data.concretized(model)])
+
     for d in model.decls():
         name = d.name()
 
-        logging.debug(name)
         if "call_value" in name:
             tx_id = name.replace("call_value", "")
             if not tx_id in creation_tx_ids:
@@ -92,10 +105,4 @@ def get_transaction_sequence(
 
                 txs[tx_id]["call_value"] = call_value
 
-    # Copy calldata
-    for tx_id in txs:
-        txs[tx_id]["calldata"] = "0x" + "".join(
-            [str(x) for x in global_state.environment.calldata.concretized(model)]
-        )
-
     return txs