Solving string constraints with Regex-dependent functions through transducers with priorities and variables
Solving string constraints with Regex-dependent functions through transducers with priorities and variables
复制标题
DOI：
10.1145/3498707
复制
发表时间：
2021-11
影响因子：
--
通讯作者：
Taolue Chen;Alejandro Flores-Lamas;M. Hague;Zhilei Han;Denghang Hu;Shuanglong Kan;A. Lin;Philipp Rümmer;Zhilin Wu
中科院分区：
文献类型：
--
作者：
Taolue Chen;Alejandro Flores-Lamas;M. Hague;Zhilei Han;Denghang Hu;Shuanglong Kan;A. Lin;Philipp Rümmer;Zhilin Wu
正则表达式是正式语言理论中的经典概念。编程语言中的正式表达式（REGEX），例如JavaScript，具有运算符的非标准语义（例如贪婪/懒惰的Kleene Star），以及其他功能，例如捕获组和参考。符号执行包含REGEXES的程序的执行吸引了符号求解器的线条求解器，以支持Regex的重要功能，但迄今缺少这样的字符串求解器。在本文中，我们提出了本地提供此类支持的第一个字符串理论和字符串求解器。我们的字符串求解器的关键思想是引入一种新的自动机模型，称为优先流式的String trandducer（PSST），以形式化REGEX依赖性字符串函数的语义。 PSST结合了优先级，这些优先级以前在优先级的有限状态自动机中引入，以捕获贪婪/懒惰的语义，而字符串变量如流式的字符串传感器中以模型捕获组。我们通过广泛的实验来验证形式语义与实际JavaScript语义的一致性。此外，为了解决字符串约束，我们表明PSST享有良好的封闭和算法属性，尤其是具有规则性的属性（即PSST下的规则约束前的预图像是常规的），并引入了一个声音的calculus，可以利用一种声音这些属性并通过拍摄后图像或图像来进行定期约束的传播。尽管字符串约束语言的满意度通常是不可确定的，但我们表明我们的方法对于所谓的直线片段是完整的。我们评估了从开源正则库产生的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.