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