diff options
| -rw-r--r-- | tex/presentation/Makefile | 28 | ||||
| -rw-r--r-- | tex/presentation/presentation.pdf | bin | 0 -> 175078 bytes | |||
| -rw-r--r-- | tex/presentation/presentation.tex | 336 | ||||
| -rw-r--r-- | tex/presentation/references.bib | 156 |
4 files changed, 520 insertions, 0 deletions
diff --git a/tex/presentation/Makefile b/tex/presentation/Makefile new file mode 100644 index 0000000..0d171d7 --- /dev/null +++ b/tex/presentation/Makefile @@ -0,0 +1,28 @@ +all: presentation.pdf + +.PHONY: remote clean +remote: + ssh honours "mkdir -p tmp/tex/presentation" + rm -f presentation.pdf + rsync -r . "honours:tmp/tex/presentation" + ssh honours "cd tmp/tex/presentation; make clean; make" + scp "honours:tmp/tex/presentation/presentation.pdf" . + +presentation.pdf: presentation.tex + pdflatex presentation + bibtex presentation + pdflatex presentation + pdflatex presentation + +clean: + rm -f `find . -name '*.log'` + rm -f `find . -name '*.dvi'` + rm -f `find . -name '*.ps'` + rm -f `find . -name '*.aux'` + rm -f `find . -name '*.blg'` + rm -f `find . -name '*.bbl'` + rm -f `find . -name '*.toc'` + rm -f `find . -name '*.lof'` + rm -f `find . -name '*.lot'` + rm -f `find . -name '*.out'` + rm -f `find . -name '*~'` diff --git a/tex/presentation/presentation.pdf b/tex/presentation/presentation.pdf Binary files differnew file mode 100644 index 0000000..f19baee --- /dev/null +++ b/tex/presentation/presentation.pdf diff --git a/tex/presentation/presentation.tex b/tex/presentation/presentation.tex new file mode 100644 index 0000000..914ba66 --- /dev/null +++ b/tex/presentation/presentation.tex @@ -0,0 +1,336 @@ +\documentclass{beamer} + +\title{Implementing and Evaluating a Strategy-Iteration Based Static Analyser within the LLVM framework} +\author{Carlo Zancanaro} +\def\sid{309222257} +\def\supervisor{Bernhard Scholz} + +\usepackage[numbers]{natbib} +\usepackage{mdframed} +\usepackage{algorithmicx} +\usepackage{tikz} +\usepackage{pgfplots} +\pgfplotsset{compat=1.4} +\algblockx[While]{While}{EndWhile}{\textbf{while}~}{\textbf{endwhile}} + +\newcommand\Z{\mathbb{Z}} +\newcommand\CZ{\overline{\Z}} +\def\newblock{\hskip .11em plus .33em minus .07em} % important line + +\begin{document} + +\begin{frame} + \maketitle +\end{frame} + +\section{Introduction} +\begin{frame}{Bugs are bad} + \begin{itemize} + \item<1-> + Money - recently Knight Capital, US\$440 million lost in a day + \item<2-> + Time - 50\% of development time is spent debugging\cite{debugging-book} + \item<3-> + Security - buffer overflows and other security flaws + \item<4-> + Lives - X-ray machines, helicopters, cars + \end{itemize} +\end{frame} +\begin{frame}{Static analysis is good} + \begin{itemize} + \item<1-> + The more bugs we can catch at compile time, the better + \item<2-> + We can't catch all bugs - Rice's theorem\cite{Rice} + \end{itemize} +\end{frame} + +\section{Prior work} +\begin{frame}[fragile]{Modelling programs} + \begin{center} + \begin{mdframed} + \begin{algorithmic} + \State $x = 0$ + \State $y = 1$ + \While {$x < 8$} + \Comment{value at start of this line} + \State $x = x + 2$ + \State $y = y + 2$ + \EndWhile + \end{algorithmic} + \end{mdframed} + \end{center} + \begin{align*} + \only<1>{~ \\ ~} + \only<2>{x &= \{0\} \\ y &= \{1\}} + \only<3>{x &= \{0, 2\} \\ y &= \{1, 3\}} + \only<4>{x &= \{0, 2, 4\} \\ y &= \{1, 3, 5\}} + \only<5>{x &= \{0, 2, 4, 6\} \\ y &= \{1, 3, 5, 7\}} + \only<6>{x &= \{0, 2, 4, 6, 8\} \\ y &= \{1, 3, 5, 7, 9\}} + \end{align*} +\end{frame} + +\begin{frame}{Abstract interpretation} + Basic idea: simplify your domain + + Instead of arbitrary subsets of $\Z$, something less precise: + + \begin{itemize} + \item + signs\cite{CousotCousot77-1}: $x \in \{ \Z, \Z^+, \Z^-, 0\}$ + \item + ranges\cite{CousotCousot77-1}: $x \le a; -x \le b, ~a,b \in \Z$ + \item + zones\cite{mine:padoII}: $x - y \le c; \pm x \le c ~c \in Z$ + \end{itemize} +\end{frame} +\begin{frame}[fragile]{Abstract interpretation} + \begin{figure} + \begin{tikzpicture}[scale=0.6,dot/.style={circle,fill,inner sep=1pt}] + \draw (0,0) -- coordinate (x axis mid) (10,0); + \draw (0,0) -- coordinate (y axis mid) (0,10); + + \foreach \x in {0,...,10} + \draw (\x,1pt) -- (\x,-3pt) + node[anchor=north] {\x}; + \node[anchor=west] at (10,0) {$x$}; + \foreach \y in {0,...,10} + \draw (1pt,\y) -- (-3pt,\y) + node[anchor=east] {\y}; + \node[anchor=south] at (0,10) {$y$}; + + \foreach \v in {0,...,4} + \node [dot,radius=0.2pt] at (0 + 2*\v,1 + 2*\v) { }; + + \draw [draw=black, fill=gray, fill opacity=0.2] + (0,1) -- (0,9) -- (8,9) -- (8,1) -- (0,1); + \end{tikzpicture} + \caption{Comparison between concrete and abstract domains} + \end{figure} +\end{frame} + +\begin{frame}{$\max$-strategy improvement} + \begin{itemize} + \item + Transform a program into equations + \item + Solve equations + \end{itemize} +\end{frame} + +\begin{frame}[fragile]{$\max$-strategy example} + \begin{center} + \begin{mdframed} + \begin{algorithmic} + \State $x = 0$ + \Comment $A$ + \While {$x \le 8$} \Comment $B$ + \State $x = x + 2$ + \EndWhile + \State print$(x)$ \Comment $C$ + \end{algorithmic} + \end{mdframed} + \end{center} + \alt<1>{\begin{align*} + ub(x)_A &\ge \infty \\ + ub(x)_B &\ge 0 \\ + ub(x)_B &\ge \min(ub(x)_B, 8) + 2 \\ + ub(x)_C &\ge ub(x)_B + \end{align*} + }{\begin{align*} + ub(x)_A &= \infty \\ + ub(x)_B &= \max(0, \min(ub(x)_B, 8) + 2) \\ + ub(x)_C &= ub(x)_B \\ + ~ + \end{align*}} + \only<2>{} +\end{frame} + +\begin{frame}[fragile]{$\max$-strategies} + A $\max$-strategy is a decision about which argument in a + $\max$-expression to choose. + \begin{align*} + ub(x)_A &= \infty \\ + ub(x)_B &= \max(\alert<2>{0}, \alert<3>{\min(ub(x)_B, 8) + 2}) \\ + ub(x)_C &= ub(x)_B + \end{align*} +\end{frame} + +\begin{frame}[fragile]{Solver} + \begin{figure} + \begin{tikzpicture} + \node [rectangle, draw, align=center](max) at (0,0) {Maximiser \\ improve strategy}; + \node [rectangle, draw, align=center](min) at (0,-3) {Minimiser \\ find assignment}; + + \path[] + (min) edge[bend left,arrows={-latex}] + node[anchor=east]{variable assignment} + (max) + + (max) edge[bend left,arrows={-latex}] + node[anchor=west]{$\max$-strategy} + (min); + \end{tikzpicture} + \caption{The high-level structure of the solver presented in + \cite{Gawlitza:2007:PFC:1762174.1762203}} + \end{figure} +\end{frame} + +\section{Contribution} +\begin{frame}[fragile]{Solver - enhancements} + The big idea: take into account data-dependencies + \begin{align*} + \alert<4>{x} &\alert<4>{= \max(0, \min(x - 1, \alert<3>{y}))} \\ + \alert<2-4>{y} &= \max(0, x + 5, x) \\ + z &= \max(0, z + 1, x) + \end{align*} +\end{frame} + +\begin{frame}[fragile]{Solver - enhancements} + \begin{figure} + \begin{tikzpicture} + \node [rectangle, draw, align=center](max) at (0,0) {Maximiser \\ improve strategy}; + \node [rectangle, draw, align=center](min) at (0,-3) {Minimiser \\ find assignment}; + + \path[] + (min) edge[bend left,arrows={-latex}] + node[anchor=east,align=right]{variable assignment \\ change set} + (max) + + (max) edge[bend left,arrows={-latex}] + node[anchor=west,align=left]{$\max$-strategy \\ change set} + (min); + \end{tikzpicture} + \caption{The high-level structure of our enhanced solver} + \end{figure} +\end{frame} + +\section{Results} +\begin{frame}{Implementation} + \begin{itemize} + \item + Implemented in C++ + \item + Integrated into the LLVM/Clang static analysis framework + \end{itemize} +\end{frame} + +\begin{frame}{Example system} + \begin{align*} + x_0 &= \max(-\infty, 0) \\ + x_1 &= \max(-\infty, x_0) \\ + x_2 &= \max(-\infty, x_1) \\ + ... &~ ... \\ + x_n &= \max(-\infty, x_{n-1}) + \end{align*} +\end{frame} + +\begin{frame}{Runtime improvements} + \begin{figure} + \begin{tikzpicture} + \begin{loglogaxis}[% + scale only axis, + width=9cm, + height=5cm, + xmin=1, xmax=65536, + xlabel=size of equation system, + ymin=0, ymax=40, + ylabel=time (in seconds), + axis on top] + \addplot[ + ybar, + bar width=0.5cm, + bar shift=0in, + fill=red, + draw=black] + plot coordinates{ + (1,0.000021982 ) + (2,0.000037083 ) + (4,0.000090918 ) + (8,0.000331411 ) + (16,0.001678790 ) + (32,0.010238535 ) + (64,0.069774912 ) + (128,0.520062180 ) + (256,3.983806321 ) + (512,31.469653195 ) + }; + + \end{loglogaxis} + \end{tikzpicture} + \caption{Performance of the naive algorithm} + \end{figure} +\end{frame} + +\begin{frame}{Runtime improvements} + \begin{figure} + \begin{tikzpicture} + \begin{loglogaxis}[% + scale only axis, + width=9cm, + height=5cm, + xmin=1, xmax=65536, + xlabel=size of equation system, + ymin=0, ymax=40, + ylabel=time (in seconds), + axis on top] + \addplot[ + ybar, + bar width=0.5cm, + bar shift=0in, + fill=red, + draw=black] + plot coordinates{ + (1,0.000044508 ) + (2,0.000063953 ) + (4,0.000094303 ) + (8,0.000176679 ) + (16,0.000312958 ) + (32,0.000642421 ) + (64,0.001194996 ) + (128,0.002451839 ) + (256,0.004786286 ) + (512,0.009280946 ) + (1024,0.019159827 ) + (2048,0.038067689 ) + (4096,0.080535540 ) + (8192,0.151181571 ) + (16384,0.339113750 ) + (32768,0.593622054 ) + (65536,1.217525509 ) + }; + + \end{loglogaxis} + \end{tikzpicture} + \caption{Performance of our improved algorithm} + \end{figure} +\end{frame} + +\section{Future work} +\begin{frame}{Future work} + \begin{itemize} + \item + Still slightly over-approximating dependencies + \item + LLVM/Clang integration is only a proof-of-concept + \end{itemize} +\end{frame} + +\begin{frame}[fragile,allowframebreaks]{References} + \phantomsection + \bibliographystyle{abbrvnat} + \bibliography{references} +\end{frame} + +\begin{frame}{Contributions} + \begin{itemize} + \item + Improvement of $\max$-strategy iteration algorithm, leveraging + sparsity of variable dependencies + \item + Implementation of a $\max$-strategy iteration based static + analyser in the LLVM/Clang framework + \end{itemize} +\end{frame} + +\end{document} diff --git a/tex/presentation/references.bib b/tex/presentation/references.bib new file mode 100644 index 0000000..29f2972 --- /dev/null +++ b/tex/presentation/references.bib @@ -0,0 +1,156 @@ +@article{DBLP:tr/trier/MI96-11, + author = {Christian Fecht and + Helmut Seidl}, + title = {An Even Faster Solver for General Systems of Equations}, + journal = {Universit{\"a}t Trier, Mathematik/Informatik, Forschungsbericht}, + volume = {96-11}, + year = {1996}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@inproceedings{CousotCousot77-1, + author = {Cousot, P{.} and Cousot, R{.}}, + title = {Abstract interpretation: a unified lattice model for static + analysis of programs by construction or approximation of + fixpoints}, + pages = {238--252}, + booktitle = {Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT + Symposium on Principles of Programming Languages}, + address = {Los Angeles, California}, + publisher = {ACM Press, New York, NY}, + year = 1977, +} +@article{mine:hosc06, + author = {Min\'e, A{.}}, + title = {The Octagon Abstract Domain}, + journal = {Higher-Order and Symbolic Computation}, + editor = {O. Danvy}, + publisher = {Springer}, + year = {2006}, + volume = {19}, + number = {1}, + pages = {31--100}, + note = {\url{http://www.di.ens.fr/~mine/publi/article-mine-HOSC06.pdf}} +} +@inproceedings{mine:padoII, + author = {Min\'e, A{.}}, + title = {A New Numerical Abstract Domain Based on Difference-Bound Matrices}, + booktitle = {Proc. of the 2d Symp. on Programs as Data Objects (PADO II)}, + series = {Lecture Notes in Computer Science}, + year = {2001}, + month = {May}, + pages = {155--172}, + volume = {2053}, + publisher = {Springer}, + location = {Aarhus, Danemark}, + note = {\url{http://www.di.ens.fr/~mine/publi/article-mine-padoII.pdf}} +} +@inproceedings{DBLP:conf/vmcai/SankaranarayananSM05, + author = {Sriram Sankaranarayanan and + Henny B. Sipma and + Zohar Manna}, + title = {Scalable Analysis of Linear Systems Using Mathematical Programming}, + booktitle = {VMCAI}, + year = {2005}, + pages = {25-41}, + ee = {http://dx.doi.org/10.1007/978-3-540-30579-8_2}, + bibsource = {DBLP, http://dblp.uni-trier.de} +} +@inproceedings{Dor:2001:CCS:647170.718291, + author = {Dor, Nurit and Rodeh, Michael and Sagiv, Shmuel}, + title = {Cleanness Checking of String Manipulations in C Programs via + Integer Analysis}, + booktitle = {Proceedings of the 8th International Symposium on Static + Analysis}, + series = {SAS '01}, + year = {2001}, + isbn = {3-540-42314-1}, + pages = {194--212}, + numpages = {19}, + url = {http://dl.acm.org/citation.cfm?id=647170.718291}, + acmid = {718291}, + publisher = {Springer-Verlag}, + address = {London, UK, UK}, +} +@INPROCEEDINGS{Yovine98modelchecking, + author = {Sergio Yovine}, + title = {Model checking timed automata}, + booktitle = {In European Educational Forum: School on Embedded + Systems}, + year = {1998}, + pages = {114--152}, + publisher = {Springer-Verlag} +} +@inproceedings{Gawlitza:2007:PFC:1762174.1762203, + author = {Gawlitza, Thomas and Seidl, Helmut}, + title = {Precise fixpoint computation through strategy iteration}, + booktitle = {Proceedings of the 16th European conference on Programming}, + series = {ESOP'07}, + year = {2007}, + isbn = {978-3-540-71314-2}, + location = {Braga, Portugal}, + pages = {300--315}, + numpages = {16}, + url = {http://dl.acm.org/citation.cfm?id=1762174.1762203}, + acmid = {1762203}, + publisher = {Springer-Verlag}, + address = {Berlin, Heidelberg}, +} +@article{tarski, + author = {Tarski, Alfred}, + title = {A lattice-theoretical fixpoint theorem and its + applications.}, + year = {1955} +} +@incollection {springerlink, + author = {Christensen, Aske and Mø, Anders and Schwartzbach, Michael}, + affiliation = {BRICS Denmark}, + title = {Precise Analysis of String Expressions}, + booktitle = {Static Analysis}, + series = {Lecture Notes in Computer Science}, + editor = {Cousot, Radhia}, + publisher = {Springer Berlin / Heidelberg}, + isbn = {978-3-540-40325-8}, + keyword = {Computer Science}, + pages = {1076-1076}, + volume = {2694}, + year = {2003} +} +% http://www.mrtc.mdh.se/projects/wcet/benchmarks.html +@InProceedings{Gustafsson:WCET2010:Benchmarks, + author = {Jan Gustafsson and Adam Betts and Andreas Ermedahl and Bj{\"{o}}rn Lisper}, + title = {The {M{\"a}lardalen} {WCET} Benchmarks -- Past, Present and Future}, + booktitle = WCET2010, + OPTcrossref = {}, + OPTkey = {}, + pages = {137--147}, + year = {2010}, + editor = {Bj{\"o}rn Lisper}, + OPTvolume = {}, + OPTnumber = {}, + OPTseries = {}, + address = {Brussels, Belgium}, + month = jul, + OPTorganization = {}, + publisher = {OCG}, + OPTnote = {}, + OPTannote = {} +} +@misc{fixpoint-slides, + author = {Helmut Seidl}, + title = {Lecture Slides in Program Optimisation}, + url = {http://www2.in.tum.de/~seidl/Courses/WS2011/Optimierung/all2011.pdf}, + urldate = {2012-11-04}, + year = {2011} +} +@article{Rice, + author = {H. Rice}, + title = {Classes of Recursively Enumerable Sets and their + Decision problems}, + year = {1953}, + journal = {Transactions of the American Mathematical Society}, + volume = {83} +} +@book{debugging-book, + title = {Why Programs Fail: A Guide to Systematic Debugging}, + author = {Andreas Zeller} +} |