Respawn the session when the transport is poisoned

[Suzu1Dev]

Depends on #10 (this branch contains its commits until that lands; rebased onto main after #11 merged, and will rebase again once #10 lands).

Problem

#10 made an incomplete frame write poison the transport, so later calls fail
fast instead of corrupting the protocol. But the session cannot recover
cleanly from that state:

• ensure_main_spawned decides in-place vs respawn from MainFramaCState
  alone and never inspects the transport. The first reload_project with
  explicit files still attempts an in-place reload on the dead transport,
  fails with BrokenPipe, and only then marks the session poisoned — recovery
  takes two calls.
• A no-arg reload_project never reaches ensure_main_spawned at all: its
  file resolution calls kernel.ast.getFiles on the dead transport first
  (src/mcp/project.rs), so the most natural retry fails forever.
• check with files=None hits the same wall through its internal
  reload_project call.
• Every other tool fails fast with a retryable: false error that names no
  remedy, even though a respawn would fix it.
• Until the last commit, the hole was wider: a server that dies
  mid-computation is observed by the in-flight READ (EOF), and
  recv_frame did not set the poison flag there, so the common crash
  shape deferred recovery by yet another call.

Reproduction

Regression tests in tests/test-transport-poison-recovery.rs run a real
Frama-C 33.0, SIGKILL the main instance, and let one getFiles turn the
resulting EPIPE into a poisoned transport (deterministic — no timeouts, no
sleeps). Against the parent commit with only src/ reverted, both tests
fail with the bug's exact signature:

• a single explicit reload must recover the session: I/O error: transport poisoned by an incomplete frame write
• same failure for the no-arg reload

The read-side half is pinned the same way: with src/ reverted,
a_peer_death_mid_read_poisons_every_later_frame fails because the EOF
arm never set the flag.

On this branch everything passes: one explicit reload_project respawns
(the pid changes), a no-arg reload recovers through the cached file list,
and a peer death observed mid-read poisons the transport immediately.

Fix

• Transport.poisoned becomes an Arc<AtomicBool> shared with the owning
  FramaCClient, so is_poisoned() is a lock-free load that never touches
  the request mutex.
• ensure_main_spawned's respawn decision gains that flag as its last
  disjunct: a poisoned transport now respawns on the first reload instead
  of failing in place to mark the session poisoned.
• The no-arg reload_project gates on is_poisoned() and resolves files
  from MainFramaCState.files — the last successfully loaded list — instead
  of asking the dead transport. An empty cache returns an error that names
  the remedy (kind: TransportPoisoned, retryable: true, suggests passing
  files explicitly). Healthy-transport behavior is unchanged.
• recv_frame's EOF and read-error arms poison the transport too,
  mirroring send_frame: after EOF the peer is gone for good, and a read
  error leaves the stream state unknowable. The read-timeout arm
  deliberately does NOT poison — the poll loop times out routinely on
  healthy servers.

Deliberately not in this PR: sandbox clients still have no respawn path
(delete + recreate is their recovery), and capping the poll loop's POLL/Kill
writes at min(remaining, WRITE_TIMEOUT) is left for later — it only
shortens error latency in a session that is already being torn down.

Testing

• New: tests/unit/frama-c-transport.rs (poison mechanics via peer-close:
  write-side, read-side, and a timeout-must-not-poison guard; all run in
  <1 s) and tests/test-transport-poison-recovery.rs (2 session-level
  regression tests, ~6 s)
• Full suite on Frama-C 33.0 / why3 1.8.2 / Alt-Ergo 2.6.3 / Z3 4.13.3:
  539 tests pass (534 baseline + 5 new)
• cargo clippy --all-targets clean

[cubic-dev-ai]

2 issues found across 9 files

Prompt for AI agents (unresolved issues)

Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.


<file name="src/frama-c/transport.rs">

<violation number="1" location="src/frama-c/transport.rs:125">
P3: When a peer dies during `recv_frame`, later calls report an incomplete frame write even though no write failed. Use a direction-neutral poison message so read-side failures remain diagnosable.</violation>
</file>

<file name="src/mcp/server.rs">

<violation number="1" location="src/mcp/server.rs:3036">
P2: When another request is failing concurrently, this one-time poison snapshot can be false. `ensure_main_spawned` then chooses in-place reload, which observes the newly poisoned transport, returns an error, and requires a second call to respawn. Serialize the poison decision with the transport request or retry through the respawn path when the reload observes a newly poisoned client.</violation>
</file>

<sub>Reply with feedback, questions, or to request a fix.

Re-trigger cubic</sub>

[cubic-dev-ai]

P2: When another request is failing concurrently, this one-time poison snapshot can be false. ensure_main_spawned then chooses in-place reload, which observes the newly poisoned transport, returns an error, and requires a second call to respawn. Serialize the poison decision with the transport request or retry through the respawn path when the reload observes a newly poisoned client.

Prompt for AI agents

Check if this issue is valid — if so, understand the root cause and fix it. At src/mcp/server.rs, line 3036:

<comment>When another request is failing concurrently, this one-time poison snapshot can be false. `ensure_main_spawned` then chooses in-place reload, which observes the newly poisoned transport, returns an error, and requires a second call to respawn. Serialize the poison decision with the transport request or retry through the respawn path when the reload observes a newly poisoned client.</comment>

<file context>
@@ -3023,7 +3027,13 @@ impl FramaCMcpServer {
+                s.poisoned
+                    || s.with_rte != new_rte
+                    || s.project_options != new_project_options
+                    || client_lock.as_ref().is_some_and(|c| c.is_poisoned())
             }
         };
</file context>

[cubic-dev-ai]

P3: When a peer dies during recv_frame, later calls report an incomplete frame write even though no write failed. Use a direction-neutral poison message so read-side failures remain diagnosable.

Prompt for AI agents

Check if this issue is valid — if so, understand the root cause and fix it. At src/frama-c/transport.rs, line 125:

<comment>When a peer dies during `recv_frame`, later calls report an incomplete frame write even though no write failed. Use a direction-neutral poison message so read-side failures remain diagnosable.</comment>

<file context>
@@ -56,4 +98,30 @@ impl Transport {
+fn poisoned_transport() -> FramaCError {
+    FramaCError::Io(std::io::Error::new(
+        std::io::ErrorKind::BrokenPipe,
+        "transport poisoned by an incomplete frame write",
+    ))
 }
</file context>

Suggested change

	"transport poisoned by an incomplete frame write",
	"transport poisoned; the connection must be replaced",

[jserv]

Rebase latest main branch and resolve conflicts.

[jserv]

Thank @Suzu1Dev for contributing!