FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions

TL;DR

FOREST is an interactive synthesizer that generates regular expressions for form validation by combining enumerative search, SMT solving, and a novel multi-tree representation, achieving high success rates on real-world tasks.

Contribution

It introduces a multi-tree representation and SMT encoding for efficient regular expression synthesis, along with user interaction to improve accuracy.

Findings

Successfully synthesized regex in 72% of real-world cases

Outperforms the state-of-the-art synthesizer REGEL

Effective divide-and-conquer approach for regex synthesis

Abstract

Form validators based on regular expressions are often used on digital forms to prevent users from inserting data in the wrong format. However, writing these validators can pose a challenge to some users. We present FOREST, a regular expression synthesizer for digital form validations. FOREST produces a regular expression that matches the desired pattern for the input values and a set of conditions over capturing groups that ensure the validity of integer values in the input. Our synthesis procedure is based on enumerative search and uses a Satisfiability Modulo Theories (SMT) solver to explore and prune the search space. We propose a novel representation for regular expressions synthesis, multi-tree, which induces patterns in the examples and uses them to split the problem through a divide-and-conquer approach. We also present a new SMT encoding to synthesize capture conditions for a given regular expression. To increase confidence in the synthesized regular expression, we implement user interaction based on distinguishing inputs. We evaluated FOREST on real-world form-validation instances using regular expressions. Experimental results show that FOREST successfully returns the desired regular expression in 72% of the instances and outperforms REGEL, a state-of-the-art regular expression synthesizer.