[Fix, CI] (Pipe): order the byte-identity listing, prove every protected region reaches its closing brace, and pin the include-closure probe count

This commit is contained in:
2026-09-08 19:08:12 -04:00
committed by rereview
parent ea38cfcb99
commit 993ce0fb76
2 changed files with 118 additions and 41 deletions
+10 -1
View File
@@ -790,7 +790,16 @@ jobs:
run: sudo apt-get update && sudo apt-get install -y clang-20 libx11-dev run: sudo apt-get update && sudo apt-get install -y clang-20 libx11-dev
- name: Include-closure assertions and negative control - name: Include-closure assertions and negative control
run: python3 scripts/check_include_closure.py --mode both --compiler clang++-20 --self-test --require-all # --expect-probes 4 (contract-v2.md 7.6): an exit code cannot tell four probes from none,
# so a --probe typo or a manifest edit that selected nothing would run zero probes and
# exit 0 - the second half of the finding that added the flag. The count is the length of
# scripts/check_include_closure.py's PROBES list and changing one means changing the other.
#
# --compiler stays clang++-20, which is what the step above installs (Debian's clang-20
# package ships /usr/bin/clang++-20). It is deliberately NOT the bare `clang++` the local
# campaign gate spells: that spelling exists because the WSL box has no clang++-20, and
# copying it here would trade a version-pinned compiler for whatever the runner has.
run: python3 scripts/check_include_closure.py --mode both --compiler clang++-20 --self-test --require-all --expect-probes 4
benchmark: benchmark:
runs-on: ubuntu-latest runs-on: ubuntu-latest
Executable → Regular
+108 -40
View File
@@ -71,6 +71,14 @@
# claim is "byte-identical", and a comment that stopped describing what the code does is exactly # claim is "byte-identical", and a comment that stopped describing what the code does is exactly
# the kind of drift a "verbatim move" is supposed to be checked for. # the kind of drift a "verbatim move" is supposed to be checked for.
# #
# THE HASH'S EXACT EXTENT, so that the claim is not read wider than it is (review F-m3, inherited
# from the parent verbatim): it starts at the beginning of the LINE THAT CARRIES THE NAME and ends
# at the region's closing brace. A return type, an attribute or a template header sitting on an
# EARLIER line of a multi-line signature is therefore OUTSIDE the hash, and changing one of those
# alone does not move this gate. The end IS covered - the self-test's tail controls below prove
# the extent reaches the closing brace - and G1's symbol report is what catches a signature that
# changed shape.
#
# Exactly one definition must be found per name. Zero or two is exit 2 (could not run), never a # Exactly one definition must be found per name. Zero or two is exit 2 (could not run), never a
# silent pass: a rename this gate could not follow must not read as "nothing moved". Two is the # silent pass: a rename this gate could not follow must not read as "nothing moved". Two is the
# expected shape of a #if/#else pair that re-spells one of these bodies beside an untouched copy - # expected shape of a #if/#else pair that re-spells one of these bodies beside an untouched copy -
@@ -363,7 +371,17 @@ def extract(rows):
return out, problems return out, problems
def perturb(rows, target, src, dst): def perturb(rows, target, src, dst, where='head'):
"""Insert one line into a region's body, at its HEAD or at its TAIL.
TWO POSITIONS, AND THE SECOND ONE IS REVIEW FINDING F-m2. Every control used to insert at the
very first byte after the opening brace, so all four of them would still have tripped if
find_definition() returned an extent that stopped short of the closing brace - nothing in the
self-test proved that a region reaches its own end, and an extractor that hashed all but the
last statement of every body would have passed the whole self-test while being blind to a
change in that statement. The `tail` position inserts immediately BEFORE the closing brace,
which is the byte such an extractor would have dropped.
"""
for name, kind, source in rows: for name, kind, source in rows:
if name != target: if name != target:
continue continue
@@ -375,15 +393,22 @@ def perturb(rows, target, src, dst):
% (target, len(hits))) % (target, len(hits)))
return 2 return 2
begin, end = hits[0] begin, end = hits[0]
# The opening brace is located in the MASKED text and then used as an offset into the if where == 'tail':
# original: a brace inside a comment or a string on the signature line would otherwise send # end is one PAST the closing brace (find_function / find_namespace both return
# the perturbation somewhere that is not the body, and the control would be proving the # `match_forward(...) + 1`), so end - 1 is the brace itself and this lands inside the
# wrong thing. Offsets are identical between the two by construction (mask() preserves # body, one character before it ends.
# length). note = '\n // p4a_untouched_regions.sh --self-test: a body whose TAIL moved.\n'
brace = masked.index('{', begin) patched = text[:end - 1] + note + text[end - 1:]
patched = (text[:brace + 1] + else:
'\n // p4a_untouched_regions.sh --self-test: a body that MOVED.\n' + # The opening brace is located in the MASKED text and then used as an offset into the
text[brace + 1:]) # original: a brace inside a comment or a string on the signature line would otherwise
# send the perturbation somewhere that is not the body, and the control would be
# proving the wrong thing. Offsets are identical between the two by construction
# (mask() preserves length).
brace = masked.index('{', begin)
patched = (text[:brace + 1] +
'\n // p4a_untouched_regions.sh --self-test: a body that MOVED.\n' +
text[brace + 1:])
open(dst, 'w', encoding='utf-8', newline='').write(patched) open(dst, 'w', encoding='utf-8', newline='').write(patched)
return 0 return 0
sys.stderr.write('[p4a-untouched] %s is not one of the regions\n' % target) sys.stderr.write('[p4a-untouched] %s is not one of the regions\n' % target)
@@ -406,7 +431,7 @@ def main(argv):
sys.stdout.write('%s %s\n' % (sha, name)) sys.stdout.write('%s %s\n' % (sha, name))
return 2 if problems else 0 return 2 if problems else 0
if mode == 'perturb': if mode == 'perturb':
return perturb(rows, argv[3], argv[4], argv[5]) return perturb(rows, argv[3], argv[4], argv[5], argv[6] if len(argv) > 6 else 'head')
sys.stderr.write('[p4a-untouched] unknown mode %r\n' % mode) sys.stderr.write('[p4a-untouched] unknown mode %r\n' % mode)
return 2 return 2
@@ -487,6 +512,31 @@ extract_baseline() {
fi fi
printf '%s %s\n' "$pinned" "$name" >> "$WORK_DIR/$out.sha" printf '%s %s\n' "$pinned" "$name" >> "$WORK_DIR/$out.sha"
done done
# ...and put the list back into the FIXED ORDER (review F-m1). The pinned rows were stripped out
# of the spec above and appended here, so without this the baseline side emits them LAST while
# extract_ref emits everything in REGIONS order. The gate itself never noticed - compare_lists
# looks rows up by name - but the documented capture workflow did: the header promises "stdout is
# always the sha list ... in the fixed order above - so a baseline capture is a plain redirect",
# and a baseline captured that way then diffed against a two-ref stdout showed seven spurious
# differences purely from row order.
reorder_sha_list "$WORK_DIR/$out.sha" || return 2
return 0
}
# Rewrite a `<sha> <region>` list in REGIONS order, in place. Rows whose name is not in REGIONS
# would be a bug in the caller rather than a difference, so they are kept at the end where they are
# visible instead of being dropped.
reorder_sha_list() {
local file=$1 name
: > "$file.ordered" || return 2
printf '%s\n' "$REGIONS" | awk -F@ '{ print $1 }' > "$WORK_DIR/reorder.names" || return 2
while read -r name; do
[ -n "$name" ] || continue
awk -v n="$name" '$2 == n { print }' "$file" >> "$file.ordered" || return 2
done < "$WORK_DIR/reorder.names"
awk 'NR == FNR { known[$0] = 1; next } !($2 in known) { print }' \
"$WORK_DIR/reorder.names" "$file" >> "$file.ordered" || return 2
mv -f "$file.ordered" "$file" || return 2
return 0 return 0
} }
@@ -524,7 +574,9 @@ compare_lists() {
# A gate that always says "identical" and a gate that is working produce the same green, so the # A gate that always says "identical" and a gate that is working produce the same green, so the
# comparison has to be shown failing. Both controls run: the POSITIVE ones (an untouched copy # comparison has to be shown failing. Both controls run: the POSITIVE ones (an untouched copy
# compares equal; an edit OUTSIDE the regions is invisible) rule out a comparison that reports # compares equal; an edit OUTSIDE the regions is invisible) rule out a comparison that reports
# every region as moved, and the four NEGATIVE ones rule out the comparison that never reports any. # every region as moved, and the eight NEGATIVE ones - D-N's four regions, each perturbed at the
# HEAD of its body and again at its TAIL - rule out both the comparison that never reports any and
# the extraction whose extent stops before the closing brace (F-m2).
if [ "${1:-}" = "--self-test" ]; then if [ "${1:-}" = "--self-test" ]; then
[ $# -eq 1 ] || { say "--self-test takes no other arguments"; exit 2; } [ $# -eq 1 ] || { say "--self-test takes no other arguments"; exit 2; }
mkdir -p "$WORK_DIR/pristine" || exit 2 mkdir -p "$WORK_DIR/pristine" || exit 2
@@ -575,39 +627,55 @@ if [ "${1:-}" = "--self-test" ]; then
fi fi
say "positive control: an edit outside the seventeen regions is invisible, in all three files" say "positive control: an edit outside the seventeen regions is invisible, in all three files"
# One negative control per SELF_TEST_FUNCTIONS entry. Each is run on its own, from the pristine # TWO negative controls per SELF_TEST_FUNCTIONS entry - one at the HEAD of the body and one at
# copy, so the message it produces has to NAME that region - a control that only proved "some # its TAIL. Each is run on its own, from the pristine copy, so the message it produces has to
# region moved" would not distinguish "this row is compared" from "this row is extracted as an # NAME that region: a control that only proved "some region moved" would not distinguish "this
# empty range and every comparison of it is vacuous". # row is compared" from "this row is extracted as an empty range and every comparison of it is
# vacuous".
#
# THE TAIL HALF IS REVIEW FINDING F-m2. With head-only controls, an extraction that returned an
# extent stopping short of the closing brace would still have tripped all four - the inserted
# line is at the very first byte of the body - so nothing here proved that a region reaches its
# own end, and a change to the LAST statement of a protected body would have been invisible to a
# gate whose self-test was fully green. The tail control inserts immediately before the closing
# brace, which is exactly the byte such an extractor would have dropped.
controls=0 controls=0
for target in $SELF_TEST_FUNCTIONS; do for target in $SELF_TEST_FUNCTIONS; do
targetSource=$(printf '%s\n' "$REGIONS" | awk -F@ -v n="$target" '$1 == n { print $3 }') targetSource=$(printf '%s\n' "$REGIONS" | awk -F@ -v n="$target" '$1 == n { print $3 }')
[ -n "$targetSource" ] || { say "$target is not one of the regions"; exit 2; } [ -n "$targetSource" ] || { say "$target is not one of the regions"; exit 2; }
rm -rf "$WORK_DIR/perturbed" for position in head tail; do
cp -r "$WORK_DIR/pristine" "$WORK_DIR/perturbed" || exit 2 rm -rf "$WORK_DIR/perturbed"
write_spec "$WORK_DIR/perturbed" "$WORK_DIR/perturbed.spec" cp -r "$WORK_DIR/pristine" "$WORK_DIR/perturbed" || exit 2
python3 "$PY" perturb "$WORK_DIR/perturbed.spec" "$target" \ write_spec "$WORK_DIR/perturbed" "$WORK_DIR/perturbed.spec"
"$WORK_DIR/pristine/$(blob_name "$targetSource")" \ python3 "$PY" perturb "$WORK_DIR/perturbed.spec" "$target" \
"$WORK_DIR/perturbed/$(blob_name "$targetSource")" || exit 2 "$WORK_DIR/pristine/$(blob_name "$targetSource")" \
python3 "$PY" extract "$WORK_DIR/perturbed.spec" > "$WORK_DIR/perturbed.sha" || exit 2 "$WORK_DIR/perturbed/$(blob_name "$targetSource")" "$position" || exit 2
if compare_lists "$WORK_DIR/pristine.sha" "$WORK_DIR/perturbed.sha" "pristine" "perturbed" \ python3 "$PY" extract "$WORK_DIR/perturbed.spec" > "$WORK_DIR/perturbed.sha" || exit 2
2> "$WORK_DIR/perturbed.err"; then if compare_lists "$WORK_DIR/pristine.sha" "$WORK_DIR/perturbed.sha" "pristine" "perturbed" \
say "NEGATIVE CONTROL DID NOT TRIP: $target's body was changed and the comparison still" 2> "$WORK_DIR/perturbed.err"; then
say "reported every region as identical. This gate cannot go red for the reason it exists, so" say "NEGATIVE CONTROL DID NOT TRIP: $target's body was changed at its $position and the"
say "every green it has ever printed means nothing." say "comparison still reported every region as identical. This gate cannot go red for the"
exit 2 say "reason it exists, so every green it has ever printed means nothing."
fi if [ "$position" = tail ]; then
if ! grep -q "FIRST REGION THAT MOVED: $target" "$WORK_DIR/perturbed.err"; then say " A TAIL control that does not trip while the head one does means the extracted"
say "NEGATIVE CONTROL TRIPPED FOR THE WRONG REASON: the comparison went red but did not name" say " extent stops before the closing brace: the last statement of every protected body"
say "$target as the first region that moved. It said:" say " is outside the hash and can be rewritten silently."
sed 's/^/[p4a-untouched] /' "$WORK_DIR/perturbed.err" >&2 fi
exit 2 exit 2
fi fi
controls=$((controls + 1)) if ! grep -q "FIRST REGION THAT MOVED: $target" "$WORK_DIR/perturbed.err"; then
say "negative control $controls: a perturbed $target body is reported, and named" say "NEGATIVE CONTROL TRIPPED FOR THE WRONG REASON: the comparison went red but did not name"
say "$target as the first region that moved ($position control). It said:"
sed 's/^/[p4a-untouched] /' "$WORK_DIR/perturbed.err" >&2
exit 2
fi
controls=$((controls + 1))
say "negative control $controls: a perturbed $target body ($position) is reported, and named"
done
done done
if [ "$controls" -ne 4 ]; then if [ "$controls" -ne 8 ]; then
say "expected FOUR negative controls (BRIEF-P4A.md D-N), ran $controls" say "expected EIGHT negative controls (BRIEF-P4A.md D-N's four regions, each at its head and at"
say "its tail), ran $controls"
exit 2 exit 2
fi fi
say "self-test passed: $controls negative controls, all tripped and all named" say "self-test passed: $controls negative controls, all tripped and all named"