From 62b18d5b2e3542bfea6f7c9a5a28c8b828b5c1c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Onur=20=C3=96zkan?= Date: Sat, 7 Nov 2026 18:12:11 +0300 Subject: [PATCH] build: replace argument dispatch and retain source-bound verification Replace argument recovery with direct build targets. Run host, target, board, coverage, Miri and selected Kani checks while retaining source identities, logs and artifacts, including failed attempts. Keep the PID proof diagnostic exception explicit and match its exact identity alongside passing contract assertions and covers. Validation: final-source verification matrix, assembled workflow tests and documentation build. --- .github/workflows/firmware.yml | 41 ++ Makefile | 137 ++-- docs/Makefile | 46 +- docs/src/boards/geprc-f722-v2.md | 6 +- docs/src/boards/kakute-f7-mini-v3.md | 6 +- docs/src/configuration.md | 2 +- docs/src/development.md | 139 ++-- docs/src/getting-started.md | 19 +- docs/src/index.md | 19 +- docs/src/reference.md | 27 +- firmware/Makefile | 98 +-- firmware/README.md | 12 +- firmware/boards/Makefile | 49 +- firmware/boards/board.mk | 77 +-- firmware/scripts/analyze-fw.py | 17 +- firmware/scripts/report-test-coverage.sh | 179 +++-- firmware/scripts/summarize-test-coverage.py | 22 +- firmware/scripts/test-analyze-fw.py | 75 ++- firmware/scripts/test-build-workflow.py | 321 +++++++++ firmware/scripts/test-verify.py | 443 ++++++++++++ firmware/scripts/verify.py | 710 ++++++++++++++++++++ firmware/tools/configurator/Makefile | 29 +- firmware/verification.toml | 166 +++++ flake.nix | 2 + scripts/make-argv.py | 275 -------- scripts/test-make-argv.py | 312 --------- 26 files changed, 2177 insertions(+), 1052 deletions(-) create mode 100644 .github/workflows/firmware.yml create mode 100644 firmware/scripts/test-build-workflow.py create mode 100644 firmware/scripts/test-verify.py create mode 100644 firmware/scripts/verify.py create mode 100644 firmware/verification.toml delete mode 100644 scripts/make-argv.py delete mode 100644 scripts/test-make-argv.py diff --git a/.github/workflows/firmware.yml b/.github/workflows/firmware.yml new file mode 100644 index 0000000..ae45d5a --- /dev/null +++ b/.github/workflows/firmware.yml @@ -0,0 +1,41 @@ +name: Firmware gates + +on: + pull_request: + push: + workflow_dispatch: + +permissions: + contents: read + +env: + CARGO_BUILD_JOBS: 2 + +jobs: + verification: + name: Source-bound firmware verification + runs-on: ubuntu-24.04 + timeout-minutes: 90 + steps: + - name: Check out source + uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 + - name: Install Nix + uses: cachix/install-nix-action@75c75c31ebece974e48ebc36b4ad125bd97bd97b # v31 + - name: Fetch pinned dependencies + working-directory: firmware + run: nix develop .. -c cargo fetch --locked + - name: Install the coverage compiler and matching LLVM tools + run: nix develop -c rustup toolchain install nightly-2025-08-01 --profile minimal --component llvm-tools-preview + - name: Install manifest-pinned Miri and Kani tools + run: nix develop -c make verification-tools + - name: Host, target, board, coverage, Miri and Kani gates + run: nix develop -c make verification + - name: Retain verification evidence, including failed attempts + if: always() + uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2 + with: + name: firmware-verification + path: | + firmware/target/verification/** + firmware/target/verification-tools/setup-*/*.log + if-no-files-found: warn diff --git a/Makefile b/Makefile index b134d2b..a99d080 100644 --- a/Makefile +++ b/Makefile @@ -1,115 +1,88 @@ -override SHELL := /bin/sh -override MAKEFLAGS += --no-print-directory +SHELL := /bin/sh +MAKEFLAGS += --no-print-directory +export CARGO_BUILD_JOBS ?= 2 .DEFAULT_GOAL := help .DELETE_ON_ERROR: -override FIRMWARE_DIR := firmware -override DOCS_DIR := docs -override CONFIGURATOR_DIR := firmware/tools/configurator -override BOARD_DIRS := $(patsubst %/,%,$(wildcard firmware/boards/*/)) - -override COMPONENT_TARGETS := $(FIRMWARE_DIR) $(DOCS_DIR) firmware/boards $(BOARD_DIRS) \ - $(CONFIGURATOR_DIR) - -override PRIMARY_GOAL := $(firstword $(MAKECMDGOALS)) -override ROUTED_GOAL := $(filter $(PRIMARY_GOAL),$(COMPONENT_TARGETS)) - -ifneq ($(ROUTED_GOAL),) - -# The dispatcher reads the original argv so application arguments retain their -# ordering and boundaries even when Make interprets them as goals or variables. -override ROUTE_DEFAULT_TARGET := run -override ROUTE_LOCAL_TARGETS := help -ifeq ($(PRIMARY_GOAL),$(FIRMWARE_DIR)) -override ROUTE_LOCAL_TARGETS += fmt clippy test docs pre-commit check clean -endif -ifeq ($(PRIMARY_GOAL),$(DOCS_DIR)) -override ROUTE_DEFAULT_TARGET := check -override ROUTE_LOCAL_TARGETS += check -endif -ifneq ($(filter $(PRIMARY_GOAL),$(BOARD_DIRS)),) -override ROUTE_LOCAL_TARGETS += flash -endif - -.PHONY: $(PRIMARY_GOAL) - -$(PRIMARY_GOAL): - +@exec python3 scripts/make-argv.py route "$(PRIMARY_GOAL)" make \ - $(ROUTE_DEFAULT_TARGET) $(ROUTE_LOCAL_TARGETS) - -# Additional command-line words are application arguments, not outer targets. -.DEFAULT: - @: - -else - -.PHONY: help nix-shell build fmt test pre-commit check clean +.NOTPARALLEL: +.PHONY: help nix-shell build boards docs configurator fmt test app-native-test coverage verification verification-tools miri kani verification-inventory pre-commit check clean help: ## Show the command interface (the default) @printf '%s\n' 'Kaptan developer commands' '' \ - 'Usage: make -- [arguments...]' \ - ' make help' \ - '' 'The -- is the standard end of Make options; application flags follow it.' \ - '' 'Repository workflows' \ + 'Usage: make ' '' \ ' help Show this help' \ ' nix-shell Enter the Nix development shell' \ ' build Build all firmware and documentation' \ + ' boards Build and package every board' \ + ' docs Test and build the mdBook project' \ + ' configurator Start the local configurator web application' \ ' fmt Check Rust, shell, Python, Nix, and TOML formatting' \ - ' test Run Rust and script tests' \ + ' test Run shared-library, host algorithm, and script tests' \ + ' app-native-test Check the app UTF conversion function with a host API stub' \ + ' coverage Required final strict-core line/branch coverage gate' \ + ' verification Run all gates and retain source-bound evidence' \ + ' verification-tools Install the pinned Miri and Kani tools' \ + ' miri Run the manifest-selected Miri checks' \ + ' kani Run the manifest-selected Kani proofs' \ + ' verification-inventory Show verification owners, claims and gaps' \ ' pre-commit Run fmt, firmware clippy/test/docs, and mdBook checks' \ ' check Run pre-commit plus whitespace checks' \ ' clean Remove generated build artifacts' \ - '' 'Directory targets' \ - ' firmware fmt, clippy, test, docs, pre-commit, check, or clean' \ - ' firmware -- Pass other arguments to cargo' \ - ' firmware/boards -- ' \ - ' Build and package every board; args go to cargo build' \ - ' firmware/boards/ -- ' \ - ' Build and package one board; args go to cargo build' \ - ' firmware/boards/ flash -- ' \ - ' Build, package, and flash one board over DFU' \ - ' docs Test and build the mdBook project' \ - ' docs -- Pass explicit arguments to mdbook' \ - ' firmware/tools/configurator -- ' \ - ' Pass args to kaptan-configurator' \ - '' 'Examples' \ - ' make firmware -- test --workspace --locked --offline' \ - ' make firmware clippy' \ - ' make firmware docs' \ - ' make firmware/boards/kakute-f7-mini-v3' \ - ' make firmware/boards/kakute-f7-mini-v3 flash' \ - ' make docs -- build' \ - ' make firmware/tools/configurator' + '' 'Component workflows' \ + ' make -C firmware help' \ + ' make -C firmware/boards/ build|flash' \ + ' make -C docs build|test|check|clean' \ + '' 'Native tools (run from firmware/)' \ + ' make test' \ + ' cargo run --locked --offline -p kaptan-configurator -- --baud 115200' nix-shell: ## Enter the reproducible Nix development shell nix develop -build: ## Build all firmware boards and documentation - +@$(MAKE) -C firmware/boards run - +@$(MAKE) -C $(DOCS_DIR) run -- build +build: boards ## Build all firmware boards and documentation + +@$(MAKE) -C docs build + +boards: + +@$(MAKE) -C firmware/boards build + +docs: + +@$(MAKE) -C docs check + +configurator: + +@$(MAKE) -C firmware/tools/configurator run fmt: - +@$(MAKE) -C $(FIRMWARE_DIR) fmt + +@$(MAKE) -C firmware fmt shfmt -d $$(rg --files -g '*.sh') ruff format --check $$(rg --files -g '*.py') + ruff check firmware/scripts nixfmt --check $$(rg --files -g '*.nix') taplo format --check $$(rg --files -g '*.toml') test: - python3 -m unittest scripts/test-make-argv.py - +@$(MAKE) -C $(FIRMWARE_DIR) test + +@$(MAKE) -C firmware test + +@$(MAKE) app-native-test + +app-native-test: + python3 ground_suite/windows/runner/test_utf8_from_utf16.py \ + --work-dir "$(or $(CARGO_TARGET_DIR),target)/native-tests/utf8" + +coverage: + +@$(MAKE) -C firmware coverage + +verification verification-tools miri kani verification-inventory: + +@$(MAKE) -C firmware $@ pre-commit: fmt test - +@$(MAKE) -C $(FIRMWARE_DIR) clippy - +@$(MAKE) -C $(FIRMWARE_DIR) docs - +@$(MAKE) -C $(DOCS_DIR) check + +@$(MAKE) -C firmware clippy + +@$(MAKE) -C firmware docs + +@$(MAKE) -C docs check + @printf '%s\n' 'Pre-commit passed. Coverage was not run; make coverage is a required final gate.' check: pre-commit ## Run pre-commit plus whitespace checks git diff HEAD --check clean: ## Remove firmware and documentation build artifacts - +@$(MAKE) -C $(FIRMWARE_DIR) clean - +@$(MAKE) -C $(DOCS_DIR) run -- clean - -endif + +@$(MAKE) -C firmware clean + +@$(MAKE) -C docs clean diff --git a/docs/Makefile b/docs/Makefile index ddce0dd..cdad57a 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -1,38 +1,26 @@ -override SHELL := /bin/sh -override MAKEFLAGS += --no-print-directory +SHELL := /bin/sh +MAKEFLAGS += --no-print-directory .DEFAULT_GOAL := help .DELETE_ON_ERROR: -override MDBOOK := mdbook - -override PRIMARY_GOAL := $(firstword $(MAKECMDGOALS)) - -ifeq ($(PRIMARY_GOAL),run) - -.PHONY: run - -# Application arguments may also look like Make goals. The run recipe recovers -# their exact boundaries from the original invocation. -.DEFAULT: - @: - -else - -.PHONY: help run check +.PHONY: help build test check clean help: - @printf '%s\n' 'Usage: make docs -- ' '' \ - 'With no arguments, mdbook test and mdbook build are run.' \ - 'Example: make docs -- build' '' \ - 'Project target:' \ - ' check Run mdbook test and mdbook build' + @printf '%s\n' 'Usage: make -C docs build|test|check|clean' '' \ + ' build Build the book' \ + ' test Test book examples' \ + ' check Test and build the book' \ + ' clean Remove generated documentation' '' \ + 'For other options, run mdbook directly from docs/.' -endif +build: + mdbook build -check: - $(MDBOOK) test - $(MDBOOK) build +test: + mdbook test -run: - @exec python3 ../scripts/make-argv.py exec run $(MDBOOK) +check: test build + +clean: + mdbook clean diff --git a/docs/src/boards/geprc-f722-v2.md b/docs/src/boards/geprc-f722-v2.md index c83b696..b09fb5a 100644 --- a/docs/src/boards/geprc-f722-v2.md +++ b/docs/src/boards/geprc-f722-v2.md @@ -14,7 +14,7 @@ pins PB0/PB1/PB4/PB5 low. From the repository root: ```sh -make firmware/boards/geprc-f722-v2 +make -C firmware/boards/geprc-f722-v2 build ``` The packaging script validates the ELF against the shared F722 linker layout @@ -31,7 +31,7 @@ listed `0483:df11` target before flashing: ```sh dfu-util --list -make firmware/boards/geprc-f722-v2 flash +make -C firmware/boards/geprc-f722-v2 flash ``` ## MAVLink over USB @@ -41,7 +41,7 @@ enumerates as `Kaptan / GEPRC TAKER F722 V2 (ICM-42688-P)`, normally `/dev/ttyACM*` on Linux. Run: ```sh -make firmware/tools/configurator +make configurator ``` Open `http://127.0.0.1:4861` and connect `/dev/serial/by-id/` or diff --git a/docs/src/boards/kakute-f7-mini-v3.md b/docs/src/boards/kakute-f7-mini-v3.md index 12bdb44..4164ea1 100644 --- a/docs/src/boards/kakute-f7-mini-v3.md +++ b/docs/src/boards/kakute-f7-mini-v3.md @@ -15,7 +15,7 @@ motor pins PB0/PB1/PB4/PB5/PB6/PB7 low. From the repository root: ```sh -make firmware/boards/kakute-f7-mini-v3 +make -C firmware/boards/kakute-f7-mini-v3 build ``` The packaging script uses the shared F722 linker layout and prints the flash @@ -37,7 +37,7 @@ application offset. ```sh dfu-util --list -make firmware/boards/kakute-f7-mini-v3 flash +make -C firmware/boards/kakute-f7-mini-v3 flash ``` ## MAVLink over USB @@ -47,7 +47,7 @@ enumerates as `Kaptan / Kakute F7 Mini V3`, normally `/dev/ttyACM*` on Linux. Then launch the target-described web UI: ```sh -make firmware/tools/configurator +make configurator ``` Open `http://127.0.0.1:4861` and connect `/dev/serial/by-id/` or diff --git a/docs/src/configuration.md b/docs/src/configuration.md index 2ba6b61..fb0cbbe 100644 --- a/docs/src/configuration.md +++ b/docs/src/configuration.md @@ -58,7 +58,7 @@ Build and flash the board image, boot normally, connect the board's USB port, and run from the repository root: ```sh -make firmware/tools/configurator +make configurator ``` Open `http://127.0.0.1:4861`, enter the device path in the Connection section, diff --git a/docs/src/development.md b/docs/src/development.md index be7f919..f8a8751 100644 --- a/docs/src/development.md +++ b/docs/src/development.md @@ -1,57 +1,118 @@ # Development and verification -## Command layout +Use the locked Nix shell. Run Cargo from `firmware/`, which pins Rust 1.90.0. +Keep total Cargo concurrency at two jobs. `make help` lists repository commands. -Each component owns its Makefile: the Cargo workspace, all-board workflows, -individual boards, tools, and documentation each define commands in their own -directory. The root Makefile contains repository-wide workflows and routes a -directory path to that directory's Makefile. +## Setup and required gates -The standard `--` ends Make's own options. Every following argument uses the -selected application's native command line. For example, -`make firmware -- test --workspace --locked --offline` runs `cargo test ---workspace --locked --offline` from `firmware`. Board paths are -the complete build-and-package command, so they need no invented operation -name. - -## Fast host checks +From the repository root: ```sh -make firmware -- fmt --all --check -make firmware -- test --workspace --locked --offline -make firmware -- clippy --workspace --all-targets \ - --exclude kaptan-geprc-f722-v2 \ - --exclude kaptan-kakute-f7-mini-v3 --locked --offline -- -D warnings +nix develop -c sh -c 'cd firmware && cargo fetch --locked' +nix develop -c rustup toolchain install nightly-2025-08-01 \ + --profile minimal --component llvm-tools-preview +nix develop -c make verification-tools +nix develop -c make verification ``` -## Target checks +Setup needs network access. Verification uses offline dependencies and runs +host, target, board, coverage, Miri and Kani gates sequentially. Kani runs one +harness at a time. Firmware CI runs +the same command and retains evidence on failure. Keep source fixed during a run. + +| Command, inside `nix develop` | Scope | +| --- | --- | +| `make pre-commit` | Formatting, host tests, host/embedded Clippy, API docs and mdBook. Does not run coverage. | +| `make -C firmware target-checks` | Sensor-free consumers, the portable runtime on ARM, and linked RTIC cross-route fixtures. | +| `make boards` | Both release board images and final-image placement checks. | +| `make coverage` | Strict core line/branch gate and informational totals for other host crates. | +| `make miri` / `make kani` | Manifest-selected checks with their own evidence receipts. | +| `make verification-inventory` | Package ownership, property claims, assumptions and gaps. | +| `env CARGO_BUILD_JOBS=1 make -j1 -C docs check` | Test examples and render mdBook. Review changed links and anchors separately. | + +Host gates exclude the two bare-metal boards and include platform contracts. +They enable `kaptan-navigation/sensor-snapshots`. Navigation itself is unconditional. +Host platform tests must not invoke MMIO. Rust 1.90.0 runs all doctests and +compile-pass/fail fixtures. The test gate also runs the configurator's Node tests, +Python script tests, release-LTO final-link cases and the UTF conversion helper. + +Run the native helpers separately with `make -C firmware native-test` and +`make app-native-test`. The default artifact directories are +`firmware/target/native-tests/final-link/` and `target/native-tests/utf8/`. +`CARGO_TARGET_DIR` relocates them. The UTF helper uses a host +API stub and 16-bit `wchar_t`; it does not build the Windows runner. See the +[final-link fixture](../../firmware/libs/kaptan-err-reportable-macros/tests/final_link.md) +for its archive-extraction limit. + +## Evidence and proof scope + +[verification.toml](../../firmware/verification.toml) owns exact tool versions, +package/harness selection, required covers, claims, assumptions and gaps. Every +workspace package must have one verification area. + +By default, each run creates a new directory under `firmware/target/verification/`. It retains +tracked and nonignored untracked source, hashes, Git state, commands, tool +identities, logs, Kani exports, successful coverage reports, board ELF/binary +artifacts and `receipt.json`. Source drift fails the receipt. To choose a fresh +output directory: ```sh -make firmware/boards -make firmware -- clippy \ - -p kaptan-geprc-f722-v2 -p kaptan-kakute-f7-mini-v3 \ - --target thumbv7em-none-eabihf --locked --offline -- -D warnings +nix develop -c python3 firmware/scripts/verify.py all --output /tmp/kaptan-review ``` -`make firmware docs` builds Rust API documentation with warnings denied. -`make docs` checks and builds the separate mdBook project. `make pre-commit` -runs both documentation checks along with repository formatting, host and -embedded Clippy, Rust and script tests. `make check` -adds a whitespace check. `make build` builds and packages release firmware and -builds the mdBook project. +Miri checks executed paths and schedules, not all interleavings or physical DMA. +Kani checks the manifest's component contracts with default checks and unwind +assertions enabled. Required covers must be satisfied. Missing results, timeouts, +unsupported operations and unexpected failures fail the gate. -## Strict core coverage +The PID result has one qualification: finite operands can overflow to opposite +infinities whose sum is NaN. The implementation rejects that intermediate value +before changing state. Kani's raw verdict remains `Failure`. The runner accepts +only the exact declared diagnostic, function and location, with the contract +assertions and covers satisfied. Reviewed unreachable automatic checks are +recorded separately. No check is disabled or input domain narrowed. A passing +repository receipt therefore does not mean every raw Kani verdict passed. -```sh -cd firmware -scripts/report-test-coverage.sh -``` +These checks do not establish numerical accuracy, vehicle stability, arbitrary +safety histories, MMIO behavior or MCU timing. Kani's +[UB coverage](https://model-checking.github.io/kani/undefined-behaviour.html) and +[floating-point models](https://model-checking.github.io/kani/rust-feature-support.html#floating-point-operations) +have further limits. Source review and independent numerical evidence remain +required. No certification or tool qualification is claimed. -The strict gate requires 100% line and branch coverage for `kaptan-math`, -`kaptan-navigation`, `kaptan-control`, and `kaptan-safety`. It isolates each -core package's coverage artifacts, unions LCOV source-line records, and uses -full LLVM source spans to merge generic branch instantiations without lowering -the gate. +## Compiler contracts + +| Contract | Enforcement and limit | +| --- | --- | +| Frames, rotation direction and position versus velocity | Distinct types and compile-fail examples. Raw sensor labeling still needs validation. | +| Allocator motor count | Const-generic dimensions. These do not establish physical mixer geometry. | +| Validated configuration and output authority | Private fields and distinct types, with compile-fail examples. Constructors and current admission policy remain responsible for validation. | +| Numerical-core unsafe operations | `forbid(unsafe_code)` in math, navigation, control, safety and runtime. Dependencies and generated export attributes remain separate boundaries. | +| Representation limits | Const assertions for navigation masks, field counts, runtime size and board storage. Object size does not measure peak stack. | +| Schemas and UART catalogs | Derive diagnostics and const validation. Received settings still need runtime validation. | +| Shared resources | Rust ownership and RTIC's resource graph. Device completion, barriers and MMIO validity remain hardware obligations. | +| Error IDs and flash-busy placement | Release final-link fixtures and packaged ELF checks, within their documented linker scope. | + +Strict Clippy retains unsafe-operation and undocumented-unsafe-block lints. +A target or feature excluded from a build is not checked by that build. + +## Coverage + +`cargo-llvm-cov 0.8.7` comes from the locked Nix shell. The script selects +`nightly-2025-08-01`, its matching LLVM tools and the `dev` profile. Normal gates +keep Rust 1.90.0. Reports default to `firmware/target/test-coverage/`; an absolute +`CARGO_TARGET_DIR` relocates them. The verification runner uses a separate build directory. + +Math, navigation, control and safety require 100% lines and branch outcomes. +Empty denominators fail. The summarizer unions LCOV source lines and LLVM branch +spans across generic instantiations. Other totals are informational, but any +test/report failure fails the gate. An absent instrumented host body is unavailable. + +All host-testable members are included. Navigation enables `sensor-snapshots` +and MAVLink enables `sensor-telemetry`. Compiler-diagnostic fixtures remain on +Rust 1.90.0: coverage selects `--lib --test section` for `kaptan-config-derive` +and `--lib` for `kaptan-err-reportable-macros`. Their reported runtime coverage +does not establish compiler-phase macro coverage. ## Ground suite builds diff --git a/docs/src/getting-started.md b/docs/src/getting-started.md index 6af039a..683b465 100644 --- a/docs/src/getting-started.md +++ b/docs/src/getting-started.md @@ -17,14 +17,29 @@ From the repository root, discover the developer commands with: make help ``` -Run the repository checks with: +Fetch the pinned Rust dependencies once before the offline checks: + +```sh +cd firmware +cargo fetch --locked +``` + +From the repository root, run the checks with: ```sh make pre-commit +make coverage ``` Bare-metal board packages are not host-test targets. Check them with the target-specific commands in [Development and verification](development.md). +Pre-commit does not run coverage. The separate required coverage gate needs +the dated nightly setup documented there. Shared navigation and sensor snapshot +conversion remain covered through `kaptan-navigation/sensor-snapshots`. + +For the app, enter `nix develop .#ground-suite`. Its locked Flutter and Dart +tools are separate from the firmware shell. App analysis +and web/Linux build commands are listed in the development guide. ## Repository layout @@ -45,7 +60,7 @@ The manual is an [mdBook](https://rust-lang.github.io/mdBook/) project. The repository's Nix development shell provides the checked tool version: ```sh -nix develop -c make docs -- build +nix develop -c make -C docs build ``` The generated static site is written to `target/docs/`. diff --git a/docs/src/index.md b/docs/src/index.md index 16483eb..96aff9f 100644 --- a/docs/src/index.md +++ b/docs/src/index.md @@ -1,8 +1,6 @@ # Overview -Kaptan is an embedded Rust flight-controller project. This manual is the -single source of project documentation: board support, safety boundaries, -development workflow, and design references live here as Markdown. +Kaptan is an embedded Rust flight-controller project. > **Status:** The board images do not yet run the flight runtime or implement > motor drivers. Motor pins are inhibited at startup. Physical flight has not @@ -15,19 +13,10 @@ development workflow, and design references live here as Markdown. - Board work belongs under [Boards](boards/index.md). - [Configuration](configuration.md) explains target-described user settings and immutable F722 hardware policy. -- [Logs](logs.md) and [Errors](errors.md) describe the custom MAVLink - observability surface and its current safety scope. +- [Logs](logs.md) and [Errors](errors.md) describe MAVLink diagnostics. - Before submitting changes, follow [Development and verification](development.md). ## Documentation conventions -Documentation is centralized in `docs/src/`; individual crates and board -directories do not carry README files. The top-level `firmware/README.md` -only defines the firmware workspace boundary. Keep pages in Markdown, add each -page to `SUMMARY.md`, and place commands beside the assumptions and safety -boundary they depend on. - -The current configuration contract is target-described. Each F722 board exposes -only values consumed by that compiled target. Physical F722 hardware selection -remains immutable board policy. No writable -snapshot can bypass an immutable safety decision. +Keep documentation in `docs/src/`, add pages to `SUMMARY.md`, and place commands +beside their prerequisites. diff --git a/docs/src/reference.md b/docs/src/reference.md index 034b510..5d1a5da 100644 --- a/docs/src/reference.md +++ b/docs/src/reference.md @@ -1,31 +1,24 @@ # Reference -This page collects stable limits and points to the detailed contracts. - | Surface | Current contract | | --- | --- | | F722 persistence | One bounded native-width scalar snapshot inside each slot of a power-loss-safe two-slot flash journal. | -| Public config artifact | One canonical self-describing KCFG file containing generated metadata, factory values, and the complete committed candidate. | +| Public config artifact | Canonical KCFG v3 with generated metadata, finite/nonzero flags, factory values, selected-view values and exact expected-base values. | +| Flight profile | Generated schema and required compiled installation for the portable runtime. See [Configuration](configuration.md#flight-configuration). | +| Navigation service | Fusion, prediction and initialization completion run on due 100-Hz control service. Early ticks supervise cached evidence; admission alone cannot renew capabilities. | +| Navigation model bound | Navigation-owned 25-m/sĀ² free-flight acceleration envelope, checked against the complete profile's thrust and mass. Contact impulses are outside this bound. | | File transfer | Custom `FILE_CONTROL` (51025) and `FILE_DATA` (51026), one owner-bound stop-and-wait transfer, 246-byte data chunks, CRC-32C. | | Diagnostics | `LOG` (51020) for macro-produced level/text; `ERROR` (51021) for a bounded reportable `{ error_id, raised_at[96] }` firmware error. | -| Publications | Kaptan-native `HEARTBEAT` (51027), `IMU` (51028), `RANGE` (51029), and `OPTICAL_FLOW` (51030); exact integer units and monotonic `u64` microseconds. | +| Publications | Kaptan-native `HEARTBEAT` (51027), `IMU` (51028), `RANGE` (51029), and `OPTICAL_FLOW` (51030). IMU has a 28-byte payload, extra CRC 22 and `i32` mrad/s gyro axes. | +| F722 clock | Shared TIM2 1-MHz epoch, CC1 100-Hz service. DWT is reserved for the SRAM flash-poll timeout. | | F722 configuration | `/config/user.kcfg`; target-described fields and board factory values over local USB CDC-ACM or a directly wired unsigned UART with motor outputs physically inhibited. | Read [Configuration](configuration.md) for configuration ownership, artifact, -and file contracts, [Logs](logs.md) for receiver decoding and filtering, and +and file contracts, [Architecture](architecture.md#monotonic-time) for clock +assumptions, [Logs](logs.md) for receiver decoding and filtering, and [Errors](errors.md) for reportable errors and panic scope. ## Verification -Before review, run: - -```sh -make pre-commit -make build -``` - -The target-specific lint verifies the local configuration receiver and journal -path. The host suite separately asserts that configuration ingress cannot reach -an actuator path. The ELF checks prove that the flash-busy operation is linked -into executable SRAM and reject compiler-outlined control flow or PC-relative -literal loads outside that section. +Use [Development and verification](development.md) for the required gates, +tool setup and evidence limits. diff --git a/firmware/Makefile b/firmware/Makefile index 42ec754..80f53b8 100644 --- a/firmware/Makefile +++ b/firmware/Makefile @@ -1,65 +1,58 @@ -override SHELL := /bin/sh -override MAKEFLAGS += --no-print-directory +SHELL := /bin/sh +MAKEFLAGS += --no-print-directory export CARGO_BUILD_JOBS ?= 2 .DEFAULT_GOAL := help .DELETE_ON_ERROR: -override CARGO := cargo -override PYTHON := python3 -override CARGO_FLAGS := --locked --offline - override BOARDS := geprc-f722-v2 kakute-f7-mini-v3 override BOARD_PACKAGES := $(addprefix kaptan-,$(BOARDS)) override BOARD_PACKAGE_ARGS := $(addprefix -p ,$(BOARD_PACKAGES)) override HOST_EXCLUDES := $(addprefix --exclude ,$(BOARD_PACKAGES)) +override HOST_FEATURES := --features kaptan-navigation/sensor-snapshots -override PRIMARY_GOAL := $(firstword $(MAKECMDGOALS)) - -run: - @exec python3 ../scripts/make-argv.py exec run $(CARGO) - -ifeq ($(PRIMARY_GOAL),run) - -.PHONY: run - -# Application arguments may also look like Make goals. The run recipe recovers -# their exact boundaries from the original invocation. -.DEFAULT: - @: - -else - -.PHONY: help run fmt clippy test native-test docs pre-commit check clean +.NOTPARALLEL: +.PHONY: help fmt clippy test native-test docs coverage target-checks verification verification-tools miri kani verification-inventory pre-commit check clean help: - @printf '%s\n' 'Usage: make firmware -- ' '' \ - 'Example: make firmware -- test --workspace --locked --offline' '' \ + @printf '%s\n' 'Usage: make -C firmware ' '' \ 'Workspace targets:' \ ' fmt Check Rust formatting' \ ' clippy Run host and embedded Clippy checks' \ ' test Run Rust and firmware script tests' \ ' native-test Check cross-crate error IDs at Rust/C++ release final link' \ ' docs Build Rust API documentation with warnings denied' \ + ' coverage Required final strict-core line/branch coverage gate' \ + ' verification Run all gates and retain source-bound evidence' \ + ' verification-tools Install the pinned Miri and Kani tools' \ + ' miri Run the manifest-selected Miri checks' \ + ' kani Run the manifest-selected Kani proofs' \ + ' verification-inventory Show verification owners, claims and gaps' \ + ' target-checks Check sensor-free consumers and link cross-route fixtures' \ ' pre-commit Run fmt, clippy, test, and docs' \ ' check Alias for pre-commit' \ - ' clean Remove Cargo build artifacts' + ' clean Remove Cargo build artifacts' '' \ + 'For other Cargo options, run cargo directly from firmware/.' \ + 'Host gates exclude bare-metal boards; navigation/sensor-snapshots is enabled.' fmt: - $(CARGO) fmt --all --check + cargo fmt --all --check clippy: - $(CARGO) clippy --workspace --all-targets $(HOST_EXCLUDES) \ - $(CARGO_FLAGS) -- -D warnings - $(CARGO) clippy -p platform-stm32f7 --all-targets \ - $(CARGO_FLAGS) -- -D warnings - $(CARGO) clippy $(BOARD_PACKAGE_ARGS) --target thumbv7em-none-eabihf \ - $(CARGO_FLAGS) -- -D warnings + cargo clippy --workspace --all-targets $(HOST_EXCLUDES) \ + $(HOST_FEATURES) --locked --offline -- -D warnings + cargo clippy -p platform-stm32f7 --all-targets \ + --locked --offline -- -D warnings + cargo clippy $(BOARD_PACKAGE_ARGS) $(addprefix --bin ,$(BOARD_PACKAGES)) --target thumbv7em-none-eabihf \ + --locked --offline -- -D warnings test: - $(CARGO) test --workspace $(CARGO_FLAGS) - $(PYTHON) -m unittest \ - scripts/test-analyze-fw.py scripts/test-summarize-test-coverage.py + cargo +1.90.0 test --workspace $(HOST_EXCLUDES) $(HOST_FEATURES) --locked --offline + cargo +1.90.0 test -p platform-stm32f7 -p synopsys-usb-otg --lib --locked --offline + node --test tools/configurator/web/view.test.cjs + python3 -m unittest scripts/test-analyze-fw.py \ + scripts/test-summarize-test-coverage.py scripts/test-build-workflow.py \ + scripts/test-verify.py +@$(MAKE) native-test native-test: @@ -67,14 +60,37 @@ native-test: --work-dir "$(or $(CARGO_TARGET_DIR),target)/native-tests/final-link" docs: - RUSTDOCFLAGS='-D warnings' $(CARGO) doc --workspace --no-deps \ - $(HOST_EXCLUDES) $(CARGO_FLAGS) + RUSTDOCFLAGS='-D warnings' cargo doc --workspace --no-deps \ + $(HOST_EXCLUDES) $(HOST_FEATURES) --locked --offline + +coverage: + scripts/report-test-coverage.sh + +verification: + python3 scripts/verify.py all + +verification-tools: + python3 scripts/verify.py setup + +miri kani: + python3 scripts/verify.py $@ + +verification-inventory: + python3 scripts/verify.py inventory + +target-checks: + cargo check -p kaptan-configurator -p kaptan-diagnostics-mavlink --locked --offline + cargo check -p kaptan-mavlink -p kaptan-log --no-default-features --locked --offline + cargo check -p kaptan-flight-runtime --no-default-features \ + --target thumbv7em-none-eabihf --locked --offline + RUSTFLAGS='-C link-arg=-Tlink.x -L platforms/stm32f7/link/f722' \ + cargo build -p platform-stm32f7 --example mpu_dual_uart --example icm_dual_uart \ + --release --target thumbv7em-none-eabihf --locked --offline pre-commit: fmt clippy test docs + @printf '%s\n' 'Pre-commit passed. Coverage was not run; make coverage is a required final gate.' check: pre-commit clean: - $(CARGO) clean - -endif + cargo clean diff --git a/firmware/README.md b/firmware/README.md index 4d195ac..f1a1293 100644 --- a/firmware/README.md +++ b/firmware/README.md @@ -11,17 +11,15 @@ firmware/ ā””ā”€ā”€ scripts/ packaging, analysis, and coverage helpers ``` -This workspace owns its Makefile. From this directory, list its commands with: +List commands from this directory: ```sh make help ``` -From the repository root, the firmware path is a direct Cargo proxy. For -example, `make firmware -- test --workspace --locked --offline` runs the host -test suite. Build and package every supported board with -`make firmware/boards`, or select one board by its directory path. -Run `make firmware clippy` for Rust lints and `make firmware docs` for API -documentation with warnings denied. +Run Cargo directly from this directory. Build and package every supported board +with `make -C boards build`, or one with `make -C boards/ build`. +The workspace pins Rust 1.90.0. See +[development checks](../docs/src/development.md) for the supported workflows. The board images do not yet run the flight runtime or implement motor drivers. Motor pins are inhibited at startup. Physical flight has not been qualified. diff --git a/firmware/boards/Makefile b/firmware/boards/Makefile index 394d1fb..1226c51 100644 --- a/firmware/boards/Makefile +++ b/firmware/boards/Makefile @@ -1,44 +1,31 @@ -override SHELL := /bin/sh -override MAKEFLAGS += --no-print-directory +SHELL := /bin/sh +MAKEFLAGS += --no-print-directory +export CARGO_BUILD_JOBS ?= 2 .DEFAULT_GOAL := help .DELETE_ON_ERROR: -override CARGO := cargo -override CARGO_FLAGS := --locked --offline - override EMBEDDED_TARGET := thumbv7em-none-eabihf -override TARGET_DIR := ../target/$(EMBEDDED_TARGET)/release -override SCRIPTS_DIR := ../scripts +CARGO_TARGET_DIR ?= ../target +override TARGET_DIR := $(CARGO_TARGET_DIR)/$(EMBEDDED_TARGET)/release override BOARDS := geprc-f722-v2 kakute-f7-mini-v3 override BOARD_PACKAGES := $(addprefix kaptan-,$(BOARDS)) override BOARD_PACKAGE_ARGS := $(addprefix -p ,$(BOARD_PACKAGES)) +override BOARD_BIN_ARGS := $(addprefix --bin ,$(BOARD_PACKAGES)) -override PRIMARY_GOAL := $(firstword $(MAKECMDGOALS)) - -run: - @exec python3 ../../scripts/make-argv.py exec run $(CARGO) build --release \ - $(CARGO_FLAGS) $(BOARD_PACKAGE_ARGS) --target $(EMBEDDED_TARGET) - @set -e; for board in $(BOARD_PACKAGES); do \ - $(SCRIPTS_DIR)/create-dfu-image.sh $(TARGET_DIR)/$$board; \ - done - -ifeq ($(PRIMARY_GOAL),run) - -.PHONY: run - -# Application arguments may also look like Make goals. The run recipe recovers -# their exact boundaries from the original invocation. -.DEFAULT: - @: - -else - -.PHONY: help run +.NOTPARALLEL: +.PHONY: help build help: - @printf '%s\n' 'Usage: make firmware/boards -- ' '' \ - 'With no arguments, every board is built and packaged.' + @printf '%s\n' 'Usage: make -C firmware/boards build' '' \ + ' build Build and package every board in release mode' \ + 'CARGO_TARGET_DIR defaults to firmware/target; relative overrides are relative to firmware/boards/.' \ + 'For one board: make -C firmware/boards/ build|flash' -endif +build: + cargo build --release --locked --offline $(BOARD_PACKAGE_ARGS) $(BOARD_BIN_ARGS) \ + --target $(EMBEDDED_TARGET) --target-dir "$(CARGO_TARGET_DIR)" + @set -e; for board in $(BOARD_PACKAGES); do \ + ../scripts/create-dfu-image.sh "$(TARGET_DIR)/$$board"; \ + done diff --git a/firmware/boards/board.mk b/firmware/boards/board.mk index 3625f54..899f896 100644 --- a/firmware/boards/board.mk +++ b/firmware/boards/board.mk @@ -1,69 +1,30 @@ -override SHELL := /bin/sh -override MAKEFLAGS += --no-print-directory +SHELL := /bin/sh +MAKEFLAGS += --no-print-directory +export CARGO_BUILD_JOBS ?= 2 .DEFAULT_GOAL := help .DELETE_ON_ERROR: -override CARGO := cargo -override CARGO_FLAGS := --locked --offline -override DFU_UTIL := dfu-util - override EMBEDDED_TARGET := thumbv7em-none-eabihf override PACKAGE := kaptan-$(BOARD) -override TARGET_DIR := ../../target/$(EMBEDDED_TARGET)/release -override CREATE_IMAGE := ../../scripts/create-dfu-image.sh +CARGO_TARGET_DIR ?= ../../target +override ELF := $(CARGO_TARGET_DIR)/$(EMBEDDED_TARGET)/release/$(PACKAGE) -override DFU_DEVICE := 0483:df11 -override DFU_ALT := 0 -override DFU_ADDRESS := 0x08000000:leave - -override PRIMARY_GOAL := $(firstword $(MAKECMDGOALS)) - -run: - @exec python3 ../../../scripts/make-argv.py exec run $(CARGO) build --release \ - $(CARGO_FLAGS) -p $(PACKAGE) --target $(EMBEDDED_TARGET) - $(CREATE_IMAGE) $(TARGET_DIR)/$(PACKAGE) - -_build: - $(CARGO) build --release $(CARGO_FLAGS) -p $(PACKAGE) \ - --target $(EMBEDDED_TARGET) - $(CREATE_IMAGE) $(TARGET_DIR)/$(PACKAGE) - -flash: _build - @printf '%s\n' 'Flashing $(TARGET_DIR)/$(PACKAGE).bin to $(DFU_DEVICE)' - @exec python3 ../../../scripts/make-argv.py exec flash \ - $(DFU_UTIL) --device $(DFU_DEVICE) --alt $(DFU_ALT) \ - --dfuse-address $(DFU_ADDRESS) \ - --download $(TARGET_DIR)/$(PACKAGE).bin - -ifeq ($(PRIMARY_GOAL),run) - -.PHONY: run - -# Application arguments may also look like Make goals. The run recipe recovers -# their exact boundaries from the original invocation. -.DEFAULT: - @: - -else - -ifeq ($(PRIMARY_GOAL),flash) - -.PHONY: flash _build - -.DEFAULT: - @: - -else - -.PHONY: help run flash _build +.NOTPARALLEL: +.PHONY: help build flash help: - @printf '%s\n' 'Usage: make firmware/boards/$(BOARD) -- ' '' \ - ' make firmware/boards/$(BOARD) flash -- ' '' \ - 'With no arguments, this board is built and packaged.' \ - 'The flash target builds, packages, and writes this board over DFU.' + @printf '%s\n' 'Usage: make -C firmware/boards/$(BOARD) build|flash' '' \ + ' build Build and package $(PACKAGE) in release mode' \ + ' flash Build, package, and write $(PACKAGE) over DFU' '' \ + 'CARGO_TARGET_DIR defaults to firmware/target; relative overrides are relative to this board directory.' \ + 'For custom Cargo or DFU options, invoke cargo or dfu-util directly.' -endif +build: + cargo build --release --locked --offline -p $(PACKAGE) --bin $(PACKAGE) \ + --target $(EMBEDDED_TARGET) --target-dir "$(CARGO_TARGET_DIR)" + ../../scripts/create-dfu-image.sh "$(ELF)" -endif +flash: build + dfu-util --device 0483:df11 --alt 0 --dfuse-address 0x08000000:leave \ + --download "$(ELF).bin" diff --git a/firmware/scripts/analyze-fw.py b/firmware/scripts/analyze-fw.py index d78994c..76f807f 100755 --- a/firmware/scripts/analyze-fw.py +++ b/firmware/scripts/analyze-fw.py @@ -5,6 +5,7 @@ Usage: scripts/analyze-fw.py """ +import argparse import json import re from collections import namedtuple @@ -33,7 +34,6 @@ def number(text): def run(command): - """Run a tool and return stdout.""" return subprocess.run(command, check=True, text=True, capture_output=True).stdout @@ -128,9 +128,8 @@ def merged_span_size(spans): def region_usage(name, layout, section_list, load_segments): """Return runtime or load-image bytes occupying one linker region. - Allocated-section VMAs account for runtime RAM, while PT_LOAD physical file - spans account for initializers stored in flash (notably a future `.data`). - Taking their union avoids counting ordinary flash sections twice. + Section VMAs count runtime RAM. PT_LOAD physical spans count flash storage, + including RAM initializers. Their union avoids counting flash sections twice. """ spans = [ (section.address, section.address + section.size) @@ -260,11 +259,11 @@ def sram_control_flow_errors(section, disassembly): def main(): - if len(sys.argv) != 3: - raise ValueError(f"usage: {sys.argv[0]} ") - - elf = Path(sys.argv[1]) - memory_x = Path(sys.argv[2]) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("elf", type=Path) + parser.add_argument("memory_x", type=Path) + args = parser.parse_args() + elf, memory_x = args.elf, args.memory_x if not elf.is_file(): raise ValueError(f"ELF does not exist: {elf}") if not memory_x.is_file(): diff --git a/firmware/scripts/report-test-coverage.sh b/firmware/scripts/report-test-coverage.sh index 049c7a4..bb17ca6 100755 --- a/firmware/scripts/report-test-coverage.sh +++ b/firmware/scripts/report-test-coverage.sh @@ -1,94 +1,90 @@ #!/usr/bin/env sh -# Per-workspace-crate line and branch coverage report. -# -# This is deliberately a report over every host-testable workspace package, -# not a misleading aggregate. STM32F7 platform/board images are target-only: -# their `panic-halt` handler cannot link into the host test harness, so they -# are reported as N/A and must be covered by target checks plus bench -# evidence instead. -# -# Prerequisites (kept out of the firmware dependency graph): -# cargo install cargo-llvm-cov --locked -# rustup toolchain install nightly --component llvm-tools-preview -# python3 (standard library only, for strict source-level accounting) +# Host workspace coverage. The four strict-core packages require 100% source +# lines and branch outcomes; all other package totals are informational. +# Run from firmware/ in the locked Nix shell (cargo-llvm-cov 0.8.7). +# Install the separate coverage compiler with: +# rustup toolchain install nightly-2025-08-01 --profile minimal --component llvm-tools-preview set -eu -if ! cargo llvm-cov --version >/dev/null 2>&1; then - echo "cargo-llvm-cov is required; install it with: cargo install cargo-llvm-cov --locked" >&2 +export RUSTUP_TOOLCHAIN=nightly-2025-08-01 +export CARGO_BUILD_JOBS=2 +if [ "$(cargo llvm-cov --version)" != "cargo-llvm-cov 0.8.7" ]; then + echo "Use cargo-llvm-cov 0.8.7 from nix develop (flake.lock)." >&2 exit 127 fi - -if ! rustup toolchain list | grep -q '^nightly'; then - echo "nightly with llvm-tools-preview is required for branch coverage" >&2 - exit 127 +if [ -n "${RUSTC_BOOTSTRAP:-}" ] || [ -n "${RUSTC:-}" ] || [ -n "${RUSTDOC:-}" ]; then + echo "Coverage requires the pinned compiler without RUSTC_BOOTSTRAP/RUSTC/RUSTDOC overrides." >&2 + exit 2 fi - -if ! python3 --version >/dev/null 2>&1; then - echo "python3 is required for strict source-level coverage accounting" >&2 - exit 127 -fi - +sysroot=$(rustc --print sysroot) +host=$(rustc -vV | awk '/^host:/ { print $2 }') +export LLVM_COV="$sysroot/lib/rustlib/$host/bin/llvm-cov" +export LLVM_PROFDATA="$sysroot/lib/rustlib/$host/bin/llvm-profdata" +rustc -vV +cargo llvm-cov --version +"$LLVM_COV" --version +"$LLVM_PROFDATA" --version +echo "Coverage profile: dev; compiler and LLVM tools: $RUSTUP_TOOLCHAIN" python3 scripts/test-summarize-test-coverage.py -# Keep instrumentation products outside a possibly shared target directory. -: "${CARGO_TARGET_DIR:=/tmp/kaptan-test-coverage}" -export CARGO_TARGET_DIR -mkdir -p "$CARGO_TARGET_DIR" - -# `cargo llvm-cov` merges every instrumented object below `CARGO_TARGET_DIR`. -# A shared target directory therefore makes a later strict-core report include -# an unexecuted copy of a shared dependency built while testing an earlier -# package. Keep reports together but isolate each strict-core invocation. The -# non-core packages retain the shared directory: several intentionally -# target-only crates have no host-instrumented object to export by themselves. +# Keep coverage out of ordinary build artifacts. Strict-core invocations also +# need separate object directories to avoid unexecuted dependency duplicates. +: "${CARGO_TARGET_DIR:=$PWD/target/test-coverage}" coverage_root=$CARGO_TARGET_DIR +mkdir -p "$coverage_root" -core_incomplete=0 +# Discover current workspace members, including host platform contracts and +# proc-macro runtime harnesses. Only bare-metal boards are excluded. +# Put the strict core first so unrelated test failures cannot hide its gaps. +cargo metadata --no-deps --format-version 1 --locked --offline >"$coverage_root/metadata.json" +python3 - "$coverage_root/metadata.json" >"$coverage_root/packages.txt" <<'PY' +import json +from pathlib import Path +import sys + +metadata = json.loads(Path(sys.argv[1]).read_text()) +excluded = {"kaptan-geprc-f722-v2", "kaptan-kakute-f7-mini-v3"} +core = {"kaptan-math", "kaptan-navigation", "kaptan-control", "kaptan-safety"} +packages = [p for p in metadata["packages"] if p["id"] in metadata["workspace_members"] and p["name"] not in excluded] +if not core <= {p["name"] for p in packages}: + raise ValueError("missing strict-core package") +for package in sorted(packages, key=lambda p: (p["name"] not in core, p["name"])): + source = Path(package["manifest_path"]).parent.relative_to(metadata["workspace_root"]) + print(package["name"], f"/{source}/") +PY report_package() { package=$1 source_path=$2 shift 2 + lcov_report="$coverage_root/$package.lcov" case "$package" in kaptan-math | kaptan-navigation | kaptan-control | kaptan-safety) package_target_dir="$coverage_root/$package" - lcov_report="$coverage_root/$package.lcov" json_report="$coverage_root/$package.json" report_format=strict-core ;; *) - package_target_dir=$coverage_root - lcov_report="$coverage_root/$package.lcov" + package_target_dir="$coverage_root/other" report_format=lcov ;; esac + printf '\nCoverage package: %s; extra arguments: %s\n' "$package" "$*" + CARGO_TARGET_DIR="$package_target_dir" cargo llvm-cov --profile dev \ + --locked --offline --branch --no-report -p "$package" "$@" || return 1 + CARGO_TARGET_DIR="$package_target_dir" cargo llvm-cov report --profile dev \ + --locked --offline --lcov --output-path "$lcov_report" || return 1 case "$report_format" in strict-core) - # Keep the strict core isolated, then export both representations - # from the same test run. LCOV `DA` defines source lines; JSON - # coordinates define branch identities across generic instances. - RUSTC_BOOTSTRAP=1 CARGO_TARGET_DIR="$package_target_dir" cargo llvm-cov \ - --branch \ - --no-report \ - -p "$package" \ - "$@" - RUSTC_BOOTSTRAP=1 CARGO_TARGET_DIR="$package_target_dir" cargo llvm-cov report \ - --lcov \ - --output-path "$lcov_report" - RUSTC_BOOTSTRAP=1 CARGO_TARGET_DIR="$package_target_dir" cargo llvm-cov report \ - --json \ - --output-path "$json_report" + # LCOV DA defines source lines. JSON spans identify branch outcomes + # across generic instances. Both exports use the same compiler/profile. + CARGO_TARGET_DIR="$package_target_dir" cargo llvm-cov report --profile dev \ + --locked --offline --json --output-path "$json_report" || return 1 totals=$(python3 scripts/summarize-test-coverage.py \ - "$lcov_report" "$json_report" "$source_path") + "$lcov_report" "$json_report" "$source_path") || return 1 ;; lcov) - RUSTC_BOOTSTRAP=1 CARGO_TARGET_DIR="$package_target_dir" cargo llvm-cov \ - --branch \ - --lcov \ - --output-path "$lcov_report" \ - -p "$package" \ - "$@" totals=$(awk -v source_path="$source_path" ' /^SF:/ { selected = index($0, source_path) != 0 } selected && /^LF:/ { lines_found += substr($0, 4) } @@ -98,42 +94,45 @@ report_package() { END { printf "%d %d %d %d", lines_hit, lines_found, branches_hit, branches_found } - ' "$lcov_report") + ' "$lcov_report") || return 1 ;; esac + # Both summarizers emit exactly four space-separated integer counters. + # shellcheck disable=SC2086 set -- $totals - printf '%-26s lines %s/%s, branches %s/%s\n' "$package" "$1" "$2" "$3" "$4" - - case "$package" in - kaptan-math | kaptan-navigation | kaptan-control | kaptan-safety) - if [ "$1" -ne "$2" ] || [ "$3" -ne "$4" ]; then - core_incomplete=1 + printf '%-30s lines %s/%s, branches %s/%s\n' "$package" "$1" "$2" "$3" "$4" + if [ "$report_format" = strict-core ]; then + if [ "$2" -eq 0 ] || [ "$4" -eq 0 ] || [ "$1" -ne "$2" ] || [ "$3" -ne "$4" ]; then + echo "$package: FAIL strict 100% line/branch gate" >&2 + return 1 fi - ;; - esac + elif [ "$2" -eq 0 ]; then + echo "$package: no instrumented host source; coverage unavailable" + fi } -echo "Host test coverage (reports: $CARGO_TARGET_DIR; strict core unions LCOV DA lines and JSON branches)" -report_package kaptan-actuator /libs/kaptan-actuator/ -report_package kaptan-control /libs/kaptan-control/ -report_package kaptan-data-channel /libs/kaptan-data-channel/ -report_package kaptan-dma /libs/kaptan-dma/ -report_package kaptan-drivers /libs/kaptan-drivers/ -report_package kaptan-i2c /libs/kaptan-i2c/ -report_package kaptan-math /libs/kaptan-math/ -report_package kaptan-mavlink /libs/kaptan-mavlink/ --features sensor-telemetry -report_package kaptan-navigation /libs/kaptan-navigation/ --features sitl -report_package kaptan-safety /libs/kaptan-safety/ -report_package kaptan-sensor /libs/kaptan-sensor/ -report_package kaptan-spi /libs/kaptan-spi/ -report_package kaptan-time /libs/kaptan-time/ -report_package kaptan-tx /libs/kaptan-tx/ +echo "Host test coverage (reports: $coverage_root; strict core unions LCOV DA lines and JSON branches)" +echo "UI/compile-fail suites run under Rust 1.90.0 in make test, not under coverage nightly." +echo "Proc-macro runtime-harness totals do not establish compiler-phase macro coverage." +incomplete=0 +while read -r package source_path; do + set -- + case "$package" in + kaptan-navigation) set -- --features sensor-snapshots ;; + kaptan-mavlink) set -- --features sensor-telemetry ;; + # Diagnostic snapshots describe the production compiler's output. Keep + # those suites in stable make test; instrument the runtime harnesses here. + kaptan-config-derive) set -- --lib --test section ;; + kaptan-err-reportable-macros) set -- --lib ;; + esac + if ! report_package "$package" "$source_path" "$@"; then + echo "$package: coverage/test failure (see diagnostics above)" >&2 + incomplete=1 + fi +done <"$coverage_root/packages.txt" -echo "platform-stm32f7 target-only/N/A (run cargo check -p platform-stm32f7 --lib)" -echo "kaptan-geprc-f722-v2 target-only/N/A (run its thumbv7em-none-eabihf check)" -echo "kaptan-kakute-f7-mini-v3 target-only/N/A (run its thumbv7em-none-eabihf check)" - -if [ "$core_incomplete" -ne 0 ]; then - echo "Strict core coverage is incomplete; reports above identify each crate." >&2 +echo "kaptan-geprc-f722-v2, kaptan-kakute-f7-mini-v3: target-only; make boards validates release images" +if [ "$incomplete" -ne 0 ]; then + echo "Coverage gate failed. Strict core gaps and test/report failures are listed above." >&2 exit 1 fi diff --git a/firmware/scripts/summarize-test-coverage.py b/firmware/scripts/summarize-test-coverage.py index 3d8a722..c6671a0 100644 --- a/firmware/scripts/summarize-test-coverage.py +++ b/firmware/scripts/summarize-test-coverage.py @@ -1,24 +1,16 @@ #!/usr/bin/env python3 """Summarize strict-core LCOV lines and LLVM JSON branches by source location. -`llvm-cov` emits one coverage record for every generic monomorphization. Its -per-file totals add those records, which can report an uncovered duplicate even -when the corresponding source line or branch has been exercised by another -monomorphization. This helper instead applies the gate to source locations: +Merge generic monomorphizations by source location. A location is covered if +any instance executed it: -* a source line is identified by its LCOV `DA` file and line number; -* a branch outcome is identified by its full source span; and -* a location is covered when any matching monomorphization executed it. +* lines use LCOV `DA` file and line numbers +* branch outcomes use their full source spans -JSON segments are deliberately not used as a line denominator: they mark LLVM -instrumentation-region boundaries, not every source line represented by an -LCOV `DA` record. Replacing `DA` with segments would silently lower the strict -line denominator. +JSON segments mark instrumentation boundaries and omit some `DA` lines. +Using them would undercount the line denominator. -Macro-expansion records are deliberately rejected. Their source span denotes -the invocation, not necessarily the expanded predicate, so folding them into -the source-level key would make the gate unsound. Extend this helper with an -explicit expansion identity before adding macro-expanded strict-core coverage. +Reject macro expansions: invocation spans cannot distinguish expanded predicates. """ from __future__ import annotations diff --git a/firmware/scripts/test-analyze-fw.py b/firmware/scripts/test-analyze-fw.py index ce92bcd..c33ef95 100644 --- a/firmware/scripts/test-analyze-fw.py +++ b/firmware/scripts/test-analyze-fw.py @@ -3,11 +3,18 @@ import importlib.util import json +from pathlib import Path +import contextlib +import io +import tempfile import unittest +from unittest.mock import patch def load_analyzer_module(): - spec = importlib.util.spec_from_file_location("analyze_fw", "scripts/analyze-fw.py") + spec = importlib.util.spec_from_file_location( + "analyze_fw", Path(__file__).with_name("analyze-fw.py") + ) assert spec is not None and spec.loader is not None module = importlib.util.module_from_spec(spec) spec.loader.exec_module(module) @@ -179,6 +186,72 @@ class FirmwareMemoryValidationTests(unittest.TestCase): ANALYZER.sram_control_flow_errors(section, literal)[0], ) + def test_cli_requires_and_checks_executable_sram_code(self): + with tempfile.TemporaryDirectory() as temporary: + root = Path(temporary) + elf, memory = root / "firmware", root / "memory.x" + elf.touch() + memory.write_text( + "MEMORY {\nFLASH : ORIGIN = 0x08000000, LENGTH = 256\nRAM : ORIGIN = 0x20000000, LENGTH = 128\n}\n" + ) + segments = [ANALYZER.LoadSegment(0x08000000, 0x08000000, 0x20, 0x20)] + for executable in (False, True): + with self.subTest(executable=executable): + sections = [ + ANALYZER.Section(".data", 0x10, 0x20000000, True, executable) + ] + with ( + patch("sys.argv", ["analyze-fw.py", str(elf), str(memory)]), + patch.object(ANALYZER, "llvm_tool", return_value="llvm-tool"), + patch.object( + ANALYZER, + "elf_layout", + return_value=(sections, segments), + ), + patch.object( + ANALYZER, "run", return_value="20000000: bx lr" + ) as run, + contextlib.redirect_stdout(io.StringIO()), + ): + if executable: + ANALYZER.main() + self.assertEqual(run.call_count, 2) + else: + with self.assertRaisesRegex( + ValueError, + "Flash-operation placement validation failed", + ): + ANALYZER.main() + + def test_cli_rejects_common_memory_bounds(self): + with tempfile.TemporaryDirectory() as temporary: + elf, memory = Path(temporary) / "firmware", Path(temporary) / "memory.x" + elf.touch() + memory.write_text( + "FLASH : ORIGIN = 0x08000000, LENGTH = 256\nRAM : ORIGIN = 0x20000000, LENGTH = 128\n" + ) + with ( + patch( + "sys.argv", + ["analyze-fw.py", str(elf), str(memory)], + ), + patch.object(ANALYZER, "llvm_tool", return_value="llvm-readobj"), + patch.object(ANALYZER, "run", return_value=""), + patch.object( + ANALYZER, + "elf_layout", + return_value=( + [ANALYZER.Section(".data", 0x81, 0x20000000, True, False)], + [ANALYZER.LoadSegment(0x20000000, 0x080000FF, 2, 0x81)], + ), + ), + contextlib.redirect_stdout(io.StringIO()), + ): + with self.assertRaisesRegex( + ValueError, "firmware memory validation failed" + ): + ANALYZER.main() + if __name__ == "__main__": unittest.main() diff --git a/firmware/scripts/test-build-workflow.py b/firmware/scripts/test-build-workflow.py new file mode 100644 index 0000000..b60eea3 --- /dev/null +++ b/firmware/scripts/test-build-workflow.py @@ -0,0 +1,321 @@ +#!/usr/bin/env python3 +"""Exercise board Makefiles with fake Cargo, image creation, and DFU tools.""" + +import json +import os +from pathlib import Path +import shutil +import subprocess +import tempfile +import unittest + + +FIRMWARE = Path(__file__).resolve().parents[1] +BOARDS = ("geprc-f722-v2", "kakute-f7-mini-v3") +TARGET = "thumbv7em-none-eabihf" +FAKE_TOOL = """#!/usr/bin/env python3 +import json +import os +from pathlib import Path +import sys + +tool = Path(sys.argv[0]).name +args = sys.argv[1:] +with open(os.environ["WORKFLOW_LOG"], "a") as log: + log.write(json.dumps({"tool": tool, "args": args}) + "\\n") +if os.environ.get("FAIL_TOOL") == tool: + sys.exit(1) +if tool == "cargo": + if args[0] != "build" or not all( + flag in args for flag in ("--release", "--locked", "--offline") + ): + raise ValueError("expected locked offline release build") + directory = Path(args[args.index("--target-dir") + 1]) + directory /= args[args.index("--target") + 1] + directory /= "release" + directory.mkdir(parents=True, exist_ok=True) + for index, arg in enumerate(args): + if arg == "--bin": + binary = args[index + 1] + (directory / binary).write_text("fresh " + binary) +elif tool == "create-dfu-image.sh": + if len(args) != 1: + raise ValueError("expected one ELF") + elf = Path(args[0]) + if elf.read_text() != "fresh " + elf.name: + raise ValueError("stale ELF") + Path(str(elf) + ".bin").write_text(elf.read_text()) +elif tool == "dfu-util": + image = Path(args[args.index("--download") + 1]) + if image.read_text() != "fresh " + image.stem: + raise ValueError("stale image") +else: + raise AssertionError(tool) +""" + + +class BoardWorkflowTests(unittest.TestCase): + def setUp(self): + temporary = tempfile.TemporaryDirectory(prefix="kaptan-workflow-") + self.addCleanup(temporary.cleanup) + self.root = Path(temporary.name) + self.boards = self.root / "firmware" / "boards" + self.boards.mkdir(parents=True) + for relative in ("Makefile", "board.mk", *(f"{b}/Makefile" for b in BOARDS)): + destination = self.boards / relative + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(FIRMWARE / "boards" / relative, destination) + for relative in ( + "bin/cargo", + "bin/dfu-util", + "firmware/scripts/create-dfu-image.sh", + ): + tool = self.root / relative + tool.parent.mkdir(parents=True, exist_ok=True) + tool.write_text(FAKE_TOOL) + tool.chmod(0o755) + self.log = self.root / "events.jsonl" + self.environment = dict(os.environ) + for name in ("CARGO_TARGET_DIR", "MAKEFLAGS", "MFLAGS", "MAKEOVERRIDES"): + self.environment.pop(name, None) + self.environment.update( + PATH=f"{self.root / 'bin'}{os.pathsep}{os.environ['PATH']}", + WORKFLOW_LOG=str(self.log), + ) + # A wrong packaging path must fail even when old build outputs exist. + self.seed_stale(self.root / "firmware" / "target") + + def seed_stale(self, target_dir): + release = target_dir / TARGET / "release" + release.mkdir(parents=True, exist_ok=True) + for board in BOARDS: + for suffix in ("", ".bin"): + (release / f"kaptan-{board}{suffix}").write_text("stale") + + def run_make(self, directory, goal, target_dir=None, fail="", variables=()): + self.log.unlink(missing_ok=True) + environment = dict(self.environment, FAIL_TOOL=fail) + if target_dir is not None: + environment["CARGO_TARGET_DIR"] = target_dir + result = subprocess.run( + [ + "make", + "--no-print-directory", + "-j2", + "-C", + str(directory), + goal, + *variables, + ], + env=environment, + capture_output=True, + text=True, + timeout=30, + ) + events = ( + [json.loads(line) for line in self.log.read_text().splitlines()] + if self.log.exists() + else [] + ) + return result, events + + def test_selected_board_artifact_directory_and_identity(self): + for board in BOARDS: + directory = self.boards / board + for target_dir in ( + None, + "local artifacts", + str(self.root / "external artifacts"), + ): + with self.subTest(board=board, target_dir=target_dir): + result, events = self.run_make( + directory, + "flash", + target_dir, + variables=( + "BOARD=wrong", + "PACKAGE=wrong", + "EMBEDDED_TARGET=wrong", + ), + ) + self.assertEqual( + result.returncode, 0, result.stdout + result.stderr + ) + self.assertEqual( + [event["tool"] for event in events], + ["cargo", "create-dfu-image.sh", "dfu-util"], + ) + args = events[0]["args"] + self.assertEqual(args[args.index("-p") + 1], f"kaptan-{board}") + self.assertEqual(args[args.index("--bin") + 1], f"kaptan-{board}") + self.assertEqual(args[args.index("--target") + 1], TARGET) + expected = directory / (target_dir or "../../target") + self.assertEqual( + (directory / args[args.index("--target-dir") + 1]).resolve(), + expected.resolve(), + ) + elf = expected / TARGET / "release" / f"kaptan-{board}" + self.assertEqual( + (directory / events[1]["args"][0]).resolve(), elf.resolve() + ) + self.assertEqual( + (directory / events[2]["args"][-1]).resolve(), + Path(str(elf) + ".bin").resolve(), + ) + + def test_all_boards_use_one_artifact_directory(self): + for target_dir in ( + None, + "local artifacts", + str(self.root / "external artifacts"), + ): + with self.subTest(target_dir=target_dir): + result, events = self.run_make(self.boards, "build", target_dir) + self.assertEqual(result.returncode, 0, result.stdout + result.stderr) + self.assertEqual( + [event["tool"] for event in events], + ["cargo", "create-dfu-image.sh", "create-dfu-image.sh"], + ) + expected = self.boards / (target_dir or "../target") + args = events[0]["args"] + self.assertEqual( + (self.boards / args[args.index("--target-dir") + 1]).resolve(), + expected.resolve(), + ) + self.assertEqual( + [ + (self.boards / event["args"][0]).resolve() + for event in events[1:] + ], + [ + (expected / TARGET / "release" / f"kaptan-{b}").resolve() + for b in BOARDS + ], + ) + + def test_failures_stop_packaging_and_flashing_even_with_stale_outputs(self): + target_dir = self.root / "external artifacts" + for directory, goal in ( + (self.boards, "build"), + *((self.boards / board, "flash") for board in BOARDS), + ): + for failed_tool in ("cargo", "create-dfu-image.sh"): + with self.subTest(directory=directory, failed_tool=failed_tool): + self.seed_stale(target_dir) + result, events = self.run_make( + directory, goal, str(target_dir), failed_tool + ) + self.assertNotEqual(result.returncode, 0) + self.assertEqual( + [event["tool"] for event in events], + ["cargo"] if failed_tool == "cargo" else ["cargo", failed_tool], + ) + for board in BOARDS: + image = target_dir / TARGET / "release" / f"kaptan-{board}.bin" + self.assertEqual(image.read_text(), "stale") + + +class PackagingValidationTests(unittest.TestCase): + def test_real_packager_validates_sram_and_bounds_before_objcopy(self): + fake = """#!/usr/bin/env python3 +import os +from pathlib import Path +import sys +name = Path(sys.argv[0]).name +if name == "rustc": + print("host: test-host" if sys.argv[1] == "-vV" else os.environ["FAKE_SYSROOT"]) +elif name == "llvm-readobj": + print(os.environ["ELF_METADATA"]) +elif name == "llvm-objdump": + print("20000000: bx lr") +elif name == "llvm-objcopy": + Path(os.environ["OBJCOPY_LOG"]).touch() + Path(sys.argv[-1]).write_bytes(b"validated image") +else: + raise AssertionError(name) +""" + with tempfile.TemporaryDirectory(prefix="kaptan-package-") as temporary: + root = Path(temporary) + tools = root / "lib/rustlib/test-host/bin" + tools.mkdir(parents=True) + for path in ( + root / "rustc", + *(tools / f"llvm-{tool}" for tool in ("readobj", "objdump", "objcopy")), + ): + path.write_text(fake) + path.chmod(0o755) + elf, memory, log = ( + root / "arbitrary-name.elf", + root / "memory.x", + root / "objcopy-called", + ) + elf.touch() + image = elf.with_suffix(".bin") + memory.write_text( + "FLASH : ORIGIN = 0x08000000, LENGTH = 256\nRAM : ORIGIN = 0x20000000, LENGTH = 128\n" + ) + for executable, size, accepted in ( + (True, 16, True), + (False, 16, False), + (True, 129, False), + ): + with self.subTest(executable=executable, size=size): + image.write_bytes(b"previous image") + log.unlink(missing_ok=True) + flags = [{"Name": "SHF_ALLOC"}] + if executable: + flags.append({"Name": "SHF_EXECINSTR"}) + metadata = [ + { + "Sections": [ + { + "Section": { + "Name": {"Name": ".data"}, + "Size": size, + "Address": 0x20000000, + "Flags": {"Flags": flags}, + } + } + ], + "ProgramHeaders": [ + { + "ProgramHeader": { + "Type": {"Name": "PT_LOAD"}, + "VirtualAddress": 0x20000000, + "PhysicalAddress": 0x08000000, + "FileSize": size, + "MemSize": size, + } + } + ], + } + ] + result = subprocess.run( + [ + str(FIRMWARE / "scripts/create-dfu-image.sh"), + str(elf), + str(memory), + ], + env=dict( + os.environ, + PATH=f"{root}{os.pathsep}{os.environ['PATH']}", + FAKE_SYSROOT=str(root), + ELF_METADATA=json.dumps(metadata), + OBJCOPY_LOG=str(log), + ), + capture_output=True, + text=True, + timeout=10, + ) + self.assertEqual( + result.returncode == 0, accepted, result.stdout + result.stderr + ) + self.assertEqual(log.exists(), accepted) + self.assertEqual( + image.read_bytes(), + b"validated image" if accepted else b"previous image", + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/firmware/scripts/test-verify.py b/firmware/scripts/test-verify.py new file mode 100644 index 0000000..52dfd79 --- /dev/null +++ b/firmware/scripts/test-verify.py @@ -0,0 +1,443 @@ +import copy +import importlib.util +import json +import os +from pathlib import Path +import signal +import subprocess +import sys +import tempfile +import time +import unittest +from unittest import mock + + +SCRIPT = Path(__file__).with_name("verify.py") +SPEC = importlib.util.spec_from_file_location("verify", SCRIPT) +verify = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(verify) + + +class VerificationTests(unittest.TestCase): + def setUp(self): + self.temporary = tempfile.TemporaryDirectory() + self.addCleanup(self.temporary.cleanup) + self.directory = Path(self.temporary.name) + + def test_contract_cannot_remove_whole_proof_or_interpreter_gates(self): + contract, _ = verify.load_contract() + loader = verify.tomllib.load + for section, field, value in ( + (None, "properties", []), + ("miri", "packages", []), + ("miri", "packages", ["kaptan-log", "kaptan-log"]), + ("miri", "seeds", []), + ("miri", "seeds", [0, 0]), + ("miri", "seeds", [-1]), + ("miri", "seeds", [True]), + ): + damaged = copy.deepcopy(contract) + (damaged[section] if section else damaged)[field] = value + + def load(source): + if Path(source.name).name == "verification.toml": + return damaged + return loader(source) + + with ( + self.subTest(field=field, value=value), + mock.patch.object(verify.tomllib, "load", side_effect=load), + self.assertRaises(ValueError), + ): + verify.load_contract() + + def proof(self): + prop = { + "id": "example", + "harnesses": ["proof"], + "covers": [1], + "package": "example", + "source": "proof.rs", + } + report = { + "metadata": { + "version": "1.0", + "kani_version": "0.68.0", + "target": "x86_64-unknown-linux-gnu", + }, + "tools": {"rustc": "pinned rustc"}, + "harness_metadata": [ + { + "pretty_name": "proof", + "crate_name": "example", + "source": {"file": "proof.rs"}, + } + ], + "verification_results": { + "summary": { + "total_harnesses": 1, + "executed": 1, + "status": "completed", + "successful": 1, + "failed": 0, + }, + "results": [ + { + "harness_id": "proof", + "status": "Success", + "checks": [ + { + "category": "assertion", + "status": "Success", + "description": "assertion failed: invariant", + "function": "proof", + }, + {"category": "cover", "status": "Satisfied"}, + ], + } + ], + }, + } + return prop, report + + def validate(self, prop, report, exit_code=0): + path = self.directory / "proof.json" + path.write_text(json.dumps(report)) + return verify.validate_kani( + path, prop, "0.68.0", "x86_64-unknown-linux-gnu", exit_code, "pinned rustc" + ) + + def test_failed_missing_vacuous_and_unknown_proofs_cannot_pass(self): + prop, report = self.proof() + self.assertTrue(self.validate(prop, report)["raw_verifier_passed"]) + for status in ( + "Failure", + "Undetermined", + "SolverError", + "Unreachable", + "new-status", + ): + damaged = copy.deepcopy(report) + damaged["verification_results"]["results"][0]["checks"][0]["status"] = ( + status + ) + with self.subTest(status=status), self.assertRaises(ValueError): + self.validate(prop, damaged) + for status in ("Unreachable", "Unsatisfiable", "Undetermined"): + damaged = copy.deepcopy(report) + damaged["verification_results"]["results"][0]["checks"][1]["status"] = ( + status + ) + with self.subTest(cover=status), self.assertRaises(ValueError): + self.validate(prop, damaged) + damaged = copy.deepcopy(report) + damaged["verification_results"]["results"][0]["checks"].pop() + with self.assertRaises(ValueError): + self.validate(prop, damaged) + damaged["verification_results"]["results"] = [] + with self.assertRaises(ValueError): + self.validate(prop, damaged) + with self.assertRaises(ValueError): + self.validate(prop, report, exit_code=1) + damaged = copy.deepcopy(report) + damaged["harness_metadata"][0]["source"]["file"] = "another.rs" + with self.assertRaises(ValueError): + self.validate(prop, damaged) + damaged = copy.deepcopy(report) + damaged["tools"]["rustc"] = "different compiler" + with self.assertRaises(ValueError): + self.validate(prop, damaged) + + def test_pid_exception_preserves_raw_failure_and_rejects_other_failures(self): + prop, report = self.proof() + prop.update( + id="control.pid-state", + harnesses=["kani_proofs::pid_update_preserves_bounds_or_state"], + intermediate_nan_line=196, + ) + result = report["verification_results"]["results"][0] + result.update(harness_id=prop["harnesses"][0], status="Failure") + report["harness_metadata"][0]["pretty_name"] = prop["harnesses"][0] + report["verification_results"]["summary"].update(successful=0, failed=1) + diagnostic = { + "category": "NaN", + "status": "Failure", + "description": "NaN on addition", + "function": "Pid::update_with_valid_time", + "location": { + "file": "libs/kaptan-control/src/lib.rs", + "line": "196", + "column": "13", + }, + } + result["checks"].append(diagnostic) + accepted = self.validate(prop, report, exit_code=1) + self.assertFalse(accepted["raw_verifier_passed"]) + self.assertTrue(accepted["contract_checks_passed"]) + for field, value in ( + ("category", "overflow"), + ("description", "NaN on division"), + ("function", "different"), + ): + damaged = copy.deepcopy(report) + damaged["verification_results"]["results"][0]["checks"][-1][field] = value + with self.subTest(field=field), self.assertRaises(ValueError): + self.validate(prop, damaged, exit_code=1) + result["checks"].append(copy.deepcopy(diagnostic)) + with self.assertRaises(ValueError): + self.validate(prop, report, exit_code=1) + + def test_miri_cannot_pass_with_empty_ignored_or_filtered_suites(self): + path = self.directory / "miri.log" + template = "test result: ok. {} passed; 0 failed; {} ignored; 0 measured; {} filtered out" + for passed, ignored, filtered in ((0, 0, 0), (1, 1, 0), (1, 0, 1)): + path.write_text(template.format(passed, ignored, filtered)) + with self.assertRaises(ValueError): + verify.validate_miri(path, 1) + path.write_text(template.format(4, 0, 0)) + self.assertEqual(verify.validate_miri(path, 1), 4) + with self.assertRaises(ValueError): + verify.validate_miri(path, 2) + + def test_snapshot_includes_untracked_bytes_modes_and_deletions(self): + path = self.directory / "untracked.rs" + path.write_text("original") + with mock.patch.object( + verify.subprocess, + "check_output", + return_value=b"untracked.rs\0deleted.rs\0", + ): + before = verify.snapshot(self.directory) + path.write_text("edited") + self.assertNotEqual(before, verify.snapshot(self.directory)) + path.write_text("original") + path.chmod(0o755) + self.assertNotEqual(before, verify.snapshot(self.directory)) + path.unlink() + self.assertTrue( + all( + entry["kind"] == "absent" + for entry in verify.snapshot(self.directory)["entries"] + ) + ) + + def test_compiler_and_target_environment_overrides_are_rejected(self): + for name in ( + "RUSTFLAGS", + "MIRIFLAGS", + "CARGO_BUILD_RUSTFLAGS", + "CARGO_BUILD_RUSTC_WRAPPER", + "CARGO_ENCODED_RUSTDOCFLAGS", + "CARGO_PROFILE_RELEASE_OVERFLOW_CHECKS", + "CARGO_TARGET_X86_64_UNKNOWN_LINUX_GNU_RUSTFLAGS", + ): + with self.subTest(name=name), self.assertRaises(ValueError): + verify.reject_overrides({name: "override"}) + verify.reject_overrides({"PATH": "/bin", "CARGO_TARGET_DIR": "/tmp/build"}) + + def test_make_controls_cannot_skip_gate_recipes_or_override_commands(self): + (self.directory / "Makefile").write_text( + "COMMAND = touch executed\n.PHONY: gate\ngate:\n\t$(COMMAND)\n" + ) + injected = self.directory / "injected.mk" + injected.write_text("override COMMAND = true\n") + for controls in ( + {"MAKEFLAGS": "n"}, + {"MAKEFLAGS": "t"}, + {"MFLAGS": "-n", "GNUMAKEFLAGS": "-n"}, + {"MAKEFLAGS": "-- COMMAND=true", "MAKEOVERRIDES": "COMMAND=true"}, + {"MAKEFILES": str(injected)}, + ): + with self.subTest(controls=controls): + marker = self.directory / "executed" + marker.unlink(missing_ok=True) + result = verify.run( + ["make", "-C", str(self.directory), "gate"], + self.directory / "make.log", + verify.make_environment(os.environ | controls), + 5, + ) + self.assertTrue(result["passed"]) + self.assertTrue(marker.exists()) + + def test_optimized_final_link_rejects_invalid_outcomes(self): + fixture = ( + SCRIPT.parents[1] / "libs/kaptan-err-reportable-macros/tests/final_link.py" + ) + harness = """ +import importlib.util,subprocess,sys +spec=importlib.util.spec_from_file_location('final_link',sys.argv[1]) +fixture=importlib.util.module_from_spec(spec); spec.loader.exec_module(fixture) +failure=sys.argv[3] +def run(arguments, cwd): + linking=arguments[0]=='c++' or arguments[-1]=='error-id-app' + duplicate=any('used-duplicate' in arg for arg in arguments) + code=int(linking and duplicate and failure=='diagnostic') + return subprocess.CompletedProcess(arguments,code, + 'host: test-host\\n' if arguments[0]=='rustc' else '', + 'unrelated link failure' if code else '') +fixture.run=run +sys.argv=[sys.argv[1],'--work-dir',sys.argv[2]] +fixture.main() +""" + for case, diagnostic in ( + ("success", "duplicate unexpectedly linked"), + ("diagnostic", "unrelated link failure"), + ): + with self.subTest(case=case): + result = subprocess.run( + [ + sys.executable, + "-O", + "-c", + harness, + str(fixture), + str(self.directory / case), + case, + ], + capture_output=True, + text=True, + timeout=10, + ) + self.assertNotEqual(result.returncode, 0) + self.assertIn(diagnostic, result.stderr) + + def test_source_intake_drift_and_finalization_failures_leave_failed_receipts(self): + baseline = {"sha256": "baseline", "entries": []} + changed = {"sha256": "changed", "entries": []} + for stage, snapshots in ( + ("intake", [ValueError("unavailable source")]), + ("archive", [baseline, baseline]), + ("drift", [baseline, baseline, changed, changed]), + ("finalization", [baseline, baseline, baseline, OSError("final snapshot")]), + ): + output = self.directory / stage + result = { + "completed": True, + "passed": True, + "exit_code": 0, + "log": "unused", + } + with ( + self.subTest(stage=stage), + mock.patch.object( + sys, "argv", [str(SCRIPT), "host", "--output", str(output)] + ), + mock.patch.object(verify.signal, "signal"), + mock.patch.object(verify, "snapshot", side_effect=snapshots), + mock.patch.object(verify, "capture", return_value="identity"), + mock.patch.object(verify, "run", return_value=result), + mock.patch.object( + verify.tarfile, + "open", + wraps=verify.tarfile.open, + side_effect=OSError("archive") if stage == "archive" else None, + ), + ): + self.assertEqual(verify.main(), 1) + receipt = json.loads((output / "receipt.json").read_text()) + self.assertFalse(receipt["passed"]) + if stage != "archive": + self.assertFalse(receipt["source_stable"]) + + def test_launch_failure_and_timeout_are_recorded(self): + failed = verify.run( + ["/no-such-verification-program"], + self.directory / "missing.log", + os.environ, + 1, + ) + self.assertFalse(failed["completed"]) + timed = verify.run( + [sys.executable, "-c", "import time; time.sleep(30)"], + self.directory / "timeout.log", + os.environ, + 0.05, + ) + self.assertFalse(timed["passed"]) + self.assertFalse(timed["completed"]) + + def test_repeated_termination_kills_the_owned_process_group(self): + pid_file = self.directory / "child.pid" + receipt = self.directory / "result.json" + child = ( + "import os,time,pathlib; pathlib.Path(%r).write_text(str(os.getpid())); time.sleep(30)" + % str(pid_file) + ) + harness = """ +import importlib.util,json,os,pathlib,signal,sys +spec=importlib.util.spec_from_file_location('verify',sys.argv[1]) +v=importlib.util.module_from_spec(spec); spec.loader.exec_module(v) +for s in (signal.SIGINT,signal.SIGTERM): signal.signal(s,v.interrupt) +r=v.run([sys.executable,'-c',sys.argv[2]],pathlib.Path(sys.argv[3]),os.environ,30) +pathlib.Path(sys.argv[4]).write_text(json.dumps(r)) +""" + parent = subprocess.Popen( + [ + sys.executable, + "-c", + harness, + str(SCRIPT), + child, + str(self.directory / "signal.log"), + str(receipt), + ] + ) + + def cleanup(): + if pid_file.exists(): + try: + os.killpg(int(pid_file.read_text()), signal.SIGKILL) + except ProcessLookupError: + pass + if parent.poll() is None: + parent.kill() + parent.wait() + + self.addCleanup(cleanup) + deadline = time.monotonic() + 5 + while not pid_file.exists() and time.monotonic() < deadline: + time.sleep(0.01) + self.assertTrue(pid_file.exists()) + child_pid = int(pid_file.read_text()) + os.kill(parent.pid, signal.SIGTERM) + os.kill(parent.pid, signal.SIGTERM) + self.assertEqual(parent.wait(timeout=5), 0) + self.assertFalse(json.loads(receipt.read_text())["completed"]) + with self.assertRaises(ProcessLookupError): + os.kill(child_pid, 0) + + def test_cancellation_during_spawn_successful_wait_or_cleanup_cannot_pass(self): + for stage in ("spawn", "wait", "cleanup"): + process = mock.Mock(pid=999999) + + def wait(**_kwargs): + if stage == "wait": + os.kill(os.getpid(), signal.SIGTERM) + return 0 + + def spawn(*_args, **_kwargs): + if stage == "spawn": + os.kill(os.getpid(), signal.SIGTERM) + return process + + def kill(*_args): + if stage == "cleanup": + os.kill(os.getpid(), signal.SIGTERM) + + process.wait.side_effect = wait + with ( + self.subTest(stage=stage), + mock.patch.object(verify.subprocess, "Popen", side_effect=spawn), + mock.patch.object(verify.os, "killpg", side_effect=kill), + ): + result = verify.run( + ["fake-child"], self.directory / f"{stage}.log", os.environ, 1 + ) + self.assertFalse(result["passed"]) + self.assertFalse(result["completed"]) + process.wait.assert_called() + + +if __name__ == "__main__": + unittest.main() diff --git a/firmware/scripts/verify.py b/firmware/scripts/verify.py new file mode 100644 index 0000000..a446da6 --- /dev/null +++ b/firmware/scripts/verify.py @@ -0,0 +1,710 @@ +#!/usr/bin/env python3 +"""Run the fixed verification gates and retain source-bound evidence.""" + +import argparse +import hashlib +import json +import os +from pathlib import Path +import platform +import re +import shutil +import signal +import subprocess +import sys +import tarfile +import time +import tomllib + + +ROOT = Path(__file__).resolve().parents[2] +FIRMWARE = ROOT / "firmware" +GATES = ("host", "targets", "boards", "coverage", "miri", "kani") + + +class Interrupted(Exception): + pass + + +def interrupt(signum, _frame): + raise Interrupted(f"Received signal {signum}") + + +def reject_overrides(environment): + fixed = { + "RUSTFLAGS", + "CARGO_ENCODED_RUSTFLAGS", + "RUSTC", + "RUSTDOC", + "RUSTDOCFLAGS", + "CARGO_ENCODED_RUSTDOCFLAGS", + "RUSTC_WRAPPER", + "RUSTC_WORKSPACE_WRAPPER", + "RUSTC_BOOTSTRAP", + "MIRIFLAGS", + "MIRI_SYSROOT", + "MIRI_LIB_SRC", + "MIRI_NO_STD", + "KANIFLAGS", + "CBMC", + } + rejected = [ + key + for key, value in environment.items() + if value + and ( + key in fixed + or ( + key.startswith("CARGO_BUILD_") + and key not in ("CARGO_BUILD_JOBS", "CARGO_BUILD_TARGET_DIR") + ) + or key.startswith("CARGO_PROFILE_") + or (key.startswith("CARGO_TARGET_") and key != "CARGO_TARGET_DIR") + ) + ] + if rejected: + raise ValueError( + f"Remove verification overrides: {', '.join(sorted(rejected))}" + ) + + +def make_environment(environment): + # A wrapper's dry-run, touch or command-line overrides must not suppress gates. + controls = {"MAKEFLAGS", "MFLAGS", "MAKEOVERRIDES", "GNUMAKEFLAGS", "MAKEFILES"} + return {key: value for key, value in environment.items() if key not in controls} + + +def sha256(path): + digest = hashlib.sha256() + with path.open("rb") as source: + for chunk in iter(lambda: source.read(1024 * 1024), b""): + digest.update(chunk) + return digest.hexdigest() + + +def capture(argv, cwd=FIRMWARE, env=None): + return subprocess.check_output(argv, cwd=cwd, env=env, text=True).strip() + + +def snapshot(root=ROOT): + names = subprocess.check_output( + ["git", "ls-files", "--cached", "--others", "--exclude-standard", "-z"], + cwd=root, + ).split(b"\0") + entries = [] + for name in sorted({os.fsdecode(name) for name in names if name}): + path = root / name + if path.is_symlink(): + raise ValueError( + f"Source symlink requires an explicit input boundary: {name}" + ) + entry = {"path": name, "kind": "absent"} + if path.is_file(): + entry.update( + kind="file", sha256=sha256(path), mode=path.stat().st_mode & 0o777 + ) + elif path.exists(): + raise ValueError(f"Unsupported source entry: {name}") + entries.append(entry) + encoded = json.dumps(entries, sort_keys=True, separators=(",", ":")).encode() + return {"sha256": hashlib.sha256(encoded).hexdigest(), "entries": entries} + + +def load_contract(): + with (FIRMWARE / "verification.toml").open("rb") as source: + contract = tomllib.load(source) + if contract["format"] != 1: + raise ValueError("Unsupported verification contract format") + with (FIRMWARE / "Cargo.toml").open("rb") as source: + workspace = tomllib.load(source)["workspace"] + packages = {} + for member in workspace["members"]: + with (FIRMWARE / member / "Cargo.toml").open("rb") as source: + name = tomllib.load(source)["package"]["name"] + packages[name] = member + declared = [name for area in contract["areas"] for name in area["packages"]] + if len(declared) != len(set(declared)) or set(declared) != set(packages): + raise ValueError( + "Every workspace package must have exactly one verification area" + ) + property_ids = [prop["id"] for prop in contract["properties"]] + if not property_ids or len(property_ids) != len(set(property_ids)): + raise ValueError("Empty or duplicate property inventory") + for prop in contract["properties"]: + if ( + prop["package"] not in packages + or not prop["harnesses"] + or len(prop["harnesses"]) != len(set(prop["harnesses"])) + or len(prop["covers"]) != len(prop["harnesses"]) + or any(count <= 0 for count in prop["covers"]) + or not (FIRMWARE / prop["source"]).is_file() + ): + raise ValueError( + f"Invalid proof owner or empty harness inventory: {prop['id']}" + ) + miri = contract["miri"] + if ( + not miri["packages"] + or len(miri["packages"]) != len(set(miri["packages"])) + or not set(miri["packages"]) <= set(packages) + or not miri["seeds"] + or len(miri["seeds"]) != len(set(miri["seeds"])) + or any(type(seed) is not int or not 0 <= seed < 2**64 for seed in miri["seeds"]) + ): + raise ValueError( + "Miri requires known distinct packages and nonempty distinct u64 seeds" + ) + return contract, packages + + +def reviewed_unreachable(harness, check): + addition = "attempt to add with overflow" + shift = "attempt to shift left with overflow" + reviewed = { + ( + "kani_proofs::clock_regression_requires_successful_inhibited_reset", + "kani_proofs::clock_regression_requires_successful_inhibited_reset::{closure#0}", + addition, + ), + ( + "kani_proofs::failed_commit_preserves_error_and_latches_inhibition", + "kani_proofs::failed_commit_preserves_error_and_latches_inhibition::{closure#1}", + addition, + ), + ( + "kani_proofs::dshot_symbols_round_trip_and_end_low", + "core::fmt::Arguments::<'_>::from_str", + shift, + ), + ( + "kani_proofs::pid_constructor_establishes_invariant", + "core::fmt::Arguments::<'_>::from_str", + shift, + ), + } + return ( + check["category"] == "assertion" + and (harness, check["function"], check["description"]) in reviewed + ) + + +def pid_rejected_nan(prop, harness, check): + return ( + prop["id"] == "control.pid-state" + and harness == "kani_proofs::pid_update_preserves_bounds_or_state" + and check["category"] == "NaN" + and check["description"] == "NaN on addition" + and check["function"] == "Pid::update_with_valid_time" + and check["location"] + == { + "file": "libs/kaptan-control/src/lib.rs", + "line": str(prop["intermediate_nan_line"]), + "column": "13", + } + ) + + +def validate_kani(path, prop, version, target, exit_code, rustc): + report = json.loads(path.read_text()) + expected = prop["harnesses"] + expected_covers = dict(zip(expected, prop["covers"], strict=True)) + qualified = prop["id"] == "control.pid-state" + failures = int(qualified) + metadata = report["metadata"] + if ( + metadata["version"] != "1.0" + or metadata["kani_version"] != version + or metadata["target"] != target + or report["tools"]["rustc"] != rustc + ): + raise ValueError( + "Kani version or target differs from the verification contract" + ) + owner = prop["package"].replace("-", "_") + harness_metadata = report["harness_metadata"] + if ( + len(harness_metadata) != len(expected) + or {item["pretty_name"] for item in harness_metadata} != set(expected) + or any( + item["crate_name"] != owner or item["source"]["file"] != prop["source"] + for item in harness_metadata + ) + ): + raise ValueError( + "Kani harness ownership differs from the verification contract" + ) + results = report["verification_results"]["results"] + names = [result["harness_id"] for result in results] + summary = report["verification_results"]["summary"] + if ( + not expected + or len(names) != len(set(names)) + or set(names) != set(expected) + or summary["status"] != "completed" + or summary["total_harnesses"] != len(expected) + or summary["executed"] != len(expected) + or summary["successful"] != len(expected) - failures + or summary["failed"] != failures + or exit_code != failures + ): + raise ValueError("Kani did not complete the exact required harness inventory") + accepted = [] + unreachable = [] + for result in results: + is_pid_update = ( + qualified + and result["harness_id"] + == "kani_proofs::pid_update_preserves_bounds_or_state" + ) + if result["status"] != ("Failure" if is_pid_update else "Success"): + raise ValueError(f"Kani harness failed: {result['harness_id']}") + checks = result["checks"] + covers = [check for check in checks if check["category"] == "cover"] + if len(covers) != expected_covers[result["harness_id"]] or any( + check["status"] != "Satisfied" for check in covers + ): + raise ValueError( + f"Missing or unsatisfied reachability evidence: {result['harness_id']}" + ) + assertions = [check for check in checks if check["category"] != "cover"] + if not assertions: + raise ValueError( + "A proof needs assertions as well as reachability witnesses" + ) + for check in assertions: + if check["status"] == "Success": + continue + if check["status"] == "Unreachable" and reviewed_unreachable( + result["harness_id"], check + ): + unreachable.append(check) + elif check["status"] == "Failure" and pid_rejected_nan( + prop, result["harness_id"], check + ): + accepted.append(check) + else: + raise ValueError(f"Unproved assertion: {check}") + if len(accepted) != failures: + raise ValueError("The reviewed intermediate-NaN diagnostic changed") + return { + "raw_summary": summary, + "raw_verifier_passed": exit_code == 0, + "contract_checks_passed": True, + "expected_intermediate_nan": accepted, + "reviewed_unreachable": unreachable, + "tools": report["tools"], + } + + +def validate_miri(log, package_count): + results = re.findall( + r"test result: ok\. (\d+) passed; (\d+) failed; (\d+) ignored; " + r"\d+ measured; (\d+) filtered out", + log.read_text(), + ) + if len(results) != package_count or any( + int(passed) == 0 or int(failed) or int(ignored) or int(filtered) + for passed, failed, ignored, filtered in results + ): + raise ValueError( + "Miri must execute every selected library suite without ignored tests" + ) + return sum(int(result[0]) for result in results) + + +def run(argv, log, env, timeout): + started = time.time() + monotonic_start = time.monotonic() + result = {"argv": argv, "cwd": str(FIRMWARE), "started_unix": started} + process = None + pending = [] + handlers = {} + + def defer(signum, _frame): + pending[:] = [signum] + + with log.open("wb") as output: + try: + # Keep cancellation deferred until the owned process group is reaped. + # Children inherit neither a blocked mask nor Python signal handlers. + for signum in (signal.SIGINT, signal.SIGTERM): + handlers[signum] = signal.signal(signum, defer) + process = subprocess.Popen( + argv, + cwd=FIRMWARE, + env=env, + stdout=output, + stderr=subprocess.STDOUT, + start_new_session=True, + ) + while True: + if pending: + raise Interrupted(f"Received signal {pending[0]}") + remaining = timeout - (time.monotonic() - monotonic_start) + if remaining <= 0: + raise subprocess.TimeoutExpired(argv, timeout) + try: + result["exit_code"] = process.wait(timeout=min(remaining, 0.1)) + result["completed"] = True + break + except subprocess.TimeoutExpired: + continue + except ( + subprocess.TimeoutExpired, + Interrupted, + KeyboardInterrupt, + OSError, + ) as error: + result.update(completed=False, error=str(error), exit_code=None) + finally: + if process is not None: + try: + os.killpg(process.pid, signal.SIGKILL) + except ProcessLookupError: + pass + process.wait() + for signum, handler in handlers.items(): + signal.signal(signum, handler) + if pending: + result.update( + completed=False, error=f"Received signal {pending[0]}", exit_code=None + ) + result.update( + seconds=time.monotonic() - monotonic_start, log=str(log), log_sha256=sha256(log) + ) + result["passed"] = result["completed"] and result["exit_code"] == 0 + return result + + +def tool_paths(contract): + install = ( + FIRMWARE / "target/verification-tools" / f"kani-{contract['kani']['version']}" + ) + return install, install / "home" + + +def setup(contract): + install, home = tool_paths(contract) + env = os.environ | {"CARGO_BUILD_JOBS": "2", "KANI_HOME": str(home)} + commands = [ + [ + "rustup", + "toolchain", + "install", + contract["miri"]["toolchain"], + "--profile", + "minimal", + "--component", + "miri,rust-src", + ], + ["cargo", f"+{contract['miri']['toolchain']}", "miri", "setup"], + [ + "cargo", + "+1.90.0", + "install", + "kani-verifier", + "--locked", + "--version", + contract["kani"]["version"], + "--root", + str(install), + ], + [str(install / "bin/cargo-kani"), "kani", "setup"], + ] + logs = FIRMWARE / "target/verification-tools" / f"setup-{time.time_ns()}" + logs.mkdir(parents=True) + for index, command in enumerate(commands): + result = run(command, logs / f"{index}.log", env, 3600) + if not result["passed"]: + raise ValueError(f"Tool setup failed: {result}") + print(f"Tool setup logs: {logs}") + + +def main(): + for signum in (signal.SIGINT, signal.SIGTERM): + signal.signal(signum, interrupt) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("gate", choices=(*GATES, "all", "setup", "inventory")) + parser.add_argument( + "--output", type=Path, help="New evidence directory; must not exist" + ) + args = parser.parse_args() + if args.gate in ("setup", "inventory"): + contract, packages = load_contract() + if args.gate == "setup": + setup(contract) + else: + print(json.dumps({"packages": packages, "contract": contract}, indent=2)) + return 0 + selected = GATES if args.gate == "all" else (args.gate,) + output = ( + args.output or FIRMWARE / "target/verification" / str(time.time_ns()) + ).resolve() + if output.is_relative_to(ROOT) and not output.is_relative_to(FIRMWARE / "target"): + raise ValueError("Evidence inside the repository must be under firmware/target") + output.mkdir(parents=True, exist_ok=False) + baseline = None + receipt = { + "format": 1, + "completed": False, + "passed": False, + "source_stable": False, + "source": None, + "host": platform.platform(), + "python": sys.version, + "gates": [], + } + build = FIRMWARE / "target/verification-build" + env = make_environment(os.environ) | { + "CARGO_BUILD_JOBS": "2", + "RUSTUP_TOOLCHAIN": "1.90.0", + "CARGO_TARGET_DIR": str(build / "stable"), + "CARGO_NET_OFFLINE": "true", + } + try: + reject_overrides(os.environ) + baseline = snapshot() + receipt["source"] = baseline + contract, packages = load_contract() + receipt.update( + contract=contract, + packages=packages, + head=capture(["git", "rev-parse", "HEAD"]), + git_status=capture( + ["git", "status", "--porcelain=v1", "--untracked-files=all"] + ), + ) + archive = output / "source.tar.gz" + with tarfile.open(archive, "w:gz") as source: + for entry in baseline["entries"]: + if entry["kind"] == "file": + source.add( + ROOT / entry["path"], arcname=entry["path"], recursive=False + ) + receipt["source_archive_sha256"] = sha256(archive) + install, kani_home = tool_paths(contract) + receipt["rustc"] = capture(["rustc", "+1.90.0", "-vV"], env=env) + receipt["cargo"] = capture(["cargo", "+1.90.0", "-V"], env=env) + for gate in selected: + if snapshot() != baseline: + raise ValueError("Source changed before gate execution") + commands = [] + gate_env = dict(env) + if gate in ("host", "targets", "boards", "coverage"): + target = { + "host": "pre-commit", + "targets": "target-checks", + "boards": "boards", + "coverage": "coverage", + }[gate] + directory = FIRMWARE if gate == "targets" else ROOT + if gate == "coverage": + gate_env["CARGO_TARGET_DIR"] = str(build / "coverage") + commands.append( + (gate, ["make", "-C", str(directory), target], gate_env, None) + ) + elif gate == "miri": + miri = contract["miri"] + receipt["miri"] = capture( + ["cargo", f"+{miri['toolchain']}", "miri", "--version"], env=env + ) + receipt["miri_rustc"] = capture( + ["rustc", f"+{miri['toolchain']}", "-vV"], env=env + ) + sysroot = Path( + capture( + ["rustc", f"+{miri['toolchain']}", "--print", "sysroot"], + env=env, + ) + ) + receipt["miri_binary_sha256"] = sha256(sysroot / "bin/miri") + gate_env["CARGO_TARGET_DIR"] = str(build / "miri") + for seed in miri["seeds"]: + seeded = gate_env | { + "MIRIFLAGS": " ".join(miri["flags"] + [f"-Zmiri-seed={seed}"]) + } + command = [ + "cargo", + f"+{miri['toolchain']}", + "miri", + "test", + "--locked", + "--offline", + "--target", + miri["target"], + "--lib", + ] + for package in miri["packages"]: + command += ["-p", package] + commands.append((f"miri-{seed}", command, seeded, None)) + else: + kani = contract["kani"] + gate_env["KANI_HOME"] = str(kani_home) + binary = str(install / "bin/cargo-kani") + receipt["kani"] = capture( + [binary, "kani", "--version", "--verbose"], env=gate_env + ) + receipt["kani_launcher_sha256"] = sha256(Path(binary)) + bundle = kani_home / f"kani-{kani['version']}" + receipt["kani_toolchain"] = ( + (bundle / "rust-toolchain-version").read_text().strip() + ) + receipt["kani_rustc"] = (bundle / "rustc-version").read_text().strip() + if receipt["kani_toolchain"] != f"{kani['toolchain']}-{kani['target']}": + raise ValueError( + "Kani bundled compiler differs from the pinned toolchain" + ) + receipt["kani_binary_hashes"] = { + name: sha256(bundle / "bin" / name) + for name in ("kani-compiler", "cbmc", "goto-instrument") + } + for prop in contract["properties"]: + export = output / f"{prop['id']}.json" + command = [ + binary, + "kani", + "--lib", + "-p", + prop["package"], + "--target-dir", + str(build / "kani"), + "--jobs", + "1", + "--solver", + kani["solver"], + "-Z", + "unstable-options", + "--harness-timeout", + str(kani["harness_timeout_seconds"]), + "--export-json", + str(export), + ] + commands.append((prop["id"], command, gate_env, prop)) + for name, command, command_env, prop in commands: + print(f"Verifying {name}; evidence: {output}", flush=True) + result = run(command, output / f"{name}.log", command_env, 3600) + result.update( + gate=gate, + name=name, + environment={ + key: value + for key, value in command_env.items() + if env.get(key) != value + or key + in ( + "CARGO_BUILD_JOBS", + "CARGO_TARGET_DIR", + "RUSTUP_TOOLCHAIN", + "CARGO_NET_OFFLINE", + ) + }, + ) + receipt["gates"].append(result) + if result["completed"] and (result["passed"] or gate == "kani"): + try: + if gate == "miri": + result["tests_passed"] = validate_miri( + Path(result["log"]), len(contract["miri"]["packages"]) + ) + elif gate == "kani": + export = output / f"{prop['id']}.json" + result["proof_summary"] = validate_kani( + export, + prop, + kani["version"], + kani["target"], + result["exit_code"], + receipt["kani_rustc"], + ) + result["export_sha256"] = sha256(export) + result["passed"] = True + if not result["proof_summary"]["raw_verifier_passed"]: + print( + "PID contract checks passed; expected intermediate-NaN diagnostic. Raw Kani verdict remains Failure.", + flush=True, + ) + elif gate == "boards": + artifacts = [] + for board in ("geprc-f722-v2", "kakute-f7-mini-v3"): + for suffix in ("", ".bin"): + path = ( + build + / "stable/thumbv7em-none-eabihf/release" + / f"kaptan-{board}{suffix}" + ) + retained = output / "artifacts" / path.name + retained.parent.mkdir(exist_ok=True) + shutil.copy2(path, retained) + artifacts.append( + { + "path": str(retained), + "sha256": sha256(retained), + } + ) + result["artifacts"] = artifacts + elif gate == "coverage": + reports = build / "coverage" + names = ["metadata.json", "packages.txt"] + names += [ + f"{line.split()[0]}.lcov" + for line in (reports / "packages.txt") + .read_text() + .splitlines() + ] + names += [ + f"{package}.json" + for package in ( + "kaptan-math", + "kaptan-navigation", + "kaptan-control", + "kaptan-safety", + ) + ] + retained = output / "coverage" + retained.mkdir() + result["reports"] = [] + for name in names: + destination = retained / name + shutil.copy2(reports / name, destination) + result["reports"].append( + { + "path": str(destination), + "sha256": sha256(destination), + } + ) + except (ValueError, KeyError, OSError) as error: + result.update(passed=False, validation_error=str(error)) + if snapshot() != baseline: + raise ValueError("Source changed during gate execution") + (output / "receipt.json").write_text( + json.dumps(receipt, indent=2) + "\n" + ) + if not result["passed"]: + raise ValueError(f"Gate failed: {name}; see {result['log']}") + receipt["completed"] = True + receipt["passed"] = True + except ( + ValueError, + OSError, + subprocess.CalledProcessError, + Interrupted, + KeyboardInterrupt, + ) as error: + receipt["error"] = str(error) + print(error, file=sys.stderr) + finally: + # Finish the failure receipt even if cancellation arrives a second time. + for signum in (signal.SIGINT, signal.SIGTERM): + signal.signal(signum, signal.SIG_IGN) + try: + receipt["source_stable"] = baseline is not None and snapshot() == baseline + except (ValueError, OSError, subprocess.CalledProcessError) as error: + receipt.update(source_stable=False, finalization_error=str(error)) + receipt["passed"] = receipt["passed"] and receipt["source_stable"] + (output / "receipt.json").write_text(json.dumps(receipt, indent=2) + "\n") + print(f"Verification receipt: {output / 'receipt.json'}") + return 0 if receipt["passed"] else 1 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/firmware/tools/configurator/Makefile b/firmware/tools/configurator/Makefile index e05cc29..e451e2e 100644 --- a/firmware/tools/configurator/Makefile +++ b/firmware/tools/configurator/Makefile @@ -1,32 +1,17 @@ -override SHELL := /bin/sh -override MAKEFLAGS += --no-print-directory +SHELL := /bin/sh +MAKEFLAGS += --no-print-directory .DEFAULT_GOAL := help .DELETE_ON_ERROR: -override CARGO := cargo -override CARGO_FLAGS := --locked --offline - -override PRIMARY_GOAL := $(firstword $(MAKECMDGOALS)) - -ifeq ($(PRIMARY_GOAL),run) - -.PHONY: run - -.DEFAULT: - @: - -else - .PHONY: help run help: ## Show configurator commands @printf '%s\n' 'Configurator' '' \ 'Start the local web application, then select the serial device in the browser:' \ - ' make firmware/tools/configurator' + ' make configurator' '' \ + 'Command syntax from firmware/:' \ + ' cargo run --locked --offline -p kaptan-configurator -- [--source-system ID] [--serial PATH] [--baud RATE]' -endif - -run: ## Run the configurator with the remaining command-line arguments - @exec python3 ../../../scripts/make-argv.py exec run \ - $(CARGO) run $(CARGO_FLAGS) -p kaptan-configurator -- +run: ## Start the local configurator web application + cargo run --locked --offline -p kaptan-configurator diff --git a/firmware/verification.toml b/firmware/verification.toml new file mode 100644 index 0000000..afe4197 --- /dev/null +++ b/firmware/verification.toml @@ -0,0 +1,166 @@ +format = 1 + +[miri] +toolchain = "nightly-2026-06-23" +target = "x86_64-unknown-linux-gnu" +packages = ["kaptan-spi", "kaptan-err-reportable", "kaptan-log"] +seeds = [0, 1, 2, 3, 4, 5, 6, 7] +flags = [ + "-Zmiri-strict-provenance", + "-Zmiri-symbolic-alignment-check", + "-Zmiri-preemption-rate=1", +] +claim = "Existing unit tests and bounded concurrent ownership tests execute with provenance, aliasing, validity and race checks enabled." +limits = "Executed schedules only. Host memory stands in for DMA. No device quiescence, interrupt or MMIO claim." + +[kani] +version = "0.68.0" +toolchain = "nightly-2026-08-21" +target = "x86_64-unknown-linux-gnu" +solver = "cadical" +harness_timeout_seconds = 300 + +[[properties]] +id = "math.sqrt-domain" +package = "kaptan-math" +source = "libs/kaptan-math/src/kani_proofs.rs" +harnesses = ["kani_proofs::sqrt_preserves_domain_and_zero_sign"] +covers = [6] +claim = "All f32 input bit patterns obey square-root domain classification and preserve signed zero. Positive finite inputs return positive finite values." +assumptions = "Kani's floating-point arithmetic model; actual four-iteration implementation, with unwind bound 5." +limits = "No accuracy bound, normalization proof or target floating-point equivalence." + +[[properties]] +id = "control.pid-state" +package = "kaptan-control" +source = "libs/kaptan-control/src/kani_proofs.rs" +harnesses = [ + "kani_proofs::pid_constructor_establishes_invariant", + "kani_proofs::pid_update_preserves_bounds_or_state", +] +covers = [3, 3] +intermediate_nan_line = 196 +claim = "The constructor establishes the PID invariant. One update returns finite bounded output and integral, or retains the complete previous state on error. Reset establishes zero integral." +assumptions = "Validated arbitrary configuration and any finite prior integral within its configured bound. Dynamic inputs span all f32 bit patterns." +limits = "Raw Kani reports Failure for one reviewed intermediate-NaN diagnostic at the declared location. Contract assertions and covers pass; the implementation rejects that NaN before state mutation. No tracking-performance, vehicle-stability or complete controller proof." + +[[properties]] +id = "safety.commit-authority" +package = "kaptan-safety" +source = "libs/kaptan-safety/src/kani_proofs.rs" +harnesses = [ + "kani_proofs::commit_requires_current_health_and_completed_dwell", + "kani_proofs::failed_commit_preserves_error_and_latches_inhibition", + "kani_proofs::clock_regression_requires_successful_inhibited_reset", +] +covers = [4, 1, 2] +claim = "Named public-operation histories check health and dwell before commit, preserve commit errors, latch inhibition, and require successful inhibition to reset a regressed clock." +assumptions = "Positive dwell, arbitrary u64 times and health flags. Callbacks return normally. Each harness declares its finite operation history." +limits = "No arbitrary-history, complete flight-runtime or physical-output proof." + +[[properties]] +id = "actuator.dshot-format" +package = "kaptan-actuator" +source = "libs/kaptan-actuator/src/kani_proofs.rs" +harnesses = [ + "kani_proofs::dshot_frame_preserves_payload_and_checksum", + "kani_proofs::dshot_symbols_round_trip_and_end_low", + "kani_proofs::dshot_timer_rounding_keeps_compares_inside_period", + "kani_proofs::arming_duration_product", + "kani_proofs::arming_frame_count", +] +covers = [3, 2, 2, 2, 3] +claim = "Packet payload/checksum, MSB-first symbol encoding, trailing low symbols and timer rounding satisfy their integer contracts. Arming counts compose a bounded duration/cadence product with a separately proved minimum-frame conversion." +assumptions = "Supported DShot rates and constructor-admitted throttle values. Timer clocks, durations and dispatch cadences span their complete integer types; duration construction admits 1..=8,000 ms. Frame conversion spans all u64 products; frames_at composition is source-reviewed." +limits = "This reference crate is not linked to a physical actuator route. No electrical or execution-timing claim." + +# Every workspace package must belong to exactly one area. New owners require +# an explicit account of their evidence and outstanding obligations. +[[areas]] +name = "Numerical core" +packages = ["kaptan-math", "kaptan-navigation", "kaptan-control"] +checks = ["host", "coverage", "targets"] +gap = "Independent numerical tests and strict coverage remain necessary. Complete estimator correctness, error enclosures and target floating-point behavior are not formally established." + +[[areas]] +name = "Flight authority" +packages = ["kaptan-safety", "kaptan-flight-runtime"] +checks = ["host", "coverage", "targets"] +gap = "Named safety proofs do not cover every runtime history, mission requirement or physical output consumer." + +[[areas]] +name = "Actuator reference" +packages = ["kaptan-actuator"] +checks = ["host", "coverage"] +gap = "No composed physical actuator route or vehicle qualification." + +[[areas]] +name = "Unsafe library ownership" +packages = ["kaptan-spi", "kaptan-log", "kaptan-err-reportable"] +checks = ["host", "coverage", "miri"] +gap = "Miri explores finitely many executions. Actual DMA completion and interrupt interference remain hardware obligations." + +[[areas]] +name = "Configuration" +packages = [ + "kaptan-config", + "kaptan-config-derive", + "kaptan-flight-config", + "kaptan-ports", +] +checks = ["host", "coverage"] +gap = "Schema compiler fixtures, runtime validation and journal tests do not constitute exhaustive parser or physical power-loss proofs." + +[[areas]] +name = "Drivers and observations" +packages = ["kaptan-drivers", "kaptan-sensor", "kaptan-i2c", "kaptan-time"] +checks = ["host", "coverage"] +gap = "Mock bus tests do not establish sensor accuracy, wiring, timing, freshness or recovery on silicon." + +[[areas]] +name = "Communication" +packages = [ + "kaptan-mavlink", + "kaptan-file-mavlink", + "kaptan-diagnostics-mavlink", + "kaptan-data-channel", + "kaptan-tx", +] +checks = ["host", "coverage"] +gap = "Protocol and queue tests do not exhaust every hostile input, transport failure or interleaving." + +[[areas]] +name = "Compiler-generated error identities" +packages = ["kaptan-err-reportable-macros"] +checks = ["host", "coverage"] +gap = "Compiler fixtures and final-link checks cover named cases. Runtime-harness coverage does not measure macro expansion coverage." + +[[areas]] +name = "MCU platform" +packages = ["platform-stm32f7"] +checks = ["host", "coverage", "targets", "boards"] +gap = "USB wait deadlines and terminal faults have host regression checks. MMIO, assembly, caches, DMA quiescence, interrupt timing, WCET and peak stack remain outside host proof and interpreter evidence." + +[[areas]] +name = "Board images" +packages = ["kaptan-geprc-f722-v2", "kaptan-kakute-f7-mini-v3"] +checks = ["targets", "boards"] +gap = "Linked ELF placement checks and image hashes do not qualify physical hardware or flight." + +[[areas]] +name = "Configurator" +packages = ["kaptan-configurator"] +checks = ["host", "coverage", "targets"] +gap = "Hosted serial/HTTP and browser-state tests are not exhaustive OS, UI or security verification." + +[[components]] +name = "Ground suite" +path = "ground_suite" +checks = ["host: native UTF conversion helper"] +gap = "Flutter/native product builds and operational behavior need their separate documented platform gates." + +[[components]] +name = "Build scripts and documentation" +path = "." +checks = ["host: formatting, script tests, API documentation and mdBook"] +gap = "The evidence runner and tools remain trusted software requiring review. No tool qualification or certification credit is asserted." diff --git a/flake.nix b/flake.nix index 1c49716..b42d759 100644 --- a/flake.nix +++ b/flake.nix @@ -23,8 +23,10 @@ packages = [ pkgs.rustup pkgs.gcc + pkgs.cargo-llvm-cov pkgs.dfu-util pkgs.mdbook + pkgs.nodejs pkgs.ripgrep pkgs.ruff pkgs.shfmt diff --git a/scripts/make-argv.py b/scripts/make-argv.py deleted file mode 100644 index 44e5b7c..0000000 --- a/scripts/make-argv.py +++ /dev/null @@ -1,275 +0,0 @@ -#!/usr/bin/env python3 -"""Preserve application argv across GNU Make's command-line parser. - -GNU Make removes variable assignments, consumes its first ``--``, and flattens -quoted goal names in ``MAKECMDGOALS``. Linux exposes the original NUL-delimited -argument vector in procfs, which lets the Makefiles keep a conventional -``make component -- application arguments`` interface without rebuilding a -command string in the shell. -""" - -from __future__ import annotations - -import base64 -import errno -import json -import os -from pathlib import Path -import re -import sys -from typing import NoReturn - - -PAYLOAD_ENV = "KAPTAN_MAKE_ARGV" -ARG_COUNT_ENV = "KAPTAN_MAKE_ARG_COUNT" -_MAKE_FLAG_ENV = ("MAKEFLAGS", "MFLAGS") - - -class ArgumentRecoveryError(RuntimeError): - """Raised when the original Make invocation cannot be recovered.""" - - -def encode_arguments(arguments: list[str]) -> str: - """Encode an argument vector into an ASCII-only environment value.""" - - document = json.dumps(arguments, ensure_ascii=True, separators=(",", ":")) - return base64.urlsafe_b64encode(document.encode("ascii")).decode("ascii") - - -def decode_arguments(encoded: str) -> list[str]: - """Decode an argument vector produced by :func:`encode_arguments`.""" - - try: - document = base64.b64decode(encoded, altchars=b"-_", validate=True) - arguments = json.loads(document.decode("ascii")) - except (ValueError, UnicodeError, json.JSONDecodeError) as error: - raise ArgumentRecoveryError( - f"invalid application argument payload in {PAYLOAD_ENV}" - ) from error - - if not isinstance(arguments, list) or not all( - isinstance(argument, str) for argument in arguments - ): - raise ArgumentRecoveryError( - f"invalid application argument payload in {PAYLOAD_ENV}" - ) - return arguments - - -def read_process_arguments(pid: int, proc_root: Path = Path("/proc")) -> list[str]: - """Read one process's exact NUL-delimited argv from procfs.""" - - path = proc_root / str(pid) / "cmdline" - try: - raw = path.read_bytes() - except OSError as error: - raise ArgumentRecoveryError( - f"cannot read {path}; exact Make argument forwarding requires Linux /proc" - ) from error - - if not raw: - raise ArgumentRecoveryError(f"cannot recover arguments from empty {path}") - if not raw.endswith(b"\0"): - raise ArgumentRecoveryError( - f"cannot recover unterminated arguments from {path}" - ) - return [os.fsdecode(argument) for argument in raw[:-1].split(b"\0")] - - -def read_parent_pid(pid: int, proc_root: Path = Path("/proc")) -> int: - """Read a process's parent PID from procfs.""" - - path = proc_root / str(pid) / "status" - try: - status = path.read_text(encoding="utf-8") - except OSError as error: - raise ArgumentRecoveryError( - f"cannot read {path}; exact Make argument forwarding requires Linux /proc" - ) from error - - for line in status.splitlines(): - if line.startswith("PPid:"): - return int(line.split(":", 1)[1].strip()) - raise ArgumentRecoveryError(f"cannot find PPid in {path}") - - -def find_make_arguments(marker: str, start_pid: int | None = None) -> list[str]: - """Find the nearest parent Make invocation containing *marker*.""" - - pid = os.getppid() if start_pid is None else start_pid - visited: set[int] = set() - - while pid > 1 and pid not in visited: - visited.add(pid) - arguments = read_process_arguments(pid) - executable = Path(arguments[0]).name if arguments else "" - if marker in arguments and executable.endswith("make"): - return arguments - pid = read_parent_pid(pid) - - raise ArgumentRecoveryError( - f"cannot find a parent Make invocation containing {marker!r}; " - "exact argument forwarding requires Linux /proc" - ) - - -def _tail_after_marker(make_arguments: list[str], marker: str) -> list[str]: - try: - marker_index = make_arguments.index(marker) - except ValueError as error: - raise ArgumentRecoveryError( - f"cannot find {marker!r} in the parent Make invocation" - ) from error - - return make_arguments[marker_index + 1 :] - - -def arguments_after_marker(make_arguments: list[str], marker: str) -> list[str]: - """Return arguments following *marker*, consuming one following ``--``.""" - - arguments = _tail_after_marker(make_arguments, marker) - if arguments[:1] == ["--"]: - return arguments[1:] - return arguments - - -def select_route( - make_arguments: list[str], - component: str, - default_target: str, - local_targets: set[str], -) -> tuple[str, list[str]]: - """Select a local Make target and the exact application payload. - - ``default_target`` applies only when the component has no arguments. An - explicit delimiter or backward-compatible unknown words always select the - component's ``run`` target. - """ - - arguments = _tail_after_marker(make_arguments, component) - if "--" in arguments: - separator = arguments.index("--") - before_separator = arguments[:separator] - payload = arguments[separator + 1 :] - if len(before_separator) == 1 and before_separator[0] in local_targets: - return before_separator[0], payload - if before_separator: - raise ArgumentRecoveryError( - f"unexpected words before -- for {component}: " - + " ".join(repr(word) for word in before_separator) - ) - return "run", payload - - if not arguments: - return default_target, [] - if len(arguments) == 1 and arguments[0] in local_targets: - return arguments[0], [] - return "run", arguments - - -def assignment_names(arguments: list[str]) -> set[str]: - """Return environment names which GNU Make may treat as assignments.""" - - names: set[str] = set() - for argument in arguments[1:]: - for operator in (":::=", "::=", ":=", "+=", "?=", "!=", "="): - if operator in argument: - name, _ = argument.split(operator, 1) - if name: - names.add(name) - break - return names - - -def scrub_make_environment( - environment: dict[str, str], make_arguments: list[str] -) -> dict[str, str]: - """Remove recursive-Make flags and command-line variable side effects.""" - - clean = environment.copy() - clean.pop("MAKEOVERRIDES", None) - for name in _MAKE_FLAG_ENV: - value = clean.get(name, "") - separator = re.search(r"(?:^|\s)--(?:\s|$)", value) - flags = value[: separator.start()].strip() if separator else value.strip() - if flags: - clean[name] = flags - else: - clean.pop(name, None) - for name in assignment_names(make_arguments): - clean.pop(name, None) - return clean - - -def route( - component: str, - make_program: str, - default_target: str, - local_targets: set[str], -) -> NoReturn: - """Recover argv and exec the component's selected recursive Make target.""" - - make_arguments = find_make_arguments(component) - target, payload = select_route( - make_arguments, component, default_target, local_targets - ) - environment = scrub_make_environment(dict(os.environ), make_arguments) - environment[PAYLOAD_ENV] = encode_arguments(payload) - environment[ARG_COUNT_ENV] = str(len(payload)) - os.execvpe( - make_program, - [make_program, "--no-print-directory", "-C", component, target], - environment, - ) - - -def execute(marker: str, command: list[str]) -> NoReturn: - """Append recovered arguments to *command* and exec it without a shell.""" - - if not command: - raise ArgumentRecoveryError("exec requires a command prefix") - - environment = dict(os.environ) - encoded = environment.pop(PAYLOAD_ENV, None) - environment.pop(ARG_COUNT_ENV, None) - if encoded is None: - make_arguments = find_make_arguments(marker) - arguments = arguments_after_marker(make_arguments, marker) - environment = scrub_make_environment(environment, make_arguments) - else: - arguments = decode_arguments(encoded) - environment = scrub_make_environment(environment, ["make"]) - - os.execvpe(command[0], [*command, *arguments], environment) - - -def usage() -> str: - return ( - "usage:\n" - " make-argv.py route COMPONENT MAKE_PROGRAM DEFAULT_TARGET [LOCAL_TARGET ...]\n" - " make-argv.py exec MARKER COMMAND [COMMAND_ARG ...]" - ) - - -def main(arguments: list[str] | None = None) -> int: - arguments = sys.argv[1:] if arguments is None else arguments - try: - if arguments[:1] == ["route"] and len(arguments) >= 4: - route(arguments[1], arguments[2], arguments[3], set(arguments[4:])) - elif arguments[:1] == ["exec"] and len(arguments) >= 3: - execute(arguments[1], arguments[2:]) - else: - raise ArgumentRecoveryError(usage()) - except ArgumentRecoveryError as error: - print(f"make-argv: {error}", file=sys.stderr) - return 2 - except OSError as error: - program = error.filename or "command" - detail = error.strerror or str(error) - print(f"make-argv: cannot execute {program}: {detail}", file=sys.stderr) - return 127 if error.errno == errno.ENOENT else 126 - return 0 - - -if __name__ == "__main__": - raise SystemExit(main()) diff --git a/scripts/test-make-argv.py b/scripts/test-make-argv.py deleted file mode 100644 index c8e6f05..0000000 --- a/scripts/test-make-argv.py +++ /dev/null @@ -1,312 +0,0 @@ -#!/usr/bin/env python3 -"""Tests for exact argument forwarding through GNU Make.""" - -import importlib.util -import io -import json -from pathlib import Path -import shutil -import subprocess -import sys -import tempfile -import unittest -from unittest import mock - - -SPEC = importlib.util.spec_from_file_location( - "make_argv", Path(__file__).with_name("make-argv.py") -) -assert SPEC is not None and SPEC.loader is not None -MAKE_ARGV = importlib.util.module_from_spec(SPEC) -SPEC.loader.exec_module(MAKE_ARGV) - - -class ArgumentEncodingTests(unittest.TestCase): - def test_round_trip_preserves_exact_arguments(self): - arguments = [ - "--key=one", - "two words", - "", - "--key=one", - "$HOME", - "--", - "--key=two", - ] - - self.assertEqual( - MAKE_ARGV.decode_arguments(MAKE_ARGV.encode_arguments(arguments)), - arguments, - ) - - def test_rejects_invalid_payload(self): - with self.assertRaisesRegex( - MAKE_ARGV.ArgumentRecoveryError, "invalid application argument payload" - ): - MAKE_ARGV.decode_arguments("not-base64!") - - @mock.patch.object( - MAKE_ARGV, "execute", side_effect=FileNotFoundError(2, "missing", "tool") - ) - def test_missing_application_has_a_concise_error(self, _execute): - errors = io.StringIO() - - with mock.patch("sys.stderr", errors): - status = MAKE_ARGV.main(["exec", "run", "tool"]) - - self.assertEqual(status, 127) - self.assertEqual(errors.getvalue(), "make-argv: cannot execute tool: missing\n") - - -class RouteSelectionTests(unittest.TestCase): - def test_delimiter_makes_test_an_application_argument(self): - target, arguments = MAKE_ARGV.select_route( - ["make", "firmware", "--", "test"], - "firmware", - "run", - {"test", "clippy"}, - ) - - self.assertEqual(target, "run") - self.assertEqual(arguments, ["test"]) - - def test_no_delimiter_selects_a_known_local_target(self): - target, arguments = MAKE_ARGV.select_route( - ["make", "firmware", "test"], - "firmware", - "run", - {"test", "clippy"}, - ) - - self.assertEqual(target, "test") - self.assertEqual(arguments, []) - - def test_configurable_no_argument_default(self): - target, arguments = MAKE_ARGV.select_route( - ["make", "docs"], "docs", "check", {"help"} - ) - - self.assertEqual(target, "check") - self.assertEqual(arguments, []) - - def test_explicit_docs_arguments_select_run_not_no_argument_default(self): - target, arguments = MAKE_ARGV.select_route( - ["make", "docs", "--", "--version"], "docs", "check", {"help"} - ) - - self.assertEqual(target, "run") - self.assertEqual(arguments, ["--version"]) - - def test_unknown_words_without_delimiter_remain_application_arguments(self): - target, arguments = MAKE_ARGV.select_route( - ["make", "firmware/tools/sitl", "move", "5", "two words"], - "firmware/tools/sitl", - "run", - {"help"}, - ) - - self.assertEqual(target, "run") - self.assertEqual(arguments, ["move", "5", "two words"]) - - def test_local_flash_keeps_every_argument_after_delimiter(self): - target, arguments = MAKE_ARGV.select_route( - [ - "make", - "firmware/boards/example", - "flash", - "--", - "--device=0483:df11", - "", - "--", - "$HOME", - ], - "firmware/boards/example", - "run", - {"flash", "help"}, - ) - - self.assertEqual(target, "flash") - self.assertEqual(arguments, ["--device=0483:df11", "", "--", "$HOME"]) - - -class EnvironmentTests(unittest.TestCase): - def test_scrubs_make_flags_and_command_line_assignments(self): - environment = { - "PATH": "/bin", - "MAKEFLAGS": "-- CARGO=wrong", - "MAKEOVERRIDES": "CARGO=wrong", - "MFLAGS": "--", - "CARGO": "wrong", - "OTHER": "keep", - } - - clean = MAKE_ARGV.scrub_make_environment( - environment, - ["make", "firmware", "--", "CARGO=wrong", "--key=value"], - ) - - self.assertEqual(clean, {"PATH": "/bin", "OTHER": "keep"}) - - def test_preserves_make_execution_flags_without_overrides(self): - clean = MAKE_ARGV.scrub_make_environment( - { - "MAKEFLAGS": "n --no-print-directory -- --key=value", - "MFLAGS": "-n -- --key=value", - "MAKEOVERRIDES": "--key=value", - }, - ["make", "firmware", "--", "--key=value"], - ) - - self.assertEqual( - clean, - {"MAKEFLAGS": "n --no-print-directory", "MFLAGS": "-n"}, - ) - - @mock.patch.object(MAKE_ARGV.os, "execvpe") - @mock.patch.object(MAKE_ARGV, "find_make_arguments") - def test_route_execs_recursive_make_with_encoded_payload( - self, find_make_arguments, execvpe - ): - payload = ["--key=one", "two words", "", "--", "--key=one"] - find_make_arguments.return_value = [ - "make", - "firmware/tools/sitl", - "--", - *payload, - ] - - with mock.patch.dict( - MAKE_ARGV.os.environ, - {"PATH": "/bin", "MAKEFLAGS": "n -- --key=one"}, - clear=True, - ): - MAKE_ARGV.route("firmware/tools/sitl", "make", "run", {"help"}) - - program, arguments, environment = execvpe.call_args.args - self.assertEqual(program, "make") - self.assertEqual( - arguments, - [ - "make", - "--no-print-directory", - "-C", - "firmware/tools/sitl", - "run", - ], - ) - self.assertEqual( - MAKE_ARGV.decode_arguments(environment[MAKE_ARGV.PAYLOAD_ENV]), payload - ) - self.assertEqual(environment[MAKE_ARGV.ARG_COUNT_ENV], str(len(payload))) - self.assertEqual(environment["MAKEFLAGS"], "n") - - @mock.patch.object(MAKE_ARGV.os, "execvpe") - def test_exec_uses_routed_payload_without_shell_joining(self, execvpe): - payload = ["--key=one", "two words", "", "$HOME", "--", "--key=one"] - environment = { - MAKE_ARGV.PAYLOAD_ENV: MAKE_ARGV.encode_arguments(payload), - MAKE_ARGV.ARG_COUNT_ENV: str(len(payload)), - "PATH": "/bin", - "MAKEFLAGS": "-- --key=one", - } - - with mock.patch.dict(MAKE_ARGV.os.environ, environment, clear=True): - MAKE_ARGV.execute("run", ["example-app", "fixed argument"]) - - program, arguments, child_environment = execvpe.call_args.args - self.assertEqual(program, "example-app") - self.assertEqual(arguments, ["example-app", "fixed argument", *payload]) - self.assertEqual(child_environment, {"PATH": "/bin"}) - - @mock.patch.object(MAKE_ARGV.os, "execvpe") - @mock.patch.object(MAKE_ARGV, "find_make_arguments") - def test_direct_local_make_exec_recovers_arguments( - self, find_make_arguments, execvpe - ): - payload = ["--key=value", "two words", "", "--", "$HOME"] - find_make_arguments.return_value = ["make", "run", "--", *payload] - - with mock.patch.dict(MAKE_ARGV.os.environ, {"PATH": "/bin"}, clear=True): - MAKE_ARGV.execute("run", ["example-app"]) - - self.assertEqual(execvpe.call_args.args[1], ["example-app", *payload]) - - -class ProcfsTests(unittest.TestCase): - def test_procfs_preserves_a_final_empty_argument(self): - with tempfile.TemporaryDirectory() as directory: - process_directory = Path(directory, "123") - process_directory.mkdir() - Path(process_directory, "cmdline").write_bytes(b"make\0run\0\0") - - self.assertEqual( - MAKE_ARGV.read_process_arguments(123, Path(directory)), - ["make", "run", ""], - ) - - def test_procfs_failure_is_actionable(self): - with tempfile.TemporaryDirectory() as directory: - with self.assertRaisesRegex( - MAKE_ARGV.ArgumentRecoveryError, "requires Linux /proc" - ): - MAKE_ARGV.read_process_arguments(123, Path(directory)) - - -@unittest.skipUnless(Path("/proc/self/cmdline").is_file(), "requires Linux procfs") -class MakeIntegrationTests(unittest.TestCase): - def test_recursive_make_preserves_exact_application_argv(self): - make = shutil.which("make") - if make is None: - self.skipTest("GNU Make is unavailable") - - helper = Path(__file__).with_name("make-argv.py").resolve() - with tempfile.TemporaryDirectory() as directory: - root = Path(directory) - component = root / "component" - component.mkdir() - output = root / "arguments.json" - application = root / "record-arguments.py" - application.write_text( - "import json, pathlib, sys\n" - "pathlib.Path(sys.argv[1]).write_text(json.dumps(sys.argv[2:]))\n", - encoding="utf-8", - ) - (root / "Makefile").write_text( - ".PHONY: component\n" - "component:\n" - f"\t+@exec {sys.executable} {helper} route component make run help\n" - ".DEFAULT:\n" - "\t@:\n", - encoding="utf-8", - ) - (component / "Makefile").write_text( - ".PHONY: run\n" - "run:\n" - f"\t@exec {sys.executable} {helper} exec run " - f"{sys.executable} {application} {output}\n" - ".DEFAULT:\n" - "\t@:\n", - encoding="utf-8", - ) - payload = [ - "--key=one", - "two words", - "", - "--key=one", - "$HOME", - "--", - "--key=two", - ] - - subprocess.run( - [make, "component", "--", *payload], - cwd=root, - check=True, - capture_output=True, - text=True, - ) - - self.assertEqual(json.loads(output.read_text(encoding="utf-8")), payload) - - -if __name__ == "__main__": - unittest.main()