\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
\usepackage{../data}
\usepackage{../graphics}
\usepackage{../grammar}
\usepackage{soul}


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


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


similarly\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 have
help from the computer. `Program' is here to be understood to be
quite 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}[c]
\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 also
many in LLVM (some of them highest-level critical)\bigskip
\item about CompCert:

\begin{bubble}[10cm]\small ``The striking thing about our CompCert
results is that the middle-end bugs we found in all other
compilers are absent. As of early 2011, the under-development
version of CompCert is the only compiler we have tested for
which Csmith cannot find wrong-code errors. This is not for
lack of trying: we have devoted about six CPU-years to the
task.'' 
\end{bubble} 
\end{itemize}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\end{document}

%%% Local Variables:  
%%% mode: latex
%%% TeX-master: t
%%% End: