Repairing Regex-Dependent String Functions
Nariyoshi Chida

Tachio Terauchi

nariyoshichidamm@gmail.com
NTT Social Informatics Laboratories
Japanterauchi@waseda.jp
Waseda University
Japan

ABSTRACT
Regex-dependent string functions are string functions that takeregular expressions (regexes) as parameters and are popular meansof manipulating strings. They are frequently used for, e.g., stringtransformation and substring search. Despite the importance, writing these functions is far from easy. To rectify this situation, recent
research made significant progress by proposing automated methods for synthesizing regexes based on Programming by Examples(PBE). However, there still is a gap between these methods andthe goal of synthesizing regex-dependent string functions. First,
the existing methods focus on whole-string matching, whereas
most regex-dependent string functions adopt substring matching.
Second, the existing methods focus only on the regex, but many
commonly used regex-dependent string functions, such as replace
and replaceAll, also take as parameter a replacement to specify how
the substrings matched to the regex will be replaced.
This paper fills the gap by presenting the first PBE-based method
for repairing regex-dependent string functions. Like the recent
methods for regex synthesis, our algorithm builds on enumerative
search with pruning and SMT constraint solving, but with extensions to support substring matching and replacement. The main
challenge is the large search space. We address the challenge by
novel ideas such as incorporation of origin information in examples to identify the locations of substrings to be matched, a new
substring-context-aware pruning technique, and a novel use of SMT
constraints to insert captures that can be referred from the replacement. Additionally, we identify a novel necessary and sufficientcondition that can be used to detect and filter unrepairable instances.
We implemented our algorithm as a prototype tool called R2-DS
and evaluated it on real-world benchmarks. Results show that ouralgorithm efficiently repairs the bugs in the real world and finds
high-quality repairs.

CCS CONCEPTS• Software and its engineering → Software notations andtools; • Theory of computation → Regular languages.

KEYWORDS
Regular Expression, Programming by Example, Program Repair

Permission to make digital or hard copies of part or all of this work for personal orclassroom use is granted without fee provided that copies are not made or distributedfor profit or commercial advantage and that copies bear this notice and the full citationon the first page. Copyrights for third-party components of this work must be honored.
For all other uses, contact the owner/author(s).
ASE ’24, October 27-November 1, 2024, Sacramento, CA, USA© 2024 Copyright held by the owner/author(s).
ACM ISBN 979-8-4007-1248-7/24/10
https://doi.org/10.1145/3691620.3695005

ACM Reference Format:
Nariyoshi Chida and Tachio Terauchi. 2024. Repairing Regex-Dependent
String Functions. In 39th IEEE/ACM International Conference on AutomatedSoftware Engineering (ASE ’24), October 27-November 1, 2024, Sacramento, CA,
USA. ACM, New York, NY, USA, 12 pages. https://doi.org/10.1145/3691620.
36950051

INTRODUCTION

Modern programming languages provide various built-in string
functions that take regular expressions (regexes) as parameters.
Such regex-dependent string functions include repalceAll, which
replaces all substrings matched to the given regex with possiblydifferent strings, and search, which finds a substring matched to thegiven regex. These regex-dependent string functions play an important role in string manipulations in programs. For example, they
are used for sanitizing untrusted substrings [33, 34], parsing [11],and extracting substrings [29, 31]. Despite the importance, writing
regex-dependent string functions is far from an easy task and is acommon source of bugs in software [23, 32, 43].
In response, researchers have developed automated methods forsynthesizing regexes based on Programming By Examples (PBE) [12,17, 18, 25, 28, 35, 42, 45]. However, despite the advances made bythese works, there is still a gap between them and synthesizing
regex-dependent string functions.
Substring Matching: Although the prior works focus on wholestring matching, most regex-dependent string functions adopt substring matching. Therefore, even if we synthesize a regex using
the existing methods, there is no guarantee that the regex matches
the intended substrings when we use it through regex-dependent
string functions.
Replacement: Commonly used regex-dependent string functions for string transformations such as replace and replaceAll takeas parameter a replacement to specify how to replace the substrings
matched by the given regex. Since the behavior of replaceAll depends on both the regex and the replacement, it is not possible tosynthesize regex-dependent string functions by focusing only on
one of them.
In this paper, we fill the gap by proposing the first PBE-basedalgorithm for repairing regex-dependent string functions. For space,most of the paper focuses on replaceAll, one of the most popular
regex-dependent string functions [11]. However, the core ideas
are easily applicable to the other regex-dependent string functions
such as replace and search (cf. Sec. 6). Our algorithm takes a setof examples that describe the desired input-output of the function
to be synthesized, and the goal is to find a pair of a regex and areplacement such that replaceAll using the pair as the parametersbehaves consistently with the examples. To bias the solution to theuser-intended one, our algorithm can be given a "pre-repair" pairof a regex and a replacement as an additional input so that the goal

ASE ’24, October 27-November 1, 2024, Sacramento, CA, USA

is not only to find the parameters consistent with the examples but
to find one that is syntactically close to the given pre-repair ones.
Like the recent methods for regex synthesis, our algorithm builds
on enumerative search with pruning and SMT constraint solving,
but with extensions to support substring matching and replacement. The main challenge is the large search space. We address thechallenge by novel ideas such as incorporation of origin informationin examples to identify the locations of substrings to be matched,a new substring-context-aware pruning technique, and a novel useof SMT constraints to insert captures that can be referred from thereplacement. Additionally, we identify a novel necessary and sufficient condition that can be used to detect and filter unrepairable
instances.
We have implemented our algorithm as a tool called R2-DS (Repairer for Regex-Dependent String functions). R2-DS is designed
for JavaScript. This is needed because different regex engines often have different semantics that give different behavior to regexdependent string functions, and we have to pick one for concreteness. However, we think that the core ideas of the paper are applicable to regex-dependent string functions in others such as Python
and Java. We evaluated R2-DS on real-world benchmarks collectedfrom GitHub and StackOverflow. Results show that R2-DS canfind a high-quality repair efficiently. In summary, we make thefollowing contributions.
• We introduce the replaceAll-repair problem, which is thefirst problem of repairing replaceAll function from examples.
Concretely, we incorporate origin information in examples
to help specifying the user’s intention and reasoning about
the repair easier (Sec. 4.1), define a novel origin semantics
of replaceAll functions (Sec. 4.2), and with them, formallydefine the repair problem (Sec. 4.3).
• We show that, in contrast to the repair problems for regexes
studied in prior works, our repair problem has instancesthat do not have a solution. Additionally, we show a novel
necessary and sufficient condition for our repair problem
instance to have a solution (Sec. 4.4).
• We propose the first PBE-based algorithm for repairing replaceAll functions (Sec. 5). Our algorithm supports substring
matching and replacement. Especially, our algorithm incorporates a new substring-context-aware pruning technique and a novel use of SMT constraints to insert captures. We show that our ideas are applicable to the otherregex-dependent string functions such as replace and search(Sec. 6).
• We implement our algorithm in a tool called R2-DS and evaluate it on real-world benchmarks (Sec. 7). Results show that
R2-DS can efficiently repair the real-world bugs of regexdependent string functions. We also conduct an ablation
study which shows usefulness of the newly introduced techniques of context-aware pruning and SMT-constraint-based
insertion of captures.

2

OVERVIEWIn this section, we give an example, inspired by StackOverflow
posts [39, 40], to illustrate how the users represent their intentions
using our examples, and how R2-DS solves the repair problem.

Chida and Terauchi

Motivating Example. The user wants to replace all substringsof the form [𝑥]𝑦 [𝑥], where 𝑥 and 𝑦 are strings, with 𝑥 : 𝑦, unlesspreceded by the character #. For example, the user wants to replace the text "[a]ab[a], [b]c[a]" with "a:ab, [b]c[a]" andthe text "#[b]de[b], [a]c[a]" with "#[b]de[b], a:c". For thispurpose, the user prepared the regex (?<!#)\[(1 .∗ )1 \].∗ \[\1\] andthe replacement $1:$2 as parameters of replaceAll. Roughly, replaceAll functions behave like the following. For an input string
𝑤 with the regex reg and the replacement rep, it tries to match reg
at each position of 𝑤 from left to right. If the matching succeeds,
it replaces the matched substring with a string obtained from rep,and otherwise, it does nothing, and the character at the position
remains. The user prepared \[(1 .∗ )1 \].∗ \[\1\] to find substringsof the form [𝑥]𝑦 [𝑥], where \[ and \] match the characters [ and ],respectively, .∗ matches any string, and the backreference \1 refers
to the string matched by the capturing group (1 .∗ )1 . Additionally,
to rule out substrings preceded by #, the regex checks the context
using the negative lookbehind (?<!#). The user prepared $1:$2 toconstruct 𝑥 : 𝑦 by referring to 𝑥 and 𝑦 of the matched substring[𝑥]𝑦 [𝑥] using references $1 and $2.
Unfortunately, there are bugs in these user-prepared parameters.
First, the user prepared the reference $2 to refer to the substring
matched to the second .∗ , but forgot to write a capturing groupwhose index is 2. Therefore, the unassigned reference $2 is treatedas just the string $2. Second, the second .∗ matches the substring"ab[a], [b]c" of the first text and not the intended substring "ab",due to the behavior of regex engines. Consequently, for the two
texts, the outputs of replaceAll with the user-prepared parameters are "a:$2" and "#[b]de[b], a:$2", respectively, which are
undesired.
Repair Problem. Our tool R2-DS can automatically repair the
bugs by solving the replaceAll-repair problem. The repair problem
takes a regex reg, a replacement rep, and a set E of examples, whichreflect the user’s intention about the repair. The solution is a pairof a regex reg ′ and a replacement rep′ such that replaceAll using
the pair as the parameters behaves consistently with the examples
in E and the pair is syntactically close to the given pre-repair ones,or ⊥, meaning that there is no solution for the given instance. The
examples describe a desired input-output relation of the function
to be synthesized. We write an example as 𝑤𝑖𝑛 ⇝ 𝑤𝑜𝑢𝑡 , where 𝑤𝑖𝑛
and 𝑤𝑜𝑢𝑡 are the input and output with origin information. Origin
information is denoted by L𝑖 and M𝑖 , and L𝑖 𝑤M𝑖 in the input (resp.
output) indicates that 𝑤 is the 𝑖th substring matched to the regex(resp. obtained from the replacement). For example, L1𝑎M1𝑎L2𝑎M2 ⇝L1𝑋 M1𝑎L2𝑋 M2 means that the user wants to replace the input 𝑎𝑎𝑎
with the output 𝑋𝑎𝑋 by replacing the first and the last characters 𝑎with 𝑋 . In the case of the motivating example, the user may prepare
the examples "L1 [a]ab[a]M1 , [b]c[a]⇝L1 a:abM1 , [b]c[a]" and"#[b]de[b], L1 [a]c[a]M1 ⇝#[b]de[b], L1 a:cM1 ". Note that, in
PBE scenarios, the number of examples should be small for usability.
Repair Algorithm. R2-DS first checks whether the given instance has a solution, and if no then it outputs ⊥ and halts immediately. Otherwise, it starts the repair process. The instance inour running example has a solution, and therefore, R2-DS moves
on to the repair process. Roughly, the repair process iterates thefollowing steps until it finds a solution: enumerating templates(Searching Templates) and checking whether the templates can beRepairing Regex-Dependent String Functions

instantiated into a solution using SMT constraint solving (SMT
Constraint Solving).
Searching Templates. R2-DS enumerates pairs of regex and replacement templates. A regex (resp. replacement) template is a regex(resp. replacement) with holes, denoted by □. A hole is a placeholder
to be replaced with a concrete expression. Intuitively, it represents apart that is currently under repair. To enumerate the templates, R2DS changes the structures of regex and replacement templates byadding, reducing, and expanding holes. After some iterations, R2-DS
finds the pair of the templates ((?<!#)\[(1 .∗ )1 \]□∗ \[\1\], $1:□).
SMT Constraint Solving. R2-DS checks whether or not the
template can be instantiated into a solution by replacing the holes
in the regex template with a character set and replacing the holes
in the replacement template with a character or a reference withinsertions of capturing groups into a regex as needed. To checkthis, R2-DS prepares variables that correspond to the holes in thetemplates, and constructs an SMT constraint 𝜙 over the variables
such that 𝜙 is satisfiable iff there is an instantiation of the regex
and replacement templates that satisfy the examples. A subtle point
here is that our constraints encode the information about insertionsof capturing groups. We do this by inserting a virtual capturinggroup at each subexpression of the regex template to keep trackof the substring matched by the subexpression, and refer to theinformation in the part of the constraint for replacement templates
to decide whether we actually should insert the capturing groups.
Next, R2-DS checks the satisfiability of the constraint using an
SMT solver. If satisfiable, it constructs the regex and the replacement
pair from the satisfying assignment. Otherwise, it moves on to thetemplate pruning to reduce the search space. Our pruning techniquebuilds on the existing techniques for regex synthesis [12, 17, 18,
28, 35]; Namely, we build over- and under-approximations fromthe templates and check whether the approximations correctlyclassify the examples. However, we extend them to be context-aware(cf. Sec. 5.3 for details).
In the case of the above templates, the SMT constraint is satisfiable. From the satisfying assignment to the constraint, we obtain theregex (?<!#)\[(1 .∗ )1 \](2 [ˆ␣,\[\]] ∗ )2 \[\1\] and the replacment$1:$2. Note that the regex template was instantiated by replacing
its hole with the character set [ˆ␣,\[\]] that accepts any character except for the white space ␣ and the characters ,, [, and ], thereplacement template was instantiated by replacing its hole with
the new reference $2, and a capturing group corresponding to the
new reference was inserted at an appropriate subexpression of theregex.

3

PRELIMINARIESThis section briefly reviews the syntax and the semantics of regexes.
Since there are several variants of regexes in practice [5, 13, 20], we
focus on those of JavaScript, a popular programming language forbuilding web applications with regex-dependent string functions.
Specifically, this paper follows the semantics of regexes and regexdependent string functions of the ECMAScript® 2023 Language
Specification [22]. We first introduce the notations used in thepaper.
General Notation. We write N for the set of natural numbers
not including 0, N0 for N ∪ {0}, [𝑖..𝑗] for the set {𝑖, 𝑖 + 1, · · · , 𝑗 }ASE ’24, October 27-November 1, 2024, Sacramento, CA, USA

where 𝑖, 𝑗 ∈ N and 𝑖 ≤ 𝑗, [𝑖] for [1..𝑖], and · for the concatenation ofsequences. We will omit · if it is clear from context. For a sequence𝑙, we write |𝑙 | for its length, and for 𝑖, 𝑗 ∈ {0, 1, · · · , |𝑙 | − 1} with𝑖 ≤ 𝑗, 𝑙 [𝑖] for the 𝑖th element, 𝑙 [𝑖..𝑗] for 𝑙 [𝑖] · 𝑙 [𝑖 + 1] · · · 𝑙 [ 𝑗], and𝑙 [𝑖..𝑗) for 𝑙 [𝑖..𝑗 − 1] if 𝑖 ≤ 𝑗 − 1 and otherwise, i.e., if 𝑖 > 𝑗 − 1, 𝜖.
We use _ to omit unimportant elements. For a function 𝑓 , we use
𝑑𝑜𝑚(𝑓 ) to denote the domain of 𝑓 .
Regex. Let us fix a finite alphabet Σ. The syntax of regexes isdefined:𝑟::=[𝐶] | 𝜖 | 𝑟 · 𝑟 | 𝑟 |𝑟 | 𝑟 {𝑖, 𝑗 } | 𝑟 {𝑖, 𝑗 }? |(𝑘 𝑟 )𝑘 | \𝑘 | (?=𝑟 ) | (?!𝑟 ) | (?<=𝑟 ) | (?<!𝑟 ), where 𝐶 ⊆ Σ, 𝑖 ∈ N0 , 𝑗 ∈ N0 ∪ {∞} with 𝑖 ≤ 𝑗, and 𝑘 ∈ N.
Here, 𝑖 ≤ ∞ for all 𝑖 ∈ N0 . [𝐶] is a character set, which matches acharacter in 𝐶. For readability, we write 𝑎 for [{𝑎}], [𝑎𝑏 · · · 𝑐] for[{𝑎, 𝑏, · · · , 𝑐}], . for [Σ], and [ˆ𝐶] for [Σ \ 𝐶]. The operators 𝜖 and𝑟 ·𝑟 (or just 𝑟𝑟 when there is no ambiguity) are the empty string andthe concatenation, respectively, and their semantics are standard.
The operator 𝑟 1 |𝑟 2 is the deterministic union that first tries to match
𝑟 1 , and if the whole matching cannot succeed with 𝑟 1 , then it tries
to match 𝑟 2 . The operator 𝑟 {𝑖, 𝑗 } (resp. 𝑟 {𝑖, 𝑗 }? ) is the greedy (resp.
lazy) bounded repetition, which tries to match 𝑟 at least 𝑖 times andat most 𝑗 times as many (resp. few) as possible if 𝑗 ∈ N0 . When𝑗 = ∞, it tries to match 𝑟 at least 𝑖 times as many (resp. few) as
possible. From these operators, we can construct other quantifiers
as syntactic sugar: 𝑟 ∗ = 𝑟 {0, ∞}, 𝑟 ∗? = 𝑟 {0, ∞}? , 𝑟 + = 𝑟 {1, ∞},𝑟 +? = 𝑟 {1, ∞}? , 𝑟 ? = 𝑟 {0, 1}, and 𝑟 ?? = 𝑟 {0, 1}? .
The remaining operators are real-world extensions. The operators (𝑘 𝑟 )𝑘 and \𝑘 are the capturing group and the backreference,
respectively. The capturing group (𝑘 𝑟 )𝑘 tries to match 𝑟 and, if thematching succeeds, it stores the matched substring into an environment with the index 𝑘. An environment Γ is a mapping froman index 𝑘 to the substring matched to the 𝑘th capturing group.
The backreference \𝑘 refers to the substring matched to the corresponding capturing group (𝑘 𝑟 )𝑘 . If there is no such substring (i.e.,𝑘 ∉ 𝑑𝑜𝑚(Γ)), \𝑘 is evaluated to an empty string 𝜖. Also, we assume
that every capturing group in a regex has a unique index. That is,
our semantics follows 𝜖- and no-label-repetition-semantics [5], andthis is actually consistent with the ECMAScript® Language Specification. The operators (?=𝑟 ) and (?!𝑟 ) are positive and negative
lookaheads, respectively, which try to match 𝑟 without any character consumption, such that (?=𝑟 ) (resp. (?!𝑟 )) succeeds if 𝑟 succeeds(resp. fails). The operators (?<=𝑟 ) and (?<!𝑟 ) are positive and negative lookbehinds, respectively. They are analogous to lookaheads,
but with the direction of the matching reversed, i.e., lookbehinds
try to match from right to left.
We next briefly review the semantics of regexes. In this paper,
we use the formal semantics defined by Chida and Terauchi [18]for repairing regexes that follows the ECMAScript® 2023 Language
Specification. The semantics is defined as the deterministic matching relation (𝑟, 𝑤, 𝑝) ⇓ 𝑥, where 𝑥 ∈ {(𝑝 ′, Γ ′ ), failed}.1 Roughly,
this states that if 𝑥 = (𝑝 ′, Γ ′ ), then the matching of 𝑟 on the input
string 𝑤 at the position 𝑝 succeeds, changes the position 𝑝 to 𝑝 ′ , andcaptures substring as described by the environment Γ ′ . If 𝑥 = failed,
1We use a simplified version of the relation introduced in [18]. This corresponds tothe judgement (𝑟, 𝜖, 𝑤, 𝑝, ∅, forward, true) ⇓ _, where 𝜖 is a continuation regex, ∅ isan environment, forward is a direction of the matching, and true is a flag, in [18].

ASE ’24, October 27-November 1, 2024, Sacramento, CA, USA

it means that the matching fails at that state. We do not describe therules of the relation in this paper and refer interested readers to [18]for full details. As pointed out in [38], the semantics introduced in[18] handles option operators 𝑟 ? and 𝑟 ?? incorrectly. To ensure thecorrectness, we correct the bug by introducing bounded repetitions
that were not considered in [18], extending the semantics of [18]with rules for them, and encoding options by them as mentioned
above. The details can be found in the long version of this paper.

4

THE REPAIR PROBLEM

In this section, we define the replaceAll-repair problem. We first
define in Sec. 4.1 strings with origin information and with them
define examples for the problem. Next in Sec. 4.2, we define an
origin semantics of replaceAll functions and formally define what itmeans for a regex and a replacement to be consistent with examples.
In Sec. 4.3, we define the repair problem and show that it has
unsolvable instances. Finally, we identify a necessary and sufficientcondition for a problem instance to have a solution in Sec. 4.4.

4.1

String with Origin Information

A string with origin information is a pair (𝑤, 𝜂) where 𝑤 is a stringand 𝜂 is a list of pairs of integers of the form [(𝑝 1, 𝑝 1′ ), (𝑝 2, 𝑝 2′ ), · · · ,(𝑝𝑛 , 𝑝𝑛′ )] for some 𝑛 ∈ N0 (𝜂 = 𝜖 if 𝑛 = 0) satisfying 𝑝𝑖 , 𝑝𝑖′ ∈ N0 and𝑝𝑖 ≤ 𝑝𝑖′ for all 𝑖 ∈ [𝑛], 𝑝 ′𝑗 ≤ 𝑝 𝑗+1 for all 𝑗 ∈ [𝑛 − 1], and 𝑝𝑖 < 𝑝 𝑗 for
all 𝑖 < 𝑗 where 𝑖, 𝑗 ∈ [𝑛]. For a string with origin information (𝑤, 𝜂),each element 𝜂 [𝑖] = (𝑝, 𝑝 ′ ) of the origin information 𝜂 indicatesthe substring 𝑤 [𝑝..𝑝 ′ ). From this, we assume that 𝑝 ′ ≤ |𝑤 | foreach element. For readability, we use L𝑖 ·M𝑖 to denote a substring
represented by the 𝑖th element of 𝜂, i.e., 𝑤 [𝑝..𝑝 ′ ) for (𝑤, 𝜂) with
𝜂 [𝑖] = (𝑝, 𝑝 ′ ). For example, we represent the string with origin
information (𝑎𝑏𝑐𝑑, [(0, 1), (2, 3), (4, 4)]) as L1𝑎M1𝑏L2𝑐M2𝑑L3 M3 .
An example is a tuple (𝑤, 𝜂, 𝜃 ), where (𝑤, 𝜂) is a string with origin information and 𝜃 is output fragments which is a list of strings
such that |𝜂| = |𝜃 |. Here, 𝑤 is an input to replaceAll functions,and 𝜂 and 𝜃 describe how the output is obtained from the input.
Specifically, an example (𝑤, 𝜂, 𝜃 ) states that regexes of desired replaceAll functions should match only the substrings 𝑤 [𝑝, 𝑝 ′ ) for
each 𝜂 [𝑖] = (𝑝, 𝑝 ′ ) where 0 ≤ 𝑖 < |𝜂|, and the matched substrings
should be replaced with the output fragment 𝜃 [𝑖]. For instance, theexample (𝑎𝑏𝑎𝑐, [(0, 1), (2, 3)], [𝑑, 𝑑]) reflects the user’s intention
that for the given input 𝑎𝑏𝑎𝑐, desired replaceAll functions should
return the output 𝑑𝑏𝑑𝑐 whose first and second characters 𝑑 of theoutput originates from the first and second characters 𝑎 of the input, respectively. Hereafter, we use output(𝑤, 𝜂, 𝜃 ) to denote theoutput obtained from 𝑤 by replacing all substrings 𝑤 [𝑝, 𝑝 ′ ), where𝜂 [𝑖] = (𝑝, 𝑝 ′ ), with 𝜃 [𝑖]. Also, for readability, we use 𝑤𝑖𝑛 ⇝ 𝑤𝑜𝑢𝑡
to denote an example (𝑤, 𝜂, 𝜃 ), where 𝑤𝑖𝑛 is the string with origin
information (𝑤, 𝜂) and 𝑤𝑜𝑢𝑡 is the string with origin information obtained from 𝑤 by replacing all occurrences L𝑖 𝑤 ′ M𝑖 of 𝑤𝑖𝑛 with L𝑖 𝜃 [𝑖−1]M𝑖 . For instance, we write the above example as L1𝑎M1𝑏L2𝑎M2𝑐 ⇝L1𝑑M1𝑏L2𝑑M2𝑐 and output(𝑎𝑏𝑎𝑐, [(0, 1), (2, 3)], [𝑑, 𝑑]) = 𝑑𝑏𝑑𝑐.

4.2

Origin Semantics

We first review the replaceAll function and then give its origin
semantics. The replaceAll function takes a string 𝑤, a regex reg, anda replacement rep, and returns a string by replacing the substrings

Chida and Terauchi

𝑝 < |𝑤 | (reg, 𝑤, 𝑝) ⇓ (𝑝 ′, Γ) JrepK Γ = 𝑥
𝑝 ′′ = ite(𝑝 ′ ≠ 𝑝, 𝑝 ′, 𝑝 + 1)
(𝑤, 𝑝 ′′, reg, rep) ↩→ (𝑤 ′, 𝜂)(𝑤, 𝑝, reg, rep) ↩→ (𝑥 · 𝑤 ′, [(𝑝, 𝑝 ′ )] · 𝜂)
𝑝 = |𝑤 |(reg, 𝑤, 𝑝) ⇓ (𝑝 ′, Γ)

JrepK Γ = 𝑥(𝑤, 𝑝, reg, rep) ↩→ (𝑥, [(𝑝, 𝑝 ′ )])𝑝 < |𝑤 |(reg, 𝑤, 𝑝) ⇓ failed(𝑤, 𝑝 + 1, reg, rep) ↩→ (𝑤 ′, 𝜂)(𝑤, 𝑝, reg, rep) ↩→ (𝑤 [𝑝] · 𝑤 ′, 𝜂)
𝑝 = |𝑤 |(reg, 𝑤, 𝑝) ⇓ failed(𝑤, 𝑝, reg, rep) ↩→ (𝜖, [])Figure 1: Rules for replaceAll. The function ite is defined by:ite(true, 𝐴, 𝐵) = 𝐴 and ite(false, 𝐴, 𝐵) = 𝐵.
matched to reg with the strings constructed from rep. Replacements
are defined by the following syntax: 𝑠 ::= 𝜖 | 𝑎 | $𝑖 | 𝑠 · 𝑠, where 𝜖is the empty string, 𝑎 is a character, $𝑖 is a reference, and 𝑠 · 𝑠 is aconcatenation. A reference is of the form $𝑖 where 𝑖 ∈ N, and like abackreference of regexes, it refers to the substring associated with
the index 𝑖 in an environment Γ, i.e., Γ(𝑖). Hereafter, we refer toreplaceAll(reg, rep) as replaceAll with the regex parameter reg andthe replacement parameter rep.
The origin semantics of replaceAll is defined as the relation(𝑤, 𝑝, reg, rep) ↩→ (𝑤 ′, 𝜂), where 𝑤 and 𝑤 ′ are strings, 𝑝 is a position in 𝑤, reg is a regex, rep is a replacement, and 𝜂 is an origin
information. Roughly, the relation (𝑤, 𝑝, reg, rep) ↩→ (𝑤 ′, 𝜂) statesthat running replaceAll(reg, rep) on 𝑤 from the position 𝑝 outputs
the string with origin information (𝑤 ′, 𝜂).
Figure 1 shows the rules defining the semantics. Here, we use
the deterministic matching relation (reg, 𝑤, 𝑝) ⇓ _ described inSec. 3 to obtain the results of regex matching. JrepK Γ denotes thestring constructed from the replacement rep under the environment
Γ. Formally, it is defined by: J𝜖K Γ = 𝜖, J𝑎 · repK Γ = 𝑎 · (JrepK Γ),
and J$𝑖 · repK Γ = Γ(𝑖) · (JrepK Γ). Here, we let Γ(𝑖) = 𝜖 if 𝑖 ∉𝑑𝑜𝑚(Γ).2 There is a rule per each of the following four situations:the matching (reg, 𝑤, 𝑝) succeeds or not and the position is the endof the input string or not. If the matching succeeds, i.e., (reg, 𝑤, 𝑝) ⇓(𝑝 ′, Γ), then the function appends the string JrepK Γ and the origin
information (𝑝, 𝑝 ′ ) to the output, and continues the replacementfrom the position 𝑝 ′ if 𝑝 ≠ 𝑝 ′ and 𝑝 + 1 if 𝑝 = 𝑝 ′ . If the matching
fails, it appends the character 𝑐 to the output, where 𝑐 = 𝑤 [𝑝] if
𝑝 < |𝑤 | and otherwise 𝑐 = 𝜖, and continues the matching from theposition 𝑝 + 1. If the position 𝑝 reaches the end of 𝑤, i.e., 𝑝 = |𝑤 |, it
behaves similarly to the above rules, but the replacement ends.
Example 4.1. Consider the evaluation of replaceAll(𝑎(?=(1 .)1 ),𝑋 $1𝑋 ) on the input string 𝑎𝑏. The derivation tree is as follows.
Here, 𝐴𝑖 denotes (𝑎(?=(1 .)1 ), 𝑎𝑏, 𝑖) for 𝑖 ∈ {0, 1}.
2 This differs from the actual behavior of replaceAll in ECMAScript. Namely, in theactual replaceAll, if a reference 𝑖 is unassigned (i.e., 𝑖 ∉ 𝑑𝑜𝑚 (Γ) ), the string constructedfrom $𝑖 depends on the regex. Specifically, if the number of capturing groups in theregex is less than 𝑖 , $𝑖 is evaluated to the string $𝑖 ; otherwise, it is evaluated to 𝜖 .
Although it is easy to modify the rules to follow the actual behavior, for simplicity,
our rules always evaluate unassigned references to 𝜖 . Note that if one wants to write
the string $𝑖 in a replacement, they can do so without using an unassigned referenceby writing $$𝑖 [22].

Repairing Regex-Dependent String Functions···
𝐴0 ⇓ (1, {(1, 𝑏)})
J𝑋 $1𝑋 K {(1, 𝑏)} = 𝑋𝑏𝑋
𝐵(𝑎𝑏, 0, 𝑎(?=(1 .)1 ), 𝑋 $1𝑋 ) ↩→ (𝑋𝑏𝑋𝑏, [(0, 1)])The subderivation 𝐵 is as follows.
···
𝐴1 ⇓ failed(𝑎𝑏, 2, 𝑎(?=(1 .)1 ), 𝑋 $1𝑋 ) ↩→ (𝜖, [])(𝑎𝑏, 1, 𝑎(?=(1 .)1 ), 𝑋 $1𝑋 ) ↩→ (𝑏, [])That is, for the input string 𝑎𝑏, replaceAll(𝑎(?=(1 .)1 ), 𝑋 $1𝑋 ) replaces the substring 𝑎 with the string 𝑋𝑏𝑋 and leaving the otherparts unchanged.
We are now ready to define the notion of consistency with examples.
Definition 4.2 (Consistency). We say that replaceAll(reg, rep) is
consistent with (or, satisfies) an example (𝑤, 𝜂, 𝜃 ) if (𝑤, 0, reg, rep) ↩→(output(𝑤, 𝜂, 𝜃 ), 𝜂). For a set of examples E, we say that replaceAll(reg,rep) satisfies the set of examples if it satisfies all examples in E.
For instance, replaceAll(𝑎(?=(1 .)1 ), 𝑋 $1𝑋 ) satisfies the example(𝑎𝑏, [(0, 1)], [𝑋𝑏𝑋 ]) because output(𝑎𝑏, [(0, 1)], [𝑋𝑏𝑋 ]) = 𝑋𝑏𝑋𝑏
and (𝑎𝑏, 0, 𝑎(?=(1 .)1 ), 𝑋 $1𝑋 ) ↩→ (𝑋𝑏𝑋𝑏, [(0, 1)]).

4.3

Problem Formulation

Before we define the repair problem, we consider a metric to measure the quality of a repair. We base our metric on those from theprior works for regex synthesis [17, 18, 35]. They used a notion
called edit distance between two regexes so that a regex of a shortdistance from a pre-repair regex is deemed to be of high quality.
The metric is justified by the assumption that the pre-repair regex
may be incorrect but close to the intended one. Like the prior works,
we deem parameters (i.e., a regex and a replacement) of a shortdistance from pre-repair parameters to be high quality. Since weconsider repairing a replacement in addition to a regex, we use thesum of edit distances of the two as the metric, but with a certain
modification on the definition of edit distance regarding insertionsof capturing groups.
Definition 4.3 (Capture-insertion relation). Given a set of integers
𝐼 , we define the relation ⇒𝐼 over regexes where 𝑟 ⇒𝐼 𝑟 ′ iff it ispossible to rewrite 𝑟 to 𝑟 ′ using associativity of the binary operators (i.e., the concatenation and the union) and inserting capturinggroups (𝑖 ·)𝑖 where 𝑖 ∉ 𝐼 .
As explained below, the relation plays the role of inserting capturing groups into a regex at no cost. Let |𝑟 | denote the number of
AST nodes of 𝑟 .
Definition 4.4 (Edit Distance). For subtrees 𝑟 1, 𝑟 2, · · · , 𝑟𝑛 of a regex
𝑟 , the edit 𝑒 = 𝑟 [𝑟 1′ /𝑟 1, · · · , 𝑟𝑛′ /𝑟𝑛 ] replaces 𝑟𝑖 with 𝑟𝑖′ where 𝑖 ∈ [𝑛].
Í
The cost of the edit is 𝑖 ∈ [𝑛] , |𝑟𝑖 | + |𝑟𝑖′ |. Then, for two regexes 𝑟 1
and 𝑟 2 , the edit distance between 𝑟 1 and 𝑟 2 is the minimum cost ofan edit that rewrites 𝑟 1 to some 𝑟 2′ s.t. 𝑟 2′ ⇒𝐼 𝑟 2 where 𝐼 is the setof indexes of capturing groups and backreferences in 𝑟 2′ .
We lift the edit distance to replacements by interpreting a replacement as a regex consisting of a character set, a backreference,
and a concatenation. Then, the edit distance between two parameters 𝑓1 = (reg 1, rep1 ) and 𝑓2 = (reg 2, rep2 ), denoted 𝐷 (𝑓1, 𝑓2 ), is𝑑 reg + 𝑑 rep , where 𝑑 reg (resp. 𝑑 rep ) is the edit distance between reg 1
and reg 2 (resp. rep1 and rep2 ). For example, for 𝑓1 = (𝑎 · 𝑏 · 𝑐, 𝑑 · 𝑒)

ASE ’24, October 27-November 1, 2024, Sacramento, CA, USA

and 𝑓2 = (𝑒 ∗ · (1𝑏 · 𝑐)1, 𝑑 · 𝑓 · $1), 𝐷 (𝑓1, 𝑓2 ) = 7 because the edit
distance between the regexes is 3 (i.e., the cost of replacing 𝑎 with𝑒 ∗ ) and the edit distance between the replacements is 4 (i.e., thecost of replacing 𝑒 with 𝑓 · $1). Note that there is no cost to insert a
capturing group into 𝑏 · 𝑐 because 𝑒 ∗ · 𝑏 · 𝑐 ⇒ ∅ 𝑒 ∗ · (1𝑏 · 𝑐)1 .
Note that edit distance used in prior works [17, 18, 35] is a restriction of Definition 4.4 obtained by asserting 𝑟 2′ = 𝑟 2 , i.e., it is
the minimum cost of an edit that rewrites 𝑟 1 to 𝑟 2 . We extend theprior definition by the capture-insertion relation because insertionsof capturing groups are quite common in practice (e.g., [39, 41])but the prior definition allots high costs to such an insertion as it
would be represented by a replacement of 𝑟 to (𝑖 𝑟 )𝑖 which costs
2· |𝑟 | +1. We refer to the long version of this paper for further details
including real-world cases that motivated our new definition.
It is worth noting that we can compute the minimum edit distances efficiently by treating binary operators as 𝑛-ary operatorsand computing the normal form. For example, ·(𝑎, 𝑏, 𝑐) is the uniquenormal form of both (𝑎 · 𝑏) · 𝑐 and 𝑎 · (𝑏 · 𝑐).
We now define the repair problem.
Definition 4.5 (The Repair Problem). Given a regex reg, a replacement rep, and a set of examples E, the replaceAll-repair problem isthe problem of synthesizing a pair 𝑓2 = (reg ′, rep′ ) of a regex anda replacement such that 𝑓2 satisfies E and the distance between
𝑓1 = (reg, rep) and 𝑓2 is minimal, i.e., for any 𝑓3 = (reg ′′, rep′′ ) thatsatisfies E, 𝐷 (𝑓1, 𝑓2 ) ≤ 𝐷 (𝑓1, 𝑓3 ).
Our repair problem is NP-hard. The proof is by a reduction fromthe extraction-regex-repair problem [18] that is known as NP-hard.
We show the proof in the long version of this paper.
Theorem 4.6. The repair problem is NP-hard.
While a PBE regex repair or synthesis problem often has theguarantee that every instance has some solution [17, 18, 35], ourproblem has unsolvable instances.
Theorem 4.7. The repair problem has an unsolvable instance.
Proof. There is no pair of a regex and a replacement that satisfies the set of examples E = {L1𝑎M1 ⇝ L1𝑏M1, L1𝑐M1 ⇝ L1𝑑M1 }. To
see this, note that the output fragments require that the replacement
should be evaluated to the different characters 𝑏 and 𝑑 dependingon the input string, and so, the replacement must have a reference.
However, a reference can only refer to the characters that appear
in the inputs, but these characters do not appear in the inputs.
Therefore, there is no replacement that satisfies the examples. □4.4

Necessary and Sufficient Condition

We now turn to identifying a necessary and sufficient condition
for a problem instance to have a solution. We first introduce somenotations. We use 𝑜𝑢𝑡 (E) to denote the set of all output fragments
in E, i.e., 𝑜𝑢𝑡 (E) = {𝑤 ∈ Σ∗ | (_, _, 𝜃 ) ∈ E ∧ 𝜃 [𝑖] = 𝑤 for some 𝑖}.
Also, we define the function filter(𝑤, 𝑤 ′ ) that returns a string obtained from 𝑤 by replacing all characters that appear in 𝑤 ′ with 𝜖.
For example, filter(𝑎𝑏𝑐𝑑𝑒𝑏, 𝑏𝑑) = 𝑎𝑐𝑒. We say that 𝑣 is a scatteredsubstring of 𝑤 if 𝑤 = 𝑤 1 · 𝑣 [0] · 𝑤 2 · 𝑣 [1] · · · 𝑤𝑚 · 𝑣 [|𝑣 | − 1] · 𝑤𝑚+1 .
We now show the condition.
Theorem 4.8. A repair problem instance (reg, rep, E) is solvable
if and only if the following holds: There exists a string 𝑤 ∈ Σ∗ s.t. forASE ’24, October 27-November 1, 2024, Sacramento, CA, USA

Algorithm 1: The Repair Algorithm
Input: Regex reg, Replacement rep, Set of Examples E
Output: Solution (reg ′, rep′ ) or ⊥ if there is no solution
1: if isSolvable(E) = false then2:
return ⊥3: 𝑄 ← {(reg, rep)}
4: while 𝑄 is not empty do
5:(𝑡 reg , 𝑡 rep ) ← 𝑄.𝑝𝑜𝑝 ()6:
if isFeasible(𝑡 reg ) = true ∧ isFeasible(𝑡 rep ) = true then7:
if preTest(𝑡 reg ) = true ∧ preTest(𝑡 rep ) = true then8:
𝜙 ← genConst(𝑡 reg , 𝑡 rep , E)
9:if 𝜙 is satisfiable then10:
(reg ′, rep′ ) ← completion(𝑡 reg , 𝑡 rep , 𝜙)11:
return (reg ′, rep′ )12:𝑄.𝑝𝑢𝑠ℎ(expandHole(𝑡 reg , 𝑡 rep ))13:
𝑄.𝑝𝑢𝑠ℎ(addOrReduceHole(𝑡 reg , 𝑡 rep ))all 𝑤 ′ ∈ 𝑜𝑢𝑡 (E), 𝑤 is a scattered substring of 𝑤 ′ and filter(𝑤 ′, 𝑤𝑖𝑛 )is a scattered substring of 𝑤, where 𝑤𝑖𝑛 is the input string of 𝑤 ′ .
This condition rules out unsolvable instances. For instance, let us
consider the set of examples {L1𝑎M1 ⇝ L1𝑎𝑏M1, L1𝑎𝑎M1 ⇝ L1𝑎𝑏𝑏M1 }which does not satisfy the condition. To see that it is indeed unsolvable, note that from L1𝑎𝑎M1 ⇝ L1𝑎𝑏𝑏M1 , we can see that the
replacement of a solution must have 𝑏𝑏 in the subexpression. Thisis because the input 𝑎𝑎 does not contain 𝑏, and therefore, we cannot
use a reference to construct 𝑏𝑏. But then the output fragment of
the other example (i.e., L1𝑎𝑏M1 ) must have a substring 𝑏𝑏, which itdoes not.
The condition is also a sufficient condition. Roughly, this isshown by constructing a replacement that is consistent with all
output fragments by using references, and a regex that matches
correct substrings denoted by the origin information and extracts
substrings that are required by the references in the replacement.
We refer to the long version of this paper for the proof.
We emphasize that the condition is not only of theoretical interest but also useful in practice. For instance, let us consider the casewhere the user wants to replace all occurrences of **𝑥** in a Markdown document with <strong>𝑥</strong>, where 𝑥 is a string,e.g., replacing “**a** and **b**” with “<strong>a</strong> and<strong>b</strong>”. For this purpose, the user may prepare theexample:L1 **M1 aL2 **M2 and L3 **M3 bL4 **M4 ⇝L1 <strong>M1 aL2 </strong>M2 and L3 <strong>M3 bL4 </strong>M4 .

While the example may at first seem intuitive, it turns out that there
is no solution for this example. Indeed, the example violates thecondition stipulated in Theorem 4.8, and automatically detected soby the algorithm given in Sec. 5.1. The user can then try to comeup with a different example, e.g.,
L1 **a**M1 and L2 **b**M2 ⇝L1 <strong>a</strong>M1 and L2 <strong>b</strong>M2

which turns out to be solvable, and our tool is able to return a repair
that is consistent with the example.

Chida and Terauchi

5

THE REPAIR ALGORITHM

Algorithm 1 overviews our repair algorithm. Our algorithm takes
a repair problem instance (reg, rep, E). It outputs either a pair(reg ′, rep′ ) of a regex and a replacement that satisfies E and is minimal w.r.t. the edit distance from the input (reg, rep) or ⊥, meaningthat the given instance does not have a solution. Our algorithm consists of five steps: checking the necessary and sufficient condition(lines 1-2), initializing a template (line 3), pruning infeasible templates (lines 6-7), SMT constraint solving (lines 8-10), and templateenumeration (lines 12 and 13). We next explain each step.
Checking Necessary and Sufficient Condition. Our algorithm
first checks whether or not the given instance has a solution (line 1)
by checking the condition given in Theorem 4.8. If the check fails,
our algorithm immediately halts by outputting ⊥ (line 2). Otherwise,
it starts the repair process. The details are described in Sec. 5.1.
Initialize a Template. Our algorithm maintains a priority queue
𝑄 of pairs of a regex template and a replacement template. A regex(resp. replacement) template 𝑡 reg (resp. 𝑡 rep ) is a regex (resp. replacement) with hole □. A hole is a placeholder to be replaced with aconcrete regex (resp. replacement). During the repair process, ouralgorithm adds/expands/reduces the holes to change the structureof the templates (cf. Template Enumeration). As discussed in
Sec 4.3, we treat the concatenation and the union as 𝑛-ary operators in the templates. Entries in 𝑄 are ordered according to the edit
distance from the input regex and replacement pair in ascendingorder.3 This ensures the minimality of repaired parameters. Initially,
our algorithm pushes the input pair (reg, rep) into 𝑄 (line 3).
Pruning Infeasible Templates. Then, our algorithm retrieves
the top element (𝑡 reg , 𝑡 rep ) of 𝑄 (line 5), and uses lightweight techniques to prune infeasible regex and replacement templates andreduce the search space (line 6). We first describe the pruning
technique for regex templates. We define some terminologies. For(𝑤, 𝜂, 𝜃 ) ∈ E, we call the position 𝑖 in 𝑤 positive if there exists 𝑗 s.t.
𝜂 [ 𝑗] = (𝑝, 𝑝 ′ ) and 𝑝 ≤ 𝑖 ≤ 𝑝 ′ , and negative otherwise. Our pruning
technique checks for each (𝑤, 𝜂, 𝜃 ) ∈ E and positive position 𝑝 in
𝑤 s.t. 𝜂 [𝑖] = (𝑝, 𝑝 ′ ) (resp. negative position 𝑝), if 𝑡 reg cannot be
instantiated into a regex that matches the substring 𝑤 [𝑝, 𝑝 ′ ) (resp.
fails to match 𝑤 at 𝑝). If so, we do not need to consider 𝑡 reg or thetemplates obtained by expanding the holes in 𝑡 reg and so can safely
prune those templates. To check this, our technique constructs
context-aware over- and under-approximations of 𝑡 reg and checks
their matchings with the substrings at the positions. The pruning
technique is implemented by the predicate isFeasible(𝑡 reg ) whose
details are deferred to Sec. 5.3.
As for pruning replacement templates, recall that a replacement
can be seen as a regex composed of a character, a concatenation,
and a backreference. Therefore, we build an over-approximation𝑟 ⊤ from the replacement template by applying the methods fromthe prior work [17, 18, 35] and check whether the regex accepts
all output fragments, i.e., we check ∀𝑤 ∈ 𝑜𝑢𝑡 (E).𝑤 ∈ 𝐿(𝑟 ⊤ ). If thecheck fails, then we safely prune the template and any templates
obtainable by expanding the holes in it. The check is implemented
by the predicate isFeasible(𝑡 rep ).

3 The edit distance between templates is defined in the same manner as that of regexes

and replacements.

Repairing Regex-Dependent String Functions

SMT Constraint Solving. If the templates (𝑡 reg , 𝑡 rep ) pass thepruning, then our algorithm checks whether they can be instantiated into a regex and replacement pair that satisfies the examples
by replacing holes in the regex template with character sets andreplacing holes in the replacement template with characters orreferences. To check this, our algorithm constructs an SMT constraint that is satisfiable iff there exists such an instantiation (line 8).
The constraint contains the boolean variables that correspond tothe holes in the templates, and they represent the ways of fillingthe corresponding holes with concrete expressions. Therefore, if
the constraint is satisfiable, we can reconstruct the instantiationfrom the satisfying assignment. The details of the SMT constraint
generation method are discussed in Sec. 5.2.
After building the constraint, our algorithm checks its satisfiability using an off-the-shelf SMT solver such as Z3 [21] (line 9). If it
is satisfiable, our algorithm reconstructs a regex and replacement
pair from 𝑡 reg and 𝑡 rep using the assignments (line 10) as remarked
above, and applies the generalization method introduced in [35]that uses MaxSMT solving to the regex to enhance the quality of
the repair. Namely, it tries to replace character sets that filled theholes with common character sets such as [𝑎-𝑧], [𝐴-𝑍 ], and [0-9]while maintaining consistency with the examples. Note that thegeneralization process does not affect the edit distance.
Template Enumeration. If the templates (𝑡 reg , 𝑡 rep ) cannot
be a solution, our algorithm changes their structures to generate
additional templates. Specifically, our algorithm first expands a holein the templates (line 12) by replacing it with an expression whose
immediate subexpressions are holes. For example, let 𝑡 reg = 𝑎|□and 𝑡 rep = □ · 𝑏. Then, expandHole(𝑡 reg , 𝑡 rep ) = {(𝑎|𝜖, 𝑡 rep ), (𝑎|(□ ·□), 𝑡 rep ), · · · , (𝑎|(?<!□), 𝑡 rep )}∪{(𝑡 reg , □·□·𝑏)}. Next, our algorithm
adds a hole in the templates by replacing the leaf subexpression(i.e., a character set, 𝜖, or a backreference for regex templates anda character or a reference for replacement templates) with a hole(line 13). Additionally, our algorithm reduces an expression whose
immediate subexpressions are holes with a hole. For example, let𝑡 reg = □∗ ·𝑎 and 𝑡 rep = □·□·𝑏. Then, addOrReduceHole(𝑡 reg , 𝑡 rep ) ={(□∗ · □, 𝑡 rep ), (□ · 𝑎, 𝑡 rep ), (𝑡 reg , □ · □ · □), (𝑡 reg , □ · 𝑏)}. This part isessentially the same as the prior works on regex synthesis andrepair [17, 18, 35] with a straightforward adoption to replacement
templates, and therefore, we refer to them for more details.

5.1

Checking the Condition

Recall that the condition shown in Theorem 4.8 requires that there
exists a string 𝑤 ∈ Σ∗ such that for all output fragments 𝑤𝑜𝑢𝑡 ∈𝑜𝑢𝑡 (E), (i) 𝑤 is a scattered substring of 𝑤𝑜𝑢𝑡 and (ii) filter(𝑤𝑜𝑢𝑡 , 𝑤𝑖𝑛 )is a scattered substring of 𝑤, where 𝑤𝑖𝑛 is the input string of 𝑤𝑜𝑢𝑡 .
We show an efficient method for checking the condition. Our key
insight is that we can represent the strings that satisfy (i) and (ii) as
pure regexes (i.e., regexes that do not have lookarounds and backreferences), and check the existence of such a string 𝑤 by checking
the non-emptiness of the intersection of these pure regexes. Precisely, in the case of (i), for each 𝑤𝑜𝑢𝑡,𝑖 ∈ 𝑜𝑢𝑡 (E), we can constructa regex that defines the set of all scattered substrings of 𝑤𝑜𝑢𝑡,𝑖as 𝑟𝑖 = 𝑤𝑜𝑢𝑡,𝑖 [0] ? · · · 𝑤𝑜𝑢𝑡,𝑖 [|𝑤𝑜𝑢𝑡,𝑖 | − 1] ? . In the case of (ii), foreach 𝑤𝑜𝑢𝑡,𝑖 ∈ 𝑜𝑢𝑡 (E) and the corresponding input string 𝑤𝑖𝑛,𝑖 , let

ASE ’24, October 27-November 1, 2024, Sacramento, CA, USA

Algorithm 2: genConstForExample
Input: Regex Template 𝑡 reg , Replacement Template 𝑡 rep ,Example 𝑒 = (𝑤, 𝜂, 𝜃 )Output: SMT Constraint 𝜙
Ó
1: 𝜙 ← 𝑖 ∈ [𝑛] (Σ𝑏 ∈𝔅𝑖 𝑏 = 1)
2: for 𝑝 ∈ {0, 1, · · · , |𝑤 |} do3:
𝑆 reg ← compute𝑆 reg (𝑡 reg , 𝑤, 𝑝)
4:
if 𝑝 is positive and 𝜂 [ 𝑗] = (𝑝, 𝑝 ′ ) for some 𝑗 thenÔ5:
𝜙 ← 𝜙 ∧ (𝑝 ′ ,Γ ′ ,𝜙 ′ ) ∈𝑆 reg (𝜙 ′ ∧ Φrep (𝑡 rep , 𝜃 [ 𝑗], Γ ′ ))6:else if 𝑝 is negative thenÔ7:
𝜙 ← 𝜙 ∧ ¬( (_,_,𝜙 ′ ) ∈𝑆 reg 𝜙 ′ )8: return 𝜙filter(𝑤𝑜𝑢𝑡,𝑖 , 𝑤𝑖𝑛,𝑖 ) = 𝑤 𝑓 ,𝑖 . Then, we can construct a regex that defines the set of all strings that have 𝑤 𝑓 ,𝑖 as a scattered substring as
𝑟𝑖′ = .∗ · 𝑤 𝑓 [0] · · · .∗ · 𝑤 𝑓 [|𝑤 𝑓 | − 1] · .∗ . Therefore, we can construct
the set of strings that satisfies both (i) and (ii) as the intersection ofthese regexes, i.e., 𝐿(𝑟 1 )∩𝐿(𝑟 2 ) · · ·∩𝐿(𝑟 |𝑜𝑢𝑡 ( E ) | )∩𝐿(𝑟 1′ )∩𝐿(𝑟 2′ ) · · ·∩′𝐿(𝑟 |𝑜𝑢𝑡). The condition is satisfied iff the intersection is not(E) |empty.
For example, E = {L1𝑎M1 ⇝ L1𝑎𝑎𝑏M1, L1𝑏M1 ⇝ L1𝑎𝑏𝑏M1 }. Here,filter(𝑎𝑎𝑏, 𝑎) = 𝑏 and filter(𝑎𝑏𝑏,𝑏) = 𝑎. To check the condition, weconstruct the regexes described above as follows: 𝑟 1 = 𝑎 ?𝑎 ?𝑏 ? ,𝑟 2 = 𝑎 ?𝑏 ?𝑏 ? , 𝑟 1′ = .∗𝑏.∗ , and 𝑟 2′ = .∗𝑎.∗ . In this case, 𝑎𝑏 ∈ 𝐿(𝑟 1 ) ∩𝐿(𝑟 2 ) ∩ 𝐿(𝑟 1′ ) ∩ 𝐿(𝑟 2′ ). Therefore, the condition is satisfied and so
the instance is solvable.

5.2

SMT Constraint Generation

We describe the SMT constraint generation method. The SMT constraint contains the following boolean variables. For the regex template 𝑡 reg , we use the boolean variables 𝑣𝑖𝑎 , such that 𝑣𝑖𝑎 is true iff
the character set [𝐶] that corresponds to the 𝑖th hole of 𝑡 reg accepts
the character 𝑎, i.e., 𝑎 ∈ 𝐶. In what follows, we assume that eachnode 𝑡 of a regex template is identified by a unique index 𝑐𝑡 . For
the replacement template 𝑡 rep , we use three types of boolean vari$𝑗

ables: 𝑣𝑖𝑎 , 𝑣𝑖 , and 𝑣𝑖$𝑐𝑡 , where 𝑎 ∈ Σ, 𝑖, 𝑗 ∈ N, and 𝑐𝑡 is an index$𝑗identifying a node of the AST of 𝑡 reg , such that 𝑣𝑖𝑎 (resp. 𝑣𝑖 ) istrue iff the 𝑖th hole of 𝑡 rep is 𝑎 (resp. the reference $𝑗). The variables
𝑣𝑖$𝑐𝑡 are used to insert new capturing groups. Specifically, 𝑣𝑖$𝑐𝑡 istrue iff the subexpression that corresponds to the 𝑖th hole of 𝑡 rep isthe reference $𝑐𝑡 with the capturing group whose index is 𝑐𝑡 andwhose immediate subexpression is 𝑡 newly inserted into 𝑡 reg . The
insertion is done in a way that respects the 𝑛-ary operator normal
form (cf. Sec. 4.3). That is, we regard 𝑡 = ⊙(𝑡𝑘 , · · · , 𝑡𝑙 ) to be a subexpression of 𝑡 ′ = ⊙(𝑡 1, 𝑡 2, · · · , 𝑡𝑘 , · · · , 𝑡𝑙 , · · · , 𝑡𝑛 ) where ⊙ ∈ {·, |} sothat the index 𝑐𝑡 identifies 𝑡 and inserting a capturing group at 𝑡changes 𝑡 ′ to ⊙(𝑡 1, 𝑡 2, · · · , 𝑡𝑘 −1, (𝑐𝑡 ⊙(𝑡𝑘 , · · · , 𝑡𝑙 ))𝑐𝑡 , 𝑡𝑙+1, · · · , 𝑡𝑛 ) in
the new template.
With these variables, we build the SMT constraint 𝜙 as follows:Ó
𝜙 = 𝑒 ∈ E genConstForExample(𝑡 reg , 𝑡 rep , 𝑒). That is, for each example 𝑒 ∈ E, we construct an SMT constraint that encodes thecondition for satisfying 𝑒. Algorithm 2 shows genConstForExample.
First, it initializes 𝜙 with the constraints asserting that for each holein 𝑡 rep , the number of boolean variables corresponding to the hole

ASE ’24, October 27-November 1, 2024, Sacramento, CA, USA

and assigned to true is exactly 1 (line 1). Here, 𝑛 is the number ofholes in 𝑡 rep , and 𝔅𝑖 is the set of boolean variables that correspondto the 𝑖th hole of 𝑡 rep . Then, for each position 𝑝 s.t. ∃𝑗 . 𝜂 [ 𝑗] = (𝑝, _)or 𝑝 is negative (cf. Sec. 5 Pruning Infeasible Templates), it simulates the matchings of regexes instantiated from 𝑡 reg on 𝑤 at 𝑝and computes the set 𝑆 reg of succeeded matching results (line 3). A
matching result is of the form (𝑝 ′, Γ ′, 𝜙 ′ ) where 𝑝 ′ is a position in 𝑤,
Γ ′ is an environment, and 𝜙 ′ is an SMT constraint. The triple meansthat if 𝑡 reg is instantiated into a regex 𝑟 according to a satisfying
assignment to 𝜙 ′ , the matching of 𝑟 on 𝑤 at position 𝑝 moves the
position to 𝑝 ′ and the environment after the matching is Γ ′ . Using
these triples, we construct the SMT constraint for the example at theposition 𝑝 as follows: if ∃𝑗 .𝜂 [ 𝑗] = (𝑝, _), for each matching result(𝑝 ′, Γ ′, 𝜙 ′ ) ∈ 𝑆 reg , we construct a constraint Φrep (𝑡 rep , 𝜃 [ 𝑗], Γ ′ ) that
encodes the condition that 𝑡 rep outputs the correct output fragment
𝜃 [ 𝑗] under Γ ′ and take the conjunction of the constraint with 𝜙 ′(lines 4-5). If the position is negative, we take the negation of the
disjunction of all constraints for succeeding the matching (lines 67). The encoding of the regex and replacement templates at theposition 𝑝 is done by the functions compute𝑆 reg (line 3) and Φrep(line 5), respectively. We elaborate on these functions in the rest of
this section.
SMT Constraint Generation for Regex Templates. We adopt
and extend the method introduced in [18]. Namely, like the methodof [18], compute𝑆 reg uses the following judgment to obtain thematching results: (𝑡, 𝑤, 𝑝) d 𝑆 reg , where 𝑡 is a regex template, 𝑤 is
an input string, 𝑝 is a position in 𝑤, and 𝑆 reg is the set of succeeded
matching results.4 However, to accommodate the insertion of new
captures that can be referred from the replacement, we extend themethod to keep track of substrings matched by subexpressions
by insert a virtual capturing group to each subexpression of 𝑡 reg ,except for the concatenation and the union (insertion of new capturing groups at concatenations and unions are handled by the
SMT constraint for the replacement described below). Recall thateach node 𝑡 of the AST of a regex template has a unique index
𝑐𝑡 . We use the indexes for inserting virtual capturing groups. For
example, the result of inserting virtual capturing groups into 𝑎𝑏 ∗is (𝑐𝑎 𝑎)𝑐𝑎 (𝑐𝑏 ∗ (𝑐𝑏 𝑏)𝑐∗𝑏 )𝑐𝑏 ∗ . Consequently, compute𝑆 reg (𝑡 reg , 𝑤, 𝑝) =′ , 𝑤, 𝑝) d 𝑆′
𝑆 reg , where (𝑡 reg
reg and 𝑡 reg is the regex template obtained from 𝑡 reg by inserting virtual capturing groups as describedabove.
SMT Constraint Generation for Replacement Templates. The
function Φrep is defined as: Φrep (𝑡 rep , 𝑤, Γ) = 𝜙 rep ∧ ¬𝜙 overlap . Here,𝜙 rep is the SMT constraint that encodes the condition that 𝑡 rep isconsistent with the output fragment 𝑤 under the environment Γand ¬𝜙 overlap is the SMT constraint that rules out assignments that
require inserting capturing groups into 𝑛-ary operators with anoverlap. We elaborate on the construction of 𝜙 rep and 𝜙 overlap below.
First, 𝜙 rep is defined as: 𝜙 rep = Φ′ (𝑡 rep · ⊣, 𝑤 · ⊣, Γ), where ⊣ ∉ Σ
is a special endmarker character that denotes the end of a sequence.
Φ′ is defined by: Φ′ (⊣, 𝑤, Γ) = true if 𝑤 [0] =⊣ and false otherwise,Φ′ (𝑎 · 𝑡 rep , 𝑤, Γ) = Φ′ (𝑡 rep , 𝑤 [1..|𝑤 |), Γ) if 𝑤 [0] = 𝑎 and false otherwise, Φ′ ($𝑖 · 𝑡 rep , 𝑤, Γ) = Φ′ (𝑡 rep , 𝑣, Γ) if 𝑤 = J$𝑖K Γ · 𝑣 and false
4 This corresponds to (𝑡, 𝜖, 𝑤, 𝑝, ∅, forward, true) d (𝑆reg , _ ) , where 𝜖 is the initial
continuation regex template, ∅ is the initial environment, forward is the direction,true is the flag, in the actual rules given in [18].

Chida and Terauchi

Algorithm 3: Φ$𝑐𝑡
′ , Output
Input: Replacement Template 𝑡 rep = □𝑖 · 𝑡 rep
fragment 𝑤, Environment Γ
Output: SMT Constraint 𝜙
1: 𝜙 ← false
2: for all 𝑐 𝑡 ∈ 𝑑𝑜𝑚(Γ) do
3:
if 𝑡 = ⊙(𝑡 1, 𝑡 2, · · · , 𝑡𝑛 ) where ⊙ ∈ {·, |} then4:for 𝑝 from 1 to 𝑛, 𝑝 ′ from 𝑝 + 1 to 𝑛 do
5:
if ∃𝑢.𝑤 = Γ(𝑐𝑡𝑝 ) · · · Γ(𝑐𝑡𝑝 ′ ) · 𝑢 then$𝑐 ⊙ (𝑡𝑝 ···𝑡𝑝 ′ )′ , 𝑢, Γ) ∧ 𝑣
𝜙 ← 𝜙 ∨ (Φ′ (𝑡 rep𝑖7:else if ∃𝑢.𝑤 = Γ(𝑐𝑡 ) · 𝑢 then′ , 𝑢, Γ) ∧ 𝑣 $𝑐𝑡 )8:𝜙 ← 𝜙 ∨ (Φ′ (𝑡 rep𝑖
9: return 𝜙6:)otherwise, and Φ′ (□𝑖 · 𝑡 rep , 𝑤, Γ) = 𝜙𝑎 ∨ 𝜙 $𝑗 ∨ Φ$𝑐𝑡 (□𝑖 · 𝑡 rep , 𝑤, Γ)
where □𝑖 denotes the 𝑖th hole in the replacement template passed𝑤 [0]to Φrep . In the last case, 𝜙𝑎 = Φ′ (𝑤 [0] ·𝑡 rep , 𝑤, Γ) ∧𝑣𝑖
if 𝑤 [0] ≠⊣Ô$𝑗′and false otherwise, 𝜙 $𝑗 = 𝑗 ∈𝑑𝑜𝑚 (Γ) (Φ ($𝑗 · 𝑡 rep , 𝑤, Γ) ∧ 𝑣𝑖 ), andthe function Φ$𝑐𝑡 is defined below.
Roughly, Φ′ evaluates 𝑡 rep on 𝑤 from left to right and checks′ iswhether the string obtained from the first element 𝑡 of 𝑡 rep = 𝑡 ·𝑡 rep′
consistent with the prefix of 𝑤. Specifically, Φ (𝑡 · 𝑡 rep , 𝑤, Γ) checks
whether JtK Γ is a prefix of 𝑤 if 𝑡 ≠ □ and otherwise, i.e., 𝑡 = □, it
simulates all the possible ways of filling the hole, i.e., filling thehole with a character 𝑎, a reference $𝑗 s.t. ( 𝑗 𝑟 ) 𝑗 appears in 𝑡 reg , or areference $𝑐𝑡 that requires wrapping the subexpression 𝑡 with thecapturing group whose index is 𝑐𝑡 and refers to it. The first two cases
are analogous to the cases of Φ′ (𝑎 · 𝑡 rep , 𝑤, Γ) and Φ′ ($𝑗 · 𝑡 rep , 𝑤, Γ),respectively, but with the difference that we take the conjunction of
the variable 𝑣𝑖𝑥 , where 𝑥 ∈ {𝑤 [0], $𝑗 }, with the SMT constraint constructed from the remaining encoding. The third case tries to insert
a new capturing group into a regex and refers to it. This is accomplished by the function Φ$𝑐𝑡 shown in Algorithm 3. The basic idea issimilar to the case for $𝑗, except for the handling of 𝑛-ary operators.
Namely, for the case that the virtual capturing group under consideration is an 𝑛-ary concatenation or union, we simulate all possible
insertions of a capturing group into the subexpressions. That is, for
an 𝑛-ary operator 𝑡 = ⊙(𝑡 1, · · · , 𝑡𝑛 ) and each of its subexpression𝑡 ′ = ⊙(𝑡𝑝 , · · · , 𝑡𝑝 ′ ) where 1 ≤ 𝑝 < 𝑝 ′ ≤ 𝑛, we simulate the insertion ⊙(𝑡 1, · · · , 𝑡𝑝 −1, (𝑐𝑡 ′ ⊙(𝑡𝑝 , · · · , 𝑡𝑝 ′ ))𝑐𝑡 ′ , 𝑡𝑝 ′ +1, · · · , 𝑡𝑛 ) (lines 3-6).
ÔSecondly, 𝜙 overlap is defined as: 𝜙 overlap = (𝑣1 ,𝑣2 ) ∈𝑉 (𝑣 1 ∧ 𝑣 2 ),$𝑐 ′where 𝑉 is the set of pairs (𝑣𝑖$𝑐𝑡 , 𝑣 𝑗 𝑡 ) of variables s.t. the subex$𝑐 ′pressions 𝑡 and 𝑡 ′ has an overlap. Precisely, (𝑣𝑖$𝑐𝑡 , 𝑣 𝑗 𝑡 ) ∈ 𝑉 if and$𝑐 ′only if (1) 𝑣𝑖$𝑐𝑡 and 𝑣 𝑗 𝑡 both appear in 𝜙 rep , (2) neither 𝑡 is a subtree of 𝑡 ′ nor 𝑡 ′ is a subtree of 𝑡, and (3) 𝑡 and 𝑡 ′ share a common
node. For example, let us consider the regex template 𝑎𝑏𝑐, the replacement template □1 □2 , and the output fragment 𝑎𝑏𝑏𝑐. In thiscase, the replacement $𝑐1$𝑐2 instantiated from □1 □2 can satisfy
the output fragment 𝑎𝑏𝑏𝑐 if the references $𝑐1 and $𝑐2 refer tothe subexpressions 𝑎𝑏 and 𝑏𝑐 of the regex template, respectively.
However, if we insert the capturing groups in such a way, then it
yields an overlap of capturing groups, i.e., it yields the expression

Repairing Regex-Dependent String Functions(𝑐1𝑎(𝑐2𝑏)𝑐1𝑐)𝑐2 which is invalid according to the syntax of regexes.
Therefore, to rule out such invalid insertions, we add the SMT
constraint ¬𝜙 overlap = ¬(𝑣 1$𝑐𝑎𝑏 ∧ 𝑣 2$𝑐𝑏𝑐 ).

5.3

Pruning Infeasible Templates

We show the construction of over- and under-approximations ofa regex template for substring matching. The construction is composed of two steps: approximation and addition of the context. The
first step uses the existing approximations of regex templates forwhole matching [17, 18, 28, 35]. Roughly, the existing methods
replace holes with .∗ or ∅, depending on the polarity. For example, let us consider the regex template (?<=𝑎□)□(?!□). The overand under-approximations are (?<=𝑎.∗ ).∗ (?!∅) and (?<=𝑎∅)∅(?!.∗ ),respectively. The second step extends the approximations to becontext-aware.
We first consider the over-approximation. For a position 𝑝 s.t.
𝜂 [𝑖] = (𝑝, 𝑝 ′ ) for some 𝑖 and (𝑤, 𝜂, 𝜃 ) ∈ E, we prepend ˆ𝑤 [0..𝑝)and append 𝑤 [𝑝 ′ ..|𝑤 |)$ to the over-approximation, where ˆ and $are anchors that match the start and end of a string, respectively, andare syntactic sugar of lookarounds [26]. Specifically, let 𝑟 ⊤ be theover-approximation. Then, the context-aware over-approximation′ = ˆ𝑤 [0..𝑝)·𝑟 ·𝑤 [𝑝 ′ ..|𝑤 |)$, and we implement isFeasible(𝑡 )is 𝑟 ⊤⊤reg′ ). For example, let us consider the regex
to reurn false if 𝑤 ∉ 𝐿(𝑟 ⊤template (?<!□|𝑎)𝑏 and the example 𝑎L1𝑏M1𝑐 ⇝ _. Then, the context′ is ˆ𝑎·(?<!∅|𝑎)𝑏 ·𝑐$. Since 𝑎𝑏𝑐 ∉ 𝐿(𝑟 ′ ),aware over-approximation 𝑟 ⊤⊤we can safely avoid expanding the hole. Indeed, we cannot obtaina solution from the regex template regardless of the replacement
template because the negative lookbehind always fails to matchthe substring 𝑏.
We next consider making the under-approximation contextaware. This is similar to the case of over-approximation, but in thiscase, there is no need to care about the position where the matching finishes. Therefore, we append .∗ $ to the under-approximation.
Specifically, let 𝑟 ⊥ be the under-approximation. Then, for eachnegative position 𝑝, the context-aware under-approximation is′ = ˆ𝑤 [0..𝑝) ·𝑟 · .∗ $, and we implement isFeasible(𝑡 ) to return𝑟⊥⊥
reg′ ). For example, let us consider the regex temfalse if 𝑤 ∈ 𝐿(𝑟 ⊥plate (?<!𝑑□). and the example 𝑎L1𝑏M1𝑐 ⇝ _. The context-aware
under-approximation at position 2 is ˆ𝑎𝑏 · (?<!𝑑.∗ ). · .∗ $. We makeisFeasible(𝑡 reg ) return true if neither cases apply.
Finally, like the prior works [17, 18, 35], we use a variant preTestof the pruning techniques (line 7). The variant is almost the sameas the over-approximation case of isFeasible except that we replace
holes with . instead of .∗ .

6

OTHER REGEX-DEPENDENT STRING
FUNCTIONSWe discuss how to apply our core ideas to other representative
regex-dependent string functions such as search, replace, match,and exec.
Like replaceAll, replace takes a string as the input, and a regex
and replacement pair as the parameter, and returns an output string.
The only difference is that, whereas replaceAll replaces all matchedsubstrings, replace replaces only the first matched substring. We
can adapt our algorithm to repair the parameters of replace by a

ASE ’24, October 27-November 1, 2024, Sacramento, CA, USAminor modification to the pruning techniques and the SMT constraint generation method for regex templates so that they stop
after reaching the only position denoted by the origin information.
The search function takes a string as the input and a regex as
the parameter, and returns the first matched position or −1 if there
are no substrings of the string matching the regex. We can treat the
repair problem for search as a special case of the repair problem
for replace. That is, we add an origin information to the positionof the example string where the substring should be matched (orwith no origin information for an example string on which the
to-be-synthesized function should return −1) and set the output
fragments for all examples and the replacement parameter to besome fixed character 𝑎 ∈ Σ (our algorithm is optimized to not
modify the replacement in such a case).
The match function takes a string as the input and a regex as theparameter, and returns a list of matched substrings. If the matchfunction has the global flag, it returns a list of all matched substrings; otherwise, it returns a list containing only the first matchedsubstring. We can treat this in the same way as that of search described above if it does not have a global flag. If it has, it can behandled as replaceAll by letting the origin information identify
the positions of substrings that should be matched, and setting
the output fragments and the replacement parameter to a fixedcharacter.
The exec function takes a string as the input and a regex as theparameter, and returns a list whose first element is the first matchedsubstring and the other elements are substrings extracted by capturing groups. From this, it can be handled in a similar way as theapproach for search with a minor extension. That is, to address thesubstrings to be extracted, we add information about the substrings
to be extracted into examples and extend the algorithm to check thecorrectness of the extraction. The extension to the algorithm is only
a minor one because, as described in Sec. 5.2, the SMT constraint
generation method computes matching results that already include
the information about extraction (i.e., the environment) to handle
backreferences in regexes and references in replacements.

7

EVALUATION

We implemented our algorithm as a tool called R2-DS. It is written
in Java and uses Z3 [21] as the SMT solver. We evaluated R2-DS
to answer the following questions: (RQ1) Can R2-DS repair realworld bugs of regex-dependent string functions in a reasonable
time? (RQ2) Are the repaired functions high-quality? (RQ3) How
impactful are the newly introduced techniques of context-aware
pruning and SMT-constraint-based insertion of captures? Our experiments were conducted on Intel(R) Xeon(R) Platinum 8360Y
CPU @ 2.40GHz. To answer RQ3, we prepared R2-DS𝑤𝑜/𝑝 and R2DS𝑤𝑜/𝑐 , which are variants of R2-DS with the pruning techniqueand the insertion of capturing groups disabled, respectively.
Benchmarks. We collected our benchmark tasks from GitHub
commits and StackOverflow posts. Specifically, we collected theparameters of before and after repairs as the incorrect and correct
parameters. We prepared the examples by using the ones provided
in the commits/posts when they are available, and adding new ones
or removing inappropriate ones manually by ourselves as neededASE ’24, October 27-November 1, 2024, Sacramento, CA, USA

Chida and Terauchi

Table 1: Solved instances.

R2-DS
R2-DS𝑤𝑜/𝑝
R2-DS𝑤𝑜/𝑐

instances
Solved (120)
109 (90.8%)
90 (75%)76 (63.3%)

running time (seconds)
min medmax
0.117 0.763 1451.92
0.081 1.853 1795.3
0.145 0.853 681.805(e.g., when none was provided or ones that trigger Regular Expression Denial-of-Service (ReDoS) vulnerability [19], which makes theregex matching slow, were provided). As a result, for each instance,
we prepared at least 5 examples that have non-empty origin information (we call them positive examples), at least 5 examples thathave empty origin information (we call them negative examples),and at most 15 examples in total.5 From the examples, we used atmost 5 examples for the synthesis. The remaining examples areused as left-out example sets to measure the quality of the repairs.
To find the commits and posts, we first looked at all commits
in the lists provided by [23] that studied string-related bugs ina wide variety of GitHub projects written in JavaScript and [44]that studied regex-related bugs in popular GitHub projects suchas Apache, Mozilla, Facebook, and Google. Among these, we havecollected the commits that change the parameters of replaceAll,
replace, or search.6 This gave us 34 benchmarks. Next, we searchedon GitHub Advanced Search and StackOverflow with keywords
such as “replaceAll”, “bug”, and “JavaScript” and collected the ones
that change the parameters of replaceAll, replace, or search. In total,
we collected 120 benchmark tasks (21 from [23], 13 from [44], and86 from GitHub Advanced Search and StackOverflow). Amongthe 120, 97 are instances of replaceAll, 15 are instances of replace,and 8 are instances of search. The average and maximum sizes of
the regexes (resp. replacements), measured as the number of AST
nodes, are 16.43 and 193 (resp. 7.06 and 105). Also, 5 regexes have abounded repetition, 42 (resp. 4) regexes have a (resp. lazy) Kleenestar, 15 (resp. 2) regexes have a (resp. lazy) Kleene plus, 12 regexes
have an option, a regex has a backreference, 4 (resp. 1) regexes havea negative lookbehind (resp. lookahead), 20 (resp. 14) regexes havethe anchor ˆ (resp. $) [26], and 20 replacements have a reference.
The data set is provided as supplementary material.
Validation. Our algorithm generates only correct parameters,i.e., the function using the repaired parameters behaves consistently
with the examples. To verify this, we prepared a JavaScript program and confirmed that the function with the repaired parametersindeed returns correct outputs for all inputs in all cases.
RQ1: Efficiency To answer RQ1, we measured the minimum,
median, and maximum running times of solving the instances,with a timeout of 30 minutes.7 Table 1 reports the results. R2-DS
could solve 90.8% of instances (91.7% of replaceAll instances, 80%of replace instances, and 100% of search instances) within 50.71
seconds on average. In some cases, R2-DS could not find a solution within the time limit. We inspected these cases and foundthat, as the existing methods for regex synthesis [17, 18, 28, 35],
R2-DS suffered from the cases that required large changes from
5 In some cases, the correct regex is one that accepts any strings, and so we do notprepare any negative examples for such cases.
6 Due to time constraints, we do not evaluate R2-DS on match and exec. We leave themfor future work.
7 On an instance that has a solution, R2-DS is guaranteed to terminate and return asolution if given unbounded time and resource.

Figure 2: Scalability.

Figure 3: F1 scores.

Figure 4: Impact of the pruning (left) and the capture insertions (right).

the original. For example, R2-DS could not the repair of the regex[␣]+ , where ␣ is the white space, when the intended solution was[␣]+ (?=([ˆ’]∗ ’[ˆ’]∗ ’)∗ [ˆ’]∗ $) because such a repair requires appending a large expression. In summary, R2-DS can repair real-world
regex-dependent functions efficiently.
Additionally, we evaluated how R2-DS scales as the size of theregex-dependent string function parameters increases, by comparing the running times of R2-DS over the sizes. Figure 2 shows theplot. The points on the border colored in blue show that R2-DS
could not find a solution within the time limit. As the figure shows,
R2-DS could find a solution in a short time, even for large parameters. In summary, the performance of R2-DS scales with respect tothe size of regex-dependent string functions.
RQ2: Quality Following the approach used in [18, 35], we measured the quality of the repairs with respect to left-out example sets.
That is, we measured the F1 scores using the left-out examples. The
×𝑅
F1 score is calculated as 𝐹 1 = 2×𝑃
𝑃 +𝑅 , where 𝑃 is the precision and 𝑅
𝑃 , where 𝑇 𝑃
is the recall. The precision 𝑃 is calculated as 𝑃 = 𝑇 𝑃𝑇+𝐹
𝑃
(resp. 𝐹 𝑃) is the number of positive (resp. negative) examples thatare (resp. not) satisfied by the functions. The recall 𝑅 is calculated
𝑃 , where 𝐹 𝑁 is the number of positive examples thatas 𝑅 = 𝑇 𝑃𝑇+𝐹𝑁
are not satisfied by the functions. Therefore, the F1 score is between
0 and 1, and scores that are close to 1 imply the high quality of
the repairs. Figure 3 shows the results. The median and average of
the F1 scores are 1 and 0.84, respectively. We inspected the repairs
with low F1 scores and observed that R2-DS could not find a highquality repair when the instances require a large change from theoriginal. In summary, R2-DS can produce repairs that generalize wellto left-out example sets, and therefore of high-quality.
RQ3: Impact of the new techniques To evaluate the impact of
the new techniques on R2-DS’s overall performance, we conductedRepairing Regex-Dependent String Functions

an ablation study in which we disabled some of them. In this evaluation, we consider the two ablations: R2-DS without the pruning
techniques and R2-DS without insertions of capturing groups as
SMT constraints, which we refer to as R2-DS𝑤𝑜/𝑝 and R2-DS𝑤𝑜/𝑐 ,respectively. We compared them against R2-DS, which incorporates
both techniques.
Figure 4 shows the results. The points above the diagonal indicatethat R2-DS could find a solution faster with the new techniquerather than without it. The points colored in blue on the borderindicate that the tool could not find a solution within the time
limit. Overall, R2-DS achieved 85.13× (resp. 35.01%×) speedups
against R2-DS𝑤𝑜/𝑝 (resp. R2-DS𝑤𝑜/𝑐 ) on average. We also observedthat R2-DS𝑤𝑜/𝑝 (resp. R2-DS𝑤𝑜/𝑐 ) could not solve 19 (resp. 33)
instances that R2-DS was able to solve. However, in a few cases, weobserved negative performance impacts. We inspected such casesand observed that the new pruning technique can occasionallyintroduce ReDoS (a similar issue was observed in [18] for regex
synthesis). As for the capture-insertion technique, the negative
effect was also due to it changing edit distance (cf. Sec. 4.3) between
templates that in some rare cases adversely affect their order inthe priority queue. In summary, the new pruning technique andconstraint-based capturing-group-insertion technique introduced in
the paper are highly impactful to the performance of the algorithm.

ASE ’24, October 27-November 1, 2024, Sacramento, CA, USA

9

CONCLUSION

This paper presented the first PBE-based method for repairing regexdependent string functions. Our algorithm builds on the techniquesfrom the prior work on PBE-based regex sythesis and repair but
incorporates the following key novelties to address the large search
space: origin information in examples to identify the locations of
substrings to be matched, a new substring-context-aware pruning
technique, and a novel use of SMT constraints to insert capturesthat can referred from the replacement. Additionally, we identified
a novel necessary and sufficient condition that can be used to detectand filter unrepairable instances. We implemented our algorithm asa tool called R2-DS and evaluated it on real-world benchmarks. The
results show that R2-DS can repair real-world bugs efficiently, findhigh-quality repairs, and the new pruning and capture insertion
techniques significantly improve the performance.

ACKNOWLEDGMENTS
We thank anonymous reviewers for their useful comments. This
work was supported by JSPS KAKENHI Grant Numbers JP23K24826,
JP20K20625, and JP23K20380.

DATA-AVAILABILITY STATEMENT
The artifact of this paper is publicly available at [36].

8

RELATED WORK

There is a lot of work on synthesizing regexes from examples [1, 7–
10, 12, 17, 18, 24, 25, 27, 28, 30, 35, 37, 42, 45]. However, all of theworks focus only on regexes and do not consider replacements,
which are essential for regex-dependent string functions like replaceAll and replace. Additionally, all of them focus on whole string
matching and do not support substring matching, which is alsoessential for many regex-dependent string functions. In fact, as
we showed in Sec. 4.4, our problem differs significantly from the
problems addressed in the prior works in that, our problem has
instances that do not have a solution, whereas the PBE regex synthesis and repair problems addressed in the prior works always
have a solution. We mention that there are several methods forgenerating regexes based on genetic programming [2–4] that consider substring matching. However, they focus only on regexes andcannot be synthesize or repair regex-dependent string functions
like replaceAll and replace that require replacements. Also, unlike
ours or other PBE-based methods, these methods do not guaranteethat the synthesis result is consistent with the given examples.
Origin information was introduced by Bojańczyk [6] to clarify
how the output is constructed from the input in transducers. Inspired by the idea, we incorporated origin information into our
examples to specify the desired outputs in the PBE scenario. To ourknowledge, our work is the first to use origin information in thesetting of PBE-based synthesis or repair.
Finally, we mention that there are many works on detecting
bugs of regex-dependent string functions. Many of them focus
on the replaceAll function due to its practical importance [13–16].
However, these works focus on detecting bugs and do not consider
synthesis or repair.

REFERENCES[1] 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/S00199958(78)90683-6[2] 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[3] Alberto Bartoli, Andrea De Lorenzo, Eric Medvet, and Fabiano Tarlao. 2014.
Playing Regex Golf with Genetic Programming. In Proceedings of the 2014
Annual Conference on Genetic and Evolutionary Computation (Vancouver, BC,
Canada) (GECCO ’14). Association for Computing Machinery, New York, NY,
USA, 1063–1070. https://doi.org/10.1145/2576768.2598333[4] 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[5] Martin Berglund and Brink van der Merwe. 2022. Re-examining regular expressions with backreferences. Theoretical Computer Science (2022). https://doi.org/10.1016/j.tcs.2022.10.041[6] Mikołaj Bojańczyk. 2014. Transducers with Origin Information. In Automata,
Languages, and Programming, Javier Esparza, Pierre Fraigniaud, Thore Husfeldt,
and Elias Koutsoupias (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg,
26–37.
[7] 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[8] Alvis Brāzma. 1995. Learning of regular expressions by pattern matching. In
Computational Learning Theory, Paul Vitányi (Ed.). Springer Berlin Heidelberg,
Berlin, Heidelberg, 392–403.
[9] Alvis Brāzma and Kārlis Čerāns. 1994. Efficient learning of regular expressions
from good examples. In Algorithmic Learning Theory, Setsuo Arikawa and Klaus P.
Jantke (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 76–90.
[10] Alvis Brāzma and Kārlis Čerāns. 1997. Noise-tolerant efficient inductive synthesisof regular expressions from good examples. New Gen. Comput. 15, 1 (mar 1997),
105–140. https://doi.org/10.1007/BF03037562[11] Carl Chapman and Kathryn T. Stolee. 2016. Exploring Regular Expression Usage
and Context in Python. In Proceedings of the 25th International Symposium on
Software Testing and Analysis (Saarbrücken, Germany) (ISSTA 2016). Association
for Computing Machinery, New York, NY, USA, 282–293. https://doi.org/10.
1145/2931037.2931073

ASE ’24, October 27-November 1, 2024, Sacramento, CA, USA[12] Qiaochu Chen, Xinyu Wang, Xi Ye, Greg Durrett, and Isil Dillig. 2020. MultiModal Synthesis of Regular Expressions. In Proceedings of the 41st ACM SIGPLAN
Conference on Programming Language Design and Implementation (London, UK)(PLDI 2020). Association for Computing Machinery, New York, NY, USA, 487–502.
https://doi.org/10.1145/3385412.3385988[13] Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu. 2017.
What is Decidable about String Constraints with the ReplaceAll Function. 2,
POPL, Article 3 (dec 2017), 29 pages. https://doi.org/10.1145/3158091[14] 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[15] Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin,
Philipp Rümmer, and Zhilin Wu. 2020. A Decision Procedure for Path Feasibility ofString Manipulating Programs with Integer Data Type. In Automated Technology
for Verification and Analysis, Dang Van Hung and Oleg Sokolsky (Eds.). Springer
International Publishing, Cham, 325–342.
[16] Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu.
2019. Decision procedures for path feasibility of string-manipulating programswith complex operations. Proc. ACM Program. Lang. 3, POPL, Article 49 (jan2019), 30 pages. https://doi.org/10.1145/3290362[17] Nariyoshi Chida and Tachio Terauchi. 2022. Repairing DoS Vulnerability of RealWorld Regexes. In 2022 IEEE Symposium on Security and Privacy (SP). 2060–2077.
https://doi.org/10.1109/SP46214.2022.9833597[18] Nariyoshi Chida and Tachio Terauchi. 2023. Repairing Regular Expressions for
Extraction. Proc. ACM Program. Lang. 7, PLDI, Article 173 (jun 2023), 24 pages.
https://doi.org/10.1145/3591287[19] Scott Crosby. 2003. Denial of Service through Regular Expressions. USENIX
Association, Washington, D.C.
[20] 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
Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering
Conference and Symposium on the Foundations of Software Engineering (Tallinn,
Estonia) (ESEC/FSE 2019). Association for Computing Machinery, New York, NY,
USA, 443–454. https://doi.org/10.1145/3338906.3338909[21] Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In
Proceedings of the Theory and Practice of Software, 14th International Conferenceon Tools and Algorithms for the Construction and Analysis of Systems (Budapest,
Hungary) (TACAS’08/ETAPS’08). Springer-Verlag, Berlin, Heidelberg, 337–340.
[22] ECMA International. 2022. ECMAScript® 2023 Language Specification. https://tc39.es/ecma262/multipage/#sec-intro.
[23] Aryaz Eghbali and Michael Pradel. 2021. No strings attached: an empirical studyof string-related software bugs. In Proceedings of the 35th IEEE/ACM International
Conference on Automated Software Engineering (Virtual Event, Australia) (ASE’20). Association for Computing Machinery, New York, NY, USA, 956–967. https://doi.org/10.1145/3324884.3416576[24] 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[25] 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.
[26] Jeffrey Friedl. 2006. Mastering Regular Expressions. O’Reilly Media, Inc.
[27] Efim Kinber. 2010. Learning Regular Expressions from Representative Examples
and Membership Queries. In Grammatical Inference: Theoretical Results and Applications, José M. Sempere and Pedro García (Eds.). Springer Berlin Heidelberg,
Berlin, Heidelberg, 94–108.
[28] Mina Lee, Sunbeom So, and Hakjoo Oh. 2016. Synthesizing Regular Expressions
from Examples for Introductory Automata Assignments. SIGPLAN Not. 52, 3 (oct2016), 70–80. https://doi.org/10.1145/3093335.2993244[29] 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/D08-1003[30] 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[31] 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

Chida and Terauchi[32] 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[33] Chris O’Hara. 2024. Validator.js. https://github.com/validatorjs/validator.js/[Online; accessed 1-June-2024].
[34] OWASP. 2024. Input Validation Cheat Sheet. https://cheatsheetseries.owasp.org/
cheatsheets/Input_Validation_Cheat_Sheet.html [Online; accessed 1-June-2024].
[35] 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[36] R2-DS. 2024. https://github.com/NariyoshiChida/ASE2024/.
[37] Thomas Rebele, Katerina Tzompanaki, and Fabian M. Suchanek. 2018. Adding
Missing Words to Regular Expressions. In Advances in Knowledge Discovery andData Mining, Dinh Phung, Vincent S. Tseng, Geoffrey I. Webb, Bao Ho, Mohadeseh
Ganji, and Lida Rashidi (Eds.). Springer International Publishing, Cham, 67–79.
[38] Noé De Santo, Aurèle Barrière, and Clément Pit-Claudel. 2024. A Coq Mechanization of JavaScript Regular Expression Semantics. arXiv:2403.11919 [cs.PL][39] StackOverflow. 2012. Javascript replace() and $1 issue. https://stackoverflow.
com/questions/13368906/javascript-replace-and-1-issue?rq=3 [Online; accessed
1-June-2024].
[40] StackOverflow. 2013. replace in java with a regex doesn’t replace from left toright. https://stackoverflow.com/questions/18901525/replace-in-java-with-aregex-doesnt-replace-from-left-to-right [Online; accessed 1-June-2024].
[41] StackOverflow. 2017. Java regex not replacing my pattern. https://stackoverflow.
com/questions/42778804/java-regex-not-replacing-my-pattern/42778862 [Online; accessed 1-June-2024].
[42] Mojtaba Valizadeh and Martin Berger. 2023. Search-Based Regular Expression
Inference on a GPU. Proc. ACM Program. Lang. 7, PLDI, Article 160 (jun 2023),
23 pages. https://doi.org/10.1145/3591274[43] 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[44] Peipei Wang, Chris Brown, Jamie A. Jennings, and Kathryn T. Stolee. 2022. Demystifying regular expression bugs: A comprehensive study on regular expression
bug causes, fixes, and testing. Empirical Softw. Engg. 27, 1 (jan 2022), 35 pages.
https://doi.org/10.1007/s10664-021-10033-1[45] 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

Received 20 February 2007; revised 12 March 2009; accepted 5 June 2009