diff --git a/.claude/skills/elfuse-verify/SKILL.md b/.claude/skills/elfuse-verify/SKILL.md index 05a826d1..f5bdbb90 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 @@ -82,8 +124,107 @@ 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 +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: 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 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 +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 @@ -130,6 +271,52 @@ 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" +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 +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 +352,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 +642,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/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/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/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 9d121021..7dfd771f 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,82 @@ CPP_DEFS := # git ls-files 'src/*.c' and tally the exits. FRAMAC_STUB_DIR := frama-c-stubs -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) \ +# 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 + +# 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%,$(MUTANT_INCDIR) $(FRAMAC_INCLUDE_DIRS)) \ + $(patsubst %,-include %,$(FRAMAC_FORCE_INCLUDES)) \ $(CPP_DEFS) # One proof per attacker-facing parser. Each is declared by a single @@ -148,7 +222,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 @@ -272,15 +346,19 @@ 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 \ 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 \ @@ -438,6 +516,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)" \ + $(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)') + # 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. @@ -491,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) \ @@ -521,10 +625,12 @@ 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),) \ - $(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 7b083a6b..bca2319d 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,29 @@ 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]") + +# 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: + 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 +1240,201 @@ 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}", - ] +# 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), +) + + +# 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 + # 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, timeout=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 timeout is not None: + args.append(f"FRAMAC_TIMEOUT={timeout}") + 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 +1453,139 @@ 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 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): @@ -1229,8 +1598,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,30 +1610,82 @@ 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 + ) + # 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: - ok, out = run_target(target, copy, f"mutants/{target}-mut{idx:02d}") + verdict_scope = None + ok, out = run_target( + target, copy, f"mutants/{target}-mut{idx:02d}", incdir=shadow + ) if ok: return "MISSED", "the target still passed" - # 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})" - # 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 "caught", "" - 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" + # 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 + # --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}" + + # 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): @@ -1299,6 +1720,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. @@ -1335,7 +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: + if check_goal_owner() or check_classify(): + return 1 + 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: @@ -1386,8 +1838,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 +1891,103 @@ 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. + shadow_pairs = [(tgt, s) for tgt, s in pairs if mutates_included_header(tgt, s)] + if 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) + 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,29 +1996,60 @@ 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], + ) ) - - # 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"] + 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 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] @@ -1494,24 +2067,97 @@ 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"): # ELSEWHERE is a failure 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 "" + 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, + # 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, {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)} 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) 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 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() 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;