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)