What Is Decidable about String Constraints with the
ReplaceAll Function (Technical Report)
TAOLUE CHEN, Birkbeck, University of London, United Kingdom
YAN CHEN, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences,
China and University of Chinese Academy of Sciences, China
MATTHEW HAGUE, Royal Holloway, University of London, United Kingdom
ANTHONY W. LIN, University of Oxford, United Kingdom
ZHILIN WU, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences,
China
The theory of strings with concatenation has been widely argued as the basis of constraint solving for verifying
string-manipulating programs. However, this theory is far from adequate for expressing many string constraints
that are also needed in practice; for example, the use of regular constraints (pattern matching against a regularexpression), and the string-replace function (replacing either the first occurrence or all occurrences of a“pattern” string constant/variable/regular expression by a “replacement” string constant/variable), among
many others. Both regular constraints and the string-replace function are crucial for such applications as
analysis of JavaScript (or more generally HTML5 applications) against cross-site scripting (XSS) vulnerabilities,
which motivates us to consider a richer class of string constraints. The importance of the string-replace function(especially the replace-all facility) is increasingly recognised, which can be witnessed by the incorporation of
the function in the input languages of several string constraint solvers.
Recently, it was shown that any theory of strings containing the string-replace function (even the mostrestricted version where pattern/replacement strings are both constant strings) becomes undecidable if we do
not impose some kind of straight-line (aka acyclicity) restriction on the formulas. Despite this, the straightline restriction is still practically sensible since this condition is typically met by string constraints that are
generated by symbolic execution. In this paper, we provide the first systematic study of straight-line string
constraints with the string-replace function and the regular constraints as the basic operations. We showthat a large class of such constraints (i.e. when only a constant string or a regular expression is permitted in
the pattern) is decidable. We note that the string-replace function, even under this restriction, is sufficiently
powerful for expressing the concatenation operator and much more (e.g. extensions of regular expressions
with string variables). This gives us the most expressive decidable logic containing concatenation, replace, andregular constraints under the same umbrella. Our decision procedure for the straight-line fragment follows
an automata-theoretic approach, and is modular in the sense that the string-replace terms are removed one
by one to generate more and more regular constraints, which can then be discharged by the state-of-the-art
string constraint solvers. We also show that this fragment is, in a way, a maximal decidable subclass of the
Authors’ addresses: Taolue Chen, Department of Computer Science and Information Systems, Birkbeck, University of
London, Malet Street, London, WC1E 7HX, United Kingdom, taolue@dcs.bbk.ac.uk; Yan Chen, State Key Laboratory ofComputer Science, Institute of Software, Chinese Academy of Sciences, China , University of Chinese Academy of Sciences,
China; Matthew Hague, Department of Computer Science, Royal Holloway, University of London, Egham Hill, Egham,
Surrey, TW20 0EX, United Kingdom, matthew.hague@rhul.ac.uk; Anthony W. Lin, Department of Computer Science,
University of Oxford, Wolfson Buildin, Parks Road, Oxford, OX1 3QD, United Kingdom, anthony.lin@cs.ox.ac.uk; Zhilin
Wu, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China.
Permission to make digital or hard copies of all or part 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 and thefull citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored.
Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires
prior specific permission and/or a fee. Request permissions from permissions@acm.org.
© 2018 Copyright held by the owner/author(s). Publication rights licensed to the Association for Computing Machinery.
2475-1421/2018/1-ART3
https://doi.org/10.1145/3158091

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3

3:2

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

straight-line fragment with string-replace and regular constraints. To this end, we show undecidability results
for the following two extensions: (1) variables are permitted in the pattern parameter of the replace function,(2) length constraints are permitted.
CCS Concepts: • Theory of computation → Automated reasoning; Verification by model checking;
Program verification; Program analysis; Logic and verification; Complexity classes;
Additional Key Words and Phrases: String Constraints, ReplaceAll, Decision Procedures, Constraint Solving,
Straight-Line Programs
ACM Reference Format:
Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu. 2018. What Is Decidable about String
Constraints with the ReplaceAll Function (Technical Report). Proc. ACM Program. Lang. 2, POPL, Article 3(January 2018), 36 pages. https://doi.org/10.1145/3158091

1

INTRODUCTION

The problem of automatically solving string constraints (aka satisfiability of logical theories overstrings) has recently witnessed renewed interests [Abdulla et al. 2017, 2014; Bjørner et al. 2009;
D’Antoni and Veanes 2013; Hooimeijer et al. 2011; Kiezun et al. 2012; Liang et al. 2014; Lin andBarceló 2016; Saxena et al. 2010; Trinh et al. 2014, 2016; Veanes et al. 2012; Wang et al. 2016; Yu et al.
2014; Zheng et al. 2013] because of important applications in the analysis of string-manipulating
programs. For example, program analysis techniques like symbolic execution [Cadar et al. 2006;
Godefroid et al. 2005; King 1976; Sen et al. 2013] would systematically explore executions in a
program and collect symbolic path constraints, which could then be solved using a constraint
solver and used to determine which location in the program to continue exploring. To successfully
apply a constraint solver in this instance, it is crucial that the constraint language precisely models
the data types in the program, along with the data-type operations used. In the context of stringmanipulating programs, this could include concatenation, regular constraints (i.e. pattern matching
against a regular expression), string-length functions, and the string-replace functions, among
many others.
Perhaps the most well-known theory of strings for such applications as the analysis of stringmanipulating programs is the theory of strings with concatenation (aka word equations), whose
decidability was shown by Makanin [Makanin 1977] in 1977 after it was open for many years. More
importantly, this theory remains decidable even when regular constraints are incorporated into
the language [Schulz 1990]. However, whether adding the string-length function preserves thedecidability remains a long-standing open problem [Büchi and Senger 1990; Ganesh et al. 2012].
Another important string operation—especially in popular scripting languages like Python,
JavaScript, and PHP—is the string-replace function, which may be used to replace either the firstoccurrence or all occurrences of a string (a string constant/variable, or a regular expression)by another string (a string constant/variable). The replace function (especially the replace-all
functionality) is omnipresent in HTML5 applications [Lin and Barceló 2016; Trinh et al. 2016; Yu
et al. 2014]. For example, a standard industry defense against cross-site scripting (XSS) vulnerabilities
includes sanitising untrusted strings before adding them into the DOM (Document Object Model)or the HTML document. This is typically done by various metacharacter-escaping mechanisms(see, for instance, [Hooimeijer et al. 2011; Kern 2014; Williams et al. 2017]). An example of such amechanism is backslash-escape, which replaces every occurrence of quotes and double-quotes (i.e.
' and ") in the string by \' and \". In addition to sanitisers, common JavaScript functionalities
like document.write() and innerHTML apply an implicit browser transduction — which decodes
HTML codes (e.g. &#39; is replaced by ') in the input string — before inserting the input string
into the DOM. Both of these examples can be expressed by (perhaps multiple) applications of theProceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:3

string-replace function. Moreover, although these examples replace constants by constants, thepopularity of template systems such as Mustache [Wanstrath 2009] and Closure Templates [Google
2015] demonstrate the need for replacements involving variables. Using Mustache, a web-developer,
for example, may define an HTML fragment with placeholders that is instantiated with user data
during the construction of the delivered page.
Example 1.1. We give a simple example demonstrating a (naive) XSS vulnerability to illustrate
the use of string-replace functions. Consider the HTML fragment below.
<h1> User <span onMouseOver="popupText('{{bio}}')">{{userName}}</span> </h1>This HTML fragment is a template as might be used with systems such as Mustache to display
a user on a webpage. For each user that is to be displayed – with their username and biography stored in variables user and bio respectively – the string {{userName}} will be replaced byuser and the string {{bio}} will be replaced by bio. For example, a user Amelia with biography
Amelia was born in 1979... would result in the HTML below.
<h1> User<span onMouseOver="popupText('Amelia was born in 1979...')">
Amelia </span> </h1>This HTML would display User Amelia, and, when the mouse is placed over Amelia, her biography
would appear, thanks to the onMouseOver attribute in the span element.
Unfortunately, this template could be insecure if the user biography is not adequately sanitised:
A user could enter a malicious biography, such as '); alert('Boo!'); alert(' which would
cause the following instantiation of the span element1 .
<span onMouseOver="popupText(''); alert('Boo!'); alert('')">
Now, when the mouse is placed over the user name, the malicious JavaScript alert('Boo!') is
executed.
The presence of such malicious injections of code can be detected using string constraint solving
and XSS attack patterns given as regular expressions [Balzarotti et al. 2008; Saxena et al. 2010; Yu
et al. 2014]. For our example, given an attack pattern P and template temp, we would generate theconstraint
x 1 = replaceAll(temp, {{userName}}, user) ∧ x 2 = replaceAll(x 1 , {{bio}}, bio) ∧ x 2 ∈ P
which would detect if the HTML generated by instantiating the template is susceptible to the attack
identified by P.
□
In general, the string-replace function has three parameters, and in the current mainstream
language such as Python and JavaScript, all of the three parameters can be inserted as string variables.
As result, when we perform program analysis for, for instance, detecting security vulnerabilities as
described above, one often obtains string constraints of the form z = replaceAll(x, p, y), where x, y
are string constants/variables, and p is either a string constant/variable or a regular expression. Sucha constraint means that z is obtained by replacing all occurrences of p in x with y. For convenience,
we call x, p, y as the subject, the pattern, and the replacement parameters respectively.
The replaceAll function is a powerful string operation that goes beyond the expressivenessof concatenation. (On the contrary, as we will see later, concatenation can be expressed by the
replaceAll function easily.) It was shown in a recent POPL paper [Lin and Barceló 2016] thatany theory of strings containing the string-replace function (even the most restricted version
1 Readers familiar with Mustache and Closure Templates may expect single quotes to be automatically escaped. How-ever, we have tested our example with the latest versions of mustache.js [Lehnardt and contributors 2015] and Closure
Templates [Google 2015] (as of July 2017) and observed that the exploit is not disarmed by their automatic escaping features.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:4

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

where pattern/replacement strings are both constant strings) becomes undecidable if we do not
impose some kind of straight-line restriction2 on the formulas. Nonetheless, as already noted in[Lin and Barceló 2016], the straight-line restriction is reasonable since it is typically satisfied byconstraints that are generated by symbolic execution, e.g., all constraints in the standard Kaluza
benchmarks [Saxena et al. 2010] with 50,000+ test cases generated by symbolic execution on
JavaScript applications were noted in [Ganesh et al. 2012] to satisfy this condition. Intuitively,
as elegantly described in [Bjørner et al. 2009], constraints from symbolic execution on stringmanipulating programs can be viewed as the problem of path feasibility over loopless stringmanipulating programs S with variable assignments and assertions, i.e., generated by the grammar
S ::= y := f (x 1 , . . . , x n ) | assert(д(x 1 , . . . , x n )) | S 1 ; S 2
where f : (Σ∗ ) n → Σ∗ and д : (Σ∗ ) n → {0, 1} are some string functions. Straight-line programs withassertions can be obtained by turning such programs into a Static Single Assignment (SSA) form
(i.e. introduce a new variable on the left hand side of each assignment). A partial decidability result
can be deduced from [Lin and Barceló 2016] for the straight-line fragment of the theory of strings,
where (1) f in the above grammar is either a concatenation of string constants and variables, or
the replaceAll function where the pattern and the replacement are both string constants, and (2) дis a boolean combination of regular constraints. In fact, the decision procedure therein admits
finite-state transducers, which subsume only the aforementioned simple form of the replaceAllfunction. The decidability boundary of the straight-line fragment involving the replaceAll functionin its general form (e.g., when the replacement parameter is a variable) remains open.
Contribution. We investigate the decidability boundary of the theory SL[replaceAll] of strings involving the replaceAll function and regular constraints, with the straight-line restriction introduced
in [Lin and Barceló 2016]. We provide a decidability result for a large fragment of SL[replaceAll],
which is sufficiently powerful to express the concatenation operator. We show that this decidability
result is in a sense maximal by showing that several important natural extensions of the logic resultin undecidability. We detail these results below:• If the pattern parameters of the replaceAll function are allowed to be variables, then thesatisfiability of SL[replaceAll] is undecidable (cf. Proposition 4.1).
• If the pattern parameters of the replaceAll function are regular expressions, then the satisfiability of SL[replaceAll] is decidable and in EXPSPACE (cf. Theorem 4.2). In addition, we showthat the satisfiability problem is PSPACE-complete for several cases that are meaningful inpractice (cf. Corollary 4.7). This strictly generalises the decidability result in [Lin and Barceló
2016] of the straight-line fragment with concatenation, regular constraints, and the replaceAllfunction where patterns/replacement parameters are constant strings.
• If SL[replaceAll], where the pattern parameter of the replaceAll function is a constant letter, isextended with the string-length constraint, then satisfiability becomes undecidable again. In
fact, this undecidability can be obtained with either integer constraints, character constraints,
or constraints involving the IndexOf function (cf. Theorem 9.4 and Proposition 9.6).
Our decision procedure for SL[replaceAll] where the pattern parameters of the replaceAll function
are regular expressions follows an automata-theoretic approach. The key idea can be illustrated asfollows. Let us consider the simple formula C ≡ x = replaceAll(y, a, z) ∧ x ∈ e 1 ∧ y ∈ e 2 ∧ z ∈ e 3 .
Suppose that A1 , A2 , A3 are the nondeterministic finite state automata corresponding to e 1 , e 2 , e 3
respectively. We effectively eliminate the use of replaceAll by nondeterministically generatingfrom A1 a new regular constraint A2′ for y as well as a new regular constraint A3′ for z. These
2 Similar notions that appear in the literature of string constraints (without replace) include acyclicity [Abdulla et al. 2014]

and solved form [Ganesh et al. 2012]

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:5

constraints incorporate the effect of the replaceAll function (i.e. all regular constraints are on the“source” variables). Then, the satisfiability of C is turned into testing the nonemptiness of theintersection of A2 and A2′ , as well as the nonemptiness of the intersection of A3 and A3′ . When
there are multiple occurrences of the replaceAll function, this process can be iterated. Our decision
procedure enjoys the following advantages:• It is automata-theoretic and built on clean automaton constructions, moreover, when theformula is satisfiable, a solution can be synthesised. For example, in the aforementioned XSS
vulnerability detection example, one can synthesise the values of the variables user and bio
for a potential attack.
• The decision procedure is modular in that the replaceAll terms are removed one by one
to generate more and more regular constraints (emptiness of the intersection of regularconstraints could be efficiently handled by state-of-the-art solvers like [Wang et al. 2016]).
• The decision procedure requires exponential space (thus double exponential time), but underassumptions that are reasonable in practice, the decision procedure uses only polynomial
space, which is not worse than other string logics (which can encode the PSPACE-complete
problem of checking emptiness of the intersection of regular constraints).
Organisation. This paper is organised as follows: Preliminaries are given in Section 2. The corestring language is defined in Section 3. The main results of this paper are summarised in Section 4.
The decision procedure is presented in Section 6-8, case by case. The extensions of the core string
language are investigated in Section 9. The related work can be found in Section 10. The appendix
contains missing proofs and additional examples.
2

PRELIMINARIES

General Notation. Let Z and N denote the set of integers and natural numbers respectively. For
k ∈ N, let [k] = {1, · · · , k}. For a vector x⃗ = (x 1 , · · · , x n ), let |⃗x | denote the length of x⃗ (i.e., n) andx⃗ [i] denote x i for each i ∈ [n].
Regular Languages. Fix a finite alphabet Σ. Elements in Σ∗ are called strings. Let ε denote theempty string and Σ+ = Σ∗ \ {ε}. We will use a, b, · · · to denote letters from Σ and u, v, w, · · · todenote strings from Σ∗ . For a string u ∈ Σ∗ , let |u| denote the length of u (in particular, |ε | = 0). A
position of a nonempty string u of length n is a number i ∈ [n] (Note that the first position is 1,
instead of 0). In addition, for i ∈ [|u |], let u[i] denote the i-th letter of u. For two strings u 1 , u 2 , weuse u 1 · u 2 to denote the concatenation of u 1 and u 2 , that is, the string v such that |v | = |u 1 | + |u 2 |and for each i ∈ [|u 1 |], v[i] = u 1 [i] and for each i ∈ |u 2 |, v[|u 1 | + i] = u 2 [i]. Let u, v be two strings.
If v = u · v ′ for some string v ′, then u is said to be a prefix of v. In addition, if u , v, then u is said
to be a strict prefix of v. If u is a prefix of v, that is, v = u · v ′ for some string v ′, then we use u −1v
to denote v ′. In particular, ε −1v = v.
A language over Σ is a subset of Σ∗ . We will use L 1 , L 2 , . . . to denote languages. For two languages
L 1 , L 2 , we use L 1 ∪ L 2 to denote the union of L 1 and L 2 , and L 1 · L 2 to denote the concatenation of
L 1 and L 2 , that is, the language {u 1 · u 2 | u 1 ∈ L 1 , u 2 ∈ L 2 }. For a language L and n ∈ N, we define
Ln , the iteration of L for n times, inductively as follows: L0 = {ε} and Ln = L · Ln−1 for n > 0. We
S nalso use L∗ to denote the iteration of L for arbitrarily many times, that is, L∗ =L . Moreover,n∈NS
let L+ =Ln .
n ∈N\{0}Definition 2.1 (Regular expressions RegExp).
e = ∅ | ε | a | e + e | e ◦ e | e ∗ , where a ∈ Σ.
defProceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:6

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

Since + is associative and commutative, we also write (e 1 + e 2 ) + e 3 as e 1 + e 2 + e 3 for brevity. We
use the abbreviation e + ≡ e ◦ e ∗ . Moreover, for Γ = {a 1 , · · · , an } ⊆ Σ, we use the abbreviations
Γ ≡ a 1 + · · · + an and Γ ∗ ≡ (a 1 + · · · + an ) ∗ .
We define L(e) to be the language defined by e, that is, the set of strings that match e, inductively
as follows: L(∅) = ∅, L(ε ) = {ε}, L(a) = {a}, L(e 1 +e 2 ) = L(e 1 ) ∪ L(e 2 ), L(e 1 ◦e 2 ) = L(e 1 ) · L(e 2 ),L(e 1∗ ) = (L(e 1 )) ∗ . In addition, we use |e | to denote the number of symbols occurring in e.
A nondeterministic finite automaton (NFA) A on Σ is a tuple (Q, δ, q 0 , F ), where Q is a finite set ofstates, q 0 ∈ Q is the initial state, F ⊆ Q is the set of final states, and δ ⊆ Q × Σ × Q is the transition
relation. For a string w = a 1 . . . an , a run of A on w is a state sequence q 0 . . . qn such that for eachi ∈ [n], (qi−1 , ai , qi ) ∈ δ . A run q 0 . . . qn is accepting if qn ∈ F . A string w is accepted by A if there
is an accepting run of A on w. We use L(A) to denote the language defined by A, that is, theset of strings accepted by A. We will use A, B, · · · to denote NFAs. For a string w = a 1 . . . an , wewalso use the notation q 1 −−→ qn+1 to denote the fact that there are q 2 , . . . , qn ∈ Q such that for eachAi ∈ [n], (qi , ai , qi+1 ) ∈ δ . For an NFA A = (Q, δ, q 0 , F ) and q, q ′ ∈ Q, we use A (q, q ′ ) to denote the
NFA obtained from A by changing the initial state to q and the set of final states to {q ′ }. The size ofan NFA A = (Q, δ, q 0 , F ), denoted by |A|, is defined as |Q |, the number of states. For convenience,
we will also call an NFA without initial and final states, that is, a pair (Q, δ ), as a transition graph.
It is well-known (e.g. see [Hopcroft and Ullman 1979]) that regular expressions and NFAs are
expressively equivalent, and generate precisely all regular languages. In particular, from a regularexpression, an equivalent NFA can be constructed in linear time. Moreover, regular languages areclosed under Boolean operations, i.e., union, intersection, and complementation. In particular, given
two NFA A1 = (Q 1 , δ 1 , q 0,1 , F 1 ) and A2 = (Q 2 , δ 2 , q 0,2 , F 2 ) on Σ, the intersection L(A1 ) ∩ L(A2 ) is
recognised by the product automaton A1 ×A2 of A1 and A2 defined as (Q 1 ×Q 2 , δ, (q 0,1 , q 0,2 ), F 1 ×F 2 ),where δ comprises the transitions ((q 1 , q 2 ), a, (q 1′ , q 2′ )) such that (q 1 , a, q 1′ ) ∈ δ 1 and (q 2 , a, q 2′ ) ∈ δ 2 .
Graph-Theoretical Notation. A DAG (directed acyclic graph) G is a finite directed graph (V , E)with no directed cycles, where V (resp. E ⊆ V × V ) is a set of vertices (resp. edges). Equivalently, a
DAG is a directed graph that has a topological ordering, which is a sequence of the vertices suchthat every edge is directed from an earlier vertex to a later vertex in the sequence. An edge (v, v ′ )in G is called an incoming edge of v ′ and an outgoing edge of v. If (v, v ′ ) ∈ E, then v ′ is called asuccessor of v and v is called a predecessor of v ′. A path π in G is a sequence v0 e1 v1 · · · vn−1 en vn
such that for each i ∈ [n], we have ei = (vi−1 , vi ) ∈ E. The length of the path π is the number n ofedges in π . If there is a path from v to v ′ (resp. from v ′ to v) in G, then v ′ is said to be reachable(resp. co-reachable) from v in G. If v is reachable from v ′ in G, then v ′ is also called an ancestorof v in G. In addition, an edge (v ′, v ′′ ) is said to be reachable (resp. co-reachable) from v if v ′ isreachable from v (resp. v ′′ is co-reachable from v). The in-degree (resp. out-degree) of a vertex v isthe number of incoming (resp. outgoing) edges of v. A subgraph G ′ of G = (V , E) is a directed graph(V ′, E ′ ) with V ′ ⊆ V and E ′ ⊆ E. Let G ′ be a subgraph of G. Then G \ G ′ is the graph obtained fromG by removing all the edges in G ′.
Computational Complexity. In this paper, we study not only decidability but also the complexityof string logics. In particular, we shall deal with the following computational complexity classes(see [Hopcroft and Ullman 1979] for more details): PSPACE (problems solvable in polynomial space
and thus in exponential time), and EXPSPACE (problems solvable in exponential space and thus
in double exponential time). Verification problems that have complexity PSPACE or beyond (see[Baier and Katoen 2008] for a few examples) have substantially benefited from techniques such as
symbolic model checking [McMillan 1993].
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function
3

3:7

THE CORE CONSTRAINT LANGUAGE

In this section, we define a general string constraint language that supports concatenation, thereplaceAll function, and regular constraints. Throughout this section, we fix an alphabet Σ.
3.1

Semantics of the replaceAll Function

To define the semantics of the replaceAll function, we note that the function encompasses threeparameters: the first parameter is the subject string, the second parameter is a pattern that is astring or a regular expression, and the third parameter is the replacement string. When the patternparameter is a string, the semantics is somehow self-explanatory. However, when it is a regularexpression, there is no consensus on the semantics even for the mainstream programming languages
such as Python and Javascript. This is particularly the case when interpreting the union (akaalternation) operator in regular expressions or performing a replaceAll with a pattern that matches
ε. In this paper, we mainly focus on the semantics of leftmost and longest matching. Our handlingof ε matches is consistent with our testing of the implementation in Python and the sed commandwith the --posix flag. We also assume union is commutative (e.g. replaceAll(aa, a + aa, b) =replaceAll(aa, aa + a, b) = b) as specified by POSIX, but often ignored in practice (where bb is acommon result in the former case).
Definition 3.1. Let u, v be two strings such that v = v 1uv 2 for some v 1 , v 2 and e be a regularexpression. We say that u is the leftmost and longest matching of e in v if one of the following two
conditions hold,• case ε < L(e):(1) leftmost: u ∈ L(e), and (v 1′ ) −1v < L(e ◦ Σ∗ ) for every strict prefix v 1′ of v 1 ,(2) longest: for every nonempty prefix v 2′ of v 2 , u · v 2′ < L(e).
• case ε ∈ L(e):(1) leftmost: u ∈ L(e), and v 1 = ε,(2) longest: for every nonempty prefix v 2′ of v 2 , u · v 2′ < L(e).
Example 3.2. Let us first consider Σ = {0, 1}, v = 1010101, v 1 = 1, u = 010, v 2 = 101, ande = 0∗ 01(0∗ + 1∗ ). Then v = v 1uv 2 , and the leftmost and longest matching of e in v is u. This isbecause u ∈ L(e), ε −1v = v < L(e ◦ Σ∗ ) (notice that v 1 has only one strict prefix, i.e. ε), and noneof u1 = 0101, u10 = 01010, and u101 = 010101 belong to L(e) (notice that v 2 has three nonempty
prefixes, i.e. 1, 10, 101). For another example, let us consider Σ = {a, b, c}, v = baac, v 1 = ε, u = ε,v 2 = v, and e = a ∗ . Then v = v 1uv 2 and the leftmost and longest matching of e in v is u. This isbecause u ∈ L(e), v 1 = ε, and b, ba, baa, baac < L(e). On the other hand, similarly, one can verify
that the leftmost and longest matching of e = a ∗ in v = aac is u = aa.
Definition 3.3. The semantics of replaceAll(u, e, v), where u, v are strings and e is a regularexpression, is defined inductively as follows:• if u < L(Σ∗ ◦e◦Σ∗ ), that is, u does not contain any substring from L(e), then replaceAll(u, e, v) =u,• otherwise,– if ε ∈ L(e) and u is the leftmost and longest matching of e in u, then replaceAll(u, e, v) = v,
– if ε ∈ L(e), u = u 1 · a · u 2 , u 1 is the leftmost and longest matching of e in u, and a ∈ Σ, thenreplaceAll(u, e, v) = v · a · replaceAll(u 2 , e, v),– if ε < L(e), u = u 1 · u 2 · u 3 , and u 2 is the leftmost and longest matching of e in u, thenreplaceAll(u, e, v) = u 1 · v · replaceAll(u 3 , e, v).
Example 3.4. At first, replaceAll(abab, ab, d ) = d ·replaceAll(ab, ab, d ) = dd ·replaceAll(ϵ, ab, d ) =dd · ε = dd and replaceAll(baac, a + , b) = bbc. In addition, replaceAll(aaaa, “”, d ) = dadadadad andProceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:8

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

replaceAll(baac, a ∗ , b) = bbbcb. The argument for replaceAll(baac, a ∗ , b) = bbbcb proceeds asfollows: The leftmost and longest matching of a ∗ in baac is u 1 = ε, where baac = u 1 · b · u 2 andu 2 = aac. Then replaceAll(baac, a ∗ , b) = b · b · replaceAll(aac, a ∗ , b). Since aa is the leftmost andlongest matching of a ∗ in aac, we have replaceAll(aac, a ∗ , b) = b · c · replaceAll(ε, a ∗ , b) = bcb.
Therefore, we get replaceAll(baac, a ∗ , b) = bbbcb. (The readers are invited to test this in Python
and sed.)
3.2

Straight-Line String Constraints With the replaceAll Function

We consider the String data type Str, and assume a countable set of variables x, y, z, · · · of Str.
Definition 3.5 (Relational and regular constraints). Relational constraints and regular constraints
are defined by the following rules,
s
p
φ
ψ

=
=
def
=
def
=

def

def

x |u
x |e
x = s ◦ s | x = replaceAll(s, p, s) | φ ∧ φx ∈ e | ψ ∧ψ

(string terms)(pattern terms)(relational constraints)(regular constraints)

where x is a string variable, u ∈ Σ∗ and e is a regular expression over Σ.
For a formula φ (resp. ψ ), let Vars(φ) (resp. Vars(ψ )) denote the set of variables occurring in φ(resp. ψ ). Given a relational constraint φ, a variable x is called a source variable of φ if φ does notcontain a conjunct of the form x = s 1 ◦ s 2 or x = replaceAll(−, −, −).
We then notice that, with the replaceAll function in its general form, the concatenation operation
is in fact redundant.
Proposition 3.6. The concatenation operation (◦) can be simulated by the replaceAll function.
Proof. It is sufficient to observe that a relational constraint x = s 1 ◦ s 2 can be rewritten as
x ′ = replaceAll(ab, a, s 1 ) ∧ x = replaceAll(x ′, b, s 2 ),where a, b are two fresh letters.

□

In light of Proposition 3.6, in the sequel, we will dispense the concatenation operator mostly andfocus on the string constraints that involve the replaceAll function only.
Another example to show the power of the replaceAll function is that it can simulate theextension of regular expressions with string variables, which is supported by the mainstream
scripting languages like Python, Javascript, and PHP. For instance, x ∈ y ∗ can be expressed byx = replaceAll(x ′, a, y) ∧ x ′ ∈ a ∗ , where x ′ is a fresh variable and a is a fresh letter.
The generality of the constraint language makes it undecidable, even in very simple cases. To
retain decidability, we follow [Lin and Barceló 2016] and focus on the “straight-line fragment" of thelanguage. This straight-line fragment captures the structure of straight-line string-manipulating
programs with the replaceAll string operation.
Definition 3.7 (Straight-line relational constraints). A relational constraint φ with the replaceAllV
deffunction is straight-line, if φ =x i = Pi such that1≤i ≤m• x 1 , . . . , xm are mutually distinct,• for each i ∈ [m], all the variables in Pi are either source variables, or variables from{x 1 , . . . , x i−1 },Remark 3.8. Checking whether a relational constraint φ is straight-line can be done in linear time.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:9

Definition 3.9 (Straight-line string constraints). A straight-line string constraint C with thereplaceAll function (denoted by SL[replaceAll]) is defined as φ ∧ ψ , where• φ is a straight-line relational constraint with the replaceAll function, and• ψ is a regular constraint.
Example 3.10. The following string constraint belongs to SL[replaceAll]:C ≡ x 2 = replaceAll(x 1 , 0, y1 ) ∧ x 3 = replaceAll(x 2 , 1, y2 ) ∧ x 1 ∈ {0, 1}∗ ∧ y1 ∈ 1∗ ∧ y2 ∈ 0∗ .
4 THE SATISFIABILITY PROBLEM
In this paper, we focus on the satisfiability problem of SL[replaceAll], which is formalised as follows.
Given an SL[replaceAll] constraint C, decide whether C is satisfiable.
To approach this problem, we identify several fragments of SL[replaceAll], depending on whether
the pattern and the replacement parameters are constants or variables. We shall investigate extensively the satisfiability problem of the fragments of SL[replaceAll].
We begin with the case where the pattern parameters of the replaceAll terms are variables. It
turns out that in this case the satisfiability problem of SL[replaceAll] is undecidable. The proof is bya reduction from Post’s Correspondence Problem. Due to space constraints we relegate the proof
to Appendix A.
Proposition 4.1. The satisfiability problem of SL[replaceAll] is undecidable, if the pattern parameters of the replaceAll terms are allowed to be variables.
In light of Proposition 4.1, we shall focus on the case that the pattern parameters of the replaceAllterms are constants, being a single letter, a constant string, or a regular expression. The main resultof the paper is summarised as the following Theorem 4.2.
Theorem 4.2. The satisfiability problem of SL[replaceAll] is decidable in EXPSPACE, if the patternparameters of the replaceAll terms are regular expressions.
The following three sections are devoted to the proof of Theorem 4.2.
• We start with the single-letter case that the pattern parameters of the replaceAll terms are
single letters (Section 6),• then consider the constant-string case that the pattern parameters of the replaceAll terms areconstant strings (Section 7),• and finally the regular-expression case that the pattern parameters of the replaceAll terms are
regular expressions (Section 8).
We first introduce a graphical representation of SL[replaceAll] formulae as follows.
Definition 4.3 (Dependency graph). Suppose C = φ ∧ ψ is an SL[replaceAll] formula where thepattern parameters of the replaceAll terms are regular expressions. Define the dependency graph of C
as GC = (Vars(φ), EC ), such that for each i ∈ [m], if x i = replaceAll(z, ei , z ′ ), then (x i , (l, ei ), z) ∈ EC
and (x i , (r, ei ), z ′ ) ∈ EC . A final (resp. initial) vertex in GC is a vertex in GC without successors (resp.
predecessors). The edges labelled by (l, ei ) and (r, ei ) are called the l-edges and r-edges respectively.
The depth of GC is the maximum length of the paths in GC . In particular, if φ is empty, then thedepth of GC is zero.
Note that GC is a DAG where the out-degree of each vertex is two or zero.
Definition 4.4 (Diamond index and l-length). Let C be an SL[replaceAll] formula and GC =(Vars(φ), EC ) be its dependency graph. A diamond ∆ in GC is a pair of vertex-disjoint simple paths
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:10

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

from z to z ′ for some z, z ′ ∈ Vars(φ). The vertices z and z ′ are called the source and destination
vertex of the diamond respectively. A diamond ∆2 with the source vertex z 2 and destination vertex
z 2′ is said to be reachable from another diamond ∆1 with the source vertex z 1 and destination vertex
z 1′ if z 2 is reachable from z 1′ (possibly z 2 = z 1′ ). The diamond index of GC , denoted by Idxdmd (GC ),is defined as the maximum length of the diamond sequences ∆1 · · · ∆n in GC such that for eachi ∈ [n − 1], ∆i+1 is reachable from ∆i . The l-length of a path in GC is the number of l-edges in thepath. The l-length of GC , denoted by Lenlft (GC ), is the maximum l-length of paths in GC .
For each dependency graph GC , since each diamond uses at least one l-edge, we know that
Idxdmd (GC ) ≤ Lenlft (GC ).
Proposition 4.5. Let C be an SL[replaceAll] formula and GC = (Vars(φ), EC ) be its dependency
graph. For each pair of distinct vertices z, z ′ in GC , there are at most (|Vars(φ)||EC |) O (Idxdmd (GC ))different paths from z to z ′.
It follows from Proposition 4.5 that for a class of SL[replaceAll] formulae C such that Idxdmd (GC )is bounded by a constant c, there are polynomially many different paths between each pair ofdistinct vertices in GC .
Example 4.6. Let GC be the dependency graph illustrated in Figure 1. It is easy to see that
Idxdmd (GC ) is 3. In addition, there are 23 = 8 paths from x 1 to y1 . If we generalise GC in Figure 1 toa dependency graph comprising n diamonds from x 1 to x 2 , · · · , from x n−1 to x n , and from x n to y1
respectively, then the diamond index of the resulting dependency graph is n and there are 2n paths
from x 1 to y1 in the graph.
(l, a1 )(l, a2 )x2

x1(r, a1 )(l, a3 )x3(r, a2 )y1(r, a3 )Fig. 1. The diamond index and the number of paths in GC

In Section 6–8, we will apply a refined analysis of the complexity of the decision procedures forproving Theorem 4.2 and get the following results.
Corollary 4.7. The satisfiability problem is PSPACE-complete for the following fragments ofSL[replaceAll]:• the single-letter case, plus the condition that the diamond indices of the dependency graphs arebounded by a constant c,• the constant-string case, plus the condition that the l-lengths of the dependency graphs arebounded by a constant c,• the regular-expression case, plus the condition that the l-lengths of the dependency graphs are at
most 1.
Corollary 4.7 partially justifies our choice to present the decision procedures for the single-letter,
constant-string, and regular-expression case separately. Intuitively, when the pattern parametersof the replaceAll terms become less restrictive, the decision procedures become more involved, andmore constraints should be imposed on the dependency graphs in order to achieve the PSPACE
upper-bound. The PSPACE lower-bound follows from the observation that nonemptiness of theintersection of the regular expressions e 1 , · · · , en over the alphabet {0, 1}, which is a PSPACEcomplete problem, can be reduced to the satisfiability of the formula x ∈ e 1 ∧ · · · ∧ x ∈ en , whichfalls into all fragments of SL[replaceAll] specified in Corollary 4.7. At last, we remark that theProceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:11

restrictions in Corollary 4.7 are partially inspired by the benchmarks in practice. Diamond indices(intuitively, the “nesting depth” of replaceAll(x, a, x )) are likely to be small in practice because theconstraints like replaceAll(x, a, x ) are rather artificial and rarely occur in practice. Moreover, thel-length reflects the nesting depth of replaceall w.r.t. the first parameter, which is also likely to besmall. Finally, for string constraints with concatenation and replaceAll where pattern/replacement
parameters are constants, the diamond index is no greater than the “dimension” defined in [Lin andBarceló 2016], where it was shown that existing benchmarks mostly have “dimensions" at mostthree for such string constraints.
5

OUTLINE OF DECISION PROCEDURES

We describe our decision procedure across three sections (Section 6–Section 8). This means theideas can be introduced in a step-by-step fashion, which we hope helps the reader. In addition, bypresenting separate algorithms, we can give the fine-grained complexity analysis required to show
Corollary 4.7. We first outline the main ideas needed by our approach.
We will use automata-theoretic techniques. That is, we make use of the fact that regular expressions can be represented as NFAs. We can then consider a very simple string expression, which
is a single regular constraint x ∈ e. It is well-known that an NFA A can be constructed that isequivalent to e. We can also test in LOGSPACE whether there is some word w accepted by A. If
this is the case, then this word can be assigned to x, giving a satisfying assignment to the constraint.
If this is not the case, then there is no satisfying assignment.
A more complex case is a conjunction of several constraints of the form x ∈ e. If the constraints
apply to different variables, they can be treated independently to find satisfying assignments. If theconstraints apply to the same variable, then they can be merged into a single NFA. Intuitively, takex ∈ e 1 ∧ x ∈ e 2 and A1 and A2 equivalent to e 1 and e 2 respectively. We can use the fact that NFA
are closed under intersection a check if there is a word accepted by A1 × A2 . If this is the case, we
can construct a satisfying assignment to x from an accepting run of A1 × A2 .
In the general case, however, variables are not independent, but may be related by a use of
replaceAll. In this case, we perform a kind of replaceAll elimination. That is, we successively remove
instances of replaceAll from the constraint, building up an expanded set of regular constraints(represented as automata). Once there are no more instances of replaceAll we can solve the regularconstraints as above. Briefly, we identify some x = replaceAll(y, e, z) where x does not appear
as an argument to any other use of replaceAll. We then transform any regular constraints on x
into additional constraints on y and z. This allows us to remove the variable x since the extended
constraints on y and z are sufficient for determining satisfiability. Moreover, from a satisfying
assignment to y and z we can construct a satisfying assignment to x as well. This is the technicalpart of our decision procedure and is explained in detail in the following sections, for increasingly
complex uses of replaceAll.
6

DECISION PROCEDURE FOR SL[replaceAll]: THE SINGLE-LETTER CASE

In this section, we consider the single-letter case, that is, for the SL[replaceAll] formula C = φ ∧ ψ ,every term of the form replaceAll(z, e, z ′ ) in φ satisfies that e = a for a ∈ Σ. We begin by explaining
the idea of the decision procedure in the case where there is a single use of a replaceAll(−, −, −)term. Then we describe the decision procedure in full details.
6.1

A Single Use of replaceAll(−, −, −)Let us start with the simple case thatC ≡ x = replaceAll(y, a, z) ∧ x ∈ e 1 ∧ y ∈ e 2 ∧ z ∈ e 3 ,Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:12

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

where, for i = 1, 2, 3, we suppose Ai = (Q i , δi , q 0,i , Fi ) is the NFA corresponding to the regularexpression ei .
From the semantics, C is satisfiable if and only if x, y, z can be assigned with strings u, v, w so
that: (1) u is obtained from v by replacing all the occurrences of a in v with w, and (2) u, v, w are
accepted by A1 , A2 , A3 respectively. Let u, v, w be the strings satisfying these two constraints. As
u is accepted by A1 , there must be an accepting run of A1 on u. Let v = v 1av 2a · · · avk such that foreach i ∈ [k], vi ∈ (Σ \ {a}) ∗ . Then u = v 1wv 2w · · · wvk and there are states q 1 , q 1′ , · · · , qk −1 , qk′ −1 , qk
such that
vk
v1
v2
w
w
w
q 0,1 −−→ q 1 −−→ q 1′ −−→ q 2 −−→ q 2′ · · · qk −1 −−→ qk′ −1 −−→ qk
A1
A1
A1
A1
A1
A1
(
)
T
′
and qk ∈ F 1 . Let Tz denote (qi , qi ) | i ∈ [k − 1] . Then w ∈ L(A3 ) ∩L(A1 (q, q ′ )). In(q,q ′ ) ∈Tz

addition, let B A1,a,Tz be the NFA obtained from A1 by removing all the a-transitions first and thenadding the a-transitions (q, a, q ′ ) for (q, q ′ ) ∈ Tz . Then
v1

a

v2

a

a

vk

BA1 , a,Tz

BA1 , a,Tz

BA1 , a,Tz

BA1 , a,Tz

BA1 , a,Tz

BA1 , a,Tz′
q 0,1 −−−−−−−→ q 1 −−−−−−−→ q 1′ −−−−−−−→ q 2 −−−−−−−→ q 2′ · · · qk−1 −−−−−−−→ qk−1−−−−−−−→ qk .

Therefore, v ∈ L(A2 ) ∩ L(B A1,a,Tz ). We deduce that there is Tz ⊆ Q 1 × Q 1 such that L(A3 ) ∩T
L(A1 (q, q ′ )) , ∅ and L(A2 ) ∩ L(B A1,a,Tz ) , ∅. In addition, it is not hard to see that(q,q ′ ) ∈Tz

this condition is also sufficient for the satisfiability of C. The arguments proceed as follows: LetTv ∈ L(A2 ) ∩ L(B A1,a,Tz ) and w ∈ L(A3 ) ∩L(A1 (q, q ′ )). From v ∈ L(B A1,a,Tz ), we(q,q ′ ) ∈Tz

know that there is an accepting run of B A1,a,Tz on v. Recall that B A1,a,Tz is obtained from A1 by
first removing all the a-transitions, then adding all the transitions (q, a, q ′ ) for (q, q ′ ) ∈ Tz . Supposev = v 1av 2 · · · avk such that vi ∈ (Σ \ {a}) ∗ for each i ∈ [k] and
v1

a

v2

a

a

vk

BA1 , a,Tz

BA1 , a,Tz

BA1 , a,Tz

BA1 , a,Tz

BA1 , a,Tz

BA1 , a,Tz

q 0,1 −−−−−−−→ q 1 −−−−−−−→ q 1′ −−−−−−−→ q 2 −−−−−−−→ q 2′ · · · qk −1 −−−−−−−→ qk′ −1 −−−−−−−→ qk
v1

is an accepting run of B A1,a,Tz on v. Then q 0,1 −−→ q 1 , and for each i ∈ [k − 1] we have (qi , qi′ ) ∈ Tz
A1

v i +1and qi′ −−−→ qi+1 ; moreover, qk ∈ F 1 . Let u = replaceAll(v, a, w ) = v 1wv 2 · · · wvk . Since w ∈A1
T
L(A1 (q, q ′ )), we infer that(q,q ′ ) ∈Tz

v1

w

v2

w

w

vk

A1

A1

A1

A1

A1

A1

q 0,1 −−→ q 1 −−→ q 1′ −−→ q 2 −−→ q 2′ · · · qk −1 −−→ qk′ −1 −−→ qk
is an accepting run of A1 on u. Therefore, u is accepted by A1 and C is satisfiable.
Proposition 6.1. We have C ≡ x = replaceAll(y, a, z) ∧ x ∈ e 1 ∧ y ∈ e 2 ∧ z ∈ e 3 is satisfiable iff
Tthere exists Tz ⊆ Q 1 × Q 1 with L(A3 ) ∩L(A1 (q, q ′ )) , ∅ and L(A2 ) ∩ L(B A1,a,Tz ) , ∅.
(q,q ′ ) ∈Tz

From Proposition 6.1, we can decide the satisfiability of C in polynomial space as follows:
Step I. Nondeterministically choose a set Tz ⊆ Q 1 × Q 1 .
Step II. Nondeterministically choose an accepting run of the product automaton of A3 andA1 (q, q ′ ) for (q, q ′ ) ∈ Tz .
Step III. Nondeterministically choose an accepting run of the product automaton of A2 and
B A1,a,Tz .
During Step II and III, it is sufficient to record Tz and a state of the product automaton, which
occupies only a polynomial space.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:13

The above decision procedure can be easily generalised to the case that there are multiple
atomic regular constraints for x. For instance, let x ∈ e 1,1 ∧ x ∈ e 1,2 and for j = 1, 2, A1, j =(Q 1, j , δ 1, j , q 0,1, j , F 1, j ) be the NFA corresponding to e 1, j . Then in Step I, two sets T1,z ⊆ Q 1,1 × Q 1,1
and T2,z ⊆ Q 1,2 × Q 1,2 are nondeterministically chosen, moreover, Step II and III are adjusted
accordingly.
Example 6.2. Let C ≡ x = replaceAll(y, 0, z) ∧ x ∈ e 1 ∧ y ∈ e 2 ∧ z ∈ e 3 , where e 1 = (0 +1) ∗ (00(0 + 1) ∗ + 11(0 + 1) ∗ ), e 2 = (01) ∗ , and e 3 = (10) ∗ . The NFA A1 , A2 , A3 corresponding to
e 1 , e 2 , e 3 respectively are illustrated in Figure 2. Let Tz = {(q 0 , q 0 ), (q 1 , q 2 )}. ThenT
L(A3 ) ∩L(A1 (q, q ′ )) = L(A3 ) ∩ L(A1 (q 0 , q 0 )) ∩ L(A1 (q 1 , q 2 ))(q,q ′ ) ∈Tz=,

L((10) ∗ ) ∩ L((0 + 1) ∗ ) ∩ L(1(0 + 1) ∗ )∅.

In addition, B A1,0,Tz (also illustrated in Figure 2) is obtained from A1 by removing all the 0transitions, then adding the transitions (q 0 , 0, q 0 ) and (q 1 , 0, q 2 ). Then
L(A2 ) ∩ L(B A1,0,Tz ) = L((01) ∗ ) ∩ L((0 + 1) ∗ 101∗ ) , ∅.
T
We can choose z to be a string from L(A3 ) ∩L(A1 (q, q ′ )) = L((10) ∗ ) ∩ L((0 + 1) ∗ ) ∩(q,q ′ ) ∈Tz

L(1(0+1) ∗ ), say 10, and y to be a string from L(A2 )∩L(B A1,0,Tz ) = L((01) ∗ )∩L((0+1) ∗ 101∗ ), say
0101, then we set x to replaceAll(0101, 0, 10) = 101101, which is in L(A1 ). Thus, C is satisfiable. □
0

0

q3
0

0

q00

1

A2

q10

1

A1

q0
1

0

q4

1

1

0
q1

q000

q2

1

A3

q100

0

1

q3

q4
1

0

BA1 ,0,Tz

q0
1

0
1
q1

1

q2
1

Fig. 2. An example for the single-letter case: One replaceAll

6.2

The General CaseLet us now consider the general case where C contains multiple occurrences of replaceAll(−, −, −)terms. Then the satisfiability of C is decided by the following two-step procedure.
Step I. We utilise the dependency graph C and compute nondeterministically a collection of atomic
regular constraints E (x ) for each variable x, in a top-down manner.
Notice that E (x ) is represented succinctly as a set of pairs (T , P), where T = (Q, δ ) is atransition graph and P ⊆ Q × Q. The intention of (T , P) is to represent succinctly the collection
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:14

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wuof the atomic regular constraints containing (Q, δ, q, {q ′ }) for each (q, q ′ ) ∈ P, where q is the initialstate and {q ′ } is the set of final states.
Initially, let G 0 := GC . In addition, for each variable x, we define E0 (x ) as follows: Let x ∈e 1 ∧ · · · ∧ x ∈ en be the conjunction of all the atomic regular constraints related to x in C. For eachi ∈ [n], let Ai = (Q i , δi , q 0,i , Fi ) be the NFA corresponding to ei . We nondeterministically chooseqi ∈ Fi and set E0 (x ) := ((Q i , δi ), {(q 0,i , qi )}) | i ∈ [n] .
We begin with i := 0 and repeat the following procedure until we reach some i where G i is anempty graph, i.e. a graph without edges. Note that G 0 was defined above.
(1) Select a vertex x of G i such that x has no predecessors and has two successors via edges(x, (l, a), y) and (x, (r, a), z) in G i . Suppose Ei (x ) = {(T1 , P1 ), · · · , (Tk , Pk )}, where for eachj ∈ [k], Tj = (Q j , δ j ). Then Ei+1 (z) and Ei+1 (y) and G i+1 are computed as follows:(a) For each j ∈ [k], nondeterministically choose a set T j,z ⊆ Q j × Q j .
(b) If y , z, then let()()
Ei+1 (z) := Ei (z) ∪ (Tj ,T j,z ) | j ∈ [k] and Ei+1 (y) := Ei (y) ∪ (TTj ,a,Tj, z , Pj ) | j ∈ [k]where TTj ,a,Tj, z is obtained from Tj by first removing all the a-transitions, then adding all the()
transitions (q, a, q ′ ) for (q, q ′ ) ∈ T j,z . Otherwise, let Ei+1 (z) := Ei (z)∪ (Tj ,T j,z ) | j ∈ [k] ∪()(TTj ,a,Tj, z , Pj ) | j ∈ [k] . In addition, for each vertex x ′ distinct from y, z, let Ei+1 (x ′ ) :=Ei (x ′ ).
(c) Let G i+1 := G i \ {(x, (l, a), y), (x, (r, a), z)}.
(2) Let i := i + 1.
For each variable x, let E (x ) denote the set Ei (x ) after exiting the above loop.
Step II. Output “satisfiable” if for each source variable x there is an accepting run of the product of
all the NFA in E (x ); otherwise, output “unsatisfiable”.
It remains to argue the correctness and complexity of the above procedure and show how to
obtain satisfying assignments to satisfiable constraints. Correctness follows a similar argument to
Proposition 6.1 and is presented in Appendix B. Intuitively, Proposition 6.1 shows our procedurecorrectly eliminates occurrences of replaceAll until only regular constraints remain.
If, in the case that the equation is satisfiable, one wishes to obtain a satisfying assignment to all
variables, we can proceed as follows. First, for each source variable x, nondeterministically choose
an accepting run of the product of all the NFA in E (x ). As argued in Appendix B, the word labelling
this run satisfies all regular constraints on x since it is taken from a language that is guaranteed
to be a subset of the set of words satisfying the original constraints. For non-source variables, wederive an assignment as in Proposition 6.1, proceeding by induction from the source variables. Thatis, select some variable x such that x is derived from variables y and z and assignments to both y andz have already been obtained. The value for x is immediately obtained by performing the replaceAll
operation using the assignments to y and z. That this value satisfies all regular constraints on x
follows the same argument as Proposition 6.1. The procedure terminates when all variables havebeen assigned.
We now give an example before proceeding to the complexity analysis.
Example 6.3. Suppose C ≡ x = replaceAll(y, 0, z) ∧y = replaceAll(y ′, 1, z ′ ) ∧x ∈ e 1 ∧y ∈ e 2 ∧z ∈e 3 ∧y ′ ∈ e 4 ∧ z ′ ∈ e 5 , where e 1 , e 2 , e 3 are as in Example 6.2, e 4 = 0∗ 1∗ 0∗ 1∗ , and e 5 = 0∗ 1∗ . Let A4 , A5
be the NFA corresponding to e 4 and e 5 respectively (see Figure 3). The dependency graph GC of C
is illustrated in Figure 3. Let T1 , · · · , T5 be the transition graph of A1 , · · · , A5 respectively. Thenthe collection of regular constraints E (·) are computed as follows.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:15• Let G 0 = GC . Pick the sets E0 (x ) = {(T1 , {(q 0 , q 2 )})}, E0 (y) = {(T2 , {(q 0′ , q 0′ )})}, E0 (z) ={(T3 , {(q 0′′, q 0′′ )})}, E0 (y ′ ) = {(T4 , {(p0 , p1 )})}, and E0 (z ′ ) = {(T5 , {(p0′ , p1′ )})} nondeterministically.
• Select the vertex x in G 0 , construct E1 (y) and E1 (z) as in Example 6.2, that is, nondeterministically choose Tz = {(q 0 , q 0 ), (q 1 , q 2 )}, let
E1 (z) = {(T3 , {(q 0′′, q 0′′ )}), (T1 , {(q 0 , q 0 ), (q 1 , q 2 )})} and E1 (y) = {(T2 , {(q 0′ , q 0′ )}), (TT1,0,Tz , {(q 0 , q 2 )})},
where TT1,0,Tz is the transition graph of B A1,0,Tz illustrated in Figure 2. In addition, E1 (x ) =E0 (x ), E1 (y ′ ) = E0 (y ′ ) and E1 (z ′ ) = E0 (z ′ ). Finally, we get G 1 from G 0 by removing the twoedges from x.
• Select the vertex y in G 1 , construct E2 (y ′ ) and E2 (z ′ ) as follows: Nondeterministically choose
T1,z ′ = {(q 0′ , q 0′ )} for T2 and T2,z ′ = {(q 0 , q 1 ), (q 1 , q 2 )} for TT1,0,Tz , let
E2 (z ′ ) = (T5 , {(p0′ , p1′ )}), (T2 , {(q 0′ , q 0′ )}), (TT1,0,Tz , {(q 0 , q 1 ), (q 1 , q 2 )}) , and()
E2 (y ′ ) = (T4 , {(p0 , p1 )}), (TT2,1,T1, z ′ , {(q 0′ , q 0′ )}), (TTT1, 0,Tz ,1,T2, z ′ , {(q 0 , q 2 )}) ,where TT2,1,T1, z ′ and TTT1, 0,Tz ,1,T2, z ′ are shown in Figure 4. In addition, E2 (x ) = E1 (x ), E2 (y) =E1 (y), and E2 (z) = E1 (z). Finally, we get G 2 from G 1 by removing the two edges from y.
Since G 2 contains no edges, we have E (x ) = E2 (x ), similarly for E (y), E (z), E (y ′ ), and E (z ′ ).
For the three source variables y ′, z ′, z, it is not hard to check that 01 belongs to the intersectionof the regular constraints in E (z ′ ), 11 belongs to the intersection of the regular constraints in
E (y ′ ), and 10 belongs to the intersection of the regular constraints in E (z). Then y takes the value
replaceAll(11, 1, 01) = 0101 ∈ L(e 2 ), and x takes the value replaceAll(0101, 0, 10) = 101101 ∈ L(e 1 ).
Therefore, C is satisfiable.
□
GC
0
A4

p0

1
1

0
0

p1

1

p2

0
A5

1

x

p3

(l, 0)(r, 0)yz(l, 1)(r, 1)

y0

z0

1
1

p00

p01

Fig. 3. An example for the single-letter case: Multiple replaceAll

q3

1
0
q00

q4

0

TT2 ,1,T1,z0

q10

TTT1 ,0,Tz ,1,T2,z0

q0

1

1
q1

0

q2

Fig. 4. TT2,1,T1, z ′ and TTT1, 0,Tz ,1,T2, z ′Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:16

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

6.2.1 Complexity. To show our decision procedure works in exponential space, it is sufficient toshow that the cardinalities of the sets E (x ) are exponential w.r.t. the size of C.
Proposition 6.4. The cardinalities of E (x ) for the variables x in GC are at most exponential in
Idxdmd (GC ), the diamond index of GC .
Therefore, according to Proposition 6.4, if the diamond index of GC is bounded by a constant c,then the cardinalities of E (x ) become polynomial in the size of C and we obtain a polynomial spacedecision procedure. In this case, we conclude that the satisfiability problem is PSPACE-complete.
Proof of Proposition 6.4. Let K be the maximum of |E0 (x )| for x ∈ Vars(φ). For each variable
x in GC , all the regular constraints in E (x ) are either from E0 (x ), or are generated from some regularconstraints from E0 (x ′ ) for the ancestors x ′ of x. Let x ′ be an ancestor of x. Then for each (T , P) ∈E0 (x ′ ), according to Step I in the decision procedure, by an induction on the maximum length ofthe paths in from x ′ to x, we can show that the number of elements in E (x ) that are generated from(T , P) is at most the number of different paths from x ′ to x. From Proposition 4.5, we know that
there are at most (|Vars(φ)| · |EC |) O (Idxdmd (GC )) different paths from x ′ to x. Since there are at most|Vars(φ)| ancestors of x, we deduce that |E (x )| ≤ K · |Vars(φ)| · (|Vars(φ)||EC |) O (Idxdmd (GC )) .
□7

DECISION PROCEDURE FOR SL[replaceAll]: THE CONSTANT-STRING CASE

In this section, we consider the constant-string special case, that is, for an SL[replaceAll] formulaC = φ ∧ ψ , every term of the form replaceAll(z, e, z ′ ) in φ satisfies that e = u for u ∈ Σ+ . Note thatthe case when u = ϵ will be dealt with in Section 8.
Again, let us start with the simple situation that C ≡ x = replaceAll(y, u, z) ∧ x ∈ e 1 ∧ y ∈e 2 ∧ z ∈ e 3 , where |u | ≥ 2. For i = 1, 2, 3, let Ai = (Q i , δi , q 0,i , Fi ) be the NFA corresponding to ei .
In addition, let k = |u | and u = a 1 · · · ak with ai ∈ Σ for each i ∈ [k].
From the semantics, C is satisfiable iff x, y, z can be assigned with strings v, w, w ′ such that: (1)v = replaceAll(w, u, w ′ ), and (2) v, w, w ′ are accepted by A1 , A2 , A3 respectively. Let v, w, w ′ be
the strings satisfying these two constraints. Since v = replaceAll(w, u, w ′ ), we know that there arestrings w 1 , w 2 , · · · , w n such that w = w 1uw 2 · · · uw n and v = w 1w ′w 2 · · · w ′w n . As v is accepted by
A1 , there is an accepting run of A1 on v, say
w1

w′

w2

w′

w′

wn

A1

A1

A1

A1

A1

A1

′
q 0,1 −−→ q 1 −−→ q 1′ −−→ q 2 −−→ q 2′ · · · qn−1 −−→ qn−1−−→ qn .

Let Tz = {(qi , qi′ )T(q,q ′ ) ∈Tz| i∈ [n]}. Then w ′∈ L(A3 ) ∩T(q,q ′ ) ∈Tz

L(A1 (q, q ′ )). Therefore, L(A3 ) ∩L(A1 (q, q ′ )) , ∅. Similar to the single-letter case, we construct an NFA B A1,u,Tz to char-acterise the satisfiability of C. More precisely, C is satisfiable iff there is Tz ⊆ Q 1 × Q 1 such thatT
L(A3 ) ∩L(A1 (q, q ′ )) , ∅ and L(A2 ) ∩ L(B A1,u,Tz ) , ∅. Intuitively, when reading the(q,q ′ ) ∈Tz

string w, B A1,u,Tz simulates the generation of v from w and w ′ (that is, the replacement of every
occurrence of u in w with w ′) and verifies that v is accepted by A1 , by using Tz . To build B A1,u,Tz ,we utilise the concepts of window profiles and parsing automata defined below. Intuitively, awindow profile keeps track of which positions in the preceding characters could form the beginningof a match of u.
Definition 7.1 (window profiles w.r.t. u). Let v be a nonempty string with k = |v |, and i ∈ [k].
→−Then the window profile of the position i in v w.r.t. u is W ∈ {⊥, ⊤}k −1 defined as follows:→−• If i ≥ k − 1, then for each j ∈ [k − 1], W [j] = ⊤ iff v[i − j + 1] · · · v[i] = u[1] · · · u[j].
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:17

→
−
• If i < k − 1, then for each j ∈ [i], W [j] = ⊤ iff v[i − j + 1] · · · v[i] = u[1] · · · u[j], and for each→−j : i < j ≤ k − 1, W [j] = ⊥.
Let WPu denote the set of window profiles of the positions in nonempty strings w.r.t. u.
Proposition 7.2. |WPu | ≤ |u |.
→−Proof. Let k = |u |. For each profile W , let v be a nonempty string and i be a position of v such→−−→ as follows:that for each j ∈ [k − 1], W [j] = ⊤ iff v[i − j + 1] . . . v[i] = u[1] . . . u[j]. Define idxW→−−
→ is the maximum of such indices j ∈ [k − 1],
If there is j ∈ [k − 1] such that W [j] = ⊤, then idxW→−−
→ = 0. The following fact holds for W and idx−→:
otherwise, idxWW→−−
→ < j ′ ≤ k − 1, W [j ′ ] = ⊥,• for each j ′ : idxW
→
−
→
−
−
→ + 1] · · · v[i] = u[1] · · · u[idx−→ ], the values of W [1], · · · , W [idx−→]• in addition, since v[i − idxW
W
W
−
→ ].
are completely determined by u[1] · · · u[idxW
→
−
→
−
−
→ . Then ηLet η : WPu → {0} ∪ [k − 1] be a function such that for each W ∈ WPu , η(W ) = idxW−−→′→
− −−→′→−−→ = idx−−→′ iff W = W . Therefore, we
is an injective function, since for every W , W ∈ WPu , idxWW
conclude that |WPu | ≤ k.
□
Example 7.3. Let Σ = {0, 1}, u = 010. Then WPu = {⊥⊥, ⊤⊥, ⊥⊤}.
• Consider the string v = 1 and the position i = 1 in v. Since v[1] = 1 , u[1] = 0, the window
profile of i in v w.r.t. u is ⊥⊥.
• Consider the string v = 00 and the position i = 2 in v. Since v[2] = u[1] and v[1]v[2] ,u[1]u[2], the window profile of i in v w.r.t. u is ⊤⊥.
• Consider the string v = 01 and the position i = 2 in v. Since v[2] , u[1] and v[1]v[2] =u[1]u[2], the window profile of i in v w.r.t. u is ⊥⊤.
Note that ⊤⊤ < WPu , since for every string v and the position i in v, if v[i − 1]v[i] = u[1]u[2] = 01,
then v[i] = 1 , 0 = u[1].
We will construct a parsing automaton Au from u, which parses a string v containing at least
one occurrence of u (i.e. v ∈ Σ∗uΣ∗ ) into v 1uv 2u . . . vl uvl +1 such that v j u[1] . . . u[k − 1] < Σ∗uΣ∗for each 1 ≤ j ≤ l. This ensures that the only occurrence of u in each v j u is a suffix. Finally, we
also require vl +1 < Σ∗uΣ∗ . The window profiles w.r.t. u will be used to ensure that v is correctly
parsed, namely, the first, second, · · · , occurrences of u are correctly identified.
Definition 7.4 (Parsing automata). Given a string u we define the parsing automaton Au to be
the NFA (Qu , δu , q 0,u , Fu ) where q 0,u = q 0 and the remaining components are given below.


 



→
−
→
−
→
−
→
−
• Qu = q 0 ∪ search, W W ∈ WPu ∪ vfy, j, W
j ∈ [k − 1], W ∈ WPu , where q 0 is
a distinguished state whose purpose will become clear later on, and the tags “search" and“vfy" are used to denote whether Au is in the “search” mode to search for the next occurrenceof u, or in the “verify” mode to verify that the current position is a part of an occurrence of u.
• δu is defined as follows.



→
−
→
−
– The transition q 0 , a, search, W∈ δu , where W [1] = ⊤ iff a = u[1], and for each→−i : 2 ≤ i ≤ k − 1, W [i] = ⊥.

→
−
→
−
– The transition q 0 , u[1], vfy, 1, W ∈ δu , where W [1] = ⊤ and for each i : 2 ≤ i ≤ k − 1,→−
W [i] = ⊥.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:18

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu


→
−
→
−
– For each state search, W and a ∈ Σ such that W [k − 1] = ⊥ or a , u[k],−−→ 
−−→→−∗ the transition search, W , a, search, W ′ ∈ δu , where W ′[1] = ⊤ iff a = u[1], and−−→→−for each i : 2 ≤ i ≤ k − 1, W ′[i] = ⊤ iff (W [i − 1] = ⊤ and a = u[i]),
−−→
−−→
→
−
∗ if a = u[1], then the transition search, W , a, vfy, 1, W ′ ∈ δu , where W ′[1] = ⊤,−−→′→−and for each i : 2 ≤ i ≤ k − 1, W [i] = ⊤ iff (W [i − 1] = ⊤ and a = u[i]).
→−– For each state vfy, i − 1, W and a ∈ Σ such that∗ 2 ≤ i ≤ k − 1,→−
∗ W [i − 1] = ⊤, a = u[i], and→−∗ either W [k − 1] = ⊥ or a , u[k],−−→ −−→→−
we have vfy, i − 1, W , a, vfy, i, W ′ ∈ δu , where for each j : 2 ≤ j ≤ k − 1, W ′[j] = ⊤→−iff W [j − 1] = ⊤ and a = u[j].
→−→−– For each state vfy, k − 1, W and a ∈ Σ such that W [k − 1] = ⊤ and a = u[k], we have



→
−
vfy, k − 1, W , a, q 0 ∈ δu .
→−Note that the constraint W [k − 1] = ⊥ or a , u[k] is used to guarantee that each occurrenceof the state q 0 , except the first one, witnesses the first occurrence of u from the beginning→−or after its previous occurrence. In other words, the constraint W [k − 1] = ⊥ or a , u[k] isused to guarantee that after an occurrence of q 0 , if q 0 has not been reached again, then u isforbidden tooccur.




→
−
→
−
• Fu = q 0 ∪ search, W W ∈ WPu .
→−
Note that the states vfy, j, W are not final states, since, when in these states, the verificationof the current occurrence of u has not been complete yet.





→
−
→
−
→
−
→
−
search, W W ∈ WPu , and Q vfy,i = vfy, i, W W ∈ WPu for each i ∈ [k −S
1]. In addition, let Q vfy =Q vfy,i . Suppose v = v 1uv 2u · · · vl uvl +1 such that v j u[1] . . . u[k −1] <Let Q search =i ∈[k −1]Σ∗uΣ∗ for each 1 ≤ j ≤ l, in addition, vl +1 < Σ∗uΣ∗ . Then there exists a unique accepting run r of
Au on v such that the state sequence in r is of the form q 0 r 1 q 0 r 2 q 0 · · · rl q 0 rl +1 , where for eachj ∈ [l], r j ∈ L((Q search ) + ◦ Q vfy,1 ◦ · · · ◦ Q vfy,k−1 ), and rl +1 ∈ L((Q search ) ∗ ).
Example 7.5. Consider u = 010 in Example 7.3. The parsing automaton Au is illustrated in
Figure 5. Note that there are no 0-transitions out of (search, ⊥⊤), since this would imply an
occurrence of u = 010, which should be verified by the states from Q vfy , more precisely, by the state
sequence q 0 (vfy, 1, ⊤⊥)(vfy, 2, ⊥⊤)q 0 .
We are ready to present the construction of B A1,u,Tz . The NFA B A1,u,Tz is constructed by thefollowing three-step procedure.
(1) Construct the product automaton A1 × Au . Note that the initial state of A1 × Au is (q 0 , q 0 )and the set of final states of A1 × Au is F 1 × Fu .
(2) Remove from A1 × Au all the (incoming or outgoing) transitions associated with the statesfrom Q 1 × Q vfy .
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:19

0
0
0

0
q0

0

(search, >⊥)(verify, 1, >⊥)1(verify, 2, ⊥>)

1
0
0

1
(search, ⊥⊥)1(search, ⊥>)1

Fig. 5. The parsing automaton Au for u = 010(3) For each pair (q, q ′ ) ∈ Tz and each sequence of transitions in Au of the form





−−→   −−→−−→ 
−−−→p, u[1], vfy, 1, W1′ , vfy, 1, W1′ , u[2], vfy, 2, W2′ , · · · , vfy, k − 1, Wk′−1 , u[k], q 0 ,→−where p = q 0 or p = search, W , add the following transitions

 
 
−−→     −−→ 
−−→  (q, p), u[1], q, vfy, 1, W1′, q, vfy, 1, W1′ , u[2], q, vfy, 2, W2′,··· ,  −−−′→ −−−′→     −−−′→ , q, vfy, k − 1, Wk −1 , u[k], (q ′, q 0 ) .
q, vfy, k − 2, Wk −2 , u[k − 1], q, vfy, k − 1, Wk −1
Note that the number of aforementioned sequences of transitions in Au is at most |Q search | +1,
−−→
−−−→
→
−
since W1′, . . . , Wk′−1 are completely determined by W and u. Intuitively, when Au identifies
an occurrence of u, if the current state of A1 is q, then after reading the occurrence of u,
B A1,u,Tz jumps from q to some state q ′ such that (q, q ′ ) ∈ Tz .
Example 7.6. Consider C ≡ x = replaceAll(y, u, z) ∧ x ∈ e 1 ∧ y ∈ e 2 ∧ z ∈ e 3 , where u = 010,
and e 1 , e 2 , e 3 are as in Example 6.2 (cf. Figure 2). Let Tz = {(q 0 , q 0 ), (q 1 , q 2 )}. The NFA B A1,u,Tz isobtained from the product automaton A1 × Au (which we give in the appendix for reference)by first removing all the transitions associated with the states from Q 1 × Q vfy , then adding thetransitions according to Tz as aforementioned (see Figure 6, where thick edges indicate addedtransitions). It is routine to check that 01010101 is accepted by B A1,u,Tz and A2 . Moreover, 10 ∈L(A3 ) ∩ L(A1 (q 0 , q 0 )) ∩ L(A1 (q 1 , q 2 )). Let y be 01010101 and z be 10. Then x takes the value
replaceAll(01010101, 010, 10) = 101101, which is accepted by A1 . Therefore, C is satisfiable.
For the more general case that the SL[replaceAll] formula C contains more than one occurrence of
replaceAll(−, −, −) terms, similar to the single-letter case in Section 6, we can nondeterministicallyremove the edges in the dependency graph GC in a top-down manner and reduce the satisfiabilityof C to the satisfiability of a collection of regular constraints for source variables.
Complexity. When constructing G i+1 from G i , suppose the two edges from x to y and z respectively are currently removed, let the labels of the two edges be (l, u) and (r, u) respectively. Theneach element (T , P) of Ei (x ) may be transformed into an element (T ′, P ′ ) of Ei+1 (y) such that|T ′ | = O (|u||T |), meanwhile, it may also be transformed into an element (T ′′, P ′′ ) of Ei+1 (z)such that T ′′ has the same state space as T . In each step of the decision procedure, the state
space of the regular constraints may be multiplied by a factor |u |. The state space of these regularconstraints is at most exponential in the end, so that we can still solve the nonemptiness problemof the intersection of all these regular constraints in exponential space. In addition, if the l-length
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:20

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu
00(q0 , (verify, 2, ⊥>))

(q4 , (search, >⊥))

1

1

(q0 , (verify, 1, >⊥))
0
(q0 , q0 ) 0
0 1 1(q4 , (search, ⊥>))
000

(q0 , (search, ⊥⊥))
1

1

0

0

1

(q0 , (search, >⊥))
0

0

1

1

1
0

(q1 , (search, ⊥⊥))
0

(q3 , (search, >⊥))

1

1

(q0 , (search, ⊥>))

1

1

(q4 , (search, ⊥⊥))

(q1 , (search, ⊥>)) 1(q2 , (search, ⊥⊥))

001

(q1 , (verify, 1, >⊥))

1

(q1 , (verify, 2, ⊥>))

0

(q2 , (search, ⊥>))

1
(q2 , q0 )0

(q2 , (search, >⊥))

1

0

Fig. 6. The NFA B A1,u,Tz for u = 010 and Tz = {(q 0 , q 0 ), (q 1 , q 2 )}of GC is bounded by a constant c, then for each source variable, we get polynomially many regularconstraints, where each of them has a state space of polynomial size. Therefore, we can get apolynomial space algorithm. See Appendix D for a detailed analysis.
8

DECISION PROCEDURE FOR SL[replaceAll]: THE REGULAR-EXPRESSION CASE

We consider the case that the second parameter of the replaceAll function is a regular expression.
The decision procedure presented below is a generalisation of those in Section 6 and Section 7.
As in the previous sections, we will again start with the simple situation that C ≡ x =replaceAll(y, e 0 , z) ∧ x ∈ e 1 ∧ y ∈ e 2 ∧ z ∈ e 3 . For 0 ≤ i ≤ 3, let Ai = (Q i , δi , q 0,i , Fi ) be the
NFA corresponding to ei .
Let us first consider the special case L(e 0 ) = {ε}. Then according to the semantics, for each stringu = a 1 · · · an , replaceAll(u, e 0 , v) = va 1v · · · vanv. We can solve the satisfiability of C as follows:(1) Guess a set Tz ⊆ Q 1 × Q 1 .
(2) Construct B A1,ε,Tz from A1 and Tz as follows: For each (q, q ′ ) ∈ Tz , add to A1 a transition(q, ε, q ′ ). Then transform the resulting NFA into one without ε-transitions (which can bedone in polynomial time).
T(3) Decide the nonemptiness of L(A2 ) ∩ L(B A1,ε,Tz ) and L(A3 ) ∩L(A1 (q, q ′ )).
(q,q ′ ) ∈Tz

Next, let us assume that L(e 0 ) , {ε}. For simplicity of presentation, we assume ε < L(e 0 ). The
case that ε ∈ L(e 0 ) can be dealt with in a slightly more technical albeit similar way.
Since ε < L(e 0 ), we have q 0,0 < F 0 . In addition, without loss of generality, we assume that there
are no incoming transitions for q 0,0 in A0 .
To check the satisfiability of C, similar to the constant-string case, we construct a parsing
automaton Ae0 that parses a string v ∈ Σ∗e 0 Σ∗ into v 1u 1v 2u 2 . . . vl ul vl +1 such that• for each j ∈ [l], u j is the leftmost and longest matching of e 0 in (v 1u 1 . . . v j−1u j−1 ) −1v,
• vl +1 < Σ∗e 0 Σ∗ .
We will first give an intuitive description of the behaviour of the automaton Ae0 . We start with
an automaton that can have an infinite number of states and describe the automaton as starting newProceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:21“threads”, i.e., run multiple copies of A0 on the input word (similar to alternating automata). We
also show how this automaton can be implemented using only a finite number of states. Intuitively,in order to search for the leftmost and longest matching of e 0 , Ae0 behaves as follows.
• Ae0 has two modes, “left” and “long”, which intuitively means searching for the first and last
position of the leftmost and longest matching of e 0 respectively.
• When in the “left” mode, Ae0 starts a new thread of A0 in each position and records the setof states of the threads into a vector. In addition, it nondeterministically makes a “leftmost”
guessing, that is, guesses that the current position is the first position of the leftmost andlongest matching. If it makes such a guessing, it enters the “long” mode, runs the thread
started in the current position and searches for the last position of the leftmost and longest
matching. Moreover, it stores in a set S the union of the sets of states of all the threads thatwere started before the current position and continues running these threads to make surethat, in these threads, the final states will not be reached (thus, the current position is indeed
the first position of the leftmost and longest matching).
• When in the “long” mode, Ae0 runs a thread of A0 to search for the last position of theleftmost and longest matching. If the set of states of the thread contains a final state, thenAe0 nondeterministically guesses that the current position is the last position of the leftmost
and longest matching. If it makes such a guessing, then it resets the set of states of the thread
and starts a new round of searching for the leftmost and longest matching. In addition, it
stores the original set of states of the thread into a set S and continues running the thread tomake sure that in this thread, the final states will not be reached (thus, the current position
is indeed the last position of the leftmost and longest matching).
• Since the length of the vectors of the sets of states of the threads may become unbounded,in order to obtain a finite state automaton, the following trick is applied. Suppose that thevector is S 1S 2 · · · Sn . For each pair of indices i, j : i < j and each q ∈ Si ∩ S j , remove q from S j .
The application of this trick is justified by the following arguments: Since q occurs in both
Si and S j and the thread i was started before the thread j, even if from q a final state can bereached in the future, the position where the thread j was started cannot be the first positionof the leftmost and longest matching, since the state q is also a state of the thread i and theposition where the thread i was started is before the position where the thread i was started.
Before presenting the construction of Ae0 in detail, let us introduce some additional notation.
For S ⊆ Q 0 and a ∈ Σ, let δ 0 (S, a) denote {q ′ ∈ Q 0 | ∃q ∈ S. (q, a, q ′ ) ∈ δ 0 }. For a ∈ Σ and avector ρ = S 1 · · · Sn such that Si ⊆ Q 0 for each i ∈ [n], let δ 0 (ρ, a) = δ 0 (S 1 , a) · · · δ 0 (Sn , a).
For a vector S 1 · · · Sn such that Si ⊆ Q 0 for each i ∈ [n], we define red(S 1 · · · Sn ) inductively:• If n = 1, then red(S 1 ) = S 1 if S 1 , ∅, and red(S 1 ) = ε otherwise.
• If n > 1, thenSred(S 1 · · · Sn−1 )if Sn ⊆Si ,
i ∈[n−1]red(S 1 · · · Sn ) = SSi ) o/w
 red(S 1 · · · Sn−1 )(Sn \i ∈[n−1]For instance, red(∅{q}) = {q} andred({q 1 , q 2 }{q 1 , q 3 }{q 2 , q 4 }) = red({q 1 , q 2 }{q 1 , q 3 }){q 4 } = red({q 1 , q 2 }){q 3 }{q 4 } = {q 1 , q 2 }{q 3 }{q 4 }.
We give the formal description of Ae0 = (Q e0 , δ e0 , q 0,e0 , Fe0 ) below. The automaton will containstates of the form (ρ, m, S ) where ρ is the vector S 1 · · · Sn recording the set of states of the threadsof A0 . The second component m is either left or long indicating the mode. Finally S is the set ofstates representing all threads for which final states must not be reached.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:22

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu• Q e0 comprises– the tuples ({q 0,0 }, left, S ) such that S ⊆ Q 0 ,– the tuples (ρ{q 0,0 }, left, S ) such that ρ = S 1 · · · Sn with n ≥ 1 satisfying that for each i ∈ [n],Si ⊆ Q 0 \ {q 0,0 }, and for each pair of indices i, j : i < j, Si ∩ S j = ∅, moreover, S ⊆ Q 0 \ F 0 ,– the tuples (S 1 , long, S ) such that S 1 ⊆ Q 0 , S ⊆ Q 0 \ F 0 and S 1 ⊈ S;
• q 0,e0 = ({q 0,0 }, left, ∅),• Fe0 comprises the states of the form (−, left, −) ∈ Q e0 ,• δ e0 is defined as follows:– (continue left) suppose (ρ{q 0,0 }, left, S ) ∈ Q e0 such that ρ = S 1 · · · Sn with n ≥ 0 (n = 0
Smeans that ρ is empty), a ∈ Σ,
δ 0 (S j , a) ∪ δ 0 ({q 0,0 }, a) ∩ F 0 = ∅, and δ 0 (S, a) ∩ F 0 = ∅,j ∈[n]then(ρ{q 0,0 }, left, S ), a, red(δ 0 (ρ{q 0,0 }, a)){q 0,0 }, left, δ 0 (S, a) ∈ δ e0 ,
 SIntuitively, in a state (ρ, left, S ), ifδ 0 (S j , a)∪δ 0 ({q 0,0 }, a) ∩F 0 = ∅ and δ 0 (S, a)∩F 0 = ∅,j ∈[n]

then Ae0 can choose to stay in the “left” mode. Moreover, no states occur more thanonce in red(δ 0 (ρ{q 0,0 }, a)){q 0,0 }, since q 0,0 does not occur in red(δ 0 (ρ{q 0,0 }, a)), (from theassumption that there are no incoming transitions for q 0,0 in A0 ),– (start long) supposen ≥ 0, a ∈ Σ,
 S(ρ{q 0,0 }, left,
 S ) ∈ Q e0 such that ρ = S 1 · · · Sn withS
δ 0 (S, a) ∩ F 0 = ∅,
δ 0 (S j , a), thenδ 0 (S j , a) ∩ F 0 = ∅, and δ 0 ({q 0,0 }, a) ⊈ δ 0 (S, a) ∪j ∈[n]j ∈[n][*. (ρ{q }, left, S ), a, *.δ ({q }, a), long, δ (S, a) ∪
δ 0 (S j , a) +/+/ ∈ δ e0 .
0,0
0
0,0
0
j ∈[n],,-Intuitively,
from
a
state
(ρ{q
},
left,
S
)
with
ρ
=
S
·
·
·
S
,
when
reading a letter a, if
0,0
1
n
 S

S
δ 0 (S j , a) ∩ F 0 = ∅, δ 0 (S, a) ∩ F 0 = ∅, and δ 0 ({q 0,0 }, a) ⊈ δ 0 (S, a) ∪
δ 0 (S j , a),j ∈[n]j ∈[n]

then Ae0 guesses that the current position is the first position of the leftmost and longest
matching, it goes to the “long” mode, in addition, it keeps in the first component of thecontrol state only the set of states of the thread started in the current position, and puts
the union of the sets of the states of all the threads that have been started before, namely,Sδ 0 (S j , a), into the third component to guarantee that none of these threads will reachj ∈[n]

a final state in the future (thus the guessing that the current position is the first position of
the leftmost and longest matching is correct),– (continue long) suppose (S 1 , long, S ) ∈ Q e0 , δ 0 (S, a) ∩ F 0 = ∅, and δ 0 (S 1 , a) ⊈ δ 0 (S, a), then((S 1 , long, S ), a, (δ 0 (S 1 , a), long, δ 0 (S, a))) ∈ δ e0 ,intuitively, Ae0 guesses that the current position is not the last position of the leftmost andlongest matching and continues the “long” mode,– (end long) suppose (S 1 , long, S ) ∈ Q e0 , δ 0 (S 1 , a) ∩ F 0 , ∅, and δ 0 (S, a) ∩ F 0 = ∅, then((S 1 , long, S ), a, ({q 0,0 }, left, δ 0 (S, a) ∪ δ 0 (S 1 , a))) ∈ δ e0 ,intuitively, when δ 0 (S 1 , a) ∩ F 0 , ∅ and δ 0 (S, a) ∩ F 0 = ∅, Ae0 guesses that the current
position is the last position of the leftmost and longest matching, resets the first component
to {q 0,0 }, goes to the “left” mode, and puts δ 0 (S 1 , a) to the third component to guaranteethat the current thread will not reach a final state in the future (thus the guessing that thecurrent position is the last position of the leftmost and longest matching is correct).
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:23– (a matches e 0 ) suppose (ρ{q 0,0 }, left, S ) ∈ Q e0 such that ρ = S 1 · · · Sn with n ≥ 0, a ∈ Σ,S
δ 0 (S j , a) ∩ F 0 = ∅, δ 0 ({q 0,0 }, a) ∩ F 0 , ∅, and δ 0 (S, a) ∩ F 0 = ∅, thenj ∈[n][*. (ρ{q }, left, S ), a, *.{q }, left, δ (S, a) ∪
δ 0 (S j , a) ∪ δ 0 ({q 0,0 }, a) +/+/ ∈ δ e0 ,
0,0
0,0
0
j ∈[n],,-intuitively,
from
a
state
(ρ{q
},
left,
S
)
with
ρ
=
S
·
·
·
S
,
when
readinga letter a, if
0,0
1
n
 S

δ 0 (S j , a) ∩ F 0 = ∅, δ 0 ({q 0,0 }, a) ∩ F 0 , ∅, and δ 0 (S, a) ∩ F 0 = ∅, then Ae0 guesses thatj ∈[n]

a is simply the leftmost and longest matching of e 0 (e.g. when e 0 = a), then it directly goes tothe “left” mode (without going to the “long” mode), resets the first component of the control
state to {q 0,0 }, and puts the union of the sets of the states of all the threads that have beenS
started, including the one started in the current position, namely,δ 0 (S j , a)∪δ 0 ({q 0,0 }, a),j ∈[n]

into the third component to guarantee that none of these threads will reach a final state inSδ 0 (S j , a) is used to validate the leftmost guessing and δ 0 ({q 0,0 }, a) is
the future (wherej ∈[n]

used to validate the longest guessing).
Let Q left = {(−, left, −) ∈ Q e0 }, Q long = {(−, long, −) ∈ Q e0 }, and v = v 1u 1v 2u 2 · · · vl ul vl +1 suchthat u j is the leftmost and longest matching of e 0 in (v 1u 1 · · · v j−1u j−1 ) −1v for each j ∈ [l], in
addition, vl +1 < Σ∗eΣ∗ . Then there exists a unique accepting run r of Ae0 on v such that the state
sequence in r is of the form({q 0,0 }, left, ∅) r 1 ({q 0,0 }, left, −) r 2 ({q 0,0 }, left, −) · · · rl ({q 0,0 }, left, −) rl +1 ,where for each j ∈ [l], r j ∈ L((Q left ) ∗ ◦ (Q long ) ∗ ), and rl +1 ∈ L((Q left ) ∗ ). Intuitively, each occurrenceof the state subsequence from L((Q long ) ∗ ◦({q 0,0 }, left, −)), except the first one, witnesses the leftmost
and longest matching of e 0 in v from the beginning or after the previous such a matching.
Since in the first component ρq 0,0 of each state of Ae0 , no states from A0 occur more than once,
it is not hard to see that |Ae0 | is 2O (p ( | A0 |)) for some polynomial p.
Given Tz ⊆ Q 1 × Q 1 , we construct B A1,e0,Tz by the following three-step procedure.
(1) Construct the product of A1 and Ae0 .
(2) Remove all transitions associated with states from Q 1 ×Q long , in addition, remove all transitionsof the form ((q, (ρ{q 0,0 }, left, S )), a, (q ′, ({q 0,0 }, left, S ′ ))) such that δ 0 (q 0,0 , a) ∩ F 0 , ∅.
(3) For each pair (q, q ′ ) ∈ Tz , do the following,• for each transition[*. (ρ{q }, left, S ), a, *.δ ({q }, a), long, δ (S, a) ∪
δ 0 (S j , a) +/+/ ∈ δ e0 ,
0,0
0
0,0
0
j ∈[n],,-S
δ 0 (S j , a) +++ ,add a transition * q, (ρ{q 0,0 }, left, S ) , a, *q, *δ 0 ({q 0,0 }, a), long, δ 0 (S, a) ∪
j
∈[n]
,
, ,
--• for each transition((S 1 , long, S ), a, (δ 0 (S 1 , a), long, δ 0 (S, a))) ∈ δ e0 ,add a transition ((q, (S 1 , long, S )), a, (q, (δ 0 (S 1 , a), long, δ 0 (S, a)))) ,• for each transition((S 1 , long, S ), a, ({q 0,0 }, left, δ 0 (S, a) ∪ δ 0 (S 1 , a))) ∈ δ e0 ,add a transition ((q, (S 1 , long, S )), a, (q ′, ({q 0,0 }, left, δ 0 (S, a) ∪ δ 0 (S 1 , a)))),
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:24

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin WuSδ 0 (S j , a) ∪ δ 0 ({q 0,0 }, a) ++ ∈ δ e0 , add• for each * (ρ{q 0,0 }, left, S ), a, *{q 0,0 }, left, δ 0 (S, a) ∪
j
∈[n]
,
,
-a transition[*. (q, (ρ{q }, left, S )), a, *.q ′, *.{q }, left, δ (S, a) ∪
δ 0 (S j , a) ∪ δ 0 ({q 0,0 }, a) +/+/+/ .
0,0
0,0
0
j ∈[n],, ,---Since |Ae0 | is 2O (p ( | A0 |)) , it follows that |B A1,e0,Tz | is |A1 | · 2O (p ( | A0 |)) . In addition, since |A0 | =O (|e 0 |), we deduce that |B A1,e0,Tz | is |A1 | · 2O (p ( |e0 |)) .
For the more general case that the SL[replaceAll] formula C contains more than one occurrenceof replaceAll(−, −, −) terms, we still nondeterministically remove the edges in the dependency
graph GC in a top-down manner and reduce the satisfiability of C to the satisfiability of a collectionof regular constraints for source variables.
Complexity. In each step of the reduction, suppose the two edges out of x are currently removed,
let the two edges be from x to y and z and labeled by (l, e) and (r, e) respectively, then eachelement of (T , P) of Ei (x ) may be transformed into an element (T ′, P ′ ) of Ei+1 (y) such that|T ′ | = |T | · 2O (p ( |e |)) , meanwhile, it may also be transformed into an element (T ′′, P ′′ ) of Ei+1 (y)such that T ′′ has the same state space as T . Thus, after the reduction, for each source variable
x, E (x ) may contain exponentially many elements, and each of them may have a state spaceof exponential size. To solve the nonemptiness problem of the intersection of all these regularconstraints, the exponential space is sufficient. In addition, if the l-length of GC is at most one, we
can show that for each source variable x, E (x ) corresponds to the intersection of polynomiallymany regular constraints, where each of them has a state space at most exponential size. To solve
the nonemptiness of the intersection of these regular constraints, a polynomial space is sufficient.
See Appendix E for a detailed analysis.
9

UNDECIDABLE EXTENSIONSIn this section, we consider the language SL[replaceAll] extended with either integer constraints,character constraints, or IndexOf constraints, and show that each of such extensions leads toundecidability. We will use variables of, in additional to the type Str, the Integer data type Int. The
type Str consists of the string variables as in the previous sections. A variable of type Int, usuallyreferred to as an integer variable, ranges over the set N of natural numbers. Recall that, in previous
sections, we have used x, y, z, . . . to denote the variables of Str type. Hereafter we typically use
l, m, n, . . . to denote the variables of Int. The choice of omitting negative integers is for simplicity.
Our results can be easily extended to the case where Int includes negative integers.
We begin by defining the kinds of constraints we will use to extend SL[replaceAll]. First, we
describe integer constraints, which express constraints on the length or number of occurrences ofsymbols in words.
Definition 9.1 (Integer constraints). An atomic integer constraint over Σ is an expression of theform a 1t 1 + · · · + an tn ≤ d where a 1 , · · · , an , d ∈ Z are constant integers (represented in binary),and each term ti is either(1) an integer variable n;(2) |x | where x is a string variable; or(3) |x |a where x is string variable and a ∈ Σ is a constant letter.
Here, |x | and |x |a denote the length of x and the number of occurrences of a in x, respectively.
An integer constraint over Σ is a Boolean combination of atomic integer constraints over Σ.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:25

Character constraints, on the other hand, allow to compare symbols from different strings. The
formal definitions are given as follows.
Definition 9.2 (Character constraints). An atomic character constraint over Σ is an equation of theform x[t 1 ] = y[t 2 ] where• x and y are either a string variable or a constant string in Σ∗ , and• t 1 and t 2 are either integer variables or constant positive integers.
Here, the interpretation of x[t 1 ] is the t 1 -th letter of x. In case that x does not have the t 1 -th letteror y does not have the t 2 -th letter, the constraint x[t 1 ] = y[t 2 ] is false by convention.
A character constraint over Σ is a Boolean combination of atomic character constraints over Σ.
We also consider the constraints involving the IndexOf function.
Definition 9.3 (IndexOf Constraints). An atomic IndexOf constraint over Σ is a formula of theform t o IndexOf(s 1 , s 2 ), where• t is an integer variable, or a positive integer (recall that here we assume that the first positionof a string is 1), or the value 0 (denoting that there is no occurrence of s 1 in s 2 ),• o ∈ {≥, ≤}, and• s 1 , s 2 are either string variables or constant strings.
We consider the first-occurrence semantics of IndexOf. More specifically, t ≥ IndexOf(s 1 , s 2 ) holds
if t is no less than the first position in s 2 where s 1 occurs, similarly for t ≤ IndexOf(s 1 , s 2 ).
An IndexOf constraint over Σ is a Boolean combination of atomic IndexOf constraints over Σ.
We will show that the extension of SL[replaceAll] with integer constraints entails undecidability,
by a reduction from (a variant of) the Hilbert’s 10th problem, which is well-known to be undecidable[Matiyasevich 1993]. For space reasons, all proofs appear in Appendix G. Intuitively, we want to finda solution to f (x 1 , · · · , x n ) = д(x 1 , · · · , x n ) in the natural numbers, where f and д are polynomials
with positive coefficients. We can use the length of string variables over a unary alphabet {a} torepresent integer variables, addition can be performed with concatenation, and multiplication of x
and y with replaceAll(x, a, y). The integer constraint |x | = |y| asserts the equality of f and д. Notethat the use of concatenation can be further dispensed since, by Proposition 3.6, concatenation isexpressible by replaceAll at the price of a slightly extended alphabet.
Theorem 9.4. For the extension of SL[replaceAll] with integer constraints, the satisfiability problem
is undecidable, even if only a single integer constraint of the form |x | = |y| or |x |a = |y|a is used.
Notice that the extension of SL[replaceAll] with only one integer constraint of the form |x | = |y|entails undecidability. We remark that the undecidability result here does not follow from theundecidability result for the extension of word equations with the letter-counting modalities in[Büchi and Senger 1990], since the formula by [Büchi and Senger 1990] is not straight-line.
By utilising a further result on Diophantine equations, we show that for the extension ofSL[replaceAll] with integer constraints, even if the SL[replaceAll] formulae are simple (in the sensethat their dependency graphs are of depth at most one), the satisfiability problem is still undecidable(note that no restrictions are put on the integer constraints in this case).
Theorem 9.5. For the extension of SL[replaceAll] with integer constraints, even if SL[replaceAll]formulae are restricted to those whose dependency graphs are of depth at most one, the satisfiability
problem is still undecidable.
By essentially encoding |x | = |y| with character or IndexOf constraints, we show:
Proposition 9.6. For the extension of SL[replaceAll] with either the character constraints or theIndexOf constraints, the satisfiability problem is undecidable.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:26
10

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu
RELATED WORK

We now discuss some related work. We split our discussion into two categories: (1) theoreticalresults in terms of decidability and complexity; (2) practical (but generally incomplete) approaches
used in string solvers. We emphasise work on replaceAll functions as they are our focus.
Theoretical Results. We have discussed in Section 1 works on string constraints with the theory of
strings with concatenation. This research programme builds on the question of solving satisfiabilityof word equations, i.e., a string equation α = β containing concatenation of string constants andvariables. Makanin showed decidability [Makanin 1977], whose upper bound was improved to
PSPACE in [Plandowski 2004] using a word compression technique. A simpler algorithm was inrecent years proposed in [Jez 2017] using the recompression technique. The best lower bound for thisproblem is still NP, and closing this complexity gap is a long-standing open problem. Decidability(in fact, the PSPACE upper bound) can be retained in the presence of regular constraints (e.g. see[Schulz 1990]). This can be extended to existential theory of concatenation with regular constraints
using the technique of [Büchi and Senger 1990]. The replace-all operator cannot be expressed by
the concatenation operator alone. For this reason, our decidability of the fragment of SL[replaceAll]cannot be derived from the results from the theory of concatenation alone.
Regarding the extension with length constraints, it is still a long-standing open problem whether
word equations with length constraints is decidable, though it is known that letter-counting (e.g.
counting the number of occurrences of 0s and 1s separately) yields undecidability [Büchi and Senger1990]. It was shown in [Lin and Barceló 2016] that the length constraints (in fact, letter-counting)can be added to the subclass of SL[replaceAll] where the pattern/replacement are constants, while
preserving decidability. In contrast, if we allow variables on the replacement parameters of formulas
in SL[replaceAll], we can easily encode the Hilbert’s 10th problem with length (integer) constraints.
The replaceAll function can be seen as a special, yet expressive, string transformation function,
aka string transducer. From this viewpoint, the closest work is [Lin and Barceló 2016], which we
discuss extensively in the introduction. Here, we discuss two further recent transducer models:streaming string transducers [Alur and Cerný 2010] and symbolic transducers [Veanes et al. 2012].
A streaming string transducer is a finite state machine where a finite set of string variables areused to store the intermediate results for output. The replaceAll(x, e, y) term can be modelled by
an extension of streaming string transducers with parameters, that is, a streaming string transducer
which reads an input string (interpreted as the value of x), uses y as a free string variable which ispresumed to be read-only, and updates a string variable z, which stores the computation result, by
a string term which may involve y. Nevertheless, to the best of our knowledge, this extension of
streaming string transducers has not been investigated so far.
Symbolic transducers are an extension of Mealy machine to infinite alphabets by using a variable cur to represent the symbol in the current position, and replacing the input and output
letters in transitions with unary predicates φ(cur ) and terms involving cur respectively. Symbolictransducers can model replaceAll functions when the third parameter is a constant. Inspired bysymbolic transducers, it is perhaps an interesting future work to consider an extension of thereplaceAll function by allowing predicates as patterns. For instance, one may consider the term
replaceAll(x, cur ≡ 0 mod 2, y) which replaces every even number in x with y.
Finally, the replaceAll function is related to Array Folds Logic introduced by Daca et al [Dacaet al. 2016]. The authors considered an extension of the quantifier-free theory of integer arrayswith counting. The main feature of the logic is the fold terms, borrowed from the folding concept infunctional programming languages. Intuitively, a fold term applies a function to every element of
the array to compute an output. If strings are treated as arrays over a finite domain (the alphabet),
the replaceAll function can be seen as a fold term. Nevertheless, the replaceAll function goes beyond
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:27

the fold terms considered in [Daca et al. 2016], since it outputs a string (an array), instead of an
integer. Therefore, the results in [Daca et al. 2016] cannot be applied to our setting.
Practical Solvers. A large amount of recent work develops practical string solvers including
Kaluza [Saxena et al. 2010], Hampi [Kiezun et al. 2012], Z3-str [Zheng et al. 2013], CVC4 [Lianget al. 2014], Stranger [Yu et al. 2014], Norn [Abdulla et al. 2014], S3 and S3P [Trinh et al. 2014, 2016],
and FAT [Abdulla et al. 2017]. Among them, only Stranger, S3, and S3P support replaceAll.
In the Stranger tool, an automata-based approach was provided for symbolic analysis of PHP
programs, where two different semantics replaceAll were considered, namely, the leftmost andlongest matching as well as the leftmost and shortest matching. Nevertheless, they focused on
the abstract-interpretation based analysis of PHP programs and provided an over-approximationof all the possible values of the string variables at each program point. Therefore, their string
constraint solving algorithm is not an exact decision procedure. In contrast, we provided a decision
procedure for the straight-line fragment with the rather general replaceAll function, where thepattern parameter can be arbitrary regular expressions and the replacement parameter can bevariables. In the latter case, we consider the leftmost and longest semantics mainly for simplicity,and the decision procedure can be adapted to the leftmost and shortest semantics easily.
The S3 and S3P tools also support the replaceAll function, where some progressive searchingstrategies were provided to deal with the non-termination problem caused by the recursively defined
string operations (of which replaceAll is a special case). Nevertheless, the solvers are incomplete asreasoning about unbounded strings defined recursively is in general an undecidable problem.
11

CONCLUSION

We have initiated a systematic investigation of the decidability of the satisfiability problem forthe straight-line fragments of string constraints involving the replaceAll function and regularconstraints. The straight-line restriction is known to be appropriate for applications in symbolic
execution of string-manipulating programs [Lin and Barceló 2016]. Our main result is a decision
procedure for a large fragment of the logic, wherein the pattern parameters are regular expressions(which covers a large proportion of the usage of the replaceAll function in practice). Concatenation
is obtained for free since concatenation can be easily expressed in this fragment. We have shownthat the decidability of this fragment cannot be substantially extended. This is achieved by showingthat if either (1) the pattern parameters are allowed to be variables, or (2) the length constraints
are incorporated in the fragment, then we get the undecidability. Our work clarified importantfundamental issues surrounding the replaceAll functions in string constraint solving and provided
a novel decision procedure which paved a way to a string solver that is able to fully support the
replaceAll function. This would be the most immediate future work.
ACKNOWLEDGMENTS
T. Chen is supported by the Australian Research Council under Grant No. DP160101652 and the Engineering and Physical Sciences Research Council under Grant No. EP/P00430X/1. M. Hague is supported by the Engineering and Physical Sciences Research Council under Grant No. EP/K009907/1.
A. Lin is supported by the European Research Council (ERC) under the European Union’s Horizon
2020 research and innovation programme (grant agreement no 759969). Z. Wu is supported by the
National Natural Science Foundation of China under Grant No. 61472474 and Grant No. 61572478,
the INRIA-CAS joint research project “Verification, Interaction, and Proofs”,

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:28

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

REFERENCES
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, and Philipp Rümmer.
2017. Flatten and conquer: a framework for efficient analysis of string constraints. In Proceedings of the 38th ACM
SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017.
602–617. https://doi.org/10.1145/3062341.3062384
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman.
2014. String Constraints for Verification. In CAV. 150–166.
Rajeev Alur and Pavol Cerný. 2010. Expressiveness of streaming string transducers. In IARCS Annual Conference onFoundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India.
1–12.
Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press.
Davide Balzarotti, Marco Cova, Viktoria Felmetsger, Nenad Jovanovic, Engin Kirda, Christopher Kruegel, and Giovanni Vigna.
2008. Saner: Composing Static and Dynamic Analysis to Validate Sanitization in Web Applications. In 2008 IEEE Symposium
on Security and Privacy (S&P 2008), 18-21 May 2008, Oakland, California, USA. 387–401. https://doi.org/10.1109/SP.2008.22
Nikolaj Bjørner, Nikolai Tillmann, and Andrei Voronkov. 2009. Path feasibility analysis for string-manipulating programs.
In TACAS. 307–321.
J Richard Büchi and Steven Senger. 1990. Definability in the existential theory of concatenation and undecidable extensionsof this theory. In The Collected Works of J. Richard Büchi. Springer, 671–683.
Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. 2006. EXE: Automatically Generating
Inputs of Death. In Proceedings of the 13th ACM Conference on Computer and Communications Security (CCS ’06). ACM,
New York, NY, USA, 322–335. https://doi.org/10.1145/1180405.1180445
Przemyslaw Daca, Thomas A. Henzinger, and Andrey Kupriyanov. 2016. Array Folds Logic. In Computer Aided Verification 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II. 230–248.
Loris D’Antoni and Margus Veanes. 2013. Static Analysis of String Encoders and Decoders. In VMCAI. 209–228.
Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, and Martin C. Rinard. 2012. Word Equations with Length Constraints:
What’s Decidable?. In Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC
2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers. 209–226. https://doi.org/10.1007/978-3-642-39611-3_21
Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed Automated Random Testing. SIGPLAN Not. 40, 6(June 2005), 213–223. https://doi.org/10.1145/1064978.1065036
Google. 2015. Closure Templates. https://developers.google.com/closure/templates/. Referred July 2017.
Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes. 2011. Fast and Precise Sanitizer
Analysis with BEK. In USENIX Security Symposium.
John E. Hopcroft and Jeffrey D. Ullman. 1979. Introduction to Automata Theory, Languages and Computation. Addison-Wesley.
Artur Jez. 2017. Word equations in linear space. CoRR abs/1702.00736 (2017). http://arxiv.org/abs/1702.00736
Christoph Kern. 2014. Securing the tangled web. Commun. ACM 57, 9 (2014), 38–47. https://doi.org/10.1145/2643134
Adam Kiezun et al. 2012. HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars.
ACM Trans. Softw. Eng. Methodol. 21, 4 (2012), 25.
James C. King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19, 7 (1976), 385–394. https://doi.org/10.
1145/360248.360252
Jan Lehnardt and contributors. 2015. mustache.js. https://github.com/janl/mustache.js/. Referred July 2017.
Tianyi Liang, Andrew Reynolds, Cesare Tinelli, Clark Barrett, and Morgan Deters. 2014. A DPLL(T) Theory Solver for a
Theory of Strings and Regular Expressions. In CAV. 646–662.
Anthony W. Lin and Pablo Barceló. 2016. String Solving with Word Equations and Transducers: Towards a Logic for Analysing
Mutation XSS. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL ’16). Springer, 123–136.
Gennady S Makanin. 1977. The problem of solvability of equations in a free semigroup. Sbornik: Mathematics 32, 2 (1977),
129–198.
Yuri V. Matiyasevich. 1993. Hilbert’s Tenth Problem. MIT Press, Cambridge, MA, USA.
K. L. McMillan. 1993. Symbolic model checking. Kluwer.
Wojciech Plandowski. 2004. Satisfiability of word equations with constants is in PSPACE. J. ACM 51, 3 (2004), 483–496.
https://doi.org/10.1145/990308.990312
Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. 2010. A Symbolic Execution
Framework for JavaScript. In 31st IEEE Symposium on Security and Privacy, S&P 2010, 16-19 May 2010, Berleley/Oakland,
California, USA. 513–528. https://doi.org/10.1109/SP.2010.38
Klaus U. Schulz. 1990. Makanin’s Algorithm for Word Equations - Two Improvements and a Generalization. In Word
Equations and Related Topics, First International Workshop, IWWERT ’90, Tübingen, Germany, October 1-3, 1990, Proceedings.
85–150. https://doi.org/10.1007/3-540-55124-7_4

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:29

Koushik Sen, Swaroop Kalasapur, Tasneem G. Brutch, and Simon Gibbs. 2013. Jalangi: a selective record-replay and dynamic
analysis framework for JavaScript. In Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT
Symposium on the Foundations of Software Engineering, ESEC/FSE’13, Saint Petersburg, Russian Federation, August 18-26,
2013. 488–498. https://doi.org/10.1145/2491411.2491447
Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. 2014. S3: A Symbolic String Solver for Vulnerability Detection in Web
Applications. In CCS. 1232–1243.
Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. 2016. Progressive Reasoning over Recursively-Defined Strings. In
Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings,
Part I. Springer, 218–240.
Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjørner. 2012. Symbolic finite statetransducers: algorithms and applications. In POPL. 137–150.
Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, and Jie-Hong R. Jiang. 2016. String Analysis via Automata
Manipulation with Logic Circuit Representation. In Computer Aided Verification - 28th International Conference, CAV
2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I (Lecture Notes in Computer Science), Vol. 9779. Springer,
241–260. https://doi.org/10.1007/978-3-319-41528-4
Chris Wanstrath. 2009. Mustache: Logic-less Templates. https://mustache.github.io/. Referred July 2017.
Jeff Williams, Jim Manico, and Neil Mattatall. 2017. XSS Prevention Cheat Sheet. https://www.owasp.org/index.php/XSS_(Cross_Site_Scripting)_Prevention_Cheat_Sheet. Referred July 2017.
Fang Yu, Muath Alkhalaf, Tevfik Bultan, and Oscar H. Ibarra. 2014. Automata-based Symbolic String Analysis for Vulnerability
Detection. Form. Methods Syst. Des. 44, 1 (2014), 44–70.
Yunhui Zheng, Xiangyu Zhang, and Vijay Ganesh. 2013. Z3-str: a Z3-based string solver for web application analysis. In
ESEC/SIGSOFT FSE. 114–124.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:30

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

Appendix“What Is Decidable about String Constraints with the ReplaceAll Function”
We provide below proofs and examples that were omitted from the main text due to spaceconstraints.
A

PROOF OF PROPOSITION 4.1

We recall Proposition 4.1 and then give its proof.
Proposition 4.1 The satisfiability problem of SL[replaceAll] is undecidable, if the second parametersof the replaceAll terms are allowed to be variables.
Proof. We reduce from the Post Correspondence Problem (PCP). Recall that the input of the
problem consists of two finite lists α 1 , . . . , α N and β 1 , . . . , β N of nonempty strings over Σ. A solution
to this problem is a sequence of indices (i k )1≤k ≤K with K ≥ 1 and 1 ≤ i k ≤ N for all k, such that
α i 1 . . . α i K = βi 1 . . . βi K . The PCP problem is to decide whether such a solution exists or not.
Without loss of generality, suppose Σ ∩ [N ] = ∅ and $ < Σ ∪ [N ]. Let Σ ′ = Σ ∪ [N ] ∪ {$}. We
will construct an SL[replaceAll] formula C over Σ ′ such that the PCP instance has a solution iff C
is satisfiable. To this end, the formula C utilises the capability that the second parameter of thereplaceAll terms may be variables.
Let x 1 , · · · , x N , y1 , · · · , y N , z be mutually distinct string variables. Then the formula C = φ ∧ ψ ,
where
V
φ =
(x i = replaceAll(x i−1 , i, α i ) ∧ yi = replaceAll(yi−1 , i, βi )) ∧ z = replaceAll(x N , y N , $),ψi ∈[N ]

= x 0 ∈ (1 + · · · + N ) + ∧ z ∈ $.

It is not hard to see that φ is a straight-line relational constraint, thus C is an SL[replaceAll]formula. Note that in replaceAll(x N , y N , $), the second parameter is a variable. We show that C issatisfiable iff the PCP instance has a solution: C is satisfiable iff there is a string i 1 · · · i K ∈ L((1+· · ·+N ) + ) such that when x 0 is assigned with i 1 · · · i K , the value of z is $. Since z = replaceAll(x N , y N , $)and x N , y N ∈ Σ+ , we know that z is $ iff the values of x N and y N are the same. Therefore, C issatisfiable iff there is a string i 1 · · · i K ∈ L((1 + · · · + N ) + ) such that when x 0 is assigned with
i 1 · · · i K , the values of x N and y N are the same. Therefore, C is satisfiable iff there is a sequence ofindices i 1 · · · i K such that α i 1 · · · α i K = βi 1 · · · βi K , that is, the PCP instance has a solution.
□B

SECTION 6: THE CORRECTNESS OF THE DECISION PROCEDURE

We argue that the procedure in Section 6.2 is correct. Note that Proposition 6.1 removed a single
replaceAll(−, −, −) to obtain only regular constraints. Each step of our decision procedure effectively
eliminates a replaceAll(−, −, −). Similar to Proposition 6.1, each step maintains the satisfiability
from the preceding step.
In more detail, from each G i we can define a constraint Ci . This constraint is a conjunction of
the following atomic constraints.
• For each variable x such that (x, (l, a), y) and (x, (r, a), z) are the edges in G i , we assert in Ci
that x = replaceAll(y, a, z).
• In addition, for each variable x such that Ei (x ) is not empty, moreover, either x is a source
variable in GC (not G i ) or there are (incoming or outgoing) edges connected to x in G i , let ei (x )be the regular expression equivalent to the conjunction of all constraints in Ei (x ) (Note thatthe conjunction of multiple regular expressions still defines a regular language). We assert
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:31

in Ci that x ∈ ei (x ). Note that if x is not a source variable in GC and there are no edges
connected to x in G i , then the regular constraints in Ei (x ) are not included into Ci .
It is immediate that C 0 is equivalent to C. We require the following proposition, which gives us
the correctness of the decision procedure by induction. Note that the final Ci when exiting the loop
will be a conjunction of regular constraints on the source variables.
Proposition B.1. For each i, let the l-edge and the r-edge from x to y and z respectively be the twoedges removed from G i to construct G i+1 . Then Ci is satisfiable iff there are sets T j,z such that Ci+1 issatisfiable.
We can see the above proposition by observing that, in each step, Ci is of the form
x = replaceAll(y, a, z) ∧ x ∈ ei (x ) ∧ y ∈ ei (y) ∧ z ∈ ei (z) ∧ C ′where C ′ does not contain x, and Ci+1 is of the formy ∈ ei+1 (y) ∧ z ∈ ei+1 (z) ∧ C ′ .
Note that C ′ remains unchanged since only the two edges leaving x are removed from G i andEi+1 (x ′ ) = Ei (x ′ ) for all x ′ distinct from x, y, and z. First assume y , z. Supposing Ci is satisfiable,
an argument similar to that of Proposition 6.1 shows that there are sets T j,z such that the same valuesof y and z also satisfy ei+1 (y) and ei+1 (z). Since C ′ is unchanged, all x ′ distinct from x, y, and z canalso keep the same value. Thus, Ci+1 is also satisfiable. In the other direction, suppose that there aresets T j,z such that Ci+1 is satisfiable. Take a satisfying assignment to Ci+1 . From the assignment to y
and z we obtain as in Proposition 6.1 an assignment to x that satisfies replaceAll(y, a, z) ∧ x ∈ ei (x ).
Furthermore, the assignments for y and z also satisfy ei (y) and ei (z) since Ei (y) and Ei (z) aresubsets of Ei+1 (y) and Ei+1 (z). Finally, since C ′ is unchanged, the assignments to all other variables
also transfer, giving us a satisfying assignment to Ci as required. In the case where y = z, thearguments proceed analogously to the case y , z.
C

THE PRODUCT AUTOMATON A1 × Au FOR u = 010

In Figure 7 we give the product automaton A1 × Au for u = 010. This is a straightforward productconstruction, but may be useful for reference when understanding Figure 6 which shows theautomaton B A1,u,Tz which is derived from the product.
D

COMPLEXITY ANALYSIS IN SECTION 7

We provide a more detailed analysis of the complexity of the algorithm for the constant string case,described in Section 7. A summary of this argument already appears in Section 7.
When constructing G i+1 from G i , suppose the two edges from x to y and z respectively are
currently removed, let the labels of the two edges be (l, u) and (r, u) respectively, then each element(T , P) of Ei (x ) may be transformed into an element (T ′, P ′ ) of Ei+1 (y) such that |T ′ | = O (|u ||T |),meanwhile, it may also be transformed into an element (T ′′, P ′′ ) of Ei+1 (z) such that T ′′ has thesame state space as T . Thus, for each source variable x, E (x ) contains at most exponentially many
elements, and each of them may have a state space of at most exponential size. For instance, for apath from x ′ to x where the constant strings u 1 , · · · , un occur in the labels of edges, an element(T , P) ∈ E0 (x ′ ) may induce an element (T ′, P ′ ) of E (x ) such that |T ′ | ≤ |T ||u 1 | · · · |un |, whichis exponential in the worst case. To solve the nonemptiness problem of the intersection of all theseregular constraints, the exponential space is sufficient. Consequently, in this case, we still obtain an
EXPSPACE upper-bound.
Let us now consider the special situation that the l-length of GC is bounded by a constant c. Since
Idxdmd (GC ) ≤ Lenlft (GC ), we know that Idxdmd (GC ) is also bounded by c. Therefore, according toProceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:32

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu
0(q0 , (verify, 2, ⊥>))

(q3 , q0 )(q1 , (verify, 2, ⊥>))

0
0

1
0
0
(q0 , q0 )1

(q4 , (search, >⊥))

(q3 , (verify, 1, >⊥))

0

1

0

1

(q0 , (verify, 1, >⊥))

0

0

0

(q0 , (search, ⊥⊥))
1

0

0

1

0

(q1 , (search, ⊥⊥))
1

1

0

(q0 , (search, >⊥))
0

1
1

0
(q3 , (search, >⊥))
0{q4 } × Au

(q0 , (search, ⊥>))
1
(q , (search, ⊥>)) 1
1(q4 , (verify, 1, >⊥))

{q2 } × Au
(q2 , (search, ⊥⊥))

Fig. 7. The NFA A1 × Au for u = 010

Proposition 4.5, there are at most polynomially different paths in GC , we deduce that for each source
variable x, E (x ) contains at most polynomially many elements. In addition, since the number ofl-edges in each path is bounded by c, during the execution of the decision procedure, the numberof times when (T , P) of Ei (x ) may be transformed into an element (T ′, P ′ ) of Ei+1 (y) such that|T ′ | = O (|u ||T |) is bounded by c. Therefore, for each source variable x and each element (T ′′, P ′′ )in E (x ), |T ′′ | is at most polynomial in the size of C. We then conclude that for each source variable
x, E (x ) corresponds to the intersection of polynomially many regular constraints such that each ofthem has a state space of polynomial size. Therefore, the nonemptiness of the intersection of all
the regular constraints in E (x ) can be solved in polynomial space. In this situation, we obtain a
PSPACE upper-bound.
E

COMPLEXITY ANALYSIS IN SECTION 8

We provide a more detailed analysis of the complexity of the algorithm for the regular-expression
case, described in Section 8. A summary of this argument already appears in Section 8.
In each step of the reduction, suppose the two edges out of x are currently removed, let the twoedges be from x to y and z and labeled by (l, e) and (r, e) respectively, then each element of (T , P)of Ei (x ) may be transformed into an element (T ′, P ′ ) of Ei+1 (y) such that |T ′ | = |T | · 2O (p ( |e |)) ,meanwhile, it may also be transformed into an element (T ′′, P ′′ ) of Ei+1 (y) such that T ′′ has thesame state space as T . Thus, after the reduction, for each source variable x, E (x ) may containexponentially many elements, and each of them may have a state space of exponential size, more
precisely, if we start from a vertex x without predecessors, with an element (T , P) in E0 (x ), and go
to a source variable y through a path where k edges have been traversed and removed, let e 1 , · · · , ek
be the regular expressions occurring in the labels of these edges, then the resulting element in E (y)has a state space of size |T | · 2O (p ( |e1 |)) · 2O (p ( |e2 |)) · · · · · 2O (p ( |ek |)) in the worst case. To solve thenonemptiness problem of the intersection of all these regular constraints, the exponential spaceis sufficient. Consequently, for the most general case of regular expressions, we still obtain an
EXPSPACE upper-bound.
On the other hand, for the situation that the l-length of GC is at most one, we wan to show that thealgorithm runs in polynomial space. Suppose the l-length of GC is at most one. Then the diamondindex of GC is at most one as well. According to Proposition 4.5, there are only polynomially many
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function

3:33

paths in GC . Nevertheless, for each source variable x, E (x ) may contain an element (T , P) suchthat |T | is exponential. Since |P | may be exponential, (T , P) may correspond to the intersection of
exponentially many regular constraints. However, we can show that |P | is at most polynomial, as aresult of the fact that the l-length of GC is at most one. The arguments proceed as follows: Suppose
two edges from x to y, z respectively are removed, and an element (T ′, P ′ ) of Ei+1 (y) such that|T ′ | is exponential and |P ′ | is polynomial, is generated from an element of (T , P) of Ei (x ). Theny must be a source variable in GC . Otherwise, there is an l-edge out of y and the l-length of GC is
at least two, a contradiction. Therefore, y is a source variable in GC , (T ′, P ′ ) will not be used togenerate the regular constraints for the other variables. In other words, y is a source variable in
GC , and (T ′, P ′ ) ∈ E (y) with |P ′ | polynomial. We then conclude that for each source variable x,|E (x )| is at most polynomial in the size of C and for each element (T , P) ∈ E (x ), |P | is polynomialin the size of C. Therefore, for each source variable x, E (x ) corresponds to the intersection ofpolynomially many regular constraints, where each of them has a state space at most exponential
size. To solve the nonemptiness of the intersection of these regular constraints, the polynomial
space is sufficient. We obtain a PSPACE upper-bound for the situation that the l-length of GC is at
most one.
F

EXAMPLES IN SECTION 8

Due to space constraints, we did not provide examples of the decision procedure for the regularexpression case. We provide some examples here.
Example F.1. Let e 0 = 0∗ 01(1∗ + 0∗ ). Then A0 and Ae0 are illustrated in Figure 8, where sleft andslong are the abbreviations of left and long respectively. Letus use the state ({q 0,1 }{q 0,0 }, sleft, ∅) toillustrate the construction. Since δ 0 ({q 0,1 }, 0) ∪δ 0 ({q 0,0 }, 0) ∩ F 0 = {q 0,1 } ∩ F 0 = ∅, δ 0 (∅, 0) ∩ F 0 = ∅,and red(δ 0 ({q 0,1 }, 0)δ 0 ({q 0,0 }, 0)) = {q 0,1 }, we deduce that the transition(({q 0,1 }{q 0,0 }, sleft, ∅), 0, ({q 0,1 }{q 0,0 }, sleft, ∅)) ∈ δ e0 .
On the other hand, it is impossible to go from the state ({q 0,1 }{q 0,0 }, sleft, ∅) to the “long” mode.
This is due to the fact that δ 0 ({q 0,0 }, 0) = {q 0,1 } ⊆ δ 0 ({q 0,1 }, 0) = {q 0,1 }. In addition, there are no 1transitions out of ({q 0,1 }{q 0,0 }, sleft, ∅). This is due to the fact that δ 0 ({q 0,1 }, 1)∩F 0 = {q 0,2 , q 0,3 }∩F 0 ,
∅.

q0,0

A0
0

Ae0

0
q0,1
1

1
({q0,0 }, sleft, ∅)

1

q0,2

q0,3

0

1

0
({q0,1 }{q0,0 }, sleft, ∅)

0 ({q

0

0

0

1
({q0,0 }, sleft, {q0,2 })000,2 }, slong, ∅)0({q0,1 }, slong, ∅)1({q0,0 }, sleft, {q0,3 })1
1
0({q0,0 }, sleft, {q0,2 , q0,3 })({q0,2 , q0,3 }, slong, ∅)
0

1
1

1

({q0,3 }, slong, ∅)Fig. 8. The NFA A0 and Ae0 for e 0 = 0∗ 01(1∗ + 0∗ )Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:34

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

Example F.2. Let C ≡ x = replaceAll(y, e 0 , z) ∧ x ∈ e 1 ∧ y ∈ e 2 ∧ z ∈ e 3 , where e 1 , e 2 , e 3 are as in
Example 6.2 (cf. Figure 2) and e 0 is as in Example F.1 (cf. Figure 8). Suppose Tz = {(q 0 , q 0 ), (q 1 , q 2 )}.
Then the NFA B A1,e0,Tz is as illustrated in Figure 9, where the thick edges denote the addedtransitions. Let us use the state (q 1 , ({q 0,0 }, left, ∅)) to exemplify the construction. The transition ((q 1 , ({q 0,0 }, left, ∅)), 1, (q 2 , ({q 0,0 }, left, ∅))) is in A1 × Ae0 . Since δ 0 (q 0,0 , 1) ∩ F 0 = ∅, thistransition is not removed and is thus in B A1,e0,Tz . On the other hand, since there are no 0transitions out of q 1 in A1 , there are no 0-transitions from (q 1 , ({q 0,0 }, left, ∅)) to some state fromQ left in B A1,e0,Tz . Moreover, because (({q 0,0 }, left, ∅), 0, ({q 0,1 }, long, ∅)) ∈ δ e0 and (q 1 , q 2 ) ∈ Tz ,the transition ((q 1 , ({q 0,0 }, left, ∅)), 0, (q 1 , ({q 0,1 }, long, ∅))) is added. One may also note that there
are no 0-transitions from (q 2 , ({q 0,0 }, left, ∅)) to the state (q 2 , ({q 0,1 }, long, ∅)), because there areno pairs (q2, −) ∈ Tz . It is not hard to see that 010101 ∈ L(A2 ) ∩ L(B A1,e0,Tz ). In addition,
10 ∈ L(A3 ) ∩ L(A1 (q 0 , q 0 )) ∩ L(A1 (q 1 , q 2 )). Let y be 010101 and z be 10. Then x takes the value
replaceAll(010101, e 0 , 10) = 10 · replaceAll(101, e 0 , 10) = 10110, which is accepted by A1 . Therefore,
C is satisfiable.
0(q3 , ({q0,1 }{q0,0 }, sleft, ∅))11(q1 , ({q0,0 }, sleft, ∅))1(q4 , ({q0,1 }{q0,0 }, sleft, ∅))00(q0 , ({q0,0 }, sleft, ∅))

0

0

0

0

0

(q0 , ({q0,1 }{q0,0 }, sleft, ∅))1(q0 , ({q0,0 }, sleft, {q0,2 }))0(q0 , ({q0,2 }, slong, ∅))

0

0

0

0

1

0

(q0 , ({q0,1 }, slong, ∅))(q0 , ({q0,0 }, sleft, {q0,3 }))

1

1

1

1

0
q0 , ({q0,0 }, sleft, {q0,2 , q0,3 }))(q0 , ({q0,2 , q0,3 }, slong, ∅))11(q0 , ({q0,3 }, slong, ∅))001(q2 , ({q0,0 }, sleft, ∅))00(q2 , ({q0,1 }{q0,0 }, sleft, ∅))001(q2 , ({q0,0 }, sleft, {q0,2 }))(q2 , ({q0,0 }, sleft, {q0,3 }))0(q1 , ({q0,2 }, slong, ∅))(q1 , ({q0,1 }, slong, ∅))1

1
0q2 , ({q0,0 }, sleft, {q0,2 , q0,3 }))01(q1 , ({q0,2 , q0,3 }, slong, ∅))1
1

1(q1 , ({q0,3 }, slong, ∅))Fig. 9. The NFA B A1,e0,Tz

G

UNDECIDABILITY PROOFS FOR SECTION 9

We provide the proofs of the theorems and propositions in Section 9 which show the undecidabilityof various extensions of our string constraints.
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

What Is Decidable about String Constraints with the ReplaceAll Function
G.1

3:35

Proof of Theorem 9.4

We begin with the first Theorem, which is recalled below.
Proposition 9.4 For the extension of SL[replaceAll] with integer constraints, the satisfiability problem
is undecidable, even if only a single integer constraint |x | = |y| is used.
Proof. The basic idea of the reduction is to simulate the two polynomials f (x 1 , · · · , x n ) andд(x 1 , · · · , x n ), where x 1 , · · · , x n range over the set of natural numbers, with two SL[◦, replaceAll]formulae C f , Cд over a unary alphabet {a}, with the output string variables yf , yд respectively, andsimulate the equality f (x 1 , · · · , x n ) = д(x 1 , · · · , x n ) with the integer constraint |yf | = |yд | (whichis equivalent to yf = yд , since yf , yд represent strings over the unary alphabet {a}).
A polynomial f (x 1 , · · · , x n ) or д(x 1 , · · · , x n ) where x 1 , · · · , x n range over the set of natural
numbers, can be simulated by an SL[◦, replaceAll] formula over an unary alphabet {a} as follows:
The natural numbers are represented by the strings over the alphabet {a}. A string variable isintroduced for each subexpression of f (x 1 , · · · , x n ). The numerical addition operator + is simulatedby the string operation ◦ and the multiplication operator ∗ is simulated by replaceAll. Since it is easy
to figure out how the simulation proceeds, we will only use an example to illustrate it and omit thedetails here. Let us consider f (x 1 , x 2 ) = x 12 + 2x 1x 2 + 5. By abusing the notation, we also use x 1 , x 2
as string variables in the simulation. We will introduce a string variable for each subexpression inf (x 1 , x 2 ), namely the variables yx 12 , yx 1 x 2 , y2x 1 x 2 , yx 12 +2x 1 x 2 , yf (x 1,x 2 ) . Then f (x 1 , x 2 ) is simulated by
the SL[◦, replaceAll] formulaCf≡ yx 12 = replaceAll(x 1 , a, x 1 ) ∧ yx 1 x 2 = replaceAll(x 1 , a, x 2 ) ∧y2x 1 x 2 = replaceAll(aa, a, yx 1 x 2 ) ∧ yx 12 +2x 1 x 2 = yx 12 ◦ y2x 1 x 2 ∧yf (x 1,x 2 ) = yx 12 +2x 1 x 2 ◦ aaaaa ∧ x 1 ∈ a ∗ ∧ x 2 ∈ a ∗ .

Then according to Proposition 3.6, C f , Cд can be turned into equivalent SL[replaceAll] formula
C f′ , Cд′ by introducing fresh letters.
Since C f′ and Cд′ share only source variables x 1 , · · · , x n , we know that C f′ ∧ Cд′ is still an
SL[replaceAll] formula. From the construction of C f′ , Cд′ , it is evident that for every pair of polynomials f (x 1 , · · · , x n ) and д(x 1 , · · · , x n ), f (x 1 , · · · , x n ) = д(x 1 , · · · , x n ) has a solution in natural
numbers iff C f′ ∧ Cд′ ∧ |yf | = |yд | is satisfiable. The proof is complete.
□
G.2

Undecidability of Depth-1 Dependency Graph

We recall the undecidability of a depth-1 dependency graph before providing the proof below.
Theorem9.5 For the extension of SL[replaceAll] with integer constraints, even if SL[replaceAll] formulae are restricted to those whose dependency graphs are of depth at most one, the satisfiability
problem is still undecidable.
A linear polynomial (resp. quadratic polynomial) is a polynomial with degree at most one (resp.
with degree at most two) where each coefficient is an integer.
Theorem G.1 ([?]). The following problem is undecidable: Determine whether a system of equationsof the following form has a solution in natural numbers,
Ai = B i ,i = 1, · · · , k,yi Fi = G i ∧ yi Hi = Ii , i = 1, · · · , m,where Ai , Bi , Fi , G i are linear polynomials on the variables x 1 , · · · , x n (Note that each variable yi
occurs in exactly two quadratic equations).
Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.

3:36

Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu

We can get a reduction from the problem in Theorem G.1 to the satisfiability of the extensionof SL[replaceAll] with integer constraints as follows: For each monomial yi x j in the quadratic
polynomials, we use an SL[replaceAll] formula zyi x j = replaceAll(yi , a, x j ) to simulate yi x j , wherezyi x j are freshly introduced string variables. Since each equation yi Fi = G i or yi Hi = Ii can beseen as a linear combination of the terms yi x j and x j for i ∈ [m] and j ∈ [n], we can replace eachvariable x j with |x j |, and each term yi x j with |zyi x j |, thus transform them into the (linear) integer
constraints Fi′ = G i′ or Hi′ = Ii′. Similarly, after replacing each variable x j with |x j |, we transform
each equation Ai = Bi into an integer constraint Ai′ = Bi′ . Therefore, we get a formulaVVV
zyi x j = replaceAll(yi , a, x j ) ∧yi ∈ a ∗ ∧x j ∈ a∗ ∧i ∈[m], j ∈[n]i ∈[m]j ∈[n]V ′V
Ai = Bi′ ∧(Fi′ = G i′ ∧ Hi′ = Ii′ ),i ∈[k ]i ∈[m]

where the dependency graph of the SL[replaceAll] subformula is of depth at most one.
G.3

Undecidability of the Character Constraints

We provide part of the proof of Proposition 9.6, in particular, we show the undecidability of character
constraints.
Proposition G.2. For the extension of SL[replaceAll] with character constraints, the satisfiability
problem is undecidable.
The arguments for Proposition G.2 proceed as follows. Recall that in the proof of Theorem 9.4,
we get a formula C f ∧ Cд ∧ |yf | = |yд | such that f (x 1 , · · · , x n ) = д(x 1 , · · · , x n ) has a solution innatural numbers iff C f ∧Cд ∧ |yf | = |yд | is satisfiable. Let $ , a. Suppose z f = yf ◦ $, and zд = yд ◦ $.
Then |yf | = |yд | can be captured by z f [n] = $[1] ∧ zд [n] = $[1], where n is a variable of type Int.
More precisely, we haveC f ∧ Cд ∧ |yf | = |yд | is satisfiableiff
C f ∧ Cд ∧ z f = yf ◦ $ ∧ zд = yд ◦ $ ∧ z f [n] = $[1] ∧ zд [n] = $[1] is satisfiable.
Therefore, we get a reduction from Hilbert’s tenth problem to the satisfiability problem for theextension of SL[replaceAll] with character constraints.
G.4

Undecidability of the IndexOf Constraints

We provide the final part of the proof of Proposition 9.6, in particular, we show the undecidabilityof IndexOf constraints.
Proposition G.3. For the extension of SL[replaceAll] with the IndexOf constraints, the satisfiability
problem is undecidable.
Proposition G.2 follows from the following observation and Theorem 9.4: For any two string
variables x, y over a unary alphabet, 1 = IndexOf(x, y) iff x is a prefix of y. Therefore, |x | = |y| iff
1 = IndexOf(x, y) ∧ 1 = IndexOf(y, x ). This implies that in the proof of Theorem 9.4, we can replace|yf | = |yд | with 1 = IndexOf(yf , yд ) ∧ 1 = IndexOf(yд , yf ) and get a reduction from Hilbert’stenth problem to the satisfiability problem for the extension of SL[replaceAll] with the IndexOf
constraints. Note that = can be simulated as a conjunction of ≤ and ≥.

Proceedings of the ACM on Programming Languages, Vol. 2, No. POPL, Article 3. Publication date: January 2018.