From 3d206f03985b50beacae843d880bccdc91a9f424 Mon Sep 17 00:00:00 2001
From: Carlo Zancanaro <carlo@pc-4w14-0.cs.usyd.edu.au>
Date: Mon, 10 Sep 2012 17:04:34 +1000
Subject: Thesis updating.
---
tex/thesis/litreview/litreview.tex | 426 ++++++++++++++++++++++---------------
1 file changed, 258 insertions(+), 168 deletions(-)
(limited to 'tex/thesis/litreview')
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}
--
cgit v1.2.3