diff --git a/mythril/laser/ethereum/state.py b/mythril/laser/ethereum/state.py index d1421cd8..20c17c62 100644 --- a/mythril/laser/ethereum/state.py +++ b/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)) ): diff --git a/mythril/laser/ethereum/transaction/symbolic.py b/mythril/laser/ethereum/transaction/symbolic.py index 563bf1b7..c4a04bc2 100644 --- a/mythril/laser/ethereum/transaction/symbolic.py +++ b/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) diff --git a/mythril/laser/ethereum/transaction/transaction_models.py b/mythril/laser/ethereum/transaction/transaction_models.py index eb85b295..4aee343f 100644 --- a/mythril/laser/ethereum/transaction/transaction_models.py +++ b/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 diff --git a/tests/laser/transaction/symbolic_test.py b/tests/laser/transaction/symbolic_test.py index 2ca12f63..5c18d190 100644 --- a/tests/laser/transaction/symbolic_test.py +++ b/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