Address feedback: make tag required and simplify global executor init

Co-authored-by: 0xkarmacoma <[email protected]>

Author: Copilot

src/halmos/__main__.py

@@ -430,8 +430,8 @@ def setup(ctx: FunctionContext) -> Exec:
                 path_ctx = PathContext(
                     args=args,
                     path_id=path_id,
-                    query=query,
                     solving_ctx=ctx.solving_ctx,
+                    query=query,
                     tag=ctx.info.sig,
                 )
                 solver_output = solve_low_level(path_ctx)
@@ -874,8 +874,8 @@ def handle_assertion_violation(
         path_ctx = PathContext(
             args=args,
             path_id=path_id,
-            query=query,
             solving_ctx=ctx.solving_ctx,
+            query=query,
             tag=probe_tag if probe_tag else ctx.info.sig,
         )
 
@@ -1094,8 +1094,8 @@ def run_test(ctx: FunctionContext) -> TestResult:
             path_ctx = PathContext(
                 args=args,
                 path_id=path_id,
-                query=ex.path.to_smt2(args),
                 solving_ctx=ctx.solving_ctx,
+                query=ex.path.to_smt2(args),
                 tag=ctx.info.sig,
             )
             solver_output = solve_low_level(path_ctx)

src/halmos/processes.py

@@ -34,7 +34,7 @@ def shutdown_all(self):
 class PopenFuture(concurrent.futures.Future):
     cmd: list[str]
     timeout: float | None  # in seconds, None means no timeout
-    tag: str | None  # optional tag for grouping and selective cancellation
+    tag: str  # tag for grouping and selective cancellation
     process: subprocess.Popen | None
     stdout: str | None
     stderr: str | None
@@ -43,10 +43,9 @@ class PopenFuture(concurrent.futures.Future):
     end_time: float | None
     _exception: Exception | None
 
-    def __init__(
-        self, cmd: list[str], timeout: float | None = None, tag: str | None = None
-    ):
+    def __init__(self, cmd: list[str], tag: str, timeout: float | None = None):
         super().__init__()
+        assert tag, "tag cannot be empty"
         self.cmd = cmd
         self.timeout = timeout
         self.tag = tag
@@ -199,18 +198,17 @@ def submit(self, future: PopenFuture) -> PopenFuture:
 
     def interrupt(self, tag: str) -> None:
         """Interrupts all futures with the specified tag.
-        
+
         Args:
-            tag: The tag identifying futures to interrupt. 
-                 Futures without tags are not affected.
+            tag: The tag identifying futures to interrupt.
+                 Futures with a different tag are not affected.
         """
-        if not tag:
-            return
-            
+        assert tag, "tag cannot be empty"
+
         with self._lock:
             # Find all futures with the matching tag and cancel them
             futures_to_cancel = [f for f in self._futures if f.tag == tag]
-            
+
         # Cancel outside the lock to avoid deadlocks
         for future in futures_to_cancel:
             future.cancel()
@@ -251,22 +249,13 @@ def _join(self):
 
 
 # Global PopenExecutor instance for shared use across all tests and probes
-_global_executor: PopenExecutor | None = None
-_global_executor_lock = threading.Lock()
+_executor = PopenExecutor()
+ExecutorRegistry().register(_executor)
 
 
 def get_global_executor() -> PopenExecutor:
-    """Get the global PopenExecutor instance, creating it if necessary."""
-    global _global_executor
-    
-    if _global_executor is None:
-        with _global_executor_lock:
-            if _global_executor is None:
-                _global_executor = PopenExecutor()
-                # Register with the ExecutorRegistry so it gets shut down properly
-                ExecutorRegistry().register(_global_executor)
-    
-    return _global_executor
+    """Get the global PopenExecutor instance."""
+    return _executor
 
 
 def main():
@@ -293,7 +282,7 @@ def done_callback(future: PopenFuture):
         ]
 
         futures = [
-            PopenFuture(command.split(), tag=f"test-{i}")
+            PopenFuture(command.split(), f"test-{i}")
             for i, command in enumerate(commands)
         ]
 

src/halmos/solve.py

@@ -274,8 +274,8 @@ class PathContext:
     path_id: int
     solving_ctx: SolvingContext
     query: SMTQuery
+    tag: str  # tag for grouping solver queries
     is_refined: bool = False
-    tag: str | None = None  # optional tag for grouping solver queries
 
     @property
     def dump_file(self) -> Path:
@@ -290,8 +290,8 @@ def refine(self) -> "PathContext":
             path_id=self.path_id,
             solving_ctx=self.solving_ctx,
             query=refine(self.query),
-            is_refined=True,
             tag=self.tag,
+            is_refined=True,
         )
 
 
@@ -494,7 +494,7 @@ def solve_low_level(path_ctx: PathContext) -> SolverOutput:
         else args.solver_command
     )
     cmd_with_file = cmd_list + [smt2_filename]
-    future = PopenFuture(cmd_with_file, timeout=timeout_seconds, tag=path_ctx.tag)
+    future = PopenFuture(cmd_with_file, path_ctx.tag, timeout=timeout_seconds)
 
     # starts the subprocess asynchronously
     get_global_executor().submit(future)

tests/test_global_executor.py

@@ -38,19 +38,30 @@ def test_popen_future_with_tag(self):
         cmd = ["echo", "hello"]
         tag = "test-tag"
 
-        future = PopenFuture(cmd, tag=tag)
+        future = PopenFuture(cmd, tag)
 
         assert future.cmd == cmd
         assert future.tag == tag
 
-    def test_popen_future_without_tag(self):
-        """Test that PopenFuture works without tag parameter."""
+    def test_popen_future_with_minimal_args(self):
+        """Test that PopenFuture works with minimal required parameters."""
         cmd = ["echo", "hello"]
+        tag = "test-minimal"
 
-        future = PopenFuture(cmd)
+        future = PopenFuture(cmd, tag)
 
         assert future.cmd == cmd
-        assert future.tag is None
+        assert future.tag == tag
+
+    def test_popen_future_empty_tag_assertion(self):
+        """Test that PopenFuture raises assertion error for empty tag."""
+        cmd = ["echo", "hello"]
+        
+        try:
+            PopenFuture(cmd, "")
+            raise AssertionError("Expected AssertionError for empty tag")
+        except AssertionError:
+            pass  # Expected
 
     def test_interrupt_by_tag(self):
         """Test that interrupt() cancels futures with matching tags."""
@@ -64,7 +75,7 @@ def test_interrupt_by_tag(self):
         future3 = Mock(spec=PopenFuture)
         future3.tag = "tag1"
         future4 = Mock(spec=PopenFuture)
-        future4.tag = None
+        future4.tag = "tag3"
 
         # Add to executor's futures list
         executor._futures = [future1, future2, future3, future4]
@@ -79,16 +90,20 @@ def test_interrupt_by_tag(self):
         future4.cancel.assert_not_called()
 
     def test_interrupt_with_empty_tag(self):
-        """Test that interrupt() with empty tag does nothing."""
+        """Test that interrupt() with empty tag raises assertion error."""
         executor = get_global_executor()
 
         # Create mock future
         future = Mock(spec=PopenFuture)
         future.tag = "some-tag"
         executor._futures = [future]
 
-        # Interrupt with empty tag
-        executor.interrupt("")
+        # Interrupt with empty tag should raise assertion error
+        try:
+            executor.interrupt("")
+            raise AssertionError("Expected AssertionError for empty tag")
+        except AssertionError:
+            pass  # Expected
 
         # No futures should be cancelled
         future.cancel.assert_not_called()

tests/test_solver_integration.py

@@ -1,13 +1,14 @@
 # SPDX-License-Identifier: AGPL-3.0
 
-from unittest.mock import Mock, patch
+import contextlib
 import tempfile
 from pathlib import Path
+from unittest.mock import Mock, patch
 
-from halmos.solve import SolvingContext, PathContext, solve_low_level
-from halmos.sevm import SMTQuery
 from halmos.config import Config as HalmosConfig
-from halmos.processes import get_global_executor, PopenFuture
+from halmos.processes import PopenFuture, get_global_executor
+from halmos.sevm import SMTQuery
+from halmos.solve import PathContext, SolvingContext, solve_low_level
 
 
 class TestSolverIntegration:
@@ -51,11 +52,9 @@ def mock_submit(future):
 
             # Mock the global executor's submit method
             with patch.object(get_global_executor(), 'submit', side_effect=mock_submit):
-                try:
-                    solve_low_level(path_ctx)
-                except Exception:
+                with contextlib.suppress(Exception):
                     # We expect this might fail due to mocking, that's OK
-                    pass
+                    solve_low_level(path_ctx)
 
                 # Verify that a future was submitted with the correct tag
                 assert len(submitted_futures) == 1