Merge branch 'main' into embrace-uv

pyproject.toml

@@ -25,7 +25,8 @@ dependencies = [
     "sortedcontainers>=2.4.0",
     "toml>=0.10.2",
     "z3-solver==4.12.6.0",
-    "eth_hash[pysha3]>=0.7.0"
+    "eth_hash[pysha3]>=0.7.0",
+    "rich>=13.9.4"
 ]
 dynamic = ["version"]
 

src/halmos/__main__.py

@@ -15,9 +15,11 @@
 from concurrent.futures import ThreadPoolExecutor
 from copy import deepcopy
 from dataclasses import asdict, dataclass
+from datetime import timedelta
 from enum import Enum
 from importlib import metadata
 
+from rich.status import Status
 from z3 import (
     Z3_OP_CONCAT,
     BitVec,
@@ -733,14 +735,22 @@ def future_callback(future_model):
             f"# of potential paths involving assertion violations: {len(future_models)} / {len(result_exs)}  (--solver-threads {args.solver_threads})"
         )
 
-    if args.early_exit:
-        while not (
-            len(counterexamples) > 0 or all([fm.done() for fm in future_models])
-        ):
-            time.sleep(1)
+    # display assertion solving progress
+    if not args.no_status or args.early_exit:
+        with Status("") as status:
+            while True:
+                if args.early_exit and len(counterexamples) > 0:
+                    break
+                done = sum(fm.done() for fm in future_models)
+                total = len(future_models)
+                if done == total:
+                    break
+                elapsed = timedelta(seconds=int(timer.elapsed()))
+                status.update(f"[{elapsed}] solving queries: {done} / {total}")
+                time.sleep(0.1)
 
+    if args.early_exit:
         thread_pool.shutdown(wait=False, cancel_futures=True)
-
     else:
         thread_pool.shutdown(wait=True)
 

src/halmos/config.py

@@ -296,6 +296,12 @@ class Config:
         short="st",
     )
 
+    no_status: bool = arg(
+        help="disable progress display",
+        global_default=False,
+        group=debugging,
+    )
+
     debug: bool = arg(
         help="run in debug mode",
         global_default=False,

src/halmos/sevm.py

@@ -5,7 +5,9 @@
 from collections.abc import Callable, Iterator
 from copy import deepcopy
 from dataclasses import dataclass, field
+from datetime import timedelta
 from functools import reduce
+from timeit import default_timer as timer
 from typing import (
     Any,
     ForwardRef,
@@ -14,6 +16,7 @@
 )
 
 from eth_hash.auto import keccak
+from rich.status import Status
 from z3 import (
     UGE,
     UGT,
@@ -144,6 +147,7 @@
 
 # TODO: make this configurable
 MAX_MEMORY_SIZE = 2**20
+PULSE_INTERVAL = 2**13
 
 FOUNDRY_CALLER = 0x1804C8AB1F12E6BBF3894D4083F33E07309D1F38
 FOUNDRY_ORIGIN = FOUNDRY_CALLER
@@ -1655,6 +1659,10 @@ class Worklist:
     def __init__(self):
         self.stack = []
 
+        # status data
+        self.completed_paths = 0
+        self.start_time = timer()
+
     def push(self, ex: Exec, step: int):
         self.stack.append(WorklistItem(ex, step))
 
@@ -2061,6 +2069,7 @@ def callback(new_ex: Exec, stack, step_id):
                 if subcall.is_stuck():
                     # internal errors abort the current path,
                     # so we don't need to add it to the worklist
+                    stack.completed_paths += 1
                     yield new_ex
                     return
 
@@ -2402,6 +2411,7 @@ def callback(new_ex: Exec, stack, step_id):
 
             if subcall.is_stuck():
                 # internal errors abort the current path,
+                stack.completed_paths += 1
                 yield new_ex
                 return
 
@@ -2630,13 +2640,18 @@ def gen_nested_ite(curr: int) -> BitVecRef:
         return ZeroExt(248, gen_nested_ite(0))
 
     def run(self, ex0: Exec) -> Iterator[Exec]:
+        with Status("") as status:
+            yield from self._run(ex0, status)
+
+    def _run(self, ex0: Exec, status: Status) -> Iterator[Exec]:
         step_id: int = 0
         stack: Worklist = Worklist()
         stack.push(ex0, 0)
 
         def finalize(ex: Exec):
             # if it's at the top-level, there is no callback; yield the current execution state
             if ex.callback is None:
+                stack.completed_paths += 1
                 yield ex
 
             # otherwise, execute the callback to return to the parent execution context
@@ -2651,6 +2666,20 @@ def finalize(ex: Exec):
                 prev_step_id: int = item.step
                 step_id += 1
 
+                # display progress
+                if not self.options.no_status and step_id % PULSE_INTERVAL == 0:
+                    elapsed = timer() - stack.start_time
+                    speed = step_id / elapsed
+
+                    # hh:mm:ss
+                    elapsed_fmt = timedelta(seconds=int(elapsed))
+
+                    status.update(
+                        f"[{elapsed_fmt}] {speed:.0f} ops/s"
+                        f" | completed paths: {stack.completed_paths}"
+                        f" | outstanding paths: {len(stack)}"
+                    )
+
                 if not ex.path.is_activated():
                     ex.path.activate()
 
@@ -3121,6 +3150,7 @@ def finalize(ex: Exec):
                 if not ex.is_halted():
                     # return data shouldn't be None, as it is considered being stuck
                     ex.halt(data=ByteVec(), error=err)
+                stack.completed_paths += 1
                 yield ex  # early exit; do not call finalize()
                 continue