--- 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