What Is Decidable about String Constraints with the ReplaceAll Function

TL;DR

This paper investigates the decidability of string constraints involving the replaceAll function under straight-line restrictions, introducing a decidable class that balances expressiveness and computational feasibility.

Contribution

It provides the first systematic study of straight-line string constraints with replaceAll and regular constraints, identifying a large decidable fragment and a decision procedure based on automata theory.

Findings

A large class of straight-line string constraints with replaceAll is decidable.

The decision procedure is automata-theoretic and modular, removing replaceAll terms iteratively.

Extensions such as variable patterns and length constraints lead to undecidability.

Abstract

Recently, it was shown that any theory of strings containing the string-replace function (even the most restricted 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 straight-line 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 show that 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, and regular 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 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.