On the complexity of modern regex matching

Modern regex features

$r ::= \varepsilon~|~c~|~r{\cdot}r~|~r{\shortmid}r~|~r*$

+ capture groups:: a(b*)c
+ backreferences:: ^(.+)\1+$
+ lookarounds:: Beg((?!End).)*End
= lots of ReDoS

How hard are modern regexes?

Regex dialect	Complexity class
Textbook regexes	$\in$ P
Modern-regex folklore	NP-complete (wrong!)
[Uezato 24]	PSPACE-complete
Real-world regex matching	This work!

Prior work

$\approxeq$

$\Leftrightarrow$

ECMAScript 2023 specification

Warblre mechanization [1],
Linden semantics [2]

[Uezato 24]: lookarounds + backrefs PSPACE-complete for custom, nonbacktracking semantics.

Problem:

Can we say something about matching and parsing complexity for a real, large specification?

Solution:

We showed, with Rocq proofs, that
JavaScript regex matching is PSPACE-complete.

Contributions: We give the first complexity results for a modern regex language, against a realistic semantics, with mechanized reductions and bounds on computation depth, using a new construction with no explicit negations.

NP- and PSPACE-hardness

Reduction from SAT [Dominus 98]: \[ \begin{align*} \varphi =~&({\color{blue}x_1} \lor {\color{green}x_2}) \land \neg {\color{green}x_2} \\ r =~&\langle (_1 \texttt{\color{blue}a})|\texttt{\color{blue}a} \rangle \texttt{;}\langle (_2 \texttt{\color{green}a})|\texttt{\color{green}a} \rangle \texttt{;} & \text{sets $x_1$ and $x_2$} \\ & \langle {\color{blue}\backslash{}1}|\backslash{}2 \rangle\texttt; & \text{checks $x_1 \lor x_2$} \\ & \backslash{}2\texttt{\color{green}a}\texttt; & \text{checks $\neg x_2$} \\ s =~&``\texttt{{\color{blue}a};{\color{green}a};{\color{blue}a};{\color{green}a};}" \end{align*} \]

Extension to QBF (adapted from [Uezato 24]): \[ \begin{align*} q =~&\exists {\color{blue}x_1}. \neg\exists {\color{green}x_2}. ({\color{blue}x_1} \lor {\color{green}x_2}) \land \neg {\color{green}x_2} \\ r =~&\langle (_1 \texttt{\color{blue}a})|\texttt{\color{blue}a} \rangle \texttt{;} \textbf{\color{red}(?!} \langle (_2 \texttt{\color{green}a})|\texttt{\color{green}a} \rangle \texttt{;} \langle \backslash{}1|\backslash{}2 \rangle\texttt; \backslash{}2\texttt{a}\texttt;\textbf{\color{red})} \\ s =~&``\texttt{\hspace{3.85mm}{\color{blue}a}\hspace{3.85mm};\hspace{10mm}{\color{green}a}\hspace{4.5mm};\hspace{4.5mm}a\hspace{4.4mm};\hspace{2mm}a\hspace{1.5mm};}" \end{align*} \]

Who needs negation?

Key idea: use atomic lookarounds.

Atomic lookarounds: if $A$ succeeds but $(?{=}A)C$ fails, then $(?{=}A|B)C$ will not backtrack to try $(?{=}B)C.$

Our new negation-free construction:

\[ \begin{align*} q =~&\exists {\color{blue}x_1}. \neg\exists {\color{green}x_2}. ({\color{blue}x_1} \lor {\color{green}x_2}) \land \neg {\color{green}x_2} \\ r =~&\langle (_1 \texttt{\color{blue}a})|\texttt{\color{blue}a} \rangle \texttt{;} \textbf{\color{red}(?{=}} \langle (_2 \texttt{\color{green}a})|\texttt{\color{green}a} \rangle \texttt{;} \\ &\langle \backslash 1 | \backslash 2 \rangle\texttt; \backslash 2 \texttt{a;} \\ &\mathbf{\color{red} | \langle \texttt{a;}\rangle{*}\textbf(_\mathit{z} \texttt{z}\textbf{))}} {\color{purple} \langle \texttt{a;}\rangle{*}\backslash k\langle z \rangle \$} \\ s =~&``\texttt{{\color{blue}a};{\color{green}a};a;a;z}" \end{align*} \]

PSPACE membership, without TMs!

New argument: bound the recursion depth
and the size of the arguments of the
recursive backtracking algorithm by
a polynomial of $|r|$ and $|s|$.

Rocq proofs: prove validity of reduction, bound computation depth

1. Model $\mathrm{QBF}_{\neg\exists}$

Definition qbf: Type :=
  list quantifier * formula.
Definition qbf_true
  (q: qbf): Prop :=
  (* ... *).

2. Encode reduction

Definition def_var_regex
  (v: variable): regex :=
  Sequence
    (Disjunction (Group v (Char a))
      (Char a)) (Char semicolon).
(* ... *)

3. Prove vs. Linden semantics

Theorem qbf_regex: forall q,
  accepts (regexOf q) (stringOf q) 
  <-> qbf_true q.

4. Bound computation depth

Theorem tree_depth_bound:
  forall r s t, is_tree r s t ->
    tree_depth t <= 2*(1 + (
      (1 + |s|ₛ) * |r|ᵣ +
      (1 + |s|ₛ) * |r|ᵣ^2)).

$\footnotesize\hspace{.75cm}= \mathcal{O}(|s| \cdot |r|^2)$

Extension: regex parsing without lookarounds is OptP-complete

OptP [Krentel 86]: functions computed as the maximum output over the accepting branches of an NP Turing machine.

New result: regex parsing without lookarounds is OptP-hard.

Proof: by reduction from a canonical OptP-complete problem.

Reduction from SAT
+ backtracking semantics
= reduction from LEXICOGRAPHIC SAT

New result: regex parsing without lookarounds is in OptP.

Proof: We bound the execution time of an NP algorithm that produces the branch history. It uses a checker that takes as input a bitstring of choices, returns it if it leads to a match and rejects otherwise.

Future work

Unexpanded complexity: $ r\{3\} \nrightarrow rrr $.
Connection with Turing machines.
Other regex languages and features.

References

[1]: N. De Santo, A. Barrière and C. Pit-Claudel, "A Coq Mechanization of JavaScript Regular Expression Semantics," ICFP'24.
[2]: A. Barrière, V. Deng and C. Pit-Claudel, "Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics and Its Applications," POPL'26.
[Uezato 24]: Y. Uezato, "Regular Expressions with Backreferences and Lookaheads Capture NLOG," ICALP'24.
[Dominus 98]: M. J. Dominus, "Perl Regular Expression Matching is NP-Complete," 1998.
[Krentel 86]: M. W. Krentel, "The complexity of optimization problems," STOC'86.

Regex dialect	Complexity class
Textbook regexes	\(\in\) P
Modern-regex folklore	NP-complete (wrong!)
[Uezato 24]	PSPACE-complete
Real-world regex matching	This work!