From 85072d56c3827075b3a74cd9078ade4fbc8bc7e6 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Wed, 20 Nov 2024 16:29:47 -0800
Subject: [PATCH] handle info, warn, error

---
 src/halmos/__main__.py   |  4 ++--
 src/halmos/assertions.py |  4 ++--
 src/halmos/bytevec.py    |  2 +-
 src/halmos/config.py     |  2 +-
 src/halmos/console.py    |  4 +++-
 src/halmos/sevm.py       |  2 +-
 src/halmos/utils.py      | 17 +++-----------
 src/halmos/warnings.py   | 50 +++++++++++++++++++++++++++++-----------
 8 files changed, 49 insertions(+), 36 deletions(-)

diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index 808ecde1..61007f1b 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -78,14 +78,12 @@
     con,
     create_solver,
     cyan,
-    error,
     green,
     hexify,
     indent_text,
     red,
     stringify,
     unbox_int,
-    warn,
     yellow,
 )
 from .warnings import (
@@ -96,8 +94,10 @@
     PARSING_ERROR,
     REVERT_ALL,
     debug,
+    error,
     logger,
     logger_unique,
+    warn,
     warn_code,
 )
 
diff --git a/src/halmos/assertions.py b/src/halmos/assertions.py
index de9e432e..303d4730 100644
--- a/src/halmos/assertions.py
+++ b/src/halmos/assertions.py
@@ -13,8 +13,8 @@
     is_bv,
 )
 
-from halmos.exceptions import HalmosException
-from halmos.utils import (
+from .exceptions import HalmosException
+from .utils import (
     bytes_to_bv_value,
     extract_bytes,
     extract_bytes32_array_argument,
diff --git a/src/halmos/bytevec.py b/src/halmos/bytevec.py
index c060c979..711764fc 100644
--- a/src/halmos/bytevec.py
+++ b/src/halmos/bytevec.py
@@ -16,8 +16,8 @@
     extract_bytes,
     try_bv_value_to_bytes,
     unbox_int,
-    warn,
 )
+from .warnings import warn
 
 UnwrappedBytes = bytes | Byte
 WrappedBytes = ForwardRef("Chunk") | ForwardRef("ByteVec")
diff --git a/src/halmos/config.py b/src/halmos/config.py
index c889da3b..4de4cd1f 100644
--- a/src/halmos/config.py
+++ b/src/halmos/config.py
@@ -10,7 +10,7 @@
 
 import toml
 
-from .utils import warn
+from .warnings import warn
 
 # common strings
 internal = "internal"
diff --git a/src/halmos/console.py b/src/halmos/console.py
index 13d3e471..a5c160a3 100644
--- a/src/halmos/console.py
+++ b/src/halmos/console.py
@@ -7,7 +7,6 @@
     extract_funsig,
     extract_string_argument,
     hexify,
-    info,
     int_of,
     magenta,
     render_address,
@@ -15,6 +14,9 @@
     render_bytes,
     render_int,
     render_uint,
+)
+from .warnings import (
+    info,
     warn,
 )
 
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
index da88cb58..9854659b 100644
--- a/src/halmos/sevm.py
+++ b/src/halmos/sevm.py
@@ -124,13 +124,13 @@
     uint160,
     uint256,
     unbox_int,
-    warn,
 )
 from .warnings import (
     INTERNAL_ERROR,
     LIBRARY_PLACEHOLDER,
     debug,
     debug_once,
+    warn,
     warn_code,
 )
 
diff --git a/src/halmos/utils.py b/src/halmos/utils.py
index 62e1c899..bb82cbe3 100644
--- a/src/halmos/utils.py
+++ b/src/halmos/utils.py
@@ -36,8 +36,9 @@
     substitute,
 )
 
-from halmos.exceptions import HalmosException, NotConcreteError
-from halmos.mapper import Mapper
+from .exceptions import HalmosException, NotConcreteError
+from .mapper import Mapper
+from .warnings import warn
 
 # order of the secp256k1 curve
 secp256k1n = (
@@ -593,18 +594,6 @@ def magenta(text: str) -> str:
 color_error = red
 
 
-def error(text: str) -> None:
-    print(color_error(text))
-
-
-def warn(text: str) -> None:
-    print(color_warn(text))
-
-
-def info(text: str) -> None:
-    print(color_info(text))
-
-
 def indent_text(text: str, n: int = 4) -> str:
     return "\n".join(" " * n + line for line in text.splitlines())
 
diff --git a/src/halmos/warnings.py b/src/halmos/warnings.py
index e96bfee1..92bc7325 100644
--- a/src/halmos/warnings.py
+++ b/src/halmos/warnings.py
@@ -3,7 +3,37 @@
 
 from rich.logging import RichHandler
 
-from .utils import color_warn
+#
+# Basic logging
+#
+
+logging.basicConfig(
+    format="%(message)s",
+    handlers=[RichHandler(level=logging.NOTSET, show_time=False)],
+)
+
+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
+#
 
 
 class UniqueLoggingFilter(logging.Filter):
@@ -17,26 +47,18 @@ def filter(self, record):
         return True
 
 
-logging.basicConfig(
-    format="%(message)s",
-    handlers=[RichHandler(level=logging.NOTSET, show_time=False, show_level=False)],
-)
-
-logger = logging.getLogger("halmos")
-
-# logger with filtering out duplicate log messages
 logger_unique = logging.getLogger("halmos.unique")
 logger_unique.addFilter(UniqueLoggingFilter())
 
 
-def debug(text: str) -> None:
-    logger.debug(text)
-
-
 def debug_once(text: str) -> None:
     logger_unique.debug(text)
 
 
+#
+# Warnings with error code
+#
+
 WARNINGS_BASE_URL = "https://github.com/a16z/halmos/wiki/warnings"
 
 
@@ -59,4 +81,4 @@ def url(self) -> str:
 
 
 def warn_code(error_code: ErrorCode, msg: str):
-    logger.warning(f"{color_warn(msg)}\n(see {error_code.url()})")
+    logger.warning(f"{msg}\n(see {error_code.url()})")