From c6bf2e0803d4ea83bda580d011b921a496cb219b Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Fri, 28 Aug 2026 19:20:00 +0800 Subject: [PATCH 1/7] Drop the three F-CIL fields that were always empty "prog_public", "pragmas" and "texts" 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. --- ast-utils/src/ast_utils_export.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) 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)); ] From 7a62fb16409eba08e9e1cd818b315faf69025caf Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Fri, 28 Aug 2026 19:20:00 +0800 Subject: [PATCH 2/7] Stop building a verify_program_step value the caller drops "compute_topological_order" is called for the order it writes into session state, and "tool_result_json" then built a value from its answer that the next line discarded. --- src/mcp/analysis.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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 ( From dce936625af4a04287b89c60d921078fa06d871f Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Fri, 28 Aug 2026 19:21:24 +0800 Subject: [PATCH 3/7] Report both meanings of EPERM from killpg The comment reached one meaning by eliminating three cases measured 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. macOS kill(2) names a fourth in 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 answers EPERM when one member was mid-reap. That is what an ordinary teardown does. Both meanings are stated now and EPERM gets its own arm and its own message. No behavior change: nothing on this path retried or escalated before and nothing does now. --- src/mcp/proc.rs | 37 ++++++++++++++++++++++++++----------- 1 file changed, 26 insertions(+), 11 deletions(-) diff --git a/src/mcp/proc.rs b/src/mcp/proc.rs index 7baeae8..946e232 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"), } } From 8b021eaf1187dc7ca89bab378ebe0f7dd1f477ed Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Fri, 28 Aug 2026 19:22:29 +0800 Subject: [PATCH 4/7] Read every workflow job through one parser This file had four hand parses of "which lines name a job", and its own "step_command" comment records what that costs: three copies of one parsing rule was three chances to fix it in two places, and a drift between them put the parser gap back without any copy failing. The copies differed in which trap they fell into. Two read a comment line as a job, so a commented-out " # release:" named one. 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, which is a guard that keeps passing while it has stopped checking that job. "workflow_jobs" is the survivor and it fixes a third trap none of them had: a comment at column zero is not a key, and treating it as one ended the jobs scan and dropped every job below it. Three more parses were spelled twice and are now shared. "sorted_files" carries the directory read that "ci_command_text" and "workflow_files" both did. "all_workflow_jobs" answers "every job in every workflow" once. "flow_list" reads a YAML flow list, which had already drifted: the matrix parse strips quotes and nothing else did. The parser's own property, that it reads jobs and not the on: trigger keys sitting at the same indent, moves from a stray assertion inside the cppo guard to a test of the parser. --- tests/unit/repo-guards.rs | 282 ++++++++++++++++++++++++-------------- 1 file changed, 176 insertions(+), 106 deletions(-) diff --git a/tests/unit/repo-guards.rs b/tests/unit/repo-guards.rs index a668345..7f7dd89 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) @@ -1346,30 +1432,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 +1475,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!( From c8da9532754dfd9f2b92951a1768291c08b6e19e Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Fri, 28 Aug 2026 19:23:36 +0800 Subject: [PATCH 5/7] Fail the stdio lane on a connection refusal The bind/listen race is retried in "connect_when_listening", and its deadline says "never listened" on the same line as the io error. A "Connection refused" without that qualifier came from a path the retry does not reach, so "check-stdio-refusal.sh" fails on one. It runs from the workflow and from "run-gates.sh" under the same "want stdio", so the suite cannot run without its check, and it treats an absent, empty or unreadable log as a failure rather than as nothing to scan. grep answers 1 for no match and 2 for a failure to read, and collapsing those is how a gate passes by not running. Four things the check needed before it could mean anything. "probe_requests" reported the same race in its own words, so the guard would have gone red on the known bug. Both sites build the message through "never_listened" now, and both count absorbed refusals and warn on recovery, so a race the probe swallows is no longer invisible to the drift count. Its deadline is 120 times shorter than the spawn's, which makes it the likelier of the two to trip. The recovered race left no trace at all. It is a tracing warn against an EnvFilter that admits ERROR only when RUST_LOG is unset, so the stdio step sets it, "run-gates.sh" matches, and a guard pins the two equal: drop it from either and the script reports zero races for every run, which is what a healthy run reports. Aligning the probe's wording put it inside the allowlist, and unlike "connect_when_listening", whose message rides an Err into a failed tool call, a probe failure is only a field in a payload. A probe timeout would have turned all fifty requests into "not_probed" and gone green. The new stdio test asserts on the reason, so the by-design skips still pass. The scan runs only when the suite ran. Without the step outcome test, "!cancelled()" would also fire when an earlier failed step skipped the suite, and scanning a log nobody wrote is what forced the earlier version to tolerate a missing one. --- .github/workflows/ci.yml | 26 ++++++++++++- scripts/check-stdio-refusal.sh | 70 ++++++++++++++++++++++++++++++++++ scripts/run-gates.sh | 6 ++- src/mcp/budgets.rs | 7 ++++ src/mcp/proc.rs | 38 +++++++++++++----- src/mcp/selfcheck.rs | 25 ++++++++++-- tests/test-mcp-stdio.rs | 57 +++++++++++++++++++++++++++ tests/unit/repo-guards.rs | 40 +++++++++++++++++++ 8 files changed, 254 insertions(+), 15 deletions(-) create mode 100755 scripts/check-stdio-refusal.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c4c2d3c..0409275 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -125,6 +125,7 @@ jobs: persist-credentials: false - run: scripts/check-artifacts.sh + # 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 +252,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/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/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 946e232..ad5becc 100644 --- a/src/mcp/proc.rs +++ b/src/mcp/proc.rs @@ -260,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. /// @@ -305,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 7f7dd89..f551210 100644 --- a/tests/unit/repo-guards.rs +++ b/tests/unit/repo-guards.rs @@ -1250,6 +1250,46 @@ fn gate_of(command: &str) -> Option { words.next().is_none_or(|word| word.starts_with('-')).then_some(gate) } +/// 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 From 5f0905e8e44f74f7be0c3ca22366b426d8158088 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Fri, 28 Aug 2026 19:24:12 +0800 Subject: [PATCH 6/7] Scan dependencies for advisories "checks: write" is scoped to artifact-scans alone, the way release scopes "contents: write", because the action reports by creating a check run and the workflow floor is "contents: read". Skipped on pull requests from forks, where GitHub caps the token at read-only whatever the block says, so the action fails there on a clean tree; a dependency arriving that way is still scanned on the push that merges it. Deliberately not in "run-gates.sh": its verdict comes from a database that moves on its own rather than from the tree, so the same commit can pass today and fail tomorrow. That also puts it outside every existing guard, since "gate_of" reads cargo commands and "scripts/" paths and not "uses:" steps, so a guard pins the action and its permission together. Checking them separately would let the permission move to any other job while the guard stayed green. --- .github/workflows/ci.yml | 40 +++++++++++++++++++++++++----- tests/unit/repo-guards.rs | 52 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 86 insertions(+), 6 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 0409275..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,47 @@ 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. diff --git a/tests/unit/repo-guards.rs b/tests/unit/repo-guards.rs index f551210..80881d3 100644 --- a/tests/unit/repo-guards.rs +++ b/tests/unit/repo-guards.rs @@ -1250,6 +1250,58 @@ 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() + ); +} + /// 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 From b8d9b02bae3dbb465598151827b3a74dfcc33ae4 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Fri, 28 Aug 2026 19:24:47 +0800 Subject: [PATCH 7/7] Fail when a lane does not gate 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. 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. --- tests/unit/repo-guards.rs | 59 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 59 insertions(+) diff --git a/tests/unit/repo-guards.rs b/tests/unit/repo-guards.rs index 80881d3..826be60 100644 --- a/tests/unit/repo-guards.rs +++ b/tests/unit/repo-guards.rs @@ -1302,6 +1302,65 @@ fn ci_still_scans_dependencies_for_advisories() { ); } +/// 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