diff -r 52263ffd17b9 -r 681c36b2af27 slides/slides09.tex --- 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{ +\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: -