--- a/slides/slides09.tex Sun Nov 24 16:30:34 2019 +0000
+++ b/slides/slides09.tex Thu Nov 28 08:18:57 2019 +0000
@@ -1,3 +1,4 @@
+% !TEX program = xelatex
\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
@@ -6,6 +7,7 @@
\usepackage{../grammar}
\usepackage{soul}
\usepackage{mathpartir}
+\usetikzlibrary{shapes,arrows,shadows}
% beamer stuff
\renewcommand{\slidecaption}{CFL 09, King's College London}
@@ -26,147 +28,456 @@
\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)\\
+ 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}
\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,fragile]
+\frametitle{Functional Programming}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}}
+\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);
-\mbox{}\\[-18mm]\mbox{}
+def fact(n) = if n == 0 then 1 else n * fact(n - 1);
-{\lstset{language=While}\fontsize{10}{12}\selectfont
-\texttt{\lstinputlisting{../progs/fib.while}}}
+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{BF***}
+\frametitle{Factorial on the JVM}
-some big array, say \texttt{a}; 7 (8) instructions:
+\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 \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}
+ \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}[c,fragile]
-\frametitle{Arrays in While}
+\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{itemize}
-\item \texttt{new arr[15000]}\medskip
-\item \texttt{x := 3 + arr[3 + y]}\medskip
-\item \texttt{arr[42 * n] := ...}
-\end{itemize}
+\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 Instructions}
+\small
+
+\begin{lstlisting}[language=LLVM]
+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]
+let tmp0 = add 1 a in
+let tmp1 = mul b 5 in
+let tmp2 = add 3 tmp1 in
+let tmp3 = add tmp0 tmp2 in
+ tmp3
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{New Arrays}
+\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}
-\begin{lstlisting}[mathescape,numbers=none,language=While]
- new arr[number]
-\end{lstlisting}\bigskip\bigskip
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile,c]
+\frametitle{K-(Intermediate)Language}
+\footnotesize
-\begin{lstlisting}[mathescape,numbers=none,language=While]
- ldc number
- newarray int
- astore loc_var
+\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
+abstract class KExp
+abstract class KVal
+
+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
+
+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
+
+\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}[c,fragile]
-\frametitle{Array Update}
+\begin{frame}[fragile,c]
+\frametitle{CPS-Translation}
+\small
-\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
+\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}
+\small
+\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}{\texttt{z}}$@*) 5 in
+let tmp2 = add 3 tmp1 in
+let tmp3 = add tmp0 tmp2 in
+ KReturn tmp3
+\end{lstlisting}
\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c,fragile]
-\frametitle{Array Lookup in AExp}
+\begin{frame}[fragile,c]
+\frametitle{CPS-Translation}
+\small
-\begin{lstlisting}[mathescape,numbers=none,language=While]
- ...arr[...]...
-\end{lstlisting}\bigskip\bigskip
+\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\bigskip
-\begin{lstlisting}[mathescape,numbers=none,language=While]
- aload loc_var
- index_aexp
- iaload
+\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 Sequence(e1, e2) =>
+ CPS(e1)(_ => CPS(e2)(y2 => k(y2)))
+ ...
+ }
+\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}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
+\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]
\large\bf
-Using a compiler, \\how can you mount the\\ perfect attack against a system?
+Using a compiler, \\
+how can you mount the\\
+perfect attack against a system?
-\end{frame}}
+\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -323,6 +634,129 @@
\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]
@@ -533,122 +967,3 @@
\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:
-