\documentclass[a4paper,UKenglish]{lipics}

\usepackage{graphic}

\usepackage{data}

\usepackage{tikz-cd}

%\usepackage{algorithm}

\usepackage{amsmath}

\usepackage[noend]{algpseudocode}

\usepackage{enumitem}

\usepackage{nccmath}

\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\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\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{Practical Example of Regex}

%TODO: read rules libraries and the explanation for some of the rules

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.

\subsection{The problem: Efficient Matching and Lexing}

A programmer writes patterns to process texts,

where a regex is a structured symbolic pattern

specifying what the string should be like.

The above regex looks complicated, but can be 

described by some basic constructs:

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.

and the underlying algorithmic problem is:

\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}

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:

\begin{figure}

\centering

\includegraphics[scale=0.5]{pics/regex_nfa_base.png}

\end{figure}

\begin{figure}

\centering

\includegraphics[scale=0.5]{pics/regex_nfa_seq1.png}

\end{figure}

\begin{figure}

\centering

\includegraphics[scale=0.5]{pics/regex_nfa_seq2.png}

\end{figure}

\begin{figure}

\centering

\includegraphics[scale=0.5]{pics/regex_nfa_alt.png}

\end{figure}

\begin{figure}

\centering

\includegraphics[scale=0.5]{pics/regex_nfa_star.png}

\end{figure}

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