mirror of
https://github.com/MobileGL-Dev/MobileGL
synced 2026-11-07 01:53:24 +09:00
[MG_Remote, CI] (P6/dl): the Fatal census gate, and the one death under MG_Remote that named nothing
Exit gate S7, and the precondition for CONTRACT-P6 5.2's funnel rather than
its replacement.
S7 says "a bare abort() added outside Session::Fail -> the census gate goes
red". Session::Fail does not exist: it is the 93-site refactor 5.2 describes,
and it is not in this commit. What IS checkable today is the property that
funnel exists to guarantee and that every consumer already depends on - every
death under MG_Remote/ names a FAMILY, in a Fatal{Word} marker a grep can
find. run_trace_case.cmake reds a split retrace on any `Fatal{` line, the
retrace lane's refusal census counts them by name, and MEASUREMENTS quotes
the distinct words. A death with no word is invisible to all three.
TWO RULES, BECAUSE ONE WOULD LAUNDER THE OTHER. An abort must carry a marker
within twelve lines; and every WireLogFatal call must carry one in its format
string. WireLog.cpp's own abort is exempt from the first rule ONLY because its
five callers satisfy the second - a funnel that accepted an unmarked string
would be a hole shaped exactly like the rule.
THE BASELINE BOUNDS SILENCE, NOT DEATHS. Abort sites may grow freely; a new
family word may not appear unrecorded. Freezing the total would make every new
guard a gate change, which is how a gate stops being run. The wire's FatalCode
has seven values and the internal vocabulary is thirty-two, which is the
divergence D2 exists to bound - so growing it has to be an act, not an
accident.
THE CENSUS ALSO CORRECTS ITSELF. Its first run reported WireLog.h's own PROSE
as an unmarked death: the comment explaining why the stderr echo exists
contains the words std::abort(). So the scanner strips comments before
matching, with a character-level pass rather than a regex - a `"http://"`
inside a string literal is not a comment - while KEEPING string literals,
because the markers it looks for live in them. Real numbers after that fix:
93 abort sites, 32 family words, 0 unmarked. a6 had counted 92 and 30 from a
scan that did not make the distinction.
AND THE ONE REAL FINDING. a6 named two aborts with no marker at all;
WireLog.cpp's is the sanctioned funnel, so the genuine one is
PersistentMapTracker's invalid-MOBILEGL_IPC_ADOPT_TIER death. It now carries
Fatal{UnimplementedAdoptTier}, which is what makes the census zero.
R-16 both ways, run: a bare std::abort() reds it naming the file and line, and
a new family word reds it naming the word and how to record it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This commit is contained in:
Claude Opus 5
@@ -1984,6 +1984,14 @@ jobs:
|
||||
- name: Checkout repo
|
||||
uses: actions/checkout@v6
|
||||
|
||||
# `dl` / exit gate S7. CHEAP AND EARLY, on a job that only reads the tree: it needs no
|
||||
# build, so a death that names no family is reported in seconds rather than after the
|
||||
# matrix. What it refuses is a std::abort() under MG_Remote/ with no Fatal{Family} marker,
|
||||
# and a family word that appeared without being recorded - the vocabulary drifts on
|
||||
# purpose or not at all (CONTRACT-P6 5.2's D2 ruling).
|
||||
- name: Fatal census (S7)
|
||||
run: python3 scripts/ci/fatal_census.py
|
||||
|
||||
- name: Load trace cases
|
||||
id: trace-cases
|
||||
run: |
|
||||
|
||||
@@ -1047,14 +1047,20 @@ namespace MobileGL::MG_Remote::Client {
|
||||
// map_persistent, so a mis-set run gets through EGL bring-up and a frame of setup
|
||||
// first. Moving it to the parse means a knob-validity rule in ConfigLoader, which is
|
||||
// c0's file; filed for the integrator rather than taken here.
|
||||
// `dl` (CONTRACT-P6 5.2): THE FAMILY WORD THIS SITE NEVER CARRIED. a6 found two aborts
|
||||
// under MG_Remote/ with no Fatal{ marker at all, so "the log stays verbatim" was not true
|
||||
// of them and no family grep could see them - this is one. (The other, WireLog.cpp's, is
|
||||
// the sanctioned funnel: every one of its callers passes a Fatal{ string of its own.)
|
||||
if (tier <= 1) {
|
||||
MGLOG_F("MGPipe: MOBILEGL_IPC_ADOPT_TIER=%u names adoption tier T%u, which P11 implements "
|
||||
"and P5 does not; P5 runs at T2 (emulate) only.",
|
||||
MGLOG_F("MGPipe: Fatal{UnimplementedAdoptTier, \"T%u\"} - MOBILEGL_IPC_ADOPT_TIER=%u "
|
||||
"names an adoption tier P11 implements and P5 does not; P5 runs at T2 "
|
||||
"(emulate) only.",
|
||||
static_cast<unsigned>(tier), static_cast<unsigned>(tier));
|
||||
} else {
|
||||
MGLOG_F("MGPipe: MOBILEGL_IPC_ADOPT_TIER=%u is not an adoption tier; the only values are 0 "
|
||||
"and 1 (P11) and 2 (emulate, the P5 default).",
|
||||
static_cast<unsigned>(tier));
|
||||
MGLOG_F("MGPipe: Fatal{UnimplementedAdoptTier, \"%u\"} - MOBILEGL_IPC_ADOPT_TIER=%u is "
|
||||
"not an adoption tier; the only values are 0 and 1 (P11) and 2 (emulate, the "
|
||||
"P5 default).",
|
||||
static_cast<unsigned>(tier), static_cast<unsigned>(tier));
|
||||
}
|
||||
std::abort();
|
||||
}
|
||||
|
||||
@@ -0,0 +1,225 @@
|
||||
#!/usr/bin/env python3
|
||||
"""The Fatal census gate (CONTRACT-P6 5.2, exit gate S7).
|
||||
|
||||
WHAT IT REFUSES: a `std::abort()` under MG_Remote/ that carries no family word.
|
||||
|
||||
S7 says "a bare abort() added outside Session::Fail -> the census gate goes red". Session::Fail
|
||||
does not exist yet - it is the 94-site funnel 5.2 describes, and this file is its precondition
|
||||
rather than its replacement. What CAN be checked today is the property that funnel exists to
|
||||
guarantee and that every consumer already depends on: every death names a FAMILY, in a
|
||||
`Fatal{Word...}` marker, on a line a grep can find.
|
||||
|
||||
That is not as weak as it sounds. a6's census found the vocabulary had drifted to 30 family
|
||||
words against a 7-value wire FatalCode, and found two aborts carrying no marker at all - so "the
|
||||
log stays verbatim" was untrue of them and no census could see them. Everything downstream reads
|
||||
these markers: run_trace_case.cmake reds a split retrace on any `Fatal{` line, the retrace lane's
|
||||
refusal census counts them by name, and MEASUREMENTS quotes the distinct words. A death with no
|
||||
word is invisible to all of it.
|
||||
|
||||
TWO SANCTIONED SHAPES, both spelled out rather than inferred:
|
||||
|
||||
1. the marker is within kMarkerWindow lines above the abort;
|
||||
2. the abort is inside the WireLogFatal funnel (Transport/WireLog.*), whose callers each pass
|
||||
a `Fatal{` format string - which this file also checks, because a funnel that accepted an
|
||||
unmarked string would launder exactly what rule 1 refuses.
|
||||
|
||||
THE BASELINE IS A CEILING ON SILENCE, NOT ON DEATHS. The count of abort sites may grow; the set
|
||||
of family words may not grow unrecorded. Freezing the total would make every new guard a gate
|
||||
change, which is how a gate stops being run.
|
||||
"""
|
||||
import argparse
|
||||
import json
|
||||
import re
|
||||
import sys
|
||||
from pathlib import Path
|
||||
|
||||
ROOT = Path(__file__).resolve().parents[2]
|
||||
SCAN_ROOT = ROOT / "MobileGL" / "MG_Remote"
|
||||
BASELINE = Path(__file__).with_name("fatal_census_baseline.json")
|
||||
|
||||
# The funnel's own files. WireLog.cpp's abort is reached only through WireLogFatal, and rule 2
|
||||
# checks that every CALLER passes a family word - so the death is named by the caller. Both files
|
||||
# are exempt from rule 2 as well: a function's own declaration and definition match any
|
||||
# call-shaped regex, and reporting them would be reporting the funnel for being one.
|
||||
FUNNEL_FILES = {
|
||||
"MobileGL/MG_Remote/Transport/WireLog.cpp",
|
||||
"MobileGL/MG_Remote/Transport/WireLog.h",
|
||||
}
|
||||
|
||||
# Twelve lines: long enough for a wrapped MGLOG_F argument list (the longest in the tree runs to
|
||||
# eight continuation lines), short enough that an unrelated marker further up cannot cover an
|
||||
# abort it has nothing to do with.
|
||||
kMarkerWindow = 12
|
||||
|
||||
MARKER = re.compile(r"Fatal\{([A-Za-z][A-Za-z0-9]*)")
|
||||
ABORT = re.compile(r"\bstd::abort\(\)")
|
||||
WIRE_LOG_FATAL_CALL = re.compile(r"WireLogFatal\s*\(")
|
||||
|
||||
|
||||
def strip_comments(text):
|
||||
"""Blank out comments, keeping line numbering and STRING LITERALS intact.
|
||||
|
||||
Both halves matter. Comments have to go because WireLog.h's own prose contains the words
|
||||
`std::abort()` while explaining why the stderr echo exists - the first run of this gate
|
||||
reported that sentence as an unmarked death. String literals have to STAY, because the family
|
||||
markers this file looks for live inside them.
|
||||
|
||||
A character-level pass rather than a regex, because `"http://..."` inside a string is not a
|
||||
comment and a regex with no string state says it is.
|
||||
"""
|
||||
out = []
|
||||
index = 0
|
||||
length = len(text)
|
||||
quote = None
|
||||
while index < length:
|
||||
char = text[index]
|
||||
if quote is not None:
|
||||
out.append(char)
|
||||
if char == "\\" and index + 1 < length:
|
||||
out.append(text[index + 1])
|
||||
index += 2
|
||||
continue
|
||||
if char == quote:
|
||||
quote = None
|
||||
index += 1
|
||||
continue
|
||||
if char == '"' or char == "'":
|
||||
quote = char
|
||||
out.append(char)
|
||||
index += 1
|
||||
continue
|
||||
if char == "/" and index + 1 < length and text[index + 1] == "/":
|
||||
while index < length and text[index] != "\n":
|
||||
index += 1
|
||||
continue
|
||||
if char == "/" and index + 1 < length and text[index + 1] == "*":
|
||||
index += 2
|
||||
while index + 1 < length and not (text[index] == "*" and text[index + 1] == "/"):
|
||||
# Newlines survive so every reported line number stays the file's own.
|
||||
if text[index] == "\n":
|
||||
out.append("\n")
|
||||
index += 1
|
||||
index += 2
|
||||
continue
|
||||
out.append(char)
|
||||
index += 1
|
||||
return "".join(out)
|
||||
|
||||
|
||||
def source_files():
|
||||
for path in sorted(SCAN_ROOT.rglob("*")):
|
||||
if path.suffix not in (".cpp", ".h"):
|
||||
continue
|
||||
# A death test's deliberate abort is not a production death.
|
||||
if "MG_Test" in path.parts:
|
||||
continue
|
||||
yield path
|
||||
|
||||
|
||||
def relative(path):
|
||||
return path.relative_to(ROOT).as_posix()
|
||||
|
||||
|
||||
def census():
|
||||
unmarked = []
|
||||
families = set()
|
||||
aborts = 0
|
||||
unnamed_funnel_calls = []
|
||||
|
||||
for path in source_files():
|
||||
raw = path.read_text(encoding="utf-8", errors="replace")
|
||||
text = strip_comments(raw)
|
||||
lines = text.split("\n")
|
||||
rel = relative(path)
|
||||
|
||||
for word in MARKER.findall(text):
|
||||
families.add(word)
|
||||
|
||||
if rel not in FUNNEL_FILES:
|
||||
# Rule 2: every WireLogFatal call carries a family word. The call may wrap, so the
|
||||
# window covers its continuation lines.
|
||||
for index, line in enumerate(lines):
|
||||
if not WIRE_LOG_FATAL_CALL.search(line):
|
||||
continue
|
||||
window = "\n".join(lines[index:index + kMarkerWindow])
|
||||
if not MARKER.search(window):
|
||||
unnamed_funnel_calls.append({"file": rel, "line": index + 1,
|
||||
"text": line.strip()})
|
||||
|
||||
for index, line in enumerate(lines):
|
||||
if not ABORT.search(line):
|
||||
continue
|
||||
aborts += 1
|
||||
if rel in FUNNEL_FILES:
|
||||
continue # rule 2 covers it
|
||||
window = "\n".join(lines[max(0, index - kMarkerWindow):index + 1])
|
||||
if not MARKER.search(window):
|
||||
unmarked.append({"file": rel, "line": index + 1, "text": line.strip()})
|
||||
|
||||
return {
|
||||
"abort_sites": aborts,
|
||||
"unmarked_aborts": unmarked,
|
||||
"unnamed_funnel_calls": unnamed_funnel_calls,
|
||||
"families": sorted(families),
|
||||
}
|
||||
|
||||
|
||||
def main():
|
||||
parser = argparse.ArgumentParser()
|
||||
parser.add_argument("--write-baseline", action="store_true",
|
||||
help="Record today's numbers. Run it when a family is deliberately added.")
|
||||
parser.add_argument("--json", action="store_true", help="Print the census and exit 0.")
|
||||
args = parser.parse_args()
|
||||
|
||||
result = census()
|
||||
if args.json:
|
||||
print(json.dumps(result, indent=2))
|
||||
return 0
|
||||
|
||||
if args.write_baseline:
|
||||
BASELINE.write_text(json.dumps({"abort_sites": result["abort_sites"],
|
||||
"families": result["families"]}, indent=2) + "\n",
|
||||
encoding="utf-8")
|
||||
print(f"fatal census baseline written: {result['abort_sites']} abort sites, "
|
||||
f"{len(result['families'])} families")
|
||||
return 0
|
||||
|
||||
failures = []
|
||||
for entry in result["unmarked_aborts"]:
|
||||
failures.append(
|
||||
f"{entry['file']}:{entry['line']} aborts with no Fatal{{Family}} marker within "
|
||||
f"{kMarkerWindow} lines. Every death under MG_Remote/ must name a family: the split "
|
||||
f"retrace reds on `Fatal{{`, the refusal census counts by name, and a death with no "
|
||||
f"word is invisible to both.")
|
||||
for entry in result["unnamed_funnel_calls"]:
|
||||
failures.append(
|
||||
f"{entry['file']}:{entry['line']} calls WireLogFatal with no Fatal{{Family}} in its "
|
||||
f"format string. The funnel's own abort is exempt from the rule above ONLY because "
|
||||
f"its callers carry the word; a call that does not would launder exactly what the "
|
||||
f"rule refuses.")
|
||||
|
||||
if BASELINE.is_file():
|
||||
baseline = json.loads(BASELINE.read_text(encoding="utf-8"))
|
||||
# A NEW FAMILY WORD IS A DELIBERATE ACT and has to be recorded, because the wire's
|
||||
# FatalCode has seven values while the internal vocabulary is already five times that -
|
||||
# the divergence 5.2's funnel exists to bound. Growth is allowed; unrecorded growth is not.
|
||||
added = sorted(set(result["families"]) - set(baseline.get("families", [])))
|
||||
if added:
|
||||
failures.append(
|
||||
"new Fatal family word(s) with no baseline entry: " + ", ".join(added) +
|
||||
". Add them with `python3 scripts/ci/fatal_census.py --write-baseline` in the "
|
||||
"same commit that introduces them - the point is that the vocabulary grows on "
|
||||
"purpose rather than by accident (CONTRACT-P6 5.2's D2 ruling).")
|
||||
|
||||
print(f"fatal census: {result['abort_sites']} abort sites under MG_Remote/, "
|
||||
f"{len(result['families'])} distinct family words, "
|
||||
f"{len(result['unmarked_aborts'])} unmarked")
|
||||
if failures:
|
||||
for message in failures:
|
||||
print(f"::error::{message}", file=sys.stderr)
|
||||
return 1
|
||||
return 0
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
sys.exit(main())
|
||||
@@ -0,0 +1,37 @@
|
||||
{
|
||||
"abort_sites": 93,
|
||||
"families": [
|
||||
"AbiMismatch",
|
||||
"ApplyThreadJoinTimeout",
|
||||
"ApplyThreadNotRunning",
|
||||
"ArchiveEmpty",
|
||||
"ArtefactsMissing",
|
||||
"BarrierTimeout",
|
||||
"BarrierViolation",
|
||||
"BlobMissing",
|
||||
"ClientTablesUninstalled",
|
||||
"EventRingOverflow",
|
||||
"NoClientSession",
|
||||
"PresentCreditTimeout",
|
||||
"ProtocolCorruption",
|
||||
"ReadbackDeclined",
|
||||
"ReadbackReplyShort",
|
||||
"ReplyError",
|
||||
"ReplyMissing",
|
||||
"ReplyStatusInvalid",
|
||||
"ReplyTooLarge",
|
||||
"RetirementWaitFailed",
|
||||
"RingOverrun",
|
||||
"RoleViolation",
|
||||
"StageSnapshotTooNarrow",
|
||||
"UncarriedInitialBytes",
|
||||
"UnexpectedMapAccept",
|
||||
"UnimplementedAdoptTier",
|
||||
"UnimplementedClientSession",
|
||||
"UnimplementedWritebackWait",
|
||||
"UnmigratedSurface",
|
||||
"UnmigratedVerb",
|
||||
"UnsetCallMask",
|
||||
"UnsizedReadback"
|
||||
]
|
||||
}
|
||||
Reference in New Issue
Block a user