# DF-5580 VERDICT

**Finding:** `sys/platform/pc64/x86_64/__udivti3.c` — the
`__udivmodti4` masked-select initialization performs shift operations whose
counts are outside the domain of the shifted 64-bit operands (count ≥ 64,
or counts produced by unsigned wraparound of negative values like
`sr - n_udword_bits` with `sr < 64`). Ten sites: lines 231, 233, 235, 236,
238, 240, 242, 243 (the `d.s.high == 0, d.s.low != 0` non-power-of-2 path,
`sr ∈ [2,127]`) and lines 274, 277 (the `d.s.high != 0` path at
`sr == 64` exactly).

**Status: reproduced** (the UB condition itself), **impact: none today**
(no wrong division results on the shipping toolchain — proven), severity
Low / hardening, confidence certain.

## Root cause analysis (path:line)

The file is the 2009–2014 compiler-rt/libgcc `udivmodti4` ("Translated from
Figure 3-40 of The PowerPC Compiler Writer's Guide"). Instead of branching
on `sr`, it computes q/r initialization *branchlessly*:

* `__udivti3.c:231` `q.s.low = (n.s.low << (n_utword_bits - sr)) & ((long)(int)(n_udword_bits - sr) >> 63);`
  — the shift count `128 - sr` reaches 126 when `sr = 2`, but `n.s.low` is
  64-bit: UB whenever `sr ≤ 64`. The mask `(int)(64-sr) >> 63` is zero in
  exactly those cases, so the poisoned value is discarded — by
  construction, not by the standard.
* `__udivti3.c:233-237` — `n.s.low << (n_udword_bits - sr)` with
  `64 - sr` wrapped to ~2^64 when `sr > 64`; `n.s.low >> (sr - n_udword_bits)`
  with `sr - 64` wrapped negative when `sr < 64`. Masked the same way.
* `__udivti3.c:238-239` — `n.s.high >> sr` with `sr ∈ [64,127]`: count ≥
  width. Masked.
* `__udivti3.c:240-244` — `n.s.high >> (sr - n_udword_bits)` wrapped
  negative when `sr < 64`; `n.s.low >> sr` when `sr ≥ 64`. Masked.
* `__udivti3.c:274-278` — in the `d.s.high != 0` path `sr ∈ [1,64]`;
  at `sr == 64` both `n.s.high >> sr` and `n.s.low >> sr` shift 64-bit
  operands by exactly 64. Masked.

Range proofs (verified mechanically by the sr-boundary battery and by the
UBSan census): `sr = 1 + 64 + clz(d.s.low) − clz(n.s.high)` at :203 with
`d.s.low` neither 0 nor a power of two (both handled earlier) gives
`sr ∈ [2,127]`; at :250 `sr = clz(d.s.high) − clz(n.s.high)` guarded by
`:252` gives `sr ∈ [1,64]` after `++sr`.

Why the code is nonetheless *functionally* correct today: each
out-of-domain shift's result is ANDed with a predicate mask that is
provably zero whenever the shift is out of domain. gcc 8.3 (and every gcc
to date) emits `shl/shr reg, cl` (count taken mod 64) and the mask kills
it. The differential harness shows 6.46 billion vectors across three
independent runs (two seed sets baseline + fixed source) with **zero**
deviations from hardware `unsigned __int128` division, and the running
kernel's own exported `__udivti3` symbol agrees on 268.7M vectors pushed
through `/dev/df5580`.

Why it is still a finding: C11 6.5.7p3 makes each such evaluation
undefined behavior. A compiler is entitled to constant-fold, hoist, or
propagate poison from these subexpressions. Every future toolchain update
(base cc upgrade, clang import, LTO experiment) re-rolls the dice on the
correctness of **all** in-kernel 128-bit division — which is
`muldivu64()` (`sys/sys/systm.h:505-513`), used by lapic timer reload
(`sys/platform/pc64/apic/lapic.c:556,675,704,726`), i8254 clock
(`sys/platform/pc64/isa/clock.c:351,419,472,824`), timekeeping
(`sys/kern/kern_clock.c:916,1386,…`), cputimer freq conversion
(`sys/kern/kern_cputimer.c:205`), and hyperv vmbus (`sys/dev/virtual/hyperv/vmbus/vmbus.c:365`).
Silent wrong timer math is a correctness and availability hazard, and
wrong quotients in future callers could become memory-safety issues
(lengths derived from division). Upstream LLVM deleted this
branchless-mask implementation from compiler-rt years ago (modern
`udivmodti4` uses a `divq`-based 128/64 fast path plus a simple
shift-subtract loop with no masked selects).

Secondary implementation-defined (not UB) behaviors noted and accepted:
`(long)(int)` sign-extending mask tricks, arithmetic `>>` of negative
`_int128_t` at `:301-302`, and union type-punning at `:82-89` (kernel
builds with `-fno-strict-aliasing -fno-strict-overflow`, visible in
`mod_build.log`).

## Verification narrative (what was run, what happened)

1. **Userspace differential, baseline source.** `df5580_diff.c` includes
   the kernel file verbatim, compiled by the guest's gcc 8.3 — the same
   compiler that built the running kernel (`.comment` in `env.txt`).
   Batteries: 539×539 edge cross-product (283,514 pairs incl. all-ones,
   2^k±1, high-half patterns), exhaustive [0,2048)² (4,194,303 pairs),
   37,954 vectors pinned to `sr ∈ [57,69]` (the exact shift-count boundary),
   and 2^31 biased-random 128-bit pairs (dividend bit-length biased near
   divisor bit-length). Two independent seed sets.
   **Result: 2,151,999,419 vectors per run, 0 mismatches, both runs**
   (`run.log`, `run.2.log`).
2. **UBSan, baseline source.** With hand-written handler stubs (no
   libubsan on DF 6.5): abort-mode run terminates with
   `UBSAN-FIRED: shift exponent out of bounds at __udivti3.c:274:25
   (value=18446744073709551615 shift=64)` — exit 134 (`ub_abort.log`,
   `status_ub_abort.txt: ubsan_baseline_rc=134`). Recover-mode census over
   edge+exhaustive+sr64: **1,017,186 events, all ten sites firing**
   (`ub_census.txt`), including `shift=4294967291` — the negative-wrapped
   `sr − 64` count class at `:236`/`:240`.
3. **In-kernel verification.** KLD `df5580.ko` resolves the kernel's own
   global `__udivti3` (`nm /boot/kernel/kernel` →
   `ffffffff80bdabb0 T __udivti3`); its `/dev/df5580` ioctl runs caller
   vectors through the kernel symbol. 4,101 chunks × 65,536 =
   ~268.7M vectors (edge + sr-boundary + biased random), expected values
   computed natively in userspace. **0 mismatches**
   (`kmod_kldtest_run.log`).
4. **Fix validation (see fix fields).** `fix.diff` replaces the two
   masked-select blocks with the explicit `if (sr == 64) / else if
   (sr < 64) / else` and `if (sr < 64) / else` initialization that the
   file's own comments already spell out (the pre-rewrite upstream code).
   Validation: (a) patched source passes the identical 2.15B-vector
   battery with 0 mismatches (`run_fixed.log`, 313 s — ~10% faster than
   baseline); (b) UBSan abort-mode on the patched source completes the
   edge battery clean, rc 0 (`ub_abort_fixed.log`,
   `status_ub_abort_fixed.txt`); (c) the patched source compiled with
   kernel CFLAGS (`-Werror` clean) as KLD `df5580fix.ko` and executed in
   kernel context agrees with both the kernel baseline symbol and native
   division on all ~268.7M vectors. A full single-fix kernel rebuild was
   not performed (non-memory-corruption finding; contract requires kernel
   rebuild only for reproduced memory corruption) — the KLD route executes
   the patched code in kernel context with kernel flags, which is
   equivalent evidence for a pure codegen change.

## Negative results (checked and killed, pass-2 depth)

* **Algorithm correctness (Knuth/PPCWG loop):** no wrong-result bug found
  at any reachable input; ~6.7B total vectors across userspace + kernel
  contexts, quotient and remainder both checked. The `add-back`/carry
  trick at `:301-304` (`(_int128_t)(d.all − r.all − 1) >> 127`) is
  implementation-defined (gcc: sar) but gcc-defined and verified.
* **div==0:** `b == 0` reaches `% d.s.low` at `:116-117` / `:135-136` →
  #DE → panic. Documented libgcc-compatible contract ("K != 0"); all
  in-tree callers pass nonzero divisors (frequencies/constants). Caller
  DF-5554's crafted-capacity class is 64-bit hardware `div`, does not link
  `__udivti3`. Not a defect of this file.
* **Memory safety:** no pointers, arrays, or lengths in the file; the only
  write is `*rem` (NULL-checked at :115,:123,:134,:144,:156,:170,:189,:253,:307).
  No OOB/UAF/leak surface exists here.
* **`__umodti3` absence:** only `__udivti3` is compiled in
  (`sys/platform/pc64/conf/files:151`); kernel 128-bit modulo with runtime
  divisor would fail to link — none exists in-tree today.
* **Union type-punning `:82-89`:** fine under the kernel's
  `-fno-strict-aliasing` (see `mod_build.log` flags).
* **Harness bugs found and fixed during verification** (documented for
  reproducibility): edge-set builder could write 536 entries into a
  512-slot array; the sr-boundary generator truncated its 128-bit dividend
  to 64 bits (declared `uint64_t n`), silently reducing that battery to
  fast-path vectors — fixed and re-run; both are visible in the pack
  sources as shipped.

## 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.