ReGiS: Regular Expression Simplification via Rewrite-Guided Synthesis

Expression simplification is an important task necessary in a variety of domains, e.g., compilers, 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 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 simplification. We demonstrate the flexibility and practicality of our approach by applying ReGiS to regular expression denial of service (ReDoS) attack prevention. Many real-world regular expression matching engines are vulnerable to these complexity-based attacks, and while much research has focused on detecting vulnerable regular expressions, we provide a way for developers to go further, by automatically transforming their regular expressions to remove vulnerabilities.