From 35fd6edcd5769a45a3071d5da6e75117631ede0b Mon Sep 17 00:00:00 2001 From: Henson Choi Date: Fri, 29 May 2026 17:51:37 +0900 Subject: [PATCH 22/26] Document the get_reduced_frame_status cascade invariant per Jian He's review The RF_* classifier is an early-return cascade whose branches are not mutually exclusive, so reordering them changes the result. This is the standard cascade idiom -- each branch is a minimal test premised on the negations the preceding returns have established -- not a logic flaw, but the structure left the contract implicit. update_reduced_frame() records the match as exactly one of three (rpr_match_matched, rpr_match_length) shapes: (false, 1), (true, 0), or (true, >= 1). Spell that out in the header, add the missing RF_EMPTY_MATCH return value, and annotate each branch with a "by here" note stating the running invariant -- notably why the empty match must be classified before the range test. No behavior change. --- src/backend/executor/nodeWindowAgg.c | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) diff --git a/src/backend/executor/nodeWindowAgg.c b/src/backend/executor/nodeWindowAgg.c index 99858d22dad..4cf1a9ac67b 100644 --- a/src/backend/executor/nodeWindowAgg.c +++ b/src/backend/executor/nodeWindowAgg.c @@ -4306,6 +4306,16 @@ clear_reduced_frame(WindowAggState *winstate) * RF_FRAME_HEAD pos is the start of the current match * RF_SKIPPED pos is inside the current match but not the start * RF_UNMATCHED pos is processed but not part of any match + * RF_EMPTY_MATCH pos is the start of an empty (zero-length) match + * + * update_reduced_frame() records the current match as exactly one of three + * (rpr_match_matched, rpr_match_length) shapes: (false, 1) for unmatched, + * (true, 0) for an empty match, and (true, >= 1) for a real match. The + * tests below form a cascade with early returns: each is a minimal check + * that relies on the negations the preceding returns have already + * established, so their order is significant. The "by here" notes spell + * out the running invariant; reordering a test would misclassify one of + * the three shapes. */ static int get_reduced_frame_status(WindowAggState *winstate, int64 pos) @@ -4316,17 +4326,31 @@ get_reduced_frame_status(WindowAggState *winstate, int64 pos) if (!winstate->rpr_match_valid) return RF_NOT_DETERMINED; - /* Empty match: covers only the start position */ + /* + * By here the record is valid and holds one of the three shapes above. + * + * The empty match (true, 0) must be classified first: it has length 0, so + * the range test below would compute start + length == start and reject + * its own start position as out of range. + */ if (pos == start && winstate->rpr_match_matched && length == 0) return RF_EMPTY_MATCH; - /* Outside the result range */ + /* + * By here length >= 1 -- the only zero-length record, the empty match, + * has been handled -- so [start, start + length) is a well-formed range. + */ if (pos < start || pos >= start + length) return RF_NOT_DETERMINED; + /* + * By here pos lies within [start, start + length). An unmatched record + * is (false, 1), so this returns for its single in-range position. + */ if (!winstate->rpr_match_matched) return RF_UNMATCHED; + /* By here the match is real (true, >= 1) and pos is one of its rows. */ if (pos == start) return RF_FRAME_HEAD; -- 2.50.1 (Apple Git-155)