sen-material: comparison slides/slides09.tex

equal deleted inserted replaced

-:8eab185fb187
+:cf02511469d6
 \documentclass[dvipsnames,14pt,t]{beamer}
 \usepackage{../slides}
 \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}
 \newcommand{\bl}[1]{\textcolor{blue}{#1}}
 similarly\bigskip
 \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
 \small This can be a gigantic proof. The only hope is to have
 \item working purely in the \emph{dynamic world} does not work -\!-\!- infinite state space\bigskip
 \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
 created, then the file actually does not spread
 \end{itemize}\bigskip\pause
 \item Very hard: Anything interesting about programs is equivalent
 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}
 \end{frame}
 \begin{textblock}{0}(7.8,2.5)
 \small
 \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
 a := a * n
 n := n + -1
 | \meta{Exp} = \meta{Exp}
 | \meta{num}
 | \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}}
 \begin{textblock}{0}(7.8,3.5)
 \small
 \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
 n := n + -1
 goto top
 \end{textblock}
 \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
 %%% TeX-master: t

changeset 333	cf02511469d6
parent 332	8eab185fb187
child 334	6f08b13c0242