diff options
Diffstat (limited to 'tex/thesis/litreview')
| -rw-r--r-- | tex/thesis/litreview/litreview.tex | 426 |
1 files changed, 258 insertions, 168 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex index f227112..d2c5d6f 100644 --- a/tex/thesis/litreview/litreview.tex +++ b/tex/thesis/litreview/litreview.tex @@ -122,9 +122,9 @@ We can now begin our construction of our collecting semantics $V^\#[v], \forall v \in N$. \begin{align} -V^\# [st] &\ge \alpha(\Z^n) \label{eqn:start-node} \\ -V^\# [v] &\ge \llb s_{(u,v)} \rrb ^\# (V^\# [u]) & \forall (u,v) \in -E \label{eqn:confluence} + V^\# [st] &\ge \alpha(\Z^n) \label{eqn:start-node} \\ + V^\# [v] &\ge \llb s_{(u,v)} \rrb ^\# (V^\# [u]) & \forall (u,v) \in + E \label{eqn:confluence} \end{align} In the first equation, the possible abstract states of the start node @@ -187,29 +187,34 @@ concretization functions. \label{example:partial-ordered-construction} As an example, let us consider the following program: - - \begin{lstlisting} + + \begin{figure}[here] + \begin{minipage}{5cm} + \begin{lstlisting} x = 1 while x <= 99: - x = x + 1 - \end{lstlisting} - - \begin{figure} - \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 = 1$} (B) - (B) edge [loop right] node[right]{$x \le 99: x = x + 1$} (B) - (B) edge node[right]{$x > 99$} (C); - - \end{tikzpicture} - \caption{The CFG for Example + x = x + 1 + \end{lstlisting} + \end{minipage} + \hfill + \begin{minipage}{0.45\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 = 1$} (B) + (B) edge [loop right] node[right]{$x \le 99: x = x + 1$} (B) + (B) edge node[right]{$x > 99$} (C); + + \end{tikzpicture} + \end{minipage} + + \caption{Program and CFG for Example \ref{example:partial-ordered-construction}} \label{fig:partial-ordered-construction} \end{figure} @@ -218,9 +223,10 @@ concretization functions. \ref{fig:partial-ordered-construction}. We will now attempt to derive a system of inequalities from this for - the \emph{upper bound} of $x$: + the \emph{least upper bound} of $x$: \begin{align*} - ub(x) &= v \in \CZ \text{ such that } x \le v & \forall x \in \Z + ub: & ~\text{\bf Vars} \to \CZ \\ + ub(x) &= \min\{v \in \CZ ~|~ x \le v\} \end{align*} For $A$ the value of $x$ is entirely unknown, so no useful bound can @@ -275,7 +281,8 @@ concretization functions. \end{example} -\subsubsection{Lattice construction} +\subsection{Lattice construction} +\label{subsec:lattice-construction} The partial-ordering formulation considered above is a helpful presentation of the problem in terms of constraints, but an equivalent @@ -291,164 +298,247 @@ operator ($\land$), which are defined by the following relationships: \end{align*} In the case that we are considering, with $x, y \in \CZ$, the meet and -join operators correspond with $\min$ and $\max$, respectively. This -allows us to simplify our original system of inequalities to the -following: +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 following: \begin{align*} - ub(x_A) &\ge \infty \\ - ub(x_B) &\ge \max(1, \min(ub(x_B), 99) + 1) \\ - ub(x_C) &\ge ub(x_B) + ub(x_A) &= \infty \\ + ub(x_B) &= \max(1, \min(ub(x_B), 99) + 1) \\ + ub(x_C) &= ub(x_B) \end{align*} The two constraints on the upper bound of $x_B$ can be combined into -the one constraint by taking the maximum of the two constraints (that -is, by meeting the less restrictive constraint). This ensures that if -the combined constraint is satisfied then both of the original -constraints must also be satisfied. - - - -%\begin{example} - -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{lstlisting} -x = 0 -y = x -while x < 10: - x = x + 1 - y = y + x -\end{lstlisting} - -This program, as a CFG: - -\begin{center} -\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; y = x$} (B) - (B) edge [loop right] node[right]{$x < 10: x = x + 1; y = y + x$} (B) - (B) edge node[right]{$x \ge 10$} (C); - -\end{tikzpicture} -\end{center} - -%\end{example} +one constraint by taking the maximum of them. This is because $x > +\max(a, b) ~\implies~ x > a \text{ and } x > b$ -We will now try to derive an equation system for the \emph{upper} and -\emph{lower} bounds of $x$ and $y$. -In order to properly capture the state of the variables at each state -we will consider the abstract state as a vector of the form $(x_u, --x_l, y_u, -y_l)$. $x_u$ and $y_u$ are the upper bounds of $x$ and $y$ -respectively. $x_l$ and $y_l$ are the lower bounds of $x$ and $y$, -which are then negated, as explained above, to convert them into upper -bound problems. -Each statement in our example program is now a transformation on a -vector rather than a scalar (as our original example was). This makes -the equation system significantly more complex. - -Let us begin by deriving the equation system for the simplest node in -the CFG, $A$. - -\begin{eqnarray*} - \left(\begin{array}{c} - x_u \\ y_u \\ -x_l \\ -y_l - \end{array}\right)_A - &=& - \left(\begin{array}{c} - \infty \\ \infty \\ \infty \\ \infty - \end{array}\right) -\end{eqnarray*} - -This is the same as saying that $x$ and $y$ each lie within the range -$[-\infty, \infty]$. In other words: both $x$ and $y$ are unbounded at -node $A$ and we know nothing of their possible values. - -For node $B$ we, again, must take into account two transformations to -our state. The first is by the edge $A \to B$, the second by -the edge $B \to B$. We then take the less-restrictive of these -two bounds (which, again, is the $\max$ of the two). - -Let us begin with $A \to B$. +\begin{example} + \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 <= 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} -\begin{eqnarray*} -\left(\begin{array}{c} -x_u \\ y_u \\ -x_l \\ -y_l -\end{array}\right)_{AB} -&=& -\left(\begin{array}{c} -0 \\ 0 \\ 0 \\ 0 -\end{array}\right) \\ -\end{eqnarray*} + We will 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 + $(ub(x), -lb(x))$, that is the upper bound of $x$, $ub(x)$, and the + \emph{negated} lower bound of $x$, $-lb(x)$. The greatest fixpoint + of our system of equations over $\CZ^2$ will then give us our 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 + constraint must contain the entirety of $\CZ$. This corresponds to + $ub(x) = \infty, lb(x) = -\infty$, which gives us the following + inequality: + \begin{align*} + \left(\begin{array}{c} + ub(x)_A \\ -lb(x)_A + \end{array}\right) + &\ge + \left(\begin{array}{c} + \infty \\ \infty + \end{array}\right) + \end{align*} -This edge merely sets $x$ to $0$ and $y$ to $x$ (which is now the -constant $0$), so both the upper and lower bounds are $0$. This is the -simplest sort of edge possible, as it just sets both bounds to a -constant. + As before, the node $B$ is the first of particular interest to + us. With two incoming edges we must have two constraints for this + node. -Now, on to $B \to B$. + 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: + \begin{align*} + \left(\begin{array}{c} + ub(x)_B \\ -lb(x)_B + \end{array}\right) + &\ge + \left(\begin{array}{c} + 1 \\ -1 + \end{array}\right) + \end{align*} -\begin{eqnarray*} - \left(\begin{array}{c} - x_u \\ y_u \\ -x_l \\ -y_l - \end{array}\right)_{BB} - &=& - \left(\begin{array}{cccc} - 1 & 0 & 0 & 0 \\ - 1 & 1 & 0 & 0 \\ - 0 & 0 & 1 & 0 \\ - 0 & 0 & 1 & 1 - \end{array}\right) - \left(\begin{array}{c} - \min(x_u, 9) \\ y_u \\ -x_l \\ -y_l - \end{array}\right)_B - + - \left(\begin{array}{c} - 1 \\ 0 \\ -1 \\ 0 - \end{array}\right) -\end{eqnarray*} + The constraint from the edge $B \to B$ is somewhat more + complicated. The transformation $x = x + 1$ is represented by the + matrix/vector operations of multiplication and + addition. Multiplication by the identity matrix indicates that $x$ + itself is present in the right-hand side of the transformation, + while the addition of the vector \(\left(\begin{array}{c} 1 \\ -1 + \end{array}\right) \) captures the effect of the addition on + each of the bounds (increasing each of the bounds by one). + + The $x <= 9$ conditional, which is present on the edge, is captured + by the restriction on the growth of the upper bound. \(\min(ub(x)_B, + 9)\) ensures the upper-bound's growth is limited by the value + $9$. It should be noted that there is no bound placed on the + lower-bound as the program only bounds $x$'s growth from above on + this edge. + \begin{align*} + \left(\begin{array}{c} + ub(x)_B \\ -lb(x)_B + \end{array}\right) + &\ge + \left[\begin{array}{cc} + 1 & 0 \\ + 0 & 1 + \end{array}\right] + \left(\begin{array}{c} + \min(ub(x)_B, 99) \\ + -lb(x)_B + \end{array}\right) + + + \left(\begin{array}{c} + 1 \\ + -1 + \end{array}\right) + \end{align*} + The edge $B \to C$ is quite simple as it simply 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 + following inequality: + \begin{align*} + \left(\begin{array}{c} + ub(x)_C \\ + -lb(x)_C + \end{array}\right) + &\ge + \left(\begin{array}{c} + ub(x)_B \\ + \min(-lb(x)_B, 99) + \end{array}\right) + \end{align*} + This gives us the following inequalities for this program: + \begin{align*} + \left(\begin{array}{c} + ub(x)_A \\ -lb(x)_A + \end{array}\right) + &\ge + \left(\begin{array}{c} + \infty \\ \infty + \end{array}\right) + \\ + \left(\begin{array}{c} + ub(x)_B \\ -lb(x)_B + \end{array}\right) + &\ge + \left(\begin{array}{c} + 1 \\ -1 + \end{array}\right) + \\ + \left(\begin{array}{c} + ub(x)_B \\ -lb(x)_B + \end{array}\right) + &\ge + \left[\begin{array}{cc} + 1 & 0 \\ + 0 & 1 + \end{array}\right] + \left(\begin{array}{c} + \min(ub(x)_B, 99) \\ + -lb(x)_B + \end{array}\right) + + + \left(\begin{array}{c} + 1 \\ + -1 + \end{array}\right) + \\ + \left(\begin{array}{c} + ub(x)_C \\ + -lb(x)_C + \end{array}\right) + &\ge + \left(\begin{array}{c} + ub(x)_B \\ + \min(-lb(x)_B, 99) + \end{array}\right) + \end{align*} + By combining these expressions as discussed in Section + \ref{subsec:lattice-construction} we can obtain the following system + of equations: + \begin{align*} + \left(\begin{array}{c} + ub(x)_A \\ -lb(x)_A + \end{array}\right) + &= + \left(\begin{array}{c} + \infty \\ \infty + \end{array}\right) + \\ + \left(\begin{array}{c} + ub(x)_B \\ -lb(x)_B + \end{array}\right) + &= + \max\left( + \left(\begin{array}{c} + 1 \\ -1 + \end{array}\right), + \left[\begin{array}{cc} + 1 & 0 \\ + 0 & 1 + \end{array}\right] + \left(\begin{array}{c} + \min(ub(x)_B, 99) \\ + -lb(x)_B + \end{array}\right) + + + \left(\begin{array}{c} + 1 \\ + -1 + \end{array}\right) + \right) + \\ + \left(\begin{array}{c} + ub(x)_C \\ + -lb(x)_C + \end{array}\right) + &= + \left(\begin{array}{c} + ub(x)_B \\ + \min(-lb(x)_B, 99) + \end{array}\right) + \end{align*} -\begin{eqnarray*} - \left(\begin{array}{c} - x_u \\ y_u \\ -x_l \\ -y_l - \end{array}\right)_B - &=& - \max\left( - \left(\begin{array}{c} - x_u \\ y_u \\ -x_l \\ -y_l - \end{array}\right)_{AB}, - \left(\begin{array}{c} - x_u \\ y_u \\ -x_l \\ -y_l - \end{array}\right)_{BB} - \right) -\end{eqnarray*} +\end{example} -The bounds for $x$ and $y$ at node $C$ are very similar to those at -node $B$, except that $x$ has one additional constraint added to it on -the bottom. This changes its equation system slightly. -\begin{eqnarray*} - \left(\begin{array}{c} - x_u \\ y_u \\ -x_l \\ -y_l - \end{array}\right)_C - &=& - \left(\begin{array}{c} - x_u \\ y_u \\ -x_l \\ -y_l - \end{array}\right)_{B} -\end{eqnarray*} \subsection{Formalities} |