diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c4c2d3c..61be6f6 100644 --- a/.github/workflows/ci.yml +++ b/.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, diff --git a/ast-utils/src/ast_utils_export.ml b/ast-utils/src/ast_utils_export.ml index 5e649a9..84fb879 100644 --- a/ast-utils/src/ast_utils_export.ml +++ b/ast-utils/src/ast_utils_export.ml @@ -1508,7 +1508,6 @@ 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); @@ -1516,9 +1515,12 @@ let dump_project () : Yojson.Basic.t = ("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)); ] diff --git a/scripts/check-stdio-refusal.sh b/scripts/check-stdio-refusal.sh new file mode 100755 index 0000000..f36d6b0 --- /dev/null +++ b/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 +# within : 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)" diff --git a/scripts/run-gates.sh b/scripts/run-gates.sh index 467372b..da5c45a 100755 --- a/scripts/run-gates.sh +++ b/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 diff --git a/src/mcp/analysis.rs b/src/mcp/analysis.rs index 36d6903..4d21172 100644 --- a/src/mcp/analysis.rs +++ b/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 ( diff --git a/src/mcp/budgets.rs b/src/mcp/budgets.rs index 82b4445..80200ae 100644 --- a/src/mcp/budgets.rs +++ b/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. diff --git a/src/mcp/proc.rs b/src/mcp/proc.rs index 7baeae8..ad5becc 100644 --- a/src/mcp/proc.rs +++ b/src/mcp/proc.rs @@ -156,13 +156,20 @@ pub fn sandbox_kill_target(pid: u32, pgid: Option) -> Option { /// 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) { 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) { 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; diff --git a/src/mcp/selfcheck.rs b/src/mcp/selfcheck.rs index b852d9b..2e14222 100644 --- a/src/mcp/selfcheck.rs +++ b/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}")); } } }; diff --git a/tests/test-mcp-stdio.rs b/tests/test-mcp-stdio.rs index 2d50340..dabf441 100644 --- a/tests/test-mcp-stdio.rs +++ b/tests/test-mcp-stdio.rs @@ -6641,6 +6641,63 @@ async fn self_check_canary_judges_the_backend_without_disturbing_the_session() { let _ = client.cancel().await; } +/// self_check reached its probe, rather than reporting every request unprobed. +/// +/// The probe's give-up now says "never listened", which is the wording +/// scripts/check-stdio-refusal.sh reads as a diagnosed bind/listen race and +/// filters out of its search for an unexplained refusal. That is right for +/// connect_when_listening, whose message rides an Err into a failed tool call +/// and reddens whichever test produced it. It is not right here, because an +/// unreached probe is only a field in a payload: a probe that timed out under +/// the parallel suite turned every request into not_probed, the tripwire +/// filtered the line, and nothing at all went red. +/// +/// Asserted on the reason and not the status, because not_probed is also the +/// honest answer for the requests self_check deliberately does not call. Those +/// carry one fixed reason; every other reason means the probe could not run and +/// the report says nothing about the plugin. +#[tokio::test] +async fn self_check_probes_rather_than_reporting_every_request_unprobed() { + let tmp = tempfile::tempdir().expect("tempdir"); + let c_file = tmp.path().join("probe-target.c"); + std::fs::write(&c_file, "int id(int x)\n{\n return x;\n}\n").expect("write fixture"); + let client = spawn_mcp_client(c_file.to_str().unwrap()).await; + + let report = call_tool_json(&client, "self_check", json!({})).await.unwrap(); + + for field in ["required_requests", "ast_utils_registered_requests"] { + let requests = report[field] + .as_array() + .unwrap_or_else(|| panic!("{field} is not an array: {report}")); + + // An empty array would satisfy the loop below without checking anything, + // which is the shape of a guard that passes by not running. + assert!(!requests.is_empty(), "{field} is empty: {report}"); + + let undone: Vec<&Value> = requests + .iter() + .filter(|request| { + request["status"] == "not_probed" + && request["reason"] != "not a public MCP dependency" + }) + .collect(); + + // One entry and a count, not the vector. A probe that could not connect + // fails every request with one reason, and printing fifty copies of it + // buries the reason that is the whole diagnosis. + assert!( + undone.is_empty(), + "{field}: self_check could not probe {} of {} requests, so its report \ + describes nothing. First: {}", + undone.len(), + requests.len(), + undone[0] + ); + } + + let _ = client.cancel().await; +} + /// A prover timeout is reported as a timeout, distinct from a goal WP could /// not prove. /// diff --git a/tests/unit/repo-guards.rs b/tests/unit/repo-guards.rs index a668345..826be60 100644 --- a/tests/unit/repo-guards.rs +++ b/tests/unit/repo-guards.rs @@ -476,20 +476,7 @@ fn ci_command_text(root: &std::path::Path) -> String { let mut text = String::new(); for dir in [".github/workflows", ".ci"] { let dir = root.join(dir); - let mut paths: Vec = std::fs::read_dir(&dir) - .unwrap_or_else(|error| panic!("{}: {error}", dir.display())) - .flatten() - .map(|entry| entry.path()) - .filter(|path| { - path.extension() - .is_some_and(|ext| ext == "yml" || ext == "yaml" || ext == "sh") - }) - .collect(); - - // read_dir order is arbitrary, and a guard that reports what it found - // is read by a human. - paths.sort(); - for path in paths { + for path in sorted_files(&dir, &["yml", "yaml", "sh"]) { text.push_str(&std::fs::read_to_string(&path).unwrap_or_default()); text.push('\n'); } @@ -503,6 +490,144 @@ fn ci_command_text(root: &std::path::Path) -> String { text } +/// Every file in a directory with one of these extensions, sorted. +/// +/// read_dir order is arbitrary and a guard that reports what it found is read +/// by a human, so the sort is part of the contract rather than a nicety. +fn sorted_files(dir: &std::path::Path, exts: &[&str]) -> Vec { + let mut paths: Vec = std::fs::read_dir(dir) + .unwrap_or_else(|error| panic!("{}: {error}", dir.display())) + .flatten() + .map(|entry| entry.path()) + .filter(|path| { + path.extension().is_some_and(|ext| exts.iter().any(|want| ext == *want)) + }) + .collect(); + paths.sort(); + paths +} + +/// Every workflow file, sorted. +/// +/// The directory rather than ci.yml by name, which is the lesson ci_command_text +/// above records: the artifact scan once lived in a second workflow file and a +/// guard reading one file by name reported all clear having compared nothing. +fn workflow_files(root: &std::path::Path) -> Vec { + let dir = root.join(".github/workflows"); + let paths = sorted_files(&dir, &["yml", "yaml"]); + assert!(!paths.is_empty(), "{}: no workflow files", dir.display()); + paths +} + +/// Every job in every workflow, with the file each came from. +/// +/// The two guards that ask "which job does X" both want this, and spelling it +/// twice was two shapes for one question in a single commit. +fn all_workflow_jobs(root: &std::path::Path) -> Vec<(std::path::PathBuf, String, String)> { + workflow_files(root) + .into_iter() + .flat_map(|path| { + let text = std::fs::read_to_string(&path).unwrap_or_default(); + workflow_jobs(&text).into_iter().map(move |(name, body)| (path.clone(), name, body)) + }) + .collect() +} + +/// The entries of a YAML flow list, "[a, b]", unquoted. +/// +/// Two guards parse one of these and they had drifted before they were two +/// days old: the matrix parse strips quotes and the needs parse did not, so a +/// needs written ["build"] would have compared a quoted name against a bare one +/// and reported every job as ungating. +fn flow_list(text: &str) -> Vec { + let Some(inner) = text.split_once('[').and_then(|(_, rest)| rest.split_once(']')) else { + return Vec::new(); + }; + inner + .0 + .split(',') + .map(|entry| entry.trim().trim_matches('"').trim_matches('\'').to_string()) + .filter(|entry| !entry.is_empty()) + .collect() +} + +/// A workflow's jobs, as name and body. +/// +/// One definition, for the reason step_command below records: three copies of +/// one parsing rule was three chances to fix it in two places. This file had +/// four copies of this one by 2026-08-28, and every caller now goes through +/// this one. The copies differed in which trap they fell into: two read a +/// comment line as a job, so " # release:" named one, and two tested the raw +/// line for a closing colon, so a header carrying a trailing comment stopped +/// being a header and its job merged into the one above it. +/// +/// Only inside the jobs: mapping. Indentation alone cannot say what a job is: +/// the on: trigger keys push: and pull_request: sit at the same two spaces, so +/// a scan without that check collected them as jobs and gave the first one the +/// whole top-of-file comment block as its body. Harmless while that comment +/// says nothing a caller greps for, and a trap the day it does. +fn workflow_jobs(text: &str) -> Vec<(String, String)> { + let mut jobs: Vec<(String, String)> = Vec::new(); + let mut in_jobs = false; + for line in text.lines() { + // Before the column test, not after: a comment at column zero is not a + // key, and treating it as one ended the scan and dropped every job + // below it. ci.yml has no such comment today, which is the only reason + // nothing failed. + if line.trim_start().starts_with('#') { + continue; + } + if !line.starts_with(' ') && !line.trim().is_empty() { + in_jobs = line.trim_end() == "jobs:"; + continue; + } + if !in_jobs { + continue; + } + // A trailing comment does not stop a line from naming a job, and YAML + // allows one. Testing the raw line for a closing colon made + // " build: # note" fail the test, which merged that job into its + // predecessor and let a caller searching one body read two jobs as one. + // Found by a control that added such a comment; the guard it broke was + // failing green. + let header = match line.split_once(" #") { + Some((before, _)) => before, + None => line, + } + .trim_end(); + let is_job_header = + line.starts_with(" ") && !line.starts_with(" ") && header.ends_with(':'); + if is_job_header { + jobs.push((header.trim().trim_end_matches(':').to_string(), String::new())); + } else if let Some((_, body)) = jobs.last_mut() { + body.push_str(line); + body.push('\n'); + } + } + jobs +} + +/// workflow_jobs reads jobs, and reads nothing else as one. +/// +/// The property lived as a stray assertion inside the cppo guard, which is +/// where the parser used to be inlined. It belongs to the parser: the on: +/// trigger keys push: and pull_request: sit at the same two spaces a job name +/// does, so a scan that does not track the jobs: mapping collects them, and a +/// caller then greps a body that is really the top-of-file comment block. +#[test] +fn workflow_jobs_reads_jobs_and_not_trigger_keys() { + let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR")); + let jobs = all_workflow_jobs(root); + + assert!(!jobs.is_empty(), "no workflow job was read, so this guard compared nothing"); + let stray: Vec<&String> = jobs + .iter() + .map(|(_, name, _)| name) + .filter(|name| ["push", "pull_request", "schedule", "workflow_dispatch"].contains(&name.as_str())) + .collect(); + assert!(stray.is_empty(), "the job scan collected an on: trigger key as a job: {stray:?}"); +} + /// The command a workflow step runs, or the line unchanged when it runs none. /// /// A step is either "run: " on one line or a command inside a @@ -730,12 +855,8 @@ fn ci_frama_c_version_matches_supported_minimum() { let matrix: Vec = workflow .lines() - .filter_map(|line| line.trim().strip_prefix("frama-c-version:")) - .flat_map(|list| { - list.trim().trim_start_matches('[').trim_end_matches(']').split(',') - }) - .map(|entry| entry.trim().trim_matches('"').to_string()) - .filter(|entry| !entry.is_empty()) + .filter(|line| line.trim().starts_with("frama-c-version:")) + .flat_map(flow_list) .collect(); assert!( @@ -853,49 +974,14 @@ fn ci_builds_the_plugin_on_the_supported_floor() { // "opam install" and for "cppo" separately is satisfied by a cache key, a // step name, or a comment, and even requiring both on one line is satisfied // by whichever other lane still installs it. - let ci = std::fs::read_to_string(root.join(".github/workflows/ci.yml")).expect("ci.yml"); - let mut jobs: Vec<(String, String)> = Vec::new(); - - // Only inside the jobs: block. Indentation alone cannot say what a job is: - // the on: trigger keys push: and pull_request: sit at the same two spaces, - // so a scan without this collected them as jobs and gave the first one the - // whole top-of-file comment block as its body. Harmless while that comment - // says nothing about dune, and a trap the day it does. - let mut in_jobs = false; - for line in ci.lines() { - if !line.starts_with(' ') && !line.trim().is_empty() { - in_jobs = line.trim_end() == "jobs:"; - continue; - } - if !in_jobs { - continue; - } - let is_job_header = line.starts_with(" ") - && !line.starts_with(" ") - && line.trim_end().ends_with(':') - && !line.trim_start().starts_with('#'); - if is_job_header { - jobs.push((line.trim().trim_end_matches(':').to_string(), String::new())); - } else if let Some((_, body)) = jobs.last_mut() { - body.push_str(line); - body.push('\n'); - } - } - assert!( - jobs.iter().all(|(name, _)| name != "push" && name != "pull_request"), - "the job scan collected an on: trigger key as a job: {:?}", - jobs.iter().map(|(name, _)| name).collect::>() - ); - - let plugin_builders: Vec<&(String, String)> = jobs - .iter() - .filter(|(_, body)| body.contains("dune build")) - .collect(); + let jobs = all_workflow_jobs(root); + let plugin_builders: Vec<&(std::path::PathBuf, String, String)> = + jobs.iter().filter(|(_, _, body)| body.contains("dune build")).collect(); assert!( !plugin_builders.is_empty(), "no ci.yml job runs dune build, so this guard compared nothing" ); - for (name, body) in plugin_builders { + for (_, name, body) in plugin_builders { assert!( body.lines() .map(str::trim) @@ -1164,6 +1250,157 @@ fn gate_of(command: &str) -> Option { words.next().is_none_or(|word| word.starts_with('-')).then_some(gate) } +/// The dependency advisory scan is still in a workflow, with the permission it +/// needs. +/// +/// gate_of below recognises a cargo command or a scripts/ path, so this one is +/// invisible to every guard around it: it is a uses: step, and it is the one +/// check deliberately absent from scripts/run-gates.sh because its verdict +/// comes from a database rather than from the tree. Nothing would fail if it +/// were deleted, which is the shape this file already has four guards for. +/// +/// The permission is checked inside the job that runs the action, because the +/// two are one thing. The action reports by creating a check run and the +/// workflow floor is contents: read, so the job running it needs checks: write +/// of its own. Asserting the two independently over the whole file was the +/// first version and it did not say that: the permission could move to any +/// other job, or to a job that runs nothing, and the guard stayed green while +/// the step lost what it needs. +#[test] +fn ci_still_scans_dependencies_for_advisories() { + let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR")); + + // A line predicate rather than a rewritten body, and comment blindness only + // where it is needed. documented_gate_list_covers_ci reads a fenced block + // rather than a whole document for the same reason: the comment above the + // permissions block explains why artifact-scans grants checks: write, so a + // whole-text search left the guard green with the permission deleted. The + // permission test below needs no such care, since a comment line cannot + // equal "checks: write" once trimmed. + let runs = |body: &String, needle: &str| { + body.lines().any(|line| !line.trim_start().starts_with('#') && line.contains(needle)) + }; + + let jobs = all_workflow_jobs(root); + let scanning: Vec<&(std::path::PathBuf, String, String)> = + jobs.iter().filter(|(_, _, body)| runs(body, "rustsec/audit-check@")).collect(); + assert_eq!( + scanning.len(), + 1, + "expected exactly one job to run an advisory scan, found these. None means \ + a vulnerable dependency lands green: {:?}", + scanning.iter().map(|(_, name, _)| name).collect::>() + ); + + let (path, name, body) = scanning[0]; + assert!( + body.lines().any(|line| line.trim() == "checks: write"), + "{}: job {name} runs the advisory action and does not grant itself \ + checks: write. The workflow floor is contents: read, so the action \ + cannot create the check run it reports through:\n{body}", + path.display() + ); +} + +/// Every lane gates the release. +/// +/// A job that runs and is not among the release job's needs can be red while +/// the rolling tag is republished, which is a green badge over a binary nothing +/// vouched for. Measured on 2026-08-28: release needs five jobs while CLAUDE.md +/// described four, having dropped plugin-floor, so the document did not say that +/// a Frama-C 32.1 build failure blocks a release. No guard can read that +/// document, since it is never checked in, so this pins the fact rather than the +/// prose. +/// +/// A job that deliberately does not gate a release will fail here. That is the +/// intent: it is a decision worth writing down rather than one worth inferring +/// from an absence. +#[test] +fn the_release_waits_for_every_lane() { + let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR")); + + let jobs = all_workflow_jobs(root); + + // The release job's own needs, read out of its body, so a needs belonging + // to some other job cannot stand in for the one being checked. + let releases: Vec<&(std::path::PathBuf, String, String)> = + jobs.iter().filter(|(_, name, _)| name == "release").collect(); + assert_eq!( + releases.len(), + 1, + "expected exactly one release job across the workflows, found {}", + releases.len() + ); + let (path, _, release) = releases[0]; + + let needs = release + .lines() + .find(|line| line.trim_start().starts_with("needs:")) + .unwrap_or_else(|| panic!("{}: the release job declares no needs", path.display())); + let listed = flow_list(needs); + assert!( + !listed.is_empty(), + "{}: the release needs is empty or not a flow list, so this guard \ + compared nothing: {needs}", + path.display() + ); + + let ungating: Vec<&String> = jobs + .iter() + .filter(|(job_path, name, _)| { + job_path == path && name != "release" && !listed.contains(name) + }) + .map(|(_, name, _)| name) + .collect(); + assert!( + ungating.is_empty(), + "{}: these jobs run and the release does not wait for them, so each can \ + be red while the rolling tag is republished: {ungating:?}. Add them to \ + needs, or record why they do not gate a release", + path.display() + ); +} + +/// The stdio suite runs under the same RUST_LOG in CI and in the runner. +/// +/// src/main.rs builds its subscriber from the environment, and EnvFilter admits +/// ERROR only when RUST_LOG is unset, so the recovered-race warn that +/// scripts/check-stdio-refusal.sh counts exists only when this variable is set. +/// Drop it from either caller and the script prints "0 recovered" for every run, +/// which is exactly what a healthy run prints. That is the silent-drift shape +/// this file already has several tests about, and it arrived with the two +/// callers rather than by drift between them. +#[test] +fn the_stdio_suite_runs_under_one_log_level() { + let root = std::path::Path::new(env!("CARGO_MANIFEST_DIR")); + const DIRECTIVE: &str = "RUST_LOG: frama_c_mcp=warn"; + const RUNNER: &str = "RUST_LOG=frama_c_mcp=warn"; + + let stdio: Vec<(std::path::PathBuf, String, String)> = all_workflow_jobs(root) + .into_iter() + .filter(|(_, _, body)| body.contains("--test test-mcp-stdio")) + .collect(); + assert_eq!(stdio.len(), 1, "expected one job to run the stdio suite, found {}", stdio.len()); + assert!( + stdio[0].2.lines().any(|line| line.trim() == DIRECTIVE), + "the workflow job running the stdio suite does not set {DIRECTIVE}, so its \ + log carries no recovered-race warn and check-stdio-refusal.sh reports \ + zero for every run" + ); + + let runner = + std::fs::read_to_string(root.join("scripts/run-gates.sh")).expect("run-gates.sh"); + assert!( + runner.lines().any(|line| { + line.trim_start().starts_with("want stdio") + && line.contains(RUNNER) + && line.contains("--test test-mcp-stdio") + }), + "scripts/run-gates.sh runs the stdio suite without {RUNNER}, so a local run \ + cannot reproduce what CI scans" + ); +} + /// scripts/run-gates.sh runs every gate CI runs. /// /// The runner is what the documents send a person to, so a gate CI has and the @@ -1346,30 +1583,42 @@ fn jobs_running_repo_scripts_check_out_the_repo() { let mut offenders = Vec::new(); let mut checked = 0; - for entry in std::fs::read_dir(root.join(".github/workflows")) - .expect("workflows dir") - .flatten() - { - let path = entry.path(); - if !path.extension().is_some_and(|ext| ext == "yml" || ext == "yaml") { - continue; - } + for path in workflow_files(root) { let workflow = std::fs::read_to_string(&path).unwrap_or_default(); - // Jobs are the keys at one indent level under "jobs:", and steps run in - // file order, so a linear scan is enough to know whether the checkout + // Steps run in file order and workflow_jobs keeps a body in that order, + // so a linear scan of each body is enough to know whether the checkout // came first. A YAML parser would be better and is not worth a - // dependency for five jobs. - let mut job = String::new(); - let mut checkout_at = None; - let mut runs_repo_script = false; - let mut step = 0usize; - let mut finish = |job: &str, checkout: Option, runs: bool| { - if !runs { - return; + // dependency for six jobs. + for (job, body) in workflow_jobs(&workflow) { + let mut checkout_at = None; + let mut runs_repo_script = false; + let mut step = 0usize; + + for line in body.lines() { + let indent = line.len() - line.trim_start().len(); + let trimmed = line.trim(); + + // Steps sit at six spaces. Counting every "- " would also count + // the build matrix's include entries, which are not steps. + if indent == 6 && trimmed.starts_with("- ") { + step += 1; + } + if trimmed.contains("actions/checkout") && checkout_at.is_none() { + checkout_at = Some(step); + } + if (trimmed.contains(".ci/") || trimmed.contains("scripts/")) + && !trimmed.starts_with('#') + { + runs_repo_script = true; + } + } + + if !runs_repo_script { + continue; } checked += 1; - match checkout { + match checkout_at { Some(1) => {} Some(at) => offenders.push(format!( "{job}: checks out at step {at} rather than first, so an earlier \ @@ -1377,35 +1626,7 @@ fn jobs_running_repo_scripts_check_out_the_repo() { )), None => offenders.push(format!("{job}: runs a repo script with no checkout")), } - }; - - for line in workflow.lines() { - let indent = line.len() - line.trim_start().len(); - let trimmed = line.trim(); - - // A key at two spaces, inside jobs, is a new job. - if indent == 2 && trimmed.ends_with(':') && !trimmed.starts_with('#') { - finish(&job, checkout_at, runs_repo_script); - job = trimmed.trim_end_matches(':').to_string(); - (checkout_at, runs_repo_script, step) = (None, false, 0); - continue; - } - - // Steps sit at six spaces. Counting every "- " would also count the - // build matrix's include entries, which are not steps. - if indent == 6 && trimmed.starts_with("- ") { - step += 1; - } - if trimmed.contains("actions/checkout") && checkout_at.is_none() { - checkout_at = Some(step); - } - if (trimmed.contains(".ci/") || trimmed.contains("scripts/")) - && !trimmed.starts_with('#') - { - runs_repo_script = true; - } } - finish(&job, checkout_at, runs_repo_script); } assert!(