From 37ad9e7acdc04faa3fef5d1509752dd26fbfbf2a Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 7 May 2020 12:54:07 +0000 Subject: [PATCH 1/6] Initial commit of dev-detect-transaction-reordering. --- manticore/ethereum/__init__.py | 1 + manticore/ethereum/cli.py | 2 + manticore/ethereum/detectors.py | 206 ++++++++++++++++++++++- tests/ethereum/contracts/sqrt.sol | 16 ++ tests/ethereum/contracts/sqrt_better.sol | 22 +++ tests/ethereum/test_general.py | 28 +++ 6 files changed, 274 insertions(+), 1 deletion(-) create mode 100644 tests/ethereum/contracts/sqrt.sol create mode 100644 tests/ethereum/contracts/sqrt_better.sol diff --git a/manticore/ethereum/__init__.py b/manticore/ethereum/__init__.py index 068a7c8be..250dc8b8d 100644 --- a/manticore/ethereum/__init__.py +++ b/manticore/ethereum/__init__.py @@ -17,6 +17,7 @@ DetectUninitializedStorage, DetectRaceCondition, DetectManipulableBalance, + DetectTransactionReordering, ) from .account import EVMAccount, EVMContract from .solidity import SolidityMetadata diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index 388fe7b30..e4257c265 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -13,6 +13,7 @@ DetectRaceCondition, DetectorClassification, DetectManipulableBalance, + DetectTransactionReordering, ) from ..core.plugin import Profiler from .manticore import ManticoreEVM @@ -55,6 +56,7 @@ def get_detectors_classes(): DetectExternalCallAndLeak, DetectEnvInstruction, DetectManipulableBalance, + DetectTransactionReordering, # The RaceCondition detector has been disabled for now as it seems to collide with IntegerOverflow detector # DetectRaceCondition ] diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py index 521525e28..dbecfb5eb 100644 --- a/manticore/ethereum/detectors.py +++ b/manticore/ethereum/detectors.py @@ -1,7 +1,7 @@ from manticore.core.smtlib.visitors import simplify import hashlib from enum import Enum -from typing import Optional +from typing import Optional, Iterable import logging from contextlib import contextmanager @@ -15,6 +15,9 @@ taint_with, ) from ..core.plugin import Plugin +from ..platforms.evm import Transaction +from ..utils import config +from .state import State logger = logging.getLogger(__name__) @@ -871,3 +874,204 @@ def did_evm_execute_instruction_callback(self, state, instruction, arguments, re for op in arguments: if istainted(op, "BALANCE"): self.add_finding_here(state, "Manipulable balance used in a strict comparison") + + +DEBUG_REPLAY = False + +WARNED = "warned" +TROUBLEMAKER = "troublemaker" +IN_DID_RUN_CALLBACK = "in_did_run_callback" +REPLAYING = "replaying" + + +class DetectTransactionReordering(Detector): + """ + Detects cases where: + * transaction Y returns successfully + * there exists a transaction X from a distinct account such that when X precedes Y, Y reverts + """ + + ARGUMENT = "transaction-reordering" + HELP = "Susceptible to transaction reordering attacks" + IMPACT = DetectorClassification.MEDIUM + CONFIDENCE = DetectorClassification.HIGH + + def __init__(self, *args, **kwargs): + super().__init__(*args, **kwargs) + + @classmethod + def state_context_name(cls, name: str): + return cls.__name__ + "." + name + + @classmethod + def debug(cls, msg: str, *args): + logger.debug(cls.__name__ + ": " + msg, *args) + + @classmethod + def info(cls, msg: str, *args): + logger.info(cls.__name__ + ": " + msg, *args) + + def will_run_callback(self, states: Iterable[State]): + with self.locked_context(value_type=dict) as context: + if context.get(IN_DID_RUN_CALLBACK): + return + + if not context.get(WARNED): + consts = config.get_group("evm") + if consts.sha3 is consts.sha3.symbolicate: + logger.warn( + "Unsound symbolication can cause the transaction reordering attack" + + " detector to produce false positives" + ) + context[WARNED] = True + + if not context.get(TROUBLEMAKER): + # sam.moelius: Use same initial balance as in ManticoreEVM.multi_tx_analysis. + troublemaker = self.manticore.create_account( + balance=10000000000000000000, + name="troublemaker", + ) + context[TROUBLEMAKER] = troublemaker.address + self.debug("troublemaker = %s", hex(troublemaker.address)) + + for state in states: + if state.platform._pending_transaction.type != "CALL": + continue + + with state as new_state: + # sam.moelius: The state returned by StateBase.__enter__ references the original + # platform, but we want an actual copy so that we can clear its + # _pending_transaction field. As convoluted as this may seem, the easiest way + # to completely copy a state appears to be to _save and re_load it. + state_id = self.manticore._save(new_state) + new_state = self.manticore._load(state_id) + new_state.platform._pending_transaction = None + assert self.manticore._save(new_state, state_id) == state_id + + assert self.state_context_name("state_id") not in state.context + state.context[self.state_context_name("state_id")] = state_id + + self.debug("saved state %r as state %r", state.id, state_id) + + def did_close_transaction_callback(self, state: State, tx: Transaction): + if not tx.is_human: + return + + if tx.sort != "CALL": + return + + with self.locked_context(value_type=dict) as context: + + if not context.get(IN_DID_RUN_CALLBACK): + + state_id = state.context[self.state_context_name("state_id")] + del state.context[self.state_context_name("state_id")] + + if tx.return_value != 0: + tx = tx.concretize(state, constrain=True) + with self.locked_context("queue", list) as context_queue: + context_queue.append((state_id, tx)) + self.debug("queued (%s, %s)", state_id, tx) + else: + # sam.moelius: Do not remove state_id. There could be multiple states whose + # self.state_context_name("state_id") field is state_id. + # self.manticore._remove(state_id) + pass + + else: + + if context.get(REPLAYING): + if tx.return_value == 0: + assert not DEBUG_REPLAY, str(state.platform) + self.add_finding( + state, + tx.address, + 0, + f"{tx.result} following transaction reordering", + False, + ) + + def did_run_callback(self): + with self.locked_context(value_type=dict) as context: + if context.get(IN_DID_RUN_CALLBACK): + return + + # sam.moelius: Exiting early avoids unnecessary log messages. + with self.locked_context("queue", list) as context_queue: + if not context_queue: + return + + context[IN_DID_RUN_CALLBACK] = True + + # sam.moelius: Leaving the "with" block saves the context. + + saved_states = [] + with self.manticore.locked_context("ethereum.saved_states", list) as context_saved_states: + while context_saved_states: + saved_states.append(context_saved_states.pop()) + + queue = [] + with self.locked_context("queue", list) as context_queue: + while context_queue: + queue.append(context_queue.pop()) + + self.info("injecting symbolic transaction (%d queued states)", len(queue)) + + for state_id, tx in queue: + # sam.moelius: Manticore deletes states in the ready queue. But this state_id may have + # been queued with multiple txs. So make a copy of this state. + state = self.manticore._load(state_id) + with state as new_state: + state_id = self.manticore._save(new_state) + self.debug("copied state %r to state %r", state.id, state_id) + + assert not self.manticore._ready_states + self.manticore._ready_states.append(state_id) + + if not DEBUG_REPLAY: + troublemaker = None + with self.locked_context(value_type=dict) as context: + troublemaker = context[TROUBLEMAKER] + context[REPLAYING] = False + + symbolic_address = self.manticore.make_symbolic_value() + symbolic_data = self.manticore.make_symbolic_buffer(320) + symbolic_value = self.manticore.make_symbolic_value() + + self.manticore.transaction( + caller=troublemaker, + address=symbolic_address, + data=symbolic_data, + value=symbolic_value, + ) + + self.info( + "replaying original transaction (%d alive states)", + self.manticore.count_ready_states(), + ) + + with self.locked_context(value_type=dict) as context: + context[REPLAYING] = True + + self.manticore.transaction( + caller=tx.caller, + data=tx.data, + address=tx.address, + value=tx.value, + gas=tx.gas, + price=tx.price, + ) + + # sam.moelius: Move ready states to the terminated list so that test cases are generated + # for them. + while self.manticore._ready_states: + state_id = self.manticore._ready_states.pop() + self.manticore._terminated_states.append(state_id) + + with self.manticore.locked_context("ethereum.saved_states", list) as context_saved_states: + assert not context_saved_states + while saved_states: + context_saved_states.append(saved_states.pop()) + + with self.locked_context(value_type=dict) as context: + context[IN_DID_RUN_CALLBACK] = False diff --git a/tests/ethereum/contracts/sqrt.sol b/tests/ethereum/contracts/sqrt.sol new file mode 100644 index 000000000..c63ee9589 --- /dev/null +++ b/tests/ethereum/contracts/sqrt.sol @@ -0,0 +1,16 @@ +contract Sqrt { + uint256 n; + + constructor(uint256 _n) public payable { + require(0 < _n, "not positive"); + n = _n; + } + + function submit(uint256 _x) external { + require(0 < _x, "not positive"); + require(_x * _x <= n, "too big"); + require(n < (_x + 1) * (_x + 1), "too small"); + n = 0; + msg.sender.transfer(address(this).balance); + } +} diff --git a/tests/ethereum/contracts/sqrt_better.sol b/tests/ethereum/contracts/sqrt_better.sol new file mode 100644 index 000000000..4f91c4306 --- /dev/null +++ b/tests/ethereum/contracts/sqrt_better.sol @@ -0,0 +1,22 @@ +contract Sqrt { + uint256 n; + mapping(address => bytes32) commits; + + constructor(uint256 _n) public payable { + require(0 < _n, "not positive"); + n = _n; + } + + function commit(bytes32 _value) external { + commits[msg.sender] = _value; + } + + function reveal(uint256 _x, uint256 _salt) external { + require(keccak256(abi.encode(_x, _salt)) == commits[msg.sender], "not committed to"); + require(0 < _x, "not positive"); + require(_x * _x <= n, "too big"); + require(n < (_x + 1) * (_x + 1), "too small"); + n = 0; + msg.sender.transfer(address(this).balance); + } +} diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index f77c5a58a..3d670bc90 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -21,6 +21,7 @@ State, DetectExternalCallAndLeak, DetectIntegerOverflow, + DetectTransactionReordering, Detector, NoAliveStates, ABI, @@ -31,6 +32,7 @@ from manticore.ethereum.solidity import SolidityMetadata from manticore.platforms import evm from manticore.platforms.evm import EVMWorld, ConcretizeArgument, concretized_args, Return, Stop +from manticore.utils import config, log from manticore.utils.deprecated import ManticoreDeprecationWarning solver = Z3Solver.instance() @@ -61,6 +63,32 @@ def test_int_ovf(self): self.assertIn("Unsigned integer overflow at MUL instruction", all_findings) +class EthDetectorsTransactionReordering(unittest.TestCase): + def test_transaction_reordering(self): + # log.set_verbosity(5) + consts = config.get_group("evm") + consts.sha3 = consts.sha3.concretize + mevm = ManticoreEVM() + mevm.register_detector(DetectTransactionReordering()) + filename = os.path.join(THIS_DIR, "contracts/sqrt.sol") + mevm.multi_tx_analysis(filename, tx_limit=1) + mevm.finalize() + self.assertEqual(len(mevm.global_findings), 1) + all_findings = "".join([x[2] for x in mevm.global_findings]) + self.assertIn("REVERT following transaction reordering", all_findings) + + def test_transaction_reordering_better(self): + # log.set_verbosity(5) + consts = config.get_group("evm") + consts.sha3 = consts.sha3.concretize + mevm = ManticoreEVM() + mevm.register_detector(DetectTransactionReordering()) + filename = os.path.join(THIS_DIR, "contracts/sqrt_better.sol") + mevm.multi_tx_analysis(filename, tx_limit=2) + mevm.finalize() + self.assertEqual(len(mevm.global_findings), 0) + + class EthAbiTests(unittest.TestCase): _multiprocess_can_split = True From 1d09a8d1c2f8c08ec6b01edd7db4adbacd79ab25 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 7 May 2020 16:01:43 +0000 Subject: [PATCH 2/6] Try to get matcoin tests to pass. --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5720c1a81..6b54bf6e9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -157,7 +157,7 @@ jobs: mkdir truffle_tests cd truffle_tests truffle unbox metacoin - manticore . --contract MetaCoin --workspace output + manticore . --exclude-all --contract MetaCoin --workspace output ### The original comment says we should get 41 states, but after implementing the shift ### insructions, we get 31. Was the original comment a typo? From d29c711d5ae0e46180abc1651d45cd684a4caada Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 7 May 2020 16:03:06 +0000 Subject: [PATCH 3/6] Minor rewording. --- manticore/ethereum/detectors.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py index dbecfb5eb..39b560071 100644 --- a/manticore/ethereum/detectors.py +++ b/manticore/ethereum/detectors.py @@ -888,7 +888,7 @@ class DetectTransactionReordering(Detector): """ Detects cases where: * transaction Y returns successfully - * there exists a transaction X from a distinct account such that when X precedes Y, Y reverts + * for some transaction X from a different account, when X precedes Y, Y reverts """ ARGUMENT = "transaction-reordering" From f48617da3ee2cb362673668580ed1d433d072c9d Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Thu, 7 May 2020 16:03:50 +0000 Subject: [PATCH 4/6] Add test. --- tests/ethereum/contracts/basic.sol | 12 ++++++++++++ tests/ethereum/test_general.py | 17 +++++++++++++++-- 2 files changed, 27 insertions(+), 2 deletions(-) create mode 100644 tests/ethereum/contracts/basic.sol diff --git a/tests/ethereum/contracts/basic.sol b/tests/ethereum/contracts/basic.sol new file mode 100644 index 000000000..597e96e18 --- /dev/null +++ b/tests/ethereum/contracts/basic.sol @@ -0,0 +1,12 @@ +contract Basic { + uint256 n; + + constructor(uint256 _n) public { + n = _n; + } + + function submit(uint256 _x) external { + require(_x == n, "wrong value"); + n++; + } +} diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index 3d670bc90..ee2e01ce7 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -64,7 +64,20 @@ def test_int_ovf(self): class EthDetectorsTransactionReordering(unittest.TestCase): - def test_transaction_reordering(self): + def test_transaction_reordering_basic(self): + # log.set_verbosity(5) + consts = config.get_group("evm") + consts.sha3 = consts.sha3.concretize + mevm = ManticoreEVM() + mevm.register_detector(DetectTransactionReordering()) + filename = os.path.join(THIS_DIR, "contracts/basic.sol") + mevm.multi_tx_analysis(filename, tx_limit=1) + mevm.finalize() + self.assertEqual(len(mevm.global_findings), 1) + all_findings = "".join([x[2] for x in mevm.global_findings]) + self.assertIn("REVERT following transaction reordering", all_findings) + + def test_transaction_reordering_sqrt(self): # log.set_verbosity(5) consts = config.get_group("evm") consts.sha3 = consts.sha3.concretize @@ -77,7 +90,7 @@ def test_transaction_reordering(self): all_findings = "".join([x[2] for x in mevm.global_findings]) self.assertIn("REVERT following transaction reordering", all_findings) - def test_transaction_reordering_better(self): + def test_transaction_reordering_sqrt_better(self): # log.set_verbosity(5) consts = config.get_group("evm") consts.sha3 = consts.sha3.concretize From 5fe64f4cedf06de29ad51431ed54a1d82d0d9810 Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Wed, 3 Jun 2020 13:22:26 +0000 Subject: [PATCH 5/6] Renaming: "transaction reordering" -> "transaction displacement" --- manticore/ethereum/__init__.py | 2 +- manticore/ethereum/cli.py | 4 ++-- manticore/ethereum/detectors.py | 13 ++++++------- tests/ethereum/test_general.py | 20 ++++++++++---------- 4 files changed, 19 insertions(+), 20 deletions(-) diff --git a/manticore/ethereum/__init__.py b/manticore/ethereum/__init__.py index 250dc8b8d..25a059846 100644 --- a/manticore/ethereum/__init__.py +++ b/manticore/ethereum/__init__.py @@ -17,7 +17,7 @@ DetectUninitializedStorage, DetectRaceCondition, DetectManipulableBalance, - DetectTransactionReordering, + DetectTransactionDisplacement, ) from .account import EVMAccount, EVMContract from .solidity import SolidityMetadata diff --git a/manticore/ethereum/cli.py b/manticore/ethereum/cli.py index e4257c265..7d4b0b80a 100644 --- a/manticore/ethereum/cli.py +++ b/manticore/ethereum/cli.py @@ -13,7 +13,7 @@ DetectRaceCondition, DetectorClassification, DetectManipulableBalance, - DetectTransactionReordering, + DetectTransactionDisplacement, ) from ..core.plugin import Profiler from .manticore import ManticoreEVM @@ -56,7 +56,7 @@ def get_detectors_classes(): DetectExternalCallAndLeak, DetectEnvInstruction, DetectManipulableBalance, - DetectTransactionReordering, + DetectTransactionDisplacement, # The RaceCondition detector has been disabled for now as it seems to collide with IntegerOverflow detector # DetectRaceCondition ] diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py index 39b560071..1656c1433 100644 --- a/manticore/ethereum/detectors.py +++ b/manticore/ethereum/detectors.py @@ -884,15 +884,15 @@ def did_evm_execute_instruction_callback(self, state, instruction, arguments, re REPLAYING = "replaying" -class DetectTransactionReordering(Detector): +class DetectTransactionDisplacement(Detector): """ Detects cases where: * transaction Y returns successfully * for some transaction X from a different account, when X precedes Y, Y reverts """ - ARGUMENT = "transaction-reordering" - HELP = "Susceptible to transaction reordering attacks" + ARGUMENT = "transaction-displacement" + HELP = "Susceptible to transaction displacement attacks" IMPACT = DetectorClassification.MEDIUM CONFIDENCE = DetectorClassification.HIGH @@ -920,7 +920,7 @@ def will_run_callback(self, states: Iterable[State]): consts = config.get_group("evm") if consts.sha3 is consts.sha3.symbolicate: logger.warn( - "Unsound symbolication can cause the transaction reordering attack" + "Unsound symbolication can cause the transaction displacement attack" + " detector to produce false positives" ) context[WARNED] = True @@ -928,8 +928,7 @@ def will_run_callback(self, states: Iterable[State]): if not context.get(TROUBLEMAKER): # sam.moelius: Use same initial balance as in ManticoreEVM.multi_tx_analysis. troublemaker = self.manticore.create_account( - balance=10000000000000000000, - name="troublemaker", + balance=10000000000000000000, name="troublemaker", ) context[TROUBLEMAKER] = troublemaker.address self.debug("troublemaker = %s", hex(troublemaker.address)) @@ -987,7 +986,7 @@ def did_close_transaction_callback(self, state: State, tx: Transaction): state, tx.address, 0, - f"{tx.result} following transaction reordering", + f"{tx.result} caused by transaction displacement", False, ) diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index ee2e01ce7..255c99490 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -21,7 +21,7 @@ State, DetectExternalCallAndLeak, DetectIntegerOverflow, - DetectTransactionReordering, + DetectTransactionDisplacement, Detector, NoAliveStates, ABI, @@ -63,39 +63,39 @@ def test_int_ovf(self): self.assertIn("Unsigned integer overflow at MUL instruction", all_findings) -class EthDetectorsTransactionReordering(unittest.TestCase): - def test_transaction_reordering_basic(self): +class EthDetectorsTransactionDisplacement(unittest.TestCase): + def test_transaction_displacement_basic(self): # log.set_verbosity(5) consts = config.get_group("evm") consts.sha3 = consts.sha3.concretize mevm = ManticoreEVM() - mevm.register_detector(DetectTransactionReordering()) + mevm.register_detector(DetectTransactionDisplacement()) filename = os.path.join(THIS_DIR, "contracts/basic.sol") mevm.multi_tx_analysis(filename, tx_limit=1) mevm.finalize() self.assertEqual(len(mevm.global_findings), 1) all_findings = "".join([x[2] for x in mevm.global_findings]) - self.assertIn("REVERT following transaction reordering", all_findings) + self.assertIn("REVERT caused by transaction displacement", all_findings) - def test_transaction_reordering_sqrt(self): + def test_transaction_displacement_sqrt(self): # log.set_verbosity(5) consts = config.get_group("evm") consts.sha3 = consts.sha3.concretize mevm = ManticoreEVM() - mevm.register_detector(DetectTransactionReordering()) + mevm.register_detector(DetectTransactionDisplacement()) filename = os.path.join(THIS_DIR, "contracts/sqrt.sol") mevm.multi_tx_analysis(filename, tx_limit=1) mevm.finalize() self.assertEqual(len(mevm.global_findings), 1) all_findings = "".join([x[2] for x in mevm.global_findings]) - self.assertIn("REVERT following transaction reordering", all_findings) + self.assertIn("REVERT caused by transaction displacement", all_findings) - def test_transaction_reordering_sqrt_better(self): + def test_transaction_displacement_sqrt_better(self): # log.set_verbosity(5) consts = config.get_group("evm") consts.sha3 = consts.sha3.concretize mevm = ManticoreEVM() - mevm.register_detector(DetectTransactionReordering()) + mevm.register_detector(DetectTransactionDisplacement()) filename = os.path.join(THIS_DIR, "contracts/sqrt_better.sol") mevm.multi_tx_analysis(filename, tx_limit=2) mevm.finalize() From 4412c66102d56fcfb98fbcb45c497f5ced9d26dc Mon Sep 17 00:00:00 2001 From: Samuel Moelius Date: Tue, 9 Jun 2020 19:21:08 +0000 Subject: [PATCH 6/6] Add optimization. --- manticore/ethereum/detectors.py | 111 +++++++++++++++++++------------- 1 file changed, 68 insertions(+), 43 deletions(-) diff --git a/manticore/ethereum/detectors.py b/manticore/ethereum/detectors.py index 1656c1433..77318a6ad 100644 --- a/manticore/ethereum/detectors.py +++ b/manticore/ethereum/detectors.py @@ -1014,58 +1014,83 @@ def did_run_callback(self): while context_queue: queue.append(context_queue.pop()) - self.info("injecting symbolic transaction (%d queued states)", len(queue)) + self.info("injecting transactions (%d queued states)", len(queue)) for state_id, tx in queue: - # sam.moelius: Manticore deletes states in the ready queue. But this state_id may have - # been queued with multiple txs. So make a copy of this state. - state = self.manticore._load(state_id) - with state as new_state: - state_id = self.manticore._save(new_state) - self.debug("copied state %r to state %r", state.id, state_id) - - assert not self.manticore._ready_states - self.manticore._ready_states.append(state_id) - - if not DEBUG_REPLAY: - troublemaker = None - with self.locked_context(value_type=dict) as context: - troublemaker = context[TROUBLEMAKER] - context[REPLAYING] = False + # sam.moelius: This is an optimization. In the first iteration, the troublemaker's + # transaction has the same data as the original transaction. If the replayed original + # transaction then reverts, no symbolic exploration is performed. + for copy_tx in True, False: + # sam.moelius: Manticore deletes states in the ready queue. But this state_id may + # have been queued with multiple txs. So make a copy of this state. + state = self.manticore._load(state_id) + with state as new_state: + new_state_id = self.manticore._save(new_state) + self.debug("copied state %r to state %r", state.id, new_state_id) - symbolic_address = self.manticore.make_symbolic_value() - symbolic_data = self.manticore.make_symbolic_buffer(320) - symbolic_value = self.manticore.make_symbolic_value() + assert not self.manticore._ready_states + self.manticore._ready_states.append(new_state_id) - self.manticore.transaction( - caller=troublemaker, - address=symbolic_address, - data=symbolic_data, - value=symbolic_value, + if not DEBUG_REPLAY: + troublemaker = None + with self.locked_context(value_type=dict) as context: + troublemaker = context[TROUBLEMAKER] + context[REPLAYING] = False + + symbolic_address = self.manticore.make_symbolic_value() + symbolic_data = self.manticore.make_symbolic_buffer( + 320 if not copy_tx else len(tx.data) + ) + symbolic_value = self.manticore.make_symbolic_value() + + if copy_tx: + self.manticore.constrain(symbolic_data == tx.data) + + self.manticore.transaction( + caller=troublemaker, + address=symbolic_address, + data=symbolic_data, + value=symbolic_value, + ) + + self.info( + "replaying original transaction (%d alive states)", + self.manticore.count_ready_states(), ) - self.info( - "replaying original transaction (%d alive states)", - self.manticore.count_ready_states(), - ) + with self.locked_context(value_type=dict) as context: + context[REPLAYING] = True - with self.locked_context(value_type=dict) as context: - context[REPLAYING] = True + terminated_state_count = self.manticore.count_terminated_states() - self.manticore.transaction( - caller=tx.caller, - data=tx.data, - address=tx.address, - value=tx.value, - gas=tx.gas, - price=tx.price, - ) + self.manticore.transaction( + caller=tx.caller, + data=tx.data, + address=tx.address, + value=tx.value, + gas=tx.gas, + price=tx.price, + ) - # sam.moelius: Move ready states to the terminated list so that test cases are generated - # for them. - while self.manticore._ready_states: - state_id = self.manticore._ready_states.pop() - self.manticore._terminated_states.append(state_id) + # sam.moelius: Move ready states to the terminated list so that test cases are + # generated for them. + while self.manticore._ready_states: + state_id = self.manticore._ready_states.pop() + self.manticore._terminated_states.append(state_id) + + # sam.moelius: This check could not be done in the loop just above, because states + # may have been added to the terminated list when the original transaction was + # replayed. + exit_early = False + for i in range(terminated_state_count, self.manticore.count_terminated_states()): + state_id = self.manticore._terminated_states[i] + state = self.manticore._load(state_id) + if self.get_findings(state): + exit_early = True + self.debug("exiting early") + break + if exit_early: + break with self.manticore.locked_context("ethereum.saved_states", list) as context_saved_states: assert not context_saved_states