Merge pull request #620 from nbanmp/fix_calldata_indexing

Fix issue where the new calldata constraints are overwritten.

mythril/laser/ethereum/state.py

@@ -61,7 +61,6 @@ class Calldata:
     @property
     def constraints(self):
         constraints = []
-
         if self.concrete:
             for calldata_byte in self.starting_calldata:
                 if type(calldata_byte) == int:
@@ -74,11 +73,11 @@ class Calldata:
             constraints.append(
                 ForAll(x, Implies(self[x] != 0, UGT(self.calldatasize, x)))
             )
-
         return constraints
 
     def concretized(self, model):
         result = []
+
         for i in range(
             get_concrete_int(model.eval(self.calldatasize, model_completion=True))
         ):

mythril/laser/ethereum/transaction/symbolic.py

@@ -89,7 +89,7 @@ def _setup_global_state_for_execution(laser_evm, transaction):
             )
         )
 
-        global_state.mstate.constraints = transaction.world_state.node.constraints
+        global_state.mstate.constraints += transaction.world_state.node.constraints
         new_node.constraints = global_state.mstate.constraints
 
     global_state.world_state.transaction_sequence.append(transaction)

mythril/laser/ethereum/transaction/transaction_models.py

@@ -173,6 +173,9 @@ class ContractCreationTransaction:
 
         global_state = GlobalState(self.world_state, environment, None)
         global_state.environment.active_function_name = "constructor"
+        global_state.mstate.constraints.extend(
+            global_state.environment.calldata.constraints
+        )
 
         return global_state
 

tests/laser/transaction/symbolic_test.py

@@ -10,6 +10,9 @@ from mythril.laser.ethereum.svm import LaserEVM
 from mythril.laser.ethereum.state import WorldState, Account
 import unittest.mock as mock
 from unittest.mock import MagicMock
+from mythril.laser.ethereum.transaction.symbolic import (
+    _setup_global_state_for_execution,
+)
 
 
 def _is_message_call(_, transaction):
@@ -67,3 +70,25 @@ def test_execute_contract_creation(mocked_setup: MagicMock):
     # laser_evm.exec.assert_called_once()
     assert laser_evm.exec.call_count == 1
     assert len(laser_evm.open_states) == 0
+
+
+def test_calldata_constraints_in_transaction():
+    # Arrange
+    laser_evm = LaserEVM({})
+    world_state = WorldState()
+
+    correct_constraints = [MagicMock(), MagicMock(), MagicMock()]
+
+    transaction = MessageCallTransaction(
+        world_state, Account("ca11ee"), Account("ca114")
+    )
+    transaction.call_data = MagicMock()
+    transaction.call_data.constraints = correct_constraints
+
+    # Act
+    _setup_global_state_for_execution(laser_evm, transaction)
+
+    # Assert
+    state = laser_evm.work_list[0]
+    for constraint in correct_constraints:
+        assert constraint in state.environment.calldata.constraints