Optimizing Regular Expressions via Rewrite-Guided Synthesis
Optimizing Regular Expressions via Rewrite-Guided Synthesis
复制标题
DOI：
10.1145/3559009.3569664
复制
发表时间：
2021-04
期刊：
影响因子：
--
通讯作者：
Jedidiah McClurg;Miles Claver;J. Garner;J. Vossen;Jordan Schmerge;M. E. Belviranli
中科院分区：
文献类型：
--
作者：
Jedidiah McClurg;Miles Claver;J. Garner;J. Vossen;Jordan Schmerge;M. E. Belviranli
正则表达式在现代系统中无处不在。现实世界中的许多正则表达式效率低下，有时甚至容易受到基于复杂性的攻击。虽然许多研究都集中在检测低效正则表达式或在硬件层面加速正则表达式匹配，但我们研究的是自动转换正则表达式以消除低效。我们将这一问题简化为一般表达式优化，这是编译器之外的各种领域（如数字逻辑设计等）所必需的一项重要任务。带有成本函数的语法指导合成（SyGuS）可用于此目的，但在大量候选表达式中进行有序枚举的成本可能高得令人望而却步。等价饱和是一种替代方法，可以高效地构建和维护由重写规则生成的表达式等价类，但该过程可能无法达到饱和，这意味着无法确认全局最小性。我们提出了一种名为 "重写指导合成"（ReGiS）的新方法，其中 SyGuS 和基于等价饱和的重写之间的独特相互作用有助于克服这些问题，从而为表达式优化提供了一个高效、可扩展的框架。
Regular expressions are pervasive in modern systems. Many real-world regular expressions are inefficient, sometimes to the extent that they are vulnerable to complexity-based attacks, and while much research has focused on detecting inefficient regular expressions or accelerating regular expression matching at the hardware level, we investigate automatically transforming regular expressions to remove inefficiencies. We reduce this problem to general expression optimization, an important task necessary in a variety of domains even beyond compilers, e.g., digital logic design, etc. Syntax-guided synthesis (SyGuS) with a cost function can be used for this purpose, but ordered enumeration through a large space of candidate expressions can be prohibitively expensive. Equality saturation is an alternative approach which allows efficient construction and maintenance of expression equivalence classes generated by rewrite rules, but the procedure may not reach saturation, meaning global minimality cannot be confirmed. We present a new approach called rewrite-guided synthesis (ReGiS), in which a unique interplay between SyGuS and equality saturation-based rewriting helps to overcome these problems, resulting in an efficient, scalable framework for expression optimization.