From 2a910c5737fa1986311e46224735e6caee535a9f Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Sat, 5 Sep 2026 16:23:05 +0800 Subject: [PATCH 1/6] Emit verify profiles from the recipe's variables The frama-c MCP server can run the proofs make verify runs, but only if it loads the same program. Every field that decides that (sources, functions, memory model, machdep, include paths, force-includes, defines, provers, timeout) had to be restated by hand on the server side, and a hand-written function set is the drift a proof gate cannot afford: it produces a confident answer about a program the build system does not prove. print-verify-profiles emits that JSON from the variables the verify- recipe consumes, so the two cannot disagree. The include directories and force-includes move into FRAMAC_INCLUDE_DIRS and FRAMAC_FORCE_INCLUDES, named once and turned into -I and -include flags by FRAMAC_CPP_ARGS, because spelling either list twice is the drift this arrangement exists to prevent. They were duplicated at first, under a comment claiming they could not. FRAMAC_ISYSTEM_DIRS is used unquoted rather than through patsubst. Its value carries a shell substitution containing a space, so a patsubst over it splits mid-command and emits "-isystem $(frama-c -isystem -print-share-path)/libc". That mangling still proves green on any target whose sources need no libc, which is most of them. nostdinc and the isystem path are emitted rather than omitted. Without them the real macOS headers win over Frama-C's modeled libc and some files parse as a different program: src/syscall/sys.c is one, whose rusage _Static_assert only holds against the modeled header. BUILD_FLAVOR_GOALS also skips print-% goals. check-proof-targets.py shells out to make print-verify-targets on every make check, and a sub-make evaluates the build-flavor guard while it reads the makefiles. Without the skip, running that scanner beside a sanitizer build wipes the build's objects from under it. --- .claude/skills/elfuse-verify/SKILL.md | 352 +++++++++++++++++++++++++- mk/common.mk | 9 +- mk/verify.mk | 71 +++++- scripts/emit-verify-profiles.py | 196 ++++++++++++++ 4 files changed, 618 insertions(+), 10 deletions(-) create mode 100755 scripts/emit-verify-profiles.py diff --git a/.claude/skills/elfuse-verify/SKILL.md b/.claude/skills/elfuse-verify/SKILL.md index 05a826d1..06deae67 100644 --- a/.claude/skills/elfuse-verify/SKILL.md +++ b/.claude/skills/elfuse-verify/SKILL.md @@ -1,6 +1,6 @@ --- name: elfuse-verify -description: How elfuse validates a change - choosing the lanes for the area you touched, the test matrix, make check, and the Frama-C proof targets declared in mk/verify.mk, including how to drive the frama-c MCP server on a stuck proof. Use when adding bounds math to src/proved/, writing or repairing ACSL contracts, running or debugging make verify / verify-mutants, touching frama-c-stubs/, adding a test lane, or deciding what to run before calling work done. +description: How elfuse validates a change - choosing the lanes for the area you touched, the test matrix, make check, and the Frama-C proof targets declared in mk/verify.mk, including how to drive the frama-c MCP server on a stuck proof and how to read its proof_coverage report. Use when adding bounds math to src/proved/, writing or repairing ACSL contracts, running or debugging make verify / verify-mutants, asking how much of a target is actually proved, touching frama-c-stubs/, adding a test lane, or deciding what to run before calling work done. --- # Validating an elfuse change @@ -8,6 +8,36 @@ description: How elfuse validates a change - choosing the lanes for the area you Two independent gates: the runtime tests and the proofs. A change to attacker-facing bounds math needs both. +Independent in what they prove, not in what they consume. Run them one after +the other, never concurrently. `make verify` re-invokes itself parallel and +`verify-mutants` fans out too, while the runtime lanes are wall-clock +sensitive, so overlapping them makes the machine fail tests that a serial run +passes. Measured here: `make check` alongside the proof gate drove an 8-core +host to a load average of 43.8 against a busy threshold of 4.8, and +`test-thread-churn` timed out twice at 60 s and reported FAIL. The same binary +on the same tree at load 4.0 finishes in 0.34 s, three runs out of three. +Nothing was wrong with it. Neither mitigation saves you at that load, since +`test_host_is_busy` only skips the throughput guardrail and the runner only +re-runs once. A timing FAIL is worth nothing as evidence either way: it is not +a regression you can act on, and a serial re-run is the only thing that tells +you whether it was real. + +The pure source scanners are the exception, and they are the cheap early +signal while something long is in flight: `check-lock-order`, +`check-eintr-contract`, `check-atomics`, `check-proof-targets`, +`check-stub-shadow` and `check-syscall-coverage` read the tree, cost seconds, +and fail long before a full lane would. Five of the six are on `make check`; +`check-stub-shadow` is a prerequisite of every `verify-*` target instead, so it +is not reached by `make check` alone. Running one directly with +`python3 scripts/.py` costs nothing and needs no arguments. + +Five of the six write nothing. `check-proof-targets` is the one that does: +it shells out to `make print-verify-targets` rather than reading +`mk/verify.mk`, and a sub-make evaluates the build-flavor guard while it reads +the makefiles. `print-%` goals are skipped by that guard for exactly this +reason (`mk/common.mk`), so the scanner is safe to run beside a build; if you +add a scanner that invokes make on some other goal, it is not. + ## Choosing what to run `docs/testing.md`, section "Validation Strategy By Change Type", is a table @@ -40,6 +70,18 @@ Modes and what a failure in each means: Rosetta fixtures on first run. musl is Alpine's only libc, so glibc-dynamic lanes skip unless `GUEST_GLIBC_*` points at an external sysroot. +A fixture download that fails is not always a download failure. Some networks +answer plain HTTP with a page of their own, which arrives as a valid 200 and +only breaks at whatever tries to parse it: `make check` here failed at +`ar: Inappropriate file type or format` on a busybox `.deb` that was 2997 bytes +of HTML. The suite already knows this happens, which is what the `wget` lane's +"no unintercepted http to example.com from this host" skip is about. So when a +fixture step fails on a malformed archive, check what actually arrived before +believing the archive is at fault, and prefer an HTTPS source: `build/busybox` +now rewrites the mirror the Debian page lists to `deb.debian.org`, since the +per-country mirrors it offers are plain HTTP and not all of them answer HTTPS +at all. + ### Writing a test lane The runner is already hardened, and every one of these exists because a test @@ -130,6 +172,51 @@ Supporting gates, all of which run per target: links, so a wrong constant cannot fail a build, it silently changes what the proof reasons about. +### Choosing the next target + +Parsability decides it before anything else does: a file Frama-C cannot parse +cannot be proved, however good a candidate it looks. Test that first, because +it costs one invocation and rules candidates out for free. + +``` +FC=$(command -v frama-c) +ARGS="-nostdinc -isystem $($FC -print-share-path)/libc -Iframa-c-stubs \ + -include prelude.h -include macos-libc.h -Isrc -Ibuild" +$FC -machdep gcc_x86_64 -cpp-extra-args="$ARGS" +``` + +`CPP_DEFS` is empty for every target but `verify-gva`, so leaving it out +matches what most targets are proved under. A failure names its own cause: +`'sys/attr.h' file not found` is the real modeling gap and ends the matter, +while `Cannot resolve variable X` is a missing declaration and is fixable +under `frama-c-stubs/`. + +`parse_surface` does the same probe over a whole file list and groups the +failures by cause, which is the faster way to survey the tree. Give it the +flags above as `include_paths`, `isystem_paths`, `nostdinc` and +`force_includes`: a survey run without them measures a different program and +its blocked set fills with files that parse perfectly well. Measured with the +flags missing it reported 39 of 60 parsing against 46 of 60 true, and its +largest blocker group was a phantom. + +Whatever the probe, read which header stopped a file and whose include it was. +A leaked include costs every file downstream of it and nothing to remove: +deleting one unused `sys/mount.h` from `runtime/procemu.h` took three files +straight into the parsing set. + +Then rank what survives by whether it actually holds attacker-facing bounds +math. The shape that has worked every time is a self-contained codec or walk +over a guest-chosen blob: pure arithmetic, libc-only includes, an explicit +output-buffer bound, and no syscalls. A file whose header comment already says +it treats its input as untrusted and is free of project dependencies is +telling you it was written to be proved. + +Two things that look like candidates and are not. A file whose length +arithmetic is all delegated to an already-proved header adds nothing but a +second harness. And a translation table with no arithmetic, however +attacker-reachable, has no obligations worth generating: `-wp-rte` on it +proves that a switch is a switch. + ### Memory models, and what no model checks Each target picks its own model via `VERIFY__MODEL` in `mk/verify.mk`, @@ -165,21 +252,254 @@ rewriting a contract on suspicion. Retrying the unproved goals distinguishes that only needed a longer timeout. `create_sandbox` is the honest way to try a strengthening without touching the real source. +Read the `self_check` result rather than the absence of an error: a degraded +server still answers, and the answer looks like a normal response. +`frama_c.status: ok` says only that the binary runs. The fields that decide +whether the interactive path works at all are `socket_spawn`, and +`wp.available` / `eva.available` under `capabilities`. + +Do not read a failed `socket_spawn` as a missing `ast_utils` plugin without +checking. Its probes are time-bounded, so on a loaded host they time out and +report `error` or `unknown` for a plugin that is installed and works. Seen +here at load 75 on 8 cores: `socket_spawn` reported "the probe process exited +or never created one" and `ast_utils` came back `unknown`, while +`frama-c -load-module ast_utils_plugin -print-libc` succeeded immediately and +the plugin sat in Frama-C's plugin directory the whole time. `opam_switch_hint` +timing out in the same report is the tell. Confirm with that one-line load +before concluding anything, and re-run `self_check` on a quiet machine; only +if the plugin is genuinely absent is the install +`cd ast-utils && dune install` in the frama-c-mcp checkout. + +`reload_project` does not take a raw preprocessor string. It takes structured +flags, and an unknown key is accepted and dropped rather than refused, so a +call carrying `cpp_extra_args` parses with none of them and then fails on a +header that is on the real include path. Mirror `FRAMAC_CPP_ARGS` field by +field instead; for this tree that is + +``` +include_paths: ["frama-c-stubs", "src", "build"] +force_includes: ["prelude.h", "macos-libc.h"] +machdep: "gcc_x86_64" +``` + +Those three lines are `FRAMAC_INCLUDE_DIRS`, `FRAMAC_FORCE_INCLUDES` and +`FRAMAC_DATA_MODEL` from `mk/verify.mk`, and they are reproduced here only to +show the shape; take the live values from `make print-verify-profiles` below +rather than from this block, which nothing gates. + +`nostdinc` and `isystem_paths` are fields, and they are not optional detail on +this platform: without them the real macOS headers win over the modeled libc, +and a file whose parse depends on that shadowing loads as a different program. +Two measurements from when they could not be expressed, both worth knowing +because they are what a load under the wrong headers looks like. +`src/syscall/sys.c` parsed under the `mk/verify.mk` flags and failed without +them, on a `_Static_assert` over `struct rusage` that only holds against the +modeled header, which put it and six others in `parse_surface`'s blocked set: +39 of 60 reported against 46 of 60 true. + +The flags are not the only way the two can differ, and the other way cost me a +wrong diagnosis. On `src/syscall/net.c` the server reported `recv_at`'s +`pointer_alignment` obligation unproved, surviving `retry_unproved` at double +the budget, which is its own strongest test for a goal that is unprovable +rather than slow. Under `mk/verify.mk` the same three functions discharge 6 of +6 and that obligation is never generated. I recorded that here as a header +artifact; it was not. The cause was RTE: the kernel's generator and WP's own +are different analyses, the kernel emits `pointer_alignment` assertions and +WP's does not, and the server was starting Frama-C with `-rte` where the recipe +passes `-wp-rte`. Fixed upstream, but the shape is worth keeping: a +`pointer_alignment` goal the build never generates is the signature of the +wrong RTE generator, not of a hard proof. + +So the rule is not "distrust the server", it is "pass the flags". A profile +from `make print-verify-profiles` carries both, and `nostdinc` must be stated +for a profile to be proof evidence at all. When you load by hand instead, pass +`nostdinc` and `isystem_paths` yourself, or you are measuring another program. + Two rules about what any of that proves: - The MCP's default WP model is not what every target uses. A goal that discharges under defaults says nothing about whether `make verify-` passes. Always mirror the target's own `VERIFY__MODEL`. +- A prover budget is wall-clock, so on a saturated machine a goal can reach it + whatever its difficulty. Read `wp_timeout_triage` before believing a timeout + verdict: it carries `host_load_per_cpu` in its evidence and drops to + `confidence: low` above one runnable thread per CPU, and again when the + reading is `"unavailable"`, since an unread host is not a quiet one. Only a + measured quiet host earns `confidence: high`. +- Re-running is not re-measuring, and this is the trap. WP's cache defaults to + `Update`, so it stores timeout verdicts too and replays them. Measured here: + the same six functions, run under load (one-minute average 40 to 61 on 8 + cores) and again at load 3.3, produced the identical `proof_receipt` sha256, + with every timeout goal carrying `from_cache: true`. The second run proved + nothing and looked exactly like the first. + + The response says so now. `measurement` reports `replayed`, `unproved` and + `unproved_replayed`, and `every_unproved_goal_was_replayed` is the one to + read: when it is true the run attempted none of its own failures, and + `wp_timeout_triage` drops to `confidence: low` saying so. Pass + `cache: "None"` to prove everything in the run. It is the same distinction + `proof_coverage` draws between `fresh_valid` and `cached_valid`, and it + costs a re-prove, so spend it when a verdict is about to become a decision. +- `retry_unproved` settles slow against unprovable, and nothing else. It + re-runs the timed-out goals at double the budget and reports which flip, so + an empty `flipped` means more time is not the fix. It does not check that the + program under it is the one you meant: on `src/syscall/net.c` a goal survived + it and was still an artifact of the wrong header environment. Rule out the + load, the cache, and the flags before reading it as a property of the code. +- The connected server is whatever binary is installed, which can lag the + source tree. A behavior described here that the running server does not show + means the installed binary predates it, not that the description is wrong; + `self_check` reports the server version. - The MCP is an accelerator, never the gate. A change lands on `make verify` plus `make verify-mutants`, run from the Makefile, because that is what CI runs and what a contributor without the server can reproduce. Never report a proof as done on MCP evidence alone, and never add a workflow step, script, or CI job that depends on the server being connected. -It also answers the coverage question rather than just the green/red one: -asking for goal counts shows how much of the property table has a verdict, +It also answers the coverage question rather than just the green/red one, which is how you find a target that passes because it is proving less than you -thought. +thought. `proof_coverage` is the tool for that: + +``` +# denominator: every defined function of the loaded project +proof_coverage {} + +# denominator: the function set that target declares +proof_coverage {verify_profile: "", detail: "full"} +``` + +It measures stored conclusions, not the last run, so it reports nothing until +`store_function_conclusion` has filed a receipt from a `run_wp` on the real +project. With nothing loaded and nothing stored it answers `0 of 0`, +`incomplete`, and an empty function list rather than an error, which is easy to +skim as a clean report. Check the denominator before reading the percent. + +Sandbox receipts are refused on purpose: a sandbox proves an extracted copy +whose uncontracted callees are stubs. Merge the annotations back, re-run WP on +the main project, and store that receipt. + +Read a row's `reason` as the instruction, and treat an empty one as the only +thing that counts. Three of them come up here more than the others: + +- `stale_source` after a single edit. A receipt hashes the whole loaded file + set, not the one file its function lives in, so touching any source reds the + entire report. Expect it; it is not a signal about the function you edited. +- `unverified_callee`, propagated through the call chain. Fix what + `blocking_callees` names first. +- `proved_under_a_goal_filter`, meaning the run passed `prop` and left the + unselected obligations unattempted. That is the "proving less than you + thought" case caught by name. + +One limit on the number, on top of the two rules above. It reads WP only, so +`complete` is a statement about proof obligations generated by the ACSL, RTE +and WP configuration that produced those receipts. A requirement no contract +states is not an uncovered row, it is absent from the denominator entirely, so +coverage cannot tell you the property table is complete. + +### Calibrate the server before trusting a number from it + +Run one already-green target through it and compare the obligation count with +what the matching `make verify-` reports. Use `iov`: three functions, one +header, and a known answer of 40 of 40. + +``` +make verify- # the answer, for name=iov +reload_project {verify_profiles: , + verify_profile: "iov"} +run_wp {verify_profile: "iov", cache: "None"} +``` + +The counts must match exactly. Every wrong conclusion this file records came +from skipping that check, and each was invisible without it: + +- The server refused 20 of the 21 targets outright with + `invalid WP model 'typed'`, comparing the name case-sensitively where + Frama-C does not care. A profile emitted faithfully from the recipe was + rejected by the tool whose whole purpose is to run that recipe's proof. +- With that fixed it answered 42 obligations to the recipe's 40, both extras + `pointer_alignment` on one function, because it started Frama-C with kernel + `-rte` where the recipe passes `-wp-rte`. Those are different analyses and + the larger one is not the target's. +- `caveat`, which one target is proved under, is accepted by Frama-C and named + nowhere in `-wp-h`, so a list built from that help text called it invalid. + +None of those announced themselves. Each produced a confident, well-formatted +answer about a program the build system does not prove, and `retry_unproved` +confirmed one of them. Two numbers side by side is the cheapest thing that +catches the whole class, and it costs one target. + +### Making the MCP prove what the Makefile proves + +`make print-verify-profiles` emits the `verify_profiles` JSON for all of +`mk/verify.mk`, one entry per target, carrying the sources, functions, model, +machdep, include paths, defines, provers, timeout and a `reproduce` command. +It comes from the same variables the `verify-` recipe consumes, so a +profile and a Makefile run cannot disagree about what a target proves. Emit +it, never hand-write it: a hand-written function set is the drift the whole +mechanism exists to prevent. + +That property is only as good as the sharing. The two lists the profile and the +recipe both need, include directories and force-includes, live in +`FRAMAC_INCLUDE_DIRS` and `FRAMAC_FORCE_INCLUDES`; `FRAMAC_CPP_ARGS` turns them +into `-I` and `-include` flags with `patsubst`, and the emitter passes them +through as the bare directories and headers the schema wants. Spelling either +list twice is the bug this arrangement exists to prevent, and it is not +hypothetical: they were duplicated at first, under a comment claiming they +could not drift. If you add an include path, add it there and check both sides +move: + +``` +make print-verify-profiles FRAMAC_INCLUDE_DIRS="... extra" | grep extra +make -n verify-align FRAMAC_INCLUDE_DIRS="... extra" | grep -- -Iextra +``` + +The emitter refuses rather than emitting a profile that cannot be used: no +sources, no functions, an empty or blank model, no provers, a non-positive +timeout, a `CPP_DEFS` token that is not a `-D`, or no targets at all. Each +names the make variable to look at. That matters because the server's own +refusal comes much later and names none of them: a profile missing one required +field is accepted for loading and then rejected by every `run_wp` and every +`store_function_conclusion` that names it, which reads as a broken target +rather than as an empty variable on the command line that produced it. + +That closes the loop between the two tools: + +``` +make print-verify-profiles # from the build system +reload_project {verify_profiles: , verify_profile: ""} +run_wp {verify_profile: ""} +store_function_conclusion {function, status: "verified", + proof_receipt_sha256, verify_profile: ""} +proof_coverage {verify_profile: "", detail: "full"} +``` + +The JSON goes in as the object or as its text: the `verify_profiles` parameter +is untyped, so a client that stringifies it is not making a mistake, and the +server decodes either. Naming the profile is what makes each step mean the +target rather than the server's defaults. A run that deviated from the profile +is refused as that target's evidence rather than quietly accepted, and a +conclusion stored without one records what was proved but not what it settles. + +Three things to know when feeding it in. The profile carries `nostdinc` and +`isystem_paths` alongside the include paths, all four from the same +`mk/verify.mk` variables the recipe uses, so the load the server makes is the +one the recipe makes. The model strings are the +Makefile's own spelling (`typed`, `caveat`, `Bytes`), which is the point: +normalizing them here would make the profile prove something the recipe does +not. And every profile carries `rte: true`, because every `verify-` +recipe passes `-wp-rte`: that flag decides which obligations exist at all, so a +load without it gives a strictly smaller set. The server treats it as part of +the load identity, so a non-RTE load is refused as that target's evidence +rather than quietly accepted, and a profile that omits it can load sources but +cannot be proof evidence. + +`rte: true` means WP's generator specifically, not Frama-C's kernel one. They +are different analyses over the same code and the kernel's is larger: it emits +`pointer_alignment` assertions WP's does not. The server used to start Frama-C +with kernel `-rte` here, which is how a profiled `iov` run answered 42 +obligations to the recipe's 40 with both extras unproved. Worth knowing because +the field cannot express the difference, so the only way to see it is the +calibration above. ### frama-c-stubs/ @@ -222,9 +542,29 @@ which have shipped before: - A lane that could not run is named along with the risk that leaves. It is never rounded up into the passing set. +- The exit status a gate reports is the one to quote, and it is not always the + one you are shown. A backgrounded `make check > log 2>&1; echo $?` reports + the status of the whole command line, so a trailing `echo` makes a failing + make look like a success: this happened three times in one session, twice + hiding a real non-zero make. Read the status from inside the command, or read + the log for `make: *** [target] Error N` and the suite's own `Results:` line. + A single green summary line proves nothing on its own either, since `make` + stops at the first failing step and the suites after it never print. - A count, a latency, or a coverage figure is recomputed before it is quoted, - including from this file. A number carried forward from a document reads as - measured and is not. + including from this file and from `CLAUDE.md`, whose counts drift because + nothing gates them. Measured in one session: 21 verify targets against its + 20, 32 file-scope locks against its 31, 17 files under `src/proved/` against + the 15 it lists. The gates print the live number, so take it from + `make print-verify-targets` and from what `check-lock-order` and + `check-proof-targets` report. A number carried forward from a document reads + as measured and is not. +- The `PROVED n of n` line is not in `build/verify-.log`, which carries + Frama-C's own `[wp] Proved goals: N / N` instead. It is check-wp-result.py's + console output, colorized unconditionally, with the escape sitting between + `PROVED` and the count. So a total summed from a `make verify` transcript + with a naive `grep -oE 'PROVED +[0-9]+ of [0-9]+'` silently matches nothing + and reports an empty sum rather than failing. Strip the escapes first + (`sed 's/\x1b\[[0-9;]*m//g'`), or total the logs on `Proved goals` instead. - A proof is done when `make verify` and `make verify-mutants` say so from the Makefile. MCP goals discharging is progress, not a verdict. - A failure blamed on the environment earns one reproduction attempt under the diff --git a/mk/common.mk b/mk/common.mk index 13c2f19b..c8070069 100644 --- a/mk/common.mk +++ b/mk/common.mk @@ -79,7 +79,14 @@ BUILD_FLAVOR_STAMP := $(BUILD_DIR)/.build-flavor # goal-less invocation is one of them: .DEFAULT_GOAL is help, while # MAKECMDGOALS stays empty, so filtering the skip list out of the goals and # testing what remains covers both that and a mixed "make help elfuse". -BUILD_FLAVOR_GOALS := $(filter-out clean distclean help,$(MAKECMDGOALS)) +# +# print-% is in the list because those goals only print variables, and because +# something other than a person invokes them: check-proof-targets.py shells out +# to "make print-verify-targets" and runs on every "make check". Without the +# skip, that sub-make evaluates the flavor guard with whatever CFLAGS its own +# environment produces, so running the scanner beside a sanitizer build wipes +# that build's objects from under it. +BUILD_FLAVOR_GOALS := $(filter-out clean distclean help print-%,$(MAKECMDGOALS)) ifneq ($(BUILD_FLAVOR_GOALS),) BUILD_FLAVOR_PREV := $(shell cat $(BUILD_FLAVOR_STAMP) 2>/dev/null) diff --git a/mk/verify.mk b/mk/verify.mk index 9d121021..cd29e8ea 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -1,7 +1,8 @@ # Frama-C WP proofs .PHONY: verify check-contracts verify-mutants check-char-signedness \ - check-stub-constants check-stub-shadow print-verify-targets + check-stub-constants check-stub-shadow print-verify-targets \ + print-verify-profiles # Frama-C proof of the ELF parsing core. ELF headers come from untrusted # binaries, so every offset and extent computed from them is discharged as a @@ -124,9 +125,48 @@ CPP_DEFS := # git ls-files 'src/*.c' and tally the exits. FRAMAC_STUB_DIR := frama-c-stubs +# Split out of FRAMAC_CPP_ARGS because print-verify-profiles has to state the +# same two lists in the schema's own shape (bare directories, bare headers) +# rather than as -I and -include flags. Written once here so the recipe and the +# emitted profile cannot name different include paths, which the MCP compares +# byte for byte as part of a receipt's load identity: a profile that declared a +# path the recipe does not pass would accept a proof run under a different +# header set as that target's evidence. +FRAMAC_INCLUDE_DIRS := $(FRAMAC_STUB_DIR) src $(BUILD_DIR) +FRAMAC_FORCE_INCLUDES := prelude.h macos-libc.h + +# Recursively expanded: $(FRAMAC) is resolved when the recipe or the emitter +# asks, not while this file is read, so a FRAMAC override still picks its own +# libc. Shared for the same reason as the two lists above: the modeled libc and +# the flag that lets it win are what decide which declarations a file is +# compiled against, so the recipe and the profile must name one environment. +# +# One directory, and used unquoted rather than through patsubst: the value +# carries a shell substitution containing a space, so a $(patsubst %,-isystem %) +# over it splits mid-command and emits +# "-isystem $(frama-c -isystem -print-share-path)/libc". That mangling still +# proves green on any target whose sources need no libc, which is most of them. +FRAMAC_ISYSTEM_DIRS = $$($(FRAMAC) -print-share-path)/libc + +# The per-target checks a verify- target runs beside Frama-C. A consumer +# of the emitted profiles runs the prover, not this recipe, so these do not +# happen there. Named in the profile so a verdict obtained elsewhere is not +# mistaken for this target's, which needs all of them. +# +# The first two are prerequisites rather than recipe lines, and they belong +# here for the same reason the recipe's three do, more so: they are what says +# the stub headers a profile-driven load reaches for declare what the SDK +# declares. A run that skipped them proved a different frama-c-stubs/. +FRAMAC_BUILD_GATES := scripts/check-stub-constants.py \ + scripts/check-stub-shadow.py \ + scripts/check-acsl-coverage.py \ + scripts/check-char-signedness.py \ + scripts/check-wp-result.py + FRAMAC_CPP_ARGS = -nostdinc \ - -isystem $$($(FRAMAC) -print-share-path)/libc \ - -I$(FRAMAC_STUB_DIR) -include prelude.h -include macos-libc.h -Isrc -I$(BUILD_DIR) \ + -isystem $(FRAMAC_ISYSTEM_DIRS) \ + $(patsubst %,-I%,$(FRAMAC_INCLUDE_DIRS)) \ + $(patsubst %,-include %,$(FRAMAC_FORCE_INCLUDES)) \ $(CPP_DEFS) # One proof per attacker-facing parser. Each is declared by a single @@ -438,6 +478,31 @@ VERIFY_RULES := $(addprefix verify-,$(VERIFY_TARGET_NAMES)) print-verify-targets: @printf '%s\n' $(VERIFY_TARGET_NAMES) +# The MCP refuses a named run whose load deviated from the target's profile, so +# this is what lets "proof_coverage {verify_profile: ...}" and a stored +# conclusion mean the same thing "make verify-" means. Emitted from these +# variables rather than written by hand so it cannot drift from the recipe: the +# fields below are the ones the shared recipe consumes. +# +# -nostdinc and the -isystem libc are emitted, not omitted. Without them the +# real macOS headers win over Frama-C's modeled libc and some files parse as a +# different program (src/syscall/sys.c is one: its rusage _Static_assert only +# holds against the modeled header), so a consumer that could not express them +# was loading something weaker than what make verify- proves. + +## Print the verify_profiles JSON that frama-c-mcp loads and proves under +print-verify-profiles: + @python3 scripts/emit-verify-profiles.py \ + --machdep '$(FRAMAC_DATA_MODEL)' \ + --provers '$(FRAMAC_PROVERS)' \ + --timeout '$(FRAMAC_TIMEOUT)' \ + --include-paths '$(FRAMAC_INCLUDE_DIRS)' \ + --force-includes '$(FRAMAC_FORCE_INCLUDES)' \ + --isystem-paths "$(FRAMAC_ISYSTEM_DIRS)" \ + --nostdinc \ + --build-gates '$(FRAMAC_BUILD_GATES)' \ + $(foreach t,$(VERIFY_TARGETS),--target '$(call lc,$(t))|$(VERIFY_$(t)_SRC)|$(VERIFY_$(t)_FCTS)|$(VERIFY_$(t)_MODEL)|$(VERIFY_$(t)_MIN_GOALS)|$(VERIFY_$(t)_CPP_DEFS)') + # One rule template, instantiated per target. The target-specific variables # below are exactly what the shared recipe consumes; NAME and TARGET differ only # because a mutation run overrides NAME to keep concurrent logs apart. diff --git a/scripts/emit-verify-profiles.py b/scripts/emit-verify-profiles.py new file mode 100755 index 00000000..4907b53d --- /dev/null +++ b/scripts/emit-verify-profiles.py @@ -0,0 +1,196 @@ +#!/usr/bin/env python3 +"""Emit the verify_profiles JSON that frama-c-mcp loads and proves under. + +The point of emitting it rather than writing it by hand is that it cannot then +drift from the command that decides. Every field here is the same make variable +the verify- recipe consumes, so a profile and a "make verify-" run +prove the same functions, over the same sources, under the same model. + +Make expands the per-target variables and passes them in; this only assembles +JSON, which make cannot quote correctly on its own. +""" + +import argparse +import json +import os +import shlex +import sys + + +def split_defines(raw, target): + """Strip the -D that make carries and the schema refuses. + + shlex rather than str.split so -DMSG="two words" survives as one define + instead of becoming two. A token that is not a -D is refused rather than + passed through: the schema takes defines only, and a -U or a -include + arriving here would be recorded as a macro named "-Ufoo". + """ + try: + toks = shlex.split(raw) + except ValueError as exc: + # shlex raises on an unbalanced quote. Uncaught it is a traceback out + # of a make recipe, which names this file's internals rather than the + # VERIFY__CPP_DEFS that produced it. + sys.exit(f"target {target!r}: cannot split CPP_DEFS {raw!r}: {exc}") + out = [] + for tok in toks: + if not tok.startswith("-D"): + sys.exit(f"target {target!r}: {tok!r} in CPP_DEFS is not a -D define") + out.append(tok[2:]) + return out + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--machdep", required=True) + ap.add_argument("--provers", required=True) + ap.add_argument("--timeout", required=True, type=int) + ap.add_argument("--include-paths", required=True) + ap.add_argument("--force-includes", required=True) + ap.add_argument("--isystem-paths", default="") + ap.add_argument( + "--build-gates", + default="", + help="checks the verify- recipe runs that a consumer of these " + "profiles does not", + ) + ap.add_argument( + "--nostdinc", + action="store_true", + help="the recipe drops the default system include directories", + ) + ap.add_argument( + "--target", + action="append", + default=[], + help="name|sources|functions|model|min_goals|cpp_defs", + ) + args = ap.parse_args() + + include_paths = args.include_paths.split() + force_includes = args.force_includes.split() + isystem_paths = args.isystem_paths.split() + build_gates = args.build_gates.split() + + # Refused rather than emitted empty, like the rest. -nostdinc with nowhere + # to find a libc is not a configuration any recipe means, and a profile + # claiming it would never match the load the recipe makes. + if args.nostdinc and not isystem_paths: + sys.exit("--nostdinc with no --isystem-paths; check FRAMAC_ISYSTEM_DIRS") + + # The emptiness test above cannot see the failure it was written for. + # FRAMAC_ISYSTEM_DIRS is a shell substitution with a literal "/libc" glued + # to it, so a frama-c that is missing or answers nothing yields the + # non-empty, nonexistent "/libc" and the profile is emitted with exit 0. + # Ask the filesystem instead, which is the only thing that distinguishes a + # resolved share path from a stub of one. + for path in isystem_paths: + if not os.path.isdir(path): + sys.exit( + f"--isystem-paths {path!r} is not a directory; check " + "FRAMAC_ISYSTEM_DIRS and whether $(FRAMAC) resolves" + ) + provers = args.provers.replace(",", " ").split() + + # Refused for the reason the per-target fields below are. A profile with a + # blank machdep, no provers, or a non-positive timeout still registers and + # still loads sources, and is then refused at every run_wp and every stored + # conclusion naming it, which reads as a broken target rather than as the + # empty variable on the command line that emitted it. machdep gets the same + # treatment as model and for the same reason: any value defaulted here + # would be one the recipe does not pass. + machdep = args.machdep.strip() + if not machdep: + sys.exit("no machdep; check FRAMAC_DATA_MODEL") + if not provers: + sys.exit("no provers; check FRAMAC_PROVERS") + if args.timeout <= 0: + sys.exit(f"timeout {args.timeout} is not positive; check FRAMAC_TIMEOUT") + + profiles = {} + for spec in args.target: + # Bounded so the last field absorbs any further separator. Defines are + # last precisely because a -D value may legitimately contain one, as + # -DFLAGS=(A|B) does; the fields before it cannot. + parts = spec.split("|", 5) + if len(parts) != 6: + sys.exit(f"malformed --target: {spec!r}") + name, sources, functions, model, min_goals, defines = parts + if not name: + sys.exit(f"--target with no name: {spec!r}") + + # Refused rather than emitted empty. The server needs both to check a + # run or a conclusion against this target, and a profile carrying + # neither would register a name that silently never matches. A target + # whose _FCTS or _SRC went missing in mk/verify.mk fails here instead. + source_list = sources.split() + function_list = functions.split() + if not source_list: + sys.exit(f"target {name!r} has no sources; check VERIFY_*_SRC") + if not function_list: + sys.exit(f"target {name!r} has no functions; check VERIFY_*_FCTS") + + # Not defaulted. Any spelling chosen here would be one the recipe does + # not pass, and the profile would then prove under a model the target + # does not use. + model_name = model.strip() + if not model_name: + sys.exit(f"target {name!r} has no model; check VERIFY_*_MODEL") + + # Refused rather than emitted absent: every target in mk/verify.mk + # carries one, so a missing value means the block was edited wrong, and + # a profile without it silently drops the check. + try: + floor = int(min_goals) + except ValueError: + sys.exit(f"target {name!r} has no min_goals; check VERIFY_*_MIN_GOALS") + if floor <= 0: + sys.exit( + f"target {name!r} has min_goals {floor}; a floor of zero checks nothing" + ) + + profiles[name] = { + "sources": source_list, + "functions": function_list, + # Stored stripped, matching the check above. The server compares + # the model string against the one the receipt records, so a + # trailing space in a VERIFY_*_MODEL assignment would make every + # run under this profile fail to be evidence about its own target. + "model": model_name, + "machdep": machdep, + "include_paths": include_paths, + "defines": split_defines(defines, name), + "force_includes": force_includes, + "isystem_paths": isystem_paths, + # The floor on obligations generated. "N of N discharged" is not + # evidence on its own: an emptied body or a dropped contract + # discharges 0 of 0, and this is the only check that catches it. + "min_goals": floor, + # Named, not exported: a consumer of these profiles runs Frama-C, + # not the recipe, so these checks do not happen there. + "build_gates": build_gates, + # Recorded because it decides which declarations a file is compiled + # against: without it the host's real headers shadow the modeled + # libc and the same source is a different program. + "nostdinc": args.nostdinc, + "provers": provers, + "timeout_seconds": args.timeout, + # Every verify- recipe passes -wp-rte. Recorded because it + # decides which obligations exist at all, so a run without it + # discharges a strictly smaller set than the target proves. + "rte": True, + "reproduce": f"make verify-{name}", + } + + # An empty set emits valid JSON that the server then refuses whole, naming + # neither this script nor the variable that came up empty. Fail where the + # cause is still visible. + if not profiles: + sys.exit("no targets; check VERIFY_TARGETS in mk/verify.mk") + + json.dump(profiles, sys.stdout, indent=2, sort_keys=True) + sys.stdout.write("\n") + + +if __name__ == "__main__": + main() From 83cedce53e5213748abf85aa6c1e6e7ddb675683 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Sat, 5 Sep 2026 21:50:46 +0800 Subject: [PATCH 2/6] Report the frames WP invents for missing bodies Frama-C words a missing spec two ways, and only one of them was being read. "Neither code nor explicit exits and terminates" leaves a hand-written assigns in force and completes the rest; "Neither code nor specification" generates the frame as well. The second is the stronger assumption and was the one the pattern did not match, so the "assumed (spec generated, body not analyzed)" line named the weaker case and hid the stronger one. log_impl arrives through that second wording. Every proof of a function that logs therefore rested on an invented assigns \nothing, and no report anywhere said so; verify-elf disclosed memcpy and pread while the frame it had actually assumed went unnamed. Across the 21 targets log_impl is the only name this surfaces. The other four already matched, so nothing that was reported stops being reported. --- scripts/check-wp-result.py | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/scripts/check-wp-result.py b/scripts/check-wp-result.py index 481dc383..70f74c0a 100644 --- a/scripts/check-wp-result.py +++ b/scripts/check-wp-result.py @@ -48,8 +48,15 @@ USER_ERROR = re.compile(r"^.*User Error: *") # A function WP took on faith: it generated a spec instead of analyzing a body. +# Frama-C words this two ways and the difference matters. "Neither code nor +# explicit exits and terminates" leaves a hand-written assigns in force; +# "Neither code nor specification" generates the frame too, which is the +# stronger assumption and was the one this pattern used to miss. log_impl came +# through that second wording, so every proof of a function that logs rested on +# an invented assigns \nothing that no report named. ASSUMED = re.compile( - r"Neither code nor explicit .* for function ([A-Za-z_][A-Za-z_0-9]*)," + r"Neither code nor (?:explicit|specification).* for function " + r"([A-Za-z_][A-Za-z_0-9]*)," ) # Printed verbatim under their respective banners. Kept as literal blocks From 521b64a6a5aac271bd5dfc78d7a893964ab1fdc4 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Sat, 5 Sep 2026 16:23:43 +0800 Subject: [PATCH 3/6] Contract the two proved functions that had none elf_place_segment and futex_uaddr_is_aligned sat in their targets' -wp-fct lists with no ACSL contract, so WP proved only that their bodies commit no runtime error. Nothing there can reject a broken source: widen an alignment mask or move a bounds comparison and every obligation still discharges. A proof that cannot reject a broken source proves nothing, and these two had been passing that way for a while. elf_place_segment now states the property its caller depends on: an accepted placement never overlaps the runtime infra reserve. That reserve holds the page-table pool, the shim code and the EL1-only shim data, so a segment the loader accepts on top of it is a guest-controlled write into elfuse's own control structures. No assigns clause, and that is the honest answer rather than an omission. The function logs on both rejection paths, log.c locks a mutex and writes stderr, and WP checks a frame against log_impl's generated spec, which is assigns \nothing. A frame stated here would discharge against that assumption and still be false, which serves a caller worse than no frame at all. It is also the only place the question arises: of the six contracted functions in elf.c only this one logs. Its \separated precondition discharges and is kept, because stating the non-aliasing beats leaving it implicit in the caveat model's assumptions. \valid on the two out-parameters is deliberately absent and that was measured, not assumed: with both stated, the matching obligations in elf_check_placement time out at the 30s budget on a host at 0.3 runnable threads per CPU with the WP cache defeated, so it is the model and not the machine. Caveat already assumes a formal pointer parameter is valid, which is why the body proves without them. futex_uaddr_is_aligned states its result in the bit domain rather than as uaddr % 4 == 0. The readable form does not discharge: bridging modulo and bitmask on a 64-bit value is what exhausts the prover, not the property. Both floors move with the obligations they generate: elf 156 to 159, futexdeadline 128 to 130. MIN_GOALS is a tripwire against an emptied body or a dropped contract, which prove 0 of 0, and it only means that while it sits at the target's baseline. --- mk/verify.mk | 4 ++-- src/core/elf.c | 30 +++++++++++++++++++++++++++++- src/runtime/futex.c | 14 ++++++++++++++ 3 files changed, 45 insertions(+), 3 deletions(-) diff --git a/mk/verify.mk b/mk/verify.mk index cd29e8ea..30f919ca 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -188,7 +188,7 @@ VERIFY_ELF_FCTS := elf_add_no_wrap elf_phdr_gpa_in_segment \ elf_place_segment elf_check_placement elf_record_load \ elf_read_interp \ $(VERIFY_UTILS_FCTS) -VERIFY_ELF_MIN_GOALS ?= 156 +VERIFY_ELF_MIN_GOALS ?= 159 VERIFY_ELF_MODEL := caveat # Includes utils.h and elf.h: elf.c includes both, and utils.h already carries @@ -320,7 +320,7 @@ VERIFY_FUTEXDEADLINE_FCTS := futex_remaining_ns futex_quantum_deadline \ linux_timespec_is_valid futex_uaddr_is_aligned \ timespec_valid timespec_valid_capped \ timespec_to_ns_sat timespec_to_poll_ms -VERIFY_FUTEXDEADLINE_MIN_GOALS ?= 128 +VERIFY_FUTEXDEADLINE_MIN_GOALS ?= 130 VERIFY_FUTEXDEADLINE_MODEL := typed VERIFY_FUTEXDEADLINE_SCAN := src/runtime/futex.c src/proved/timespec.h VERIFY_FUTEXDEADLINE_CLAIM := for ANY guest deadline and ANY cap the wait \ diff --git a/src/core/elf.c b/src/core/elf.c index 95160784..9ac44e27 100644 --- a/src/core/elf.c +++ b/src/core/elf.c @@ -680,7 +680,35 @@ bool elf_interp_is_loadable(const elf_info_t *info, const char *display_path) * Returns false, with the reason logged, when the window puts the segment * outside guest memory or on top of the runtime infra reserve. When infra_lo == * infra_hi the caller opted out (early bring-up before guest_t is wired up); - * the guest_size bound still applies. + * the guest_size bound still applies. An accepted placement never overlaps the + * runtime infra reserve. That is the property the caller depends on and the one + * worth stating: the reserve holds the page-table pool, the shim code and the + * EL1-only shim data, so a segment the loader accepts on top of it is a + * guest-controlled write into elfuse's own control structures. + * + * valid(gpa_out) and valid(zero_len_out) are deliberately absent, and that was + * measured rather than assumed. With both stated, the two matching call-site + * obligations in elf_check_placement time out at the 30s budget on a quiet host + * (0.3 runnable threads per CPU) with the WP cache defeated, so it is the + * caveat model and not the machine: caveat already assumes a formal pointer + * parameter is valid, which is why the body proves without them. separated is + * kept because it does discharge, and stating the non-aliasing in the contract + * beats leaving it implicit in the model choice. + * + * assigns is deliberately absent, and its absence is the honest answer rather + * than a gap. This function logs, and WP proves a frame against log_impl's + * generated spec (assigns \nothing) rather than against log.c, which locks a + * mutex and writes stderr. A frame stated here would therefore discharge and + * still be false, which is worse for a caller than no frame at all. Removing it + * costs 13 frame obligations and no ensures: the placement bounds above are + * what the caller actually depends on, and they prove either way. + */ +/*@ + requires \separated(gpa_out, zero_len_out); + ensures \result != 0 ==> *gpa_out + *zero_len_out <= guest_size; + ensures \result != 0 ==> !(infra_lo < infra_hi && + *gpa_out < infra_hi && + *gpa_out + *zero_len_out > infra_lo); */ static bool elf_place_segment(const elf_segment_t *seg, const char *display_path, diff --git a/src/runtime/futex.c b/src/runtime/futex.c index 5eb59b09..00aba18d 100644 --- a/src/runtime/futex.c +++ b/src/runtime/futex.c @@ -332,6 +332,20 @@ static inline unsigned futex_hash(uint64_t uaddr) return futex_bucket_index(uaddr, FUTEX_BUCKETS); } +/* Linux requires a futex word to be naturally aligned, and every op checks this + * before the address reaches a bucket. Stated as a contract because without one + * a widened or narrowed mask breaks no obligation: the proof would pass on a + * body it never constrained, and the mutation gate would have nothing to + * reject. + * + * The ensures is in the bit domain rather than the more readable "uaddr % 4 == + * 0" because the prover times out bridging modulo and bitmask on a 64-bit + * value. Measured at the 30s budget, and a fresh cache does not help. + */ +/*@ + assigns \nothing; + ensures \result <==> (uaddr & 0x3) == 0; + */ static inline bool futex_uaddr_is_aligned(uint64_t uaddr) { return (uaddr & 0x3) == 0; From 2f076628fd6fa83e880dd378fbb6e43c7c3118d3 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Sat, 5 Sep 2026 16:24:06 +0800 Subject: [PATCH 4/6] Make the mutation gate say what it actually proves Three things it could not do, and one it claimed that was not true. A function proved by two targets could only be mutated in the one whose VERIFY__SRC named its file. hex_nibble lives in src/utils.h and is proved by verify-elf and verify-rsp precisely because assuming it once was a past mistake, and neither could mutate it. The runner now stages a mutant header below its own directory and hands that directory to MUTANT_INCDIR, where it precedes src/ in the include search. What a target may mutate widens from its source to its source plus the headers in VERIFY__SCAN, which is already its declared input closure. The staged path mirrors the original's path under src/ and MUTANT_INCDIR is the staging root, not the copy's parent. Deriving it as the parent got src/utils.h right by luck and every nested header wrong: "proved/netlink.h" resolved to /proved/netlink.h, missed, fell through -Isrc to the real header, and the run proved unmutated code while reporting a mutation nobody caught. The unmutated baseline cannot catch that, though a comment here claimed it could. The baseline stages a copy identical to the file it shadows, so whether the preprocessor opens the shadow or falls through, the program proved is the same and the run passes either way. A probe staging a copy that carries #error does catch it, and it reads the log rather than make's stdout, since the recipe redirects Frama-C there and a non-zero exit alone is equally what a broken override gives. The probe runs serially, unlike everything else here. It answers a yes/no question from make's exit status, and that status is the one thing a concurrent sibling can spoil: alongside the baseline pool it reported "the target proved anyway" for a staged header whose first line is #error, while the identical invocation by hand exited non-zero with the probe named twice in its log. A control that can report the opposite of the truth is worse than no control. A mutation is scored caught when a goal comes back open, and open has two causes: the prover reached a conclusion the mutant cannot satisfy, or it ran out of budget. Only the first is refutation. Both are now reported apart, and both still count, because measurement says the first never happens here: across every mutation log the tag is [Timeout], never [Unknown] or [Failed], and raising the budget eightfold to 240s on a host at 0.3 to 0.6 runnable threads per CPU left all four futexdeadline mutations exhausting exactly as at 30s. Refusing to count exhaustion would not make the gate stricter, it would make caught unreachable. What separates a broken contract from a hard one is the baseline: it proves every goal, and each mutant exhausts on the one its own function owns. Mutation runs pass -wp-cache none. WP's cache defaults to update and stores a timeout as a verdict just like a conclusion, so a replayed timeout would be a catch with no prover run behind it. make verify keeps its cache, which is what makes a re-prove cheap. --- .claude/skills/elfuse-verify/SKILL.md | 90 ++++- docs/testing.md | 1 + mk/tests.mk | 15 +- mk/verify.mk | 51 ++- scripts/check-mutants.py | 464 +++++++++++++++++++++++--- 5 files changed, 568 insertions(+), 53 deletions(-) diff --git a/.claude/skills/elfuse-verify/SKILL.md b/.claude/skills/elfuse-verify/SKILL.md index 06deae67..0e1af83b 100644 --- a/.claude/skills/elfuse-verify/SKILL.md +++ b/.claude/skills/elfuse-verify/SKILL.md @@ -127,6 +127,91 @@ Apple's 3.81. `verify-mutants` accepts `MUTANT_TARGET=`, `MUTANT_JOBS=`, and `MUTANT_SINCE=` for a changed-only run. +Read past the "N mutations, N caught" line. It also prints the proved functions +that have no mutation yet, and that list, not the caught count, is the honest +measure of what the gate covers: all-caught alongside a handful of functions +nobody has tried to break says the gate is green and that those proofs have +never been asked whether they would reject a broken source. They are not +failures, and they are not covered either. + +Recompute that list before quoting it, and read what it counts. It counts +distinct functions now; it used to count `(target, function)` pairs, so a +function proved by two targets showed up twice and read as uncovered under its +second target even though the first mutates it. That inflated the gap fourfold +the last time it was checked - twelve listings, three functions. + +A function can also sit in a `_FCTS` list with no ACSL contract at all, proved +only for absence of runtime errors. Nothing there can reject a mutation, so +adding one is wasted effort until the function has a contract: that is the fix, +and it is usually two lines. Write the contract in the domain the code is in, +too. `futex_uaddr_is_aligned` would not discharge as `uaddr % 4 == 0` and does +as `(uaddr & 0x3) == 0`, because bridging modulo and bitmask on a 64-bit value +is what the prover times out on, not the property itself. + +Adding a contract raises the obligation count, so raise +`VERIFY__MIN_GOALS` with it. That floor is a tripwire against an emptied +body or a dropped contract, which prove 0 of 0 and would otherwise pass; it is +meant to sit at the target's baseline. Two contracts added here left it 15 and +2 obligations low, and nothing failed to say so, because a floor is only ever +compared against from below. + +Mutating a function that lives in an included header rather than in +`VERIFY__SRC` works: the runner stages the mutant in its own directory and +prepends it via `MUTANT_INCDIR`, where it shadows the real header. What a +target may mutate is its source plus the headers in its `VERIFY__SCAN`. + +The staged path must mirror the original's path under `src/`, and +`MUTANT_INCDIR` must be the staging ROOT rather than the copy's parent, because +the spelling in the `#include` is what the preprocessor searches for. Deriving +it as the parent got `src/utils.h` right by luck and every nested header wrong: +`"proved/netlink.h"` resolved to `/proved/netlink.h`, missed, fell +through `-Isrc` to the real header, and the run proved unmutated code while +reporting a mutation nobody caught. + +The unmutated baseline cannot catch that, and it is worth knowing why, because +the comment that claimed it could was wrong. The baseline stages a copy +identical to the file it shadows, so whether the preprocessor opens the shadow +or falls through, the program proved is the same and the run passes either way. +What does catch it is a probe: stage a copy carrying `#error`, require the run +to fail naming it, and read the LOG rather than make's stdout, since the recipe +redirects Frama-C there and a non-zero exit alone is also what a broken +override gives. It costs a parse, not a proof. + +### A mutation is caught by exhaustion here, not by refutation + +Worth knowing before tightening the gate on principle. An open goal means the +prover either reached a conclusion the mutant cannot satisfy (`[Unknown]`, +`[Failed]`) or ran out of budget (`[Timeout]`, `[Stepout]`), and only the first +is a refutation. In this tree the first never happens: across every mutation +log the tag is `[Timeout]`, and raising the budget eightfold to 240s on a host +at 0.3 to 0.6 runnable threads per CPU left all four `futexdeadline` mutations +exhausting exactly as they did at 30s. Alt-Ergo and Z3 do not refute these +goals, they grind. So refusing to count exhaustion does not make the gate +stricter, it makes "caught" unreachable and the gate permanently red. + +What separates a broken contract from a merely hard one is the baseline, not +the tag: the unmutated source proves every goal, and the mutant, narrowed to +the mutated function, exhausts on that function's own goal. A goal that were +only hard would exhaust in the baseline too, and a failing baseline is fatal +rather than scored. The residual gap is a mutation that turns an easy true goal +into a hard true one, which no verdict tag available here would catch either. + +Two things follow. Report the resource verdicts separately so the count never +reads as "these proofs refute their mutants". And do not diagnose them as load +without measuring: a mutation run fans out and becomes its own load source, so +a split computed during a parallel run will always disqualify itself. Serial +(`MUTANT_JOBS=1`) on a quiet host is the only measurement that means anything, +and here it returned the same answer. + +The mutation runs pass `-wp-cache none` for a related reason. WP's cache +defaults to `update` and stores a timeout as a stored verdict just like a +conclusion, so a replayed timeout would be a catch obtained with no prover run +at all. `make verify` keeps its cache, which is what makes a re-prove cheap; +only the mutation gate, where a fresh verdict is the whole point, turns it off. +That distinction is not academic: an `elf_place_segment` contract retried here +came back Timeout from the cache on a quiet host, and only defeating the cache +showed the real result. + `scripts/proof-scope.py` decides which targets a diff can reach, and `.github/workflows/verify.yml` builds its jobs from it, so a target the branch cannot affect gets no runner. It answers two questions: which targets to prove, @@ -182,7 +267,8 @@ it costs one invocation and rules candidates out for free. FC=$(command -v frama-c) ARGS="-nostdinc -isystem $($FC -print-share-path)/libc -Iframa-c-stubs \ -include prelude.h -include macos-libc.h -Isrc -Ibuild" -$FC -machdep gcc_x86_64 -cpp-extra-args="$ARGS" +FILE=src/syscall/fs-stat.c +$FC -machdep gcc_x86_64 -cpp-extra-args="$ARGS" "$FILE" ``` `CPP_DEFS` is empty for every target but `verify-gva`, so leaving it out @@ -327,7 +413,7 @@ Two rules about what any of that proves: reading is `"unavailable"`, since an unread host is not a quiet one. Only a measured quiet host earns `confidence: high`. - Re-running is not re-measuring, and this is the trap. WP's cache defaults to - `Update`, so it stores timeout verdicts too and replays them. Measured here: + `update`, so it stores timeout verdicts too and replays them. Measured here: the same six functions, run under load (one-minute average 40 to 61 on 8 cores) and again at load 3.3, produced the identical `proof_receipt` sha256, with every timeout goal carrying `from_cache: true`. The second run proved diff --git a/docs/testing.md b/docs/testing.md index ca91bee4..0e5ace4c 100644 --- a/docs/testing.md +++ b/docs/testing.md @@ -500,6 +500,7 @@ Suggested minimum validation: | Rosetta hosting, x86_64 dispatch, VZ ioctls, AOT cache | `make elfuse && make test-rosetta-all` | | Broad behavioral changes | `make elfuse && make check && make test-matrix` | | Debugger or ptrace flow | `make elfuse && make test-gdbstub` | +| ACSL contracts, `src/proved/`, `mk/verify.mk`, the mutation harness | `make verify && make verify-mutants`, in that order and never beside a runtime lane: both fan out, and the timing lanes fail under the load they create. Add `make check` only when the change touches code rather than annotations | ## OCI Image CLI diff --git a/mk/tests.mk b/mk/tests.mk index 12c2251d..7dceee39 100644 --- a/mk/tests.mk +++ b/mk/tests.mk @@ -7,7 +7,7 @@ # src/elfuse-limits.h. ELFUSE_HOST_NOFILE_MIN ?= $(shell bash "$(CURDIR)/tests/test-config.sh" --host-nofile) -.PHONY: test-hello test-all check check-syscall-coverage check-eintr-contract check-lock-order check-atomics check-ascii check-svc-tails check-skill-refs test-gdbstub test-coreutils test-busybox test-shim-futex-stats test-vcpu-watchdog \ +.PHONY: test-hello test-all check check-syscall-coverage check-eintr-contract check-lock-order check-atomics check-ascii check-svc-tails check-skill-refs check-proof-targets test-gdbstub test-coreutils test-busybox test-shim-futex-stats test-vcpu-watchdog \ test-static-bins \ test-dynamic test-dynamic-coreutils test-glibc-dynamic \ test-glibc-coreutils test-perf \ @@ -80,6 +80,17 @@ test-mremap-tail-emfile: $(ELFUSE_BIN) $(BUILD_DIR)/test-mremap-tail-emfile check-syscall-coverage: @python3 scripts/check-syscall-coverage.py +## Verify every src/proved/ header is proved by a target make actually generates +# +# Local as well as in CI. This was the one gate of the set that only ran in +# .github/workflows/lint.yml, so a header added under src/proved/ with no +# matching VERIFY__SRC block passed make check and failed the branch later. +# It asks make for the target list rather than reading mk/verify.mk, which is +# the whole point of it: a VERIFY__SRC written below the := that builds +# VERIFY_TARGETS parses fine and generates no rule. +check-proof-targets: + @python3 scripts/check-proof-targets.py + ## Verify every path that can report EINTR states whether it may be restarted check-eintr-contract: @python3 scripts/check-eintr-contract.py @@ -287,7 +298,7 @@ check-sanitizer: $(ELFUSE_BIN) $(TEST_DEPS) $(CHECK_HOST_UNIT_BINS) $(CHECK_SHARED_LANES) ## Run the unit test suite plus busybox applet validation -check: $(ELFUSE_BIN) $(TEST_DEPS) check-syscall-coverage check-eintr-contract check-lock-order check-atomics check-ascii check-svc-tails check-skill-refs test-config test-runner \ +check: $(ELFUSE_BIN) $(TEST_DEPS) check-syscall-coverage check-eintr-contract check-lock-order check-atomics check-ascii check-svc-tails check-skill-refs check-proof-targets test-config test-runner \ $(CHECK_HOST_UNIT_BINS) @bash tests/driver.sh -e $(ELFUSE_BIN) -d $(TEST_DIR) -v $(CHECK_SHARED_LANES) diff --git a/mk/verify.mk b/mk/verify.mk index 30f919ca..6effe5bd 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -163,9 +163,43 @@ FRAMAC_BUILD_GATES := scripts/check-stub-constants.py \ scripts/check-char-signedness.py \ scripts/check-wp-result.py -FRAMAC_CPP_ARGS = -nostdinc \ +# One spelling. The recipe puts it in FRAMAC_CPP_ARGS and the emitter passes it +# as a flag, so stating it twice is the drift the split above exists to prevent: +# drop it from one and a consumer proves against the real macOS headers while +# make verify- proves against the modeled libc. +FRAMAC_NOSTDINC := -nostdinc + +# A mutation of an INCLUDED header cannot travel through VERIFY__SRC, which +# names one file and is what the prover is pointed at. The mutation runner +# stages the broken header in its own directory and hands that directory over +# here, where it precedes src/ in the include search and therefore shadows the +# real one. +# +# Assigned, not ?=, so it is empty for every ordinary run and stays that way. A +# make command line still overrides it, which is the only caller there is; ?= +# would additionally let a stray environment variable of this name prepend an +# include directory to all 21 proof targets, silently proving a program nobody +# asked for. +# +# Both forms were measured, and they differ, which is the whole point: +# make -n verify-align MUTANT_INCDIR=/tmp/x puts -I/tmp/x first, as intended +# MUTANT_INCDIR=/tmp/x make -n verify-align injects nothing under := +# The second is the environment form. Under ?= it did inject; under := it does +# not, and the command line still wins. Read the second line as the fix +# working, not as evidence of a leak. +MUTANT_INCDIR := + +# WP's cache defaults to 'update', which stores a verdict and replays it. For +# make verify that is what makes a re-run cheap, and it is left alone. For the +# mutation gate it is wrong: a mutation is scored caught when a goal comes back +# open, WP records a TIMEOUT as a stored verdict just like a conclusion, and a +# replayed timeout is therefore a catch obtained with no prover run at all. The +# mutation runner sets this to none so every mutation verdict is measured. +WP_CACHE := + +FRAMAC_CPP_ARGS = $(FRAMAC_NOSTDINC) \ -isystem $(FRAMAC_ISYSTEM_DIRS) \ - $(patsubst %,-I%,$(FRAMAC_INCLUDE_DIRS)) \ + $(patsubst %,-I%,$(MUTANT_INCDIR) $(FRAMAC_INCLUDE_DIRS)) \ $(patsubst %,-include %,$(FRAMAC_FORCE_INCLUDES)) \ $(CPP_DEFS) @@ -312,9 +346,13 @@ their callers honor these preconditions stay test-covered # function left out of the set is an assumed axiom whether or not this target # calls it, and dropping timespec_to_poll_ms fails the gate by name. # -# The cost is that verify-mutants lists those four as unmutated under this -# target as well as under verify-timespec, where they are mutated. That is a -# second target proving the same functions, not lost coverage. +# Those four are proved here and mutated under verify-timespec. The coverage +# summary counts both ways for exactly this shape: they are covered by function, +# and they show in the per-target list as proved here without a mutation of +# their own. That second list is not a gap to close by reflex. A mutation under +# one target says nothing about another that proves the same function under a +# different model, so it is worth adding only where the two environments differ +# enough to matter. VERIFY_FUTEXDEADLINE_SRC := src/runtime/futex.c VERIFY_FUTEXDEADLINE_FCTS := futex_remaining_ns futex_quantum_deadline \ linux_timespec_is_valid futex_uaddr_is_aligned \ @@ -499,7 +537,7 @@ print-verify-profiles: --include-paths '$(FRAMAC_INCLUDE_DIRS)' \ --force-includes '$(FRAMAC_FORCE_INCLUDES)' \ --isystem-paths "$(FRAMAC_ISYSTEM_DIRS)" \ - --nostdinc \ + $(if $(FRAMAC_NOSTDINC),--nostdinc,) \ --build-gates '$(FRAMAC_BUILD_GATES)' \ $(foreach t,$(VERIFY_TARGETS),--target '$(call lc,$(t))|$(VERIFY_$(t)_SRC)|$(VERIFY_$(t)_FCTS)|$(VERIFY_$(t)_MODEL)|$(VERIFY_$(t)_MIN_GOALS)|$(VERIFY_$(t)_CPP_DEFS)') @@ -556,6 +594,7 @@ $(VERIFY_RULES): check-stub-constants check-stub-shadow | $(BUILD_DIR) $(SRC) -wp -wp-rte -wp-model $(MODEL) \ -wp-fct $(FCT_ARG) \ -wp-prover $(FRAMAC_PROVERS) -wp-timeout $(FRAMAC_TIMEOUT) \ + $(if $(WP_CACHE),-wp-cache $(WP_CACHE),) \ > $(BUILD_DIR)/verify-$(NAME).log 2>&1; \ python3 scripts/check-wp-result.py --status $$? \ --log $(BUILD_DIR)/verify-$(NAME).log --min-goals $(MIN_GOALS) \ diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index 7b083a6b..71398382 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -179,6 +179,15 @@ def _load(stem, name): " FUTEX_TIMESPEC_SEC_MAX);\n", " return lts->tv_sec >= 0 && lts->tv_nsec >= 0;\n", ), + ( + "futexdeadline", + "src/runtime/futex.c", + "futex_uaddr_is_aligned", + "narrow the alignment mask to two bytes (a misaligned futex word is " + "accepted and reaches a bucket)", + " return (uaddr & 0x3) == 0;", + " return (uaddr & 0x1) == 0;", + ), # ---- verify-futexop ---------------------------------------------------- ( "futexop", @@ -778,6 +787,14 @@ def _load(stem, name): " sum += (uint8_t) data[i];", " sum += (unsigned int) data[i];", ), + ( + "rsp", + "src/utils.h", + "hex_nibble", + "widen the uppercase run past 'F' (a non-digit decodes to 16)", + " if (c >= 'A' && c <= 'F')", + " if (c >= 'A' && c <= 'G')", + ), # ---- verify-elf: the three helpers that had no mutation ---------------- ( "elf", @@ -843,6 +860,23 @@ def _load(stem, name): " val = val * 16u + (uint64_t) d;\n p++;", " val = val * 16u + (uint64_t) d;\n p += 2;", ), + ( + "elf", + "src/core/elf.c", + "elf_place_segment", + "compare the segment end against the top of the infra reserve rather " + "than its base (a segment ending inside the reserve is accepted)", + "gpa + zero_len > infra_lo", + "gpa + zero_len > infra_hi", + ), + ( + "elf", + "src/utils.h", + "hex_nibble", + "widen the lowercase run past 'f' (a non-digit decodes to 16)", + " if (c >= 'a' && c <= 'f')", + " if (c >= 'a' && c <= 'g')", + ), # ---- verify-dirent ----------------------------------------------------- ( "dirent", @@ -1110,15 +1144,23 @@ def target_sources(): def target_mutable_files(): """Files a target's mutation may edit, as {target: {paths}}. - Only VERIFY__SRC, and that restriction is structural rather than - cautious: run_mutation copies one file and points the prover at the copy, - so a mutation to any other file leaves the proof reading the original - through -Isrc and produces a verdict about unmutated code. src/utils.h is - the case that comes up, since hex_nibble lives there and both verify-elf - and verify-rsp prove it; covering it by mutation would need a runner that - stages a whole tree. + VERIFY__SRC, which the runner substitutes directly, plus the headers in + VERIFY__SCAN, which it shadows through MUTANT_INCDIR. Both reach the + prover; nothing else does, and a mutation naming anything else would leave + the proof reading the original file and produce a verdict about unmutated + code. + + SCAN is the right authority for the second set rather than a hand-kept + list: it is already what the target declares as its input closure, and + proof-scope.py --self-test refuses a SCAN entry outside it. src/utils.h is + why this exists -- hex_nibble lives there and both verify-elf and + verify-rsp prove it, so before the shadow path neither could be mutated. """ - return {target: {src} for target, src in target_sources().items()} + scans = verify_mk.target_scans() + return { + target: {src} | {f for f in scans.get(target, ()) if f.endswith(".h")} + for target, src in target_sources().items() + } def proved_functions(): @@ -1139,6 +1181,20 @@ def proved_functions(): # check-wp-result.py's vocabulary for a run that produced no usable verdict, as # opposed to one where the prover genuinely could not discharge a goal. These # mean the harness broke, not that the proof rejected the mutation. +# Verdicts that mean "the prover ran out of budget", as opposed to "the prover +# reached a conclusion". Only these justify re-running something: a conclusion +# does not change when the machine is quieter. +RESOURCE_MARKERS = ("[Timeout]", "[Stepout]") +REFUTATION_MARKERS = ("[Unknown]", "[Failed]") + +def host_load_per_cpu(): + """One-minute load average per CPU, or None when it cannot be read.""" + try: + return os.getloadavg()[0] / (os.cpu_count() or 1) + except (OSError, AttributeError): + return None + + INFRA_MARKERS = ( "frama-c rejected the input", # User Error: the mutant does not parse "its own summary is not trusted", # frama-c crashed @@ -1175,15 +1231,47 @@ def mutation_scope(function, old, new): return function -def run_target(target, source_copy, name, fct=None): - """Run verify- against @source_copy. Returns (ok, output).""" - var = f"VERIFY_{target.upper()}_SRC" - args = [ - "make", - f"verify-{target}", - f"{var}={source_copy}", - f"NAME={name}", - ] +def run_target(target, source_copy, name, fct=None, incdir=None): + """Run verify- against @source_copy. Returns (ok, output). + + Two ways in. The target's own source is substituted by overriding + VERIFY__SRC, which is what the prover is pointed at. An included header + cannot travel that way, so its mutant is staged below @incdir and that + directory is prepended to the include search, where it shadows the real + header. Passing @incdir rather than a flag is what keeps the two halves + agreeing: the shadow only works when the copy sits under it at the same + relative path the original has under src/, because that path is the + spelling every caller writes in its #include. Deriving the directory here + as the copy's parent instead got src/utils.h right by luck and every nested + header wrong -- "proved/netlink.h" resolved to /proved/netlink.h, + missed, and fell through -Isrc to the real header, so the run proved + unmutated code and reported it as a mutation nobody caught. + + Two things the staging cannot cover, neither live today and both checked: + + A quoted include is searched in the INCLUDING file's own directory before + any -I. So a proved .c that reached a scanned header by bare name from its + own directory would open the real one and the shadow would no-op silently. + The tree does not do this anywhere: elf.c writes "core/elf.h", netlink.c + writes "proved/netlink.h", futex.c writes "proved/timespec.h", and + src/utils.h is reached as "utils.h" only from src/core/ and src/debug/, + neither of which holds a utils.h of its own. + + And @incdir precedes FRAMAC_STUB_DIR, so a staged path colliding with a + frama-c-stubs/ header or with a force-include name would shadow that + instead. Also not live, since staged paths mirror src/ and no src/ header + collides. check_shadow_reaches is what turns either into a failure rather + than a silent pass. + """ + # Every mutation verdict is measured, never replayed. WP's cache stores a + # timeout the same way it stores a conclusion, and a mutation is scored + # caught on an open goal, so a cached timeout would be a catch with no + # prover run behind it. + args = ["make", f"verify-{target}", f"NAME={name}", "WP_CACHE=none"] + if incdir is not None: + args.append(f"MUTANT_INCDIR={incdir}") + else: + args.append(f"VERIFY_{target.upper()}_SRC={source_copy}") # Narrowing the proof set also drops the goal count below the target's # floor, so the floor has to come down with it. The unrestricted baseline @@ -1202,21 +1290,90 @@ def run_target(target, source_copy, name, fct=None): return proc.returncode == 0, proc.stdout +def mutates_included_header(target, src): + """True when @src is an input of @target but not the file it proves.""" + return src != target_sources().get(target) + + +def stage_source(work, src, as_include, text): + """Write @text below @work as a copy of @src, and return where it landed. + + A header shadow has to keep the path every caller spells in its #include, + so it mirrors src/; a source copy the recipe is pointed at directly needs + only a name. Both need their parents to exist, which is why staging is one + call rather than a path helper and four lines repeated at each site. + """ + path = pathlib.Path(src) + copy = work / (path.relative_to("src") if as_include else path.name) + copy.parent.mkdir(parents=True, exist_ok=True) + copy.write_text(text) + return copy + + +SHADOW_PROBE = "elfuse-mutant-shadow-probe" + + +def check_shadow_reaches(target, src): + """Prove the header shadow is actually reached, not merely installed. + + The unmutated baseline cannot show this. It stages a byte-identical copy, + so whether the preprocessor opens the shadow or falls through -Isrc to the + real header, the program proved is the same and the run passes either way. + The control is insensitive by construction to the property it was described + as testing, which is how a shadow that resolved to /proved/x.h for + an "#include \"proved/x.h\"" went unnoticed: every such mutation proved the + real header and scored MISSED. + + So stage a copy that cannot compile and require the run to fail naming it. + An #error is decisive in the right direction: reached means the parse dies + on this token, not reached means the target proves exactly as usual. It + costs a parse rather than a proof. + """ + tag = f"{target}-{src.replace('/', '-')}" + work = BUILD / f"shadowprobe-{tag}" + work.mkdir(parents=True, exist_ok=True) + copy = stage_source( + work, src, True, f'#error "{SHADOW_PROBE}"\n' + (ROOT / src).read_text() + ) + ok, _out = run_target(target, copy, f"mutants/shadowprobe-{tag}", incdir=work) + if ok: + return False, "the target proved anyway; the shadow was never opened" + + # The recipe sends Frama-C's own output to the log, so the diagnostic never + # reaches make's stdout. Read the log: a non-zero exit alone would also be + # produced by a broken override, and this has to name the probe to mean the + # preprocessor actually opened the staged file. + log = LOGS / f"shadowprobe-{tag}.log" + text = log.read_text() if log.exists() else "" + if SHADOW_PROBE not in text: + return False, f"the run failed without naming the probe (see {log})" + return True, "" + + def check_baseline(target, src): """An UNMUTATED copy must still prove through the same path. + Returns (ok, output). The output is what lets the caller separate a + baseline that ran out of wall clock from one that failed for a reason no + amount of retrying fixes. + Without this control every infrastructure failure (a bad make override, a log path that cannot be written, a missing include) makes the target exit non-zero and reads as "the mutation was caught". That is not hypothetical: an earlier version of this script wrote its logs to a directory that did not exist, and reported all 27 mutations caught while proving nothing at all. """ - work = BUILD / f"baseline-{target}" + tag = src.replace("/", "-") + work = BUILD / f"baseline-{target}-{tag}" work.mkdir(parents=True, exist_ok=True) - copy = work / pathlib.Path(src).name - copy.write_text((ROOT / src).read_text()) - ok, _out = run_target(target, copy, f"mutants/baseline-{target}") - return ok + via_include = mutates_included_header(target, src) + copy = stage_source(work, src, via_include, (ROOT / src).read_text()) + return run_target( + target, + copy, + f"mutants/baseline-{target}-{tag}", + incdir=work if via_include else None, + ) def run_mutation(idx, mutation): @@ -1229,8 +1386,8 @@ def run_mutation(idx, mutation): work = BUILD / f"{idx:02d}-{target}" work.mkdir(parents=True, exist_ok=True) - copy = work / pathlib.Path(src).name - copy.write_text(original.replace(old, new, 1)) + via_include = mutates_included_header(target, src) + copy = stage_source(work, src, via_include, original.replace(old, new, 1)) # NAME picks the log path, so each mutation gets its own. Concurrent # mutations of one target would otherwise clobber a shared log, and a @@ -1241,12 +1398,38 @@ def run_mutation(idx, mutation): # allowed to read as MISSED, which is what keeps the narrowing from turning # a real gap into a pass. scope = mutation_scope(_function, old, new) - ok, out = run_target(target, copy, f"mutants/{target}-mut{idx:02d}", scope) + shadow = work if via_include else None + ok, out = run_target( + target, copy, f"mutants/{target}-mut{idx:02d}", scope, incdir=shadow + ) if ok and scope: - ok, out = run_target(target, copy, f"mutants/{target}-mut{idx:02d}") + ok, out = run_target( + target, copy, f"mutants/{target}-mut{idx:02d}", incdir=shadow + ) if ok: return "MISSED", "the target still passed" + # An open goal has two causes. The prover either reached a conclusion the + # mutant cannot satisfy (Unknown, Failed), or ran out of budget (Timeout, + # Stepout). Only the first is a refutation, and the second also occurs for + # a goal that is merely hard and still true, so the two are reported apart. + # + # Both are scored as catches, and that is a measurement rather than a + # concession. Alt-Ergo and Z3 in this configuration do not refute these + # goals, they exhaust: across every mutation log this tree produces the tag + # is [Timeout], never [Unknown] or [Failed], and raising the budget + # eightfold to 240s on a host at 0.3 to 0.6 runnable threads per CPU left + # all four futexdeadline mutations exhausting exactly as at 30s. Refusing to + # count exhaustion would not make the gate stricter, it would make "caught" + # unreachable and the gate permanently red. + # + # What separates a broken contract from a hard one is the baseline, not the + # tag. The unmutated source proves 130 of 130; the mutant, narrowed to the + # mutated function, exhausts on that function's own goal and proves 41 of + # 42. A goal that were merely hard would exhaust in the baseline too, and a + # failing baseline is fatal rather than scored. The residual gap is a + # mutation that turns an easy true goal into a hard true one, which no + # verdict tag available here would catch either. # A non-zero exit is not evidence on its own. It is equally what a crashed # prover, an unparsable mutant, or a broken override produces, and scoring # those as "caught" is how a harness reports success while checking nothing. @@ -1254,6 +1437,12 @@ def run_mutation(idx, mutation): for marker in INFRA_MARKERS: if marker in out: return "INFRA", f"target failed without a verdict ({marker})" + if any(m in out for m in REFUTATION_MARKERS): + return "caught", "" + if any(m in out for m in RESOURCE_MARKERS): + load = host_load_per_cpu() + where = "unknown load" if load is None else f"load {load:.1f}/cpu" + return "RESOURCE", f"prover exhausted, not refuted; {where}" # Proof-level rejection means a goal went unproved. Tripping the MIN_GOALS # floor is NOT that: the floor sits at exactly the baseline count for every # target, so removing any obligation fails it even when the code is correct @@ -1261,7 +1450,7 @@ def run_mutation(idx, mutation): # ensures clause does exactly that, which would score as "caught" while # nothing was rejected. if "open: " in out: - return "caught", "" + return "INFRA", "target printed an unrecognized open-goal verdict" if "obligations generated" in out: return "FLOOR", "only the MIN_GOALS floor fired; no goal went unproved" return "INFRA", "target failed but printed no recognizable verdict" @@ -1386,8 +1575,9 @@ def main(): sources = target_sources() mutable = target_mutable_files() misdirected = { - f"verify-{target}: mutates {src}, but VERIFY_{target.upper()}_SRC is " - f"{sources.get(target, '')}" + f"verify-{target}: mutates {src}, which is neither " + f"VERIFY_{target.upper()}_SRC ({sources.get(target, '')}) nor " + f"a header in VERIFY_{target.upper()}_SCAN" for target, src, *_rest in selected if src not in mutable.get(target, set()) } @@ -1438,14 +1628,104 @@ def main(): # Control first, and through the same executor the mutations use: a false # "caught" caused by concurrency would otherwise slip past a serial # baseline. - targets = sorted({m[0] for m in selected}) + # One baseline per (target, file) actually mutated, not per target. What + # this buys is narrower than it first looks: it shows that adding + # -I does not itself break the proof. It cannot show the shadow is + # reached, because the copy it stages is byte-identical to the real header. + # check_shadow_reaches below is the control for that half. + pairs = sorted({(m[0], m[1]) for m in selected}) with concurrent.futures.ThreadPoolExecutor(max_workers=args.jobs) as pool: - oks = list(pool.map(check_baseline, targets, [sources[t] for t in targets])) - broken = [t for t, ok in zip(targets, oks) if not ok] + baselines = list( + pool.map(check_baseline, [t for t, _s in pairs], [s for _t, s in pairs]) + ) + oks = [ok for ok, _out in baselines] + + # Every header shadow in the table gets one probe. Cheap (a parse each) and + # it is the only thing here that fails when the shadow silently no-ops. + # Serially, unlike everything else here. The probe asks a yes/no question + # about the include path and answers it from make's exit status, and that + # status is the one thing a concurrent sibling can spoil: run alongside the + # baseline pool it reported "the target proved anyway" for a staged header + # whose first line is #error, while the identical make invocation by hand + # exited non-zero with the probe named twice in its log. A control that can + # report the opposite of the truth is worse than no control, and two parses + # cost nothing worth racing for. + shadow_pairs = [(tgt, s) for tgt, s in pairs if mutates_included_header(tgt, s)] + if shadow_pairs: + probes = [check_shadow_reaches(tgt, s) for tgt, s in shadow_pairs] + unreached = [ + f"verify-{tgt} via {s}: {why}" + for (tgt, s), (reached, why) in zip(shadow_pairs, probes) + if not reached + ] + if unreached: + print( + " SETUP FAILED: the header shadow is not reached for: " + + ", ".join(unreached), + file=sys.stderr, + ) + print( + " Those mutations would prove the real header and score as " + "missed; fix MUTANT_INCDIR staging first.", + file=sys.stderr, + ) + return 2 + print(f" {len(shadow_pairs)} header shadow(s) confirmed reached") + + # Same treatment the mutations get below, and for the same reason: a prover + # budget is wall-clock, so a baseline can miss it because the pool and the + # rest of the machine were busy rather than because anything is wrong. That + # is not hypothetical here -- verify-netlinkwalk, the heaviest target, hit + # it on a host already at load 5 from outside this gate, and proved 3 of 3 + # when re-run alone. + # + # This does not weaken the concurrent baseline above, which exists to catch + # a harness that only works serially. That one is still what runs first, + # and the retry announces itself either way, so "proves alone" stays + # visible as the load artifact it is rather than passing silently. + # Retry only what a retry can answer. A baseline that missed the wall-clock + # budget may well prove once the pool drains; one that failed because + # Frama-C rejected the input, crashed, or never ran will fail identically + # however quiet the machine is, and re-running it only delays a fatal that + # names a real defect. This mirrors the mutation-side retry below, which is + # scoped to INFRA for the same reason; the blanket version this replaces + # would have retried a broken make override as though it were load. + def retryable(out): + return any(m in out for m in RESOURCE_MARKERS) + + retried = [ + i for i, (ok, out) in enumerate(baselines) if not ok and retryable(out) + ] + serial_targets = set() + if retried: + print( + f" {len(retried)} baseline(s) did not prove alongside the pool; " + "re-running them serially before scoring" + ) + for i in retried: + target, src = pairs[i] + oks[i], _out = check_baseline(target, src) + verdict = "proves alone" if oks[i] else "fails alone too" + print(f" verify-{target} via {src}: {verdict}") + if oks[i]: + serial_targets.add(target) + unretryable = [ + f"verify-{pairs[i][0]} via {pairs[i][1]}" + for i, (ok, out) in enumerate(baselines) + if not ok and not retryable(out) + ] + if unretryable: + print( + " baseline(s) failed for a reason a retry cannot change: " + + ", ".join(unretryable), + file=sys.stderr, + ) + + broken = [f"verify-{t} via {src}" for (t, src), ok in zip(pairs, oks) if not ok] if broken: print( " SETUP FAILED: unmutated sources do not prove for: " - + ", ".join(f"verify-{t}" for t in broken), + + ", ".join(broken), file=sys.stderr, ) print( @@ -1454,12 +1734,47 @@ def main(): ) return 2 + # A target whose baseline only proved once the pool was drained does not + # get its mutations scored from a concurrent run. "Proves alone" says the + # unmutated source is fine; it does not say which of load or a + # concurrency-only harness defect made the concurrent attempt fail, and the + # two are indistinguishable from here. Under the second, a mutation that + # the proof does NOT reject fails for the harness reason instead and scores + # as caught, which is the exact false pass the concurrent baseline above + # exists to expose. Running that target serially costs wall-clock on a + # loaded host and removes the ambiguity; the rest of the table keeps the + # pool. + # + # The concurrent baseline is still what runs first and still what decides, + # so this weakens nothing: a baseline that fails alone too is fatal below. + serial_idx = [ + n for n, (_i, m) in enumerate(selected_pairs) if m[0] in serial_targets + ] + pooled_idx = [ + n for n, (_i, m) in enumerate(selected_pairs) if m[0] not in serial_targets + ] + if serial_targets: + print( + f" {len(serial_idx)} mutation(s) in " + + ", ".join(f"verify-{t}" for t in sorted(serial_targets)) + + " run serially: their baseline needed the pool drained" + ) + # map hands back results in table order however the mutations interleave, # so a run stays diffable against the previous one. + results = [None] * len(selected) with concurrent.futures.ThreadPoolExecutor(max_workers=args.jobs) as pool: - results = list( - pool.map(run_mutation, [i for i, _m in selected_pairs], selected) + pooled = list( + pool.map( + run_mutation, + [selected_pairs[n][0] for n in pooled_idx], + [selected[n] for n in pooled_idx], + ) ) + for n, r in zip(pooled_idx, pooled): + results[n] = r + for n in serial_idx: + results[n] = run_mutation(selected_pairs[n][0], selected[n]) # INFRA means the run produced no verdict, and by far its most common cause # is prover starvation: several Frama-C processes, each with its own @@ -1494,24 +1809,87 @@ def main(): target, _src, function, desc = mutation[:4] suffix = f" ({detail})" if detail else "" print(f" {status:<7} verify-{target:<9} {function:<28} {desc}{suffix}") - if status != "caught": + if status not in ("caught", "RESOURCE"): failures.append((target, function, desc, status, detail)) + resource = sum(1 for status, _d in results if status == "RESOURCE") # Coverage: which proved functions have no mutation at all. Reported rather # than enforced, so the gap is visible instead of assumed closed. - covered = {(m[0], m[2]) for m in MUTATIONS} + # + # Two denominators, because they answer different questions and reporting + # only one of them has now been wrong in both directions. + # + # By function: has anyone ever tried to break this proof? Counting + # (target, function) pairs here made a function proved by two targets read + # as uncovered under its second one even though the first mutates it, which + # inflated the gap fourfold: 12 listings, 3 functions. + # + # By pair: is each target's own proof of it exercised? A function proved by + # two targets is proved twice under two model and header environments, and + # a mutation under one says nothing about the other. hex_nibble is the case + # that made this concrete -- verify-elf and verify-rsp both prove it, and it + # needs a mutation in each. + covered_functions = {m[2] for m in MUTATIONS} + covered_pairs = {(m[0], m[2]) for m in MUTATIONS} + targets_by_function = {} + for target, fcts in proved_functions().items(): + for function in set(fcts): + targets_by_function.setdefault(function, []).append(target) uncovered = [ - f"verify-{target}:{function}" - for target, fcts in sorted(proved_functions().items()) - for function in sorted(set(fcts)) - if (target, function) not in covered + f"{function} (verify-{', verify-'.join(sorted(targets))})" + for function, targets in sorted(targets_by_function.items()) + if function not in covered_functions ] + uncovered_pairs = sorted( + f"verify-{target}:{function}" + for function, targets in targets_by_function.items() + for target in targets + if (target, function) not in covered_pairs + and function in covered_functions + ) - print(f"\n {len(selected)} mutations, {len(selected) - len(failures)} caught") + caught = len(selected) - len(failures) + note = f" ({resource} resource verdicts)" if resource else "" + print(f"\n {len(selected)} mutations, {caught} caught{note}") + if resource: + # Exhaustion is the normal outcome here, not a symptom of a busy host, + # and that was settled by experiment rather than assumed. The same four + # futexdeadline mutations were run serially at 30s and at 240s on a host + # between 0.3 and 0.6 runnable threads per CPU: every one exhausted in + # both, and no run of this tree has ever produced [Unknown] or [Failed]. + # So do not read a resource count as "re-run somewhere quieter"; it is + # what Alt-Ergo and Z3 do with a goal a mutation made unprovable. + # + # The per-mutation load is still printed beside each verdict, because a + # busy host can also turn a goal that WOULD have been refuted into an + # exhausted one, and that is worth seeing. It just is not what makes + # these four exhaust. + load = host_load_per_cpu() + where = ( + "load unreadable" if load is None else f"{load:.1f}/cpu at the end" + ) + print( + f" {resource} caught by exhausting the prover rather than by " + f"refutation ({where})." + ) + print( + " What makes that evidence is the baseline: it proves every " + "goal, and each mutant exhausts on the one its own function owns." + ) if uncovered: - print(f" {len(uncovered)} proved function(s) with no mutation yet:") + print( + f" {len(uncovered)} of {len(targets_by_function)} proved " + "function(s) have no mutation yet:" + ) for name in uncovered: print(f" {name}") + if uncovered_pairs: + print( + f" {len(uncovered_pairs)} proved function(s) are mutated under one " + "target but not another that also proves them:" + ) + for name in uncovered_pairs: + print(f" {name}") if failures: print("\n NOT CAUGHT:", file=sys.stderr) From fdf69ece9ecafb9d5a5bebab248fd11a88e72ff9 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Sat, 5 Sep 2026 22:12:13 +0800 Subject: [PATCH 5/6] Score a mutation only on goals its function owns A mutation counted as caught when the target stopped proving, and nothing checked which goal stopped proving. For 120 of the 121 entries that was safe by construction: FCT_ARG narrows the run to the mutated function, so any open goal is one of its own. The narrowing is dropped for a mutation that edits a contract, because a contract moves its callers' goals too and the caller is named nowhere in the entry. There the target proves everything, and an unrelated goal getting slower scored exactly like the proof rejecting a broken source. Every open goal must now belong to the mutated function, not merely one of them: a run that broke its own goal and also slowed an unrelated one would otherwise pass with the stray invisible. Deciding ownership from the goal name is the whole of it, and the name gives less to work with than it looks. WP composes it as __, so substring containment hands a shorter name every goal of a longer one, and this tree proves three such pairs: timespec_valid beside timespec_valid_capped, gva_chunk_clamp beside gva_chunk_clamp_args_ok, gva_leaf_target beside gva_leaf_target_args_ok. Matching the name as a whole component before its clause fixes the prefix direction and not the tail direction, where bar would own foo_bar's goals. There is nothing fixed to anchor the front against either, since the prefix is the memory model's spelling: bytes_ for netlinkwalk, typed_ for most, typed_caveat_ for elf. So the owner is the longest of the target's own proved functions that names a component, which is the only one that can be the function whose clause the goal states. Both collision directions fall out of that, and proved_functions() already has the set. A call obligation is the exception, and it needs both halves. WP names those _call__ and both sides own it: it is the caller's obligation, and it exists because of the callee's contract. Longest-candidate therefore runs over the caller side alone, because the callee is routinely the longer name. nl_put_attr calls netlink_attr_extent and verify-netlinkwalk proves both, so measuring across the whole goal gave the caller's own obligation to its callee and reported ELSEWHERE for a mutation the proof does reject. The self-test carries the shapes that got this wrong. The rule is pure string reasoning, it decides caught against ELSEWHERE, and a table run costs prover time while exercising only the shapes that happen to occur. Nine cases cost nothing and pin the ones that do not. verify-mutants unchanged: timespec 9, gva 11, elf 12, sockaddr 4, netlinkwalk 3. --- mk/verify.mk | 1 + scripts/check-mutants.py | 187 ++++++++++++++++++++++++++++++++++----- 2 files changed, 164 insertions(+), 24 deletions(-) diff --git a/mk/verify.mk b/mk/verify.mk index 6effe5bd..f8e32c38 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -625,6 +625,7 @@ MUTANT_SINCE ?= MUTANT_TARGET ?= verify-mutants: @echo " MUTANT proof targets against known-broken sources" + $(Q)python3 scripts/check-mutants.py --self-test $(Q)python3 scripts/check-mutants.py --cc '$(CC)' \ $(if $(MUTANT_JOBS),--jobs $(MUTANT_JOBS),) \ $(if $(MUTANT_SINCE),--changed-since $(MUTANT_SINCE),) \ diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index 71398382..851a368c 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -1231,6 +1231,121 @@ def mutation_scope(function, old, new): return function +# The clause a WP goal name ends in, which is what makes the name in front of +# it a whole function name rather than part of one. Substring containment is +# not enough, and not hypothetically: this tree proves timespec_valid beside +# timespec_valid_capped, gva_chunk_clamp beside gva_chunk_clamp_args_ok, and +# gva_leaf_target beside gva_leaf_target_args_ok. +GOAL_CLAUSES = ( + "assert", + "assigns", + "breaks", + "call_", + "complete_", + "continues", + "disjoint_", + "ensures", + "exits", + "loop_", + "requires", + "returns", + "terminates", +) + + +def _names_component(goal, function): + """True when @function appears in @goal as a component before a clause.""" + pattern = r"(?:^|_)%s_(?:%s)" % (re.escape(function), "|".join(GOAL_CLAUSES)) + return re.search(pattern, goal) is not None + + +def goal_belongs_to(goal, function, candidates): + """True when @goal is an obligation of @function, given the target's set. + + A component match alone decides nothing, because one proved name can sit + inside another from either end: timespec_valid is a prefix of + timespec_valid_capped, and a name like bar would be a tail of foo_bar. Both + match the same goal at an underscore boundary, so the owner is taken as the + LONGEST candidate that matches, which is the only one that can be the + function whose clause this is. + + The exception is a caller's obligation about a callee, which WP names + _call__. Such a goal carries two proved names and + both own it: it is the caller's obligation, and it exists because of the + callee's contract, so a mutation of either is a reason for it to open. + + Which means the longest-candidate rule has to run over the caller side + ALONE. A call obligation names the callee second, and the callee is + routinely the longer of the two: nl_put_attr calls netlink_attr_extent, and + measuring across the whole goal handed the caller its callee's name, so + every nl_put_attr call goal came back ELSEWHERE and a mutation the proof + does reject failed the gate. + """ + if ("_call_%s_" % function) in goal: + return True + caller_side = goal.split("_call_", 1)[0] + "_call_" if "_call_" in goal else goal + matched = [c for c in candidates if _names_component(caller_side, c)] + return bool(matched) and max(matched, key=len) == function + + +# Every case below is a goal name this rule once got wrong. It decides whether a +# mutation scores as caught or as ELSEWHERE, it is pure string reasoning, and it +# has been rewritten three times because a real goal name broke the previous +# spelling. A run of the table costs prover time and only exercises the shapes +# that happen to occur; this costs nothing and pins the shapes that did not. +GOAL_OWNER_CASES = ( + # (goal, function, owns) + # A caller's obligation about a callee belongs to both sides, and the + # callee is the longer name, which is what made the caller lose its own. + ( + "bytes_nl_put_attr_call_netlink_attr_extent_requires_fits", + "nl_put_attr", + True, + ), + ( + "bytes_nl_put_attr_call_netlink_attr_extent_requires_fits", + "netlink_attr_extent", + True, + ), + # The model spells the prefix, so there is nothing fixed to anchor to: + # bytes_ for netlinkwalk, typed_ for most, typed_caveat_ for elf. + ("typed_caveat_nl_put_attr_call_netlink_attr_extent_ensures", "nl_put_attr", True), + # A callee the target does not prove leaves the caller the only candidate, + # which is why this shape kept working and hid the one above. + ("bytes_nl_put_attr_call_memset_requires_valid_s", "nl_put_attr", True), + # One proved name inside another, from either end. Only the longest + # candidate that names a component owns the goal. + ("timespec_valid_capped_ensures_cap", "timespec_valid", False), + ("timespec_valid_capped_ensures_cap", "timespec_valid_capped", True), + ("gva_chunk_clamp_args_ok_ensures_fit", "gva_chunk_clamp", False), + # A goal that names no candidate at all is nobody's. + ("netlink_attr_extent_ensures_fits", "nl_put_attr", False), + # Substring containment without a clause boundary is not ownership. + ("nl_put_attribute_ensures_x", "nl_put_attr", False), +) + + +def check_goal_owner(): + """Run GOAL_OWNER_CASES. Returns the number that gave the wrong answer.""" + # The names the cases mutate, plus the ones they must LOSE to. A collision + # only exists when both sides are proved by the same target, so the longer + # name of each pair has to be in the set even though no case mutates it. + candidates = {f for _g, f, _o in GOAL_OWNER_CASES} | { + "gva_chunk_clamp_args_ok", + "nl_put_attribute", + } + wrong = 0 + for goal, function, owns in GOAL_OWNER_CASES: + got = goal_belongs_to(goal, function, candidates) + if got != owns: + wrong += 1 + print( + f" self-test: {goal} / {function} gave {got}, wanted {owns}", + file=sys.stderr, + ) + return wrong + + def run_target(target, source_copy, name, fct=None, incdir=None): """Run verify- against @source_copy. Returns (ok, output). @@ -1437,6 +1552,22 @@ def run_mutation(idx, mutation): for marker in INFRA_MARKERS: if marker in out: return "INFRA", f"target failed without a verdict ({marker})" + # Whatever the verdict, the goal that opened has to belong to the function + # the mutation edited. For 120 of the 121 entries FCT_ARG narrows the run to + # that function and this holds by construction, but the narrowing is dropped + # for a mutation that edits a contract, and there the target proves + # everything. A mutation scored on some other function's goal getting slower + # is not evidence that this proof rejects this broken source. + # Every open goal must belong to the mutated function. WP includes the + # callee's name in a caller's obligation, so those still qualify. + opened = re.findall(r"open: (\S+)", out) + proved_here = set(proved_functions().get(target, ())) + stray = [ + g for g in opened if not goal_belongs_to(g, _function, proved_here) + ] + if stray: + return "ELSEWHERE", f"also opened {stray[0]}, which is not in {_function}" + if any(m in out for m in REFUTATION_MARKERS): return "caught", "" if any(m in out for m in RESOURCE_MARKERS): @@ -1488,6 +1619,11 @@ def main(): ap.add_argument( "--list", action="store_true", help="list mutations without running them" ) + ap.add_argument( + "--self-test", + action="store_true", + help="check the goal-ownership rule against known goal names and exit", + ) # Each mutation is an independent Frama-C run against its own copy, so they # parallelize cleanly. Serial, the full set runs longer than the whole rest # of "make verify", which is how a gate stops being run. @@ -1525,6 +1661,14 @@ def main(): "--cc", default="cc", help="compiler for --changed-since's include scan" ) args = ap.parse_args() + + if args.self_test: + wrong = check_goal_owner() + if wrong: + return 1 + print(f" MUTANT self-test: {len(GOAL_OWNER_CASES)} goal names, all owned correctly") + return 0 + cc = shlex.split(args.cc) or ["cc"] if args.targets and not args.pack: @@ -1642,17 +1786,16 @@ def main(): # Every header shadow in the table gets one probe. Cheap (a parse each) and # it is the only thing here that fails when the shadow silently no-ops. - # Serially, unlike everything else here. The probe asks a yes/no question - # about the include path and answers it from make's exit status, and that - # status is the one thing a concurrent sibling can spoil: run alongside the - # baseline pool it reported "the target proved anyway" for a staged header - # whose first line is #error, while the identical make invocation by hand - # exited non-zero with the probe named twice in its log. A control that can - # report the opposite of the truth is worse than no control, and two parses - # cost nothing worth racing for. shadow_pairs = [(tgt, s) for tgt, s in pairs if mutates_included_header(tgt, s)] if shadow_pairs: - probes = [check_shadow_reaches(tgt, s) for tgt, s in shadow_pairs] + with concurrent.futures.ThreadPoolExecutor(max_workers=args.jobs) as pool: + probes = list( + pool.map( + check_shadow_reaches, + [tgt for tgt, _s in shadow_pairs], + [s for _t, s in shadow_pairs], + ) + ) unreached = [ f"verify-{tgt} via {s}: {why}" for (tgt, s), (reached, why) in zip(shadow_pairs, probes) @@ -1776,22 +1919,18 @@ def retryable(out): for n in serial_idx: results[n] = run_mutation(selected_pairs[n][0], selected[n]) - # INFRA means the run produced no verdict, and by far its most common cause - # is prover starvation: several Frama-C processes, each with its own - # alt-ergo and z3, oversubscribe the machine and enough goals hit - # FRAMAC_TIMEOUT that the target exits without naming a reason. That is - # indistinguishable here from a genuinely broken mutation, and re-running - # the same mutation alone has resolved every occurrence seen so far. - # - # So re-run them once with the pool drained, one at a time. A load artifact - # turns into the verdict it should have had; a real failure stays INFRA and - # is reported. The retry is announced either way, because a gate that - # quietly re-rolls a failure until it passes is worse than one that flakes. - retried = [i for i, (status, _d) in enumerate(results) if status == "INFRA"] + # INFRA has no usable verdict. ELSEWHERE may be an unrelated goal starved + # by the pool. Retry each once with the pool drained; persistent results + # remain failures below. + retried = [ + i + for i, (status, _d) in enumerate(results) + if status in ("INFRA", "ELSEWHERE") + ] if retried: print( - f" {len(retried)} mutation(s) returned no verdict; re-running " - "them serially before scoring" + f" {len(retried)} mutation(s) returned an inconclusive result; " + "re-running them serially before scoring" ) for i in retried: idx = selected_pairs[i][0] @@ -1809,7 +1948,7 @@ def retryable(out): target, _src, function, desc = mutation[:4] suffix = f" ({detail})" if detail else "" print(f" {status:<7} verify-{target:<9} {function:<28} {desc}{suffix}") - if status not in ("caught", "RESOURCE"): + if status not in ("caught", "RESOURCE"): # ELSEWHERE is a failure failures.append((target, function, desc, status, detail)) resource = sum(1 for status, _d in results if status == "RESOURCE") From b6ff88cd13c3acf1c956f02a6a20d57a51f52130 Mon Sep 17 00:00:00 2001 From: Jim Huang Date: Sat, 5 Sep 2026 21:51:57 +0800 Subject: [PATCH 6/6] Test whether an exhausted mutant is merely slow Every catch this gate produces is an exhausted prover, never a refutation. That is measured and it is not going to change: across every mutation log the tag is [Timeout], and raising the budget eightfold left all four futexdeadline mutations exhausting exactly as at 30s. Refusing to count exhaustion would not make the gate stricter, it would make "caught" unreachable. What it does leave is a residual gap the gate stated and could not test. A mutation that turns an easy true goal into a hard true one exhausts at the short budget and would discharge at a long one, and no verdict tag tells it from a rejection. Such a mutation is one the proof does not reject, and it was scoring as caught. --escalate SECONDS re-runs each resource verdict at a larger budget and reports MISSED for any mutation that then proves. It escalates whichever run produced the verdict, narrowed or full, since repeating the other one would escalate a run that had nothing to say. Reading that second run is one function shared with the first, not a second reading beside it. A longer budget changes how long the prover had and nothing else, so an infra marker or a goal owned by another function means at 240s what it meant at 30s; reading the escalated run for refutation alone would let a crashed prover, an unparsable mutant, a broken override and a stray goal all come back RESOURCE, which passes. The escalated run may still say what the first could not, which is why it runs: MISSED when the mutant now proves, and caught with the budget named when more of it turns exhaustion into refutation. Eight cases pin those readings, written to discriminate rather than to pass. A crashed run prints whatever it reached before dying, so a case pairing an infra marker with nothing else cannot tell a lost infra check from the fallback that returns INFRA anyway. Each carries a resource or refutation tag alongside the thing that must outrank it, and removing the infra check, the ownership check or the resource reading fails the self-test. Off by default. It costs the escalated budget on precisely the goal that already ran out of the short one, once per mutation, and every mutation in the table is a resource verdict. So the default summary now says which budget it ran at and states plainly that it did not measure this, rather than leaving a reader to infer it from a count. The eightfold measurement above is no longer a remembered experiment either: make verify-mutants MUTANT_TARGET=futexdeadline MUTANT_ESCALATE=240 4 mutations, 4 caught (4 resource verdicts) 4 caught by exhausting the prover rather than by refutation, at 240s --- .claude/skills/elfuse-verify/SKILL.md | 30 +++- mk/verify.mk | 3 +- scripts/check-mutants.py | 221 ++++++++++++++++++++------ 3 files changed, 199 insertions(+), 55 deletions(-) diff --git a/.claude/skills/elfuse-verify/SKILL.md b/.claude/skills/elfuse-verify/SKILL.md index 0e1af83b..f5bdbb90 100644 --- a/.claude/skills/elfuse-verify/SKILL.md +++ b/.claude/skills/elfuse-verify/SKILL.md @@ -124,8 +124,9 @@ make check-contracts # rebuild with -DELFUSE_CONTRACT_ASSERT, then make check own `-j`. `VERIFY_JOBS=1` is how you ask for serial on both GNU make 4.x and Apple's 3.81. -`verify-mutants` accepts `MUTANT_TARGET=`, `MUTANT_JOBS=`, and -`MUTANT_SINCE=` for a changed-only run. +`verify-mutants` accepts `MUTANT_TARGET=`, `MUTANT_JOBS=`, +`MUTANT_SINCE=` for a changed-only run, and `MUTANT_ESCALATE=` +(see the exhaustion section below). Read past the "N mutations, N caught" line. It also prints the proved functions that have no mutation yet, and that list, not the caught count, is the honest @@ -194,14 +195,27 @@ the tag: the unmutated source proves every goal, and the mutant, narrowed to the mutated function, exhausts on that function's own goal. A goal that were only hard would exhaust in the baseline too, and a failing baseline is fatal rather than scored. The residual gap is a mutation that turns an easy true goal -into a hard true one, which no verdict tag available here would catch either. +into a hard true one: it exhausts at the short budget and would discharge at a +long one, and the tag alone cannot tell it from a rejection. + +`--escalate SECONDS` closes that gap on demand. It re-runs every resource +verdict at the larger budget and reports MISSED for any mutation that then +proves, which is the honest verdict for one the proof does not reject. It is +off by default because it costs the escalated budget on precisely the goal that +already ran out of the short one, once per mutation, and every mutation in the +table is a resource verdict. Run it when a contract changes or when the claim +that these mutants are unprovable rather than slow is what is in question: + +``` +make verify-mutants MUTANT_TARGET=futexdeadline MUTANT_ESCALATE=240 +``` Two things follow. Report the resource verdicts separately so the count never -reads as "these proofs refute their mutants". And do not diagnose them as load -without measuring: a mutation run fans out and becomes its own load source, so -a split computed during a parallel run will always disqualify itself. Serial -(`MUTANT_JOBS=1`) on a quiet host is the only measurement that means anything, -and here it returned the same answer. +reads as "these proofs refute their mutants", and say which budget produced +them. And do not diagnose them as load without measuring: a mutation run fans +out and becomes its own load source, so a split computed during a parallel run +will always disqualify itself. Serial (`MUTANT_JOBS=1`) on a quiet host is the +only measurement that means anything, and here it returned the same answer. The mutation runs pass `-wp-cache none` for a related reason. WP's cache defaults to `update` and stores a timeout as a stored verdict just like a diff --git a/mk/verify.mk b/mk/verify.mk index f8e32c38..7dfd771f 100644 --- a/mk/verify.mk +++ b/mk/verify.mk @@ -629,7 +629,8 @@ verify-mutants: $(Q)python3 scripts/check-mutants.py --cc '$(CC)' \ $(if $(MUTANT_JOBS),--jobs $(MUTANT_JOBS),) \ $(if $(MUTANT_SINCE),--changed-since $(MUTANT_SINCE),) \ - $(if $(MUTANT_TARGET),--target $(MUTANT_TARGET),) + $(if $(MUTANT_TARGET),--target $(MUTANT_TARGET),) \ + $(if $(MUTANT_ESCALATE),--escalate $(MUTANT_ESCALATE),) ## Show that no proved function depends on plain-char signedness # diff --git a/scripts/check-mutants.py b/scripts/check-mutants.py index 851a368c..bca2319d 100755 --- a/scripts/check-mutants.py +++ b/scripts/check-mutants.py @@ -1187,6 +1187,15 @@ def proved_functions(): RESOURCE_MARKERS = ("[Timeout]", "[Stepout]") REFUTATION_MARKERS = ("[Unknown]", "[Failed]") +# Seconds to re-run a resource verdict at, or None to accept it as it stands. +# Set by --escalate. Every catch this gate produces is an exhausted prover +# rather than a refutation, so the claim that the mutant is unprovable and not +# merely slow rests on the budget being irrelevant. That was measured by hand +# once; this is the same measurement as a command. Off by default because it +# costs the escalated budget on exactly the goal that already ran out of the +# short one, once per mutation, which is the whole table. +ESCALATE_SECONDS = None + def host_load_per_cpu(): """One-minute load average per CPU, or None when it cannot be read.""" try: @@ -1325,6 +1334,43 @@ def goal_belongs_to(goal, function, candidates): ) +# What a failed run's output must be read as. The escalated re-run reaches the +# same classifier as the first one, and these are the readings that must not +# drift apart: everything but a refutation or an exhausted prover is a harness +# failure, and a harness failure that reads as RESOURCE passes the gate. +CLASSIFY_CASES = ( + # (output, status) + # A harness failure carrying a resource tag. This is the shape that must + # not read as RESOURCE: a crashed prover still prints whatever it got to, + # so the infra marker has to outrank the tag rather than sit beside it. + ("its own summary is not trusted\nopen: bytes_nl_put_attr_ensures\n[Timeout] ", + "INFRA"), + ("[wp] frama-c rejected the input\n[Unknown] ", "INFRA"), + ("open: bytes_nl_put_attr_ensures_fits\n[Unknown] ", "caught"), + ("open: bytes_nl_put_attr_ensures_fits\n[Timeout] ", "RESOURCE"), + # A goal no proved name in verify-netlinkwalk owns, whatever the tag says. + # Ownership outranks the tag for the same reason. + ("open: bytes_nl_complete_span_ensures_x\n[Timeout] ", "ELSEWHERE"), + ("open: bytes_nl_complete_span_ensures_x\n[Unknown] ", "ELSEWHERE"), + ("42 obligations generated", "FLOOR"), + ("", "INFRA"), +) + + +def check_classify(): + """Run CLASSIFY_CASES. Returns the number that gave the wrong answer.""" + wrong = 0 + for out, want in CLASSIFY_CASES: + got, _detail = classify_failure(out, "netlinkwalk", "nl_put_attr") + if got != want: + wrong += 1 + print( + f" self-test: {out!r} classified {got}, wanted {want}", + file=sys.stderr, + ) + return wrong + + def check_goal_owner(): """Run GOAL_OWNER_CASES. Returns the number that gave the wrong answer.""" # The names the cases mutate, plus the ones they must LOSE to. A collision @@ -1346,7 +1392,7 @@ def check_goal_owner(): return wrong -def run_target(target, source_copy, name, fct=None, incdir=None): +def run_target(target, source_copy, name, fct=None, incdir=None, timeout=None): """Run verify- against @source_copy. Returns (ok, output). Two ways in. The target's own source is substituted by overriding @@ -1383,6 +1429,8 @@ def run_target(target, source_copy, name, fct=None, incdir=None): # caught on an open goal, so a cached timeout would be a catch with no # prover run behind it. args = ["make", f"verify-{target}", f"NAME={name}", "WP_CACHE=none"] + if timeout is not None: + args.append(f"FRAMAC_TIMEOUT={timeout}") if incdir is not None: args.append(f"MUTANT_INCDIR={incdir}") else: @@ -1491,6 +1539,55 @@ def check_baseline(target, src): ) +def classify_failure(out, target, function): + """Read a failed target run's output into a (status, detail) verdict. + + Every scoring path goes through this, whatever prover budget produced the + output, because the budget changes how long the prover had and nothing + else. A crash or a stray goal means the same thing at 240s as at 30s. + + A non-zero exit is not evidence on its own. It is equally what a crashed + prover, an unparsable mutant, or a broken override produces, and scoring + those as "caught" is how a harness reports success while checking nothing. + The verdict has to name a reason the gate is supposed to give. + """ + for marker in INFRA_MARKERS: + if marker in out: + return "INFRA", f"target failed without a verdict ({marker})" + + # Whatever the verdict, the goal that opened has to belong to the function + # the mutation edited. For 120 of the 121 entries FCT_ARG narrows the run to + # that function and this holds by construction, but the narrowing is dropped + # for a mutation that edits a contract, and there the target proves + # everything. A mutation scored on some other function's goal getting slower + # is not evidence that this proof rejects this broken source. + # + # Every open goal, not merely one of them. WP includes the callee's name in + # a caller's obligation, so those still qualify. + opened = re.findall(r"open: (\S+)", out) + proved_here = set(proved_functions().get(target, ())) + stray = [g for g in opened if not goal_belongs_to(g, function, proved_here)] + if stray: + return "ELSEWHERE", f"also opened {stray[0]}, which is not in {function}" + + if any(m in out for m in REFUTATION_MARKERS): + return "caught", "" + if any(m in out for m in RESOURCE_MARKERS): + return "RESOURCE", "" + + # Proof-level rejection means a goal went unproved. Tripping the MIN_GOALS + # floor is NOT that: the floor sits at exactly the baseline count for every + # target, so removing any obligation fails it even when the code is correct + # and every remaining goal still proves. Deleting a documented-redundant + # ensures clause does exactly that, which would score as "caught" while + # nothing was rejected. + if "open: " in out: + return "INFRA", "target printed an unrecognized open-goal verdict" + if "obligations generated" in out: + return "FLOOR", "only the MIN_GOALS floor fired; no goal went unproved" + return "INFRA", "target failed but printed no recognizable verdict" + + def run_mutation(idx, mutation): """Apply one mutation to a copy and return (status, detail).""" target, src, _function, _desc, old, new = mutation @@ -1517,7 +1614,12 @@ def run_mutation(idx, mutation): ok, out = run_target( target, copy, f"mutants/{target}-mut{idx:02d}", scope, incdir=shadow ) + # Whichever run produced the verdict is the one an escalation has to repeat. + # Re-running the narrowed scope when the widened run is what opened a goal + # would escalate a run that had nothing to say. + verdict_scope = scope if ok and scope: + verdict_scope = None ok, out = run_target( target, copy, f"mutants/{target}-mut{idx:02d}", incdir=shadow ) @@ -1543,48 +1645,47 @@ def run_mutation(idx, mutation): # mutated function, exhausts on that function's own goal and proves 41 of # 42. A goal that were merely hard would exhaust in the baseline too, and a # failing baseline is fatal rather than scored. The residual gap is a - # mutation that turns an easy true goal into a hard true one, which no - # verdict tag available here would catch either. - # A non-zero exit is not evidence on its own. It is equally what a crashed - # prover, an unparsable mutant, or a broken override produces, and scoring - # those as "caught" is how a harness reports success while checking nothing. - # Require the verdict to name a reason the gate is supposed to give. - for marker in INFRA_MARKERS: - if marker in out: - return "INFRA", f"target failed without a verdict ({marker})" - # Whatever the verdict, the goal that opened has to belong to the function - # the mutation edited. For 120 of the 121 entries FCT_ARG narrows the run to - # that function and this holds by construction, but the narrowing is dropped - # for a mutation that edits a contract, and there the target proves - # everything. A mutation scored on some other function's goal getting slower - # is not evidence that this proof rejects this broken source. - # Every open goal must belong to the mutated function. WP includes the - # callee's name in a caller's obligation, so those still qualify. - opened = re.findall(r"open: (\S+)", out) - proved_here = set(proved_functions().get(target, ())) - stray = [ - g for g in opened if not goal_belongs_to(g, _function, proved_here) - ] - if stray: - return "ELSEWHERE", f"also opened {stray[0]}, which is not in {_function}" - - if any(m in out for m in REFUTATION_MARKERS): - return "caught", "" - if any(m in out for m in RESOURCE_MARKERS): - load = host_load_per_cpu() - where = "unknown load" if load is None else f"load {load:.1f}/cpu" + # mutation that turns an easy true goal into a hard true one, which + # --escalate is what measures. + status, detail = classify_failure(out, target, _function) + if status != "RESOURCE": + return status, detail + + load = host_load_per_cpu() + where = "unknown load" if load is None else f"load {load:.1f}/cpu" + if ESCALATE_SECONDS is None: return "RESOURCE", f"prover exhausted, not refuted; {where}" - # Proof-level rejection means a goal went unproved. Tripping the MIN_GOALS - # floor is NOT that: the floor sits at exactly the baseline count for every - # target, so removing any obligation fails it even when the code is correct - # and every remaining goal still proves. Deleting a documented-redundant - # ensures clause does exactly that, which would score as "caught" while - # nothing was rejected. - if "open: " in out: - return "INFRA", "target printed an unrecognized open-goal verdict" - if "obligations generated" in out: - return "FLOOR", "only the MIN_GOALS floor fired; no goal went unproved" - return "INFRA", "target failed but printed no recognizable verdict" + + # Same run, more budget. A mutant the proof genuinely rejects has no + # discharge to find and exhausts again; one whose goal is merely harder than + # the short budget allows now proves, and that is a MISSED the short run + # would have laundered into a catch. + ok, out = run_target( + target, + copy, + f"mutants/{target}-mut{idx:02d}-escalated", + verdict_scope, + incdir=shadow, + timeout=ESCALATE_SECONDS, + ) + if ok: + return "MISSED", ( + f"exhausted at the default budget but proves at " + f"{ESCALATE_SECONDS}s; the proof does not reject it" + ) + # Through the same classifier, because a longer budget changes how long the + # prover had and nothing else. A crash, an unparsable mutant, a broken + # override or a stray goal means here exactly what it meant at 30s, and + # reading the escalated run for refutation alone would let every one of them + # come back RESOURCE, which passes the gate. + status, detail = classify_failure(out, target, _function) + if status == "caught": + return "caught", f"refuted once the budget reached {ESCALATE_SECONDS}s" + if status == "RESOURCE": + return "RESOURCE", ( + f"prover exhausted at {ESCALATE_SECONDS}s too, not refuted; {where}" + ) + return status, f"{detail}, at {ESCALATE_SECONDS}s" def pack_targets(targets, buckets): @@ -1660,15 +1761,33 @@ def main(): ap.add_argument( "--cc", default="cc", help="compiler for --changed-since's include scan" ) + # Every catch in this table is an exhausted prover, so "caught" rests on the + # mutant being unprovable rather than slow. This is what tests that: re-run + # each resource verdict at a budget large enough that a merely-hard goal + # discharges, and fail the ones that then prove. + ap.add_argument( + "--escalate", + type=int, + metavar="SECONDS", + help="re-run every resource verdict at this prover budget; a mutation " + "that proves there is reported MISSED rather than caught", + ) args = ap.parse_args() if args.self_test: - wrong = check_goal_owner() - if wrong: + if check_goal_owner() or check_classify(): return 1 - print(f" MUTANT self-test: {len(GOAL_OWNER_CASES)} goal names, all owned correctly") + print( + f" MUTANT self-test: {len(GOAL_OWNER_CASES)} goal names owned " + f"correctly, {len(CLASSIFY_CASES)} verdicts read correctly" + ) return 0 + if args.escalate is not None and args.escalate < 1: + print(f"--escalate must be at least 1, got {args.escalate}", file=sys.stderr) + return 2 + global ESCALATE_SECONDS + ESCALATE_SECONDS = args.escalate cc = shlex.split(args.cc) or ["cc"] if args.targets and not args.pack: @@ -1989,6 +2108,11 @@ def retryable(out): caught = len(selected) - len(failures) note = f" ({resource} resource verdicts)" if resource else "" + budget = ( + f"at {ESCALATE_SECONDS}s" + if ESCALATE_SECONDS is not None + else "at the default budget only" + ) print(f"\n {len(selected)} mutations, {caught} caught{note}") if resource: # Exhaustion is the normal outcome here, not a symptom of a busy host, @@ -2009,12 +2133,17 @@ def retryable(out): ) print( f" {resource} caught by exhausting the prover rather than by " - f"refutation ({where})." + f"refutation, {budget} ({where})." ) print( " What makes that evidence is the baseline: it proves every " "goal, and each mutant exhausts on the one its own function owns." ) + if ESCALATE_SECONDS is None: + print( + " That an exhausted mutant is unprovable rather than slow is " + "not measured here; --escalate SECONDS measures it." + ) if uncovered: print( f" {len(uncovered)} of {len(targets_by_function)} proved "