Merge pull request #67 from crytic/62-fix-examples

Fixes the BrokenMetaCoin example

etheno/manticoreclient.py

@@ -30,12 +30,14 @@ def manticoreimport(name, *args, **kwargs):
 # ####END####
 
 from manticore.ethereum import ManticoreEVM
+from manticore.exceptions import NoAliveStates
 import manticore
 
 from . import logger
 from . import threadwrapper
 from .client import EthenoClient, jsonrpc, DATA, QUANTITY
 from .etheno import _CONTROLLER
+from .manticoreutils import manticore_is_new_enough
 
 def encode_hex(data):
     if data is None:
@@ -139,15 +141,24 @@ def eth_getTransactionReceipt(self, tx_hash, rpc_client_result = None):
     def multi_tx_analysis(self, contract_address = None, tx_limit=None, tx_use_coverage=True, args=None):
         if contract_address is None:
             for contract_address in self.contracts:
-                self.multi_tx_analysis(contract_address = contract_address, tx_limit = tx_limit, tx_use_coverage = tx_use_coverage, args = args)
+                self.multi_tx_analysis(
+                    contract_address=contract_address,
+                    tx_limit=tx_limit,
+                    tx_use_coverage=tx_use_coverage,
+                    args=args
+                )
             return
 
         tx_account = self.etheno.accounts
 
-        prev_coverage = 0
         current_coverage = 0
         tx_no = 0
-        while (current_coverage < 100 or not tx_use_coverage) and not self.manticore.is_shutdown():
+        if manticore_is_new_enough(0, 3, 0):
+            shutdown_test = 'is_killed'
+        else:
+            shutdown_test = 'is_shutdown'
+
+        while (current_coverage < 100 or not tx_use_coverage) and not getattr(self.manticore, shutdown_test)():
             try:
                 self.logger.info("Starting symbolic transaction: %d" % tx_no)
 
@@ -158,7 +169,11 @@ def multi_tx_analysis(self, contract_address = None, tx_limit=None, tx_use_cover
                                  address=contract_address,
                                  data=symbolic_data,
                                  value=symbolic_value)
-                self.logger.info("%d alive states, %d terminated states" % (self.manticore.count_running_states(), self.manticore.count_terminated_states()))
+                if manticore_is_new_enough(0, 3, 0):
+                    # TODO: find the equivalent functions to get state counts in v0.3.0
+                    pass
+                else:
+                    self.logger.info("%d alive states, %d terminated states" % (self.manticore.count_running_states(), self.manticore.count_terminated_states()))
             except NoAliveStates:
                 break
 

etheno/manticoreutils.py

@@ -33,15 +33,42 @@ def manticore_is_new_enough(*required_version):
     return True
 
 
+"""Detectors that should not be included in the results from `get_detectors()` (e.g., because they are buggy)"""
+if manticore_is_new_enough(0, 2, 3):
+    # At some point after Manticore 0.2.2, these all stopped working:
+    DETECTOR_BLACKLIST = {
+        manticore.ethereum.detectors.DetectDelegatecall,
+        manticore.ethereum.detectors.DetectEnvInstruction,
+        manticore.ethereum.detectors.DetectExternalCallAndLeak,
+        manticore.ethereum.detectors.DetectIntegerOverflow,
+        manticore.ethereum.detectors.DetectInvalid,
+        manticore.ethereum.detectors.DetectRaceCondition,
+        manticore.ethereum.detectors.DetectReentrancyAdvanced,
+        manticore.ethereum.detectors.DetectReentrancySimple,
+        manticore.ethereum.detectors.DetectSuicidal,
+        manticore.ethereum.detectors.DetectUninitializedMemory,
+        manticore.ethereum.detectors.DetectUninitializedStorage,
+        manticore.ethereum.detectors.DetectUnusedRetVal
+    }
+else:
+    DETECTOR_BLACKLIST = set()
+
+
 def get_detectors():
     for name, obj in inspect.getmembers(manticore.ethereum.detectors):
-        if inspect.isclass(obj) and issubclass(obj, manticore.ethereum.detectors.Detector) and obj != manticore.ethereum.detectors.Detector:
+        if inspect.isclass(obj)\
+                and issubclass(obj, manticore.ethereum.detectors.Detector)\
+                and obj != manticore.ethereum.detectors.Detector\
+                and obj not in DETECTOR_BLACKLIST:
             yield obj
 
 
 def register_all_detectors(manticore):
     for detector in get_detectors():
-        manticore.register_detector(detector())
+        try:
+            manticore.register_detector(detector())
+        except Exception as e:
+            manticore.logger.warning(f"Unable to register detector {detector!r}: {e!s}")
 
 
 class StopAtDepth(Detector):
@@ -50,8 +77,10 @@ class StopAtDepth(Detector):
     def __init__(self, max_depth):
         self.max_depth = max_depth
 
-        def will_start_run_callback(self, *args):
-            with self.manticore.locked_context('seen_rep', dict) as reps:
+        stop_at_death = self
+
+        def will_start_run_callback(*args):
+            with stop_at_death.manticore.locked_context('seen_rep', dict) as reps:
                 reps.clear()
 
         # this callback got renamed to `will_run_callback` in Manticore 0.3.0
@@ -66,7 +95,7 @@ def will_decode_instruction_callback(self, state, pc):
         world = state.platform
         with self.manticore.locked_context('seen_rep', dict) as reps:
             item = (world.current_transaction.sort == 'CREATE', world.current_transaction.address, pc)
-            if not item in reps:
+            if item not in reps:
                 reps[item] = 0
             reps[item] += 1
             if reps[item] > self.max_depth: