summaryrefslogtreecommitdiff
path: root/tex/thesis/litreview
diff options
context:
space:
mode:
Diffstat (limited to 'tex/thesis/litreview')
-rw-r--r--tex/thesis/litreview/litreview.tex125
1 files changed, 78 insertions, 47 deletions
diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex
index 983bb44..d223f36 100644
--- a/tex/thesis/litreview/litreview.tex
+++ b/tex/thesis/litreview/litreview.tex
@@ -276,14 +276,11 @@ interpretation over zones.
\end{figure}
We now attempt to derive a system of inequalities from this for the
- \emph{least upper bound} of $x$ at each program point.
- \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 denote these values by $ub_A(x)$, $ub_B(x)$ and
- $ub_C(x)$.
+ \emph{least upper bound} of a variable $x$ at each program
+ point. That is, we want to find a value $ub(x)$ such that, for all
+ possible executions of the program $x \le ub(x)$. We wish to find a
+ value for $ub(x)$ at each program point in our 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
@@ -370,10 +367,14 @@ equation system can be constructed to aid us in locating the
For every partial-ordering on a set there exists an equivalent
lattice, defined in terms of a meet operator ($\vee$) and a join
-operator ($\land$), which are defined by the following relationships:
+operator ($\land$), which are defined by:
\begin{align*}
- x \le y ~&\iff~ x \vee y = y \\
- x \le y ~&\iff~ x \land y = x
+ x \vee y = z \iff z \ge x, z \ge y, (w \ge x, w \ge y \implies w \ge
+ z, \forall w) \\
+ x \land y = z \iff z \le x, z \le y, (w \le x, w \le y \implies w \le
+ z, \forall w)
+ %x \le y ~&\iff~ x \vee y = y \\
+ %x \le y ~&\iff~ x \land y = x
\end{align*}
In the case of Example \ref{example:partial-ordered-construction},
@@ -595,47 +596,77 @@ constraint system.
\section{Min-cost flow}
-This matrix fomulation sufficient to calculate bounds on individual
+The matrix formulation is sufficient to calculate bounds on individual
program variables, as in the interval domain, but in doing so there is
a significant loss of precision. In order to reclaim some of this
-precision we can use a relational domain.
-
-
-
-
-
-\endinput
-
-\subsection{Example solve}
-\label{sec-1-3-5}
-
+precision we use a relational domain, such as zones.
-Reconsidering our earlier equation system, we now attempt to find
-the minimal fixpoint by means of \emph{policy iteration} and
-\emph{fixpoint iteration}.
+We use a ``template constraint matrix'' to specify interesting values
+for our analysis. A template constraint matrix is an $m \times n$
+matrix, where $n$ is the number of program variables and $m$ is the
+number of interesting abstract values.
-\begin{eqnarray*}
-x &=& \max(1, \min(x, 99) + 1) \\
-\end{eqnarray*}
-
-At the beginning and end of each player's turn we will have a variable
-assignment $\{ x \to ? \}$, which will start with the value
-$\{ x \to -\infty \}$.
+\begin{example}
+ If we have two program variables $x_1$ and $x_2$ then we can analyse
+ for values $x_1$, $-x_1$, $x_2$, $-x_2$, $(x_1 - x_2)$ and $(x_2 -
+ x_1)$. If we are only interested in the values of $x_1$, $x_2$ and
+ $(x_2 - x_1)$ then we set our template constraint matrix to be
+ \begin{align*}
+ T &= \left[\begin{array}{cc}
+ 1 & 0 \\
+ 0 & 1 \\
+ -1 & 1
+ \end{array}\right]
+ \end{align*}
+\end{example}
-The $\max$ player then gets a chance to play. They choose to improve
-the strategy by choosing for $x$ to take the value $1$. The $\min$
-player then has no choice but to find a variable assignment $\{ x
-\to 1 \}$, as the $\max$ player has left them no choice.
+This template constraint matrix also specifies the topology of a
+graph. By considering each row as an edge, and each column as a node,
+we can produce a directed graph $G$, such that for each row an edge
+exists between the column containing a $1$ and the column containing a
+$-1$ in that row. In order to guarantee that all rows exist in $G$ it
+is also necessary to add an extra ``dummy node'' such that any
+unspecified edges are adjacent to the dummy node.
-Play then returns to the $\max$ player who chooses, again, to improve
-their strategy to instead map $x$ to $\min(x, 99) + 1$. This time the
-$\min$ player must make a decision. It solves $x = \min(x, 99) + 1$
-for it's maximal fixpoint, deciding to use the $99$ value (as the $x$
-value will grow without bound with the $+ 1$, thereby making $99$ the
-minimum of the two options) and returning $\{ x \to 100 \}$ as
-the new assignment.
+\begin{example}
+ For the template constraint matrix
+ \begin{align*}
+ T &= \left[\begin{array}{cc}
+ 1 & 0 \\
+ 0 & 1 \\
+ -1 & 1
+ \end{array}\right]
+ \end{align*}
-The $\max$ player has no further way to improve their strategy, as $1
-< 100$, so the game is over. The minimal fixpoint of the original
-system has been found as $x = 100$.
+ \noindent we construct a directed graph
+
+ \begin{center}
+ \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
+ distance=2.5cm]
+ \node (x1)[draw,circle] {$x1$};
+ \node (x2)[draw,circle,below of=x1] {$x2$};
+ \node (dummy)[draw,circle,below right of=x1] {dummy};
+
+ \path
+ (x1) edge[->,bend left] node {} (dummy)
+ (x2) edge[->,bend left] node {} (x1)
+ (x2) edge[->,bend left] node {} (dummy);
+ \end{tikzpicture}.
+ \end{center}
+\end{example}
+Once we have determined the topology of this graph, we then perform
+abstract interpretation by assigning the nodes ``supplies'' and the
+edges ``costs''. The supplies correspond to a statement's semantics,
+capturing the combination of variables which are the result of a given
+assignment, while the costs consider the incoming values of variables
+into the statement.
+
+We use the min-cost flow problem on this graph as an operator in our
+equation systems. We fix the topology and the costs in the graph and
+then consider it as a function of its edge costs, which are the
+abstract values entering this node. The validity of this approach is
+considered by Gawlitza et al.~\cite{EasyChair:117}, where it is shown
+that the min-cost flow problem, when considered as a function of its
+edge weights is monotonic and quasi-expansive, thereby making it a
+valid operator in our equation systems.