\documentclass[dvipsnames,14pt,t]{beamer}\usepackage{../slides}\usepackage{../langs}\usepackage{../data}\usepackage{../graphics}\usepackage{../grammar}\usepackage{soul}\usepackage{mathpartir}% beamer stuff\renewcommand{\slidecaption}{CFL 09, King's College London}\newcommand{\bl}[1]{\textcolor{blue}{#1}} \begin{document}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[t]\frametitle{% \begin{tabular}{@ {}c@ {}} \\[-3mm] \LARGE Compilers and \\[-2mm] \LARGE Formal Languages (9)\\[3mm] \end{tabular}} \normalsize \begin{center} \begin{tabular}{ll} Email: & christian.urban at kcl.ac.uk\\ Office: & N\liningnums{7.07} (North Wing, Bush House)\\ Slides: & KEATS (also homework is there)\\ \end{tabular} \end{center}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[t]\frametitle{While Language}\begin{center}\bl{\begin{tabular}{@{}lcl@{}}\\[-12mm] \meta{Stmt} & $::=$ & $\texttt{skip}$\\ & $|$ & \textit{Id}\;\texttt{:=}\;\meta{AExp}\\ & $|$ & \texttt{if}\; \meta{BExp} \;\texttt{then}\; \meta{Block} \;\texttt{else}\; \meta{Block}\\ & $|$ & \texttt{while}\; \meta{BExp} \;\texttt{do}\; \meta{Block}\\ & $|$ & \texttt{read}\;\textit{Id}\\ & $|$ & \texttt{write}\;\textit{Id}\\ & $|$ & \texttt{write}\;\textit{String}\medskip\\\meta{Stmts} & $::=$ & \meta{Stmt} \;\texttt{;}\; \meta{Stmts} $|$ \meta{Stmt}\medskip\\\meta{Block} & $::=$ & \texttt{\{}\,\meta{Stmts}\,\texttt{\}} $|$ \meta{Stmt}\medskip\\\meta{AExp} & $::=$ & \ldots\\\meta{BExp} & $::=$ & \ldots\\\end{tabular}}\end{center}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}}\mbox{}\\[-18mm]\mbox{}{\lstset{language=While}\fontsize{10}{12}\selectfont\texttt{\lstinputlisting{../progs/fib.while}}}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c,fragile]\frametitle{BF***}some big array, say \texttt{a}; 7 (8) instructions:\begin{itemize}\item \texttt{>} move \texttt{ptr++}\item \texttt{<} move \texttt{ptr-{}-}\item \texttt{+} add \texttt{a[ptr]++}\item \texttt{-} subtract \texttt{a[ptr]-{}-}\item \texttt{.} print out \texttt{a[ptr]} as ASCII\item \texttt{[} if \texttt{a[ptr] == 0} jump just after the corresponding \texttt{]}; otherwise \texttt{ptr++}\item \texttt{]} if \texttt{a[ptr] != 0} jump just after the corresponding \texttt{[}; otherwise \texttt{ptr++}\end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c,fragile]\frametitle{Arrays in While}\begin{itemize}\item \texttt{new arr[15000]}\medskip \item \texttt{x := 3 + arr[3 + y]}\medskip \item \texttt{arr[42 * n] := ...}\end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c,fragile]\frametitle{New Arrays}\begin{lstlisting}[mathescape,numbers=none,language=While] new arr[number]\end{lstlisting}\bigskip\bigskip\begin{lstlisting}[mathescape,numbers=none,language=While] ldc number newarray int astore loc_var\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c,fragile]\frametitle{Array Update}\begin{lstlisting}[mathescape,numbers=none,language=While] arr[...] := \end{lstlisting}\bigskip\bigskip\begin{lstlisting}[mathescape,numbers=none,language=While] aload loc_var index_aexp value_aexp iastore\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c,fragile]\frametitle{Array Lookup in AExp}\begin{lstlisting}[mathescape,numbers=none,language=While] ...arr[...]... \end{lstlisting}\bigskip\bigskip\begin{lstlisting}[mathescape,numbers=none,language=While] aload loc_var index_aexp iaload\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\mode<presentation>{\begin{frame}[c]\large\bfUsing a compiler, \\how can you mount the\\ perfect attack against a system?\end{frame}}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\mode<presentation>{\begin{frame}[c]{\large\bfWhat is a \alert{perfect} attack?}\bigskip\begin{enumerate}\item you can potentially completely take over a target system\item your attack is (nearly) undetectable\item the victim has (almost) no chance to recover\end{enumerate}\end{frame}}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\mode<presentation>{\begin{frame}[c] \begin{center} \begin{tikzpicture}[scale=1] \onslide<1->{ \node (A) at (0,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=17mm] {}; \node [below right] at (A.north west) {\footnotesize\begin{tabular}{@{}l@{}} \only<1,2>{clean}\only<3->{\alert{hacked}}\\compiler\end{tabular}};} \onslide<2->{ \node (B) at (-2,2) [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {}; \node [below right] at (B.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(src)\end{tabular}}; \node (C) at (2,2) [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {}; \node [below right] at (C.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(bin)\end{tabular}}; \draw[->, line width=2mm] (B) -- (C); } \onslide<3->{\node [above left=-1.5mm] at (C.south east) {\footnotesize \alert{$\blacksquare$}};} \end{tikzpicture} \end{center}\end{frame}}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\mode<presentation>{\begin{frame}[c] \begin{center} \begin{tikzpicture}[scale=1] \onslide<1->{ \node (A) at (0,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {}; \node [below right] at (A.north west) {\small V0.01}; \node [below right] (A1) at (A.south west) {\small Scala}; \node [below right] (A1) at (A1.south west) {\small\textcolor{gray}{host language}}; \node [above right] at (A.north west) {my compiler (src)};} \onslide<2->{ \node (B) at (1.8,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {}; \node [below right] at (B.north west) {\small V0.02}; \node [below right] at (B.south west) {\small Scala}; \node at (3,0) {\ldots}; \node (C) at (5,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {}; \node [below right] at (C.north west) {\small V1.00}; \node [below right] at (C.south west) {\small Scala};} \onslide<3->{ \node (D) at (6.8,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {}; \node [below right] at (D.north west) {\small V1.00}; \node (E) at (6.8,2) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {}; \node [below right] at (E.north west) {\small V1.01};} \onslide<4->{ \node (F) at (8.6,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {}; \node [below right] at (F.north west) {\small V1.01}; \node (G) at (8.6,2) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {}; \node [below right] at (G.north west) {\small V1.02}; \node at (9.8,0) {\ldots}; \node at (9.8,2) {\ldots}; \node at (8,-2) {\textcolor{gray}{\begin{tabular}{@{}l@{}}no host language\\needed\end{tabular}}}; } \end{tikzpicture} \end{center}\end{frame}}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode<presentation>{ \begin{frame}<1-3> \frametitle{\LARGE\begin{tabular}{c}Hacking Compilers \end{tabular}} %Why is it so paramount to have a small trusted code base (TCB)? \bigskip\bigskip \begin{columns} \begin{column}{2.7cm} \begin{minipage}{2.5cm}% \begin{tabular}{c@ {}} \includegraphics[scale=0.2]{../pics/ken-thompson.jpg}\\[-1.8mm] \footnotesize Ken Thompson\\[-1.8mm] \footnotesize Turing Award, 1983\\ \end{tabular} \end{minipage} \end{column} \begin{column}{9cm} \begin{tabular}{l@ {\hspace{1mm}}p{8cm}} & Ken Thompson showed how to hide a Trojan Horse in a compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm] & No amount of source level verification will protect you from such Thompson-hacks.\\[2mm] \end{tabular} \end{column} \end{columns} \only<2>{ \begin{textblock}{6}(4,2) \begin{tikzpicture} \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] {\normalsize \begin{minipage}{8cm} \begin{quote} \includegraphics[scale=0.05]{../pics/evil.png} \begin{enumerate} \item[1)] Assume you ship the compiler as binary and also with sources. \item[2)] Make the compiler aware when it compiles itself. \item[3)] Add the Trojan horse. \item[4)] Compile. \item[5)] Delete Trojan horse from the sources of the compiler. \item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{} \end{enumerate} \end{quote} \end{minipage}}; \end{tikzpicture} \end{textblock}} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \begin{center} \includegraphics[scale=0.6]{../pics/bridge-limits.png} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\frametitle{Compilers \& Boeings 777}First flight in 1994. They want to achieve triple redundancy in hardwarefaults.\bigskipThey compile 1 Ada program to\medskip\begin{itemize}\item Intel 80486\item Motorola 68040 (old Macintosh's)\item AMD 29050 (RISC chips used often in laser printers)\end{itemize}\medskipusing 3 independent compilers.\bigskip\pause\small Airbus uses C and static analysers. Recently started using CompCert.\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\frametitle{Goal}Remember the Bridges example?\begin{itemize}\item Can we look at our programs and somehow ensurethey are bug free/correct?\pause\bigskip\item Very hard: Anything interesting about programs is equivalentto the Halting Problem, which is undecidable.\pause\bigskip\item \alert{Solution:} We avoid this ``minor'' obstacle by being as close as possible of deciding the halting problem, without actually deciding the halting problem. \small$\quad\Rightarrow$ yes, no, don't know (static analysis)\end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state.png} \end{center} \begin{itemize} \item depending on some initial input, a program (behaviour) will ``develop'' over time. \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state2.png} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state3.jpg} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state4.jpg} \end{center} \begin{itemize} \item to be avoided \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state5.png} \end{center} \begin{itemize} \item this needs more work \end{itemize} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{What is Static Analysis?} \begin{center} \includegraphics[scale=0.4]{../pics/state6.png} \end{center} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c,fragile] \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] Are Vars Definitely Initialised?\end{tabular}}Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskipProg.~1:\\\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language=While,xleftmargin=3mm]if x < 1 then y := x else y := x + 1;y := y + 1\end{lstlisting}\medskip Prog.~2:\\\begin{lstlisting}[numbers=none, basicstyle=\ttfamily, language=While,xleftmargin=3mm]if x < x then y := y + 1 else y := x;y := y + 1\end{lstlisting} \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c,fragile] \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm] Are Vars Definitely Initialised?\end{tabular}} What should the rules be for deciding when a variable is initialised?\bigskip\pause\begin{itemize}\item variable \texttt{x} is definitely initialized after \texttt{skip}\\ iff \texttt{x} is definitely initialized before \texttt{skip}.\end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c,fragile]% \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]% Are Vars Definitely Initialised?\end{tabular}}$\bl{A}$ is the set of definitely defined variables:\begin{center}\begin{tabular}{c} \bl{\infer{\mbox{}}{A\triangleright\texttt{skip}\triangleright{}A}}\qquad \bl{\infer{vars(a) \subseteq A}{A\triangleright (\texttt{x\,:=\,a})\triangleright\{x\}\cup A}} \medskip\\\pause \bl{\infer{A_1\triangleright{}s_1\triangleright{}A_2 \quad A_2\triangleright{}s_2\triangleright{}A_3} {A_1\triangleright{}(s_1 ; s_2)\triangleright{}A_3}} \medskip\\\pause \bl{\infer{vars(b)\subseteq A\quad A\triangleright{}s_1\triangleright{}A_1 \quad A\triangleright{}s_2\triangleright{}A_2} {A\triangleright(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\triangleright{}A_1\cap A_2}} \medskip\\\pause \bl{\infer{vars(b)\subseteq A\quad A\triangleright{}s\triangleright{}A'} {A\triangleright(\texttt{while}\;b\;\texttt{do}\;s)\triangleright{}A}}\pause\end{tabular} \end{center}\hfill we start with $\bl{A = \{\}}$\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c] \frametitle{Dijkstra on Testing} \begin{bubble}[10cm] ``Program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence.'' \end{bubble}\bigskip \small What is good about compilers: the either seem to work, or go horribly wrong (most of the time). \end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\frametitle{\Large Proving Programs to be Correct}\begin{bubble}[10cm]\small{\bf Theorem:} There are infinitely many prime numbers.\medskip\\{\bf Proof} \ldots\\\end{bubble}\bigskipsimilarly\bigskip\begin{bubble}[10cm]\small{\bf Theorem:} The program is doing what it is supposed to be doing.\medskip{\bf Long, long proof} \ldots\\\end{bubble}\bigskip\medskip\small This can be a gigantic proof. The only hope is to havehelp from the computer. `Program' is here to be understood to bequite general (compiler, OS, \ldots).\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c]\frametitle{Can This Be Done?}\begin{itemize}\item in 2008, verification of a small C-compiler\begin{itemize}\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''\item is as good as \texttt{gcc -O1}, but much, much less buggy \end{itemize}\end{itemize}\begin{center} \includegraphics[scale=0.12]{../pics/compcert.png}\end{center}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[t]\frametitle{Fuzzy Testing C-Compilers}\begin{itemize}\item tested GCC, LLVM and others by randomly generating C-programs\item found more than 300 bugs in GCC and alsomany in LLVM (some of them highest-level critical)\bigskip\item about CompCert:\begin{bubble}[10.7cm]\small ``The striking thing about our CompCertresults is that the middle-end bugs we found in all othercompilers are absent. As of early 2011, the under-developmentversion of CompCert is the only compiler we have tested forwhich Csmith cannot find wrong-code errors. This is not forlack of trying: we have devoted about six CPU-years to thetask.'' \end{bubble} \end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \begin{frame}[c]\frametitle{Next Week}\begin{itemize}\item Revision Lecture\medskip\item How many strings are in $\bl{L(a^*)}$?\pause\medskip\item How many strings are in $\bl{L((a + b)^*)}$?\\ Are there more than in $\bl{L(a^*)}$?\end{itemize}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \end{document}%%% Local Variables: %%% mode: latex%%% TeX-master: t%%% End: