diff options
Diffstat (limited to 'tex/thesis/introduction')
| -rw-r--r-- | tex/thesis/introduction/introduction.tex | 65 |
1 files changed, 57 insertions, 8 deletions
diff --git a/tex/thesis/introduction/introduction.tex b/tex/thesis/introduction/introduction.tex index ffc6cd2..17473af 100644 --- a/tex/thesis/introduction/introduction.tex +++ b/tex/thesis/introduction/introduction.tex @@ -36,9 +36,42 @@ in some way \emph{verify} the software before running it. While it is possible to write programs in a way that is easier to verify, it is still a difficult and expensive process to provide verification. -Recently there has been work done in automatically analysing programs -in order to identify bugs. This work is broadly classed \emph{static - analysis} and this thesis contributes to this work. +There has been a continuous stream of research into automatically +analysing programs in order to identify bugs from the late 70s to the +present\cite{CousotCousot77-1,EasyChair:117}. This work is broadly +classed \emph{static analysis} and this thesis contributes to this +work. + +Due to Rice's Theorem\cite{Rice} we know that it is impossible to +perform a perfect static analysis in general. In order to overcome +this many approaches to static analysis have been developed, including +the framework of abstract interpretation presented by Cousot and +Cousot\cite{CousotCousot77-1}. In this framework we consider a program +in a simplified, \emph{abstract}, domain. This allows us to perform a +sound analysis in general at the expense of precision. + +Two abstract domains which are particularly well-known and useful are +those of \emph{interval} and \emph{zones}. The interval abstract +domain consists of restricting variables in the range $[a,b]$. This +domain can be useful for avoiding such program errors as division by +zero errors and out of bounds memory accesses. The abstract domain of +zones allows us to further place a bound on the difference between +variables $x - y \le c$. This allows us to be more precise in our +analysis, thereby avoiding false-positives, at the cost of speed. + +The process of determining appropriate bounds for program variables +has traditionally been performed by performing several Kleene +iterations, followed by a \emph{widening} and \emph{narrowing}. These +widening and narrowing operators ensure termination, but once again at +the cost of precision. As an alternative to these operators we can, in +some instances, use a game-theoretic approach to compute the abstract +semantics of a program\cite{EasyChair:117}. This approach is less +general than widening and narrowing, but performs precise abstract +interpretation over zones. + +In this thesis we present an implementation of this game-theoretic +algorithm, along with our own enhancements which improve its +performance on real-world data. @@ -56,7 +89,7 @@ Theoretical contribution: \item We present a demand-driven strategy improvement algorithm for solving monotonic, expansive equation systems involving $\min$ and - $\max$ operators + $\max$ operators. \end{enumerate} Systems contribution: @@ -64,13 +97,29 @@ Systems contribution: \item We develop a solver for monotonic, expansive equation systems based on the work of Gawlitza et al.\cite{EasyChair:117} with several - improvements + improvements. \item We analyse the performance of our improved solver on a set of - equation systems to demonstrate the effect of our improvements + equation systems to demonstrate the effect of our improvements. \item We integrate our solver into the LLVM framework to perform analysis - over Zones\cite{mine:padoII} + over Zones\cite{mine:padoII}. \item - We analyse the performance of our LLVM analysis on various program inputs + We analyse the performance of our LLVM analysis on various program + inputs. \end{enumerate} + +\section{Structure of the thesis} + +In Chapter \ref{chap:litreview} we review the background literature in +the field of static analysis, laying the basis for the rest of the +thesis. %TODO: more + +We present our theoretical contribution in \ref{chap:contribution}: a +demand-driven strategy improvement algorithm. We present the algorithm +along with an evaluation of its performance on realistic problems. + +Our implementation is discussed in Chapter +\ref{chap:implementation}. We discuss several aspects of our +implementation before evaluating the results of our analysis on +several programs. |