% !TEX program = xelatex
\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
\usepackage{../slides}
\usepackage{../langs}
\usepackage{../data}
\usepackage{../graphics}
\usepackage{../grammar}
\usepackage{soul}
\usepackage{mathpartir}
\usetikzlibrary{shapes,arrows,shadows}

% 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\\[3mm] 
  \end{tabular}}

  \normalsize
  \begin{center}
  \begin{tabular}{ll}
    Email:  & christian.urban at kcl.ac.uk\\
    %Office Hours: & Thursdays 12 -- 14\\
    %Location: & N7.07 (North Wing, Bush House)\\
    Slides \& Progs: & KEATS (also homework is there)\\  
  \end{tabular}
  \end{center}

  \begin{center}
    \begin{tikzpicture}
      \node[drop shadow,fill=white,inner sep=0pt] 
      {\footnotesize\rowcolors{1}{capri!10}{white}
        \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
          1 Introduction, Languages          & 6 While-Language \\
          2 Regular Expressions, Derivatives & 7 Compilation, JVM \\
          3 Automata, Regular Languages      & 8 Compiling Functional Languages \\
          4 Lexing, Tokenising               & \cellcolor{blue!50} 9 Optimisations \\
          5 Grammars, Parsing                & 10 LLVM \\ \hline
        \end{tabular}%
      };
    \end{tikzpicture}
  \end{center}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{The Fun Language}

\footnotesize
\begin{textblock}{13}(0.9,3)
\begin{lstlisting}[]numbers=none]
def fib(n) = if n == 0 then 0 
             else if n == 1 then 1 
             else fib(n - 1) + fib(n - 2);

def fact(n) = if n == 0 then 1 else n * fact(n - 1);

def ack(m, n) = if m == 0 then n + 1
                else if n == 0 then ack(m - 1, 1)
                else ack(m - 1, ack(m, n - 1));
                
def gcd(a, b) = if b == 0 then a else gcd(b, a % b);                
\end{lstlisting}
\end{textblock}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{Factorial Funct.~on the JVM}

\begin{textblock}{7}(1,1.8)\footnotesize
\begin{minipage}{6cm}
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
.method public static facT(II)I 
.limit locals 2
.limit stack 6
  iload 0
  ldc 0
  if_icmpne If_else_2
  iload 1
  goto If_end_3
If_else_2:
  iload 0
  ldc 1
  isub
  iload 0
  iload 1
  imul
  invokestatic fact/fact/facT(II)I
If_end_3:
  ireturn
.end method 
\end{lstlisting}
\end{minipage}
\end{textblock}

\begin{textblock}{7}(6,7)
\begin{bubble}[7cm]\small
\begin{lstlisting}[language=Lisp,
                   basicstyle=\ttfamily, 
                   numbers=none,
                   xleftmargin=1mm,linebackgroundcolor=\color{cream}]
def facT(n, acc) = 
  if n == 0 then acc 
  else facT(n - 1, n * acc);
\end{lstlisting}
\end{bubble}
\end{textblock}

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


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{LLVM}

\begin{itemize}
  \item Chris Lattner, Vikram Adve (started in 2000)
  \item Apple hired Lattner in 2006
  \item modular architecture, LLVM-IR
  \item \texttt{lli} and \texttt{llc} 
\end{itemize}

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



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\tikzstyle{sensor}=[draw, fill=blue!20, text width=3.8em, line width=1mm,
    text centered, minimum height=2em,drop shadow]
\tikzstyle{ann} = [above, text width=4em, text centered]
\tikzstyle{sc} = [sensor, text width=7em, fill=red!20, 
    minimum height=6em, rounded corners, drop shadow,line width=1mm]

\begin{frame}[fragile,c]
\frametitle{LLVM: Overview}

\begin{tikzpicture}
    % Validation Layer is the same except that there are a set of nodes and links which are added
   
    \path (0,0) node (IR) [sc] {\textbf{LLVM-IR}\\ Optimisations};
    \path (IR.west)+(-2.2,1.7) node (sou1) [sensor] {C++};
    \path (IR.west)+(-2.2,0.5) node (sou2)[sensor] {C};
    \path (IR.west)+(-2.2,-1.0) node (dots)[ann] {$\vdots$}; 
    \path (IR.west)+(-2.2,-1.8) node (sou3)[sensor] {Haskell};    

    \path [draw,->,line width=1mm] (sou1.east) -- node [above] {} (IR.160);
    \path [draw,->,line width=1mm] (sou2.east) -- node [above] {} (IR.180);
    \path [draw,->,line width=1mm] (sou3.east) -- node [above] {} (IR.200);

    \path (IR.east)+(2.2,2.0)  node (tar1)[sensor] {x86};
    \path (IR.east)+(2.2,0.8)  node (tar2)[sensor] {ARM};
    \path (IR.east)+(2.2,-0.4) node (tar3)[sensor] {MIPS}; 
    \path (IR.east)+(2.2,-1.6) node (tar4)[sensor] {RISC}; 
    \path (IR.east)+(2.2,-2.8) node (tar5)[sensor] {Power PC};
    \path (IR.east)+(2.2,-4.2) node (dots2)[ann] {$\vdots$};

    \path [draw,<-,line width=1mm] (tar1.west) -- node [above] {} (IR.10);
    \path [draw,<-,line width=1mm] (tar2.west) -- node [above] {} (IR.5);
    \path [draw,<-,line width=1mm] (tar3.west) -- node [above] {} (IR.0);
    \path [draw,<-,line width=1mm] (tar4.west) -- node [above] {} (IR.-5);
    \path [draw,<-,line width=1mm] (tar5.west) -- node [above] {} (IR.-10);
    
\end{tikzpicture}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,t]
\frametitle{LLVM-IR}
\small

\begin{textblock}{7.7}(8,11.4)
\begin{bubble}[5cm]\small
\begin{lstlisting}[language=Lisp,
                   numbers=none,
                   xleftmargin=1mm,linebackgroundcolor=\color{cream}]
def fact(n) =
  if n == 0 then 1 
  else n * fact(n - 1)
\end{lstlisting}
\end{bubble}
\end{textblock}

\begin{lstlisting}[language=LLVM,xleftmargin=-7mm]
define i32 @fact (i32 %n) {
   %tmp_19 = icmp eq i32  %n, 0
   br i1 %tmp_19, label %if_br_23, label %else_br_24

if_br_23:
   ret i32 1

else_br_24:
   %tmp_21 = sub i32  %n, 1
   %tmp_22 = call i32 @fact (i32 %tmp_21)
   %tmp_20 = mul i32  %n, %tmp_22
   ret i32 %tmp_20
}
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{LLVM Types}

\tt
\begin{center}
\begin{tabular}{ll}
boolean & i1 \\
byte    & i8 \\
short   & i16\\
char    & i16\\
integer & i32\\
long    & i64\\
float   & float\\
double  & double\\
*\_      & pointer to \\
**\_     & pointer to a pointer to\\
\mbox{}[\_]    & arrays of\\
\end{tabular}
\end{center}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{LLVM-IR Instructions}
\small

\begin{lstlisting}[language=LLVM,xleftmargin=0mm]
br i1 %var, label %if_br, label %else_br

icmp eq i32  %x, %y     ; for equal
icmp sle i32 %x, %y     ;   signed less or equal
icmp slt i32 %x, %y     ;   signed less than
icmp ult i32 %x, %y     ;   unsigned less than 

%var = call i32 @foo(...args...)
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{SSA Format}

\bl{$(1 + a) + (3 + (b * 5))$}\bigskip\bigskip

\begin{lstlisting}[language=LLVM]
tmp0 = add 1 a   
tmp1 = mul b 5 
tmp2 = add 3 tmp1 
tmp3 = add tmp0 tmp2  
\end{lstlisting}\bigskip\bigskip

\hfill Static Single Assignment

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{Abstract Syntax Trees}
\footnotesize

\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
// Fun language (expressions)
abstract class Exp 
abstract class BExp 

case class Call(name: String, args: List[Exp]) extends Exp
case class If(a: BExp, e1: Exp, e2: Exp) extends Exp
case class Write(e: Exp) extends Exp
case class Var(s: String) extends Exp
case class Num(i: Int) extends Exp
case class Aop(o: String, a1: Exp, a2: Exp) extends Exp
case class Sequence(e1: Exp, e2: Exp) extends Exp
case class Bop(o: String, a1: Exp, a2: Exp) extends BExp  
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{K-(Intermediate)Language}
\footnotesize

\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
abstract class KExp
abstract class KVal

// K-Values
case class KVar(s: String) extends KVal
case class KNum(i: Int) extends KVal
case class Kop(o: String, v1: KVal, v2: KVal) extends KVal
case class KCall(o: String, vrs: List[KVal]) extends KVal
case class KWrite(v: KVal) extends KVal

// K-Expressions
case class KIf(x1: String, e1: KExp, e2: KExp) extends KExp
case class KLet(x: String, v: KVal, e: KExp) extends KExp
case class KReturn(v: KVal) extends KExp
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{CPS-Translation}
\small

\begin{lstlisting}[language=Scala,numbers=none]
def CPS(e: Exp)(k: KVal => KExp) : KExp = 
  e match { ... }
\end{lstlisting}
\bigskip\bigskip

the continuation \texttt{k} can be thought of:\medskip

\small
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
let tmp0 = add 1 a in   
let tmp1 = mul (*@$\Box$@*) 5 in 
let tmp2 = add 3 tmp1 in 
let tmp3 = add tmp0 tmp2 in
  KReturn tmp3 
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{CPS-Translation}
\small

\begin{lstlisting}[language=Scala,numbers=none]
def CPS(e: Exp)(k: KVal => KExp) : KExp = 
  e match { 
     case Var(s) => k(KVar(s)) 
     case Num(i) => k(KNum(i))
     ...
  }
\end{lstlisting}
\bigskip\bigskip

\small
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
let tmp0 = add 1 a in   
let tmp1 = mul (*@$\Box$@*) 5 in 
let tmp2 = add 3 tmp1 in 
let tmp3 = add tmp0 tmp2 in
  KReturn tmp3 
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{CPS-Translation}
\small

\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
def CPS(e: Exp)(k: KVal => KExp) : KExp = e match { 
  case Aop(o, e1, e2) => {
    val z = Fresh("tmp")
    CPS(e1)(y1 => 
      CPS(e2)(y2 => 
               KLet(z, Kop(o, y1, y2), k(KVar(z)))))
  } ...
}
\end{lstlisting}
\mbox{}\\[-8mm]%
%
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
...
let z = op (*@$\Box_{y_1}$@*) (*@$\Box_{y_2}$@*)
let tmp0 = add 1 a in   
let tmp1 = mul (*@$\Box\!\!\!\!\raisebox{0.6mm}{\alert{\texttt{z}}}$@*) 5 in 
let tmp2 = add 3 tmp1 in 
let tmp3 = add tmp0 tmp2 in
  KReturn tmp3 
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{CPS-Translation}
\small

\begin{lstlisting}[language=Scala,numbers=none]
def CPS(e: Exp)(k: KVal => KExp) : KExp = 
  e match { 
    case Sequence(e1, e2) => 
      CPS(e1)(_ => CPS(e2)(y2 => k(y2)))
     ...
  }
\end{lstlisting}
\bigskip

\small
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
let tmp0 = add 1 a in   
let tmp1 = mul (*@$\Box$@*) 5 in 
let tmp2 = add 3 tmp1 in 
let tmp3 = add tmp0 tmp2 in
  KReturn tmp3 
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{CPS-Translation}
\small

\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
def CPS(e: Exp)(k: KVal => KExp) : KExp = 
  e match { 
    ...
    case If(Bop(o, b1, b2), e1, e2) => {
      val z = Fresh("tmp")
      CPS(b1)(y1 => 
        CPS(b2)(y2 => 
          KLet(z, Kop(o, y1, y2), 
                KIf(z, CPS(e1)(k), CPS(e2)(k)))))
     }
    ...
  }
\end{lstlisting}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{The Basic Language, 1980+}

\begin{lstlisting}[language={[Visual]Basic},numbers=none]
 5 LET S = 0
10 INPUT V 
20 PRINT "Input number"
30 IF N = 0 THEN GOTO 99 
40 FOR I = 1 TO N 
45 LET S = S + V(I) 
50 NEXT I 
60 PRINT S/N 
70 GOTO 5 
99 END
\end{lstlisting}

\hfill ``Spaghetti Code''
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{Target Specific ASM}

\begin{lstlisting}[language={},numbers=none]
llc -march=x86-64 fact.ll 
llc -march=arm fact.ll


Intel:  xorl  %eax, %eax
ARM:    mov   pc, lr
\end{lstlisting}

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



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]

\large\bf
Using a compiler, \\
how can you mount the\\ 
perfect attack against a system?

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mode<presentation>{
\begin{frame}[c]

{\large\bf
What 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]
  \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}[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 also
many in LLVM (some of them highest-level critical)\bigskip
\item about CompCert:

\begin{bubble}[10.7cm]\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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

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





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \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 hardware
faults.\bigskip

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

using 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 ensure
they are bug free/correct?\pause\bigskip

\item Very hard: Anything interesting about programs is equivalent
to 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}?\bigskip

Prog.~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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

