使用ReplaceAll函数可以判定字符串约束的哪些内容
What Is Decidable about String Constraints with the ReplaceAll Function
摘要：
最近，有研究表明，任何包含字符串替换函数的字符串理论（即使是最严格的版本，其中模式/替换字符串都是常量字符串）都变得不可判定，如果我们不对公式施加某种直线（又名非循环性）限制。尽管如此，直线限制实际上仍然是合理的，因为这个条件通常由符号执行生成的字符串约束来满足。在本文中，我们提供了第一个系统的研究，直线字符串约束的字符串替换功能和规则的约束作为基本操作。我们表明，一个大类的这种约束（即当只有一个常量字符串或正则表达式是允许的模式）是可判定的。我们注意到，即使在这种限制下，字符串替换函数也足够强大，可以表达连接运算符和更多内容（例如，使用字符串变量扩展正则表达式）。这为我们提供了最具表达力的可判定逻辑，其中包含同一保护伞下的连接、替换和正则约束。我们的直线片段的决策过程遵循自动机理论的方法，并且是模块化的，在这个意义上，字符串替换项被一个接一个地移除，以生成越来越多的规则约束，然后可以由最先进的字符串约束求解器排出。我们还表明，这个片段是，在某种程度上，一个最大的可判定子类的直线片段字符串替换和定期的限制。为此，我们给出了以下两种扩展的不可判定性结果：（1）在替换函数的模式参数中允许变量，（2）允许长度约束。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
