DF-5714 — sys/libkern/ffs.c is dead code (not compiled anywhere), latent body proven correct over the full 2^32 domain

What this pack proves (all on the DragonFly guest, sources cksum-pinned to the audit tree)

1. DEAD FILE — sys/libkern/ffs.c is referenced by nothing: - absent from sys/conf/files (libkern block lines 2195–2237 lists every libkern file that is compiled; ffs.c, ffsl.c, flsl.c, flsll.c are all missing), - the only supported architecture is x86_64 (sys/cpu/ contains only x86_64), where every kernel TU instead uses the sys/cpu/x86_64/include/cpufunc.h:266-273 static __inline ffs() (#define HAVE_INLINE_FFS → __builtin_ffs), - ffs.c:33's #include <string.h> cannot even resolve in a kernel build (-nostdinc, sys/conf/kern.pre.mk:61; no sys/string.h exists) — empirically demonstrated in build.log / dead_compile.log.
2. LATENT BODY CORRECT — the verbatim ffs.c body, renamed at the preprocessor level and compiled at -O2, matches __builtin_ffs (== the live kernel semantics via cpufunc.h) on all 4,294,967,296 inputs, 0 mismatches (run.log T1). The mask >>= 1 arithmetic-shift-on-negative (ffs.c:46) is implementation-defined in C but produces bit-exact results on the kernel toolchain (gcc 8.3), including mask=INT_MIN → 32 and the mask == 0 → 0 guard (ffs.c:43-44). ffsl.c twin: 50,002,088 edge/exhaustive-pair/random cases, 0 mismatches (T2). There is no ffsll in the kernel at all (zero callers, zero definitions).
3. CONSUMER CENSUS (102 live ffs( call sites) — every live caller consumes the cpufunc.h inline; no caller passes a 64-bit value that would truncate (all operands are already int/u_int width; the 64-bit users correctly call ffsl). Guard-page class N/A: ffs.c:39-47 is pure register arithmetic — no pointer parameters, no dereference.
4. FIX VALIDATED (compile level — the level at which the "bug" lives) — a naive include swap is NOT enough: cpufunc.h:269's static __inline ffs collides with any out-of-line definition (recorded in fix_compile.log). The final fix.diff (include swap + FreeBSD-style #if !defined(HAVE_INLINE_FFS) gate) compiles kernel-style: FIX2COMPILE-OK in build.log / fix2_compile.log.

Reproduce

scp -r . dfbsd:/tmp/df5714/        # or: git clone of this pack
ssh dfbsd                          # root
sh /tmp/df5714/build.sh            # ~30 s: verbatim compiles + proofs
sh /tmp/df5714/run.sh              # ~26 s: T1 full-domain sweep + T2-T5

Expected decisive lines (see run.log):

T1 ffs full-domain: 4294967296 cases, 0 mismatches ...
T2 ffsl: 50002088 cases, 0 mismatches (vs __builtin_ffsl)
...
DEADPROOF-OK: ffs.c cannot compile in-kernel:      (build.log)
FIX2COMPILE-OK: guarded ffs.c compiles kernel-style (build.log)
HARNESS-PASS

The same harness also carries the strcmp.c negative evidence (T3/T4 — see ../neg-evidence-strcmp-pass2/).

VERDICT — DF-5714: sys/libkern/ffs.c dead-file status + latent-correctness proof

Status: reproduced (impact: none — dead code, Info-severity hygiene finding). Confidence: certain. Attempts: 5. All claims machine-demonstrated on the DragonFly guest (uname in env.txt; guest sources cksum-identical to the audit tree: ffs.c 3349697062 1930 / ffsl.c 1444671719 1875 / strcmp.c 180206468 2066).

The claim, and how each part was proven

1. ffs.c is not compiled into any DragonFly kernel or module. - sys/conf/files libkern block (lines 2195–2237) has no ffs.c entry (nor ffsl.c/flsl.c/flsll.c). Verified on host and guest (grep -c "libkern/ffs.c" /usr/src/sys/conf/files → 0, env.txt). - sys/cpu/ contains only x86_64 — the only supported platform — and every kernel TU gets ffs as static __inline from sys/cpu/x86_64/include/cpufunc.h:266-273 (#define HAVE_INLINE_FFS + __builtin_ffs). - Empirical: cc -O2 -nostdinc -I/usr/src/sys -c /usr/src/sys/libkern/ffs.c → ffs.c:33:10: fatal error: string.h: No such file or directory (dead_compile.log; kernel uses -nostdinc, sys/conf/kern.pre.mk:61). The file cannot even be compiled in-kernel as committed.
2. The latent body is arithmetically perfect. Full-domain sweep of all 2^32 masks: verbatim kernel ffs.c body (renamed -Dffs=k_ffs, compiled -O2, called through a volatile function pointer) vs __builtin_ffs == the live cpufunc.h inline: 0 / 4,294,967,296 mismatches (run.log T1). This simultaneously clears every arithmetic candidate: mask == 0 → 0 (ffs.c:43-44), the negative/INT_MIN inputs (returns 32), the implementation-defined mask >>= 1 signed right shift (ffs.c:46) — output-identical on the kernel toolchain gcc 8.3, because the loop only ever inspects the low bit and terminates at the lowest set bit, so arithmetic vs logical refill is unobservable. ffsl.c twin (which uses an explicitly unsigned shift, ffsl.c:44): 50,002,088 cases, 0 mismatches (T2). No ffsll exists anywhere in the kernel (zero definitions, zero callers).
3. Compiler-builtin interplay. There is no loop-idiom → self-call or builtin-substitution hazard: the out-of-line body is dead, and the live inline is the builtin by construction (cpufunc.h:271). The only real interplay landmine is the reverse one, demonstrated in fix_compile.log: an out-of-line ffs cannot coexist with cpufunc.h's static __inline ffs in one TU — so re-adding libkern/ffs.c to conf/files would break the x86_64 build twice over (missing string.h, then inline/outline collision).
4. Consumer census (why this is Info, not higher). 102 live ffs( call sites in-tree (excluding contrib): all resolve to the inline; none passes a 64-bit argument that would truncate (the census grep for 64-bit-shaped operands produced only already-32-bit expressions: msdosfs_fat.c:764/782 u_int bitmaps, drm 32-bit register masks, am7990.c:169/173 int ring counts). 64-bit bit-scans correctly use ffsl. Guard-page class is vacuous for ffs — no memory operands.
5. Fix. fix.diff: #include <string.h> → #include <sys/libkern.h> + FreeBSD-style #if !defined(HAVE_INLINE_FFS) gate around the body. Baseline (unfixed) reproduced: kernel-style compile fails (DEADPROOF-OK record). Patched: compiles kernel-style, body correctly compiles away on x86_64 (FIX2COMPILE-OK, fix2_compile.log; the guest-validated f_ffs2.c is byte-identical to the diff's result). Deletion of the file is the equally-valid alternative fix (maintainer's choice); the diff is the conservative variant.

Why no further escalation was pursued

No memory-safety primitive exists in this file (pure register function, no pointers), and the file is not linked anywhere — there is no runtime kernel behavior to attack. The pass-2 deliverable is the dead-file status (precedent: DF-5700 bcmp.c, same class) plus the machine-checked latent-correctness proof that closes the file's arithmetic questions permanently.

Rig honesty notes (all intermediate artifacts kept)

• run.1.log: first run had a harness bug — the guard-page fault cases (G3/G4) reused the page buffer left by G2 (…'A',NUL at the edge), so the walk mismatched in-bounds instead of reaching the guard. Fixed by re-arming the page; final run.log shows SIGSEGV for both kernel body and libc.
• run.2.log: second run had a dead-code-elimination artifact in the libc control ((void)strcmp(...) with unused result is elided by gcc -O2). Fixed by consuming the result; final run shows libc faulting identically to the kernel body.
• p2_harness_v1.c: the initial harness source, kept for the record.
• fix_compile.log: the naive-fix failure (inline collision) — evidence that the correct fix must include the HAVE_INLINE_FFS gate.

Fix status (batch validation)

Applied with the 36 sibling fix.diffs of this batch in findings/poc/_batch41/all_fixes.patch; single in-guest make -j6 nativekernel KERNCONF=X86_64_GENERIC completed RC=0 with zero errors under -Werror (full log: findings/poc/_batch41/fix_build8.log). Behavior A/B intentionally skipped for this Info-tier item.

(No fix.diff for this item: documented recommendation only - see Fix above.)