diff options
Diffstat (limited to 'tex/thesis/litreview/litreview.tex')
| -rw-r--r-- | tex/thesis/litreview/litreview.tex | 81 |
1 files changed, 43 insertions, 38 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex index 1e0ef90..109864e 100644 --- a/tex/thesis/litreview/litreview.tex +++ b/tex/thesis/litreview/litreview.tex @@ -10,19 +10,19 @@ \chapter{Preliminaries} \label{chap:litreview} -In this chapter we will review the relevant portion of literature -pertaining to static analysis. We will briefly cover the semantics of -programs generally before looking more closely at the framework of -abstract interpretation for program analysis. The chapter will -conclude with an explanation of one particular method of abstract -interpretation over zones. +In this chapter we review the relevant literature pertaining to static +analysis. We briefly cover the semantics of programs generally before +looking more closely at the framework of abstract interpretation for +program analysis. The chapter concludes with an explanation of the +particular method of abstract interpretation over intervals and zones +which is implemented in this thesis. \section{Program Semantics} In order to perform any static analysis of a program it is necessary to have some notion of the \emph{semantics}, or meaning, of a program. The semantics of a program can be captured in several ways, -but for our purposes we will consider \emph{denotational}, or +but for our purposes we consider \emph{denotational}, or \emph{mathematical}, \emph{semantics}\cite{SCOTT70B}. Denotational semantics views a program as a (partial) function built @@ -77,7 +77,7 @@ following example: One possible abstraction would be to instead consider a variable's \emph{sign}. That is, to consider $x$ as satisfying one of the - following (the symbols in parentheses will be used to refer to these + following (the symbols in parentheses are used to refer to these values from now): \begin{align*} x &\in \Z & (\pm) \\ @@ -180,14 +180,14 @@ to perform abstract interpretation over zones. \subsection{Partial-ordering Formulation} -To begin our construction of the equation systems we first need to -formalise one of a CFG. For our purposes we will consider a CFG to be -a tuple $G = (N, E, s, st)$. A finite set of \emph{control-points} -$N$, a finite set $E \subseteq N \times N$ of \emph{edges} between -these control points (ie. if $(u,v) \in E$ then an edge exists in the -CFG from $u$ to $v$). A mapping $s: N \times N \to \Stmt$ taking each -edge in the CFG to a \emph{statement} $\in \Stmt$. $st \in N$ denotes -the special \emph{start control-point}. +To begin our construction of the equation systems we need to formalise +one of a CFG. We consider a CFG to be a tuple $G = (N, E, s, st)$. A +finite set of \emph{control-points} $N$, a finite set $E \subseteq N +\times N$ of \emph{edges} between these control points (ie. if $(u,v) +\in E$ then an edge exists in the CFG from $u$ to $v$). A mapping $s: +N \times N \to \Stmt$ taking each edge in the CFG to a +\emph{statement} $\in \Stmt$. $st \in N$ denotes the special +\emph{start control-point}. We can now begin our construction of our abstract semantics $V^\#[v], \forall v \in N$. @@ -280,15 +280,15 @@ least as big as the complete set of abstract states (as in \label{fig:partial-ordered-construction} \end{figure} - We will now attempt to derive a system of inequalities from this for - the \emph{least upper bound} + We now attempt to derive a system of inequalities from this for the + \emph{least upper bound} \begin{align*} ub: {} & ~\Vars \to \CZ \\ ub(x) &= \min\{v \in \CZ ~|~ x \le v\}. \end{align*} We wish to find a value for $ub(x)$ at each program point in our - original program. We will denote these values by $ub_A(x)$, - $ub_B(x)$ and $ub_C(x)$. + original program. We denote these values by $ub_A(x)$, $ub_B(x)$ and + $ub_C(x)$. For $A$ the value of $x$ is entirely unknown, so no useful bound can be given. The possible values of $x$ are bounded only by the top @@ -307,10 +307,10 @@ least as big as the complete set of abstract states (as in The edge from $B$ to itself is somewhat more complex. To begin with it changes the value of $x$ depending on the previous value of - $x$. It also is executed conditionally (when $x \le 99$), which will - affect the bound on $x$. Because the condition limits the growth of - $x$ the corresponding equation for this edge is $ub(x_B) \ge - \min(x, 99) + 1$. + $x$. It also is executed conditionally (when $x \le 99$), which + affects the bound on $x$. Because the condition limits the growth of + $x$ the corresponding equation for this edge is $ub(x_B) \ge \min(x, + 99) + 1$. This leaves us with two simultaneous constraints on the value of $ub(x_B)$. @@ -348,7 +348,7 @@ least as big as the complete set of abstract states (as in The partial-ordering formulation considered above is a helpful presentation of the problem in terms of constraints, but an equivalent system can be constructed to aid us in locating the \emph{least} -solution to the system. +solution to the constraint system. For every partial-ordering on a set there exists an equivalent lattice, defined in terms of a meet operator ($\vee$) and a join @@ -358,10 +358,11 @@ operator ($\land$), which are defined by the following relationships: x \le y ~&\iff~ x \land y = x \end{align*} -In the case that we are considering, with $x, y \in \CZ$, the meet and -join operators correspond with $\max$ and $\min$, respectively. This -allows us to simplify the system of inequalities in Example -\ref{example:partial-ordered-construction} to the following: +In the case of Example \ref{example:partial-ordered-construction}, +with $x, y \in \CZ$, the meet and join operators correspond with +$\max$ and $\min$, respectively. This allows us to simplify the system +of inequalities in Example \ref{example:partial-ordered-construction} +to the following: \begin{align*} ub(x_A) &= \infty \\ ub(x_B) &= \max(1, \min(ub(x_B), 99) + 1) \\ @@ -370,7 +371,11 @@ allows us to simplify the system of inequalities in Example The two constraints on the upper bound of $x_B$ can be combined into one constraint by taking the maximum of them. This is because $x \ge -\max(a, b) ~\implies~ x \ge a \text{ and } x \ge b$ +\max(a, b) ~\implies~ x \ge a \text{ and } x \ge b$. The +Knaster-Tarski Fixpoint +%We change from using $\ge$ in our constraints to using $=$ in our +%equation system as a consequence of the Knaster-Tarski Fixpoint +%Theorem\cite{Knaster-Tarski}. @@ -378,19 +383,19 @@ one constraint by taking the maximum of them. This is because $x \ge \label{example:both-bounds} In order to determine a lower bound for $x$ at each program point it - is sufficient to determine an \emph{upper} bound for $-x$. We will - again consider the program fragment in Figure + is sufficient to determine an \emph{upper} bound for $-x$. We again + consider the program fragment in Figure \ref{fig:partial-ordered-construction}. - We will now try to derive an equation system for the \emph{upper} - and \emph{lower} bounds of $x$. + We now try to derive an equation system for the \emph{upper} and + \emph{lower} bounds of $x$. In order to capture the state of the variables at each program point - we will consider the abstract state as the two-dimensional vector + we consider the abstract state as the two-dimensional vector $(ub(x), -lb(x))$, that is the upper bound of $x$, $ub(x)$, and the \emph{negated} lower bound of $x$, $-lb(x)$. The least fixpoint of - our system of equations over $\CZ^2$ will then give us our bounds - for $ub(x)$ and $lb(x)$. + our system of equations over $\CZ^2$ then gives us bounds for + $ub(x)$ and $lb(x)$. To begin with, let us once again consider the node $A$. At the point of $A$ there is no information as to the bounds of $x$, so our @@ -580,7 +585,7 @@ one constraint by taking the maximum of them. This is because $x \ge \label{sec-1-3-5} -Reconsidering our earlier equation system, we will now attempt to find +Reconsidering our earlier equation system, we now attempt to find the minimal fixpoint by means of \emph{policy iteration} and \emph{fixpoint iteration}. |