--- a/slides/slides09.tex Wed Nov 18 03:02:28 2015 +0000
+++ b/slides/slides09.tex Fri Nov 20 02:23:24 2015 +0000
@@ -62,12 +62,196 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t,fragile]
+\frametitle{Compiling AExps}
+
+For example \bl{$1 + ((2 * 3) + (4 - 3))$}:\medskip
+
+\begin{columns}[T]
+\begin{column}{.3\textwidth}
+\begin{center}
+\bl{\begin{tikzpicture}
+\tikzset{level distance=12mm,sibling distance=4mm}
+\tikzset{edge from parent/.style={draw,very thick}}
\Tree [.$+$ [.$1$ ] [.$+$ [.$*$ $2$ $3$ ] [.$-$ $4$ $3$ ]]]
\end{tikzpicture}}
+\end{center}
+\end{column}
+\begin{column}{.3\textwidth}
+\begin{lstlisting}[language=JVMIS,numbers=none]
+ldc 1
+ldc 2
+ldc 3
+imul
+ldc 4
+ldc 3
+isub
+iadd
+iadd
+\end{lstlisting}
+\end{column}
+\end{columns}\bigskip
+
+\small
+Traverse tree in post-order \bl{$\Rightarrow$} code for
+stack-machine
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling AExps}
+
+\bl{
+\begin{center}
+\begin{tabular}{lcl}
+$\textit{compile}(n, E)$ & $\dn$ & $\pcode{ldc}\;n$\smallskip\\
+$\textit{compile}(a_1 + a_2, E)$ & $\dn$ \\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\;\textit{compile}(a_2, E)\;@\; \pcode{iadd}$}\smallskip\\
+$\textit{compile}(a_1 - a_2, E)$ & $\dn$ \\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{isub}$}\smallskip\\
+$\textit{compile}(a_1 * a_2, E)$ & $\dn$ \\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{imul}$}\smallskip\\
+$\textit{compile}(a_1 \backslash a_2, E)$ & $\dn$\\
+\multicolumn{3}{c}{$\qquad\textit{compile}(a_1, E) \;@\; \textit{compile}(a_2, E)\;@\; \pcode{idiv}$}\smallskip\\
+$\textit{compile}(x, E)$ & $\dn$ & $\pcode{iload}\;E(x)$\\
+\end{tabular}
+\end{center}}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Ifs}
+
+For example
+
+\begin{lstlisting}[mathescape,numbers=none,language={}]
+if 1 = 1 then x := 2 else y := 3
+\end{lstlisting}
+
+
+\begin{center}
+\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
+ ldc 1
+ ldc 1
+ if_icmpne L_ifelse $\quad\tikz[remember picture] \node (C) {\mbox{}};$
+ ldc 2
+ istore 0
+ goto L_ifend $\quad\tikz[remember picture] \node (A) {\mbox{}};$
+L_ifelse: $\quad\tikz[remember picture] \node[] (D) {\mbox{}};$
+ ldc 3
+ istore 1
+L_ifend: $\quad\tikz[remember picture] \node[] (B) {\mbox{}};$
+\end{lstlisting}
+\end{center}
+
+\begin{tikzpicture}[remember picture,overlay]
\draw[->,very thick] (A) edge [->,to path={-- ++(10mm,0mm)
+ -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (B.east);
+ \draw[->,very thick] (C) edge [->,to path={-- ++(10mm,0mm)
+ -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (D.east);
\end{tikzpicture}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Whiles}
+
+For example
+
+\begin{lstlisting}[mathescape,numbers=none,language={}]
+while x <= 10 do x := x + 1
+\end{lstlisting}
+
+
+\begin{center}
+\begin{lstlisting}[mathescape,language=JVMIS,numbers=none]
+L_wbegin: $\quad\tikz[remember picture] \node[] (LB) {\mbox{}};$
+ iload 0
+ ldc 10
+ if_icmpgt L_wend $\quad\tikz[remember picture] \node (LC) {\mbox{}};$
+ iload 0
+ ldc 1
+ iadd
+ istore 0
+ goto L_wbegin $\quad\tikz[remember picture] \node (LA) {\mbox{}};$
+L_wend: $\quad\tikz[remember picture] \node[] (LD) {\mbox{}};$
+\end{lstlisting}
+\end{center}
+
+\begin{tikzpicture}[remember picture,overlay]
+ \draw[->,very thick] (LA) edge [->,to path={-- ++(12mm,0mm)
+ -- ++(0mm,17.3mm) |- (\tikztotarget)},line width=1mm] (LB.east);
+ \draw[->,very thick] (LC) edge [->,to path={-- ++(12mm,0mm)
+ -- ++(0mm,-17.3mm) |- (\tikztotarget)},line width=1mm] (LD.east);
\end{tikzpicture}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Writes}
+
+\small
+\begin{lstlisting}[language=JVMIS,mathescape,
+ numbers=none,xleftmargin=-6mm]
+.method public static write(I)V
+ .limit locals 1
+ .limit stack 2
+ getstatic java/lang/System/out
+ Ljava/io/PrintStream;
+ iload 0
+ invokevirtual java/io/PrintStream/println(I)V
+ return
+.end method
+
+
+
+iload $E(x)$
+invokestatic XXX/XXX/write(I)V
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c,fragile]
+\frametitle{Compiling Main}
+
+\footnotesize
+\begin{lstlisting}[language=JVMIS,mathescape,
+ numbers=none,xleftmargin=-6mm]
+.class public XXX.XXX
+.super java/lang/Object
+
+.method public <init>()V
+ aload_0
+ invokenonvirtual java/lang/Object/<init>()V
+ return
+.end method
+
+.method public static main([Ljava/lang/String;)V
+ .limit locals 200
+ .limit stack 200
+
+ $\textit{\ldots{}here comes the compiled code\ldots}$
+
+ return
+.end method
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c,fragile]
\frametitle{Functional Programming}
\footnotesize
\begin{textblock}{13}(0.9,3)
-\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
+\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);
@@ -137,76 +321,16 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Arithmetic Functions}
-
-Compilation of some aritmetic functions:
-
-\begin{center}
-\begin{tabular}{lcl}
-\texttt{Aop("+", a1, a2)} & $\Rightarrow$ & \texttt{...iadd}\\
-\texttt{Aop("-", a1, a2)} & $\Rightarrow$ & \texttt{...isub}\\
-\texttt{Aop("*", a1, a2)} & $\Rightarrow$ & \texttt{...imul}\\
-\texttt{Aop("/", a1, a2)} & $\Rightarrow$ & \texttt{...idiv}\\
-\texttt{Aop("\%", a1, a2)} & $\Rightarrow$ & \texttt{...irem}\\
-\end{tabular}
-\end{center}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Boolean Expressions}
-
-Compilation of Boolean expressions:
-
-\begin{center}
-\begin{tikzpicture}[node distance=2mm and 4mm,
- block/.style={rectangle, minimum size=1cm, draw=black, line width=1mm},
- point/.style={rectangle, inner sep=0mm, minimum size=0mm, fill=red},
- skip loop/.style={red, line width=1mm, to path={-- ++(0,-10mm) -| (\tikztotarget)}}]
-\node (A1) [point] {};
-\node (b) [block, right=of A1] {code of \bl{$b$}};
-\node (A2) [point, right=of b] {};
-\node (cs1) [block, right=of A2] {code of \bl{$cs_1$}};
-\node (A3) [point, right=of cs1] {};
-\node (cs2) [block, right=of A3] {code of \bl{$cs_2$}};
-\node (A4) [point, right=of cs2] {};
-
-\only<1>{
-\draw (A1) edge [->, red, line width=1mm] (b);
-\draw (b) edge [->, red, line width=1mm] (A2);
-\draw (A2) edge [skip loop] (A3);
-\draw (A3) edge [->, red, line width=1mm] (cs2);
-\draw (cs2) edge [->,red, line width=1mm] (A4);
-\node [below=of cs1] {\raisebox{-5mm}{\small{}conditional jump}};}
-\end{tikzpicture}
-\end{center}
-
-\begin{center}
-\begin{tabular}{lcl}
-\texttt{Bop("==", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpne...}\\
-\texttt{Bop("!=", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpeq...}\\
-\texttt{Bop("<", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpge...}\\
-\texttt{Bop("<=", a1, a2)} & $\Rightarrow$ & \texttt{...if\_icmpgt...}\\
-\end{tabular}
-\end{center}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c, fragile]
\frametitle{Sequences}
-Compiling \texttt{arg1 ; arg2}:\bigskip
+Compiling \texttt{exp1 ; exp2}:\bigskip
-\begin{lstlisting}[language=JVMIS, numbers=none]
-...arg1...
+\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
+$\textit{compile}$(exp1)
pop
-...arg1...
+$\textit{compile}$(exp2)
\end{lstlisting}
\end{frame}
@@ -216,25 +340,38 @@
\begin{frame}[c, fragile]
\frametitle{Write}
-Compiling call to \texttt{write(arg)}:\bigskip
+Compiling call to \texttt{write(1+2)}:\bigskip
-\begin{lstlisting}[language=JVMIS, numbers=none]
-...arg...
+\begin{lstlisting}[mathescape,language=JVMIS, numbers=none]
+$\textit{compile}$(1+2)
dup
invokestatic XXX/XXX/write(I)V
\end{lstlisting}\bigskip
\small
-needs a helper function
+needs the helper method
+\footnotesize
+\begin{lstlisting}[language=JVMIS,
+ xleftmargin=2mm,
+ numbers=none]
+.method public static write(I)V
+ .limit locals 1
+ .limit stack 2
+ getstatic java/lang/System/out Ljava/io/PrintStream;
+ iload 0
+ invokevirtual java/io/PrintStream/println(I)V
+ return
+.end method
+\end{lstlisting}
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c, fragile]
+\begin{frame}[t, fragile]
\frametitle{Function Definitions}
\footnotesize
@@ -251,12 +388,14 @@
.end method
\end{lstlisting}\bigskip
-\small We will need for definitions\footnotesize\medskip
+\small We will need for definitions, like\footnotesize\medskip
\begin{lstlisting}[language=JVMIS,
xleftmargin=2mm,
numbers=none]
-.method public static f (I...I)I
+def fname (x1, ... , xn) = ...
+
+.method public static fname (I...I)I
.limit locals ??
.limit stack ??
??
@@ -269,28 +408,28 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c, fragile]
\frametitle{Stack Estimation}
-\footnotesize
-\begin{center}
-\begin{lstlisting}[language=Scala,basicstyle=\ttfamily, numbers=none]
-def max_stack_exp(e: Exp): Int = e match {
- case Call(_, args) => args.map(max_stack_exp).sum
- case If(a, e1, e2) => max_stack_bexp(a) +
- (List(max_stack_exp(e1), max_stack_exp(e1)).max)
- case Write(e) => max_stack_exp(e) + 1
- case Var(_) => 1
- case Num(_) => 1
- case Aop(_, a1, a2) =>
- max_stack_exp(a1) + max_stack_exp(a2)
- case Sequ(e1, e2) =>
- List(max_stack_exp(e1), max_stack_exp(e2)).max
-}
+\small
+\mbox{}\\[-15mm]
-def max_stack_bexp(e: BExp): Int = e match {
- case Bop(_, a1, a2) =>
- max_stack_exp(a1) + max_stack_exp(a2)
-}
-\end{lstlisting}
-\end{center}
+\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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -304,7 +443,7 @@
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
.method public static suc(I)I
.limit locals 1
-.limit stack 3
+.limit stack 2
iload 0
ldc 1
iadd
@@ -337,7 +476,7 @@
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
.method public static add(II)I
.limit locals 2
-.limit stack 6
+.limit stack 5
iload 0
ldc 0
if_icmpne If_else
@@ -526,173 +665,97 @@
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\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]
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ \begin{frame}[c]
+ \frametitle{Dijkstra on Testing}
- \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}};
+ \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
- \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);
- }
+ \small
+ What is good about compilers: the either seem to work,
+ or go horribly wrong (most of the time).
- \onslide<3->{\node [above left=-1.5mm] at (C.south east) {\footnotesize \alert{$\blacksquare$}};}
-
- \end{tikzpicture}
- \end{center}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
+ \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
\begin{frame}[c]
+\frametitle{\Large Proving Programs to be Correct}
- \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)};}
+\begin{bubble}[10cm]
+\small
+{\bf Theorem:} There are infinitely many prime
+numbers.\medskip\\
- \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};
+{\bf Proof} \ldots\\
+\end{bubble}\bigskip
- \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};}
+
+similarly\bigskip
- \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};
+\begin{bubble}[10cm]
+\small
+{\bf Theorem:} The program is doing what
+it is supposed to be doing.\medskip
- \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}
+{\bf Long, long proof} \ldots\\
+\end{bubble}\bigskip\medskip
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \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{frame}[c]
+\frametitle{Can This Be Done?}
- \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]
+\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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- & Therefore in safety-critical systems it is important to rely
- on only a very small TCB.
- \end{tabular}
- \end{column}
- \end{columns}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Fuzzy Testing C-Compilers}
+
+\begin{itemize}
+\item tested GCC, LLVM and others by randomly generating
+C-programs
+\item found more than 300 bugs in GCC and also
+many in LLVM (some of them highest-level critical)\bigskip
+\item about CompCert:
- \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}}
+\begin{bubble}[10cm]\small ``The striking thing about our CompCert
+results is that the middle-end bugs we found in all other
+compilers are absent. As of early 2011, the under-development
+version of CompCert is the only compiler we have tested for
+which Csmith cannot find wrong-code errors. This is not for
+lack of trying: we have devoted about six CPU-years to the
+task.''
+\end{bubble}
+\end{itemize}
- \end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}