diff options
Diffstat (limited to 'tex/presentation/main.tex')
| -rw-r--r-- | tex/presentation/main.tex | 290 |
1 files changed, 290 insertions, 0 deletions
diff --git a/tex/presentation/main.tex b/tex/presentation/main.tex new file mode 100644 index 0000000..286e4a7 --- /dev/null +++ b/tex/presentation/main.tex @@ -0,0 +1,290 @@ +\documentclass{beamer} + +\usetheme{Hannover} +\usepackage{amsmath,stmaryrd,listings} + +\title{{\bf Static Analysis \\ through \\Abstract Interpretation, \\Convex Optimization, and\\ Strategy Iteration}} + +\author{ + {\bf Thomas Martin Gawlitza} + \\[3pt] + joint work with + \\[3pt] + {\bf Helmut Seidl} +} + +\newcommand\N{\mathbb{N}} +\newcommand\Z{\mathbb{Z}} +\newcommand\CZ{\overline{\Z}} + +\let\max\undefined +\newcommand\max{\lor} +\let\min\undefined +\newcommand\min{\land} + +\begin{document} + +\begin{frame} + \maketitle +\end{frame} + +\begin{frame} + \tableofcontents +\end{frame} + +\section{Example} +\begin{frame}{Example} + \begin{eqnarray*} + x_1 &=& 0 \max (-1 + x_1 \min x_2) \\ + x_2 &=& 0 \max 5 + x_1 \max x_1 \\ + x_3 &=& 0 \max 1 + x_3 \max 0 + x_1 + \end{eqnarray*} + +\end{frame} + +\section{Definitions} +\begin{frame}{Preliminary Definitions} + \begin{center} + Strange notation: \\ + $x \max y = \text{max}(x, y)$ \\ + $x \min y = \text{min}(x, y)$ \\ + \uncover<2->{ + \bigskip + {\bf Monotone:} $x \leq y \implies f(x) \leq f(y) ~~ \forall x,y$ + } + + \uncover<3->{ + \bigskip + {\bf Assignment:} $\rho$ is always a variable assignment (from $X \rightarrow \CZ$) + } + \end{center} +\end{frame} + +\begin{frame}{Systems of Equations} + \begin{align*} + \varepsilon = \{ x_1 = e_1, x_2 = e_2, ... x_n = e_n \} + \end{align*} + \uncover<2->{ + \begin{align*} + \text{\bf Solutions: } & \rho = \llbracket \varepsilon \rrbracket \rho \\ + \text{\bf Presolutions: } & \rho \leq \llbracket \varepsilon \rrbracket \rho \\ + \text{\bf Fixpoint: } & f(x) = x \\ + \text{\bf Least fixpoint: } & \mu f \\ + \end{align*} + } + \uncover<3->{ + {\bf Evaluation:} + $\text{with } \rho ~ \epsilon ~ Vars(\varepsilon) \rightarrow \CZ$ \\ + \begin{align*} + (\llbracket \varepsilon \rrbracket \rho)(x) & := \llbracket e \rrbracket \rho \\ + \llbracket x \rrbracket \rho & := \rho (x) \\ + \llbracket f(e_1, ... e_k) \rrbracket & := f(\llbracket e_1 \rrbracket \rho, + ... \llbracket e_k \rrbracket \rho) + \end{align*} + } +\end{frame} + +\begin{frame}{Operators on $\CZ$} + Working in $\CZ = \Z \cup \{\infty, -\infty\}$ + + \bigskip + \begin{displaymath} + x +^{-\infty} y = \left\{ \begin{array}{ll} + -\infty & \text{if } -\infty \in \{x,y\} \\ + \infty & \text{if } -\infty \not\in \{x,y\} \text{ and } \infty \in \{x,y\} \\ + x + y & \text{if } x,y \in \Z \\ + \end{array} \right. + \end{displaymath} + \begin{displaymath} + x +^{\infty} y = \left\{ \begin{array}{ll} + \infty & \text{if } \infty \in \{x,y\} \\ + -\infty & \text{if } \infty \not\in \{x,y\} \text{ and } -\infty \in \{x,y\} \\ + x + y & \text{if } x,y \in \Z \\ + \end{array} \right. + \end{displaymath} + \begin{displaymath} + \begin{array}{lr} + x \cdot \infty = \infty \cdot x = \infty, + x \cdot -\infty = -\infty \cdot x = -\infty + & \forall x > 0 \\ + x \cdot \infty = \infty \cdot x = -\infty, + x \cdot -\infty = -\infty \cdot x = \infty + & \forall x < 0 \\ + 0 \cdot \infty = \infty \cdot 0 = + 0 \cdot -\infty = -\infty \cdot 0 = 0 & + \end{array} + \end{displaymath} +\end{frame} + +\begin{frame}{Expansivity} + $f$ is upward-expansive in $X'$ iff + + \bigskip + \begin{center} + $f(\rho \oplus \{x \mapsto \rho(x) + \delta\}) \geq f(\rho) + \delta)$ + ~~ $\forall x \in X', \rho \in X \rightarrow \CZ, \delta \in \N$ + \end{center} +\end{frame} + +\section{Max-strategies} +\begin{frame}{Max-strategies} + Assume for every $x = e \in \varepsilon$, $e$ is of the + form $e_1 \max e_2 \max ... \max e_k$. + + Then a $\max$-$strategy$ $\sigma$ maps each $e$ to one of its $e_k$. + + \bigskip + For all $\max$ strategies $\sigma$ the expression $e\sigma$ is defined as: + \begin{align*} + (e_1 \max ... \max e_k)\sigma & = (\sigma(e_1 \max ... \max e_k))\sigma \\ + (f(e_1,...e_k))\sigma & = f(e_1\sigma, ..., e_k\sigma) + \end{align*} + where $f \not = \max$ +\end{frame} + +\begin{frame}{Max-strategies} + We may need to change strategy throughout our evaluation. + + Consider the system: $\varepsilon = \{x_1 = x_1 + 1 \max 0\}$. + + Let: + \begin{align*} + \sigma_1 & = \{x_1 + 1 \max 0 \mapsto x_1 + 1\} \\ + \sigma_2 & = \{x_1 + 1 \max 0 \mapsto 0\} + \end{align*} + + \uncover<2->{ + This gives us: + } + \begin{align*} + \uncover<2->{ + \mu \llbracket \varepsilon (\sigma_1) \rrbracket & = \{x_1 \mapsto -\infty\} \\ + \mu \llbracket \varepsilon (\sigma_2) \rrbracket & = \{x_1 \mapsto 0\} \\ + } + \uncover<3->{ + \mu \llbracket \varepsilon \rrbracket & = \{x_1 \mapsto \infty\} + } + \end{align*} +\end{frame} + +\section{Bellman-Ford} +\begin{frame}{BF-functions} + $X$ a set. A monotone $f: (X \rightarrow \CZ) \rightarrow CZ$ is called + a \emph{Bellman-Ford function} iff, $\forall \rho, \rho': X \rightarrow \CZ$ + with $\rho' \geq \rho$ the following holds: + + \bigskip + If $f(\rho') > f(\rho)$ then $\exists x \in X$ and some $\delta \in \CZ\setminus\{-\infty\}$ such that: + \begin{align*} + \rho'(x) & > \rho(x) \\ + f(\rho') & = \rho'(x) + \delta \\ + f(\rho'') & \geq \rho''(x) + \delta ~~ \forall \rho'' \geq \rho' + \end{align*} +\end{frame} + +\begin{frame}{A quick lemma} + Let $\varepsilon$ be a system of \emph{BF-equations} with $n$ variables. \\ + Let $\rho^{(i)} = \llbracket\varepsilon\rrbracket^i(\_ \mapsto -\infty) ~~ \forall i \in \N$. \\ + The following holds for every $x \in Vars(\varepsilon)$: \\ + If there exists some $k > n$ with $\rho^{(k)}(x) > \rho^{(n)}(x)$, then + $\mu\llbracket\varepsilon\rrbracket(x) = \infty$. +\end{frame} + +\begin{frame}{The algorithm} + ~ \\ + {\bf Input:} A system of BF-equations with $n$ variables \\ + {\bf Output:} The least solution $\mu\llbracket\varepsilon\rrbracket$ of \varepsilon \\ + \begin{displaymath} + ~ \\ + \rho \leftarrow (\_ \mapsto -\infty) \\ + {\bf for} i = 1 {\bf to} n {\bf do} \rho \leftarrow \llbracket\varepsilon\rrbracket\rho \\ + \rho \leftarrow \rho' \text{ where } \rho'(x) = \left\{ \begin{array}{ll} + \rho(x) & \text{if } (\llbracket\varepsilon\rrbracket\rho)(x) \leq \rho(x) \\ + \infty & \text{if } (\llbracket\varepsilon\rrbracket\rho)(x) > \rho(x) + \end{array} \right. \forall x \in X \\ + {\bf for} i = 1 {\bf to} n-1 {\bf do} \rho \leftarrow \rho \max \llbracket\varepsilon\rrbracket\rho \\ + {\bf return} \rho \\ + ~ + \end{displaymath} +\end{frame} + +\begin{frame}{Example} + \begin{align*} + x & = 1 \\ + y & = y + x \max -10 \\ + z & = x \cdot^+ y + \end{align*} + Where $\cdot^+$ is defined by: + \begin{displaymath} + x \cdot^+ y = \left\{ \begin{array}{l l} + x \cdot y & \text{if } x, y > 0 \\ + -\infty & \text{if } x \le 0 \text{ or } y \le 0 + \end{array} \forall x,y \in \CZ + \end{displaymath} +\end{frame} + +\section{Max-strategy improvement} +\begin{frame}{Max-strategy improvement} + {\bf General idea:} + \begin{itemize} + \item Pick a max-strategy + \item Perform fixpoint iteration + \item Improve strategy + \item Repeat until we have a solution + \end{itemize} +\end{frame} + +\begin{frame}{What is an improvement?} + If we have $\varepsilon$ a system of equations, $\sigma$ a $\max$-strategy + for $\varepsilon$ and $\rho$ a presolution of $\varepsilon(\sigma)$, then we + call a $\max$-strategy $\sigma'$ is called an improvement of $\sigma$ with + respect to $\rho$ iff: + \begin{itemize} + \item if $\rho \not \in {\bf Sol}(\varepsilon)$, then $\llbracket\varepsilon(\sigma')\rrbracket\rho > \rho$ + \item for all $\max$-expression $e \in S_{\max}(\varepsilon)$ the following holds: \\ + If $\sigma'(e) \not = \sigma(e)$, then $\llbracket e\sigma'\rrbracket\rho > \llbracket e\sigma\rrbracket\rho$ + \end{itemize} +\end{frame} + +\begin{frame}{Algorithm} + ~ \\ + {\bf Input:} + \begin{itemize} + \item A system $\varepsilon$ of monotone equations over a complete linearly ordered set \\ + \item A $\max$-strategy $\sigma_{init}$ for $\varepsilon$ \\ + \item A pre-solution $\rho_{init}$ of $\varepsilon(\sigma_{init})$ with $\rho_{init} \le \mu\llbracket\varepsilon\rrbracket$ + \end{itemize} + {\bf Output:} The least solution $\mu\llbracket\varepsilon\rrbracket$ of $\varepsilon$ + \begin{displaymath} + ~ \\ + \sigma \leftarrow \sigma_{init} \\ + \rho \leftarrow \rho_{init} \\ + \text{while }(\rho \not \in {\bf Sol}(\varepsilon)) \{ \\ + ~~~~ \sigma \leftarrow P_{\max}(\sigma, \rho) \\ + ~~~~ \rho \leftarrow \mu_{\ge\rho} \llbracket\varepsilon(\sigma)\rrbracket \\ + \} \\ + {\bf return} \rho + ~ + \end{displaymath} +\end{frame} + +\begin{frame}{Another related lemma} + Whenever the $\max$-strategy improvement algorithm terminates, it + returns the least solution $\mu\llbracket\varepsilon\rrbracket$. +\end{frame} + +\begin{frame}{Example} + \begin{align*} + x_1 & = 0 \max x_1 + x_2 - 4 \\ + x_2 & = -1 \max ((x_1 + 1 \max 2 \cdot x_2) \min 5) + \end{align*} +\end{frame} + +\section{Feasibility} + +\section{Extended Integer Equations} + +\section{Abstract Interpretation over Zones} + + +\end{document} |