mirror of
https://github.com/MobileGL-Dev/MobileGL
synced 2026-11-07 01:53:24 +09:00
swung0x48
faf19a6aaa
- ID-116's static rule failed on a row no package in this phase may touch. pa retired the per-draw program pull, which unmasked GetTransformFeedbackProgram@DrawArrays (11 entries): BARRIER_PULLED, on kWaitNone draw_vbo, and ruled out of P5e entirely by CONTRACT-P5E section 5.7, with a retiring phase of "P3b/P4b (Espryt), P7 (Magma)". The rule was wrong, not the code. - A pull is now admitted if the field is BARRIER_PULLED, the verb has a stamp row, the field is in the verb class's may-read mask, and EITHER the verb's op is statically barriered OR the field's retiring phase does not name P5e. 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 pull is legal by construction and the only open question is whose debt it is. The retiring-phase column is exactly that answer and was already in the table. - A verb with NO stamp row still admits nothing under either disjunct: the server stamps only MGP_VERB_OP_LIST's ops, so any other bit would be a row nothing can exercise. 111 -> 174 pairs. - The phase column is matched as a TOKEN, not a substring, so a "P5" or a future "P5e2" cannot answer for "P5e". - All six of ID-125's survivors checked: GetFramebufferBindingSlot@ReadPixels and GetTextureUnitObject@CopyTexImage2D by disjunct 1; GetTransformFeedbackProgram@DrawArrays (P3b/P4b), GetTextureObject@CopyImageSubData (P7) and ValidateProgramName@ShaderStorageBlockBinding (P9) by disjunct 2. GetTextureObject@CopyImageSubData holds by BOTH, asserted separately. GetProgramForDraw@DrawArrays, GetBoundVertexArray@DrawArrays and GetProgramForDispatch@DispatchCompute stay rejected. - Magma's GetFramebufferBindingSlot@Clear is NOT admitted and cannot be: the retiring-phase column is one string for both backends and it names P5e for Espryt. The DirectVulkan entries get their own lane label instead (item 7), which keeps the Espryt allowlist about Espryt. - StrictErrorsAlsoPromotesTheStickyForwards is RENAMED to StrictErrorsReachTheStickyForwardsAndNameThemByField and restated. Not one of the seven sticky forwards names P5e (P7, P7/P9, P7/P13, P9), so on a stamped verb they are all admitted now. The claim that still has teeth is that the detector REACHES them - asserted by rsp moving and by the marker naming the field and its phase, so "did not abort" cannot pass for "never detected". The Fatal half keeps its own case next door on GetBoundVertexArray, a P5e row. - Six new derivation controls, including one that makes GetTransformFeedbackProgram this phase's debt and requires it to leave the unbarriered verb's allowlist - without which disjunct 2 could be a constant `true` and every other control would still hold.
1172 lines
63 KiB
Python
1172 lines
63 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 (GetFramebufferBindingSlot@ReadPixels, GetTextureUnitObject@CopyTexImage2D) still be
|
|
admitted. Without (1) those two 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.
|
|
|
|
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)}
|
|
op_for_verb = {}
|
|
for op, verb in verb_ops:
|
|
op_for_verb[verb] = op
|
|
|
|
masks = []
|
|
pairs = []
|
|
for verb in verbs:
|
|
words = [0, 0]
|
|
op = op_for_verb.get(verb)
|
|
barriered = op is not None and waits.get(op) not in (None, "kWaitNone")
|
|
# 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:62-69 already
|
|
// rules the shape for GetBufferBindingSlot - "THE ROW STAYS ONE ROW ... the field is ONE array
|
|
// that a second row of the same name could only duplicate" - 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 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)
|
|
ownership_text = read(OWNERSHIP_DEF)
|
|
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")
|
|
|
|
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.
|
|
_, _, _, _, _, counts = run()
|
|
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 (MG_Remote/CONTRACT-P5E.md 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 --------------------
|
|
expect("GetFramebufferBindingSlot@ReadPixels is admitted by disjunct 1 (read_pixels waits)",
|
|
"GetFramebufferBindingSlot@ReadPixels" in derived)
|
|
expect("GetTextureUnitObject@CopyTexImage2D is admitted by disjunct 1",
|
|
"GetTextureUnitObject@CopyTexImage2D" 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 unbarrier(op):
|
|
edited, count = re.subn(
|
|
r"(/\*\s*\d+\s+" + op + r"\s*\*/\s*static_cast<Uint8>\()kWait\w+(\))",
|
|
r"\1kWaitNone\2", wire_inc, count=1)
|
|
if count != 1:
|
|
sys.exit("gen_pipe_field_ownership: self-test: could not unbarrier %s - the control's "
|
|
"own edit no longer matches generated/PipeWire.inc" % op)
|
|
return edited
|
|
|
|
unwaited = unbarrier("ReadPixels")
|
|
expect("unbarriering ReadPixels' op drops its P5e-owed pair "
|
|
"(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))
|
|
|
|
# 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.
|
|
op_for_verb = {verb: op for op, verb in parse_ownership(ownership_text)[3]}
|
|
ownership_now, phase_now = run()[0], run()[1]
|
|
unbarriered_p5e = sorted(
|
|
pair for pair in derived
|
|
if (lambda f, v: (op_for_verb.get(v) is None
|
|
or waits_real.get(op_for_verb[v]) in (None, "kWaitNone"))
|
|
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 "
|
|
"derived section 7 allowlist is %d <field>@<verb> pair(s)"
|
|
% (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)
|
|
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())
|