一句话：提出首个原生支持 RegEx（贪婪/懒惰、捕获组）的字符串理论与求解器，核心为带优先级的流式字符串转换器 PSST。
编程语言中的正则表达式（RegEx）具有贪婪/懒惰 Kleene 星、捕获组与引用等非标准语义，现有字符串求解器难以原生支持，阻碍了含 RegEx 程序的符号执行。本文提出首个原生支持这些特性的字符串理论与求解器，核心是新的自动机模型 PSST——在流式字符串转换器中引入优先级（刻画贪婪/懒惰）与字符串变量（刻画捕获组）。作者证明 PSST 保持正则性（正则约束的原像仍正则），并给出可靠矢列演算，通过前像/后像传播正则约束；该方法在 straight-line 片段上完备，实验表明其语义与 JavaScript 实际语义一致，并在 195000 余条约束上于精度与效率两方面显著优于现有符号执行方法。
Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provides such support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is generally undecidable, we show that our approach is complete for the so-called straight-line fragment. We evaluate the performance of our string solver on over 195000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods (via symbolic execution) in both precision and efficiency.
@article{paperbot1566,
title = {Solving string constraints with Regex-dependent functions through transducers with priorities and variables},
author = {Taolue Chen and Alejandro Flores-Lamas and Matthew Hague and Zhilei Han and Denghang Hu and Shuanglong Kan and Anthony W. Lin and Philipp Rümmer and Zhilin Wu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498707}
}