# HG changeset patch # User Chengsong # Date 1648155583 0 # Node ID 31abe0e496bc89cd0f45d2aa9afbc94285f6cc88 # Parent 2e7c7111c0beed8ff58de56be015f3cba1b91d4d forget diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/ChengsongPhDThesis.tex --- a/ChengsongPhdThesis/ChengsongPhDThesis.tex Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,2132 +0,0 @@ -\documentclass[a4paper,UKenglish]{lipics} -\usepackage{graphic} -\usepackage{data} - -%\usepackage{algorithm} -\usepackage{amsmath} -\usepackage[noend]{algpseudocode} -\usepackage{enumitem} -\usepackage{nccmath} -\usepackage{tikz-cd} -\usetikzlibrary{positioning} - -\definecolor{darkblue}{rgb}{0,0,0.6} -\hypersetup{colorlinks=true,allcolors=darkblue} -\newcommand{\comment}[1]% -{{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}} - -% \documentclass{article} -%\usepackage[utf8]{inputenc} -%\usepackage[english]{babel} -%\usepackage{listings} -% \usepackage{amsthm} -%\usepackage{hyperref} -% \usepackage[margin=0.5in]{geometry} -%\usepackage{pmboxdraw} - -\title{POSIX Regular Expression Matching and Lexing} -\author{Chengsong Tan} -\affil{King's College London\\ -London, UK\\ -\texttt{chengsong.tan@kcl.ac.uk}} -\authorrunning{Chengsong Tan} -\Copyright{Chengsong Tan} - -\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% -\newcommand{\ZERO}{\mbox{\bf 0}} -\newcommand{\ONE}{\mbox{\bf 1}} -\def\lexer{\mathit{lexer}} -\def\mkeps{\mathit{mkeps}} - -\def\DFA{\textit{DFA}} -\def\bmkeps{\textit{bmkeps}} -\def\retrieve{\textit{retrieve}} -\def\blexer{\textit{blexer}} -\def\flex{\textit{flex}} -\def\inj{\mathit{inj}} -\def\Empty{\mathit{Empty}} -\def\Left{\mathit{Left}} -\def\Right{\mathit{Right}} -\def\Stars{\mathit{Stars}} -\def\Char{\mathit{Char}} -\def\Seq{\mathit{Seq}} -\def\Der{\mathit{Der}} -\def\nullable{\mathit{nullable}} -\def\Z{\mathit{Z}} -\def\S{\mathit{S}} -\def\rup{r^\uparrow} - -\newcommand{\PDER}{\textit{PDER}} -\newcommand{\flts}{\textit{flts}} -\newcommand{\distinctBy}{\textit{distinctBy}} -\newcommand{\map}{\textit{map}} -\newcommand{\size}{\textit{size}} -\def\awidth{\mathit{awidth}} -\def\pder{\mathit{pder}} -\def\maxterms{\mathit{maxterms}} -\def\bsimp{\mathit{bsimp}} - -%\theoremstyle{theorem} -%\newtheorem{theorem}{Theorem} -%\theoremstyle{lemma} -%\newtheorem{lemma}{Lemma} -%\newcommand{\lemmaautorefname}{Lemma} -%\theoremstyle{definition} -%\newtheorem{definition}{Definition} -\algnewcommand\algorithmicswitch{\textbf{switch}} -\algnewcommand\algorithmiccase{\textbf{case}} -\algnewcommand\algorithmicassert{\texttt{assert}} -\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}% -% New "environments" -\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}% -\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}% -\algtext*{EndSwitch}% -\algtext*{EndCase}% - - -\begin{document} - -\maketitle - -\begin{abstract} - Brzozowski introduced in 1964 a beautifully simple algorithm for - regular expression matching based on the notion of derivatives of - regular expressions. In 2014, Sulzmann and Lu extended this - algorithm to not just give a YES/NO answer for whether or not a - regular expression matches a string, but in case it does also - answers with \emph{how} it matches the string. This is important for - applications such as lexing (tokenising a string). The problem is to - make the algorithm by Sulzmann and Lu fast on all inputs without - breaking its correctness. We have already developed some - simplification rules for this, but have not yet proved that they - preserve the correctness of the algorithm. We also have not yet - looked at extended regular expressions, such as bounded repetitions, - negation and back-references. -\end{abstract} - -\section{Introduction} -\subsection{Basic Regex Introduction} - -Suppose (basic) regular expressions are given by the following grammar: -\[ r ::= \ZERO \mid \ONE - \mid c - \mid r_1 \cdot r_2 - \mid r_1 + r_2 - \mid r^* -\] - -Problem of matching: - -\begin{center} -\begin{tabular}{lcr} -$\textit{Match}(r, s)$ & $ = $ & $\textit{if}\; s \in L(r)\; \textit{output} \; \textit{YES}$\\ -& & $\textit{else} \; \textit{output} \; \textit{NO}$ -\end{tabular} -\end{center} -Omnipresent use of regexes in modern -software. -Examples: Snort, Bro, etc? -\subsubsection{The rules for network intrusion analysis tools } -TODO: read rules libraries such as Snort and the explanation for some of the rules -TODO: pcre/pcre2? -TODO: any other libraries? - - -There has been many widely used libraries such as -Henry Spencer's regexp(3), RE2, etc. -They are fast and successful, but ugly corner cases -allowing the $\textit{ReDoS}$ attack exist, and -is a non-negligible protion. -\subsection{The practical problem} -These corner cases either -\begin{itemize} -\item -go unnoticed until they -cause considerable grief in real life -\item -or force the regex library writers to pose -restrictions on the input, limiting the -choice a programmer has when using regexes. -\end{itemize} - -Motivation: -We want some library that supports as many constructs as possible, -but still gives formal guarantees on the correctness and running -time. - -\subsection{Regexes that brought down CloudFlare} - - -matching some string $s$ with a regex - -\begin{verbatim} -(?:(?:\"|'|\]|\}|\\|\d| -(?:nan|infinity|true|false|null|undefined|symbol|math) -|\`|\-|\+)+[)]*;?((?:\s|-|~|!|{}|\|\||\+)*.*(?:.*=.*))) -\end{verbatim} - - -%Could be from a network intrusion detection algorithm. -%Checking whether there is some malicious code -%in the network data blocks being routed. -%If so, discard the data and identify the sender for future alert. -\section{Existing approaches} -\subsection{Shortcomings of different methods} - - -\subsubsection{ NFA's} -$\bold{Problems With This:}$ -\begin{itemize} -\item -Can be slow especially when many states are active. -\item -Want Lexing Results: Can have Exponential different matching results. -\end{itemize} - - -One regular expression can have multiple lexical values. For example -for the regular expression $(a+b)^*$, it has a infinite list of -values corresponding to it: $\Stars\,[]$, $\Stars\,[\Left(Char(a))]$, -$\Stars\,[\Right(Char(b))]$, $\Stars\,[\Left(Char(a),\,\Right(Char(b))]$, -$\ldots$, and vice versa. -Even for the regular expression matching a certain string, there could -still be more than one value corresponding to it. -Take the example where $r= (a^*\cdot a^*)^*$ and the string -$s=\underbrace{aa\ldots a}_\text{n \textit{a}s}$. -The number of different ways of matching -without allowing any value under a star to be flattened -to an empty string can be given by the following formula: -\begin{center} - $C_n = (n+1)+n C_1+\ldots + 2 C_{n-1}$ -\end{center} -and a closed form formula can be calculated to be -\begin{equation} - C_n =\frac{(2+\sqrt{2})^n - (2-\sqrt{2})^n}{4\sqrt{2}} -\end{equation} -which is clearly in exponential order. -A lexer aimed at getting all the possible values has an exponential -worst case runtime. Therefore it is impractical to try to generate -all possible matches in a run. In practice, we are usually -interested about POSIX values, which by intuition always -match the leftmost regular expression when there is a choice -and always match a sub part as much as possible before proceeding -to the next token. For example, the above example has the POSIX value -$ \Stars\,[\Seq(Stars\,[\underbrace{\Char(a),\ldots,\Char(a)}_\text{n iterations}], Stars\,[])]$. -The output of an algorithm we want would be a POSIX matching -encoded as a value.\\ -$\mathbf{TODO:}$ -\begin{itemize} -\item -Illustrate graphically how you can match $a*a**$ with $aaa$ in different ways. -\item -Give a backtracking algorithm, and explain briefly why this can be exponentially slow. -(When there is a matching, it finds straight away; where there is not one, this fails to -recognize immediately that a match cannot be possibly found, and tries out all remaining -possibilities, etc.) -\item -From the above point, are there statical analysis tools that single out those malicious -patterns and tell before a lexer is even run? -Have a more thorough survey of the Birmingham paper. -Give out the suitable scenarios for such static analysis algorithms. - -\end{itemize} - -\subsubsection{DFAs} -The tool JFLEX uses it. -Advantages: super fast on most regexes \\ -TODO: show it being fast on a lot of inputs\\ -Disavantages: -state explosion for bounded repetitions due to -theoretic bottleneck of having to remember exactly what the -suffix up to length $n$ of input string is. -"Countdown States activation problem": -$.*a.{100}$ requires $2^100$ + DFA states. -Example: -Converting $((a|b )*b.{10}){3}$ to a $\DFA$ -gives the error: -\begin{verbatim} -147972 states before minimization, 79107 states in minimized DFA -Old file "search.java" saved as "search.java~" -Writing code to "search.java" - -Unexpected exception encountered. This indicates a bug in JFlex. -Please consider filing an issue at http://github.com/jflex-de/jflex/issues/new - - -character value expected -java.lang.IllegalArgumentException: character value expected - at jflex.generator.PackEmitter.emitUC(PackEmitter.java:105) - at jflex.generator.CountEmitter.emit(CountEmitter.java:116) - at jflex.generator.Emitter.emitDynamicInit(Emitter.java:530) - at jflex.generator.Emitter.emit(Emitter.java:1369) - at jflex.generator.LexGenerator.generate(LexGenerator.java:115) - at jflex.Main.generate(Main.java:320) - at jflex.Main.main(Main.java:336) -\end{verbatim} - -\subsubsection{variant of DFA's} -counting set automata -\\ -TODO: microsoft 2020 oopsla CsA work, need to add bibli entry, and read, understand key novelty, learn to benchmark like it -\\ -TODO: find weakness of such counting set automata? -\\ -Other variants? - -\subsubsection{NFA and Regex: isomorphic structure} -TODO: define mathematically an isomorphism?\\ - - - -\subsubsection{variants of NFA's} -How about acting on regular expressions themselves? Certain copies represent verbose info--that they will always match the same string--prune away! - -\subsection{Brzozowski's derivatives} - -\subsection{Sulzmann and Lu's algorithm} - -\subsection{Bit-coded algorithm} -+bitcodes! -Built on top of derivatives, but with auxiliary bits -\subsection{Correctness Proof} - -Not proven by Sulzmann and Lu - -Proven by Ausaf and Urban!! - - -For this we have started with looking at the proof of -\begin{equation}\label{lexer} -\blexer \; (r^\uparrow) s = \lexer \;r \;s, -\end{equation} - -%\noindent -%might provide us insight into proving -%\begin{center} -%$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$ -%\end{center} - -\noindent -which established that the bit-sequence algorithm produces the same -result as the original algorithm, which does not use -bit-sequences. -The proof uses two ``tricks''. One is that it uses a \flex-function - -\begin{center} -\begin{tabular}{lcl} -$\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \; (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\ -$\textit{flex} \;r\; f\; [\,] $ & $\dn$ & $f$ -\end{tabular} -\end{center} - -\noindent - -The intuition behind the $\flex$ function is that - it accumulates a series of $\inj$ function applications when doing derivatives - in a $\mathit{LIFO}$ manner. The arguments of the $\inj$ functions are kept by - remembering which character - was chopped off and what the regular expression looks like before - chopping off that character. - The $\mathit{LIFO}$ order was achieved by putting the newest $\inj$ application - always before the application of $f$, the previously accumulated function applications.\\ -Therefore, the function $\flex$, when acted on a string $s@[c]$ where the last -character is $c$, by nature can have its last injection function revealed already: -\begin{equation}\label{flex} -\flex \; r \; id \; (s@[c]) \; v = \flex \; r \; id \; s \; (inj \; (r\backslash s) \; c\; v). -\end{equation} -that the last character can be taken off, and the injection it causes be applied to -the argument value $v$. - -Ausaf and Urban proved that the Sulzmann and Lu's lexers -can be charactarized by the $\flex$ function: -\begin{center} -$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$. -\end{center} - -\noindent -This property says that the Sulzmann and Lu's $\lexer$ does lexing by -stacking up injection functions while doing derivatives, -explicitly showing the order of characters being -injected back in each step. - -\noindent -The other trick, which is the crux in the existing proof, -is the use of the $\retrieve$-function: -\begin{center} -\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}} - $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\ - $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\ - $\textit{retrieve}\,(_{bs}\sum a::as)\,(\Left\,v)$ & $\dn$ & - $bs \,@\, \textit{retrieve}\,a\,v$\\ - $\textit{retrieve}\,(_{bs}\sum a::as)\,(\Right\,v)$ & $\dn$ & - $\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\sum as)\,v$\\ - $\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ & - $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\ - $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ & - $bs \,@\, [0]$\\ - $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\ - \multicolumn{3}{l}{ - \hspace{3cm}$bs \,@\, [1] \,@\, \textit{retrieve}\,a\,v\,@\, - \textit{retrieve}\,(_{[]}a^*)\,(\Stars\,vs)$}\\ -\end{tabular} -\end{center} - -\noindent -Sulzmann and Lu proposed this function, but did not prove -anything about it. Ausaf and Urban made use of the -fact about $\retrieve$ in their proof: - \begin{equation}\label{retrieve_reversible} - \retrieve\; \rup \backslash c \; v = \retrieve \; \rup (\inj \;r \;c \; v) - \end{equation} -This says that $\retrieve$ will always pick up -partial information about a lexing value value and transform it into suitable bitcodes. -If the information is in the regular expression (stored as bitcodes), it will keep those -bitcodes with the guidance of the value, -if the information is in the value, which has been injected back to the value, -it will "digest" and transform that part of the value to bitcodes. - -\noindent - -Using this together with ~\eqref{flex}, we can prove that the bitcoded version of -lexer is the same as Sulzmann and Lu's lexer: -\begin{center} -$\lexer \; r \; s = \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{bmkeps}\; (\rup \backslash s) ) r = \blexer \; r \; s$ -\end{center} -\noindent -\begin{proof} -We express $\bmkeps$ using $\retrieve$, and the theorem to prove becomes: -\begin{center} -$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$ -\end{center} -\noindent -We prove the above by reverse induction on string $s$(meaning that the inductive step is on -$s @ [c]$ rather than $c :: s$). -$v$ takes arbitrary values.\\ -The base case goes through trivially.\\ -For the inductive step, assuming -$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$ -holds for all values $v$. Now we need to show that -$ \flex \; r\; id\; s@[c]\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash (s@[c])) \; v \;) r$.\\ -~\eqref{flex} allows us to do the following rewrite: -\begin{center} -$ \flex \; r\; id\; (s@[c])\; v = \flex \; r \; id\; s\; (\inj \; (r \backslash s) \; c\; v)= \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; (\inj \; (r\backslash s) \;c\;v)\;) r$ -\end{center} -~\eqref{retrieve_reversible} allows us to further rewrite the $\mathit{RHS}$ of the above to -\begin{center} -$\textit{decode} \; (\textit{retrieve}\; (\rup \backslash (s @ [c])) \; v\;) \;r$ -\end{center} - - -\end{proof} - - - -\section{My Work} - -\subsection{an improved version of bit-coded algorithm: with simp!} - -\subsection{a correctness proof for bitcoded algorithm} - -\subsection{finiteness proof } -\subsubsection{closed form} -We can give the derivative of regular expressions -with respect to string a closed form with respect to simplification: -\begin{itemize} -\item -closed form for sequences: -\begin{verbatim} -lemma seq_closed_form: shows -"rsimp (rders_simp (RSEQ r1 r2) s) = -rsimp ( RALTS ( (RSEQ (rders_simp r1 s) r2) # - (map (rders r2) (vsuf s r1)) - ) - )" -\end{verbatim} -where the recursive function $\textit{vsuf}$ is defined as -\begin{verbatim} -fun vsuf :: "char list -> rrexp -> char list list" where -"vsuf [] _ = []" -|"vsuf (c#cs) r1 = (if (rnullable r1) then (vsuf cs (rder c r1)) @ [c # cs] - else (vsuf cs (rder c r1)) - ) " - -\end{verbatim} -\item -closed form for stars: -\begin{verbatim} -lemma star_closed_form: - shows "rders_simp (RSTAR r0) (c#s) = -rsimp ( RALTS ( -(map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) -(star_updates s r [[c]]) ) ))" -\end{verbatim} -where the recursive function $\textit{star}\_\textit{updates}$ is defined as -\begin{verbatim} -fun star_update :: "char -> rrexp -> char list list -> char list list" where -"star_update c r [] = []" -|"star_update c r (s # Ss) = (if (rnullable (rders_simp r s)) - then (s@[c]) # [c] # (star_update c r Ss) - else (s@[c]) # (star_update c r Ss) )" - -fun star_updates :: "char list -> rrexp -> char list list -> char list list" - where -"star_updates [] r Ss = Ss" -| "star_updates (c # cs) r Ss = star_updates cs r (star_update c r Ss)" - -\end{verbatim} - - -\end{itemize} -These closed form is a formalization of the intuition - that we can push in the derivatives -of compound regular expressions to its sub-expressions, and the resulting -expression is a linear combination of those sub-expressions' derivatives. -\subsubsection{Estimation of closed forms' size} -And thanks to $\textit{distinctBy}$ helping with deduplication, -the linear combination can be bounded by the set enumerating all -regular expressions up to a certain size : -\begin{verbatim} - -lemma star_closed_form_bounded_by_rdistinct_list_estimate: - shows "rsize (rsimp ( RALTS ( (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) - (star_updates s r [[c]]) ) ))) <= - Suc (sum_list (map rsize (rdistinct (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) - (star_updates s r [[c]]) ) {}) ) )" - - lemma distinct_list_rexp_up_to_certain_size_bouded_by_set_enumerating_up_to_that_size: - shows "\forallr\in set rs. (rsize r ) <= N ==> sum_list (map rsize (rdistinct rs {})) <= - (card (rexp_enum N))* N" - - lemma ind_hypo_on_ders_leads_to_stars_bounded: - shows "\foralls. rsize (rders_simp r0 s) <= N ==> - (sum_list (map rsize (rdistinct (map (\lambda s1. RSEQ (rders_simp r0 s1) (RSTAR r0) ) - (star_updates s r [[c]]) ) {}) ) ) <= -(card (rexp_enum (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0))) -" -\end{verbatim} - -With the above 3 lemmas, we can argue that the inductive hypothesis -$r_0$'s derivatives is bounded above leads to $r_0^*$'s -derivatives being bounded above. -\begin{verbatim} - -lemma r0_bounded_star_bounded: - shows "\foralls. rsize (rders_simp r0 s) <= N ==> - \foralls. rsize (rders_simp (RSTAR r0) s) <= -(card (rexp_enum (Suc (N + rsize (RSTAR r0))))) * (Suc (N + rsize (RSTAR r0)))" -\end{verbatim} - - -And we have a similar argument for the sequence case. -\subsection{stronger simplification needed} - -\subsubsection{Bounded List of Terms} -We have seen that without simplification the size of $(a+aa)^*$ -grows exponentially and unbounded(where we omit certain nested -parentheses among the four terms in the last explicitly written out regex): - -\def\ll{\stackrel{\_\backslash{} a}{\longrightarrow}} -\begin{center} -\begin{tabular}{rll} -$(a + aa)^*$ & $\ll$ & $(\ONE + \ONE{}a) \cdot (a + aa)^*$\\ -& $\ll$ & $(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* \;+\; (\ONE + \ONE{}a) \cdot (a + aa)^*$\\ -& $\ll$ & $(\ZERO + \ZERO{}a + \ZERO) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^* \;+\; $\\ -& & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\ -& $\ll$ & \ldots \hspace{15mm}(regular expressions of sizes 98, 169, 283, 468, 767, \ldots) -\end{tabular} -\end{center} - -But if we look closely at the regex -\begin{center} -\begin{tabular}{rll} -& & $\qquad(\ZERO + \ZERO{}a + \ONE) \cdot (a + aa)^* + (\ONE + \ONE{}a) \cdot (a + aa)^*$\\ -\end{tabular} -\end{center} -we realize that: -\begin{itemize} -\item -The regex is equivalent to an alternative taking a long-flattened list, -where each list is a sequence, and the second child of that sequence -is always $(a+aa)^*$. In other words, the regex is a "linear combination" -of terms of the form $(a+aa)\backslash s \cdot (a+aa)^*$ ($s$ is any string). -\item -The number of different terms of the shape $(a+aa) \backslash s \cdot (a+aa)^*$ is -bounded because the first child $(a+aa) \backslash s$ can only be one of -$(\ZERO + \ZERO{}a + \ZERO)$, $(\ZERO + \ZERO{}a + \ONE)$, -$(\ONE + \ONE{}a)$ and $(\ZERO + \ZERO{}a)$. -\item -With simplification we have that the regex is additionally reduced to, - -where each term $\bsimp((a+aa)\backslash s ) $ -is further reduced to only -$\ONE$, $\ONE + a$ and $\ZERO$. - - -\end{itemize} -Generalizing this to any regular expression of the form -$\sum_{s\in L(r)} \bsimp(r\backslash s ) \cdot r^*$, -we have the closed-form for star regex's string derivative as below: -$\forall r \;s.\; \exists sl. \; s.t.\;\bsimp(r^* \backslash s) = \bsimp(\sum_{s'\in sl}(r\backslash s') \cdot r^* )$. - -The regex $\bsimp(\sum_{s' \in sl}(r\backslash s') \cdot r^*)$ is bounded by -$\distinctBy(\flts(\sum_{s'\in sl}(\bsimp(r \backslash s')) \cdot r^*))$, -which again is bounded by $\distinctBy(\sum_{s'\in sl}(\bsimp(r\backslash s')) \cdot r^*)$. -This might give us a polynomial bound on the length of the list -$\distinctBy[(\bsimp(r\backslash s')) \cdot r^* | {s'\in sl} ]$, if the terms in -$\distinctBy[(\bsimp (r\backslash s')) | {s' \in sl}]$ has a polynomial bound. -This is unfortunately not true under our current $\distinctBy$ function: -If we let $r_n = ( (aa)^* + (aaa)^* + \ldots + \underline{(a\ldots a)^*}{n \,a's}) $, -then we have that $\textit{maxterms} r_n = \textit{sup} (\textit{length} [\bsimp(r_n\backslash s') | s' \in sl]) = -L.C.M(1,\ldots, n)$. According to \href{http://oeis.org/A003418}{OEISA003418} -this grows exponentially quickly. So we have found a regex $r_n$ where -$\textit{maxterms} (r_n ^* \backslash s) \geq 2^{(n-1)}$. - - -\subsubsection{stronger version of \distinctBy} -\href{https://www.researchgate.net/publication/340874991_Partial_derivatives_of_regular_expressions_and_finite_automaton_constructions}{Antimirove} -has proven a linear bound on the number of terms in the "partial derivatives" of a regular expression: -\begin{center} -$\size (\PDER(r)) \leq \awidth (r)$. -\end{center} - -The proof is by structural induction on the regular expression r. -The hard cases are the sequence case $r_1\cdot r_2$ and star case $r^*$. -The central idea that allows the induction to go through for this bound is on the inclusion: -\begin{center} -$\pder_{s@[c]} (a\cdot b) \subseteq (\pder_{s@[c]} a ) \cdot b \cup (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))$ -\end{center} - -This way, - -\begin{center} -\begin{tabular}{lcl} -$| \pder_{s@[c]} (a\cdot b) |$ & $ \leq$ & $ | (\pder_{s@[c]} a ) \cdot b \cup (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\ -& $\leq$ & $| (\pder_{s@[c]} a ) \cdot b| + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\ -& $=$ & $\awidth(a) + \awidth(b)$ \\ -& $=$ & $\awidth(a+b)$ -\end{tabular} -\end{center} - -we have that a compound regular expression $a\cdot b$'s subterms - is bounded by its sub-expression's derivatives terms. - -This argument can be modified to bound the terms in -our version of regex with strong simplification: -\begin{center} -\begin{tabular}{lcl} -$| \maxterms (\bsimp (a\cdot b) \backslash s)|$ & $=$ & $ |maxterms(\bsimp( (a\backslash s \cdot b) + \sum_{s'\in sl}(b\backslash s') ))|$\\ -& $\leq$ & $| (\pder_{s@[c]} a ) \cdot b| + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\ -& $=$ & $\awidth(a) + \awidth(b)$ \\ -& $=$ & $\awidth(a+b)$ -\end{tabular} -\end{center} - - - - -\subsection{cubic bound} -Bounding the regex's subterms by -its alphabetic width. - -The entire expression's size can be bounded by -number of subterms times each subterms' size. - - - - - -\section{Support for bounded repetitions and other constructs} -Example: -$.*a.\{100\}$ after translation to $\DFA$ and minimization will -always take over $2^{100}$ states. - -\section{Towards a library with fast running time practically} - -registers and cache-related optimizations? -JVM related optimizations? - -\section{Past Report materials} - -Deciding whether a string is in the language of the regex -can be intuitively done by constructing an NFA\cite{Thompson_1968}: -and simulate the running of it. - -Which should be simple enough that modern programmers -have no problems with it at all? -Not really: - -Take $(a^*)^*\,b$ and ask whether -strings of the form $aa..a$ match this regular -expression. Obviously this is not the case---the expected $b$ in the last -position is missing. One would expect that modern regular expression -matching engines can find this out very quickly. Alas, if one tries -this example in JavaScript, Python or Java 8 with strings like 28 -$a$'s, one discovers that this decision takes around 30 seconds and -takes considerably longer when adding a few more $a$'s, as the graphs -below show: - -\begin{center} -\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}} -\begin{tikzpicture} -\begin{axis}[ - xlabel={$n$}, - x label style={at={(1.05,-0.05)}}, - ylabel={time in secs}, - enlargelimits=false, - xtick={0,5,...,30}, - xmax=33, - ymax=35, - ytick={0,5,...,30}, - scaled ticks=false, - axis lines=left, - width=5cm, - height=4cm, - legend entries={JavaScript}, - legend pos=north west, - legend cell align=left] -\addplot[red,mark=*, mark options={fill=white}] table {re-js.data}; -\end{axis} -\end{tikzpicture} - & -\begin{tikzpicture} -\begin{axis}[ - xlabel={$n$}, - x label style={at={(1.05,-0.05)}}, - %ylabel={time in secs}, - enlargelimits=false, - xtick={0,5,...,30}, - xmax=33, - ymax=35, - ytick={0,5,...,30}, - scaled ticks=false, - axis lines=left, - width=5cm, - height=4cm, - legend entries={Python}, - legend pos=north west, - legend cell align=left] -\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data}; -\end{axis} -\end{tikzpicture} - & -\begin{tikzpicture} -\begin{axis}[ - xlabel={$n$}, - x label style={at={(1.05,-0.05)}}, - %ylabel={time in secs}, - enlargelimits=false, - xtick={0,5,...,30}, - xmax=33, - ymax=35, - ytick={0,5,...,30}, - scaled ticks=false, - axis lines=left, - width=5cm, - height=4cm, - legend entries={Java 8}, - legend pos=north west, - legend cell align=left] -\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data}; -\end{axis} -\end{tikzpicture}\\ -\multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings - of the form $\underbrace{aa..a}_{n}$.} -\end{tabular} -\end{center} - -Why? -Using $\textit{NFA}$'s that can backtrack. -%TODO: what does it mean to do DFS BFS on NFA's - - -Then how about determinization? -\begin{itemize} -\item - Turning NFA's to DFA's can cause the size of the automata -to blow up exponentially. -\item -Want to extract submatch information. -For example, -$r_1 \cdot r_2$ matches $s$, -want to know $s = s_1@s_2$ where $s_i$ -corresponds to $r_i$. Where $s_i$ might be the -attacker's ip address. -\item -Variants such as counting automaton exist. -But usually made super fast on a certain class -of regexes like bounded repetitions: -\begin{verbatim} -.*a.{100} -\end{verbatim} -On a lot of inputs this works very well. -On average good practical performance. -~10MiB per second. -But cannot be super fast on all inputs of regexes and strings, -can be imprecise (incorrect) when it comes to more complex regexes. - -\end{itemize} -%TODO: real world example? - - - -\subsection{derivatives} -Q: -Is there an efficient lexing algorithm with provable guarantees on -correctness and running time? -Brzozowski Derivatives\cite{Brzozowski1964}! - -\begin{center} - \begin{tabular}{lcl} - $\nullable(\ZERO)$ & $\dn$ & $\mathit{false}$ \\ - $\nullable(\ONE)$ & $\dn$ & $\mathit{true}$ \\ - $\nullable(c)$ & $\dn$ & $\mathit{false}$ \\ - $\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\ - $\nullable(r_1\cdot r_2)$ & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\ - $\nullable(r^*)$ & $\dn$ & $\mathit{true}$ \\ - \end{tabular} - \end{center} - - - -This function simply tests whether the empty string is in $L(r)$. -He then defined -the following operation on regular expressions, written -$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$): - -\begin{center} -\begin{tabular}{lcl} - $\ZERO \backslash c$ & $\dn$ & $\ZERO$\\ - $\ONE \backslash c$ & $\dn$ & $\ZERO$\\ - $d \backslash c$ & $\dn$ & - $\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\ -$(r_1 + r_2)\backslash c$ & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\ -$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\ - & & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\ - & & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\ - $(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\ -\end{tabular} -\end{center} - - - - -\begin{ceqn} -\begin{equation}\label{graph:01} -\begin{tikzcd} -r_0 \arrow[r, "\backslash c_0"] \arrow[d] & r_1 \arrow[r, "\backslash c_1"] \arrow[d] & r_2 \arrow[r, dashed] \arrow[d] & r_n \arrow[d, "mkeps" description] \\ -v_0 & v_1 \arrow[l,"inj_{r_0} c_0"] & v_2 \arrow[l, "inj_{r_1} c_1"] & v_n \arrow[l, dashed] -\end{tikzcd} -\end{equation} -\end{ceqn} -Nicely functional, correctness easily provable, but suffers -from large stack size with long strings, and -inability to perform even moderate simplification. - - - -The Sulzmann and Lu's bit-coded algorithm: -\begin{figure} -\centering -\includegraphics[scale=0.3]{bitcoded_sulzmann.png} -\end{figure} - -This one-phase algorithm is free from the burden of large stack usage: - -\begin{center} -\begin{tikzpicture}[scale=2,node distance=1.9cm, - every node/.style={minimum size=7mm}] -\node (r0) {$r_0$}; -\node (r1) [right=of r0]{$r_1$}; -\draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash\,c_0$}; -\node (r2) [right=of r1]{$r_2$}; -\draw[->, line width = 0.2mm](r1)--(r2) node[above,midway] {$\backslash\,c_1$}; -\node (rn) [right=of r2]{$r_n$}; -\draw[dashed,->,line width=0.2mm](r2)--(rn) node[above,midway] {} ; -\draw (rn) node[anchor=west] {\;\raisebox{3mm}{$\nullable$}}; -\node (bs) [below=of rn]{$bs$}; -\draw[->,line width=0.2mm](rn) -- (bs); -\node (v0) [left=of bs] {$v_0$}; -\draw[->,line width=0.2mm](bs)--(v0) node[below,midway] {$\textit{decode}$}; -\draw (rn) node[anchor=north west] {\;\raisebox{-8mm}{$\textit{collect bits}$}}; -\draw[->, line width=0.2mm](v0)--(r0) node[below, midway] {}; -\end{tikzpicture} -\end{center} - - - -This is functional code, and easily provable (proof by Urban and Ausaf). - -But it suffers from exponential blows even with the simplification steps: -\begin{figure} -\centering -\includegraphics[scale= 0.3]{pics/nub_filter_simp.png} -\end{figure} -claim: Sulzmann and Lu claimed it linear $w.r.t$ input. - -example that blows it up: -$(a+aa)^*$ -\section{Contributions} -\subsection{Our contribution 1} -an improved version of the above algorithm that solves most blow up -cases, including the above example. - -a formalized closed-form for string derivatives: -\[ (\sum rs) \backslash_s s = simp(\sum_{r \in rs}(r \backslash_s s)) \] -\[ (r1\cdot r2) \backslash_s s = simp(r_1 \backslash_s s \cdot r_2 + \sum_{s' \in Suffix(s)} r_2 \backslash_s s' )\] -\[r0^* \backslash_s s = simp(\sum_{s' \in substr(s)} (r0 \backslash_s s') \cdot r0^*) \] - - - -Also with a size guarantee that make sure the size of the derivatives -don't go up unbounded. - - -\begin{theorem} -Given a regular expression r, we have -\begin{center} -$\exists N_r.\; s.t. \;\forall s. \; |r \backslash_s s| < N_r$ -\end{center} -\end{theorem} - -The proof for this is using partial derivative's terms to bound it. -\begin{center} -\begin{tabular}{lcl} -$| \maxterms (\bsimp (a\cdot b) \backslash s)|$ & $=$ & $ |maxterms(\bsimp( (a\backslash s \cdot b) + \sum_{s'\in sl}(b\backslash s') ))|$\\ -& $\leq$ & $| (\pder_{s@[c]} a ) \cdot b| + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\ -& $=$ & $\awidth(a) + \awidth(b)$ \\ -& $=$ & $\awidth(a+b)$ -\end{tabular} -\end{center} - - -\subsection{Our Contribution 2} -more aggressive simplification that prunes away sub-parts -of a regex based on what terms has appeared before. -Which gives us a truly linear bound on the input length. - - - -\section{To be completed} - -benchmarking our algorithm against JFLEX -counting set automata, Silex, other main regex engines (incorporate their ideas such -as zippers and other data structures reducing memory use). - -extend to back references. - - - - - - -\noindent These are clearly abysmal and possibly surprising results. One -would expect these systems to do much better than that---after all, -given a DFA and a string, deciding whether a string is matched by this -DFA should be linear in terms of the size of the regular expression and -the string? - -Admittedly, the regular expression $(a^*)^*\,b$ is carefully chosen to -exhibit this super-linear behaviour. But unfortunately, such regular -expressions are not just a few outliers. They are actually -frequent enough to have a separate name created for -them---\emph{evil regular expressions}. In empiric work, Davis et al -report that they have found thousands of such evil regular expressions -in the JavaScript and Python ecosystems \cite{Davis18}. Static analysis -approach that is both sound and complete exists\cite{17Bir}, but the running -time on certain examples in the RegExLib and Snort regular expressions -libraries is unacceptable. Therefore the problem of efficiency still remains. - -This superlinear blowup in matching algorithms sometimes causes -considerable grief in real life: for example on 20 July 2016 one evil -regular expression brought the webpage -\href{http://stackexchange.com}{Stack Exchange} to its -knees.\footnote{\url{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}} -In this instance, a regular expression intended to just trim white -spaces from the beginning and the end of a line actually consumed -massive amounts of CPU-resources---causing web servers to grind to a -halt. This happened when a post with 20,000 white spaces was submitted, -but importantly the white spaces were neither at the beginning nor at -the end. As a result, the regular expression matching engine needed to -backtrack over many choices. In this example, the time needed to process -the string was $O(n^2)$ with respect to the string length. This -quadratic overhead was enough for the homepage of Stack Exchange to -respond so slowly that the load balancer assumed there must be some -attack and therefore stopped the servers from responding to any -requests. This made the whole site become unavailable. Another very -recent example is a global outage of all Cloudflare servers on 2 July -2019. A poorly written regular expression exhibited exponential -behaviour and exhausted CPUs that serve HTTP traffic. Although the -outage had several causes, at the heart was a regular expression that -was used to monitor network -traffic.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}} - -The underlying problem is that many ``real life'' regular expression -matching engines do not use DFAs for matching. This is because they -support regular expressions that are not covered by the classical -automata theory, and in this more general setting there are quite a few -research questions still unanswered and fast algorithms still need to be -developed (for example how to treat efficiently bounded repetitions, negation and -back-references). -%question: dfa can have exponential states. isn't this the actual reason why they do not use dfas? -%how do they avoid dfas exponential states if they use them for fast matching? - -There is also another under-researched problem to do with regular -expressions and lexing, i.e.~the process of breaking up strings into -sequences of tokens according to some regular expressions. In this -setting one is not just interested in whether or not a regular -expression matches a string, but also in \emph{how}. Consider for -example a regular expression $r_{key}$ for recognising keywords such as -\textit{if}, \textit{then} and so on; and a regular expression $r_{id}$ -for recognising identifiers (say, a single character followed by -characters or numbers). One can then form the compound regular -expression $(r_{key} + r_{id})^*$ and use it to tokenise strings. But -then how should the string \textit{iffoo} be tokenised? It could be -tokenised as a keyword followed by an identifier, or the entire string -as a single identifier. Similarly, how should the string \textit{if} be -tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would -``fire''---so is it an identifier or a keyword? While in applications -there is a well-known strategy to decide these questions, called POSIX -matching, only relatively recently precise definitions of what POSIX -matching actually means have been formalised -\cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}. Such a -definition has also been given by Sulzmann and Lu \cite{Sulzmann2014}, -but the corresponding correctness proof turned out to be faulty -\cite{AusafDyckhoffUrban2016}. Roughly, POSIX matching means matching -the longest initial substring. In the case of a tie, the initial -sub-match is chosen according to some priorities attached to the regular -expressions (e.g.~keywords have a higher priority than identifiers). -This sounds rather simple, but according to Grathwohl et al \cite[Page -36]{CrashCourse2014} this is not the case. They wrote: - -\begin{quote} -\it{}``The POSIX strategy is more complicated than the greedy because of -the dependence on information about the length of matched strings in the -various subexpressions.'' -\end{quote} - -\noindent -This is also supported by evidence collected by Kuklewicz -\cite{Kuklewicz} who noticed that a number of POSIX regular expression -matchers calculate incorrect results. - -Our focus in this project is on an algorithm introduced by Sulzmann and -Lu in 2014 for regular expression matching according to the POSIX -strategy \cite{Sulzmann2014}. Their algorithm is based on an older -algorithm by Brzozowski from 1964 where he introduced the notion of -derivatives of regular expressions~\cite{Brzozowski1964}. We shall -briefly explain this algorithm next. - -\section{The Algorithm by Brzozowski based on Derivatives of Regular -Expressions} - -Suppose (basic) regular expressions are given by the following grammar: -\[ r ::= \ZERO \mid \ONE - \mid c - \mid r_1 \cdot r_2 - \mid r_1 + r_2 - \mid r^* -\] - -\noindent -The intended meaning of the constructors is as follows: $\ZERO$ -cannot match any string, $\ONE$ can match the empty string, the -character regular expression $c$ can match the character $c$, and so -on. - -The ingenious contribution by Brzozowski is the notion of -\emph{derivatives} of regular expressions. The idea behind this -notion is as follows: suppose a regular expression $r$ can match a -string of the form $c\!::\! s$ (that is a list of characters starting -with $c$), what does the regular expression look like that can match -just $s$? Brzozowski gave a neat answer to this question. He started -with the definition of $nullable$: -\begin{center} - \begin{tabular}{lcl} - $\nullable(\ZERO)$ & $\dn$ & $\mathit{false}$ \\ - $\nullable(\ONE)$ & $\dn$ & $\mathit{true}$ \\ - $\nullable(c)$ & $\dn$ & $\mathit{false}$ \\ - $\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\ - $\nullable(r_1\cdot r_2)$ & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\ - $\nullable(r^*)$ & $\dn$ & $\mathit{true}$ \\ - \end{tabular} - \end{center} -This function simply tests whether the empty string is in $L(r)$. -He then defined -the following operation on regular expressions, written -$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$): - -\begin{center} -\begin{tabular}{lcl} - $\ZERO \backslash c$ & $\dn$ & $\ZERO$\\ - $\ONE \backslash c$ & $\dn$ & $\ZERO$\\ - $d \backslash c$ & $\dn$ & - $\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\ -$(r_1 + r_2)\backslash c$ & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\ -$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\ - & & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\ - & & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\ - $(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\ -\end{tabular} -\end{center} - -%Assuming the classic notion of a -%\emph{language} of a regular expression, written $L(\_)$, t - -\noindent -The main property of the derivative operation is that - -\begin{center} -$c\!::\!s \in L(r)$ holds -if and only if $s \in L(r\backslash c)$. -\end{center} - -\noindent -For us the main advantage is that derivatives can be -straightforwardly implemented in any functional programming language, -and are easily definable and reasoned about in theorem provers---the -definitions just consist of inductive datatypes and simple recursive -functions. Moreover, the notion of derivatives can be easily -generalised to cover extended regular expression constructors such as -the not-regular expression, written $\neg\,r$, or bounded repetitions -(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so -straightforwardly realised within the classic automata approach. -For the moment however, we focus only on the usual basic regular expressions. - - -Now if we want to find out whether a string $s$ matches with a regular -expression $r$, we can build the derivatives of $r$ w.r.t.\ (in succession) -all the characters of the string $s$. Finally, test whether the -resulting regular expression can match the empty string. If yes, then -$r$ matches $s$, and no in the negative case. To implement this idea -we can generalise the derivative operation to strings like this: - -\begin{center} -\begin{tabular}{lcl} -$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\ -$r \backslash [\,] $ & $\dn$ & $r$ -\end{tabular} -\end{center} - -\noindent -and then define as regular-expression matching algorithm: -\[ -match\;s\;r \;\dn\; nullable(r\backslash s) -\] - -\noindent -This algorithm looks graphically as follows: -\begin{equation}\label{graph:*} -\begin{tikzcd} -r_0 \arrow[r, "\backslash c_0"] & r_1 \arrow[r, "\backslash c_1"] & r_2 \arrow[r, dashed] & r_n \arrow[r,"\textit{nullable}?"] & \;\textrm{YES}/\textrm{NO} -\end{tikzcd} -\end{equation} - -\noindent -where we start with a regular expression $r_0$, build successive -derivatives until we exhaust the string and then use \textit{nullable} -to test whether the result can match the empty string. It can be -relatively easily shown that this matcher is correct (that is given -an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$). - - -\section{Values and the Algorithm by Sulzmann and Lu} - -One limitation of Brzozowski's algorithm is that it only produces a -YES/NO answer for whether a string is being matched by a regular -expression. Sulzmann and Lu~\cite{Sulzmann2014} extended this algorithm -to allow generation of an actual matching, called a \emph{value} or -sometimes also \emph{lexical value}. These values and regular -expressions correspond to each other as illustrated in the following -table: - - -\begin{center} - \begin{tabular}{c@{\hspace{20mm}}c} - \begin{tabular}{@{}rrl@{}} - \multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\ - $r$ & $::=$ & $\ZERO$\\ - & $\mid$ & $\ONE$ \\ - & $\mid$ & $c$ \\ - & $\mid$ & $r_1 \cdot r_2$\\ - & $\mid$ & $r_1 + r_2$ \\ - \\ - & $\mid$ & $r^*$ \\ - \end{tabular} - & - \begin{tabular}{@{\hspace{0mm}}rrl@{}} - \multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\ - $v$ & $::=$ & \\ - & & $\Empty$ \\ - & $\mid$ & $\Char(c)$ \\ - & $\mid$ & $\Seq\,v_1\, v_2$\\ - & $\mid$ & $\Left(v)$ \\ - & $\mid$ & $\Right(v)$ \\ - & $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\ - \end{tabular} - \end{tabular} -\end{center} - -\noindent -No value corresponds to $\ZERO$; $\Empty$ corresponds to $\ONE$; -$\Char$ to the character regular expression; $\Seq$ to the sequence -regular expression and so on. The idea of values is to encode a kind of -lexical value for how the sub-parts of a regular expression match the -sub-parts of a string. To see this, suppose a \emph{flatten} operation, -written $|v|$ for values. We can use this function to extract the -underlying string of a value $v$. For example, $|\mathit{Seq} \, -(\textit{Char x}) \, (\textit{Char y})|$ is the string $xy$. Using -flatten, we can describe how values encode lexical values: $\Seq\,v_1\, -v_2$ encodes a tree with two children nodes that tells how the string -$|v_1| @ |v_2|$ matches the regex $r_1 \cdot r_2$ whereby $r_1$ matches -the substring $|v_1|$ and, respectively, $r_2$ matches the substring -$|v_2|$. Exactly how these two are matched is contained in the children -nodes $v_1$ and $v_2$ of parent $\textit{Seq}$. - -To give a concrete example of how values work, consider the string $xy$ -and the regular expression $(x + (y + xy))^*$. We can view this regular -expression as a tree and if the string $xy$ is matched by two Star -``iterations'', then the $x$ is matched by the left-most alternative in -this tree and the $y$ by the right-left alternative. This suggests to -record this matching as - -\begin{center} -$\Stars\,[\Left\,(\Char\,x), \Right(\Left(\Char\,y))]$ -\end{center} - -\noindent -where $\Stars \; [\ldots]$ records all the -iterations; and $\Left$, respectively $\Right$, which -alternative is used. The value for -matching $xy$ in a single ``iteration'', i.e.~the POSIX value, -would look as follows - -\begin{center} -$\Stars\,[\Seq\,(\Char\,x)\,(\Char\,y)]$ -\end{center} - -\noindent -where $\Stars$ has only a single-element list for the single iteration -and $\Seq$ indicates that $xy$ is matched by a sequence regular -expression. - -The contribution of Sulzmann and Lu is an extension of Brzozowski's -algorithm by a second phase (the first phase being building successive -derivatives---see \eqref{graph:*}). In this second phase, a POSIX value -is generated in case the regular expression matches the string. -Pictorially, the Sulzmann and Lu algorithm is as follows: - -\begin{ceqn} -\begin{equation}\label{graph:2} -\begin{tikzcd} -r_0 \arrow[r, "\backslash c_0"] \arrow[d] & r_1 \arrow[r, "\backslash c_1"] \arrow[d] & r_2 \arrow[r, dashed] \arrow[d] & r_n \arrow[d, "mkeps" description] \\ -v_0 & v_1 \arrow[l,"inj_{r_0} c_0"] & v_2 \arrow[l, "inj_{r_1} c_1"] & v_n \arrow[l, dashed] -\end{tikzcd} -\end{equation} -\end{ceqn} - -\noindent -For convenience, we shall employ the following notations: the regular -expression we start with is $r_0$, and the given string $s$ is composed -of characters $c_0 c_1 \ldots c_{n-1}$. In the first phase from the -left to right, we build the derivatives $r_1$, $r_2$, \ldots according -to the characters $c_0$, $c_1$ until we exhaust the string and obtain -the derivative $r_n$. We test whether this derivative is -$\textit{nullable}$ or not. If not, we know the string does not match -$r$ and no value needs to be generated. If yes, we start building the -values incrementally by \emph{injecting} back the characters into the -earlier values $v_n, \ldots, v_0$. This is the second phase of the -algorithm from the right to left. For the first value $v_n$, we call the -function $\textit{mkeps}$, which builds the lexical value -for how the empty string has been matched by the (nullable) regular -expression $r_n$. This function is defined as - - \begin{center} - \begin{tabular}{lcl} - $\mkeps(\ONE)$ & $\dn$ & $\Empty$ \\ - $\mkeps(r_{1}+r_{2})$ & $\dn$ - & \textit{if} $\nullable(r_{1})$\\ - & & \textit{then} $\Left(\mkeps(r_{1}))$\\ - & & \textit{else} $\Right(\mkeps(r_{2}))$\\ - $\mkeps(r_1\cdot r_2)$ & $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\ - $mkeps(r^*)$ & $\dn$ & $\Stars\,[]$ - \end{tabular} - \end{center} - - -\noindent There are no cases for $\ZERO$ and $c$, since -these regular expression cannot match the empty string. Note -also that in case of alternatives we give preference to the -regular expression on the left-hand side. This will become -important later on about what value is calculated. - -After the $\mkeps$-call, we inject back the characters one by one in order to build -the lexical value $v_i$ for how the regex $r_i$ matches the string $s_i$ -($s_i = c_i \ldots c_{n-1}$ ) from the previous lexical value $v_{i+1}$. -After injecting back $n$ characters, we get the lexical value for how $r_0$ -matches $s$. For this Sulzmann and Lu defined a function that reverses -the ``chopping off'' of characters during the derivative phase. The -corresponding function is called \emph{injection}, written -$\textit{inj}$; it takes three arguments: the first one is a regular -expression ${r_{i-1}}$, before the character is chopped off, the second -is a character ${c_{i-1}}$, the character we want to inject and the -third argument is the value ${v_i}$, into which one wants to inject the -character (it corresponds to the regular expression after the character -has been chopped off). The result of this function is a new value. The -definition of $\textit{inj}$ is as follows: - -\begin{center} -\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l} - $\textit{inj}\,(c)\,c\,Empty$ & $\dn$ & $Char\,c$\\ - $\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\ - $\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\ - $\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\ - $\textit{inj}\,(r_1 \cdot r_2)\,c\,\Left(Seq(v_1,v_2))$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\ - $\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$ & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\ - $\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$ & $\dn$ & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\ -\end{tabular} -\end{center} - -\noindent This definition is by recursion on the ``shape'' of regular -expressions and values. To understands this definition better consider -the situation when we build the derivative on regular expression $r_{i-1}$. -For this we chop off a character from $r_{i-1}$ to form $r_i$. This leaves a -``hole'' in $r_i$ and its corresponding value $v_i$. -To calculate $v_{i-1}$, we need to -locate where that hole is and fill it. -We can find this location by -comparing $r_{i-1}$ and $v_i$. For instance, if $r_{i-1}$ is of shape -$r_a \cdot r_b$, and $v_i$ is of shape $\Left(Seq(v_1,v_2))$, we know immediately that -% -\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b \,+\, r_b\backslash c,\] - -\noindent -otherwise if $r_a$ is not nullable, -\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b,\] - -\noindent -the value $v_i$ should be $\Seq(\ldots)$, contradicting the fact that -$v_i$ is actually of shape $\Left(\ldots)$. Furthermore, since $v_i$ is of shape -$\Left(\ldots)$ instead of $\Right(\ldots)$, we know that the left -branch of \[ (r_a \cdot r_b)\backslash c = -\bold{\underline{ (r_a\backslash c) \cdot r_b} }\,+\, r_b\backslash c,\](underlined) - is taken instead of the right one. This means $c$ is chopped off -from $r_a$ rather than $r_b$. -We have therefore found out -that the hole will be on $r_a$. So we recursively call $\inj\, -r_a\,c\,v_a$ to fill that hole in $v_a$. After injection, the value -$v_i$ for $r_i = r_a \cdot r_b$ should be $\Seq\,(\inj\,r_a\,c\,v_a)\,v_b$. -Other clauses can be understood in a similar way. - -%\comment{Other word: insight?} -The following example gives an insight of $\textit{inj}$'s effect and -how Sulzmann and Lu's algorithm works as a whole. Suppose we have a -regular expression $((((a+b)+ab)+c)+abc)^*$, and want to match it -against the string $abc$ (when $abc$ is written as a regular expression, -the standard way of expressing it is $a \cdot (b \cdot c)$. But we -usually omit the parentheses and dots here for better readability. This -algorithm returns a POSIX value, which means it will produce the longest -matching. Consequently, it matches the string $abc$ in one star -iteration, using the longest alternative $abc$ in the sub-expression (we shall use $r$ to denote this -sub-expression for conciseness): - -\[((((a+b)+ab)+c)+\underbrace{abc}_r)\] - -\noindent -Before $\textit{inj}$ is called, our lexer first builds derivative using -string $abc$ (we simplified some regular expressions like $\ZERO \cdot -b$ to $\ZERO$ for conciseness; we also omit parentheses if they are -clear from the context): - -%Similarly, we allow -%$\textit{ALT}$ to take a list of regular expressions as an argument -%instead of just 2 operands to reduce the nested depth of -%$\textit{ALT}$ - -\begin{center} -\begin{tabular}{lcl} -$r^*$ & $\xrightarrow{\backslash a}$ & $r_1 = (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r^*$\\ - & $\xrightarrow{\backslash b}$ & $r_2 = (\ZERO+\ZERO+\ONE \cdot \ONE + \ZERO + \ONE \cdot \ONE \cdot c) \cdot r^* +(\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^*$\\ - & $\xrightarrow{\backslash c}$ & $r_3 = ((\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot \ONE) \cdot r^* + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^*) + $\\ - & & $\phantom{r_3 = (} ((\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^* + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^* )$ -\end{tabular} -\end{center} - -\noindent -In case $r_3$ is nullable, we can call $\textit{mkeps}$ -to construct a lexical value for how $r_3$ matched the string $abc$. -This function gives the following value $v_3$: - - -\begin{center} -$\Left(\Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty,\Empty))), \Stars [])))$ -\end{center} -The outer $\Left(\Left(\ldots))$ tells us the leftmost nullable part of $r_3$(underlined): - -\begin{center} - \begin{tabular}{l@{\hspace{2mm}}l} - & $\big(\underline{(\ZERO+\ZERO+\ZERO+ \ZERO+ \ONE \cdot \ONE \cdot \ONE) \cdot r^*} - \;+\; (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^*\big)$ \smallskip\\ - $+$ & $\big((\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^* - \;+\; (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^* \big)$ - \end{tabular} - \end{center} - -\noindent - Note that the leftmost location of term $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot - \ONE) \cdot r^*$ (which corresponds to the initial sub-match $abc$) allows - $\textit{mkeps}$ to pick it up because $\textit{mkeps}$ is defined to always choose the - left one when it is nullable. In the case of this example, $abc$ is - preferred over $a$ or $ab$. This $\Left(\Left(\ldots))$ location is - generated by two applications of the splitting clause - -\begin{center} - $(r_1 \cdot r_2)\backslash c \;\;(when \; r_1 \; nullable) \, = (r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c.$ -\end{center} - -\noindent -By this clause, we put $r_1 \backslash c \cdot r_2 $ at the -$\textit{front}$ and $r_2 \backslash c$ at the $\textit{back}$. This -allows $\textit{mkeps}$ to always pick up among two matches the one with a longer -initial sub-match. Removing the outside $\Left(\Left(...))$, the inside -sub-value - -\begin{center} - $\Seq(\Right(\Seq(\Empty, \Seq(\Empty, \Empty))), \Stars [])$ -\end{center} - -\noindent -tells us how the empty string $[]$ is matched with $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot -\ONE \cdot \ONE) \cdot r^*$. We match $[]$ by a sequence of two nullable regular -expressions. The first one is an alternative, we take the rightmost -alternative---whose language contains the empty string. The second -nullable regular expression is a Kleene star. $\Stars$ tells us how it -generates the nullable regular expression: by 0 iterations to form -$\ONE$. Now $\textit{inj}$ injects characters back and incrementally -builds a lexical value based on $v_3$. Using the value $v_3$, the character -c, and the regular expression $r_2$, we can recover how $r_2$ matched -the string $[c]$ : $\textit{inj} \; r_2 \; c \; v_3$ gives us - \begin{center} - $v_2 = \Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty, c))), \Stars [])),$ - \end{center} -which tells us how $r_2$ matched $[c]$. After this we inject back the character $b$, and get -\begin{center} -$v_1 = \Seq(\Right(\Seq(\Empty, \Seq(b, c))), \Stars [])$ -\end{center} - for how - \begin{center} - $r_1= (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r*$ - \end{center} - matched the string $bc$ before it split into two substrings. - Finally, after injecting character $a$ back to $v_1$, - we get the lexical value tree - \begin{center} - $v_0= \Stars [\Right(\Seq(a, \Seq(b, c)))]$ - \end{center} - for how $r$ matched $abc$. This completes the algorithm. - -%We omit the details of injection function, which is provided by Sulzmann and Lu's paper \cite{Sulzmann2014}. -Readers might have noticed that the lexical value information is actually -already available when doing derivatives. For example, immediately after -the operation $\backslash a$ we know that if we want to match a string -that starts with $a$, we can either take the initial match to be - - \begin{center} -\begin{enumerate} - \item[1)] just $a$ or - \item[2)] string $ab$ or - \item[3)] string $abc$. -\end{enumerate} -\end{center} - -\noindent -In order to differentiate between these choices, we just need to -remember their positions---$a$ is on the left, $ab$ is in the middle , -and $abc$ is on the right. Which of these alternatives is chosen -later does not affect their relative position because the algorithm does -not change this order. If this parsing information can be determined and -does not change because of later derivatives, there is no point in -traversing this information twice. This leads to an optimisation---if we -store the information for lexical values inside the regular expression, -update it when we do derivative on them, and collect the information -when finished with derivatives and call $\textit{mkeps}$ for deciding which -branch is POSIX, we can generate the lexical value in one pass, instead of -doing the rest $n$ injections. This leads to Sulzmann and Lu's novel -idea of using bitcodes in derivatives. - -In the next section, we shall focus on the bitcoded algorithm and the -process of simplification of regular expressions. This is needed in -order to obtain \emph{fast} versions of the Brzozowski's, and Sulzmann -and Lu's algorithms. This is where the PhD-project aims to advance the -state-of-the-art. - - -\section{Simplification of Regular Expressions} - -Using bitcodes to guide parsing is not a novel idea. It was applied to -context free grammars and then adapted by Henglein and Nielson for -efficient regular expression lexing using DFAs~\cite{nielson11bcre}. -Sulzmann and Lu took this idea of bitcodes a step further by integrating -bitcodes into derivatives. The reason why we want to use bitcodes in -this project is that we want to introduce more aggressive simplification -rules in order to keep the size of derivatives small throughout. This is -because the main drawback of building successive derivatives according -to Brzozowski's definition is that they can grow very quickly in size. -This is mainly due to the fact that the derivative operation generates -often ``useless'' $\ZERO$s and $\ONE$s in derivatives. As a result, if -implemented naively both algorithms by Brzozowski and by Sulzmann and Lu -are excruciatingly slow. For example when starting with the regular -expression $(a + aa)^*$ and building 12 successive derivatives -w.r.t.~the character $a$, one obtains a derivative regular expression -with more than 8000 nodes (when viewed as a tree). Operations like -$\textit{der}$ and $\nullable$ need to traverse such trees and -consequently the bigger the size of the derivative the slower the -algorithm. - -Fortunately, one can simplify regular expressions after each derivative -step. Various simplifications of regular expressions are possible, such -as the simplification of $\ZERO + r$, $r + \ZERO$, $\ONE\cdot r$, $r -\cdot \ONE$, and $r + r$ to just $r$. These simplifications do not -affect the answer for whether a regular expression matches a string or -not, but fortunately also do not affect the POSIX strategy of how -regular expressions match strings---although the latter is much harder -to establish. Some initial results in this regard have been -obtained in \cite{AusafDyckhoffUrban2016}. - -Unfortunately, the simplification rules outlined above are not -sufficient to prevent a size explosion in all cases. We -believe a tighter bound can be achieved that prevents an explosion in -\emph{all} cases. Such a tighter bound is suggested by work of Antimirov who -proved that (partial) derivatives can be bound by the number of -characters contained in the initial regular expression -\cite{Antimirov95}. He defined the \emph{partial derivatives} of regular -expressions as follows: - -\begin{center} -\begin{tabular}{lcl} - $\textit{pder} \; c \; \ZERO$ & $\dn$ & $\emptyset$\\ - $\textit{pder} \; c \; \ONE$ & $\dn$ & $\emptyset$ \\ - $\textit{pder} \; c \; d$ & $\dn$ & $\textit{if} \; c \,=\, d \; \{ \ONE \} \; \textit{else} \; \emptyset$ \\ - $\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \; r_2$ \\ - $\textit{pder} \; c \; r_1 \cdot r_2$ & $\dn$ & $\textit{if} \; nullable \; r_1 $\\ - & & $\textit{then} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} \cup pder \; c \; r_2 \;$\\ - & & $\textit{else} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} $ \\ - $\textit{pder} \; c \; r^*$ & $\dn$ & $ \{ r' \cdot r^* \mid r' \in pder \; c \; r \} $ \\ - \end{tabular} - \end{center} - -\noindent -A partial derivative of a regular expression $r$ is essentially a set of -regular expressions that are either $r$'s children expressions or a -concatenation of them. Antimirov has proved a tight bound of the sum of -the size of \emph{all} partial derivatives no matter what the string -looks like. Roughly speaking the size sum will be at most cubic in the -size of the regular expression. - -If we want the size of derivatives in Sulzmann and Lu's algorithm to -stay below this bound, we would need more aggressive simplifications. -Essentially we need to delete useless $\ZERO$s and $\ONE$s, as well as -deleting duplicates whenever possible. For example, the parentheses in -$(a+b) \cdot c + bc$ can be opened up to get $a\cdot c + b \cdot c + b -\cdot c$, and then simplified to just $a \cdot c + b \cdot c$. Another -example is simplifying $(a^*+a) + (a^*+ \ONE) + (a +\ONE)$ to just -$a^*+a+\ONE$. Adding these more aggressive simplification rules helps us -to achieve the same size bound as that of the partial derivatives. - -In order to implement the idea of ``spilling out alternatives'' and to -make them compatible with the $\text{inj}$-mechanism, we use -\emph{bitcodes}. Bits and bitcodes (lists of bits) are just: - -%This allows us to prove a tight -%bound on the size of regular expression during the running time of the -%algorithm if we can establish the connection between our simplification -%rules and partial derivatives. - - %We believe, and have generated test -%data, that a similar bound can be obtained for the derivatives in -%Sulzmann and Lu's algorithm. Let us give some details about this next. - - -\begin{center} - $b ::= S \mid Z \qquad -bs ::= [] \mid b:bs -$ -\end{center} - -\noindent -The $S$ and $Z$ are arbitrary names for the bits in order to avoid -confusion with the regular expressions $\ZERO$ and $\ONE$. Bitcodes (or -bit-lists) can be used to encode values (or incomplete values) in a -compact form. This can be straightforwardly seen in the following -coding function from values to bitcodes: - -\begin{center} -\begin{tabular}{lcl} - $\textit{code}(\Empty)$ & $\dn$ & $[]$\\ - $\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\ - $\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\ - $\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\ - $\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\ - $\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\ - $\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\; - code(\Stars\,vs)$ -\end{tabular} -\end{center} - -\noindent -Here $\textit{code}$ encodes a value into a bitcodes by converting -$\Left$ into $\Z$, $\Right$ into $\S$, the start point of a non-empty -star iteration into $\S$, and the border where a local star terminates -into $\Z$. This coding is lossy, as it throws away the information about -characters, and also does not encode the ``boundary'' between two -sequence values. Moreover, with only the bitcode we cannot even tell -whether the $\S$s and $\Z$s are for $\Left/\Right$ or $\Stars$. The -reason for choosing this compact way of storing information is that the -relatively small size of bits can be easily manipulated and ``moved -around'' in a regular expression. In order to recover values, we will -need the corresponding regular expression as an extra information. This -means the decoding function is defined as: - - -%\begin{definition}[Bitdecoding of Values]\mbox{} -\begin{center} -\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}} - $\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\ - $\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\ - $\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ & - $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\; - (\Left\,v, bs_1)$\\ - $\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ & - $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\; - (\Right\,v, bs_1)$\\ - $\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ & - $\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\ - & & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\ - & & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\ - $\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\ - $\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ & - $\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\ - & & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\ - & & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\ - - $\textit{decode}\,bs\,r$ & $\dn$ & - $\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\ - & & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\; - \textit{else}\;\textit{None}$ -\end{tabular} -\end{center} -%\end{definition} - -Sulzmann and Lu's integrated the bitcodes into regular expressions to -create annotated regular expressions \cite{Sulzmann2014}. -\emph{Annotated regular expressions} are defined by the following -grammar:%\comment{ALTS should have an $as$ in the definitions, not just $a_1$ and $a_2$} - -\begin{center} -\begin{tabular}{lcl} - $\textit{a}$ & $::=$ & $\textit{ZERO}$\\ - & $\mid$ & $\textit{ONE}\;\;bs$\\ - & $\mid$ & $\textit{CHAR}\;\;bs\,c$\\ - & $\mid$ & $\textit{ALTS}\;\;bs\,as$\\ - & $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\ - & $\mid$ & $\textit{STAR}\;\;bs\,a$ -\end{tabular} -\end{center} -%(in \textit{ALTS}) - -\noindent -where $bs$ stands for bitcodes, $a$ for $\bold{a}$nnotated regular -expressions and $as$ for a list of annotated regular expressions. -The alternative constructor($\textit{ALTS}$) has been generalized to -accept a list of annotated regular expressions rather than just 2. -We will show that these bitcodes encode information about -the (POSIX) value that should be generated by the Sulzmann and Lu -algorithm. - - -To do lexing using annotated regular expressions, we shall first -transform the usual (un-annotated) regular expressions into annotated -regular expressions. This operation is called \emph{internalisation} and -defined as follows: - -%\begin{definition} -\begin{center} -\begin{tabular}{lcl} - $(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\ - $(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\ - $(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\ - $(r_1 + r_2)^\uparrow$ & $\dn$ & - $\textit{ALTS}\;[]\,List((\textit{fuse}\,[\Z]\,r_1^\uparrow),\, - (\textit{fuse}\,[\S]\,r_2^\uparrow))$\\ - $(r_1\cdot r_2)^\uparrow$ & $\dn$ & - $\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\ - $(r^*)^\uparrow$ & $\dn$ & - $\textit{STAR}\;[]\,r^\uparrow$\\ -\end{tabular} -\end{center} -%\end{definition} - -\noindent -We use up arrows here to indicate that the basic un-annotated regular -expressions are ``lifted up'' into something slightly more complex. In the -fourth clause, $\textit{fuse}$ is an auxiliary function that helps to -attach bits to the front of an annotated regular expression. Its -definition is as follows: - -\begin{center} -\begin{tabular}{lcl} - $\textit{fuse}\;bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\ - $\textit{fuse}\;bs\,(\textit{ONE}\,bs')$ & $\dn$ & - $\textit{ONE}\,(bs\,@\,bs')$\\ - $\textit{fuse}\;bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ & - $\textit{CHAR}\,(bs\,@\,bs')\,c$\\ - $\textit{fuse}\;bs\,(\textit{ALTS}\,bs'\,as)$ & $\dn$ & - $\textit{ALTS}\,(bs\,@\,bs')\,as$\\ - $\textit{fuse}\;bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ & - $\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\ - $\textit{fuse}\;bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ & - $\textit{STAR}\,(bs\,@\,bs')\,a$ -\end{tabular} -\end{center} - -\noindent -After internalising the regular expression, we perform successive -derivative operations on the annotated regular expressions. This -derivative operation is the same as what we had previously for the -basic regular expressions, except that we beed to take care of -the bitcodes: - - %\begin{definition}{bder} -\begin{center} - \begin{tabular}{@{}lcl@{}} - $(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ - $(\textit{ONE}\;bs)\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\ - $(\textit{CHAR}\;bs\,d)\,\backslash c$ & $\dn$ & - $\textit{if}\;c=d\; \;\textit{then}\; - \textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\ - $(\textit{ALTS}\;bs\,as)\,\backslash c$ & $\dn$ & - $\textit{ALTS}\;bs\,(as.map(\backslash c))$\\ - $(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ & - $\textit{if}\;\textit{bnullable}\,a_1$\\ - & &$\textit{then}\;\textit{ALTS}\,bs\,List((\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\ - & &$\phantom{\textit{then}\;\textit{ALTS}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\ - & &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\,\backslash c)\,a_2$\\ - $(\textit{STAR}\,bs\,a)\,\backslash c$ & $\dn$ & - $\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\,\backslash c))\, - (\textit{STAR}\,[]\,r)$ -\end{tabular} -\end{center} -%\end{definition} - -\noindent -For instance, when we unfold $\textit{STAR} \; bs \; a$ into a sequence, -we need to attach an additional bit $Z$ to the front of $r \backslash c$ -to indicate that there is one more star iteration. Also the $SEQ$ clause -is more subtle---when $a_1$ is $\textit{bnullable}$ (here -\textit{bnullable} is exactly the same as $\textit{nullable}$, except -that it is for annotated regular expressions, therefore we omit the -definition). Assume that $bmkeps$ correctly extracts the bitcode for how -$a_1$ matches the string prior to character $c$ (more on this later), -then the right branch of $ALTS$, which is $fuse \; bmkeps \; a_1 (a_2 -\backslash c)$ will collapse the regular expression $a_1$(as it has -already been fully matched) and store the parsing information at the -head of the regular expression $a_2 \backslash c$ by fusing to it. The -bitsequence $bs$, which was initially attached to the head of $SEQ$, has -now been elevated to the top-level of $ALTS$, as this information will be -needed whichever way the $SEQ$ is matched---no matter whether $c$ belongs -to $a_1$ or $ a_2$. After building these derivatives and maintaining all -the lexing information, we complete the lexing by collecting the -bitcodes using a generalised version of the $\textit{mkeps}$ function -for annotated regular expressions, called $\textit{bmkeps}$: - - -%\begin{definition}[\textit{bmkeps}]\mbox{} -\begin{center} -\begin{tabular}{lcl} - $\textit{bmkeps}\,(\textit{ONE}\;bs)$ & $\dn$ & $bs$\\ - $\textit{bmkeps}\,(\textit{ALTS}\;bs\,a::as)$ & $\dn$ & - $\textit{if}\;\textit{bnullable}\,a$\\ - & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\ - & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(\textit{ALTS}\;bs\,as)$\\ - $\textit{bmkeps}\,(\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & - $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\ - $\textit{bmkeps}\,(\textit{STAR}\;bs\,a)$ & $\dn$ & - $bs \,@\, [\S]$ -\end{tabular} -\end{center} -%\end{definition} - -\noindent -This function completes the value information by travelling along the -path of the regular expression that corresponds to a POSIX value and -collecting all the bitcodes, and using $S$ to indicate the end of star -iterations. If we take the bitcodes produced by $\textit{bmkeps}$ and -decode them, we get the value we expect. The corresponding lexing -algorithm looks as follows: - -\begin{center} -\begin{tabular}{lcl} - $\textit{blexer}\;r\,s$ & $\dn$ & - $\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\ - & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\ - & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ - & & $\;\;\textit{else}\;\textit{None}$ -\end{tabular} -\end{center} - -\noindent -In this definition $\_\backslash s$ is the generalisation of the derivative -operation from characters to strings (just like the derivatives for un-annotated -regular expressions). - -The main point of the bitcodes and annotated regular expressions is that -we can apply rather aggressive (in terms of size) simplification rules -in order to keep derivatives small. We have developed such -``aggressive'' simplification rules and generated test data that show -that the expected bound can be achieved. Obviously we could only -partially cover the search space as there are infinitely many regular -expressions and strings. - -One modification we introduced is to allow a list of annotated regular -expressions in the \textit{ALTS} constructor. This allows us to not just -delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but -also unnecessary ``copies'' of regular expressions (very similar to -simplifying $r + r$ to just $r$, but in a more general setting). Another -modification is that we use simplification rules inspired by Antimirov's -work on partial derivatives. They maintain the idea that only the first -``copy'' of a regular expression in an alternative contributes to the -calculation of a POSIX value. All subsequent copies can be pruned away from -the regular expression. A recursive definition of our simplification function -that looks somewhat similar to our Scala code is given below: -%\comment{Use $\ZERO$, $\ONE$ and so on. -%Is it $ALTS$ or $ALTS$?}\\ - -\begin{center} - \begin{tabular}{@{}lcl@{}} - - $\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\ - &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\ - &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\ - &&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\ - &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\ - &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\ - - $\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\ - &&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\ - &&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\ - &&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\ - - $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$ -\end{tabular} -\end{center} - -\noindent -The simplification does a pattern matching on the regular expression. -When it detected that the regular expression is an alternative or -sequence, it will try to simplify its children regular expressions -recursively and then see if one of the children turn into $\ZERO$ or -$\ONE$, which might trigger further simplification at the current level. -The most involved part is the $\textit{ALTS}$ clause, where we use two -auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested -$\textit{ALTS}$ and reduce as many duplicates as possible. Function -$\textit{distinct}$ keeps the first occurring copy only and remove all later ones -when detected duplicates. Function $\textit{flatten}$ opens up nested \textit{ALTS}. -Its recursive definition is given below: - - \begin{center} - \begin{tabular}{@{}lcl@{}} - $\textit{flatten} \; (\textit{ALTS}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \; - (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\ - $\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \; as' $ \\ - $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise) -\end{tabular} -\end{center} - -\noindent -Here $\textit{flatten}$ behaves like the traditional functional programming flatten -function, except that it also removes $\ZERO$s. Or in terms of regular expressions, it -removes parentheses, for example changing $a+(b+c)$ into $a+b+c$. - -Suppose we apply simplification after each derivative step, and view -these two operations as an atomic one: $a \backslash_{simp}\,c \dn -\textit{simp}(a \backslash c)$. Then we can use the previous natural -extension from derivative w.r.t.~character to derivative -w.r.t.~string:%\comment{simp in the [] case?} - -\begin{center} -\begin{tabular}{lcl} -$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp}\, c) \backslash_{simp}\, s$ \\ -$r \backslash_{simp} [\,] $ & $\dn$ & $r$ -\end{tabular} -\end{center} - -\noindent -we obtain an optimised version of the algorithm: - - \begin{center} -\begin{tabular}{lcl} - $\textit{blexer\_simp}\;r\,s$ & $\dn$ & - $\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\ - & & $\;\;\textit{if}\; \textit{bnullable}(a)$\\ - & & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\ - & & $\;\;\textit{else}\;\textit{None}$ -\end{tabular} -\end{center} - -\noindent -This algorithm keeps the regular expression size small, for example, -with this simplification our previous $(a + aa)^*$ example's 8000 nodes -will be reduced to just 6 and stays constant, no matter how long the -input string is. - - - -\section{Current Work} - -We are currently engaged in two tasks related to this algorithm. The -first task is proving that our simplification rules actually do not -affect the POSIX value that should be generated by the algorithm -according to the specification of a POSIX value and furthermore obtain a -much tighter bound on the sizes of derivatives. The result is that our -algorithm should be correct and faster on all inputs. The original -blow-up, as observed in JavaScript, Python and Java, would be excluded -from happening in our algorithm. For this proof we use the theorem prover -Isabelle. Once completed, this result will advance the state-of-the-art: -Sulzmann and Lu wrote in their paper~\cite{Sulzmann2014} about the -bitcoded ``incremental parsing method'' (that is the lexing algorithm -outlined in this section): - -\begin{quote}\it - ``Correctness Claim: We further claim that the incremental parsing - method in Figure~5 in combination with the simplification steps in - Figure 6 yields POSIX parse tree [our lexical values]. We have tested this claim - extensively by using the method in Figure~3 as a reference but yet - have to work out all proof details.'' -\end{quote} - -\noindent -We like to settle this correctness claim. It is relatively -straightforward to establish that after one simplification step, the part of a -nullable derivative that corresponds to a POSIX value remains intact and can -still be collected, in other words, we can show that -%\comment{Double-check....I -%think this is not the case} -%\comment{If i remember correctly, you have proved this lemma. -%I feel this is indeed not true because you might place arbitrary -%bits on the regex r, however if this is the case, did i remember wrongly that -%you proved something like simplification does not affect $\textit{bmkeps}$ results? -%Anyway, i have amended this a little bit so it does not allow arbitrary bits attached -%to a regex. Maybe it works now.} - -\begin{center} - $\textit{bmkeps} \; a = \textit{bmkeps} \; \textit{bsimp} \; a\;($\textit{provided}$ \; a\; is \; \textit{bnullable} )$ -\end{center} - -\noindent -as this basically comes down to proving actions like removing the -additional $r$ in $r+r$ does not delete important POSIX information in -a regular expression. The hard part of this proof is to establish that - -\begin{center} - $ \textit{blexer}\_{simp}(r, \; s) = \textit{blexer}(r, \; s)$ -\end{center} -%comment{This is not true either...look at the definion blexer/blexer-simp} - -\noindent That is, if we do derivative on regular expression $r$ and then -simplify it, and repeat this process until we exhaust the string, we get a -regular expression $r''$($\textit{LHS}$) that provides the POSIX matching -information, which is exactly the same as the result $r'$($\textit{RHS}$ of the -normal derivative algorithm that only does derivative repeatedly and has no -simplification at all. This might seem at first glance very unintuitive, as -the $r'$ could be exponentially larger than $r''$, but can be explained in the -following way: we are pruning away the possible matches that are not POSIX. -Since there could be exponentially many -non-POSIX matchings and only 1 POSIX matching, it -is understandable that our $r''$ can be a lot smaller. we can still provide -the same POSIX value if there is one. This is not as straightforward as the -previous proposition, as the two regular expressions $r'$ and $r''$ might have -become very different. The crucial point is to find the -$\textit{POSIX}$ information of a regular expression and how it is modified, -augmented and propagated -during simplification in parallel with the regular expression that -has not been simplified in the subsequent derivative operations. To aid this, -we use the helper function retrieve described by Sulzmann and Lu: -\begin{center} -\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}} - $\textit{retrieve}\,(\textit{ONE}\,bs)\,\Empty$ & $\dn$ & $bs$\\ - $\textit{retrieve}\,(\textit{CHAR}\,bs\,c)\,(\Char\,d)$ & $\dn$ & $bs$\\ - $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Left\,v)$ & $\dn$ & - $bs \,@\, \textit{retrieve}\,a\,v$\\ - $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Right\,v)$ & $\dn$ & - $bs \,@\, \textit{retrieve}\,(\textit{ALTS}\,bs\,as)\,v$\\ - $\textit{retrieve}\,(\textit{SEQ}\,bs\,a_1\,a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ & - $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\ - $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,[])$ & $\dn$ & - $bs \,@\, [\S]$\\ - $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\ - \multicolumn{3}{l}{ - \hspace{3cm}$bs \,@\, [\Z] \,@\, \textit{retrieve}\,a\,v\,@\, - \textit{retrieve}\,(\textit{STAR}\,[]\,a)\,(\Stars\,vs)$}\\ -\end{tabular} -\end{center} -%\comment{Did not read further}\\ -This function assembles the bitcode -%that corresponds to a lexical value for how -%the current derivative matches the suffix of the string(the characters that -%have not yet appeared, but will appear as the successive derivatives go on. -%How do we get this "future" information? By the value $v$, which is -%computed by a pass of the algorithm that uses -%$inj$ as described in the previous section). -using information from both the derivative regular expression and the -value. Sulzmann and Lu poroposed this function, but did not prove -anything about it. Ausaf and Urban used it to connect the bitcoded -algorithm to the older algorithm by the following equation: - - \begin{center} $inj \;a\; c \; v = \textit{decode} \; (\textit{retrieve}\; - (r^\uparrow)\backslash_{simp} \,c)\,v)$ - \end{center} - -\noindent -whereby $r^\uparrow$ stands for the internalised version of $r$. Ausaf -and Urban also used this fact to prove the correctness of bitcoded -algorithm without simplification. Our purpose of using this, however, -is to establish - -\begin{center} -$ \textit{retrieve} \; -a \; v \;=\; \textit{retrieve} \; (\textit{simp}\,a) \; v'.$ -\end{center} -The idea is that using $v'$, a simplified version of $v$ that had gone -through the same simplification step as $\textit{simp}(a)$, we are able -to extract the bitcode that gives the same parsing information as the -unsimplified one. However, we noticed that constructing such a $v'$ -from $v$ is not so straightforward. The point of this is that we might -be able to finally bridge the gap by proving - -\begin{center} -$\textit{retrieve} \; (r^\uparrow \backslash s) \; v = \;\textit{retrieve} \; -(\textit{simp}(r^\uparrow) \backslash s) \; v'$ -\end{center} - -\noindent -and subsequently - -\begin{center} -$\textit{retrieve} \; (r^\uparrow \backslash s) \; v\; = \; \textit{retrieve} \; -(r^\uparrow \backslash_{simp} \, s) \; v'$. -\end{center} - -\noindent -The $\textit{LHS}$ of the above equation is the bitcode we want. This -would prove that our simplified version of regular expression still -contains all the bitcodes needed. The task here is to find a way to -compute the correct $v'$. - -The second task is to speed up the more aggressive simplification. Currently -it is slower than the original naive simplification by Ausaf and Urban (the -naive version as implemented by Ausaf and Urban of course can ``explode'' in -some cases). It is therefore not surprising that the speed is also much slower -than regular expression engines in popular programming languages such as Java -and Python on most inputs that are linear. For example, just by rewriting the -example regular expression in the beginning of this report $(a^*)^*\,b$ into -$a^*\,b$ would eliminate the ambiguity in the matching and make the time -for matching linear with respect to the input string size. This allows the -DFA approach to become blindingly fast, and dwarf the speed of our current -implementation. For example, here is a comparison of Java regex engine -and our implementation on this example. - -\begin{center} -\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}} -\begin{tikzpicture} -\begin{axis}[ - xlabel={$n*1000$}, - x label style={at={(1.05,-0.05)}}, - ylabel={time in secs}, - enlargelimits=false, - xtick={0,5,...,30}, - xmax=33, - ymax=9, - scaled ticks=true, - axis lines=left, - width=5cm, - height=4cm, - legend entries={Bitcoded Algorithm}, - legend pos=north west, - legend cell align=left] -\addplot[red,mark=*, mark options={fill=white}] table {bad-scala.data}; -\end{axis} -\end{tikzpicture} - & -\begin{tikzpicture} -\begin{axis}[ - xlabel={$n*1000$}, - x label style={at={(1.05,-0.05)}}, - %ylabel={time in secs}, - enlargelimits=false, - xtick={0,5,...,30}, - xmax=33, - ymax=9, - scaled ticks=false, - axis lines=left, - width=5cm, - height=4cm, - legend entries={Java}, - legend pos=north west, - legend cell align=left] -\addplot[cyan,mark=*, mark options={fill=white}] table {good-java.data}; -\end{axis} -\end{tikzpicture}\\ -\multicolumn{3}{c}{Graphs: Runtime for matching $a^*\,b$ with strings - of the form $\underbrace{aa..a}_{n}$.} -\end{tabular} -\end{center} - - -Java regex engine can match string of thousands of characters in a few milliseconds, -whereas our current algorithm gets excruciatingly slow on input of this size. -The running time in theory is linear, however it does not appear to be the -case in an actual implementation. So it needs to be explored how to -make our algorithm faster on all inputs. It could be the recursive calls that are -needed to manipulate bits that are causing the slow down. A possible solution -is to write recursive functions into tail-recusive form. -Another possibility would be to explore -again the connection to DFAs to speed up the algorithm on -subcalls that are small enough. This is very much work in progress. - -\section{Conclusion} - -In this PhD-project we are interested in fast algorithms for regular -expression matching. While this seems to be a ``settled'' area, in -fact interesting research questions are popping up as soon as one steps -outside the classic automata theory (for example in terms of what kind -of regular expressions are supported). The reason why it is -interesting for us to look at the derivative approach introduced by -Brzozowski for regular expression matching, and then much further -developed by Sulzmann and Lu, is that derivatives can elegantly deal -with some of the regular expressions that are of interest in ``real -life''. This includes the not-regular expression, written $\neg\,r$ -(that is all strings that are not recognised by $r$), but also bounded -regular expressions such as $r^{\{n\}}$ and $r^{\{n..m\}}$). There is -also hope that the derivatives can provide another angle for how to -deal more efficiently with back-references, which are one of the -reasons why regular expression engines in JavaScript, Python and Java -choose to not implement the classic automata approach of transforming -regular expressions into NFAs and then DFAs---because we simply do not -know how such back-references can be represented by DFAs. -We also plan to implement the bitcoded algorithm -in some imperative language like C to see if the inefficiency of the -Scala implementation -is language specific. To make this research more comprehensive we also plan -to contrast our (faster) version of bitcoded algorithm with the -Symbolic Regex Matcher, the RE2, the Rust Regex Engine, and the static -analysis approach by implementing them in the same language and then compare -their performance. - - -\section{discarded} -haha -\bibliographystyle{plain} -\bibliography{root,regex_time_complexity} - - - -\end{document} diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/bad-scala.data --- a/ChengsongPhdThesis/bad-scala.data Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -%% LaTeX2e file `bad-scala.data' -%% generated by the `filecontents' environment -%% from source `mentoringMeeting' on 2022/02/22. -%% -1 0.048028 -2 0.126308 -3 0.169670 -4 0.264180 -5 0.384297 -6 0.612785 -7 0.817211 -8 1.089386 -9 1.363222 -10 1.644981 -11 1.987046 -12 2.416012 -13 2.920956 -14 3.398956 -15 3.739649 -16 4.329977 -17 4.932896 -18 5.633909 -19 6.436107 -20 6.927233 -21 7.441163 -22 8.242139 -23 8.901034 -24 9.680487 -25 10.496226 -26 11.385733 -27 12.247613 -28 13.990491 -29 14.245804 -30 15.206283 diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/bitcoded_sulzmann.png Binary file ChengsongPhdThesis/bitcoded_sulzmann.png has changed diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/cc-by.pdf Binary file ChengsongPhdThesis/cc-by.pdf has changed diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/data.sty --- a/ChengsongPhdThesis/data.sty Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,123 +0,0 @@ -% The data files, written on the first run. - - -\begin{filecontents}{re-python2.data} -1 0.033 -5 0.036 -10 0.034 -15 0.036 -18 0.059 -19 0.084 -20 0.141 -21 0.248 -22 0.485 -23 0.878 -24 1.71 -25 3.40 -26 7.08 -27 14.12 -28 26.69 -\end{filecontents} - - -% JavaScript, example (a*)*b -\begin{filecontents}{re-js.data} -5 0.061 -10 0.061 -15 0.061 -20 0.070 -23 0.131 -25 0.308 -26 0.564 -28 1.994 -30 7.648 -31 15.881 -32 32.190 -\end{filecontents} - -% Java 8, example (a*)*b -\begin{filecontents}{re-java.data} -5 0.00298 -10 0.00418 -15 0.00996 -16 0.01710 -17 0.03492 -18 0.03303 -19 0.05084 -20 0.10177 -21 0.19960 -22 0.41159 -23 0.82234 -24 1.70251 -25 3.36112 -26 6.63998 -27 13.35120 -28 29.81185 -\end{filecontents} - -% Java, example (a*)b -\begin{filecontents}{good-java.data} -1 1.5633E-5 -2 1.299E-5 -3 1.1451E-5 -4 1.5846E-5 -5 1.9934E-5 -6 2.174E-5 -7 2.7669E-5 -8 2.8657E-5 -9 2.8161E-5 -10 2.8729E-5 -11 3.5367E-5 -12 3.701E-5 -13 3.84E-5 -14 4.1329E-5 -15 4.8116E-5 -16 5.3597E-5 -17 4.6792E-5 -18 5.8618E-5 -19 6.2078E-5 -20 6.4702E-5 -21 6.1464E-5 -22 6.4693E-5 -23 6.1667E-5 -24 7.1466E-5 -25 7.8089E-5 -26 7.4661E-5 -27 7.5628E-5 -28 8.9169E-5 -29 9.4161E-5 -30 9.8494E-5 -\end{filecontents} - -\begin{filecontents}{bad-scala.data} -1 0.048028 -2 0.126308 -3 0.169670 -4 0.264180 -5 0.384297 -6 0.612785 -7 0.817211 -8 1.089386 -9 1.363222 -10 1.644981 -11 1.987046 -12 2.416012 -13 2.920956 -14 3.398956 -15 3.739649 -16 4.329977 -17 4.932896 -18 5.633909 -19 6.436107 -20 6.927233 -21 7.441163 -22 8.242139 -23 8.901034 -24 9.680487 -25 10.496226 -26 11.385733 -27 12.247613 -28 13.990491 -29 14.245804 -30 15.206283 -\end{filecontents} \ No newline at end of file diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/good-java.data --- a/ChengsongPhdThesis/good-java.data Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -%% LaTeX2e file `good-java.data' -%% generated by the `filecontents' environment -%% from source `mentoringMeeting' on 2022/02/22. -%% -1 1.5633E-5 -2 1.299E-5 -3 1.1451E-5 -4 1.5846E-5 -5 1.9934E-5 -6 2.174E-5 -7 2.7669E-5 -8 2.8657E-5 -9 2.8161E-5 -10 2.8729E-5 -11 3.5367E-5 -12 3.701E-5 -13 3.84E-5 -14 4.1329E-5 -15 4.8116E-5 -16 5.3597E-5 -17 4.6792E-5 -18 5.8618E-5 -19 6.2078E-5 -20 6.4702E-5 -21 6.1464E-5 -22 6.4693E-5 -23 6.1667E-5 -24 7.1466E-5 -25 7.8089E-5 -26 7.4661E-5 -27 7.5628E-5 -28 8.9169E-5 -29 9.4161E-5 -30 9.8494E-5 diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/graphic.sty --- a/ChengsongPhdThesis/graphic.sty Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -\usepackage{tikz} -%\usepackage{pgf} -%\usetikzlibrary{positioning} -%\usetikzlibrary{calc} -%\usetikzlibrary{automata} -%\usetikzlibrary{arrows} -%\usetikzlibrary{backgrounds} -%\usetikzlibrary{fit} -%\usepackage{tikz-qtree} -\usepackage{pgfplots} - -%\pgfplotsset{compat=1.15} diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/lipics-logo-bw.pdf Binary file ChengsongPhdThesis/lipics-logo-bw.pdf has changed diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/lipics.cls --- a/ChengsongPhdThesis/lipics.cls Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,646 +0,0 @@ -%% -%% This is file `lipics.cls', -%% generated with the docstrip utility. -%% -%% The original source files were: -%% -%% lipics.dtx (with options: `class') -%% -%% ----------------------------------------------------------------- -%% Author: le-tex publishing services -%% -%% This file is part of the lipics package for preparing -%% LIPICS articles. -%% -%% Copyright (C) 2010 Schloss Dagstuhl -%% ----------------------------------------------------------------- -\NeedsTeXFormat{LaTeX2e}[2005/12/01] -\ProvidesClass{lipics} - [2010/09/27 v1.1 LIPIcs articles] -\emergencystretch1em -\advance\hoffset-1in -\advance\voffset-1in -\advance\hoffset2.95mm -\newif\if@nobotseplist \@nobotseplistfalse -\def\@endparenv{% - \addpenalty\@endparpenalty\if@nobotseplist\else\addvspace\@topsepadd\fi\@endpetrue} -\def\@doendpe{% - \@endpetrue - \def\par{\@restorepar - \everypar{}% - \par - \if@nobotseplist - \addvspace\topsep - \addvspace\partopsep - \global\@nobotseplistfalse - \fi - \@endpefalse}% - \everypar{{\setbox\z@\lastbox}% - \everypar{}% - \if@nobotseplist\global\@nobotseplistfalse\fi - \@endpefalse}} -\def\enumerate{% - \ifnum \@enumdepth >\thr@@\@toodeep\else - \advance\@enumdepth\@ne - \edef\@enumctr{enum\romannumeral\the\@enumdepth}% - \expandafter - \list - \csname label\@enumctr\endcsname - {\advance\partopsep\topsep - \topsep\z@\@plus\p@ - \ifnum\@listdepth=\@ne - \labelsep0.72em - \else - \ifnum\@listdepth=\tw@ - \labelsep0.3em - \else - \labelsep0.5em - \fi - \fi - \usecounter\@enumctr\def\makelabel##1{\hss\llap{##1}}}% - \fi} -\def\endenumerate{\ifnum\@listdepth=\@ne\global\@nobotseplisttrue\fi\endlist} -\def\itemize{% - \ifnum \@itemdepth >\thr@@\@toodeep\else - \advance\@itemdepth\@ne - \edef\@itemitem{labelitem\romannumeral\the\@itemdepth}% - \expandafter - \list - \csname\@itemitem\endcsname - {\advance\partopsep\topsep - \topsep\z@\@plus\p@ - \ifnum\@listdepth=\@ne - \labelsep0.83em - \else - \ifnum\@listdepth=\tw@ - \labelsep0.75em - \else - \labelsep0.5em - \fi - \fi - \def\makelabel##1{\hss\llap{##1}}}% - \fi} -\def\enditemize{\ifnum\@listdepth=\@ne\global\@nobotseplisttrue\fi\endlist} -\def\@sect#1#2#3#4#5#6[#7]#8{% - \ifnum #2>\c@secnumdepth - \let\@svsec\@empty - \else - \refstepcounter{#1}% - \protected@edef\@svsec{\@seccntformat{#1}\relax}% - \fi - \@tempskipa #5\relax - \ifdim \@tempskipa>\z@ - \begingroup - #6{% - \@hangfrom{\hskip #3\relax - \ifnum #2=1 - \colorbox[rgb]{0.99,0.78,0.07}{\kern0.15em\@svsec\kern0.15em}\quad - \else - \@svsec\quad - \fi}% - \interlinepenalty \@M #8\@@par}% - \endgroup - \csname #1mark\endcsname{#7}% - \addcontentsline{toc}{#1}{% - \ifnum #2>\c@secnumdepth \else - \protect\numberline{\csname the#1\endcsname}% - \fi - #7}% - \else - \def\@svsechd{% - #6{\hskip #3\relax - \@svsec #8}% - \csname #1mark\endcsname{#7}% - \addcontentsline{toc}{#1}{% - \ifnum #2>\c@secnumdepth \else - \protect\numberline{\csname the#1\endcsname}% - \fi - #7}}% - \fi - \@xsect{#5}} -\def\@seccntformat#1{\csname the#1\endcsname} -\def\@biblabel#1{\textcolor{darkgray}{\sffamily\bfseries#1}} -\def\copyrightline{% - \ifx\@serieslogo\@empty - \else - \setbox\@tempboxa\hbox{\includegraphics[height=42\p@]{\@serieslogo}}% - \rlap{\hspace\textwidth\hspace{-\wd\@tempboxa}\hspace{\z@}% - \vtop to\z@{\vskip-0mm\unhbox\@tempboxa\vss}}% - \fi - \scriptsize - \vtop{\hsize\textwidth - \nobreakspace\\ - \@Copyright - \ifx\@Event\@empty\else\@Event.\\\fi - \ifx\@Editors\@empty\else - \@Eds: \@Editors - ; pp. \thepage--\pageref{LastPage}% - \\ - \fi - \setbox\@tempboxa\hbox{\includegraphics[height=14\p@,trim=0 15 0 0]{lipics-logo-bw}}% - \hspace*{\wd\@tempboxa}\enskip - \href{http://www.dagstuhl.de/lipics/}% - {Leibniz International Proceedings in Informatics}\\ - \smash{\unhbox\@tempboxa}\enskip - \href{http://www.dagstuhl.de}% - {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik, Dagstuhl Publishing, Germany}}} -\def\ps@plain{\let\@mkboth\@gobbletwo - \let\@oddhead\@empty - \let\@evenhead\@empty - \let\@evenfoot\copyrightline - \let\@oddfoot\copyrightline} -\def\lipics@opterrshort{Option "\CurrentOption" not supported} -\def\lipics@opterrlong{The option "\CurrentOption" from article.cls is not supported by lipics.cls.} -\DeclareOption{a5paper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{b5paper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{legalpaper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{executivepaper}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{landscape}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{10pt}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{11pt}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{12pt}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{oneside}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{twoside}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{titlepage}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{notitlepage}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{onecolumn}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{twocolumn}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{fleqn}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{openbib}{\@latexerr{\lipics@opterrshort}{\lipics@opterrlong}} -\DeclareOption{a4paper}{\PassOptionsToClass{\CurrentOption}{article} - \advance\hoffset-2.95mm - \advance\voffset8.8mm} -\DeclareOption{numberwithinsect}{\let\numberwithinsect\relax} -\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}} -\ProcessOptions -\LoadClass[twoside,notitlepage,fleqn]{article} -\renewcommand\normalsize{% - \@setfontsize\normalsize\@xpt{13}% - \abovedisplayskip 10\p@ \@plus2\p@ \@minus5\p@ - \abovedisplayshortskip \z@ \@plus3\p@ - \belowdisplayshortskip 6\p@ \@plus3\p@ \@minus3\p@ - \belowdisplayskip \abovedisplayskip - \let\@listi\@listI} -\normalsize -\renewcommand\small{% - \@setfontsize\small\@ixpt{11.5}% - \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@ - \abovedisplayshortskip \z@ \@plus2\p@ - \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@ - \def\@listi{\leftmargin\leftmargini - \topsep 4\p@ \@plus2\p@ \@minus2\p@ - \parsep 2\p@ \@plus\p@ \@minus\p@ - \itemsep \parsep}% - \belowdisplayskip \abovedisplayskip -} -\renewcommand\footnotesize{% - \@setfontsize\footnotesize{8.5}{9.5}% - \abovedisplayskip 6\p@ \@plus2\p@ \@minus4\p@ - \abovedisplayshortskip \z@ \@plus\p@ - \belowdisplayshortskip 3\p@ \@plus\p@ \@minus2\p@ - \def\@listi{\leftmargin\leftmargini - \topsep 3\p@ \@plus\p@ \@minus\p@ - \parsep 2\p@ \@plus\p@ \@minus\p@ - \itemsep \parsep}% - \belowdisplayskip \abovedisplayskip -} -\renewcommand\large{\@setfontsize\large{10.5}{13}} -\renewcommand\Large{\@setfontsize\Large{12}{14}} -\setlength\parindent{1.5em} -\setlength\headheight{3mm} -\setlength\headsep {10mm} -\setlength\footskip{3mm} -\setlength\textwidth{140mm} -\setlength\textheight{222mm} -\setlength\oddsidemargin{32mm} -\setlength\evensidemargin{38mm} -\setlength\marginparwidth{25mm} -\setlength\topmargin{13mm} -\setlength{\skip\footins}{2\baselineskip \@plus 4\p@ \@minus 2\p@} -\def\@listi{\leftmargin\leftmargini - \parsep\z@ \@plus\p@ - \topsep 8\p@ \@plus2\p@ \@minus4\p@ - \itemsep \parsep} -\let\@listI\@listi -\@listi -\def\@listii {\leftmargin\leftmarginii - \labelwidth\leftmarginii - \advance\labelwidth-\labelsep - \topsep 4\p@ \@plus2\p@ \@minus\p@ - \parsep\z@ \@plus\p@ - \itemsep \parsep} -\def\@listiii{\leftmargin\leftmarginiii - \labelwidth\leftmarginiii - \advance\labelwidth-\labelsep - \topsep 2\p@ \@plus\p@\@minus\p@ - \parsep \z@ - \partopsep \p@ \@plus\z@ \@minus\p@ - \itemsep \z@ \@plus\p@} -\def\ps@headings{% - \def\@evenhead{\large\sffamily\bfseries - \llap{\hbox to0.5\oddsidemargin{\thepage\hss}}\leftmark\hfil}% - \def\@oddhead{\large\sffamily\bfseries\rightmark\hfil - \rlap{\hbox to0.5\oddsidemargin{\hss\thepage}}}% - \def\@oddfoot{\hfil - \rlap{% - \vtop{% - \vskip10mm - \colorbox[rgb]{0.99,0.78,0.07} - {\@tempdima\evensidemargin - \advance\@tempdima1in - \advance\@tempdima\hoffset - \hb@xt@\@tempdima{% - \textcolor{darkgray}{\normalsize\sffamily - \bfseries\quad - \expandafter\textsolittle - \expandafter{\@EventShortName}}% - \strut\hss}}}}} - \let\@evenfoot\@empty - \let\@mkboth\markboth - \let\sectionmark\@gobble - \let\subsectionmark\@gobble} -\pagestyle{headings} -\renewcommand\maketitle{\par - \begingroup - \renewcommand\thefootnote{\@fnsymbol\c@footnote}% - \if@twocolumn - \ifnum \col@number=\@ne - \@maketitle - \else - \twocolumn[\@maketitle]% - \fi - \else - \newpage - \global\@topnum\z@ % Prevents figures from going at top of page. - \@maketitle - \fi - \thispagestyle{plain}\@thanks - \endgroup - \setcounter{footnote}{0}% - \global\let\thanks\relax - \global\let\maketitle\relax - \global\let\@maketitle\relax - \global\let\@thanks\@empty - \global\let\@author\@empty - \global\let\@date\@empty - \global\let\@title\@empty - \global\let\title\relax - \global\let\author\relax - \global\let\date\relax - \global\let\and\relax -} -\newwrite\tocfile -\def\@maketitle{% - \newpage - \null\vskip-\baselineskip - \vskip-\headsep - \@titlerunning - \@authorrunning - \let \footnote \thanks - \parindent\z@ \raggedright - {\LARGE\sffamily\bfseries\mathversion{bold}\@title \par}% - \vskip 1.5em% - \ifnum\c@authors=0 % - \@latexerr{No \noexpand\author given}% - {Provide at least one author. See the LIPIcs class documentation.}% - \else - \@author - \fi - \bgroup - \let\footnote\@gobble - \immediate\openout\tocfile=\jobname.vtc - \protected@write\tocfile{}{% - \string\contitem - \string\title{\@title}% - \string\author{\AB@authfortoc}% - \string\page{\thepage}}% - \closeout\tocfile - \egroup - \par} -\setcounter{secnumdepth}{4} -\renewcommand\section{\@startsection {section}{1}{\z@}% - {-3.5ex \@plus -1ex \@minus -.2ex}% - {2.3ex \@plus.2ex}% - {\sffamily\Large\bfseries\raggedright}} -\renewcommand\subsection{\@startsection{subsection}{2}{\z@}% - {-3.25ex\@plus -1ex \@minus -.2ex}% - {1.5ex \@plus .2ex}% - {\sffamily\Large\bfseries\raggedright}} -\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}% - {-3.25ex\@plus -1ex \@minus -.2ex}% - {1.5ex \@plus .2ex}% - {\sffamily\Large\bfseries\raggedright}} -\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}% - {-3.25ex \@plus-1ex \@minus-.2ex}% - {1.5ex \@plus .2ex}% - {\sffamily\large\bfseries\raggedright}} -\renewcommand\subparagraph{\@startsection{subparagraph}{5}{\z@}% - {3.25ex \@plus1ex \@minus .2ex}% - {-1em}% - {\sffamily\normalsize\bfseries}} -\setlength\leftmargini \parindent -\setlength\leftmarginii {1.2em} -\setlength\leftmarginiii{1.2em} -\setlength\leftmarginiv {1.2em} -\setlength\leftmarginv {1.2em} -\setlength\leftmarginvi {1.2em} -\renewcommand\labelenumi{% - \textcolor{darkgray}{\sffamily\bfseries\mathversion{bold}\theenumi.}} -\renewcommand\labelenumii{% - \textcolor{darkgray}{\sffamily\bfseries\mathversion{bold}\theenumii.}} -\renewcommand\labelenumiii{% - \textcolor{darkgray}{\sffamily\bfseries\mathversion{bold}\theenumiii.}} -\renewcommand\labelenumiv{% - \textcolor{darkgray}{\sffamily\bfseries\mathversion{bold}\theenumiv.}} -\renewcommand\labelitemi{% - \textcolor[rgb]{0.6,0.6,0.61}{\ifnum\@listdepth=\@ne - \rule{0.67em}{0.33em}% - \else - \rule{0.45em}{0.225em}% - \fi}} -\renewcommand\labelitemii{% - \textcolor[rgb]{0.6,0.6,0.61}{\rule{0.45em}{0.225em}}} -\renewcommand\labelitemiii{% - \textcolor[rgb]{0.6,0.6,0.61}{\sffamily\bfseries\textasteriskcentered}} -\renewcommand\labelitemiv{% - \textcolor[rgb]{0.6,0.6,0.61}{\sffamily\bfseries\textperiodcentered}} -\renewenvironment{description} - {\list{}{\advance\partopsep\topsep\topsep\z@\@plus\p@ - \labelwidth\z@ \itemindent-\leftmargin - \let\makelabel\descriptionlabel}} - {\ifnum\@listdepth=\@ne\global\@nobotseplisttrue\fi\endlist} -\renewcommand*\descriptionlabel[1]{% - \hspace\labelsep\textcolor{darkgray}{\sffamily\bfseries\mathversion{bold}#1}} -\renewenvironment{abstract}{% - \vskip\bigskipamount - \noindent - \rlap{\color[rgb]{0.51,0.50,0.52}\vrule\@width\textwidth\@height1\p@}% - \hspace*{7mm}\fboxsep1.5mm\colorbox[rgb]{1,1,1}{\raisebox{-0.4ex}{% - \large\selectfont\sffamily\bfseries\abstractname}}% - \vskip3\p@ - \fontsize{9.5}{12.5}\selectfont - \noindent\ignorespaces} - {\ifx\@subjclass\@empty\else - \vskip\baselineskip\noindent - \subjclassHeading\@subjclass - \fi - \ifx\@keywords\@empty\else - \vskip\baselineskip\noindent - \keywordsHeading\@keywords - \fi - \ifx\@DOI\@empty\else - \vskip\baselineskip\noindent - \doiHeading\doi{\@DOI}% - \fi} -\renewenvironment{thebibliography}[1] - {\if@noskipsec \leavevmode \fi - \par - \@tempskipa-3.5ex \@plus -1ex \@minus -.2ex\relax - \@afterindenttrue - \@tempskipa -\@tempskipa \@afterindentfalse - \if@nobreak - \everypar{}% - \else - \addpenalty\@secpenalty\addvspace\@tempskipa - \fi - \noindent - \rlap{\color[rgb]{0.51,0.50,0.52}\vrule\@width\textwidth\@height1\p@}% - \hspace*{7mm}\fboxsep1.5mm\colorbox[rgb]{1,1,1}{\raisebox{-0.4ex}{% - \normalsize\sffamily\bfseries\refname}}% - \@xsect{1ex \@plus.2ex}% - \list{\@biblabel{\@arabic\c@enumiv}}% - {\leftmargin8.5mm - \labelsep\leftmargin - \settowidth\labelwidth{\@biblabel{#1}}% - \advance\labelsep-\labelwidth - \usecounter{enumiv}% - \let\p@enumiv\@empty - \renewcommand\theenumiv{\@arabic\c@enumiv}}% - \fontsize{9.5}{12.5}\selectfont - \sloppy - \clubpenalty4000 - \@clubpenalty \clubpenalty - \widowpenalty4000% - \sfcode`\.\@m} - {\def\@noitemerr - {\@latex@warning{Empty `thebibliography' environment}}% - \endlist} -\renewcommand\footnoterule{% - \kern-8\p@ - {\color[rgb]{0.60,0.60,0.61}\hrule\@width40mm\@height1\p@}% - \kern6.6\p@} -\renewcommand\@makefntext[1]{% - \parindent\z@\hangindent1em - \leavevmode - \hb@xt@1em{\@makefnmark\hss}#1} -\usepackage[utf8]{inputenc} -\IfFileExists{lmodern.sty}{\RequirePackage{lmodern}}{} -\RequirePackage[T1]{fontenc} -\RequirePackage{textcomp} -\RequirePackage[mathscr]{eucal} -\RequirePackage{amssymb} -\RequirePackage{soul} -\sodef\textsolittle{}{.12em}{.5em\@plus.08em\@minus.06em}% - {.4em\@plus.275em\@minus.183em} -\RequirePackage{color} -\definecolor{darkgray}{rgb}{0.31,0.31,0.33} -\RequirePackage{babel} -\RequirePackage[tbtags,fleqn]{amsmath} -\RequirePackage{amsthm} -\thm@headfont{% - \textcolor{darkgray}{$\blacktriangleright$}\nobreakspace\sffamily\bfseries} -\def\th@remark{% - \thm@headfont{% - \textcolor{darkgray}{$\blacktriangleright$}\nobreakspace\sffamily}% - \normalfont % body font - \thm@preskip\topsep \divide\thm@preskip\tw@ - \thm@postskip\thm@preskip -} -\def\@endtheorem{\endtrivlist}%\@endpefalse -\renewcommand\qedsymbol{\textcolor{darkgray}{\ensuremath{\blacktriangleleft}}} -\renewenvironment{proof}[1][\proofname]{\par - \pushQED{\qed}% - \normalfont \topsep6\p@\@plus6\p@\relax - \trivlist - \item[\hskip\labelsep - \color{darkgray}\sffamily\bfseries - #1\@addpunct{.}]\ignorespaces -}{% - \popQED\endtrivlist%\@endpefalse -} -\theoremstyle{plain} -\newtheorem{theorem}{Theorem} -\newtheorem{lemma}[theorem]{Lemma} -\newtheorem{corollary}[theorem]{Corollary} -\theoremstyle{definition} -\newtheorem{definition}[theorem]{Definition} -\newtheorem{example}[theorem]{Example} -\theoremstyle{remark} -\newtheorem*{remark}{Remark} -\ifx\numberwithinsect\relax - \@addtoreset{theorem}{section} - \edef\thetheorem{\expandafter\noexpand\thesection\@thmcountersep\@thmcounter{theorem}} -\fi -\RequirePackage{graphicx} -\RequirePackage{array} -\let\@classzold\@classz -\def\@classz{% - \expandafter\ifx\d@llarbegin\begingroup - \toks \count@ = - \expandafter{\expandafter\small\the\toks\count@}% - \fi - \@classzold} -\RequirePackage{multirow} -\RequirePackage{tabularx} -\RequirePackage[online]{threeparttable} -\def\TPTtagStyle#1{#1)} -\def\tablenotes{\small\TPT@defaults - \@ifnextchar[\TPT@setuptnotes\TPTdoTablenotes} % ] -\RequirePackage{listings} -\lstset{basicstyle=\small\ttfamily,% - backgroundcolor=\color[rgb]{0.85,0.85,0.86},% - frame=single,framerule=0pt,xleftmargin=\fboxsep,xrightmargin=\fboxsep} -\RequirePackage{lastpage} -\IfFileExists{doi.sty} - {\RequirePackage{doi}% - \renewcommand*{\doitext}{}} - {\RequirePackage{hyperref}% - \def\doi##1{##1}} -\hypersetup{pdfborder={0 0 0}} -\RequirePackage[labelsep=space,singlelinecheck=false,% - font={up,small},labelfont={sf,bf},% - listof=false]{caption}%"listof" instead of "list" for backward compatibility -\@ifpackagelater{hyperref}{2009/12/09} - {\captionsetup{compatibility=false}}%cf. http://groups.google.de/group/comp.text.tex/browse_thread/thread/db9310eb540fbbd8/42e30f3b7b3aa17a?lnk=raot - {} -\DeclareCaptionLabelFormat{boxed}{% - \kern0.05em{\color[rgb]{0.99,0.78,0.07}\rule{0.73em}{0.73em}}% - \hspace*{0.67em}\bothIfFirst{#1}{~}#2} -\captionsetup{labelformat=boxed} -\captionsetup[table]{position=top} -\RequirePackage[figuresright]{rotating} -\RequirePackage{subfig} -\def\titlerunning#1{\gdef\@titlerunning{{\let\footnote\@gobble\markboth{#1}{#1}}}} -\def\authorrunning#1{% - \gdef\@authorrunning{\expandafter\def\expandafter\@tempa\expandafter{#1}% - \ifx\@tempa\@empty\else\markright{#1}\fi}} -\titlerunning{\@title} -\authorrunning{\AB@authrunning} -\newcommand*\volumeinfo[6]{% - {\gdef\@Editors{#1}% - \gdef\@Eds{Editor}\ifnum #2>1 \gdef\@Eds{Editors}\fi - \gdef\@Event{#3}% - \setcounter{page}{#6}}} -\volumeinfo{}{1}{}{}{}{1} -\RequirePackage{authblk} -\renewcommand*\Authand{{ and }} -\renewcommand*\Authfont{\Large\bfseries\mathversion{bold}} -\renewcommand*\AB@authnote[1]{\textsuperscript{#1}} -\renewcommand*\AB@affilnote[1]{\protect\item[#1]} -\renewcommand*\Affilfont{\fontsize{9.5}{12}\selectfont} -\setlength\affilsep{\baselineskip} -\newcommand\AB@authrunning{} -\newcommand\AB@authfortoc{} -\renewcommand\author[2][]% - {\ifnewaffil\addtocounter{affil}{1}% - \edef\AB@thenote{\arabic{affil}}\fi - \if\relax#1\relax\def\AB@note{\AB@thenote}\else\def\AB@note{#1}% - \setcounter{Maxaffil}{0}\fi - \ifnum\value{authors}>1\relax - \@namedef{@sep\number\c@authors}{\Authsep}\fi - \addtocounter{authors}{1}% - \begingroup - \let\protect\@unexpandable@protect \let\and\AB@pand - \def\thanks{\protect\thanks}\def\footnote{\protect\footnote}% - \@temptokena=\expandafter{\AB@authors}% - {\def\\{\protect\\[\@affilsep]\protect\Affilfont - \protect\AB@resetsep}% - \xdef\AB@author{\AB@blk@and#2}% - \ifnewaffil\gdef\AB@las{}\gdef\AB@lasx{\protect\Authand}\gdef\AB@as{}% - \xdef\AB@authors{\the\@temptokena\AB@blk@and}% - \else - \xdef\AB@authors{\the\@temptokena\AB@as\AB@au@str}% - \global\let\AB@las\AB@lasx\gdef\AB@lasx{\protect\Authands}% - \gdef\AB@as{\Authsep}% - \fi - \gdef\AB@au@str{#2}}% - \@temptokena=\expandafter{\AB@authlist}% - \let\\=\authorcr - \xdef\AB@authlist{\the\@temptokena - \protect\@nameuse{@sep\number\c@authors}% - \protect\Authfont#2\AB@authnote{\AB@note}}% - %new - \@temptokena=\expandafter{\AB@authrunning}% - \let\\=\authorcr - \xdef\AB@authrunning{\the\@temptokena - \protect\@nameuse{@sep\number\c@authors}#2}% - % - %new - \@temptokena=\expandafter{\AB@authfortoc}% - \let\\=\authorcr - \xdef\AB@authfortoc{\the\@temptokena - \expandafter\noexpand\csname @sep\number\c@authors\endcsname#2}% - % - \endgroup - \ifnum\value{authors}>2\relax - \@namedef{@sep\number\c@authors}{\Authands}\fi - \newaffilfalse -} -\renewcommand\affil[2][]% - {\newaffiltrue\let\AB@blk@and\AB@pand - \if\relax#1\relax\def\AB@note{\AB@thenote}\else\def\AB@note{#1}% - \setcounter{Maxaffil}{0}\fi - \begingroup - \let\protect\@unexpandable@protect - \def\thanks{\protect\thanks}\def\footnote{\protect\footnote}% - \@temptokena=\expandafter{\AB@authors}% - {\def\\{\protect\\\protect\Affilfont}\xdef\AB@temp{#2}}% - \xdef\AB@authors{\the\@temptokena\AB@las\AB@au@str - \protect\\[\affilsep]\protect\Affilfont\AB@temp}% - \gdef\AB@las{}\gdef\AB@au@str{}% - {\xdef\AB@temp{#2}}% - \@temptokena=\expandafter{\AB@affillist}% - \xdef\AB@affillist{\the\@temptokena \AB@affilsep - \AB@affilnote{\AB@note}\protect\Affilfont\AB@temp}% - \endgroup - \let\AB@affilsep\AB@affilsepx} -\renewcommand\@author{\ifx\AB@affillist\AB@empty\AB@authrunning\else - \ifnum\value{affil}>\value{Maxaffil}\def\rlap##1{##1}% - \AB@authlist\\[\affilsep] - \labelwidth1.5em\labelsep\z@\leftmargini\labelwidth - \edef\@enumctr{enumi}% - \list\theenumi{\usecounter\@enumctr\def\makelabel##1{\rlap{##1}\hss}}% - \AB@affillist - \endlist - \else \AB@authors\fi\fi} -\newcommand*\Copyright[1]{% - \def\@Copyright{% - \setbox\@tempboxa\hbox{\includegraphics[height=14\p@,clip]{cc-by}}% - \hspace*{\wd\@tempboxa}\enskip\ifx#1\@empty \else \textcopyright\ #1;\\\fi - \href{http://creativecommons.org/licenses/by/3.0/}% - {\smash{\unhbox\@tempboxa}}\enskip - licensed under Creative Commons License CC-BY\\ - }} -\Copyright{\@empty} -\def\keywords#1{\def\@keywords{#1}} -\let\@keywords\@empty -\def\keywordsHeading{% - \textcolor{darkgray}{\fontsize{9.5}{12.5}\sffamily\bfseries - Keywords and phrases\enskip}} -\def\subjclass#1{\gdef\@subjclass{#1}} -\let\@subjclass\@empty -\def\subjclassHeading{% - \textcolor{darkgray}{\fontsize{9.5}{12.5}\sffamily\bfseries - 1998 ACM Subject Classification\enskip}} -\def\doiHeading{% - \textcolor{darkgray}{\fontsize{9.5}{12.5}\sffamily\bfseries - Digital Object Identifier\enskip}} -\def\serieslogo#1{\gdef\@serieslogo{#1}} -\serieslogo{} -\def\EventShortName#1{\gdef\@EventShortName{#1}} -\EventShortName{} -\def\DOI#1{\gdef\@DOI{#1}} -\DOI{} -\endinput -%% -%% End of file `lipics.cls'. diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/pics/nub_filter_simp.png Binary file ChengsongPhdThesis/pics/nub_filter_simp.png has changed diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/pics/regex_nfa_alt.png Binary file ChengsongPhdThesis/pics/regex_nfa_alt.png has changed diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/pics/regex_nfa_base.png Binary file ChengsongPhdThesis/pics/regex_nfa_base.png has changed diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/pics/regex_nfa_seq1.png Binary file ChengsongPhdThesis/pics/regex_nfa_seq1.png has changed diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/pics/regex_nfa_seq2.png Binary file ChengsongPhdThesis/pics/regex_nfa_seq2.png has changed diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/pics/regex_nfa_star.png Binary file ChengsongPhdThesis/pics/regex_nfa_star.png has changed diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/re-java.data --- a/ChengsongPhdThesis/re-java.data Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -%% LaTeX2e file `re-java.data' -%% generated by the `filecontents' environment -%% from source `mentoringMeeting' on 2022/02/22. -%% -5 0.00298 -10 0.00418 -15 0.00996 -16 0.01710 -17 0.03492 -18 0.03303 -19 0.05084 -20 0.10177 -21 0.19960 -22 0.41159 -23 0.82234 -24 1.70251 -25 3.36112 -26 6.63998 -27 13.35120 -28 29.81185 diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/re-js.data --- a/ChengsongPhdThesis/re-js.data Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,15 +0,0 @@ -%% LaTeX2e file `re-js.data' -%% generated by the `filecontents' environment -%% from source `mentoringMeeting' on 2022/02/22. -%% -5 0.061 -10 0.061 -15 0.061 -20 0.070 -23 0.131 -25 0.308 -26 0.564 -28 1.994 -30 7.648 -31 15.881 -32 32.190 diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/re-python2.data --- a/ChengsongPhdThesis/re-python2.data Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -%% LaTeX2e file `re-python2.data' -%% generated by the `filecontents' environment -%% from source `mentoringMeeting' on 2022/02/22. -%% -1 0.033 -5 0.036 -10 0.034 -15 0.036 -18 0.059 -19 0.084 -20 0.141 -21 0.248 -22 0.485 -23 0.878 -24 1.71 -25 3.40 -26 7.08 -27 14.12 -28 26.69 diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/regex_time_complexity.bib --- a/ChengsongPhdThesis/regex_time_complexity.bib Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,66 +0,0 @@ -%% This BibTeX bibliography file was created using BibDesk. -%% https://bibdesk.sourceforge.io/ - -%% Created for CS TAN at 2022-02-22 23:40:24 +0000 - - -%% Saved with string encoding Unicode (UTF-8) - - - -@article{SulzmannLu14, - author = {Martin Sulzmann, Kennie Zhuo Ming Lu}, - date-added = {2022-02-22 23:36:08 +0000}, - date-modified = {2022-02-22 23:40:23 +0000}, - journal = {FLOPS}, - title = {POSIX Regular Expression Parsing with Derivatives}, - year = {2014}, - bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAdcmVnZXgtcGFyc2luZy1kZXJpdmF0aXZlcy5wZGZPEQGoAAAAAAGoAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8dcmVnZXgtcGFyc2luZy1kZXJpdmF0aXZlcy5wZGYAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAABAAIAAAogY3UAAAAAAAAAAAAAAAAACXJlZ2V4X2JpYgAAAgBHLzpVc2Vyczpjc3RhbjpEcm9wYm94OldvcmtzcGFjZTpyZWdleF9iaWI6cmVnZXgtcGFyc2luZy1kZXJpdmF0aXZlcy5wZGYAAA4APAAdAHIAZQBnAGUAeAAtAHAAYQByAHMAaQBuAGcALQBkAGUAcgBpAHYAYQB0AGkAdgBlAHMALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEVVc2Vycy9jc3Rhbi9Ecm9wYm94L1dvcmtzcGFjZS9yZWdleF9iaWIvcmVnZXgtcGFyc2luZy1kZXJpdmF0aXZlcy5wZGYAABMAAS8AABUAAgAM//8AAAAIAA0AGgAkAEQAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAAB8A==}} - -@article{Thompson_1968, - author = {Ken Thompson}, - date-added = {2022-02-22 23:24:32 +0000}, - date-modified = {2022-02-22 23:24:32 +0000}, - doi = {10.1145/363347.363387}, - journal = {Communications of the {ACM}}, - month = {jun}, - number = {6}, - pages = {419--422}, - publisher = {Association for Computing Machinery ({ACM})}, - title = {Programming Techniques: Regular expression search algorithm}, - url = {https://doi.org/10.1145%2F363347.363387}, - volume = {11}, - year = 1968, - bdsk-url-1 = {https://doi.org/10.1145%2F363347.363387}, - bdsk-url-2 = {https://doi.org/10.1145/363347.363387}} - -@article{Baeza_Yates_1996, - author = {Ricardo A. Baeza-Yates and Gaston H. Gonnet}, - date-added = {2022-02-22 22:54:46 +0000}, - date-modified = {2022-02-22 22:54:46 +0000}, - doi = {10.1145/235809.235810}, - journal = {Journal of the {ACM}}, - month = {nov}, - number = {6}, - pages = {915--936}, - publisher = {Association for Computing Machinery ({ACM})}, - title = {Fast text searching for regular expressions or automaton searching on tries}, - url = {https://doi.org/10.1145%2F235809.235810}, - volume = {43}, - year = 1996, - bdsk-url-1 = {https://doi.org/10.1145%2F235809.235810}, - bdsk-url-2 = {https://doi.org/10.1145/235809.235810}} - -@article{BaezaYates96, - author = {Baeza-Yates, Ricardo A.; Gonnet, Gaston H.}, - date-added = {2022-02-22 22:43:23 +0000}, - date-modified = {2022-02-22 22:51:43 +0000}, - journal = {J. ACM}, - number = {no. 6}, - pages = {915--936.}, - rss-description = {MR1434907 68Q25 (68P05) -Baeza-Yates, Ricardo A.; Gonnet, Gaston H. Fast text searching for regular expressions or automaton searching on tries. J. ACM 43 (1996), no. 6, 915--936.}, - title = {Fast text searching for regular expressions or automaton searching on tries.}, - volume = {43 (1996)}, - year = {1996}, - bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAmcHRyZWVzX3N1YmxpbmVhcl9yZWdleDk2QmFlemVZYXRlcy5wZGZPEQHKAAAAAAHKAAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8fcHRyZWVzX3N1YmxpbmVhcl9yI0ZGRkZGRkZGLnBkZgAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAABAAIAAAogY3UAAAAAAAAAAAAAAAAACXJlZ2V4X2JpYgAAAgBQLzpVc2Vyczpjc3RhbjpEcm9wYm94OldvcmtzcGFjZTpyZWdleF9iaWI6cHRyZWVzX3N1YmxpbmVhcl9yZWdleDk2QmFlemVZYXRlcy5wZGYADgBOACYAcAB0AHIAZQBlAHMAXwBzAHUAYgBsAGkAbgBlAGEAcgBfAHIAZQBnAGUAeAA5ADYAQgBhAGUAegBlAFkAYQB0AGUAcwAuAHAAZABmAA8AGgAMAE0AYQBjAGkAbgB0AG8AcwBoACAASABEABIATlVzZXJzL2NzdGFuL0Ryb3Bib3gvV29ya3NwYWNlL3JlZ2V4X2JpYi9wdHJlZXNfc3VibGluZWFyX3JlZ2V4OTZCYWV6ZVlhdGVzLnBkZgATAAEvAAAVAAIADP//AAAACAANABoAJABNAAAAAAAAAgEAAAAAAAAABQAAAAAAAAAAAAAAAAAAAhs=}} diff -r 2e7c7111c0be -r 31abe0e496bc ChengsongPhdThesis/root.bib --- a/ChengsongPhdThesis/root.bib Thu Mar 24 20:52:34 2022 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,351 +0,0 @@ -%% This BibTeX bibliography file was created using BibDesk. -%% https://bibdesk.sourceforge.io/ - -%% Created for CS TAN at 2022-02-23 13:45:03 +0000 - - -%% Saved with string encoding Unicode (UTF-8) - - - -@article{Thompson_1968, - author = {Ken Thompson}, - date-added = {2022-02-23 13:44:42 +0000}, - date-modified = {2022-02-23 13:44:42 +0000}, - doi = {10.1145/363347.363387}, - journal = {Communications of the {ACM}}, - month = {jun}, - number = {6}, - pages = {419--422}, - publisher = {Association for Computing Machinery ({ACM})}, - title = {Programming Techniques: Regular expression search algorithm}, - url = {https://doi.org/10.1145%2F363347.363387}, - volume = {11}, - year = 1968, - bdsk-url-1 = {https://doi.org/10.1145%2F363347.363387}, - bdsk-url-2 = {https://doi.org/10.1145/363347.363387}} - -@article{17Bir, - author = {Asiri Rathnayake and Hayo Thielecke}, - date-added = {2019-08-18 17:57:30 +0000}, - date-modified = {2019-08-18 18:00:13 +0000}, - journal = {arXiv:1405.7058}, - title = {Static Analysis for Regular Expression Exponential Runtime via Substructural Logics}, - year = {2017}} - -@article{nielson11bcre, - author = {Lasse Nielsen, Fritz Henglein}, - date-added = {2019-07-03 21:09:39 +0000}, - date-modified = {2019-07-03 21:17:33 +0000}, - journal = {LATA}, - title = {Bit-coded Regular Expression Parsing}, - year = {2011}, - bdsk-file-1 = {YnBsaXN0MDDSAQIDBFxyZWxhdGl2ZVBhdGhZYWxpYXNEYXRhXxAyLi4vLi4vTXkgTWFjIChNYWNCb29rLVBybykvRGVza3RvcC9mcml0ei1wYXBlci5wZGZPEQF+AAAAAAF+AAIAAAxNYWNpbnRvc2ggSEQAAAAAAAAAAAAAAAAAAAAAAAAAQkQAAf////8PZnJpdHotcGFwZXIucGRmAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA/////wAAAAAAAAAAAAAAAAACAAMAAAogY3UAAAAAAAAAAAAAAAAAB0Rlc2t0b3AAAAIAQi86VXNlcnM6Y3N0YW46RHJvcGJveDpNeSBNYWMgKE1hY0Jvb2stUHJvKTpEZXNrdG9wOmZyaXR6LXBhcGVyLnBkZgAOACAADwBmAHIAaQB0AHoALQBwAGEAcABlAHIALgBwAGQAZgAPABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgARAASAEBVc2Vycy9jc3Rhbi9Ecm9wYm94L015IE1hYyAoTWFjQm9vay1Qcm8pL0Rlc2t0b3AvZnJpdHotcGFwZXIucGRmABMAAS8AABUAAgAM//8AAAAIAA0AGgAkAFkAAAAAAAACAQAAAAAAAAAFAAAAAAAAAAAAAAAAAAAB2w==}} - -@misc{SE16, - author = {StackStatus}, - date-added = {2019-06-26 11:28:41 +0000}, - date-modified = {2019-06-26 16:07:31 +0000}, - keywords = {ReDos Attack}, - month = {July}, - rating = {5}, - read = {1}, - title = {Stack Overflow Outage Postmortem}, - url = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}, - year = {2016}, - bdsk-url-1 = {https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}} - -@article{HosoyaVouillonPierce2005, - author = {H.~Hosoya and J.~Vouillon and B.~C.~Pierce}, - journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)}, - number = 1, - pages = {46--90}, - title = {{R}egular {E}xpression {T}ypes for {XML}}, - volume = 27, - year = {2005}} - -@misc{POSIX, - note = {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}}, - title = {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition}, - year = {2004}} - -@inproceedings{AusafDyckhoffUrban2016, - author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, - booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)}, - pages = {69--86}, - series = {LNCS}, - title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)}, - volume = {9807}, - year = {2016}} - -@article{aduAFP16, - author = {F.~Ausaf and R.~Dyckhoff and C.~Urban}, - issn = {2150-914x}, - journal = {Archive of Formal Proofs}, - note = {\url{http://www.isa-afp.org/entries/Posix-Lexing.shtml}, Formal proof development}, - title = {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions}, - year = 2016} - -@techreport{CrashCourse2014, - annote = {draft report}, - author = {N.~B.~B.~Grathwohl and F.~Henglein and U.~T.~Rasmussen}, - institution = {University of Copenhagen}, - title = {{A} {C}rash-{C}ourse in {R}egular {E}xpression {P}arsing and {R}egular {E}xpressions as {T}ypes}, - year = {2014}} - -@inproceedings{Sulzmann2014, - author = {M.~Sulzmann and K.~Lu}, - booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)}, - pages = {203--220}, - series = {LNCS}, - title = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives}, - volume = {8475}, - year = {2014}} - -@inproceedings{Sulzmann2014b, - author = {M.~Sulzmann and P.~van Steenhoven}, - booktitle = {Proc.~of the 23rd International Conference on Compiler Construction (CC)}, - pages = {174--191}, - series = {LNCS}, - title = {{A} {F}lexible and {E}fficient {ML} {L}exer {T}ool {B}ased on {E}xtended {R}egular {E}xpression {S}ubmatching}, - volume = {8409}, - year = {2014}} - -@book{Pierce2015, - author = {B.~C.~Pierce and C.~Casinghino and M.~Gaboardi and M.~Greenberg and C.~Hri\c{t}cu and V.~Sj\"{o}berg and B.~Yorgey}, - note = {\url{http://www.cis.upenn.edu/~bcpierce/sf}}, - publisher = {Electronic textbook}, - title = {{S}oftware {F}oundations}, - year = {2015}} - -@misc{Kuklewicz, - author = {C.~Kuklewicz}, - howpublished = {\url{https://wiki.haskell.org/Regex_Posix}}, - title = {{R}egex {P}osix}} - -@article{Vansummeren2006, - author = {S.~Vansummeren}, - journal = {ACM Transactions on Programming Languages and Systems}, - number = {3}, - pages = {389--428}, - title = {{T}ype {I}nference for {U}nique {P}attern {M}atching}, - volume = {28}, - year = {2006}} - -@inproceedings{Asperti12, - author = {A.~Asperti}, - booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)}, - pages = {283--298}, - series = {LNCS}, - title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence}, - volume = {7406}, - year = {2012}} - -@inproceedings{Frisch2004, - author = {A.~Frisch and L.~Cardelli}, - booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)}, - pages = {618--629}, - series = {LNCS}, - title = {{G}reedy {R}egular {E}xpression {M}atching}, - volume = {3142}, - year = {2004}} - -@article{Antimirov95, - author = {V.~Antimirov}, - journal = {Theoretical Computer Science}, - pages = {291--319}, - title = {{P}artial {D}erivatives of {R}egular {E}xpressions and {F}inite {A}utomata {C}onstructions}, - volume = {155}, - year = {1995}} - -@inproceedings{Nipkow98, - author = {T.~Nipkow}, - booktitle = {Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)}, - pages = {1--15}, - series = {LNCS}, - title = {{V}erified {L}exical {A}nalysis}, - volume = 1479, - year = 1998} - -@article{Brzozowski1964, - author = {J.~A.~Brzozowski}, - journal = {Journal of the {ACM}}, - number = {4}, - pages = {481--494}, - title = {{D}erivatives of {R}egular {E}xpressions}, - volume = {11}, - year = {1964}} - -@article{Leroy2009, - author = {X.~Leroy}, - journal = {Communications of the ACM}, - number = 7, - pages = {107--115}, - title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler}, - volume = 52, - year = 2009} - -@inproceedings{Paulson2015, - author = {L.~C.~Paulson}, - booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)}, - pages = {231--245}, - series = {LNAI}, - title = {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets}, - volume = {9195}, - year = {2015}} - -@article{Wu2014, - author = {C.~Wu and X.~Zhang and C.~Urban}, - journal = {Journal of Automatic Reasoning}, - number = {4}, - pages = {451--480}, - title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions}, - volume = {52}, - year = {2014}} - -@inproceedings{Regehr2011, - author = {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr}, - booktitle = {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)}, - pages = {283--294}, - title = {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers}, - year = {2011}} - -@article{Norrish2014, - author = {A.~Barthwal and M.~Norrish}, - journal = {Journal of Computer and System Sciences}, - number = {2}, - pages = {346--362}, - title = {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}}, - volume = {80}, - year = {2014}} - -@article{Thompson1968, - author = {K.~Thompson}, - issue_date = {June 1968}, - journal = {Communications of the ACM}, - number = {6}, - pages = {419--422}, - title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm}, - volume = {11}, - year = {1968}} - -@article{Owens2009, - author = {S.~Owens and J.~H.~Reppy and A.~Turon}, - journal = {Journal of Functinal Programming}, - number = {2}, - pages = {173--190}, - title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined}, - volume = {19}, - year = {2009}} - -@inproceedings{Sulzmann2015, - author = {M.~Sulzmann and P.~Thiemann}, - booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory and Applications (LATA)}, - pages = {275--286}, - series = {LNCS}, - title = {{D}erivatives for {R}egular {S}huffle {E}xpressions}, - volume = {8977}, - year = {2015}} - -@inproceedings{Chen2012, - author = {H.~Chen and S.~Yu}, - booktitle = {Proc.~in the International Workshop on Theoretical Computer Science (WTCS)}, - pages = {343--356}, - series = {LNCS}, - title = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication}, - volume = {7160}, - year = {2012}} - -@article{Krauss2011, - author = {A.~Krauss and T.~Nipkow}, - journal = {Journal of Automated Reasoning}, - pages = {95--106}, - title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra}, - volume = 49, - year = 2012} - -@inproceedings{Traytel2015, - author = {D.~Traytel}, - booktitle = {Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)}, - pages = {487--503}, - series = {LIPIcs}, - title = {{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}}, - volume = {41}, - year = {2015}} - -@inproceedings{Traytel2013, - author = {D.~Traytel and T.~Nipkow}, - booktitle = {Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)}, - pages = {3-12}, - title = {{A} {V}erified {D}ecision {P}rocedure for {MSO} on {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions}, - year = 2013} - -@inproceedings{Coquand2012, - author = {T.~Coquand and V.~Siles}, - booktitle = {Proc.~of the 1st International Conference on Certified Programs and Proofs (CPP)}, - pages = {119--134}, - series = {LNCS}, - title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory}, - volume = {7086}, - year = {2011}} - -@inproceedings{Almeidaetal10, - author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa}, - booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)}, - pages = {59-68}, - series = {LNCS}, - title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq}, - volume = {6482}, - year = {2010}} - -@article{Owens2008, - author = {S.~Owens and K.~Slind}, - journal = {Higher-Order and Symbolic Computation}, - number = {4}, - pages = {377--409}, - title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic}, - volume = {21}, - year = {2008}} - -@article{Owens2, - author = {S.~Owens and K.~Slind}, - bibsource = {dblp computer science bibliography, http://dblp.org}, - biburl = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08}, - doi = {10.1007/s10990-008-9038-0}, - journal = {Higher-Order and Symbolic Computation}, - number = {4}, - pages = {377--409}, - timestamp = {Wed, 16 Dec 2009 13:51:02 +0100}, - title = {Adapting functional programs to higher order logic}, - url = {http://dx.doi.org/10.1007/s10990-008-9038-0}, - volume = {21}, - year = {2008}, - bdsk-url-1 = {http://dx.doi.org/10.1007/s10990-008-9038-0}} - -@misc{PCRE, - title = {{PCRE - Perl Compatible Regular Expressions}}, - url = {http://www.pcre.org}, - bdsk-url-1 = {http://www.pcre.org}} - -@inproceedings{OkuiSuzuki2010, - author = {S.~Okui and T.~Suzuki}, - booktitle = {Proc.~of the 15th International Conference on Implementation and Application of Automata (CIAA)}, - pages = {231--240}, - series = {LNCS}, - title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions}, - volume = {6482}, - year = {2010}} - -@techreport{OkuiSuzukiTech, - author = {S.~Okui and T.~Suzuki}, - institution = {University of Aizu}, - title = {{D}isambiguation in {R}egular {E}xpression {M}atching via {P}osition {A}utomata with {A}ugmented {T}ransitions}, - year = {2013}} - -@inproceedings{Davis18, - author = {J.~C.~Davis and C.~.A.~Coghlan and F.~Servant and D.~Lee}, - booktitle = {Proc.~of the 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE)}, - numpages = {11}, - pages = {246--256}, - title = {{T}he {I}mpact of {R}egular {E}xpression {D}enial of {S}ervice ({ReDoS}) in {P}ractice: {A}n {E}mpirical {S}tudy at the {E}cosystem {S}cale}, - year = {2018}}