summaryrefslogtreecommitdiff
path: root/tex/thesis/litreview/litreview.tex
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/litreview/litreview.tex')
-rw-r--r--tex/thesis/litreview/litreview.tex81
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}.