From 5108df30dfc7a7ffdd9e0dcadce8a7b2e38945a0 Mon Sep 17 00:00:00 2001 From: Chun-Hung Tseng Date: Fri, 14 Aug 2026 11:20:29 +0200 Subject: [PATCH 1/5] Split mk/analysis.mk into three files by concern mk/analysis.mk held three unrelated things in 595 lines: the clang-format and shellcheck file lists, the clang-tidy, scan-build and Infer entry points, and the Frama-C proof targets with the WP machinery that turns them into rules. Branches touching different halves of it still conflict. mk/verify.mk keeps the proofs, mk/lint.mk and mk/format.mk take the rest. The proof target table stays with the machinery rather than becoming a fourth file. VERIFY_TARGETS reads $(.VARIABLES) with :=, so it sees only what make has parsed so far, and check-proof-targets.py catches a VERIFY__SRC block written below that line by comparing the table against "make print-verify-targets". A table in its own file is always parsed first, which makes that comparison unfalsifiable: the check would report success for the one mistake it was written to catch. scripts/analysis-mk.py becomes scripts/verify-mk.py and gains joined_text(), so check-mutants.py and check-char-signedness.py drop the private copies of that reader they each carried and the makefile is named in one place. check-mutants.py's HARNESS_FILES lists mk/verify.mk in place of mk/analysis.mk; mk/format.mk and mk/lint.mk are left out because neither can change a proof verdict, which is what that set selects for. Targets, recipes and variables are unchanged: "make -n verify" prints the same recipe for all seventeen proofs, and "make help" lists the same entries, with print-verify-targets now printing after analyze because the awk scans MAKEFILE_LIST in include order. --- .github/workflows/main.yml | 10 +-- Makefile | 4 +- frama-c-stubs/Hypervisor/Hypervisor.h | 4 +- frama-c-stubs/gcc-atomics.h | 2 +- mk/format.mk | 50 +++++++++++ mk/lint.mk | 56 ++++++++++++ mk/{analysis.mk => verify.mk} | 107 +---------------------- scripts/check-acsl-coverage.py | 2 +- scripts/check-char-signedness.py | 23 +++-- scripts/check-mutants.py | 29 +++--- scripts/check-proof-targets.py | 40 ++++----- scripts/{analysis-mk.py => verify-mk.py} | 29 +++--- 12 files changed, 187 insertions(+), 169 deletions(-) create mode 100644 mk/format.mk create mode 100644 mk/lint.mk rename mk/{analysis.mk => verify.mk} (84%) rename scripts/{analysis-mk.py => verify-mk.py} (53%) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 4d29e126..4043c877 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -6,7 +6,7 @@ # tidy-macos : clang-tidy via `make lint` # verify-mutants: per target, the Frama-C WP proof AND the mutations that # show it bites; one runner per target, sharded from -# mk/analysis.mk's VERIFY__SRC list +# 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 @@ -119,7 +119,7 @@ jobs: run: python3 scripts/gen-syscall-dispatch.py --output "$RUNNER_TEMP/dispatch.h" - name: Proof target consistency - # Three lists name the same proved sources: mk/analysis.mk's targets, + # Three lists name the same proved sources: mk/verify.mk's targets, # the verify-mutants matrix below, 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 @@ -224,7 +224,7 @@ jobs: - name: clang-tidy (make lint) run: make lint - # The proof target list has ONE home, mk/analysis.mk's VERIFY__SRC + # 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. @@ -240,7 +240,7 @@ jobs: - name: Checkout uses: actions/checkout@v7 - - name: Read the targets from mk/analysis.mk + - name: Read the targets from mk/verify.mk id: list run: | set -euo pipefail @@ -273,7 +273,7 @@ jobs: # without a barrier that made every shard wait for the slowest proof. # # The matrix comes from the proof-targets job above, which reads - # mk/analysis.mk, so this list cannot drift from the targets that exist. + # mk/verify.mk, so this list cannot drift from the targets that exist. verify-mutants: name: Proof and mutations (${{ matrix.target }}) needs: proof-targets diff --git a/Makefile b/Makefile index 58ad9ce0..b653ad72 100644 --- a/Makefile +++ b/Makefile @@ -445,5 +445,7 @@ $(BUILD_DIR)/test-mremap-tail-emfile: tests/test-mremap-tail-emfile.c | $(BUILD_ $(Q)$(CROSS_COMPILE)gcc -D_GNU_SOURCE -static -O2 -o $@ $< include mk/tests.mk -include mk/analysis.mk +include mk/lint.mk +include mk/verify.mk +include mk/format.mk include mk/help.mk diff --git a/frama-c-stubs/Hypervisor/Hypervisor.h b/frama-c-stubs/Hypervisor/Hypervisor.h index 81847d82..904e348f 100644 --- a/frama-c-stubs/Hypervisor/Hypervisor.h +++ b/frama-c-stubs/Hypervisor/Hypervisor.h @@ -14,9 +14,9 @@ * Deliberately outside src/. A compile resolves headers through -Isrc, so a * stub living there would sit on the real build's include path and could shadow * the SDK header the binary must link against. Up here nothing but - * FRAMAC_STUB_DIR in mk/analysis.mk can reach it. + * FRAMAC_STUB_DIR in mk/verify.mk can reach it. * - * This is reached only through mk/analysis.mk, never by a compile. Nothing + * This is reached only through mk/verify.mk, never by a compile. Nothing * proved reads any constant defined here, so the values matter only in that * they must not collide: HV_REG_X0 + n is how src/hvutil.h names a register, * which needs the X registers consecutive and in order, and the rest are diff --git a/frama-c-stubs/gcc-atomics.h b/frama-c-stubs/gcc-atomics.h index d839c1f9..5d9157ef 100644 --- a/frama-c-stubs/gcc-atomics.h +++ b/frama-c-stubs/gcc-atomics.h @@ -22,7 +22,7 @@ * function-like macro over its prototype fails the preprocessor outright. * * Modeled as the single-threaded reads and writes they reduce to, which is the - * same trade -D_Atomic= already makes in mk/analysis.mk and carries the same + * same trade -D_Atomic= already makes in mk/verify.mk and carries the same * limit: sound for the per-function runtime-error and bounds obligations these * targets discharge, NOT sound for any analysis of concurrent behaviour. The * memory order argument is evaluated and discarded, so a call that computes it diff --git a/mk/format.mk b/mk/format.mk new file mode 100644 index 00000000..64ff6426 --- /dev/null +++ b/mk/format.mk @@ -0,0 +1,50 @@ +# Source formatting + +.PHONY: check-format indent + +# Tracked source-like files only. Avoid editor/agent worktrees and other +# untracked mirrors under dot-directories. +C_FORMAT_FILES := $(shell git ls-files --cached --others --exclude-standard \ + -- 'src/**/*.[ch]' 'src/*.[ch]' \ + 'tests/*.c' 'tests/*.h' \ + 'frama-c-stubs/**/*.h' 'frama-c-stubs/*.h') +SHELL_SCRIPTS := $(shell git ls-files --cached --others --exclude-standard \ + -- '*.sh') +PYTHON_FORMAT_FILES := $(shell git ls-files --cached --others \ + --exclude-standard -- '*.py') + +## Check formatting: C (clang-format --dry-run) + shell (shellcheck) +check-format: check-syscall-dispatch + @echo " FMT src/ tests/ (check)" + $(Q)$(CLANG_FORMAT) --dry-run --Werror $(C_FORMAT_FILES) + @echo " MATRIX skip lists" + $(Q)bash .ci/check-matrix-lists.sh + @printf " SHCHK %d scripts\n" $(words $(SHELL_SCRIPTS)) + @fail=0; \ + for f in $(SHELL_SCRIPTS); do \ + if shellcheck --severity=warning "$$f" 2>&1; then \ + printf " $(GREEN)OK$(RESET) %s\n" "$$f"; \ + else \ + printf " $(RED)FAIL$(RESET) %s\n" "$$f"; \ + fail=$$((fail + 1)); \ + fi; \ + done; \ + if [ "$$fail" -eq 0 ]; then \ + printf "$(GREEN)All %d scripts pass$(RESET)\n" $(words $(SHELL_SCRIPTS)); \ + else \ + printf "$(RED)%d script(s) have warnings$(RESET)\n" "$$fail"; \ + exit 1; \ + fi + +## Indent all C, shell, and Python files in-place +indent: gen-syscall-dispatch + @echo " FMT src/ tests/" + $(Q)$(CLANG_FORMAT) -i $(C_FORMAT_FILES) + @if command -v shfmt >/dev/null 2>&1; then \ + printf " SHFMT %d scripts\n" $(words $(SHELL_SCRIPTS)); \ + shfmt -w -ln=bash -i 4 -ci -bn -fn -sr $(SHELL_SCRIPTS); \ + fi + @if command -v black >/dev/null 2>&1 && [ -n "$(PYTHON_FORMAT_FILES)" ]; then \ + printf " BLACK %d files\n" $(words $(PYTHON_FORMAT_FILES)); \ + black --quiet $(PYTHON_FORMAT_FILES); \ + fi diff --git a/mk/lint.mk b/mk/lint.mk new file mode 100644 index 00000000..82ac7f76 --- /dev/null +++ b/mk/lint.mk @@ -0,0 +1,56 @@ +# Static analysis + +.PHONY: lint analyze infer-uninit + +CLANG_TIDY ?= clang-tidy +INFER ?= infer + +# Missing-tool diagnostics, in the shape the verify-* targets already use: +# name the tool, name the install, fail on purpose. Without this a developer +# running lint/analyze/infer-uninit gets "make: clang-tidy: No such file or +# directory / Error 1", which reads like a broken Makefile rather than a +# missing dependency, on three of the eleven CI jobs. +define require-tool + @command -v $(1) >/dev/null 2>&1 || { \ + printf " $(RED)%s not found$(RESET) (%s)\n" "$(1)" "$(2)"; \ + exit 1; \ + } +endef + +## Run clang-tidy on all source files +lint: $(BUILD_DIR)/shim_blob.h $(BUILD_DIR)/version.h + $(call require-tool,$(CLANG_TIDY),brew install llvm -- or set CLANG_TIDY=) + @echo " TIDY src/" + $(Q)$(CLANG_TIDY) $(SRCS) -- $(CFLAGS) -Isrc -I$(BUILD_DIR) + +## Re-run Infer with the uninitialized-value checker that .inferconfig disables +infer-uninit: | $(BUILD_DIR) + $(call require-tool,$(INFER),brew install infer -- or set INFER=) + @echo " INFER uninitialized-value checker (disabled in .inferconfig)" + @echo " A count of 0 means the suppression is no longer needed and" + @echo " .inferconfig should be deleted. Anything else is the known" + @echo " false-positive class: Pulse cannot prove guest_copy's" + @echo " chunked loop fills its destination." + @status=0; \ + $(INFER) run --keep-going --enable-issue-type PULSE_UNINITIALIZED_VALUE \ + --results-dir $(BUILD_DIR)/infer-uninit \ + -- $(MAKE) -B elfuse > $(BUILD_DIR)/infer-uninit.log 2>&1 || status=$$?; \ + if [ "$$status" -ne 0 ] && [ "$$status" -ne 2 ]; then \ + printf " $(RED)FAILED$(RESET) infer exited %s; this is an analysis\n" "$$status"; \ + printf " failure, not an audit result. See $(BUILD_DIR)/infer-uninit.log\n"; \ + exit 1; \ + fi; \ + if [ ! -s $(BUILD_DIR)/infer-uninit/report.json ]; then \ + printf " $(RED)FAILED$(RESET) infer produced no report\n"; exit 1; \ + fi; \ + python3 -c "import json,sys; \ + d=json.load(open('$(BUILD_DIR)/infer-uninit/report.json')); \ + u=[x for x in d if x['bug_type']=='PULSE_UNINITIALIZED_VALUE']; \ + print(' %d PULSE_UNINITIALIZED_VALUE finding(s) across %d file(s)' \ + % (len(u), len({x['file'] for x in u})))" + +## Run clang static analyzer (scan-build) +analyze: + $(call require-tool,scan-build,brew install llvm) + @echo " SCAN elfuse" + $(Q)scan-build --use-cc=$(CC) $(MAKE) -B elfuse diff --git a/mk/analysis.mk b/mk/verify.mk similarity index 84% rename from mk/analysis.mk rename to mk/verify.mk index fb007911..0253be8d 100644 --- a/mk/analysis.mk +++ b/mk/verify.mk @@ -1,40 +1,7 @@ -# Static analysis and formatting - -.PHONY: lint analyze check-format indent verify \ - check-contracts verify-mutants check-char-signedness \ - check-stub-constants print-verify-targets infer-uninit - -CLANG_TIDY ?= clang-tidy -INFER ?= infer - -# Tracked source-like files only. Avoid editor/agent worktrees and other -# untracked mirrors under dot-directories. -C_FORMAT_FILES := $(shell git ls-files --cached --others --exclude-standard \ - -- 'src/**/*.[ch]' 'src/*.[ch]' \ - 'tests/*.c' 'tests/*.h' \ - 'frama-c-stubs/**/*.h' 'frama-c-stubs/*.h') -SHELL_SCRIPTS := $(shell git ls-files --cached --others --exclude-standard \ - -- '*.sh') -PYTHON_FORMAT_FILES := $(shell git ls-files --cached --others \ - --exclude-standard -- '*.py') - -# Missing-tool diagnostics, in the shape the verify-* targets already use: -# name the tool, name the install, fail on purpose. Without this a developer -# running lint/analyze/infer-uninit gets "make: clang-tidy: No such file or -# directory / Error 1", which reads like a broken Makefile rather than a -# missing dependency, on three of the eleven CI jobs. -define require-tool - @command -v $(1) >/dev/null 2>&1 || { \ - printf " $(RED)%s not found$(RESET) (%s)\n" "$(1)" "$(2)"; \ - exit 1; \ - } -endef +# Frama-C WP proofs -## Run clang-tidy on all source files -lint: $(BUILD_DIR)/shim_blob.h $(BUILD_DIR)/version.h - $(call require-tool,$(CLANG_TIDY),brew install llvm -- or set CLANG_TIDY=) - @echo " TIDY src/" - $(Q)$(CLANG_TIDY) $(SRCS) -- $(CFLAGS) -Isrc -I$(BUILD_DIR) +.PHONY: verify check-contracts verify-mutants check-char-signedness \ + check-stub-constants print-verify-targets # Frama-C proof of the ELF parsing core. ELF headers come from untrusted # binaries, so every offset and extent computed from them is discharged as a @@ -525,71 +492,3 @@ check-contracts: @echo " CONTRACT proved/gva.h call-site preconditions (5 of 9 clauses)" $(Q)$(MAKE) BUILD_DIR=$(BUILD_DIR)/contracts \ EXTRA_CFLAGS="-DELFUSE_CONTRACT_ASSERT $(EXTRA_CFLAGS)" check - -## Re-run Infer with the uninitialized-value checker that .inferconfig disables -infer-uninit: | $(BUILD_DIR) - $(call require-tool,$(INFER),brew install infer -- or set INFER=) - @echo " INFER uninitialized-value checker (disabled in .inferconfig)" - @echo " A count of 0 means the suppression is no longer needed and" - @echo " .inferconfig should be deleted. Anything else is the known" - @echo " false-positive class: Pulse cannot prove guest_copy's" - @echo " chunked loop fills its destination." - @status=0; \ - $(INFER) run --keep-going --enable-issue-type PULSE_UNINITIALIZED_VALUE \ - --results-dir $(BUILD_DIR)/infer-uninit \ - -- $(MAKE) -B elfuse > $(BUILD_DIR)/infer-uninit.log 2>&1 || status=$$?; \ - if [ "$$status" -ne 0 ] && [ "$$status" -ne 2 ]; then \ - printf " $(RED)FAILED$(RESET) infer exited %s; this is an analysis\n" "$$status"; \ - printf " failure, not an audit result. See $(BUILD_DIR)/infer-uninit.log\n"; \ - exit 1; \ - fi; \ - if [ ! -s $(BUILD_DIR)/infer-uninit/report.json ]; then \ - printf " $(RED)FAILED$(RESET) infer produced no report\n"; exit 1; \ - fi; \ - python3 -c "import json,sys; \ - d=json.load(open('$(BUILD_DIR)/infer-uninit/report.json')); \ - u=[x for x in d if x['bug_type']=='PULSE_UNINITIALIZED_VALUE']; \ - print(' %d PULSE_UNINITIALIZED_VALUE finding(s) across %d file(s)' \ - % (len(u), len({x['file'] for x in u})))" - -## Run clang static analyzer (scan-build) -analyze: - $(call require-tool,scan-build,brew install llvm) - @echo " SCAN elfuse" - $(Q)scan-build --use-cc=$(CC) $(MAKE) -B elfuse - -## Check formatting: C (clang-format --dry-run) + shell (shellcheck) -check-format: check-syscall-dispatch - @echo " FMT src/ tests/ (check)" - $(Q)$(CLANG_FORMAT) --dry-run --Werror $(C_FORMAT_FILES) - @echo " MATRIX skip lists" - $(Q)bash .ci/check-matrix-lists.sh - @printf " SHCHK %d scripts\n" $(words $(SHELL_SCRIPTS)) - @fail=0; \ - for f in $(SHELL_SCRIPTS); do \ - if shellcheck --severity=warning "$$f" 2>&1; then \ - printf " $(GREEN)OK$(RESET) %s\n" "$$f"; \ - else \ - printf " $(RED)FAIL$(RESET) %s\n" "$$f"; \ - fail=$$((fail + 1)); \ - fi; \ - done; \ - if [ "$$fail" -eq 0 ]; then \ - printf "$(GREEN)All %d scripts pass$(RESET)\n" $(words $(SHELL_SCRIPTS)); \ - else \ - printf "$(RED)%d script(s) have warnings$(RESET)\n" "$$fail"; \ - exit 1; \ - fi - -## Indent all C, shell, and Python files in-place -indent: gen-syscall-dispatch - @echo " FMT src/ tests/" - $(Q)$(CLANG_FORMAT) -i $(C_FORMAT_FILES) - @if command -v shfmt >/dev/null 2>&1; then \ - printf " SHFMT %d scripts\n" $(words $(SHELL_SCRIPTS)); \ - shfmt -w -ln=bash -i 4 -ci -bn -fn -sr $(SHELL_SCRIPTS); \ - fi - @if command -v black >/dev/null 2>&1 && [ -n "$(PYTHON_FORMAT_FILES)" ]; then \ - printf " BLACK %d files\n" $(words $(PYTHON_FORMAT_FILES)); \ - black --quiet $(PYTHON_FORMAT_FILES); \ - fi diff --git a/scripts/check-acsl-coverage.py b/scripts/check-acsl-coverage.py index cc8ef829..35d1baa8 100644 --- a/scripts/check-acsl-coverage.py +++ b/scripts/check-acsl-coverage.py @@ -108,7 +108,7 @@ def contracted_definitions(text): # The gcc_x86_64 data model is a sound stand-in for arm64 macOS on every # property these proofs use EXCEPT plain-char signedness (see the table in -# mk/analysis.mk). What keeps the results signedness-independent is that no +# mk/verify.mk). What keeps the results signedness-independent is that no # proved function reads a plain char without an explicit (unsigned char) or # (uint8_t) cast first. # diff --git a/scripts/check-char-signedness.py b/scripts/check-char-signedness.py index fd3cdcaa..c9531adb 100755 --- a/scripts/check-char-signedness.py +++ b/scripts/check-char-signedness.py @@ -4,7 +4,7 @@ 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/analysis.mk). The risk only exists where proved code reads +(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. @@ -47,14 +47,25 @@ ROOT = pathlib.Path(__file__).resolve().parent.parent -def analysis_mk(): - """mk/analysis.mk with line continuations joined.""" - return re.sub(r"\\\n", " ", (ROOT / "mk" / "analysis.mk").read_text()) +# 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 +# was an underscore in the filename, which the tree does not use anywhere. +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() def proof_sources(): """{target: (source path, [proved function names])}.""" - text = analysis_mk() + text = verify_mk.joined_text() utils = "" m = re.search(r"^VERIFY_UTILS_FCTS\s*:=\s*(.*)$", text, re.MULTILINE) if m: @@ -213,7 +224,7 @@ def main(): return 2 targets = {args.target: targets[args.target]} if not targets: - print("no proof targets found in mk/analysis.mk", file=sys.stderr) + print("no proof targets found in mk/verify.mk", file=sys.stderr) return 2 # Two distinct failure classes, reported with two distinct headers. An diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index f91210a6..4da00998 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -66,17 +66,17 @@ # 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 # was an underscore in the filename, which the tree does not use anywhere. -def _load_analysis_mk(): +def _load_verify_mk(): import importlib.util - path = pathlib.Path(__file__).resolve().parent / "analysis-mk.py" - spec = importlib.util.spec_from_file_location("analysis_mk", path) + 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 -analysis_mk_table = _load_analysis_mk() +verify_mk = _load_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,18 +883,13 @@ def _load_analysis_mk(): ] -def analysis_mk(): - """mk/analysis.mk with make line continuations joined.""" - return re.sub(r"\\\n", " ", (ROOT / "mk" / "analysis.mk").read_text()) - - # 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 mk/analysis.mk to build the "make verify-" a -# mutation is judged by; the individual VERIFY_*_SRC/_SCAN/ -# _FCTS lines in mk/analysis.mk are covered separately by target_inputs() -# below, but everything else in that file (the shared recipe, MIN_GOALS, +# 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/main.yml belongs here for the same reason even though it @@ -909,11 +904,11 @@ def analysis_mk(): # apiece. HARNESS_FILES = { "scripts/check-mutants.py", - "scripts/analysis-mk.py", + "scripts/verify-mk.py", "scripts/check-wp-result.py", "scripts/check-acsl-coverage.py", "scripts/check-char-signedness.py", - "mk/analysis.mk", + "mk/verify.mk", "mk/toolchain.mk", "Makefile", ".github/workflows/main.yml", @@ -1003,7 +998,7 @@ def target_inputs(cc): def target_sources(): """VERIFY__SRC for every target, as {target: path}.""" - return analysis_mk_table.target_sources() + return verify_mk.target_sources() def target_mutable_files(): @@ -1022,7 +1017,7 @@ def target_mutable_files(): def proved_functions(): """Every function named in a VERIFY_*_FCTS list, as {target: [names]}.""" - text = analysis_mk() + text = verify_mk.joined_text() shared = re.search(r"^VERIFY_UTILS_FCTS\s*:=\s*(.*)$", text, re.MULTILINE) utils = shared.group(1) if shared else "" out = {} diff --git a/scripts/check-proof-targets.py b/scripts/check-proof-targets.py index d25be03e..d3b82205 100755 --- a/scripts/check-proof-targets.py +++ b/scripts/check-proof-targets.py @@ -4,7 +4,7 @@ Three places name the same set of proved sources, and nothing but this script keeps them in agreement: - 1. mk/analysis.mk's VERIFY__SRC entries -- the targets themselves. + 1. mk/verify.mk's VERIFY__SRC entries -- the targets themselves. 2. .github/workflows/main.yml's verify-mutants matrix -- the CI sharding. 3. src/proved/ -- the directory the proved headers live in. @@ -19,7 +19,7 @@ a list of its own. What is checked here is that it stays that way, and that the list make generates is the whole list: a VERIFY__SRC block written below the line that snapshots them is invisible to make and to CI while -still reading as a target in this file. +still reading as a target in that file. Usage: check-proof-targets.py @@ -36,17 +36,17 @@ # 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 # was an underscore in the filename, which the tree does not use anywhere. -def _load_analysis_mk(): +def _load_verify_mk(): import importlib.util - path = pathlib.Path(__file__).resolve().parent / "analysis-mk.py" - spec = importlib.util.spec_from_file_location("analysis_mk", path) + 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 -analysis_mk = _load_analysis_mk() +verify_mk = _load_verify_mk() PROVED_DIR = ROOT / "src" / "proved" @@ -71,7 +71,7 @@ def make_target_names(): """The target names make actually generates rules for. Deliberately asks make rather than reading the file, because the two can - disagree. mk/analysis.mk derives its list with + disagree. mk/verify.mk derives its list with "VERIFY_TARGETS := $(filter VERIFY_%_SRC,$(.VARIABLES))", and := is immediate: .VARIABLES holds only what make has read so far, so a VERIFY__SRC block written below that line is invisible to it. The block @@ -94,7 +94,7 @@ def make_target_names(): def workflow_matrix_is_derived(): - """Whether the verify-mutants matrix is built from mk/analysis.mk. + """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 @@ -126,7 +126,7 @@ def workflow_matrix_is_derived(): " verify-mutants' matrix.target is not derived: " f"{shape}\n" f" It should be exactly {expected} so the target list has one " - "home in mk/analysis.mk. Another job's output would be derived " + "home in mk/verify.mk. Another job's output would be derived " "too, but from something this script does not read.", file=sys.stderr, ) @@ -135,7 +135,7 @@ def workflow_matrix_is_derived(): def main(): - mk = analysis_mk.targets() + mk = verify_mk.targets() if not workflow_matrix_is_derived(): return 2 @@ -146,10 +146,10 @@ def main(): dropped = {t.lower() for t in mk} - generated if dropped: print( - " VERIFY__SRC block(s) in mk/analysis.mk that make generates " - "no rule for. Nothing fails today: the proof simply never runs, " - "here or in CI. Move the block above the 'VERIFY_TARGETS :=' " - "line, which snapshots the target list at the point it appears:", + " VERIFY__SRC block(s) that make generates no rule for. " + "Nothing fails today: the proof simply never runs, here or in " + "CI. Move the block above the 'VERIFY_TARGETS :=' line, which " + "snapshots the target list at the point it appears:", file=sys.stderr, ) for t in sorted(dropped): @@ -161,12 +161,12 @@ def main(): # exists but is untracked, and breaks every fresh clone and CI checkout. missing_files = { src - for src in analysis_mk.sources() + for src in verify_mk.sources() if src.startswith("src/proved/") and not (ROOT / src).exists() } if missing_files: print( - " VERIFY__SRC entries in mk/analysis.mk naming a file that " + " VERIFY__SRC entries in mk/verify.mk naming a file that " "does not exist. The build and the proofs reference it, so a " "fresh clone fails even though this tree works:", file=sys.stderr, @@ -177,7 +177,7 @@ def main(): untracked = { src - for src in analysis_mk.sources() + for src in verify_mk.sources() if src.startswith("src/proved/") and src not in tracked_sources() } if untracked: @@ -191,12 +191,12 @@ def main(): print(f" {src}", file=sys.stderr) return 1 - unproved = proved_dir_sources() - analysis_mk.sources() + unproved = proved_dir_sources() - verify_mk.sources() if unproved: print( " file(s) under src/proved/ that no verify- target " "proves. The directory name says otherwise, so either add a " - "VERIFY__SRC block in mk/analysis.mk or move the file out:", + "VERIFY__SRC block in mk/verify.mk or move the file out:", file=sys.stderr, ) for f in sorted(unproved): @@ -204,7 +204,7 @@ def main(): return 1 print( - f" {len(mk)} proof target(s) in mk/analysis.mk, all with a proved " + f" {len(mk)} proof target(s) in mk/verify.mk, all with a proved " f"source; the CI matrix is derived from that list, and all " f"{len(proved_dir_sources())} file(s) under src/proved/ are proved " "by one" diff --git a/scripts/analysis-mk.py b/scripts/verify-mk.py similarity index 53% rename from scripts/analysis-mk.py rename to scripts/verify-mk.py index da04c67b..3fe4639e 100644 --- a/scripts/analysis-mk.py +++ b/scripts/verify-mk.py @@ -1,27 +1,32 @@ -"""The one reader of mk/analysis.mk's VERIFY__* variables. +"""The one reader of mk/verify.mk's VERIFY__* variables. -check-mutants.py and check-proof-targets.py both need the proof-target table, -and each had grown its own regex over the same lines: three patterns spelling -"VERIFY__SRC" three ways, differing only in which capture group they kept. -They agree today, so nothing was broken; they are three places to update when -the variable naming changes, in a pair of scripts whose entire job is catching -exactly that kind of drift somewhere else. +check-mutants.py, check-proof-targets.py and check-char-signedness.py all need +the proof-target table, and each had grown its own regex over the same lines: +patterns spelling "VERIFY__SRC" three ways, differing only in which capture +group they kept. They agree today, so nothing was broken; they are three places +to update when the variable naming changes, in scripts whose entire job is +catching exactly that kind of drift somewhere else. Load this instead of re-deriving it. The filename is kebab-case per CLAUDE.md, -which no import statement can name, so both consumers pull it in by path with -importlib; see _load_analysis_mk in either script. +which no import statement can name, so each consumer pulls it in by path with +importlib; see _load_verify_mk there. """ import pathlib import re ROOT = pathlib.Path(__file__).resolve().parent.parent -ANALYSIS_MK = ROOT / "mk" / "analysis.mk" +VERIFY_MK = ROOT / "mk" / "verify.mk" def text(): - """mk/analysis.mk as text.""" - return ANALYSIS_MK.read_text() + """mk/verify.mk as text.""" + return VERIFY_MK.read_text() + + +def joined_text(): + """mk/verify.mk with make line continuations joined.""" + return re.sub(r"\\\n", " ", text()) def target_sources(): From d552fe30ed94d6bb55cbb03f7bb0457621d99e5f Mon Sep 17 00:00:00 2001 From: Chun-Hung Tseng Date: Fri, 14 Aug 2026 11:24:51 +0200 Subject: [PATCH 2/5] Split GitHub Actions workflow by dependency cluster .github/workflows/main.yml ran ten jobs in 869 lines, so a branch touching the runtime matrix conflicted with one touching the proof sharding. It splits along its needs edges, leaving no dependency to cross a file boundary: lint.yml, build.yml (build-macos -> runtime-macos), static-analysis.yml (tidy-macos, scan-macos, infer-macos) and verify.yml (proof-targets -> verify-mutants -> verify and verify-mutants-gate). Job ids, job names, steps, env, matrices, caches and artifact names are copied unchanged, so every required status check keeps the name branch protection requires. That is also why the jobs are not routed through a reusable workflow: one called with workflow_call reports as " / ", which renames the check and unrequires it silently. check-proof-targets.py reads the verify-mutants matrix out of verify.yml, and check-mutants.py's HARNESS_FILES names verify.yml alone, since that is the file deciding which target a shard passes to --target and the other three cannot reach the mutation run. Each file carries its own copy of the on:, concurrency: and permissions: blocks, so ${{ github.workflow }} now yields four cancellation groups instead of one. A new push still cancels every in-flight job of a pull request; cancelling one workflow by hand no longer cancels the rest, and a manual run takes one workflow_dispatch per file. --- .github/workflows/build.yml | 371 +++++++++++ .github/workflows/lint.yml | 109 ++++ .github/workflows/main.yml | 869 -------------------------- .github/workflows/static-analysis.yml | 210 +++++++ .github/workflows/verify.yml | 254 ++++++++ mk/lint.mk | 2 +- scripts/check-mutants.py | 6 +- scripts/check-proof-targets.py | 8 +- 8 files changed, 952 insertions(+), 877 deletions(-) create mode 100644 .github/workflows/build.yml create mode 100644 .github/workflows/lint.yml delete mode 100644 .github/workflows/main.yml create mode 100644 .github/workflows/static-analysis.yml create mode 100644 .github/workflows/verify.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 00000000..e9373039 --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,371 @@ +# Build elfuse and run the HVF runtime tests. +# +# build-macos : compile + entitlement check on macOS Apple Silicon +# runtime-macos : HVF runtime tests on self-hosted Apple Silicon, +# including release, ASAN, UBSAN, and TSAN variants +# +# Runtime and sanitizer tests require Hypervisor.framework, which +# GitHub-hosted macOS runners do not expose. Those tests run on self-hosted +# Apple Silicon runners; the hosted job stops at build. +name: Build + +on: + push: + branches: [main] + paths-ignore: + - '**.md' + - 'docs/**' + - 'LICENSE' + pull_request: + branches: [main] + paths-ignore: + - '**.md' + - 'docs/**' + - 'LICENSE' + workflow_dispatch: + +# Cancel in-progress runs for the same PR; keep main runs going. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} + +permissions: + contents: read + +jobs: + # Build verification on macOS Apple Silicon (no HVF runtime tests). + # Hosted runners don't expose Hypervisor.framework, so this job stops at + # `make elfuse` + entitlement check. + build-macos: + name: Build (macOS Apple Silicon) + runs-on: macos-15 + timeout-minutes: 15 + env: + GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy + HOMEBREW_NO_INSTALL_CLEANUP: 1 + HOMEBREW_NO_AUTO_UPDATE: 1 + BREW_PKGS: binutils + steps: + - name: Checkout + uses: actions/checkout@v7 + + - name: Cache Homebrew downloads + # No restore-keys: a partial match would mask upstream regressions. + uses: actions/cache@v6 + with: + path: ~/Library/Caches/Homebrew/downloads + key: brew-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} + + - name: Confirm host is arm64 + run: | + set -euo pipefail + uname -mrs + test "$(uname -m)" = "arm64" + + - name: Install GNU objcopy + # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. + run: | + set -euo pipefail + brew install --quiet $BREW_PKGS + "$GNU_OBJCOPY" --version | head -1 + + - name: Build elfuse + run: | + set -euo pipefail + clang --version | head -1 + make elfuse + + - name: Verify HVF entitlement is embedded + run: | + set -euo pipefail + codesign -d --entitlements - build/elfuse 2>&1 \ + | grep -q 'com\.apple\.security\.hypervisor' + + - name: Upload elfuse binary + if: ${{ !cancelled() }} + uses: actions/upload-artifact@v7 + with: + name: elfuse-${{ runner.os }}-${{ runner.arch }} + path: build/elfuse + retention-days: 7 + if-no-files-found: warn + + runtime-macos: + name: Runtime (${{ matrix.name }}) + needs: build-macos + if: > + github.repository == 'sysprog21/elfuse' && + (github.event_name == 'push' || github.event_name == 'pull_request') + 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 + # that, a TSAN-slowed guest overruns both, surfacing as TIMEOUT reds + # indistinguishable from a real hang. + timeout-minutes: ${{ matrix.job_timeout }} + strategy: + fail-fast: false + max-parallel: 4 + matrix: + include: + - name: Release + sanitizer: release + extra_cflags: '' + asan_options: '' + ubsan_options: '' + tsan_options: '' + test_timeout: '' + job_timeout: 20 + run_matrix: true + check_target: check + brew_pkgs: binutils qemu + - name: ASAN + sanitizer: asan + extra_cflags: -O1 -g -fsanitize=address -fno-omit-frame-pointer + asan_options: abort_on_error=1:detect_leaks=0 + ubsan_options: '' + tsan_options: '' + test_timeout: '30' + job_timeout: 30 + run_matrix: false + check_target: check-sanitizer + brew_pkgs: binutils + - name: UBSAN + sanitizer: ubsan + extra_cflags: -O1 -g -fsanitize=undefined -fno-sanitize-recover=undefined -fno-omit-frame-pointer + asan_options: '' + ubsan_options: halt_on_error=1:print_stacktrace=1 + tsan_options: '' + test_timeout: '30' + job_timeout: 30 + run_matrix: false + check_target: check-sanitizer + brew_pkgs: binutils + - name: TSAN + sanitizer: tsan + extra_cflags: -O1 -g -fsanitize=thread -fno-omit-frame-pointer + asan_options: '' + ubsan_options: '' + tsan_options: halt_on_error=1 + test_timeout: '60' + job_timeout: 45 + run_matrix: false + check_target: check-sanitizer + brew_pkgs: binutils + + # contents: read for the checkout; pull-requests: read so the guard can + # query the PR's current HEAD. (actions: write would let the guard + # cancel the run instead of failing it, but repo policy caps the token + # at actions: read, so the guard fails fast with a clear reason instead.) + permissions: + contents: read + pull-requests: read + + concurrency: + group: runtime-macos-${{ matrix.sanitizer }}-${{ github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} + + env: + LINUX_TOOLCHAIN: /opt/toolchain/aarch64-linux-gnu + GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy + EXTRA_CFLAGS: ${{ matrix.extra_cflags }} + ASAN_OPTIONS: ${{ matrix.asan_options }} + UBSAN_OPTIONS: ${{ matrix.ubsan_options }} + TSAN_OPTIONS: ${{ matrix.tsan_options }} + # Empty on the release leg leaves each script its own default: 60s in + # tests/driver.sh, 10s in tests/lib/test-runner.sh. The 30 on the ASAN + # and UBSAN legs is therefore a raise for the lanes and a cut for the + # driver. + TEST_TIMEOUT: ${{ matrix.test_timeout }} + HOMEBREW_NO_INSTALL_CLEANUP: 1 + HOMEBREW_NO_AUTO_UPDATE: 1 + # qemu is only needed by test-matrix (release leg); sanitizer legs run the + # fixture-free check-sanitizer subset and skip it. + BREW_PKGS: ${{ matrix.brew_pkgs }} + # Parallelize compilation; the guest-test cross-compile and elfuse build + # dominate the non-test wall time. + MAKEFLAGS: -j8 + + steps: + # Fail fast if this run targets a commit that is no longer the PR's + # HEAD. cancel-in-progress covers "commit 2 pushed while commit 1 is + # still running", but NOT a manual "Re-run jobs" on an old run: a + # re-run replays the original event payload (a frozen head.sha) + # against this single self-hosted runner, which would otherwise burn + # the full job timeout re-testing stale code. Compare the frozen + # head.sha against the live PR HEAD; when they differ, exit 1 with a + # clear "commit is no longer the latest" message. We fail (rather than + # cancel) because repo policy caps the token at actions: read, so the + # cancel API is unavailable. exit 1 also stops the job, so the later + # steps are skipped automatically -- no per-step guard needed. The + # lookup fails open: if HEAD can't be determined the job runs. + - name: Fail fast if superseded by a newer PR commit + if: github.event_name == 'pull_request' + env: + GH_TOKEN: ${{ github.token }} + REPO: ${{ github.repository }} + PR_NUMBER: ${{ github.event.pull_request.number }} + RUN_SHA: ${{ github.event.pull_request.head.sha }} + run: | + set -uo pipefail + # curl and system python3 are always present on macOS; jq/gh are + # not guaranteed on a self-hosted runner, so don't depend on them. + latest=$(curl -fsSL \ + -H "Authorization: Bearer $GH_TOKEN" \ + -H "Accept: application/vnd.github+json" \ + "https://api.github.com/repos/$REPO/pulls/$PR_NUMBER" \ + | python3 -c 'import json,sys; print(json.load(sys.stdin)["head"]["sha"])') \ + || latest="" + echo "Run targets : $RUN_SHA" + echo "PR HEAD now : ${latest:-}" + if [ -n "$latest" ] && [ "$latest" != "$RUN_SHA" ]; then + echo "::error::This run targets $RUN_SHA, but PR #$PR_NUMBER HEAD is now $latest -- the commit is no longer the latest. Failing instead of re-testing stale code on the self-hosted runner; re-run CI on the current commit." + exit 1 + fi + + - name: Checkout + uses: actions/checkout@v7 + + - name: Restore cached test fixtures + # Only the release leg needs fixtures: the sanitizer legs run the + # fixture-free check-sanitizer subset. + if: ${{ matrix.run_matrix }} + # actions/checkout's default clean:true runs `git clean -ffdx`, which + # wipes externals/test-fixtures (gitignored) on this self-hosted + # runner even though its disk otherwise persists across runs. + # fetch-fixtures.sh is already idempotent -- it skips re-downloading + # Alpine packages when externals/test-fixtures/versions.lock still + # matches -- so stash that tree outside the workspace and restore it + # here as a real directory. The qemu lane in tests/test-matrix.sh + # shares the workspace root with the guest over virtio-9p, and a + # symlink pointing outside that root does not resolve inside the + # guest, so this must be a real copy, not a symlink. + run: | + cache="$HOME/.cache/elfuse-ci/test-fixtures" + if [ -d "$cache" ]; then + mkdir -p externals + rm -rf externals/test-fixtures + cp -Rc "$cache" externals/test-fixtures + echo "Restored test fixtures ($(du -sh externals/test-fixtures | cut -f1), lock: $(head -1 externals/test-fixtures/versions.lock 2>/dev/null || echo none))" + else + echo "No fixtures cache at $cache; tests fetch on demand" + fi + + - name: Host info + run: | + sw_vers + uname -a + uname -m + sysctl kern.hv_support || true + test "$(uname -m)" = "arm64" + + - name: Cache Homebrew downloads + uses: actions/cache@v6 + with: + path: ~/Library/Caches/Homebrew/downloads + key: brew-runtime-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} + + - name: Install missing Homebrew packages + run: | + missing=() + + for pkg in $BREW_PKGS; do + if ! brew list --formula "$pkg" >/dev/null 2>&1; then + missing+=("$pkg") + fi + done + + if [ "${#missing[@]}" -gt 0 ]; then + brew install --quiet "${missing[@]}" + else + echo "All Homebrew packages are already installed: $BREW_PKGS" + fi + + - name: Tool versions + run: | + command -v make + command -v "$GNU_OBJCOPY" + make -V .MAKE.VERSION 2>/dev/null || true + "$GNU_OBJCOPY" --version | head -1 + qemu-aarch64 --version | head -1 || true + python3 --version + + - name: Check Rosetta for Linux + # Rosetta is exercised only by test-matrix (release leg); the + # check-sanitizer subset has no x86_64-via-Rosetta tests. + if: ${{ matrix.run_matrix }} + run: | + ROSETTA=/Library/Apple/usr/libexec/oah/RosettaLinux/rosetta + + if [ ! -x "$ROSETTA" ]; then + echo "::error::Rosetta for Linux runtime was not found at $ROSETTA" + echo + echo "Install Rosetta on the self-hosted Mac runner first:" + echo " sudo softwareupdate --install-rosetta --agree-to-license" + echo + echo "Current /Library/Apple/usr/libexec/oah contents:" + ls -R /Library/Apple/usr/libexec/oah || true + exit 1 + fi + + ls -l "$ROSETTA" + + - name: Build elfuse + # make does not track EXTRA_CFLAGS changes, so an object built for one + # sanitizer must not be reused for another. Checkout already wipes + # build/ (git clean -ffdx), but clean explicitly so the leg builds from + # scratch even on a workspace that was not freshly cleaned. + run: | + make clean + make EXTRA_CFLAGS="$EXTRA_CFLAGS" elfuse + + - name: Verify HVF entitlement is embedded + run: | + codesign -d --entitlements - build/elfuse 2>&1 \ + | grep -q 'com\.apple\.security\.hypervisor' + + - name: test-hello + run: | + make EXTRA_CFLAGS="$EXTRA_CFLAGS" test-hello + + - name: test-multi-vcpu + run: | + make EXTRA_CFLAGS="$EXTRA_CFLAGS" test-multi-vcpu + + - name: make check + # Release runs the full check suite; sanitizer legs run check-sanitizer, + # a representative internal-implementation subset (the release lane plus + # test-matrix already cover Linux syscall compatibility). + run: | + make EXTRA_CFLAGS="$EXTRA_CFLAGS" ${{ matrix.check_target }} + + - name: Test matrix + if: ${{ matrix.run_matrix }} + run: | + bash tests/test-matrix.sh all + + - name: Upload runtime binary + if: ${{ !cancelled() }} + uses: actions/upload-artifact@v7 + with: + name: elfuse-runtime-${{ matrix.sanitizer }}-${{ runner.os }}-${{ runner.arch }} + path: build/elfuse + retention-days: 7 + if-no-files-found: warn + + - name: Save test fixtures cache + # Persist externals/test-fixtures outside the workspace so the next + # run's "Restore cached test fixtures" step can skip re-downloading + # unchanged Alpine packages. Runs even if an earlier step failed, as + # long as the job wasn't cancelled, so a fixture-unrelated test + # failure doesn't cost the next run its cache. + if: ${{ !cancelled() && matrix.sanitizer == 'release' }} + run: | + if [ -d externals/test-fixtures ]; then + cache="$HOME/.cache/elfuse-ci/test-fixtures" + mkdir -p "$(dirname "$cache")" + rm -rf "$cache" + cp -Rc externals/test-fixtures "$cache" + echo "Saved test fixtures ($(du -sh "$cache" | cut -f1))" + else + echo "No externals/test-fixtures to save" + fi diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml new file mode 100644 index 00000000..d00bad68 --- /dev/null +++ b/.github/workflows/lint.yml @@ -0,0 +1,109 @@ +# Formatting and static checks on a fast Linux runner. +# +# All sub-checks run even if an earlier one fails so the report shows every +# problem at once instead of stopping at the first. +name: Lint + +on: + push: + branches: [main] + paths-ignore: + - '**.md' + - 'docs/**' + - 'LICENSE' + pull_request: + branches: [main] + paths-ignore: + - '**.md' + - 'docs/**' + - 'LICENSE' + workflow_dispatch: + +# Cancel in-progress runs for the same PR; keep main runs going. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} + +permissions: + contents: read + +jobs: + # Lint: formatting + static analysis on a fast Linux runner. + lint: + name: Lint (Linux) + runs-on: ubuntu-24.04 + timeout-minutes: 10 + env: + # Single source of truth for the apt package list. Used by both the + # cache key (so unrelated workflow edits don't bust the cache) and + # the install step. + LINT_PKGS: clang-format-22 cppcheck shellcheck + steps: + - name: Checkout + uses: actions/checkout@v7 + + - name: Cache apt packages + uses: actions/cache@v6 + with: + path: ~/apt-cache + key: apt-${{ runner.os }}-${{ env.LINT_PKGS }} + + - name: Add LLVM apt repo (clang-format-22) + # 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: | + set -euo pipefail + sudo install -d -m 0755 /etc/apt/keyrings + wget -qO- https://apt.llvm.org/llvm-snapshot.gpg.key \ + | sudo tee /etc/apt/keyrings/llvm.asc > /dev/null + echo "deb [signed-by=/etc/apt/keyrings/llvm.asc] http://apt.llvm.org/noble/ llvm-toolchain-noble-22 main" \ + | sudo tee /etc/apt/sources.list.d/llvm.list + + - name: Install tools + run: | + set -euo pipefail + mkdir -p ~/apt-cache + sudo apt-get update + # shellcheck disable=SC2086 -- LINT_PKGS is a space-separated list. + 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() }} + 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() }} + run: | + set -euo pipefail + mapfile -d '' files < <(git ls-files -z -- '.ci/*.sh') + shellcheck --severity=warning "${files[@]}" + + - name: cppcheck + if: ${{ !cancelled() }} + 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/main.yml b/.github/workflows/main.yml deleted file mode 100644 index 4043c877..00000000 --- a/.github/workflows/main.yml +++ /dev/null @@ -1,869 +0,0 @@ -# Build elfuse and run the lint + analysis suites. -# -# Jobs run in parallel where runner capacity allows: -# lint : format/newline/security/cppcheck/dispatch on Linux -# build-macos : compile + entitlement check on macOS Apple Silicon -# tidy-macos : clang-tidy via `make lint` -# 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 -# scan-macos : LLVM scan-build via `make analyze` -# infer-macos : Facebook Infer capture + analyze over the full build -# runtime-macos : HVF runtime tests on self-hosted Apple Silicon, -# including release, ASAN, UBSAN, and TSAN variants -# -# Runtime and sanitizer tests require Hypervisor.framework, which -# GitHub-hosted macOS runners do not expose. Those tests run on self-hosted -# Apple Silicon runners; the hosted job stops at build. -# -# Within the lint job, all sub-checks run even if an earlier one fails so -# the report shows every problem at once instead of stopping at the first. -name: CI - -on: - push: - branches: [main] - paths-ignore: - - '**.md' - - 'docs/**' - - 'LICENSE' - pull_request: - branches: [main] - paths-ignore: - - '**.md' - - 'docs/**' - - 'LICENSE' - workflow_dispatch: - -# Cancel in-progress runs for the same PR; keep main runs going. -concurrency: - group: ${{ github.workflow }}-${{ github.ref }} - cancel-in-progress: ${{ github.event_name == 'pull_request' }} - -permissions: - contents: read - -jobs: - # Lint: formatting + static analysis on a fast Linux runner. - lint: - name: Lint (Linux) - runs-on: ubuntu-24.04 - timeout-minutes: 10 - env: - # Single source of truth for the apt package list. Used by both the - # cache key (so unrelated workflow edits don't bust the cache) and - # the install step. - LINT_PKGS: clang-format-22 cppcheck shellcheck - steps: - - name: Checkout - uses: actions/checkout@v7 - - - name: Cache apt packages - uses: actions/cache@v6 - with: - path: ~/apt-cache - key: apt-${{ runner.os }}-${{ env.LINT_PKGS }} - - - name: Add LLVM apt repo (clang-format-22) - # 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: | - set -euo pipefail - sudo install -d -m 0755 /etc/apt/keyrings - wget -qO- https://apt.llvm.org/llvm-snapshot.gpg.key \ - | sudo tee /etc/apt/keyrings/llvm.asc > /dev/null - echo "deb [signed-by=/etc/apt/keyrings/llvm.asc] http://apt.llvm.org/noble/ llvm-toolchain-noble-22 main" \ - | sudo tee /etc/apt/sources.list.d/llvm.list - - - name: Install tools - run: | - set -euo pipefail - mkdir -p ~/apt-cache - sudo apt-get update - # shellcheck disable=SC2086 -- LINT_PKGS is a space-separated list. - 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() }} - 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() }} - run: | - set -euo pipefail - mapfile -d '' files < <(git ls-files -z -- '.ci/*.sh') - shellcheck --severity=warning "${files[@]}" - - - name: cppcheck - if: ${{ !cancelled() }} - 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 below, 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 - - # Build verification on macOS Apple Silicon (no HVF runtime tests). - # Hosted runners don't expose Hypervisor.framework, so this job stops at - # `make elfuse` + entitlement check. - build-macos: - name: Build (macOS Apple Silicon) - runs-on: macos-15 - timeout-minutes: 15 - env: - GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy - HOMEBREW_NO_INSTALL_CLEANUP: 1 - HOMEBREW_NO_AUTO_UPDATE: 1 - BREW_PKGS: binutils - steps: - - name: Checkout - uses: actions/checkout@v7 - - - name: Cache Homebrew downloads - # No restore-keys: a partial match would mask upstream regressions. - uses: actions/cache@v6 - with: - path: ~/Library/Caches/Homebrew/downloads - key: brew-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} - - - name: Confirm host is arm64 - run: | - set -euo pipefail - uname -mrs - test "$(uname -m)" = "arm64" - - - name: Install GNU objcopy - # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. - run: | - set -euo pipefail - brew install --quiet $BREW_PKGS - "$GNU_OBJCOPY" --version | head -1 - - - name: Build elfuse - run: | - set -euo pipefail - clang --version | head -1 - make elfuse - - - name: Verify HVF entitlement is embedded - run: | - set -euo pipefail - codesign -d --entitlements - build/elfuse 2>&1 \ - | grep -q 'com\.apple\.security\.hypervisor' - - - name: Upload elfuse binary - if: ${{ !cancelled() }} - uses: actions/upload-artifact@v7 - with: - name: elfuse-${{ runner.os }}-${{ runner.arch }} - path: build/elfuse - retention-days: 7 - if-no-files-found: warn - - # clang-tidy via `make lint`. Runs in parallel with build/scan jobs. - # Advisory: .clang-tidy sets WarningsAsErrors='', so findings are logged - # for review but do not gate the job. - tidy-macos: - name: clang-tidy (macOS Apple Silicon) - runs-on: macos-15 - timeout-minutes: 20 - env: - GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy - HOMEBREW_NO_INSTALL_CLEANUP: 1 - HOMEBREW_NO_AUTO_UPDATE: 1 - # binutils is needed because make lint depends on the shim_blob.h - # generated by the assembly + objcopy pipeline. - BREW_PKGS: binutils llvm - CLANG_TIDY: /opt/homebrew/opt/llvm/bin/clang-tidy - 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: Install Homebrew packages - # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. - run: | - set -euo pipefail - brew install --quiet $BREW_PKGS - "$CLANG_TIDY" --version | head -1 - - - name: Generate build/dispatch.h, shim_blob.h, version.h - # `make lint` depends on these generated headers; building the - # full elfuse binary is unnecessary, so just satisfy the deps. - run: make build/shim_blob.h build/version.h build/dispatch.h - - - name: clang-tidy (make lint) - run: make lint - - # 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. - # - # Runs on Linux with no toolchain: "make print-verify-targets" only reads the - # makefile, so this costs seconds and gates nothing. - proof-targets: - name: Enumerate proof targets - runs-on: ubuntu-latest - outputs: - targets: ${{ steps.list.outputs.targets }} - steps: - - name: Checkout - uses: actions/checkout@v7 - - - name: Read the targets from mk/verify.mk - 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" - - # Frama-C WP proofs of the attacker-facing arithmetic, plus the mutation gate - # that shows those proofs bite. One runner per proof target. - # - # GATING, unlike tidy-macos and scan-macos: the inputs these proofs cover come - # from untrusted binaries and from the guest itself, so an unproved - # obligation fails the job instead of being logged for review. Without this - # 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 all sixteen targets 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 }}) - needs: proof-targets - 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 - # Deliberately far below the verify job's 120, and the single biggest - # term in this job's runtime. A mutation is caught by leaving a goal - # open, and an open goal is one both provers spend the whole timeout - # failing to discharge, so every caught mutation costs two full - # timeouts per goal. The verify job wants headroom because one - # [Timeout] there is a false proof regression; here the pressure runs - # the other way. - # - # Cutting it does not weaken the verdict, because check-mutants.py - # proves an UNMUTATED copy of each source through this same path - # first (check_baseline). A value too tight to prove real code fails - # that control loudly instead of silently scoring mutations as caught. - # The margin is wide: all nine targets together discharge 392 - # obligations in 31s locally, the slowest single target in 9s. - 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: Install Homebrew packages - # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. - run: | - set -euo pipefail - brew install --quiet $BREW_PKGS - - # 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 - 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: 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 - - - 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: 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. - 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 - - - name: Upload prover log - if: always() - uses: actions/upload-artifact@v7 - with: - name: verify-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. - 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 - if: always() - runs-on: ubuntu-latest - timeout-minutes: 5 - steps: - - name: Require every matrix leg to have passed - run: | - set -euo pipefail - result='${{ needs.verify-mutants.result }}' - echo "mutation matrix: $result" - [ "$result" = success ] || exit 1 - - # LLVM scan-build via `make analyze`. Runs in parallel with build/tidy. - # Advisory: scan-build's Make target does not pass --status-bugs, so - # findings appear in logs and in the uploaded HTML report but do not - # gate the job. - scan-macos: - name: scan-build (macOS Apple Silicon) - runs-on: macos-15 - timeout-minutes: 25 - env: - GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy - HOMEBREW_NO_INSTALL_CLEANUP: 1 - HOMEBREW_NO_AUTO_UPDATE: 1 - BREW_PKGS: binutils llvm - LLVM_BIN: /opt/homebrew/opt/llvm/bin - 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: Install Homebrew packages - # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. - # scan-build has no --version; piping --help into `head -1` makes - # perl take SIGPIPE on the closed stdout and exit non-zero, which - # under pipefail fails the step. Just confirm the binary exists. - run: | - set -euo pipefail - brew install --quiet $BREW_PKGS - test -x "$LLVM_BIN/scan-build" - "$LLVM_BIN/clang" --version | head -1 - - - name: scan-build (make analyze) - run: | - set -euo pipefail - export PATH="$LLVM_BIN:$PATH" - mkdir -p build/scan-build - scan-build -o build/scan-build --use-cc="$(command -v clang)" \ - make -B elfuse - - - name: Upload scan-build report - if: ${{ !cancelled() }} - uses: actions/upload-artifact@v7 - with: - name: scan-build-${{ runner.os }}-${{ runner.arch }} - path: build/scan-build - retention-days: 7 - if-no-files-found: ignore - - # Facebook Infer over the full elfuse build. Must run on macOS Apple - # Silicon because the build needs Hypervisor.framework and -arch arm64; - # Infer captures the real clang invocations, so it sees every TU. - # - # Gating (unlike tidy-macos/scan-macos): a separate step turns Infer's - # report.json into inline ::error:: annotations plus a job summary, then - # fails the job. Findings surface on the PR instead of a silent exit code, - # so bugs are pruned at PR time instead of merged. - infer-macos: - name: Infer (macOS Apple Silicon) - runs-on: macos-15 - timeout-minutes: 25 - env: - GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy - HOMEBREW_NO_INSTALL_CLEANUP: 1 - HOMEBREW_NO_AUTO_UPDATE: 1 - BREW_PKGS: binutils - 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: Install GNU objcopy - # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. - run: | - set -euo pipefail - brew install --quiet $BREW_PKGS - "$GNU_OBJCOPY" --version | head -1 - - - name: Setup Infer - # infer_version pins the Infer binary; the action itself tracks the v1 - # tag. - uses: srz-zumix/setup-infer@v1 - with: - infer_version: v1.3.0 - - # .inferconfig disables PULSE_UNINITIALIZED_VALUE repo-wide. Pulse cannot - # prove guest_copy's chunked "while (copied < len)" loop fills its - # destination, so every guest_read_small caller looks uninitialized; the - # findings were audited and every caller checks the return value. The rest - # of the Infer gate is untouched: null dereference, use-after-free, leaks, - # dead stores and stack-address escape all still fail the job. - # - # The cost is real and repo-wide: a genuinely uninitialized read added - # after this point is not caught here. Scoping it narrower was tried and - # is worse -- the findings span thirteen files including syscall.c and - # proc.c, so a path block list suppresses the same class over most of the - # syscall surface while being harder to read, and censor-report does not - # take effect through `infer run` in v1.3.0. `make infer-uninit` re-runs - # the analysis with the checker back on and prints the count, so whether - # an Infer upgrade has made this unnecessary is one command away. - - name: Infer capture + analyze (make -B elfuse) - # -B forces a clean rebuild so Infer captures every translation unit. - # Non-C build steps (shim.S assembly, objcopy) pass through untouched. - # No --fail-on-issue here: `infer run` must exit 0 so the reporting - # step below runs and surfaces findings before the job fails. - # --keep-going tolerates a frontend failure on an odd TU, but that can - # also mask a total capture miss (wrapper never intercepts clang, 0 - # files analyzed). The count guard fails the job on that silent no-op. - run: | - set -euo pipefail - infer run --keep-going -- make -B elfuse 2>&1 | tee infer-run.log - n=$(grep -oE 'Found [0-9]+ source file' infer-run.log \ - | grep -oE '[0-9]+' | tail -1 || true) - echo "Infer captured ${n:-0} source files" - test "${n:-0}" -gt 0 - - - name: Report Infer findings - # Emit GitHub annotations + a job summary from report.json, then exit - # non-zero if any finding exists. Runs even when a prior step failed so - # a partial report is still surfaced. - if: ${{ !cancelled() }} - run: python3 scripts/infer-annotate.py infer-out/report.json - - - name: Upload Infer report - if: ${{ !cancelled() }} - uses: actions/upload-artifact@v7 - with: - name: infer-${{ runner.os }}-${{ runner.arch }} - path: infer-out/report.txt - retention-days: 7 - if-no-files-found: warn - - runtime-macos: - name: Runtime (${{ matrix.name }}) - needs: build-macos - if: > - github.repository == 'sysprog21/elfuse' && - (github.event_name == 'push' || github.event_name == 'pull_request') - 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 widened per leg. Without - # that, a TSAN-slowed guest overruns the 10s default TEST_TIMEOUT and the - # 20-minute job budget, surfacing as TIMEOUT reds indistinguishable from a - # real hang. - timeout-minutes: ${{ matrix.job_timeout }} - strategy: - fail-fast: false - max-parallel: 4 - matrix: - include: - - name: Release - sanitizer: release - extra_cflags: '' - asan_options: '' - ubsan_options: '' - tsan_options: '' - test_timeout: '' - job_timeout: 20 - run_matrix: true - check_target: check - brew_pkgs: binutils qemu - - name: ASAN - sanitizer: asan - extra_cflags: -O1 -g -fsanitize=address -fno-omit-frame-pointer - asan_options: abort_on_error=1:detect_leaks=0 - ubsan_options: '' - tsan_options: '' - test_timeout: '30' - job_timeout: 30 - run_matrix: false - check_target: check-sanitizer - brew_pkgs: binutils - - name: UBSAN - sanitizer: ubsan - extra_cflags: -O1 -g -fsanitize=undefined -fno-sanitize-recover=undefined -fno-omit-frame-pointer - asan_options: '' - ubsan_options: halt_on_error=1:print_stacktrace=1 - tsan_options: '' - test_timeout: '30' - job_timeout: 30 - run_matrix: false - check_target: check-sanitizer - brew_pkgs: binutils - - name: TSAN - sanitizer: tsan - extra_cflags: -O1 -g -fsanitize=thread -fno-omit-frame-pointer - asan_options: '' - ubsan_options: '' - tsan_options: halt_on_error=1 - test_timeout: '60' - job_timeout: 45 - run_matrix: false - check_target: check-sanitizer - brew_pkgs: binutils - - # contents: read for the checkout; pull-requests: read so the guard can - # query the PR's current HEAD. (actions: write would let the guard - # cancel the run instead of failing it, but repo policy caps the token - # at actions: read, so the guard fails fast with a clear reason instead.) - permissions: - contents: read - pull-requests: read - - concurrency: - group: runtime-macos-${{ matrix.sanitizer }}-${{ github.ref }} - cancel-in-progress: ${{ github.event_name == 'pull_request' }} - - env: - LINUX_TOOLCHAIN: /opt/toolchain/aarch64-linux-gnu - GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy - EXTRA_CFLAGS: ${{ matrix.extra_cflags }} - ASAN_OPTIONS: ${{ matrix.asan_options }} - UBSAN_OPTIONS: ${{ matrix.ubsan_options }} - TSAN_OPTIONS: ${{ matrix.tsan_options }} - # Empty on the release leg falls back to test-runner.sh's 10s default. - TEST_TIMEOUT: ${{ matrix.test_timeout }} - HOMEBREW_NO_INSTALL_CLEANUP: 1 - HOMEBREW_NO_AUTO_UPDATE: 1 - # qemu is only needed by test-matrix (release leg); sanitizer legs run the - # fixture-free check-sanitizer subset and skip it. - BREW_PKGS: ${{ matrix.brew_pkgs }} - # Parallelize compilation; the guest-test cross-compile and elfuse build - # dominate the non-test wall time. - MAKEFLAGS: -j8 - - steps: - # Fail fast if this run targets a commit that is no longer the PR's - # HEAD. cancel-in-progress covers "commit 2 pushed while commit 1 is - # still running", but NOT a manual "Re-run jobs" on an old run: a - # re-run replays the original event payload (a frozen head.sha) - # against this single self-hosted runner, which would otherwise burn - # the full job timeout re-testing stale code. Compare the frozen - # head.sha against the live PR HEAD; when they differ, exit 1 with a - # clear "commit is no longer the latest" message. We fail (rather than - # cancel) because repo policy caps the token at actions: read, so the - # cancel API is unavailable. exit 1 also stops the job, so the later - # steps are skipped automatically -- no per-step guard needed. The - # lookup fails open: if HEAD can't be determined the job runs. - - name: Fail fast if superseded by a newer PR commit - if: github.event_name == 'pull_request' - env: - GH_TOKEN: ${{ github.token }} - REPO: ${{ github.repository }} - PR_NUMBER: ${{ github.event.pull_request.number }} - RUN_SHA: ${{ github.event.pull_request.head.sha }} - run: | - set -uo pipefail - # curl and system python3 are always present on macOS; jq/gh are - # not guaranteed on a self-hosted runner, so don't depend on them. - latest=$(curl -fsSL \ - -H "Authorization: Bearer $GH_TOKEN" \ - -H "Accept: application/vnd.github+json" \ - "https://api.github.com/repos/$REPO/pulls/$PR_NUMBER" \ - | python3 -c 'import json,sys; print(json.load(sys.stdin)["head"]["sha"])') \ - || latest="" - echo "Run targets : $RUN_SHA" - echo "PR HEAD now : ${latest:-}" - if [ -n "$latest" ] && [ "$latest" != "$RUN_SHA" ]; then - echo "::error::This run targets $RUN_SHA, but PR #$PR_NUMBER HEAD is now $latest -- the commit is no longer the latest. Failing instead of re-testing stale code on the self-hosted runner; re-run CI on the current commit." - exit 1 - fi - - - name: Checkout - uses: actions/checkout@v7 - - - name: Restore cached test fixtures - # Only the release leg needs fixtures: the sanitizer legs run the - # fixture-free check-sanitizer subset. - if: ${{ matrix.run_matrix }} - # actions/checkout's default clean:true runs `git clean -ffdx`, which - # wipes externals/test-fixtures (gitignored) on this self-hosted - # runner even though its disk otherwise persists across runs. - # fetch-fixtures.sh is already idempotent -- it skips re-downloading - # Alpine packages when externals/test-fixtures/versions.lock still - # matches -- so stash that tree outside the workspace and restore it - # here as a real directory. The qemu lane in tests/test-matrix.sh - # shares the workspace root with the guest over virtio-9p, and a - # symlink pointing outside that root does not resolve inside the - # guest, so this must be a real copy, not a symlink. - run: | - cache="$HOME/.cache/elfuse-ci/test-fixtures" - if [ -d "$cache" ]; then - mkdir -p externals - rm -rf externals/test-fixtures - cp -Rc "$cache" externals/test-fixtures - echo "Restored test fixtures ($(du -sh externals/test-fixtures | cut -f1), lock: $(head -1 externals/test-fixtures/versions.lock 2>/dev/null || echo none))" - else - echo "No fixtures cache at $cache; tests fetch on demand" - fi - - - name: Host info - run: | - sw_vers - uname -a - uname -m - sysctl kern.hv_support || true - test "$(uname -m)" = "arm64" - - - name: Cache Homebrew downloads - uses: actions/cache@v6 - with: - path: ~/Library/Caches/Homebrew/downloads - key: brew-runtime-${{ runner.os }}-${{ runner.arch }}-${{ env.BREW_PKGS }} - - - name: Install missing Homebrew packages - run: | - missing=() - - for pkg in $BREW_PKGS; do - if ! brew list --formula "$pkg" >/dev/null 2>&1; then - missing+=("$pkg") - fi - done - - if [ "${#missing[@]}" -gt 0 ]; then - brew install --quiet "${missing[@]}" - else - echo "All Homebrew packages are already installed: $BREW_PKGS" - fi - - - name: Tool versions - run: | - command -v make - command -v "$GNU_OBJCOPY" - make -V .MAKE.VERSION 2>/dev/null || true - "$GNU_OBJCOPY" --version | head -1 - qemu-aarch64 --version | head -1 || true - python3 --version - - - name: Check Rosetta for Linux - # Rosetta is exercised only by test-matrix (release leg); the - # check-sanitizer subset has no x86_64-via-Rosetta tests. - if: ${{ matrix.run_matrix }} - run: | - ROSETTA=/Library/Apple/usr/libexec/oah/RosettaLinux/rosetta - - if [ ! -x "$ROSETTA" ]; then - echo "::error::Rosetta for Linux runtime was not found at $ROSETTA" - echo - echo "Install Rosetta on the self-hosted Mac runner first:" - echo " sudo softwareupdate --install-rosetta --agree-to-license" - echo - echo "Current /Library/Apple/usr/libexec/oah contents:" - ls -R /Library/Apple/usr/libexec/oah || true - exit 1 - fi - - ls -l "$ROSETTA" - - - name: Build elfuse - # make does not track EXTRA_CFLAGS changes, so an object built for one - # sanitizer must not be reused for another. Checkout already wipes - # build/ (git clean -ffdx), but clean explicitly so the leg builds from - # scratch even on a workspace that was not freshly cleaned. - run: | - make clean - make EXTRA_CFLAGS="$EXTRA_CFLAGS" elfuse - - - name: Verify HVF entitlement is embedded - run: | - codesign -d --entitlements - build/elfuse 2>&1 \ - | grep -q 'com\.apple\.security\.hypervisor' - - - name: test-hello - run: | - make EXTRA_CFLAGS="$EXTRA_CFLAGS" test-hello - - - name: test-multi-vcpu - run: | - make EXTRA_CFLAGS="$EXTRA_CFLAGS" test-multi-vcpu - - - name: make check - # Release runs the full check suite; sanitizer legs run check-sanitizer, - # a representative internal-implementation subset (the release lane plus - # test-matrix already cover Linux syscall compatibility). - run: | - make EXTRA_CFLAGS="$EXTRA_CFLAGS" ${{ matrix.check_target }} - - - name: Test matrix - if: ${{ matrix.run_matrix }} - run: | - bash tests/test-matrix.sh all - - - name: Upload runtime binary - if: ${{ !cancelled() }} - uses: actions/upload-artifact@v7 - with: - name: elfuse-runtime-${{ matrix.sanitizer }}-${{ runner.os }}-${{ runner.arch }} - path: build/elfuse - retention-days: 7 - if-no-files-found: warn - - - name: Save test fixtures cache - # Persist externals/test-fixtures outside the workspace so the next - # run's "Restore cached test fixtures" step can skip re-downloading - # unchanged Alpine packages. Runs even if an earlier step failed, as - # long as the job wasn't cancelled, so a fixture-unrelated test - # failure doesn't cost the next run its cache. - if: ${{ !cancelled() && matrix.sanitizer == 'release' }} - run: | - if [ -d externals/test-fixtures ]; then - cache="$HOME/.cache/elfuse-ci/test-fixtures" - mkdir -p "$(dirname "$cache")" - rm -rf "$cache" - cp -Rc externals/test-fixtures "$cache" - echo "Saved test fixtures ($(du -sh "$cache" | cut -f1))" - else - echo "No externals/test-fixtures to save" - fi diff --git a/.github/workflows/static-analysis.yml b/.github/workflows/static-analysis.yml new file mode 100644 index 00000000..be0f0746 --- /dev/null +++ b/.github/workflows/static-analysis.yml @@ -0,0 +1,210 @@ +# Static analyzers over the macOS Apple Silicon build. +# +# tidy-macos : clang-tidy via `make lint` +# scan-macos : LLVM scan-build via `make analyze` +# infer-macos : Facebook Infer capture + analyze over the full build +name: Static analysis + +on: + push: + branches: [main] + paths-ignore: + - '**.md' + - 'docs/**' + - 'LICENSE' + pull_request: + branches: [main] + paths-ignore: + - '**.md' + - 'docs/**' + - 'LICENSE' + workflow_dispatch: + +# Cancel in-progress runs for the same PR; keep main runs going. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} + +permissions: + contents: read + +jobs: + # clang-tidy via `make lint`. Runs in parallel with build/scan jobs. + # Advisory: .clang-tidy sets WarningsAsErrors='', so findings are logged + # for review but do not gate the job. + tidy-macos: + name: clang-tidy (macOS Apple Silicon) + runs-on: macos-15 + timeout-minutes: 20 + env: + GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy + HOMEBREW_NO_INSTALL_CLEANUP: 1 + HOMEBREW_NO_AUTO_UPDATE: 1 + # binutils is needed because make lint depends on the shim_blob.h + # generated by the assembly + objcopy pipeline. + BREW_PKGS: binutils llvm + CLANG_TIDY: /opt/homebrew/opt/llvm/bin/clang-tidy + 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: Install Homebrew packages + # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. + run: | + set -euo pipefail + brew install --quiet $BREW_PKGS + "$CLANG_TIDY" --version | head -1 + + - name: Generate build/dispatch.h, shim_blob.h, version.h + # `make lint` depends on these generated headers; building the + # full elfuse binary is unnecessary, so just satisfy the deps. + run: make build/shim_blob.h build/version.h build/dispatch.h + + - name: clang-tidy (make lint) + run: make lint + + # LLVM scan-build via `make analyze`. Runs in parallel with build/tidy. + # Advisory: scan-build's Make target does not pass --status-bugs, so + # findings appear in logs and in the uploaded HTML report but do not + # gate the job. + scan-macos: + name: scan-build (macOS Apple Silicon) + runs-on: macos-15 + timeout-minutes: 25 + env: + GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy + HOMEBREW_NO_INSTALL_CLEANUP: 1 + HOMEBREW_NO_AUTO_UPDATE: 1 + BREW_PKGS: binutils llvm + LLVM_BIN: /opt/homebrew/opt/llvm/bin + 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: Install Homebrew packages + # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. + # scan-build has no --version; piping --help into `head -1` makes + # perl take SIGPIPE on the closed stdout and exit non-zero, which + # under pipefail fails the step. Just confirm the binary exists. + run: | + set -euo pipefail + brew install --quiet $BREW_PKGS + test -x "$LLVM_BIN/scan-build" + "$LLVM_BIN/clang" --version | head -1 + + - name: scan-build (make analyze) + run: | + set -euo pipefail + export PATH="$LLVM_BIN:$PATH" + mkdir -p build/scan-build + scan-build -o build/scan-build --use-cc="$(command -v clang)" \ + make -B elfuse + + - name: Upload scan-build report + if: ${{ !cancelled() }} + uses: actions/upload-artifact@v7 + with: + name: scan-build-${{ runner.os }}-${{ runner.arch }} + path: build/scan-build + retention-days: 7 + if-no-files-found: ignore + + # Facebook Infer over the full elfuse build. Must run on macOS Apple + # Silicon because the build needs Hypervisor.framework and -arch arm64; + # Infer captures the real clang invocations, so it sees every TU. + # + # Gating (unlike tidy-macos/scan-macos): a separate step turns Infer's + # report.json into inline ::error:: annotations plus a job summary, then + # fails the job. Findings surface on the PR instead of a silent exit code, + # so bugs are pruned at PR time instead of merged. + infer-macos: + name: Infer (macOS Apple Silicon) + runs-on: macos-15 + timeout-minutes: 25 + env: + GNU_OBJCOPY: /opt/homebrew/opt/binutils/bin/objcopy + HOMEBREW_NO_INSTALL_CLEANUP: 1 + HOMEBREW_NO_AUTO_UPDATE: 1 + BREW_PKGS: binutils + 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: Install GNU objcopy + # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. + run: | + set -euo pipefail + brew install --quiet $BREW_PKGS + "$GNU_OBJCOPY" --version | head -1 + + - name: Setup Infer + # infer_version pins the Infer binary; the action itself tracks the v1 + # tag. + uses: srz-zumix/setup-infer@v1 + with: + infer_version: v1.3.0 + + # .inferconfig disables PULSE_UNINITIALIZED_VALUE repo-wide. Pulse cannot + # prove guest_copy's chunked "while (copied < len)" loop fills its + # destination, so every guest_read_small caller looks uninitialized; the + # findings were audited and every caller checks the return value. The rest + # of the Infer gate is untouched: null dereference, use-after-free, leaks, + # dead stores and stack-address escape all still fail the job. + # + # The cost is real and repo-wide: a genuinely uninitialized read added + # after this point is not caught here. Scoping it narrower was tried and + # is worse -- the findings span thirteen files including syscall.c and + # proc.c, so a path block list suppresses the same class over most of the + # syscall surface while being harder to read, and censor-report does not + # take effect through `infer run` in v1.3.0. `make infer-uninit` re-runs + # the analysis with the checker back on and prints the count, so whether + # an Infer upgrade has made this unnecessary is one command away. + - name: Infer capture + analyze (make -B elfuse) + # -B forces a clean rebuild so Infer captures every translation unit. + # Non-C build steps (shim.S assembly, objcopy) pass through untouched. + # No --fail-on-issue here: `infer run` must exit 0 so the reporting + # step below runs and surfaces findings before the job fails. + # --keep-going tolerates a frontend failure on an odd TU, but that can + # also mask a total capture miss (wrapper never intercepts clang, 0 + # files analyzed). The count guard fails the job on that silent no-op. + run: | + set -euo pipefail + infer run --keep-going -- make -B elfuse 2>&1 | tee infer-run.log + n=$(grep -oE 'Found [0-9]+ source file' infer-run.log \ + | grep -oE '[0-9]+' | tail -1 || true) + echo "Infer captured ${n:-0} source files" + test "${n:-0}" -gt 0 + + - name: Report Infer findings + # Emit GitHub annotations + a job summary from report.json, then exit + # non-zero if any finding exists. Runs even when a prior step failed so + # a partial report is still surfaced. + if: ${{ !cancelled() }} + run: python3 scripts/infer-annotate.py infer-out/report.json + + - name: Upload Infer report + if: ${{ !cancelled() }} + uses: actions/upload-artifact@v7 + with: + name: infer-${{ runner.os }}-${{ runner.arch }} + path: infer-out/report.txt + retention-days: 7 + if-no-files-found: warn diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml new file mode 100644 index 00000000..c4258700 --- /dev/null +++ b/.github/workflows/verify.yml @@ -0,0 +1,254 @@ +# 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 +name: Proofs + +on: + push: + branches: [main] + paths-ignore: + - '**.md' + - 'docs/**' + - 'LICENSE' + pull_request: + branches: [main] + paths-ignore: + - '**.md' + - 'docs/**' + - 'LICENSE' + workflow_dispatch: + +# Cancel in-progress runs for the same PR; keep main runs going. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: ${{ github.event_name == 'pull_request' }} + +permissions: + contents: read + +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. + # + # Runs on Linux with no toolchain: "make print-verify-targets" only reads the + # makefile, so this costs seconds and gates nothing. + proof-targets: + name: Enumerate proof targets + runs-on: ubuntu-latest + outputs: + targets: ${{ steps.list.outputs.targets }} + steps: + - name: Checkout + uses: actions/checkout@v7 + + - name: Read the targets from mk/verify.mk + 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" + + # Frama-C WP proofs of the attacker-facing arithmetic, plus the mutation gate + # that shows those proofs bite. One runner per proof target. + # + # GATING, unlike tidy-macos and scan-macos: the inputs these proofs cover come + # from untrusted binaries and from the guest itself, so an unproved + # obligation fails the job instead of being logged for review. Without this + # 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 }}) + needs: proof-targets + 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: Install Homebrew packages + # shellcheck disable=SC2086 -- BREW_PKGS is a space-separated list. + run: | + set -euo pipefail + brew install --quiet $BREW_PKGS + + # 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 + 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: 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 + + - 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: 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. + 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 + + - name: Upload prover log + if: always() + uses: actions/upload-artifact@v7 + with: + name: verify-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. + 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 + if: always() + runs-on: ubuntu-latest + timeout-minutes: 5 + steps: + - name: Require every matrix leg to have passed + run: | + set -euo pipefail + result='${{ needs.verify-mutants.result }}' + echo "mutation matrix: $result" + [ "$result" = success ] || exit 1 diff --git a/mk/lint.mk b/mk/lint.mk index 82ac7f76..1e47aa03 100644 --- a/mk/lint.mk +++ b/mk/lint.mk @@ -9,7 +9,7 @@ INFER ?= infer # name the tool, name the install, fail on purpose. Without this a developer # running lint/analyze/infer-uninit gets "make: clang-tidy: No such file or # directory / Error 1", which reads like a broken Makefile rather than a -# missing dependency, on three of the eleven CI jobs. +# missing dependency. define require-tool @command -v $(1) >/dev/null 2>&1 || { \ printf " $(RED)%s not found$(RESET) (%s)\n" "$(1)" "$(2)"; \ diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index 4da00998..2b769430 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -892,8 +892,8 @@ def _load_verify_mk(): # 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/main.yml belongs here for the same reason even though it -# never touches a proof: it is what decides, per CI matrix leg, which target +# .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 @@ -911,7 +911,7 @@ def _load_verify_mk(): "mk/verify.mk", "mk/toolchain.mk", "Makefile", - ".github/workflows/main.yml", + ".github/workflows/verify.yml", } diff --git a/scripts/check-proof-targets.py b/scripts/check-proof-targets.py index d3b82205..9f9e694a 100755 --- a/scripts/check-proof-targets.py +++ b/scripts/check-proof-targets.py @@ -5,7 +5,7 @@ keeps them in agreement: 1. mk/verify.mk's VERIFY__SRC entries -- the targets themselves. - 2. .github/workflows/main.yml's verify-mutants matrix -- the CI sharding. + 2. .github/workflows/verify.yml's verify-mutants matrix -- the CI sharding. 3. src/proved/ -- the directory the proved headers live in. The third is the one the directory name rests on. src/proved/ claims its @@ -14,7 +14,7 @@ path. Without this check the directory could hold an unproved file and still read as a guarantee, which is worse than no directory at all. -.github/workflows/main.yml's verify-mutants job shards one runner per proof +.github/workflows/verify.yml's verify-mutants job shards one runner per proof target, and its matrix is fromJson of "make print-verify-targets" rather than a list of its own. What is checked here is that it stays that way, and that the list make generates is the whole list: a VERIFY__SRC block written @@ -107,7 +107,7 @@ def workflow_matrix_is_derived(): matrix faithfully reproduces a target list that silently dropped a block. """ expected = "${{ fromJson(needs.proof-targets.outputs.targets) }}" - text = (ROOT / ".github" / "workflows" / "main.yml").read_text() + 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 # fromJson in a later job. @@ -115,7 +115,7 @@ def workflow_matrix_is_derived(): if not m: print( " could not find verify-mutants' matrix.target in " - ".github/workflows/main.yml; the job may have been renamed or " + ".github/workflows/verify.yml; the job may have been renamed or " "restructured, so update this check to match", file=sys.stderr, ) From 7363e6586e81df558568076389feb07b80ecec4d Mon Sep 17 00:00:00 2001 From: Chun-Hung Tseng Date: Fri, 14 Aug 2026 15:18:43 +0200 Subject: [PATCH 3/5] Run the HVF tests on a manual Build dispatch runtime-macos was gated to push and pull_request, so "Run workflow" on Build ran build-macos alone and reported green with every HVF and sanitizer leg skipped. A skipped required check does not block a merge, as verify-mutants-gate's comment in verify.yml already records, so a manual run could stand in for testing that never happened. The gate predates the split: main.yml carried the same if: under an on: block that already listed workflow_dispatch. Adding the event rather than dropping the trigger keeps the manual re-run, which is what the self-hosted runners need after an outage. The repository guard is untouched, so a fork still cannot reach them. Only the PR-head guard step reads pull_request context and it carries its own if:. --- .github/workflows/build.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index e9373039..234eb28d 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -95,7 +95,8 @@ jobs: needs: build-macos if: > github.repository == 'sysprog21/elfuse' && - (github.event_name == 'push' || github.event_name == 'pull_request') + (github.event_name == 'push' || github.event_name == 'pull_request' || + github.event_name == 'workflow_dispatch') 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 From f5d207055e03edec0bd6d963bb5f45c787a0b6d2 Mon Sep 17 00:00:00 2001 From: Chun-Hung Tseng Date: Fri, 14 Aug 2026 15:21:39 +0200 Subject: [PATCH 4/5] Add build/dispatch.h to lint's prerequisites On a tree without the generated headers, "make lint" fails: src/debug/syscall-hist.c:18:10: error: 'dispatch.h' file not found src/syscall/syscall.c:78:10: error: 'dispatch.h' file not found Found compiler error(s). make: *** [lint] Error 1 The target listed shim_blob.h and version.h only, while clang-tidy runs over $(SRCS), two of whose files include the dispatch.h that $(DISPATCH_HEADER) generates. mk/analysis.mk carried the same list, so the gap predates the split. tidy-macos hid it with a step that generated all three headers before calling make lint, which meant CI never exercised the target's own dependencies. That step goes with the fix. --- .github/workflows/static-analysis.yml | 5 ----- mk/lint.mk | 2 +- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/.github/workflows/static-analysis.yml b/.github/workflows/static-analysis.yml index be0f0746..891998d2 100644 --- a/.github/workflows/static-analysis.yml +++ b/.github/workflows/static-analysis.yml @@ -61,11 +61,6 @@ jobs: brew install --quiet $BREW_PKGS "$CLANG_TIDY" --version | head -1 - - name: Generate build/dispatch.h, shim_blob.h, version.h - # `make lint` depends on these generated headers; building the - # full elfuse binary is unnecessary, so just satisfy the deps. - run: make build/shim_blob.h build/version.h build/dispatch.h - - name: clang-tidy (make lint) run: make lint diff --git a/mk/lint.mk b/mk/lint.mk index 1e47aa03..bb6906b8 100644 --- a/mk/lint.mk +++ b/mk/lint.mk @@ -18,7 +18,7 @@ define require-tool endef ## Run clang-tidy on all source files -lint: $(BUILD_DIR)/shim_blob.h $(BUILD_DIR)/version.h +lint: $(BUILD_DIR)/shim_blob.h $(BUILD_DIR)/version.h $(DISPATCH_HEADER) $(call require-tool,$(CLANG_TIDY),brew install llvm -- or set CLANG_TIDY=) @echo " TIDY src/" $(Q)$(CLANG_TIDY) $(SRCS) -- $(CFLAGS) -Isrc -I$(BUILD_DIR) From 15996f3767b589b3daef2e3f1b1e51cdab6111e2 Mon Sep 17 00:00:00 2001 From: Chun-Hung Tseng Date: Fri, 14 Aug 2026 15:22:55 +0200 Subject: [PATCH 5/5] Fail check-format when shellcheck is missing Without shellcheck on PATH the loop read the shell's 127 as a warning like any other, so the target ended: /bin/sh: shellcheck: command not found ... 39 script(s) have warnings counting scripts none of which was checked. require-tool, which lint, analyze and infer-uninit already call, names the tool and the install and stops there. The command -v guards on shfmt and black in indent are deliberately the other shape: a formatter that skips itself changes nothing, while a checker that skips itself reports a pass it never earned. mk/analysis.mk carried the same loop, so this predates the split. --- mk/format.mk | 1 + 1 file changed, 1 insertion(+) diff --git a/mk/format.mk b/mk/format.mk index 64ff6426..548f6c35 100644 --- a/mk/format.mk +++ b/mk/format.mk @@ -19,6 +19,7 @@ check-format: check-syscall-dispatch $(Q)$(CLANG_FORMAT) --dry-run --Werror $(C_FORMAT_FILES) @echo " MATRIX skip lists" $(Q)bash .ci/check-matrix-lists.sh + $(call require-tool,shellcheck,brew install shellcheck) @printf " SHCHK %d scripts\n" $(words $(SHELL_SCRIPTS)) @fail=0; \ for f in $(SHELL_SCRIPTS); do \