From 04cb455a13727e420f178f3bbe459ecf67aa5a33 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Tue, 7 Jan 2025 12:11:55 -0800
Subject: [PATCH] fix: add warnings when --width or --depth limits reached
 (#433)

---
 src/halmos/__main__.py |  7 +++++--
 src/halmos/logs.py     | 42 +++++++++++++++++++++++-------------------
 src/halmos/sevm.py     |  9 ++++++++-
 tests/test_fixtures.py | 10 ++++++++--
 4 files changed, 44 insertions(+), 24 deletions(-)

diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index 1d4cde8e..1d247ada 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -423,7 +423,7 @@ def setup(
     setup_timer = NamedTimer("setup")
     setup_timer.create_subtimer("decode")
 
-    sevm = SEVM(args)
+    sevm = SEVM(args, setup_info)
     setup_ex = deploy_test(creation_hexcode, deployed_hexcode, sevm, args, libs, solver)
 
     setup_timer.create_subtimer("run")
@@ -586,7 +586,7 @@ def run(
     # calldata
     #
 
-    sevm = SEVM(args)
+    sevm = SEVM(args, fun_info)
     path = Path(solver)
     path.extend_path(setup_ex.path)
 
@@ -742,6 +742,9 @@ def future_callback(future_model):
 
         # 0 width is unlimited
         if args.width and idx >= args.width:
+            warn(
+                f"{funsig}: incomplete execution due to the specified limit: --width {args.width}"
+            )
             break
 
     num_execs = idx + 1
diff --git a/src/halmos/logs.py b/src/halmos/logs.py
index 1919e75d..da51d3ba 100644
--- a/src/halmos/logs.py
+++ b/src/halmos/logs.py
@@ -15,22 +15,6 @@
 logger = logging.getLogger("halmos")
 
 
-def debug(text: str) -> None:
-    logger.debug(text)
-
-
-def info(text: str) -> None:
-    logger.info(text)
-
-
-def warn(text: str) -> None:
-    logger.warning(text)
-
-
-def error(text: str) -> None:
-    logger.error(text)
-
-
 #
 # Logging with filtering out duplicate log messages
 #
@@ -51,8 +35,28 @@ def filter(self, record):
 logger_unique.addFilter(UniqueLoggingFilter())
 
 
+def logger_for(allow_duplicate=True) -> logging.Logger:
+    return logger if allow_duplicate else logger_unique
+
+
+def debug(text: str, allow_duplicate=True) -> None:
+    logger_for(allow_duplicate).debug(text)
+
+
+def info(text: str, allow_duplicate=True) -> None:
+    logger_for(allow_duplicate).info(text)
+
+
+def warn(text: str, allow_duplicate=True) -> None:
+    logger_for(allow_duplicate).warning(text)
+
+
+def error(text: str, allow_duplicate=True) -> None:
+    logger_for(allow_duplicate).error(text)
+
+
 def debug_once(text: str) -> None:
-    logger_unique.debug(text)
+    debug(text, allow_duplicate=False)
 
 
 #
@@ -80,5 +84,5 @@ def url(self) -> str:
 LOOP_BOUND = ErrorCode("loop-bound")
 
 
-def warn_code(error_code: ErrorCode, msg: str):
-    logger.warning(f"{msg}\n(see {error_code.url()})")
+def warn_code(error_code: ErrorCode, msg: str, allow_duplicate=True):
+    logger_for(allow_duplicate).warning(f"{msg}\n(see {error_code.url()})")
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index e20479ed..f52b4610 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -57,6 +57,7 @@
 from z3.z3util import is_expr_var
 
 from .bytevec import ByteVec, Chunk, ConcreteChunk, UnwrappedBytes
+from .calldata import FunctionInfo
 from .cheatcodes import Prank, halmos_cheat_code, hevm_cheat_code
 from .config import Config as HalmosConfig
 from .console import console
@@ -1703,12 +1704,14 @@ def __len__(self) -> int:
 
 class SEVM:
     options: HalmosConfig
+    fun_info: FunctionInfo
     storage_model: type[SomeStorage]
     logs: HalmosLogs
     steps: Steps
 
-    def __init__(self, options: HalmosConfig) -> None:
+    def __init__(self, options: HalmosConfig, fun_info: FunctionInfo) -> None:
         self.options = options
+        self.fun_info = fun_info
         self.logs = HalmosLogs()
         self.steps: Steps = {}
 
@@ -2718,6 +2721,10 @@ def finalize(ex: Exec):
                 opcode = insn.opcode
 
                 if (max_depth := self.options.depth) and step_id > max_depth:
+                    warn(
+                        f"{self.fun_info.sig}: incomplete execution due to the specified limit: --depth {max_depth}",
+                        allow_duplicate=False,
+                    )
                     continue
 
                 # TODO: clean up
diff --git a/tests/test_fixtures.py b/tests/test_fixtures.py
index d6834a1a..bf321ea4 100644
--- a/tests/test_fixtures.py
+++ b/tests/test_fixtures.py
@@ -1,6 +1,7 @@
 import pytest
 
 from halmos.__main__ import mk_solver
+from halmos.calldata import FunctionInfo
 from halmos.config import default_config
 from halmos.sevm import SEVM
 
@@ -11,8 +12,13 @@ def args():
 
 
 @pytest.fixture
-def sevm(args):
-    return SEVM(args)
+def fun_info():
+    return FunctionInfo("test", "test()", "f8a8fd6d")
+
+
+@pytest.fixture
+def sevm(args, fun_info):
+    return SEVM(args, fun_info)
 
 
 @pytest.fixture