Fix the slowdown due to create going through every instruction (#1762)

* Check for 'unchecked' before turning off Integer module

* Use threading during solving constraints

* Hide segfaults

* Misc fixes

* Misc fixes

* Misc fixes

* reformat with black

mythril/interfaces/cli.py

@@ -533,7 +533,7 @@ def add_analysis_args(options):
     options.add_argument(
         "--pruning-factor",
         type=float,
-        default=1,
+        default=None,
         help="Checks for reachability at the rate of <pruning-factor> (range 0-1.0). Where 1.0 would mean checking for every execution",
     )
     options.add_argument(

mythril/laser/ethereum/instructions.py

@@ -60,7 +60,7 @@ from mythril.laser.ethereum.transaction import (
     ContractCreationTransaction,
     tx_id_manager,
 )
-
+from mythril.support.model import get_model
 from mythril.support.support_utils import get_code_hash
 
 from mythril.support.loader import DynLoader
@@ -1733,17 +1733,24 @@ class Instruction:
         code_raw = []
         code_end = call_data.size
         size = call_data.size
+
         if isinstance(size, BitVec):
             # Other size restriction checks handle this
             if size.symbolic:
-                size = 10**5
+                size = 10**4
             else:
                 size = size.value
-        for i in range(size):
+        code_raw = []
-            if call_data[i].symbolic:
+        constraints = global_state.world_state.constraints
-                code_end = i
+        model = get_model(constraints)
+        if isinstance(call_data, ConcreteCalldata):
+            for element in call_data.concrete(model):
+                if isinstance(element, BitVec) and element.symbolic:
                     break
-            code_raw.append(call_data[i].value)
+                if isinstance(element, BitVec):
+                    code_raw.append(element.value)
+                else:
+                    code_raw.append(element)
 
         if len(code_raw) < 1:
             global_state.mstate.stack.append(1)
@@ -1804,6 +1811,7 @@ class Instruction:
             call_value=call_value,
             contract_address=contract_address,
         )
+        log.info("Raise transaction start signal")
         raise TransactionStartSignal(transaction, self.op_code, global_state)
 
     @StateTransition(is_state_mutation_instruction=True)

mythril/laser/ethereum/state/calldata.py

@@ -200,7 +200,10 @@ class BasicConcreteCalldata(BaseCalldata):
         :param model:
         :return:
         """
-        return self._calldata
+        concrete_calldata = []
+        for data in self._calldata:
+            concrete_calldata.append(model.eval(data, model_completion=True))
+        return concrete_calldata
 
     @property
     def size(self) -> int:

mythril/mythril/mythril_analyzer.py

@@ -23,6 +23,8 @@ from mythril.laser.execution_info import ExecutionInfo
 
 log = logging.getLogger(__name__)
 
+LARGE_TIME = 300
+
 
 class MythrilAnalyzer:
     """
@@ -69,6 +71,12 @@ class MythrilAnalyzer:
         args.solver_log = cmd_args.solver_log
         args.transaction_sequences = cmd_args.transaction_sequences
 
+        if args.pruning_factor is None:
+            if self.execution_timeout > LARGE_TIME:
+                args.pruning_factor = 1
+            else:
+                args.pruning_factor = 0
+
     def dump_statespace(self, contract: EVMContract = None) -> str:
         """
         Returns serializable statespace of the contract

mythril/support/model.py

@@ -105,7 +105,6 @@ def get_model(
         try:
             result, s = thread_result.get(solver_timeout)
         except TimeoutError:
-            log.debug("Timeout/Error encountered while solving expression using z3")
             result = unknown
         except Exception:
             log.warning("Encountered an exception while solving expression using z3")

mythril/support/support_args.py

@@ -10,7 +10,7 @@ class Args(object, metaclass=Singleton):
 
     def __init__(self):
         self.solver_timeout = 10000
-        self.pruning_factor = 1
+        self.pruning_factor = None
         self.unconstrained_storage = False
         self.parallel_solving = False
         self.call_depth_limit = 3