Address feedback: simplify tagging API and remove unnecessary tests

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

Author: Copilot

src/halmos/__main__.py

@@ -722,7 +722,7 @@ def _compute_frontier(ctx: ContractContext, depth: int) -> Iterator[Exec]:
                             ex=post_ex,
                             panic_found=panic_found,
                             description=msg,
-                            probe_tag=probe_tag,
+                            tag=probe_tag,
                         )
                     except ShutdownError:
                         if args.debug:
@@ -821,7 +821,7 @@ def handle_assertion_violation(
         ex: Exec,
         panic_found: bool,
         description: str = None,
-        probe_tag: str = None,
+        tag: str | None = None,
     ) -> None:
         """
         Handles a potential assertion violation by solving it in a separate process.
@@ -876,7 +876,7 @@ def handle_assertion_violation(
             path_id=path_id,
             solving_ctx=ctx.solving_ctx,
             query=query,
-            tag=probe_tag if probe_tag else ctx.info.sig,
+            tag=tag if tag else ctx.info.sig,
         )
 
         # ShutdownError may be raised here and will be handled by the caller
@@ -974,8 +974,8 @@ def _solve_end_to_end_callback(
 
             # we have a valid counterexample, so we are eligible for early exit
             if args.early_exit:
-                debug(f"Interrupting {ctx.info.name}'s solver queries")
-                get_global_executor().interrupt(ctx.info.name)
+                debug(f"Interrupting {ctx.info.sig}'s solver queries")
+                get_global_executor().interrupt(ctx.info.sig)
         else:
             warn_str = f"Counterexample (potentially invalid): {model}"
             warn_code(COUNTEREXAMPLE_INVALID, warn_str)

tests/test_executor.py

@@ -0,0 +1,81 @@
+# SPDX-License-Identifier: AGPL-3.0
+
+from unittest.mock import Mock
+
+from halmos.processes import PopenFuture, get_global_executor
+
+
+def test_popen_future_with_tag():
+    """Test that PopenFuture accepts and stores tag parameter."""
+    cmd = ["echo", "hello"]
+    tag = "test-tag"
+
+    future = PopenFuture(cmd, tag)
+
+    assert future.cmd == cmd
+    assert future.tag == tag
+
+
+def test_popen_future_with_minimal_args():
+    """Test that PopenFuture works with minimal required parameters."""
+    cmd = ["echo", "hello"]
+    tag = "test-minimal"
+
+    future = PopenFuture(cmd, tag)
+
+    assert future.cmd == cmd
+    assert future.tag == tag
+
+
+def test_popen_future_empty_tag_assertion():
+    """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():
+    """Test that interrupt() cancels futures with matching tags."""
+    executor = get_global_executor()
+
+    # Create mock futures with different tags
+    future1 = Mock(spec=PopenFuture)
+    future1.tag = "tag1"
+    future2 = Mock(spec=PopenFuture)
+    future2.tag = "tag2"
+    future3 = Mock(spec=PopenFuture)
+    future3.tag = "tag1"
+    future4 = Mock(spec=PopenFuture)
+    future4.tag = "tag3"
+
+    # Add to executor's futures list
+    executor._futures = [future1, future2, future3, future4]
+
+    # Interrupt tag1
+    executor.interrupt("tag1")
+
+    # Check that only futures with tag1 were cancelled
+    future1.cancel.assert_called_once()
+    future2.cancel.assert_not_called()
+    future3.cancel.assert_called_once()
+    future4.cancel.assert_not_called()
+
+
+def test_interrupt_nonexistent_tag():
+    """Test that interrupt() with non-existent tag does nothing."""
+    executor = get_global_executor()
+
+    # Create mock future
+    future = Mock(spec=PopenFuture)
+    future.tag = "existing-tag"
+    executor._futures = [future]
+
+    # Interrupt with non-existent tag
+    executor.interrupt("nonexistent-tag")
+
+    # No futures should be cancelled
+    future.cancel.assert_not_called()