diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 00000000..234eb28d --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,372 @@ +# 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' || + 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 + # 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 4d29e126..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/analysis.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/analysis.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/analysis.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/analysis.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/analysis.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..891998d2 --- /dev/null +++ b/.github/workflows/static-analysis.yml @@ -0,0 +1,205 @@ +# 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: 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/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..548f6c35 --- /dev/null +++ b/mk/format.mk @@ -0,0 +1,51 @@ +# 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 + $(call require-tool,shellcheck,brew install shellcheck) + @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..bb6906b8 --- /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. +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 $(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) + +## 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..2b769430 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,22 +883,17 @@ 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 -# 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 @@ -909,14 +904,14 @@ 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", + ".github/workflows/verify.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..9f9e694a 100755 --- a/scripts/check-proof-targets.py +++ b/scripts/check-proof-targets.py @@ -4,8 +4,8 @@ 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. - 2. .github/workflows/main.yml's verify-mutants matrix -- the CI sharding. + 1. mk/verify.mk's VERIFY__SRC entries -- the targets themselves. + 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,12 +14,12 @@ 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 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 @@ -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, ) @@ -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():