Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and VariablesRemote
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.
Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 25mResearch paper | Software Model-Checking as Cyclic-Proof SearchRemote POPL DOI Media Attached | ||
10:45 25mResearch paper | Induction Duality: Primal-Dual Search for InvariantsRemote POPL Oded Padon VMware Research; Stanford University, James R. Wilcox Certora, Jason R. Koenig Stanford University, Kenneth L. McMillan University of Texas at Austin, Alex Aiken Stanford University DOI Media Attached | ||
11:10 25mResearch paper | Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive FunctionsRemote POPL Hari Govind V K University of Waterloo, Sharon Shoham Tel Aviv University, Arie Gurfinkel University of Waterloo DOI Media Attached | ||
11:35 25mResearch paper | Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and VariablesRemote POPL Taolue Chen Birkbeck University of London, Alejandro Flores Lamas Royal Holloway University of London, Matthew Hague Royal Holloway University of London, Zhilei Han Tsinghua University, Denghang Hu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Zhilin Wu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences DOI Media Attached |