|
438
|
1 |
\documentclass[a4paper,UKenglish]{lipics}
|
|
|
2 |
\usepackage{graphic}
|
|
|
3 |
\usepackage{data}
|
|
|
4 |
\usepackage{tikz-cd}
|
|
|
5 |
%\usepackage{algorithm}
|
|
|
6 |
\usepackage{amsmath}
|
|
|
7 |
\usepackage[noend]{algpseudocode}
|
|
|
8 |
\usepackage{enumitem}
|
|
|
9 |
\usepackage{nccmath}
|
|
|
10 |
|
|
|
11 |
\usetikzlibrary{positioning}
|
|
|
12 |
|
|
|
13 |
\definecolor{darkblue}{rgb}{0,0,0.6}
|
|
|
14 |
\hypersetup{colorlinks=true,allcolors=darkblue}
|
|
|
15 |
\newcommand{\comment}[1]%
|
|
|
16 |
{{\color{red}$\Rightarrow$}\marginpar{\raggedright\small{\bf\color{red}#1}}}
|
|
|
17 |
|
|
|
18 |
% \documentclass{article}
|
|
|
19 |
%\usepackage[utf8]{inputenc}
|
|
|
20 |
%\usepackage[english]{babel}
|
|
|
21 |
%\usepackage{listings}
|
|
|
22 |
% \usepackage{amsthm}
|
|
|
23 |
%\usepackage{hyperref}
|
|
|
24 |
% \usepackage[margin=0.5in]{geometry}
|
|
|
25 |
%\usepackage{pmboxdraw}
|
|
|
26 |
|
|
|
27 |
\title{POSIX Regular Expression Matching and Lexing}
|
|
|
28 |
\author{Chengsong Tan}
|
|
|
29 |
\affil{King's College London\\
|
|
|
30 |
London, UK\\
|
|
|
31 |
\texttt{chengsong.tan@kcl.ac.uk}}
|
|
|
32 |
\authorrunning{Chengsong Tan}
|
|
|
33 |
\Copyright{Chengsong Tan}
|
|
|
34 |
|
|
|
35 |
\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
|
|
|
36 |
\newcommand{\ZERO}{\mbox{\bf 0}}
|
|
|
37 |
\newcommand{\ONE}{\mbox{\bf 1}}
|
|
|
38 |
\def\lexer{\mathit{lexer}}
|
|
|
39 |
\def\mkeps{\mathit{mkeps}}
|
|
|
40 |
|
|
441
|
41 |
\def\bmkeps{\textit{bmkeps}}
|
|
|
42 |
\def\retrieve{\textit{retrieve}}
|
|
|
43 |
\def\blexer{\textit{blexer}}
|
|
|
44 |
\def\flex{\textit{flex}}
|
|
438
|
45 |
\def\inj{\mathit{inj}}
|
|
|
46 |
\def\Empty{\mathit{Empty}}
|
|
|
47 |
\def\Left{\mathit{Left}}
|
|
|
48 |
\def\Right{\mathit{Right}}
|
|
|
49 |
\def\Stars{\mathit{Stars}}
|
|
|
50 |
\def\Char{\mathit{Char}}
|
|
|
51 |
\def\Seq{\mathit{Seq}}
|
|
|
52 |
\def\Der{\mathit{Der}}
|
|
|
53 |
\def\nullable{\mathit{nullable}}
|
|
|
54 |
\def\Z{\mathit{Z}}
|
|
|
55 |
\def\S{\mathit{S}}
|
|
441
|
56 |
\def\rup{r^\uparrow}
|
|
438
|
57 |
|
|
|
58 |
|
|
|
59 |
\def\awidth{\mathit{awidth}}
|
|
|
60 |
\def\pder{\mathit{pder}}
|
|
|
61 |
\def\maxterms{\mathit{maxterms}}
|
|
|
62 |
\def\bsimp{\mathit{bsimp}}
|
|
|
63 |
|
|
|
64 |
%\theoremstyle{theorem}
|
|
|
65 |
%\newtheorem{theorem}{Theorem}
|
|
|
66 |
%\theoremstyle{lemma}
|
|
|
67 |
%\newtheorem{lemma}{Lemma}
|
|
|
68 |
%\newcommand{\lemmaautorefname}{Lemma}
|
|
|
69 |
%\theoremstyle{definition}
|
|
|
70 |
%\newtheorem{definition}{Definition}
|
|
|
71 |
\algnewcommand\algorithmicswitch{\textbf{switch}}
|
|
|
72 |
\algnewcommand\algorithmiccase{\textbf{case}}
|
|
|
73 |
\algnewcommand\algorithmicassert{\texttt{assert}}
|
|
|
74 |
\algnewcommand\Assert[1]{\State \algorithmicassert(#1)}%
|
|
|
75 |
% New "environments"
|
|
|
76 |
\algdef{SE}[SWITCH]{Switch}{EndSwitch}[1]{\algorithmicswitch\ #1\ \algorithmicdo}{\algorithmicend\ \algorithmicswitch}%
|
|
|
77 |
\algdef{SE}[CASE]{Case}{EndCase}[1]{\algorithmiccase\ #1}{\algorithmicend\ \algorithmiccase}%
|
|
|
78 |
\algtext*{EndSwitch}%
|
|
|
79 |
\algtext*{EndCase}%
|
|
|
80 |
|
|
|
81 |
|
|
|
82 |
\begin{document}
|
|
|
83 |
|
|
|
84 |
\maketitle
|
|
|
85 |
|
|
|
86 |
\begin{abstract}
|
|
|
87 |
Brzozowski introduced in 1964 a beautifully simple algorithm for
|
|
|
88 |
regular expression matching based on the notion of derivatives of
|
|
|
89 |
regular expressions. In 2014, Sulzmann and Lu extended this
|
|
|
90 |
algorithm to not just give a YES/NO answer for whether or not a
|
|
|
91 |
regular expression matches a string, but in case it does also
|
|
|
92 |
answers with \emph{how} it matches the string. This is important for
|
|
|
93 |
applications such as lexing (tokenising a string). The problem is to
|
|
|
94 |
make the algorithm by Sulzmann and Lu fast on all inputs without
|
|
|
95 |
breaking its correctness. We have already developed some
|
|
|
96 |
simplification rules for this, but have not yet proved that they
|
|
|
97 |
preserve the correctness of the algorithm. We also have not yet
|
|
|
98 |
looked at extended regular expressions, such as bounded repetitions,
|
|
|
99 |
negation and back-references.
|
|
|
100 |
\end{abstract}
|
|
|
101 |
|
|
|
102 |
\section{Introduction}
|
|
440
|
103 |
\subsection{Basic Regex Introduction}
|
|
|
104 |
Suppose (basic) regular expressions are given by the following grammar:
|
|
|
105 |
\[ r ::= \ZERO \mid \ONE
|
|
|
106 |
\mid c
|
|
|
107 |
\mid r_1 \cdot r_2
|
|
|
108 |
\mid r_1 + r_2
|
|
|
109 |
\mid r^*
|
|
|
110 |
\]
|
|
|
111 |
|
|
|
112 |
Problem of matching:
|
|
438
|
113 |
|
|
440
|
114 |
\begin{center}
|
|
|
115 |
\begin{tabular}{lcr}
|
|
|
116 |
$\textit{Match}(r, s)$ & $ = $ & $\textit{if}\; s \in L(r)\; \textit{output} \; \textit{YES}$\\
|
|
|
117 |
& & $\textit{else} \; \textit{output} \; \textit{NO}$
|
|
|
118 |
\end{tabular}
|
|
|
119 |
\end{center}
|
|
|
120 |
|
|
|
121 |
|
|
|
122 |
\subsection{The practical problem}
|
|
|
123 |
Introduce the problem of matching a pattern with a string.
|
|
|
124 |
Why important?
|
|
|
125 |
Need to be fast, real-time, on large inputs.
|
|
|
126 |
Examples: Snort, Bro, etc?
|
|
|
127 |
\subsubsection{The rules for network intrusion analysis tools }
|
|
|
128 |
TODO: read rules libraries such as Snort and the explanation for some of the rules
|
|
|
129 |
TODO: pcre/pcre2?
|
|
|
130 |
TODO: any other libraries?
|
|
|
131 |
|
|
|
132 |
|
|
|
133 |
\subsection{Regexes that brought down CloudFlare}
|
|
|
134 |
|
|
|
135 |
|
|
438
|
136 |
matching some string $s$ with a regex
|
|
|
137 |
|
|
|
138 |
\begin{verbatim}
|
|
|
139 |
(?:(?:\"|'|\]|\}|\\|\d|
|
|
|
140 |
(?:nan|infinity|true|false|null|undefined|symbol|math)
|
|
|
141 |
|\`|\-|\+)+[)]*;?((?:\s|-|~|!|{}|\|\||\+)*.*(?:.*=.*)))
|
|
|
142 |
\end{verbatim}
|
|
|
143 |
|
|
|
144 |
|
|
|
145 |
%Could be from a network intrusion detection algorithm.
|
|
|
146 |
%Checking whether there is some malicious code
|
|
|
147 |
%in the network data blocks being routed.
|
|
|
148 |
%If so, discard the data and identify the sender for future alert.
|
|
440
|
149 |
\section{Existing approaches}
|
|
|
150 |
\subsection{Shortcomings of different methods}
|
|
438
|
151 |
|
|
440
|
152 |
|
|
|
153 |
\subsubsection{ NFA's}
|
|
441
|
154 |
$\bold{Problems With This:}$
|
|
|
155 |
\begin{itemize}
|
|
|
156 |
\item
|
|
440
|
157 |
Can be slow especially when many states are active.
|
|
441
|
158 |
\item
|
|
|
159 |
Want Lexing Results: Can have Exponential different matching results.
|
|
|
160 |
\end{itemize}
|
|
|
161 |
|
|
|
162 |
|
|
|
163 |
One regular expression can have multiple lexical values. For example
|
|
|
164 |
for the regular expression $(a+b)^*$, it has a infinite list of
|
|
|
165 |
values corresponding to it: $\Stars\,[]$, $\Stars\,[\Left(Char(a))]$,
|
|
|
166 |
$\Stars\,[\Right(Char(b))]$, $\Stars\,[\Left(Char(a),\,\Right(Char(b))]$,
|
|
|
167 |
$\ldots$, and vice versa.
|
|
|
168 |
Even for the regular expression matching a certain string, there could
|
|
|
169 |
still be more than one value corresponding to it.
|
|
|
170 |
Take the example where $r= (a^*\cdot a^*)^*$ and the string
|
|
|
171 |
$s=\underbrace{aa\ldots a}_\text{n \textit{a}s}$.
|
|
|
172 |
The number of different ways of matching
|
|
|
173 |
without allowing any value under a star to be flattened
|
|
|
174 |
to an empty string can be given by the following formula:
|
|
|
175 |
\begin{center}
|
|
|
176 |
$C_n = (n+1)+n C_1+\ldots + 2 C_{n-1}$
|
|
|
177 |
\end{center}
|
|
|
178 |
and a closed form formula can be calculated to be
|
|
|
179 |
\begin{equation}
|
|
|
180 |
C_n =\frac{(2+\sqrt{2})^n - (2-\sqrt{2})^n}{4\sqrt{2}}
|
|
|
181 |
\end{equation}
|
|
|
182 |
which is clearly in exponential order.
|
|
|
183 |
A lexer aimed at getting all the possible values has an exponential
|
|
|
184 |
worst case runtime. Therefore it is impractical to try to generate
|
|
|
185 |
all possible matches in a run. In practice, we are usually
|
|
|
186 |
interested about POSIX values, which by intuition always
|
|
|
187 |
match the leftmost regular expression when there is a choice
|
|
|
188 |
and always match a sub part as much as possible before proceeding
|
|
|
189 |
to the next token. For example, the above example has the POSIX value
|
|
|
190 |
$ \Stars\,[\Seq(Stars\,[\underbrace{\Char(a),\ldots,\Char(a)}_\text{n iterations}], Stars\,[])]$.
|
|
|
191 |
The output of an algorithm we want would be a POSIX matching
|
|
|
192 |
encoded as a value.\\
|
|
|
193 |
$\mathbf{TODO:}$
|
|
|
194 |
\begin{itemize}
|
|
|
195 |
\item
|
|
|
196 |
Illustrate graphically how you can match $a*a**$ with $aaa$ in different ways.
|
|
|
197 |
\item
|
|
|
198 |
Give a backtracking algorithm, and explain briefly why this can be exponentially slow.
|
|
|
199 |
(When there is a matching, it finds straight away; where there is not one, this fails to
|
|
|
200 |
recognize immediately that a match cannot be possibly found, and tries out all remaining
|
|
|
201 |
possibilities, etc.)
|
|
|
202 |
\item
|
|
|
203 |
From the above point, are there statical analysis tools that single out those malicious
|
|
|
204 |
patterns and tell before a lexer is even run?
|
|
|
205 |
Have a more thorough survey of the Birmingham paper.
|
|
|
206 |
Give out the suitable scenarios for such static analysis algorithms.
|
|
|
207 |
|
|
|
208 |
\end{itemize}
|
|
438
|
209 |
|
|
440
|
210 |
\subsubsection{DFAs}
|
|
|
211 |
The tool JFLEX uses it.
|
|
|
212 |
Advantages: super fast on most regexes \\
|
|
|
213 |
TODO: show it being fast on a lot of inputs\\
|
|
|
214 |
Disavantages:
|
|
|
215 |
state explosion for bounded repetitions due to
|
|
|
216 |
theoretic bottleneck of having to remember exactly what the
|
|
|
217 |
suffix up to length $n$ of input string is.
|
|
|
218 |
"Countdown States activation problem":
|
|
|
219 |
$.*a.{100}$ requires $2^100$ + DFA states.
|
|
|
220 |
\subsubsection{variant of DFA's}
|
|
|
221 |
counting set automata
|
|
|
222 |
\\
|
|
|
223 |
TODO: microsoft 2020 oopsla CsA work, need to add bibli entry, and read, understand key novelty, learn to benchmark like it
|
|
|
224 |
\\
|
|
|
225 |
TODO: find weakness of such counting set automata?
|
|
|
226 |
\\
|
|
|
227 |
Other variants?
|
|
|
228 |
|
|
|
229 |
\subsubsection{NFA and Regex: isomorphic structure}
|
|
|
230 |
TODO: define mathematically an isomorphism?\\
|
|
|
231 |
|
|
438
|
232 |
|
|
|
233 |
|
|
440
|
234 |
\subsubsection{variants of NFA's}
|
|
|
235 |
How about acting on regular expressions themselves? Certain copies represent verbose info--that they will always match the same string--prune away!
|
|
|
236 |
|
|
|
237 |
\subsection{Brzozowski's derivatives}
|
|
|
238 |
|
|
|
239 |
\subsection{Sulzmann and Lu's algorithm}
|
|
|
240 |
|
|
|
241 |
\subsection{Bit-coded algorithm}
|
|
|
242 |
+bitcodes!
|
|
|
243 |
Built on top of derivatives, but with auxiliary bits
|
|
|
244 |
\subsection{Correctness Proof}
|
|
441
|
245 |
|
|
|
246 |
Not proven by Sulzmann and Lu
|
|
|
247 |
|
|
|
248 |
Proven by Ausaf and Urban!!
|
|
|
249 |
|
|
|
250 |
|
|
|
251 |
For this we have started with looking at the proof of
|
|
|
252 |
\begin{equation}\label{lexer}
|
|
|
253 |
\blexer \; (r^\uparrow) s = \lexer \;r \;s,
|
|
|
254 |
\end{equation}
|
|
|
255 |
|
|
|
256 |
%\noindent
|
|
|
257 |
%might provide us insight into proving
|
|
|
258 |
%\begin{center}
|
|
|
259 |
%$\blexer \; r^\uparrow \;s = \blexers \; r^\uparrow \;s$
|
|
|
260 |
%\end{center}
|
|
|
261 |
|
|
|
262 |
\noindent
|
|
|
263 |
which established that the bit-sequence algorithm produces the same
|
|
|
264 |
result as the original algorithm, which does not use
|
|
|
265 |
bit-sequences.
|
|
|
266 |
The proof uses two ``tricks''. One is that it uses a \flex-function
|
|
|
267 |
|
|
|
268 |
\begin{center}
|
|
|
269 |
\begin{tabular}{lcl}
|
|
|
270 |
$\textit{flex} \;r\; f\; (c\!::\!s) $ & $\dn$ & $\textit{flex} \; (r\backslash c) \;(\lambda v. f (inj \; r \; c \; v)) \;s$ \\
|
|
|
271 |
$\textit{flex} \;r\; f\; [\,] $ & $\dn$ & $f$
|
|
|
272 |
\end{tabular}
|
|
|
273 |
\end{center}
|
|
|
274 |
|
|
|
275 |
\noindent
|
|
|
276 |
|
|
|
277 |
The intuition behind the $\flex$ function is that
|
|
|
278 |
it accumulates a series of $\inj$ function applications when doing derivatives
|
|
|
279 |
in a $\mathit{LIFO}$ manner. The arguments of the $\inj$ functions are kept by
|
|
|
280 |
remembering which character
|
|
|
281 |
was chopped off and what the regular expression looks like before
|
|
|
282 |
chopping off that character.
|
|
|
283 |
The $\mathit{LIFO}$ order was achieved by putting the newest $\inj$ application
|
|
|
284 |
always before the application of $f$, the previously accumulated function applications.\\
|
|
|
285 |
Therefore, the function $\flex$, when acted on a string $s@[c]$ where the last
|
|
|
286 |
character is $c$, by nature can have its last injection function revealed already:
|
|
|
287 |
\begin{equation}\label{flex}
|
|
|
288 |
\flex \; r \; id \; (s@[c]) \; v = \flex \; r \; id \; s \; (inj \; (r\backslash s) \; c\; v).
|
|
|
289 |
\end{equation}
|
|
|
290 |
that the last character can be taken off, and the injection it causes be applied to
|
|
|
291 |
the argument value $v$.
|
|
|
292 |
|
|
|
293 |
Ausaf and Urban proved that the Sulzmann and Lu's lexers
|
|
|
294 |
can be charactarized by the $\flex$ function:
|
|
|
295 |
\begin{center}
|
|
|
296 |
$\lexer \;r\; s = \flex \;\textit{id} \; r\;s \;(\mkeps \; (r\backslash s))$.
|
|
|
297 |
\end{center}
|
|
|
298 |
|
|
|
299 |
\noindent
|
|
|
300 |
This property says that the Sulzmann and Lu's $\lexer$ does lexing by
|
|
|
301 |
stacking up injection functions while doing derivatives,
|
|
|
302 |
explicitly showing the order of characters being
|
|
|
303 |
injected back in each step.
|
|
|
304 |
|
|
|
305 |
\noindent
|
|
|
306 |
The other trick, which is the crux in the existing proof,
|
|
|
307 |
is the use of the $\retrieve$-function:
|
|
|
308 |
\begin{center}
|
|
|
309 |
\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
|
|
|
310 |
$\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\
|
|
|
311 |
$\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\
|
|
|
312 |
$\textit{retrieve}\,(_{bs}\sum a::as)\,(\Left\,v)$ & $\dn$ &
|
|
|
313 |
$bs \,@\, \textit{retrieve}\,a\,v$\\
|
|
|
314 |
$\textit{retrieve}\,(_{bs}\sum a::as)\,(\Right\,v)$ & $\dn$ &
|
|
|
315 |
$\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\sum as)\,v$\\
|
|
|
316 |
$\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &
|
|
|
317 |
$bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\
|
|
|
318 |
$\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ &
|
|
|
319 |
$bs \,@\, [0]$\\
|
|
|
320 |
$\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\
|
|
|
321 |
\multicolumn{3}{l}{
|
|
|
322 |
\hspace{3cm}$bs \,@\, [1] \,@\, \textit{retrieve}\,a\,v\,@\,
|
|
|
323 |
\textit{retrieve}\,(_{[]}a^*)\,(\Stars\,vs)$}\\
|
|
|
324 |
\end{tabular}
|
|
|
325 |
\end{center}
|
|
|
326 |
|
|
|
327 |
\noindent
|
|
|
328 |
Sulzmann and Lu proposed this function, but did not prove
|
|
|
329 |
anything about it. Ausaf and Urban made use of the
|
|
|
330 |
fact about $\retrieve$ in their proof:
|
|
|
331 |
\begin{equation}\label{retrieve_reversible}
|
|
|
332 |
\retrieve\; \rup \backslash c \; v = \retrieve \; \rup (\inj \;r \;c \; v)
|
|
|
333 |
\end{equation}
|
|
|
334 |
This says that $\retrieve$ will always pick up
|
|
|
335 |
partial information about a lexing value value and transform it into suitable bitcodes.
|
|
|
336 |
If the information is in the regular expression (stored as bitcodes), it will keep those
|
|
|
337 |
bitcodes with the guidance of the value,
|
|
|
338 |
if the information is in the value, which has been injected back to the value,
|
|
|
339 |
it will "digest" and transform that part of the value to bitcodes.
|
|
|
340 |
|
|
|
341 |
\noindent
|
|
|
342 |
|
|
|
343 |
Using this together with ~\eqref{flex}, we can prove that the bitcoded version of
|
|
|
344 |
lexer is the same as Sulzmann and Lu's lexer:
|
|
|
345 |
\begin{center}
|
|
|
346 |
$\lexer \; r \; s = \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{bmkeps}\; (\rup \backslash s) ) r = \blexer \; r \; s$
|
|
|
347 |
\end{center}
|
|
|
348 |
\noindent
|
|
|
349 |
\begin{proof}
|
|
|
350 |
We express $\bmkeps$ using $\retrieve$, and the theorem to prove becomes:
|
|
|
351 |
\begin{center}
|
|
|
352 |
$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$
|
|
|
353 |
\end{center}
|
|
|
354 |
\noindent
|
|
|
355 |
We prove the above by reverse induction on string $s$(meaning that the inductive step is on
|
|
|
356 |
$s @ [c]$ rather than $c :: s$).
|
|
|
357 |
$v$ takes arbitrary values.\\
|
|
|
358 |
The base case goes through trivially.\\
|
|
|
359 |
For the inductive step, assuming
|
|
|
360 |
$ \flex \; r\; id\; s\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash s) \; v \;) r$
|
|
|
361 |
holds for all values $v$. Now we need to show that
|
|
|
362 |
$ \flex \; r\; id\; s@[c]\; v = \textit{decode} \;( \textit{retrieve}\; (\rup \backslash (s@[c])) \; v \;) r$.\\
|
|
|
363 |
~\eqref{flex} allows us to do the following rewrite:
|
|
|
364 |
\begin{center}
|
|
|
365 |
$ \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$
|
|
|
366 |
\end{center}
|
|
|
367 |
~\eqref{retrieve_reversible} allows us to further rewrite the $\mathit{RHS}$ of the above to
|
|
|
368 |
\begin{center}
|
|
|
369 |
$\textit{decode} \; (\textit{retrieve}\; (\rup \backslash (s @ [c])) \; v\;) \;r$
|
|
|
370 |
\end{center}
|
|
|
371 |
|
|
|
372 |
|
|
|
373 |
\end{proof}
|
|
|
374 |
|
|
|
375 |
|
|
440
|
376 |
|
|
|
377 |
\section{My Work}
|
|
|
378 |
|
|
|
379 |
\subsection{an improved version of bit-coded algorithm: with simp!}
|
|
438
|
380 |
|
|
440
|
381 |
\subsection{a correctness proof for bitcoded}
|
|
|
382 |
|
|
|
383 |
\subsection{finiteness proof }
|
|
|
384 |
|
|
|
385 |
\subsection{stronger simplification}
|
|
|
386 |
|
|
|
387 |
|
|
|
388 |
\subsection{cubic bound}
|
|
|
389 |
|
|
438
|
390 |
|
|
440
|
391 |
|
|
|
392 |
|
|
|
393 |
|
|
|
394 |
|
|
|
395 |
|
|
|
396 |
|
|
|
397 |
|
|
|
398 |
|
|
|
399 |
|
|
|
400 |
\subsection{Too Detailed too basic? regex to NFA translation}
|
|
438
|
401 |
|
|
|
402 |
Deciding whether a string is in the language of the regex
|
|
|
403 |
can be intuitively done by constructing an NFA\cite{Thompson_1968}:
|
|
|
404 |
and simulate the running of it:
|
|
|
405 |
\begin{figure}
|
|
|
406 |
\centering
|
|
|
407 |
\includegraphics[scale=0.5]{pics/regex_nfa_base.png}
|
|
|
408 |
\end{figure}
|
|
|
409 |
|
|
|
410 |
\begin{figure}
|
|
|
411 |
\centering
|
|
|
412 |
\includegraphics[scale=0.5]{pics/regex_nfa_seq1.png}
|
|
|
413 |
\end{figure}
|
|
|
414 |
|
|
|
415 |
\begin{figure}
|
|
|
416 |
\centering
|
|
|
417 |
\includegraphics[scale=0.5]{pics/regex_nfa_seq2.png}
|
|
|
418 |
\end{figure}
|
|
|
419 |
|
|
|
420 |
\begin{figure}
|
|
|
421 |
\centering
|
|
|
422 |
\includegraphics[scale=0.5]{pics/regex_nfa_alt.png}
|
|
|
423 |
\end{figure}
|
|
|
424 |
|
|
|
425 |
|
|
|
426 |
\begin{figure}
|
|
|
427 |
\centering
|
|
|
428 |
\includegraphics[scale=0.5]{pics/regex_nfa_star.png}
|
|
|
429 |
\end{figure}
|
|
|
430 |
|
|
|
431 |
Which should be simple enough that modern programmers
|
|
|
432 |
have no problems with it at all?
|
|
|
433 |
Not really:
|
|
|
434 |
|
|
|
435 |
Take $(a^*)^*\,b$ and ask whether
|
|
|
436 |
strings of the form $aa..a$ match this regular
|
|
|
437 |
expression. Obviously this is not the case---the expected $b$ in the last
|
|
|
438 |
position is missing. One would expect that modern regular expression
|
|
|
439 |
matching engines can find this out very quickly. Alas, if one tries
|
|
|
440 |
this example in JavaScript, Python or Java 8 with strings like 28
|
|
|
441 |
$a$'s, one discovers that this decision takes around 30 seconds and
|
|
|
442 |
takes considerably longer when adding a few more $a$'s, as the graphs
|
|
|
443 |
below show:
|
|
|
444 |
|
|
|
445 |
\begin{center}
|
|
|
446 |
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
|
|
|
447 |
\begin{tikzpicture}
|
|
|
448 |
\begin{axis}[
|
|
|
449 |
xlabel={$n$},
|
|
|
450 |
x label style={at={(1.05,-0.05)}},
|
|
|
451 |
ylabel={time in secs},
|
|
|
452 |
enlargelimits=false,
|
|
|
453 |
xtick={0,5,...,30},
|
|
|
454 |
xmax=33,
|
|
|
455 |
ymax=35,
|
|
|
456 |
ytick={0,5,...,30},
|
|
|
457 |
scaled ticks=false,
|
|
|
458 |
axis lines=left,
|
|
|
459 |
width=5cm,
|
|
|
460 |
height=4cm,
|
|
|
461 |
legend entries={JavaScript},
|
|
|
462 |
legend pos=north west,
|
|
|
463 |
legend cell align=left]
|
|
|
464 |
\addplot[red,mark=*, mark options={fill=white}] table {re-js.data};
|
|
|
465 |
\end{axis}
|
|
|
466 |
\end{tikzpicture}
|
|
|
467 |
&
|
|
|
468 |
\begin{tikzpicture}
|
|
|
469 |
\begin{axis}[
|
|
|
470 |
xlabel={$n$},
|
|
|
471 |
x label style={at={(1.05,-0.05)}},
|
|
|
472 |
%ylabel={time in secs},
|
|
|
473 |
enlargelimits=false,
|
|
|
474 |
xtick={0,5,...,30},
|
|
|
475 |
xmax=33,
|
|
|
476 |
ymax=35,
|
|
|
477 |
ytick={0,5,...,30},
|
|
|
478 |
scaled ticks=false,
|
|
|
479 |
axis lines=left,
|
|
|
480 |
width=5cm,
|
|
|
481 |
height=4cm,
|
|
|
482 |
legend entries={Python},
|
|
|
483 |
legend pos=north west,
|
|
|
484 |
legend cell align=left]
|
|
|
485 |
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
|
|
|
486 |
\end{axis}
|
|
|
487 |
\end{tikzpicture}
|
|
|
488 |
&
|
|
|
489 |
\begin{tikzpicture}
|
|
|
490 |
\begin{axis}[
|
|
|
491 |
xlabel={$n$},
|
|
|
492 |
x label style={at={(1.05,-0.05)}},
|
|
|
493 |
%ylabel={time in secs},
|
|
|
494 |
enlargelimits=false,
|
|
|
495 |
xtick={0,5,...,30},
|
|
|
496 |
xmax=33,
|
|
|
497 |
ymax=35,
|
|
|
498 |
ytick={0,5,...,30},
|
|
|
499 |
scaled ticks=false,
|
|
|
500 |
axis lines=left,
|
|
|
501 |
width=5cm,
|
|
|
502 |
height=4cm,
|
|
|
503 |
legend entries={Java 8},
|
|
|
504 |
legend pos=north west,
|
|
|
505 |
legend cell align=left]
|
|
|
506 |
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
|
|
|
507 |
\end{axis}
|
|
|
508 |
\end{tikzpicture}\\
|
|
|
509 |
\multicolumn{3}{c}{Graphs: Runtime for matching $(a^*)^*\,b$ with strings
|
|
|
510 |
of the form $\underbrace{aa..a}_{n}$.}
|
|
|
511 |
\end{tabular}
|
|
|
512 |
\end{center}
|
|
|
513 |
|
|
|
514 |
Why?
|
|
|
515 |
Using $\textit{NFA}$'s that can backtrack.
|
|
|
516 |
%TODO: what does it mean to do DFS BFS on NFA's
|
|
|
517 |
|
|
|
518 |
|
|
|
519 |
Then how about determinization?
|
|
|
520 |
\begin{itemize}
|
|
|
521 |
\item
|
|
|
522 |
Turning NFA's to DFA's can cause the size of the automata
|
|
|
523 |
to blow up exponentially.
|
|
|
524 |
\item
|
|
|
525 |
Want to extract submatch information.
|
|
|
526 |
For example,
|
|
|
527 |
$r_1 \cdot r_2$ matches $s$,
|
|
|
528 |
want to know $s = s_1@s_2$ where $s_i$
|
|
|
529 |
corresponds to $r_i$. Where $s_i$ might be the
|
|
|
530 |
attacker's ip address.
|
|
|
531 |
\item
|
|
|
532 |
Variants such as counting automaton exist.
|
|
|
533 |
But usually made super fast on a certain class
|
|
|
534 |
of regexes like bounded repetitions:
|
|
|
535 |
\begin{verbatim}
|
|
|
536 |
.*a.{100}
|
|
|
537 |
\end{verbatim}
|
|
|
538 |
On a lot of inputs this works very well.
|
|
|
539 |
On average good practical performance.
|
|
|
540 |
~10MiB per second.
|
|
|
541 |
But cannot be super fast on all inputs of regexes and strings,
|
|
|
542 |
can be imprecise (incorrect) when it comes to more complex regexes.
|
|
|
543 |
|
|
|
544 |
\end{itemize}
|
|
|
545 |
%TODO: real world example?
|
|
|
546 |
|
|
|
547 |
|
|
|
548 |
|
|
|
549 |
\subsection{derivatives}
|
|
|
550 |
Q:
|
|
|
551 |
Is there an efficient lexing algorithm with provable guarantees on
|
|
|
552 |
correctness and running time?
|
|
|
553 |
Brzozowski Derivatives\cite{Brzozowski1964}!
|
|
|
554 |
|
|
|
555 |
\begin{center}
|
|
|
556 |
\begin{tabular}{lcl}
|
|
|
557 |
$\nullable(\ZERO)$ & $\dn$ & $\mathit{false}$ \\
|
|
|
558 |
$\nullable(\ONE)$ & $\dn$ & $\mathit{true}$ \\
|
|
|
559 |
$\nullable(c)$ & $\dn$ & $\mathit{false}$ \\
|
|
|
560 |
$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
|
|
|
561 |
$\nullable(r_1\cdot r_2)$ & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
|
|
|
562 |
$\nullable(r^*)$ & $\dn$ & $\mathit{true}$ \\
|
|
|
563 |
\end{tabular}
|
|
|
564 |
\end{center}
|
|
|
565 |
|
|
|
566 |
|
|
|
567 |
|
|
|
568 |
This function simply tests whether the empty string is in $L(r)$.
|
|
|
569 |
He then defined
|
|
|
570 |
the following operation on regular expressions, written
|
|
|
571 |
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
|
|
|
572 |
|
|
|
573 |
\begin{center}
|
|
|
574 |
\begin{tabular}{lcl}
|
|
|
575 |
$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
576 |
$\ONE \backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
577 |
$d \backslash c$ & $\dn$ &
|
|
|
578 |
$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
|
|
|
579 |
$(r_1 + r_2)\backslash c$ & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
|
|
|
580 |
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
|
|
|
581 |
& & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
|
|
|
582 |
& & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
|
|
|
583 |
$(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\
|
|
|
584 |
\end{tabular}
|
|
|
585 |
\end{center}
|
|
|
586 |
|
|
|
587 |
|
|
|
588 |
|
|
|
589 |
|
|
|
590 |
\begin{ceqn}
|
|
|
591 |
\begin{equation}\label{graph:01}
|
|
|
592 |
\begin{tikzcd}
|
|
|
593 |
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] \\
|
|
|
594 |
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]
|
|
|
595 |
\end{tikzcd}
|
|
|
596 |
\end{equation}
|
|
|
597 |
\end{ceqn}
|
|
|
598 |
Nicely functional, correctness easily provable, but suffers
|
|
|
599 |
from large stack size with long strings, and
|
|
|
600 |
inability to perform even moderate simplification.
|
|
|
601 |
|
|
|
602 |
|
|
|
603 |
|
|
|
604 |
The Sulzmann and Lu's bit-coded algorithm:
|
|
|
605 |
\begin{figure}
|
|
|
606 |
\centering
|
|
|
607 |
\includegraphics[scale=0.3]{bitcoded_sulzmann.png}
|
|
|
608 |
\end{figure}
|
|
|
609 |
|
|
|
610 |
This one-phase algorithm is free from the burden of large stack usage:
|
|
|
611 |
|
|
|
612 |
\begin{center}
|
|
|
613 |
\begin{tikzpicture}[scale=2,node distance=1.9cm,
|
|
|
614 |
every node/.style={minimum size=7mm}]
|
|
|
615 |
\node (r0) {$r_0$};
|
|
|
616 |
\node (r1) [right=of r0]{$r_1$};
|
|
|
617 |
\draw[->,line width=0.2mm](r0)--(r1) node[above,midway] {$\backslash\,c_0$};
|
|
|
618 |
\node (r2) [right=of r1]{$r_2$};
|
|
|
619 |
\draw[->, line width = 0.2mm](r1)--(r2) node[above,midway] {$\backslash\,c_1$};
|
|
|
620 |
\node (rn) [right=of r2]{$r_n$};
|
|
|
621 |
\draw[dashed,->,line width=0.2mm](r2)--(rn) node[above,midway] {} ;
|
|
|
622 |
\draw (rn) node[anchor=west] {\;\raisebox{3mm}{$\nullable$}};
|
|
|
623 |
\node (bs) [below=of rn]{$bs$};
|
|
|
624 |
\draw[->,line width=0.2mm](rn) -- (bs);
|
|
|
625 |
\node (v0) [left=of bs] {$v_0$};
|
|
|
626 |
\draw[->,line width=0.2mm](bs)--(v0) node[below,midway] {$\textit{decode}$};
|
|
|
627 |
\draw (rn) node[anchor=north west] {\;\raisebox{-8mm}{$\textit{collect bits}$}};
|
|
|
628 |
\draw[->, line width=0.2mm](v0)--(r0) node[below, midway] {};
|
|
|
629 |
\end{tikzpicture}
|
|
|
630 |
\end{center}
|
|
|
631 |
|
|
|
632 |
|
|
|
633 |
|
|
|
634 |
This is functional code, and easily provable (proof by Urban and Ausaf).
|
|
|
635 |
|
|
|
636 |
But it suffers from exponential blows even with the simplification steps:
|
|
|
637 |
\begin{figure}
|
|
|
638 |
\centering
|
|
|
639 |
\includegraphics[scale= 0.3]{pics/nub_filter_simp.png}
|
|
|
640 |
\end{figure}
|
|
|
641 |
claim: Sulzmann and Lu claimed it linear $w.r.t$ input.
|
|
|
642 |
|
|
|
643 |
example that blows it up:
|
|
|
644 |
$(a+aa)^*$
|
|
|
645 |
\section{Contributions}
|
|
|
646 |
\subsection{Our contribution 1}
|
|
|
647 |
an improved version of the above algorithm that solves most blow up
|
|
|
648 |
cases, including the above example.
|
|
|
649 |
|
|
|
650 |
a formalized closed-form for string derivatives:
|
|
|
651 |
\[ (\sum rs) \backslash_s s = simp(\sum_{r \in rs}(r \backslash_s s)) \]
|
|
|
652 |
\[ (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' )\]
|
|
|
653 |
\[r0^* \backslash_s s = simp(\sum_{s' \in substr(s)} (r0 \backslash_s s') \cdot r0^*) \]
|
|
|
654 |
|
|
|
655 |
|
|
|
656 |
|
|
|
657 |
Also with a size guarantee that make sure the size of the derivatives
|
|
|
658 |
don't go up unbounded.
|
|
|
659 |
|
|
|
660 |
|
|
|
661 |
\begin{theorem}
|
|
|
662 |
Given a regular expression r, we have
|
|
|
663 |
\begin{center}
|
|
|
664 |
$\exists N_r.\; s.t. \;\forall s. \; |r \backslash_s s| < N_r$
|
|
|
665 |
\end{center}
|
|
|
666 |
\end{theorem}
|
|
|
667 |
|
|
|
668 |
The proof for this is using partial derivative's terms to bound it.
|
|
|
669 |
\begin{center}
|
|
|
670 |
\begin{tabular}{lcl}
|
|
|
671 |
$| \maxterms (\bsimp (a\cdot b) \backslash s)|$ & $=$ & $ |maxterms(\bsimp( (a\backslash s \cdot b) + \sum_{s'\in sl}(b\backslash s') ))|$\\
|
|
|
672 |
& $\leq$ & $| (\pder_{s@[c]} a ) \cdot b| + | (\bigcup_{s' \in Suf(s@[c])} (\pder_{s'} \; b))|$\\
|
|
|
673 |
& $=$ & $\awidth(a) + \awidth(b)$ \\
|
|
|
674 |
& $=$ & $\awidth(a+b)$
|
|
|
675 |
\end{tabular}
|
|
|
676 |
\end{center}
|
|
|
677 |
|
|
|
678 |
|
|
|
679 |
\subsection{Our Contribution 2}
|
|
|
680 |
more aggressive simplification that prunes away sub-parts
|
|
|
681 |
of a regex based on what terms has appeared before.
|
|
|
682 |
Which gives us a truly linear bound on the input length.
|
|
|
683 |
|
|
|
684 |
|
|
|
685 |
|
|
|
686 |
\section{To be completed}
|
|
|
687 |
|
|
|
688 |
benchmarking our algorithm against JFLEX
|
|
|
689 |
counting set automata, Silex, other main regex engines (incorporate their ideas such
|
|
|
690 |
as zippers and other data structures reducing memory use).
|
|
|
691 |
|
|
|
692 |
extend to back references.
|
|
|
693 |
|
|
|
694 |
|
|
|
695 |
|
|
|
696 |
|
|
|
697 |
|
|
|
698 |
|
|
|
699 |
\noindent These are clearly abysmal and possibly surprising results. One
|
|
|
700 |
would expect these systems to do much better than that---after all,
|
|
|
701 |
given a DFA and a string, deciding whether a string is matched by this
|
|
|
702 |
DFA should be linear in terms of the size of the regular expression and
|
|
|
703 |
the string?
|
|
|
704 |
|
|
|
705 |
Admittedly, the regular expression $(a^*)^*\,b$ is carefully chosen to
|
|
|
706 |
exhibit this super-linear behaviour. But unfortunately, such regular
|
|
|
707 |
expressions are not just a few outliers. They are actually
|
|
|
708 |
frequent enough to have a separate name created for
|
|
|
709 |
them---\emph{evil regular expressions}. In empiric work, Davis et al
|
|
|
710 |
report that they have found thousands of such evil regular expressions
|
|
|
711 |
in the JavaScript and Python ecosystems \cite{Davis18}. Static analysis
|
|
|
712 |
approach that is both sound and complete exists\cite{17Bir}, but the running
|
|
|
713 |
time on certain examples in the RegExLib and Snort regular expressions
|
|
|
714 |
libraries is unacceptable. Therefore the problem of efficiency still remains.
|
|
|
715 |
|
|
|
716 |
This superlinear blowup in matching algorithms sometimes causes
|
|
|
717 |
considerable grief in real life: for example on 20 July 2016 one evil
|
|
|
718 |
regular expression brought the webpage
|
|
|
719 |
\href{http://stackexchange.com}{Stack Exchange} to its
|
|
|
720 |
knees.\footnote{\url{https://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}}
|
|
|
721 |
In this instance, a regular expression intended to just trim white
|
|
|
722 |
spaces from the beginning and the end of a line actually consumed
|
|
|
723 |
massive amounts of CPU-resources---causing web servers to grind to a
|
|
|
724 |
halt. This happened when a post with 20,000 white spaces was submitted,
|
|
|
725 |
but importantly the white spaces were neither at the beginning nor at
|
|
|
726 |
the end. As a result, the regular expression matching engine needed to
|
|
|
727 |
backtrack over many choices. In this example, the time needed to process
|
|
|
728 |
the string was $O(n^2)$ with respect to the string length. This
|
|
|
729 |
quadratic overhead was enough for the homepage of Stack Exchange to
|
|
|
730 |
respond so slowly that the load balancer assumed there must be some
|
|
|
731 |
attack and therefore stopped the servers from responding to any
|
|
|
732 |
requests. This made the whole site become unavailable. Another very
|
|
|
733 |
recent example is a global outage of all Cloudflare servers on 2 July
|
|
|
734 |
2019. A poorly written regular expression exhibited exponential
|
|
|
735 |
behaviour and exhausted CPUs that serve HTTP traffic. Although the
|
|
|
736 |
outage had several causes, at the heart was a regular expression that
|
|
|
737 |
was used to monitor network
|
|
|
738 |
traffic.\footnote{\url{https://blog.cloudflare.com/details-of-the-cloudflare-outage-on-july-2-2019/}}
|
|
|
739 |
|
|
|
740 |
The underlying problem is that many ``real life'' regular expression
|
|
|
741 |
matching engines do not use DFAs for matching. This is because they
|
|
|
742 |
support regular expressions that are not covered by the classical
|
|
|
743 |
automata theory, and in this more general setting there are quite a few
|
|
|
744 |
research questions still unanswered and fast algorithms still need to be
|
|
|
745 |
developed (for example how to treat efficiently bounded repetitions, negation and
|
|
|
746 |
back-references).
|
|
|
747 |
%question: dfa can have exponential states. isn't this the actual reason why they do not use dfas?
|
|
|
748 |
%how do they avoid dfas exponential states if they use them for fast matching?
|
|
|
749 |
|
|
|
750 |
There is also another under-researched problem to do with regular
|
|
|
751 |
expressions and lexing, i.e.~the process of breaking up strings into
|
|
|
752 |
sequences of tokens according to some regular expressions. In this
|
|
|
753 |
setting one is not just interested in whether or not a regular
|
|
|
754 |
expression matches a string, but also in \emph{how}. Consider for
|
|
|
755 |
example a regular expression $r_{key}$ for recognising keywords such as
|
|
|
756 |
\textit{if}, \textit{then} and so on; and a regular expression $r_{id}$
|
|
|
757 |
for recognising identifiers (say, a single character followed by
|
|
|
758 |
characters or numbers). One can then form the compound regular
|
|
|
759 |
expression $(r_{key} + r_{id})^*$ and use it to tokenise strings. But
|
|
|
760 |
then how should the string \textit{iffoo} be tokenised? It could be
|
|
|
761 |
tokenised as a keyword followed by an identifier, or the entire string
|
|
|
762 |
as a single identifier. Similarly, how should the string \textit{if} be
|
|
|
763 |
tokenised? Both regular expressions, $r_{key}$ and $r_{id}$, would
|
|
|
764 |
``fire''---so is it an identifier or a keyword? While in applications
|
|
|
765 |
there is a well-known strategy to decide these questions, called POSIX
|
|
|
766 |
matching, only relatively recently precise definitions of what POSIX
|
|
|
767 |
matching actually means have been formalised
|
|
|
768 |
\cite{AusafDyckhoffUrban2016,OkuiSuzuki2010,Vansummeren2006}. Such a
|
|
|
769 |
definition has also been given by Sulzmann and Lu \cite{Sulzmann2014},
|
|
|
770 |
but the corresponding correctness proof turned out to be faulty
|
|
|
771 |
\cite{AusafDyckhoffUrban2016}. Roughly, POSIX matching means matching
|
|
|
772 |
the longest initial substring. In the case of a tie, the initial
|
|
|
773 |
sub-match is chosen according to some priorities attached to the regular
|
|
|
774 |
expressions (e.g.~keywords have a higher priority than identifiers).
|
|
|
775 |
This sounds rather simple, but according to Grathwohl et al \cite[Page
|
|
|
776 |
36]{CrashCourse2014} this is not the case. They wrote:
|
|
|
777 |
|
|
|
778 |
\begin{quote}
|
|
|
779 |
\it{}``The POSIX strategy is more complicated than the greedy because of
|
|
|
780 |
the dependence on information about the length of matched strings in the
|
|
|
781 |
various subexpressions.''
|
|
|
782 |
\end{quote}
|
|
|
783 |
|
|
|
784 |
\noindent
|
|
|
785 |
This is also supported by evidence collected by Kuklewicz
|
|
|
786 |
\cite{Kuklewicz} who noticed that a number of POSIX regular expression
|
|
|
787 |
matchers calculate incorrect results.
|
|
|
788 |
|
|
|
789 |
Our focus in this project is on an algorithm introduced by Sulzmann and
|
|
|
790 |
Lu in 2014 for regular expression matching according to the POSIX
|
|
|
791 |
strategy \cite{Sulzmann2014}. Their algorithm is based on an older
|
|
|
792 |
algorithm by Brzozowski from 1964 where he introduced the notion of
|
|
|
793 |
derivatives of regular expressions~\cite{Brzozowski1964}. We shall
|
|
|
794 |
briefly explain this algorithm next.
|
|
|
795 |
|
|
|
796 |
\section{The Algorithm by Brzozowski based on Derivatives of Regular
|
|
|
797 |
Expressions}
|
|
|
798 |
|
|
|
799 |
Suppose (basic) regular expressions are given by the following grammar:
|
|
|
800 |
\[ r ::= \ZERO \mid \ONE
|
|
|
801 |
\mid c
|
|
|
802 |
\mid r_1 \cdot r_2
|
|
|
803 |
\mid r_1 + r_2
|
|
|
804 |
\mid r^*
|
|
|
805 |
\]
|
|
|
806 |
|
|
|
807 |
\noindent
|
|
|
808 |
The intended meaning of the constructors is as follows: $\ZERO$
|
|
|
809 |
cannot match any string, $\ONE$ can match the empty string, the
|
|
|
810 |
character regular expression $c$ can match the character $c$, and so
|
|
|
811 |
on.
|
|
|
812 |
|
|
|
813 |
The ingenious contribution by Brzozowski is the notion of
|
|
|
814 |
\emph{derivatives} of regular expressions. The idea behind this
|
|
|
815 |
notion is as follows: suppose a regular expression $r$ can match a
|
|
|
816 |
string of the form $c\!::\! s$ (that is a list of characters starting
|
|
|
817 |
with $c$), what does the regular expression look like that can match
|
|
|
818 |
just $s$? Brzozowski gave a neat answer to this question. He started
|
|
|
819 |
with the definition of $nullable$:
|
|
|
820 |
\begin{center}
|
|
|
821 |
\begin{tabular}{lcl}
|
|
|
822 |
$\nullable(\ZERO)$ & $\dn$ & $\mathit{false}$ \\
|
|
|
823 |
$\nullable(\ONE)$ & $\dn$ & $\mathit{true}$ \\
|
|
|
824 |
$\nullable(c)$ & $\dn$ & $\mathit{false}$ \\
|
|
|
825 |
$\nullable(r_1 + r_2)$ & $\dn$ & $\nullable(r_1) \vee \nullable(r_2)$ \\
|
|
|
826 |
$\nullable(r_1\cdot r_2)$ & $\dn$ & $\nullable(r_1) \wedge \nullable(r_2)$ \\
|
|
|
827 |
$\nullable(r^*)$ & $\dn$ & $\mathit{true}$ \\
|
|
|
828 |
\end{tabular}
|
|
|
829 |
\end{center}
|
|
|
830 |
This function simply tests whether the empty string is in $L(r)$.
|
|
|
831 |
He then defined
|
|
|
832 |
the following operation on regular expressions, written
|
|
|
833 |
$r\backslash c$ (the derivative of $r$ w.r.t.~the character $c$):
|
|
|
834 |
|
|
|
835 |
\begin{center}
|
|
|
836 |
\begin{tabular}{lcl}
|
|
|
837 |
$\ZERO \backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
838 |
$\ONE \backslash c$ & $\dn$ & $\ZERO$\\
|
|
|
839 |
$d \backslash c$ & $\dn$ &
|
|
|
840 |
$\mathit{if} \;c = d\;\mathit{then}\;\ONE\;\mathit{else}\;\ZERO$\\
|
|
|
841 |
$(r_1 + r_2)\backslash c$ & $\dn$ & $r_1 \backslash c \,+\, r_2 \backslash c$\\
|
|
|
842 |
$(r_1 \cdot r_2)\backslash c$ & $\dn$ & $\mathit{if} \, nullable(r_1)$\\
|
|
|
843 |
& & $\mathit{then}\;(r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c$\\
|
|
|
844 |
& & $\mathit{else}\;(r_1\backslash c) \cdot r_2$\\
|
|
|
845 |
$(r^*)\backslash c$ & $\dn$ & $(r\backslash c) \cdot r^*$\\
|
|
|
846 |
\end{tabular}
|
|
|
847 |
\end{center}
|
|
|
848 |
|
|
|
849 |
%Assuming the classic notion of a
|
|
|
850 |
%\emph{language} of a regular expression, written $L(\_)$, t
|
|
|
851 |
|
|
|
852 |
\noindent
|
|
|
853 |
The main property of the derivative operation is that
|
|
|
854 |
|
|
|
855 |
\begin{center}
|
|
|
856 |
$c\!::\!s \in L(r)$ holds
|
|
|
857 |
if and only if $s \in L(r\backslash c)$.
|
|
|
858 |
\end{center}
|
|
|
859 |
|
|
|
860 |
\noindent
|
|
|
861 |
For us the main advantage is that derivatives can be
|
|
|
862 |
straightforwardly implemented in any functional programming language,
|
|
|
863 |
and are easily definable and reasoned about in theorem provers---the
|
|
|
864 |
definitions just consist of inductive datatypes and simple recursive
|
|
|
865 |
functions. Moreover, the notion of derivatives can be easily
|
|
|
866 |
generalised to cover extended regular expression constructors such as
|
|
|
867 |
the not-regular expression, written $\neg\,r$, or bounded repetitions
|
|
|
868 |
(for example $r^{\{n\}}$ and $r^{\{n..m\}}$), which cannot be so
|
|
|
869 |
straightforwardly realised within the classic automata approach.
|
|
|
870 |
For the moment however, we focus only on the usual basic regular expressions.
|
|
|
871 |
|
|
|
872 |
|
|
|
873 |
Now if we want to find out whether a string $s$ matches with a regular
|
|
|
874 |
expression $r$, we can build the derivatives of $r$ w.r.t.\ (in succession)
|
|
|
875 |
all the characters of the string $s$. Finally, test whether the
|
|
|
876 |
resulting regular expression can match the empty string. If yes, then
|
|
|
877 |
$r$ matches $s$, and no in the negative case. To implement this idea
|
|
|
878 |
we can generalise the derivative operation to strings like this:
|
|
|
879 |
|
|
|
880 |
\begin{center}
|
|
|
881 |
\begin{tabular}{lcl}
|
|
|
882 |
$r \backslash (c\!::\!s) $ & $\dn$ & $(r \backslash c) \backslash s$ \\
|
|
|
883 |
$r \backslash [\,] $ & $\dn$ & $r$
|
|
|
884 |
\end{tabular}
|
|
|
885 |
\end{center}
|
|
|
886 |
|
|
|
887 |
\noindent
|
|
|
888 |
and then define as regular-expression matching algorithm:
|
|
|
889 |
\[
|
|
|
890 |
match\;s\;r \;\dn\; nullable(r\backslash s)
|
|
|
891 |
\]
|
|
|
892 |
|
|
|
893 |
\noindent
|
|
|
894 |
This algorithm looks graphically as follows:
|
|
|
895 |
\begin{equation}\label{graph:*}
|
|
|
896 |
\begin{tikzcd}
|
|
|
897 |
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}
|
|
|
898 |
\end{tikzcd}
|
|
|
899 |
\end{equation}
|
|
|
900 |
|
|
|
901 |
\noindent
|
|
|
902 |
where we start with a regular expression $r_0$, build successive
|
|
|
903 |
derivatives until we exhaust the string and then use \textit{nullable}
|
|
|
904 |
to test whether the result can match the empty string. It can be
|
|
|
905 |
relatively easily shown that this matcher is correct (that is given
|
|
|
906 |
an $s = c_0...c_{n-1}$ and an $r_0$, it generates YES if and only if $s \in L(r_0)$).
|
|
|
907 |
|
|
|
908 |
|
|
|
909 |
\section{Values and the Algorithm by Sulzmann and Lu}
|
|
|
910 |
|
|
|
911 |
One limitation of Brzozowski's algorithm is that it only produces a
|
|
|
912 |
YES/NO answer for whether a string is being matched by a regular
|
|
|
913 |
expression. Sulzmann and Lu~\cite{Sulzmann2014} extended this algorithm
|
|
|
914 |
to allow generation of an actual matching, called a \emph{value} or
|
|
|
915 |
sometimes also \emph{lexical value}. These values and regular
|
|
|
916 |
expressions correspond to each other as illustrated in the following
|
|
|
917 |
table:
|
|
|
918 |
|
|
|
919 |
|
|
|
920 |
\begin{center}
|
|
|
921 |
\begin{tabular}{c@{\hspace{20mm}}c}
|
|
|
922 |
\begin{tabular}{@{}rrl@{}}
|
|
|
923 |
\multicolumn{3}{@{}l}{\textbf{Regular Expressions}}\medskip\\
|
|
|
924 |
$r$ & $::=$ & $\ZERO$\\
|
|
|
925 |
& $\mid$ & $\ONE$ \\
|
|
|
926 |
& $\mid$ & $c$ \\
|
|
|
927 |
& $\mid$ & $r_1 \cdot r_2$\\
|
|
|
928 |
& $\mid$ & $r_1 + r_2$ \\
|
|
|
929 |
\\
|
|
|
930 |
& $\mid$ & $r^*$ \\
|
|
|
931 |
\end{tabular}
|
|
|
932 |
&
|
|
|
933 |
\begin{tabular}{@{\hspace{0mm}}rrl@{}}
|
|
|
934 |
\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
|
|
|
935 |
$v$ & $::=$ & \\
|
|
|
936 |
& & $\Empty$ \\
|
|
|
937 |
& $\mid$ & $\Char(c)$ \\
|
|
|
938 |
& $\mid$ & $\Seq\,v_1\, v_2$\\
|
|
|
939 |
& $\mid$ & $\Left(v)$ \\
|
|
|
940 |
& $\mid$ & $\Right(v)$ \\
|
|
|
941 |
& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
|
|
|
942 |
\end{tabular}
|
|
|
943 |
\end{tabular}
|
|
|
944 |
\end{center}
|
|
|
945 |
|
|
|
946 |
\noindent
|
|
|
947 |
No value corresponds to $\ZERO$; $\Empty$ corresponds to $\ONE$;
|
|
|
948 |
$\Char$ to the character regular expression; $\Seq$ to the sequence
|
|
|
949 |
regular expression and so on. The idea of values is to encode a kind of
|
|
|
950 |
lexical value for how the sub-parts of a regular expression match the
|
|
|
951 |
sub-parts of a string. To see this, suppose a \emph{flatten} operation,
|
|
|
952 |
written $|v|$ for values. We can use this function to extract the
|
|
|
953 |
underlying string of a value $v$. For example, $|\mathit{Seq} \,
|
|
|
954 |
(\textit{Char x}) \, (\textit{Char y})|$ is the string $xy$. Using
|
|
|
955 |
flatten, we can describe how values encode lexical values: $\Seq\,v_1\,
|
|
|
956 |
v_2$ encodes a tree with two children nodes that tells how the string
|
|
|
957 |
$|v_1| @ |v_2|$ matches the regex $r_1 \cdot r_2$ whereby $r_1$ matches
|
|
|
958 |
the substring $|v_1|$ and, respectively, $r_2$ matches the substring
|
|
|
959 |
$|v_2|$. Exactly how these two are matched is contained in the children
|
|
|
960 |
nodes $v_1$ and $v_2$ of parent $\textit{Seq}$.
|
|
|
961 |
|
|
|
962 |
To give a concrete example of how values work, consider the string $xy$
|
|
|
963 |
and the regular expression $(x + (y + xy))^*$. We can view this regular
|
|
|
964 |
expression as a tree and if the string $xy$ is matched by two Star
|
|
|
965 |
``iterations'', then the $x$ is matched by the left-most alternative in
|
|
|
966 |
this tree and the $y$ by the right-left alternative. This suggests to
|
|
|
967 |
record this matching as
|
|
|
968 |
|
|
|
969 |
\begin{center}
|
|
|
970 |
$\Stars\,[\Left\,(\Char\,x), \Right(\Left(\Char\,y))]$
|
|
|
971 |
\end{center}
|
|
|
972 |
|
|
|
973 |
\noindent
|
|
|
974 |
where $\Stars \; [\ldots]$ records all the
|
|
|
975 |
iterations; and $\Left$, respectively $\Right$, which
|
|
|
976 |
alternative is used. The value for
|
|
|
977 |
matching $xy$ in a single ``iteration'', i.e.~the POSIX value,
|
|
|
978 |
would look as follows
|
|
|
979 |
|
|
|
980 |
\begin{center}
|
|
|
981 |
$\Stars\,[\Seq\,(\Char\,x)\,(\Char\,y)]$
|
|
|
982 |
\end{center}
|
|
|
983 |
|
|
|
984 |
\noindent
|
|
|
985 |
where $\Stars$ has only a single-element list for the single iteration
|
|
|
986 |
and $\Seq$ indicates that $xy$ is matched by a sequence regular
|
|
|
987 |
expression.
|
|
|
988 |
|
|
|
989 |
The contribution of Sulzmann and Lu is an extension of Brzozowski's
|
|
|
990 |
algorithm by a second phase (the first phase being building successive
|
|
|
991 |
derivatives---see \eqref{graph:*}). In this second phase, a POSIX value
|
|
|
992 |
is generated in case the regular expression matches the string.
|
|
|
993 |
Pictorially, the Sulzmann and Lu algorithm is as follows:
|
|
|
994 |
|
|
|
995 |
\begin{ceqn}
|
|
|
996 |
\begin{equation}\label{graph:2}
|
|
|
997 |
\begin{tikzcd}
|
|
|
998 |
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] \\
|
|
|
999 |
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]
|
|
|
1000 |
\end{tikzcd}
|
|
|
1001 |
\end{equation}
|
|
|
1002 |
\end{ceqn}
|
|
|
1003 |
|
|
|
1004 |
\noindent
|
|
|
1005 |
For convenience, we shall employ the following notations: the regular
|
|
|
1006 |
expression we start with is $r_0$, and the given string $s$ is composed
|
|
|
1007 |
of characters $c_0 c_1 \ldots c_{n-1}$. In the first phase from the
|
|
|
1008 |
left to right, we build the derivatives $r_1$, $r_2$, \ldots according
|
|
|
1009 |
to the characters $c_0$, $c_1$ until we exhaust the string and obtain
|
|
|
1010 |
the derivative $r_n$. We test whether this derivative is
|
|
|
1011 |
$\textit{nullable}$ or not. If not, we know the string does not match
|
|
|
1012 |
$r$ and no value needs to be generated. If yes, we start building the
|
|
|
1013 |
values incrementally by \emph{injecting} back the characters into the
|
|
|
1014 |
earlier values $v_n, \ldots, v_0$. This is the second phase of the
|
|
|
1015 |
algorithm from the right to left. For the first value $v_n$, we call the
|
|
|
1016 |
function $\textit{mkeps}$, which builds the lexical value
|
|
|
1017 |
for how the empty string has been matched by the (nullable) regular
|
|
|
1018 |
expression $r_n$. This function is defined as
|
|
|
1019 |
|
|
|
1020 |
\begin{center}
|
|
|
1021 |
\begin{tabular}{lcl}
|
|
|
1022 |
$\mkeps(\ONE)$ & $\dn$ & $\Empty$ \\
|
|
|
1023 |
$\mkeps(r_{1}+r_{2})$ & $\dn$
|
|
|
1024 |
& \textit{if} $\nullable(r_{1})$\\
|
|
|
1025 |
& & \textit{then} $\Left(\mkeps(r_{1}))$\\
|
|
|
1026 |
& & \textit{else} $\Right(\mkeps(r_{2}))$\\
|
|
|
1027 |
$\mkeps(r_1\cdot r_2)$ & $\dn$ & $\Seq\,(\mkeps\,r_1)\,(\mkeps\,r_2)$\\
|
|
|
1028 |
$mkeps(r^*)$ & $\dn$ & $\Stars\,[]$
|
|
|
1029 |
\end{tabular}
|
|
|
1030 |
\end{center}
|
|
|
1031 |
|
|
|
1032 |
|
|
|
1033 |
\noindent There are no cases for $\ZERO$ and $c$, since
|
|
|
1034 |
these regular expression cannot match the empty string. Note
|
|
|
1035 |
also that in case of alternatives we give preference to the
|
|
|
1036 |
regular expression on the left-hand side. This will become
|
|
|
1037 |
important later on about what value is calculated.
|
|
|
1038 |
|
|
|
1039 |
After the $\mkeps$-call, we inject back the characters one by one in order to build
|
|
|
1040 |
the lexical value $v_i$ for how the regex $r_i$ matches the string $s_i$
|
|
|
1041 |
($s_i = c_i \ldots c_{n-1}$ ) from the previous lexical value $v_{i+1}$.
|
|
|
1042 |
After injecting back $n$ characters, we get the lexical value for how $r_0$
|
|
|
1043 |
matches $s$. For this Sulzmann and Lu defined a function that reverses
|
|
|
1044 |
the ``chopping off'' of characters during the derivative phase. The
|
|
|
1045 |
corresponding function is called \emph{injection}, written
|
|
|
1046 |
$\textit{inj}$; it takes three arguments: the first one is a regular
|
|
|
1047 |
expression ${r_{i-1}}$, before the character is chopped off, the second
|
|
|
1048 |
is a character ${c_{i-1}}$, the character we want to inject and the
|
|
|
1049 |
third argument is the value ${v_i}$, into which one wants to inject the
|
|
|
1050 |
character (it corresponds to the regular expression after the character
|
|
|
1051 |
has been chopped off). The result of this function is a new value. The
|
|
|
1052 |
definition of $\textit{inj}$ is as follows:
|
|
|
1053 |
|
|
|
1054 |
\begin{center}
|
|
|
1055 |
\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}
|
|
|
1056 |
$\textit{inj}\,(c)\,c\,Empty$ & $\dn$ & $Char\,c$\\
|
|
|
1057 |
$\textit{inj}\,(r_1 + r_2)\,c\,\Left(v)$ & $\dn$ & $\Left(\textit{inj}\,r_1\,c\,v)$\\
|
|
|
1058 |
$\textit{inj}\,(r_1 + r_2)\,c\,Right(v)$ & $\dn$ & $Right(\textit{inj}\,r_2\,c\,v)$\\
|
|
|
1059 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Seq(v_1,v_2)$ & $\dn$ & $Seq(\textit{inj}\,r_1\,c\,v_1,v_2)$\\
|
|
|
1060 |
$\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)$\\
|
|
|
1061 |
$\textit{inj}\,(r_1 \cdot r_2)\,c\,Right(v)$ & $\dn$ & $Seq(\textit{mkeps}(r_1),\textit{inj}\,r_2\,c\,v)$\\
|
|
|
1062 |
$\textit{inj}\,(r^*)\,c\,Seq(v,Stars\,vs)$ & $\dn$ & $Stars((\textit{inj}\,r\,c\,v)\,::\,vs)$\\
|
|
|
1063 |
\end{tabular}
|
|
|
1064 |
\end{center}
|
|
|
1065 |
|
|
|
1066 |
\noindent This definition is by recursion on the ``shape'' of regular
|
|
|
1067 |
expressions and values. To understands this definition better consider
|
|
|
1068 |
the situation when we build the derivative on regular expression $r_{i-1}$.
|
|
|
1069 |
For this we chop off a character from $r_{i-1}$ to form $r_i$. This leaves a
|
|
|
1070 |
``hole'' in $r_i$ and its corresponding value $v_i$.
|
|
|
1071 |
To calculate $v_{i-1}$, we need to
|
|
|
1072 |
locate where that hole is and fill it.
|
|
|
1073 |
We can find this location by
|
|
|
1074 |
comparing $r_{i-1}$ and $v_i$. For instance, if $r_{i-1}$ is of shape
|
|
|
1075 |
$r_a \cdot r_b$, and $v_i$ is of shape $\Left(Seq(v_1,v_2))$, we know immediately that
|
|
|
1076 |
%
|
|
|
1077 |
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b \,+\, r_b\backslash c,\]
|
|
|
1078 |
|
|
|
1079 |
\noindent
|
|
|
1080 |
otherwise if $r_a$ is not nullable,
|
|
|
1081 |
\[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b,\]
|
|
|
1082 |
|
|
|
1083 |
\noindent
|
|
|
1084 |
the value $v_i$ should be $\Seq(\ldots)$, contradicting the fact that
|
|
|
1085 |
$v_i$ is actually of shape $\Left(\ldots)$. Furthermore, since $v_i$ is of shape
|
|
|
1086 |
$\Left(\ldots)$ instead of $\Right(\ldots)$, we know that the left
|
|
|
1087 |
branch of \[ (r_a \cdot r_b)\backslash c =
|
|
|
1088 |
\bold{\underline{ (r_a\backslash c) \cdot r_b} }\,+\, r_b\backslash c,\](underlined)
|
|
|
1089 |
is taken instead of the right one. This means $c$ is chopped off
|
|
|
1090 |
from $r_a$ rather than $r_b$.
|
|
|
1091 |
We have therefore found out
|
|
|
1092 |
that the hole will be on $r_a$. So we recursively call $\inj\,
|
|
|
1093 |
r_a\,c\,v_a$ to fill that hole in $v_a$. After injection, the value
|
|
|
1094 |
$v_i$ for $r_i = r_a \cdot r_b$ should be $\Seq\,(\inj\,r_a\,c\,v_a)\,v_b$.
|
|
|
1095 |
Other clauses can be understood in a similar way.
|
|
|
1096 |
|
|
|
1097 |
%\comment{Other word: insight?}
|
|
|
1098 |
The following example gives an insight of $\textit{inj}$'s effect and
|
|
|
1099 |
how Sulzmann and Lu's algorithm works as a whole. Suppose we have a
|
|
|
1100 |
regular expression $((((a+b)+ab)+c)+abc)^*$, and want to match it
|
|
|
1101 |
against the string $abc$ (when $abc$ is written as a regular expression,
|
|
|
1102 |
the standard way of expressing it is $a \cdot (b \cdot c)$. But we
|
|
|
1103 |
usually omit the parentheses and dots here for better readability. This
|
|
|
1104 |
algorithm returns a POSIX value, which means it will produce the longest
|
|
|
1105 |
matching. Consequently, it matches the string $abc$ in one star
|
|
|
1106 |
iteration, using the longest alternative $abc$ in the sub-expression (we shall use $r$ to denote this
|
|
|
1107 |
sub-expression for conciseness):
|
|
|
1108 |
|
|
|
1109 |
\[((((a+b)+ab)+c)+\underbrace{abc}_r)\]
|
|
|
1110 |
|
|
|
1111 |
\noindent
|
|
|
1112 |
Before $\textit{inj}$ is called, our lexer first builds derivative using
|
|
|
1113 |
string $abc$ (we simplified some regular expressions like $\ZERO \cdot
|
|
|
1114 |
b$ to $\ZERO$ for conciseness; we also omit parentheses if they are
|
|
|
1115 |
clear from the context):
|
|
|
1116 |
|
|
|
1117 |
%Similarly, we allow
|
|
|
1118 |
%$\textit{ALT}$ to take a list of regular expressions as an argument
|
|
|
1119 |
%instead of just 2 operands to reduce the nested depth of
|
|
|
1120 |
%$\textit{ALT}$
|
|
|
1121 |
|
|
|
1122 |
\begin{center}
|
|
|
1123 |
\begin{tabular}{lcl}
|
|
|
1124 |
$r^*$ & $\xrightarrow{\backslash a}$ & $r_1 = (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r^*$\\
|
|
|
1125 |
& $\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^*$\\
|
|
|
1126 |
& $\xrightarrow{\backslash c}$ & $r_3 = ((\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot \ONE) \cdot r^* + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^*) + $\\
|
|
|
1127 |
& & $\phantom{r_3 = (} ((\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^* + (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^* )$
|
|
|
1128 |
\end{tabular}
|
|
|
1129 |
\end{center}
|
|
|
1130 |
|
|
|
1131 |
\noindent
|
|
|
1132 |
In case $r_3$ is nullable, we can call $\textit{mkeps}$
|
|
|
1133 |
to construct a lexical value for how $r_3$ matched the string $abc$.
|
|
|
1134 |
This function gives the following value $v_3$:
|
|
|
1135 |
|
|
|
1136 |
|
|
|
1137 |
\begin{center}
|
|
|
1138 |
$\Left(\Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty,\Empty))), \Stars [])))$
|
|
|
1139 |
\end{center}
|
|
|
1140 |
The outer $\Left(\Left(\ldots))$ tells us the leftmost nullable part of $r_3$(underlined):
|
|
|
1141 |
|
|
|
1142 |
\begin{center}
|
|
|
1143 |
\begin{tabular}{l@{\hspace{2mm}}l}
|
|
|
1144 |
& $\big(\underline{(\ZERO+\ZERO+\ZERO+ \ZERO+ \ONE \cdot \ONE \cdot \ONE) \cdot r^*}
|
|
|
1145 |
\;+\; (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^*\big)$ \smallskip\\
|
|
|
1146 |
$+$ & $\big((\ZERO+\ONE+\ZERO + \ZERO + \ZERO) \cdot r^*
|
|
|
1147 |
\;+\; (\ZERO+\ZERO+\ZERO + \ONE + \ZERO) \cdot r^* \big)$
|
|
|
1148 |
\end{tabular}
|
|
|
1149 |
\end{center}
|
|
|
1150 |
|
|
|
1151 |
\noindent
|
|
|
1152 |
Note that the leftmost location of term $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot \ONE \cdot
|
|
|
1153 |
\ONE) \cdot r^*$ (which corresponds to the initial sub-match $abc$) allows
|
|
|
1154 |
$\textit{mkeps}$ to pick it up because $\textit{mkeps}$ is defined to always choose the
|
|
|
1155 |
left one when it is nullable. In the case of this example, $abc$ is
|
|
|
1156 |
preferred over $a$ or $ab$. This $\Left(\Left(\ldots))$ location is
|
|
|
1157 |
generated by two applications of the splitting clause
|
|
|
1158 |
|
|
|
1159 |
\begin{center}
|
|
|
1160 |
$(r_1 \cdot r_2)\backslash c \;\;(when \; r_1 \; nullable) \, = (r_1\backslash c) \cdot r_2 \,+\, r_2\backslash c.$
|
|
|
1161 |
\end{center}
|
|
|
1162 |
|
|
|
1163 |
\noindent
|
|
|
1164 |
By this clause, we put $r_1 \backslash c \cdot r_2 $ at the
|
|
|
1165 |
$\textit{front}$ and $r_2 \backslash c$ at the $\textit{back}$. This
|
|
|
1166 |
allows $\textit{mkeps}$ to always pick up among two matches the one with a longer
|
|
|
1167 |
initial sub-match. Removing the outside $\Left(\Left(...))$, the inside
|
|
|
1168 |
sub-value
|
|
|
1169 |
|
|
|
1170 |
\begin{center}
|
|
|
1171 |
$\Seq(\Right(\Seq(\Empty, \Seq(\Empty, \Empty))), \Stars [])$
|
|
|
1172 |
\end{center}
|
|
|
1173 |
|
|
|
1174 |
\noindent
|
|
|
1175 |
tells us how the empty string $[]$ is matched with $(\ZERO+\ZERO+\ZERO + \ZERO + \ONE \cdot
|
|
|
1176 |
\ONE \cdot \ONE) \cdot r^*$. We match $[]$ by a sequence of two nullable regular
|
|
|
1177 |
expressions. The first one is an alternative, we take the rightmost
|
|
|
1178 |
alternative---whose language contains the empty string. The second
|
|
|
1179 |
nullable regular expression is a Kleene star. $\Stars$ tells us how it
|
|
|
1180 |
generates the nullable regular expression: by 0 iterations to form
|
|
|
1181 |
$\ONE$. Now $\textit{inj}$ injects characters back and incrementally
|
|
|
1182 |
builds a lexical value based on $v_3$. Using the value $v_3$, the character
|
|
|
1183 |
c, and the regular expression $r_2$, we can recover how $r_2$ matched
|
|
|
1184 |
the string $[c]$ : $\textit{inj} \; r_2 \; c \; v_3$ gives us
|
|
|
1185 |
\begin{center}
|
|
|
1186 |
$v_2 = \Left(\Seq(\Right(\Seq(\Empty, \Seq(\Empty, c))), \Stars [])),$
|
|
|
1187 |
\end{center}
|
|
|
1188 |
which tells us how $r_2$ matched $[c]$. After this we inject back the character $b$, and get
|
|
|
1189 |
\begin{center}
|
|
|
1190 |
$v_1 = \Seq(\Right(\Seq(\Empty, \Seq(b, c))), \Stars [])$
|
|
|
1191 |
\end{center}
|
|
|
1192 |
for how
|
|
|
1193 |
\begin{center}
|
|
|
1194 |
$r_1= (\ONE+\ZERO+\ONE \cdot b + \ZERO + \ONE \cdot b \cdot c) \cdot r*$
|
|
|
1195 |
\end{center}
|
|
|
1196 |
matched the string $bc$ before it split into two substrings.
|
|
|
1197 |
Finally, after injecting character $a$ back to $v_1$,
|
|
|
1198 |
we get the lexical value tree
|
|
|
1199 |
\begin{center}
|
|
|
1200 |
$v_0= \Stars [\Right(\Seq(a, \Seq(b, c)))]$
|
|
|
1201 |
\end{center}
|
|
|
1202 |
for how $r$ matched $abc$. This completes the algorithm.
|
|
|
1203 |
|
|
|
1204 |
%We omit the details of injection function, which is provided by Sulzmann and Lu's paper \cite{Sulzmann2014}.
|
|
|
1205 |
Readers might have noticed that the lexical value information is actually
|
|
|
1206 |
already available when doing derivatives. For example, immediately after
|
|
|
1207 |
the operation $\backslash a$ we know that if we want to match a string
|
|
|
1208 |
that starts with $a$, we can either take the initial match to be
|
|
|
1209 |
|
|
|
1210 |
\begin{center}
|
|
|
1211 |
\begin{enumerate}
|
|
|
1212 |
\item[1)] just $a$ or
|
|
|
1213 |
\item[2)] string $ab$ or
|
|
|
1214 |
\item[3)] string $abc$.
|
|
|
1215 |
\end{enumerate}
|
|
|
1216 |
\end{center}
|
|
|
1217 |
|
|
|
1218 |
\noindent
|
|
|
1219 |
In order to differentiate between these choices, we just need to
|
|
|
1220 |
remember their positions---$a$ is on the left, $ab$ is in the middle ,
|
|
|
1221 |
and $abc$ is on the right. Which of these alternatives is chosen
|
|
|
1222 |
later does not affect their relative position because the algorithm does
|
|
|
1223 |
not change this order. If this parsing information can be determined and
|
|
|
1224 |
does not change because of later derivatives, there is no point in
|
|
|
1225 |
traversing this information twice. This leads to an optimisation---if we
|
|
|
1226 |
store the information for lexical values inside the regular expression,
|
|
|
1227 |
update it when we do derivative on them, and collect the information
|
|
|
1228 |
when finished with derivatives and call $\textit{mkeps}$ for deciding which
|
|
|
1229 |
branch is POSIX, we can generate the lexical value in one pass, instead of
|
|
|
1230 |
doing the rest $n$ injections. This leads to Sulzmann and Lu's novel
|
|
|
1231 |
idea of using bitcodes in derivatives.
|
|
|
1232 |
|
|
|
1233 |
In the next section, we shall focus on the bitcoded algorithm and the
|
|
|
1234 |
process of simplification of regular expressions. This is needed in
|
|
|
1235 |
order to obtain \emph{fast} versions of the Brzozowski's, and Sulzmann
|
|
|
1236 |
and Lu's algorithms. This is where the PhD-project aims to advance the
|
|
|
1237 |
state-of-the-art.
|
|
|
1238 |
|
|
|
1239 |
|
|
|
1240 |
\section{Simplification of Regular Expressions}
|
|
|
1241 |
|
|
|
1242 |
Using bitcodes to guide parsing is not a novel idea. It was applied to
|
|
|
1243 |
context free grammars and then adapted by Henglein and Nielson for
|
|
|
1244 |
efficient regular expression lexing using DFAs~\cite{nielson11bcre}.
|
|
|
1245 |
Sulzmann and Lu took this idea of bitcodes a step further by integrating
|
|
|
1246 |
bitcodes into derivatives. The reason why we want to use bitcodes in
|
|
|
1247 |
this project is that we want to introduce more aggressive simplification
|
|
|
1248 |
rules in order to keep the size of derivatives small throughout. This is
|
|
|
1249 |
because the main drawback of building successive derivatives according
|
|
|
1250 |
to Brzozowski's definition is that they can grow very quickly in size.
|
|
|
1251 |
This is mainly due to the fact that the derivative operation generates
|
|
|
1252 |
often ``useless'' $\ZERO$s and $\ONE$s in derivatives. As a result, if
|
|
|
1253 |
implemented naively both algorithms by Brzozowski and by Sulzmann and Lu
|
|
|
1254 |
are excruciatingly slow. For example when starting with the regular
|
|
|
1255 |
expression $(a + aa)^*$ and building 12 successive derivatives
|
|
|
1256 |
w.r.t.~the character $a$, one obtains a derivative regular expression
|
|
|
1257 |
with more than 8000 nodes (when viewed as a tree). Operations like
|
|
|
1258 |
$\textit{der}$ and $\nullable$ need to traverse such trees and
|
|
|
1259 |
consequently the bigger the size of the derivative the slower the
|
|
|
1260 |
algorithm.
|
|
|
1261 |
|
|
|
1262 |
Fortunately, one can simplify regular expressions after each derivative
|
|
|
1263 |
step. Various simplifications of regular expressions are possible, such
|
|
|
1264 |
as the simplification of $\ZERO + r$, $r + \ZERO$, $\ONE\cdot r$, $r
|
|
|
1265 |
\cdot \ONE$, and $r + r$ to just $r$. These simplifications do not
|
|
|
1266 |
affect the answer for whether a regular expression matches a string or
|
|
|
1267 |
not, but fortunately also do not affect the POSIX strategy of how
|
|
|
1268 |
regular expressions match strings---although the latter is much harder
|
|
|
1269 |
to establish. Some initial results in this regard have been
|
|
|
1270 |
obtained in \cite{AusafDyckhoffUrban2016}.
|
|
|
1271 |
|
|
|
1272 |
Unfortunately, the simplification rules outlined above are not
|
|
|
1273 |
sufficient to prevent a size explosion in all cases. We
|
|
|
1274 |
believe a tighter bound can be achieved that prevents an explosion in
|
|
|
1275 |
\emph{all} cases. Such a tighter bound is suggested by work of Antimirov who
|
|
|
1276 |
proved that (partial) derivatives can be bound by the number of
|
|
|
1277 |
characters contained in the initial regular expression
|
|
|
1278 |
\cite{Antimirov95}. He defined the \emph{partial derivatives} of regular
|
|
|
1279 |
expressions as follows:
|
|
|
1280 |
|
|
|
1281 |
\begin{center}
|
|
|
1282 |
\begin{tabular}{lcl}
|
|
|
1283 |
$\textit{pder} \; c \; \ZERO$ & $\dn$ & $\emptyset$\\
|
|
|
1284 |
$\textit{pder} \; c \; \ONE$ & $\dn$ & $\emptyset$ \\
|
|
|
1285 |
$\textit{pder} \; c \; d$ & $\dn$ & $\textit{if} \; c \,=\, d \; \{ \ONE \} \; \textit{else} \; \emptyset$ \\
|
|
|
1286 |
$\textit{pder} \; c \; r_1+r_2$ & $\dn$ & $pder \; c \; r_1 \cup pder \; c \; r_2$ \\
|
|
|
1287 |
$\textit{pder} \; c \; r_1 \cdot r_2$ & $\dn$ & $\textit{if} \; nullable \; r_1 $\\
|
|
|
1288 |
& & $\textit{then} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} \cup pder \; c \; r_2 \;$\\
|
|
|
1289 |
& & $\textit{else} \; \{ r \cdot r_2 \mid r \in pder \; c \; r_1 \} $ \\
|
|
|
1290 |
$\textit{pder} \; c \; r^*$ & $\dn$ & $ \{ r' \cdot r^* \mid r' \in pder \; c \; r \} $ \\
|
|
|
1291 |
\end{tabular}
|
|
|
1292 |
\end{center}
|
|
|
1293 |
|
|
|
1294 |
\noindent
|
|
|
1295 |
A partial derivative of a regular expression $r$ is essentially a set of
|
|
|
1296 |
regular expressions that are either $r$'s children expressions or a
|
|
|
1297 |
concatenation of them. Antimirov has proved a tight bound of the sum of
|
|
|
1298 |
the size of \emph{all} partial derivatives no matter what the string
|
|
|
1299 |
looks like. Roughly speaking the size sum will be at most cubic in the
|
|
|
1300 |
size of the regular expression.
|
|
|
1301 |
|
|
|
1302 |
If we want the size of derivatives in Sulzmann and Lu's algorithm to
|
|
|
1303 |
stay below this bound, we would need more aggressive simplifications.
|
|
|
1304 |
Essentially we need to delete useless $\ZERO$s and $\ONE$s, as well as
|
|
|
1305 |
deleting duplicates whenever possible. For example, the parentheses in
|
|
|
1306 |
$(a+b) \cdot c + bc$ can be opened up to get $a\cdot c + b \cdot c + b
|
|
|
1307 |
\cdot c$, and then simplified to just $a \cdot c + b \cdot c$. Another
|
|
|
1308 |
example is simplifying $(a^*+a) + (a^*+ \ONE) + (a +\ONE)$ to just
|
|
|
1309 |
$a^*+a+\ONE$. Adding these more aggressive simplification rules helps us
|
|
|
1310 |
to achieve the same size bound as that of the partial derivatives.
|
|
|
1311 |
|
|
|
1312 |
In order to implement the idea of ``spilling out alternatives'' and to
|
|
|
1313 |
make them compatible with the $\text{inj}$-mechanism, we use
|
|
|
1314 |
\emph{bitcodes}. Bits and bitcodes (lists of bits) are just:
|
|
|
1315 |
|
|
|
1316 |
%This allows us to prove a tight
|
|
|
1317 |
%bound on the size of regular expression during the running time of the
|
|
|
1318 |
%algorithm if we can establish the connection between our simplification
|
|
|
1319 |
%rules and partial derivatives.
|
|
|
1320 |
|
|
|
1321 |
%We believe, and have generated test
|
|
|
1322 |
%data, that a similar bound can be obtained for the derivatives in
|
|
|
1323 |
%Sulzmann and Lu's algorithm. Let us give some details about this next.
|
|
|
1324 |
|
|
|
1325 |
|
|
|
1326 |
\begin{center}
|
|
|
1327 |
$b ::= S \mid Z \qquad
|
|
|
1328 |
bs ::= [] \mid b:bs
|
|
|
1329 |
$
|
|
|
1330 |
\end{center}
|
|
|
1331 |
|
|
|
1332 |
\noindent
|
|
|
1333 |
The $S$ and $Z$ are arbitrary names for the bits in order to avoid
|
|
|
1334 |
confusion with the regular expressions $\ZERO$ and $\ONE$. Bitcodes (or
|
|
|
1335 |
bit-lists) can be used to encode values (or incomplete values) in a
|
|
|
1336 |
compact form. This can be straightforwardly seen in the following
|
|
|
1337 |
coding function from values to bitcodes:
|
|
|
1338 |
|
|
|
1339 |
\begin{center}
|
|
|
1340 |
\begin{tabular}{lcl}
|
|
|
1341 |
$\textit{code}(\Empty)$ & $\dn$ & $[]$\\
|
|
|
1342 |
$\textit{code}(\Char\,c)$ & $\dn$ & $[]$\\
|
|
|
1343 |
$\textit{code}(\Left\,v)$ & $\dn$ & $\Z :: code(v)$\\
|
|
|
1344 |
$\textit{code}(\Right\,v)$ & $\dn$ & $\S :: code(v)$\\
|
|
|
1345 |
$\textit{code}(\Seq\,v_1\,v_2)$ & $\dn$ & $code(v_1) \,@\, code(v_2)$\\
|
|
|
1346 |
$\textit{code}(\Stars\,[])$ & $\dn$ & $[\Z]$\\
|
|
|
1347 |
$\textit{code}(\Stars\,(v\!::\!vs))$ & $\dn$ & $\S :: code(v) \;@\;
|
|
|
1348 |
code(\Stars\,vs)$
|
|
|
1349 |
\end{tabular}
|
|
|
1350 |
\end{center}
|
|
|
1351 |
|
|
|
1352 |
\noindent
|
|
|
1353 |
Here $\textit{code}$ encodes a value into a bitcodes by converting
|
|
|
1354 |
$\Left$ into $\Z$, $\Right$ into $\S$, the start point of a non-empty
|
|
|
1355 |
star iteration into $\S$, and the border where a local star terminates
|
|
|
1356 |
into $\Z$. This coding is lossy, as it throws away the information about
|
|
|
1357 |
characters, and also does not encode the ``boundary'' between two
|
|
|
1358 |
sequence values. Moreover, with only the bitcode we cannot even tell
|
|
|
1359 |
whether the $\S$s and $\Z$s are for $\Left/\Right$ or $\Stars$. The
|
|
|
1360 |
reason for choosing this compact way of storing information is that the
|
|
|
1361 |
relatively small size of bits can be easily manipulated and ``moved
|
|
|
1362 |
around'' in a regular expression. In order to recover values, we will
|
|
|
1363 |
need the corresponding regular expression as an extra information. This
|
|
|
1364 |
means the decoding function is defined as:
|
|
|
1365 |
|
|
|
1366 |
|
|
|
1367 |
%\begin{definition}[Bitdecoding of Values]\mbox{}
|
|
|
1368 |
\begin{center}
|
|
|
1369 |
\begin{tabular}{@{}l@{\hspace{1mm}}c@{\hspace{1mm}}l@{}}
|
|
|
1370 |
$\textit{decode}'\,bs\,(\ONE)$ & $\dn$ & $(\Empty, bs)$\\
|
|
|
1371 |
$\textit{decode}'\,bs\,(c)$ & $\dn$ & $(\Char\,c, bs)$\\
|
|
|
1372 |
$\textit{decode}'\,(\Z\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
|
|
|
1373 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}\;
|
|
|
1374 |
(\Left\,v, bs_1)$\\
|
|
|
1375 |
$\textit{decode}'\,(\S\!::\!bs)\;(r_1 + r_2)$ & $\dn$ &
|
|
|
1376 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r_2\;\textit{in}\;
|
|
|
1377 |
(\Right\,v, bs_1)$\\
|
|
|
1378 |
$\textit{decode}'\,bs\;(r_1\cdot r_2)$ & $\dn$ &
|
|
|
1379 |
$\textit{let}\,(v_1, bs_1) = \textit{decode}'\,bs\,r_1\;\textit{in}$\\
|
|
|
1380 |
& & $\textit{let}\,(v_2, bs_2) = \textit{decode}'\,bs_1\,r_2$\\
|
|
|
1381 |
& & \hspace{35mm}$\textit{in}\;(\Seq\,v_1\,v_2, bs_2)$\\
|
|
|
1382 |
$\textit{decode}'\,(\Z\!::\!bs)\,(r^*)$ & $\dn$ & $(\Stars\,[], bs)$\\
|
|
|
1383 |
$\textit{decode}'\,(\S\!::\!bs)\,(r^*)$ & $\dn$ &
|
|
|
1384 |
$\textit{let}\,(v, bs_1) = \textit{decode}'\,bs\,r\;\textit{in}$\\
|
|
|
1385 |
& & $\textit{let}\,(\Stars\,vs, bs_2) = \textit{decode}'\,bs_1\,r^*$\\
|
|
|
1386 |
& & \hspace{35mm}$\textit{in}\;(\Stars\,v\!::\!vs, bs_2)$\bigskip\\
|
|
|
1387 |
|
|
|
1388 |
$\textit{decode}\,bs\,r$ & $\dn$ &
|
|
|
1389 |
$\textit{let}\,(v, bs') = \textit{decode}'\,bs\,r\;\textit{in}$\\
|
|
|
1390 |
& & $\textit{if}\;bs' = []\;\textit{then}\;\textit{Some}\,v\;
|
|
|
1391 |
\textit{else}\;\textit{None}$
|
|
|
1392 |
\end{tabular}
|
|
|
1393 |
\end{center}
|
|
|
1394 |
%\end{definition}
|
|
|
1395 |
|
|
|
1396 |
Sulzmann and Lu's integrated the bitcodes into regular expressions to
|
|
|
1397 |
create annotated regular expressions \cite{Sulzmann2014}.
|
|
|
1398 |
\emph{Annotated regular expressions} are defined by the following
|
|
|
1399 |
grammar:%\comment{ALTS should have an $as$ in the definitions, not just $a_1$ and $a_2$}
|
|
|
1400 |
|
|
|
1401 |
\begin{center}
|
|
|
1402 |
\begin{tabular}{lcl}
|
|
|
1403 |
$\textit{a}$ & $::=$ & $\textit{ZERO}$\\
|
|
|
1404 |
& $\mid$ & $\textit{ONE}\;\;bs$\\
|
|
|
1405 |
& $\mid$ & $\textit{CHAR}\;\;bs\,c$\\
|
|
|
1406 |
& $\mid$ & $\textit{ALTS}\;\;bs\,as$\\
|
|
|
1407 |
& $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\
|
|
|
1408 |
& $\mid$ & $\textit{STAR}\;\;bs\,a$
|
|
|
1409 |
\end{tabular}
|
|
|
1410 |
\end{center}
|
|
|
1411 |
%(in \textit{ALTS})
|
|
|
1412 |
|
|
|
1413 |
\noindent
|
|
|
1414 |
where $bs$ stands for bitcodes, $a$ for $\bold{a}$nnotated regular
|
|
|
1415 |
expressions and $as$ for a list of annotated regular expressions.
|
|
|
1416 |
The alternative constructor($\textit{ALTS}$) has been generalized to
|
|
|
1417 |
accept a list of annotated regular expressions rather than just 2.
|
|
|
1418 |
We will show that these bitcodes encode information about
|
|
|
1419 |
the (POSIX) value that should be generated by the Sulzmann and Lu
|
|
|
1420 |
algorithm.
|
|
|
1421 |
|
|
|
1422 |
|
|
|
1423 |
To do lexing using annotated regular expressions, we shall first
|
|
|
1424 |
transform the usual (un-annotated) regular expressions into annotated
|
|
|
1425 |
regular expressions. This operation is called \emph{internalisation} and
|
|
|
1426 |
defined as follows:
|
|
|
1427 |
|
|
|
1428 |
%\begin{definition}
|
|
|
1429 |
\begin{center}
|
|
|
1430 |
\begin{tabular}{lcl}
|
|
|
1431 |
$(\ZERO)^\uparrow$ & $\dn$ & $\textit{ZERO}$\\
|
|
|
1432 |
$(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\
|
|
|
1433 |
$(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\
|
|
|
1434 |
$(r_1 + r_2)^\uparrow$ & $\dn$ &
|
|
|
1435 |
$\textit{ALTS}\;[]\,List((\textit{fuse}\,[\Z]\,r_1^\uparrow),\,
|
|
|
1436 |
(\textit{fuse}\,[\S]\,r_2^\uparrow))$\\
|
|
|
1437 |
$(r_1\cdot r_2)^\uparrow$ & $\dn$ &
|
|
|
1438 |
$\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\
|
|
|
1439 |
$(r^*)^\uparrow$ & $\dn$ &
|
|
|
1440 |
$\textit{STAR}\;[]\,r^\uparrow$\\
|
|
|
1441 |
\end{tabular}
|
|
|
1442 |
\end{center}
|
|
|
1443 |
%\end{definition}
|
|
|
1444 |
|
|
|
1445 |
\noindent
|
|
|
1446 |
We use up arrows here to indicate that the basic un-annotated regular
|
|
|
1447 |
expressions are ``lifted up'' into something slightly more complex. In the
|
|
|
1448 |
fourth clause, $\textit{fuse}$ is an auxiliary function that helps to
|
|
|
1449 |
attach bits to the front of an annotated regular expression. Its
|
|
|
1450 |
definition is as follows:
|
|
|
1451 |
|
|
|
1452 |
\begin{center}
|
|
|
1453 |
\begin{tabular}{lcl}
|
|
|
1454 |
$\textit{fuse}\;bs\,(\textit{ZERO})$ & $\dn$ & $\textit{ZERO}$\\
|
|
|
1455 |
$\textit{fuse}\;bs\,(\textit{ONE}\,bs')$ & $\dn$ &
|
|
|
1456 |
$\textit{ONE}\,(bs\,@\,bs')$\\
|
|
|
1457 |
$\textit{fuse}\;bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ &
|
|
|
1458 |
$\textit{CHAR}\,(bs\,@\,bs')\,c$\\
|
|
|
1459 |
$\textit{fuse}\;bs\,(\textit{ALTS}\,bs'\,as)$ & $\dn$ &
|
|
|
1460 |
$\textit{ALTS}\,(bs\,@\,bs')\,as$\\
|
|
|
1461 |
$\textit{fuse}\;bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ &
|
|
|
1462 |
$\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\
|
|
|
1463 |
$\textit{fuse}\;bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ &
|
|
|
1464 |
$\textit{STAR}\,(bs\,@\,bs')\,a$
|
|
|
1465 |
\end{tabular}
|
|
|
1466 |
\end{center}
|
|
|
1467 |
|
|
|
1468 |
\noindent
|
|
|
1469 |
After internalising the regular expression, we perform successive
|
|
|
1470 |
derivative operations on the annotated regular expressions. This
|
|
|
1471 |
derivative operation is the same as what we had previously for the
|
|
|
1472 |
basic regular expressions, except that we beed to take care of
|
|
|
1473 |
the bitcodes:
|
|
|
1474 |
|
|
|
1475 |
%\begin{definition}{bder}
|
|
|
1476 |
\begin{center}
|
|
|
1477 |
\begin{tabular}{@{}lcl@{}}
|
|
|
1478 |
$(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
|
|
|
1479 |
$(\textit{ONE}\;bs)\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
|
|
|
1480 |
$(\textit{CHAR}\;bs\,d)\,\backslash c$ & $\dn$ &
|
|
|
1481 |
$\textit{if}\;c=d\; \;\textit{then}\;
|
|
|
1482 |
\textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\
|
|
|
1483 |
$(\textit{ALTS}\;bs\,as)\,\backslash c$ & $\dn$ &
|
|
|
1484 |
$\textit{ALTS}\;bs\,(as.map(\backslash c))$\\
|
|
|
1485 |
$(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
|
|
|
1486 |
$\textit{if}\;\textit{bnullable}\,a_1$\\
|
|
|
1487 |
& &$\textit{then}\;\textit{ALTS}\,bs\,List((\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\
|
|
|
1488 |
& &$\phantom{\textit{then}\;\textit{ALTS}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\
|
|
|
1489 |
& &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\,\backslash c)\,a_2$\\
|
|
|
1490 |
$(\textit{STAR}\,bs\,a)\,\backslash c$ & $\dn$ &
|
|
|
1491 |
$\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\,\backslash c))\,
|
|
|
1492 |
(\textit{STAR}\,[]\,r)$
|
|
|
1493 |
\end{tabular}
|
|
|
1494 |
\end{center}
|
|
|
1495 |
%\end{definition}
|
|
|
1496 |
|
|
|
1497 |
\noindent
|
|
|
1498 |
For instance, when we unfold $\textit{STAR} \; bs \; a$ into a sequence,
|
|
|
1499 |
we need to attach an additional bit $Z$ to the front of $r \backslash c$
|
|
|
1500 |
to indicate that there is one more star iteration. Also the $SEQ$ clause
|
|
|
1501 |
is more subtle---when $a_1$ is $\textit{bnullable}$ (here
|
|
|
1502 |
\textit{bnullable} is exactly the same as $\textit{nullable}$, except
|
|
|
1503 |
that it is for annotated regular expressions, therefore we omit the
|
|
|
1504 |
definition). Assume that $bmkeps$ correctly extracts the bitcode for how
|
|
|
1505 |
$a_1$ matches the string prior to character $c$ (more on this later),
|
|
|
1506 |
then the right branch of $ALTS$, which is $fuse \; bmkeps \; a_1 (a_2
|
|
|
1507 |
\backslash c)$ will collapse the regular expression $a_1$(as it has
|
|
|
1508 |
already been fully matched) and store the parsing information at the
|
|
|
1509 |
head of the regular expression $a_2 \backslash c$ by fusing to it. The
|
|
|
1510 |
bitsequence $bs$, which was initially attached to the head of $SEQ$, has
|
|
|
1511 |
now been elevated to the top-level of $ALTS$, as this information will be
|
|
|
1512 |
needed whichever way the $SEQ$ is matched---no matter whether $c$ belongs
|
|
|
1513 |
to $a_1$ or $ a_2$. After building these derivatives and maintaining all
|
|
|
1514 |
the lexing information, we complete the lexing by collecting the
|
|
|
1515 |
bitcodes using a generalised version of the $\textit{mkeps}$ function
|
|
|
1516 |
for annotated regular expressions, called $\textit{bmkeps}$:
|
|
|
1517 |
|
|
|
1518 |
|
|
|
1519 |
%\begin{definition}[\textit{bmkeps}]\mbox{}
|
|
|
1520 |
\begin{center}
|
|
|
1521 |
\begin{tabular}{lcl}
|
|
|
1522 |
$\textit{bmkeps}\,(\textit{ONE}\;bs)$ & $\dn$ & $bs$\\
|
|
|
1523 |
$\textit{bmkeps}\,(\textit{ALTS}\;bs\,a::as)$ & $\dn$ &
|
|
|
1524 |
$\textit{if}\;\textit{bnullable}\,a$\\
|
|
|
1525 |
& &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\
|
|
|
1526 |
& &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(\textit{ALTS}\;bs\,as)$\\
|
|
|
1527 |
$\textit{bmkeps}\,(\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ &
|
|
|
1528 |
$bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
|
|
|
1529 |
$\textit{bmkeps}\,(\textit{STAR}\;bs\,a)$ & $\dn$ &
|
|
|
1530 |
$bs \,@\, [\S]$
|
|
|
1531 |
\end{tabular}
|
|
|
1532 |
\end{center}
|
|
|
1533 |
%\end{definition}
|
|
|
1534 |
|
|
|
1535 |
\noindent
|
|
|
1536 |
This function completes the value information by travelling along the
|
|
|
1537 |
path of the regular expression that corresponds to a POSIX value and
|
|
|
1538 |
collecting all the bitcodes, and using $S$ to indicate the end of star
|
|
|
1539 |
iterations. If we take the bitcodes produced by $\textit{bmkeps}$ and
|
|
|
1540 |
decode them, we get the value we expect. The corresponding lexing
|
|
|
1541 |
algorithm looks as follows:
|
|
|
1542 |
|
|
|
1543 |
\begin{center}
|
|
|
1544 |
\begin{tabular}{lcl}
|
|
|
1545 |
$\textit{blexer}\;r\,s$ & $\dn$ &
|
|
|
1546 |
$\textit{let}\;a = (r^\uparrow)\backslash s\;\textit{in}$\\
|
|
|
1547 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
|
|
|
1548 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
|
1549 |
& & $\;\;\textit{else}\;\textit{None}$
|
|
|
1550 |
\end{tabular}
|
|
|
1551 |
\end{center}
|
|
|
1552 |
|
|
|
1553 |
\noindent
|
|
|
1554 |
In this definition $\_\backslash s$ is the generalisation of the derivative
|
|
|
1555 |
operation from characters to strings (just like the derivatives for un-annotated
|
|
|
1556 |
regular expressions).
|
|
|
1557 |
|
|
|
1558 |
The main point of the bitcodes and annotated regular expressions is that
|
|
|
1559 |
we can apply rather aggressive (in terms of size) simplification rules
|
|
|
1560 |
in order to keep derivatives small. We have developed such
|
|
|
1561 |
``aggressive'' simplification rules and generated test data that show
|
|
|
1562 |
that the expected bound can be achieved. Obviously we could only
|
|
|
1563 |
partially cover the search space as there are infinitely many regular
|
|
|
1564 |
expressions and strings.
|
|
|
1565 |
|
|
|
1566 |
One modification we introduced is to allow a list of annotated regular
|
|
|
1567 |
expressions in the \textit{ALTS} constructor. This allows us to not just
|
|
|
1568 |
delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but
|
|
|
1569 |
also unnecessary ``copies'' of regular expressions (very similar to
|
|
|
1570 |
simplifying $r + r$ to just $r$, but in a more general setting). Another
|
|
|
1571 |
modification is that we use simplification rules inspired by Antimirov's
|
|
|
1572 |
work on partial derivatives. They maintain the idea that only the first
|
|
|
1573 |
``copy'' of a regular expression in an alternative contributes to the
|
|
|
1574 |
calculation of a POSIX value. All subsequent copies can be pruned away from
|
|
|
1575 |
the regular expression. A recursive definition of our simplification function
|
|
|
1576 |
that looks somewhat similar to our Scala code is given below:
|
|
|
1577 |
%\comment{Use $\ZERO$, $\ONE$ and so on.
|
|
|
1578 |
%Is it $ALTS$ or $ALTS$?}\\
|
|
|
1579 |
|
|
|
1580 |
\begin{center}
|
|
|
1581 |
\begin{tabular}{@{}lcl@{}}
|
|
|
1582 |
|
|
|
1583 |
$\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp} \; a_2) \; \textit{match} $ \\
|
|
|
1584 |
&&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow \ZERO$ \\
|
|
|
1585 |
&&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow \ZERO$ \\
|
|
|
1586 |
&&$\quad\textit{case} \; (\ONE, a_2') \Rightarrow \textit{fuse} \; bs \; a_2'$ \\
|
|
|
1587 |
&&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow \textit{fuse} \; bs \; a_1'$ \\
|
|
|
1588 |
&&$\quad\textit{case} \; (a_1', a_2') \Rightarrow \textit{SEQ} \; bs \; a_1' \; a_2'$ \\
|
|
|
1589 |
|
|
|
1590 |
$\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
|
|
|
1591 |
&&$\quad\textit{case} \; [] \Rightarrow \ZERO$ \\
|
|
|
1592 |
&&$\quad\textit{case} \; a :: [] \Rightarrow \textit{fuse bs a}$ \\
|
|
|
1593 |
&&$\quad\textit{case} \; as' \Rightarrow \textit{ALTS}\;bs\;as'$\\
|
|
|
1594 |
|
|
|
1595 |
$\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$
|
|
|
1596 |
\end{tabular}
|
|
|
1597 |
\end{center}
|
|
|
1598 |
|
|
|
1599 |
\noindent
|
|
|
1600 |
The simplification does a pattern matching on the regular expression.
|
|
|
1601 |
When it detected that the regular expression is an alternative or
|
|
|
1602 |
sequence, it will try to simplify its children regular expressions
|
|
|
1603 |
recursively and then see if one of the children turn into $\ZERO$ or
|
|
|
1604 |
$\ONE$, which might trigger further simplification at the current level.
|
|
|
1605 |
The most involved part is the $\textit{ALTS}$ clause, where we use two
|
|
|
1606 |
auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested
|
|
|
1607 |
$\textit{ALTS}$ and reduce as many duplicates as possible. Function
|
|
|
1608 |
$\textit{distinct}$ keeps the first occurring copy only and remove all later ones
|
|
|
1609 |
when detected duplicates. Function $\textit{flatten}$ opens up nested \textit{ALTS}.
|
|
|
1610 |
Its recursive definition is given below:
|
|
|
1611 |
|
|
|
1612 |
\begin{center}
|
|
|
1613 |
\begin{tabular}{@{}lcl@{}}
|
|
|
1614 |
$\textit{flatten} \; (\textit{ALTS}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \;
|
|
|
1615 |
(\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\
|
|
|
1616 |
$\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \; as' $ \\
|
|
|
1617 |
$\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise)
|
|
|
1618 |
\end{tabular}
|
|
|
1619 |
\end{center}
|
|
|
1620 |
|
|
|
1621 |
\noindent
|
|
|
1622 |
Here $\textit{flatten}$ behaves like the traditional functional programming flatten
|
|
|
1623 |
function, except that it also removes $\ZERO$s. Or in terms of regular expressions, it
|
|
|
1624 |
removes parentheses, for example changing $a+(b+c)$ into $a+b+c$.
|
|
|
1625 |
|
|
|
1626 |
Suppose we apply simplification after each derivative step, and view
|
|
|
1627 |
these two operations as an atomic one: $a \backslash_{simp}\,c \dn
|
|
|
1628 |
\textit{simp}(a \backslash c)$. Then we can use the previous natural
|
|
|
1629 |
extension from derivative w.r.t.~character to derivative
|
|
|
1630 |
w.r.t.~string:%\comment{simp in the [] case?}
|
|
|
1631 |
|
|
|
1632 |
\begin{center}
|
|
|
1633 |
\begin{tabular}{lcl}
|
|
|
1634 |
$r \backslash_{simp} (c\!::\!s) $ & $\dn$ & $(r \backslash_{simp}\, c) \backslash_{simp}\, s$ \\
|
|
|
1635 |
$r \backslash_{simp} [\,] $ & $\dn$ & $r$
|
|
|
1636 |
\end{tabular}
|
|
|
1637 |
\end{center}
|
|
|
1638 |
|
|
|
1639 |
\noindent
|
|
|
1640 |
we obtain an optimised version of the algorithm:
|
|
|
1641 |
|
|
|
1642 |
\begin{center}
|
|
|
1643 |
\begin{tabular}{lcl}
|
|
|
1644 |
$\textit{blexer\_simp}\;r\,s$ & $\dn$ &
|
|
|
1645 |
$\textit{let}\;a = (r^\uparrow)\backslash_{simp}\, s\;\textit{in}$\\
|
|
|
1646 |
& & $\;\;\textit{if}\; \textit{bnullable}(a)$\\
|
|
|
1647 |
& & $\;\;\textit{then}\;\textit{decode}\,(\textit{bmkeps}\,a)\,r$\\
|
|
|
1648 |
& & $\;\;\textit{else}\;\textit{None}$
|
|
|
1649 |
\end{tabular}
|
|
|
1650 |
\end{center}
|
|
|
1651 |
|
|
|
1652 |
\noindent
|
|
|
1653 |
This algorithm keeps the regular expression size small, for example,
|
|
|
1654 |
with this simplification our previous $(a + aa)^*$ example's 8000 nodes
|
|
|
1655 |
will be reduced to just 6 and stays constant, no matter how long the
|
|
|
1656 |
input string is.
|
|
|
1657 |
|
|
|
1658 |
|
|
|
1659 |
|
|
|
1660 |
\section{Current Work}
|
|
|
1661 |
|
|
|
1662 |
We are currently engaged in two tasks related to this algorithm. The
|
|
|
1663 |
first task is proving that our simplification rules actually do not
|
|
|
1664 |
affect the POSIX value that should be generated by the algorithm
|
|
|
1665 |
according to the specification of a POSIX value and furthermore obtain a
|
|
|
1666 |
much tighter bound on the sizes of derivatives. The result is that our
|
|
|
1667 |
algorithm should be correct and faster on all inputs. The original
|
|
|
1668 |
blow-up, as observed in JavaScript, Python and Java, would be excluded
|
|
|
1669 |
from happening in our algorithm. For this proof we use the theorem prover
|
|
|
1670 |
Isabelle. Once completed, this result will advance the state-of-the-art:
|
|
|
1671 |
Sulzmann and Lu wrote in their paper~\cite{Sulzmann2014} about the
|
|
|
1672 |
bitcoded ``incremental parsing method'' (that is the lexing algorithm
|
|
|
1673 |
outlined in this section):
|
|
|
1674 |
|
|
|
1675 |
\begin{quote}\it
|
|
|
1676 |
``Correctness Claim: We further claim that the incremental parsing
|
|
|
1677 |
method in Figure~5 in combination with the simplification steps in
|
|
|
1678 |
Figure 6 yields POSIX parse tree [our lexical values]. We have tested this claim
|
|
|
1679 |
extensively by using the method in Figure~3 as a reference but yet
|
|
|
1680 |
have to work out all proof details.''
|
|
|
1681 |
\end{quote}
|
|
|
1682 |
|
|
|
1683 |
\noindent
|
|
|
1684 |
We like to settle this correctness claim. It is relatively
|
|
|
1685 |
straightforward to establish that after one simplification step, the part of a
|
|
|
1686 |
nullable derivative that corresponds to a POSIX value remains intact and can
|
|
|
1687 |
still be collected, in other words, we can show that
|
|
|
1688 |
%\comment{Double-check....I
|
|
|
1689 |
%think this is not the case}
|
|
|
1690 |
%\comment{If i remember correctly, you have proved this lemma.
|
|
|
1691 |
%I feel this is indeed not true because you might place arbitrary
|
|
|
1692 |
%bits on the regex r, however if this is the case, did i remember wrongly that
|
|
|
1693 |
%you proved something like simplification does not affect $\textit{bmkeps}$ results?
|
|
|
1694 |
%Anyway, i have amended this a little bit so it does not allow arbitrary bits attached
|
|
|
1695 |
%to a regex. Maybe it works now.}
|
|
|
1696 |
|
|
|
1697 |
\begin{center}
|
|
|
1698 |
$\textit{bmkeps} \; a = \textit{bmkeps} \; \textit{bsimp} \; a\;($\textit{provided}$ \; a\; is \; \textit{bnullable} )$
|
|
|
1699 |
\end{center}
|
|
|
1700 |
|
|
|
1701 |
\noindent
|
|
|
1702 |
as this basically comes down to proving actions like removing the
|
|
|
1703 |
additional $r$ in $r+r$ does not delete important POSIX information in
|
|
|
1704 |
a regular expression. The hard part of this proof is to establish that
|
|
|
1705 |
|
|
|
1706 |
\begin{center}
|
|
|
1707 |
$ \textit{blexer}\_{simp}(r, \; s) = \textit{blexer}(r, \; s)$
|
|
|
1708 |
\end{center}
|
|
|
1709 |
%comment{This is not true either...look at the definion blexer/blexer-simp}
|
|
|
1710 |
|
|
|
1711 |
\noindent That is, if we do derivative on regular expression $r$ and then
|
|
|
1712 |
simplify it, and repeat this process until we exhaust the string, we get a
|
|
|
1713 |
regular expression $r''$($\textit{LHS}$) that provides the POSIX matching
|
|
|
1714 |
information, which is exactly the same as the result $r'$($\textit{RHS}$ of the
|
|
|
1715 |
normal derivative algorithm that only does derivative repeatedly and has no
|
|
|
1716 |
simplification at all. This might seem at first glance very unintuitive, as
|
|
|
1717 |
the $r'$ could be exponentially larger than $r''$, but can be explained in the
|
|
|
1718 |
following way: we are pruning away the possible matches that are not POSIX.
|
|
|
1719 |
Since there could be exponentially many
|
|
|
1720 |
non-POSIX matchings and only 1 POSIX matching, it
|
|
|
1721 |
is understandable that our $r''$ can be a lot smaller. we can still provide
|
|
|
1722 |
the same POSIX value if there is one. This is not as straightforward as the
|
|
|
1723 |
previous proposition, as the two regular expressions $r'$ and $r''$ might have
|
|
|
1724 |
become very different. The crucial point is to find the
|
|
|
1725 |
$\textit{POSIX}$ information of a regular expression and how it is modified,
|
|
|
1726 |
augmented and propagated
|
|
|
1727 |
during simplification in parallel with the regular expression that
|
|
|
1728 |
has not been simplified in the subsequent derivative operations. To aid this,
|
|
|
1729 |
we use the helper function retrieve described by Sulzmann and Lu:
|
|
|
1730 |
\begin{center}
|
|
|
1731 |
\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
|
|
|
1732 |
$\textit{retrieve}\,(\textit{ONE}\,bs)\,\Empty$ & $\dn$ & $bs$\\
|
|
|
1733 |
$\textit{retrieve}\,(\textit{CHAR}\,bs\,c)\,(\Char\,d)$ & $\dn$ & $bs$\\
|
|
|
1734 |
$\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Left\,v)$ & $\dn$ &
|
|
|
1735 |
$bs \,@\, \textit{retrieve}\,a\,v$\\
|
|
|
1736 |
$\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Right\,v)$ & $\dn$ &
|
|
|
1737 |
$bs \,@\, \textit{retrieve}\,(\textit{ALTS}\,bs\,as)\,v$\\
|
|
|
1738 |
$\textit{retrieve}\,(\textit{SEQ}\,bs\,a_1\,a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &
|
|
|
1739 |
$bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\
|
|
|
1740 |
$\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,[])$ & $\dn$ &
|
|
|
1741 |
$bs \,@\, [\S]$\\
|
|
|
1742 |
$\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\
|
|
|
1743 |
\multicolumn{3}{l}{
|
|
|
1744 |
\hspace{3cm}$bs \,@\, [\Z] \,@\, \textit{retrieve}\,a\,v\,@\,
|
|
|
1745 |
\textit{retrieve}\,(\textit{STAR}\,[]\,a)\,(\Stars\,vs)$}\\
|
|
|
1746 |
\end{tabular}
|
|
|
1747 |
\end{center}
|
|
|
1748 |
%\comment{Did not read further}\\
|
|
|
1749 |
This function assembles the bitcode
|
|
|
1750 |
%that corresponds to a lexical value for how
|
|
|
1751 |
%the current derivative matches the suffix of the string(the characters that
|
|
|
1752 |
%have not yet appeared, but will appear as the successive derivatives go on.
|
|
|
1753 |
%How do we get this "future" information? By the value $v$, which is
|
|
|
1754 |
%computed by a pass of the algorithm that uses
|
|
|
1755 |
%$inj$ as described in the previous section).
|
|
|
1756 |
using information from both the derivative regular expression and the
|
|
|
1757 |
value. Sulzmann and Lu poroposed this function, but did not prove
|
|
|
1758 |
anything about it. Ausaf and Urban used it to connect the bitcoded
|
|
|
1759 |
algorithm to the older algorithm by the following equation:
|
|
|
1760 |
|
|
|
1761 |
\begin{center} $inj \;a\; c \; v = \textit{decode} \; (\textit{retrieve}\;
|
|
|
1762 |
(r^\uparrow)\backslash_{simp} \,c)\,v)$
|
|
|
1763 |
\end{center}
|
|
|
1764 |
|
|
|
1765 |
\noindent
|
|
|
1766 |
whereby $r^\uparrow$ stands for the internalised version of $r$. Ausaf
|
|
|
1767 |
and Urban also used this fact to prove the correctness of bitcoded
|
|
|
1768 |
algorithm without simplification. Our purpose of using this, however,
|
|
|
1769 |
is to establish
|
|
|
1770 |
|
|
|
1771 |
\begin{center}
|
|
|
1772 |
$ \textit{retrieve} \;
|
|
|
1773 |
a \; v \;=\; \textit{retrieve} \; (\textit{simp}\,a) \; v'.$
|
|
|
1774 |
\end{center}
|
|
|
1775 |
The idea is that using $v'$, a simplified version of $v$ that had gone
|
|
|
1776 |
through the same simplification step as $\textit{simp}(a)$, we are able
|
|
|
1777 |
to extract the bitcode that gives the same parsing information as the
|
|
|
1778 |
unsimplified one. However, we noticed that constructing such a $v'$
|
|
|
1779 |
from $v$ is not so straightforward. The point of this is that we might
|
|
|
1780 |
be able to finally bridge the gap by proving
|
|
|
1781 |
|
|
|
1782 |
\begin{center}
|
|
|
1783 |
$\textit{retrieve} \; (r^\uparrow \backslash s) \; v = \;\textit{retrieve} \;
|
|
|
1784 |
(\textit{simp}(r^\uparrow) \backslash s) \; v'$
|
|
|
1785 |
\end{center}
|
|
|
1786 |
|
|
|
1787 |
\noindent
|
|
|
1788 |
and subsequently
|
|
|
1789 |
|
|
|
1790 |
\begin{center}
|
|
|
1791 |
$\textit{retrieve} \; (r^\uparrow \backslash s) \; v\; = \; \textit{retrieve} \;
|
|
|
1792 |
(r^\uparrow \backslash_{simp} \, s) \; v'$.
|
|
|
1793 |
\end{center}
|
|
|
1794 |
|
|
|
1795 |
\noindent
|
|
|
1796 |
The $\textit{LHS}$ of the above equation is the bitcode we want. This
|
|
|
1797 |
would prove that our simplified version of regular expression still
|
|
|
1798 |
contains all the bitcodes needed. The task here is to find a way to
|
|
|
1799 |
compute the correct $v'$.
|
|
|
1800 |
|
|
|
1801 |
The second task is to speed up the more aggressive simplification. Currently
|
|
|
1802 |
it is slower than the original naive simplification by Ausaf and Urban (the
|
|
|
1803 |
naive version as implemented by Ausaf and Urban of course can ``explode'' in
|
|
|
1804 |
some cases). It is therefore not surprising that the speed is also much slower
|
|
|
1805 |
than regular expression engines in popular programming languages such as Java
|
|
|
1806 |
and Python on most inputs that are linear. For example, just by rewriting the
|
|
|
1807 |
example regular expression in the beginning of this report $(a^*)^*\,b$ into
|
|
|
1808 |
$a^*\,b$ would eliminate the ambiguity in the matching and make the time
|
|
|
1809 |
for matching linear with respect to the input string size. This allows the
|
|
|
1810 |
DFA approach to become blindingly fast, and dwarf the speed of our current
|
|
|
1811 |
implementation. For example, here is a comparison of Java regex engine
|
|
|
1812 |
and our implementation on this example.
|
|
|
1813 |
|
|
|
1814 |
\begin{center}
|
|
|
1815 |
\begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
|
|
|
1816 |
\begin{tikzpicture}
|
|
|
1817 |
\begin{axis}[
|
|
|
1818 |
xlabel={$n*1000$},
|
|
|
1819 |
x label style={at={(1.05,-0.05)}},
|
|
|
1820 |
ylabel={time in secs},
|
|
|
1821 |
enlargelimits=false,
|
|
|
1822 |
xtick={0,5,...,30},
|
|
|
1823 |
xmax=33,
|
|
|
1824 |
ymax=9,
|
|
|
1825 |
scaled ticks=true,
|
|
|
1826 |
axis lines=left,
|
|
|
1827 |
width=5cm,
|
|
|
1828 |
height=4cm,
|
|
|
1829 |
legend entries={Bitcoded Algorithm},
|
|
|
1830 |
legend pos=north west,
|
|
|
1831 |
legend cell align=left]
|
|
|
1832 |
\addplot[red,mark=*, mark options={fill=white}] table {bad-scala.data};
|
|
|
1833 |
\end{axis}
|
|
|
1834 |
\end{tikzpicture}
|
|
|
1835 |
&
|
|
|
1836 |
\begin{tikzpicture}
|
|
|
1837 |
\begin{axis}[
|
|
|
1838 |
xlabel={$n*1000$},
|
|
|
1839 |
x label style={at={(1.05,-0.05)}},
|
|
|
1840 |
%ylabel={time in secs},
|
|
|
1841 |
enlargelimits=false,
|
|
|
1842 |
xtick={0,5,...,30},
|
|
|
1843 |
xmax=33,
|
|
|
1844 |
ymax=9,
|
|
|
1845 |
scaled ticks=false,
|
|
|
1846 |
axis lines=left,
|
|
|
1847 |
width=5cm,
|
|
|
1848 |
height=4cm,
|
|
|
1849 |
legend entries={Java},
|
|
|
1850 |
legend pos=north west,
|
|
|
1851 |
legend cell align=left]
|
|
|
1852 |
\addplot[cyan,mark=*, mark options={fill=white}] table {good-java.data};
|
|
|
1853 |
\end{axis}
|
|
|
1854 |
\end{tikzpicture}\\
|
|
|
1855 |
\multicolumn{3}{c}{Graphs: Runtime for matching $a^*\,b$ with strings
|
|
|
1856 |
of the form $\underbrace{aa..a}_{n}$.}
|
|
|
1857 |
\end{tabular}
|
|
|
1858 |
\end{center}
|
|
|
1859 |
|
|
|
1860 |
|
|
|
1861 |
Java regex engine can match string of thousands of characters in a few milliseconds,
|
|
|
1862 |
whereas our current algorithm gets excruciatingly slow on input of this size.
|
|
|
1863 |
The running time in theory is linear, however it does not appear to be the
|
|
|
1864 |
case in an actual implementation. So it needs to be explored how to
|
|
|
1865 |
make our algorithm faster on all inputs. It could be the recursive calls that are
|
|
|
1866 |
needed to manipulate bits that are causing the slow down. A possible solution
|
|
|
1867 |
is to write recursive functions into tail-recusive form.
|
|
|
1868 |
Another possibility would be to explore
|
|
|
1869 |
again the connection to DFAs to speed up the algorithm on
|
|
|
1870 |
subcalls that are small enough. This is very much work in progress.
|
|
|
1871 |
|
|
|
1872 |
\section{Conclusion}
|
|
|
1873 |
|
|
|
1874 |
In this PhD-project we are interested in fast algorithms for regular
|
|
|
1875 |
expression matching. While this seems to be a ``settled'' area, in
|
|
|
1876 |
fact interesting research questions are popping up as soon as one steps
|
|
|
1877 |
outside the classic automata theory (for example in terms of what kind
|
|
|
1878 |
of regular expressions are supported). The reason why it is
|
|
|
1879 |
interesting for us to look at the derivative approach introduced by
|
|
|
1880 |
Brzozowski for regular expression matching, and then much further
|
|
|
1881 |
developed by Sulzmann and Lu, is that derivatives can elegantly deal
|
|
|
1882 |
with some of the regular expressions that are of interest in ``real
|
|
|
1883 |
life''. This includes the not-regular expression, written $\neg\,r$
|
|
|
1884 |
(that is all strings that are not recognised by $r$), but also bounded
|
|
|
1885 |
regular expressions such as $r^{\{n\}}$ and $r^{\{n..m\}}$). There is
|
|
|
1886 |
also hope that the derivatives can provide another angle for how to
|
|
|
1887 |
deal more efficiently with back-references, which are one of the
|
|
|
1888 |
reasons why regular expression engines in JavaScript, Python and Java
|
|
|
1889 |
choose to not implement the classic automata approach of transforming
|
|
|
1890 |
regular expressions into NFAs and then DFAs---because we simply do not
|
|
|
1891 |
know how such back-references can be represented by DFAs.
|
|
|
1892 |
We also plan to implement the bitcoded algorithm
|
|
|
1893 |
in some imperative language like C to see if the inefficiency of the
|
|
|
1894 |
Scala implementation
|
|
|
1895 |
is language specific. To make this research more comprehensive we also plan
|
|
|
1896 |
to contrast our (faster) version of bitcoded algorithm with the
|
|
|
1897 |
Symbolic Regex Matcher, the RE2, the Rust Regex Engine, and the static
|
|
|
1898 |
analysis approach by implementing them in the same language and then compare
|
|
|
1899 |
their performance.
|
|
|
1900 |
|
|
|
1901 |
\bibliographystyle{plain}
|
|
|
1902 |
\bibliography{root,regex_time_complexity}
|
|
|
1903 |
|
|
|
1904 |
|
|
|
1905 |
|
|
|
1906 |
\end{document}
|