Conversation
A guest supplies msg_control verbatim, and sys_sendmsg walked it as a hand-rolled TLV loop. Each entry's cmsg_len is eight bytes read straight out of guest memory and drives both the payload extent the host copies and the advance to the next entry, so the no-underflow and termination argument rested entirely on the ordering of two guards. Move that arithmetic to src/syscall/cmsg-math.h and prove it: make verify-cmsg discharges 17 of 17 obligations. Follows the gva-math.h pattern, since net-msg.c cannot be given to Frama-C (it includes the macOS socket headers) while the extracted header needs only stdint.h. The host CMSG_SPACE / CMSG_LEN / CMSG_FIRSTHDR / CMSG_NXTHDR macros stay outside the proof boundary. They describe the macOS layout, and a stub for them would be an unchecked model of the thing in question; the caller keeps them and passes only Linux-side numbers in. The recvmsg direction, which does use those macros, is not covered. Two details the prover forced. The align-up is written as advance -= advance % CMSG_LINUX_ALIGN rather than (len + 7) & ~7: the bitwise form leaves both next_pos bounds open because the prover must first establish the mask is one less than a power of two. And the contract needs an exact-advance postcondition, not just a bound: with only next_pos > pos and the overshoot bound, dropping the align-up entirely satisfies every clause, staying memory-safe while walking to a misaligned next header. Those two next_pos bounds are corollaries of it, kept because they state termination and the caller's own bound check in the form the caller reasons about. Four mutations confirm the gate bites: dropping either guard, changing the align-up addend, and dropping the align-up altogether. Both directions now use the named constants. sys_sendmsg bounds msg_controllen against CMSG_LINUX_CTL_MAX before narrowing it to size_t, so the check that establishes the proof's precondition is spelled the same way the precondition is; sys_recvmsg, which builds the control buffer rather than walking a guest-supplied one and so stays outside the proof, was migrated off its own literals to stop the two drifting apart. Behavior preservation checked rather than assumed: 46 million differential cases against the original inline arithmetic found zero mismatches, and the subtract-the-remainder align-up is a pure identity with (x + 7) & ~7 across the whole uint64 range including wraparound.
The FUSE daemon is another guest process, so the reply header it writes to /dev/fuse is hostile input. Its len field decides how many bytes the host copies out of the frame buffer. That is not a hypothetical concern: the fuse_read_common overrun fixed earlier was a defect of exactly this class, in this file. Move the frame arithmetic to src/syscall/fuse-math.h and prove it: make verify-fuse discharges 27 of 27 obligations. fuse.c cannot be given to Frama-C (pthread plus the macOS headers), while the extracted header needs only stdint.h. fuse_out_header_t moves with it so a _Static_assert ties FUSE_OUT_HDR_BYTES to the struct the code actually memcpys. Three helpers. fuse_frame_count_ok bounds the daemon's write. fuse_reply_extent computes the payload extent, and its load-bearing postcondition is FUSE_OUT_HDR_BYTES + reply_len <= count, which is what the caller's memcpy from buf + FUSE_OUT_HDR_BYTES rests on. fuse_clamp_negotiated_write is why this target is worth more than a subtraction. A read reply is a header plus at most max_write payload bytes, and fuse_dev_write rejects frames above FUSE_FRAME_CAP, so FUSE_OUT_HDR_BYTES + max_write <= FUSE_FRAME_CAP is what keeps a successfully negotiated size from producing replies the write path then refuses. That was a prose claim in a comment and is now a proved postcondition. A mutation setting FUSE_MAX_NEGOTIATED_WRITE equal to FUSE_FRAME_CAP fails the proof, which is what shows the 256 bytes of slack are load-bearing rather than arbitrary. Five mutations confirm the gate bites: dropping either half of the hdr_len guard, dropping the frame ceiling, making the clamp a no-op, and removing the slack. Scope is the frame level only. Per-opcode payload extents would drag about 125 lines of ABI struct definitions out of fuse.c and would collapse to reply_len >= want, generating almost nothing to prove; they stay test-covered. FUSE_FRAME_CAP changed type from size_t to unsigned long long in the move, so every use in the tree was audited. Both macros are now referenced only inside the proved header and two call sites, with no signed comparison and no test uses, so no conversion changed. A 361,344-case differential test of the new helpers against the original inline arithmetic, covering the uint32 hdr.len boundaries and the clamp round trip, found zero mismatches.
guest.c cannot be given to Frama-C, so nothing checked that its call sites honor gva-math.h's nine requires clauses. One of them says so in a comment at guest.c:1477. This narrows that gap; it does not close it. Only five of the nine clauses have a C expression. The four pointer ones do not: assert(p != NULL) is strictly weaker than \valid(p), and assert(a != b) misses overlapping distinct pointers into one object, which is exactly the drift worth catching. Those stay review-only and the header says so. Rather than restating each precondition inline, the expressible clauses are factored into two predicates carrying ensures \result != 0 <==> (...) contracts, proved by make verify-gva. A restated condition can drift weaker than the clause it mirrors with nothing to notice; a predicate with an iff cannot, because weakening it fails the proof. One expression serves both the contract and the runtime check. verify-gva now runs with -DELFUSE_CONTRACT_ASSERT so the prover sees the checks too and must discharge each from the clause it mirrors. That extends the guarantee from the predicate bodies to the wiring: a check handed permuted arguments fails the proof rather than surfacing later as a spurious abort. 40 of 40 becomes 66 of 66. What the proof cannot catch is a check wired to a constant that satisfies the predicate instead of to the real argument, since that stays derivable. tests/test-gva-contracts.c covers it from the other side by violating each conjunct in a forked child and requiring the check to reject. Verified complementary: that mutation keeps verify-gva green at 66 of 66 and fails the test. make check-contracts rebuilds with the checks live and runs the suite; 82 passed, 0 failed, no check fired, so every call site the suite reaches honors all five clauses. Injecting a deliberately wrong call into guest.c aborts under that build and is silent without it. Two hazards found in review and fixed. assert.h re-reads NDEBUG at every include, so -DNDEBUG would have rebuilt, run the whole suite, and reported success while checking nothing; #undef NDEBUG closes that. And check-contracts now builds into its own directory: sharing BUILD_DIR left instrumented objects behind, so a later make elfuse relinked them into a default-looking binary carrying asserts on the guest_read / guest_write hot path. Confirmed by symbol count, 0 in the default build after a full contracts run, 1 in the contracts tree.
build_linux_stack lays out argc/argv/envp/auxv the way binfmt_elf does, and two things there are easy to get wrong and hard to see wrong. The string region walks down from stack_top by a guest-controlled number of guest-controlled lengths. The structured area must leave SP 16-byte aligned AND pointing directly at argc; a libc that finds either wrong does not fail cleanly, it reads argv from the wrong offset. New src/core/stack-math.h, proved by make verify-stack at 36 of 36. stack.c cannot be given to Frama-C (it pulls in Hypervisor.framework via guest.h and proc.h) while the extracted header needs only stdint.h. Not a bug fix. An earlier reading suspected a guest could drive the descent past the stack guard; it cannot, because read_string_array caps combined argv/envp bytes at 2 MiB and the entry count at 131072 against an 8 MiB stack. What changes is that containment is now held by stack_take's own postcondition rather than by an argument about caps in a different file. The other half is worth more. total_entries = 35 + extra + argc + envc is a hand-maintained count of the pushes below it, explained by a fifteen-line comment. Adding an AUX() entry without updating it would leave SP misaligned or short of argc with nothing to say so. The count now precomputes the expected final SP through stack_pushed_words and stack_final_sp, and the function fails loudly if the SP actually reached differs. Verified by injecting an extra AUX(): it reports which count is out of sync instead of booting a broken stack. The floor is stack_base + STACK_GUARD_SIZE, not stack_base. Two reviewers independently caught that: the low 4 KiB of the region is the PROT_NONE guard, so bare stack_base would let the descent walk into it and fail later inside guest_write with a worse diagnostic. argc is now bounded below as well as above. A negative argc makes the uint64 total_entries cast about 2^64, violating the STACK_MAX_WORDS precondition, after which the word count wraps and stack_final_sp can report success with a garbage SP. No caller does this today; the check makes the code discharge the precondition rather than leaving it as an argument about other files. sys_execve now checks build_linux_stack's 0 return before programming SP_EL0 from it. Past the point of no return there is no image to go back to, so it aborts in the same shape as the other post-reset fatal errors. The argc bound it could reject on is enforced upstream by an identical cap, so the live path is allocation failure. _Static_assert pins STACK_ALIGN to 16 and STACK_WORD to sizeof(uint64_t): the proofs are parameterized over both, so changing either would still prove while breaking the layout. The push-count identity was checked rather than assumed: 20 AUX sites, 2 conditional, so the auxv words plus the three terminators equal total_entries for all four combinations of execfd and vdso presence. Confirmed empirically over 107584 cases, every final SP 16-aligned. Named verify-stack, not verify-auxv, to match the file and prefix the way the five sibling targets do.
Linux and macOS disagree about sockaddr: Linux has a 2-byte family and no length byte, macOS has a 1-byte length plus a 1-byte family. Every bind, connect, sendto, recvfrom and accept reshapes an address, and the length driving that reshape is guest-supplied on the way in. Both directions subtract the family bytes and clamp against the destination, and each subtraction underflows if its guard is dropped. An underflowed length here is a memcpy extent, so the result is a host overrun rather than a truncated address. New src/syscall/sockaddr-math.h, proved by make verify-sockaddr at 11 of 11. One clamp serves both directions because the destination capacity arrives as a plain integer rather than a struct: the proof names no socket type at all. That matters beyond tidiness. Frama-C 31 does define struct sockaddr_storage, but with the POSIX layout and no ss_len field, so proving against it would be proving against the wrong struct. Both converters now call the helpers and the clamp logic is gone from their bodies, which is the condition the TODO set for keeping this as a target rather than closing it. At 11 obligations it is the smallest of the seven, but each of the four mutations breaks a distinct property: dropping the destination clamp, accepting under-length addresses, returning no payload at all, and dropping the source precondition. Two pins added in review, both the same shape: a constant the proofs are parameterized over would still prove if changed while the code around it broke. SOCKADDR_FAMILY_BYTES is asserted to be 2, since setting it to 1 would make net-abi.c accept 1-byte sockaddrs and copy from the wrong payload boundary. The other pin is load-bearing in a subtler way. mac_len is socklen_t and is now widened to uint64_t before the length guard, where the old code compared it directly. That is equivalent only because socklen_t is unsigned on this platform; were it signed, a negative length would widen to a huge value, pass the guard, and be clamped to the destination size rather than rejected. _Static_assert((socklen_t) -1 > 0) makes the dependency fail the build instead of failing silently. Writing the guard as mac_len < 0 instead would be a tautological compare on an unsigned type.
Every claim that a proof actually binds has been established by a reviewer editing a body and watching the target fail. None of it was recorded, so each contract change re-established it from scratch or, more often, did not. make verify-mutants now carries 30 mutations, each of which must make its target fail, and reports which proved functions have none yet (8 of 27 today). Mutations run against copies under build/mutants via VERIFY_<TARGET>_SRC, so a run never edits the tree. That is not fastidiousness: hand mutation testing with cp-and-restore left a mutated source on disk twice during this work, and a reviewer independently observed one of those windows. Most of the effort went into not reporting success for the wrong reason, because a harness that does that is worse than none. Three ways it did: - An early version wrote logs to a directory that did not exist. Every run failed on the redirect, and all 27 mutations reported caught while proving nothing. A baseline control now requires an UNMUTATED copy of each source to still prove before any verdict counts. - Concurrent runs shared build/verify-<name>.log. A clobbered log makes the recipe exit non-zero, which reads as caught. Each run now gets its own log via a NAME override. - A mutation naming a file its target does not analyze silently analyzed the wrong file. The first rsp entry mutated hex_nibble in utils.h, which verify-rsp includes rather than analyzes; the baseline control caught it. A guard now rejects any mutation whose source is not its target's VERIFY_<T>_SRC, and the rsp entries moved to gdbstub-rsp.c. The subtlest one came from review. A non-zero exit is not evidence: a crashed prover or an unparsable mutant produces one too. Worse, MIN_GOALS sits at exactly the baseline count for all seven targets, so deleting a documented-redundant ensures clause, with the code untouched and every remaining goal proving, also fails the target. Both scored as caught. Verdicts are now classified from the output: a goal must go UNPROVED. Floor-only failures report FLOOR and infrastructure failures report INFRA, and both fail the run rather than counting. Under that stricter rule all 30 mutations still pass, which is the evidence the harness was supposed to gather and previously only assumed. check-acsl-coverage.py also gained the plain-char check. gcc_x86_64 makes plain char signed where arm64 macOS makes it unsigned, and what keeps the proofs signedness-independent is that no proved function reads a plain char without an explicit cast. Deciding that for an expression needs a C front end, which this tree does not have; what a regex can do is require any proved function taking a plain char to be on an allowlist, so a new one cannot appear silently. Writing it found the makefile comment had listed three such functions when there are four: gdb_parse_hex was missing.
make verify-netlink proves the arithmetic behind both netlink walks: 44 of 44 obligations. The request parse reads an rtattr chain out of bytes the guest wrote, so its per-entry bounds are worth a proof on their own; the reply span walk is here for termination. The termination half turned out to matter more than expected. nl_complete_span rounded hdr->nlmsg_len up in uint32 arithmetic, which wraps to 0 for nlmsg_len >= 0xFFFFFFFD, so the cursor advanced by nothing and the loop spun forever holding nl_lock. An earlier reading of this, mine, called that unreachable because ns->buf holds only elfuse's own synthesized replies. The bytes are ours; the cursor is not. nl_complete_span returns to_copy when no whole message fits and the caller advances buf_pos by it, so a guest receiving fewer bytes than one header moves the cursor to a non-header offset. Eight bytes into a reply sits nlmsg_seq, echoed straight from the guest's own request. A guest that asks with seq 0xFFFFFFFF and then receives 8 bytes reads its own value back as an nlmsg_len on the next receive. Widening to uint64_t removes the wrap; the proved postcondition that the span is strictly positive is what makes the loop terminate for any header. The cursor landing off a message boundary is a separate defect and is recorded in TODO.md. It no longer hangs, but it still parses from mid-message. Also here: the two walk structs and their header lengths moved into the proved header with static assertions tying the byte constants to the struct sizes, NLMSG_ALIGN and RTA_ALIGN collapsed into the one proved align-up so the reply builders and the walks cannot round differently, and the span header is now read by memcpy rather than a typed cast, since the cursor is not guaranteed to be suitably aligned. Behavior preservation checked rather than assumed: 107 million cases over the rtattr guard rewrite (off + rta_len > total became rta_len > total - off), the uint16 cast site in the attribute builder, and the span computation, with zero divergence outside the three wrap values above. Four mutations added to verify-mutants, all caught. A fifth, changing the wire alignment from 4 to 8, is deliberately not in the table: the static assertion rejects it at build time, so the harness correctly classified it INFRA rather than crediting the proof for catching it.
make verify-sigframe proves where a signal frame lands: 15 of 15 obligations. The base must be 16-byte aligned, because the handler runs with it as SP under AAPCS64, and the frame must sit wholly below the interrupted SP without the subtraction wrapping. Placed wrong, the handler runs on a misaligned stack or over memory that was still live. The header names no frame type. The size arrives as a plain integer, so no guest ABI struct had to move out of signal.h, which is what the TODO entry named as the condition for dropping this target rather than building it. Scope is placement only. Whether the frame's field offsets match arch/arm64/kernel/signal.c is the property that actually breaks libc, nothing here establishes it, and no golden-layout test covers it either. That gap is recorded as its own item rather than left as an unexamined assumption. The contract pins both directions. Every other clause is guarded by a non-zero result, so a body that always refuses would satisfy them all; an iff fixes when the function must succeed, which is also what catches an off-by-one rejection at the floor. The distance bound does something narrower than it looks: with the alignment it leaves exactly one legal base, so the frame cannot sit an aligned slot lower than required. Two related defects fixed here. The static assertion tying the frame size to LINUX_MINSIGSTKSZ has to account for the up-to-15 bytes align-down consumes, or a future frame of 5110 would pass it while minimum-size altstacks failed. And sigaltstack validated ss_size but not that ss_sp + ss_size wraps: delivery computes the altstack top as that sum, so a wrapping pair gave a low address unrelated to the stack the guest described. Rejected with EINVAL now, stricter than Linux, whose do_sigaltstack checks only the minimum size. The altstack floor is the one behavior change: placement can now fail there, where before only absolute underflow was checked. It cannot fire, and the static assertion is what says so, since sigaltstack rejects under 5120 and a frame is 4688. The margin is real but not large, and it shrinks whenever the frame grows. Behavior preservation on the normal-stack path checked rather than assumed: 1.25 million differential cases over the guard rewrite and the align-down, including the full uint64 edges, with zero divergence.
![cubic-dev-ai[bot]](https://avatars.githubusercontent.com/in/1082092?s=60&v=4){kind=small}
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Seven of the eight findings from the PR #277 review were valid. The eighth is real but predates this branch, so it is recorded rather than fixed here. One was a genuine miss of mine. sigframe-math.h claimed the frame's field layout "is checked by a golden-layout test". No such test exists, and I had written that correction once already; the edit was an unguarded string replacement that silently matched nothing after the text had been reworded, so it never landed. The header now states the gap, which TODO.md already tracks. The contract-check plumbing had two holes worth closing: - gva-math.h reached its checks through assert.h with NDEBUG undefined. That enabled every unrelated assert in the including translation unit and left NDEBUG cleared for whatever it included next. Calling abort() directly cannot be switched off by a caller's -DNDEBUG, needs no header, and fails with SIGABRT specifically. - test-gva-contracts.c accepted any terminating signal as a rejection. A mis-wired check would fall through into the arithmetic the precondition guards, and gva % granule with granule == 0 is undefined behavior that can itself kill the child, which would have been scored as the check firing. It now requires SIGABRT, which is why abort() is the right primitive above. Verified by neutering the check: six cases fail where the old test reported them caught. check-acsl-coverage.py scanned only the parameter list for a plain char, so a plain char local or return type in a proved function passed the gate. It now scans the whole definition with comments and literals blanked first. A char reached through a typedef still needs a C front end, and the comment says so instead of implying full coverage. Two comments were wrong: FUSE_MAX_PAGES is the capability flag that enables max_pages negotiation, not a page count, and sigframe_base leaves *base untouched on failure rather than zeroing it. CI time, which is what the mutation step actually cost: The step ran over 43 minutes against a 60-minute job timeout, not the 5 minutes the comment claimed. Two compounding causes. --jobs defaulted to half the cores, and a 3-core runner resolves that to 1, so the set ran serially where it had been 4-way parallel locally. And a caught mutation is the expensive case: the prover grinds against goals it cannot discharge until the per-goal timeout expires, measured at 71s per caught mutation against 15s to prove the same file unmutated. Mutation runs now use a 5s per-goal timeout instead of 30s, which is sound because the baseline control runs at the same value: a timeout too tight for correct code fails the baseline and reports SETUP FAILED rather than scoring a mutation as caught. With --jobs set explicitly in CI, the full set drops from 318s to 149s locally and all 40 mutations are still caught.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
All five findings were valid. The important one reverses my own change from the previous commit. Lowering the per-goal prover timeout for mutation runs is unsound, and the argument I gave for it only covered one direction. A broken contract is never refuted; the goal simply becomes unprovable and the prover grinds until the budget expires, so a caught mutation is reported as a timeout. Measured: every caught mutation in the table fails with [Timeout] at both 5s and 30s, never with a definitive verdict. A goal that is merely hard but still true times out identically, so a shorter budget silently converts a genuine MISS into a "caught" and hides the gap this file exists to find. Proving the unmutated file at the short budget shows the budget suits correct code, not weakly-broken code. Reverted to the engineering timeout, with the reasoning recorded so the next person who sees the obvious speedup finds out why it is not taken. The CI cost is handled by parallelism alone, which is sound: 318s to 248s locally. MUTANT_JOBS now threads through the make target, so CI calls `make verify-mutants MUTANT_JOBS=4` instead of invoking the script behind make's back, which also makes the step name true again. Three smaller ones: - The brace matcher in the plain-char scan had no guard for a definition with no closing brace. It would have run to end of file and blamed one function for chars belonging to every function after it. Unterminated definitions are now reported as a parse failure instead. - Two headers pointed readers at TODO.md, which is a per-developer working doc and deliberately untracked, so it does not exist from the repository's point of view. They now state the gap directly. - The plain-char check is documented as a tripwire rather than as enforcement. It cannot see a char reached through a typedef or a macro, which is why the allowlist entries are hand-audited; the comment said so about typedefs but claimed more than it delivers.
Second pass on the one finding from the review round I answered by weakening the claim rather than strengthening the check. The complaint was that a proved function can hide a plain-char access behind a macro, so the gate does not enforce the invariant it describes. Rewording the comment resolved the mismatch; it did not close the hole. check-char-signedness.py closes it. Each proved source is compiled twice, once with -fsigned-char and once with -funsigned-char, and the emitted code compared. A source whose code is identical contains no plain-char access at all, which the same front end that expands the macros and resolves the typedefs settles outright. Verified against the case the regex cannot see: a char reached through a macro in gva-math.h is invisible to check-acsl-coverage.py and reported by this immediately. What the comparison does NOT mean is worth stating, because the first version of this script got it wrong and would have failed the build. A source that differs is not thereby broken. A correct read casts to (unsigned char) first, and that cast costs a mask under -fsigned-char and nothing under -funsigned-char, so correct code differs too. The compiler cannot separate a safe read from an unsafe one. So the result is a complete detector of plain-char USE, not of signedness dependence, and a source that reads any plain char goes on an allowlist carrying the audit that justifies it. Today that is 8 sources containing no plain char at all and one, gdbstub-rsp.c, that takes it off the RSP wire in four functions and casts at every read. That is exactly the invariant mk/analysis.mk records, now held by something other than a comment. The regex stays. It names the offending function, which is what makes a failure actionable, and the two run together under make verify; neither replaces the other and each says which half it covers.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
…diff Four review findings, all valid, and two of them show the char gate was measuring the wrong thing twice over. Comparing whole objects answers the wrong question. A unit like elf.c is full of ordinary code that reads a plain char quite properly, and judging the file reported that as though a proved function were at fault. It now compares per function, by splitting the disassembly on symbol labels, so the answer is about proved code and the report names the function. Comparing at -O2 lets the optimizer delete a plain-char read whose result is unused, so the objects agree while the source Frama-C reasons about still contains the read. Measured: a dead widening read is missed at -O1 and -O2 and caught at -O0. Those two together change what the gate means, for the better. At -O0 an explicit (unsigned char) cast emits the same mask under both settings, so a correctly written read compares equal and only a genuine dependence stands out. That is the invariant itself rather than a proxy, which is why the allowlist is gone: it admits no exception, and a proved function that depends on plain-char signedness needs the cast, not a waiver. All 31 proved functions pass with nothing waived. Also: the no-code guard tested object length, which an object with metadata and no code would pass, so it asks nm for defined symbols; and CC is now tokenized, so a wrapper or a flag-bearing override such as CC='cc -DTEST' works instead of arriving as stray arguments. The brace matcher in check-acsl-coverage.py ran on unpreprocessed source, so a definition whose #if branches open braces unevenly never balanced and would have failed make verify on perfectly good code. It now narrows to the signature rather than erroring, which is the right call now that the compiler gate covers bodies completely. Separately, on CI cost. verify-mutants is slow because each caught mutation grinds unprovable goals to the per-goal timeout, and that timeout cannot be lowered without making "caught" unsound. Narrowing -wp-fct to the mutated function does not help either: the cost is the one timeout, not the goal count, and it trips MIN_GOALS. What does help is not re-verifying targets a branch never touched, so MUTANT_SINCE scopes the run to sources that differ from a ref and CI passes the PR base. The full set still runs on a push to the base, so the guarantee is never weaker than the branch being merged into. This branch creates almost every proved source, so it only drops 40 to 34; a later PR touching one header would run four.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
The verify job failed on the last commit, and the scoping I added for CI
cost is what broke it:
fatal: <base>...HEAD: no merge base
cannot diff against <base>
make: *** [verify-mutants] Error 2
Three-dot diff asks git for a merge base, which a CI shallow clone does
not have. Two-dot asks what this actually wanted, which files differ
between two trees, and needs no ancestry. Reproduced the exact failure
locally against a commit with no common history, and confirmed two-dot
works where three-dot reports the same fatal.
The deeper mistake was making a speed-up able to fail the gate at all. It
now falls back to running everything when it cannot work out what to
skip, and CI only passes a base once the fetch for it succeeded. An
optimization that cannot determine scope must do all the work; failing,
or skipping silently, both turn it into a correctness problem.
Filtering on the target's source path alone was too narrow in the same
way. verify-rsp reads utils.h, so a change there can flip a verdict while
gdbstub-rsp.c is untouched, and that mutation would have been skipped.
Scoping now uses each target's full proof-input set, which VERIFY_*_SCAN
already records, and any change to the harness or the proof config runs
the whole set regardless.
check-acsl-coverage.py's brace matcher degrades to the signature when
#if branches leave braces unbalanced, and that was only safe if something
else covered the body. Nothing did: check-char-signedness.py was a
separate target, so `make verify-gva` on its own had no body coverage. It
is now part of the shared recipe, so every verify-* target carries it.
That change needed one more thing, which the baseline control caught
immediately: mutation runs override NAME for the log path, so passing
NAME to the signedness check asked about a target that does not exist and
all nine baselines failed. NAME is the log name and TARGET is the
identity; they were one variable doing two jobs.
Also: otool missing now degrades to the error the surrounding code
already reports rather than a traceback, since that binary is
load-bearing for the whole gate.
make check fails locally on test-thread-churn under this session's memory
pressure and passes standalone in 0.8s; all four CI Runtime jobs pass it.
That is the munmap-zeroing item already recorded, not a regression here.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
Three findings, all valid. --target on check-char-signedness.py silently emptied the target dict on a typo and fell through to "no proof targets found in mk/analysis.mk", which blames the wrong file. It now checks membership first and lists the valid names. HARNESS_FILES was missing mk/toolchain.mk, which sets CC, and CC is exactly what check-char-signedness.py compiles the probe with. A change there can flip a verdict with no proved source touched at all. The bigger one: target_inputs() trusted VERIFY_*_SCAN as each target's complete dependency set. SCAN is hand-maintained, which is exactly the kind of thing that goes stale silently, a proved header gains an include, nobody remembers to mirror it into SCAN, and a mutation touching only the new file gets skipped with no diagnostic. It now runs `cc -MM` against each proved source and uses the compiler's own include closure instead. That is not a hypothetical improvement: elf.c and gdbstub-rsp.c both pull in headers SCAN never listed (debug/log.h, gdbstub-rsp.h), so the old filter was already narrower than it claimed to be, not just theoretically capable of becoming so. Verified: cc -MM on gva-math.h returns exactly itself, matching that it has no internal includes today; on gdbstub-rsp.c and elf.c it returns the wider set the SCAN lines were missing. Full mutation set stays 40 of 40 caught, all nine targets still prove.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
include_closure fell back to {src} whenever cc -MM failed to run or
produced output it could not parse. That is the same silent-narrowing
bug the SCAN-based approach had, just moved one layer down: {src} alone
is indistinguishable from a correctly-scanned header that genuinely has
no includes, so a broken scan and a clean one report the same shape and
the caller has no way to tell them apart.
include_closure and target_inputs now return None on any scan failure,
compile error or malformed -MM output alike, and the caller treats that
exactly like an unresolvable --changed-since ref: run the full mutation
set rather than guess. Verified directly against the function, a broken
compiler now returns None instead of {src}, and target_inputs returns
None for the whole map rather than hiding one broken target inside an
otherwise normal-looking result.
Also: include_closure hardcoded "cc" instead of using the configured
compiler, so it could disagree with what --cc was told to use. It now
takes cc through the same --cc flag and shlex tokenizing that
check-char-signedness.py already established, wired through
`make verify-mutants` via CC.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
include_closure() and compare() both called subprocess.run(cc + [...]) with no guard against cc itself being missing or non-executable. subprocess.run raises OSError before a CompletedProcess exists in that case, so the existing "if proc.returncode != 0" checks never execute and the whole harness crashes with an unhandled traceback instead of falling back the way every other scan failure here does. Found by agy review, reproduced directly in Python before and after the fix (crash, then a clean None / error tuple). check-char-signedness.py's main() also printed the same "depends on plain-char signedness" header whenever its failures list was non-empty, even when every entry was an infra error (bad compiler, otool missing) rather than a genuine signedness finding -- reproduced with --cc pointed at a nonexistent binary across all 9 targets, which correctly exits 1 but wrongly claimed a signedness dependency that was never checked. Split the single list into char_failures/infra_failures so the header matches what actually happened. make verify: 9/9 PROVED. make verify-mutants: 40/40 caught. make check: 70/71 (test-thread-churn is the known timeout flake under load; reran it standalone twice, both pass).
Every CI run on this branch pays the full 40-mutation cost: 40-57 min, against a 5-min outlier where MUTANT_SINCE actually got to scope the run. Measured across 7 recent runs of this PR's "Prove the gate bites" step. The reason is structural, not a regression: MUTANT_SINCE forces the full set whenever the diff touches mk/analysis.mk or scripts/check-mutants.py (the HARNESS_FILES fail-closed rule), and every commit in this review-response round touches one or both, since that is what the reviews are about. Splits the mutation gate into its own job, `needs: verify` so a broken baseline proof fails fast without spending nine runners mutating it, matrixed one leg per proof target (cmsg, elf, fuse, gva, netlink, rsp, sigframe, sockaddr, stack; fail-fast: false so one target's failure does not hide the others). Each leg now runs `make verify-mutants MUTANT_TARGET=<target>`, a new mk/analysis.mk variable that forwards check-mutants.py's existing --target flag (already used for local single-target runs, not previously exercised from CI). Wall-clock drops from the sum of all 40 mutations to roughly the slowest single target's share, at the cost of 9 parallel runners instead of 1. --target filters MUTATIONS before --changed-since is evaluated (scripts/check-mutants.py:672-674), so a shard's HARNESS_FILES fallback still only re-runs that shard's own mutations, not the full 40 -- confirmed locally: `--target cmsg --changed-since HEAD~1` prints "harness or proof config changed; running the full set" and lists exactly cmsg's 4 mutations, not all 40. Reviewed by Codex and agy before committing, since matrix behavior can't be fully exercised locally: - Codex flagged that splitting into per-target job names could drop the mutation gate from required status checks if branch protection names the old single job. Checked directly: `gh api repos/sysprog21/elfuse/branches/main/protection` returns "Branch not protected", and rulesets are empty, so nothing was enforced before this change either -- not a regression. - agy flagged the new per-shard log artifacts lacked retention-days, unlike 5 of the other 6 upload-artifact steps in this file. Added retention-days: 7 to match. - Both confirmed the opam cache populated by `verify` is reachable by the matrix legs (same cache key, needs: verify orders the save before the restores) and that MUTANT_SINCE + MUTANT_TARGET compose correctly. YAML validated with a real yaml.safe_load and actionlint; the only actionlint findings are pre-existing, in the untouched lint job.
There was a problem hiding this comment.
2 issues found across 4 files (changes from recent commits).
Prompt for AI agents (unresolved issues)
Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.
<file name=".github/workflows/main.yml">
<violation number="1" location=".github/workflows/main.yml:330">
P1: Mutation failures can be merged without blocking the PR if branch protection still requires only `Frama-C WP proofs (make verify)`, because the mutation gate is now a separate set of checks. A stable aggregate check that needs all matrix legs, or branch-protection entries for every leg, should be made the required gate.</violation>
<violation number="2" location=".github/workflows/main.yml:418">
P2: A PR that changes only this workflow can report a green mutation gate without running any mutants, including changes that remove a matrix target or alter its invocation. The changed-since scope should force the full mutation set when the workflow changes, such as by treating `.github/workflows/main.yml` as a harness input.</violation>
</file>
Tip: Review your code locally with the cubic CLI to iterate faster.
Re-trigger cubic
| # The matrix list is VERIFY_<T>_SRC's targets from mk/analysis.mk, hand-kept | ||
| # in step: a target missing here silently drops its mutation coverage from | ||
| # CI with no error, so add new proof targets to both places. | ||
| verify-mutants: |
There was a problem hiding this comment.
P1: Mutation failures can be merged without blocking the PR if branch protection still requires only Frama-C WP proofs (make verify), because the mutation gate is now a separate set of checks. A stable aggregate check that needs all matrix legs, or branch-protection entries for every leg, should be made the required gate.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At .github/workflows/main.yml, line 330:
<comment>Mutation failures can be merged without blocking the PR if branch protection still requires only `Frama-C WP proofs (make verify)`, because the mutation gate is now a separate set of checks. A stable aggregate check that needs all matrix legs, or branch-protection entries for every leg, should be made the required gate.</comment>
<file context>
@@ -305,21 +307,104 @@ jobs:
+ # The matrix list is VERIFY_<T>_SRC's targets from mk/analysis.mk, hand-kept
+ # in step: a target missing here silently drops its mutation coverage from
+ # CI with no error, so add new proof targets to both places.
+ verify-mutants:
+ name: Mutation gate (${{ matrix.target }})
+ needs: verify
</file context>
| # optimization. | ||
| base="${{ github.event.pull_request.base.sha }}" | ||
| if [ -n "$base" ] && git fetch --no-tags --depth=1 origin "$base"; then | ||
| make verify-mutants MUTANT_JOBS=4 MUTANT_TARGET=${{ matrix.target }} MUTANT_SINCE="$base" |
There was a problem hiding this comment.
P2: A PR that changes only this workflow can report a green mutation gate without running any mutants, including changes that remove a matrix target or alter its invocation. The changed-since scope should force the full mutation set when the workflow changes, such as by treating .github/workflows/main.yml as a harness input.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At .github/workflows/main.yml, line 418:
<comment>A PR that changes only this workflow can report a green mutation gate without running any mutants, including changes that remove a matrix target or alter its invocation. The changed-since scope should force the full mutation set when the workflow changes, such as by treating `.github/workflows/main.yml` as a harness input.</comment>
<file context>
@@ -330,20 +415,19 @@ jobs:
base="${{ github.event.pull_request.base.sha }}"
if [ -n "$base" ] && git fetch --no-tags --depth=1 origin "$base"; then
- make verify-mutants MUTANT_JOBS=4 MUTANT_SINCE="$base"
+ make verify-mutants MUTANT_JOBS=4 MUTANT_TARGET=${{ matrix.target }} MUTANT_SINCE="$base"
else
- make verify-mutants MUTANT_JOBS=4
</file context>
Two issues from cubic review 4883042273, both confirmed before fixing: check-char-signedness.py's main() returned inside the infra_failures block, so a target with a genuine plain-char signedness finding never reached the char_failures block when another target also had an infra error (bad compiler, otool missing) -- the real finding was reduced to its bare per-target row with the diagnosis and cast advice silently dropped. Reproduced by monkeypatching compare() to return a CHAR finding for cmsg and an INFRA error for elf in one run: only the ERROR header printed before the fix; both headers print after moving the return to the end. check-mutants.py's HARNESS_FILES did not include .github/workflows/main.yml, even though that file now decides, per CI matrix leg, which --target name reaches the script and whether --changed-since runs at all. A PR that only edits the workflow (a mistyped target, a dropped matrix entry, a MUTANT_TARGET that stops being forwarded) would verify against whatever proof sources it happens to touch, which is nothing when the PR is CI-only -- the exact silent-narrowing failure mode this file exists to close for every other harness input. Added it to HARNESS_FILES; reproduced with --changed-since HEAD~1 --target cmsg against the commit that touched the workflow, which now prints "harness or proof config changed; running the full set" and lists cmsg's own 4 mutations instead of silently reporting nothing to re-verify. The third finding in this review (branch protection dropping the mutation gate from required checks) was already checked and found inapplicable when Codex raised the same concern last round: `gh api repos/sysprog21/elfuse/branches/main/protection` returns "Branch not protected" and rulesets are empty, re-confirmed just now. Nothing enforced the old single job either, so the matrix split changes nothing here. make verify: 9/9 PROVED. make verify-mutants: 40/40 caught. make check: 70/71 (test-thread-churn is the known timeout flake under load; reran it standalone twice, both pass).
linux_errno() already returns the negative Linux errno (its own doc
comment says so, and 202 other call sites in the tree use it as
"return linux_errno();"). This function instead did
"return -linux_errno();", double-negating a failure back into a
positive value.
The one caller that checks the result, sys_mremap, does
"if (err < 0) { ...best-effort recovery...; return err; }" -- with the
double negation, that check was never true on this path's failure, so
hvf_remap_segments_best_effort's recovery was silently skipped and the
function fell through to hv_vm_map against a slab whose backing
restore may have failed.
Found during a project-wide analysis sweep; verified by reading both
the callee and the caller directly before fixing, and confirmed via
`make elfuse` that the one-line fix builds clean.
…rs table-driven
Three related path-handling cleanups from a project-wide analysis sweep:
path_tr_nofollow() (src/syscall/path.h) replaces the same
"(flags & LINUX_AT_SYMLINK_NOFOLLOW) ? PATH_TR_NOFOLLOW : PATH_TR_NONE"
ternary copy-pasted at 8+ call sites across fs.c, fs-stat.c, and
fs-xattr.c (the last already had it extracted to a local `nofollow`
bool, so the same helper covers both call shapes).
sys_openat_path's no-sysroot fast path called raw openat(AT_FDCWD,
pathp, ...) with the guest path string instead of tx.host_path, even
though path_translate_at had already been called and populated tx
above it. Not exploitable today -- the branch is gated on
!proc_get_sysroot(), and path_translate_at's own resolvers hand back
a relative path untouched when there is no sysroot to redirect into
(verified by reading sysroot_seed_host_path, which returns the path
unchanged whenever !proc_sysroot_snapshot() or the path is relative)
-- but it was a latent trap if this branch's guard conditions ever
change. Now routes through tx.host_path consistently.
proc_virtual_dir_path was an 11-way else-if chain hand-coding
/proc/self/*, /proc/net, and duplicate /proc/<pid>/* forms of the same
paths. Replaced with: a single pid-to-self prefix normalization (so
"/proc/<mypid>/..." is rewritten to "/proc/self/..." once instead of
every table entry needing a numeric-pid twin), a small
{canonical-path} table walked in a loop for the static cases, and one
dynamic branch left for /proc/self/task/<tid> since that needs numeric
parsing rather than a literal match. Traced every branch by hand
against the original to confirm no behavior changed (in particular,
that pid-to-self normalization only feeds the same lookup table the
old code's specific suffix checks fed, so nothing new is now
recognized that the original code rejected).
Verified: make elfuse builds clean; test-proc, test-proc-fidelity, and
test-procfs pass; full make check is 70/71 (test-thread-churn is the
pre-existing timeout flake under load, confirmed by rerunning it
standalone).
core/bootstrap.h and core/sysroot.h each included syscall/internal.h (492 lines of cross-module lock-ordering declarations and the FD table) for the sole purpose of getting LINUX_PATH_MAX for buffer sizing -- confirmed by reading both files in full; neither uses anything else internal.h declares. New src/syscall/linux-limits.h holds just that one constant. internal.h now includes it instead of defining the macro directly, so all 22 existing internal.h-reaching users keep working unchanged; the two core headers include the small header directly instead of dragging in syscall-layer coordination state they never touch. Verified: touching internal.h forces a near-full rebuild (36 includers), which ran clean; make check is 70/71 (the pre-existing test-thread-churn flake, not a regression).
proc_slot_alloc doubled capacity on exhaustion but never shrank; the
three lookup helpers (find_by_host_pid, find_by_guest_pid,
find_by_reserved) always scanned proc_table_capacity, so a historical
burst of concurrent children permanently taxed every future wait4/kill
lookup even after all of them had exited and been reaped.
proc_find_free_entry() already scans the whole table once per fork
admission; changed it to stop short-circuiting on the first free slot
so the same pass also learns whether every entry is idle right now.
When it is, and capacity has grown past the initial static buffer,
the grown array is freed and the table resets to the small initial
buffer -- the same reset proc_init() does at startup. This is safe
without new locking: every caller already holds pid_lock, and the
file's own documented invariant ("no pointer into this array survives
unlocking") means nothing can be holding a stale pointer once nothing
in the table is active or reserved.
Not free-running: the scan was already unconditional overhead paid by
posix_spawn and the guest memory IPC transfer that surrounds every
fork, so folding the emptiness check into the same pass costs nothing
extra on the common case (finds a free slot immediately, keeps
scanning trailing entries it already had to touch anyway to answer
"how many active").
Verified with an ad hoc 3-round stress test (not part of the permanent
suite): each round forks 20 children concurrently, forcing table
growth well past the initial capacity of 8, then reaps all of them
before the next round starts, exercising the shrink path three times
in a row with correct exit-code propagation throughout. Also ran
test-fork-exec, test-mt-fork, test-clone3, test-clone-childtid,
test-process-lifecycle, and test-cow-fork directly, plus full make
check (70/71, the pre-existing test-thread-churn timeout flake under
load, not a regression -- confirmed standalone).
fuse_node_ref_hold_locked and fuse_node_ref_drop_locked track how many outstanding FUSE_LOOKUP references the guest holds per nodeid, via a linear scan over session->node_refs[FUSE_MAX_NODE_REFS=4096] -- twice per hold (existing-entry search, then free-slot search) and once per drop. A large directory walk (ls -R over an sshfs/ntfs-3g/AppImage mount) degrades toward O(n^2) in outstanding refs, all under session->lock, serializing every other FUSE op on that session. Adds an open-addressing hash table (node_ref_hash[8192], linear probing, EMPTY/TOMBSTONE sentinels) mapping nodeid -> node_refs[] index, and a free-list stack (node_ref_free[4096]) for O(1) slot allocation. All access stays under session->lock as before -- this is a data-structure swap for the same single-threaded-at-a-time semantics, not a concurrency change. Two real bugs surfaced while stress-testing before this was trusted, neither of which the existing test-fuse-alpine suite would have caught (it doesn't exercise enough distinct nodeids or hold/drop churn to hit either): 1. The first version's insert had a comment claiming an open slot always exists because live entries never exceed FUSE_MAX_NODE_REFS. Wrong: tombstones accumulate independently of live count under hold/drop churn and can fill the table even at low live occupancy. Fixed with fuse_node_ref_hash_rebuild(), a full compaction that clears every tombstone by re-inserting the live entries, triggered whenever live+tombstone occupancy would reach 3/4 of the table. 2. fuse_node_ref_drop_locked did `memset(&node_refs[idx], 0, ...)` before calling fuse_node_ref_hash_remove(session, nodeid) -- but hash_remove's probe identifies the right hash slot by comparing node_refs[idx].nodeid == nodeid, and the memset already zeroed that field, so the comparison silently failed and the hash slot was never tombstoned. The slot looked permanently "live" in the hash table pointing at freed, reused node_refs[] data. Fixed by reordering: hash_remove first, then memset. Both were caught by a 2-million-operation randomized stress test (hold/drop/lookup, comparing against a naive linear-scan oracle) run standalone, not part of the tree -- it reliably aborted within a few hundred thousand operations before fix 1, and produced silent oracle mismatches before fix 2. Reran clean across 5 different seeds (10M total ops, 0 mismatches) after both fixes. Reviewed by Codex before committing given the two self-caught bugs warranted a skeptical second pass rather than trusting one clean stress run. It confirmed the reordering fix and the 3/4 threshold's termination argument, and found one more real issue: the tombstone counter wasn't decremented when an insert reused a tombstone slot, overestimating occupancy (safe direction -- more frequent rebuilds than strictly needed, not fewer). Fixed and reverified against the same 5-seed stress run. make elfuse builds clean; test-fuse-alpine passes; full make check is 82 passed, 0 failed, 2 skipped (of 84) -- test-thread-churn, the pre-existing timeout flake under load noted in earlier commits this session, did not trigger this run.
…hole call sys_msync was dispatched via SC_LOCKED, holding the single global mmap_lock (which also gates every thread's mmap/brk/munmap/mprotect) for the entire call -- including a real fsync(2) and an O(regions^2) diff-and-write pass comparing guest memory against the backing file. A guest thread calling msync(MS_SYNC) on a large file-backed shared mapping could stall every other thread's memory syscalls for however long the disk flush took. sys_msync now manages mmap_lock itself (dispatched via SC_FORWARD) and only defers the plain fsync(2) calls until after the lock is released, on duped fds -- matching the existing sc_sync_impl pattern in this same file for plain sync(2). Everything that touches guest memory (the coverage check, the diff-and-write pass in sync_shared_aliases_range, the cross-region refresh pass in refresh_shared_region_range) still runs entirely under the lock, unchanged from before. That scope came from a real critical bug in the first attempt, caught by Codex before it was trusted: the initial version snapshotted per-region host pointers (resolved once via host_ptr_for_gpa under the lock) alongside duped fds, then ran the diff/refresh passes against that snapshot AFTER releasing the lock. A duped fd keeps the underlying FILE alive across a concurrent munmap of the original mapping, but does nothing to keep the GUEST MEMORY at that host address attributed to the same region -- a concurrent munmap+mmap could hand the same host VA range to something else entirely while the unlocked diff pass was still reading it, silently writing the new mapping's bytes into the old file, or the old file's bytes into the new mapping. My own concurrency stress test (unrelated regions churning while msync ran) didn't exercise this, since it never targeted the SAME region msync was operating on; Codex's review caught it by reasoning through the ownership argument rather than needing a test to reproduce it. Two more issues surfaced across two further review rounds on the corrected version, both fixed: - The post-unlock fsync loop was skipping fsync entirely for already-queued regions if a LATER region's diff/refresh failed and broke the loop, silently downgrading durability the original inline-fsync-per-region code guaranteed for the earlier regions. Fixed: every queued fd is fsynced unconditionally; only the first failure (diff/refresh or fsync) becomes the reported error. - The fsync fd-scratch array was allocated unconditionally, so a plain msync() or msync(MS_ASYNC) call -- which never fsyncs -- could newly fail with ENOMEM over an allocation it did not need. Fixed: allocated only when MS_SYNC is set. Also fixed a bug caught before any review, while writing the first version: the scratch array was sized from g->nregions read BEFORE mmap_lock was acquired, letting a concurrent mapping grow nregions before the lock was actually taken and undersizing the array relative to the locked loop's own bound. Fixed by sizing to the fixed GUEST_MAX_REGIONS capacity instead. Verified: full make check is 82 passed, 0 failed, 2 skipped (of 84). A targeted concurrency stress test (not part of the tree) -- one thread looping msync(MS_SYNC) on a real file-backed MAP_SHARED region while another does 4000 rounds of mmap/mprotect/munmap on unrelated anonymous regions -- ran clean across 3 separate runs after this version, verifying final content both via the mapping and via a fresh pread bypassing it.
abi.h (819 lines) mixed two concerns that change at different rates and are needed by different consumers: the SYS_* Linux syscall-number dispatch table, and everything else -- errno values, open/mmap/AT_* flag constants, wire-format structs (linux_stat_t, linux_statx_t, etc.), and the FD table (fd_entry_t, FD_TABLE_SIZE, FD_* type tags). 36 files included it; a change to either half forced a rebuild of every one of them regardless of which half a given file actually used. Checked before doing this (not assumed): grepped every includer for literal SYS_* token usage, and separately confirmed which files expand the generated SYSCALL_TABLE_ENTRIES(_) X-macro from build/dispatch.h (that macro's body itself references SYS_* tokens as arguments, so a file expanding it needs SYS_* even without spelling out any SYS_* identifier itself). Result: only syscall.c (the dispatch switch) and debug/syscall-hist.c (re-expands the same macro for a name table) ever touch SYS_*. Every other includer wanted the other half only. src/syscall/linux-wire.h now holds that other half verbatim (moved, not rewritten). abi.h keeps just the SYS_* defines and the syscall_init/syscall_dispatch entry-point declarations. Every file that included abi.h for the wire half now includes linux-wire.h instead; syscall.c includes both; syscall-hist.c is unchanged (SYS_* only, confirmed it uses zero LINUX_*/linux_*_t/FD_* symbols). core/bootstrap.c, runtime/fork-state.c, and syscall/proc.c each call syscall_init()/syscall_dispatch() directly without otherwise needing abi.h's dispatch numbers, so they now include both headers too. A prior investigation pass into also splitting internal.h (locks/FD table vs. misc cross-module helpers) found that split isn't worth doing as scoped: the "misc helpers" are built directly on FD-table primitives, so a 2-way cut would still force nearly every one of internal.h's 33 includers to pull in both halves anyway, changing nothing about anyone's real rebuild scope. Left internal.h alone; if this is revisited it needs a genuinely different 3-way cut, scoped on its own. A header-only change like this fails at compile time, not at runtime, if an include is missing -- so the safety net here was `make clean && make elfuse` and a full `make check` (which alone compiles ~80 additional test binaries against the same headers), not runtime testing. Both are clean: make elfuse and make check build with zero compiler warnings; make check is 82 passed, 0 failed, 2 skipped (of 84), same as every other clean run this session. clang-format and cppcheck pass on every touched file (thread.h needed a manual reformat after the abi.h -> linux-wire.h rename shifted an aligned trailing comment column).
There was a problem hiding this comment.
3 issues found across 44 files (changes from recent commits).
Prompt for AI agents (unresolved issues)
Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.
<file name="src/syscall/mem.c">
<violation number="1" location="src/syscall/mem.c:1394">
P1: A failed slab restore is now reported as success, so overlay teardown can continue with the host VA still backed by the file and later guest writes can corrupt that file. Returning the negative Linux errno preserves the helper's documented contract and lets callers abort cleanup.</violation>
</file>
<file name="src/syscall/linux-limits.h">
<violation number="1" location="src/syscall/linux-limits.h:16">
P3: The comment claims core/guest.c uses a literal 4096, but guest.c sizes pages via the PAGE_SIZE/GUEST_PAGE_SIZE macros and has no literal 4096. Update the comment to reference only core/stack.c so it does not mislead a maintainer hunting for the literal.</violation>
</file>
<file name="src/syscall/abi.h">
<violation number="1" location="src/syscall/abi.h:14">
P3: The new header comment claims syscall.c and syscall-hist.c "are the only files needing both, and each already includes linux-wire.h separately for that half," but that is factually inaccurate: syscall-hist.c does not include linux-wire.h at all (it uses zero wire symbols), and proc.c, fork-state.c, and bootstrap.c also include abi.h (for the syscall_dispatch/syscall_init entry-point declarations) while needing the wire half in addition. Please correct the comment so it doesn't mislead a future refactor about which files depend on which half.</violation>
</file>
Tip: Review your code locally with the cubic CLI to iterate faster.
Re-trigger cubic
| } | ||
| if (p == MAP_FAILED) | ||
| return -linux_errno(); | ||
| return linux_errno(); |
There was a problem hiding this comment.
P1: A failed slab restore is now reported as success, so overlay teardown can continue with the host VA still backed by the file and later guest writes can corrupt that file. Returning the negative Linux errno preserves the helper's documented contract and lets callers abort cleanup.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At src/syscall/mem.c, line 1394:
<comment>A failed slab restore is now reported as success, so overlay teardown can continue with the host VA still backed by the file and later guest writes can corrupt that file. Returning the negative Linux errno preserves the helper's documented contract and lets callers abort cleanup.</comment>
<file context>
@@ -1383,7 +1391,7 @@ static int hvf_restore_slab_backing(guest_t *g, uint64_t ipa, uint64_t len)
}
if (p == MAP_FAILED)
- return -linux_errno();
+ return linux_errno();
return 0;
}
</file context>
| #pragma once | ||
|
|
||
| /* Linux PATH_MAX (4096): used for path buffer sizing in syscall handlers. | ||
| * Literal 4096 in core/guest.c and core/stack.c means actual page size, not |
There was a problem hiding this comment.
P3: The comment claims core/guest.c uses a literal 4096, but guest.c sizes pages via the PAGE_SIZE/GUEST_PAGE_SIZE macros and has no literal 4096. Update the comment to reference only core/stack.c so it does not mislead a maintainer hunting for the literal.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At src/syscall/linux-limits.h, line 16:
<comment>The comment claims core/guest.c uses a literal 4096, but guest.c sizes pages via the PAGE_SIZE/GUEST_PAGE_SIZE macros and has no literal 4096. Update the comment to reference only core/stack.c so it does not mislead a maintainer hunting for the literal.</comment>
<file context>
@@ -0,0 +1,19 @@
+#pragma once
+
+/* Linux PATH_MAX (4096): used for path buffer sizing in syscall handlers.
+ * Literal 4096 in core/guest.c and core/stack.c means actual page size, not
+ * this.
+ */
</file context>
Suggested change
| * Literal 4096 in core/guest.c and core/stack.c means actual page size, not | |
| * Literal 4096 in core/stack.c (AT_PAGESZ) means actual page size, not |
| * syscall implementation file needs that half and never touches SYS_* at | ||
| * all, so splitting them keeps a change to one from forcing a rebuild of | ||
| * files that only wanted the other. syscall.c and syscall-hist.c are the | ||
| * only files needing both, and each already includes linux-wire.h |
There was a problem hiding this comment.
P3: The new header comment claims syscall.c and syscall-hist.c "are the only files needing both, and each already includes linux-wire.h separately for that half," but that is factually inaccurate: syscall-hist.c does not include linux-wire.h at all (it uses zero wire symbols), and proc.c, fork-state.c, and bootstrap.c also include abi.h (for the syscall_dispatch/syscall_init entry-point declarations) while needing the wire half in addition. Please correct the comment so it doesn't mislead a future refactor about which files depend on which half.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At src/syscall/abi.h, line 14:
<comment>The new header comment claims syscall.c and syscall-hist.c "are the only files needing both, and each already includes linux-wire.h separately for that half," but that is factually inaccurate: syscall-hist.c does not include linux-wire.h at all (it uses zero wire symbols), and proc.c, fork-state.c, and bootstrap.c also include abi.h (for the syscall_dispatch/syscall_init entry-point declarations) while needing the wire half in addition. Please correct the comment so it doesn't mislead a future refactor about which files depend on which half.</comment>
<file context>
@@ -4,15 +4,22 @@
+ * syscall implementation file needs that half and never touches SYS_* at
+ * all, so splitting them keeps a change to one from forcing a rebuild of
+ * files that only wanted the other. syscall.c and syscall-hist.c are the
+ * only files needing both, and each already includes linux-wire.h
+ * separately for that half.
*/
</file context>
fork_ipc_recv_fd_table (src/runtime/fork-state.c): the loop installing received fds into fd_table skipped an entry whose guest_fd failed RANGE_CHECK via a bare `continue`, never closing the already-received host_fds[i]. Every other rejection path in the same loop (synthetic type drop, dup failure, fdopendir failure) closes the corresponding host fd first; this was the one path that didn't, leaking an inherited host fd for the life of the child process on a corrupted or malformed fork IPC payload. spawn_capture_stdout (src/core/sysroot.c): a read(2) failure other than EINTR broke out of the capture loop but the function still fell through to waitpid and returned 0 (success), silently treating a genuine read error the same as clean EOF. The function's own contract is <0 on error; a real I/O error now reports as one instead of returning success with a possibly-truncated buffer. Found by a fresh maintainability sweep of areas the prior analysis pass this session hadn't covered (src/runtime/, src/core/rosetta.c and sysroot.c, src/syscall/net*.c, src/debug/); independently verified by reading both functions directly before fixing, not taken on the sweep's word. make elfuse builds clean; make check is 70/71 (test-thread-churn, the pre-existing timeout flake under load, not a regression); ran test-mt-fork (3x) and test-fork-lowbase directly to exercise fork_ipc_recv_fd_table, and test-fuse-alpine (which drives sysroot.c's mount/case-sensitivity probing path) -- all pass.
…arden msync's deferred fsync An adversarial self-review of this session's own recent commits (run after /sc:analyze's fixes were already committed, specifically to catch anything that survived into the final diffs) found a HIGH severity memory-safety regression introduced by the proc_table shrink-on-idle change: proc_deactivate_slot_if_matches(int slot, pid_t host_pid) indexed proc_table[slot] with no bounds check. Its callers capture a raw table index while holding pid_lock, release the lock, call a wait4() that can genuinely block (proc_autoreap_exited_children's wait4(..., 0, ...) has no WNOHANG), then call this function with the stale index on return. If every entry in the table happens to go idle during that unlocked window (another reaper finishes this exact slot, or the child was already reaped concurrently and the ECHILD path fires) and a concurrent fork triggers the shrink, proc_find_free_entry frees proc_table and repoints it at the small 8-entry proc_table_initial static buffer -- making the stale index (which could be well above 8 for a table that had grown from a historical burst) out of bounds for the array proc_table now points to. Reading it is UB into whatever static storage follows; if the garbage there happens to satisfy the host_pid re-check, it's an out-of-bounds write of false to .active. Fixed by dropping the slot parameter entirely: the function now looks up the entry by host_pid via the existing proc_find_host_entry helper (already bounded to [0, proc_table_capacity) and already checking .active), which is immune to the array being resized regardless of how long the caller held the raw index. Updated all 8 call sites and removed the two now-dead `int slot = (int) i;` locals. A second, independent review round (after this fix, given the severity, before trusting it) found a sibling of the exact same pattern in sys_waitid that the first pass missed entirely: its else-arm does the identical unlock/wait4(WNOHANG)/relock dance, then used proc_table[i] directly at two points after the relock. Fixed the same way, via proc_find_host_entry(host_pid) and proc_find_host_entry(ret) instead of the stale i. A third review pass specifically grepped the file for every remaining "unlock pid_lock ... later index proc_table[i]" pattern and found no further instance (proc_deferred_reap_poll's post-relock proc_table[i] use already re-validates "i < proc_table_capacity" first, which is the correct defensive pattern this fix brings the other two call sites up to). Also from the same shrink logic: proc_find_free_entry's any_live check only tested .active and .reserved, missing .host_reap_pending -- an entry can have active=false (already consumed by wait4) while still needing a deferred host wait4(WNOHANG) reap via proc_deferred_reap_poll, which scans by host_reap_pending alone. Shrinking past such an entry would strand a real host zombie process until elfuse itself exits. Fixed by adding host_reap_pending to the condition. Smaller findings from the same review rounds, fixed alongside: - sys_msync's deferred-fsync fds were opened via plain dup(), not O_CLOEXEC, so a concurrent execve on another vCPU thread in the dup-to-close window could inherit the backing file into the new image. Switched to fcntl(fd, F_DUPFD_CLOEXEC, 0). - dup/fcntl failure was reported as the syscall's own error (an -EMFILE/-ENFILE msync(2) never defines), even though mmap_lock was still held and the region still valid at that point. Added a fallback to a direct, non-deferred fsync() on dup failure, matching what the pre-optimization code did for that region. - Multiple regions sharing one backing file each got their own dup + fsync. Added a dedup check via the existing same_backing_file() helper so one file gets fsynced once regardless of how many regions in range back onto it. - The fsync-fds scratch array was sized to the fixed GUEST_MAX_REGIONS (4096) and allocated before mmap_lock, to sidestep a pre-lock g->nregions read racing a concurrent grow. Moved the allocation to after the lock is held and the coverage check passes, sized to the now-stable g->nregions -- smaller allocation on the common case, still correct. - proc.c used ~80 LINUX_*/linux_*_t tokens while only getting them transitively through internal.h's own include of linux-wire.h. Added the direct include. This is the fourth review pass across this session's proc_table/msync work (first pass when each was originally written, a Codex round on msync specifically that caught an earlier critical bug, this adversarial pass, and a confirmation pass on the sys_waitid fix) -- each one found something the previous had missed, which is the concrete reason this file keeps citing "an independent review caught this" rather than trusting a single pass on lock-adjacent code. make elfuse and make check build with zero compiler warnings; clang-format passes; make check is 82 passed, 0 failed, 2 skipped (of 84), the same clean baseline as every other run this session. test-process-lifecycle (20/20, zombie/orphan/subreaper/wait scenarios) and two ad hoc stress tests not in the tree -- a fork/reap-all/repeat proc_table grow-shrink cycle, and a waitid(P_ALL, WNOHANG) busy-poll specifically built to maximize overlap with concurrent table shrink/regrow -- all pass clean across multiple runs.
Two findings from a high-effort code-review workflow pass over this branch's diff: Six comments across gva-math.h, cmsg-math.h, fuse-math.h, and test-gva-contracts.c wrapped make targets in backticks (`make verify-gva`, `make check-contracts`, etc.), violating this project's documented rule: source comments are ASCII only, no inline backticks, code/path/symbol references written as plain text. Stripped the backticks; the target names read fine without them. .github/workflows/main.yml's verify-mutants job hand-lists the same nine proof target names mk/analysis.mk's VERIFY_<T>_SRC entries define, one per matrix shard. The job's own comment already admitted the failure mode: a target present in one list but not the other silently drops that target's mutation coverage from CI, with no error -- the run still reports green, having simply never mutated it. Ten targets exist today (VERIFY_ELF_SRC, GVA, RSP, CMSG, FUSE, STACK, SOCKADDR, NETLINK, SIGFRAME -- nine, matching the matrix -- plus the non-target VERIFY_UTILS_FCTS, correctly excluded since it has no _SRC), but nothing checked the two lists actually agreed. Added scripts/check-mutant-matrix-sync.py: parses mk/analysis.mk's VERIFY_<T>_SRC entries and main.yml's verify-mutants matrix.target list (regex, not PyYAML, matching every other check script in this tree that reads these two files as text), diffs the two sets, and fails with the specific target name(s) on either side of a mismatch. Wired into the existing "Lint (Linux)" job as a new step alongside the structurally identical "Syscall dispatch table consistency" check, which validates a different generated-vs-hand-written pair the same way. Verified the script both ways before wiring it in: confirmed a clean pass against the current, in-sync state, then temporarily deleted one matrix entry (stack) to confirm the script reports exactly that target name and exits non-zero, before restoring the file. make check is 82 passed, 0 failed, 2 skipped (of 84), the same clean baseline as every other run this session. actionlint and a real yaml.safe_load pass on the modified workflow file; black and a syntax check pass on the new script.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
cubic-dev-ai's PR review flagged a real gap in the guest_pid-agnostic fix from the previous round: proc_deactivate_slot_if_matches and sys_waitid's preservation/consumption paths looked up the process table entry by host_pid alone after re-acquiring pid_lock following an unlocked wait4. host_pid is a host OS pid number, and the OS can reuse it the instant wait4 reaps the original child -- if a second guest fork gets admitted on another thread during that same unlocked window and happens to land the just-freed host_pid, the lookup can match that unrelated, brand new child instead of correctly recognizing "the original entry is already gone." Fixed by pairing every post-unlock host_pid lookup with a guest_pid captured from the same original entry before the unlock, and requiring both to match: - proc_deactivate_slot_if_matches gained an expect_guest_pid parameter; updated at all 8 call sites, each of which already had the matching guest_pid in scope under a different local name (guest_pid, gpid, or entry_gpid). - sys_wait4's targeted-pid polling loop and sys_waitid's reap- preservation/WNOWAIT-consumption blocks: the three remaining direct proc_find_host_entry(...) calls after an unlock gained the same `&& entry->guest_pid == X` condition, using guest_pid/entry_gpid already captured in scope. A second review round (given the sensitivity of this code, now on its third external pass this session) found one more sibling: proc_deferred_reap_poll clears host_reap_pending after its own unlock/wait4(WNOHANG)/relock using an index-plus-host_pid check that was already bounds-guarded (not the earlier OOB class) but still vulnerable to the same host_pid-reuse wrong-entry match, which could clear an unrelated child's pending-reap flag and strand the real zombie. Fixed the same way: capture guest_pid before the unlock, require it on relock alongside the existing capacity and host_pid checks. Checked and confirmed NOT needing this fix: proc_mark_child_exited already re-validates guest_pid after its own unlock/relock (pre- existing correct code), and proc_host_to_guest_pid is a single atomic lock/lookup/unlock with no intervening unlock window for reuse to occur in. Also from the same review: scripts/check-mutant-matrix-sync.py converted the parsed matrix.target list straight to a set, so two identical entries would silently compare as in-sync with mk/analysis.mk's one entry, hiding a hand-edit that doubles that target's CI job. Fixed by collecting into a list first, checking for duplicates, and only converting to a set once none are found; reproduced by temporarily duplicating one matrix entry and confirming the script reports exactly that duplicate and exits non-zero, before reverting. This is the fifth review pass across this session's proc_table/msync work; each of the last three found something the previous had missed (a stale-index OOB, a sys_waitid sibling of it, and now this host_pid-reuse class across four call sites). Two independent confirmation passes after this round's fixes found no further gap. make elfuse builds clean with zero warnings; make check is 82 passed, 0 failed, 2 skipped (of 84), the same clean baseline as every run this session. Re-ran the fork/reap grow-shrink stress test and the waitid(P_ALL) busy-poll stress test from the previous round against this version -- both clean across multiple runs.
There was a problem hiding this comment.
1 issue found across 2 files (changes from recent commits).
Prompt for AI agents (unresolved issues)
Check if these issues are valid — if so, understand the root cause of each and fix them. If appropriate, use sub-agents to investigate and fix each issue separately.
<file name="src/syscall/proc.c">
<violation number="1" location="src/syscall/proc.c:2012">
P1: Host-PID reuse can leave the original child active and make a later wait report the new child under the old guest PID. Because this condition checks only the first host-PID match, it should search for the `(host_pid, guest_pid)` pair in one scan, including the duplicated autoreap and `waitid` paths.</violation>
</file>
Tip: Review your code locally with the cubic CLI to iterate faster.
Re-trigger cubic
| guest_pid = proc_table[slot].guest_pid; | ||
| proc_table[slot].active = false; | ||
| proc_entry_t *entry = proc_find_host_entry(host_pid); | ||
| if (entry && entry->guest_pid == expect_guest_pid) { |
There was a problem hiding this comment.
P1: Host-PID reuse can leave the original child active and make a later wait report the new child under the old guest PID. Because this condition checks only the first host-PID match, it should search for the (host_pid, guest_pid) pair in one scan, including the duplicated autoreap and waitid paths.
Prompt for AI agents
Check if this issue is valid — if so, understand the root cause and fix it. At src/syscall/proc.c, line 2012:
<comment>Host-PID reuse can leave the original child active and make a later wait report the new child under the old guest PID. Because this condition checks only the first host-PID match, it should search for the `(host_pid, guest_pid)` pair in one scan, including the duplicated autoreap and `waitid` paths.</comment>
<file context>
@@ -1983,22 +1983,33 @@ int write_rusage_to_guest(guest_t *g, uint64_t gva, const struct rusage *ru)
pthread_mutex_lock(&pid_lock);
proc_entry_t *entry = proc_find_host_entry(host_pid);
- if (entry) {
+ if (entry && entry->guest_pid == expect_guest_pid) {
guest_pid = entry->guest_pid;
entry->active = false;
</file context>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary by cubic
Adds machine-checked proofs for critical arithmetic paths and enforces them in CI with mutation testing. Further hardens process management and CI checks.
New Features
src/core/stack-math.h,src/syscall/cmsg-math.h,src/syscall/fuse-math.h,src/syscall/netlink-math.h,src/syscall/sigframe-math.h,src/syscall/sockaddr-math.h; targets:verify-stack,verify-cmsg,verify-fuse,verify-netlink,verify-sigframe,verify-sockaddr,verify-gva.make verify-mutantssharded one job per target; supportsMUTANT_JOBSandMUTANT_SINCE; requires UNPROVED verdicts; inputs come from the compiler’s include closure; harness inputs includemk/toolchain.mkand.github/workflows/main.yml.verify-mutantsYAML in sync withmk/analysis.mktargets, and rejects duplicate matrix entries.Bug Fixes
guest_pidon relock; coversproc_deactivate_slot_if_matches, targeted waits insys_wait4/sys_waitid, and deferred-reap polling.guest_fdis out of range.read(2)error as failure instead of success with a truncated buffer.host_reap_pendingin “any live” checks.F_DUPFD_CLOEXEC, dedup per backing file, fall back to directfsyncon dup failure, and size scratch arrays after takingmmap_lock.Written for commit 76ca8d1. Summary will update on new commits.