handle info, warn, error

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,
 )
 

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,

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")

src/halmos/config.py

@@ -10,7 +10,7 @@
 
 import toml
 
-from .utils import warn
+from .warnings import warn
 
 # common strings
 internal = "internal"

src/halmos/console.py

@@ -7,14 +7,16 @@
     extract_funsig,
     extract_string_argument,
     hexify,
-    info,
     int_of,
     magenta,
     render_address,
     render_bool,
     render_bytes,
     render_int,
     render_uint,
+)
+from .warnings import (
+    info,
     warn,
 )
 

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,
 )
 

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())
 

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()})")