Skip to content

Commit

Permalink
minor updates
Browse files Browse the repository at this point in the history
  • Loading branch information
daejunpark committed Dec 4, 2024
1 parent a59f03c commit b9f64a2
Show file tree
Hide file tree
Showing 4 changed files with 11 additions and 9 deletions.
2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ dependencies = [
"toml>=0.10.2",
"z3-solver==4.12.6.0",
"eth_hash[pysha3]>=0.7.0",
"rich>=13.8.1"
"rich>=13.9.4"
]
dynamic = ["version"]

Expand Down
8 changes: 5 additions & 3 deletions src/halmos/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@
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

Expand Down Expand Up @@ -735,16 +736,17 @@ def future_callback(future_model):
)

# display assertion solving progress
if not args.no_pulse or args.early_exit:
with Status("solving:") as status:
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
status.update(f"solving: {done} / {total}")
elapsed = timedelta(seconds=int(timer.elapsed()))
status.update(f"[{elapsed}] solving queries: {done} / {total}")
time.sleep(0.1)

if args.early_exit:
Expand Down
2 changes: 1 addition & 1 deletion src/halmos/config.py
Original file line number Diff line number Diff line change
Expand Up @@ -296,7 +296,7 @@ class Config:
short="st",
)

no_pulse: bool = arg(
no_status: bool = arg(
help="disable progress display",
global_default=False,
group=debugging,
Expand Down
8 changes: 4 additions & 4 deletions src/halmos/sevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -1659,7 +1659,7 @@ class Worklist:
def __init__(self):
self.stack = []

# pulse data
# status data
self.completed_paths = 0
self.start_time = timer()

Expand Down Expand Up @@ -2640,7 +2640,7 @@ def gen_nested_ite(curr: int) -> BitVecRef:
return ZeroExt(248, gen_nested_ite(0))

def run(self, ex0: Exec) -> Iterator[Exec]:
with Status("pulse:") as status:
with Status("") as status:
yield from self._run(ex0, status)

def _run(self, ex0: Exec, status: Status) -> Iterator[Exec]:
Expand All @@ -2667,12 +2667,12 @@ def finalize(ex: Exec):
step_id += 1

# display progress
if not self.options.no_pulse and step_id % PULSE_INTERVAL == 0:
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 = str(timedelta(seconds=int(elapsed)))
elapsed_fmt = timedelta(seconds=int(elapsed))

status.update(
f"[{elapsed_fmt}] {speed:.0f} ops/s"
Expand Down

0 comments on commit b9f64a2

Please sign in to comment.