Certified virtual machine-based regular expression parsing.

Abstract

Regular expressions (REs) are pervasive in computing. We use REs in text editors, string search tools (like GNU-Grep) and lexical analyzers generators. Most of these tools rely on converting REs to its corresponding finite state machine or use REs derivatives for directly parse an input string. In this work, we investigated the suitability of another approach: instead of using derivatives or generating a finite state machine for a given RE, we developed a certified virtual machine-based algorithm (VM) for parsing REs, in such a way that a RE is merely a program executed by the VM over the input string. First, we developed a small-step operational semantics for the algorithm, implemented it in Haskell, tested it using QuickCheck and provided proof sketches of its correctness with respect to RE standard inductive semantics. After that, we developed a big-step operational semantics, an evolution of the small-step one. Unlike the small-step, the bigstep semantics can deal with problematic REs. We showed that the big-step semantics for our VM is also sound and complete with regard to a standard inductive semantics for REs and that the evidence produced by it denotes a valid parsing result. All of our results regarding the big-step semantics are formalized in Coq proof assistant and, from it, we extracted a certified algorithm, which we used to build a RE parsing tool using Haskell programming language. Experiments comparing the efficiency of our algorithm with another Haskell tool are reported.