[owenthcarey]

Summary

Implements RFC 0034, Fast enforcement, confirmed errors and a bounded analysis. The model stays the same: prove, check, guard, record. What changes is how each part is paid for.

After RFC 0033 the default build was correct on untuned code, but it cost more than AddressSanitizer: Lua ran at 6.0× the reference compiler's time, QuickJS at 18.5×, curl at 23× and libdeflate at 24.6×. Six of ten fresh projects did not build. Now:

• Fresh corpus (gate F1). All ten fresh34 projects build with default flags and pass their own test suites in trap and report mode, with no trap and no definite error: QuickJS, LMDB, Janet, brotli, xz, libdeflate, zlib-ng, curl, cmark and libgit2.
• Run time (gate F7). These are the default build's times over the reference compiler's. QuickJS went from 18.5× to 4.00×, curl from 23× to 3.51× and libdeflate from 24.6× to 3.16×. The geometric mean is 2.55×. Lua is at 2.43×, down from 6.0×.
• Sealed corpus (gate F2). libjpeg-turbo, opus, flac, giflib and wren were built once at the end. On that first run flac hit a false trap and one opus test ran past its time limit. Both were reduced to cases and fixed, and amendment 18 records that the set is no longer sealed for them. All five now build and pass their tests in trap and report mode.
• Detection (gate F4). 57 of the 61 bug programs in test/cases/detection/ stop before the faulty access (54 were required), and no fixed twin stops. On a new blind set of 48 programs (test/cases/detection-blind/), the default build stops 41 and ASan 44, with no false stop.

Design notes

• Guards are calls the backend lowers (§1). The prelude declares the guards instead of defining them. LLVM passes (lib/Frontend/GuardPasses.cpp) do the rest:

  • GuardCanonicalize puts guards in a form LLVM's own redundancy elimination and LICM can remove.
  • GuardMerge merges the guards along one access path.
  • GuardExpand makes what is left an inline shadow check. Functions with more than 1,024 guards get a compact form.
  • GlobalPadding pads registered globals to whole granules.

  Range caches, the epoch, the inline guard bodies and their _ool copies are deleted.

• Shadow memory (§2, amendment 1). One byte per 16-byte granule covers the whole address space. Heap objects get a live prefix and a slot tail. Stack and global objects get an exact encoding: a last-granule byte, logarithmic run bytes, and one-past and mixed markers. Everything else goes to one out-of-line slow path that rejects untracked memory in constant time.

• Registration where a guard can reach (§4, amendments 2–3). Registered locals and parameters are aligned to granules. A library call's arguments are registered only when the callee takes a callback, returns a pointer the caller uses, or guards that argument.

• Library calls (§5, amendments 4, 13, 14). Call arguments are guarded through the shadow. A copy whose length no term can state goes through a checked wrapper, which checks the destination's room, the source's bytes and that they don't overlap. %.Ns arguments are covered by the call's live guard.

• Confirmed errors (§6, amendment 7). Each candidate definite error is replayed along single paths with path conditions. It fails the build only if a feasible path reaches the site and every feasible path that does has the violation. Unconfirmed candidates are warnings.

• A bounded analysis (§7, amendments 8 and 10). The analysis counts work against a budget:

  • 20,000,000 per run;
  • per unit, 400 per site and at least 20,000,000;
  • a least share of 100,000 per run;
  • caps on retained state and blocks.

  Per-definition CFGs and the record JSON are dropped as soon as they are used. With that, libgit2's link fell from 7.8 GB.

• Fixes found on real code.

  • Escaped locals are havocked at unknown calls (amendment 11).
  • A cursor's span check needs a single target (amendment 12).
  • setjmp rewinds only on its second return (amendment 15).
  • Term arithmetic is exact over long long and is clamped only at its result, which fixes flac's memset(p, 0, count + 8).
  • Stack objects write their shadow one run at a time, which fixes opus's 229 KiB arrays entered 100M times (amendment 18).

• The RFC's Implementation amendments (1–18) record every departure from the text and the gate results.

Not met, carried forward: build cost (F5). These are build CPU over the reference compiler's, with a limit of 5×. 34 of the 41 configs measured are within it. Over it:

Project	Ratio
pcre2	13.6×
sqlite	9.7× (sqlite3.c 63 CPU s, under its 120 s target)
mujs, lmdb	7.5×, 7.4×
janet, quickjs	6.0×, 5.8×
http-parser, inih, expat	5.6×, 5.5×, 5.1×
opus (sealed)	5.78× (4.42× in a run of opus and flac alone)

curl's libtests.c peaks at 2,271 MiB, against 1,250 MiB for the reference compiler. Every cheaper budget measured failed G15 (functions over budget) or Lua's no-runtime bound.

Not met, carried forward: run time (F7 and G14). QuickJS is at 4.00× (limit 4). The geometric mean is 2.55× (limit 2.5). G14: zlib 1.62× and cJSON 1.59× (limit 1.5); Lua 2.43× meets its bound. Without the runtime the three measure 1.09, 1.00 and 1.15.

Ratchet. expected.json was rewritten from the final full run, because the work budget moves proofs in both directions. Two new warning sites in cJSON's tests were triaged false, in a class already triaged there.

Breaking changes:

• -fweavec-budget and -fweavec-unit-budget now count analysis work instead of CFG block transfers.
• A definite error that its replay does not confirm is a warning.
• The guard helpers are declarations the backend lowers, so the prelude, libweavec_chk.a and the runtime change together. Rebuild objects.

Test plan

• Unit tests: the prelude's term helpers, the library table's source wrapper option, the ledger's budget fields and the check emitter's exact terms.
• Integration tests:
  • test/Driver/driver-werror.c and weavec-archive-note.c;
  • test/Emission/guard-passes-*.c, checked-wrappers-runtime.c, runtime-oracle-checked-wrappers.c and stack-objects-callback-argument.c;
  • the rewrite oracle compares both sides with -disable-llvm-passes.
• Cases:
  • 170 new case files, among them test/cases/detection-blind/ (48 programs with fixed twins);
  • semantics/runtime/ cases for parameter neighbours, %.Ns dangling, copy sources and signed term sums;
  • soundness/ cases for escaped locals and cursors over several arrays.
• On macOS arm64:
  • the unit tests pass (697);
  • lit passes 177 of 177;
  • the runtime test passes;
  • scripts/run-cases.py passes 725 of 725 in trap, --asan and --checks verify modes.
• Corpus (scripts/corpus-gate.py):
  • --full default set: G9–G12, G15 (0.89% of functions over budget), R4 and D1 pass.
  • --set fresh34: F1 passes.
  • --set sealed34: all five build and pass; F2 fails only on opus's build ratio.
  • Benches: as in the tables above.
• scripts/check-hygiene.py passes, with line budgets of 22,000 engine and 72,000 library lines (amendment 17). scripts/check-format.sh passes.

Checklist

• Code is formatted (scripts/format.sh). clang-tidy (Homebrew LLVM) is clean on the changed files. clang-analyzer-security.ArrayBound is disabled, with a comment, because it hung on LLVM's hung-off operands.
• Public behaviour changes are documented: README (performance), the docs site (CLI budgets, troubleshooting, guarantees, adoption, build integration), docs/architecture.md, the roadmap, AGENTS.md and the corpus README.
• Conventional Commit PR title. User-visible changes are documented; the changelog is generated.
• No Clang/LLVM dependencies introduced into lib/Core.