Makes a stdio connection refusal that nothing diagnosed fail CI

.github/workflows/ci.yml

@@ -43,8 +43,9 @@ concurrency:
     ${{ github.workflow }}-${{ github.event.pull_request.head.repo.full_name || github.repository }}-${{ github.event.pull_request.head.ref || github.ref_name }}
   cancel-in-progress: ${{ github.ref != 'refs/heads/main' }}
 
-# Nothing here writes to the repository, except the release job, which raises
-# this to contents: write for itself alone.
+# The floor, raised per job by the two that need more: the release job takes
+# contents: write to publish, and artifact-scans takes checks: write because the
+# advisory action reports by creating a check run. Nothing else writes anything.
 permissions:
   contents: read
 
@@ -111,20 +112,48 @@ jobs:
       - name: Release build
         run: cargo build --release --tests
 
-  # Reads the tree and nothing else, so it costs a minute and needs no
-  # toolchain. Kept a separate job rather than a step of the fast lane because
-  # its finding is about the documents, and a person reading a red run should
-  # see which of the two it was without opening a log.
+  # No toolchain and no build. Kept a separate job rather than a step of the
+  # fast lane because its finding is about the documents, and a person reading a
+  # red run should see which of the two it was without opening a log. The
+  # advisory scan is a step here rather than a job of its own so it reuses this
+  # checkout, which is also why this job is no longer only reading the tree: it
+  # fetches a cargo-audit binary and queries the advisory database.
   artifact-scans:
     name: Artifact scans
     runs-on: ubuntu-24.04
     timeout-minutes: 10
+    # Raised for this job alone, the way the release job raises contents. The
+    # advisory action reports by creating a check run, so the workflow-wide
+    # contents: read leaves it unable to publish the only thing it produces.
+    permissions:
+      contents: read
+      checks: write
     steps:
       - uses: actions/checkout@v7
         with:
           persist-credentials: false
       - run: scripts/check-artifacts.sh
 
+      # Not in scripts/run-gates.sh, and deliberately so. Every gate the runner
+      # holds is reproducible from the commit, which is the whole reason
+      # Cargo.lock is tracked; this one answers from an advisory database that
+      # moves on its own, so it is the one check whose verdict is not a function
+      # of the tree. There is no schedule here either, so this catches a
+      # vulnerable dependency arriving rather than one discovered later; the
+      # discovered-later half is what Dependabot alerts are for.
+      #
+      # Skipped on pull requests from forks, where GitHub caps GITHUB_TOKEN at
+      # read-only whatever the permissions block says, so the action cannot
+      # create the check run it reports through and fails on a clean tree. This
+      # repository takes fork pull requests, so that is a real run and not a
+      # hypothetical one. A dependency arriving that way is still scanned, on
+      # the push that merges it.
+      - name: RustSec advisories against the tracked lockfile
+        if: ${{ github.event_name == 'push' || github.event.pull_request.head.repo.full_name == github.repository }}
+        uses: rustsec/audit-check@v2
+        with:
+          token: ${{ secrets.GITHUB_TOKEN }}
+
   # Full lane: Frama-C + WP provers + the ast-utils plugin, then the
   # integration / MCP-stdio suites that drive a real Frama-C server.
   integration:
@@ -251,11 +280,34 @@ jobs:
           cargo test --test test-store-conclusion -- --test-threads=1
 
       - name: MCP stdio E2E tests
+        id: stdio
         # Parallel, unlike the gates above: every test in this suite owns its
         # server, its frama-c and its state directory. See scripts/run-gates.sh
         # for the measurement. libtest's default is available parallelism, so
         # this follows the runner rather than pinning a count.
-        run: cargo test --test test-mcp-stdio --release
+        env:
+          # A bind/listen race the retry absorbs is reported as a tracing warn,
+          # and the default EnvFilter admits ERROR only, so without this the one
+          # signal that the flake is coming back is dropped before it reaches
+          # the log the next step scans.
+          RUST_LOG: frama_c_mcp=warn
+        run: |
+          set -o pipefail
+          cargo test --test test-mcp-stdio --release 2>&1 | tee "$RUNNER_TEMP/mcp-stdio.log"
+
+      # Not success(): a refusal is one of the things that fails the suite, so
+      # the scan has to happen on exactly the runs where the step above went
+      # red. !cancelled() alone would not be enough, because it differs from
+      # always() only on cancellation, so an earlier failed step in this job
+      # skips the suite and still reaches here to scan a log nobody wrote. The
+      # outcome check is what excludes that, and it is what lets the script
+      # treat a missing log as a failure instead of tolerating one. A tolerated
+      # missing log is a gate that passes by not running.
+      - name: Detect an unqualified stdio connection refusal
+        if: ${{ !cancelled() && (steps.stdio.outcome == 'success' || steps.stdio.outcome == 'failure') }}
+        env:
+          STDIO_LOG: ${{ runner.temp }}/mcp-stdio.log
+        run: scripts/check-stdio-refusal.sh
 
   # The supported floor, compiled but not measured. The three shell gates in
   # the lane above pin proved-goal counts to Frama-C 33.0 and Alt-Ergo 2.6.3,

ast-utils/src/ast_utils_export.ml

@@ -1508,17 +1508,19 @@ let dump_project () : Yojson.Basic.t =
 
   `Assoc [
     ("prog_defs", prog_defs_json);
-    ("prog_public", `List []);  (* TODO: collect public symbols *)
     ("prog_main", (match main_id with Some id -> `Int id | None -> `Null));
     ("ident_names", ident_names_to_json tbl);
     ("acsl_globals", dump_acsl_globals tbl);
     ("includes", `List (List.map (fun s -> `String s) includes));
     ("composites", `List (List.rev !composites));
     ("enums", `List (List.rev !enums));
     ("filename", `String (match files with f :: _ -> f | [] -> ""));
-    ("pragmas", `List []);
-    ("texts", `List []);
     ("machdep", machdep_to_json ());
-    ("version", `String "fcil-1.0");
+    (* 1.1 drops prog_public, pragmas and texts. All three arrived with the
+       initial import as empty lists and were never filled, so a reader could
+       only conclude that a project has no public symbols, no pragmas and no
+       texts, which is a different statement from the field not being
+       implemented. Nothing in this tree or outside it consumes the dump. *)
+    ("version", `String "fcil-1.1");
     ("files", `List (List.map (fun f -> `String f) files));
   ]

scripts/check-stdio-refusal.sh

@@ -0,0 +1,70 @@
+#!/usr/bin/env bash
+# Fail when the stdio suite hit a connect refusal that nothing diagnosed.
+#
+# The window between bind and listen is the known flake, and connect_when_listening
+# retries it. Its deadline says so in words, "frama-c never listened on <path>
+# within <timeout>: Connection refused", with both halves on one line, so the
+# qualifier is what separates the covered race from everything else. A refusal
+# without it came from a path the retry does not reach, and has to go red rather
+# than pass quietly as one more green run.
+#
+# The recovered count is the other half. A race the retry absorbs leaves no trace
+# in any tool result or exit status, so a suite drifting back toward the flake
+# looks exactly like a healthy one until the deadline is finally exceeded. That
+# needs RUST_LOG to admit warn; see the stdio step in .github/workflows/ci.yml.
+#
+# The log path arrives in the environment rather than as an argument because
+# tests/unit/repo-guards.rs keys a gate on the whole command string, and CI and
+# scripts/run-gates.sh write their logs to different places.
+#
+# A log that is absent, empty, or not a regular file is a failure and not a
+# quiet pass. Both callers run this only after the suite has run, so there is no
+# case left where nothing to scan is the right answer, and the earlier version
+# that exited 0 was a gate that could pass by not running. /dev/null is caught
+# by the same test, being a character device.
+set -euo pipefail
+
+log="${STDIO_LOG:?STDIO_LOG must name the stdio suite log}"
+
+if [ ! -f "$log" ] || [ ! -s "$log" ]; then
+    echo "no usable stdio log at $log: the suite output was not captured" >&2
+    exit 1
+fi
+
+# grep answers 0 for a match, 1 for none, and 2 or more for a failure to read.
+# Only the first two are answers. A blanket "|| true" collapses all three, so a
+# log that exists and cannot be read reports no refusal and the gate passes
+# without having scanned anything, which is the one outcome this script exists
+# to refuse.
+readable()
+{
+    [ "$1" -le 1 ] && return 0
+    echo "could not read $log: grep exited $1" >&2
+    exit "$1"
+}
+
+# Read and filter as two commands rather than one pipeline: under pipefail the
+# rightmost non-zero status wins, so the filter answering "no match" with 1
+# would hide the read answering "could not open" with 2. The filter reads a
+# here-string, which cannot fail that way, so "|| true" is right for it.
+status=0
+matches="$(grep -F 'Connection refused' "$log")" || status=$?
+readable "$status"
+
+unqualified=""
+if [ "$status" -eq 0 ]; then
+    unqualified="$(grep -Fv 'never listened' <<< "$matches" || true)"
+fi
+
+if [ -n "$unqualified" ]; then
+    echo "stdio suite hit Connection refused with no never listened diagnosis:" >&2
+    printf '%s\n' "$unqualified" >&2
+    exit 1
+fi
+
+# Same rule for the count, which is reported rather than gated on: a 0 that
+# means "could not look" reads exactly like a 0 that means "no races".
+count=0
+recovered="$(grep -cF 'connected only after the socket refused' "$log")" || count=$?
+readable "$count"
+echo "no unqualified refusal in $log; $recovered recovered bind/listen race(s)"

scripts/run-gates.sh

@@ -102,7 +102,11 @@ want corpus && run corpus scripts/check-tutorial-corpus.sh
 # 1160.81s serial against 218.42s at libtest's default, both 89/89. The default
 # is available parallelism rather than a pinned number, so a 4-core runner gets
 # 4 and this does not oversubscribe whatever machine it lands on.
-want stdio && run stdio cargo test --test test-mcp-stdio --release
+# RUST_LOG matches the stdio step in .github/workflows/ci.yml: without it the
+# recovered-race warn the check below counts is filtered out before the log.
+want stdio && run stdio env RUST_LOG=frama_c_mcp=warn cargo test --test test-mcp-stdio --release
+# Keyed on the same "want stdio", so the suite cannot be run without its check.
+want stdio && run stdio-refusal env STDIO_LOG="$logs/stdio.log" scripts/check-stdio-refusal.sh
 
 if [ "$ran" -eq 0 ]; then
     echo "no gate matched: ${selected[*]:-}" >&2

src/mcp/analysis.rs

@@ -4378,11 +4378,11 @@ impl FramaCMcpServer {
         }
 
         if order_missing {
-            let _ = tool_result_json(
-                self
-                    .compute_topological_order(Parameters(ComputeTopologicalOrderParams {}))
-                    .await?,
-            );
+            // Called for the order it computes into session state, not for what
+            // it answers. Serializing that answer only to drop it is what the
+            // tool_result_json here used to do.
+            self.compute_topological_order(Parameters(ComputeTopologicalOrderParams {}))
+                .await?;
         }
 
         let (

src/mcp/budgets.rs

@@ -33,6 +33,13 @@ pub const AST_COMPUTE_BUDGET: Duration = Duration::from_secs(120);
 /// never does.
 pub const PLUGIN_EXEC_BUDGET: Duration = Duration::from_secs(30);
 
+/// Ceiling on the wait for the self_check probe's throwaway Frama-C to start
+/// listening. Its own name rather than the tool probe budget below, which is
+/// the same number for an unrelated reason: waiting for a socket and waiting
+/// for a command to print its version are not the same wait. Quoted as well as
+/// enforced, since the give-up message names it.
+pub const PROBE_CONNECT_BUDGET: Duration = Duration::from_secs(5);
+
 /// Ceiling on an external command run only to ask what it is: frama-c -version,
 /// opam var switch, why3 config, a --help probe. A tool that cannot answer this
 /// quickly is not going to answer at all.

src/mcp/proc.rs

@@ -156,13 +156,20 @@ pub fn sandbox_kill_target(pid: u32, pgid: Option<u32>) -> Option<libc::pid_t> {
 /// reaped. Logging that at error level put one line per teardown into the log,
 /// which is how a real failure gets lost.
 ///
-/// EPERM is not in that set, measured rather than assumed: on macOS 25.6 a
-/// killpg against a group that never existed answers ESRCH, so does one against
-/// a child that has exited and been reaped, and a zombie still in its group
-/// answers success. What EPERM does mean is that the group is there and is
-/// somebody else's, which after pid reuse is a tree still running while the
-/// caller reports success. It stays visible, and process_is_alive below reads
-/// EPERM the same way.
+/// EPERM has two meanings here and the code cannot tell them apart, so it
+/// stays visible rather than picking one. The measured half stands: on macOS
+/// 25.6 a killpg against a group that never existed answers ESRCH, so does one
+/// against a child that has exited and been reaped, and a zombie still in its
+/// group answers success. What that elimination missed is the sentence macOS
+/// kill(2) adds to its own EPERM entry, "When signaling a process group, this
+/// error is returned if any members of the group could not be signaled", so a
+/// group that is entirely ours and was entirely signaled still answers EPERM
+/// when one member was mid-reap. The other meaning is the one worth seeing: a
+/// group that is somebody else's, which after pid reuse is a tree still running
+/// while the caller reports success.
+///
+/// "process_is_alive" below reads EPERM as alive for its own reason: it is
+/// asking a different question and is wrong in the safe direction.
 pub fn kill_frama_c_group(what: &str, pid: u32, pgid: Option<u32>) {
     let Some(target) = sandbox_kill_target(pid, pgid) else {
         tracing::error!(pid, "{what}: refusing to signal an unusable pid");
@@ -183,10 +190,18 @@ pub fn kill_frama_c_group(what: &str, pid: u32, pgid: Option<u32>) {
         return;
     }
     let err = std::io::Error::last_os_error();
-    if err.raw_os_error() == Some(libc::ESRCH) {
-        tracing::debug!(pid, error = %err, "{what}: no group left to signal");
-    } else {
-        tracing::error!(pid, error = %err, "{what}: could not kill the group");
+    match err.raw_os_error() {
+        Some(libc::ESRCH) => {
+            tracing::debug!(pid, error = %err, "{what}: no group left to signal");
+        }
+        Some(libc::EPERM) => {
+            tracing::error!(
+                pid,
+                error = %err,
+                "{what}: group partly signalled, or it is not ours after pid reuse"
+            );
+        }
+        _ => tracing::error!(pid, error = %err, "{what}: could not kill the group"),
     }
 }
 
@@ -245,6 +260,33 @@ pub fn socket_refused(e: &FramaCError) -> bool {
     matches!(e, FramaCError::Io(io) if io.kind() == std::io::ErrorKind::ConnectionRefused)
 }
 
+/// What a retry that absorbed a refusal says, once it connects.
+///
+/// A const rather than a literal at the one site that logs it, because
+/// scripts/check-stdio-refusal.sh counts these to report drift back toward the
+/// flake. Both strings that script reads are owned here; the other is
+/// "never_listened" below.
+pub(crate) const RECOVERED_RACE: &str =
+    "connected only after the socket refused: frama-c bound before it listened";
+
+/// The message a retry that never reached a listening server must carry.
+///
+/// One owner, because CI greps a stdio suite log for a "Connection refused" not
+/// accompanied by "never listened" and treats what is left as a bug the retry
+/// does not cover. A second site spelling this same failure its own way reads
+/// as that different bug, so the wording is a contract rather than prose. See
+/// scripts/check-stdio-refusal.sh.
+///
+/// Both arguments by Display, so neither caller allocates a String only to
+/// have it copied into the format below.
+pub(crate) fn never_listened(
+    socket: impl std::fmt::Display,
+    timeout: Duration,
+    e: impl std::fmt::Display,
+) -> String {
+    format!("frama-c never listened on {socket} within {timeout:?}: {e}")
+}
+
 /// Connect to a Frama-C that is still starting, retrying while the socket
 /// refuses connections.
 ///
@@ -290,20 +332,13 @@ pub async fn connect_when_listening(
                 // so a suite drifting toward the flake looks exactly like a
                 // healthy one until the timeout is finally exceeded.
                 if refusals > 0 {
-                    tracing::warn!(
-                        socket = %socket.display(),
-                        refusals,
-                        "connected only after the socket refused: frama-c bound before it listened"
-                    );
+                    tracing::warn!(socket = %socket.display(), refusals, "{RECOVERED_RACE}");
                 }
                 return Ok(client);
             }
             Err(e) if socket_not_listening_yet(&e) => {
                 if std::time::Instant::now() >= deadline {
-                    return Err(format!(
-                        "frama-c never listened on {} within {timeout:?}: {e}",
-                        socket.display()
-                    ));
+                    return Err(never_listened(socket.display(), timeout, &e));
                 }
                 refusals += u32::from(socket_refused(&e));
                 tokio::time::sleep(Duration::from_millis(25)).await;

src/mcp/selfcheck.rs

@@ -376,15 +376,32 @@ async fn probe_requests(
     // yet, so retry a refused connect for a few seconds. One throwaway
     // connection is not an option here: Frama-C answers its first client and
     // leaves the second waiting, which is what the batching below is about.
-    let deadline = std::time::Instant::now() + Duration::from_secs(5);
+    // Shaped like connect_when_listening, and reporting like it, because it is
+    // the same bind/listen race on a deadline 120 times shorter. It says so in
+    // the same words on the way out, since a refusal reported any other way
+    // reads as a bug the retry does not reach, and it counts absorbed refusals
+    // the same way, since a race this loop swallows is otherwise invisible to
+    // the drift count. See scripts/check-stdio-refusal.sh for both.
+    let deadline = std::time::Instant::now() + PROBE_CONNECT_BUDGET;
+    let mut refusals = 0u32;
     let mut transport = loop {
         match Transport::connect(socket_path).await {
-            Ok(transport) => break transport,
-            Err(e) if socket_not_listening_yet(&e) && std::time::Instant::now() < deadline => {
+            Ok(transport) => {
+                if refusals > 0 {
+                    tracing::warn!(socket = socket_path, refusals, "{RECOVERED_RACE}");
+                }
+                break transport;
+            }
+            Err(e) if socket_not_listening_yet(&e) => {
+                if std::time::Instant::now() >= deadline {
+                    let reason = never_listened(socket_path, PROBE_CONNECT_BUDGET, &e);
+                    return not_probed_requests(requests, &reason);
+                }
+                refusals += u32::from(socket_refused(&e));
                 tokio::time::sleep(Duration::from_millis(25)).await;
             }
             Err(e) => {
-                return not_probed_requests(requests, &format!("probe connection failed: {e}"))
+                return not_probed_requests(requests, &format!("probe connection failed: {e}"));
             }
         }
     };