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

@@ -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

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):

tests/binaries/795.sol

@@ -0,0 +1,7 @@
+contract Simple {
+    function f(uint a) payable public {
+        if (a == 65) {
+            revert();
+        }
+    }
+}

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))
 

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 = """