Skip to content

Commit d9f380d

Browse files
CopilotCopilot
authored
POSIX bracket soundness: opaque punct/cntrl/print/graph; non-recursive gate; adversarial tests
1 parent c1103b9 commit d9f380d

8 files changed

Lines changed: 523 additions & 51 deletions

File tree

‎cpp/ql/lib/change-notes/2026-07-17-cpp-regex-posix-brackets.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
---
22
category: minorAnalysis
33
---
4-
* The C++ regular-expression parser (`semmle.code.cpp.regex.RegexTreeView`) now recognises POSIX bracket sub-expressions inside character classes as single character-matching atoms: POSIX character classes (`[[:alpha:]]`, `[[:digit:]]`, `[[:space:]]`, ...), collating symbols (`[[.a.]]`), and equivalence classes (`[[=a=]]`). These are ECMAScript-mode extensions accepted by `std::regex` but not part of ECMA-262 JavaScript, so they were previously mis-tokenized (the class was incorrectly closed at the inner `]`). POSIX character classes with a clean Perl-escape equivalent are mapped onto `\d`/`\s`/`\w`; other POSIX classes are conservatively over-approximated as `\w` for the shared engine's escape-class reasoning.
4+
* The C++ regular-expression parser (`semmle.code.cpp.regex.RegexTreeView`) now recognises POSIX bracket sub-expressions inside character classes as single character-matching atoms: POSIX character classes (`[[:alpha:]]`, `[[:digit:]]`, `[[:space:]]`, ...), collating symbols (`[[.a.]]`), and equivalence classes (`[[=a=]]`). These are ECMAScript-mode extensions accepted by `std::regex` but not part of ECMA-262 JavaScript, so they were previously mis-tokenized (the class was incorrectly closed at the inner `]`). POSIX character classes whose match set is `\d`, `\s`, or `\w` — or a subset of one (`digit`, `xdigit`, `space`, `blank`, `word`, `alpha`, `alnum`, `upper`, `lower`) — are mapped onto `\d`/`\s`/`\w` for the shared engine's escape-class reasoning. The remaining POSIX classes (`punct`, `cntrl`, `print`, `graph`) as well as collating and equivalence classes are left opaque: they still parse as single character-consuming class-member atoms, but the shared engine treats their character set as unknown rather than unsoundly equating it with `\w`.
55
* Documented that `std::regex_constants::multiline` is detected by `RegexFlowConfigs.qll` but not currently modeled in the parse tree — `^` and `$` are always treated as string-start/string-end anchors, matching the conservative choice made by other language ReDoS analyses. Precise multiline modeling would require extending the shared `RegexTreeViewSig` signature and is left as future work.

‎cpp/ql/lib/semmle/code/cpp/regex/RegexTreeView.qll‎

Lines changed: 31 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -664,14 +664,23 @@ module Impl implements RegexTreeViewSig {
664664
* Each is treated as a single character-matching atom (a class member).
665665
*
666666
* For POSIX character classes with a clean Perl-escape equivalent
667-
* (`digit`, `space`, `word`) we map them onto `\d`, `\s`, `\w` via
668-
* `isEscapeClass`, so the shared ReDoS engine can reason about their
669-
* match sets precisely. Other POSIX classes (`alpha`, `alnum`, `upper`,
670-
* `lower`, `punct`, `cntrl`, `print`, `graph`, `xdigit`, `blank`) do not
671-
* map cleanly; they are conservatively over-approximated as `\w` for the
672-
* purpose of `isEscapeClass` — this may lead to minor imprecision when
673-
* two atoms are combined but preserves the "single-atom" treatment
674-
* required by the shared engine.
667+
* (`digit`, `space`, `word`) — or a *subset* of one (`alpha`, `alnum`,
668+
* `upper`, `lower`, `xdigit`, `blank`) — we map them onto `\d`, `\s`, `\w`
669+
* via `isEscapeClass`, so the shared ReDoS engine can reason about their
670+
* match sets.
671+
*
672+
* Other POSIX classes (`punct`, `cntrl`, `print`, `graph`) as well as
673+
* collating and equivalence classes do NOT fit any of `\d`/`\s`/`\w`:
674+
* - `[:punct:]` matches punctuation, disjoint from `\w`.
675+
* - `[:cntrl:]` matches control characters, disjoint from `\w`.
676+
* - `[:print:]` / `[:graph:]` include punctuation (and, for `print`,
677+
* space), overlapping but not contained in `\w`.
678+
* Mapping them onto `\w` would tell the shared engine that two such atoms
679+
* "overlap" via `\w`, which is unsound (produces both false positives and
680+
* false negatives in ambiguity reasoning). We therefore leave them opaque:
681+
* they are single character-consuming class members, but `isEscapeClass`
682+
* does not hold for them and the shared engine treats them as an unknown
683+
* character set (the same treatment as collating/equivalence classes).
675684
*
676685
* Collating and equivalence classes semantically may match multi-character
677686
* sequences (e.g. `[[.ll.]]`); we model them as single atoms, which is a
@@ -983,27 +992,29 @@ module Impl implements RegexTreeViewSig {
983992
exists(RegExpCharacterClassEscape escape | term = escape | escape.getValue() = clazz)
984993
or
985994
// Map POSIX bracket sub-expressions to the shared engine's escape-class
986-
// signature. Only POSIX character classes (`[:name:]`) are mapped;
987-
// collating and equivalence classes have no meaningful escape-class
988-
// equivalent and are left opaque.
995+
// signature. Only POSIX character classes (`[:name:]`) whose match set
996+
// is `\d`, `\s`, or `\w` — or a subset of one — are mapped; other
997+
// POSIX classes (`punct`, `cntrl`, `print`, `graph`) and the
998+
// collating/equivalence forms have no meaningful escape-class equivalent
999+
// and are left opaque (they still parse as single character-class atoms,
1000+
// but the shared engine treats their character set as unknown).
9891001
exists(RegExpPosixBracket posix, string name |
9901002
term = posix and
9911003
posix.getKind() = "class" and
9921004
name = posix.getName()
9931005
|
994-
// Clean equivalences.
1006+
// `[:digit:]` = `\d`; `[:xdigit:]` is a superset, treated as `\d`
1007+
// (under-approximation — sound for the shared engine's overlap
1008+
// reasoning, since it will only ever detect fewer intersections, not
1009+
// invent them).
9951010
name = ["digit", "xdigit"] and clazz = "d"
9961011
or
1012+
// `[:space:]` = `\s`; `[:blank:]` is a subset (space + tab).
9971013
name = ["space", "blank"] and clazz = "s"
9981014
or
999-
// Conservative over-approximation: alphabetic / alphanumeric / case
1000-
// classes are subsets of `\w`, so `\w` is a safe over-approximation
1001-
// for pumping-witness discovery in the shared engine. `punct`,
1002-
// `cntrl`, `print` and `graph` do not fit `\w` precisely; we map
1003-
// them here to give the engine SOME atom to reason about, at the
1004-
// cost of over-approximating their character set.
1005-
name = ["word", "alpha", "alnum", "upper", "lower", "punct", "cntrl", "print", "graph"] and
1006-
clazz = "w"
1015+
// `[:word:]` = `\w`; `[:alpha:]`, `[:alnum:]`, `[:upper:]`, `[:lower:]`
1016+
// are all subsets of `\w`.
1017+
name = ["word", "alpha", "alnum", "upper", "lower"] and clazz = "w"
10071018
)
10081019
}
10091020

‎cpp/ql/lib/semmle/code/cpp/regex/internal/ParseRegExp.qll‎

Lines changed: 58 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,52 @@ class RegExp extends StringLiteral {
5757
// Character sets (character classes [ ... ] )
5858
// ---------------------------------------------------------------------------
5959

60+
/**
61+
* Holds if `[start, end)` looks lexically like a POSIX bracket
62+
* sub-expression: an unescaped `[` at `start` followed by a mark
63+
* (`:`, `.`, or `=`) and terminated by the earliest matching `mark]`.
64+
*
65+
* This is a purely lexical recognition — it does NOT check whether the
66+
* span is actually nested inside an outer `[...]` character class. The
67+
* nesting requirement is applied on top of this in `posixBracketExpression`.
68+
*
69+
* Separating the lexical recognition from the nesting gate keeps the
70+
* predicate definitions cleanly stratified (no self-recursion under
71+
* negation).
72+
*/
73+
private predicate posixBracketCandidate(int start, int end, string kind) {
74+
exists(string mark |
75+
this.getChar(start) = "[" and
76+
not this.escapingChar(start) and
77+
(
78+
this.getChar(start + 1) = ":" and kind = "class" and mark = ":"
79+
or
80+
this.getChar(start + 1) = "." and kind = "collating" and mark = "."
81+
or
82+
this.getChar(start + 1) = "=" and kind = "equivalence" and mark = "="
83+
)
84+
|
85+
end - 2 =
86+
min(int i |
87+
i > start + 1 and this.getChar(i) = mark and this.getChar(i + 1) = "]"
88+
)
89+
)
90+
}
91+
92+
/**
93+
* Holds if `pos` is an unescaped `[` or `]` that acts as a genuine
94+
* character-class delimiter — i.e. it is NOT part of any POSIX bracket
95+
* candidate (neither the opening `[`, the closing `]`, nor any interior
96+
* character of one).
97+
*
98+
* Used to decide, purely lexically, whether a POSIX bracket candidate is
99+
* nested inside an outer, still-open `[...]` character class.
100+
*/
101+
private predicate structuralBracket(int pos) {
102+
(this.nonEscapedCharAt(pos) = "[" or this.nonEscapedCharAt(pos) = "]") and
103+
not exists(int s, int e | this.posixBracketCandidate(s, e, _) and s <= pos and pos < e)
104+
}
105+
60106
/**
61107
* Holds if `[start, end)` is a POSIX bracket sub-expression of the given
62108
* `kind`, appearing nested inside another `[...]` character class.
@@ -74,44 +120,26 @@ class RegExp extends StringLiteral {
74120
* A POSIX bracket sub-expression is only recognized when it is nested
75121
* inside another `[...]` character class, since the standard only gives
76122
* these forms meaning in that context.
123+
*
124+
* Implementation note: the "inside an outer, still-open [...]" gate is
125+
* expressed as an ordinary universal quantification over `structuralBracket`
126+
* positions (which only depend on the purely-lexical
127+
* `posixBracketCandidate` predicate). There is no self-recursion under
128+
* negation, so this predicate is trivially stratified.
77129
*/
78130
predicate posixBracketExpression(int start, int end, string kind) {
79-
exists(string mark |
80-
this.getChar(start) = "[" and
81-
(
82-
this.getChar(start + 1) = ":" and kind = "class" and mark = ":"
83-
or
84-
this.getChar(start + 1) = "." and kind = "collating" and mark = "."
85-
or
86-
this.getChar(start + 1) = "=" and kind = "equivalence" and mark = "="
87-
)
88-
|
89-
end - 2 =
90-
min(int i |
91-
i > start + 1 and this.getChar(i) = mark and this.getChar(i + 1) = "]"
92-
)
93-
) and
94-
// Gate: the `[` at `start` must lie inside an outer `[...]` character
95-
// class that has not yet been closed. Concretely: there must exist an
96-
// earlier unescaped `[` at some `q < start` such that every unescaped
97-
// `]` between `q` and `start` is itself part of some POSIX bracket
98-
// sub-expression (i.e. it is the terminator of, or lies inside, another
99-
// `posixBracketExpression`). This is a monotone recursion (POSIX
100-
// recognitions only make the gate easier to satisfy) and correctly
101-
// handles both nested top-level cases (`[[:alpha:]]`, disallowed at top
102-
// level) and adjacent POSIX brackets (`[[:alpha:][:digit:]]`).
131+
this.posixBracketCandidate(start, end, kind) and
132+
// Gate: some structural `[` at position `q < start` must not have been
133+
// closed by any structural `]` at position `r` with `q < r < start`.
103134
exists(int q |
104135
q < start and
136+
this.structuralBracket(q) and
105137
this.nonEscapedCharAt(q) = "[" and
106138
not exists(int r |
107139
q < r and
108140
r < start and
109-
this.nonEscapedCharAt(r) = "]" and
110-
not exists(int s2, int e2 |
111-
this.posixBracketExpression(s2, e2, _) and
112-
s2 < r and
113-
r < e2
114-
)
141+
this.structuralBracket(r) and
142+
this.nonEscapedCharAt(r) = "]"
115143
)
116144
)
117145
}

‎cpp/ql/test/library-tests/regex/RegexFlow.expected‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,13 @@ usedAsRegex_
4949
| test.cpp:287:18:287:28 | [[.a.]].* |
5050
| test.cpp:289:18:289:28 | [[=a=]].* |
5151
| test.cpp:292:18:292:34 | ([[:alpha:]]+)+ |
52+
| test.cpp:311:19:311:31 | [:alpha:].* |
53+
| test.cpp:317:19:317:29 | a[:b:]c.* |
54+
| test.cpp:320:19:320:51 | [[:alpha:][:digit:][:space:]].* |
55+
| test.cpp:324:19:324:35 | []a[:alpha:]].* |
56+
| test.cpp:331:19:331:35 | [[:alpha:]-z].* |
57+
| test.cpp:337:19:337:31 | [[:alpha].* |
58+
| test.cpp:346:19:346:88 | ^([[:alpha:]]+[[:digit:]]*[[:space:]]?)+([[:punct:]]\|[[:xdigit:]])+$ |
5259
regexMatchedAgainst_
5360
| test.cpp:209:18:209:25 | (a+)+b | test.cpp:211:28:211:34 | subject |
5461
| test.cpp:209:18:209:25 | (a+)+b | test.cpp:212:29:212:35 | subject |
@@ -65,6 +72,13 @@ regexMatchedAgainst_
6572
| test.cpp:287:18:287:28 | [[.a.]].* | test.cpp:288:29:288:32 | subj |
6673
| test.cpp:289:18:289:28 | [[=a=]].* | test.cpp:290:29:290:32 | subj |
6774
| test.cpp:292:18:292:34 | ([[:alpha:]]+)+ | test.cpp:293:29:293:32 | subj |
75+
| test.cpp:311:19:311:31 | [:alpha:].* | test.cpp:312:29:312:32 | subj |
76+
| test.cpp:317:19:317:29 | a[:b:]c.* | test.cpp:318:29:318:32 | subj |
77+
| test.cpp:320:19:320:51 | [[:alpha:][:digit:][:space:]].* | test.cpp:321:29:321:32 | subj |
78+
| test.cpp:324:19:324:35 | []a[:alpha:]].* | test.cpp:325:29:325:32 | subj |
79+
| test.cpp:331:19:331:35 | [[:alpha:]-z].* | test.cpp:332:29:332:32 | subj |
80+
| test.cpp:337:19:337:31 | [[:alpha].* | test.cpp:338:29:338:32 | subj |
81+
| test.cpp:346:19:346:88 | ^([[:alpha:]]+[[:digit:]]*[[:space:]]?)+([[:punct:]]\|[[:xdigit:]])+$ | test.cpp:347:29:347:32 | subj |
6882
hasIgnoreCaseFlag_
6983
| test.cpp:218:18:218:23 | foo+ |
7084
| test.cpp:225:18:225:23 | bar+ |

0 commit comments

Comments
 (0)