mirror of
https://github.com/MobileGL-Dev/MobileGL
synced 2026-11-07 01:53:24 +09:00
- the archive freeze rule goes with the directory - code comments lose citations to the removed notes
1248 lines
68 KiB
Python
1248 lines
68 KiB
Python
#!/usr/bin/env python3
|
|
# MobileGL - scripts/gen_pipe_field_ownership.py
|
|
# Copyright (c) 2025-2026 MobileGL-Dev
|
|
# Licensed under the GNU Lesser General Public License v3.0:
|
|
# https://www.gnu.org/licenses/gpl-3.0.txt
|
|
# https://www.gnu.org/licenses/lgpl-3.0.txt
|
|
# SPDX-License-Identifier: LGPL-3.0-only
|
|
# End of Source File Header
|
|
"""TABLE 2 - where every PipeInputs field's value comes from once the backend is a server.
|
|
|
|
CONTRACT-P5.md section 3 / BRIEF-P5 R-7. Reads
|
|
|
|
MobileGL/MG_Pipe/Coverage.def the 63 accessors, the 7 sticky, the 40 emitted
|
|
MobileGL/MG_Impl/Pipe/PipeFill.cpp EmittedCallSuppliesTheWholeField's refusals
|
|
MobileGL/MG_Pipe/FieldOwnership.def the hand-maintained half
|
|
|
|
and writes MobileGL/MG_Pipe/generated/PipeFieldOwnership.inc. The output is COMMITTED; CI
|
|
regenerates it and fails on a diff, exactly as gen_pipe.py's seven outputs do.
|
|
|
|
ONE CLASS PER ROW, AND THE BUILD FAILS OTHERWISE. 63 field rows + the 7 sticky forwards =
|
|
70, each in exactly one of RECORD_SUPPLIED / APPLIER_DERIVED / BARRIER_PULLED / FATAL. A
|
|
field in none of them stops this script, so the committed header can never contain an
|
|
unclassified row and --check is what catches a stale one. RECORD_SUPPLIED is DERIVED rather
|
|
than listed - it is Coverage.def's emitted list minus PipeFill.cpp's refusals - so the
|
|
mapping file cannot drift away from the emitters it describes without a red gate.
|
|
|
|
python3 scripts/gen_pipe_field_ownership.py # write it, print the summary
|
|
python3 scripts/gen_pipe_field_ownership.py --check # THE GATE: rc 1 on any hole
|
|
python3 scripts/gen_pipe_field_ownership.py --self-test # the gate's own negative controls
|
|
"""
|
|
|
|
import argparse
|
|
import os
|
|
import re
|
|
import sys
|
|
|
|
REPO_ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__)))
|
|
PIPE_DIR = os.path.join(REPO_ROOT, "MobileGL", "MG_Pipe")
|
|
GENERATED_DIR = os.path.join(PIPE_DIR, "generated")
|
|
COVERAGE_DEF = os.path.join(PIPE_DIR, "Coverage.def")
|
|
OWNERSHIP_DEF = os.path.join(PIPE_DIR, "FieldOwnership.def")
|
|
PIPE_FILL = os.path.join(REPO_ROOT, "MobileGL", "MG_Impl", "Pipe", "PipeFill.cpp")
|
|
PIPE_CALLS = os.path.join(PIPE_DIR, "PipeCalls.def")
|
|
FILL_POINTS = os.path.join(PIPE_DIR, "FillPoints.def")
|
|
# P5e (gl, ID-116): the two generated tables the admission derivation joins. They are READ, not
|
|
# restated - the whole point of ID-116 is that the allowlist is derived from the tables that
|
|
# already exist, so that retiring a verb's wait class narrows it and adding a BARRIER_PULLED row
|
|
# widens it only on barriered verbs, with no third place to keep in step.
|
|
PIPE_WIRE_INC = os.path.join(GENERATED_DIR, "PipeWire.inc")
|
|
FILL_POINTS_INC = os.path.join(GENERATED_DIR, "PipeFillPoints.inc")
|
|
OUT_NAME = "PipeFieldOwnership.inc"
|
|
|
|
CLASSES = ("RECORD_SUPPLIED", "APPLIER_DERIVED", "BARRIER_PULLED", "FATAL")
|
|
ENUMERATOR = {
|
|
"RECORD_SUPPLIED": "kRecordSupplied",
|
|
"APPLIER_DERIVED": "kApplierDerived",
|
|
"BARRIER_PULLED": "kBarrierPulled",
|
|
"FATAL": "kFatal",
|
|
}
|
|
|
|
BANNER = """// MobileGL - MobileGL/MG_Pipe/generated/{name}
|
|
// Copyright (c) 2025-2026 MobileGL-Dev
|
|
// Licensed under the GNU Lesser General Public License v3.0:
|
|
// https://www.gnu.org/licenses/gpl-3.0.txt
|
|
// https://www.gnu.org/licenses/lgpl-3.0.txt
|
|
// SPDX-License-Identifier: LGPL-3.0-only
|
|
// End of Source File Header
|
|
|
|
// TABLE 2: PipeInputs field ownership (CONTRACT-P5.md section 3, R-7).
|
|
//
|
|
// GENERATED by scripts/gen_pipe_field_ownership.py from Coverage.def, FieldOwnership.def and
|
|
// MG_Impl/Pipe/PipeFill.cpp - DO NOT EDIT. Regenerate with
|
|
// `python3 scripts/gen_pipe_field_ownership.py`; CI runs it and diffs the result.
|
|
//
|
|
// Included from MG_Backend/MGPipe/PipeInputs.h inside namespace MobileGL::MG_Pipe, which is
|
|
// the one header that both the poison check and the server's verb stamp already see. It is
|
|
// NOT included from MG_Pipe/MGPipe.h with the other seven generated files, on purpose: that
|
|
// header is in the PULL build's include closure and G1 admits no symbol motion there.
|
|
"""
|
|
|
|
|
|
def read(path):
|
|
with open(path, "r", encoding="utf-8") as handle:
|
|
return handle.read()
|
|
|
|
|
|
def mask_comments(text):
|
|
"""Blank comment bodies, keeping every offset and newline. String literals are LEFT
|
|
ALONE - unlike gen_pipe_dirty_surface.py's masker - because this file's rows carry their
|
|
retiring phase and their reason as quoted arguments."""
|
|
out = list(text)
|
|
i = 0
|
|
n = len(text)
|
|
while i < n:
|
|
if text[i] == "/" and i + 1 < n and text[i + 1] == "/":
|
|
while i < n and text[i] != "\n":
|
|
out[i] = " "
|
|
i += 1
|
|
elif text[i] == "/" and i + 1 < n and text[i + 1] == "*":
|
|
out[i] = out[i + 1] = " "
|
|
i += 2
|
|
while i < n and not (text[i] == "*" and i + 1 < n and text[i + 1] == "/"):
|
|
if text[i] != "\n":
|
|
out[i] = " "
|
|
i += 1
|
|
if i < n:
|
|
out[i] = out[i + 1] = " "
|
|
i += 2
|
|
else:
|
|
i += 1
|
|
return "".join(out)
|
|
|
|
|
|
def macro_block(text, name):
|
|
"""The body of a `#define <name>(X) ...` continued-line macro, comments blanked."""
|
|
masked = mask_comments(text)
|
|
start = masked.find("#define %s(X)" % name)
|
|
if start < 0:
|
|
sys.exit("gen_pipe_field_ownership: %s is not in the file" % name)
|
|
end = start
|
|
while True:
|
|
line_end = masked.find("\n", end)
|
|
if line_end < 0:
|
|
body = masked[start:]
|
|
break
|
|
if not masked[end:line_end].rstrip().endswith("\\"):
|
|
body = masked[start:line_end]
|
|
break
|
|
end = line_end + 1
|
|
# The rows wrap, so the continuation backslashes have to go before a row regex can see a
|
|
# row as one thing. Offsets do not matter here; only the token sequence does.
|
|
return body.replace("\\\n", "\n")
|
|
|
|
|
|
def parse_coverage(text=None):
|
|
"""The ordered 63 accessors, the 7 sticky and the 40 emitted, out of Coverage.def."""
|
|
text = read(COVERAGE_DEF) if text is None else text
|
|
accessors = re.findall(r"X\(\s*(\w+)\s*,\s*\w+\s*\)",
|
|
macro_block(text, "MGP_COVERAGE_ACCESSOR_LIST"))
|
|
sticky = re.findall(r"X\(\s*(\w+)\s*,", macro_block(text, "MGP_COVERAGE_STICKY_LIST"))
|
|
emitted = re.findall(r"X\(\s*(\w+)\s*,\s*\w+\s*\)",
|
|
macro_block(text, "MGP_COVERAGE_EMITTED_LIST"))
|
|
if not accessors:
|
|
sys.exit("gen_pipe_field_ownership: Coverage.def's accessor list did not parse")
|
|
seen = set()
|
|
for name in accessors:
|
|
if name in seen:
|
|
sys.exit("gen_pipe_field_ownership: %s appears twice in the accessor list" % name)
|
|
seen.add(name)
|
|
for name in sticky + emitted:
|
|
if name not in seen:
|
|
sys.exit("gen_pipe_field_ownership: %s is not an accessor in MGP_COVERAGE_ACCESSOR_LIST"
|
|
% name)
|
|
return accessors, sticky, emitted
|
|
|
|
|
|
def parse_supplies_whole_field(text=None):
|
|
"""The fields EmittedCallSuppliesTheWholeField REFUSES, read out of PipeFill.cpp rather
|
|
than restated here - the derivation that keeps RECORD_SUPPLIED honest is only as good as
|
|
its source, so the source is the function itself."""
|
|
text = read(PIPE_FILL) if text is None else text
|
|
masked = mask_comments(text)
|
|
start = masked.find("Bool EmittedCallSuppliesTheWholeField(MGPipeInputField field)")
|
|
if start < 0:
|
|
sys.exit("gen_pipe_field_ownership: EmittedCallSuppliesTheWholeField is not in %s"
|
|
% os.path.basename(PIPE_FILL))
|
|
false_at = masked.find("return false;", start)
|
|
if false_at < 0:
|
|
sys.exit("gen_pipe_field_ownership: EmittedCallSuppliesTheWholeField has no `return false` arm")
|
|
refused = re.findall(r"case\s+MGPipeInputField::(\w+)\s*:", masked[start:false_at])
|
|
if not refused:
|
|
sys.exit("gen_pipe_field_ownership: EmittedCallSuppliesTheWholeField refuses nothing - "
|
|
"either the function moved or the parse broke; a silently empty refusal set "
|
|
"would make every emitted field RECORD_SUPPLIED")
|
|
return refused
|
|
|
|
|
|
ROW_RE = re.compile(r"X\(\s*(\w+)\s*,\s*(\w+)\s*,\s*\"([^\"]*)\"\s*,\s*\"([^\"]*)\"\s*\)")
|
|
ARG_ROW_RE = re.compile(r"X\(\s*(\w+)\s*,\s*(\d+)\s*,\s*(\w+)\s*,\s*\"([^\"]*)\"\s*\)")
|
|
PAIR_RE = re.compile(r"X\(\s*(\w+)\s*,\s*(\w+)\s*\)")
|
|
# An exemption's reason may be one string or several adjacent ones, the way a long C literal is
|
|
# written; the row regex takes the first and the check only cares that there is one.
|
|
EXEMPT_RE = re.compile(r"X\(\s*(\w+)\s*,\s*\"([^\"]*)\"")
|
|
|
|
|
|
def parse_ownership(text=None):
|
|
text = read(OWNERSHIP_DEF) if text is None else text
|
|
fields = ROW_RE.findall(macro_block(text, "MGP_FIELD_OWNERSHIP_LIST"))
|
|
forwards = ROW_RE.findall(macro_block(text, "MGP_FIELD_OWNERSHIP_FORWARD_LIST"))
|
|
args = ARG_ROW_RE.findall(macro_block(text, "MGP_FIELD_OWNERSHIP_ARG_LIST"))
|
|
verb_ops = PAIR_RE.findall(macro_block(text, "MGP_VERB_OP_LIST"))
|
|
exempt = EXEMPT_RE.findall(macro_block(text, "MGP_VERB_OP_EXEMPT_LIST"))
|
|
if not fields:
|
|
sys.exit("gen_pipe_field_ownership: FieldOwnership.def's field list did not parse")
|
|
return fields, forwards, args, verb_ops, exempt
|
|
|
|
|
|
def parse_ops_and_verbs(calls_text=None, fill_points_text=None):
|
|
"""The two name spaces the stamp map joins, read from the files that define them: the
|
|
catalogue's calls (PipeCalls.def, which IS the MGPWireOp enum, with each call's KIND) and
|
|
the verb set (FillPoints.def, which IS MG_Backend::GLFunctionsTable's member list)."""
|
|
calls_text = read(PIPE_CALLS) if calls_text is None else calls_text
|
|
fill_points_text = read(FILL_POINTS) if fill_points_text is None else fill_points_text
|
|
calls = re.findall(r"X\(\s*(\w+)\s*,\s*\w+\s*,\s*(k\w+)\s*,",
|
|
macro_block(calls_text, "MGP_CALL_LIST"))
|
|
verbs = re.findall(r"X\(\s*(\w+)\s*,\s*(k\w+)\s*\)",
|
|
macro_block(fill_points_text, "MGP_FILL_VERB_LIST"))
|
|
if not calls:
|
|
sys.exit("gen_pipe_field_ownership: PipeCalls.def's call list did not parse")
|
|
if not verbs:
|
|
sys.exit("gen_pipe_field_ownership: FillPoints.def's verb list did not parse")
|
|
return calls, [v for v, _ in verbs]
|
|
|
|
|
|
def array_block(text, declaration):
|
|
"""The braced initialiser of a generated `... <declaration> = {` table, comments KEPT.
|
|
|
|
The generated tables carry the row's name in a trailing comment (`// DrawArrays`) and in a
|
|
leading one (`/* 58 ReadPixels */`), and those comments are the only place the row's NAME
|
|
appears - the values themselves are enumerators and hex words. So this masker's opposite is
|
|
what is wanted here: the comments are the data."""
|
|
start = text.find(declaration)
|
|
if start < 0:
|
|
sys.exit("gen_pipe_field_ownership: %r is not in the generated table it should be in - "
|
|
"the admission derivation (ID-116) reads it rather than restating it, so a "
|
|
"renamed or moved table has to stop this script rather than produce an empty "
|
|
"allowlist" % declaration)
|
|
open_at = text.find("{", start)
|
|
depth = 0
|
|
i = open_at
|
|
while i < len(text):
|
|
if text[i] == "{":
|
|
depth += 1
|
|
elif text[i] == "}":
|
|
depth -= 1
|
|
if depth == 0:
|
|
return text[open_at + 1:i]
|
|
i += 1
|
|
sys.exit("gen_pipe_field_ownership: %r never closes its initialiser" % declaration)
|
|
|
|
|
|
WAIT_ROW_RE = re.compile(r"/\*\s*\d+\s+(\w+)\s*\*/\s*static_cast<Uint8>\(\s*(k\w+)\s*\)")
|
|
|
|
|
|
def parse_wait_classes(text=None):
|
|
"""{op name: wait class enumerator} out of generated/PipeWire.inc's kMGPipeWaitClasses.
|
|
|
|
This is the STATIC half of MGPipeBarriered - the same column the emit table and the sink
|
|
both compute from - and it is what decides whether a record is one the client is parked
|
|
behind. A pair may only be admitted on a verb whose op is in it and is not kWaitNone."""
|
|
text = read(PIPE_WIRE_INC) if text is None else text
|
|
block = array_block(text, "kMGPipeWaitClasses[static_cast<SizeT>(MGPWireOp::kOpCount)] =")
|
|
rows = WAIT_ROW_RE.findall(block)
|
|
if not rows:
|
|
sys.exit("gen_pipe_field_ownership: kMGPipeWaitClasses did not parse - with no wait "
|
|
"column every op would look unbarriered and the admitted set would be silently "
|
|
"empty, which reads as 'the lane is clean' (ID-116)")
|
|
waits = {}
|
|
for op, wait in rows:
|
|
waits[op] = wait
|
|
return waits
|
|
|
|
|
|
VERB_CLASS_ROW_RE = re.compile(r"MGPipeVerbClass::(\w+)\s*,\s*//\s*(\w+)")
|
|
CLASS_MASK_ROW_RE = re.compile(r"//\s*(k\w+):[^\n]*\n\s*\{\{\s*(0x[0-9a-fA-F]+)ull\s*,\s*"
|
|
r"(0x[0-9a-fA-F]+)ull\s*\}\}")
|
|
|
|
|
|
def parse_verb_classes(text=None):
|
|
"""({verb: class}, {class: (word0, word1)}) out of generated/PipeFillPoints.inc.
|
|
|
|
kMGPipeClassFieldMask is the verb's OWN may-read table: a field outside it is one the
|
|
client's residual fill never copied for that verb, so it can never be a legitimate read
|
|
there whatever its ownership row says. Intersecting with it is ID-84's third term."""
|
|
text = read(FILL_POINTS_INC) if text is None else text
|
|
verb_rows = VERB_CLASS_ROW_RE.findall(
|
|
array_block(text, "kMGPipeVerbClass[kMGPipeVerbCount] ="))
|
|
mask_rows = CLASS_MASK_ROW_RE.findall(
|
|
array_block(text, "kMGPipeClassFieldMask[kMGPipeVerbClassCount] ="))
|
|
if not verb_rows:
|
|
sys.exit("gen_pipe_field_ownership: kMGPipeVerbClass did not parse - the admitted set "
|
|
"would lose its class intersection (ID-116)")
|
|
if not mask_rows:
|
|
sys.exit("gen_pipe_field_ownership: kMGPipeClassFieldMask did not parse - the admitted "
|
|
"set would lose its class intersection (ID-116)")
|
|
verb_class = {}
|
|
for cls, verb in verb_rows:
|
|
verb_class[verb] = cls
|
|
class_mask = {}
|
|
for cls, low, high in mask_rows:
|
|
class_mask[cls] = (int(low, 16), int(high, 16))
|
|
for verb, cls in verb_class.items():
|
|
if cls not in class_mask:
|
|
sys.exit("gen_pipe_field_ownership: verb %s is in class %s, which has no field mask"
|
|
% (verb, cls))
|
|
return verb_class, class_mask
|
|
|
|
|
|
THIS_PHASE = "P5e"
|
|
PHASE_TOKEN_RE = re.compile(r"\bP\d+[a-z]*\b")
|
|
|
|
|
|
def phase_is_owed_by_this_phase(retires):
|
|
"""Does this row's RetiringPhase column name THIS phase?
|
|
|
|
Tokenised rather than substring-matched: the column is prose ("P5e (Espryt unbarriered),
|
|
P7 (Magma)", "P3b/P4b (Espryt), P7 (Magma)", "P8 (indirect), P9 (readback), P13
|
|
(transfer)"), and a substring test would let a future "P5e2" or a "P5" answer for "P5e"."""
|
|
return THIS_PHASE in PHASE_TOKEN_RE.findall(retires)
|
|
|
|
|
|
def build_admitted(accessors, ownership, phase, verbs, verb_ops, waits, verb_class, class_mask):
|
|
"""ID-84 AS A DERIVATION (ID-116), WITH ID-125's SECOND DISJUNCT.
|
|
|
|
A <field>@<verb> pull is ADMITTED iff the field's row is BARRIER_PULLED, the field is inside
|
|
kMGPipeClassFieldMask[class of verb] - a field outside the verb's own may-read table was
|
|
never filled for it - and EITHER
|
|
|
|
1. the verb's wire op is STATICALLY BARRIERED (MGPipeWaitClassFor(op) != kWaitNone), so the
|
|
client is parked in its own wait and P5C's semantics hold for the record; OR
|
|
2. the field's RETIRING PHASE does not name this phase.
|
|
|
|
ID-125 ADDED (2) AND IT IS THE HONEST STATEMENT OF ID-84. At runtime this table is only ever
|
|
consulted on a record the server already stamped BARRIERED - CountBarrierPull's unbarriered
|
|
arm is [[noreturn]] and fires first - so the record's pull is legal by construction and the
|
|
only remaining question is whether THIS PHASE still owes the migration. The retiring-phase
|
|
column is precisely that answer, and it is already in the table.
|
|
|
|
Disjunct (1) survives as its own term because it is a stronger claim about the same pair: it
|
|
says the client waits for the record STATICALLY, which is what lets a row whose phase IS this
|
|
one still be admitted (GetTextureUnitObject@CopyTexImage2D was, until P15 made
|
|
copy_framebuffer_to_texture fire-and-forget; the self-test barriers that op again to show it).
|
|
Without (1) such a row would fail the lane; without (2) GetTransformFeedbackProgram@DrawArrays would fail it, and CONTRACT-P5E §5.7
|
|
rules transform feedback out of this phase entirely - so the lane would be red on a row no
|
|
package here is allowed to touch.
|
|
|
|
(1) IS A STATEMENT ABOUT EVERY OP THAT STAMPS THE VERB (P9, CONTRACT-P9.md §1). The mask is
|
|
per verb and the server stamps the same verb for each op in MGP_VERB_OP_LIST that names it, so
|
|
one op that publishes without a wait makes the verb's pull torn for THAT op's records.
|
|
read_pixels_to_buffer stamps ReadPixels and waits for nothing, which is why
|
|
GetFramebufferBindingSlot@ReadPixels - admitted by (1) until P9 - no longer is. The first
|
|
version of this function kept the LAST op per verb, so the answer depended on the order of the
|
|
stamp list.
|
|
|
|
A verb with no stamp row still admits NOTHING under (1): the server stamps only the ops
|
|
MGP_VERB_OP_LIST names. Under (2) it admits its non-P5e debts, which is correct for the same
|
|
reason - the mask is consulted only where a stamp already happened.
|
|
|
|
Returns (per-verb (word0, word1), the sorted <field>@<verb> pairs)."""
|
|
field_index = {name: i for i, name in enumerate(accessors)}
|
|
ops_for_verb = {}
|
|
for op, verb in verb_ops:
|
|
ops_for_verb.setdefault(verb, []).append(op)
|
|
|
|
masks = []
|
|
pairs = []
|
|
for verb in verbs:
|
|
words = [0, 0]
|
|
ops = ops_for_verb.get(verb)
|
|
op = ops[0] if ops else None
|
|
barriered = bool(ops) and all(waits.get(o) not in (None, "kWaitNone") for o in ops)
|
|
# A VERB WITH NO STAMP ROW ADMITS NOTHING UNDER EITHER DISJUNCT, and that is not an
|
|
# omission - it is the precondition both disjuncts are stated under. This table is read
|
|
# only from CountBarrierPull, which is reachable only after MGPipeServerStampVerbBoundary,
|
|
# and the server stamps only the ops MGP_VERB_OP_LIST names. A bit set for any other verb
|
|
# would be a row of the allowlist that nothing can exercise and nobody can retire.
|
|
if op is None:
|
|
masks.append((0, 0))
|
|
continue
|
|
cls = verb_class.get(verb)
|
|
if cls is None:
|
|
sys.exit("gen_pipe_field_ownership: verb %s has a stamp row but no verb class" % verb)
|
|
allowed = class_mask[cls]
|
|
for field, index in field_index.items():
|
|
if ownership[field] != "BARRIER_PULLED":
|
|
continue
|
|
if not ((allowed[index // 64] >> (index % 64)) & 1):
|
|
continue
|
|
if not barriered and phase_is_owed_by_this_phase(phase[field]):
|
|
continue
|
|
words[index // 64] |= 1 << (index % 64)
|
|
pairs.append("%s@%s" % (field, verb))
|
|
masks.append((words[0], words[1]))
|
|
return masks, sorted(pairs)
|
|
|
|
|
|
def verb_shaped_calls(calls, verbs):
|
|
"""The calls that MUST have a stamp row or an exemption, by two derived tests: the
|
|
catalogue's own kind (kCtxVerb) and a name that is also a verb's. Neither can see a call
|
|
that is a verb boundary, is not kCtxVerb and is renamed - FieldOwnership.def names the one
|
|
such call in the tree and says the phase that emits it writes its row."""
|
|
verbSet = set(verbs)
|
|
return [name for name, kind in calls if kind == "kCtxVerb" or name in verbSet]
|
|
|
|
|
|
def check_verb_ops(verb_ops, exempt, calls, verbs):
|
|
"""The stamp map, in BOTH directions.
|
|
|
|
A row whose op or verb does not exist would become a switch arm that fails to compile. An
|
|
OMITTED row is worse and is what this check exists for: the applier would run the record
|
|
under the PREVIOUS verb's serial, mask and name, so a field inside that mask reads FRESH
|
|
while holding the previous verb's value - the one failure in this package that is silent."""
|
|
opNames = [name for name, _ in calls]
|
|
if not verb_ops:
|
|
sys.exit("gen_pipe_field_ownership: MGP_VERB_OP_LIST is empty - the server would have "
|
|
"no verb boundary to stamp at and every field would read @<none>")
|
|
seen = set()
|
|
for op, verb in verb_ops:
|
|
if op not in opNames:
|
|
sys.exit("gen_pipe_field_ownership: the stamp map names op %s, which is not a call "
|
|
"in PipeCalls.def" % op)
|
|
if verb not in verbs:
|
|
sys.exit("gen_pipe_field_ownership: the stamp map names verb %s, which is not a "
|
|
"verb in FillPoints.def" % verb)
|
|
if op in seen:
|
|
sys.exit("gen_pipe_field_ownership: op %s has two stamp rows" % op)
|
|
seen.add(op)
|
|
|
|
required = verb_shaped_calls(calls, verbs)
|
|
exemptMap = {}
|
|
for op, why in exempt:
|
|
if op not in opNames:
|
|
sys.exit("gen_pipe_field_ownership: the stamp map exempts op %s, which is not a call "
|
|
"in PipeCalls.def" % op)
|
|
if op not in required:
|
|
sys.exit("gen_pipe_field_ownership: op %s is exempted from the stamp map but is not "
|
|
"verb-shaped, so it was never required - an exemption that exempts nothing "
|
|
"reads as a decision that was made" % op)
|
|
if op in seen:
|
|
sys.exit("gen_pipe_field_ownership: op %s has both a stamp row and an exemption" % op)
|
|
if not why.strip():
|
|
sys.exit("gen_pipe_field_ownership: op %s is exempted with no reason" % op)
|
|
exemptMap[op] = why
|
|
|
|
missing = [op for op in required if op not in seen and op not in exemptMap]
|
|
if missing:
|
|
sys.exit("gen_pipe_field_ownership: %d verb-shaped call(s) have no stamp row and no "
|
|
"exemption: %s - an omitted stamp point is SILENT (the record would apply under "
|
|
"the previous verb's serial, mask and name), so it is a build failure here"
|
|
% (len(missing), ", ".join(missing)))
|
|
return verb_ops, exemptMap, required
|
|
|
|
|
|
def build(accessors, sticky, emitted, refused, rows, forwards, args):
|
|
"""The join, and every gate it is allowed to fail on. Returns
|
|
(ownership, phase, why, forward rows, argument rows, counts)."""
|
|
supplied = [f for f in emitted if f not in set(refused)]
|
|
ownership = {}
|
|
phase = {}
|
|
why = {}
|
|
for field in supplied:
|
|
ownership[field] = "RECORD_SUPPLIED"
|
|
phase[field] = "-"
|
|
why[field] = "derived: Coverage.def's emitted list, and PipeFill.cpp does not refuse it"
|
|
|
|
for field, cls, retires, reason in rows:
|
|
if field not in accessors:
|
|
sys.exit("gen_pipe_field_ownership: FieldOwnership.def names %s, which is not a "
|
|
"PipeInputs field" % field)
|
|
if cls not in CLASSES:
|
|
sys.exit("gen_pipe_field_ownership: %s is in class %s, which is not one of %s"
|
|
% (field, cls, "/".join(CLASSES)))
|
|
if cls == "RECORD_SUPPLIED":
|
|
sys.exit("gen_pipe_field_ownership: %s claims RECORD_SUPPLIED, which is DERIVED and "
|
|
"may not be asserted by hand" % field)
|
|
if field in ownership:
|
|
sys.exit("gen_pipe_field_ownership: %s is in TWO classes - the derivation says "
|
|
"RECORD_SUPPLIED and FieldOwnership.def says %s" % (field, cls))
|
|
if cls == "BARRIER_PULLED" and retires.strip() in ("", "-"):
|
|
sys.exit("gen_pipe_field_ownership: %s is BARRIER_PULLED and names no retiring "
|
|
"phase - P5's debt is only sized if every row says who pays it" % field)
|
|
if cls != "BARRIER_PULLED" and retires.strip() != "-":
|
|
sys.exit("gen_pipe_field_ownership: %s is %s and names a retiring phase; only "
|
|
"BARRIER_PULLED rows have one" % (field, cls))
|
|
ownership[field] = cls
|
|
phase[field] = retires
|
|
why[field] = reason
|
|
|
|
missing = [f for f in accessors if f not in ownership]
|
|
if missing:
|
|
sys.exit("gen_pipe_field_ownership: %d field(s) in NO class, which is a build failure "
|
|
"(R-7.1): %s" % (len(missing), ", ".join(missing)))
|
|
|
|
# The seven sticky forwards' own rows. They are the seven that hand the server a frontend
|
|
# object or write into the frontend, so the gate is structurally blind on them without a
|
|
# row of their own - and the row has to agree with the field row, or the two halves of the
|
|
# same accessor would be documented as different things.
|
|
forward_map = {}
|
|
for field, cls, retires, mechanism in forwards:
|
|
if field not in sticky:
|
|
sys.exit("gen_pipe_field_ownership: %s has a FORWARD row but is not sticky in "
|
|
"Coverage.def" % field)
|
|
if field in forward_map:
|
|
sys.exit("gen_pipe_field_ownership: %s has two FORWARD rows" % field)
|
|
if cls not in CLASSES:
|
|
sys.exit("gen_pipe_field_ownership: forward %s is in class %s, which is not one of "
|
|
"%s" % (field, cls, "/".join(CLASSES)))
|
|
if ownership[field] != cls:
|
|
sys.exit("gen_pipe_field_ownership: %s's field row says %s and its forward row says "
|
|
"%s; a read of a sticky field IS a call of its forward" % (field, ownership[field], cls))
|
|
forward_map[field] = (cls, retires, mechanism)
|
|
absent = [f for f in sticky if f not in forward_map]
|
|
if absent:
|
|
sys.exit("gen_pipe_field_ownership: sticky forward(s) with no row: %s" % ", ".join(absent))
|
|
|
|
arg_rows = []
|
|
for field, arg0, cls, reason in args:
|
|
if field not in accessors:
|
|
sys.exit("gen_pipe_field_ownership: argument exception names %s, which is not a "
|
|
"PipeInputs field" % field)
|
|
if cls not in CLASSES:
|
|
sys.exit("gen_pipe_field_ownership: argument exception %s(%s) is in class %s"
|
|
% (field, arg0, cls))
|
|
if cls == ownership[field]:
|
|
sys.exit("gen_pipe_field_ownership: argument exception %s(%s) repeats the field's "
|
|
"own class (%s) and narrows nothing" % (field, arg0, cls))
|
|
arg_rows.append((field, int(arg0), cls, reason))
|
|
|
|
counts = {cls: sum(1 for f in accessors if ownership[f] == cls) for cls in CLASSES}
|
|
return ownership, phase, why, forward_map, arg_rows, counts
|
|
|
|
|
|
def emit(accessors, sticky, ownership, phase, why, forward_map, arg_rows, counts, verb_ops,
|
|
exemptMap, verbs, admitted_masks, admitted_pairs):
|
|
out = [BANNER.format(name=OUT_NAME)]
|
|
add = out.append
|
|
add("""
|
|
// The four classes. kUnclassified exists so the static_assert below has something to refuse;
|
|
// the generator never emits it, which is what makes "a field in no class fails the build"
|
|
// true at two independent points rather than one.
|
|
enum class MGPipeFieldOwnership : Uint8 {
|
|
kUnclassified = 0,
|
|
kRecordSupplied, // a pushed record supplies the WHOLE field
|
|
kApplierDerived, // the applier writes it out of records it already applies
|
|
kBarrierPulled, // P5's debt: read out of the client's residual fill under the verb barrier
|
|
kFatal, // no carrier and the reduced path never reads it
|
|
};
|
|
|
|
inline constexpr const char* kMGPipeFieldOwnershipNames[] = {
|
|
"UNCLASSIFIED", "RECORD-SUPPLIED", "APPLIER-DERIVED", "BARRIER-PULLED", "FATAL",
|
|
};
|
|
""")
|
|
add("inline constexpr MGPipeFieldOwnership kMGPipeFieldOwnership[kMGPipeInputFieldCount] = {")
|
|
for field in accessors:
|
|
add(" MGPipeFieldOwnership::%s, // %s" % (ENUMERATOR[ownership[field]], field))
|
|
add("};\n")
|
|
|
|
add("// The ROADMAP phase whose row retires the pull. \"-\" for every class but BARRIER-PULLED.")
|
|
add("inline constexpr const char* kMGPipeFieldRetiringPhase[kMGPipeInputFieldCount] = {")
|
|
for field in accessors:
|
|
add(" \"%s\", // %s" % (phase[field], field))
|
|
add("};\n")
|
|
|
|
add("// The seven sticky forwards, which are among the 63 above and need a row of their own:")
|
|
add("// they are the ones that hand the server a raw frontend object or write into the")
|
|
add("// frontend, so the exit gate is structurally blind on them without one.")
|
|
add("inline constexpr SizeT kMGPipeFieldOwnershipForwardCount = %d;" % len(sticky))
|
|
add("static_assert(kMGPipeFieldOwnershipForwardCount == kMGPipeInputStickyFieldCount,")
|
|
add(" \"the forward rows and Coverage.def's sticky set are the same seven\");")
|
|
add("inline constexpr MGPipeInputField kMGPipeFieldOwnershipForwardField[kMGPipeFieldOwnershipForwardCount] = {")
|
|
for field in sticky:
|
|
add(" MGPipeInputField::%s," % field)
|
|
add("};")
|
|
add("inline constexpr MGPipeFieldOwnership kMGPipeFieldOwnershipForward[kMGPipeFieldOwnershipForwardCount] = {")
|
|
for field in sticky:
|
|
add(" MGPipeFieldOwnership::%s, // %s" % (ENUMERATOR[forward_map[field][0]], field))
|
|
add("};")
|
|
add("inline constexpr const char* kMGPipeFieldOwnershipForwardMechanism[kMGPipeFieldOwnershipForwardCount] = {")
|
|
for field in sticky:
|
|
add(" \"%s\", // %s, retires in %s" % (forward_map[field][2], field, forward_map[field][1]))
|
|
add("};\n")
|
|
|
|
add("// CONTRACT-P5.md section 3: \"70 rows, each in exactly one class\".")
|
|
add("inline constexpr SizeT kMGPipeFieldOwnershipRowCount =")
|
|
add(" kMGPipeInputFieldCount + kMGPipeFieldOwnershipForwardCount;")
|
|
add("static_assert(kMGPipeFieldOwnershipRowCount == 70, \"table 2's row count moved\");\n")
|
|
|
|
add("""// An ARGUMENT-KEYED narrowing of one field. The field keeps its single row above; this
|
|
// says that one argument value of it belongs to a different class. Coverage.def's comment on the
|
|
// GetBufferBindingSlot row already rules the shape - "The field is one array, so it stays one
|
|
// row" - and m_pixelStore[2] is the same shape indexed by its own isUnpack argument.
|
|
struct MGPipeFieldArgumentOwnership {
|
|
MGPipeInputField Field;
|
|
Uint32 Arg0;
|
|
MGPipeFieldOwnership Class;
|
|
};""")
|
|
add("inline constexpr SizeT kMGPipeFieldArgumentOwnershipCount = %d;" % len(arg_rows))
|
|
add("inline constexpr MGPipeFieldArgumentOwnership")
|
|
add(" kMGPipeFieldArgumentOwnership[kMGPipeFieldArgumentOwnershipCount] = {")
|
|
for field, arg0, cls, reason in arg_rows:
|
|
add(" {MGPipeInputField::%s, %du, MGPipeFieldOwnership::%s}, // %s"
|
|
% (field, arg0, ENUMERATOR[cls], reason))
|
|
add("};\n")
|
|
|
|
add("""constexpr MGPipeFieldOwnership MGPipeFieldOwnershipOf(MGPipeInputField field) {
|
|
return kMGPipeFieldOwnership[static_cast<SizeT>(field)];
|
|
}
|
|
|
|
// The same answer, narrowed by the accessor's first argument. Every accessor that takes one
|
|
// may call this; only the fields with a row above answer differently from the field's class.
|
|
constexpr MGPipeFieldOwnership MGPipeFieldOwnershipOf(MGPipeInputField field, Uint32 arg0) {
|
|
for (SizeT i = 0; i < kMGPipeFieldArgumentOwnershipCount; ++i) {
|
|
if (kMGPipeFieldArgumentOwnership[i].Field == field &&
|
|
kMGPipeFieldArgumentOwnership[i].Arg0 == arg0) {
|
|
return kMGPipeFieldArgumentOwnership[i].Class;
|
|
}
|
|
}
|
|
return MGPipeFieldOwnershipOf(field);
|
|
}
|
|
|
|
constexpr const char* MGPipeFieldOwnershipName(MGPipeFieldOwnership ownership) {
|
|
return kMGPipeFieldOwnershipNames[static_cast<SizeT>(ownership)];
|
|
}
|
|
|
|
// THE BUILD FAILURE R-7.1 ASKS FOR. The generator refuses to emit an unclassified row, so
|
|
// this can only fire on a hand-edited header - which is exactly the edit the DO NOT EDIT
|
|
// banner cannot prevent on its own.
|
|
constexpr Bool MGPipeEveryFieldIsClassified() {
|
|
for (SizeT i = 0; i < kMGPipeInputFieldCount; ++i) {
|
|
if (kMGPipeFieldOwnership[i] == MGPipeFieldOwnership::kUnclassified) return false;
|
|
}
|
|
for (SizeT i = 0; i < kMGPipeFieldOwnershipForwardCount; ++i) {
|
|
if (kMGPipeFieldOwnershipForward[i] == MGPipeFieldOwnership::kUnclassified) return false;
|
|
}
|
|
return true;
|
|
}
|
|
static_assert(MGPipeEveryFieldIsClassified(),
|
|
"a PipeInputs field is in none of the four ownership classes (CONTRACT-P5 table 2, R-7.1)");
|
|
""")
|
|
add("""// WHERE THE SERVER STAMPS. The wire's op and the fill's verb are different name spaces
|
|
// and do not line up by name (draw_vbo is DrawArrays, blit is BlitFramebuffer), so this is the
|
|
// join. An op with no row is NOT a verb boundary and the applier must not stamp on it.
|
|
//
|
|
// EVERY VERB-SHAPED CALL IS ANSWERED HERE OR EXEMPTED BY NAME, and the generator refuses an
|
|
// omission: a verb-shaped record with no row would apply under the PREVIOUS verb's serial,
|
|
// mask and name, so a field inside that mask would read FRESH while holding the previous
|
|
// verb's value - the one silent failure this table has. The exemptions:""")
|
|
for op in sorted(exemptMap):
|
|
add("// %-16s %s" % (op, exemptMap[op]))
|
|
add("""constexpr MGPipeVerb MGPipeVerbForWireOp(MGPWireOp op) {
|
|
switch (op) {""")
|
|
for op, verb in verb_ops:
|
|
add(" case MGPWireOp::%s: return MGPipeVerb::%s;" % (op, verb))
|
|
add(""" default:
|
|
return MGPipeVerb::kVerbCount;
|
|
}
|
|
}
|
|
""")
|
|
add("inline constexpr SizeT kMGPipeVerbBoundaryOpCount = %d;" % len(verb_ops))
|
|
add("inline constexpr SizeT kMGPipeVerbBoundaryExemptCount = %d;" % len(exemptMap))
|
|
add("")
|
|
add("""// ---- THE §7 ALLOWLIST, DERIVED RATHER THAN WRITTEN (ID-116) --------------------------
|
|
//
|
|
// CONTRACT-P5E §7 lists the barrier-pulled reads the phase ADMITS: debts that are real, ordered
|
|
// and fresh because the client is parked behind the record, and that a LATER phase retires. It
|
|
// was also kept by hand in .github/workflows/test.yml, and that copy was wrong in both
|
|
// directions at once - it omitted GetFramebufferBindingSlot@ReadPixels, the largest survivor,
|
|
// and carried GetTextureObject@CopyImageSubData, which nothing made safe.
|
|
//
|
|
// THE RULE IS ID-84 SAID IN TABLES THAT ALREADY EXIST. A <field>@<verb> pull is admitted iff
|
|
//
|
|
// 1. the field's ownership row is BARRIER-PULLED - it is a debt and not a defect;
|
|
// 2. the verb's wire op is STATICALLY BARRIERED (kMGPipeWaitClasses[op] != kWaitNone), which
|
|
// is exactly "the client is parked in its own wait for this record", so P5C's semantics
|
|
// survive the flip for it; and
|
|
// 3. the field is inside kMGPipeClassFieldMask[class of the verb] - a field outside the
|
|
// verb's own may-read table was never filled for it, so a read there is stale by
|
|
// construction whatever its ownership row says.
|
|
//
|
|
// Which makes the allowlist move with the code instead of beside it: retiring a verb's wait
|
|
// class NARROWS it with no edit, and a new BARRIER_PULLED row widens it only on verbs that
|
|
// wait. A verb with no stamp row admits nothing - the server stamps only MGP_VERB_OP_LIST's
|
|
// ops, so no other verb can be the one a residual pull is reported against.""")
|
|
add("inline constexpr MGPipeFieldMask kMGPipeAdmittedPullMask[kMGPipeVerbCount] = {")
|
|
for verb, (low, high) in zip(verbs, admitted_masks):
|
|
add(" {{0x%016xull, 0x%016xull}}, // %s" % (low, high, verb))
|
|
add("};\n")
|
|
add("inline constexpr SizeT kMGPipeAdmittedPullPairCount = %d;" % len(admitted_pairs))
|
|
add("""
|
|
// THE PREDICATE THE STRICT KNOB ASKS (ID-117). A 69 x 128-bit table, so this costs a shift and
|
|
// a test on the apply thread - the same shape MGPipeFieldMaskHas already has.
|
|
constexpr Bool MGPipeBarrierPullAdmitted(MGPipeInputField field, MGPipeVerb verb) {
|
|
const SizeT index = static_cast<SizeT>(verb);
|
|
return index < kMGPipeVerbCount && MGPipeFieldMaskHas(kMGPipeAdmittedPullMask[index], field);
|
|
}
|
|
|
|
// THE HAND-EDIT CONTROL, MGPipeEveryFieldIsClassified's shape and for its reason: the generator
|
|
// cannot emit a bit that fails this, so it can only fire on an edited header - which is exactly
|
|
// the edit the DO NOT EDIT banner cannot prevent on its own. An admitted bit that was not a
|
|
// BARRIER-PULLED field of its verb's class would be the allowlist quietly forgiving a read that
|
|
// is torn rather than merely unmigrated.
|
|
constexpr Bool MGPipeEveryAdmittedPullIsADebtOfItsVerbsClass() {
|
|
for (SizeT v = 0; v < kMGPipeVerbCount; ++v) {
|
|
const MGPipeFieldMask& admitted = kMGPipeAdmittedPullMask[v];
|
|
const MGPipeFieldMask& mayRead =
|
|
kMGPipeClassFieldMask[static_cast<SizeT>(kMGPipeVerbClass[v])];
|
|
for (SizeT f = 0; f < kMGPipeInputFieldCount; ++f) {
|
|
const auto field = static_cast<MGPipeInputField>(f);
|
|
if (!MGPipeFieldMaskHas(admitted, field)) continue;
|
|
if (kMGPipeFieldOwnership[f] != MGPipeFieldOwnership::kBarrierPulled) return false;
|
|
if (!MGPipeFieldMaskHas(mayRead, field)) return false;
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
static_assert(MGPipeEveryAdmittedPullIsADebtOfItsVerbsClass(),
|
|
"an admitted barrier pull is not a BARRIER-PULLED field of its verb's class "
|
|
"(CONTRACT-P5E section 7, ID-84 / ID-116)");
|
|
""")
|
|
add("// The class sizes, as constants a test can pin without recounting the table.")
|
|
for cls in CLASSES:
|
|
add("inline constexpr SizeT kMGPipe%sFieldCount = %d;"
|
|
% ("".join(p.capitalize() for p in cls.split("_")), counts[cls]))
|
|
add("static_assert(%s == kMGPipeInputFieldCount, \"the four class sizes do not partition the field set\");"
|
|
% " + ".join("kMGPipe%sFieldCount" % "".join(p.capitalize() for p in cls.split("_"))
|
|
for cls in CLASSES))
|
|
return "\n".join(out) + "\n"
|
|
|
|
|
|
def write(path, text, check_only, changed):
|
|
existing = read(path) if os.path.exists(path) else None
|
|
if existing == text:
|
|
return
|
|
changed.append(os.path.basename(path))
|
|
if not check_only:
|
|
with open(path, "w", encoding="utf-8", newline="\n") as handle:
|
|
handle.write(text)
|
|
|
|
|
|
def expect_trip(name, because, fn, quiet=False):
|
|
"""A control that must exit FOR ITS OWN REASON.
|
|
|
|
The first version of this function caught any SystemExit and asked nothing about which one,
|
|
and that is exactly how control #4 came to be a silent duplicate of control #1: its
|
|
replacement string was raw, so it mangled the row instead of blanking the phase, the row
|
|
stopped parsing, and the generator exited with "a field in NO class" while the report
|
|
counted a trip for "a BARRIER_PULLED row with no retiring phase". The guard that every debt
|
|
row names its retiring phase therefore had no control at all.
|
|
|
|
`because` is a substring the control's own message must contain. This is the discipline
|
|
gen_pipe_dirty_surface.py's self_test already uses (it asserts each control's problem
|
|
string) and it is the half that was dropped."""
|
|
try:
|
|
fn()
|
|
except SystemExit as exit:
|
|
message = str(exit.code) if exit.code is not None else ""
|
|
if because in message:
|
|
return 1
|
|
if not quiet:
|
|
print("gen_pipe_field_ownership: self-test: control %r tripped for SOMEONE ELSE'S "
|
|
"reason:\n expected to contain: %s\n actually said: %s"
|
|
% (name, because, message), file=sys.stderr)
|
|
return 0
|
|
if not quiet:
|
|
print("gen_pipe_field_ownership: self-test: control did NOT trip: %s" % name, file=sys.stderr)
|
|
return 0
|
|
|
|
|
|
def require_no_barrier_pulls(ownership):
|
|
pulled = sorted(field for field, cls in ownership.items() if cls == "BARRIER_PULLED")
|
|
if pulled:
|
|
sys.exit("gen_pipe_field_ownership: P5f forbids production BARRIER_PULLED rows: "
|
|
+ ", ".join(pulled))
|
|
|
|
|
|
def self_test():
|
|
"""The negative controls (gen_pipe.py --self-test's shape): each gate must go red for its
|
|
own reason, and zero trips is itself an error."""
|
|
coverage = read(COVERAGE_DEF)
|
|
production_ownership_text = read(OWNERSHIP_DEF)
|
|
# P5f has no live debt. Exercise admission's historical branches on an explicit
|
|
# synthetic fixture, rather than requiring real client reads to keep tests alive.
|
|
ownership_text = production_ownership_text
|
|
fixture_phases = {
|
|
"GetBoundVertexArray": "P5e (Espryt unbarriered), P7 (Magma)",
|
|
"GetBufferBindingSlot": "P8/P9/P13",
|
|
"GetBufferBindingPoint": "P5e (Espryt unbarriered), P7 (Magma)",
|
|
"GetFramebufferBindingSlot": "P5e (Espryt unbarriered), P7 (Magma)",
|
|
"GetImageTextureBinding": "P5e (Espryt unbarriered), P7 (Magma)",
|
|
"GetTextureUnitObject": "P5e (Espryt unbarriered), P7 (Magma)",
|
|
"GetProgramForDraw": "P5e (Espryt unbarriered), P7 (Magma)",
|
|
"GetProgramForDispatch": "P5e (Espryt unbarriered), P7 (Magma)",
|
|
"GetTransformFeedbackProgram": "P3b/P4b (Espryt), P7 (Magma)",
|
|
"GetProgramObject": "P9", "GetTextureObject": "P7",
|
|
"ValidateProgramName": "P9", "RecordError": "P9",
|
|
}
|
|
for field, phase in fixture_phases.items():
|
|
pattern = r'(X\(\s*' + field + r'\s*,)\s*FATAL,\s*"-",'
|
|
ownership_text, count = re.subn(pattern, lambda m: m[1] + ' BARRIER_PULLED, "' + phase + '",', ownership_text)
|
|
if count not in (1, 2):
|
|
sys.exit("gen_pipe_field_ownership: fixture field is not retired: " + field)
|
|
prefix, forward = ownership_text.split("#define MGP_FIELD_OWNERSHIP_FORWARD_LIST(X)", 1)
|
|
forward = re.sub(r'(X\(RecordError,\s*BARRIER_PULLED,\s*"P9",\s*)"[^\"]*"',
|
|
r'\1"OnGlError, synthetic legacy error forward"', forward, count=1)
|
|
forward = re.sub(r'(X\(GetTextureObject,\s*BARRIER_PULLED,\s*"P7",\s*)"[^\"]*"',
|
|
r'\1"a server-side texture handle table"', forward, count=1)
|
|
ownership_text = prefix + "#define MGP_FIELD_OWNERSHIP_FORWARD_LIST(X)" + forward
|
|
fill = read(PIPE_FILL)
|
|
accessors, sticky, emitted = parse_coverage(coverage)
|
|
refused = parse_supplies_whole_field(fill)
|
|
|
|
calls, verbs = parse_ops_and_verbs()
|
|
wire_inc = read(PIPE_WIRE_INC)
|
|
points_inc = read(FILL_POINTS_INC)
|
|
|
|
def run(own_text=None, cov=None, fill_text=None, calls_text=None):
|
|
acc, stk, emt = parse_coverage(cov if cov is not None else coverage)
|
|
ref = parse_supplies_whole_field(fill_text if fill_text is not None else fill)
|
|
rows, fwd, args, verb_ops, exempt = parse_ownership(
|
|
own_text if own_text is not None else ownership_text)
|
|
c, v = parse_ops_and_verbs(calls_text) if calls_text is not None else (calls, verbs)
|
|
check_verb_ops(verb_ops, exempt, c, v)
|
|
return build(acc, stk, emt, ref, rows, fwd, args)
|
|
|
|
# The rows wrap over two lines with a trailing backslash, so every control below edits
|
|
# them through a regex whose gaps tolerate that rather than through a literal that would
|
|
# silently stop matching the day someone re-aligns the file.
|
|
GAP = r"[\s\\]*"
|
|
|
|
def edit(pattern, replacement, what, text=None):
|
|
text = ownership_text if text is None else text
|
|
edited, count = re.subn(pattern, replacement, text, count=1)
|
|
if count != 1:
|
|
sys.exit("gen_pipe_field_ownership: self-test: could not %s - the control's own "
|
|
"edit no longer matches the file it is supposed to break" % what)
|
|
return edited
|
|
|
|
# Every control below is (name, the substring its own message must contain, the edit). The
|
|
# substring is not decoration: see expect_trip.
|
|
|
|
# 1. THE HEADLINE CONTROL (exit gate E4): take one field out of the table. It is in no
|
|
# class, and that is a build failure rather than a silent default. GetBoundVertexArray is
|
|
# the control's field since P5c rv (it keeps a hand-written BARRIER_PULLED row; the value
|
|
# rows the first version used are RECORD_SUPPLIED-derived now, so they have no row to
|
|
# edit).
|
|
dropped = edit(r"X\(GetBoundVertexArray," + GAP + r"BARRIER_PULLED," + GAP + r"\"[^\"]*\","
|
|
+ GAP + r"\"[^\"]*\"\)", "", "remove GetBoundVertexArray's row")
|
|
controls = [("a field in NO class (GetBoundVertexArray's row removed)",
|
|
"field(s) in NO class",
|
|
lambda: run(own_text=dropped))]
|
|
|
|
# 2. The other direction: a field the derivation already placed in RECORD_SUPPLIED, also
|
|
# claimed by hand. E4's negative control is "move a field from supplied to FATAL".
|
|
doubled = ownership_text.replace(
|
|
"#define MGP_FIELD_OWNERSHIP_LIST(X)",
|
|
"#define MGP_FIELD_OWNERSHIP_LIST(X) X(GetClearColor, FATAL, \"-\", \"moved by hand\") \\\n", 1)
|
|
controls.append(("a RECORD_SUPPLIED field claimed by hand (supplied -> FATAL)",
|
|
"GetClearColor is in TWO classes",
|
|
lambda: run(own_text=doubled)))
|
|
|
|
# 3. A row naming something that is not a field at all.
|
|
typo = edit(r"X\(GetBoundVertexArray,", "X(GetBoundVertexArrayy,", "misspell a field name")
|
|
controls.append(("a row naming a non-field",
|
|
"GetBoundVertexArrayy, which is not a PipeInputs field",
|
|
lambda: run(own_text=typo)))
|
|
|
|
# 4. A BARRIER_PULLED row with no retiring phase: the debt is only sized if every row
|
|
# says who pays it, which is the whole of R-7.2's "rsp IS the size of the debt".
|
|
# THE REPLACEMENT IS NOT A RAW STRING. It was, and the backslashes survived into the
|
|
# substitution, mangled the row past ROW_RE's reach and made this control a silent
|
|
# duplicate of #1 for a whole round.
|
|
unphased = edit(r"(X\(GetBoundVertexArray," + GAP + r"BARRIER_PULLED,)" + GAP + r"\"[^\"]*\",",
|
|
"\\1 \"-\",", "blank a BARRIER_PULLED row's retiring phase")
|
|
controls.append(("a BARRIER_PULLED row with no retiring phase",
|
|
"GetBoundVertexArray is BARRIER_PULLED and names no retiring phase",
|
|
lambda: run(own_text=unphased)))
|
|
|
|
# 5. A class that is not one of the four.
|
|
bogus = edit(r"(X\(GetBoundVertexArray,)" + GAP + r"BARRIER_PULLED,",
|
|
"\\1 SOMEHOW_FINE,", "introduce a fifth class")
|
|
controls.append(("a fifth class",
|
|
"GetBoundVertexArray is in class SOMEHOW_FINE",
|
|
lambda: run(own_text=bogus)))
|
|
|
|
# 6. A sticky forward that lost its own row - the seven most dangerous fields are exactly
|
|
# the ones a table without forward rows is blind to.
|
|
no_forward = edit(r"X\(RecordError," + GAP + r"BARRIER_PULLED," + GAP + r"\"P9\"," + GAP
|
|
+ r"\"OnGlError[^\"]*\"\)", "", "remove RecordError's forward row")
|
|
controls.append(("a sticky forward with no row",
|
|
"sticky forward(s) with no row: RecordError",
|
|
lambda: run(own_text=no_forward)))
|
|
|
|
# 7. A forward row that disagrees with its field row.
|
|
disagree = edit(r"X\(GetTextureObject," + GAP + r"BARRIER_PULLED," + GAP + r"\"P7\"," + GAP
|
|
+ r"\"a server-side texture handle table\"\)",
|
|
"X(GetTextureObject, FATAL, \"-\", \"a server-side texture handle table\")",
|
|
"contradict GetTextureObject's field row")
|
|
controls.append(("a forward row that contradicts its field row",
|
|
"field row says BARRIER_PULLED and its forward row says FATAL",
|
|
lambda: run(own_text=disagree)))
|
|
|
|
# 8. An argument exception that narrows nothing.
|
|
same = edit(r"X\(GetPixelStoreParameters, 1, FATAL,",
|
|
"X(GetPixelStoreParameters, 1, APPLIER_DERIVED,",
|
|
"make the argument exception repeat the field's class")
|
|
controls.append(("an argument exception that repeats the field's class",
|
|
"narrows nothing",
|
|
lambda: run(own_text=same)))
|
|
|
|
# 9. THE DERIVATION'S OWN SOURCE. If EmittedCallSuppliesTheWholeField's refusals stop
|
|
# parsing, every emitted field silently becomes RECORD_SUPPLIED and eight rows of this
|
|
# table quietly contradict themselves - so an empty refusal set has to stop the script
|
|
# rather than produce a plausible table.
|
|
blinded = fill.replace("Bool EmittedCallSuppliesTheWholeField(MGPipeInputField field)",
|
|
"Bool EmittedCallSuppliesTheWholeFieldXX(MGPipeInputField field)", 1)
|
|
controls.append(("the derivation's source function renamed away",
|
|
"EmittedCallSuppliesTheWholeField is not in PipeFill.cpp",
|
|
lambda: run(fill_text=blinded)))
|
|
|
|
# 10-11. THE STAMP MAP against both name spaces.
|
|
bad_op = edit(r"X\(Clear,\s*Clear\)", "X(Klear, Clear)", "misspell a stamp map op")
|
|
controls.append(("a stamp row naming an op that does not exist",
|
|
"names op Klear, which is not a call in PipeCalls.def",
|
|
lambda: run(own_text=bad_op)))
|
|
bad_verb = edit(r"X\(DrawVbo,\s*DrawArrays\)", "X(DrawVbo, DrawArrayz)",
|
|
"misspell a stamp map verb")
|
|
controls.append(("a stamp row naming a verb that does not exist",
|
|
"names verb DrawArrayz, which is not a verb in FillPoints.def",
|
|
lambda: run(own_text=bad_verb)))
|
|
|
|
# 12. THE OMISSION, which the first version of this gate could not see at all. A
|
|
# verb-shaped call with neither a row nor an exemption is the one silent failure in
|
|
# this package: the record applies under the PREVIOUS verb's serial, mask and name.
|
|
no_row = edit(r"X\(GenerateMipmap,\s*GenerateMipmap\)", "", "remove GenerateMipmap's stamp row")
|
|
controls.append(("a verb-shaped call with no stamp row and no exemption",
|
|
"have no stamp row and no exemption: GenerateMipmap",
|
|
lambda: run(own_text=no_row)))
|
|
|
|
# 13. An exemption is a decision, so it may not be written for a call that was never
|
|
# required - that would read as a ruling where there was none.
|
|
idle = edit(r"#define MGP_VERB_OP_EXEMPT_LIST\(X\)",
|
|
"#define MGP_VERB_OP_EXEMPT_LIST(X) X(SetDynamicState, \"not verb-shaped\") \\\n",
|
|
"exempt a call that was never required")
|
|
controls.append(("an exemption for a call that is not verb-shaped",
|
|
"SetDynamicState is exempted from the stamp map but is not verb-shaped",
|
|
lambda: run(own_text=idle)))
|
|
|
|
# 14. An exemption with no reason is an absence with extra steps.
|
|
mute = edit(r"X\(Flush," + GAP + r"\"", "X(Flush, \"\" \"", "blank an exemption's reason")
|
|
controls.append(("an exemption with no reason",
|
|
"Flush is exempted with no reason",
|
|
lambda: run(own_text=mute)))
|
|
|
|
# 15. THE REQUIRED SET'S OWN SOURCE. verb_shaped_calls reads PipeCalls.def's KIND column; if
|
|
# that column stops parsing as kCtxVerb the required set collapses to the name matches
|
|
# alone and control 12 would pass for the wrong reason. Renaming the kind is the cheapest
|
|
# way to prove the kind is actually being read.
|
|
kindless = read(PIPE_CALLS).replace("kCtxVerb", "kCtxVerbb")
|
|
controls.append(("the catalogue's kCtxVerb kind renamed away",
|
|
"is exempted from the stamp map but is not verb-shaped",
|
|
lambda: run(calls_text=kindless)))
|
|
|
|
# ---- 16-18: THE ADMISSION DERIVATION'S OWN SOURCES (P5e gl, ID-116) -------------------
|
|
#
|
|
# The allowlist is DERIVED from three generated tables. Each of them is read rather than
|
|
# restated, so each of them can go missing - and a missing one does not produce a visibly
|
|
# broken allowlist, it produces a SILENTLY EMPTY or SILENTLY WIDER one. An empty admitted
|
|
# set reads in the lane as "nothing is admitted", which looks like rigour and is blindness.
|
|
def admitted_pairs_for(own_text=None, wire_text=None, points_text=None):
|
|
own, ph, _, _, _, _ = run(own_text=own_text)
|
|
_, _, _, verb_ops_now, _ = parse_ownership(
|
|
own_text if own_text is not None else ownership_text)
|
|
waits_now = parse_wait_classes(wire_text if wire_text is not None else wire_inc)
|
|
verb_class_now, class_mask_now = parse_verb_classes(
|
|
points_text if points_text is not None else points_inc)
|
|
return build_admitted(accessors, own, ph, verbs, verb_ops_now, waits_now, verb_class_now,
|
|
class_mask_now)[1]
|
|
|
|
no_waits = wire_inc.replace("kMGPipeWaitClasses[static_cast<SizeT>(MGPWireOp::kOpCount)] =",
|
|
"kMGPipeWaitClassesXX[static_cast<SizeT>(MGPWireOp::kOpCount)] =", 1)
|
|
controls.append(("the wait-class column renamed away",
|
|
"kMGPipeWaitClasses",
|
|
lambda: admitted_pairs_for(wire_text=no_waits)))
|
|
no_verb_class = points_inc.replace("kMGPipeVerbClass[kMGPipeVerbCount] =",
|
|
"kMGPipeVerbClassXX[kMGPipeVerbCount] =", 1)
|
|
controls.append(("the verb-class column renamed away",
|
|
"kMGPipeVerbClass[kMGPipeVerbCount]",
|
|
lambda: admitted_pairs_for(points_text=no_verb_class)))
|
|
no_class_mask = points_inc.replace("kMGPipeClassFieldMask[kMGPipeVerbClassCount] =",
|
|
"kMGPipeClassFieldMaskXX[kMGPipeVerbClassCount] =", 1)
|
|
controls.append(("the class field mask renamed away",
|
|
"kMGPipeClassFieldMask[kMGPipeVerbClassCount]",
|
|
lambda: admitted_pairs_for(points_text=no_class_mask)))
|
|
|
|
# THE HARNESS'S OWN CONTROL, and it is the durable form of how M-1 was found. The defect was
|
|
# not the escaping in control #4; it was that expect_trip asked "did something exit" rather
|
|
# than "did THIS exit", so a control could silently become a duplicate of another. Prove the
|
|
# harness can tell them apart: control #1's edit, asserted against control #4's reason, must
|
|
# be REJECTED. Without this line the stricter harness could itself rot back.
|
|
if expect_trip("(harness control) control #1's edit under control #4's reason",
|
|
"names no retiring phase", lambda: run(own_text=dropped), quiet=True) != 0:
|
|
sys.exit("gen_pipe_field_ownership: self-test: expect_trip accepted an exit that belongs "
|
|
"to another control - the harness cannot tell one control from another, which is "
|
|
"exactly the defect that let control #4 be a silent duplicate of control #1")
|
|
|
|
controls.append(("a retired field is reintroduced as production debt",
|
|
"P5f forbids production BARRIER_PULLED rows",
|
|
lambda: require_no_barrier_pulls(run()[0])))
|
|
|
|
trips = 0
|
|
for name, because, fn in controls:
|
|
trips += expect_trip(name, because, fn)
|
|
|
|
# The positive control: the real tables pass, and they partition the real field set.
|
|
production = run(own_text=production_ownership_text)
|
|
require_no_barrier_pulls(production[0])
|
|
counts = production[-1]
|
|
total = sum(counts.values())
|
|
if total != len(accessors):
|
|
sys.exit("gen_pipe_field_ownership: self-test: the positive control does not partition "
|
|
"the field set (%d of %d)" % (total, len(accessors)))
|
|
if len(sticky) != 7:
|
|
sys.exit("gen_pipe_field_ownership: self-test: Coverage.def no longer has seven sticky fields")
|
|
# EIGHT SINCE P5e (5.6): GetBufferBindingPoint joined the seven
|
|
# when set_shader_buffers got its Coverage.def emitted row. The number is pinned rather
|
|
# than merely derived because it is the SIZE OF THE SHAPE-ONLY SET - the rows where an
|
|
# emitted call exists and still does not supply the field - and a row that quietly left
|
|
# that set would flip to RECORD_SUPPLIED and let the residual fill skip a pull nothing
|
|
# replaces. Every addition to it is a phase's deliberate act, so it is spelled here.
|
|
if len(refused) != 8:
|
|
sys.exit("gen_pipe_field_ownership: self-test: EmittedCallSuppliesTheWholeField refuses %d "
|
|
"fields, not the eight the contract's derivation is written against" % len(refused))
|
|
# ---- THE ADMISSION DERIVATION, MOVED AND READ BACK (P5e gl, ID-116) ------------------
|
|
#
|
|
# Controls 16-18 prove the three sources are READ. These prove the three CONJUNCTS are
|
|
# USED: move each input and watch the derived allowlist move with it. A derivation that
|
|
# quietly ignored one of them would still produce a plausible table - which is exactly how
|
|
# the hand-kept copy in test.yml came to be wrong in BOTH directions at once.
|
|
derived = admitted_pairs_for()
|
|
waits_real = parse_wait_classes(wire_inc)
|
|
derivation = []
|
|
|
|
def expect(name, condition):
|
|
derivation.append((name, bool(condition)))
|
|
|
|
# ---- ID-125's six survivors, each by the disjunct that carries it --------------------
|
|
# P9 moved the first of them: read_pixels_to_buffer stamps ReadPixels and waits for nothing,
|
|
# so ReadPixels is no longer statically barriered and its P5e-owed pair leaves (the P9
|
|
# controls below put it back by barriering that op, and take it away again from the other op).
|
|
expect("GetFramebufferBindingSlot@ReadPixels is REJECTED since P9 (read_pixels_to_buffer "
|
|
"stamps ReadPixels without a wait)",
|
|
"GetFramebufferBindingSlot@ReadPixels" not in derived)
|
|
# P15 moved the second: copy_framebuffer_to_texture is fire-and-forget (kWaitNone), so
|
|
# CopyTexImage2D is no longer statically barriered and its P5e-owed pair leaves too. The
|
|
# control below barriers that op again and the pair must come back by disjunct 1.
|
|
expect("GetTextureUnitObject@CopyTexImage2D is REJECTED since P15 (copy_framebuffer_to_texture "
|
|
"waits for nothing)",
|
|
"GetTextureUnitObject@CopyTexImage2D" not in derived)
|
|
# Disjunct 2's three. Each is a debt some LATER phase owes, on a verb this phase does not
|
|
# barrier - and CONTRACT-P5E §5.7 rules transform feedback out of P5e entirely, so the
|
|
# static rule alone would have failed the lane on a row no package here may touch.
|
|
expect("GetTransformFeedbackProgram@DrawArrays is admitted by disjunct 2 (retires P3b/P4b)",
|
|
"GetTransformFeedbackProgram@DrawArrays" in derived)
|
|
expect("GetTextureObject@CopyImageSubData is admitted (retires P7)",
|
|
"GetTextureObject@CopyImageSubData" in derived)
|
|
expect("ValidateProgramName@ShaderStorageBlockBinding is admitted (retires P9)",
|
|
"ValidateProgramName@ShaderStorageBlockBinding" in derived)
|
|
# ... and the two rows this phase OWES are still rejected: both are P5e rows on an
|
|
# unbarriered verb, which is exactly the debt pa and mv are retiring.
|
|
expect("GetProgramForDraw@DrawArrays is REJECTED (a P5e row on an unbarriered verb)",
|
|
"GetProgramForDraw@DrawArrays" not in derived)
|
|
expect("GetBoundVertexArray@DrawArrays is REJECTED (a P5e row on an unbarriered verb)",
|
|
"GetBoundVertexArray@DrawArrays" not in derived)
|
|
|
|
# Conjunct 2, the wait class. ReadPixels is kWaitReply so its pairs are admitted; make the
|
|
# op kWaitNone and every @ReadPixels pair must leave, because an unbarriered record's read
|
|
# is torn BY CONSTRUCTION and no ownership row can make it legal.
|
|
# THE EDIT IS COUNTED, NOT DIFFED. ResourceCopyRegion below is ALREADY kWaitNone today, so a
|
|
# "did the text change" guard would call its own control broken while it was working
|
|
# perfectly - and once item 5 moves that op, the same guard would start passing for a
|
|
# different reason. What has to hold is that the row was FOUND.
|
|
def set_wait(op, wait_class, text=None):
|
|
edited, count = re.subn(
|
|
r"(/\*\s*\d+\s+" + op + r"\s*\*/\s*static_cast<Uint8>\()kWait\w+(\))",
|
|
r"\g<1>" + wait_class + r"\2", wire_inc if text is None else text, count=1)
|
|
if count != 1:
|
|
sys.exit("gen_pipe_field_ownership: self-test: could not set %s's wait class - the "
|
|
"control's own edit no longer matches generated/PipeWire.inc" % op)
|
|
return edited
|
|
|
|
def unbarrier(op, text=None):
|
|
return set_wait(op, "kWaitNone", text)
|
|
|
|
# P9: EVERY OP THAT STAMPS THE VERB. Barrier read_pixels_to_buffer as well and ReadPixels is
|
|
# statically barriered again, so its P5e-owed pair comes back by disjunct 1 - which proves the
|
|
# pair left above because of THAT op and not for some other reason.
|
|
rewaited = set_wait("ReadPixelsToBuffer", "kWaitApplied")
|
|
expect("barriering read_pixels_to_buffer too brings GetFramebufferBindingSlot@ReadPixels back "
|
|
"(disjunct 1 needs every op that stamps the verb to wait)",
|
|
"GetFramebufferBindingSlot@ReadPixels" in admitted_pairs_for(wire_text=rewaited))
|
|
unwaited = unbarrier("ReadPixels", rewaited)
|
|
expect("unbarriering ReadPixels' own op drops the pair again "
|
|
"(GetFramebufferBindingSlot@ReadPixels) and keeps the later phases' pairs",
|
|
"GetFramebufferBindingSlot@ReadPixels" not in admitted_pairs_for(wire_text=unwaited)
|
|
and "GetTextureObject@ReadPixels" in admitted_pairs_for(wire_text=unwaited))
|
|
|
|
recopied = set_wait("CopyFramebufferToTexture", "kWaitApplied")
|
|
expect("barriering copy_framebuffer_to_texture brings GetTextureUnitObject@CopyTexImage2D back "
|
|
"(disjunct 1)",
|
|
"GetTextureUnitObject@CopyTexImage2D" in admitted_pairs_for(wire_text=recopied))
|
|
|
|
# The same disjunct from the other side. ID-118 moved ResourceCopyRegion to a barriered wait
|
|
# class; unbarrier it again and its P5e-owed pairs go, while GetTextureObject stays admitted
|
|
# on ID-125's second disjunct because it retires in P7. BOTH disjuncts hold for that pair
|
|
# today and this control is what says they are independent rather than one masking the other.
|
|
uncopied = unbarrier("ResourceCopyRegion")
|
|
expect("unbarriering ResourceCopyRegion drops its P5e-owed @CopyImageSubData pairs",
|
|
"GetFramebufferBindingSlot@CopyImageSubData"
|
|
not in admitted_pairs_for(wire_text=uncopied))
|
|
expect("GetTextureObject@CopyImageSubData is admitted by BOTH disjuncts (ID-118 and ID-125)",
|
|
"GetTextureObject@CopyImageSubData" in admitted_pairs_for(wire_text=uncopied)
|
|
and "GetTextureObject@CopyImageSubData" in derived)
|
|
|
|
# ID-125's DISJUNCT 2, MOVED: make the transform-feedback row this phase's debt and it must
|
|
# leave the allowlist on the unbarriered draw verb. Without this the second disjunct could
|
|
# be a constant `true` and every control above would still hold.
|
|
owed_now = edit(r"X\(GetTransformFeedbackProgram," + GAP + r"BARRIER_PULLED," + GAP
|
|
+ r"\"[^\"]*\",",
|
|
"X(GetTransformFeedbackProgram, BARRIER_PULLED, \"P5e (moved by the control)\",",
|
|
"make GetTransformFeedbackProgram this phase's debt")
|
|
expect("a row whose retiring phase becomes P5e leaves the unbarriered verb's allowlist",
|
|
"GetTransformFeedbackProgram@DrawArrays" not in admitted_pairs_for(own_text=owed_now))
|
|
|
|
# Conjunct 1, the ownership row: a field that stops being a debt stops being admitted.
|
|
not_a_debt = edit(r"X\(GetFramebufferBindingSlot," + GAP + r"BARRIER_PULLED," + GAP
|
|
+ r"\"[^\"]*\"," + GAP,
|
|
"X(GetFramebufferBindingSlot, FATAL, \"-\", ",
|
|
"make GetFramebufferBindingSlot FATAL")
|
|
expect("a field that stops being BARRIER_PULLED leaves the allowlist",
|
|
not any(p.startswith("GetFramebufferBindingSlot@")
|
|
for p in admitted_pairs_for(own_text=not_a_debt)))
|
|
|
|
# AND THE RULE OVER THE WHOLE TABLE, not just its six named rows: nothing THIS PHASE owes is
|
|
# ever admitted on a verb no barriered op stamps. If this goes false the allowlist has
|
|
# started forgiving the debt P5e exists to retire.
|
|
# A verb is unbarriered when ANY op that stamps it publishes without a wait (P9) - the same
|
|
# rule build_admitted states, restated here so that the two cannot drift together.
|
|
ops_for_verb = {}
|
|
for op, verb in parse_ownership(ownership_text)[3]:
|
|
ops_for_verb.setdefault(verb, []).append(op)
|
|
ownership_now, phase_now = run()[0], run()[1]
|
|
unbarriered_p5e = sorted(
|
|
pair for pair in derived
|
|
if (lambda f, v: (not ops_for_verb.get(v)
|
|
or any(waits_real.get(o) in (None, "kWaitNone") for o in ops_for_verb[v]))
|
|
and phase_is_owed_by_this_phase(phase_now[f]))(*pair.split("@", 1)))
|
|
expect("no pair this phase owes is admitted on an unbarriered verb: "
|
|
+ (", ".join(unbarriered_p5e) or "none"),
|
|
not unbarriered_p5e)
|
|
|
|
failed = [name for name, ok in derivation if not ok]
|
|
if failed:
|
|
sys.exit("gen_pipe_field_ownership: self-test: %d admission-derivation control(s) did "
|
|
"not hold: %s" % (len(failed), "; ".join(failed)))
|
|
|
|
if trips == 0:
|
|
sys.exit("gen_pipe_field_ownership: self-test: no negative control tripped - the gates are "
|
|
"not checking anything")
|
|
if trips != len(controls):
|
|
sys.exit("gen_pipe_field_ownership: self-test: %d of %d negative controls did not trip"
|
|
% (len(controls) - trips, len(controls)))
|
|
print("gen_pipe_field_ownership: self-test: %d negative-control trip(s), each asserted against "
|
|
"its OWN message; harness control OK; positive control OK "
|
|
"(%d fields partitioned, 7 sticky forwards, 8 refusals)" % (trips, total))
|
|
print("gen_pipe_field_ownership: self-test: %d admission-derivation control(s) held; the "
|
|
"synthetic legacy allowlist is %d pair(s); production has zero debt"
|
|
% (len(derivation), len(derived)))
|
|
return 0
|
|
|
|
|
|
def main():
|
|
parser = argparse.ArgumentParser(description=__doc__)
|
|
parser.add_argument("--check", action="store_true",
|
|
help="do not write; exit 1 if regenerating would change anything")
|
|
parser.add_argument("--self-test", action="store_true",
|
|
help="run the negative controls (each gate must trip) and exit")
|
|
parser.add_argument("--print-admitted", action="store_true",
|
|
help="print the derived CONTRACT-P5E section 7 allowlist, one "
|
|
"<field>@<verb> per line, and exit - so the CI shell and the C++ "
|
|
"read the SAME table (ID-116)")
|
|
args = parser.parse_args()
|
|
|
|
if args.self_test:
|
|
return self_test()
|
|
|
|
accessors, sticky, emitted = parse_coverage()
|
|
refused = parse_supplies_whole_field()
|
|
rows, forwards, arg_rows, verb_ops, exempt = parse_ownership()
|
|
calls, verbs = parse_ops_and_verbs()
|
|
_, exemptMap, required = check_verb_ops(verb_ops, exempt, calls, verbs)
|
|
ownership, phase, why, forward_map, arg_list, counts = build(
|
|
accessors, sticky, emitted, refused, rows, forwards, arg_rows)
|
|
require_no_barrier_pulls(ownership)
|
|
waits = parse_wait_classes()
|
|
verb_class, class_mask = parse_verb_classes()
|
|
admitted_masks, admitted_pairs = build_admitted(
|
|
accessors, ownership, phase, verbs, verb_ops, waits, verb_class, class_mask)
|
|
|
|
if args.print_admitted:
|
|
# STDOUT IS THE INTERFACE. One pair per line, sorted, nothing else - the lane's marker
|
|
# ratchet reads this and compares it against what the run actually logged, so a
|
|
# decorated line here is a false red there.
|
|
for pair in admitted_pairs:
|
|
print(pair)
|
|
return 0
|
|
|
|
if not os.path.isdir(GENERATED_DIR):
|
|
os.makedirs(GENERATED_DIR)
|
|
changed = []
|
|
write(os.path.join(GENERATED_DIR, OUT_NAME),
|
|
emit(accessors, sticky, ownership, phase, why, forward_map, arg_list, counts, verb_ops,
|
|
exemptMap, verbs, admitted_masks, admitted_pairs),
|
|
args.check, changed)
|
|
|
|
print("gen_pipe_field_ownership: %d fields + %d sticky forwards = %d rows; "
|
|
"%d record-supplied (derived), %d applier-derived, %d barrier-pulled, %d fatal, "
|
|
"%d argument exception(s)"
|
|
% (len(accessors), len(sticky), len(accessors) + len(sticky),
|
|
counts["RECORD_SUPPLIED"], counts["APPLIER_DERIVED"], counts["BARRIER_PULLED"],
|
|
counts["FATAL"], len(arg_list)))
|
|
print("gen_pipe_field_ownership: stamp map: %d verb-shaped call(s) = %d row(s) + %d "
|
|
"exemption(s), 0 unanswered"
|
|
% (len(required), len(verb_ops), len(exemptMap)))
|
|
admitted_verbs = sorted({pair.split("@", 1)[1] for pair in admitted_pairs})
|
|
print("gen_pipe_field_ownership: section 7 allowlist (derived): %d admitted <field>@<verb> "
|
|
"pair(s) across %d barriered verb(s): %s"
|
|
% (len(admitted_pairs), len(admitted_verbs), ", ".join(admitted_verbs) or "-"))
|
|
pulled = [(f, phase[f]) for f in accessors if ownership[f] == "BARRIER_PULLED"]
|
|
print("gen_pipe_field_ownership: the debt, by retiring phase:")
|
|
by_phase = {}
|
|
for field, retires in pulled:
|
|
by_phase.setdefault(retires, []).append(field)
|
|
for retires in sorted(by_phase):
|
|
print("gen_pipe_field_ownership: %-42s %d" % (retires, len(by_phase[retires])))
|
|
|
|
if changed:
|
|
if args.check:
|
|
print("gen_pipe_field_ownership: OUT OF DATE: %s" % ", ".join(changed), file=sys.stderr)
|
|
return 1
|
|
print("gen_pipe_field_ownership: wrote %s" % ", ".join(changed))
|
|
else:
|
|
print("gen_pipe_field_ownership: generated file is up to date")
|
|
return 0
|
|
|
|
|
|
if __name__ == "__main__":
|
|
sys.exit(main())
|