Repairing Regular Expressions for Extraction
NARIYOSHI CHIDA, NTT Social Informatics Laboratories / Waseda University, JapanTACHIO TERAUCHI, Waseda University, Japan
While synthesizing and repairing regular expressions (regexes) based on Programming-by-Examples (PBE)
methods have seen rapid progress in recent years, all existing works only support synthesizing or repairing
regexes for membership testing, and the support for extraction is still an open problem. This paper fills thevoid by proposing the first PBE-based method for synthesizing and repairing regexes for extraction.
Our work supports regexes that have real-world extensions such as backreferences and lookarounds. The
extensions significantly affect the PBE-based synthesis and repair problem. In fact, we show that there areunsolvable instances of the problem if the synthesized regexes are not allowed to use the extensions, i.e., there
is no regex without the extensions that correctly classify the given set of examples, whereas every problem
instance is solvable if the extensions are allowed. This is in stark contrast to the case for the membershipwhere every instance is guaranteed to have a solution expressible by a pure regex without the extensions.
The main contribution of the paper is an algorithm to solve the PBE-based synthesis and repair problem forextraction. Our algorithm builds on existing methods for synthesizing and repairing regexes for membership
testing, i.e., the enumerative search algorithms with SMT constraint solving. However, significant extensions
are needed because the SMT constraints in the previous works are based on a non-deterministic semantics
of regexes. Non-deterministic semantics is sound for membership but not for extraction, because which
substrings are extracted depends on the deterministic behavior of actual regex engines. To address the issue,
we propose a new SMT constraint generation method that respects the deterministic behavior of regex
engines. For this, we first define a novel formal semantics of an actual regex engine as a deterministic big-step
operational semantics, and use it as a basis to design the new SMT constraint generation method. The key idea
to simulate the determinism in the formal semantics and the constraints is to consider continuations of regex
matching and use them for disambiguation. We also propose two new search space pruning techniques called
approximation-by-pure-regex and approximation-by-backreferences that make use of the extraction informationin the examples. We have implemented the synthesis and repair algorithm in a tool called R3 (Repairing Regex
for extRaction) and evaluated it on 50 regexes that contain real-world extensions. Our evaluation shows theeffectiveness of the algorithm and that our new pruning techniques substantially prune the search space.
CCS Concepts: • Software and its engineering → Software notations and tools; • Theory of computation→ Regular languages; Operational semantics.
Additional Key Words and Phrases: Regular Expression, Programming by Example, Program Repair
ACM Reference Format:
Nariyoshi Chida and Tachio Terauchi. 2023. Repairing Regular Expressions for Extraction. Proc. ACM Program.
Lang. 7, PLDI, Article 173 (June 2023), 31 pages. https://doi.org/10.1145/3591287

1

INTRODUCTION

Regular expressions (regexes) play a critical role for membership testing and extraction in modern
programming languages and software development. For example, they are heavily used for validating user inputs [O’Hara 2022; OWASP 2022], inspecting packets [Services 2022; Snort 2022],
Authors’ addresses: Nariyoshi Chida, nariyoshichidamm@gmail.com, NTT Social Informatics Laboratories / Waseda
University, Japan; Tachio Terauchi, Waseda University, Japan, terauchi@waseda.jp.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee
provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice andthe full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses,
contact the owner/author(s).
© 2023 Copyright held by the owner/author(s).
2475-1421/2023/6-ART173
https://doi.org/10.1145/3591287

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173

173:2Nariyoshi Chida and Tachio Terauchi

and extracting data from (unstructured) texts [Li et al. 2008; Luckie et al. 2019] in the frameworks
for building Web applications [Angular 2022; Django 2022], etc. However, despite the practicalimportance of regexes, writing or repairing regexes is an error-prone task [Michael et al. 2019;
Wang et al. 2020].
Recent works have addressed this problem by synthesizing or repairing regexes based on
Programming-by-Examples (PBE) methods which have received much attention in recent years [Chenet al. 2020; Chida and Terauchi 2022b; Ferreira et al. 2021; Lee et al. 2016; Li et al. 2021, 2020; Panet al. 2019; Zhang et al. 2020]. The PBE-based methods allow the users to write or repair regexes
automatically from examples that reflect the user’s intention. Yet, while methods for synthesizingor repairing regexes for membership testing exist, none of them can handle extraction. Additionally,
there are several works for generating a regex for extraction from examples [Bartoli et al. 2014,2016] based on genetic algorithms. However, they do not guarantee the correctness of the repair,that is, the synthesized regex is not guaranteed to conform to the given set of examples.
This paper fills the void by proposing the first PBE-based method for synthesizing and repairing
regexes for extraction. We first formally define a PBE-based repair problem called the extractionregex-repair problem.1 The problem takes a (possibly incorrect) regex, a set of positive examples,and a set of negative examples. Like in previous PBE works for membership, a negative example isa string to be rejected. However, unlike the previous works, a positive example consists of not only
a string to be accepted, but also the information of substrings to be extracted from the string. The
goal of the repair problem is to find a regex that is consistent with the given set of examples and issyntactically close to the given original one. Like in the previous PBE works, the syntactic closenessis used to bias the synthesis to one that is close to the user’s intention [Chida and Terauchi 2022b;
Pan et al. 2019], that is, the original regex may not be correct but is assumed to be close to the onethat the user intended. Our work handles regexes with real-world extensions such as backreferences
and lookarounds [Friedl 2006]. The extensions significantly affect the repair problem. In fact, weshow that there are unsolvable problem instances if repaired regexes are not allowed to use theextensions, i.e., there is no regex without the extensions that correctly classify the given set ofexamples, whereas every problem instance is solvable if the extensions are allowed. This is in stark
contrast to the case for the membership repair problem in which every instance is guaranteed tohave a solution expressible by a pure regex without the extensions.
At a high level, our algorithm for solving the extraction-regex-repair problem builds on theapproach used in the previous works on PBE-based repair methods for membership which conducts
enumerative search by repeatedly generating and solving SMT constraints that encode assertionsof the form “the given template regex can be instantiated to one that conforms with the given set ofexamples”, coupled with certain pruning techniques to reduce the search space. A template regex isa regex that contains holes to be filled. However, there are following key challenges that did notexist in the previous works that only considered membership.
The first challenge comes from the fact that regex engines in the real world run in a deterministicmanner by prioritizing the behavior of operators that potentially have an ambiguity such as theunion operator and the Kleene-star operator. The previous works that only considered membershipdo not face this challenge because the determinism of regex engines does not affect the matching
results in terms of membership testing.2 However, in the case of extraction, it does affect theresult because which substrings are extracted depends on the deterministic behavior of the regex
engine. To address the issue, we propose a new SMT constraint generation method that respects
1 Synthesis is a special case of the repair problem in which the pre-repair regex is 𝜖.
2 Technically, the membership result can be affected in some rare cases when substrings captured in positive lookarounds

are backreferenced [Chida and Terauchi 2022b; Loring et al. 2019], but the issue is not addressed in the previous PBE works.

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:3

the deterministic behavior of regex engines. For this, we first define a novel formal semantics ofan actual regex engine as a deterministic big-step operational semantics, and use it as a basis todesign the new SMT constraint generation method. The key idea to simulate the determinism in
the formal semantics and the constraints is to consider continuations of regex matching and use
them for disambiguation. There are several variants of determinism in actual regex engines that
often give different extraction results (even though many are equivalent for just membership), andin this work, we choose that of the ECMAScript 2023 language specification, that is, our semantics
and constraints emulate the behavior of the regex engines of JavaScript. However, the high-levelidea of our approach is applicable to other regex engines.
The second challenge is the large search space. The previous PBE-based methods for membership
reduced the search space by pruning useless templates based on over- and under-approximations [Chenet al. 2020; Chida and Terauchi 2022b; Lee et al. 2016; Pan et al. 2019]. That is, by creating from thetemplate regexes that over- or under-approximate the strings accepted by possible instantiations of
the template, one can cheaply detect when a template is impossible to be instantiated to a regex
that correctly classifies the examples. Although we can use the same approximations in our method
for extraction, it is not enough to reduce the search space as we shall show in our evaluation. The
increase in the search space is inevitable since, in the case of extraction, not only do we need tofind a regex that correctly classifies the examples in terms of membership only (i.e., only whether
the example string is accepted or rejected), but we also need to find places in the regex to insert
capturing groups to correctly reflect the extraction information in the examples. To address thischallenge, we propose two new over-approximation techniques called approximation-by-pure-regex
and approximation-by-backreferences. The key idea in these techniques is to modify the example
string by embedding the extraction information in it so that its membership result against a certain regex created from the template can be used to detect whether or not the template can beinstantiated to become a regex that correctly reflects the extraction information in the example.
We have implemented our algorithm as a tool called R3 (Repairing Regex for extRaction) andevaluated it on 50 regexes including ones that contain real-world extensions. To evaluate the impactof our new pruning, we compare R3 to the baseline: R3base , which does not use our new pruning
techniques. Our evaluation shows that R3 can repair regexes efficiently in a real-world situation
using few examples, and our new pruning technique substantially improves the performance.
In summary, our paper makes the following contributions.
• We give a novel deterministic formal semantics of regexes that is consistent with an actual regex engine for both membership and extraction (Section 3). Our semantics follows
the ECMAScript 2023 language specification and supports real-world extensions such as
backreferences and lookarounds.
• We define the extraction-regex-repair problem, which is the first PBE problem of repairing aregex for extraction task (Section 4). We show that real-world extensions such as lookarounds
are essential to ensure the existence of the solutions of the problem, in that there exist
instances of the problem for which there exist no solutions without the use of extensions
while every instance is solvable when the extensions are allowed.
• We give an algorithm for solving the extraction-regex-repair problem (Section 5). Our algorithm is based on an enumerative search and uses an SMT solver to find a solution. We build
on our novel formal semantics to design the new SMT constraint generation method that
respects the deterministic behavior of the regex engine (Section 5.2). Additionally, we propose
new pruning techniques to reduce the search space (Section 5.3). We emphasize that the SMT
constraint generation method and the pruning techniques are significantly different fromthose of prior works that only considered membership due to extraction-specific challenges
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:4

Nariyoshi Chida and Tachio Terauchi

such as deterministic semantics of regex engines and utilizing the extraction information in
examples. Such challenges are not addressed in any state-of-the-art regex synthesizers andrepairers for membership. Our work addresses the new challenges by novel ideas such as theuse of continuation regexes in SMT constraints and using backreferences in pruning.
• We evaluate our method on 50 regexes including ones that contain real-world extensions(Section 6). We show that R3 can find a solution efficiently, and our new pruning techniques
improve the performance substantially.
2

OVERVIEW

We overview the extraction-regex-repair problem and our PBE method that solves the problem
with an example. The example is inspired by regexes from Stack Overflow3 and Blog posts4 .
Motivating Example. The user wants to extract a text of a leaf element from an XML document
using a regex. If an XML document has two or more leaf elements, the user wants to extract theleftmost one. For example, the user wants to extract the text 𝑏 from the XML document <𝑎>𝑏</𝑎>, 𝑐from <𝑎><𝑏>𝑐</𝑏></𝑎>, and 𝑑 from <𝑎><𝑏>𝑑</𝑏><𝑐>𝑒</𝑐></𝑎>. For this purpose, the user prepared
the regex .∗? (?<=<(.∗ )1 >) (.∗? )2 (?=<[/]\1>).∗ . The regex uses the positive lookbehind (?<=<(.∗ )1 >)and the positive lookahead (?=<[/]\1>) to find the opening and closing tags, respectively, andextracts the text of the tags by the 2nd capturing group (.∗? )2 . Note that the positive lookbehindcontains the capturing group (.∗ )1 which is backreferenced in the positive lookahead by the operator\1 to ensure that the opening and closing tag names match. Unfortunately, the regex does notextract texts correctly due to the deterministic behavior of actual regex engines. For example, for
the input <𝑎><𝑏>𝑐</𝑏></𝑎>, the regex extracts <𝑏>𝑐</𝑏> rather than 𝑐.
Repair Problem. Our tool R3 can help the user to repair the regex automatically by solving theextraction-regex-repair problem. The instance of the repair problem is a (possibly incorrect) regex,
a set of positive examples, and a set of negative examples. A solution of the instance is a correct
regex, i.e., a regex that is consistent with all examples, and is syntactically close to the given regex.
A positive example is a string to be accepted with the information of substrings to be extracted.
We use L and M𝑖 to denote the information of a substring to be extracted by the 𝑖th capturinggroup. For example, the positive example 𝑎L𝑎M1𝑎 means that the regex should accept the string
𝑎𝑎𝑎 and extract the second character 𝑎. Note that a positive example specifies not only substrings
to be extracted but also the positions of the substrings, reflecting the behavior of the extraction
operations in actual regex engines. A negative example is a string to be rejected. Here, supposethat the user prepared the positive examples <𝑎><L𝑎M1 >L𝑎M2 </𝑎></𝑎> and <L𝑏M1 >L𝑐M2 </𝑏>, and thenegative example <𝑎>𝑎</𝑏>. Note that, in a PBE scenario, the number of examples should be small
for usability. A possible way for a user to prepare such examples is to first prepare membershipexamples (i.e., by only considering which strings should be accepted or rejected), following themethods recommended in prior PBE works for membership such as consulting the RegExLib
website [RegExLib 2022], and then add to the positive examples information about the positions of
the substrings to be extracted.
Repair Method. Once the user inputs the examples with the (possibly incorrect) regex, R3 generates
a candidate template of a solution (Template Generation), and then checks whether the candidate
template can be instantiated into the solution (Searching Template Instances). R3 iteratively performs
these steps until it finds a solution.
(Template Generation) R3 generates templates, which are regexes containing holes. Roughly, ahole □ is a placeholder that is to be replaced with some concrete regex. For the running example, R33 https://stackoverflow.com/questions/68248512/regex-lookahead-lookbehind
4 http://blog.gtiwari333.com/2011/12/htmlxml-tag-parsing-using-regex-in-java.html

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:5

starts with the initial template set to be the input regex .∗? (?<=<(.∗ )1 >) (.∗? )2 (?=<[/]\1>).∗ . Since
the regex does not correctly classify the examples (namely, <𝑎><L𝑎M1 >L𝑎M2 </𝑎></𝑎>),5 R3 replaces
some subexpressions with holes and expands the holes by replacing them with templates that may
contain holes. After some iterations, R3 finds the template .∗? (?<=<(□∗ )1 >)(□∗? )2 (?=<[/]\1>).∗ .
(Searching Template Instances) Then, R3 checks whether the template can be instantiated to aregex that correctly classifies the examples by replacing its holes with sets of characters. For this,R3 generates and solves an SMT constraint. The constraint generation builds on that proposed formembership [Chida and Terauchi 2022b; Pan et al. 2019]. That is, for each example, we generate
a formula over variables representing the holes in the template encoding a constraint of theform “there is an assignment to the holes that makes the template into a regex that correctlyclassifies the example”, and take the conjunction of the formulas over the examples. We make two
extensions to this to generate constraints for our extraction problem: bookkeeping of extracted
substring indexes for positive examples, and simulating the deterministic behavior of the regex
engine. While the former is a relatively straightforward extension, the latter is more subtle andwe next give an overview of how it is done. The key idea is to use continuations to encode in the
SMT constraint the deterministic behavior of the regex engine.6 For example, for the template.∗? (?<=<(□∗ )1 >)(□∗? )2 (?=<[/]\1>).∗ , the number of iterations of the lazy Kleene star □∗? depends
on the result of the matching of the continuation (?=<[/]\1>).∗ . That is, if the remaining substringof the example under consideration matches the continuation then we must not iterate the Kleene
star at all, and we encode such facts as SMT constraints, i.e., we encode conditions of the form “ifthe continuation is instantiated to match the remaining substring then ... else ...”.
If the SMT constraint is satisfiable, then R3 returns the obtained regex as the repair result.
Otherwise, R3 continues the search process by generating more templates as described above. R3
also performs template pruning to filter out useless templates. Template pruning is also used intemplate-based synthesis and repair methods for membership [Chen et al. 2020; Chida and Terauchi
2022b; Lee et al. 2016; Pan et al. 2019], and its high-level idea is simple: if a template cannot be
instantiated into a regex that is consistent with some example even if we replace the holes inthe template with arbitrary expressions, then there is no need to consider the template or any
template that can be obtained by expanding the holes of the template. However, the details of thepruning process are quite subtle, and we propose two novel pruning techniques that make use of theextraction information in positive examples, called approximation-by-pure-regex and approximationby-backreferences. Briefly, both techniques over-approximate the problem of detecting whether thetemplate can be pruned to the membership problem of whether a certain regex created from thetemplate accepts certain input strings created from the positive examples. The former techniquecreates a pure regex (i.e., one without backreferences or lookarounds) while the latter techniquedoes a more accurate but more expensive detection by creating a regex with backreferences. The
details are found in Section 5.
For the template .∗? (?<=<(□∗ )1 >)(□∗? )2 (?=<[/]\1 >).∗ , R3 finds that the generated constraint
is satisfiable, and replaces both holes with the set of characters [𝑎 − 𝑧] (which is a regex thatmatches any lowercase Latin alphabet) to return the repaired regex .∗? (?<=<( [𝑎 − 𝑧] ∗ )1 )>) ( [𝑎 −𝑧] ∗? )2 (?=</\1>).∗ , which is consistent with all the examples.

5 In general, R3 checks if the current template can be instantiated to a regex that correctly classifies the examples, by theprocess described in Searching Template Instances (note that a concrete regex is a template that does not have holes).
6 The idea to use continuations is inspired by the work of Sakuma et al. [2012] (cf. Section 7 for details).

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:63

Nariyoshi Chida and Tachio Terauchi

REGEX

In this section, we define the syntax and semantics of regexes. As remarked before, unlike the case of
membership, the deterministic behavior of the union and Kleene-star operators affect the semantics
of regexes. In this paper, we chose to the semantics of regexes used in JavaScript for two reasons.
First, JavaScript is one of the most popular programming languages for building Web applications,especially with regexes for extraction. Second, JavaScript has a language specification that defines
the syntax and semantics including that of regexes in a semi-formal fashion as the ECMAScript
language specification. We follow the latest version of the specification (as of November 2022), i.e.,
ECMAScript 2023 [ECMA International 2022].
Notation. Throughout the paper, we use the following notation. We write N for the set of natural
numbers, and [𝑖] for the set {1, 2, · · · , 𝑖} for 𝑖 ∈ N. For a sequence 𝑙, we write |𝑙 | for its length, 𝑙 [𝑖](for 0 ≤ 𝑖 < |𝑙 |) for its 𝑖th element, 𝑙 [𝑖..𝑗] for the sub-sequence from the 𝑖th element to the 𝑗thelement for 0 ≤ 𝑖 ≤ 𝑗 < |𝑙 |, and 𝑙 [𝑖..𝑗) for 𝑙 [𝑖..𝑗 − 1]. We fix a finite alphabet Σ. Then, we write𝑎, 𝑏 ∈ Σ for a character; 𝑥, 𝑦 ∈ Σ∗ for a sequence of characters (i.e., string); 𝜖 for the empty string.
For a function 𝑓 , we use 𝑑𝑜𝑚(𝑓 ) to denote the domain of 𝑓 . For a (partial) function 𝑓 , we write
𝑓 [𝛼 ↦→ 𝛽] for the (partial) function that maps 𝛼 to 𝛽 and behaves as 𝑓 for all other arguments.
3.1

Syntax and Informal Semantics

The syntax of regexes is defined as follows:𝑟::=[𝐶] | 𝜖 | 𝑟𝑟 | 𝑟 |𝑟 | 𝑟 ∗ | 𝑟 ∗? | (𝑟 )𝑖 | \𝑖 | (?=𝑟 ) | (?!𝑟 ) | (?<=𝑟 ) | (?<!𝑟 )where 𝐶 ⊆ Σ and 𝑖 ∈ N\{0}. The operator [𝐶] is the set of characters, which matches a characterin 𝐶. We write 𝑎 for [{𝑎}], . for [Σ], and [^𝐶] for [Σ \ 𝐶]. The operators 𝜖 and 𝑟 1𝑟 2 are the empty
string and the concatenation, respectively, and the semantics of the operators are standard. The
operator 𝑟 1 |𝑟 2 is the deterministic union, which first attempts to match 𝑟 1 , and if the matching fails,
then it attempts to match 𝑟 2 . The operators 𝑟 ∗ and 𝑟 ∗? are greedy and lazy Kleene stars, respectively,
which attempt to match 𝑟 as many (resp. few) as possible. The precedence order of the operators isdefined as follows: the (greedy and lazy) Kleene star, the concatenation, and the union. The left
one has a higher precedence. From these operators, we can construct the other operators definedin the ECMAScript language specification as syntactic sugars: the greedy and lazy Kleene plus 𝑟 +and 𝑟 +? as 𝑟 ∗𝑟 and 𝑟 ∗?𝑟 , respectively, the greedy and lazy optional operator 𝑟 ? and 𝑟 ?? as 𝑟 |𝜖 and𝜖 |𝑟 , respectively, and the greedy and lazy bounded repetition 𝑟 {𝑖, 𝑗 } and 𝑟 {𝑖, 𝑗 }?, where 𝑖 ≤ 𝑗, as
𝑟 1 ?𝑟 2 ? · · · 𝑟 𝑗 −𝑖 ?𝑟 𝑗 −𝑖+1 · · · 𝑟 𝑗 and 𝑟 1 ??𝑟 2 ?? · · · 𝑟 𝑗 −𝑖 ??𝑟 𝑗 −𝑖+1 · · · 𝑟 𝑗 , respectively. We often refer to regexesthat only consist of the above operators as pure regexes.
The remaining operators are real-world extensions. The operator (𝑟 )𝑖 is the capturing group, whichattempts to match 𝑟 , and if the attempt succeeds, stores the matched substring into a storage called
environment with the index 𝑖. Precisely, an environment is a mapping Γ from capturing groupindexes to substring positions such that for each capturing group index 𝑖, Γ(𝑖) is the substring
position stored at 𝑖. The captured substring positions are returned as extraction results.7 While regex
engines often allow capturing groups to be implicitly indexed by their positions, for readability
and without loss of generality, we assume that every capturing group in our paper has an explicit
index, i.e., all capturing groups in our paper are the so-called named capturing groups. However,as is often the case in real regex engines (and inevitably so when the indexes are implicit), we
require that every capturing group in a regex has a unique index, i.e., we assume the no-labelrepetition convention [Berglund and van der Merwe 2017]. The operator \𝑖 is the backreference,
7 Technically, only the last captured substring positions are returned if the capturing group is matched multiple times, andcapturing groups in negative lookaheads or lookbehinds are not subject to extraction (cf. Section 3.2).

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:7

which refers to the substring stored in the environment with the index 𝑖, and then attempts tomatch the substring. Note that, as in real regex engines, capturing groups serve the dual purpose of
returning the captured substring positions as extraction results and allowing backreferences torefer to the captured substrings. The operators (?=𝑟 ) and (?!𝑟 ) are positive and negative lookaheads,
respectively, which attempt to match (resp. not match) 𝑟 without any character consumption. The
operators (?<=𝑟 ) and (?<!𝑟 ) are positive and negative lookbehinds, respectively, which attempt tomatch (resp. not match) 𝑟 toward the left without any character consumption.
3.2

Formal Semantics

We now define the formal semantics of regexes. Traditionally, the semantics of pure regexes isdefined by induction on the structure of the pure regexes in a non-deterministic manner. In ourcase, it is difficult to use the same approach due to the real-world extensions and the determinism.
As a result, we define the semantics of regexes by a big-step semantics that models the behavior ofan actual regex engine that follows the ECMAScript 2023 language specification. Later in Section 5,
we extend the semantics to generate constraints for ensuring the correctness of repaired regexes.
We define the semantics as the deterministic matching relation (𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ ), where𝑟 is a regex, 𝑟𝑐 is a continuation regex, 𝑤 is an input string, 𝑝 and 𝑝 ′ are positions on the input
string, Γ and Γ ′ are environments, 𝑑 is a direction of the matching, and 𝑙 is a flag to indicate
whether the evaluation is in lookarounds or not. The continuation regex is a regex that needs
to be evaluated to finishing the matching. We use the continuation regex in the evaluation of
the union and Kleene-star operators to disambiguate the choice in the evaluation. For 𝑘 ∈ N, an
environment Γ : [𝑘] → N × N is a function that maps an index to a pair of integers that denotes
the position of a substring captured by the capturing-group operator with the index. The direction
is either forward or backward, meaning the position moves from left to right or from right to left,
respectively. We start an evaluation with the forward direction, and set the direction to backward
when entering lookbehinds. The flag 𝑙 is either true or false, which indicates whether the matchingis in lookarounds. We start an evaluation with the flag with false, and set the flag to true whenentering lookarounds. The judgement (𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ ) states that the regex 𝑟 attempts tomatch the input string 𝑤 from the position 𝑝 with the environment Γ, the continuation regex 𝑟𝑐 , thedirection 𝑑, and the flag 𝑙, and changes the position to 𝑝 ′ and the environment to Γ ′ . Additionally,
we write (𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ failed to denote the failure of the matching.
We now show the rules of the semantics. For space, we only describe some representative rules
shown in Figure 1. The full rules are given in Appendix E. The rules for the set-of-characters
operator say that, when the direction is forward, the matching succeeds if the character 𝑤 [𝑝] is in
the set of characters 𝐶. When the direction is backward, it looks back and checks the character𝑤 [𝑝 − 1]. The rules for the concatenation operator 𝑟 1𝑟 2 evaluate these expressions from left toright if the direction is forward and from right to left if the direction is backward. The forward
rules for the union operator 𝑟 1 |𝑟 2 first evaluate the concatenation of the subexpression 𝑟 1 and thecontinuation regex 𝑟𝑐 to check whether or not the consequent matching succeeds. If the matchingof the concatenation consumes all the remaining characters, it means that the whole matching
can be succeeded if we choose 𝑟 1 .8 From this, we then evaluate the subexpression 𝑟 1 . Otherwise,
we evaluate the subexpression 𝑟 2 . The backward rules for the union (shown in Appendix E) areanalogous but with the reverse order of 𝑟 1 and 𝑟𝑐 .
The rules for the greedy-Kleene-star operator first decide whether the iteration should beterminated by using the continuation regex. To this end, we evaluate the concatenation 𝑟 ⟨𝑟 ∗ : 𝑝⟩𝑟𝑐 .
8 Technically, this behavior is only for the case 𝑙 = false, i.e., when the union is not in a lookaround. When in a lookaround,

it is sufficient for the concatenation to just consume some prefix of the remaining characters, as stipulated by the rule.

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:8Nariyoshi Chida and Tachio Terauchi

Set of Characters𝑑 = forward

𝑝 < |𝑤 |𝑤 [𝑝] ∈ 𝐶

( [𝐶], 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 + 1, Γ)

0 ≤𝑝 −1𝑑 = backward

𝑤 [𝑝 − 1] ∈ 𝐶([𝐶], 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 − 1, Γ)Concatenation and Union𝑑 = forward(𝑟 1, 𝑟 2𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 ) 𝑑 = backward(𝑟 2, 𝑟𝑐 𝑟 1, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(𝑟 2, 𝑟𝑐 , 𝑤, 𝑝 1, Γ1, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 1, 𝑟𝑐 , 𝑤, 𝑝 1, Γ1, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 1𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ 2 )(𝑟 1𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 1𝑟𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )𝑑 = forward(𝑟 1, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(¬𝑙 ∧ 𝑝 1 = |𝑤 |) ∨ 𝑙(𝑟 1 |𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 1𝑟𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ 𝜏
𝜏 = failed ∨ (¬𝑙 ∧ 𝜏 = (𝑝 ′′, Γ ′′ ) where 𝑝 ′′ ≠ |𝑤 |)(𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )𝑑 = forward(𝑟 1 |𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )Greedy Kleene Star with Guards
𝑑 = forward(𝑟 ⟨𝑟 ∗ : 𝑝⟩𝑟𝑐 , 𝜖, 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )𝑝 1 = |𝑤 | ∨ 𝑙∗(𝑟, ⟨𝑟 : 𝑝⟩𝑟𝑐 , 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 ∗, 𝑟𝑐 , 𝑤, 𝑝 2, Γ2, 𝑑, 𝑙) ⇓ (𝑝 3, Γ3 )(𝑟 ∗, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 3, Γ3 )𝑝′ ≠ 𝑝𝑝′ = 𝑝(𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )(⟨𝑟 : 𝑝 ′ ⟩, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )(⟨𝑟 : 𝑝 ′ ⟩, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ failed

Lazy Kleene Star with Guards(𝑟𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ 𝜏
𝜏 = failed ∨ (¬𝑙 ∧ 𝜏 = (𝑝 ′, Γ ′ ) where 𝑝 ′ ≠ |𝑤 |)∗?
(𝑟 ⟨𝑟 : 𝑝⟩𝑟𝑐 , 𝜖, 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 3, Γ3 )𝑝 3 = |𝑤 | ∨ 𝑙(𝑟, ⟨𝑟 ∗? : 𝑝⟩𝑟𝑐 , 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(𝑟 ∗?, 𝑟𝑐 , 𝑤, 𝑝 1, Γ1, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )𝑑 = forward(𝑟 ∗?, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )Capturing Group, Backreference, and Positive Lookbehind(𝑟 $𝑖 , 𝑟𝑐 , 𝑤, 𝑝, Γ [𝑖 ↦→ (𝑝, ⊥)], 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )𝑑 = forward((𝑟 )𝑖 , 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )Γ(𝑖) = (𝑝 ′, 𝑝 ′′ )(𝑤 [𝑝 ′ ..𝑝 ′′ ), 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′′′, Γ ′ )(\𝑖, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′′′, Γ ′ )𝑖 ∉ 𝑑𝑜𝑚(Γ) ∨ Γ(𝑖) = (𝑝 ′, ⊥)(\𝑖, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ)𝑑 = forward

Γ(𝑖) = (𝑝, ⊥)($𝑖 , 𝑟𝑐 , 𝑤, 𝑝 ′, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ [𝑖 ↦→ (𝑝, 𝑝 ′ )])(𝑟, 𝜖, 𝑤, 𝑝, Γ, backward, true) ⇓ (𝑝 ′, Γ ′ )((?<=𝑟 ), 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ ′ )Fig. 1. Selected evaluation rules for regexes.

Here, the expression ⟨𝑟 ∗ : 𝑝⟩ is the Kleene-star operator with the guard operator that is used to
avoid non-terminating evaluation due to problematic regexes [Frisch and Cardelli 2004; Sakuma
et al. 2012], i.e., regexes of the form 𝑟 ∗ or 𝑟 ∗? where 𝑟 can match 𝜖. A guard operator ⟨𝑟 : 𝑝⟩ checks
whether or not the current position is the same as the position 𝑝. If so, then the evaluation of theguard operator fails. Otherwise, it evaluates the regex 𝑟 . We return to the explanation of the rules
for evaluating the greedy-Kleene-star operator. If the matching of the concatenation 𝑟 ⟨𝑟 ∗ : 𝑝⟩𝑟𝑐
consumes all the remaining characters, i.e., the whole matching can be succeeded even if we choose
to iterate the Kleene star, then we evaluate 𝑟 by (𝑟, ⟨𝑟 ∗ : 𝑝⟩𝑟𝑐 , 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 ), andProc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:9

continue the iteration from (𝑟 ∗, 𝑟𝑐 , 𝑤, 𝑝 2, Γ2, 𝑑, 𝑙). Here, reset(𝑟 , Γ) is an environment {(𝑖, (𝑝 ′, 𝑝 ′′ )) ∈
Γ | 𝑖 is not an index of a capturing group in 𝑟 }. This means that, for each iteration, the Kleene-star
operator returns the environment back to the state before we evaluate it. This behavior is consistent
with the ECMAScript 2023 language specification. Otherwise, i.e., the matching of the concatenation
fails or does not consume all the remaining characters, then we cannot iterate the Kleene-star
operators and therefore stop the iteration by returning the matching result (𝑝 1, Γ1 ).9 The rules
for the lazy-Kleene-star operator are similar to those for the greedy-Kleene-star operator. The
main difference is that the lazy-Kleene-star operator first checks whether the whole matching cansucceed without the iteration by (𝑟𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙). If it succeeds, then the lazy-Kleene-star operator
stops the iteration. Otherwise, it tries to iterate in a similar way as the greedy-Kleene-star operator.
The rules for the capturing-group operator (𝑟 )𝑖 evaluate the regex 𝑟 with the close symbol $𝑖 that
denotes the end of the 𝑖th capturing group. Evaluating $𝑖 closes the 𝑖th capturing group, and sets
the end position of the substring captured by the 𝑖th capturing group. We use the close symbol toevaluate backreferences in the continuation regex correctly. The rule for the backreference operator\𝑖 refers to the pair of indexes in the environment Γ(𝑖) = (𝑝 ′, 𝑝 ′′ ), and evaluates the substring
represented by the indexes, i.e., 𝑤 [𝑝 ′ ..𝑝 ′′ ). If the environment Γ does not have 𝑖 in the domain (i.e.,𝑖 ∉ 𝑑𝑜𝑚(Γ)) or the 𝑖th capturing group is not closed yet (i.e., Γ(𝑖) = (𝑝 ′, ⊥)), the backreference \𝑖 isevaluated as the empty string 𝜖, e.g., the regex \1(𝑎)1 exactly matches the string 𝑎. In this case, thebackreference is called unassigned backreference. The semantics is consistent with the ECMAScript
2023 specification that treats unassigned backreference as 𝜖.
The rule for the positive lookbehind operator (?<=𝑟 ) sets the direction to backward and the flag
to true, and then evaluates the regex 𝑟 . After evaluating the regex 𝑟 , it resets the position 𝑝 ′ to𝑝. Note that we do not reset the environment. This means that substrings captured in positive
lookbehinds can be used from outside of the positive lookbehinds. Additionally, the continuationin the hypothesis is set to 𝜖 to reflect the facts that a lookbehind only concerns whether the input
string can be scanned backward from the current position to match just the expression in the
lookbehind (i.e., 𝑟 ) and that once we move outside of the lookbehind we do not backtrack to insideof it (i.e., even in the event of a match failure in the outer continuation 𝑟𝑐 of the conclusion).
Next, we provide some examples. In Examples 3.1 and 3.3, we omit the information of directions
and flags because they are always forward and false, respectively. Additionally, in Example 3.1, we
also omit the information of environments because they are always ∅. From this, the evaluations of
Example 3.1 return a position instead of a pair of a position and an environment.
Example 3.1. The matching of (𝑎|𝑎𝑎)𝑎 on 𝑎𝑎𝑎 is:
𝑎 ∈ {𝑎}𝑎 ∈ {𝑎}(𝑎, 𝑎, 𝑎𝑎𝑎, 0) ⇓ 1(𝑎, 𝜖, 𝑎𝑎𝑎, 1) ⇓ 2(𝑎𝑎, 𝜖, 𝑎𝑎𝑎, 0) ⇓ 2
2 ≠ |𝑎𝑎𝑎|(𝑎|𝑎𝑎, 𝑎, 𝑎𝑎𝑎, 0) ⇓ 2···(𝑎𝑎, 𝑎, 𝑎𝑎𝑎, 0) ⇓ 2

𝑎 ∈ {𝑎}(𝑎, 𝜖, 𝑎𝑎𝑎, 2) ⇓ 3((𝑎|𝑎𝑎)𝑎, 𝜖, 𝑎𝑎𝑎, 0) ⇓ 3.
Since the whole matching of the regex on the string succeeds, the regex accepts the string.
Example 3.2. The matching of ..(?<=(.)1 ) on 𝑎𝑏 is:
9 This behavior is only for the case the Kleene star is not in a lookaround. The difference in the behavior when in a lookaroundis similar to that for the union.

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:10

Nariyoshi Chida and Tachio Terauchi

Γ0 (1) = (⊥, 2)𝑎∈Σ(., $1, 𝑎𝑎, 2, Γ0, backward, true) ⇓ (1, Γ0 )($1, 𝜖, 𝑎𝑎, 1, Γ0, backward, true) ⇓ (1, Γ1 )($1 ., 𝜖, 𝑎𝑎, 2, Γ0, backward, true) ⇓ (1, Γ1 )((.)1, 𝜖, 𝑎𝑎, 2, ∅, backward, true) ⇓ (1, Γ1 )···((?<=(.)1 ), 𝜖, 𝑎𝑎, 2, ∅, forward, false) ⇓ (2, Γ1 )(..(?<=(.)1 ), 𝜖, 𝑎𝑎, 0, ∅, forward, false) ⇓ (2, Γ1 )where Γ0 = {(1, (⊥, 2))} and Γ1 = {(1, (1, 2))}. The regex accepts the string, and extracts the second
character 𝑎 by the 1st capturing group.
Example 3.3. The matching of (.∗ )1 \1 on 𝑎𝑎 is:AB((.∗ )1 \1, 𝜖, 𝑎𝑎, 0, ∅) ⇓ (2, Γ1 )where Γ1 = {(1, (0, 1))} and 𝐴 and 𝐵 are subderivations. The subderivation 𝐴 is:𝑎∈Σ···(.⟨.∗ : 0⟩$1 \1, 𝜖, 𝑎𝑎, 0, Γ0 ) ⇓ (2, Γ1 )(., ⟨.∗ : 0⟩$1 \1, 𝑎𝑎, 0, Γ0 ) ⇓ (1, Γ0 )···(.∗, $1 \1, 𝑎𝑎, 0, Γ0 ) ⇓ (1, Γ0 )(.∗ $1, \1, 𝑎𝑎, 0, Γ0 ) ⇓ (1, Γ1 )((.∗ )1, \1, 𝑎𝑎, 0, ∅) ⇓ (1, Γ1 )

Γ0 (1) = (0, ⊥)($1, \1, 𝑎𝑎, 1, Γ0 ) ⇓ (1, Γ1 )where Γ0 = {(1, (0, ⊥))}.
The subderivation 𝐵 is:𝑎 ∈ {𝑎}Γ1 (1) = (0, 1)(𝑎, 𝜖, 𝑎𝑎, 1, Γ1 ) ⇓ (2, Γ1 )(\1, 𝜖, 𝑎𝑎, 1, Γ1 ) ⇓ (2, Γ1 ).
The regex accepts the input string, and extracts first character 𝑎 by the 1st capturing group.
Example 3.4. Recall the motivating example from Section 2. We show a subderivation of thematching of the repaired regex on the input string 𝑤 = <𝑎><𝑎>𝑎</𝑎></𝑎>. For the subexpression𝑟 = ( [𝑎 − 𝑧] ∗? )2 , the continuation regex 𝑟𝑐 = (?=<[/]\1 >).∗ , the position 𝑝 = 6, the environment
Γ = {(1, (4, 5))}, the direction 𝑑 = forward, and the flag 𝑙 = false, the subderivation is:($2𝑟𝑐 , 𝜖, 𝑤, 𝑝, Γ0, 𝑑, 𝑙) ⇓ failed

𝐴

𝐵

𝐶

( [𝑎 − 𝑧] ∗?, $2𝑟𝑐 , 𝑤, 𝑝, Γ0, 𝑑, 𝑙) ⇓ (𝑝 + 1, Γ0 )($2, 𝑟𝑐 , 𝑤, 𝑝 + 1, Γ0, 𝑑, 𝑙) ⇓ (𝑝 + 1, Γ1 )∗?
( [𝑎 − 𝑧] $2, 𝑟𝑐 , 𝑤, 𝑝, Γ0, 𝑑, 𝑙) ⇓ (𝑝 + 1, Γ1 )(𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 + 1, Γ1 )where Γ0 = Γ [2 ↦→ (𝑝, ⊥)] and Γ1 = Γ[2 ↦→ (𝑝, 𝑝 +1)]. The subderivation 𝐴 derives ( [𝑎−𝑧] ⟨[𝑎−𝑧] ∗? :𝑝⟩$2𝑟𝑐 , 𝜖, 𝑤, 𝑝, reset ( [𝑎 −𝑧], Γ0 ), 𝑑, 𝑙) ⇓ (|𝑤 |, Γ1 ), 𝐵 derives ( [𝑎 −𝑧], ⟨[𝑎 −𝑧] ∗? : 𝑝⟩$2𝑟𝑐 , 𝑤, 𝑝, reset ( [𝑎 −𝑧], Γ0 ), 𝑑, 𝑙) ⇓ (𝑝 + 1, Γ0 ), and 𝐶 derives ( [𝑎 − 𝑧] ∗?, $2𝑟𝑐 , 𝑤, 𝑝 + 1, Γ0, 𝑑, 𝑙) ⇓ (𝑝 + 1, Γ0 ). Therefore, theregex 𝑟 consumes and captures the 𝑝th character of 𝑤, i.e., the middle character 𝑎 of 𝑤.
Finally, we define the language of regexes for extraction called capturing language, a terminology
borrowed from [Loring et al. 2019]. A capturing language of a regex is a set of pairs of an input
string and the environment containing the information about the substrings extracted from the
input string when matched against the regex.
Definition 3.5 (Capturing Language). The capturing language L𝑐 (𝑟 ) of a regex 𝑟 is defined asL𝑐 (𝑟 ) = {(𝑤, Γ) | (𝑟, 𝜖, 𝑤, 0, ∅, forward, false) ⇓ (|𝑤 |, Γ)}.
Additionally, we define the (non-capturing) language of 𝑟 by L (𝑟 ) = {𝑤 | ∃Γ.(𝑤, Γ) ∈ L𝑐 (𝑟 )}.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:11

Validation of the formal semantics. In order to validate our semantics, we have implemented aregex engine based on our semantics, and evaluated it on the data sets used in our evaluation andregexes that involve JavaScript-specific behavior taken from Davis et al. [2019]. In all cases, wehave confirmed that the behavior of our regex engine is consistent with that of actual JavaScript
regex engines.
4

REPAIR PROBLEM

In this section, we define our PBE regex repair problem for extraction called extraction-regex-repair
problem. There are two types of examples: positive examples and negative examples. For 𝑘 ∈ N, a
positive example is a pair (𝑤, Γ) ∈ Σ∗ × ( [𝑘] → N × N) for some 𝑘 ≥ 1 that should belong to thecapturing language of the to-be synthesized regex. That is, 𝑤 is a string to be accepted and Γ denotes
the indexes of the substrings to be extracted from 𝑤. For readability, we use L𝑖 and M𝑖 (or L and M𝑖 if
there is no danger of ambiguity) to denote a substring to be extracted by the 𝑖th capturing group in
a positive example. For example, we write L1𝑎L2𝑏M2𝑐M1 to denote a positive example (𝑎𝑏𝑐, Γ) whereΓ = {(1, (0, 3)), (2, (1, 2))}. A negative example is 𝑤 ∈ Σ∗ that should not belong to the language ofthe to-be synthesized regex, i.e., a string to be rejected.
Before we define the repair problem, we recall the notion of distance from prior works on PBEbased repair of regexes [Chida and Terauchi 2022b; Pan et al. 2019]. The notion is used to quantify
the quality of a repair. That is, a regex of a short distance from the pre-repair regex is deemed to beof high quality, justified by the assumption that the pre-repair regex may not be correct but is close
to the one the user intended.
Definition 4.1 (Distance [Chida and Terauchi 2022b; Pan et al. 2019]). For subtrees 𝑟 1, . . . , 𝑟𝑛 of aregex 𝑟 , the edit 𝑟 [𝑟 1′ /𝑟 1, . . . , 𝑟𝑛′ /𝑟𝑛 ] replaces each 𝑟𝑖 with 𝑟𝑖′ . The cost of an edit is the sum of thenumber of nodes in 𝑟𝑖 and 𝑟𝑖′ (for 𝑖 ∈ [𝑛]). Given two regexes 𝑟 1 and 𝑟 2 , the distance between 𝑟 1 and𝑟 2 , 𝐷 (𝑟 1, 𝑟 2 ), is the minimum cost of an edit that rewrites 𝑟 1 to 𝑟 2 .
We now define the extraction-regex-repair problem.
Definition 4.2 (Extraction-Regex-Repair Problem). Given a regex 𝑟 1 , a set of positive examples
E + and a set of negative examples E − satisfying satisfying (𝑤, Γ1 ), (𝑤, Γ2 ) ∈ E + ⇒ Γ1 = Γ2 andE − ∩ {𝑤 | (𝑤, _) ∈ E + } = ∅, the extraction-regex-repair problem is the problem of synthesizinga regex 𝑟 2 that is consistent with the examples (i.e., E + ⊆ L𝑐 (𝑟 2 ) and E − ∩ L (𝑟 2 ) = ∅) and the
distance from 𝑟 1 is minimal (i.e., 𝐷 (𝑟 1, 𝑟 2 ) ≤ 𝐷 (𝑟 1, 𝑟 3 ) for any 𝑟 3 consistent with the examples).
In what follows, we show some interesting results regarding the extraction-regex-repair problem:(1) there are unsolvable problem instances if repaired regexes are not allowed to use the extensions(i.e., pure regexes), whereas (2) every problem instance is solvable if the extensions are allowed.
For (1), we show that there are non-trivial unsolvable problem instances, i.e., there are unsolvable problem instances even if positive examples do not have overlaps in its extraction such as(𝑎𝑏𝑐, {(1, (0, 2)), (2, (1, 3))}), represented as L1𝑎L2𝑏M1𝑐M2 .10
Theorem 4.3. There exist extraction-regex-repair-problem instances without overlaps that do nothave a pure regex solution.

Proof. Let Σ = {𝑎, 𝑏} for simplicity. Then, we show that the instance 𝑟 1 = 𝜖, E + = {(𝑎𝑏, Γ0 ), (𝑏𝑎, Γ1 )}where Γ0 = {(1, (0, 1))} and Γ1 = {(1, (1, 2))}, and E − = {𝜖, 𝑎, 𝑏, 𝑎𝑎, 𝑏𝑏} does not have a pure regex
solution. Roughly, if there exists a solution, then the form of the solution must be 𝑟 ′ (𝑟 𝑎 )1𝑟 ′′ where𝑟 𝑎 is a regex that matches the character 𝑎, and 𝑟 ′ and 𝑟 ′′ need to match the empty string 𝜖 and the
10 It is trivial to see that no pure regex can have such an extraction result. By contrast, it is an interesting consequence ofTheorem 4.4 that the repair problem is solvable even with such overlaps when the extensions are allowed.

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:12Nariyoshi Chida and Tachio Terauchi

Algorithm 1: The repair algorithm
Input: a regex 𝑟 , a set of positive examples E + , and a set of negative examples E −Output: a regex that satisfies the consistency condition and the minimal distance criteria
1: Q ← { 𝑟 }2: while Q is not empty do3:t ← Q.pop()4:
if {𝑤 | (𝑤, _) ∈ E + } ⊆ L (𝑡 ⊤ ), E − ∩ L (𝑡 ⊥ ) = ∅, and IsFeasible(𝑡, E + , .∗ ) then5:
if {𝑤 | (𝑤, _) ∈ E + } ⊆ L (𝑡 ⊤,Σ ) and IsFeasible(𝑡, E + , .) then6:
Φ ← generateConstraintForExtraction(𝑡, E +, E − )7:
if Φ is satisfiable then8:
return solution(𝑡, Φ)
9:Q.push(expandHoles(𝑡))10:Q.push(addOrReduceHoles(𝑡))character 𝑏 to be a solution. However, the regex accepts the negative example 𝑎 ∈ E − , which is acontradiction. The full proof appears in Appendix A.
□
Theorem 4.4. The extraction-regex-repair problem always has a solution.
Proof. We construct a regex that only accepts the positive examples by using lookarounds,
and therefore it satisfies the consistency condition. Then, the result follows from the fact that theexistence of a regex consistent with the examples implies the existence of a minimal such one. The
full proof appears in Appendix B.
□
These results indicate that the real-world extensions play a crucial role in the repair problem.
Finally, we show that the extraction-regex-repair problem is NP-hard. We prove this by a reduction
from the set-cover problem which is NP-complete [Karp 1972]. For this, we consider the decisionversion of the extraction-regex-repair problem. That is, given a regex 𝑟 1 , sets of positive and negative
examples, and 𝑘 ∈ N, the decision version of the extraction-regex-repair problem is the problem ofsynthesizing a regex 𝑟 2 that is consistent with the examples and satisfies 𝐷 (𝑟 1, 𝑟 2 ) ≤ 𝑘. The proof isin Appendix C.
Theorem 4.5. The extraction-regex-repair problem is NP-hard.
5

REPAIR ALGORITHM

We now describe our algorithm for solving the repair problem. At a high level, our algorithm
is based on the enumerative search with an SMT solver introduced in the previous works formembership [Chida and Terauchi 2022b; Pan et al. 2019]. The main new ideas introduced in thispaper are the SMT constraint generation that respects the deterministic semantics and the newpruning techniques that make use of the extraction information in the positive examples. We first
give an overview of our algorithm in Section 5.1, and then present the details of the new ideas in
Section 5.3 and 5.2.
5.1

Overview

Algorithm 1 shows the algorithm. Our algorithm takes as input an instance of the extraction-regexrepair problem, i.e., a regex 𝑟 , a set of positive examples E + , and a set of negative examples E − . It
returns a regex that satisfies the condition required for the solution of the problem, i.e., it is one
that is consistent with the examples and the distance from 𝑟 is minimal.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:13

Initializing a template. Our algorithm maintains a priority queue 𝑄 to store template regexes. A
template regex is a regex with the operator called hole denoted as □. More specifically, the syntaxof the template 𝑡 is defined as: 𝑡 ::= [𝐶] | 𝜖 | 𝑡𝑡 | · · · | (?<!𝑡) | □, i.e., the only difference between
the syntax of regexes and templates is the existence of the hole. Roughly, a hole is a placeholderthat is to be replaced with some concrete regex. At the beginning, our algorithm initializes thepriority queue 𝑄 to contain the given regex 𝑟 as a template at Line 1. The priority queue 𝑄 ranks
its elements by the distance so that the template that is closer to the given regex 𝑟 in terms of the
distance has a higher priority. This ensures that the returned regex satisfies the minimality criteria,
i.e., it is of minimal distance among ones that are consistent with the examples.
Template Pruning by Approximations. Next, we retrieve a template that has the highest
priority from the priority queue 𝑄 at Line 3. Then, we apply template pruning at Line 4. The test{𝑤 | (𝑤, _) ∈ E + } ⊆ L (𝑡 ⊤ ), E − ∩ L (𝑡 ⊥ ) = ∅ is analogous to the pruning used in the prior works
on membership [Chen et al. 2020; Chida and Terauchi 2022b; Lee et al. 2016; Pan et al. 2019], andworks by building an over- and under-approximating regexes 𝑡 ⊤ and 𝑡 ⊥ . The regexes satisfy theproperties L (𝑟 ′ ) ⊆ L (𝑡 ⊤ ) for any regex 𝑟 ′ obtainable by filling the holes of 𝑡 by arbitrary regexes.
Therefore, if the test fails, then we can safely prune the template and any template obtainable byexpanding the holes of the template (cf. Expanding, Adding, or Reducing Holes below). The
construction of 𝑡 ⊤ and 𝑡 ⊥ can be found in Appendix D.
However, the above pruning is not enough for our purpose because it does not consider extraction.
For example, consider a template 𝑡 = 𝑎(𝑏□)1 and a positive example L𝑎𝑏𝑐M1 . The above pruning
technique cannot discard the template because the over-approximated regex is 𝑡 ⊤ = 𝑎(𝑏.∗ )1 and{𝑎𝑏𝑐 | (𝑎𝑏𝑐, (1, 3)) ∈ E + } ⊆ L (𝑡 ⊤ ). However, 𝑡 cannot become a regex consistent with the example
because any regex obtained from it consumes the first character 𝑎 without extraction.
Thus, for positive examples, we apply new template pruning techniques for extraction introducedin this paper, denoted as IsFeasible in Algorithm 1. The idea of our pruning is to construct a regex
and an input string from a template and a positive example by embedding the information of
extraction. We defer the details of our pruning technique for extraction to Section 5.3.
Constraint Solving for Finding a Solution. If the pruning by approximations passes, thenwe check whether the template can be turned into a regex that is consistent with the examples
by replacing its holes with some sets of characters. For this, our algorithm generates an SMT
constraint at Line 6. As remarked before, the constraint generation builds on that proposed formembership [Chida and Terauchi 2022b; Pan et al. 2019], and works by generating an SMT formula
𝜙𝑒 constructed for each example 𝑒 ∈ E + ∪ E − that encodes the condition for correctly classifying
𝑒. In more detail, 𝜙𝑒 is over propositional variables 𝑣𝑖𝑎 where 𝑖 ∈ N denotes the 𝑖th hole in thetemplate and 𝑎 ∈ Σ. The variable 𝑣𝑖𝑎 is set to true if and only if the set of characters that fills theÓ
𝑖th hole contains the character 𝑎. The final constraint is the conjunction 𝑒 ∈ E + ∪E − 𝜙𝑒 , and if theconstraint is satisfiable, we obtain from the solution a regex that correctly classifies all examples. As
remarked before, one of the key innovations of our work is a method for generating a constraint that
respects the deterministic semantics of an actual regex engine. For this, we design the constraint
generation algorithm by following our novel formal semantics presented Section 3.2. We defer
further details of the constraint generation to Section 5.2. Once we find a solution, we apply thefollowing generalization technique to the solution: we add characters to the sets of charactersthat were obtained by replacing holes in the template as long as the additions do not violate theconsistency of the examples.
Expanding, Adding, or Reducing Holes. If the SMT constraint is unsatisfiable, then we continue to explore by enumerating templates. At Line 9, we expand holes in the template by replacing a hole with an expression all of whose immediate subexpressions are holes. At Line 10,
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:14

Nariyoshi Chida and Tachio TerauchiHole𝑑 = forward□ is the 𝑖th hole.

𝑝 < |𝑤 |𝑤 [𝑝 ]𝑤 [𝑝 ](□, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 + 1, Γ, 𝑣𝑖)}, {(⊥, ⊥, ¬𝑣𝑖)})

𝑑 = backward□ is the 𝑖th hole.

0 ≤𝑝 −1𝑤 [𝑝 −1]𝑤 [𝑝 −1](□, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 − 1, Γ, 𝑣𝑖)}, {(⊥, ⊥, ¬𝑣𝑖)})

Set of Characters𝑑 = forward

𝑝 < |𝑤 |𝑤 [𝑝] ∈ 𝐶

𝑑 = backward( [𝐶], 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 + 1, Γ, true)}, ∅)0 ≤𝑝 −1𝑤 [𝑝 − 1] ∈ 𝐶([𝐶], 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 − 1, Γ, true)}, ∅)Union𝑑 = forward(𝑡 1𝑡𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆 1, 𝐹 1 )𝑆 1′ = ite(𝑙, 𝑆 1, {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 1 | 𝑝 ′ = |𝑤 |})𝐹 1′ = 𝐹 1 ∪ ite(𝑙, ∅, {(⊥, ⊥, 𝜙 ′ ) | (𝑝 ′, _, 𝜙 ′ ) ∈ 𝑆 1, 𝑝 ′ ≠ |𝑤 |})ÔÔ
𝜙𝑆 1 = (_,_,𝜙 ′ ) ∈𝑆 1′ 𝜙 ′𝜙 𝐹1 = (⊥,⊥,𝜙 ′ ) ∈𝐹1′ 𝜙 ′(𝑡 1, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆 2, 𝐹 2 )(𝑡 2, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆 3, 𝐹 3 )(𝑡 1 |𝑡 2, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 ′, Γ ′, 𝜙𝑆 1 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 2 } ∪ {(𝑝 ′, Γ ′, 𝜙 𝐹1 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 3 },{(⊥, ⊥, 𝜙 𝐹1 ∧ 𝜙 ′ ) | (⊥, ⊥, 𝜙 ′ ) ∈ 𝐹 3 })Capturing Group, Backreference, and Positive Lookbehind𝑑 = forward(𝑡$𝑖 , 𝑡𝑐 , 𝑤, 𝑝, Γ [𝑖 ↦→ (𝑝, ⊥)], 𝑑, 𝑙) d (𝑆, 𝐹 )𝑑 = forward

Γ(𝑖) = (𝑝 ′, ⊥)($𝑖 , 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ [𝑖 ↦→ (𝑝 ′, 𝑝)], true)}, ∅)((𝑡)𝑖 , 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )Γ(𝑖) = (𝑝 ′, 𝑝 ′′ ) (𝑤 [𝑝 ′ ..𝑝 ′′ ), 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )𝑖 ∉ 𝑑𝑜𝑚(Γ) ∨ Γ(𝑖) = (𝑝 ′, ⊥)(\𝑖, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )(\𝑖, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, true)}, ∅)(𝑡, 𝜖, 𝑤, 𝑝, Γ, backward, true) d (𝑆, 𝐹 )((?<=𝑡), 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ ′, 𝜙 ′ ) | (_, Γ ′, 𝜙 ′ ) ∈ 𝑆 }, 𝐹 )Fig. 2. Selected rules for generating an SMT constraint.

we add a hole to the template by replacing a leaf subexpression (i.e., a set of characters [𝐶],the empty string 𝜖, or a backreference \𝑖) by a hole. Additionally, we reduce an expression having a hole as an immediate subexpression into a hole. For example, we have expandHoles(□) ={□□, □|□, □∗, □∗?, (□)𝑖 , (?=□), (?!□), (?<=□), (?<!□)}. And for the template 𝑡 = (□|□)𝑎\𝑖, we have
addOrReduceHoles(𝑡) = {□𝑎\𝑖, (□|□)□\𝑖, (□|□)𝑎□}. This part is essentially identical to that ofthe previous works [Chida and Terauchi 2022b; Pan et al. 2019], and we refer to them for further
information.
5.2

SMT Constraint Generation

We describe the SMT constraint generation. As remarked before, for each example, we construct an
SMT formula that encodes the condition that the regex obtained from a satisfying assignment to theformula correctly classifies the example. For this, we define constraint generation rules that derivejudgements of the form (𝑡, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 ). The rules are designed based on the rules of ournovel formal semantics of regexes (cf. Section 3.2) and have a similar form. Namely, 𝑡 is a templateregex, 𝑡𝑐 is a continuation template regex, 𝑤 is an input string, 𝑝 is a position on the input string, Γis an environment, 𝑑 is a direction, and 𝑙 is a flag. 𝑆 and 𝐹 are sets of results of succeeded or failed
matching with constraints. A result of succeeded (resp. failed) matching with constraints is a tuple(𝑝 ′, Γ ′, 𝜙), meaning that the matching succeeds (resp. fails) at position 𝑝 ′ with the environment Γ ′Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:15if the constraint 𝜙 is satisfiable. In the case of failed matching, 𝑝 ′ = ⊥ and Γ ′ = ⊥. For space, weshow selected rules in Figure 2. The full rules are given in Appendix F. In the figure, the function
ite is defined by: ite(true, 𝐴, 𝐵) = 𝐴 and ite(false, 𝐴, 𝐵) = 𝐵.
The main difference from the rules of the formal semantics is that the constraint generation rules
return (a pair of) sets of matching results each paired with an SMT formula, whereas the semantics
just returns a single matching result. This is so because the constraint generation rules simulate all
possible (deterministic) runs of the regex on the example string that can be obtained by changing
the sets of characters to fill the holes, pair each such result with the constraint formula that mustbe satisfied for the run that yields the result to be actually happen, and return the set of such pairs(divided into two sets: one for the successful runs, i.e., 𝑆, and one for the failing runs, i.e., 𝐹 ).
For example, in the rules for holes, the matching can succeed (resp. fail) at position 𝑝 by assigning(resp. not assigning) the character 𝑤 [𝑝] in the set of characters to fill the hole. Thus, in the case𝑤 [𝑝 ]of 𝑑 = forward, the rule returns as the successful result (𝑝 + 1, Γ, 𝑣𝑖) and as the failing result𝑤 [𝑝 −1](𝑝 − 1, Γ, 𝑣𝑖), meaning that the hole can be filled with the set of characters [𝐶] such that𝑤 [𝑝] ∈ 𝐶 (resp. 𝑤 [𝑝 − 1] ∉ 𝐶) to succeed (resp. fail) the matching. The rules for the other operators
follow the corresponding rules of the formal semantics, and similarly to the rules for holes, takecare of the fact that there can be multiple matching results due to the choice of how the holes arefilled. For example, like the corresponding rule of the formal semantics, the forward rule for theunion operator 𝑡 1 |𝑡 2 first evaluates the concatenation of the subexpression 𝑡 1 and the continuation
template regex 𝑡𝑐 . However, unlike the corresponding rule of the formal semantics, the rule ofthe concatenation 𝑡 1𝑡𝑐 returns sets of results of succeeded and failed matching with constraints.
Therefore, the rule next evaluates both cases of succeeded and failed matching. In the case of thesucceeded matching, the rule evaluates the subexpression 𝑡 1 , and obtains the sets of succeeded andfailed matching results with constraints, i.e., 𝑆 2 and 𝐹 2 , respectively. Similarly, in the case of thefailed matching, the rule evaluates the subexpression 𝑡 2 , and obtains the sets of succeeded and failed
matching results with constraints, i.e., 𝑆 3 and 𝐹 3 , respectively. Finally, from these results, the rule
constructs the results for 𝑡 1 |𝑡 2 . Specifically, the results of succeeded matching of 𝑡 1 |𝑡 2 consist of thecase that the matchings of both 𝑡 1𝑡𝑐 and 𝑡 1 succeed and the case that the matching of 𝑡 1𝑡𝑐 fails but
the matching of 𝑡 2 succeeds. Hence, they consist of (𝑝 ′, Γ ′, 𝜙𝑆1 ∧ 𝜙 ′ ), where (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 2 and 𝜙𝑆1
is the constraint for succeeding in the matching of 𝑡 1𝑡𝑐 , and (𝑝 ′, Γ ′, 𝜙 𝐹1 ∧ 𝜙 ′ ), where (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 3
and 𝜙 𝐹1 is the constraint for failing in the matching of 𝑡 1𝑡𝑐 . Also, the results of failed matching of 𝑡 1 |𝑡 2
consist of the case that the matching of both 𝑡 1𝑡𝑐 and 𝑡 2 fails. Hence, they consist of (⊥, ⊥, 𝜙 𝐹1 ∧ 𝜙 ′ )where (⊥, ⊥, 𝜙 ′ ) ∈ 𝐹 3 and 𝜙 𝐹1 is the constraint for failing in the matching of 𝑡 1𝑡𝑐 .
Finally, for a template 𝑡, a set of positive examples E + , and a set of negative examples E − , wedefine the SMT constraints as Φ = Φ+ ∧ Φ− where Φ+ and Φ− are constraints for positive andnegative examples, respectively. The constraints Φ+ and Φ− are defined as follows.
ÓÓ• Φ+ = 𝑒=(𝑤,Γ) ∈ E + encode+ (𝑡, 𝑒) where encode+ (𝑡, 𝑒) = ( |𝑤 |,Γ,𝜙 ) ∈𝑆 𝜙 andÓÓ• Φ− = 𝑤 ∈ E − ¬encode− (𝑡, 𝑤) where encode− (𝑡, 𝑤) = ( |𝑤 |,_,𝜙 ) ∈𝑆 𝜙
with (𝑡, 𝜖, 𝑤, 0, ∅, forward, false) d (𝑆, 𝐹 ).
As an example of the SMT constraint generation, consider a template 𝑡 = (𝑎|𝑎𝑎)1 (□|𝜖), a set of
positive examples E + = {L𝑎𝑎M1 }, and a set of negative examples E − = {𝑎𝑏}. Then, the constraint
for the positive example is Φ+ = ¬𝑣 1𝑎 and the constraint for the negative example is Φ− = ¬𝑣 𝑏1 .
Therefore, the constraint for the examples is Φ = ¬𝑣 1𝑎 ∧ ¬𝑣 𝑏1 . Additionally, consider the template.∗? (?<=<(□∗ )1 >)(□∗? )2 (?=<[/]\1 >).∗ from Section 2. The constraints for the subexpression 𝑡 =(□∗? )2 on the example 𝑤 =<𝑎><L𝑎M1 >L𝑎M2 </𝑎></𝑎> from the position 𝑝 = 6 with the continuation
template regex 𝑡𝑐 = (?=<[/]\1 >).∗ , the environment Γ = {(1, (4, 5))}, the direction 𝑑 = forward,
and the flag 𝑙 = true are constructed by the judgement (𝑡, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 ) where 𝑆 =Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:16

Nariyoshi Chida and Tachio Terauchi{(𝑝, Γ ∪ {(2, (6, 6))}, ¬𝑣 2𝑎 ), (𝑝 + 1, Γ ∪ {(2, (6, 7))}, 𝑣 2𝑎 )} and 𝐹 = ∅. Here, for example, the second
element (𝑝 + 1, Γ ∪ {(2, (6, 7))}, 𝑣 2𝑎 ) of 𝑆 indicates that, if the hole of (□∗? )2 is replaced with the set ofcharacters [𝐶] where 𝑎 ∈ 𝐶, then (( [𝐶] ∗? )2, (?=<[/]\1 >).∗, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 + 1, Γ ∪ {(2, (6, 7))}).
5.3

Over-Approximation for Extraction

In this section, we introduce two novel pruning techniques for extraction. We first introduce
the pruning technique that exploits backreferences, namely approximation-by-backreferences, toensure the correctness of extraction in Section 5.3.1. Although the pruning technique can support
real-world extensions, it sometimes suffers from regular expression denial of service (ReDoS) [Daviset al. 2018] that stops the repair procedure for a long time. To avoid ReDoS, we introduce ReDoS-freepruning technique for extraction, namely approximation-by-pure-regex, in Section 5.3.2. Although
the second pruning technique does not support real-world extensions, we can mitigate the ReDoS
issue by using it before we use the first pruning technique.
5.3.1 Approximation by Backreferences. We introduce our first pruning technique for extraction
approximation-by-backreferences. Given a template 𝑡 and a set of positive examples E + , the overapproximation checks whether there exists a completion 𝑟 ′ of 𝑡, i.e., a regex obtained from 𝑡 byreplacing the holes in 𝑡 with some regex, such that for each capturing group that appears in thetemplate 𝑡, 𝑟 ′ correctly extracts substrings from the positive examples. For this, it constructs aregex 𝑟 from the template 𝑡 and input strings 𝑤𝑒 from each positive example 𝑒 ∈ E + such that∀𝑒 ∈ E + . ((∃𝑟 ′ ∈ R (𝑡). (𝑒 ∈ L𝑐 (𝑟 ′ )) ⇒ 𝑤𝑒 ∈ L (𝑟 )), where R (𝑡) is the set of valid completions.
We first show the construction for the input string. The idea of the construction is to append
the information of substrings to be extracted by the 𝑖th capturing group with the delimiter #𝑖 . The
information consists of a string of the positive example and two delimiters @. We represent a
position of a substring to be extracted by surrounding the substring with the delimiters @, e.g., thestring 𝑎@𝑎@𝑏 means that the second 𝑎 should be extracted from the string 𝑎𝑎𝑏. Formally, given a
template 𝑡 and a positive example 𝑒 = (𝑤 ′, Γ), let 𝐼 = {𝑖 1, 𝑖 2, · · · , 𝑖𝑛 } be the set of indexes of capturinggroups in 𝑡, then we construct an input string 𝑤 as follow: 𝑤 = @𝑤 ′ #1𝑤𝑖 1 #2𝑤𝑖 2 # · · · #𝑛𝑤𝑖𝑛 , where,
for 𝑗 ∈ [𝑛], # 𝑗 , @ ∉ Σ and, for 𝑖 ∈ 𝐼 , 𝑤𝑖 = 𝑤 ′ [0..𝑝𝑙 )@𝑤 ′ [𝑝𝑙 ..𝑝𝑟 )@𝑤 ′ [𝑝𝑟 ..|𝑤 ′ |) with Γ(𝑖) = (𝑝𝑙 , 𝑝𝑟 ) if𝑖 ∈ 𝑑𝑜𝑚(Γ), and otherwise 𝑤𝑖 = 𝜖. That is, for the case of 𝑖 ∈ 𝐼 and 𝑖 ∈ 𝑑𝑜𝑚(Γ), 𝑤𝑖 means that thesubstring 𝑤 ′ [𝑝𝑙 ..𝑝𝑟 ) between the delimiters @ should be extracted by the 𝑖th capturing group, andthe prefix 𝑤 ′ [0..𝑝𝑙 ) and the suffix 𝑤 ′ [𝑝𝑟 ..|𝑤 ′ |) are used to indicate the position of 𝑤 [𝑝𝑙 ..𝑝𝑟 ). For
the case of 𝑖 ∉ 𝑑𝑜𝑚(Γ), 𝑤𝑖 means that the 𝑖th capturing group does not extract any substring. The
first character @ is prepended to handle the delimiters @ in the regex. For example, consider a setof positive examples E + = {𝑎LM2𝑑 }. For the positive example 𝑎LM2𝑑 = (𝑎𝑑, {(2, (1, 1))}), the input
string is @𝑤 ′ #1𝑤 1 #2𝑤 2 = @𝑎𝑑#1 #2𝑎@@𝑑. Here, 𝑤 1 = 𝜖 indicates that the 1st capturing group does
not extract any substring and 𝑤 2 = 𝑎@@𝑑 indicates that the 2nd capturing group extracts theempty string 𝜖.
Next, we show the construction of the regex. To verify the correctness of extraction, we construct
two types of expressions: 𝑟 assert1,𝐼 and 𝑟 assert2,𝐼 , where 𝐼 is a set of indexes of capturing groups. The
expressions 𝑟 assert1,𝐼 and 𝑟 assert2,𝐼 are used for verifying the correctness of extraction at the end of
the whole matching and positive lookarounds, respectively. First, the expression 𝑟 assert1,𝐼 is defined
as follows.
• For 𝐼 = {𝑖 1, 𝑖 2, · · · , 𝑖𝑛 }, 𝑟 assert1,𝐼 = 𝑟 assert1,𝑖 1 𝑟 assert1,𝑖 2 · · · 𝑟 assert1,𝑖𝑛 , where• for 𝑗 ∈ [𝑛], 𝑟 assert1,𝑖 𝑗 = # 𝑗 \prefix𝑖 𝑗 \flag𝑖 𝑗 \𝑖 𝑗 \flag𝑖 𝑗 \suffix𝑖 𝑗
In the above definition, we use a string as an index of capturing groups instead of integers forreadability. For 𝑖 𝑗 ∈ 𝐼 with 𝑗 ∈ [𝑛], the expression 𝑟 assert1,𝑖 𝑗 checks whether the extracted substringby the 𝑖 𝑗 th capturing group is correct, i.e., the expression 𝑟 assert1,𝑖 𝑗 tries to match the substring
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:17# 𝑗 𝑤𝑖 𝑗 of the input string constructed above. From this, if 𝑤𝑖 𝑗 is of form 𝑤 𝑝′ @𝑤𝑖′𝑗 @𝑤𝑠′ , then thebackreferences \prefix𝑖 𝑗 and \suffix𝑖 𝑗 try to match 𝑤 𝑝′ and 𝑤𝑠′ , respectively, the backreferences\flag𝑖 𝑗 try to match the delimiter @, and the backreference \𝑖 𝑗 tries to match 𝑤𝑖′𝑗 . Otherwise, i.e.,
𝑤𝑖 𝑗 = 𝜖, the expression tries to match the empty string 𝜖. Note that if a backreference is unassigned,then it is handled as the empty string 𝜖. As a result, if the matching succeeds, then it means thatthe 𝑖 𝑗 th capturing group extracts the correct substring in the correct position. Additionally, weneed to check the correctness of extraction in positive lookarounds because once we move outsideof positive lookarounds, then we cannot backtrack to the inside of the positive lookarounds, andtherefore, we cannot check the correctness of extraction in positive lookarounds by the expression
𝑟 assert1,𝐼 . From this, before we move outside of positive lookarounds, we check whether the extracted
substrings in the positive lookarounds are correct or not by using the expression 𝑟 assert2,𝐼 .
The expression 𝑟 assert2,𝐼 is defined as follows.
• For 𝐼 = {𝑖 1, 𝑖 2, · · · , 𝑖𝑛 } 𝑟 assert2,𝐼 = 𝑟 assert2,𝑖 1 𝑟 assert2,𝑖 2 · · · 𝑟 assert2,𝑖𝑛 , where• for 𝑗 ∈ [𝑛], 𝑟 assert2,𝑖 𝑗 = (?=[Σ ∪ {#1, #2, · · · , # 𝑗 −1, # 𝑗+1, · · · #𝑛 }] ∗ # 𝑗 𝑟 assert1,𝑖 𝑗 ).
Basically, the expression 𝑟 assert2,𝐼 behaves like the expression 𝑟 assert1,𝐼 , but the subexpressions 𝑟 assert2,𝑖is nested by a positive lookahead to change the direction of the matching to forward. Additionally,
for 𝑖 𝑗 ∈ 𝐼 , we add the Kleene star to move the position to the expression # 𝑗 𝑟 assert1,𝑖 𝑗 for checking thecorrectness of extraction of the 𝑖 𝑗 th capturing group.
With them, we construct a regex for the approximation-by-backreferences as follows. For a template 𝑡, we use 𝐼𝑡 to denote the set of indexes of capturing groups that appear in 𝑡. Given a template𝑡, we construct a regex 𝑟 = @𝑟 body𝑟 assert1,𝐼𝑡 , where 𝑟 body is calculated as follows. First, we construct
the over-approximated regex 𝑟 ⊤ by the over-approximation for membership (cf. Appendix D). Then,
we construct 𝑟 body by embedding expressions to check the correctness of extraction into the regex𝑟 ⊤ by using the function 𝛽, i.e., 𝑟 body = 𝛽 (𝑟 ⊤ ). The definition of the function 𝛽 is as follows.
𝛽 ([𝐶](resp. 𝜖))𝛽 (𝑡 1𝑡 2 )𝛽 (𝑡 1 |𝑡 2 )===[𝐶](resp. 𝜖)𝛽 (𝑡 1∗ ) = 𝛽 (𝑡 1 ) ∗𝛽 ((?<!𝑡 1 )) =𝛽 (𝑡 1 )𝛽 (𝑡 2 )𝛽 (𝑡 1∗? ) = 𝛽 (𝑡 1 ) ∗?
𝛽 ((?=𝑡 1 )) =𝛽 (𝑡 1 )|𝛽 (𝑡 2 ) 𝛽 ((?!𝑡 1 )) = (?!𝛽 (𝑡 1 )) 𝛽 ((?<=𝑡 1 )) =𝛽 ((𝑡 1 )𝑖 ) = (?<=(@)flag𝑖 (.∗ )prefix𝑖 )(𝛽 (𝑡 1 ))𝑖 (?=(.∗ )suffix𝑖 )(?<!𝛽 (𝑡 1 ))(?=𝛽 (𝑡 1 )𝑟 assert2,𝐼𝑡1 )(?<=𝑟 assert2,𝐼𝑡1 𝛽 (𝑡 1 ))Note that backreferences are eliminated by the approximation for membership. The function 𝛽
inserts the expression 𝑟 assert2,𝐼𝑡1 into positive lookarounds to verify the correctness of the extraction
before the matching moves outside of the positive lookarounds. The main part of the construction
by 𝛽 is the case of capturing groups. In that case, it inserts the positive lookbehind and the positive
lookahead before and after the 𝑖th capturing group, respectively. The positive lookbehind extracts
the delimiter @ with the index flag𝑖 and the substring from the beginning of the input string to
the position before starting the 𝑖th capturing group with the index prefix𝑖 . The positive lookahead
extracts the substring from the position after ending the 𝑖th capturing group to the end of the input
string with the index suffix𝑖 .
As a result, IsFeasible at Line 4 computes the regex 𝑟 and the input string 𝑤𝑒 for each example
𝑒 ∈ E + by the procedures described above, and checks whether 𝑤𝑒 ∈ L (𝑟 ) for each 𝑒 ∈ E + . If so,there may exist a completion and therefore R3 expands the holes in the template. Otherwise, R3
does not expand the holes. As an example of the approximation, consider a template 𝑡 = □|(𝑏)1 anda set of positive examples E + = {L𝑏M1, 𝑎}. Then, the regex obtained by the over-approximation formembership is 𝑟 ⊤ = .∗ |(𝑏)1 , i.e., the hole □ is replaced with .∗ , and the regex 𝑟 obtained by applying
the function 𝛽 to 𝑟 ⊤ and attaching @ and 𝑟 assert1,𝐼𝑡 before and after it is as follows.
𝑟=@(.∗ |(?<=(@)flag1 (.∗ )prefix1 ) (𝑏)1 (?=(.∗ )suffix1 ))#1 \prefix1 \flag1 \1\flag1 \suffix1 .
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:18

Nariyoshi Chida and Tachio Terauchi

For the positive examples L𝑏M1 and 𝑎, the input strings are 𝑤 1 = @𝑏#1 @𝑏@ and 𝑤 2 = @𝑎#1 . Recall
that unassigned backreferences in the JavaScript semantics are handled as the empty string 𝜖. From
this, in the matching of 𝑟 on 𝑤 2 , the backreferences in 𝑟 are evaluated as the empty string 𝜖.
Finally, the regex and the input strings obtained by the above construction satisfy the following
property.
Proposition 5.1. Given a template 𝑡 and a set of positive examples E + , let 𝑟 and 𝑤𝑒 for each𝑒 ∈ E + be the regex and the input strings obtained by the above construction. Then, ∀𝑒 ∈ E + . ((∃𝑟 ′ ∈R (𝑡). (𝑒 ∈ L𝑐 (𝑟 ′ )) ⇒ 𝑤𝑒 ∈ L (𝑟 )).
We use a variant of the approximation-by-backreferences at Line 5 of Algorithm 1. The variant
uses . instead of .∗ when we apply the approximation for membership.
5.3.2 Approximation by Pure Regex. Next, we introduce our second pruning technique approximationby-pure-regex. At a high level, the idea is the same as our first pruning technique, i.e., we convert atemplate and a positive example to a regex and an input string, respectively, to have the informationof substrings to be extracted. However, the second pruning technique takes a different approachto the conversion. The conversion used in the second pruning technique eliminates real-worldextensions in a template by approximating them to obtain a pure regex. From this, we can use
nonbacktracking regex engines, i.e., automata-based regex engines such as Google RE2 [Google[n. d.]] which are known as ReDoS-free regex engines [Cox 2007], for membership. Note that theregex-engine-dependent behavior does not affect results of the matching in terms of membershipand there is no automata-based regex engine that fully supports real-world extensions such as
backreferences and lookarounds11 (and therefore we cannot use automata-based regex engines forthe first pruning technique).
We first describe the conversion from a positive example to an input string. Let 𝑒 = (𝑤, Γ) be apositive example and 𝐼 be the set of indexes of capturing groups that appear in the template. Then,for each index 𝑖 ∈ 𝑑𝑜𝑚(Γ) ∩ 𝐼 , we insert the delimiters #𝑖 in the position described by Γ(𝑖), i.e., wesimply replace L𝑖 and M𝑖 with #𝑖 . For example, we convert the positive example L1 L2𝑎M2𝑏M1𝑐 to the
input string #1 #2𝑎#2𝑏#1𝑐. The delimiters indicate the positions of substrings to be extracted.
Next, we consider the conversion from a template to a pure regex. Before we describe the detailsof the conversion, we first explain the procedure to eliminate backreferences by approximating
them, which is also used in the approximation for membership. For eliminating backreferences,
we first replace backreferences \𝑖 that are always evaluated as unassigned backreferences andthose that can be evaluated as both assigned and unassigned references with the empty string
𝜖 and (\𝑖 |𝜖), respectively. For example, we convert the template ((\2□)1 (\1𝑏)2 ) ∗ to the template((𝜖□)1 (\1𝑏)2 ) ∗ because the Kleene-star operator in JavaScript resets substrings extracted in the
Kleene-star operator for each iteration (cf. Section 3), and therefore the backreference \2 is always
evaluated as an unassigned reference. Additionally, for example, we convert the template ((□)1 |𝑎)\1
to the template ((□)1 |𝑎) (\1|𝜖) because the backreference \1 may refer to the expression of the 1st
capturing group (i.e., □) or it may be an unassigned reference (i.e., 𝜖). By the replacements, therelations between backreferences and the corresponding capturing groups form a directed acyclic
graph (DAG). Therefore, we eliminate backreferences by approximating them in a topologicalorder starting from the backreference whose corresponding capturing group does not have abackreference. For this, for backreferences \𝑖 and the corresponding capturing groups (𝑡)𝑖 , wereplace \𝑖 with 𝑡 ′ where 𝑡 ′ is an expression obtained by removing capturing groups in 𝑡. For
11 Actually, automata models that are equivalent to regexes with real-world extensions are unknown even for regexes withbackreferences and (positive and negative) lookaheads [Chida and Terauchi 2022a].

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:19example, we convert the template (□)1 (\1𝑎)2 \2 to the template (□)1 (□𝑎)2 □𝑎, and the template(?=((□)2 \2)1 )\1 to the template (?=((□)2 □)1 )□□.
Now, we describe the conversion. The conversion first eliminates the real-world extensions to
obtain a pure template regex. That is, it eliminates backreferences by approximation described above,
then eliminates lookarounds by simply replacing them with the empty string 𝜖, and eliminates
capturing groups by replacing them with expressions with delimiters. We describe the eliminationof capturing groups. Since nested structures of capturing groups also form a DAG, we replace
capturing groups in a topological order starting from the capturing group that does not have acapturing group in the expression. Specifically, let 𝑡 be a template that does not have a capturinggroup as a subexpression. We replace a capturing group (𝑡)𝑖 that is (resp. not) in the Kleene-star
operator with the expression (#𝑖 𝑡#𝑖 |𝑡) (resp. #𝑖 𝑡#𝑖 ). We replace capturing groups that are in the
Kleene-star operator with the form of the union operator because the capturing groups only
extract a substring at the last iteration. For example, we convert the template (𝑎)1∗ to the template(#1𝑎#1 |𝑎) ∗ . We perform this procedure repeatedly until all capturing groups are eliminated. Finally,
the conversion uses the over-approximation for membership to obtain a pure regex from a pureregex template. As a result, for a template 𝑡 and positive examples 𝑒 ∈ E + , IsFeasible at Line 4
constructs a pure regex 𝑟 and an input string 𝑤 from 𝑡 and 𝑒 by the above procedure, respectively,
and checks whether 𝑤 ∈ L (𝑟 ). If there exists an input string 𝑤 such that 𝑤 ∉ L (𝑟 ), then we do
not expand the holes.
6

EVALUATION

We implemented our algorithm as a tool called R3 in Java with Z3 [De Moura and Bjørner 2008] as
the SMT solver. We conducted an experimental evaluation that is designed to answer the following
research questions: (RQ1) Can R3 repair a regex effectively? (RQ2) Can R3 find a high-quality
regex? (RQ3) Are the new pruning techniques useful for repairing a regex for extraction? To answer(RQ1), we measured the running time of R3 using instances described in Section 6.1. To answer(RQ2), we measured the quality of the repair based on the metrics introduced in the previous
works [Chida and Terauchi 2022b; Pan et al. 2019]. Finally, to answer (RQ3), we compared theperformance of R3 with and without our pruning techniques. In what follows, we refer to R3
without the new pruning techniques as R3base , and use R3hybrid to denote the hybrid of R3 and R3basethat returns the regex returned by the faster of the two. The experiments were run on a machinewith Intel(R) Xeon(R) Platinum 8360Y CPU @ 2.40GHz with the time limit of 30 minutes. In thisevaluation, we only consider ASCII symbols, i.e., we only use regexes over the ASCII alphabet.
Validation. Our repair algorithm guarantees to generate only correct regexes, i.e., they are consistent with all examples. We have validated that all regexes generated by R3 in this evaluation areindeed consistent with all examples by running JavaScript’s regex engines.
6.1

Data Set

There is no standard benchmark for repairing regexes for extraction. Therefore, to conduct ourexperiments, we prepared a data set collected from public GitHub projects.
GitHub data set. We collected incorrect and correct regexes for extraction from regex-related
commits of public GitHub projects. Specifically, we looked for commits that contain a change that
repairs regexes for extraction, and if so, collected the regexes before and after the repair as theincorrect and correct regexes, respectively. When such commits provide examples of correct andincorrect usage, we use them as examples for our repair methods. For commits that do not provide
examples, we prepared the examples based on the correct and incorrect regexes manually. The
examples were prepared by inspecting the differences between before and after the change of theProc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:20

Nariyoshi Chida and Tachio Terauchi(a) Running times.

(b) Distances.

(c) Percentages of changes.

Fig. 3. Histograms of the results of R3.

regexes in the commits. We prepared at least 10 positive and negative examples, respectively, foreach commit. From these examples, we use at most 5 positive and 5 negative examples for each
instance to be used for our repair algorithms. Note that, for usability, PBE methods should find asolution from a small number of examples. The remaining examples are used as left-out example
sets for evaluating the quality of repaired regexes (cf. RQ2: Quality).
We took two approaches to find the commits. First, we checked all commits in the list collectedby Wang et al. [2020] who studied real-world bugs of regexes in Apache, Mozilla, Facebook, andGoogle GitHub projects. As a result, we obtained 23 regexes. Second, inspired by the approach of
Wang et al. [2020] who searched regex-related commits, we used GitHub Advanced Search withkeywords such as “regular expression”, “regex”, and “regexp” with the keyword “bug”. We checked
the commits in the order of keyword relevance until we obtained 27 regexes, ignoring duplicates.
Consequently, we collected 50 regexes. The average and maximum sizes of the regexes (measured
as the number of AST nodes) are 38.8 and 199, respectively. Additionally, the average and maximum
numbers of capturing groups are 1.9 and 13, respectively. Finally, 24 (resp. 5) regexes have a (resp.
lazy) Kleene star, 32 (resp. 2) regexes have a (resp. lazy) Kleene plus, 9 regexes have a union operator,
17 regexes have an optional operator, 1 regex has a positive lookahead, and 1 regex has a positive
lookbehind.
Table 1. Solved instances.
RQ1: Efficiency. Table 1 reports the resultsof the number of solved instances within the
instances running time (seconds)
time limit (Solved) and the minimum, median,
Solved (50) min med
max
and maximum running times in seconds (min,R3
39 (78%)0.1
1.7
1011.7
med, and max, respectively). Additionally, weR3base36 (72%)
0.1
3.2
536.0
plot the number of regexes against the run40 (80%)
0.1
1.8
1011.7R3hybridning times. Figure 3a shows the histogram. The
times in the histogram are grouped every 2 minutes. As the table shows, R3 repaired 39 instances(78%) within the time limit. We inspected the unsolved instances, and found that R3 could not
repair the instances that (i) require large changes from the original and (ii) involve highly-nested
Kleene stars which burden the constraint generation process. These findings agree with the existing
works that are based on the enumerative search algorithms with SMT constraint solving [Chida
and Terauchi 2022b; Pan et al. 2019]. For example, R3 could not find the repair of the regex.∗ (mochitest(-debug|-e10s|-devtools-chrome)?|reftest|· · · |jittest)([0-9]+ )1 within
the time limit. The intended solution is .∗ -([0-9]+ )1 $, which is of a large distance from theoriginal. As the plot shows, majority of the instances (74.3%) can be repaired within 5 seconds. In
summary, R3 can repair a real-world regex efficiently.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:21

RQ2: Quality. As mentioned by Pan et al. [2019], repairsthat are similar to the original ones are often considered goodin PBE because they are similar to what the user intended,and the prior PBE works [Chida and Terauchi 2022b; Pan et al.
2019] used the edit distance between from the original as a
metric of repair quality. A large change indicates low quality
as such repairs may be far from what the user intended. As
Figure 3b shows, all repaired regexes were repaired within
the distance 10. Figure 3c shows the percentages of changes
from the original. As the figure shows, we observe that mostFig. 4. F1 scores.
repairs are close to the original regexes with the average
ratio of change being 5.8%, and about 87.2% of regexes were
repaired within 10% of changes.
Additionally, following the approach used by Pan et al. [2019], we also measured the quality ofrepaired regexes with respect to left-out example sets. That is, by using the examples not used in
the repair algorithms, we measured the F1 score. The F1 score is defined as follows: for the repaired
regex 𝑟 , we estimate the precision of 𝑟 by 𝑇 𝑃/(𝑇 𝑃 + 𝐹 𝑃) where 𝑇 𝑃 (resp. 𝐹 𝑃) is the number of
positive (resp. negative) examples that are correctly (resp. incorrectly) classified by 𝑟 . Additionally,
we estimate the recall of 𝑟 by 𝑇 𝑃/(𝑇 𝑃 + 𝐹 𝑁 ) where 𝐹 𝑁 is the number of positive examples that areincorrectly classified by 𝑟 . Then, the F1 score of 𝑟 is defined as (2 × recall × precision)/(recall +precision). The F1 score is between 0 and 1, and the high F1 score implies the high quality of therepaired regex. Figure 4 shows the histogram. As the figure shows, more than 87.5% of the repaired
regexes have the F1 scores of at least 0.8. We inspected the repaired regexes with low F1 scores, andfound that R3 could not find a repair with a high F1 score when the repair requires large changes
from the original. In summary, R3 can produce regexes that have high-similarity and generalize wellto left-out example sets, and therefore of high-quality.
RQ3: Impact of Over-Approximation for Extraction. To understand the impact of our new pruning techniques, we compared R3 against R3base . Figure 5 plots their running times.
The points above the diagonal means that R3 is faster thanR3base . The points on the border (colored in blue) indicate thatthe tool could not find a repair within the timeout. As theplot shows, R3 is faster than R3base in 24 instances, and R3 isslower than R3base in 16 instances. However, in 12 instancesof the 16 instances, the difference of the running times between R3 and R3base were within 0.2 seconds, whereas such Fig. 5. Effect of the pruning techniques.
is true for only 2 of the former 24 instances. We inspected
the 4 instances on which R3base was non-trivially faster, and found that, in these cases, R3 was
suffering from ReDoS (cf. Section 5.3). A possible way to address the issue is to simply set a time
limit on the approximation process. Additionally, in 4 instances, R3 solved the instance within thetimeout while R3base could not. R3 achieved 21.9× speedups on average and more than 445.9× inthe largest case. In summary, the new pruning techniques significantly improve the running times.
7

RELATED WORK

Synthesizing regexes for membership. There is much work on synthesizing or repairing a regex
from examples [Angluin 1978; Brādzma 1993; Fernau 2009; Rebele et al. 2018]. Our work is mostclosely related to the recent works on synthesizing or repairing a regex from examples [Chida andProc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:22

Nariyoshi Chida and Tachio Terauchi

Terauchi 2022b; Lee et al. 2016; Li et al. 2020; Pan et al. 2019] or from examples and natural language
descriptions [Chen et al. 2020; Li et al. 2021]. However, all these works only support for membership,
and the support for extraction is out of scope. As shown in our paper, supporting extraction requiresconsidering deterministic semantics which incurs non-trivial extensions to the prior methods that
only considered membership. Additionally, all except for Chida and Terauchi [2022b] only support
pure regexes and do not consider real-world extensions such as lookarounds and backreference.
Chida and Terauchi [2022b] support backreferences and some forms of lookarounds but not general
lookbehinds, and as remarked above, they do not consider extraction and use a non-deterministic
semantics.
Generating regexes by genetic algorithms. Bartoli et al. [2014, 2016] introduced a geneticprogramming based algorithm for generating a regex for extraction from examples. However, as
mentioned in Section 1, they do not guarantee the correctness of the repair. Additionally, theextraction considered in their work is different from ours. That is, our work considers extraction frommatching a regex against the whole given string and extracting the (positions of) substrings capturedby the capturing groups in the regex, whereas their work considers extracting the substrings of thegiven string that each matches a regex without capturing groups.
Formal semantics of regexes. Our paper’s novel formal semantics of regexes follows the ECMAScript 2023 language specification, and while its purpose in this paper is to be used as a basis fora repair algorithm, it may be of independent interest. Our semantics is inspired by those in the previous works [Chida and Terauchi 2022b; Sakuma et al. 2012]. Namely, Chida and Terauchi [2022b]
give a big-step semantics for regexes including some real-world extensions, and Sakuma et al.
[2012] give a deterministic semantics of Perl regexes using continuations and monads. However,as remarked above, the semantics of Chida and Terauchi [2022b] is non-deterministic and hence
is unsuitable to describe extraction, and that of Sakuma et al. [2012] only considers pure regexes
and does not consider real-world extensions. Other prior works on formal semantics of regexes
include the work by Loring et al. [2019] who provide a semantics that follows the ECMAScript2015 language specification. However, their goal is dynamic symbolic execution that involves
counterexample-guided refinement, and adopting their semantics to a PBE repair problem may bedifficult. Furthermore, they do not support lookbehinds. Finally, Chen et al. [2022] give a semantics
of JavaScript’s regexes by using prioritized streaming string transducers. However, they do notconsider extensions such as backreferences and lookarounds.
8

CONCLUSION

We have presented the first PBE-based method for repairing regexes for extraction. Our method
supports real-world extensions such as general lookarounds and backreferences, and we have shownthat the extensions are important for the existence of a solution to the repair problem, and that the
repair problem is NP-hard. Our algorithm for solving the repair problem makes two significant
extensions to the prior methods that only considered membership: handling of deterministic
behavior and the new pruning techniques to reduce the search space. To realize the former, we havealso presented a novel formal semantics that the ECMAScript 2023 language specification. We have
implemented the algorithm as a tool called R3 and experimentally evaluated it on a real-world data
set. The evaluation has shown that R3 can repair real-world regexes successfully and efficiently.
ACKNOWLEDGMENTS
We thank anonymous reviewers for useful comments. This work was supported by JSPS KAKENHI
Grant Numbers JP17H01720, JP18K19787, JP20H04162, JP20K20625, and JP22H03570.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:23

REFERENCES
Dana Angluin. 1978. On the complexity of minimum inference of regular sets. Information and Control 39, 3 (1978), 337–350.
https://doi.org/10.1016/S0019-9958(78)90683-6
Angular. 2022. Angular: The modern web developer’s platform. https://angular.io/ [Online; accessed 10-November-2022].
A. Bartoli, G. Davanzo, A. De Lorenzo, E. Medvet, and E. Sorio. 2014. Automatic Synthesis of Regular Expressions from
Examples. Computer 47, 12 (dec 2014), 72–80. https://doi.org/10.1109/MC.2014.344
Alberto Bartoli, Andrea De Lorenzo, Eric Medvet, and Fabiano Tarlao. 2016. Inference of Regular Expressions for Text
Extraction from Examples. IEEE Transactions on Knowledge and Data Engineering 28, 5 (2016), 1217–1230. https://doi.org/10.1109/TKDE.2016.2515587
Martin Berglund and Brink van der Merwe. 2017. Regular Expressions with Backreferences Re-examined. In Proceedingsof the Prague Stringology Conference 2017, Prague, Czech Republic, August 28-30, 2017, Jan Holub and Jan Zdárek (Eds.).
Department of Theoretical Computer Science, Faculty of Information Technology, Czech Technical University in Prague,
30–41. http://www.stringology.org/event/2017/p04.html
Alvis Brādzma. 1993. Efficient Identification of Regular Expressions from Representative Examples. In Proceedings of the
Sixth Annual Conference on Computational Learning Theory (Santa Cruz, California, USA) (COLT ’93). Association for
Computing Machinery, New York, NY, USA, 236–242. https://doi.org/10.1145/168304.168340
Qiaochu Chen, Xinyu Wang, Xi Ye, Greg Durrett, and Isil Dillig. 2020. Multi-Modal Synthesis of Regular Expressions. In
Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (London, UK) (PLDI2020). Association for Computing Machinery, New York, NY, USA, 487–502. https://doi.org/10.1145/3385412.3385988
Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony W. Lin, Philipp
Rümmer, and Zhilin Wu. 2022. Solving String Constraints with Regex-Dependent Functions through Transducers with
Priorities and Variables. Proc. ACM Program. Lang. 6, POPL, Article 45 (jan 2022), 31 pages. https://doi.org/10.1145/3498707
Nariyoshi Chida and Tachio Terauchi. 2022a. On Lookaheads in Regular Expressions with Backreferences. In 7th International
Conference on Formal Structures for Computation and Deduction (FSCD 2022) (Leibniz International Proceedings in Informatics(LIPIcs), Vol. 228), Amy P. Felty (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 15:1–15:18.
https://doi.org/10.4230/LIPIcs.FSCD.2022.15
Nariyoshi Chida and Tachio Terauchi. 2022b. Repairing DoS Vulnerability of Real-World Regexes. In 2022 IEEE Symposium
on Security and Privacy (SP). 2060–2077. https://doi.org/10.1109/SP46214.2022.9833597
Russ Cox. 2007. Regular Expression Matching Can Be Simple And Fast (but is slow in Java, Perl, PHP, Python, Ruby, ...).
https://swtch.com/~rsc/regexp/regexp1.html [Online; accessed 10-November-2022].
James C. Davis, Christy A. Coghlan, Francisco Servant, and Dongyoon Lee. 2018. The Impact of Regular Expression
Denial of Service (ReDoS) in Practice: An Empirical Study at the Ecosystem Scale. In Proceedings of the 2018 26th ACM
Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering(Lake Buena Vista, FL, USA) (ESEC/FSE 2018). Association for Computing Machinery, New York, NY, USA, 246–256.
https://doi.org/10.1145/3236024.3236027
James C. Davis, Louis G. Michael IV, Christy A. Coghlan, Francisco Servant, and Dongyoon Lee. 2019. Why Aren’t Regular
Expressions a Lingua Franca? An Empirical Study on the Re-Use and Portability of Regular Expressions. In Proceedingsof the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations ofSoftware Engineering (Tallinn, Estonia) (ESEC/FSE 2019). Association for Computing Machinery, New York, NY, USA,
443–454. https://doi.org/10.1145/3338906.3338909
Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the Theory and Practice ofSoftware, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Budapest,
Hungary) (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340.
Django. 2022. Django: The Web framework for perfectionists with deadlines. https://www.djangoproject.com/ [Online;
accessed 10-November-2022].
ECMA International. 2022. ECMAScript® 2023 Language Specification. https://tc39.es/ecma262/multipage/#sec-intro.
Henning Fernau. 2009. Algorithms for learning regular expressions from positive data. Information and Computation 207, 4(2009), 521–541. https://doi.org/10.1016/j.ic.2008.12.008
Margarida Ferreira, Miguel Terra-Neves, Miguel Ventura, Inês Lynce, and Ruben Martins. 2021. FOREST: An Interactive
Multi-tree Synthesizer for Regular Expressions. In Tools and Algorithms for the Construction and Analysis of Systems,
Jan Friso Groote and Kim Guldstrand Larsen (Eds.). Springer International Publishing, Cham, 152–169.
Jeffrey E. F. Friedl. 2006. Mastering Regular Expressions (3 ed.). O’Reilly, Beijing. https://www.safaribooksonline.com/
library/view/mastering-regular-expressions/0596528124/
Alain Frisch and Luca Cardelli. 2004. Greedy Regular Expression Matching. In Automata, Languages and Programming,
Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg,
618–629.
Google. [n. d.]. RE2. https://github.com/google/re2 [Online; accessed 10-November-2022].

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:24

Nariyoshi Chida and Tachio Terauchi

Richard M. Karp. 1972. Reducibility among Combinatorial Problems. Springer US, Boston, MA, 85–103. https://doi.org/10.
1007/978-1-4684-2001-2_9
Mina Lee, Sunbeom So, and Hakjoo Oh. 2016. Synthesizing Regular Expressions from Examples for Introductory Automata
Assignments. SIGPLAN Not. 52, 3 (oct 2016), 70–80. https://doi.org/10.1145/3093335.2993244
Yunyao Li, Rajasekar Krishnamurthy, Sriram Raghavan, Shivakumar Vaithyanathan, and H. V. Jagadish. 2008. Regular
Expression Learning for Information Extraction. In Proceedings of the 2008 Conference on Empirical Methods in Natural
Language Processing. Association for Computational Linguistics, Honolulu, Hawaii, 21–30. https://aclanthology.org/D081003
Yeting Li, Shuaimin Li, Zhiwu Xu, Jialun Cao, Zixuan Chen, Yun Hu, Haiming Chen, and Shing-Chi Cheung. 2021. TransRegex:
Multi-Modal Regular Expression Synthesis by Generate-and-Repair. In Proceedings of the 43rd International Conference on
Software Engineering (Madrid, Spain) (ICSE ’21). IEEE Press, 1210–1222. https://doi.org/10.1109/ICSE43902.2021.00111
Yeting Li, Zhiwu Xu, Jialun Cao, Haiming Chen, Tingjian Ge, Shing-Chi Cheung, and Haoren Zhao. 2020. FlashRegex:
Deducing Anti-ReDoS Regexes from Examples. In Proceedings of the 35th IEEE/ACM International Conference on AutomatedSoftware Engineering (Virtual Event, Australia) (ASE ’20). Association for Computing Machinery, New York, NY, USA,
659–671. https://doi.org/10.1145/3324884.3416556
Blake Loring, Duncan Mitchell, and Johannes Kinder. 2019. Sound Regular Expression Semantics for Dynamic Symbolic
Execution of JavaScript. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and
Implementation (Phoenix, AZ, USA) (PLDI 2019). Association for Computing Machinery, New York, NY, USA, 425–438.
https://doi.org/10.1145/3314221.3314645
Matthew Luckie, Bradley Huffaker, and k claffy. 2019. Learning Regexes to Extract Router Names from Hostnames. In
Proceedings of the Internet Measurement Conference (Amsterdam, Netherlands) (IMC ’19). Association for Computing
Machinery, New York, NY, USA, 337–350. https://doi.org/10.1145/3355369.3355589
Louis G. Michael, James Donohue, James C. Davis, Dongyoon Lee, and Francisco Servant. 2019. Regexes Are Hard:
Decision-Making, Difficulties, and Risks in Programming Regular Expressions. In Proceedings of the 34th IEEE/ACM
International Conference on Automated Software Engineering (San Diego, California) (ASE ’19). IEEE Press, 415–426.
https://doi.org/10.1109/ASE.2019.00047
Chris O’Hara. 2022. Validator.js. https://github.com/validatorjs/validator.js/ [Online; accessed 10-November-2022].
OWASP. 2022. Input Validation Cheat Sheet. https://cheatsheetseries.owasp.org/cheatsheets/Input_Validation_Cheat_
Sheet.html [Online; accessed 10-November-2022].
Rong Pan, Qinheping Hu, Gaowei Xu, and Loris D’Antoni. 2019. Automatic Repair of Regular Expressions. Proc. ACM
Program. Lang. 3, OOPSLA, Article 139 (oct 2019), 29 pages. https://doi.org/10.1145/3360565
Thomas Rebele, Katerina Tzompanaki, and Fabian M. Suchanek. 2018. Adding Missing Words to Regular Expressions. In
Advances in Knowledge Discovery and Data Mining, Dinh Phung, Vincent S. Tseng, Geoffrey I. Webb, Bao Ho, Mohadeseh
Ganji, and Lida Rashidi (Eds.). Springer International Publishing, Cham, 67–79.
RegExLib. 2022. https://regexlib.com/ [Online; accessed 10-November-2022].
Yuto Sakuma, Yasuhiko Minamide, and Andrei Voronkov. 2012. Translating regular expression matching into transducers.
Journal of Applied Logic 10, 1 (2012), 32–51. https://doi.org/10.1016/j.jal.2011.11.003 Special issue on AutomatedSpecification and Verification of Web Systems.
Amazon Web Services. 2022. Regex match rule statement. https://docs.aws.amazon.com/waf/latest/developerguide/wafrule-statement-type-regex-match.html [Online; accessed 10-November-2022].
Snort. 2022. Snort. https://www.snort.org/ [Online; accessed 10-November-2022].
Peipei Wang, Chris Brown, Jamie A. Jennings, and Kathryn T. Stolee. 2020. An Empirical Study on Regular Expression Bugs.
In Proceedings of the 17th International Conference on Mining Software Repositories (Seoul, Republic of Korea) (MSR ’20).
Association for Computing Machinery, New York, NY, USA, 103–113. https://doi.org/10.1145/3379597.3387464
Tianyi Zhang, London Lowmanstone, Xinyu Wang, and Elena L. Glassman. 2020. Interactive Program Synthesis by
Augmented Examples. In Proceedings of the 33rd Annual ACM Symposium on User Interface Software and Technology(Virtual Event, USA) (UIST ’20). Association for Computing Machinery, New York, NY, USA, 627–648. https://doi.org/10.
1145/3379337.3415900

A

PROOF OF THEOREM 4.3

Proof. For simplicity, we assume that Σ = {𝑎, 𝑏}. We show that the instance 𝑟 1 = 𝜖, E + ={(𝑎𝑏, Γ0 ), (𝑏𝑎, Γ1 )} where Γ0 = {(1, (0, 1))} (i.e., the first character 𝑎 should be extracted from 𝑎𝑏) andΓ1 = {(1, (1, 2))} (i.e., the second character 𝑎 should be extracted from 𝑏𝑎), and E − = {𝜖, 𝑎, 𝑏, 𝑎𝑎, 𝑏𝑏}(i.e., except for 𝑎𝑏 and 𝑏𝑎, the length of strings accepted by the solution should be greater thanor equal to 3) does not have a pure regex solution. Suppose for a contradiction that the instance
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:25Set of Characters and Empty String𝑑 = forward

𝑝 < |𝑤 |𝑤 [𝑝] ∈ 𝐶

𝑑 = backward

0 ≤𝑝 −1𝑤 [𝑝 − 1] ∈ 𝐶([𝐶], 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 − 1, Γ)( [𝐶], 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 + 1, Γ)(𝜖, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ)Concatenation𝑑 = forward(𝑟 1, 𝑟 2𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(𝑟 2, 𝑟𝑐 , 𝑤, 𝑝 1, Γ1, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 1𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )𝑑 = backward(𝑟 2, 𝑟𝑐 𝑟 1, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(𝑟 1, 𝑟𝑐 , 𝑤, 𝑝 1, Γ1, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 1𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )Union
𝑑 = forward(𝑟 1𝑟𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(¬𝑙 ∧ 𝑝 1 = |𝑤 |) ∨ 𝑙(𝑟 1, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 1 |𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )𝑑 = forward(𝑟 1𝑟𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ 𝜏(¬𝑙 ∧ (𝜏 = failed ∨ 𝜏 = (𝑝 ′′, Γ ′′ ) where 𝑝 ′′ ≠ |𝑤 |) ∨ (𝑙 ∧ 𝜏 = failed)(𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )𝑑 = backward(𝑟 1 |𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )(𝑟𝑐 𝑟 1, 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(¬𝑙 ∧ 𝑝 1 = |𝑤 |) ∨ 𝑙(𝑟 1, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 1 |𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )𝑑 = backward(𝑟𝑐 𝑟 1, 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ 𝜏(¬𝑙 ∧ (𝜏 = failed ∨ 𝜏 = (𝑝 ′′, Γ ′′ ) where 𝑝 ′′ ≠ |𝑤 |) ∨ (𝑙 ∧ 𝜏 = failed)(𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )(𝑟 1 |𝑟 2, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )Fig. 6. Rules for pure regexes (except for Kleene stars and repetitions).

has a pure regex solution. Let 𝑟 2 be the solution. Since 𝑟 2 is consistent with positive examples, it
has a capturing group (𝑟 𝑎 )1 where 𝑟 𝑎 matches to the character 𝑎, i.e., 𝑎 ∈ L (𝑟 𝑎 ). The capturinggroup (𝑟 𝑎 )1 does not appear in the Kleene-star operator. To prove this, suppose the capturing group
appears in the Kleene-star operator. Then, the Kleene-star operator can iterate exactly once because
if it iterates zero times, then the solution 𝑟 2 does not extract any substring, which is a contradiction.
In addition, if it iterates more than two times, for the string 𝑎𝑏, the substring extracted by thecapturing group is no longer the first character 𝑎, which is a contradiction, because the Kleene-star
operator consumes at least one character for each iteration. Therefore, the Kleene-star operator
iterates exactly once. However, in this case, we can obtain a regex 𝑟 3 that is consistent with examples
and 𝐷 (𝑟 1, 𝑟 3 ) < 𝐷 (𝑟 1, 𝑟 2 ) by replacing the Kleene-star operator 𝑟 ′∗ with the expression 𝑟 ′ which isa contradiction. Additionally, the capturing group does not appear in the union operator for thesimilar reason, i.e., for the union operator, we can obtain the smaller expression that is consistent
with examples by replacing the union operator with the subexpression that contains the capturinggroup. From this, the only operator in which the capturing group appears is the concatenation
operator. As a result, 𝑟 2 should take the form of 𝑟 ′ (𝑟 𝑎 )1𝑟 ′′ . Since 𝑟 2 is consistent with positive
examples, 𝑟 ′ and 𝑟 ′′ can match to the character 𝑏 and the empty string 𝜖, i.e., 𝜖, 𝑏 ∈ L (𝑟 ′ ) and𝜖, 𝑏 ∈ L (𝑟 ′′ ). However, if so, 𝑟 2 can match the string 𝑎 ∈ E − , which is a contradiction.
□
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:26

Nariyoshi Chida and Tachio Terauchi

Greedy Kleene Star𝑑 = forward(𝑟 ⟨𝑟 ∗ : 𝑝⟩𝑟𝑐 , 𝜖, 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(¬𝑙 ∧ 𝑝 1 = |𝑤 |) ∨ 𝑙(𝑟, ⟨𝑟 ∗ : 𝑝⟩𝑟𝑐 , 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 ∗, 𝑟𝑐 , 𝑤, 𝑝 2, Γ2, 𝑑, 𝑙) ⇓ (𝑝 3, Γ3 )(𝑟 ∗, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 3, Γ3 )∗𝑑 = backward(𝑟𝑐 ⟨𝑟 : 𝑝⟩𝑟, 𝜖, 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(¬𝑙 ∧ 𝑝 1 = |𝑤 |) ∨ 𝑙(𝑟, 𝑟𝑐 ⟨𝑟 ∗ : 𝑝⟩, 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 ∗, 𝑟𝑐 , 𝑤, 𝑝 2, Γ2, 𝑑, 𝑙) ⇓ (𝑝 3, Γ3 )(𝑟 ∗, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 3, Γ3 )Lazy Kleene Star𝑑 = forward(𝑟𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ 𝜏(¬𝑙 ∧ (𝜏 = failed ∨ 𝜏 = (𝑝 ′, Γ ′ ) where 𝑝 ′ ≠ |𝑤 |)) ∨ (𝑙 ∧ 𝜏 = failed)∗?
(𝑟 ⟨𝑟 : 𝑝⟩𝑟𝑐 , 𝜖, 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 3, Γ3 )(¬𝑙 ∧ 𝑝 3 = |𝑤 |) ∨ 𝑙(𝑟, ⟨𝑟 ∗? : 𝑝⟩𝑟𝑐 , 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(𝑟 ∗?, 𝑟𝑐 , 𝑤, 𝑝 1, Γ1, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 ∗?, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )𝑑 = backward(𝑟𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ 𝜏(¬𝑙 ∧ (𝜏 = failed ∨ 𝜏 = (𝑝 ′, Γ ′ ) where 𝑝 ′ ≠ |𝑤 |) ∨ (𝑙 ∧ 𝜏 = failed)(𝑟𝑐 ⟨𝑟 ∗? : 𝑝⟩𝑟, 𝜖, 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 3, Γ3 )(¬𝑙 ∧ 𝑝 3 = |𝑤 |) ∨ 𝑙(𝑟, 𝑟𝑐 ⟨𝑟 ∗? : 𝑝⟩, 𝑤, 𝑝, reset (𝑟, Γ), 𝑑, 𝑙) ⇓ (𝑝 1, Γ1 )(𝑟 ∗?, 𝑟𝑐 , 𝑤, 𝑝 1, Γ1, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )(𝑟 ∗?, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 2, Γ2 )Guard𝑝′ = 𝑝(𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )′(⟨𝑟 : 𝑝 ⟩, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )𝑝′ ≠ 𝑝(⟨𝑟 : 𝑝 ′ ⟩, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ failed

Fig. 7. Rules for Kleene stars.

B

PROOF OF THEOREM 4.4

Proof. Let 𝑘 be the maximum number of indexes of capturing groups in positive examples.
We assume that 𝑘 ≥ 1. Note that if 𝑘 = 0, then it is immediate since we can obtain the solution
by taking the unions of strings in positive examples. We show that we can always constructa regex that satisfies the consistency condition. Let a regex 𝑟 , a set of positive examples E + ={(𝑤 1, Γ1 ), (𝑤 2, Γ2 ), · · · , (𝑤𝑛 , Γ𝑛 )}, and a set of negative examples E − be an input instance of theextraction-regex-repair problem.
Then, we prepare a regex 𝑟 ′ = 𝑟 1𝑟 2 · · · 𝑟𝑘 𝑟 body where• for all 𝑖 ∈ [𝑘], 𝑟𝑖 = (?=(𝑟𝑖,defined |𝑟𝑖,undefined )),• 𝑟𝑖,defined = .∗ (𝑟𝑖,defined,1 |𝑟𝑖,defined,2| · · · |𝑟𝑖,defined,𝑛 )𝑖 ,((?<=(?<!.)𝑤 𝑗 [0..𝑝𝑙 ))𝑤 𝑗 [𝑝𝑙 ..𝑝𝑟 )(?=𝑤 𝑗 [𝑝𝑟 ..|𝑤 𝑗 |)(?!.))) if Γ𝑗 (𝑖) = (𝑝𝑙 , 𝑝𝑟 ),𝑟𝑖,defined,𝑗 = ∅otherwise• 𝑟𝑖,undefined = 𝑟𝑖,undefined,1 |𝑟𝑖,undefined,2| · · · |𝑟𝑖,undefined,𝑛 ,(• for 𝑗 ∈ [𝑛], 𝑟𝑖,defined,𝑗 =• for 𝑗 ∈ [𝑛], 𝑟𝑖,undefined,𝑗 =∅if Γ𝑗 (𝑖) = (𝑝𝑙 , 𝑝𝑟 ), and(?<!.)𝑤 𝑗 (?!.) otherwise• 𝑟 body = (𝑤 1 |𝑤 2 | · · · |𝑤𝑛 ).
We now show that the regex 𝑟 ′ satisfies the consistency condition by showing L𝑐 (𝑟 ′ ) = E + . We
first show that for every (𝑤 𝑗 , Γ𝑗 ) ∈ E + , (𝑤 𝑗 , Γ𝑗 ) ∈ L𝑐 (𝑟 ′ ). To prove this, we show that 𝑤 𝑗 ∈ L (𝑟 ′ ),and then, we show that 𝑟 ′ extracts correct substrings. Since 𝑟 ′ consists of the positive lookaheads
𝑟𝑖 and the expression 𝑟 body whose language is {𝑤 | (𝑤, _) ∈ E + }, 𝑟 ′ accepts 𝑤 𝑗 if all the positive
lookaheads 𝑟𝑖 succeeds. For each 𝑟𝑖 , it succeeds on 𝑤 𝑗 and correctly extracts the substrings because
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:27

Capturing Group𝑑 = forward(𝑟 $𝑖 , 𝑟𝑐 , 𝑤, 𝑝, Γ[𝑖 ↦→ (𝑝, ⊥)], 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )((𝑟 )𝑖 , 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )𝑑 = backward($𝑖 𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ[𝑖 ↦→ (⊥, 𝑝)], 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )((𝑟 )𝑖 , 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′, Γ ′ )𝑑 = forward

Γ(𝑖) = (𝑝, ⊥)($𝑖 , 𝑟𝑐 , 𝑤, 𝑝 ′, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ [𝑖 ↦→ (𝑝, 𝑝 ′ )])𝑑 = backward

Γ(𝑖) = (𝑝 ′, ⊥)($𝑖 , 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ [𝑖 ↦→ (𝑝, 𝑝 ′ )])BackreferenceΓ(𝑖) = (𝑝 ′, 𝑝 ′′ )(𝑤 [𝑝 ′ ..𝑝 ′′ ), 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′′′, Γ ′ )(\𝑖, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝 ′′′, Γ ′ )𝑖 ∉ 𝑑𝑜𝑚(Γ) ∨ Γ(𝑖) = (𝑝 ′, ⊥)(\𝑖, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ)

Lookahead(𝑟, 𝜖, 𝑤, 𝑝, Γ, forward, true) ⇓ (𝑝 ′, Γ ′ )(𝑟, 𝜖, 𝑤, 𝑝, Γ, forward, true) ⇓ failed((?=𝑟 ), 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ ′ )((?!𝑟 ), 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ)
Lookbehind(𝑟, 𝜖, 𝑤, 𝑝, Γ, backward, true) ⇓ (𝑝 ′, Γ ′ )(𝑟, 𝜖, 𝑤, 𝑝, Γ, backward, true) ⇓ failed((?<=𝑟 ), 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ ′ )((?<!𝑟 ), 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ)

Fig. 8. Rules for real-world extensions.

(1) if Γ𝑗 (𝑖) = (𝑝𝑙 , 𝑝𝑟 ), then 𝑟𝑖,defined,𝑗 = (?<=(?<!.)𝑤 𝑗 [0..𝑝𝑙 ))𝑤 𝑗 [𝑝𝑙 ..𝑝𝑟 )(?=𝑤 𝑗 [𝑝𝑟 ..|𝑤 𝑗 |)(?!.)) by theconstruction. The subexpression 𝑤 𝑗 [𝑝𝑙 ..𝑝𝑟 ) exactly matches the string 𝑤 𝑗 [𝑝𝑙 ..𝑝𝑟 ). The positive lookbehind (?<=(?<!.)𝑤 𝑗 [0..𝑝𝑙 )) asserts that the string from the beginning to the current position, i.e., 𝑝𝑙 − 1, should be exactly the string 𝑤 𝑗 [0..𝑝𝑙 ) and the positive lookahead(?=𝑤 𝑗 [𝑝𝑟 ..|𝑤 𝑗 |)(?!.)) asserts that the string from the current position, i.e., 𝑝𝑟 , to the end of
the string should be exactly the string 𝑤 𝑗 [𝑝𝑟 ..|𝑤 𝑗 |). Note that the expressions (?<!.) and (?!.)
match the beginning and the end of strings, respectively, i.e., we can see them as the syntactic
sugars of the anchor operators ^ and $ [Friedl 2006], respectively. As a result, the expression
𝑟𝑖,defined,𝑗 exactly matches 𝑤 𝑗 on the correct position. Additionally, since lookarounds do notconsume any character, the 𝑖th capturing group only extracts 𝑤 𝑗 [𝑝𝑙 ..𝑝𝑟 ).
(2) If 𝑖 ∉ 𝑑𝑜𝑚(Γ𝑗 ), then 𝑟𝑖,defined,𝑗 = ∅ that does not match any word and 𝑟𝑖,undefined,𝑗 = (?<!.)𝑤 𝑗 (?!.)
that exactly matches the string 𝑤 𝑗 . Since 𝑟𝑖,defined fails due to 𝑟𝑖,defined,𝑗 , 𝑟 𝑗 does not extract any
word, whereas the matching of 𝑟 𝑗 on 𝑤 𝑗 succeeds due to 𝑟𝑖,undefined,𝑗 .
Next, we show that for every (𝑤 𝑗 , Γ𝑗 ) ∉ E + , (𝑤 𝑗 , Γ𝑗 ) ∉ L𝑐 (𝑟 ′ ). The matching of 𝑟 ′ on 𝑤 𝑗 fails
regardless of the positive lookaheads 𝑟𝑖 because the only subexpression that consumes charactersis 𝑟 body , and it exactly matches the strings in {𝑤 | (𝑤, _) ∈ E + } by the construction. Hence,L𝑐 (𝑟 ′ ) = E + . This satisfies the consistency condition, and implies the existence of the solution.
□C

PROOF OF THEOREM 4.5

We first review SetCover.
Definition C.1. Given a finite set 𝑈 , 𝑆 ⊆ P (𝑈 ), where P (𝑈 ) denotes the powerset of a set
𝑈 , and a positive integer 𝑘, SetCover is theÐproblem of deciding whether there exists a subset
𝑇 = {𝑇1,𝑇2, · · · ,𝑇𝑛 } ⊆ 𝑆 such that 𝑛 ≤ 𝑘 and 𝑇 = 𝑈 .
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:28

Nariyoshi Chida and Tachio Terauchi

Set of Characters and Empty String𝑑 = forward

𝑝 < |𝑤 |𝑤 [𝑝] ∈ 𝐶

𝑑 = backward( [𝐶], 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 + 1, Γ, true)}, ∅)0 ≤𝑝 −1𝑤 [𝑝 − 1] ∈ 𝐶([𝐶], 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 − 1, Γ, true)}, ∅)(𝜖, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, true)}, ∅)Hole𝑑 = forward□ is the 𝑖th hole.

𝑝 < |𝑤 |𝑤 [𝑝 ]𝑤 [𝑝 ](□, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 + 1, Γ, 𝑣𝑖)}, {(⊥, ⊥, ¬𝑣𝑖)})

𝑑 = backward□ is the 𝑖th hole.

0 ≤𝑝 −1𝑤 [𝑝 −1]𝑤 [𝑝 −1](□, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 − 1, Γ, 𝑣𝑖)}, {(⊥, ⊥, ¬𝑣𝑖)})

Concatenation𝑑 = forward(𝑡 1, 𝑡 2𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )∀(𝑝𝑖 , Γ𝑖 , 𝜙𝑖 ) ∈ 𝑆. (𝑡 2, 𝑡𝑐 , 𝑤, 𝑝𝑖 , Γ𝑖 , 𝑑, 𝑙) d (𝑆𝑖 , 𝐹𝑖 )
Ð(𝑡 1𝑡 2, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ( 0≤𝑖<|𝑆 | {(𝑝 ′, Γ ′, 𝜙𝑖 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆𝑖 },Ð
𝐹 ∪ 0≤𝑖<|𝑆 | {(⊥, ⊥, 𝜙𝑖 ∧ 𝜙 ′ ) | (⊥, ⊥, 𝜙 ′ ) ∈ 𝐹𝑖 })𝑑 = backward(𝑡 2, 𝑡𝑐 𝑡 1, 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )∀(𝑝𝑖 , Γ𝑖 , 𝜙𝑖 ) ∈ 𝑆. (𝑡 1, 𝑡𝑐 , 𝑤, 𝑝𝑖 , Γ𝑖 , 𝑑, 𝑙) d (𝑆𝑖 , 𝐹𝑖 )
Ð′(𝑡 1𝑡 2, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ( 0≤𝑖<|𝑆 | {(𝑝 , Γ ′, 𝜙𝑖 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆𝑖 },Ð
𝐹 ∪ 0≤𝑖<|𝑆 | {(⊥, ⊥, 𝜙𝑖 ∧ 𝜙 ′ ) | (⊥, ⊥, 𝜙 ′ ) ∈ 𝐹𝑖 })Union

𝑑 = forward(𝑡 1𝑡𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆 1, 𝐹 1 )𝑆 1′ = ite(𝑙, 𝑆 1, {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 1 | 𝑝 ′ = |𝑤 |})𝐹 1′ = 𝐹 1 ∪ ite(𝑙, ∅, {(⊥, ⊥, 𝜙 ′ ) | (𝑝 ′, _, 𝜙 ′ ) ∈ 𝑆 1, 𝑝 ′ ≠ |𝑤 |})ÔÔ
𝜙𝑆 1 = (_,_,𝜙 ′ ) ∈𝑆 1′ 𝜙 ′𝜙 𝐹1 = (⊥,⊥,𝜙 ′ ) ∈𝐹1′ 𝜙 ′(𝑡 1, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆 2, 𝐹 2 )(𝑡 2, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆 3, 𝐹 3 )(𝑡 1 |𝑡 2, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 ′, Γ ′, 𝜙𝑆 1 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 2 } ∪ {(𝑝 ′, Γ ′, 𝜙 𝐹1 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 3 },{(⊥, ⊥, 𝜙 𝐹1 ∧ 𝜙 ′ ) | (⊥, ⊥, 𝜙 ′ ) ∈ 𝐹 3 })𝑑 = backward(𝑡𝑐 𝑡 1, 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆 1, 𝐹 1 )𝑆 1′ = ite(𝑙, 𝑆 1, {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 1 | 𝑝 ′ = |𝑤 |})𝐹 1′ = 𝐹 1 ∪ ite(𝑙, ∅, {(⊥, ⊥, 𝜙 ′ ) | (𝑝 ′, _, 𝜙 ′ ) ∈ 𝑆 1, 𝑝 ′ ≠ |𝑤 |})ÔÔ
𝜙𝑆 1 = (_,_,𝜙 ′ ) ∈𝑆 1′ 𝜙 ′𝜙 𝐹1 = (⊥,⊥,𝜙 ′ ) ∈𝐹1′ 𝜙 ′(𝑡 1, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆 2, 𝐹 2 )(𝑡 2, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆 3, 𝐹 3 )(𝑡 1 |𝑡 2, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝 ′, Γ ′, 𝜙𝑆 1 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 2 } ∪ {(𝑝 ′, Γ ′, 𝜙 𝐹1 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 3 },{(⊥, ⊥, 𝜙 𝐹1 ∧ 𝜙 ′ ) | (⊥, ⊥, 𝜙 ′ ) ∈ 𝐹 3 })Fig. 9. Rules for pure regexes (except for Kleene stars) and holes.

Proof. We give a reduction from SetCover to the repair problem. For this, we create (thedecision version of) the repair problem.
• The alphabet Σ = 𝑈 ;• The set of positive examples E + = {L𝑎M1 | 𝑎 ∈ Σ};• The set of negative examples E − = ∅;• The distance bound is 2𝑘; and• The pre-repair expression 𝑟 = (𝑟 1 |𝑟 2 | · · · |𝑟𝑛 )1 where 𝑟𝑖 = (?=[𝑇𝑖 ])𝑘 ∅[𝑇𝑖 ] for 𝑖 ∈ [𝑛].
Here, 𝑟 𝑘 is the expression obtained by concatenating 𝑟 𝑘 times.
It is easy to see that this is a polynomial reduction and is a valid instance of the repair problem.
We show that the reduction is correct, i.e., the instance of SetCover has a solution iff the instance
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:29Greedy Kleene Star𝑑 = forward(𝑡 ⟨𝑡 ∗ : 𝑝⟩𝑡𝑐 , 𝜖, 𝑤, 𝑝, reset (𝑡, Γ), 𝑑, 𝑙) d (𝑆, 𝐹 )𝑆𝑎 = ite(𝑙, 𝑆, {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 | 𝑝 ′ = |𝑤 |})ÔÔ
𝜙𝑆 = (_,_,𝜙 ′ ) ∈𝑆𝑎 𝜙 ′𝜙 𝐹 = (_,_,𝜙 ′ ) ∈𝐹 ∪(𝑆\𝑆𝑎 ) 𝜙 ′(𝑡, ⟨𝑡 ∗ : 𝑝⟩𝑡𝑐 , 𝑤, 𝑝, reset (𝑡, Γ), 𝑑, 𝑙) d (𝑆 ′, 𝐹 ′ )Ô′𝑆𝑆𝐴𝑇= {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 ′ |𝜙 ′ ∧ 𝜙𝑆 is satisfiable.}𝜙 𝐹 ′ = (⊥,⊥,𝜙 ′ ) ∈𝐹 ′ 𝜙 ′′∀(𝑝𝑖 , Γ𝑖 , 𝜙𝑖 ) ∈ 𝑆𝑆𝐴𝑇
. (𝑡 ∗, 𝑡𝑐 , 𝑤, 𝑝𝑖 , Γ𝑖 , 𝑑, 𝑙) d (𝑆𝑖 , 𝐹𝑖 )
Ð(𝑡 ∗, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, 𝜙 𝐹 ∨ (𝜙𝑆 ∧ 𝜙 𝐹 ′ ))} ∪ 0≤𝑖<|𝑆 ′ | {(𝑝 ′, Γ ′, 𝜙𝑆 ∧ 𝜙𝑖 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆𝑖 }, ∅)𝑆𝐴𝑇

𝑑 = backward(𝑡𝑐 ⟨𝑡 ∗ : 𝑝⟩𝑡, 𝜖, 𝑤, 𝑝, reset (𝑡, Γ), 𝑑, 𝑙) d (𝑆, 𝐹 )𝑆𝑎 = ite(𝑙, 𝑆, {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 | 𝑝 ′ = |𝑤 |})ÔÔ′′
𝜙𝑆 = (_,_,𝜙 ′ ) ∈𝑆𝑎 𝜙
𝜙 𝐹 = (_,_,𝜙 ′ ) ∈𝐹 ∪(𝑆\𝑆𝑎 ) 𝜙(𝑡, 𝑡𝑐 ⟨𝑡 ∗ : 𝑝⟩, 𝑤, 𝑝, reset (𝑡, Γ), 𝑑, 𝑙) d (𝑆 ′, 𝐹 ′ )
Ô
′
′
′
′
′
′
𝑆𝑆𝐴𝑇 = {(𝑝 , Γ , 𝜙 ) ∈ 𝑆 | 𝜙 ∧ 𝜙𝑆 is satisfiable.}𝜙 𝐹 ′ = (⊥,⊥,𝜙 ′ ) ∈𝐹 ′ 𝜙 ′′∀(𝑝𝑖 , Γ𝑖 , 𝜙𝑖 ) ∈ 𝑆𝑆𝐴𝑇
. (𝑡 ∗, 𝑡𝑐 , 𝑤, 𝑝𝑖 , Γ𝑖 , 𝑑, 𝑙) d (𝑆𝑖 , 𝐹𝑖 )
Ð(𝑡 ∗, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, 𝜙 𝐹 ∨ (𝜙𝑆 ∧ 𝜙 𝐹 ′ ))} ∪ 0≤𝑖<|𝑆 ′ | {(𝑝 ′, Γ ′, 𝜙𝑆 ∧ 𝜙𝑖 ∧ 𝜙 ′ ) | (𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆𝑖 }, ∅)𝑆𝐴𝑇

Lazy Kleene Star𝑑 = forward(𝑡𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )𝑆𝑎 = ite(𝑙, 𝑆, {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 | 𝑝 ′ = |𝑤 |})ÔÔ
𝜙𝑆 = (_,_,𝜙 ′ ) ∈𝑆𝑎 𝜙 ′𝜙 𝐹 = (_,_,𝜙 ′ ) ∈𝐹 ∪(𝑆\𝑆𝑎 ) 𝜙 ′(𝑡 ⟨𝑡 ∗? : 𝑝⟩𝑡𝑐 , 𝜖, 𝑤, 𝑝, reset (𝑡, Γ), 𝑑, 𝑙) d (𝑆 ′, 𝐹 ′ )ÔÔ𝑆𝑎′ = ite(𝑙, 𝑆 ′, {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 ′ | 𝑝 ′ = |𝑤 |})𝜙𝑆 ′ = (_,_,𝜙 ′ ) ∈𝑆𝑎′ 𝜙 ′𝜙 𝐹 ′ = (_,_,𝜙 ′ ) ∈𝐹 ′ ∪(𝑆 ′ \𝑆𝑎′ ) 𝜙 ′
∗?
′′
′′
′′
′
′
′
′′
′
(𝑡, ⟨𝑡 : 𝑝⟩𝑡𝑐 , 𝑤, 𝑝, reset (𝑡, Γ), 𝑑, 𝑙) d (𝑆 , 𝐹 )𝑆𝑆𝐴𝑇 = {(𝑝 , Γ , 𝜙 ) ∈ 𝑆 | 𝜙 ∧ 𝜙 𝐹 ∧ 𝜙𝑆 ′ is satisfiable.}Ô′′ . (𝑡 ∗? , 𝑡 , 𝑤, 𝑝 , Γ , 𝑑, 𝑙) d (𝑆 , 𝐹 )𝜙 𝐹 ′′ = (⊥,⊥,𝜙 ′ ) ∈𝐹 ′′ 𝜙 ′∀(𝑝𝑖 , Γ𝑖 , 𝜙𝑖 ) ∈ 𝑆𝑆𝐴𝑇
𝑐
𝑖 𝑖
𝑖 𝑖
(𝑡 ∗?, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, 𝜙𝑆 ∨ (𝜙 𝐹 ∧ 𝜙 𝐹 ′ ) ∨ (𝜙 𝐹 ∧ 𝜙𝑆 ′ ∧ 𝜙 𝐹 ′′ ))}∪
Ð
′ ′
′
′ ′ ′
0≤𝑖<|𝑆 ′′ | {(𝑝 , Γ , 𝜙 𝐹 ∧ 𝜙𝑆 ′ ∧ 𝜙𝑖 ∧ 𝜙 ) | (𝑝 , Γ , 𝜙 ) ∈ 𝑆𝑖 }, ∅)𝑆𝐴𝑇

𝑑 = backward(𝑡𝑐 , 𝜖, 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )𝑆𝑎 = ite(𝑙, 𝑆, {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 | 𝑝 ′ = |𝑤 |})ÔÔ
𝜙𝑆 = (_,_,𝜙 ′ ) ∈𝑆𝑎 𝜙 ′𝜙 𝐹 = (_,_,𝜙 ′ ) ∈𝐹 ∪(𝑆\𝑆𝑎 ) 𝜙 ′(𝑡𝑐 ⟨𝑡 ∗? : 𝑝⟩𝑡, 𝜖, 𝑤, 𝑝, reset (𝑡, Γ), 𝑑, 𝑙) d (𝑆 ′, 𝐹 ′ )ÔÔ𝑆𝑎′ = ite(𝑙, 𝑆 ′, {(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 ′ | 𝑝 ′ = |𝑤 |})𝜙𝑆 ′ = (_,_,𝜙 ′ ) ∈𝑆𝑎′ 𝜙 ′𝜙 𝐹 ′ = (_,_,𝜙 ′ ) ∈𝐹 ′ ∪(𝑆 ′ \𝑆𝑎′ ) 𝜙 ′
∗?
′′
′′
′′
′
′
′
′′
′
(𝑡, 𝑡𝑐 ⟨𝑡 : 𝑝⟩, 𝑤, 𝑝, reset (𝑡, Γ), 𝑑, 𝑙) d (𝑆 , 𝐹 )𝑆𝑆𝐴𝑇 = {(𝑝 , Γ , 𝜙 ) ∈ 𝑆 | 𝜙 ∧ 𝜙 𝐹 ∧ 𝜙𝑆 ′ is satisfiable.}Ô′′ . (𝑡 ∗? , 𝑡 , 𝑤, 𝑝 , Γ , 𝑑, 𝑙) d (𝑆 , 𝐹 )𝜙 𝐹 ′′ = (⊥,⊥,𝜙 ′ ) ∈𝐹 ′′ 𝜙 ′∀(𝑝𝑖 , Γ𝑖 , 𝜙𝑖 ) ∈ 𝑆𝑆𝐴𝑇
𝑐
1 1
𝑖 𝑖
(𝑡 ∗?, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, 𝜙𝑆 ∨ (𝜙 𝐹 ∧ 𝜙 𝐹 ′ ) ∨ (𝜙 𝐹 ∧ 𝜙𝑆 ′ ∧ 𝜙 𝐹 ′′ ))}∪
Ð
′′ ′′
′′
′′ ′′ ′′
0≤𝑖<|𝑆 ′′ | {(𝑝 , Γ , 𝜙𝑆 ∧ 𝜙𝑆 ′ ∧ 𝜙𝑖 ∧ 𝜙 ) | (𝑝 , Γ , 𝜙 ) ∈ 𝑆𝑖 }, ∅)𝑆𝐴𝑇

Guards𝑝′ = 𝑝𝑝′ ≠ 𝑝(⟨𝑡 : 𝑝 ′ ⟩, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (∅, {(𝑝, Γ, true)})(𝑡, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )(⟨𝑡 : 𝑝 ′ ⟩, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )Fig. 10. Rules for Kleene stars.

of the repair problem created above has a solution. First, we show the only if direction. Let 𝑇 ′ ⊆ 𝑇
be a solution of the instance of SetCover. Then, the solution of the repair problem is the regex𝑟 ′ = (𝑟 1′ |𝑟 2′ | · · · |𝑟𝑛′ ) where 𝑟𝑖′ = 𝑟𝑖 if 𝑇𝑖 ∉ 𝑇 ′ and otherwise 𝑟𝑖′ = ([𝑇𝑖 ])𝑘 𝜖 [𝑇𝑖 ]. That is, for all 𝑟𝑖 , if
𝑇𝑖 ∈ 𝑇 ′ , then we replace the empty set ∅ in 𝑟𝑖 with the empty string 𝜖 and otherwise 𝑟𝑖 remains thesame. Note that the distance between 𝑟 and 𝑟 ′ is 2|𝑇 ′ | ≤ 2𝑘. Additionally, the regex 𝑟 ′ is consistent
with all the examples. That is, for all 𝑎 ∈ Σ, 𝑟 ′ extracts the character 𝑎 by the 1st capturing group
because there exists 𝑇𝑖 ∈ 𝑇 ′ such that 𝑎 ∈ 𝑇𝑖 since 𝑇 ′ is a solution of the SetCover instance,
and therefore 𝑟𝑖′ = (?=[𝑇𝑖 ])𝑘 𝜖 [𝑇𝑖 ] by the construction and 𝑎 ∈ L (𝑟𝑖′ ). Also, E − is immediate sinceE − = ∅. Thus, 𝑟 ′ is a correct repair.
Next, we show the if direction. For this, we first show that the only meaningful change in the
repair is to change the ∅ in 𝑟 with 𝜖. First, any valid repair of 𝑟 does not change the capturing group
because, to change the capturing group, we need to replace all immediate subexpressions with
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

173:30

Nariyoshi Chida and Tachio Terauchi

Capturing Group𝑑 = forward(𝑡$𝑖 , 𝑡𝑐 , 𝑤, 𝑝, Γ [𝑖 ↦→ (𝑝, ⊥)], 𝑑, 𝑙) d (𝑆, 𝐹 )((𝑡)𝑖 , 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )𝑑 = backward($𝑖 𝑡, 𝑡𝑐 , 𝑤, 𝑝, Γ [𝑖 ↦→ (𝑝, ⊥)], 𝑑, 𝑙) d (𝑆, 𝐹 )((𝑡)𝑖 , 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )𝑑 = forward

Γ(𝑖) = (𝑝 ′, ⊥)($𝑖 , 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ [𝑖 ↦→ (𝑝 ′, 𝑝)], true)}, ∅)𝑑 = backward

Γ(𝑖) = (𝑝 ′, ⊥)($𝑖 , 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ [𝑖 ↦→ (𝑝, 𝑝 ′ )], true)}, ∅)BackreferenceΓ(𝑖) = (𝑝 ′, 𝑝 ′′ )(𝑤 [𝑝 ′ ..𝑝 ′′ ), 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )(\𝑖, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (𝑆, 𝐹 )𝑖 ∉ 𝑑𝑜𝑚(Γ) ∨ Γ(𝑖) = (𝑝 ′, ⊥)(\𝑖, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, true)}, ∅)Lookaheads(𝑡, 𝜖, 𝑤, 𝑝, Γ, forward, true) d (𝑆, 𝐹 )((?=𝑡), 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ ′, 𝜙 ′ ) | (_, Γ ′, 𝜙 ′ ) ∈ 𝑆 }, 𝐹 )(𝑡, 𝜖, 𝑤, 𝑝, Γ, forward, true) d (𝑆, 𝐹 )((?!𝑡), 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, 𝜙 ′ ) | (⊥, ⊥, 𝜙 ′ ) ∈ 𝐹 }, {(⊥, ⊥, 𝜙 ′ ) | (_, _, 𝜙 ′ ) ∈ 𝑆 })Lookbehinds(𝑡, 𝜖, 𝑤, 𝑝, Γ, backward, true) d (𝑆, 𝐹 )((?<=𝑡), 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ ′, 𝜙 ′ ) | (_, Γ ′, 𝜙 ′ ) ∈ 𝑆 }, 𝐹 )(𝑡, 𝜖, 𝑤, 𝑝, Γ, backward, true) d (𝑆, 𝐹 )((?<!𝑡), 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, 𝜙 ′ ) | (⊥, ⊥, 𝜙 ′ ) ∈ 𝐹 }, {(⊥, ⊥, 𝜙 ′ ) | (_, _, 𝜙 ′ ) ∈ 𝑆 })Fig. 11. Rules for real-world extensions.

holes and it immediately violates the distance bound 2𝑘 since 𝑟 has (?=𝑟𝑖 )𝑘 . For the same reason,any valid repair of 𝑟 must preserve the 𝑛 union choices, and for each 𝑟𝑖 , it is useless to change(?=[𝑇𝑖 ]). Additionally, it is also useless to change [𝑇𝑖 ] to some expression whose language contains
elements not in 𝑇𝑖 due to the 𝑘 many (?=[𝑇𝑖 ]) preceding it. Note that the changing (?=[𝑇𝑖 ])𝑘 would
exceed the distance bound. Nor, can [𝑇𝑖 ] be changed to some expression whose language does notcontain elements in 𝑇𝑖 because we do not need to exclude any character in Σ. As a result, it is easy
to see that the only meaningful change is to change ∅ with 𝜖. Therefore, the solution of the repair
problem is of the form 𝑟 ′ = (𝑟 1′ |𝑟 2′ | · · · |𝑟𝑛′ ) obtained from 𝑟 by replacing some ∅ with 𝜖. From thesolutions of the repair problem, we can construct the set 𝑇 ′ = {𝑇𝑖 | 𝑟𝑖 ≠ 𝑟𝑖′ }. Then, the set 𝑇 ′ is asolution of the instance of SetCover. This is because, since the distance bound is 2𝑘, the repairchanges at most 𝑘 empty sets. From this, there exists at most 𝑘 𝑟𝑖 such that 𝑟𝑖 ≠ 𝑟𝑖′ for 𝑖 ∈ [𝑛], andtherefore |𝑇 ′ | ≤ 𝑘 by the construction. Additionally, for all 𝑎 ∈ Σ, there exists 𝑇𝑖 such that 𝑎 ∈ 𝑇𝑖 by
the construction because 𝑟 ′ is the solution of the repair problem, and therefore there exists 𝑟𝑖′ suchthat 𝑎 ∈ L (𝑟𝑖 ) and 𝑟𝑖 ≠ 𝑟𝑖′ . Thus, 𝑇 ′ is a correct solution.
□D

APPROXIMATION FOR MEMBERSHIP

Given a template 𝑡, we construct the over- and under-approximation for membership by thefollowing procedures. First, we eliminate backreferences by approximating them. We use the sameprocedure to eliminate backreferences describes in Section 5.3.2.
Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.

Repairing Regular Expressions for Extraction

173:31

Next, we eliminate holes by approximating them. For this, we use the function 𝛼 which is defined
as follows. Below, 𝑟 = ∅ if 𝑟 = .∗ and 𝑟 = .∗ if 𝑟 = ∅.
𝛼 ( [𝐶], 𝑟 ) = [𝐶]𝛼 ((𝑡)𝑖 , 𝑟 ) = (𝛼 (𝑡, 𝑟 ))𝑖𝛼 (𝜖, 𝑟 ) = 𝜖𝛼 ((?=𝑡), 𝑟 ) = (?=𝛼 (𝑡, 𝑟 ))𝛼 (𝑡 1𝑡 2, 𝑟 ) = 𝛼 (𝑡 1, 𝑟 )𝛼 (𝑡 2, 𝑟 )𝛼 ((?!𝑡), 𝑟 ) = (?!𝛼 (𝑡, 𝑟 ))𝛼 (𝑡 1 |𝑡 2, 𝑟 ) = 𝛼 (𝑡 1, 𝑟 )|𝛼 (𝑡 2, 𝑟 ) 𝛼 ((?<=𝑡), 𝑟 ) = (?<=𝛼 (𝑡, 𝑟 ))𝛼 (𝑡 ∗, 𝑟 ) = 𝛼 (𝑡, 𝑟 ) ∗𝛼 ((?<!𝑡), 𝑟 ) = (?<!𝛼 (𝑡, 𝑟 ))𝛼 (𝑡 ∗?, 𝑟 ) = 𝛼 (𝑡, 𝑟 ) ∗?
𝛼 (□, 𝑟 ) = 𝑟
As a result, we obtain an over- (resp. under-)approximated regex 𝑟 ⊤ (resp. 𝑟 ⊥ ) by 𝛼 (𝑡 ′, .∗ ) (resp. 𝛼 (𝑡 ′, ∅)),
where 𝑡 ′ is a template obtained from 𝑡 by applying the first procedure for eliminating backreferences.
E

FULL RULES OF THE SEMANTICS

In this section, we show the full version of the rules for the formal semantics of regexes. Figures 6, 7,
and 8 show the rules for pure regexes except for Kleene stars, Kleene stars, and real-world extensions,
respectively. For the state (𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) that is not applicable for any rule in the figures, we
assume that (𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓ (𝑝, Γ) if 𝑟 is the Kleene star, and otherwise, (𝑟, 𝑟𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) ⇓failed. Below, we describe the rules that are not described in Section 3.
The rule for positive lookaheads (?=𝑟 ) first performs the matching of the expression 𝑟 with thedirection 𝑑 = forward. If the matching succeeds, then it returns the result after resetting the position
from 𝑝 ′ to 𝑝. The rule for negative lookaheads (?!𝑟 ) is similar to the rule of positive lookaheads, i.e.,
it first performs the matching of 𝑟 . However, unlike positive lookaheads, the matching of negative
lookaheads succeeds if the matching of 𝑟 fails. Additionally, negative lookaheads reset not only
the position but also the environment. The rule for negative lookbehinds is similar to the rule ofnegative lookahead. The only difference is the direction, i.e., negative lookbehinds set the direction
to 𝑑 = backward.
F

FULL RULES OF THE CONSTRAINT GENERATION RULES

In this section, we give the full version of the inference rules for the SMT constraint generation.
Figures 9, 10, and 11 show the rules for pure regexes except for Kleene stars and holes, for Kleenestars, and the real-world extensions, respectively. For the state (𝑡, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) that is not applicablefor any rule in the figure, we evaluate it as (𝑡, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d (∅, ∅) if 𝑡 is not the Kleene star, andotherwise, i.e., 𝑡 is the Kleene star, (𝑡, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙) d ({(𝑝, Γ, true)}, ∅).
These rules except for the rule of holes build on the semantics of regexes defined in Section 3. The
difference between the semantics and the inference rules is that the inference rules compute resultsof succeeded and failed matching, and construct SMT constraints based on the results. Additionally,
the inference rules have the rule of holes. Since our algorithm tries to replace holes with a set ofcharacters such that the obtained regex is consistent with examples, the rule of holes behaves likethe rule of the set-of-characters operator. That is, for (□, 𝑡𝑐 , 𝑤, 𝑝, Γ, 𝑑, 𝑙), if 𝑝 ≤ |𝑤 |, then we canreplace the hole with the sets of character [𝐶] such that 𝑤 [𝑝] ∈ 𝐶 or 𝑤 [𝑝] ∉ 𝐶. Therefore, we add
𝑤 [𝑝 ](𝑝 + 1, Γ, 𝑣𝑖) to the succeeded result, i.e., the matching at the hole succeeded and therefore the𝑤 [𝑝 ]
replaced set of characters accepts the character 𝑤 [𝑝], and (⊥, ⊥, ¬𝑣𝑖) to the failed result, i.e.,the matching at the hole failed and therefore the replaced set of characters rejects the character𝑤 [𝑝].
Received 2022-11-10; accepted 2023-03-31

Proc. ACM Program. Lang., Vol. 7, No. PLDI, Article 173. Publication date: June 2023.