[Do Not Merge] dev-evm-experiments

manticore/__main__.py

@@ -2,8 +2,12 @@
 This is the Manticore's CLI `manticore` script.
 """
 import argparse
+import cProfile
+import datetime
 import logging
+import pstats
 import sys
+from typing import Optional
 
 import pkg_resources
 
@@ -39,7 +43,31 @@ def main() -> None:
     set_verbosity(args.v)
 
     if args.argv[0].endswith(".sol") or is_supported(args.argv[0]):
+        cp: Optional[cProfile.Profile] = None
+        if args.perf:
+            # cp = cProfile.Profile()
+            # cp.enable()
+            import yappi
+            yappi.start()
+
         ethereum_main(args, logger)
+        if args.perf:
+            # cp.disable()
+            # stats = pstats.Stats(cp).sort_stats("cumtime")
+            # stats.print_stats()
+            import yappi
+            yappi.stop()
+            # threads = yappi.get_thread_stats()
+            # for thread in threads:
+            #     print(
+            #         "Function stats for (%s) (%d)" % (thread.name, thread.id)
+            #     )  # it is the Thread.__class__.__name__
+            #     yappi.get_func_stats(ctx_id=thread.id).print_all()
+            yappi.get_func_stats().print_all()
+            yappi.get_thread_stats().print_all()
+            func_stats = yappi.get_func_stats()
+            func_stats.save('callgrind.out.' + datetime.datetime.now().isoformat(), 'CALLGRIND')
+
     elif args.argv[0].endswith(".wasm") or args.argv[0].endswith(".wat"):
         wasm_main(args, logger)
     else:
@@ -180,6 +208,15 @@ def positive(value):
         "--contract", type=str, help="Contract name to analyze in case of multiple contracts"
     )
 
+    eth_flags.add_argument(
+        "--lazy-evaluation", action="store_true", help="Enable lazy solver evaluation"
+    )
+
+    eth_flags.add_argument(
+        "--perf", action="store_true", help=argparse.SUPPRESS, default=False
+    )
+
+
     eth_detectors = parser.add_argument_group("Ethereum detectors")
 
     eth_detectors.add_argument(

manticore/core/manticore.py

@@ -18,6 +18,7 @@
 from ..core.state import StateBase
 from ..core.workspace import ManticoreOutput
 from ..exceptions import ManticoreError
+from ..platforms.evm import EVM, EVMWorld
 from ..utils import config
 from ..utils.deprecated import deprecated
 from ..utils.enums import StateLists, MProcessingType
@@ -504,6 +505,20 @@ def _fork(self, state, expression, policy="ALL", setstate=None):
             def setstate(x, y):
                 pass
 
+        # print(policy)
+        # if (
+        #     self._lazy_evaluation
+        #     and (state.platform, EVMWorld)
+        #     and state.platform.current_vm
+        #     and state.platform.current_vm.jumpi_false_branch
+        #     and len(state.platform.current_vm.concrete_stack()) > 2
+        # ):
+        #
+        #     solutions = [
+        #         (state.platform.current_vm.jumpi_false_branch(), False),
+        #         (state.platform.current_vm.concrete_stack()[-2], True),
+        #     ]
+        # else:
         # Find a set of solutions for expression
         solutions = state.concretize(expression, policy)
 

manticore/core/smtlib/constraints.py

@@ -394,7 +394,7 @@ def new_bitvec(self, size, name=None, taint=frozenset(), avoid_collisions=False)
         if size <= 0:
             raise ValueError(f"Bitvec size ({size}) can't be equal to or less than 0")
         if name is None:
-            name = "BV"
+            name = "BIVEC"
             avoid_collisions = True
         if avoid_collisions:
             name = self._make_unique_name(name)