% Chapter 1

\chapter{Introduction} % Main chapter title

\label{Chapter1} % For referencing the chapter elsewhere, use \ref{Chapter1} 

%----------------------------------------------------------------------------------------

% Define some commands to keep the formatting separated from the content 

\newcommand{\keyword}[1]{\textbf{#1}}

\newcommand{\tabhead}[1]{\textbf{#1}}

\newcommand{\code}[1]{\texttt{#1}}

\newcommand{\file}[1]{\texttt{\bfseries#1}}

\newcommand{\option}[1]{\texttt{\itshape#1}}

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

\def\simp{\mathit{simp}}

\def\simpALTs{\mathit{simp}\_\mathit{ALTs}}

\def\map{\mathit{map}}

\def\distinct{\mathit{distinct}}

\def\blexersimp{\mathit{blexer}\_\mathit{simp}}

%----------------------------------------------------------------------------------------

%This part is about regular expressions, Brzozowski derivatives,

%and a bit-coded lexing algorithm with proven correctness and time bounds.

Regular expressions are widely used in modern day programming tasks.

Be it IDE with syntax hightlighting and auto completion, 

command line tools like $\mathit{grep}$ that facilitates easy 

processing of text by search and replace, network intrusion

detection systems that rejects suspicious traffic, or compiler

front ends--there is always an important phase of the

task that involves matching a regular 

exression with a string.

Given its usefulness and ubiquity, one would imagine that

modern regular expression matching implementations

are mature and fully-studied.

If you go to a popular programming language's

regex engine,

you can supply it with regex and strings of your own,

and get matching/lexing  information such as how a 

sub-part of the regex matches a sub-part of the string.

These lexing libraries are on average quite fast.

%TODO: get source for SNORT/BRO's regex matching engine/speed

For example, the regex engines some network intrusion detection

systems use are able to process

 megabytes or even gigabytes of network traffic per second.

Why do we need to have our version, if the algorithms are

blindingly fast already? Well it turns out it is not always the case.

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}  

This is clearly exponential behaviour, and 

is triggered by some relatively simple regex patterns.

This superlinear blowup in matching algorithms sometimes cause

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 a $\mathit{DoS}$ 

attack and therefore stopped the servers from responding to any

requests. This made the whole site become unavailable. 

A more 

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

%TODO: data points for some new versions of languages

These problems with regular expressions 

are not isolated events that happen

very occasionally, but actually quite widespread.

They occur so often that they get a 

name--Regular-Expression-Denial-Of-Service (ReDoS)

attack.

Davis et al. \parencite{Davis18} detected more

than 1000 super-linear (SL) regular expressions

in Node.js, Python core libraries, and npm and pypi. 

They therefore concluded that evil regular expressions

are problems more than "a parlour trick", but one that

requires

more research attention.

 \section{Why are current algorithm for regexes slow?}

Theoretical results say that regular expression matching

should be linear with respect to the input. 

You could construct

an NFA via Thompson construction, and simulate  running it.

This would be linear.

Or you could determinize the NFA into a DFA, and minimize that

DFA. Once you have the DFA, the running time is also linear, requiring just 

one scanning pass of the input.

But modern  regex libraries in popular language engines

 often want to support richer constructs

such as bounded repetitions and back-references

rather than  the most basic regular expressions.

%put in illustrations

%a{1}{3}

These make a DFA construction impossible because

of an exponential states explosion.

 They also want to support lexing rather than just matching

 for tasks that involves text processing.

 Existing regex libraries either pose restrictions on the user input, or does 

 not give linear running time guarantee.

 %TODO: give examples such as RE2 GOLANG 1000 restriction, rust no repetitions 

 For example, the Rust regex engine claims to be linear, 

 but does not support lookarounds and back-references.

 The GoLang regex library does not support over 1000 repetitions.  

 Java and Python both support back-references, but shows

catastrophic backtracking behaviours on inputs without back-references(

when the language is still regular).

 %TODO: test performance of Rust on (((((a*a*)b*)b){20})*)c  baabaabababaabaaaaaaaaababaaaababababaaaabaaabaaaaaabaabaabababaababaaaaaaaaababaaaababababaaaaaaaaaaaaac

 %TODO: verify the fact Rust does not allow 1000+ reps

 %TODO: Java 17 updated graphs? Is it ok to still use Java 8 graphs?

 Another thing about the these libraries is that there

 is no correctness guarantee.

 In some cases they either fails to generate a lexing result when there is a match,

 or gives the wrong way of matching.

It turns out that regex libraries not only suffer from 

exponential backtracking problems, 

but also undesired (or even buggy) outputs.

%TODO: comment from who

xxx commented that most regex libraries are not

correctly implementing the POSIX (maximum-munch)

rule of regular expression matching.

A concrete example would be 

the regex

\begin{verbatim}

(((((a*a*)b*)b){20})*)c

\end{verbatim}

and the string

\begin{verbatim}

baabaabababaabaaaaaaaaababaa

aababababaaaabaaabaaaaaabaab

aabababaababaaaaaaaaababaaaa

babababaaaaaaaaaaaaac

\end{verbatim}

This seemingly complex regex simply says "some $a$'s

followed by some $b$'s then followed by 1 single $b$,

and this iterates 20 times, finally followed by a $c$.

And a POSIX match would involve the entire string,"eating up"

all the $b$'s in it.

%TODO: give a coloured example of how this matches POSIXly

This regex would trigger catastrophic backtracking in 

languages like Python and Java,

whereas it gives a correct but uninformative (non-POSIX)

match in languages like Go or .NET--The match with only 

character $c$.

Backtracking or depth-first search might give us

exponential running time, and quite a few tools 

avoid that by determinising the $\mathit{NFA}$ 

into a $\mathit{DFA}$ and minimizes it.

For example, $\mathit{LEX}$ and $\mathit{JFLEX}$ are tools

in $C$ and $\mathit{JAVA}$ that generates $\mathit{DFA}$-based

lexers.

However, they do not scale well with bounded repetitions.

Bounded repetitions, usually written in the form

$r^{\{c\}}$ (where $c$ is a constant natural number),

denotes a regular expression accepting strings

that can be divided into $c$ substrings, and each 

substring is in $r$. 

%TODO: draw example NFA.

For the regular expression $(a|b)^*a(a|b)^{\{2\}}$,

an $\mathit{NFA}$ describing it would look like:

\begin{center}

\begin{tikzpicture}[shorten >=1pt,node distance=2cm,on grid,auto] 

   \node[state,initial] (q_0)   {$q_0$}; 

   \node[state, red] (q_1) [right=of q_0] {$q_1$}; 

   \node[state, red] (q_2) [right=of q_1] {$q_2$}; 

   \node[state,accepting](q_3) [right=of q_2] {$q_3$};

    \path[->] 

    (q_0) edge  node {a} (q_1)

    	  edge [loop below] node {a,b} ()

    (q_1) edge  node  {a,b} (q_2)

          edge [loop above] node {0} ()

    (q_2) edge  node  {a,b} (q_3);

\end{tikzpicture}

\end{center}

The red states are "counter states" which counts down 

the number of characters needed in addition to the current

string to make a successful match.

For example, state $q_1$ indicates a match that has

gone past the $(a|b)$ part of $(a|b)^*a(a|b)^{\{2\}}$,

and just consumed the "delimiter" $a$ in the middle, and 

need to match 2 more iterations of $a|b$ to complete.

State $q_2$ on the other hand, can be viewed as a state

after $q_1$ has consumed 1 character, and just waits

for 1 more character to complete.

Depending on the actual characters appearing in the 

input string, the states $q_1$ and $q_2$ may or may

not be active, independent from each other.

A $\mathit{DFA}$ for such an $\mathit{NFA}$ would

contain at least 4 non-equivalent states that cannot be merged, 

because subset states indicating which of $q_1$ and $q_2$

are active are at least four: $\phi$, $\{q_1\}$, 

$\{q_2\}$, $\{q_1, q_2\}$.

Generalizing this to regular expressions with larger

bounded repetitions number, we have $r^*ar^{\{n\}}$

in general would require at least $2^n$ states

in a $\mathit{DFA}$. This is to represent all different 

configurations of "countdown" states.

For those regexes, tools such as $\mathit{JFLEX}$ 

would generate gigantic $\mathit{DFA}$'s or even

give out memory errors.

For this reason, regex libraries that support 

bounded repetitions often choose to use the $\mathit{NFA}$ 

approach.

One can simulate the $\mathit{NFA}$ running in two ways:

one by keeping track of all active states after consuming 

a character, and update that set of states iteratively.

This is a breadth-first-search of the $\mathit{NFA}$.

for a path terminating

at an accepting state.

Languages like $\mathit{GO}$ and $\mathit{RUST}$ use this

type of $\mathit{NFA}$ simulation, and guarantees a linear runtime

in terms of input string length.

The other way to use $\mathit{NFA}$ for matching is to take 

a single state in a path each time, and backtrack if that path

fails. This is a depth-first-search that could end up

with exponential run time.

The reason behind backtracking algorithms in languages like

Java and Python is that they support back-references.

\subsection{Back References in Regex--Non-Regular part}

If we label sub-expressions by parenthesizing them and give 

them a number by the order their opening parenthesis appear,

$\underset{1}{(}\ldots\underset{2}{(}\ldots\underset{3}{(}\ldots\underset{4}{(}\ldots)\ldots)\ldots)\ldots)$

We can use the following syntax to denote that we want a string just matched by a 

sub-expression to appear at a certain location again exactly:

$(.*)\backslash 1$

would match the string like $\mathit{bobo}$, $\mathit{weewee}$ and etc.

Back-reference is a construct in the "regex" standard

that programmers found quite useful, but not exactly 

regular any more.

In fact, that allows the regex construct to express 

languages that cannot be contained in context-free

languages

For example, the back reference $(a^*)\backslash 1 \backslash 1$

expresses the language $\{a^na^na^n\mid n \in N\}$,

which cannot be expressed by context-free grammars.

To express such a language one would need context-sensitive

grammars, and matching/parsing for such grammars is NP-hard in 

general.

%TODO:cite reference for NP-hardness of CSG matching

For such constructs, the most intuitive way of matching is

using backtracking algorithms, and there are no known algorithms 

that does not backtrack.

%TODO:read a bit more about back reference algorithms

\section{Our Solution--Brzozowski Derivatives}

 Is it possible to have a regex lexing algorithm with proven correctness and 

 time complexity, which allows easy extensions to

  constructs like 

 bounded repetitions, negation,  lookarounds, and even back-references? 

 We propose Brzozowski's derivatives as a solution to this problem.

The main contribution of this thesis is a proven correct lexing algorithm

with formalized time bounds.

To our best knowledge, there is no lexing libraries using Brzozowski derivatives

that have a provable time guarantee, 

and claims about running time are usually speculative and backed by thin empirical

evidence.

%TODO: give references

For example, Sulzmann and Lu had proposed an algorithm  in which they

claim a linear running time.

But that was falsified by our experiments and the running time 

is actually $\Omega(2^n)$ in the worst case.

A similar claim about a theoretical runtime of $O(n^2)$ is made for the Verbatim

%TODO: give references

lexer, which calculates POSIX matches and is based on derivatives.

They formalized the correctness of the lexer, but not the complexity.

In the performance evaluation section, they simply analyzed the run time

of matching $a$ with the string $\underbrace{a \ldots a}_{\text{n a's}}$

and concluded that the algorithm is quadratic in terms of input length.

When we tried out their extracted OCaml code with our example $(a+aa)^*$,

the time it took to lex only 40 $a$'s was 5 minutes.

We therefore believe our results of a proof of performance on general

inputs rather than specific examples a novel contribution.\\

 \section{Preliminaries about Lexing Using Brzozowski derivatives}

 In the last fifteen or so years, Brzozowski's derivatives of regular

expressions have sparked quite a bit of interest in the functional

programming and theorem prover communities.  

The beauty of

Brzozowski's derivatives \parencite{Brzozowski1964} is that they are neatly

expressible in any functional language, and easily definable and

reasoned about in theorem provers---the definitions just consist of

inductive datatypes and simple recursive functions. 

Suppose we have an alphabet $\Sigma$, the strings  whose characters

are from $\Sigma$

can be expressed as $\Sigma^*$.

We use patterns to define a set of strings concisely. Regular expressions

are one of such patterns systems:

The basic regular expressions  are defined inductively

 by the following grammar:

\[			r ::=   \ZERO \mid  \ONE

			 \mid  c  

			 \mid  r_1 \cdot r_2

			 \mid  r_1 + r_2   

			 \mid r^*         

\]

The language or set of strings defined by regular expressions are defined as

%TODO: FILL in the other defs

\begin{center}

\begin{tabular}{lcl}

$L \; r_1 + r_2$ & $\dn$ & $ L \; r_1 \cup L \; r_2$\\

$L \; r_1 \cdot r_2$ & $\dn$ & $ L \; r_1 \cap L \; r_2$\\

\end{tabular}

\end{center}

Which are also called the "language interpretation".

The Brzozowski derivative w.r.t character $c$ is an operation on the regex,

where the operation transforms the regex to a new one containing

strings without the head character $c$.

Formally, we define first such a transformation on any string set, which

we call semantic derivative:

\begin{center}

$\Der \; c\; \textit{StringSet} = \{s \mid c :: s \in StringSet\}$

\end{center}

Mathematically, it can be expressed as the 

If the $\textit{StringSet}$ happen to have some structure, for example,

if it is regular, then we have that it

The the derivative of regular expression, denoted as

$r \backslash c$, is a function that takes parameters

$r$ and $c$, and returns another regular expression $r'$,

which is computed by the following recursive function:

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

\noindent

\noindent

The $\nullable$ function tests whether the empty string $""$ 

is in the language of $r$:

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

\noindent

The empty set does not contain any string and

therefore not the empty string, the empty string 

regular expression contains the empty string

by definition, the character regular expression

is the singleton that contains character only,

and therefore does not contain the empty string,

the alternative regular expression(or "or" expression)

might have one of its children regular expressions

being nullable and any one of its children being nullable

would suffice. The sequence regular expression

would require both children to have the empty string

to compose an empty string and the Kleene star

operation naturally introduced the empty string.

We can give the meaning of regular expressions derivatives

by language interpretation:

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