From fb79127bc2c6dafec0c1eea909eedf053a032ffe Mon Sep 17 00:00:00 2001 From: Mark Mossberg Date: Fri, 16 Mar 2018 17:48:36 -0400 Subject: [PATCH] Graceful exit when no states to run (#815) * rm unnecessary return, change assert to graceful handle * Add regression test * Add regression test * Correct logic * Rm unnecessary check This branch is unnecessary, if this condition is true, then ultimately the executor will do nothing, and we'll simply return anyway. * Raise NoAliveStates if no alive states to execute * docstr update * Update mult_tx_analysis to handle NoAliveStates * Fancy * Update test * Codeclimate fmt * fmt * better readability * add docstr --- manticore/ethereum.py | 28 ++++++++++++++++++++++------ manticore/manticore.py | 7 +++++++ tests/binaries/795.sol | 7 +++++++ tests/test_binaries.py | 2 +- tests/test_eth.py | 27 ++++++++++++++++++++++++++- 5 files changed, 63 insertions(+), 8 deletions(-) create mode 100644 tests/binaries/795.sol diff --git a/manticore/ethereum.py b/manticore/ethereum.py index 182cfb3..7f166b7 100644 --- a/manticore/ethereum.py +++ b/manticore/ethereum.py @@ -1,6 +1,7 @@ import string from . import Manticore +from .manticore import ManticoreError from .core.smtlib import ConstraintSet, Operators, solver, issymbolic, Array, Expression, Constant, operators from .core.smtlib.visitors import arithmetic_simplifier from .platforms import evm @@ -22,6 +23,14 @@ logger = logging.getLogger(__name__) ################ Detectors #################### +class EthereumError(ManticoreError): + pass + + +class NoAliveStates(EthereumError): + pass + + class Detector(Plugin): @property def name(self): @@ -872,7 +881,7 @@ class ManticoreEVM(Manticore): return address def transaction(self, caller, address, value, data): - ''' Issue a transaction + ''' Issue a symbolic transaction :param caller: the address of the account sending the transaction :type caller: int or EVMAccount @@ -882,12 +891,18 @@ class ManticoreEVM(Manticore): :type value: int or SValue :param data: initial data :return: an EVMAccount + :raises NoAliveStates: if there are no alive states to execute ''' if isinstance(address, EVMAccount): address = int(address) if isinstance(caller, EVMAccount): caller = int(caller) + with self.locked_context('seth') as context: + has_alive_states = context['_saved_states'] or self.initial_state is not None + if not has_alive_states: + raise NoAliveStates + if isinstance(data, self.SByte): data = (None,) * data.size with self.locked_context('seth') as context: @@ -925,7 +940,10 @@ class ManticoreEVM(Manticore): current_coverage = 0 while current_coverage < 100: - run_symbolic_tx() + try: + run_symbolic_tx() + except NoAliveStates: + break if tx_limit is not None: tx_limit -= 1 @@ -947,8 +965,7 @@ class ManticoreEVM(Manticore): # Check if there is a pending transaction with self.locked_context('seth') as context: assert context['_pending_transaction'] is not None - # there is at least one states in seth saved states - assert context['_saved_states'] or self.initial_state is not None + # there is no states added to the executor queue assert len(self._executor.list()) == 0 @@ -958,7 +975,7 @@ class ManticoreEVM(Manticore): # A callback will use _pending_transaction and issue the transaction # in each state (see load_state_callback) - result = super(ManticoreEVM, self).run(**kwargs) + super(ManticoreEVM, self).run(**kwargs) with self.locked_context('seth') as context: if len(context['_saved_states']) == 1: @@ -968,7 +985,6 @@ class ManticoreEVM(Manticore): # clear pending transcations. We are done. context['_pending_transaction'] = None - return result def save(self, state, final=False): ''' Save a state in secondary storage and add it to running or final lists diff --git a/manticore/manticore.py b/manticore/manticore.py index 19b5e65..c100880 100644 --- a/manticore/manticore.py +++ b/manticore/manticore.py @@ -33,6 +33,13 @@ logger = logging.getLogger(__name__) log.init_logging() +class ManticoreError(Exception): + """ + Top level Exception object for custom exception hierarchy + """ + pass + + def make_binja(program, disasm, argv, env, symbolic_files, concrete_start=''): def _check_disassembler_present(disasm): if is_binja_disassembler(disasm): diff --git a/tests/binaries/795.sol b/tests/binaries/795.sol new file mode 100644 index 0000000..ca471cf --- /dev/null +++ b/tests/binaries/795.sol @@ -0,0 +1,7 @@ +contract Simple { + function f(uint a) payable public { + if (a == 65) { + revert(); + } + } +} \ No newline at end of file diff --git a/tests/test_binaries.py b/tests/test_binaries.py index 9ceb96a..79f525b 100644 --- a/tests/test_binaries.py +++ b/tests/test_binaries.py @@ -128,7 +128,7 @@ class IntegrationTest(unittest.TestCase): self.assertTrue(len(actual) > 100 ) def test_eth_regressions(self): - contracts = [676, 678, 701, 714, 735, 760, 780] + contracts = [676, 678, 701, 714, 735, 760, 780, 795] for contract in contracts: self._simple_cli_run('{}.sol'.format(contract)) diff --git a/tests/test_eth.py b/tests/test_eth.py index 59ff8f5..6950ea6 100644 --- a/tests/test_eth.py +++ b/tests/test_eth.py @@ -4,7 +4,7 @@ import os from manticore.core.smtlib import ConstraintSet, operators from manticore.core.smtlib.expression import BitVec from manticore.core.state import State -from manticore.ethereum import ManticoreEVM, IntegerOverflow, Detector +from manticore.ethereum import ManticoreEVM, IntegerOverflow, Detector, NoAliveStates from manticore.platforms.evm import EVMWorld, ConcretizeStack, concretized_args @@ -92,6 +92,31 @@ class EthTests(unittest.TestCase): self.assertIn('STOP', context) self.assertIn('REVERT', context) + def test_graceful_handle_no_alive_states(self): + """ + If there are no alive states, or no initial states, we should not crash. issue #795 + """ + # initiate the blockchain + m = ManticoreEVM() + source_code = ''' + contract Simple { + function f(uint a) payable public { + if (a == 65) { + revert(); + } + } + } + ''' + + # Initiate the accounts + user_account = m.create_account(balance=1000) + contract_account = m.solidity_create_contract(source_code, owner=user_account, balance=0) + + contract_account.f(1) # it works + contract_account.f(65) # it works + with self.assertRaises(NoAliveStates): + contract_account.f(m.SValue) # no alive states, but try to run a tx anyway + def test_can_create(self): mevm = ManticoreEVM() source_code = """