# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1416916096 0
# Node ID cf02511469d68ddeae3153c773152aede9b32f9c
# Parent  8eab185fb187b0980908a05cb5609b4428fab43d
updated

diff -r 8eab185fb187 -r cf02511469d6 graphics.sty
--- a/graphics.sty	Tue Nov 25 03:30:11 2014 +0000
+++ b/graphics.sty	Tue Nov 25 11:48:16 2014 +0000
@@ -6,7 +6,7 @@
 \usepackage{pgfplots}
 
 \newenvironment{bubble}[1][]{%
-\begin{tikzpicture}%
+\begin{tikzpicture}[baseline=(current bounding box.north)]%
 \draw (0,0) node[inner sep=2mm,fill=cream,ultra thick,draw=red,rounded corners=2mm]% 
 \bgroup\begin{minipage}{#1}\raggedright{}}
 {\end{minipage}\egroup;%
diff -r 8eab185fb187 -r cf02511469d6 slides/slides09.pdf
Binary file slides/slides09.pdf has changed
diff -r 8eab185fb187 -r cf02511469d6 slides/slides09.tex
--- a/slides/slides09.tex	Tue Nov 25 03:30:11 2014 +0000
+++ b/slides/slides09.tex	Tue Nov 25 11:48:16 2014 +0000
@@ -3,6 +3,29 @@
 \usepackage{../langs}
 \usepackage{../graphics}
 \usepackage{../grammar}
+\usepackage{soul}
+
+\makeatletter
+\newenvironment<>{btHighlight}[1][]
+{\begin{onlyenv}#2\begingroup\tikzset{bt@Highlight@par/.style={#1}}\begin{lrbox}{\@tempboxa}}
+{\end{lrbox}\bt@HL@box[bt@Highlight@par]{\@tempboxa}\endgroup\end{onlyenv}}
+
+\newcommand<>\btHL[1][]{%
+  \only#2{\begin{btHighlight}[#1]\bgroup\aftergroup\bt@HL@endenv}%
+}
+\def\bt@HL@endenv{%
+  \end{btHighlight}%   
+  \egroup
+}
+\newcommand{\bt@HL@box}[2][]{%
+  \tikz[#1]{%
+    \pgfpathrectangle{\pgfpoint{1pt}{0pt}}{\pgfpoint{\wd #2}{\ht #2}}%
+    \pgfusepath{use as bounding box}%
+    \node[anchor=base west, fill=orange!30,outer sep=0pt,inner xsep=1pt, inner ysep=0pt, rounded corners=3pt, minimum height=\ht\strutbox+1pt,#1]{\raisebox{1pt}{\strut}\strut\usebox{#2}};
+  }%
+}
+\makeatother
+
 
 % beamer stuff 
 \renewcommand{\slidecaption}{APP 09, King's College London}
@@ -110,7 +133,7 @@
 \begin{bubble}[10cm]
 \small
 {\bf Theorem:} The program is doing what 
-it is supposed to be doing.\medskip
+it is sup+ed to be doing.\medskip
 
 {\bf Long, long proof} \ldots\\
 \end{bubble}\bigskip\medskip
@@ -691,7 +714,7 @@
   \item working purely on \emph{static} policies also does not\\ work -\!-\!- because of over approximation
   \smallskip
   \begin{itemize}
-  \item suppose a tainted file has type \emph{bin} and
+  \item sup+e a tainted file has type \emph{bin} and
   \item there is a role \bl{$r$} which can both read and write \emph{bin}-files\pause
   \item then we would conclude that this tainted file can spread\medskip\pause
   \item but if there is no process with role \bl{$r$} and it will never been
@@ -742,7 +765,7 @@
 to halting problem, which is undecidable.\pause\bigskip
 
 \item \alert{Solution:} We avoid this ``minor'' obstacle by
-      being as close as possible of deciding the halting
+      being as close as +sible of deciding the halting
       problem, without actually deciding the halting problem.
       $\quad\Rightarrow$ static analysis
 \end{itemize}
@@ -871,7 +894,7 @@
 \begin{bubble}[5.6cm]
 \begin{lstlisting}[numbers=none,
                    basicstyle=\ttfamily,
-                   language={},xleftmargin=3]
+                   language={},xleftmargin=3mm]
       a := 1
       n := 5 
 top:  jump? n = 0 done 
@@ -898,7 +921,7 @@
          | \meta{var}\\
 : \meta{Stmt} ::= \meta{label} :
          | \meta{var} := \meta{Exp}
-         | jump? \meta{Exp} \meta{label}
+         | jmp? \meta{Exp} \meta{label}
          | goto \meta{label}\\
 : \meta{Prog} ::= \meta{Stmt} \ldots\\
 \end{plstx}}
@@ -908,11 +931,11 @@
 \begin{bubble}[5.6cm]
 \begin{lstlisting}[numbers=none,
                    basicstyle=\ttfamily,
-                   language={},xleftmargin=3]
+                   language={},xleftmargin=3mm]
       n := 6
       m1 := 0
       m2 := 1
-top:  jump? n = 0 done
+top:  jmp? n = 0 done
       tmp := m2
       m2 := m1 + m2
       m1 := tmp
@@ -926,17 +949,255 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{Eval}
+\mbox{}\\[-18mm]\mbox{}
+
+\small
+\begin{center}
+\bl{\begin{tabular}{lcl}
+$[n]_{env}$ & $\dn$ & $n$\\
+$[x]_{env}$ & $\dn$ & $env(x)$\\
+$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} + [e_2]_{env}$\\
+$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} * [e_2]_{env}$\\
+$[e_1 = e_2]_{env}$ & $\dn$ & 
+$\begin{cases}
+1 & \text{if}\quad[e_1]_{env} = [e_2]_{env}\\
+0 & \text{otherwise}
+\end{cases}$\\
+\end{tabular}}
+\end{center}
+
+\footnotesize
+\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
+def eval_exp(e: Exp, env: Env) : Int = e match {
+  case Num(n) & n
+  case Var(x) & env(x)
+  case Plus(e1, e2) & eval_exp(e1, env) + eval_exp(e2, env)
+  case Times(e1, e2) & eval_exp(e1, env) * eval_exp(e2, env)
+  case Equ(e1, e2) & 
+    if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0
+}
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\small
+A program
+\begin{bubble}[6cm]\footnotesize
+\begin{lstlisting}[numbers=none,
+                   language={},
+                   basicstyle=\ttfamily,
+                   xleftmargin=1mm]
+      a := 1
+      n := 5 
+top:  jmp? n = 0 done 
+      a := a * n 
+      n := n + -1 
+      goto top 
+done:
+\end{lstlisting}
+\end{bubble}
+
+Some snippets
+
+\footnotesize
+\begin{columns}
+\begin{column}[t]{5cm}
+\begin{bubble}[4.5cm]
+\begin{lstlisting}[numbers=none,
+                   basicstyle=\ttfamily,
+                   language={},xleftmargin=1mm]
+""    a := 1
+      n := 5 
+top:  jmp? n = 0 done 
+      a := a * n 
+      n := n + -1 
+      goto top 
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+\begin{column}[t]{5cm}
+\begin{bubble}[4.5cm]
+\begin{lstlisting}[numbers=none,
+                   basicstyle=\ttfamily,
+                   language={},xleftmargin=1mm]
+top:  jmp? n = 0 done 
+      a := a * n 
+      n := n + -1 
+      goto top 
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+\begin{column}[t]{2cm}
+\begin{bubble}[1.1cm]
+\begin{lstlisting}[numbers=none,
+                   basicstyle=\ttfamily,
+                   language={},xleftmargin=1mm]
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+\end{columns}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{Eval for Stmts}
+\mbox{}\\[-12mm]\mbox{}
+
+Let \bl{$sn$} be the snippets of a program
+
+\small
+\begin{center}
+\bl{\begin{tabular}{lcl}
+$[\texttt{nil}]_{env}$ & $\dn$ & $env$\medskip\\
+$[\texttt{Label}(l:)::rest]_{env}$ & $\dn$ & $[rest]_{env}$\medskip\\
+$[x \,\texttt{:=}\, e::rest]_{env}$ & $\dn$ & 
+$[rest]_{(env[x:= [e]_{env}])}$\medskip\\
+$[\texttt{jmp?}\;e\;l::rest]_{env}$ & $\dn$ & 
+$\begin{cases}
+[sn(l)]_{env} & \text{if}\quad[e]_{env} = 1\\
+[rest]_{env}  & \text{otherwise}
+\end{cases}$\medskip\\
+$[\texttt{goto}\;l::rest]_{env}$ & $\dn$ & $[sn(l)]_{env}$\\
+\end{tabular}}
+\end{center}\bigskip
+
+Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{Eval in Code}
+
+\footnotesize
+\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
+def eval(sn: Snips) : Env = {
+  def eval_stmts(sts: Stmts, env: Env) : Env = sts match {
+    case Nil & env
+    case Label(l)::rest & eval_stmts(rest, env)
+    case Assign(x, e)::rest & 
+      eval_stmts(rest, env + (x -> eval_exp(e, env)))
+    case Jump(b, l)::rest & 
+      if (eval_exp(b, env) == 1) eval_stmts(sn(l), env) 
+      else eval_stmts(rest, env)
+    case Goto(l)::rest & eval_stmts(sn(l), env)
+  }
+
+  eval_stmts(sn(""), Map())
+}
+\end{lstlisting}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[fragile]
+\frametitle{The Idea}
+\small
+\mbox{}\bigskip\\
+
+\begin{columns}
+\begin{column}{5cm}
+\begin{bubble}[4.5cm]\footnotesize
+\begin{lstlisting}[numbers=none,
+                   language={},
+                   basicstyle=\ttfamily,
+                   xleftmargin=1mm]
+      a := 1
+      n := 5 
+top:  jmp? n = 0 done 
+      a := a * n 
+      n := n + -1 
+      goto top 
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+
+\begin{column}{1cm}
+\raisebox{-20mm}{\LARGE\bf$\Rightarrow$}
+\end{column}
+\begin{column}{6cm}
+\begin{bubble}[4.7cm]\footnotesize
+\begin{lstlisting}[numbers=none,
+                   language={},
+                   basicstyle=\ttfamily,
+                   xleftmargin=1mm,
+                   escapeinside={(*@}{@*)}]
+      a := (*@\hl{'+'}@*)
+      n := (*@\hl{'+'}@*) 
+top:  jmp? n = (*@\hl{'0'}@*) done 
+      a := a * n 
+      n := n + (*@\hl{'-'}@*) 
+      goto top 
+done:
+\end{lstlisting}
+\end{bubble}
+\end{column}
+\end{columns}\bigskip\bigskip
+
+Replace all constants and variables by either 
+\pcode{+}, \pcode{-} or \pcode{0}. What we want to find out
+is what the sign of \texttt{a} and \texttt{n} is (they are 
+always positive).
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{Sign Analysis?}
+
+  
+  \begin{columns}
+  \begin{column}{4cm}
+  \begin{tabular}{cc|l}
+  $e_1$ & $e_2$ & $e_1 + e_2$\\\hline{}
+  - & - & -\\
+  - & 0 & -\\
+  - & + & -, 0, +\\
+  0 & $x$ & $x$\\
+  + & - & -, 0, +\\
+  + & 0 & +\\
+  + & + & +\\
+  \end{tabular}
+  \end{column}
+
+  \begin{column}{4cm}
+  \begin{tabular}{cc|l}
+  $e_1$ & $e_2$ & $e_1 * e_2$\\\hline{}
+  - & - & +\\
+  - & 0 & 0\\
+  - & + & -\\
+  0 & $x$ & 0\\
+  + & - & -\\
+  + & 0 & 0\\
+  + & + & +\\
+  \end{tabular}
+  \end{column}
+  \end{columns}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 
 \end{document}
 
-%         n := 5 
-% top:    jump? n = 0 done 
-%         a := a * n 
-%         n := n + -1 
-%         goto top 
-% done:
-
 
 %%% Local Variables:  
 %%% mode: latex