Solving String Constraints With Regex-Dependent Functions Through\n Transducers With Priorities And Variables

Regular expressions are a classical concept in formal language theory.\nRegular expressions in programming languages (RegEx) such as JavaScript,\nfeature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as\nwell as additional features such as capturing groups and references. While\nsymbolic execution of programs containing RegExes appeals to string solvers\nnatively supporting important features of RegEx, such a string solver is\nhitherto missing. In this paper, we propose the first string theory and string\nsolver that natively provide such a support. The key idea of our string solver\nis to introduce a new automata model, called prioritized streaming string\ntransducers (PSST), to formalize the semantics of RegEx-dependent string\nfunctions. PSSTs combine priorities, which have previously been introduced in\nprioritized finite-state automata to capture greedy/lazy semantics, with string\nvariables as in streaming string transducers to model capturing groups. We\nvalidate the consistency of the formal semantics with the actual JavaScript\nsemantics by extensive experiments. Furthermore, to solve the string\nconstraints, we show that PSSTs enjoy nice closure and algorithmic properties,\nin particular, the regularity-preserving property (i.e., pre-images of regular\nconstraints under PSSTs are regular), and introduce a sound sequent calculus\nthat exploits these properties and performs propagation of regular constraints\nby means of taking post-images or pre-images. Although the satisfiability of\nthe string constraint language is undecidable, we show that our approach is\ncomplete for the so-called straight-line fragment. We evaluate the performance\nof our string solver on over 195000 string constraints generated from an\nopen-source RegEx library. The experimental results show the efficacy of our\napproach, drastically improving the existing methods in both precision and\nefficiency.\n