summaryrefslogtreecommitdiff
path: root/tex/thesis/litreview
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/litreview')
-rw-r--r--tex/thesis/litreview/litreview.tex378
1 files changed, 164 insertions, 214 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex
index 1ac34d5..1e0ef90 100644
--- a/tex/thesis/litreview/litreview.tex
+++ b/tex/thesis/litreview/litreview.tex
@@ -1,184 +1,173 @@
\newcommand{\Env}{\mathsf{Env}}
\newcommand{\PP}{\mathsf{PP}}
-\newcommand{\States}{\mathsf{States}}
+\newcommand{\states}{\mathsf{states}}
\newcommand{\state}{\mathsf{state}}
\renewcommand{\b}[1]{\mathbf{#1}}
+\newcommand{\semantics}[1]{\llb #1 \rrb}
-\chapter{Literature Review} \label{chap:litreview}
+\newcommand{\Stmt}{\mathsf{Stmt}}
+\newcommand{\Vars}{\mathsf{Vars}}
+
+\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.
\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 Denotational
-Semantics\cite{SCOTT70B}.
-
-Denotational semantics takes a view of a program as a (partial)
-function built up by the composition of many smaller functions. By
-expressing our expressions, assignments, conditionals and loops as
-smaller functions we can then compose them to determine the semantics
-of our whole program. For imperative languages we consider each
-assignment, conditional or loop as having the denotation $\llb s \rrb:
-\state \to \state$. We define their composition as $\llb s_1 ; s_2
-\rrb = \llb s_2 \rrb \circ \llb s_1 \rrb$.
-
-As an example, we'll define some denotational semantics for a simple
-language. Here our $\state$ will be a partial function $\state: I \to \N$
-\begin{figure}[H]
- \begin{minipage}{\textwidth}
- Syntax:
- \end{minipage} \\[0.1cm]
- \begin{minipage}{0.8\textwidth}
- $P ::= S$ \\
- $S ::= S_1;S_2 \mid \b{if}~ B ~\b{then}~ S_1 ~\b{else~} S_2 \mid I := E$ \\
- $E ::= E_1 + E_2 \mid I \mid N$ \\
- $B ::= E_1 = E_2 \mid \lnot B$ \\
- $I ::= $ variable identifiers \\
- $N ::= \N$
- \end{minipage}
- \\[0.5cm]
- \begin{minipage}{\textwidth}
- Semantics:
- \end{minipage} \\[0.1cm]
- \begin{minipage}{0.8\textwidth}
- $\b{P}: \state \to \state$ \\
- $\b{P}\llb S \rrb = \b{S}\llb S \rrb \{\}$ \\[0.2cm]
-
- $\b{S}: \state \to \state$ \\
- $\b{S}\llb S_1;S_2 \rrb = \lambda v . (\b{S}\llb S_2 \rrb (\b{S}\llb S_1 \rrb(v)))$ \\
- $\b{S}\llb \b{if}~ B ~\b{then}~ S_1 ~\b{else~} S_2 \rrb = \lambda v . (\b{S} \llb S_b \rrb(v))$
- where $b = \b{B}\llb B \rrb (v) + 1$ \\
- $\b{S}\llb I := E \rrb = \lambda v: (v \oplus \{ I \mapsto \b{E}\llb E \rrb(v) \})$ \\[0.2cm]
-
- $\b{E}: \state \to \N$ \\
- $\b{E}\llb E_1 + E_2 \rrb = \lambda v . (\b{E}\llb E_1 \rrb(v) + \b{E}\llb E_2 \rrb(v))$ \\
- $\b{E}\llb I \rrb = \lambda v . v(I)$ \\
- $\b{E}\llb N \rrb = \lambda v . N$ \\[0.2cm]
-
- $\b{B}: \state \to \{0,1\}$ \\
- $\b{B}\llb E_1 = E_2 \rrb = \lambda v . (\b{if}~ \b{E}\llb E_1 \rrb(v) = \b{E}\llb E_2 \rrb(v) ~\b{then}~ 1 ~\b{else}~ 0)$
- \end{minipage}
- \caption{Denotational semantics for a simple language.}
- \label{fig:denotational-semantics-example}
-\end{figure}
-
-
-
-A program's semantics can be realised by considering the possible
-values for each variable at each point in the program, which we will
-refer to as the possible \emph{states} of the program, and the
-transitions between these states performed by \emph{statements}.
-
-If we consider a finite set of control points, $N$, and a finite set
-of variables $X$ then we can capture the state of a program at a
-particular point
-
-As a formalisation of these notions we can consider these to be
-defined as follows:
+but for our purposes we will consider \emph{denotational}, or
+\emph{mathematical}, \emph{semantics}\cite{SCOTT70B}.
+
+Denotational semantics views a program as a (partial) function built
+up by the composition of many smaller functions. By expressing our
+expressions, assignments, conditionals and loops as smaller functions
+we can compose them to determine the semantics of the whole
+program. The operator $\semantics{\cdot}$ represents the semantics of
+its argument as a mathematical function.
+
+In imperative languages programs are not a series of functional
+transformations, however, each statement or expression may have
+side-effects, so it is necessary to introduce some notion of ``state''
+into our semantics. By defining $\semantics{\cdot}: \states \to
+\states$ for all statements $x$ we provide a mechanism for statements
+to perform side effects. Elements of $\states$ each represent a
+possible state for the program to be in. For example: for an
+integral assignment statement $I := E$, assigning the value of an
+expression $E$ to a variable $I$, have the following denotation:
\begin{align*}
- \Env:& X \to \Z \\
- \PP:& \{ \text{program points} \} \\
- \States:& \PP \times \Env
+ \semantics{I := E} = \lambda \rho . (\rho \oplus \{I \mapsto \semantics{E}(\rho)\})
\end{align*}
+where $\rho \in \states$ and $\semantics{E}: \states \to \Z$. Our
+$\states$ in this case are functions $\rho: \Vars \to \D$ from
+variables to values.
+
+Denotational semantics provide a formal abstract framework for us to
+analyse programs mathematically, but they do not provide a meaningful
+way to perform automated analysis of programs. As they perfectly
+capture the semantics of a program they do not avoid the consequences
+of Rice's Theorem\cite{Rice} or the Halting Problem\cite{Halting}
+which preclude us from performing precise analysis of programs in
+general.
+\section{Abstract Interpretation} \label{sec:abstract-interpretation}
+In order to work around the limitations on precise static analysis in
+general, Cousot et al.~ developed a framework for performing sound
+program analysis called ``abstract
+interpretation''\cite{CousotCousot77-1}. In this framework we consider
+a program's semantics under an abstraction. The original semantics we
+call ``concrete semantics'' and the abstracted semantics we call
+``abstract semantics''. The abstract semantics consist of replacing
+$\D$ and $\state$ from the denotational semantics with ``abstracted''
+structures.
+To provide us with some intuition of these concepts, consider the
+following example:
+\begin{example}
+ Let us assume that our program's state is represented by $\rho:
+ \Vars \to \Z$, with values coming from $\Z$.
-Let $X$ be the set of program variables, $D$ be the union of all
-possible domains from which variables can come, and $PP$ be the set of
-all edges in the Control Flow Graph of the program.
-
-\begin{eqnarray}
-Env: {} & X \to D \\
-Expr: {} & Env \to D \\
-States: {} & PP \times Env
-\end{eqnarray}
-
-$States$, then, contains every possible state for the program ($Env$)
-at each program point. A more interesting set for us is the set of
-reachable states, this is: states which the program can actually reach
-during execution. This concept of ``reachable states'' allows us to
-formally capture all possible execution states for a program. We can
-further define $Reach(p) = {e \in Env | \le p,e \ge \in States}$
-
-Unfortunately it is unfeasible to analyse the complete semantics of a
-program, due to the sheer number of possible reachable states which
-must be examined. In many cases there are an infinite number of states
-which would have to be considered to ensure a sound analysis of the
-program.
+ 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
+ values from now):
+ \begin{align*}
+ x &\in \Z & (\pm) \\
+ x &\ge 0 & (+) \\
+ x &\le 0 &(-) \\
+ x &= 0 &(0)
+ \end{align*}
+ From this abstraction we can then determine something about normal
+ arithmetic operations in our program. We know, for instance, that
+ $(+) \times (-) = (-)$, or that $0 \times (\pm) = 0$. We also, then,
+ know that $x / 0$ is certainly an error.
+
+ \label{example:abstract-interpretation}
+\end{example}
+Abstraction sacrifices precision of analysis for decidability in
+general. By abstracting our domain in a way which is ``sound'', which
+safely over-approximates our concrete semantics, we ensure that any
+analysis we perform on the abstraction is also valid for the concrete
+semantics. Unfortunately in order to make this abstraction we
+sacrifice precision, so it is possible that the analysis will identify
+errors which are not errors in the concrete semantics.
-\section{Abstract Interpretation} \label{sec:abstract-interpretation}
\subsection{General Framework}
-Cousot and Cousot developed a framework for performing sound program
-analysis called ``Abstract Interpretation''. In this framework we
-consider a program under a set of ``abstract semantics'' which, in
-some sense, simplify the program (and the analysis thereof).
-
-As a simple example one may consider the case of mathematical
-expressions over the integers. The operators \(+,\times\) perform
-operations on these integers, with their semantics being defined as
-one would expect. We may then define an abstract semantic of these
-expressions when considering only signs (and zero), for example. Then
-our abstract states contains four states: ${(+), (-), (\pm), 0}$.
-
+In order to transform between the concrete and abstract domains we
+define two functions: $\alpha$ and $\gamma$. The function $\alpha:
+2^\states \to \states_\alpha$ transforms a concrete state into an
+abstract state. The function $\gamma: \states_\alpha \to 2^\states$
+transforms an abstract state into a set of concrete states. We require
+these two functions to satisfy the properties of a Galois connection:
\begin{align*}
- ( + ) + ( + ) &= ( + ) \\
- ( + ) + ( - ) &= ( \pm ) \\
- ( - ) + ( - ) &= ( - ) \\
- x + 0 &= x \\
- ( \pm ) + x &= ( \pm ) \\
- ( + ) \times ( + ) &= ( + ) \\
- ( + ) \times ( - ) &= ( - ) \\
- ( - ) \times ( + ) &= ( - ) \\
- 0 \times x &= 0 \\
- ( \pm ) \times x &= ( \pm ), \forall x \ne 0 \\
+ a &\le \gamma(b) & \alpha(a) &\le b & \forall a, b
+ \subseteq \states.
\end{align*}
-
-This abstract semantic will give us sound results (any analysis of the
-abstract semantic will correspond to an equivalent analysis of the
-concrete semantic), but will not give us every opportunity for
-analysis (the abstraction may ignore relevant details).
-
-In order to ensure we have a useful abstract interpretation it's
-necessary to provide two operations to map between concrete states and
-abstract states. These operations we call ``abstraction'' (mapping
-from a concrete state to an abstract state), denoted by \(\alpha\),
-and ``concretization'' (mapping from an abstract state to a concrete
-state), denoted by \(\gamma\).
-
-\textbf{Write more about the abstraction/concretization functions}
+\noindent As a consequence of this, the result of abstracting $a \in
+\states$ must at least contain $a$. In particular we are looking for
+the \emph{best} abstract transformers, such that $\alpha(a)$ is as
+tight as possible for a state $a$.
+
+Abstract interpretation follows on from the idea of denotational
+semantics, and it is possible to determine the abstract semantics of
+an operation based on its concrete semantics. We use
+$\semantics{\cdot}^\#$ to represent the abstract semantics of a
+statement, and define the transformation as $\semantics{S}^\# = \alpha
+\circ \semantics{s} \circ \gamma$.
+
+Much has been written on the topic of abstract domains, ranging from
+the relatively simple, such as signs and
+intervals\cite{CousotCousot77-1} to the more complex
+zones\cite{mine:padoII}, octagons\cite{mine:hosc06} and more general
+convex polyhedra\cite{DBLP:conf/vmcai/SankaranarayananSM05}. For this
+thesis we are only concerned with \emph{intervals} and \emph{zones}.
+
+%\todo{widening}
\subsection{Intervals}
-Something about intervals.
-
-\subsection{Zones} \label{subsec:zones}
+The abstract domain of \emph{intervals} was introduced by Cousot et
+al.\cite{CousotCousot77-1} along with abstract interpretation. In this
+domain we constrain each variable $x$ to lie within a range $[a, b]
+\in \CZ^2$. This domain is finer than signs, so it allows more
+information about the program to be determined. Another equivalent
+formulation of intervals is that we are finding bounds such that
+\begin{align*}
+ x &\le b \text{ and,} \\
+ -x &\le a.
+\end{align*}
+%\noindent We are finding \emph{upper bounds} for $x$ and $-x$ at each
+%location in the program.
-In order to perform any abstract interpretation we must first
-determine which abstract domain we will consider. Cousot and Cousot
-introduced the abstract domain of ``ranges'' in their original paper
-\cite{CousotCousot77-1}. This domain constrains variables to lie
-within a range \(x \in [a, b]\) with \(x, a, b \in \Z\).
-Further work has been done the abstract domain of zones and octagons,
-which are generalised by the template polyhedral abstract domain.
+\subsection{Zones}
-Zones provide an abstract domain in which we try to put a bound on
-either a variable's magnitude ($\pm x \le c$) or to put a bound on the
-difference between two variables ($x - y \le c$).
+\emph{Zones} are an abstract domain introduced by
+Min\'e\cite{mine:padoII} which generalise intervals to include also
+bounding the differences between variables. For each variable $x$
+zones constrain the variable and its negation in the same way as intervals,
+\begin{align*}
+ x &\le b \text{ and,} \\
+ -x &\le a.
+\end{align*}
+Zones additionally provide us with bounds on \emph{differences}
+between variables. So for each pair of variables $(x,y)$, zones
+provide us with a bound
+\begin{align*}
+ x - y & \le c.
+\end{align*}
-Octagons generalise this by allowing us to vary the sign on both
-variables to derive a bound as $\pm x \pm y \le c$.
-The polyhedral abstract domain is a clear generalisation of both the
-zone and octagon abstract domains in that it determines a bound for an
-arbitrary linear combination of arbitrary program variables. For
-example, finding a bound as $c_0 x_0 + c_1 x_1 + ... + c_n x_n \le c$,
-where $c, c_i \in \R$ and $x_i$ are program variables.
\section{Min/max problem}
@@ -187,19 +176,17 @@ In \newcite{Gawlitza:2007:PFC:1762174.1762203} a conversion from a
program's Control Flow Graph (henceforth CFG) to a system of equations
involving only monotonic, expansive operators is presented. This
conversion results in an equation system which can be solved in order
-to perform Abstract Interpretation (Section
-\ref{sec:abstract-interpretation}) over Zones (Section
-\ref{subsec:zones}).
+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}
+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}. $st \in N$ denotes
+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],
@@ -254,19 +241,10 @@ we find that $V^\# [v] \ge \llb s_{(w,v)} \rrb ^\# (V^\# [w])$.
For the start node in the CFG this inequality is obviously
useless. The start node has no predecessors (by definition) and thus
must have a value that is not dependent on other nodes. We can,
-therefore, simply define the start node's possible abstract states to
-be at least as big as the complete set of abstract states (as in
+therefore, define the start node's possible abstract states to be at
+least as big as the complete set of abstract states (as in
\eqref{eqn:start-node}).
-We have not yet considered the effect that $s_{(u,v)}, \forall (u,v)
-\in E$ has on the state in each edge. The effect of the statement in
-the abstract domain depends on the statement's effect in the concrete
-domain, but for all statements we define $\llb s \rrb^\# := \alpha
-\circ \llb s \rrb \circ \gamma$. In essence this is just changing the
-environment in which the statement is acting, so the statement's
-effects are moved into our abstract domain with our abstraction and
-concretization functions.
-
\begin{example}
\label{example:partial-ordered-construction}
@@ -276,7 +254,7 @@ concretization functions.
\begin{minipage}{5cm}
\begin{lstlisting}
x = 1
- while x <= 99:
+ while x <= 9:
x = x + 1
\end{lstlisting}
\end{minipage}
@@ -292,23 +270,25 @@ concretization functions.
\path[every node/.style={fill=none}]
(A) edge node[right]{$x = 1$} (B)
- (B) edge [loop right] node[right]{$x \le 99: x = x + 1$} (B)
- (B) edge node[right]{$x > 99$} (C);
+ (B) edge [loop right] node[right]{$x \le 9: x = x + 1$} (B)
+ (B) edge node[right]{$x > 9$} (C);
\end{tikzpicture}
\end{minipage}
- \caption{Program and CFG for Example
- \ref{example:partial-ordered-construction}}
+ \caption{A simple program with its corresponding CFG}
\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} of $x$:
+ the \emph{least upper bound}
\begin{align*}
- ub: {} & ~\text{\bf Vars} \to \CZ \\
- ub(x) &= \min\{v \in \CZ ~|~ x \le v\}
+ 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)$.
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
@@ -322,8 +302,8 @@ concretization functions.
itself, the other from $A$.
The edge from $A$ to $B$ is very simple. It has no constraint and
- simply sets the value of $x$ to $1$. It corresponds to an equation
- of the form $ub(x_B) \ge 1$.
+ sets the value of $x$ to $1$. It corresponds to an equation of the
+ form $ub(x_B) \ge 1$.
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
@@ -336,7 +316,7 @@ concretization functions.
$ub(x_B)$.
\begin{align*}
ub(x_B) &\ge 1 \\
- ub(x_B) &\ge \min(ub(x_B), 99) + 1
+ ub(x_B) &\ge \min(ub(x_B), 9) + 1
\end{align*}
The upper bound on the value of $x$ for node $C$ is the same as the
@@ -355,7 +335,7 @@ concretization functions.
\begin{align*}
ub(x_A) &\ge \infty \\
ub(x_B) &\ge 1 \\
- ub(x_B) &\ge \min(ub(x_B), 99) + 1 \\
+ ub(x_B) &\ge \min(ub(x_B), 9) + 1 \\
ub(x_C) &\ge ub(x_B)
\end{align*}
@@ -398,37 +378,9 @@ 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$. For our
- second example we will consider the following program fragment:
-
- \begin{figure}[here]
- \begin{minipage}{5cm}
- \begin{lstlisting}
- x = 0
- while x <= 9:
- x = x + 1
- \end{lstlisting}
- \end{minipage}
- \hfill
- \begin{minipage}{0.5\textwidth}
- \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
- distance=2cm,main node/.style={circle,fill=blue!20,draw},every
- loop/.style={min distance=1.5cm}]
-
- \node[main node] (A) {$A$};
- \node[main node] (B) [below of=A] {$B$};
- \node[main node] (C) [below of=B] {$C$};
-
- \path[every node/.style={fill=none}]
- (A) edge node[right]{$x = 0$} (B)
- (B) edge [loop right] node[right]{$x \le 9: x = x + 1$} (B)
- (B) edge node[right]{$x > 9$} (C);
-
- \end{tikzpicture}
- \end{minipage}
- \caption{Program and CFG for Example \ref{example:both-bounds}}
- \label{fig:both-bounds}
- \end{figure}
+ is sufficient to determine an \emph{upper} bound for $-x$. We will
+ 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$.
@@ -461,7 +413,7 @@ one constraint by taking the maximum of them. This is because $x \ge
The first constraint comes from the edge $A \to B$. This edge does
not do much of interest, it ignores the preceding value of $x$ and
- simply sets $x$ to $1$. This is captured in the following inequality:
+ sets $x$ to $1$. This is captured in the following inequality:
\begin{align*}
\left(\begin{array}{c}
ub(x_B) \\ -lb(x_B)
@@ -507,7 +459,7 @@ one constraint by taking the maximum of them. This is because $x \ge
\end{array}\right)
\end{align*}
- The edge $B \to C$ is quite simple as it simply provides another
+ The edge $B \to C$ is quite simple as it provides another
restriction on the value of $x$ without any further
transformation. This restriction is placed on the lower-bound of $x$
only (leaving the upper-bound unchanged) and is captured by the
@@ -621,10 +573,8 @@ one constraint by taking the maximum of them. This is because $x \ge
-\subsection{Formalities}
-
-
+\endinput
\subsection{Example solve}
\label{sec-1-3-5}