From 8993631f76ad4b0709ac577bc3f80fa0627d5379 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Sat, 15 Aug 2026 00:25:43 +0800 Subject: [PATCH] Run only the CI a pull request can affect Every pull request paid for every workflow whatever it touched: seventeen macOS runners proving seventeen targets, three more analyzing a build, one building and testing, for a branch that edited a test script. The proofs are the bulk of that, and a target whose inputs a branch does not touch already has the verdict the base established. scripts/proof-scope.py decides which proof targets a set of changed files can reach. It takes each proved source's include closure from the compiler's own -MM, preprocessed with that target's VERIFY__CPP_DEFS and unioned with its VERIFY__SCAN list, so the scan sees what the prover sees. Inputs no closure can see widen the scope to everything: the makefiles, the checkers the recipes run, the Frama-C stub headers, the workflow itself. So does every "cannot tell" answer, whether an unresolvable base ref or a compiler scan that cannot be trusted. Narrowing on a guess turns a speed-up into a correctness problem; proving something twice does not. verify.yml asks that twice. Which targets to prove is one question; which mutation sets to re-run is the other, and it is narrower, because a file that only decides what runs cannot change whether a target rejects a broken source. SCHEDULING_FILES names those files, everything else counts as judging so an unclassified newcomer widens both, and the self-test refuses a scheduling workflow that carries a prover budget or a make invocation. An empty scope is a verdict rather than a failure. A push to main and a merge queue run prove and mutate everything, so the guarantee on the branch a pull request merges into is never the narrowed one. The jobs follow the same shape. A mutation leg proves an unmutated control through the very rule the proofs use, so the proving job takes only what the matrix will not cover, which over the last 400 commits is nothing at all: sharding the proofs cost 82 seconds of setup per leg to do 23 seconds of proving. Both halves report under the check name that predates the split, which covered proofs and mutations together and still does, and check-proof-targets.py now asserts every macOS job is reachable from it. The setup those jobs share, and the toolchain pins they have to agree on, live in .github/actions/framac; the analyzer moves to Frama-C 33.0, checked rather than assumed, at 803 of 803 obligations across all 17 targets with the mutation gate still biting. build.yml and static-analysis.yml take the cheaper mechanism their inputs allow, a paths-ignore list of what cannot reach them, on pull_request only so there is one list per file and nothing can drift. The analysis jobs analyze "make elfuse" and nothing else, which is why tests/ is inert for them. The failure directions differ from the proof scoping, and that is why one needs a self-test and the other does not: a stale entry there matches nothing and the workflow runs more, while a stale harness entry widens nothing and the proofs run less. lint.yml loses its path filter entirely, which is what makes it the place the self-test can live. It had been ignoring markdown, and check-skill-refs.py validates nothing but the markdown under .claude, which the other two workflows treat as inert, so a documentation-only pull request ran no CI at all. That checker was also wired into no workflow until now, and it failed on its first run, naming two files the CI split had already removed. lint.yml runs its package-free checks first and carries if !cancelled() on every step, the apt setup included, so one failure reports alongside the rest instead of leaving the tool-dependent checks to fail on a missing binary. verify-mk.py refuses a VERIFY__SRC naming two sources rather than keeping the first, since every consumer assumes one, and check-char-signedness.py, the last reader with its own regex over those lines, goes through the shared table now. Two harness entries answer a question about content rather than about the path, because the name rule was measurably too blunt: over the last 400 commits the top-level Makefile was the sole reason 36 of the 60 full-scope runs happened, every one of them a rule for a test binary or a source added to SRCS. It reaches a proof only through its include lines, since it defines none of the variables the verify recipe reads, and mk/config.mk qualifies the same way because it defines no rules at all. mk/common.mk does not: it owns the $(BUILD_DIR) rule every verify target carries as an order-only prerequisite, which a slicer reading values cannot see. That slicer drops what is provably inert rather than keeping what it recognizes, so an unrecognized construct widens. Reviewers found the difference the hard way: sorting the slice hid a reordered include, and override, define, a target-specific assignment, vpath and unexport each reached a proof while every line an earlier pattern read stayed byte-identical. All of them are self-test cases now, alongside the conditions the approach rests on, that neither file defines a verify rule or a target the verify rules depend on. Which names count as proof-relevant is a fixpoint, not a union: start from what mk/verify.mk expands, since that is the only file the recipe reads, then follow definitions. The union was self-defeating, because mk/config.mk references its own test lists, so NATIVE_TESTS and its neighbours counted and any edit to them re-proved everything. The seed still takes references outside an assignment's right-hand side in the other three makefiles, or mk/common.mk's "ifeq ($(V),1)", which picks the Q every recipe expands, would leave V inert. Over the same 400 commits: 231 run no proof at all, 16 run the full set, and the targets mutated fall from 1103 to 374. The data model comment was wrong where it mattered most. It claimed plain char is unsigned on arm64 macOS; it is signed there, and unsigned on aarch64-linux, which is the cross toolchain for the guest tests, both answers taken from the compilers rather than from memory. So gcc_x86_64 matches the platform the proved sources compile for on all four properties, not three. Frama-C 33 does ship a macos_arm machdep and it cannot be used here: it is not GCC-based, and the atomics stub pulls in Frama-C's __fc_gcc_builtins.h, which refuses __int128 outside a GCC-based machdep. Every target aborts at parse time, which is now the recorded reason for the pin. The mutation matrix is packed rather than one leg per target. A leg spends about 90 seconds on Homebrew and the opam switch before it proves anything, and GitHub bills wall time rounded up to the minute, so 17 legs cost 85 macOS-minutes where 5 buckets cost 61; five also fits one concurrency wave, so the wall clock improves too. check-mutants.py packs because it owns the mutation counts it packs by, and each leg still runs one target at a time so a failure names the target rather than the group. Three defects in this machinery came out of review rather than out of the self-test, and all three are now cases in it. A "printf | grep -q" under pipefail reports "unchanged" once the diff fills the pipe buffer, which would have skipped clang-format and cppcheck on exactly the largest pull requests. check-mutants.py was taking its source table through proof-scope.py, putting a file classified as unable to affect a mutation verdict on the path that decides which file gets mutated. And check-proof-targets.py's job splitter read workflow sub-keys as jobs while missing any job id not starting lowercase, so the check meant to notice a prover job leaving the required check could not see one. --- .ci/check-security.sh | 31 +- .claude/skills/elfuse-verify/SKILL.md | 30 +- .github/actions/framac/action.yml | 111 +++ .github/workflows/build.yml | 47 +- .github/workflows/lint.yml | 174 ++++- .github/workflows/static-analysis.yml | 28 +- .github/workflows/verify.yml | 407 ++++++----- mk/verify.mk | 61 +- scripts/check-char-signedness.py | 29 +- scripts/check-mutants.py | 296 +++----- scripts/check-proof-targets.py | 88 ++- scripts/check-skill-refs.py | 12 +- scripts/proof-scope.py | 928 ++++++++++++++++++++++++++ scripts/verify-mk.py | 174 ++++- src/syscall/asyncio.c | 20 +- 15 files changed, 1967 insertions(+), 469 deletions(-) create mode 100644 .github/actions/framac/action.yml create mode 100755 scripts/proof-scope.py diff --git a/.ci/check-security.sh b/.ci/check-security.sh index 9b3522d8..9a55c6e7 100755 --- a/.ci/check-security.sh +++ b/.ci/check-security.sh @@ -1,30 +1,38 @@ #!/usr/bin/env bash -# Security checks for elfuse host source files (src/ only). -# Tests are excluded -- they exercise unsafe patterns deliberately. +# Security checks for elfuse host source files (src/ only). Tests are excluded +# -- they exercise unsafe patterns deliberately. # # 1. Banned functions -- unsafe libc calls with safer alternatives. # 2. Credential / secret patterns -- catch accidental key leaks. # 3. Dangerous preprocessor -- detect disabled security features. +# 4. Agent scratch markers -- labels a tool emits to flag a deliberate +# simplification. The rationale behind one is often worth keeping; the +# label is not, because it reads as a machine's note rather than the +# author's, and nothing else in the tree notices when one survives. set -u -o pipefail failed=0 -# --- Patterns --- +# Patterns banned='(^|[^[:alnum:]_])(gets|sprintf|vsprintf|strcpy|stpcpy|strcat|atoi|atol|atoll|atof|mktemp|tmpnam|tempnam)[[:space:]]*\(' secrets='(password|secret|api_key|private_key|token)[[:space:]]*=[[:space:]]*"[^"]+' dangerous_pp='#[[:space:]]*(undef|define)[[:space:]]+((_FORTIFY_SOURCE[[:space:]]+0)|(__SSP__))' comment_only='^[[:space:]]*(//|/\*|\*|\*/)' +# Matched against comments too, unlike the three above, since that is the only +# place this appears. +scratch_marker='(^|[^[:alnum:]_])ponytail:' + # Only scan elfuse host source, not tests/ or assembly shim. # -# Each match uses process substitution rather than a shell pipeline: -# under `pipefail`, an early `grep -q` exit closes its stdin, the -# upstream filter receives SIGPIPE, and the pipeline returns non-zero -# even when the pattern matched -- silently dropping real findings. -# Process substitution puts the filter in a separate process whose exit -# status doesn't feed back into the matcher. +# Each match uses process substitution rather than a shell pipeline: under +# `pipefail`, an early `grep -q` exit closes its stdin, the upstream filter +# receives SIGPIPE, and the pipeline returns non-zero even when the pattern +# matched -- silently dropping real findings. Process substitution puts the +# filter in a separate process whose exit status doesn't feed back into the +# matcher. while IFS= read -r -d '' f; do if grep -qE "$banned" < <(grep -vE "$comment_only" -- "$f"); then echo "Banned function in $f:" @@ -41,6 +49,11 @@ while IFS= read -r -d '' f; do grep -nE "$dangerous_pp" -- "$f" | grep -vE "$comment_only" || true failed=1 fi + if grep -qE "$scratch_marker" -- "$f"; then + echo "Agent scratch marker in $f (keep the reasoning, drop the label):" + grep -nE "$scratch_marker" -- "$f" || true + failed=1 + fi done < <(git ls-files -z -- 'src/*.c' 'src/*.h' 'src/**/*.c' 'src/**/*.h') if [ $failed -eq 0 ]; then diff --git a/.claude/skills/elfuse-verify/SKILL.md b/.claude/skills/elfuse-verify/SKILL.md index faf5016f..d2c8011c 100644 --- a/.claude/skills/elfuse-verify/SKILL.md +++ b/.claude/skills/elfuse-verify/SKILL.md @@ -1,6 +1,6 @@ --- name: elfuse-verify -description: How elfuse validates a change - choosing the lanes for the area you touched, the test matrix, make check, and the Frama-C proof targets declared in mk/analysis.mk, including how to drive the frama-c MCP server on a stuck proof. Use when adding bounds math to src/proved/, writing or repairing ACSL contracts, running or debugging make verify / verify-mutants, touching frama-c-stubs/, adding a test lane, or deciding what to run before calling work done. +description: How elfuse validates a change - choosing the lanes for the area you touched, the test matrix, make check, and the Frama-C proof targets declared in mk/verify.mk, including how to drive the frama-c MCP server on a stuck proof. Use when adding bounds math to src/proved/, writing or repairing ACSL contracts, running or debugging make verify / verify-mutants, touching frama-c-stubs/, adding a test lane, or deciding what to run before calling work done. --- # Validating an elfuse change @@ -63,7 +63,7 @@ with `-wp-rte`. Every `src/proved/` header must have a matching `make verify-` target, but the reverse does not hold. A few targets prove a `.c` file directly, each -for a reason stated in the comment above it in `mk/analysis.mk`; the general +for a reason stated in the comment above it in `mk/verify.mk`; the general one is that the loops in question could only have been described as test-covered had they been split into a header. @@ -85,17 +85,33 @@ Apple's 3.81. `verify-mutants` accepts `MUTANT_TARGET=`, `MUTANT_JOBS=`, and `MUTANT_SINCE=` for a changed-only run. +`scripts/proof-scope.py` decides which targets a diff can reach, and +`.github/workflows/verify.yml` builds its jobs from it, so a target the branch +cannot affect gets no runner. It answers two questions: which targets to prove, +and, with `--mutation`, which mutation sets to re-run, the second being narrower +because a file that only schedules the run cannot change whether a target +rejects a broken source. Every "cannot tell" answer widens back to the whole +set, and a push to `main` always proves and mutates everything. + +Three things follow when adding a target or a proof input. An input reached +through `-include` or an `-I` the scan does not use is invisible to the closure +and belongs in `HARNESS_FILES` (or under `STUB_PREFIX`). A file that only picks +what runs goes in `SCHEDULING_FILES`, and the self-test refuses it if it also +carries a prover budget or a make invocation. And `proof-scope.py --self-test`, +run by `.github/workflows/lint.yml`, is what tells you the lists are still +honest. + ### Adding to src/proved/ Nothing lands there without a proof target - -`scripts/check-proof-targets.py` (a CI job in `.github/workflows/main.yml`) +`scripts/check-proof-targets.py` (a CI job in `.github/workflows/lint.yml`) fails otherwise. Callers include the header as `proved/.h`. The routine: 1. Extract the arithmetic into `src/proved/.h` with ACSL contracts. 2. Add the `VERIFY__SRC` / `VERIFY__MODEL` / `VERIFY__FCTS` - variables in `mk/analysis.mk` so the rule template instantiates + variables in `mk/verify.mk` so the rule template instantiates `verify-`. `typed` is the default choice for a model; see below. 3. `make verify-` until it discharges with `-wp-rte`. 4. `make verify-mutants MUTANT_TARGET=` - a proof that cannot reject a @@ -116,7 +132,7 @@ Supporting gates, all of which run per target: ### Memory models, and what no model checks -Each target picks its own model via `VERIFY__MODEL` in `mk/analysis.mk`, +Each target picks its own model via `VERIFY__MODEL` in `mk/verify.mk`, and the comment above it says why. Pick the model the code needs, not the model a neighbour target uses. @@ -174,7 +190,7 @@ and two files conflict), and `macos-libc.h` for Darwin constants the modeled libc omits. It sits outside `src/` on purpose so a real compile, which resolves through -`-Isrc`, cannot reach it. Only `FRAMAC_STUB_DIR` in `mk/analysis.mk` does. +`-Isrc`, cannot reach it. Only `FRAMAC_STUB_DIR` in `mk/verify.mk` does. It is tracked in git because every proof target needs it to parse. A missing declaration fails with "Cannot resolve variable" - that is how the @@ -204,5 +220,5 @@ so prefer them when the two disagree: - `docs/testing.md`, section "Validation Strategy By Change Type" - the change area to command mapping. -- `mk/analysis.mk` - the per-target `_SRC` / `_MODEL` / `_FCTS` variables and +- `mk/verify.mk` - the per-target `_SRC` / `_MODEL` / `_FCTS` variables and the comment above each explaining its model choice. diff --git a/.github/actions/framac/action.yml b/.github/actions/framac/action.yml new file mode 100644 index 00000000..2b006636 --- /dev/null +++ b/.github/actions/framac/action.yml @@ -0,0 +1,111 @@ +# Frama-C, Alt-Ergo and Z3 on a macOS runner, ready for "make verify". +# +# Two jobs in verify.yml need this identically: the one that proves, and each +# leg of the mutation matrix. Actions has no other way to share steps between +# jobs, and the alternative is a forty-line copy that drifts the first time +# either half is touched. +# +# The caller still has to "eval $(opam env --switch=...)" in its own run steps, +# since a composite action cannot export shell state to them. The switch name +# comes back as an output so nothing has to spell it twice. +# +# The toolchain pins live here rather than in the callers. They are inputs with +# defaults, so a job can still override one, but nothing has to repeat them: +# two jobs each carrying their own copy is how the proving half and the +# mutating half end up on different analyzers with no output saying so. +name: Set up Frama-C +description: Install Frama-C and the provers, from cache when the pins are unchanged + +inputs: + framac-version: + description: Frama-C version to install + # 33.0, checked rather than assumed: the whole set discharges 803 of 803 + # obligations across all 17 targets on it, with these same two provers, and + # the mutation gate still bites on the targets sampled. A proof that stops + # discharging on a newer analyzer is a real signal, so the pin exists to + # make the version an explicit decision, not to freeze it. Bumping any of + # the three is a cold opam build, since the cache key is keyed on all of + # them, and that first run is the one at risk of a job timeout. + # + # Defaults rather than required inputs because both callers want the same + # analyzer: proving on one Frama-C while mutating on another is an + # inconsistency no output would name. + default: "33.0" + alt-ergo-version: + description: Alt-Ergo version to install + default: "2.6.3" + z3-version: + description: Z3 version to install + default: "4.16.0" + brew-packages: + description: Homebrew packages the opam build needs + default: opam gmp pkg-config graphviz llvm@17 zlib + +outputs: + switch: + description: The opam switch name to eval into + value: frama-c-elfuse + +runs: + using: composite + steps: + - name: Point opam at a cacheable root + shell: bash + run: | + set -euo pipefail + echo "OPAMROOT=${{ github.workspace }}/.opam" >> "$GITHUB_ENV" + echo "OPAMCONFIRMLEVEL=unsafe-yes" >> "$GITHUB_ENV" + echo "HOMEBREW_NO_INSTALL_CLEANUP=1" >> "$GITHUB_ENV" + echo "HOMEBREW_NO_AUTO_UPDATE=1" >> "$GITHUB_ENV" + + - name: Cache Homebrew downloads + uses: actions/cache@v6 + with: + path: ~/Library/Caches/Homebrew/downloads + # Keyed on the package list, not just the workflow: changing what gets + # installed has to change the key or the cache serves the old set. + key: brew-${{ runner.os }}-${{ runner.arch }}-${{ inputs.brew-packages }} + + - name: Install Homebrew packages + shell: bash + env: + BREW_PKGS: ${{ inputs.brew-packages }} + run: | + set -euo pipefail + # BREW_PKGS is a space-separated list, so it must stay unquoted. + # shellcheck disable=SC2086 + brew install --quiet $BREW_PKGS + + # Every job sharing this action shares one key, so a warm cache costs one + # restore each. Nothing primes it: on a miss they all build Frama-C and the + # provers from source at once, which is the whole cost of bumping any of + # the three pins, and the first run after such a bump is the one at risk of + # a job timeout. A prime job would trade that for a barrier in front of + # every run; the versions move rarely enough that the miss is cheaper. + - name: Cache opam switch + id: opam-cache + uses: actions/cache@v6 + with: + path: ${{ env.OPAMROOT }} + key: opam-${{ runner.os }}-${{ runner.arch }}-frama-c${{ inputs.framac-version }}-ae${{ inputs.alt-ergo-version }}-z3${{ inputs.z3-version }} + + - name: Install Frama-C, Alt-Ergo, Z3 + if: steps.opam-cache.outputs.cache-hit != 'true' + shell: bash + run: | + set -euo pipefail + opam init -y --bare --disable-sandboxing + opam switch create frama-c-elfuse 4.14.1 + eval "$(opam env --switch=frama-c-elfuse)" + opam install -y \ + frama-c.${{ inputs.framac-version }} \ + alt-ergo.${{ inputs.alt-ergo-version }} \ + z3.${{ inputs.z3-version }} + + - name: Report the toolchain + shell: bash + run: | + set -euo pipefail + eval "$(opam env --switch=frama-c-elfuse)" + why3 config detect + frama-c -version diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 234eb28d..edd8f26b 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -9,20 +9,56 @@ # Apple Silicon runners; the hosted job stops at build. name: Build +# paths-ignore skips the run only when EVERY changed file matches, so the list +# below is what cannot reach a build or a test: prose, editor and agent +# configuration, the Frama-C stubs (reached only through mk/verify.mk, never +# through -Isrc), and the other workflows. Everything else, src/ and tests/ and +# mk/ and scripts/ and this file included, still runs the full job. Adding a +# path here says "no build or test input can depend on this"; anything new is +# unlisted and therefore builds, which is the safe direction. .gitignore is NOT +# listed for that reason: checkout's git clean -ffdx wipes exactly what it +# names, which is why the fixture-restore step further down exists at all. +# +# On pull_request only. Actions does not expand YAML anchors, so a filter on +# push too would be a second copy with nothing keeping the two in step, and a +# drift between them means a branch and its own merge commit run different +# checks. The cost of dropping it is one build on a doc-only merge to main. +# verify.yml keeps its push filter instead, and the asymmetry is the price: +# the same doc-only merge would start seventeen macOS proof legs there. +# +# The failure directions differ from the proof scoping in proof-scope.py, which +# is why that one needs a self-test and this one does not: a stale entry here +# (path renamed) matches nothing and the workflow runs MORE, while a stale +# entry in HARNESS_FILES widens nothing and the proofs run LESS. +# +# One condition on all of that: main carries no branch protection and no +# ruleset today, so a run that never starts blocks nothing. A path filter skips +# the whole run rather than reporting a skipped job, and a REQUIRED check that +# never reports stays pending forever. Whoever makes these checks required has +# to move the filtering into the jobs (a cheap classifier job plus "if:" on the +# expensive ones) at the same time. on: push: branches: [main] - paths-ignore: - - '**.md' - - 'docs/**' - - 'LICENSE' pull_request: branches: [main] paths-ignore: - '**.md' - 'docs/**' - 'LICENSE' + - '.agents/**' + - '.claude/**' + - '.editorconfig' + - '.clang-format' + - 'frama-c-stubs/**' + - '.github/workflows/lint.yml' + - '.github/workflows/static-analysis.yml' + - '.github/workflows/verify.yml' workflow_dispatch: + # A merge queue runs the merged result, not the PR, and merge_group carries + # no path filter and no pull_request payload: every check runs in full there. + # Without this trigger a queue would merge with nothing having run at all. + merge_group: # Cancel in-progress runs for the same PR; keep main runs going. concurrency: @@ -96,7 +132,8 @@ jobs: if: > github.repository == 'sysprog21/elfuse' && (github.event_name == 'push' || github.event_name == 'pull_request' || - github.event_name == 'workflow_dispatch') + github.event_name == 'workflow_dispatch' || + github.event_name == 'merge_group') runs-on: [self-hosted, macOS, arm64] # Sanitizer builds run several times slower than the release build, so the # job budget and the per-test TEST_TIMEOUT are set per leg. Without diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml index d00bad68..a4dbe4d6 100644 --- a/.github/workflows/lint.yml +++ b/.github/workflows/lint.yml @@ -4,20 +4,24 @@ # problem at once instead of stopping at the first. name: Lint +# No path filter, deliberately, and the only workflow without one. Two things +# lean on that. proof-scope.py's self-test has to run somewhere a path filter +# cannot skip, or the mechanism that decides which proofs run could skip its +# own gate. check-skill-refs.py validates the .md files under .claude/, whose +# entire input domain the old '**.md' ignore excluded and which build.yml and +# static-analysis.yml both list as inert, so a documentation-only pull request +# would otherwise run no CI at all, including the check written for exactly +# that file. on: push: branches: [main] - paths-ignore: - - '**.md' - - 'docs/**' - - 'LICENSE' pull_request: branches: [main] - paths-ignore: - - '**.md' - - 'docs/**' - - 'LICENSE' workflow_dispatch: + # A merge queue runs the merged result, not the PR, and merge_group carries + # no path filter and no pull_request payload: every check runs in full there. + # Without this trigger a queue would merge with nothing having run at all. + merge_group: # Cancel in-progress runs for the same PR; keep main runs going. concurrency: @@ -42,13 +46,137 @@ jobs: - name: Checkout uses: actions/checkout@v7 + # The checks needing nothing from LINT_PKGS run first; only clang-format, + # shellcheck and cppcheck want it. That ordering buys an earlier + # annotation rather than runner minutes, since a failing run still pays + # for the install: what skips the install is the content check further + # down, not an earlier failure. + # + # Every step from here on carries "if: !cancelled()", the setup steps + # included, because the job's contract at the top of this file is that + # one failure does not hide the rest. A default-conditioned setup step + # would be skipped by the first pre-apt failure, and the three + # tool-dependent checks would then report a missing binary instead of + # reporting on the code. + - name: Trailing newline + if: ${{ !cancelled() }} + run: .ci/check-newline.sh + + - name: Banned APIs / secrets / unsafe pp directives + if: ${{ !cancelled() }} + run: .ci/check-security.sh + + - name: Syscall dispatch table consistency + # The generator validates dispatch.tbl <-> syscall.c on every run; + # writing to a throwaway path is enough to exercise validate_wrappers(). + if: ${{ !cancelled() }} + run: python3 scripts/gen-syscall-dispatch.py --output "$RUNNER_TEMP/dispatch.h" + + - name: Proof target consistency + # Three lists name the same proved sources: mk/verify.mk's targets, + # the verify-mutants matrix in verify.yml, and src/proved/. A target + # in one but not another either drops that target's mutation coverage + # from CI with no error, or leaves an unproved header sitting in a + # directory whose name claims it is proved. + if: ${{ !cancelled() }} + run: python3 scripts/check-proof-targets.py + + - name: Proof scope self-test + # verify.yml builds its matrix from proof-scope.py's answer to "which + # proof targets can this diff reach", so that answer decides whether a + # proof runs at all. It rests on a hand-kept HARNESS_FILES list and on + # include closures, both of which rot quietly. It runs here because + # lint.yml is never narrowed, so the check cannot be skipped by the + # mechanism it checks. + # + # The one step before the apt install that needs a binary: the closures + # come from "cc -MM", and cc is the runner image's preinstalled gcc, + # not a LINT_PKGS entry. An image without one fails this step loudly + # ("cannot determine proof-input closures") rather than scoping on a + # scan it could not run, so the assumption announces itself. Installing + # a compiler here instead would put this check behind the apt step and + # cost it the fast failure. + if: ${{ !cancelled() }} + run: python3 scripts/proof-scope.py --self-test + + - name: Skill cross-references + # The .claude/ skills cite files, make targets and sections by name. + # Nothing else notices when one is renamed, and a skill that points at + # a file which no longer exists is worse than no skill: it reads as + # current. This found two dead references to a workflow and a makefile + # that the CI split had already removed. + if: ${{ !cancelled() }} + run: python3 scripts/check-skill-refs.py + + # What follows needs LINT_PKGS, and the three checks that use it read + # only C sources, the style file, and the .ci scripts that implement + # them. cppcheck alone is 50 of this job's 85 seconds and the install is + # another 12, so a pull request touching none of those would otherwise + # pay about 70 seconds for three checks with nothing to look at. + # The six checks above still run on everything, which is what lets this + # workflow carry no path filter at all. + # + # Whenever the answer is not certain (a push, a merge queue, a base that + # cannot be fetched) every check runs. A skipped check here is one whose + # inputs are unchanged, never one whose result is unknown. + - name: Which inputs changed + id: changed + if: ${{ !cancelled() }} + run: | + set -euo pipefail + run_everything() { + echo "c=true" >> "$GITHUB_OUTPUT" + echo "sh=true" >> "$GITHUB_OUTPUT" + echo "$1; running every check" + exit 0 + } + base="${{ github.event.pull_request.base.sha }}" + if [ -z "$base" ]; then + run_everything "no pull_request base to diff against" + fi + if ! git fetch --no-tags --depth=1 origin "$base"; then + run_everything "cannot fetch $base" + fi + # -z, or git renders a non-ASCII path as a quoted C string under + # core.quotePath and the anchored patterns below stop matching it. + # A path that stops matching skips a check, which is the direction + # this step must not fail in, so the diff failing takes the same + # way out as a failed fetch. + if ! files=$(git diff --name-only -z "$base" HEAD | tr '\0' '\n'); then + run_everything "cannot diff against $base" + fi + # "c" is not "a .c or .h file changed", it is "an input to + # clang-format or cppcheck changed", and those two read more than + # the sources: .clang-format is the style clang-format enforces, + # .ci/ holds the scripts that ARE the checks, and check-cppcheck.sh + # regenerates build/dispatch.h from dispatch.tbl through the + # generator before it analyzes anything. A pull request editing only + # one of those would otherwise change a check without running it. + c=false; sh=false + pat='\.(c|h)$|^\.clang-format$|^\.ci/|^src/syscall/dispatch\.tbl$' + pat="$pat"'|^scripts/gen-syscall-dispatch\.py$' + # A here-string, not a pipeline into grep. Under pipefail a "grep -q" + # that matches early exits while the writer still has bytes to push, + # the writer takes SIGPIPE, and the pipeline reports non-zero even + # though the pattern MATCHED -- so the check would read as "unchanged" + # and skip. .ci/check-security.sh carries the same trap at length. + # It needs a diff long enough to fill the pipe buffer, which is + # exactly the diff that must not skip a check. + if grep -qE "$pat" <<< "$files"; then c=true; fi + if grep -qE '^\.ci/.*\.sh$' <<< "$files"; then sh=true; fi + echo "c=$c" >> "$GITHUB_OUTPUT" + echo "sh=$sh" >> "$GITHUB_OUTPUT" + echo "C sources changed: $c; .ci shell changed: $sh" + - name: Cache apt packages + if: ${{ !cancelled() && (steps.changed.outputs.c == 'true' || steps.changed.outputs.sh == 'true') }} uses: actions/cache@v6 with: path: ~/apt-cache key: apt-${{ runner.os }}-${{ env.LINT_PKGS }} - name: Add LLVM apt repo (clang-format-22) + if: ${{ !cancelled() && (steps.changed.outputs.c == 'true' || steps.changed.outputs.sh == 'true') }} # Place the key in /etc/apt/keyrings and bind it via signed-by so # it grants trust only to the LLVM repository, not system-wide. run: | @@ -60,6 +188,7 @@ jobs: | sudo tee /etc/apt/sources.list.d/llvm.list - name: Install tools + if: ${{ !cancelled() && (steps.changed.outputs.c == 'true' || steps.changed.outputs.sh == 'true') }} run: | set -euo pipefail mkdir -p ~/apt-cache @@ -68,42 +197,19 @@ jobs: sudo apt-get install -y -o Dir::Cache::Archives="$HOME/apt-cache" \ $LINT_PKGS - - name: Trailing newline - if: ${{ !cancelled() }} - run: .ci/check-newline.sh - - name: clang-format - if: ${{ !cancelled() }} + if: ${{ !cancelled() && steps.changed.outputs.c == 'true' }} run: .ci/check-format.sh - - name: Banned APIs / secrets / unsafe pp directives - if: ${{ !cancelled() }} - run: .ci/check-security.sh - - name: shellcheck # Scoped to .ci/ -- tests/ has pre-existing warnings that the # repository's own check-format target already surfaces. - if: ${{ !cancelled() }} + if: ${{ !cancelled() && steps.changed.outputs.sh == 'true' }} run: | set -euo pipefail mapfile -d '' files < <(git ls-files -z -- '.ci/*.sh') shellcheck --severity=warning "${files[@]}" - name: cppcheck - if: ${{ !cancelled() }} + if: ${{ !cancelled() && steps.changed.outputs.c == 'true' }} run: .ci/check-cppcheck.sh - - - name: Syscall dispatch table consistency - # The generator validates dispatch.tbl <-> syscall.c on every run; - # writing to a throwaway path is enough to exercise validate_wrappers(). - if: ${{ !cancelled() }} - run: python3 scripts/gen-syscall-dispatch.py --output "$RUNNER_TEMP/dispatch.h" - - - name: Proof target consistency - # Three lists name the same proved sources: mk/verify.mk's targets, - # the verify-mutants matrix in verify.yml, and src/proved/. A target - # in one but not another either drops that target's mutation coverage - # from CI with no error, or leaves an unproved header sitting in a - # directory whose name claims it is proved. - if: ${{ !cancelled() }} - run: python3 scripts/check-proof-targets.py diff --git a/.github/workflows/static-analysis.yml b/.github/workflows/static-analysis.yml index 891998d2..c8d8a337 100644 --- a/.github/workflows/static-analysis.yml +++ b/.github/workflows/static-analysis.yml @@ -5,20 +5,40 @@ # infer-macos : Facebook Infer capture + analyze over the full build name: Static analysis +# All three jobs analyze "make elfuse" and nothing else, so tests/ joins the +# prose and configuration below: a change there cannot alter a single +# translation unit any of them sees. paths-ignore skips the run only when EVERY +# changed file matches, and anything not listed still runs the full set, which +# is the safe direction for a path that turns out to matter after all. +# +# On pull_request only, and the same conditions build.yml states at length: one +# list per file so nothing can drift, and a path filter skips the whole run, so +# a REQUIRED check that never reports would stay pending. main has no branch +# protection today; making these required means moving the filter into the +# jobs. on: push: branches: [main] - paths-ignore: - - '**.md' - - 'docs/**' - - 'LICENSE' pull_request: branches: [main] paths-ignore: - '**.md' - 'docs/**' - 'LICENSE' + - 'tests/**' + - '.agents/**' + - '.claude/**' + - '.editorconfig' + - '.clang-format' + - 'frama-c-stubs/**' + - '.github/workflows/build.yml' + - '.github/workflows/lint.yml' + - '.github/workflows/verify.yml' workflow_dispatch: + # A merge queue runs the merged result, not the PR, and merge_group carries + # no path filter and no pull_request payload: every check runs in full there. + # Without this trigger a queue would merge with nothing having run at all. + merge_group: # Cancel in-progress runs for the same PR; keep main runs going. concurrency: diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index c4258700..fe2dfc74 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -1,12 +1,15 @@ # Frama-C WP proofs of the attacker-facing arithmetic. # -# proof-targets : the proof target list, read out of mk/verify.mk -# verify-mutants: per target, the Frama-C WP proof AND the mutations that -# show it bites; one runner per target, sharded from -# mk/verify.mk's VERIFY__SRC list -# verify : aggregate check name over that matrix, kept because branch -# protection requires it by name -# verify-mutants-gate: the same aggregate under the mutation-gate name +# proof-targets : the target list, read out of mk/verify.mk and, on a pull +# request, narrowed twice: once for what the diff can prove +# differently, once for what it can mutate differently +# verify-proofs : proves whatever the matrix below will not, which is +# usually nothing, since a mutation leg proves its own target +# first as its control +# verify-mutants: the targets whose mutation verdict the diff can move, +# packed into a few runners, expensive and usually empty +# verify : both verdicts under the check name that predates the split, +# which covered both halves and still does name: Proofs on: @@ -23,6 +26,11 @@ on: - 'docs/**' - 'LICENSE' workflow_dispatch: + # A merge queue runs the merged result, not the PR, and merge_group carries + # no path filter and no pull_request payload: the proof-targets job below + # sees an empty base and proves everything. Without this trigger a queue + # would merge with nothing having run at all. + merge_group: # Cancel in-progress runs for the same PR; keep main runs going. concurrency: @@ -32,19 +40,41 @@ concurrency: permissions: contents: read +# Reaches -wp-timeout in mk/verify.mk, and both macOS jobs must inherit the +# same value: the mutation runs prove an unmutated control through the very +# recipe the proving job runs, and check-mutants.py's docstring explains how a +# shorter budget silently converts a MISS into a "caught". One block, so the +# two cannot drift. The floor is check_baseline, which proves that control +# first, so a value too tight to prove real code fails loudly instead. +env: + FRAMAC_TIMEOUT: 45 + jobs: # The proof target list has ONE home, mk/verify.mk's VERIFY__SRC # assignments. This job reads it there and the matrix below is built from the # result, so adding a proof target is a one-file edit and a target can no # longer exist locally while silently having no CI leg. # + # On a pull request it then drops the targets the branch cannot have affected, + # so the matrix below is proportional to the diff instead of spinning up a + # macOS runner per proof to re-establish a verdict the base already has. The + # scope comes from the compiler's own include closure per proved source, and + # every "cannot tell" answer inside proof-scope.py widens back to the full + # set, which is the safe direction for an optimization. A push to main always + # runs everything, so the guarantee on the branch a PR merges into is never + # the narrowed one. + # # Runs on Linux with no toolchain: "make print-verify-targets" only reads the - # makefile, so this costs seconds and gates nothing. + # makefile and the closure scan is cc -MM, so this costs seconds and gates + # nothing. proof-targets: name: Enumerate proof targets runs-on: ubuntu-latest outputs: - targets: ${{ steps.list.outputs.targets }} + rules: ${{ steps.list.outputs.rules }} + empty: ${{ steps.list.outputs.empty }} + mutants: ${{ steps.list.outputs.mutants }} + mutants_empty: ${{ steps.list.outputs.mutants_empty }} steps: - name: Checkout uses: actions/checkout@v7 @@ -53,14 +83,96 @@ jobs: id: list run: | set -euo pipefail - targets=$(make print-verify-targets) - test -n "$targets" - json=$(printf '%s\n' "$targets" | jq -R -s -c 'split("\n") | map(select(length > 0))') - echo "targets=$json" >> "$GITHUB_OUTPUT" - echo "proof targets: $json" + # Two questions, not one. Proving asks what the diff can reach; + # mutating asks the narrower "can this diff change whether a target + # rejects a broken source", which the files that only schedule the + # run cannot. See MUTATION_HARNESS_FILES in proof-scope.py. + # + # The checkout is shallow, so the base commit has to be fetched + # before it can be diffed against. A fetch that does not work falls + # through to the full list, same as a push. A merge_group event has + # no pull_request payload, so base is empty there and the queue + # proves and mutates everything. + # + # No --cc: the include scan only walks #include lines, which every C + # preprocessor agrees on. + base="${{ github.event.pull_request.base.sha }}" + if [ -n "$base" ] && git fetch --no-tags --depth=1 origin "$base"; then + # No fallback around these two: proof-scope.py answers every + # expected failure with the full set itself, so a non-zero exit + # here is the tool being broken, which should be loud. + targets=$(python3 scripts/proof-scope.py \ + --print-targets-changed-since "$base") + mutants=$(python3 scripts/proof-scope.py \ + --print-targets-changed-since "$base" --mutation) + else + # make owns the full list. proof-scope.py derives its own by regex + # over the same file and check-proof-targets.py gates the two for + # equality in lint.yml, but where no narrowing happens there is no + # reason to ask anything but make. + targets=$(make print-verify-targets) + test -n "$targets" + mutants=$targets + fi + # The proving job takes what the mutation matrix will NOT cover. + # check-mutants.py proves an unmutated control through the very same + # "make verify-" rule before it mutates anything, so a target in + # both scopes would otherwise be proved twice, once in a job of its + # own and once inside its leg. Over the last 400 commits the proof + # scope was never wider than the mutation scope, so this is usually + # empty and the macOS job does not start at all. + extra=$(comm -23 <(printf '%s\n' "$targets" | sort -u) \ + <(printf '%s\n' "$mutants" | sort -u)) + # rules is already prefixed, so the prove job needs no shell of its + # own; mutants is JSON because it is a matrix. The guard matters: + # printf runs its format once even with no arguments, so an empty + # list would yield a lone "verify-" and send make at a rule that does + # not exist. + rules="" + if [ -n "$extra" ]; then + # Word splitting is the point of the unquoted expansion. + # shellcheck disable=SC2086 + rules=$(printf 'verify-%s ' $extra) + fi + # Packed into at most five groups rather than one leg per target: + # each leg spends about 90 seconds on Homebrew and the opam switch + # before it proves anything, and GitHub bills wall time rounded up to + # the minute. Measured on a full-scope run, 17 legs cost 85 + # macOS-minutes where 5 buckets cost 61. + # + # Five because that is about what runs concurrently on macOS anyway, + # so the whole matrix fits one wave and the wall clock improves as + # well. check-mutants.py owns the packing because it owns the + # mutation counts it packs by. + # shellcheck disable=SC2086 + buckets=$(python3 scripts/check-mutants.py --pack 5 $mutants) + json=$(printf '%s\n' "$buckets" | jq -R -s -c 'split("\n") | map(select(length > 0))') + # An explicit boolean for the matrix, so neither consumer has to know + # that jq -c spells an empty list "[]", and neither fails open if that + # encoding changes. + mutants_empty=$([ "$json" = '[]' ] && echo true || echo false) + { + echo "rules=$rules" + echo "empty=$([ -z "$rules" ] && echo true || echo false)" + echo "mutants=$json" + echo "mutants_empty=$mutants_empty" + } >> "$GITHUB_OUTPUT" + echo "proof targets: ${targets//$'\n'/ }" + echo "proved by a job of their own: ${rules:-}" + echo "mutation targets: ${mutants//$'\n'/ }" + echo "packed into: $json (empty: $mutants_empty)" - # Frama-C WP proofs of the attacker-facing arithmetic, plus the mutation gate - # that shows those proofs bite. One runner per proof target. + # Frama-C WP proofs for the targets the mutation matrix will not cover. + # + # One job, not one per target: proving all 17 costs 6.5 macOS-minutes + # measured across a real run, while the setup each leg pays before it + # (Homebrew, then restoring a ~1 GB opam switch) is 82 seconds apiece. + # + # It exists for the case where a diff can change which targets get proved + # without changing any mutation verdict, since then nothing else proves them. + # In every other shape the matrix below proves each of its targets already, + # through the unmutated control check-mutants.py runs first, and this job + # skips rather than repeat that work in a runner of its own. # # GATING, unlike tidy-macos and scan-macos: the inputs these proofs cover come # from untrusted binaries and from the guest itself, so an unproved @@ -68,187 +180,156 @@ jobs: # job the proofs are only enforced when a human runs them, and they rot the # first time someone edits elf.c or gdbstub-rsp.c. # - # Proves one target and shows its mutations are rejected, one runner per - # target. Both halves live here because they are the same work: check-mutants - # runs "make verify-" on an UNMUTATED copy as its control, so a - # separate serial verify job proved every target and then every shard - # proved its own target over again. - # - # Sharding is what makes the mutation half affordable at all: a caught - # mutation grinds against every unprovable goal until FRAMAC_TIMEOUT, so the - # whole set on one runner is minutes where a single proof is seconds. Running - # the proof first inside the shard keeps the fast failure the old "needs: - # verify" edge gave, now per target rather than across all of them, and - # without a barrier that made every shard wait for the slowest proof. - # - # The matrix comes from the proof-targets job above, which reads - # mk/verify.mk, so this list cannot drift from the targets that exist. - verify-mutants: - name: Proof and mutations (${{ matrix.target }}) + # A new check name, deliberately. The historic one covered proofs AND + # mutations, because the matrix legs it aggregated ran both, so hanging it on + # a proof-only job would quietly stop enforcing half of what anyone requiring + # it expected. The combined verdict keeps that name; see the last job here. + verify-proofs: + name: Frama-C WP proofs needs: proof-targets + # Nothing to prove, so do not boot a macOS runner for it. + if: ${{ needs.proof-targets.outputs.empty != 'true' }} runs-on: macos-15 timeout-minutes: 60 - strategy: - fail-fast: false - matrix: - target: ${{ fromJson(needs.proof-targets.outputs.targets) }} - env: - HOMEBREW_NO_INSTALL_CLEANUP: 1 - HOMEBREW_NO_AUTO_UPDATE: 1 - BREW_PKGS: opam gmp pkg-config graphviz llvm@17 zlib - OPAMCONFIRMLEVEL: unsafe-yes - # Reaches -wp-timeout in mk/verify.mk and is the biggest term in this - # job's runtime: both steps below use it, and a caught mutation leaves - # a goal open that costs both provers the full value. The floor is - # check_baseline in check-mutants.py, which proves an UNMUTATED copy - # through this same path first, so a value too tight to prove real - # code fails loudly instead of scoring mutations as caught. "make - # verify" discharges 803 obligations across 17 targets in 23s - # locally, the slowest target in 19s. - FRAMAC_TIMEOUT: 45 - FRAMAC_VERSION: "31.0" - ALT_ERGO_VERSION: 2.6.3 - Z3_VERSION: 4.16.0 - OPAMROOT: ${{ github.workspace }}/.opam - OPAM_SWITCH: frama-c-elfuse steps: - name: Checkout uses: actions/checkout@v7 - - name: Cache Homebrew downloads - uses: actions/cache@v6 - with: - path: ~/Library/Caches/Homebrew/downloads - key: brew-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} + - name: Set up Frama-C + id: framac + uses: ./.github/actions/framac - - name: Install Homebrew packages - # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. + - name: Prove the selected targets + # Named targets rather than "make verify", which would prove all 17 + # whatever the scope said. The -j has to be passed here: mk/verify.mk + # adds one only inside the aggregate "verify" rule, so a list of + # verify- targets would otherwise run one prover at a time. run: | set -euo pipefail - brew install --quiet $BREW_PKGS + eval "$(opam env --switch="${{ steps.framac.outputs.switch }}")" + # -j4 for the same reason MUTANT_JOBS is 4 in the next job: the + # hosted runner has few cores and each target is a frama-c process + # holding its own goals in memory. + rules='${{ needs.proof-targets.outputs.rules }}' + # The job's "if" already covers this, so reaching it means the two + # outputs disagreed. Worth a line because the silent version is bad: + # "make -j4" with no goal falls through to .DEFAULT_GOAL, prints the + # help text, exits 0, and the check goes green having proved nothing. + test -n "$rules" || { + echo "::error::no rules to prove, but the job was not skipped" + exit 1 + } + # Word splitting is the point: rules is a space-separated list of + # make goals, produced by the job above from mk/verify.mk and never + # from anything a pull request writes. + # shellcheck disable=SC2086 + make -j4 $rules - # Every leg shares one key, so a warm cache costs one restore per leg. - # Nothing primes it any more: the job that used to build the switch first - # is gone, and proof-targets runs on Linux, so on a miss all legs build - # Frama-C and the provers from source at once. That is the whole cost of - # bumping any of the three pinned versions below, and the first run after - # such a bump is the one at risk of the 60-minute timeout. A prime job - # would trade that for a barrier in front of every run; the versions move - # rarely enough that the miss is the cheaper side. - - name: Cache opam switch - id: opam-cache - uses: actions/cache@v6 + - name: Upload prover log + if: always() + uses: actions/upload-artifact@v7 with: - path: ${{ env.OPAMROOT }} - key: opam-${{ runner.os }}-${{ runner.arch }}-frama-c${{ env.FRAMAC_VERSION }}-ae${{ env.ALT_ERGO_VERSION }}-z3${{ env.Z3_VERSION }} + name: verify-logs + path: build/verify-*.log + if-no-files-found: warn + retention-days: 7 - - name: Install Frama-C, Alt-Ergo, Z3 - if: steps.opam-cache.outputs.cache-hit != 'true' - run: | - set -euo pipefail - opam init -y --bare --disable-sandboxing - opam switch create "$OPAM_SWITCH" 4.14.1 - eval "$(opam env --switch="$OPAM_SWITCH")" - opam install -y \ - frama-c.$FRAMAC_VERSION \ - alt-ergo.$ALT_ERGO_VERSION \ - z3.$Z3_VERSION + # The mutation gate, sharded because it is the expensive half: a caught + # mutation grinds against every unprovable goal until FRAMAC_TIMEOUT, so the + # whole set on one runner is 51 macOS-minutes where the proofs are 6.5. + # + # Its matrix is a different question from the proofs above. A branch that + # edits the scheduling machinery has to re-prove everything, since which + # targets run is exactly what it changed, but it cannot change whether a + # target rejects a broken source, so nothing here needs to re-run. See + # MUTATION_HARNESS_FILES in proof-scope.py for what separates the two. + # + # check-mutants proves an UNMUTATED copy first as its control, so a leg that + # runs at all also re-establishes the proof for its own target; the job above + # is not a prerequisite and deliberately not a "needs" edge, so the two halves + # run in parallel. + verify-mutants: + name: Mutations (${{ matrix.target }}) + needs: proof-targets + # Skipped through the condition rather than through matrix expansion: + # what Actions does with a zero-entry matrix vector is observed behavior + # rather than documented syntax, and the verdict job depends on the answer. + if: ${{ needs.proof-targets.outputs.mutants_empty != 'true' }} + runs-on: macos-15 + timeout-minutes: 60 + strategy: + fail-fast: false + matrix: + target: ${{ fromJson(needs.proof-targets.outputs.mutants) }} + steps: + - name: Checkout + uses: actions/checkout@v7 - - name: Prove the target (make verify-) - # First, so a broken proof fails this shard in seconds instead of after - # its mutation set. check-mutants would catch it too, through - # check_baseline, but only after paying for the setup a second time and - # with a message about infrastructure rather than about the proof. - run: | - set -euo pipefail - eval "$(opam env --switch="$OPAM_SWITCH")" - why3 config detect - frama-c -version - make verify-${{ matrix.target }} + - name: Set up Frama-C + id: framac + uses: ./.github/actions/framac - name: Prove the gate bites (make verify-mutants) - # why3 config detect is cheap and idempotent; the proof step above - # already ran it on this runner. - # - # MUTANT_JOBS is set explicitly for the same reason as before - # sharding: this runner has few enough cores that the script's - # one-per-core default lands near serial. + # One target at a time within the bucket, so a failure names the target + # rather than the group. MUTANT_JOBS is set explicitly because this + # runner has few enough cores that the script's one-per-core default + # lands near serial. run: | set -euo pipefail - eval "$(opam env --switch="$OPAM_SWITCH")" - why3 config detect - # On a pull request, re-verify only the targets whose source the - # branch actually touches; a target it does not touch has the verdict - # the base already established. A push to the base runs the full set, - # so the guarantee is never weaker than the branch it merges into. - # The checkout is shallow, so the base commit has to be fetched - # before it can be diffed against. If that does not work the script - # says so and runs the full set, which is the safe direction for an - # optimization. - base="${{ github.event.pull_request.base.sha }}" - if [ -n "$base" ] && git fetch --no-tags --depth=1 origin "$base"; then - make verify-mutants MUTANT_JOBS=4 MUTANT_TARGET=${{ matrix.target }} MUTANT_SINCE="$base" - else - make verify-mutants MUTANT_JOBS=4 MUTANT_TARGET=${{ matrix.target }} - fi + eval "$(opam env --switch="${{ steps.framac.outputs.switch }}")" + for target in ${{ matrix.target }}; do + echo "::group::$target" + make verify-mutants MUTANT_JOBS=4 MUTANT_TARGET="$target" + echo "::endgroup::" + done - name: Upload prover log if: always() uses: actions/upload-artifact@v7 with: - name: verify-logs-${{ matrix.target }} + name: mutation-logs-${{ matrix.target }} path: | build/verify-*.log build/verify-mutants/*.log if-no-files-found: warn retention-days: 7 - # The proving moved into the matrix above, but this check name predates that - # and branch protection requires it by name, so it stays as an aggregate over - # the same matrix. The "(make verify)" suffix is kept for that continuity - # alone: this job runs no proofs itself, and renaming it would silently - # unrequire the check until someone updated the branch rule to match. + # One job owning the whole verdict, under the check name that predates this + # split. It meant "proofs and mutations both passed" when it aggregated a + # matrix whose legs ran both halves, and it means that still. Two aggregate + # jobs were one too many: a second requirable name that nothing requires, + # with the skip rules split across two scripts that had to agree. + # + # Each half's empty-scope case is a pass, and only for the exact reason its + # own job was skipped. proof-targets failing instead leaves both outputs + # empty rather than "true", which neither test accepts. + # + # if: always() is what makes this run when a leg fails; without it the job + # would be skipped, and a skipped check does not block a merge. !cancelled() + # would skip it on a cancelled run, which always() reports instead. + # + # check-proof-targets.py asserts that every macOS job in this file is in this + # job's needs, so the next split cannot quietly leave one out from under the + # name. verify: name: Frama-C WP proofs (make verify) - needs: verify-mutants - # always(), matching verify-mutants-gate below and for the reason stated - # there: a required check that is SKIPPED does not block a merge, and - # !cancelled() skips this job whenever the run is cancelled. always() makes - # it run and report the matrix verdict in that case too. - if: always() - runs-on: ubuntu-latest - steps: - - name: Report the matrix result - run: | - set -euo pipefail - result='${{ needs.verify-mutants.result }}' - if [ "$result" != "success" ]; then - echo "proof matrix did not succeed: $result" >&2 - exit 1 - fi - echo "every proof target discharged" - - # One stable check name covering the whole mutation matrix, so branch - # protection has something to require. The matrix leg names carry the target - # in them ("Mutation gate (fuse)"), which means every added proof target - # would otherwise need its own branch-protection entry, and a target added - # without that entry would be unenforced from the day it landed. - # - # needs..result is the aggregate over all legs, so this passes - # only when every one of them did. if: always() is what makes it run at all - # when a leg fails; without it this job would be skipped, and a skipped - # required check does not block a merge. A skipped matrix (verify failed - # upstream) reports "skipped" here too, which the equality test rejects. - verify-mutants-gate: - name: Mutation gate - needs: verify-mutants + needs: [proof-targets, verify-proofs, verify-mutants] if: always() runs-on: ubuntu-latest timeout-minutes: 5 steps: - - name: Require every matrix leg to have passed + - name: Require both halves to have passed run: | set -euo pipefail - result='${{ needs.verify-mutants.result }}' - echo "mutation matrix: $result" - [ "$result" = success ] || exit 1 + proofs='${{ needs.verify-proofs.result }}' + mutations='${{ needs.verify-mutants.result }}' + no_proofs='${{ needs.proof-targets.outputs.empty }}' + no_mutants='${{ needs.proof-targets.outputs.mutants_empty }}' + echo "proofs: $proofs (empty scope: ${no_proofs:-})" + echo "mutations: $mutations (empty scope: ${no_mutants:-})" + ok() { + [ "$1" = success ] || { [ "$1" = skipped ] && [ "$2" = true ]; } + } + ok "$proofs" "$no_proofs" || exit 1 + ok "$mutations" "$no_mutants" || exit 1 + echo "both halves accounted for" diff --git a/mk/verify.mk b/mk/verify.mk index 0253be8d..be780133 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -38,24 +38,35 @@ # proved "for x86_64" and no x86_64 code is involved; the flag only tells the # prover how wide a size_t is. # -# Frama-C 31 ships avr_16, avr_8, gcc_x86_16, gcc_x86_32, gcc_x86_64, -# msvc_x86_64, ppc_32, x86_16, x86_32, x86_64 -- no aarch64 entry at all. Of -# those, gcc_x86_64 is the only one that matches arm64 macOS on the properties -# these proofs rest on: +# gcc_x86_64 matches arm64 macOS, the platform this host code is compiled for, +# on every property these proofs rest on: # # property arm64 macOS gcc_x86_64 used by the proof? # pointer / long / size_t 64-bit 64-bit yes # byte order little little yes # uint64_t alignment 8 8 yes -# plain char signedness unsigned signed see below +# plain char signedness signed signed see below # -# Plain-char signedness is the one mismatch, and the RSP proof DOES cover -# functions taking plain char: gdb_hex_pair, gdb_hex_decode, gdb_parse_hex and -# rsp_checksum. What keeps the result signedness-independent is not their -# parameter types but that every use of a char value goes through an explicit -# (unsigned char) or (uint8_t) cast before it is compared or accumulated. That -# is the invariant to preserve: no proved function may read a plain char -# without such a cast. +# The signedness row is the one worth checking rather than recalling, because +# the two arm64 targets in this tree disagree: plain char is SIGNED on Apple's +# arm64, which compiles every proved source, and UNSIGNED on aarch64-linux, +# which the cross toolchain compiles the guest tests with. Both answers come +# from asking those compilers. +# +# Frama-C 33 ships a macos_arm machdep, which sounds like the honest name for +# what is being assumed here, and it is not usable: it is not GCC-based, and +# -include gcc-atomics.h pulls in Frama-C's own __fc_gcc_builtins.h, which +# refuses __int128 outside a GCC-based machdep. Measured, not assumed: every +# target aborts at parse time with "use a GCC-based machdep to enable it". +# Revisit if the atomics stub ever stops being needed. +# +# The RSP proof DOES cover functions taking plain char: gdb_hex_pair, +# gdb_hex_decode, gdb_parse_hex and rsp_checksum. What keeps their results +# signedness-independent is not their parameter types but that every use of a +# char value goes through an explicit (unsigned char) or (uint8_t) cast before +# it is compared or accumulated. That is the invariant to preserve, and it is +# what makes the data model's answer to this question stop mattering: no proved +# function may read a plain char without such a cast. # # check-acsl-coverage.py enforces the part a regex can, and its # CHAR_PARAM_ALLOWLIST carries the rest of the reasoning: a proved function @@ -389,8 +400,8 @@ $(VERIFY_RULES): check-stub-constants | $(BUILD_DIR) @echo " these compute no out-of-bounds access and no overflow" @for f in $(FCTS); do echo " - $$f"; done @echo " memory model: $(MODEL); data model: $(FRAMAC_DATA_MODEL)" - @echo " (data model is type widths only; Frama-C 31" - @echo " has no aarch64 machdep, so this is the LP64 stand-in)" + @echo " (data model is type widths only, and matches arm64" + @echo " macOS on width, order, alignment and char signedness)" @$(FRAMAC) -machdep $(FRAMAC_DATA_MODEL) \ -cpp-extra-args="$(FRAMAC_CPP_ARGS)" \ $(SRC) -wp -wp-rte -wp-model $(MODEL) \ @@ -411,8 +422,12 @@ $(VERIFY_RULES): check-stub-constants | $(BUILD_DIR) # MUTANT_JOBS overrides the script's one-per-core default, which a CI runner # with few cores would otherwise resolve to near-serial. # MUTANT_SINCE restricts the run to targets whose source differs from that ref, -# which keeps a per-PR run proportional to the diff. Leave it empty to run the -# whole set, which is what the base branch needs to do. +# for a local run that only wants what a branch touched. Leave it empty to run +# the whole set, which is what the base branch needs to do. This asks +# scripts/proof-scope.py the same question CI's mutation matrix asks, so a +# local run reproduces that scope; CI does not pass MUTANT_SINCE, since a leg +# that exists at all has a target the diff reaches and applying the scoping a +# second time inside the leg selects everything. # MUTANT_TARGET restricts the run to one proof target, letting CI shard the # full set across parallel jobs instead of one job working through all of it. # Leave it empty to run every target in one process, which is what a local @@ -432,13 +447,13 @@ verify-mutants: # Every verify-* target already runs this for itself, so "make verify" gets it # without listing it; this entry point is for checking the whole set at once. # -# The data-model note above says gcc_x86_64 differs from arm64 macOS on plain -# char signedness, and that the proofs stay sound because no proved function -# reads a plain char without an explicit cast. check-acsl-coverage.py checks -# that with a regex, which cannot see a char behind a typedef or a macro. This -# asks the compiler instead, per proved function and at -O0: identical code -# under -fsigned-char and -funsigned-char means that function behaves the same -# either way, which is the invariant rather than a proxy for it. +# The data-model note above says the tree's real arm64 compilers disagree on +# plain-char signedness, and the proofs stay portable because no proved +# function reads a plain char without an explicit cast. check-acsl-coverage.py +# checks that with a regex, which cannot see a char behind a typedef or a macro. +# This asks the compiler instead, per proved function and at -O0: identical +# code under -fsigned-char and -funsigned-char means that function behaves the +# same either way, which is the invariant rather than a proxy for it. check-char-signedness: @echo " CHARSIGN proof sources under both char signedness settings" $(Q)python3 scripts/check-char-signedness.py --cc '$(CC)' diff --git a/scripts/check-char-signedness.py b/scripts/check-char-signedness.py index c9531adb..597c5c40 100755 --- a/scripts/check-char-signedness.py +++ b/scripts/check-char-signedness.py @@ -1,12 +1,14 @@ #!/usr/bin/env python3 """Detect plain-char use in proved code with the compiler, not a regex. -Frama-C 31 has no aarch64 machdep, so every target is proved under gcc_x86_64. -That model matches arm64 macOS on pointer width, byte order and alignment, but -not on one property: it makes plain char SIGNED where arm64 makes it unsigned -(see the table in mk/verify.mk). The risk only exists where proved code reads -a plain char, so knowing exactly which sources do that is the thing worth -automating. +Every target is proved under one data model, gcc_x86_64 (see mk/verify.mk). +That model matches arm64 macOS on pointer width, byte order, alignment and +plain-char signedness, all four checked with the compilers involved rather than +assumed (see the table in mk/verify.mk). Plain char is signed on Apple's arm64 +target, which compiles every proved source, and unsigned on aarch64-linux, +which compiles the guest tests. A proved function that reads a plain char +without an explicit cast would therefore mean something different in guest-side +code, so knowing exactly which sources do that is the thing worth automating. check-acsl-coverage.py answers it with a regex, which cannot see a plain char reached through a typedef or produced by a macro. This asks the compiler @@ -71,12 +73,11 @@ def proof_sources(): if m: utils = m.group(1) - srcs = { - m.group(1).lower(): m.group(2).strip() - for m in re.finditer( - r"^VERIFY_([A-Z0-9_]+)_SRC\s*:=\s*(\S+)", text, re.MULTILINE - ) - } + # Through the shared reader, not a fourth regex over the same lines. Its + # own \S+ kept the first word of a VERIFY__SRC that named two sources, + # which is the truncation target_sources() now refuses outright; this was + # the one consumer still doing it quietly. + srcs = verify_mk.target_sources() out = {} for m in re.finditer(r"^VERIFY_([A-Z0-9_]+)_FCTS\s*:=\s*(.*)$", text, re.MULTILINE): target = m.group(1).lower() @@ -262,8 +263,8 @@ def main(): if char_failures: print( "\n proved code depends on plain-char signedness.\n" - " gcc_x86_64 makes plain char signed where arm64 macOS makes it\n" - " unsigned, so the proof would not describe the real target. Read\n" + " That would make the proved function depend on which compiler\n" + " built it, so the proof would not cover every real target. Read\n" " the char through an explicit (unsigned char) or (uint8_t) cast.", file=sys.stderr, ) diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index 2b769430..00d7bfd5 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -22,11 +22,9 @@ tree rather than the mutated copy. That is the right choice, but it means the four entries below that mutate a contract are not coverage-checked. -Scoping a run to a changed diff uses the compiler's own -MM to find each -target's full include closure, not the hand-maintained VERIFY_*_SCAN list: -a proved header gaining an include is exactly the kind of change nobody -remembers to mirror into SCAN, and -MM cannot drift from the preprocessor -that actually feeds Frama-C. +Scoping a run to a changed diff lives in proof-scope.py, which answers the +same question for the CI proof matrix. --changed-since here is that answer +applied to mutations. Runs inherit the proof's own per-goal prover timeout, and lowering it for mutation runs is unsound however tempting the speedup looks. A broken contract @@ -50,6 +48,7 @@ """ import argparse +import collections import concurrent.futures import os import pathlib @@ -58,25 +57,31 @@ import shutil import subprocess import sys -import tempfile ROOT = pathlib.Path(__file__).resolve().parent.parent # scripts/ filenames are kebab-case per CLAUDE.md, which no plain "import" -# statement can name, so the shared reader is loaded by path. The alternative +# statement can name, so a sibling module is loaded by path. The alternative # was an underscore in the filename, which the tree does not use anywhere. -def _load_verify_mk(): +def _load(stem, name): import importlib.util - path = pathlib.Path(__file__).resolve().parent / "verify-mk.py" - spec = importlib.util.spec_from_file_location("verify_mk", path) + path = pathlib.Path(__file__).resolve().parent / f"{stem}.py" + spec = importlib.util.spec_from_file_location(name, path) module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) return module -verify_mk = _load_verify_mk() +proof_scope = _load("proof-scope", "proof_scope") +# Loaded here rather than taken as proof_scope.verify_mk, even though that +# would save one parse of mk/verify.mk. This table decides which file each +# mutation copies and mutates, so reaching it through proof-scope.py would make +# that file a judging input; proof-scope.py's own SCHEDULING_FILES says it is +# not one, and a diff touching only it therefore runs no mutation leg at all. +# Two module objects over one silent contradiction. +verify_mk = _load("verify-mk", "verify_mk") BUILD = ROOT / "build" / "mutants" # The recipe writes $(BUILD_DIR)/verify-$(NAME).log, and NAME is overridden per # run to keep concurrent mutations off a shared log. That path must exist first: @@ -883,119 +888,6 @@ def _load_verify_mk(): ] -# Changing any of these can change a verdict for every target, so a run that -# sees one move must not skip anything. mk/toolchain.mk sets CC, which -# check-char-signedness.py compiles with, and the top-level Makefile is what -# pulls in both it and the mk/ files below to build the "make verify-" -# a mutation is judged by; the individual VERIFY_*_SRC/_SCAN/ -# _FCTS lines in mk/verify.mk are covered separately by target_inputs() -# below, but the rest of that file (the shared recipe, MIN_GOALS, -# FRAMAC_TIMEOUT) is not, so the whole file still belongs here. -# -# .github/workflows/verify.yml belongs here for the same reason even though -# it never touches a proof: it is what decides, per CI matrix leg, which target -# --target names and whether --changed-since runs at all. A change there -# that breaks the invocation (a mistyped target, a dropped matrix entry, a -# MUTANT_TARGET that stops reaching the script) would otherwise verify -# against whatever proof sources the same PR happens to touch, which is -# nothing when the PR only edits CI. --target already narrows a full-set -# fallback to one shard's own mutations (see the --changed-since block -# below), so this costs each shard its own subset rather than all of them -# apiece. -HARNESS_FILES = { - "scripts/check-mutants.py", - "scripts/verify-mk.py", - "scripts/check-wp-result.py", - "scripts/check-acsl-coverage.py", - "scripts/check-char-signedness.py", - "mk/verify.mk", - "mk/toolchain.mk", - "Makefile", - ".github/workflows/verify.yml", -} - - -def include_closure(cc, src, workdir): - """Files @src pulls in transitively, per the compiler, not per SCAN. - - VERIFY__SCAN is a hand-maintained guess at this, kept in step by - whoever adds a header, which is exactly the kind of thing that goes stale - silently: a proved header gains an include, nobody updates SCAN, and a - mutation touching only the new file is skipped without a diagnostic. -MM - asks the same preprocessor that stands between the source and the proof, - so the two cannot drift apart from each other. - - Returns None, not a partial answer, when the scan itself cannot be - trusted. {src} alone would be a silent narrowing indistinguishable from a - correct closure with no includes, which is exactly the failure mode this - function exists to close for SCAN; failing quietly here would just move - the bug rather than fix it. The caller treats None as grounds to run the - full mutation set, same as an unresolvable --changed-since ref. - """ - out = workdir / "closure.d" - try: - proc = subprocess.run( - cc - + [ - "-I", - str(ROOT / "src"), - "-I", - str(ROOT / "build"), - "-MM", - "-MG", - "-MF", - str(out), - str(ROOT / src), - ], - cwd=ROOT, - stdout=subprocess.DEVNULL, - stderr=subprocess.DEVNULL, - ) - except OSError: - # cc itself does not exist or is not executable. A more certain - # "cannot trust this scan" signal than a non-zero exit, and it must - # fail the same way: return None rather than let the exception - # propagate and crash the whole run instead of falling back. - return None - if proc.returncode != 0 or not out.exists(): - return None - text = out.read_text().replace("\\\n", " ") - if ":" not in text: - # Malformed -MM output. Same reasoning as a non-zero exit: an empty - # dependency list here would look identical to "genuinely no - # includes", so it cannot be told apart from data and must not be - # trusted as one. - return None - deps = text.split(":", 1)[1].split() - rooted = set() - for dep in deps: - p = pathlib.Path(dep) - rooted.add(str(p.relative_to(ROOT)) if p.is_absolute() else dep) - rooted.add(src) - return rooted - - -def target_inputs(cc): - """{target: {files whose change can alter that target's verdict}} from the - compiler's own view of what each proved source includes, or None if any - target's closure could not be trusted. - - Returning None for the whole map rather than {src} for the one broken - target is deliberate: a caller that gets a partial map back has no way to - know which entries are real and which are silently degraded, so the only - honest signal is "scope is unknown, verify everything." - """ - out = {} - with tempfile.TemporaryDirectory() as tmp: - workdir = pathlib.Path(tmp) - for target, src in target_sources().items(): - closure = include_closure(cc, src, workdir) - if closure is None: - return None - out[target] = closure - return out - - def target_sources(): """VERIFY__SRC for every target, as {target: path}.""" return verify_mk.target_sources() @@ -1161,6 +1053,32 @@ def run_mutation(idx, mutation): return "INFRA", "target failed but printed no recognizable verdict" +def pack_targets(targets, buckets): + """@targets split into at most @buckets groups, longest first. + + GitHub bills a job's wall time rounded up to the minute, and a mutation leg + spends about 90 seconds installing Homebrew and restoring a 1 GB opam + switch before it proves anything. Seventeen legs pay that seventeen times + to do about 51 minutes of work; five pay it five times. Measured on a real + full-scope run, that is 85 macOS-minutes against 61. + + Packed by mutation count, which is a rough proxy and known to be rough: + netlinkwalk carries three mutations and the slowest prover time in the set, + because its control proof alone is 92 seconds locally. A cost table would + be exact and would rot the first time a contract changed, so the imbalance + stays and costs a few minutes on whichever bucket draws that target. + """ + counts = collections.Counter(m[0] for m in MUTATIONS) + order = sorted(targets, key=lambda t: (-counts.get(t, 0), t)) + if not order: + return [] + packed = [[] for _ in range(min(buckets, len(order)))] + for target in order: + packed.sort(key=lambda b: sum(counts.get(t, 0) for t in b)) + packed[0].append(target) + return [sorted(b) for b in packed if b] + + def main(): ap = argparse.ArgumentParser() ap.add_argument("--target", help="run only mutations for this target") @@ -1180,6 +1098,16 @@ def main(): metavar="REF", help="only run mutations whose target source differs from REF", ) + # CI groups the matrix with this rather than one leg per target; see + # pack_targets for why, and .github/workflows/verify.yml for the caller. + ap.add_argument( + "--pack", + type=int, + metavar="N", + help="print the named targets packed into at most N whitespace-" + "separated groups, one per line, then exit", + ) + ap.add_argument("targets", nargs="*", help="target names, with --pack") ap.add_argument( "--jobs", type=int, @@ -1196,6 +1124,27 @@ def main(): args = ap.parse_args() cc = shlex.split(args.cc) or ["cc"] + if args.targets and not args.pack: + # Otherwise "check-mutants.py fuse" runs every mutation in the table + # and says nothing about the name it was handed. + print( + f"target names are only read with --pack; use --target for one " + f"target (got {' '.join(args.targets)})", + file=sys.stderr, + ) + return 2 + if args.pack: + if args.pack < 1: + print(f"--pack must be at least 1, got {args.pack}", file=sys.stderr) + return 2 + # No fallback to the full set when no target is named. The caller is + # CI passing the mutation scope, and that scope is empty on most pull + # requests; defaulting to everything there would expand a full matrix + # at exactly the moment the answer was "nothing to do". + for bucket in pack_targets(args.targets, args.pack): + print(" ".join(bucket)) + return 0 + # ThreadPoolExecutor raises on max_workers < 1, which would surface as a # traceback after the argument was already accepted. Reject it here. if args.jobs < 1: @@ -1210,69 +1159,13 @@ def main(): ] selected = [m for _i, m in selected_pairs] - if args.changed_since: - # Two dots, not three. Three-dot asks git for the merge base, which a - # CI shallow clone does not have, and this only ever wanted "which - # proved sources differ between these two trees" anyway. - diff = subprocess.run( - ["git", "diff", "--name-only", args.changed_since, "HEAD"], - cwd=ROOT, - stdout=subprocess.PIPE, - stderr=subprocess.PIPE, - text=True, - ) - if diff.returncode != 0: - # Run everything instead of stopping. Scoping is an optimization, - # so when it cannot tell what is safe to skip the answer is to do - # all of it. Failing the gate here, or skipping silently, both turn - # a speed-up into a correctness problem. - detail = diff.stderr.strip().splitlines() - print( - f" cannot diff against {args.changed_since}, running the full " - f"set ({detail[0] if detail else 'no detail'})" - ) - else: - touched = set(diff.stdout.split()) - if touched & HARNESS_FILES: - print(" harness or proof config changed; running the full set") - touched = None - else: - inputs = target_inputs(cc) - if inputs is None: - # The compiler's include scan itself is what could not be - # trusted, not the diff. Same rule as everywhere else in - # this block: an unknown scope means verify everything. - print( - " cannot determine proof-input closures, running the " - "full set" - ) - touched = None - else: - kept = [ - (i, m) - for i, m in selected_pairs - if inputs.get(m[0], {m[1]}) & touched - ] - skipped = 0 if touched is None else len(selected_pairs) - len(kept) - if touched is not None and skipped: - print( - f" skipping {skipped} mutation(s): target source unchanged " - f"since {args.changed_since}" - ) - if touched is not None: - selected_pairs, selected = kept, [m for _i, m in kept] - if not selected: - print(" no proved source changed; nothing to re-verify") - return 0 - if not selected: - print(f"no mutations for target {args.target!r}", file=sys.stderr) - return 2 - - if args.list: - for target, _src, function, desc, _old, _new in selected: - print(f" verify-{target:<9} {function:<28} {desc}") - return 0 - + # Validate before filtering, not after. This is a MUTATIONS-versus- + # mk/verify.mk consistency check with nothing to do with any diff, and + # running it after the scope filter meant a mutation naming a target the + # makefile does not declare could be filtered away before the check that + # reports it, which the filter then grew a clause to prevent. Hoisted, the + # filter is one membership test and "--list" gets validated too. + # # A mutation must name its target's own source. Naming an included header # instead silently analyzes the wrong file: the run still produces a # verdict, and the verdict means nothing. @@ -1292,6 +1185,35 @@ def main(): print(f" {line}", file=sys.stderr) return 2 + if args.changed_since: + # The mutation question, not the proof one: a diff that only moves + # the machinery deciding which targets run cannot change whether a + # target rejects a broken source. Passing it explicitly keeps a local + # MUTANT_SINCE run answering what CI's mutation matrix answers. + scope = proof_scope.targets_changed_since( + cc, args.changed_since, proof_scope.MUTATION_HARNESS_FILES + ) + if scope is not None: + kept = [(i, m) for i, m in selected_pairs if m[0] in scope] + skipped = len(selected_pairs) - len(kept) + if skipped: + print( + f" skipping {skipped} mutation(s): target source unchanged " + f"since {args.changed_since}" + ) + selected_pairs, selected = kept, [m for _i, m in kept] + if not selected: + print(" no proved source changed; nothing to re-verify") + return 0 + if not selected: + print(f"no mutations for target {args.target!r}", file=sys.stderr) + return 2 + + if args.list: + for target, _src, function, desc, _old, _new in selected: + print(f" verify-{target:<9} {function:<28} {desc}") + return 0 + shutil.rmtree(BUILD, ignore_errors=True) # Clear the logs too, not just the copies: CI uploads this directory as the # artifact a human reads to see WHY something was caught, and a survivor diff --git a/scripts/check-proof-targets.py b/scripts/check-proof-targets.py index 9f9e694a..d714c54c 100755 --- a/scripts/check-proof-targets.py +++ b/scripts/check-proof-targets.py @@ -97,16 +97,17 @@ def workflow_matrix_is_derived(): """Whether the verify-mutants matrix is built from mk/verify.mk. It used to be a hand-kept copy of the target list and this function - compared the two. The copy is gone: a proof-targets job runs - "make print-verify-targets" and the matrix is fromJson of its output, so - the matrix cannot drift from what make generates. What is worth checking + compared the two. The copy is gone: a proof-targets job emits the list + (from "make print-verify-targets", or from proof-scope.py narrowed to what + a pull request's diff can reach) and the matrix is fromJson of its output, + so the matrix cannot drift from what make generates. What is worth checking now is that nobody has quietly gone back to a literal list, which would restore the drift this script exists to prevent. That leaves one gap this cannot see, which make_target_names covers: the matrix faithfully reproduces a target list that silently dropped a block. """ - expected = "${{ fromJson(needs.proof-targets.outputs.targets) }}" + expected = "${{ fromJson(needs.proof-targets.outputs.mutants) }}" text = (ROOT / ".github" / "workflows" / "verify.yml").read_text() # [^\n]* rather than .*, because re.S would run the capture to the end of # the file and accept a literal list here on the strength of an unrelated @@ -134,8 +135,87 @@ def workflow_matrix_is_derived(): return True +def verdict_covers_every_prover_job(): + """Whether the historic check name still covers every job that proves. + + "Frama-C WP proofs (make verify)" aggregated a matrix whose legs ran the + proofs AND their mutations, so a branch rule requiring it enforced both. + Splitting those halves into separate jobs already moved that name once, + and a reviewer had to notice; the next split should not need one. Every + macOS job in the workflow does prover work, so each must be reachable from + that job's needs, or the name goes green without it. + """ + # Regex rather than a YAML parser, matching what this file already does + # above and keeping the lint job free of a PyYAML dependency it does not + # otherwise need. The shapes read here are the ones this workflow uses: + # a two-space job key, and needs as either a scalar or a flow list. + # + # Split the "jobs:" section rather than the whole file, and accept any + # leading identifier character rather than a lower-case letter. A key class + # of [a-z] silently drops a job named "Verify-extra" or "_probe" from BOTH + # sides of the comparison below, so a macOS job the check name does not + # reach reads as no job at all -- the exact miss this function exists to + # make loud. Splitting the whole file also read the sub-keys of "on:", + # "concurrency:" and "permissions:" as jobs. + text = (ROOT / ".github" / "workflows" / "verify.yml").read_text() + section = re.split(r"^jobs:[ \t]*$", text, maxsplit=1, flags=re.M) + if len(section) != 2: + print( + " no top-level 'jobs:' key in .github/workflows/verify.yml", + file=sys.stderr, + ) + return False + blocks = re.split(r"^ (?=[A-Za-z_])", section[1], flags=re.M)[1:] + jobs = {} + for block in blocks: + job = block.split(":", 1)[0] + needs = re.search(r"^ needs:\s*(.+)$", block, re.M) + jobs[job] = { + "name": (re.search(r"^ name:\s*(.+)$", block, re.M) or [None, ""])[1], + "runs-on": (re.search(r"^ runs-on:\s*(.+)$", block, re.M) or [None, ""])[ + 1 + ], + "needs": re.findall(r"[A-Za-z][\w-]*", needs.group(1)) if needs else [], + } + verdict = [j for j, v in jobs.items() if v["name"].endswith("(make verify)")] + if len(verdict) != 1: + print( + " expected exactly one job named '... (make verify)' in " + f".github/workflows/verify.yml, found {verdict}", + file=sys.stderr, + ) + return False + + seen, stack = set(), list(jobs[verdict[0]]["needs"]) + while stack: + job = stack.pop() + if job in seen or job not in jobs: + continue + seen.add(job) + stack.extend(jobs[job]["needs"]) + # Substring, case-folded, rather than a prefix on "macos". The hosted + # runner is "macos-15", but the self-hosted one build.yml already uses is + # the flow list "[self-hosted, macOS, arm64]", which a prefix test reads as + # a non-macOS job and stops enforcing on the day this workflow moves there. + # Over-matching only demands one more "needs" edge; under-matching drops a + # prover job out from under the required check with nothing said. + prover_jobs = {j for j, v in jobs.items() if "macos" in v["runs-on"].lower()} + missing = sorted(prover_jobs - seen) + if missing: + print( + f" {missing} run on macOS but the '{jobs[verdict[0]]['name']}' check " + "does not reach them through needs, so requiring that check would " + "not enforce them", + file=sys.stderr, + ) + return False + return True + + def main(): mk = verify_mk.targets() + if not verdict_covers_every_prover_job(): + return 1 if not workflow_matrix_is_derived(): return 2 diff --git a/scripts/check-skill-refs.py b/scripts/check-skill-refs.py index afd4490e..5a48e4ec 100755 --- a/scripts/check-skill-refs.py +++ b/scripts/check-skill-refs.py @@ -402,12 +402,16 @@ def check_file(path, paths, targets, skills, errors): ), ( "section attributed to the wrong doc", - '`docs/internals.md` has it and `docs/testing.md`, section ' + "`docs/internals.md` has it and `docs/testing.md`, section " '"Memory Layout", does not.', "no section", ), ("unknown sibling skill", "See the `elfuse-nope` skill.", "refers to skill"), - ("unresolvable shorthand", "Helpers in `fd.c/h` classify it.", "write `fd.c` and `fd.h`"), + ( + "unresolvable shorthand", + "Helpers in `fd.c/h` classify it.", + "write `fd.c` and `fd.h`", + ), ("valid repo path", "See `src/core/guest.c`.", None), ("valid include-style path", "Include it as `core/guest.h`.", None), ("valid system header", "Frama-C cannot model `sys/mount.h`.", None), @@ -476,7 +480,9 @@ def self_test(): total = len(SELF_TEST_CASES) + 1 if failures: - print(f" {len(failures)} of {total} self-test case(s) failed:", file=sys.stderr) + print( + f" {len(failures)} of {total} self-test case(s) failed:", file=sys.stderr + ) for f in failures: print(f" {f}", file=sys.stderr) return 1 diff --git a/scripts/proof-scope.py b/scripts/proof-scope.py new file mode 100755 index 00000000..01050b79 --- /dev/null +++ b/scripts/proof-scope.py @@ -0,0 +1,928 @@ +#!/usr/bin/env python3 +"""Decide which proof targets a set of changed files can affect. + +verify.yml asks this file what to run, so it decides whether a proof runs at +all on a pull request. A target the diff cannot reach keeps the verdict the +base branch already established; a push to the base still proves everything, so +the guarantee on the branch a PR merges into is never the narrowed one. + +Two questions, one code path. Without --mutation the answer is which targets to +prove; with it, which mutation sets to re-run, which a change to the machinery +that only schedules the run cannot alter. See SCHEDULING_FILES. + +Every "cannot tell" answer widens back to the full set. Scoping is an +optimization, and an optimization that guesses turns into a correctness +problem: failing the run, or narrowing on an unverified assumption, are both +worse than proving something twice. + +Two things decide the scope: + + - the include closure of each proved source, per the compiler's own -MM, + unioned with that target's VERIFY__SCAN list and preprocessed with its + VERIFY__CPP_DEFS, so the scan sees what the prover sees; + - HARNESS_FILES and STUB_PREFIX, the inputs no closure can see. + +--self-test pins what can rot in those two. It runs in lint.yml, the one +workflow with no path filter at all, so this file cannot skip the check on +itself. + +Usage: + proof-scope.py --print-targets-changed-since REF [--mutation] + proof-scope.py --self-test +""" + +import argparse +import pathlib +import re +import shlex +import subprocess +import sys +import tempfile + +ROOT = pathlib.Path(__file__).resolve().parent.parent + + +# scripts/ filenames are kebab-case per CLAUDE.md, which no plain "import" +# statement can name, so the shared reader is loaded by path. +def _load_verify_mk(): + import importlib.util + + path = pathlib.Path(__file__).resolve().parent / "verify-mk.py" + spec = importlib.util.spec_from_file_location("verify_mk", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +verify_mk = _load_verify_mk() + + +# Changing any of these can change a verdict for every target, so a run that +# sees one move must not skip anything. mk/toolchain.mk sets CC, which +# check-char-signedness.py compiles with. The individual VERIFY_*_SRC/_SCAN/ +# _FCTS lines in mk/verify.mk are covered separately by target_inputs() below, +# but the rest of that file (the shared recipe, MIN_GOALS, FRAMAC_TIMEOUT) is +# not, so the whole file still belongs here. mk/config.mk defines BUILD_DIR, +# which reaches the prover twice: as -I$(BUILD_DIR) in FRAMAC_CPP_ARGS and as +# the order-only prerequisite every verify rule carries; mk/common.mk is what +# builds that directory. The top-level Makefile owns the include of +# mk/verify.mk, so a Makefile-only diff can break the harness without touching +# any input a closure can see. None of these show up in an include closure. +# +# The scripts, the workflows and the composite actions are derived rather than +# listed: mk/verify.mk's recipes name the checkers they run, and the workflows +# name what they invoke. The rot nothing can catch from the other side is a new +# participant that nobody adds, so each derivation errs wide. The makefile half +# stays hand-listed because $(MAKEFILE_LIST) would pull in +# mk/{shim,tests,lint,...}.mk too, widening for changes that cannot reach a +# proof. +HARNESS_FILES = ( + verify_mk.recipe_scripts() + | verify_mk.proof_actions() + | verify_mk.proof_workflows() + | { + "scripts/verify-mk.py", + "Makefile", + "mk/verify.mk", + "mk/toolchain.mk", + "mk/config.mk", + "mk/common.mk", + } +) + +# The mutation gate asks a narrower question than the proofs: does THIS target +# reject THIS broken source. Two harness files cannot change that answer, so a +# branch touching only those re-proves everything, as it must, without also +# re-running 93 mutations whose sources it never touched. Measured on a real +# run, that half was 51 of the workflow's 85 macOS-minutes. +# +# An exception list, carved out of the set above rather than built beside it, +# because the derivations that fill that set are deliberately wide and this is +# the one place anything narrows. lint.yml runs the self-test and no proof. +# proof-scope.py picks the two matrices; a bug there runs the wrong set of +# targets, which is a scoping failure the self-test guards and a push to main +# corrects, not a wrong verdict about a target that did run. +# +# verify.yml is deliberately NOT here: it carries FRAMAC_TIMEOUT and the make +# invocation for the mutation runs, and check-mutants.py's docstring explains +# why a shorter timeout silently converts a MISS into a "caught". verify-mk.py +# is not here either, since it hands check-mutants.py the per-target source a +# mutation copies and mutates. self_test refuses any scheduling workflow that +# carries a mark of either kind, which is what would have caught verify.yml. +# +# The entry below carries one obligation on this file: nothing a mutation run +# judges by may reach check-mutants.py through it. That is why check-mutants.py +# loads verify-mk.py itself rather than taking proof_scope.verify_mk, which +# would have routed the per-target source table through a file listed here. +SCHEDULING_FILES = { + ".github/workflows/lint.yml", + "scripts/proof-scope.py", +} + +MUTATION_HARNESS_FILES = HARNESS_FILES - SCHEDULING_FILES + +# A file cannot schedule a run and also judge it. These marks are what judging +# looks like in a workflow: a prover budget, a mutation knob, an invocation of +# the proof recipe, or a call into the action that installs the analyzer. +JUDGING_MARKS = ("FRAMAC_", "MUTANT_", "make verify", "uses: ./.github/actions/") + + +def _proof_relevant_names(): + """Variable names whose value can reach the prover. + + A fixpoint, not a union. Start from what mk/verify.mk expands, since that + is the only file the proof recipe reads, then follow definitions: if a name + in the set is assigned somewhere in PROOF_MAKEFILES, whatever that + assignment expands joins the set. BUILD_DIR arrives because the recipe + names it; anything BUILD_DIR is built out of arrives because BUILD_DIR + does. + + Taking the plain union instead was measured and wrong in a way that + defeated the whole point: mk/config.mk references its own test-list + variables, so NATIVE_TESTS, ROSETTA_X86_64_SRCS and TEST_C_SRCS counted as + proof-relevant and any edit to them re-proved all 17 targets. That was 11 + of the 25 remaining full-scope runs over 400 commits. + + The seed is wider than mk/verify.mk for one reason. In the other three + makefiles a reference OUTSIDE an assignment's right-hand side -- in a + conditional, a prerequisite, a recipe -- decides something the fixpoint + cannot follow, because there is no assignment to walk back through. + mk/common.mk's "ifeq ($(V),1)" is what picks Q, which every verify recipe + expands; seeding only from mk/verify.mk would leave V inert and let a "V := + 1" in a sliced file prune that file out of the diff. The test-list + variables stay excluded because they are referenced only from assignment + right-hand sides, which is the whole distinction. + + That seed is deliberately not narrowed to conditionals. CFLAGS and + GENERATED_HEADERS come back with it, off mk/common.mk's compile rule, which + no proof reads; excluding them again means recognizing which rules are on + the proof path, and being wrong there narrows. Paying for a full run on the + rare mk/config.mk CFLAGS edit is the cheaper mistake. + + Still the safe direction where it cannot tell: a name reached only through + a computed reference, $($(VAR)_SRC) and the like, is invisible here, and + the slicer keeps every line it cannot classify anyway. + """ + texts = [re.sub(r"\\\n", " ", (ROOT / mk).read_text()) for mk in PROOF_MAKEFILES] + expands = lambda s: set(re.findall(r"\$[({]([A-Za-z_.][A-Za-z0-9_.-]*)[)}]", s)) + assignment = re.compile( + r"^\s*(?:(?:override|export)\s+)*([A-Za-z_.][A-Za-z0-9_.-]*)" + r"\s*(?::::?=|:=|\+=|\?=|!=|=)(.*)$", + re.M, + ) + + def outside_assignments(text): + """Names expanded anywhere but an assignment's right-hand side. + + The left-hand side counts: a computed name, "$(T)_SRC := ...", is + decided by whatever it expands. + """ + out = set() + for line in text.splitlines(): + m = assignment.match(line) + out |= expands(line[: m.end(1)] if m else line) + return out + + names = expands(texts[0]) + for text in texts[1:]: + names |= outside_assignments(text) + growing = True + while growing: + growing = False + for text in texts: + for m in assignment.finditer(text): + if m.group(1) in names and not expands(m.group(2)) <= names: + names |= expands(m.group(2)) + growing = True + return names + + +def makefile_proof_slice(text): + """The lines of the top-level Makefile a proof can be reached through. + + It is in HARNESS_FILES because it owns which mk/*.mk get read, and a + proof runs inside whatever those set up. That is also ALL it owns here: + the file uses BUILD_DIR and CC but defines neither, and its own nine + assignments (SRCS, OBJS, the dispatch generator, the test cross-compile + flags) are the elfuse build, which no proof reads. + + Treating every edit to it as proof-relevant was measured: over 400 + commits, 46 touched the Makefile and it was the sole reason 36 of them + re-proved all 17 targets, each a rule for a new test binary or a source + added to SRCS. That is 60 percent of the full-scope runs, bought by a + file whose proof surface is nine include lines. + + So the entry stays and the question narrows: did the part a proof can + reach change? The variable names come from mk/verify.mk rather than a + list here, so a recipe that starts reading something new is covered + without anyone remembering this function exists. + + Kept by exclusion rather than by recognition, which is the whole point. + An earlier version listed the constructs that count (include lines, + assignments) and dropped everything else, so every make directive it had + not thought of read as inert: "SHELL := /bin/sh", ".ONESHELL:", a + define/endef body, an "ifeq" flipped around an assignment the prover + reads. Each changes how "make verify-" runs while leaving the slice + byte-identical, which prunes the file and narrows the scope to nothing. + Listing what is PROVABLY inert instead puts the unrecognized line in the + slice, so the failure direction matches the rest of this file. + """ + read_by_verify = _proof_relevant_names() + # The assignment forms make accepts, not just the plain ones: "override", + # "export" and "unexport" can prefix any of them, and != assigns the output + # of a shell command. An "override FRAMAC_TIMEOUT := 1" this failed to + # parse would land in the slice rather than out of it, but the name is what + # decides inertness, so it has to be read correctly either way. + # + # Non-greedy on the name, because make does not require the space: a greedy + # class reads "CFLAGS+=-O2" as a variable literally called "CFLAGS+", which + # is in no proof makefile, so the line reads as inert and drops out. + assign = re.compile( + r"^\s*(?:(?:override|export|unexport)\s+)*([^\s:=]+?)\s*" + r"(?::::?=|:=|\+=|\?=|!=|=)" + ) + rule = re.compile(r"^[^\t#][^:=]*:(?!=)") + + def inert_name(name): + """Whether an assignment to @name can be ignored. + + A name no proof makefile ever expands cannot reach the prover. make's + own specials are the exception: nothing writes "$(SHELL)", yet it + decides which shell every verify recipe runs under. Dotted names go + the same way, .DEFAULT_GOAL included. + """ + return not ( + name in read_by_verify + or name.startswith(".") + or name in ("SHELL", "VPATH", "MAKEFILES", "GNUMAKEFLAGS") + ) + + kept = [] + # Continuations joined first, so a wrapped SRCS list is one logical line + # rather than a head this classifies and a tail it cannot. + for line in re.sub(r"\\\n", " ", text).splitlines(): + stripped = line.strip() + # Blank, comment, or a recipe body. A recipe under a rule this already + # calls inert cannot reach a proof either. + if not stripped or stripped.startswith("#") or line.startswith("\t"): + continue + head = assign.match(line) + if head: + if inert_name(head.group(1)): + continue + kept.append(line.rstrip()) + continue + if rule.match(line): + target, _, tail = line.partition(":") + # A target-specific override assigns for one rule, and + # "verify-fuse: FRAMAC_TIMEOUT := 1" reaches that proof with no + # line-initial assignment to see. + specific = assign.match(tail) + if specific and not inert_name(specific.group(1)): + kept.append(line.rstrip()) + continue + # .ONESHELL and .DELETE_ON_ERROR change how every recipe runs; + # .PHONY is excluded because it names what is already a rule and + # grows with every build target anyone adds. + names = target.split() + if any(n.startswith(".") and n != ".PHONY" for n in names): + kept.append(line.rstrip()) + continue + # Not blank, not a comment, not a recipe, not an assignment this can + # read, not a rule: an include, a conditional, a define, a vpath, or + # something make grew since. Unrecognized means kept. + kept.append(line.rstrip()) + # In source order, deliberately. Sorting would hide a reordering, and the + # order is load-bearing: mk/verify.mk expands "| $(BUILD_DIR)" as its rule + # is read, so moving that include above mk/config.mk leaves the prerequisite + # empty while every line of the file stays byte-identical. + return kept + + +# Harness files whose relevance is a question about content rather than about +# the path. Every other entry widens on any change, which is the safe default; +# these earn the exception by having a surface small enough to state exactly. +# +# mk/config.mk qualifies for the same reason and through the same slicer: it +# defines no rules at all, so everything a proof can reach in it is an +# assignment of a name mk/verify.mk reads (BUILD_DIR, RED, RESET). mk/common.mk +# does NOT qualify, and the difference is worth stating: it owns the +# "$(BUILD_DIR):" rule that every verify target carries as an order-only +# prerequisite, and a slicer reading assignments would not see that recipe +# change. +# +# The completeness of both rests on one condition the self-test checks: neither +# file may define a target the verify rules depend on, or a change to that +# recipe would reach a proof without touching a line the slicer reads. +CONTENT_SENSITIVE = { + "Makefile": makefile_proof_slice, + "mk/config.mk": makefile_proof_slice, +} + +# What "$(VERIFY_RULES): check-stub-constants | $(BUILD_DIR)" in mk/verify.mk +# names. A content-sensitive file that started defining one of these would put +# its recipe on the proof path. +VERIFY_PREREQUISITES = ("check-stub-constants", "$(BUILD_DIR)") + +# The makefiles a proof runs inside. Their variable references are what the +# slicer treats as proof-relevant names, and taking all four rather than +# mk/verify.mk alone is what covers a value that reaches the prover through +# another file. +PROOF_MAKEFILES = ("mk/verify.mk", "mk/toolchain.mk", "mk/common.mk", "mk/config.mk") + +# What the top-level Makefile includes, split by whether it can reach a proof. +# The inert half builds the shim, the tests, the linters and the help text; a +# proof reads none of them. +# +# The Makefile itself widens through HARNESS_FILES, so this split is not what +# decides a Makefile diff. It exists for the next makefile: a new mk/*.mk gets +# edited on its own later, without the Makefile in the same diff, and if it can +# reach a proof and is not in HARNESS_FILES the scope silently narrows. The +# self-test refuses to pass until a new include is classified one way or the +# other, which is the only moment anyone has the context to do it. +MAKEFILE_PROOF_INCLUDES = { + "mk/toolchain.mk", + "mk/config.mk", + "mk/common.mk", + "mk/verify.mk", +} +MAKEFILE_INERT_INCLUDES = { + "mk/shim.mk", + "mk/tests.mk", + "mk/lint.mk", + "mk/format.mk", + "mk/help.mk", +} + +# The stub headers reach every proof and no include closure can see them: they +# arrive through -include and -I$(FRAMAC_STUB_DIR) in FRAMAC_CPP_ARGS, which +# the -MM scan below (plain -Isrc -Ibuild) does not reproduce. A wrong constant +# there changes what every target reasons about, so a change under the +# directory widens the scope the same way mk/verify.mk does. The name comes +# from mk/verify.mk so a rename cannot leave this pointing at nothing. +STUB_PREFIX = verify_mk.stub_dir().rstrip("/") + "/" + + +def make_words(text): + """The words of a make dependency list, honoring backslash escapes. + + -MM writes a path holding a space as "with\\ space", so splitting on + whitespace tears it into two words that match no file. That direction is + the dangerous one: the real path drops out of the closure, and the target + stops being selected by a diff that touches it. Same reasoning as the -z + on the git diff below. + + The repository has no such path today. A checkout under one does, which is + ordinary on macOS, and this function is reading absolute paths built from + that checkout's location. + """ + return [w.replace("\\ ", " ") for w in re.findall(r"(?:[^\s\\]|\\.)+", text)] + + +def include_closure(cc, src, workdir, defs=()): + """Files @src pulls in transitively, per the compiler, not per SCAN. + + VERIFY__SCAN is a hand-maintained guess at this, kept in step by + whoever adds a header, which is exactly the kind of thing that goes stale + silently: a proved header gains an include, nobody updates SCAN, and a + change touching only the new file selects no target without a diagnostic. + -MM asks the same preprocessor that stands between the source and the + proof, so the two cannot drift apart from each other. + + Returns None, not a partial answer, when the scan itself cannot be + trusted. {src} alone would be a silent narrowing indistinguishable from a + correct closure with no includes, which is exactly the failure mode this + function exists to close for SCAN; failing quietly here would just move + the bug rather than fix it. The caller treats None as grounds to run + everything, same as an unresolvable ref. + + @defs carries the target's VERIFY__CPP_DEFS. The prover preprocesses + with them, so an include sitting behind one is a real input; scanning + without them would report a closure for a file the proof never sees. + """ + # -Isrc and -Ibuild are spelled here rather than read out of + # FRAMAC_CPP_ARGS, and the rest of that variable is deliberately not + # reproduced: -nostdinc and Frama-C's modeled libc only change which SYSTEM + # headers resolve, which -MM drops anyway, and the two -include stubs are + # covered by STUB_PREFIX widening instead. That leaves the two project + # include roots, whose names live in mk/config.mk (BUILD_DIR) and + # mk/verify.mk. Both are in HARNESS_FILES, so a rename of either widens the + # scope to everything on the commit that makes this copy stale. + out = workdir / "closure.d" + try: + proc = subprocess.run( + cc + + list(defs) + + [ + "-I", + str(ROOT / "src"), + "-I", + str(ROOT / "build"), + "-MM", + "-MG", + "-MF", + str(out), + str(ROOT / src), + ], + cwd=ROOT, + stdout=subprocess.DEVNULL, + stderr=subprocess.DEVNULL, + ) + except OSError: + # cc itself does not exist or is not executable. A more certain + # "cannot trust this scan" signal than a non-zero exit, and it must + # fail the same way: return None rather than let the exception + # propagate and crash the whole run instead of falling back. + return None + if proc.returncode != 0 or not out.exists(): + return None + text = out.read_text().replace("\\\n", " ") + if ":" not in text: + # Malformed -MM output. Same reasoning as a non-zero exit: an empty + # dependency list here would look identical to "genuinely no + # includes", so it cannot be told apart from data and must not be + # trusted as one. + return None + deps = make_words(text.split(":", 1)[1]) + rooted = set() + for dep in deps: + p = pathlib.Path(dep) + if not p.is_absolute(): + rooted.add(dep) + continue + try: + rooted.add(str(p.relative_to(ROOT))) + except ValueError: + # Absolute and outside the tree, which -MM is not supposed to + # report but a toolchain wrapper or a symlinked include path can + # still produce. Dropping it loses nothing, since the caller only + # ever intersects this set with "git diff --name-only" output and + # no path outside the repo can appear there. Raising, which is what + # relative_to does unguarded, would crash the run instead of + # falling back. + continue + rooted.add(src) + return rooted + + +def target_closures(cc): + """{target: {file}} straight from the compiler, or None if any target's + closure could not be trusted. + + Returning None for the whole map rather than {src} for the one broken + target is deliberate: a caller that gets a partial map back has no way to + know which entries are real and which are silently degraded, so the only + honest signal is "scope is unknown, verify everything." + + Kept separate from target_inputs so the self-test can compare SCAN against + what the compiler actually reported. Asking that question of the unioned + map is a tautology, which is how the first version of that assertion + passed while a deliberately broken SCAN list was in place. + """ + out = {} + defs = verify_mk.target_cpp_defs() + with tempfile.TemporaryDirectory() as tmp: + workdir = pathlib.Path(tmp) + for target, src in verify_mk.target_sources().items(): + closure = include_closure(cc, src, workdir, defs.get(target, ())) + if closure is None: + return None + out[target] = closure + return out + + +def target_inputs(cc, closures=None): + """{target: {files whose change can alter that target's verdict}}, or None. + + The closure, unioned with VERIFY__SCAN rather than trusting the closure + alone. SCAN is what check-acsl-coverage.py reads inside the verify- + recipe, and nothing requires it to be a subset of what the source includes. + It is one today for all 17 targets, which the self-test asserts against the + raw closures; the union is what keeps a future entry outside the closure + widening the scope instead of vanishing from it. + """ + if closures is None: + closures = target_closures(cc) + if closures is None: + return None + scans = verify_mk.target_scans() + return {t: files | set(scans.get(t, [])) for t, files in closures.items()} + + +def targets_changed_since(cc, ref, harness=None): + """The targets a diff against @ref can affect, or None when the scope + cannot be determined and everything has to run. + + @harness selects the question: HARNESS_FILES asks which proofs to run, + MUTATION_HARNESS_FILES which mutation sets to run. The difference is the + scheduling files, which pick what runs without deciding what it concludes. + + Diagnostics go to stderr so the caller that prints the target names can be + read by a machine. + """ + # Two dots, not three. Three-dot asks git for the merge base, which a CI + # shallow clone does not have, and this only ever wanted "which proved + # sources differ between these two trees" anyway. + # + # -z, so a path is delimited by NUL and arrives raw. Without it git applies + # core.quotePath and renders a non-ASCII name as an escaped C string, and + # splitting on whitespace tears a name containing a space in half; either + # one matches no closure entry, which drops the target from the scope + # silently. That is the one direction this file must not fail in. + diff = subprocess.run( + ["git", "diff", "--name-only", "-z", ref, "HEAD"], + cwd=ROOT, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + text=True, + ) + if diff.returncode != 0: + detail = diff.stderr.strip().splitlines() + print( + f" cannot diff against {ref}, running the full set " + f"({detail[0] if detail else 'no detail'})", + file=sys.stderr, + ) + return None + touched = set(diff.stdout.split("\0")) - {""} + return scope_from_touched(cc, prune_inert_content(ref, touched), harness=harness) + + +def prune_inert_content(ref, touched): + """@touched without the content-sensitive files whose proof slice is the + same at @ref as it is now. + + Cannot tell keeps the file, as everywhere else here: an unreadable base + version, or a slicer that raises, leaves the path in and the scope wide. + """ + keep = set(touched) + for path, slicer in CONTENT_SENSITIVE.items(): + if path not in keep: + continue + old = subprocess.run( + ["git", "show", f"{ref}:{path}"], + cwd=ROOT, + stdout=subprocess.PIPE, + stderr=subprocess.DEVNULL, + text=True, + ) + if old.returncode != 0: + continue + try: + unchanged = slicer(old.stdout) == slicer((ROOT / path).read_text()) + except Exception: + # The docstring promises that cannot-tell keeps the file, and a + # slicer that raises is cannot-tell however it raised: an + # unreadable file is OSError, a version of the file this cannot + # parse is whatever the slicer chose. Narrowing this to one + # exception type would turn the rest into a crash, which is the + # one thing worse than proving something twice. + continue + if unchanged: + keep.discard(path) + print( + f" {path} changed, but not the part a proof reads", + file=sys.stderr, + ) + return keep + + +def scope_from_touched(cc, touched, inputs=None, verbose=True, harness=None): + """The proof targets @touched can affect, or None for "run everything". + + Split from targets_changed_since so the decision can be exercised with a + synthetic file set; see self_test. @inputs is an already-built closure map, + since building one costs a compiler run per target. + """ + harness = HARNESS_FILES if harness is None else harness + if touched & harness or any(f.startswith(STUB_PREFIX) for f in touched): + if verbose: + print( + " harness or proof config changed; running the full set", + file=sys.stderr, + ) + return None + if inputs is None: + inputs = target_inputs(cc) + if inputs is None: + # The compiler's include scan itself is what could not be trusted, + # not the diff. Same rule: an unknown scope means verify + # everything. + if verbose: + print( + " cannot determine proof-input closures, running the full set", + file=sys.stderr, + ) + return None + return {target for target, files in inputs.items() if files & touched} + + +def makefile_includes(): + """Every makefile the build reads, per the makefiles themselves. + + Reads the top-level Makefile AND mk/*.mk, because an include one level + down is the direction that rots: a new mk/verify-extra.mk pulled in by + mk/verify.mk would reach a proof while being invisible to a scan of the + top-level file alone. + + Not "make -pn" or $(MAKEFILE_LIST), which resolve computed includes this + cannot. mk/common.mk ends with "-include $(wildcard $(BUILD_DIR)/*.d)", so + make's answer is whatever .d files that tree happens to have built: dozens + on a developer machine, none on a fresh CI checkout. A check whose result + depends on whether someone has run make is not a check. Computed paths are + skipped here for the same reason, and are the one thing this cannot see. + + Handles the forms make accepts and this tree does not use yet, since each + one missed is an include the caller silently declines to classify: the + optional -include and its sinclude synonym, several files on one line, a + trailing comment, and a backslash continuation. + """ + out = set() + for path in [ROOT / "Makefile"] + sorted((ROOT / "mk").glob("*.mk")): + text = re.sub(r"\\\n", " ", path.read_text()) + for line in re.findall(r"^\s*[-s]?include\s+([^#\n]*)", text, re.M): + out.update(w for w in line.split() if "$" not in w) + return out + + +def self_test(cc): + """Assert the scoping decision still answers the cases CI relies on. + + This file decides whether the proofs run at all, and every neighbour + (check-proof-targets, check-acsl-coverage, check-wp-result, the mutation + gate itself) exists because a hand-kept list was judged likely to rot. + HARNESS_FILES is exactly such a list. + + Only cases that can actually fail. Asking whether most harness paths widen, + or whether a target's own source selects it, are tautologies over the code + above: the first is the set membership the function tests, and the second + holds because include_closure ends by adding src. Assertions that cannot + fail read as coverage and are not. + + One named check per invariant below, each returning what it found, because + this grew to a dozen groups spanning five different questions and a reader + could no longer tell which line belonged to which claim. + """ + closures = target_closures(cc) + if closures is None: + print( + " cannot determine proof-input closures; the self-test has " + "nothing to check", + file=sys.stderr, + ) + return 1 + inputs = target_inputs(cc, closures) + scans = verify_mk.target_scans() + includes = makefile_includes() + bad = ( + _harness_paths_resolve() + + _scans_stay_inside_their_closure(scans, closures) + + _makefile_includes_are_classified(includes) + + _scheduling_files_do_not_judge() + + _content_slicers_cut_where_they_claim() + + _scope_answers_its_boundary_cases(cc, inputs) + ) + if bad: + print(" proof-scope self-test failed:", file=sys.stderr) + for line in bad: + print(f" {line}", file=sys.stderr) + return 1 + print( + f" scope self-test: {len(HARNESS_FILES)} harness path(s), " + f"{len(scans)} SCAN list(s), {len(includes)} makefile include(s), " + f"1 Makefile case, 1 inert case" + ) + return 0 + + +def _harness_paths_resolve(): + """Every harness path names something, and the derivation still finds the + workflows the hand-kept floor names.""" + bad = [] + for harness in sorted(HARNESS_FILES): + if not (ROOT / harness).exists(): + bad.append(f"{harness}: named in HARNESS_FILES but not in the tree") + # Not "the floor is in HARNESS_FILES", which is true by construction since + # the union that builds that set includes the floor. What can fail, and + # what the floor is there to absorb, is the derivation losing a workflow it + # used to find: the scope stays correct and nobody learns the marks rotted. + undiscovered = sorted( + verify_mk.KNOWN_PROOF_WORKFLOWS - verify_mk.discovered_proof_workflows() + ) + if undiscovered: + bad.append( + f"{undiscovered}: only the hand-kept floor still finds these, so the " + f"marks in verify-mk.py no longer match what they invoke" + ) + if not (ROOT / STUB_PREFIX).is_dir(): + bad.append(f"{STUB_PREFIX}: FRAMAC_STUB_DIR is not a directory") + return bad + + +def _scans_stay_inside_their_closure(scans, closures): + """SCAN is unioned into the closure, so an entry outside it widens the + scope rather than vanishing from it. + + That is the right failure direction and it hides the failure. If this ever + fires, check-acsl-coverage.py is reading a file the prover does not + preprocess, so it is checking contracts no proof consumes. + """ + bad = [] + for target, scanned in sorted(scans.items()): + stray = sorted(set(scanned) - closures.get(target, set())) + if stray: + bad.append(f"{target}: VERIFY_SCAN names {stray}, outside its closure") + return bad + + +def _makefile_includes_are_classified(includes): + """Every makefile the build reads is either proof-reaching or inert, and + the proof-reaching ones are harness paths. + + Classifying one as proof-reaching and then leaving it out of the harness + set is the way the split gets filled in wrong: the entry reads as handled + while the scope still narrows on it. + """ + bad = [] + unclassified = sorted(includes - MAKEFILE_PROOF_INCLUDES - MAKEFILE_INERT_INCLUDES) + if unclassified: + bad.append( + f"the build includes {unclassified}, which HARNESS_FILES has not " + f"classified as reaching a proof or not" + ) + unlisted = sorted(MAKEFILE_PROOF_INCLUDES - HARNESS_FILES) + if unlisted: + bad.append(f"{unlisted}: classified as reaching a proof, but not harness paths") + return bad + + +def _scheduling_files_do_not_judge(): + """The scheduling exceptions are the one narrowing decision a human makes + here, so they are checked rather than trusted. + + An earlier version of the list held verify.yml, which carries + FRAMAC_TIMEOUT and the mutation invocation, and a reviewer had to catch it. + A mark scan catches the next one at the moment it is written. + + Workflows only: proof-scope.py names FRAMAC_TIMEOUT in its own prose, and a + script that talks about the marks is not a script that carries them. + """ + bad = [] + for sched in sorted(f for f in SCHEDULING_FILES if f.startswith(".github/")): + path = ROOT / sched + if not path.exists(): + continue + carried = sorted(m for m in JUDGING_MARKS if m in path.read_text()) + if carried: + bad.append( + f"{sched}: carries {carried}, so it judges rather than schedules" + ) + return bad + + +def _content_slicers_cut_where_they_claim(): + """The content-sensitive entries narrow rather than widen, the direction + this file otherwise never goes, so their slicers are exercised. + + Two conditions their completeness rests on come first: the file must not + define a verify rule, whose recipe a slicer reading values cannot see, nor + a target the verify rules depend on. + """ + bad = [] + for path, slicer in sorted(CONTENT_SENSITIVE.items()): + text = (ROOT / path).read_text() + # Every target on a rule line, not just one alone at column 0: + # "foo check-stub-constants:" defines it too, and ${BUILD_DIR} is the + # same variable as $(BUILD_DIR) to make. + defined = set() + for line in text.splitlines(): + head = re.match(r"^([^\t#][^:=]*):(?!=)", line) + if head: + defined.update(head.group(1).split()) + proof_rules = sorted(d for d in defined if d.startswith("verify")) + if proof_rules: + bad.append( + f"{path}: defines {proof_rules}, and a slicer that reads values " + f"cannot see what a recipe does" + ) + for prereq in VERIFY_PREREQUISITES: + braced = prereq.replace("$(", "${").replace(")", "}") + if defined & {prereq, braced}: + bad.append( + f"{path}: defines {prereq}, which a verify rule depends on, " + f"so reading only its assignments is no longer enough" + ) + # A computed reference is outside what the name fixpoint can follow, so + # an assignment reached only that way would be called inert. No + # content-sensitive file constructs a name today; the day one does, + # this says so rather than narrowing quietly. + computed = [ + line.strip() for line in text.splitlines() if "$($" in line or "${$" in line + ] + if computed: + bad.append( + f"{path}: builds a variable name at {computed[:1]}, which the " + f"relevant-name fixpoint cannot follow" + ) + if not slicer(text): + bad.append(f"{path}: its proof slice is empty, so no edit can widen") + # What must stay out, which is the entire benefit: a rule for one more + # test binary and one more source on the build's own list were between + # them the sole reason 36 of 46 Makefile commits re-proved everything. + for inert, why in ( + ("$(BUILD_DIR)/test-probe: ; @true", "a build rule"), + ("SRCS += syscall/probe.c", "a source on the build's list"), + (".PHONY: probe", "a phony declaration"), + ): + if slicer(text + "\n" + inert + "\n") != slicer(text): + bad.append(f"{path}: {why} moved its proof slice") + # What must move. Each of these changes how "make verify-" runs while + # every line a slice built by recognizing assignments would read stays + # byte-identical; that slice missed the first four. + for relevant, why in ( + ("SHELL := /bin/sh", "a shell override"), + (".ONESHELL:", "a recipe-execution special target"), + ("define FRAMAC_CPP_ARGS\n-nostdinc\nendef", "a define block"), + ("ifdef PROBE\nendif", "a conditional"), + # No space around the operator, which make accepts and a greedy + # name class reads as a different variable entirely. + ("CPP_DEFS+=-DPROBE", "a spaceless append to a name a proof reads"), + ("include mk/probe.mk", "a new include"), + ("override FRAMAC_TIMEOUT := 1", "an override assignment"), + ("verify-probe: FRAMAC_TIMEOUT := 1", "a target-specific override"), + ("vpath %.h src/proved", "a vpath directive"), + ("unexport CC", "an unexport"), + ): + if slicer(text + "\n" + relevant + "\n") == slicer(text): + bad.append(f"{path}: {why} did not move its proof slice") + shuffled = list(reversed(slicer(text))) + if shuffled != slicer(text) and sorted(shuffled) == sorted(slicer(text)): + if slicer("\n".join(shuffled)) == slicer(text): + bad.append(f"{path}: reordering its slice lines did not move it") + return bad + + +def _scope_answers_its_boundary_cases(cc, inputs): + """The three end-to-end answers the CI jobs are built on. + + A harness path widens, prose selects nothing, and prune_inert_content keeps + what it cannot read. That last one is the only path in this file that takes + a harness entry OUT of a diff, so its cannot-tell direction is exercised + rather than inferred from the slicers. + """ + bad = [] + makefile_scope = scope_from_touched(cc, {"Makefile"}, inputs, verbose=False) + if makefile_scope is not None: + bad.append(f"Makefile: selects {sorted(makefile_scope)}, expected full set") + kept = prune_inert_content( + "no-such-ref-proof-scope-self-test", set(CONTENT_SENSITIVE) + ) + dropped = sorted(set(CONTENT_SENSITIVE) - kept) + if dropped: + bad.append(f"{dropped}: pruned against a ref whose version cannot be read") + inert = scope_from_touched(cc, {"README.md"}, inputs) + if inert != set(): + bad.append(f"README.md: selects {sorted(inert) if inert else 'everything'}") + return bad + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument( + "--print-targets-changed-since", + metavar="REF", + help="print the proof targets a diff against REF can affect, one per " + "line (every target when the scope cannot be determined)", + ) + ap.add_argument( + "--mutation", + action="store_true", + help="answer for the mutation gate instead, which a change to the " + "scheduling machinery cannot affect", + ) + ap.add_argument( + "--self-test", + action="store_true", + help="assert the scoping still answers its boundary cases", + ) + # Split rather than exec directly, since CC is routinely a wrapper or + # carries flags ("ccache clang", "cc -DTEST"). The default is right for the + # include scan: it only walks #include lines, which every C preprocessor + # agrees on, unlike check-char-signedness.py where the exact CC matters. + ap.add_argument("--cc", default="cc", help="compiler for the include scan") + args = ap.parse_args() + cc = shlex.split(args.cc) or ["cc"] + + if args.self_test: + return self_test(cc) + if args.print_targets_changed_since: + harness = MUTATION_HARNESS_FILES if args.mutation else HARNESS_FILES + scope = targets_changed_since(cc, args.print_targets_changed_since, harness) + for target in sorted(verify_mk.target_sources() if scope is None else scope): + print(target) + return 0 + ap.error("nothing to do: pass --self-test or --print-targets-changed-since") + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/scripts/verify-mk.py b/scripts/verify-mk.py index 3fe4639e..334ee774 100644 --- a/scripts/verify-mk.py +++ b/scripts/verify-mk.py @@ -17,6 +17,10 @@ ROOT = pathlib.Path(__file__).resolve().parent.parent VERIFY_MK = ROOT / "mk" / "verify.mk" +KNOWN_PROOF_WORKFLOWS = { + ".github/workflows/lint.yml", + ".github/workflows/verify.yml", +} def text(): @@ -29,20 +33,178 @@ def joined_text(): return re.sub(r"\\\n", " ", text()) +def _target_var(suffix): + """{target: [word]} for every VERIFY__, target lowercased. + + The name class matches what make accepts: its own target list comes from + $(patsubst VERIFY_%_SRC,%,...), and % spans digits and underscores too. A + narrower pattern here would drop such a target silently, taking it out of + every consumer while make still proved it. That reasoning is why this + pattern lives once rather than once per accessor. + + Reads the continuation-joined text, since a list assignment can wrap. + """ + return { + m.group(1).lower(): m.group(2).split() + for m in re.finditer( + rf"^VERIFY_([A-Z0-9_]+)_{suffix}\s*:=\s*(.*)$", joined_text(), re.M + ) + } + + def target_sources(): """{target: source path} for every VERIFY__SRC, target lowercased. - The name class matches what make accepts: its own list comes from - $(patsubst VERIFY_%_SRC,%,...), and % spans digits and underscores too. A - narrower pattern here would drop such a target silently, taking its source - and its mutations out of every consumer while make still proved it. + One source per target, and a second one is an error rather than a + truncation. make would accept "VERIFY_X_SRC := a.c b.c" and hand both to + the prover, so keeping the first word would drop the second out of every + consumer: out of the include closure, out of the CI scope, out of the + mutation runner's idea of what the target analyzes. That is the silent + narrowing this module exists to prevent, so it fails loudly instead. + Supporting several sources means teaching those consumers first. + """ + out = {} + for target, words in _target_var("SRC").items(): + if len(words) != 1: + raise RuntimeError( + f"VERIFY_{target.upper()}_SRC names {words}; every consumer of " + f"this table assumes exactly one source" + ) + out[target] = words[0] + return out + + +def target_scans(): + """{target: [scanned path]} for every VERIFY__SCAN, target lowercased.""" + return _target_var("SCAN") + + +def target_cpp_defs(): + """{target: [preprocessor flag]} for every VERIFY__CPP_DEFS. + + These reach the prover through FRAMAC_CPP_ARGS, so a header included behind + one of them is part of the target's real input set. Anything reconstructing + that set with its own preprocessor has to pass them or it sees a different + file. + """ + return _target_var("CPP_DEFS") + + +def recipe_scripts(): + """The scripts/*.py files mk/verify.mk names, recipes and comments alike. + + Every script a recipe runs can change a proof's verdict, and none can + appear in an include closure, so a scoping decision has to widen when one + changes. Read rather than hand-listed for the same reason as stub_dir: the + direction that rots is a NEW script wired into a recipe and forgotten, + which no test can catch from the other side, because nothing distinguishes + "not listed" from "cannot affect a proof". + + Matching a mention rather than an invocation is deliberate. Telling the two + apart means parsing recipe lines, and being wrong there drops a script, + which narrows. Being wrong the way this is wrong adds a script named only + in a comment, which widens. Only one of those two errors is safe. """ + return set(re.findall(r"scripts/[A-Za-z0-9._-]+\.py", text())) + + +def discovered_proof_workflows(): + """The .github/workflows files whose text names the proof machinery. + + A workflow that names this module, proof-scope.py, the target list, or a + verify target either decides which proofs run or checks the thing that + decides. Both can change a proof's verdict without touching any file an + include closure can see, and both are invisible from the other side: a + THIRD workflow that starts running one of these is exactly what nobody + remembers to add to a hand-kept list. Same reasoning, and same safe + direction, as recipe_scripts: matching a mention over-widens at worst. + + KNOWN_PROOF_WORKFLOWS is the floor, because the two mechanisms fail in + opposite directions. The marks are matched against YAML and prose, so + rewording an invocation, or moving it behind a variable, could silently + drop a participant; the floor cannot. A hand-kept floor in turn cannot + grow by itself, which is what the derivation is for. Renaming one of the + two files is the case the floor makes loud rather than silent: the entry + stops naming a file in the tree, and the self-test in proof-scope.py + fails on it instead of quietly scoping without it. + """ + marks = ( + "scripts/proof-scope.py", + "scripts/verify-mk.py", + "print-verify-targets", + "make verify", + ) + # Both extensions: Actions accepts .yaml as readily as .yml, and a proof + # workflow written with the other one would be discovered by neither the + # glob nor the floor. + workflows = ROOT / ".github" / "workflows" return { - m.group(1).lower(): m.group(2) - for m in re.finditer(r"^VERIFY_([A-Z0-9_]+)_SRC\s*:=\s*(\S+)", text(), re.M) + str(p.relative_to(ROOT)) + for p in sorted(workflows.glob("*.yml")) + sorted(workflows.glob("*.yaml")) + if any(mark in p.read_text() for mark in marks) } +def proof_workflows(): + """discovered_proof_workflows() with the hand-kept floor under it. + + Callers scoping a diff want the union; only the self-test wants the two + apart, so it can say when the derivation has stopped finding what the + floor is quietly carrying. + """ + return KNOWN_PROOF_WORKFLOWS | discovered_proof_workflows() + + +def proof_actions(): + """The composite actions a proof workflow calls. + + One of them installs Frama-C and the provers, so what it does decides what + the prover is: the packages, the switch, the cache key. Nothing here can + appear in an include closure either. + + Derived from the "uses: ./.github/actions/" lines in the workflows + proof_workflows() already returned, rather than from what the directory + happens to hold. A glob would pull in an action added for the build or the + analyzers, and every pull request touching it would then re-prove and + re-mutate everything, which is the cost this scoping exists to avoid. The + fallback keeps the safe direction: a directory with actions in it and no + "uses:" line found means the scan is the thing that broke, so widen. + """ + used = set() + for wf in proof_workflows(): + path = ROOT / wf + if not path.exists(): + continue + used.update( + re.findall( + r"uses:\s*\./(\.github/actions/[A-Za-z0-9._/-]+)", path.read_text() + ) + ) + present = { + str(p.relative_to(ROOT)) + for p in sorted((ROOT / ".github" / "actions").rglob("action.y*ml")) + } + named = {a for a in present if any(a.startswith(u + "/") or a == u for u in used)} + return named if named or not present else present + + +def stub_dir(): + """FRAMAC_STUB_DIR, the directory holding the analyzer's stub headers. + + Read rather than hardcoded by the consumer: those headers reach every + proof through -include and -I, where no include scan can see them, so a + scoping decision has to widen on any change under this directory. A copy + of the name elsewhere would keep pointing at the old one after a rename + and stop widening, silently. + """ + m = re.search(r"^FRAMAC_STUB_DIR\s*:=\s*(\S+)", text(), re.M) + if not m: + # Loud on purpose. A default here would be a guess about the very path + # a caller uses to decide what to re-verify. + raise RuntimeError("FRAMAC_STUB_DIR not found in mk/verify.mk") + return m.group(1) + + def targets(): """The proof target names, lowercased.""" return set(target_sources()) diff --git a/src/syscall/asyncio.c b/src/syscall/asyncio.c index 64e228e2..d3059e04 100644 --- a/src/syscall/asyncio.c +++ b/src/syscall/asyncio.c @@ -105,10 +105,10 @@ static void async_deliver(void *udata, int signum) if (!async_owner_is_local(snap.fasync_owner_type, snap.fasync_owner)) return; /* no owner, or a foreign guest pid */ - /* ponytail: owner delivery is process-wide. F_OWNER_TID does not target a - * single thread and a foreign guest pid is not forwarded across the fork - * IPC boundary. Add per-thread signal queueing + cross-process forwarding - * when a real workload needs directed SIGIO. + /* Owner delivery is process-wide: F_OWNER_TID does not target a single + * thread, and a foreign guest pid is not forwarded across the fork IPC + * boundary. Per-thread signal queueing and cross-process forwarding are + * what a workload needing directed SIGIO would require. */ signal_queue(signum); } @@ -236,9 +236,9 @@ void fasync_owner_set(int guest_fd, fd_table[guest_fd].generation == expect_gen) ofd_id = fd_table[guest_fd].ofd_id; if (ofd_id) { - /* ponytail: O(FD_TABLE_SIZE) scan to reach every alias sharing this - * open-file-description. Cold path (F_SETOWN only); an ofd_id->fd index - * is the upgrade if it ever shows up in a profile. + /* An O(FD_TABLE_SIZE) scan reaches every alias sharing this + * open-file-description. Cold path (F_SETOWN only); an ofd_id to fd + * index is the upgrade if it ever shows up in a profile. */ for (int i = 0; i < FD_TABLE_SIZE; i++) { if (fd_table[i].type == FD_CLOSED || fd_table[i].ofd_id != ofd_id) @@ -286,9 +286,9 @@ void asyncio_apply(int guest_fd, uint64_t expect_gen, bool on) fd_table[guest_fd].generation == expect_gen) ofd_id = fd_table[guest_fd].ofd_id; if (ofd_id) { - /* ponytail: O(FD_TABLE_SIZE) scan to reach every alias sharing this - * open-file-description. Cold path (O_ASYNC toggles only); an - * ofd_id->fd index is the upgrade if it ever shows up in a profile. + /* An O(FD_TABLE_SIZE) scan reaches every alias sharing this + * open-file-description. Cold path (O_ASYNC toggles only); an ofd_id to + * fd index is the upgrade if it ever shows up in a profile. */ for (int i = 0; i < FD_TABLE_SIZE; i++) { if (fd_table[i].type == FD_CLOSED || fd_table[i].ofd_id != ofd_id)