Conversation
![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.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
jserv
force-pushed
the
formal
branch
2 times, most recently
from
August 14, 2026 01:29
e66c861 to
8a14d43
Compare
procemu.c had grown to 4759 lines carrying three interceptors and a pty side table that shares nothing with them: /proc, /sys and /dev synthesis on one side, and on the other a keepalive table, a shared segment, slave accounting and the /dev/pts staging directory. The pty half moves out whole. procemu-internal.h carries the eight declarations the two halves still exchange, and the scratch-directory registry gains a named entry point so the pty side reaches it without the five statics behind it.
The loop every syscall passes through ran to 1178 lines, which makes it simultaneously the riskiest function in the tree to modify and the least readable. Five of its cases handle an exception and are otherwise self-contained: the MRS trap, the system-instruction trap, the W^X toggle, BRK from EL0, and the bad-exception halt.
Nine proof targets read their sources from files named foo-math.h, each sitting beside the .c it had been split out of. The suffix described how the file came to exist rather than what it is for, and the scattering left no way to ask what the tree actually proves. They move to src/proved/<name>.h, and check-proof-targets.py enforces membership in both directions: a header there that no target proves, and a target naming a file git does not track. Seven targets join them (align, dirent, fdset, iov, pathdepth, slice, timespec), taking the proved surface to 590 obligations over 37 functions, with 88 mutations showing those contracts constrain something rather than merely parse. Writing the contracts found four defects the tests did not. pselect6 honored fd_set bits above nfds, which Linux ignores, so it polled descriptors the caller never named and returned EBADF when one was closed; it also bounded nfds by the host FD_SETSIZE rather than the fd table size, two constants that are both 1024 on macOS and are not the same constant. ppoll and pselect6 truncated a sub-millisecond timeout to poll(0), turning a 500 microsecond wait into a spin. linux_timespec_to_ns_sat overflowed signed 64-bit arithmetic on its way to saturating. align_up_ok rejects only what it must. Padding by align - 1 before testing for overflow refuses an address that is already a multiple and lies within align - 1 of the top of the address space, where rounding up is a no-op that cannot carry. Counting in multiples is exact, and one syntactic k * align hands the alignment postcondition its witness; reaching the same value by adding align to a floor computed earlier needs distributivity the provers do not apply. The proved helpers are used where the bound is a fact about the input, not a restatement of what the caller already established. Guarding fdtable.c's one-line bitmap setters that way put the check on the harmless write, since fd_init_entry indexes fd_table with the same fd on the next line and cannot be guarded from inside a bitmap setter; an analyzer reading the pair then has to assume the table write can land anywhere. Those setters index directly, and fdset.h states the distinction so the next call site does not have to rediscover it. The proof and mutation gates stop keeping a second copy of the target list. mk/analysis.mk derives it from its own VERIFY_<T>_SRC variables, scripts/analysis-mk.py is the one reader of those, and the CI matrix is fromJson of "make print-verify-targets" rather than a hand-kept list that silently dropped a target's coverage when it fell out of step.
recvmmsg and epoll_pwait2 shared syscall_timeout_ms_or_forever, which maps an effectively-infinite request onto poll's -1. That mapping earns its keep in epoll_pwait2, where a negative timeout selects the 200 ms re-arm loop that re-checks exit_group, pending signals, futex interrupts and pty hangup. recvmmsg has no such loop: it waits in a single poll, so -1 parked it there with nothing to wake it, on a call the guest had asked to bound. It takes the saturating conversion now, which is still far past any real timeout but is actually reached.
pty_keepalive_table holds a row per master host fd, but three of the fields on it describe the pty rather than the master: the guest slave count, the seen flag, and the shared segment. Aliased masters get a row each -- dup, dup2, F_DUPFD, an SCM_RIGHTS adopt, a fork restore -- while the counting paths took "the first row in table order for this minor". So a count could be recorded against one row and handed back to the segment by another row's destruction. Closing one alias of a master then reported a hangup with the slave still open: poll returned POLLHUP and read returned EIO where Linux gives EAGAIN. Ordering the rows the other way lost the hangup instead, because the release found a fresh alias at a lower index holding no count and stopped there. A slave open that failed after the intercept had already recorded it left the count behind for good, and the master could never hang up again; O_DIRECTORY on a slave path reaches that, since the host open succeeds and only the type check rejects it. Every counting path now resolves the same accounting home for a minor: the row already holding a count, else one that has seen a slave, else the first. Ranking a row that has seen a slave above one that has not is what stops a new alias at a lower index from displacing a home whose count has just fallen to zero. A master close hands its count to another row for the same pty, and keeps the row as a master-less home when there is none. An heir mapping no segment cannot take a count that was contributed to one; in the other direction the segment learns about the count as it arrives. Reusing a row for the minor it already describes keeps its accounting rather than detaching it, except after a fresh host allocation, where the minor only returns once every fd on it is gone. The row is released once its last counted slave closes, which is what gives back the retained slave fd that pins the macOS tty. Nothing did before, so the pin outlived every use of it. That is worse than a leak: it keeps the tty half-alive after the master is torn down, and a slave open against it blocks rather than failing, so a child consulting its own pts path after the pty is gone waits forever. One case this narrows deliberately -- a child that closes every slave it holds and then reopens the path gets ENOENT, where Linux would allow it while some process still holds the master. The child cannot see that master, so its own count is the only signal it has. Two lifetime bugs sat alongside. pty_keepalive_register reported through errno, which its insert path cannot do honestly: pty_shared_attach joins an existing segment by letting an O_EXCL create fail with EEXIST and reopening, and nothing clears errno after, so a successful insert during fork restore came back as EEXIST and the caller closed an fd the table had already recorded. The number was then reused, and the guest's next open of its slave either failed or aliased an unrelated file. It returns the PTY_REG_* status instead. Separately, pty_open_slave consumed a fork-child's one-shot mapping whether the open succeeded or failed, so a child that reopened its slave, stat'd its own pts path, or read /dev/pts after the first open got ENOENT while still holding a live slave on that pty. The mapping is given up only on failure now. /dev/pts is served from a staging directory of placeholder files so getdents64 lists the right names, and the open and stat intercepts key on an absolute path, so anything measured against a descriptor for it reached a placeholder: fstatat reported a 0444 regular file rather than a character device, and openat returned that file rather than the slave. Stamping the guest spelling puts relative calls back through the intercept, for a directory fd and for a cwd alike, which is where the pty semantics and the accounting live. proc_pty_forget_host_fd replaces the four places that hand-paired the master and slave cleanups. A host fd that never becomes a guest fd has to leave both tables, the call site cannot tell which one holds it, and calling one alone is silent either way: a leaked keepalive slave, or a phantom count that suppresses the hangup for good.
make verify ran its sixteen targets one after another although each is a separate frama-c process writing its own log and sharing nothing. Only invocations that remembered -j got the parallelism. It recurses with -j itself now, and adds one only when the caller brought none: a forced -j in a submake makes it drop the inherited jobserver and start that many processes whatever the outer limit was. 46.6s to 14.4s here. Make records no -j for -j1, so that spelling still parallelizes under the 3.81 macOS ships; VERIFY_JOBS=1 is the way to ask for serial under either. Each mutation re-proved every function in its target when WP proves each function against its callees' contracts rather than their bodies, so editing a body can only move that one function's goals. Mutations prove just the function they name. Editing a contract does move its callers' goals, and no entry names the caller, so those stay at full scope; ACSL living in comments is what makes them detectable. The narrowing is arranged so it cannot change a verdict rather than merely being argued not to. A mutation the narrow run fails to catch is re-run over the whole target before it may read as MISSED, so the fast path carries the common case and a wrong scope costs time instead of coverage. Misdirecting a mutation's scope on purpose still reports it caught. 3m36s to 2m16s, all 88 still caught.
Frama-C has no Apple SDK, so every source reaching guest.h or thread.h stopped at a missing Hypervisor header before parsing began, and its portable libc omits both the type-generic __atomic_*_n builtins and a few Darwin constants the tree calls. An absent builtin is worse than an absent header: the call parses as an implicit declaration whose argument types are inferred per translation unit, so each file loads on its own and the project refuses the moment two of them infer different widths for the same name. frama-c-stubs declares what is missing and nothing else. gcc-atomics.h pulls in Frama-C's own __fc_gcc_builtins.h for the builtins it does model and stdatomic.h for the _Atomic qualifier, where Frama-C states the qualifier is ignored, so that concession is the analyzer's rather than one invented here; it adds only the generics with no entry at all. Values in the stubs are the real ones where the tree could observe them. Outside src/ deliberately: a compile resolves headers through -Isrc and would find a stub shadowing the SDK header the binary must link against. Only FRAMAC_STUB_DIR reaches them. A name none of them declares fails with "Cannot resolve variable", which is how the next one gets found.
frama-c-stubs/macos-libc.h says its values are Darwin's real ones so they cannot collide with another arm of a switch the proofs walk. That claim was wrong the day it was written: ETOOMANYREFS was given 62, which is Darwin's ELOOP, and both are arms of the same linux_errno switch. Nothing caught it because nothing was checking, and a build never will. The analyzer does not link, so a wrong value cannot fail one; it changes what the proofs reason about instead. Two arms sharing a value makes one look unreachable, and a proof over that switch is then about a program nobody ships. That is the shape of error this tree already gates with a script rather than a comment. Hung off $(VERIFY_RULES) rather than the top-level verify target, which is what makes it run at all: CI invokes "make verify-<target>" per matrix leg and "make verify-mutants", never bare "make verify". As a phony prerequisite shared by every rule it still executes once per invocation, so proving one target pays for one SDK query.
The extent was computed as "(uint16_t) (RTA_HDRLEN + datalen)" and only the aligned result was checked against the space left. For datalen at or above 65532 that cast wraps: the total comes back as 3 or less, the aligned value as 4, the space check passes, and the payload memcpy then writes up to 65535 bytes into a buffer with 4 bytes free. Nothing reaches it. The five call sites pass 4, 16, or an interface name from getifaddrs. That is unreachable by caller provenance, which is the argument netlink_msg_span directly above it was written to stop relying on, so this gets the same treatment rather than a comment. netlink_attr_extent states that a non-zero result means the total is RTA_HDRLEN + datalen, fits the 16-bit wire field, and that the aligned extent fits the buffer. The caller's remaining cast to rta_len is then lossless exactly when it returned non-zero, and both writes land inside max. Both halves of the guard carry weight and both are mutation covered: dropping the wire-field ceiling reproduces the wrap, dropping the space check runs the payload past the buffer.
netlink.h proved the rtattr arithmetic and its UNPROVED line said the walks around it stayed test-covered. Both can be proved now that netlink.c parses. nl_parse_link_filter reads an rtattr chain out of bytes the guest wrote; nl_complete_span walks the reply buffer. Their contracts state what the callers already guarantee, and the loop annotations state what the walk maintains: for the parse, that off stays bounded by reqlen so the C loop test cannot wrap, and that the name copy leaves room for its terminator. nl_put_attr's payload precondition restates memcpy's own predicate from Frama-C's string.h rather than a hand-written \valid_read, because datalen may be 0 and an empty range says nothing about the pointer while memcpy still demands \object_pointer. The memory model is Bytes, neither of the two already here. Both walks memcpy a wire header out of a uint8_t buffer at an offset the message chose, so typed leaves every memcpy validity and separation goal open at 58 of 74, and caveat cannot size the byte array at all. Typed+cast reaches 73 of 74. The four helpers are re-proved rather than assumed, for the reason VERIFY_UTILS_FCTS exists. 198 obligations, and three mutations covering what the annotations are there for: the terminator's room, the fits-the-copy guard, and the padding extent. nl_parse_link_filter joins CHAR_PARAM_ALLOWLIST. Its char * is an output buffer it only writes, fed from a uint8_t source through an explicit cast, so it reads no plain char and the gcc_x86_64 signedness cannot reach it. The compiler-based check agrees for all seven.
mem.c, guest.c and rosetta.c used va_start and va_end as local variable and parameter names for the ends of an address range. They shadow the stdarg macros. It compiles, since both are function-like and a declaration never invokes them, but procemu.c two directories away calls the real ones, and Frama-C rejects the file outright under CERT MSC38-C, which is what kept mem.c, the largest source in the tree, out of the analyzer. va_base and va_limit instead. rosetta.c already used va_base for the start of exactly this kind of range, and limit is the word the tree uses for an exclusive upper bound in mmap_limit and backing_limit. The four genuine va_start(ap, ...) call sites are untouched.
pty_keepalive_register_locked keeps guest_slave_count when it reuses a row for the minor that row already describes, because those slaves are still open. If the row had no shared segment then, the count was accumulated against nothing, and the segment it joins on this registration knows nothing about it. Each of those slaves decrements on close a total it was never added to, the shared count goes negative, and pty_slot_hung_up_locked reads that as a hangup with the slaves still open, which is the failure the row rework set out to remove. Reaching it needs pty_shared_attach to have returned NULL once, the master to close leaving the row as the pty's master-less home, and a dup, an SCM_RIGHTS adopt or a fork restore for the same minor to re-register it while the attach succeeds. The compensation is the one pty_keepalive_clear_slot_locked already makes when it hands a segment-less count to an heir that maps one, and it is guarded to the same-pty path, since every other route zeroed the count just above.
The comment over them in procemu-internal.h said four and listed five.
verify used "if: ${{ !cancelled() }}" where verify-mutants-gate below it
uses always(), for a reason that gate states: a required check reported
as skipped does not block a merge, and !cancelled() skips this job
whenever the run is cancelled. Two required checks over the same matrix
should not disagree about that.
The comment claimed the matrix restores the switch the verify job already built, but the commit that folded proving into the matrix deleted that job, and proof-targets runs on Linux so it cannot prime a macOS-keyed cache. On a miss every leg builds Frama-C and the provers from source at once, each against the same 60-minute timeout. That is the cost of bumping any of the three pinned versions, and the first run after such a bump is the one at risk. A prime job would trade it for a barrier in front of every run, so the miss is the cheaper side; the comment says so now instead of describing a job that is gone.
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.
Nine proof targets read their sources from files named foo-math.h, each sitting beside the .c it had been split out of. The suffix described how the file came to exist rather than what it is for, and the scattering left no way to ask what the tree actually proves. They move to src/proved/.h, and check-proof-targets.py enforces membership in both directions: a header there that no target proves, and a target naming a file git does not track.
Seven targets join them (align, dirent, fdset, iov, pathdepth, slice, timespec), taking the proved surface to 590 obligations over 37 functions, with 88 mutations showing those contracts constrain something rather than merely parse.
Writing the contracts found five defects the tests did not. pselect6 honored fd_set bits above nfds, which Linux ignores, so it polled descriptors the caller never named and returned EBADF when one was closed; it also bounded nfds by the host FD_SETSIZE rather than the fd table size, two constants that are both 1024 on macOS and are not the same constant. ppoll, pselect6, epoll_pwait2 and recvmmsg truncated a sub-millisecond timeout to poll(0), turning a 500 microsecond wait into a spin. epoll_pwait2 and recvmmsg converted a large finite timeout into an infinite one. linux_timespec_to_ns_sat overflowed signed 64-bit arithmetic on its way to saturating.
Two splits keep the surrounding code readable enough to check against those contracts: the pty side table leaves procemu.c for procemu-pty.c, and five HVC cases leave vcpu_run_loop_with_hooks for named handlers, halving it.
Summary by cubic
Widens and centralizes machine-checked arithmetic under src/proved/, and splits two risky hotspots (pty keepalive table; five HVC cases) to cut risk. Behavior changes: pselect6 now masks bits above nfds and bounds nfds by the fd table; ppoll/pselect6/epoll_pwait2/recvmmsg round sub‑ms waits up, clamp huge finite waits, and reject negatives with EINVAL; recvmmsg no longer parks indefinitely; signed overflow is removed from timespec math; align_up_ok admits valid top‑of‑address‑space candidates; closing one master alias no longer hangs up a live slave; dirfd‑ and cwd‑relative /dev/pts paths re‑derive through the intercept; netlink attribute writes validate 16‑bit lengths and buffer space.
Proved surface and CI
scripts/analysis-mk.py; CI’s verify-mutants matrix derives from “make print-verify-targets”;verifyandverify-mutants-gateaggregate the matrix; runs parallelize and mutations scope to the changed function with a safe whole‑target fallback.System calls and runtime
proc_pty_forget_host_fddrops stray fds from both tables; dirfd‑ and cwd‑relative /dev/pts paths re‑derive through the intercept.Written for commit 8cb3582. Summary will update on new commits.