% !TEX program = xelatex
\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
\usepackage{../slides}
\usepackage{../langs}
\usepackage{../data}
\usepackage{../graphicss}
\usepackage{../grammar}
%\usepackage{soul}
%\usepackage{mathpartir}
\usetikzlibrary{shapes,arrows,shadows}
\usepackage[most]{tcolorbox}
\newtcbox{\hl}[1][]{%
size=fbox,
tcbox raise base, nobeforeafter,
enhanced, colframe=gray,
colback=gray!30, boxrule=1pt,
fontupper=\ttfamily,
#1}
% 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 Hour: & Thurdays 15 -- 16\\
Location: & N7.07 (North Wing, Bush House)\\
Slides \& Progs: & KEATS\\
Pollev: & \texttt{\alert{https://pollev.com/cfltutoratki576}}\\
\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{Stack Estimation}
%\small
%\mbox{}\\[-15mm]%
%
%\bl{\begin{center}
%\begin{tabular}{@{\hspace{-4mm}}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
%$\textit{estimate}(n)$ & $\dn$ & $1$\\
%$\textit{estimate}(x)$ & $\dn$ & $1$\\
%$\textit{estimate}(a_1\;aop\;a_2)$ & $\dn$ &
%$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
%$\textit{estimate}(\pcode{if}\;b\;\pcode{then}\;e_1\;\pcode{else}\;e_2)$ & $\dn$ &
%$\textit{estimate}(b) +$\\
%& & $\quad max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
%$\textit{estimate}(\pcode{write}(e))$ & $\dn$ &
%$\textit{estimate}(e) + 1$\\
%$\textit{estimate}(e_1 ; e_2)$ & $\dn$ &
%$max(\textit{estimate}(e_1), \textit{estimate}(e_2))$\\
%$\textit{estimate}(f(e_1, ..., e_n))$ & $\dn$ &
%$\sum_{i = 1..n}\;estimate(e_i)$\medskip\\
%$\textit{estimate}(a_1\;bop\;a_2)$ & $\dn$ &
%$\textit{estimate}(a_1) + \textit{estimate}(a_2)$\\
%\end{tabular}
%\end{center}}
%\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{\mbox{}\hspace{5cm}Factorial}
\begin{textblock}{7}(0,1.6)\footnotesize
\begin{minipage}{6cm}
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
.method public static fact(I)I
.limit locals 1
.limit stack 6
iload 0
ldc 0
if_icmpne If_else_0
ldc 1
goto If_end_1
If_else_0:
iload 0
iload 0
ldc 1
isub
invokestatic fact/fact/fact(I)I
imul
If_end_1:
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) =
if n == 0 then 1
else n * fact(n - 1)
\end{lstlisting}
\end{bubble}
\end{textblock}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{\mbox{}\hspace{5cm}Factorial}
\begin{textblock}{7}(0,1.0)\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]
\begin{textblock}{7}(1,-0.38)\footnotesize
\begin{minipage}{6cm}
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none, escapeinside={(*@}{@*)}]
.method public static facT(II)I
.limit locals 2
.limit stack 6
(*@\hl{facT\_Start:} @*)
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
(*@\hl{istore 1} @*)
(*@\hl{istore 0} @*)
(*@\hl{goto facT\_Start} @*)
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}[t, fragile]
\frametitle{Tail Recursion}
A call to \texttt{f(args)} is usually compiled as\medskip
{\small\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
args onto stack
invokestatic .../f
\end{lstlisting}}\pause
A call is in tail position provided:\medskip
{\small\begin{itemize}
\item \texttt{if Bexp then \hl{Exp} else \hl{Exp}}
\item \texttt{Exp ; \hl{Exp}}
\item \texttt{Exp op Exp}
\end{itemize}}\medskip
then a call \texttt{f(args)} can be compiled as\medskip\small
\begin{lstlisting}[numbers=none]
prepare environment
jump to start of function
\end{lstlisting}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c, fragile]
\frametitle{Tail Recursive Call}
\footnotesize
\begin{textblock}{13}(-0.3,3)
\begin{lstlisting}[language=Scala, numbers=none]
def compile_expT(a: Exp, env: Mem, name: String): Instrs =
...
case Call(n, args) => if (name == n)
{
val stores =
args.zipWithIndex.map { case (x, y) => i"istore $y" }
args.map(a => compile_expT(a, env, "")).mkString ++
stores.reverse.mkString ++
i"goto ${n}_Start"
} else {
val is = "I" * args.length
args.map(a => compile_expT(a, env, "")).mkString ++
i"invokestatic XXX/XXX/${n}(${is})I"
}
\end{lstlisting}
\end{textblock}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{???}
\small
\begin{tabular}{cc}
\includegraphics[scale=0.2]{basic-code.jpg} &
\includegraphics[scale=0.2]{machine-code.jpg}
\end{tabular}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{Opcodes}
\small
\begin{tabular}{cc}
\includegraphics[scale=0.3]{machine-code-large.png}
\end{tabular}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}<1-2>[t]
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{Peephole Optimisations}
\begin{center}
\begin{tabular}{ll}
\texttt{ldc}: & \texttt{iconst\_0} \ldots \texttt{iconst\_5}\\
& \texttt{bipush} $n$ where $-128 < n <= 128$\bigskip\\
\texttt{iload}: & \texttt{iload\_0} \ldots \texttt{iload\_3}\bigskip\\
\texttt{istore}: & \texttt{istore\_0} \ldots \texttt{istore\_3}\\
\end{tabular}
\end{center}
\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{KLet}
\begin{lstlisting}[language=LLVM]
tmp0 = add 1 a
tmp1 = mul b 5
tmp2 = add 3 tmp1
tmp3 = add tmp0 tmp2
\end{lstlisting}
\begin{lstlisting}[language=LLVMIR]
KLet tmp0 , add 1 a in
KLet tmp1 , mul b 5 in
KLet tmp2 , add 3 tmp1 in
KLet tmp3 , add tmp0 tmp2 in
...
\end{lstlisting}
\begin{lstlisting}[language=Scala,numbers=none]
case class KLet(x: String, e1: KVal, e2: KExp)
\end{lstlisting}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile,c]
\frametitle{KLet}
\begin{lstlisting}[language=LLVM]
tmp0 = add 1 a
tmp1 = mul b 5
tmp2 = add 3 tmp1
tmp3 = add tmp0 tmp2
\end{lstlisting}
\begin{lstlisting}[language=LLVMIR]
let tmp0 = add 1 a in
let tmp1 = mul b 5 in
let tmp2 = add 3 tmp1 in
let tmp3 = add tmp0 tmp2 in
...
\end{lstlisting}
\begin{lstlisting}[language=Scala,numbers=none]
case class KLet(x: String, e1: KVal, e2: 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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}<1-20>[c]
\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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%