slides/slides09.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Tue, 14 Dec 2021 11:40:31 +0000
changeset 863 00318ffa4676
parent 853 851d8c00f033
child 864 a24633510c0a
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
     1
% !TEX program = xelatex
744
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
     2
\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{beamer}
309
640e4a05cd9b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     3
\usepackage{../slides}
215
828303e8e4af updated slides
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 207
diff changeset
     4
\usepackage{../langs}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
     5
\usepackage{../data}
309
640e4a05cd9b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
     6
\usepackage{../graphics}
379
fa2589ec0fae updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 312
diff changeset
     7
\usepackage{../grammar}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
     8
\usepackage{soul}
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
     9
\usepackage{mathpartir}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    10
\usetikzlibrary{shapes,arrows,shadows}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    11
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    12
% beamer stuff
459
858f62bc930a updated
Christian Urban <urbanc@in.tum.de>
parents: 384
diff changeset
    13
\renewcommand{\slidecaption}{CFL 09, King's College London}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    14
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    15
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    16
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    17
\begin{document}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    18
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    19
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
309
640e4a05cd9b updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 215
diff changeset
    20
\begin{frame}[t]
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    21
\frametitle{%
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    22
  \begin{tabular}{@ {}c@ {}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    23
  \\[-3mm]
459
858f62bc930a updated
Christian Urban <urbanc@in.tum.de>
parents: 384
diff changeset
    24
  \LARGE Compilers and \\[-2mm] 
744
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    25
  \LARGE Formal Languages\\[3mm] 
65
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    26
  \end{tabular}}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    27
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    28
  \normalsize
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    29
  \begin{center}
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff changeset
    30
  \begin{tabular}{ll}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    31
    Email:  & christian.urban at kcl.ac.uk\\
744
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    32
    %Office Hours: & Thursdays 12 -- 14\\
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    33
    %Location: & N7.07 (North Wing, Bush House)\\
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    34
    Slides \& Progs: & KEATS (also homework is there)\\  
538
e03107e79d26 updated
Christian Urban <urbanc@in.tum.de>
parents: 537
diff changeset
    35
  \end{tabular}
e03107e79d26 updated
Christian Urban <urbanc@in.tum.de>
parents: 537
diff changeset
    36
  \end{center}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
    37
744
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    38
  \begin{center}
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    39
    \begin{tikzpicture}
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    40
      \node[drop shadow,fill=white,inner sep=0pt] 
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    41
      {\footnotesize\rowcolors{1}{capri!10}{white}
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    42
        \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    43
          1 Introduction, Languages          & 6 While-Language \\
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    44
          2 Regular Expressions, Derivatives & 7 Compilation, JVM \\
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    45
          3 Automata, Regular Languages      & 8 Compiling Functional Languages \\
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    46
          4 Lexing, Tokenising               & \cellcolor{blue!50} 9 Optimisations \\
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    47
          5 Grammars, Parsing                & 10 LLVM \\ \hline
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    48
        \end{tabular}%
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    49
      };
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    50
    \end{tikzpicture}
a33ce6c8e2c3 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 702
diff changeset
    51
  \end{center}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    52
\end{frame}
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    53
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    54
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    55
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    56
\begin{frame}[c,fragile]
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
    57
\frametitle{The Fun Language}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    58
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    59
\footnotesize
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    60
\begin{textblock}{13}(0.9,3)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    61
\begin{lstlisting}[]numbers=none]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    62
def fib(n) = if n == 0 then 0 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    63
             else if n == 1 then 1 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    64
             else fib(n - 1) + fib(n - 2);
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    65
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    66
def fact(n) = if n == 0 then 1 else n * fact(n - 1);
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    67
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    68
def ack(m, n) = if m == 0 then n + 1
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    69
                else if n == 0 then ack(m - 1, 1)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    70
                else ack(m - 1, ack(m, n - 1));
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    71
                
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    72
def gcd(a, b) = if b == 0 then a else gcd(b, a % b);                
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    73
\end{lstlisting}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
    74
\end{textblock}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    75
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    76
\end{frame}
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
    77
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
853
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    78
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    79
\begin{frame}[c,fragile]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    80
\frametitle{\mbox{}\hspace{5cm}Factorial}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    81
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    82
\begin{textblock}{7}(0,1.0)\footnotesize
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    83
\begin{minipage}{6cm}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    84
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    85
.method public static facT(II)I 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    86
.limit locals 2
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    87
.limit stack 6
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    88
  iload 0
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    89
  ldc 0
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    90
  if_icmpne If_else_2
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    91
  iload 1
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    92
  goto If_end_3
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    93
If_else_2:
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    94
  iload 0
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    95
  ldc 1
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    96
  isub
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    97
  iload 0
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    98
  iload 1
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
    99
  imul
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   100
  invokestatic fact/fact/facT(II)I
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   101
If_end_3:
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   102
  ireturn
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   103
.end method 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   104
\end{lstlisting}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   105
\end{minipage}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   106
\end{textblock}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   107
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   108
\begin{textblock}{7}(6,7)
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   109
\begin{bubble}[7cm]\small
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   110
\begin{lstlisting}[language=Lisp,
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   111
                   basicstyle=\ttfamily, 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   112
                   numbers=none,
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   113
                   xleftmargin=1mm,linebackgroundcolor=\color{cream}]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   114
def facT(n, acc) = 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   115
  if n == 0 then acc 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   116
  else facT(n - 1, n * acc);
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   117
\end{lstlisting}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   118
\end{bubble}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   119
\end{textblock}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   120
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   121
\end{frame}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   122
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   123
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   124
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   125
\begin{frame}[fragile]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   126
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   127
\begin{textblock}{7}(1,-0.2)\footnotesize
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   128
\begin{minipage}{6cm}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   129
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none, escapeinside={(*@}{@*)}]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   130
.method public static facT(II)I 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   131
.limit locals 2
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   132
.limit stack 6
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   133
(*@\hl{facT\_Start:} @*)
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   134
  iload 0
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   135
  ldc 0
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   136
  if_icmpne If_else_2
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   137
  iload 1
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   138
  goto If_end_3
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   139
If_else_2:
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   140
  iload 0
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   141
  ldc 1
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   142
  isub
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   143
  iload 0
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   144
  iload 1
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   145
  imul
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   146
  (*@\hl{istore 1} @*)
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   147
  (*@\hl{istore 0} @*)
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   148
  (*@\hl{goto facT\_Start} @*)
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   149
If_end_3:
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   150
  ireturn
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   151
.end method 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   152
\end{lstlisting}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   153
\end{minipage}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   154
\end{textblock}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   155
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   156
\begin{textblock}{7}(6,7)
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   157
\begin{bubble}[7cm]\small
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   158
\begin{lstlisting}[language=Lisp,
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   159
                   basicstyle=\ttfamily, 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   160
                   numbers=none,
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   161
                   xleftmargin=1mm,linebackgroundcolor=\color{cream}]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   162
def facT(n, acc) = 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   163
  if n == 0 then acc 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   164
  else facT(n - 1, n * acc);
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   165
\end{lstlisting}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   166
\end{bubble}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   167
\end{textblock}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   168
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   169
\end{frame}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   170
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   171
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   172
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   173
\begin{frame}[t, fragile]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   174
\frametitle{Tail Recursion}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   175
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   176
A call to \texttt{f(args)} is usually compiled as\medskip
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   177
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   178
{\small\begin{lstlisting}[basicstyle=\ttfamily, numbers=none]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   179
  args onto stack
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   180
  invokestatic  .../f 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   181
\end{lstlisting}}\pause
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   182
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   183
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   184
A call is in tail position provided:\medskip
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   185
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   186
{\small\begin{itemize}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   187
\item \texttt{if Bexp then \hl{Exp} else \hl{Exp}}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   188
\item \texttt{Exp ; \hl{Exp}}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   189
\item \texttt{Exp  op Exp}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   190
\end{itemize}}\medskip
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   191
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   192
then a call \texttt{f(args)} can be compiled as\medskip\small
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   193
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   194
\begin{lstlisting}[numbers=none]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   195
  prepare environment
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   196
  jump to start of function
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   197
\end{lstlisting}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   198
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   199
\end{frame}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   200
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   201
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   202
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   203
\begin{frame}[c, fragile]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   204
\frametitle{Tail Recursive Call}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   205
\footnotesize
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   206
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   207
\begin{textblock}{13}(-0.3,3)
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   208
\begin{lstlisting}[language=Scala, numbers=none]
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   209
def compile_expT(a: Exp, env: Mem, name: String): Instrs = 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   210
  ...
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   211
  case Call(n, args) => if (name == n)
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   212
  {
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   213
    val stores =
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   214
      args.zipWithIndex.map { case (x, y) => i"istore $y" } 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   215
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   216
    args.map(a => compile_expT(a, env, "")).mkString ++
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   217
    stores.reverse.mkString ++ 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   218
    i"goto ${n}_Start" 
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   219
  } else {
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   220
    val is = "I" * args.length
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   221
    args.map(a => compile_expT(a, env, "")).mkString ++
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   222
    i"invokestatic XXX/XXX/${n}(${is})I"
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   223
  }
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   224
\end{lstlisting}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   225
\end{textblock}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   226
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   227
\end{frame}
851d8c00f033 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 822
diff changeset
   228
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   229
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   230
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   231
\begin{frame}[c,fragile]
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   232
\frametitle{Factorial Funct.~on the JVM}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   233
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   234
\begin{textblock}{7}(1,1.8)\footnotesize
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   235
\begin{minipage}{6cm}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   236
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   237
.method public static facT(II)I 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   238
.limit locals 2
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   239
.limit stack 6
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   240
  iload 0
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   241
  ldc 0
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   242
  if_icmpne If_else_2
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   243
  iload 1
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   244
  goto If_end_3
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   245
If_else_2:
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   246
  iload 0
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   247
  ldc 1
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   248
  isub
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   249
  iload 0
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   250
  iload 1
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   251
  imul
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   252
  invokestatic fact/fact/facT(II)I
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   253
If_end_3:
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   254
  ireturn
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   255
.end method 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   256
\end{lstlisting}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   257
\end{minipage}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   258
\end{textblock}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   259
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   260
\begin{textblock}{7}(6,7)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   261
\begin{bubble}[7cm]\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   262
\begin{lstlisting}[language=Lisp,
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   263
                   basicstyle=\ttfamily, 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   264
                   numbers=none,
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   265
                   xleftmargin=1mm,linebackgroundcolor=\color{cream}]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   266
def facT(n, acc) = 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   267
  if n == 0 then acc 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   268
  else facT(n - 1, n * acc);
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   269
\end{lstlisting}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   270
\end{bubble}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   271
\end{textblock}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   272
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   273
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   274
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   275
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   276
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   277
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   278
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   279
\frametitle{LLVM}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   280
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   281
\begin{itemize}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   282
  \item Chris Lattner, Vikram Adve (started in 2000)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   283
  \item Apple hired Lattner in 2006
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   284
  \item modular architecture, LLVM-IR
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   285
  \item \texttt{lli} and \texttt{llc} 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   286
\end{itemize}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   287
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   288
\end{frame}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   289
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   290
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   291
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   292
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   293
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   294
\tikzstyle{sensor}=[draw, fill=blue!20, text width=3.8em, line width=1mm,
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   295
    text centered, minimum height=2em,drop shadow]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   296
\tikzstyle{ann} = [above, text width=4em, text centered]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   297
\tikzstyle{sc} = [sensor, text width=7em, fill=red!20, 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   298
    minimum height=6em, rounded corners, drop shadow,line width=1mm]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   299
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   300
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   301
\frametitle{LLVM: Overview}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   302
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   303
\begin{tikzpicture}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   304
    % Validation Layer is the same except that there are a set of nodes and links which are added
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   305
   
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   306
    \path (0,0) node (IR) [sc] {\textbf{LLVM-IR}\\ Optimisations};
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   307
    \path (IR.west)+(-2.2,1.7) node (sou1) [sensor] {C++};
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   308
    \path (IR.west)+(-2.2,0.5) node (sou2)[sensor] {C};
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   309
    \path (IR.west)+(-2.2,-1.0) node (dots)[ann] {$\vdots$}; 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   310
    \path (IR.west)+(-2.2,-1.8) node (sou3)[sensor] {Haskell};    
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   311
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   312
    \path [draw,->,line width=1mm] (sou1.east) -- node [above] {} (IR.160);
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   313
    \path [draw,->,line width=1mm] (sou2.east) -- node [above] {} (IR.180);
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   314
    \path [draw,->,line width=1mm] (sou3.east) -- node [above] {} (IR.200);
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   315
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   316
    \path (IR.east)+(2.2,2.0)  node (tar1)[sensor] {x86};
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   317
    \path (IR.east)+(2.2,0.8)  node (tar2)[sensor] {ARM};
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   318
    \path (IR.east)+(2.2,-0.4) node (tar3)[sensor] {MIPS}; 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   319
    \path (IR.east)+(2.2,-1.6) node (tar4)[sensor] {RISC}; 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   320
    \path (IR.east)+(2.2,-2.8) node (tar5)[sensor] {Power PC};
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   321
    \path (IR.east)+(2.2,-4.2) node (dots2)[ann] {$\vdots$};
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   322
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   323
    \path [draw,<-,line width=1mm] (tar1.west) -- node [above] {} (IR.10);
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   324
    \path [draw,<-,line width=1mm] (tar2.west) -- node [above] {} (IR.5);
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   325
    \path [draw,<-,line width=1mm] (tar3.west) -- node [above] {} (IR.0);
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   326
    \path [draw,<-,line width=1mm] (tar4.west) -- node [above] {} (IR.-5);
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   327
    \path [draw,<-,line width=1mm] (tar5.west) -- node [above] {} (IR.-10);
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   328
    
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   329
\end{tikzpicture}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   330
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   331
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   332
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   333
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   334
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   335
\begin{frame}[fragile,t]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   336
\frametitle{LLVM-IR}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   337
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   338
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   339
\begin{textblock}{7.7}(8,11.4)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   340
\begin{bubble}[5cm]\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   341
\begin{lstlisting}[language=Lisp,
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   342
                   numbers=none,
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   343
                   xleftmargin=1mm,linebackgroundcolor=\color{cream}]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   344
def fact(n) =
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   345
  if n == 0 then 1 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   346
  else n * fact(n - 1)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   347
\end{lstlisting}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   348
\end{bubble}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   349
\end{textblock}
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   350
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   351
\begin{lstlisting}[language=LLVM,xleftmargin=-7mm]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   352
define i32 @fact (i32 %n) {
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   353
   %tmp_19 = icmp eq i32  %n, 0
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   354
   br i1 %tmp_19, label %if_br_23, label %else_br_24
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   355
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   356
if_br_23:
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   357
   ret i32 1
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   358
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   359
else_br_24:
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   360
   %tmp_21 = sub i32  %n, 1
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   361
   %tmp_22 = call i32 @fact (i32 %tmp_21)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   362
   %tmp_20 = mul i32  %n, %tmp_22
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   363
   ret i32 %tmp_20
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   364
}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   365
\end{lstlisting}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   366
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   367
\end{frame}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   368
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   369
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   370
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   371
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   372
\frametitle{LLVM Types}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   373
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   374
\tt
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   375
\begin{center}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   376
\begin{tabular}{ll}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   377
boolean & i1 \\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   378
byte    & i8 \\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   379
short   & i16\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   380
char    & i16\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   381
integer & i32\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   382
long    & i64\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   383
float   & float\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   384
double  & double\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   385
*\_      & pointer to \\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   386
**\_     & pointer to a pointer to\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   387
\mbox{}[\_]    & arrays of\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   388
\end{tabular}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   389
\end{center}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   390
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   391
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   392
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   393
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   394
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   395
\begin{frame}[fragile,c]
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   396
\frametitle{LLVM-IR Instructions}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   397
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   398
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   399
\begin{lstlisting}[language=LLVM,xleftmargin=0mm]
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   400
br i1 %var, label %if_br, label %else_br
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   401
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   402
icmp eq i32  %x, %y     ; for equal
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   403
icmp sle i32 %x, %y     ;   signed less or equal
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   404
icmp slt i32 %x, %y     ;   signed less than
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   405
icmp ult i32 %x, %y     ;   unsigned less than 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   406
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   407
%var = call i32 @foo(...args...)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   408
\end{lstlisting}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   409
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   410
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   411
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   412
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   413
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   414
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   415
\frametitle{SSA Format}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   416
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   417
\bl{$(1 + a) + (3 + (b * 5))$}\bigskip\bigskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   418
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   419
\begin{lstlisting}[language=LLVM]
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   420
tmp0 = add 1 a   
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   421
tmp1 = mul b 5 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   422
tmp2 = add 3 tmp1 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   423
tmp3 = add tmp0 tmp2  
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   424
\end{lstlisting}\bigskip\bigskip
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   425
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   426
\hfill Static Single Assignment
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   427
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   428
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   429
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   430
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   431
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   432
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   433
\frametitle{Abstract Syntax Trees}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   434
\footnotesize
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   435
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   436
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   437
// Fun language (expressions)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   438
abstract class Exp 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   439
abstract class BExp 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   440
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   441
case class Call(name: String, args: List[Exp]) extends Exp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   442
case class If(a: BExp, e1: Exp, e2: Exp) extends Exp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   443
case class Write(e: Exp) extends Exp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   444
case class Var(s: String) extends Exp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   445
case class Num(i: Int) extends Exp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   446
case class Aop(o: String, a1: Exp, a2: Exp) extends Exp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   447
case class Sequence(e1: Exp, e2: Exp) extends Exp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   448
case class Bop(o: String, a1: Exp, a2: Exp) extends BExp  
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   449
\end{lstlisting}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   450
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   451
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   452
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   453
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   454
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   455
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   456
\frametitle{K-(Intermediate)Language}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   457
\footnotesize
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   458
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   459
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   460
abstract class KExp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   461
abstract class KVal
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   462
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   463
// K-Values
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   464
case class KVar(s: String) extends KVal
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   465
case class KNum(i: Int) extends KVal
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   466
case class Kop(o: String, v1: KVal, v2: KVal) extends KVal
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   467
case class KCall(o: String, vrs: List[KVal]) extends KVal
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   468
case class KWrite(v: KVal) extends KVal
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   469
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   470
// K-Expressions
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   471
case class KIf(x1: String, e1: KExp, e2: KExp) extends KExp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   472
case class KLet(x: String, v: KVal, e: KExp) extends KExp
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   473
case class KReturn(v: KVal) extends KExp
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   474
\end{lstlisting}
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   475
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   476
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   477
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   478
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   479
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   480
\begin{frame}[fragile,c]
819
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   481
\frametitle{KLet}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   482
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   483
\begin{lstlisting}[language=LLVM]
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   484
tmp0 = add 1 a   
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   485
tmp1 = mul b 5 
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   486
tmp2 = add 3 tmp1 
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   487
tmp3 = add tmp0 tmp2  
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   488
\end{lstlisting}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   489
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   490
\begin{lstlisting}[language=LLVMIR]
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   491
  KLet tmp0 , add 1 a in  
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   492
   KLet tmp1 , mul b 5 in
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   493
    KLet tmp2 , add 3 tmp1 in 
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   494
     KLet tmp3 , add tmp0 tmp2 in
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   495
      ...
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   496
\end{lstlisting}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   497
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   498
\begin{lstlisting}[language=Scala,numbers=none]
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   499
case class KLet(x: String, e1: KVal, e2: KExp)
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   500
\end{lstlisting}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   501
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   502
\end{frame}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   503
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   504
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   505
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   506
\begin{frame}[fragile,c]
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   507
\frametitle{KLet}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   508
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   509
\begin{lstlisting}[language=LLVM]
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   510
tmp0 = add 1 a   
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   511
tmp1 = mul b 5 
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   512
tmp2 = add 3 tmp1 
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   513
tmp3 = add tmp0 tmp2  
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   514
\end{lstlisting}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   515
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   516
\begin{lstlisting}[language=LLVMIR]
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   517
  let tmp0 = add 1 a in  
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   518
   let tmp1 = mul b 5 in
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   519
    let tmp2 = add 3 tmp1 in 
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   520
     let tmp3 = add tmp0 tmp2 in
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   521
      ...
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   522
\end{lstlisting}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   523
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   524
\begin{lstlisting}[language=Scala,numbers=none]
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   525
case class KLet(x: String, e1: KVal, e2: KExp)
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   526
\end{lstlisting}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   527
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   528
\end{frame}
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   529
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   530
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   531
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   532
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   533
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
c9859fa5178f updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 744
diff changeset
   534
\begin{frame}[fragile,c]
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   535
\frametitle{CPS-Translation}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   536
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   537
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   538
\begin{lstlisting}[language=Scala,numbers=none]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   539
def CPS(e: Exp)(k: KVal => KExp) : KExp = 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   540
  e match { ... }
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   541
\end{lstlisting}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   542
\bigskip\bigskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   543
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   544
the continuation \texttt{k} can be thought of:\medskip
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   545
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   546
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   547
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   548
let tmp0 = add 1 a in   
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   549
let tmp1 = mul (*@$\Box$@*) 5 in 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   550
let tmp2 = add 3 tmp1 in 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   551
let tmp3 = add tmp0 tmp2 in
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   552
  KReturn tmp3 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   553
\end{lstlisting}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   554
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   555
\end{frame}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   556
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   557
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   558
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   559
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   560
\frametitle{CPS-Translation}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   561
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   562
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   563
\begin{lstlisting}[language=Scala,numbers=none]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   564
def CPS(e: Exp)(k: KVal => KExp) : KExp = 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   565
  e match { 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   566
     case Var(s) => k(KVar(s)) 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   567
     case Num(i) => k(KNum(i))
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   568
     ...
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   569
  }
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   570
\end{lstlisting}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   571
\bigskip\bigskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   572
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   573
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   574
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   575
let tmp0 = add 1 a in   
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   576
let tmp1 = mul (*@$\Box$@*) 5 in 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   577
let tmp2 = add 3 tmp1 in 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   578
let tmp3 = add tmp0 tmp2 in
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   579
  KReturn tmp3 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   580
\end{lstlisting}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   581
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   582
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   583
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   584
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   585
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   586
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   587
\frametitle{CPS-Translation}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   588
\small
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   589
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   590
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   591
def CPS(e: Exp)(k: KVal => KExp) : KExp = e match { 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   592
  case Aop(o, e1, e2) => {
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   593
    val z = Fresh("tmp")
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   594
    CPS(e1)(y1 => 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   595
      CPS(e2)(y2 => 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   596
               KLet(z, Kop(o, y1, y2), k(KVar(z)))))
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   597
  } ...
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   598
}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   599
\end{lstlisting}
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   600
\mbox{}\\[-8mm]%
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   601
%
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   602
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   603
...
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   604
let z = op (*@$\Box_{y_1}$@*) (*@$\Box_{y_2}$@*)
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   605
let tmp0 = add 1 a in   
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   606
let tmp1 = mul (*@$\Box\!\!\!\!\raisebox{0.6mm}{\alert{\texttt{z}}}$@*) 5 in 
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   607
let tmp2 = add 3 tmp1 in 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   608
let tmp3 = add tmp0 tmp2 in
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   609
  KReturn tmp3 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   610
\end{lstlisting}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   611
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   612
\end{frame}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   613
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   614
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   615
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   616
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   617
\frametitle{CPS-Translation}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   618
\small
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   619
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   620
\begin{lstlisting}[language=Scala,numbers=none]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   621
def CPS(e: Exp)(k: KVal => KExp) : KExp = 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   622
  e match { 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   623
    case Sequence(e1, e2) => 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   624
      CPS(e1)(_ => CPS(e2)(y2 => k(y2)))
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   625
     ...
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   626
  }
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   627
\end{lstlisting}
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   628
\bigskip
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   629
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   630
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   631
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   632
let tmp0 = add 1 a in   
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   633
let tmp1 = mul (*@$\Box$@*) 5 in 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   634
let tmp2 = add 3 tmp1 in 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   635
let tmp3 = add tmp0 tmp2 in
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   636
  KReturn tmp3 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   637
\end{lstlisting}
609
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   638
ff17a6f694dd updated
Christian Urban <urbanc@in.tum.de>
parents: 538
diff changeset
   639
\end{frame}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   640
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
310
d384fe01d0e8 updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents: 309
diff changeset
   641
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   642
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   643
\begin{frame}[fragile,c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   644
\frametitle{CPS-Translation}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   645
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   646
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   647
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   648
def CPS(e: Exp)(k: KVal => KExp) : KExp = 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   649
  e match { 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   650
    ...
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   651
    case If(Bop(o, b1, b2), e1, e2) => {
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   652
      val z = Fresh("tmp")
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   653
      CPS(b1)(y1 => 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   654
        CPS(b2)(y2 => 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   655
          KLet(z, Kop(o, y1, y2), 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   656
                KIf(z, CPS(e1)(k), CPS(e2)(k)))))
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   657
     }
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   658
    ...
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   659
  }
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   660
\end{lstlisting}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   661
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   662
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   663
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   664
702
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   665
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   666
\begin{frame}[c,fragile]
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   667
\frametitle{The Basic Language, 1980+}
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   668
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   669
\begin{lstlisting}[language={[Visual]Basic},numbers=none]
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   670
 5 LET S = 0
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   671
10 INPUT V 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   672
20 PRINT "Input number"
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   673
30 IF N = 0 THEN GOTO 99 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   674
40 FOR I = 1 TO N 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   675
45 LET S = S + V(I) 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   676
50 NEXT I 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   677
60 PRINT S/N 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   678
70 GOTO 5 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   679
99 END
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   680
\end{lstlisting}
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   681
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   682
\hfill ``Spaghetti Code''
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   683
\end{frame}
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   684
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   685
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   686
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   687
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   688
\begin{frame}[c,fragile]
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   689
\frametitle{Target Specific ASM}
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   690
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   691
\begin{lstlisting}[language={},numbers=none]
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   692
llc -march=x86-64 fact.ll 
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   693
llc -march=arm fact.ll
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   694
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   695
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   696
Intel:  xorl  %eax, %eax
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   697
ARM:    mov   pc, lr
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   698
\end{lstlisting}
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   699
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   700
\end{frame}
67ab7162a861 updated
Christian Urban <urbanc@in.tum.de>
parents: 701
diff changeset
   701
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   702
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   703
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   704
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   705
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   706
\begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   707
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   708
\large\bf
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   709
Using a compiler, \\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   710
how can you mount the\\ 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   711
perfect attack against a system?
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   712
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   713
\end{frame}
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   714
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   715
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   716
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   717
\mode<presentation>{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   718
\begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   719
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   720
{\large\bf
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   721
What is a \alert{perfect} attack?}\bigskip
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   722
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   723
\begin{enumerate}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   724
\item you can potentially completely take over a target system
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   725
\item your attack is (nearly) undetectable
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   726
\item the victim has (almost) no chance to recover
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   727
\end{enumerate}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   728
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   729
\end{frame}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   730
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   731
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   732
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   733
\mode<presentation>{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   734
\begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   735
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   736
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   737
  \begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   738
  \begin{tikzpicture}[scale=1]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   739
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   740
  \onslide<1->{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   741
  \node (A) at (0,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=17mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   742
  \node [below right] at (A.north west) {\footnotesize\begin{tabular}{@{}l@{}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   743
  \only<1,2>{clean}\only<3->{\alert{hacked}}\\compiler\end{tabular}};}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   744
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   745
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   746
  \onslide<2->{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   747
  \node (B) at (-2,2)  [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   748
  \node [below right] at (B.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(src)\end{tabular}};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   749
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   750
  \node (C) at (2,2)  [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   751
  \node [below right] at (C.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(bin)\end{tabular}};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   752
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   753
  \draw[->, line width=2mm] (B) -- (C);
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   754
  }
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   755
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   756
 \onslide<3->{\node [above left=-1.5mm] at (C.south east) {\footnotesize \alert{$\blacksquare$}};}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   757
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   758
  \end{tikzpicture}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   759
  \end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   760
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   761
\end{frame}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   762
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   763
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   764
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   765
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   766
\mode<presentation>{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   767
\begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   768
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   769
  \begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   770
  \begin{tikzpicture}[scale=1]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   771
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   772
  \onslide<1->{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   773
  \node (A) at (0,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   774
  \node [below right] at (A.north west) {\small V0.01};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   775
  \node [below right] (A1) at (A.south west) {\small Scala};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   776
  \node [below right] (A1) at (A1.south west) {\small\textcolor{gray}{host language}};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   777
  \node [above right] at (A.north west) {my compiler (src)};}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   778
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   779
  \onslide<2->{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   780
  \node (B) at (1.8,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   781
  \node [below right] at (B.north west) {\small V0.02};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   782
  \node [below right] at (B.south west) {\small Scala};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   783
  \node at (3,0) {\ldots};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   784
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   785
  \node (C) at (5,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   786
  \node [below right] at (C.north west) {\small V1.00};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   787
  \node [below right] at (C.south west) {\small Scala};}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   788
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   789
  \onslide<3->{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   790
  \node (D) at (6.8,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   791
  \node [below right] at (D.north west) {\small V1.00};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   792
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   793
  \node (E) at (6.8,2)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   794
  \node [below right] at (E.north west) {\small V1.01};}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   795
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   796
  \onslide<4->{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   797
  \node (F) at (8.6,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   798
  \node [below right] at (F.north west) {\small V1.01};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   799
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   800
  \node (G) at (8.6,2)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   801
  \node [below right] at (G.north west) {\small V1.02};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   802
  \node at (9.8,0) {\ldots};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   803
  \node at (9.8,2) {\ldots};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   804
  \node at (8,-2) {\textcolor{gray}{\begin{tabular}{@{}l@{}}no host language\\needed\end{tabular}}};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   805
  }
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   806
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   807
  \end{tikzpicture}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   808
  \end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   809
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   810
\end{frame}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   811
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   812
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   813
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   814
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   815
  \mode<presentation>{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   816
  \begin{frame}<1-3>
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   817
  \frametitle{\LARGE\begin{tabular}{c}Hacking Compilers 
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   818
  \end{tabular}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   819
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   820
  %Why is it so paramount to have a small trusted code base (TCB)?
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   821
  \bigskip\bigskip
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   822
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   823
  \begin{columns}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   824
  \begin{column}{2.7cm}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   825
  \begin{minipage}{2.5cm}%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   826
  \begin{tabular}{c@ {}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   827
  \includegraphics[scale=0.2]{../pics/ken-thompson.jpg}\\[-1.8mm]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   828
  \footnotesize Ken Thompson\\[-1.8mm]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   829
  \footnotesize Turing Award, 1983\\
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   830
  \end{tabular}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   831
  \end{minipage}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   832
  \end{column}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   833
  \begin{column}{9cm}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   834
  \begin{tabular}{l@ {\hspace{1mm}}p{8cm}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   835
 
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   836
  & Ken Thompson showed how to hide a Trojan Horse in a 
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   837
  compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   838
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   839
  & No amount of source level verification will protect 
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   840
  you from such Thompson-hacks.\\[2mm]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   841
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   842
  \end{tabular}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   843
  \end{column}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   844
  \end{columns}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   845
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   846
  \only<2>{
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   847
  \begin{textblock}{6}(4,2)
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   848
  \begin{tikzpicture}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   849
  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   850
  {\normalsize
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   851
  \begin{minipage}{8cm}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   852
  \begin{quote}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   853
  \includegraphics[scale=0.05]{../pics/evil.png}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   854
  \begin{enumerate}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   855
  \item[1)] Assume you ship the compiler as binary and also with sources.
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   856
  \item[2)] Make the compiler aware when it compiles itself.
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   857
  \item[3)] Add the Trojan horse.
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   858
  \item[4)] Compile.
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   859
  \item[5)] Delete Trojan horse from the sources of the compiler.
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   860
  \item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   861
  \end{enumerate}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   862
  \end{quote}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   863
  \end{minipage}};
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   864
  \end{tikzpicture}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   865
  \end{textblock}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   866
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   867
  \end{frame}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   868
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   869
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   870
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   871
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   872
  \begin{frame}[c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   873
  \frametitle{Dijkstra on Testing}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   874
  
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   875
  \begin{bubble}[10cm]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   876
  ``Program testing can be a very effective way to show the
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   877
  presence of bugs, but it is hopelessly inadequate for showing
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   878
  their absence.''
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   879
  \end{bubble}\bigskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   880
  
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   881
  \small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   882
  What is good about compilers: the either seem to work,
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   883
  or go horribly wrong (most of the time).
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   884
  
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   885
  \end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   886
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   887
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   888
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   889
\begin{frame}[c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   890
\frametitle{\Large Proving Programs to be Correct}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   891
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   892
\begin{bubble}[10cm]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   893
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   894
{\bf Theorem:} There are infinitely many prime 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   895
numbers.\medskip\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   896
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   897
{\bf Proof} \ldots\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   898
\end{bubble}\bigskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   899
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   900
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   901
similarly\bigskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   902
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   903
\begin{bubble}[10cm]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   904
\small
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   905
{\bf Theorem:} The program is doing what 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   906
it is supposed to be doing.\medskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   907
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   908
{\bf Long, long proof} \ldots\\
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   909
\end{bubble}\bigskip\medskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   910
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   911
\small This can be a gigantic proof. The only hope is to have
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   912
help from the computer. `Program' is here to be understood to be
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   913
quite general (compiler, OS, \ldots).
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   914
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   915
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   916
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   917
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   918
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   919
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   920
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   921
\begin{frame}[c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   922
\frametitle{Can This Be Done?}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   923
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   924
\begin{itemize}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   925
\item in 2008, verification of a small C-compiler
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   926
\begin{itemize}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   927
\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   928
\item is as good as \texttt{gcc -O1}, but much, much less buggy 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   929
\end{itemize}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   930
\end{itemize}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   931
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   932
\begin{center}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   933
  \includegraphics[scale=0.12]{../pics/compcert.png}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   934
\end{center}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   935
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   936
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   937
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   938
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   939
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   940
\begin{frame}[t]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   941
\frametitle{Fuzzy Testing C-Compilers}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   942
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   943
\begin{itemize}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   944
\item tested GCC, LLVM and others by randomly generating 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   945
C-programs
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   946
\item found more than 300 bugs in GCC and also
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   947
many in LLVM (some of them highest-level critical)\bigskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   948
\item about CompCert:
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   949
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   950
\begin{bubble}[10.7cm]\small ``The striking thing about our CompCert
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   951
results is that the middle-end bugs we found in all other
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   952
compilers are absent. As of early 2011, the under-development
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   953
version of CompCert is the only compiler we have tested for
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   954
which Csmith cannot find wrong-code errors. This is not for
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   955
lack of trying: we have devoted about six CPU-years to the
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   956
task.'' 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   957
\end{bubble} 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   958
\end{itemize}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   959
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   960
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   961
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   962
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   963
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   964
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   965
\begin{frame}[c]
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   966
\frametitle{Next Week}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   967
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   968
\begin{itemize}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   969
\item Revision Lecture\medskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   970
\item How many  strings are in $\bl{L(a^*)}$?\pause\medskip
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   971
\item How many  strings are in $\bl{L((a + b)^*)}$?\\ Are there more than
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   972
  in $\bl{L(a^*)}$?
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   973
\end{itemize}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   974
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   975
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   976
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   977
\end{frame}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   978
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   979
822
815f03652bf9 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 819
diff changeset
   980
\begin{frame}<1-20>[c]
815f03652bf9 updated
Christian Urban <christian.urban@kcl.ac.uk>
parents: 819
diff changeset
   981
\end{frame}
701
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   982
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   983
\end{document}
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   984
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   985
%%% Local Variables:  
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   986
%%% mode: latex
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   987
%%% TeX-master: t
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   988
%%% End: 
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   989
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   990
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   991
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   992
81377a3eb717 updated
Christian Urban <urbanc@in.tum.de>
parents: 612
diff changeset
   993
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   994
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   995
  \begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   996
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   997
  \begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   998
  \includegraphics[scale=0.6]{../pics/bridge-limits.png}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
   999
  \end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1000
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1001
  \end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1002
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1003
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1004
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1005
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1006
\begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1007
\frametitle{Compilers \& Boeings 777}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1008
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1009
First flight in 1994. They want to achieve triple redundancy in hardware
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1010
faults.\bigskip
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1011
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1012
They compile 1 Ada program to\medskip
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1013
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1014
\begin{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1015
\item Intel 80486
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1016
\item Motorola 68040 (old Macintosh's)
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1017
\item AMD 29050 (RISC chips used often in laser printers)
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1018
\end{itemize}\medskip
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1019
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1020
using 3 independent compilers.\bigskip\pause
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1021
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1022
\small Airbus uses C and static analysers. Recently started using CompCert.
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1023
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1024
\end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1025
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1026
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1027
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1028
\begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1029
\frametitle{Goal}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1030
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1031
Remember the Bridges example?
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1032
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1033
\begin{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1034
\item Can we look at our programs and somehow ensure
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1035
they are bug free/correct?\pause\bigskip
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1036
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1037
\item Very hard: Anything interesting about programs is equivalent
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1038
to the Halting Problem, which is undecidable.\pause\bigskip
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1039
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1040
\item \alert{Solution:} We avoid this ``minor'' obstacle by
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1041
      being as close as possible of deciding the halting
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1042
      problem, without actually deciding the halting problem.
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1043
      \small$\quad\Rightarrow$ yes, no, don't know (static analysis)
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1044
\end{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1045
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1046
\end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1047
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1048
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1049
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1050
  \begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1051
  \frametitle{What is Static Analysis?}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1052
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1053
  \begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1054
  \includegraphics[scale=0.4]{../pics/state.png}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1055
  \end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1056
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1057
  \begin{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1058
  \item depending on some initial input, a program 
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1059
  (behaviour) will ``develop'' over time.
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1060
  \end{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1061
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1062
  \end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1063
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1064
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1065
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1066
  \begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1067
  \frametitle{What is Static Analysis?}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1068
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1069
  \begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1070
  \includegraphics[scale=0.4]{../pics/state2.png}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1071
  \end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1072
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1073
  \end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1074
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1075
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1076
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1077
  \begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1078
  \frametitle{What is Static Analysis?}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1079
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1080
  \begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1081
  \includegraphics[scale=0.4]{../pics/state3.jpg}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1082
  \end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1083
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1084
  \end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1085
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1086
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1087
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1088
  \begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1089
  \frametitle{What is Static Analysis?}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1090
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1091
  \begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1092
  \includegraphics[scale=0.4]{../pics/state4.jpg}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1093
  \end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1094
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1095
  \begin{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1096
  \item to be avoided
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1097
  \end{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1098
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1099
  \end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1100
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1101
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1102
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1103
  \begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1104
  \frametitle{What is Static Analysis?}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1105
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1106
  \begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1107
  \includegraphics[scale=0.4]{../pics/state5.png}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1108
  \end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1109
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1110
  \begin{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1111
  \item this needs more work
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1112
  \end{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1113
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1114
  \end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1115
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1116
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1117
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1118
  \begin{frame}[c]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1119
  \frametitle{What is Static Analysis?}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1120
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1121
  \begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1122
  \includegraphics[scale=0.4]{../pics/state6.png}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1123
  \end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1124
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1125
  \end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1126
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1127
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1128
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1129
  \begin{frame}[c,fragile]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1130
    \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1131
                  Are Vars Definitely Initialised?\end{tabular}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1132
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1133
Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskip
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1134
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1135
Prog.~1:\\
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1136
\begin{lstlisting}[numbers=none,
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1137
                   basicstyle=\ttfamily,
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1138
                   language=While,xleftmargin=3mm]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1139
if x < 1 then y := x else y := x + 1;
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1140
y := y + 1
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1141
\end{lstlisting}\medskip     
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1142
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1143
Prog.~2:\\
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1144
\begin{lstlisting}[numbers=none,
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1145
                   basicstyle=\ttfamily,
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1146
                   language=While,xleftmargin=3mm]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1147
if x < x then y := y + 1 else y := x;
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1148
y := y + 1
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1149
\end{lstlisting}            
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1150
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1151
  \end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1152
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1153
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1154
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1155
  \begin{frame}[c,fragile]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1156
    \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1157
                  Are Vars Definitely Initialised?\end{tabular}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1158
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1159
              What should the rules be for deciding when a
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1160
              variable is initialised?\bigskip\pause
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1161
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1162
\begin{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1163
\item variable \texttt{x} is definitely initialized after
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1164
  \texttt{skip}\\
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1165
  iff \texttt{x} is definitely initialized before \texttt{skip}.
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1166
\end{itemize}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1167
  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1168
\end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1169
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1170
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1171
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1172
  \begin{frame}[c,fragile]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1173
%    \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1174
%                  Are Vars Definitely Initialised?\end{tabular}}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1175
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1176
$\bl{A}$ is the set of definitely defined variables:
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1177
              
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1178
\begin{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1179
\begin{tabular}{c}
612
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1180
  \bl{\infer{\mbox{}}{A\triangleright\texttt{skip}\triangleright{}A}}\qquad
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1181
  \bl{\infer{vars(a) \subseteq A}{A\triangleright
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1182
  (\texttt{x\,:=\,a})\triangleright\{x\}\cup A}}
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1183
  \medskip\\\pause
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1184
612
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1185
  \bl{\infer{A_1\triangleright{}s_1\triangleright{}A_2
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1186
  \quad A_2\triangleright{}s_2\triangleright{}A_3}
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1187
  {A_1\triangleright{}(s_1 ; s_2)\triangleright{}A_3}}
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1188
  \medskip\\\pause
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1189
  
612
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1190
  \bl{\infer{vars(b)\subseteq A\quad A\triangleright{}s_1\triangleright{}A_1
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1191
  \quad A\triangleright{}s_2\triangleright{}A_2}
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1192
  {A\triangleright(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\triangleright{}A_1\cap A_2}}
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1193
  \medskip\\\pause
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1194
612
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1195
  \bl{\infer{vars(b)\subseteq A\quad A\triangleright{}s\triangleright{}A'}
274477667793 updated
Christian Urban <urbanc@in.tum.de>
parents: 610
diff changeset
  1196
  {A\triangleright(\texttt{while}\;b\;\texttt{do}\;s)\triangleright{}A}}\pause
610
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1197
\end{tabular}  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1198
\end{center}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1199
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1200
\hfill we start with $\bl{A = \{\}}$
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1201
\end{frame}
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1202
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
ce5e0426c92a updated
Christian Urban <urbanc@in.tum.de>
parents: 609
diff changeset
  1203