From 62d8d7011c339f9b192099b2fc6a6d2f567f0a4d Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Wed, 28 Nov 2012 11:09:10 +1100 Subject: Ahhh! Lots of things. --- tex/thesis/litreview/litreview.tex | 125 +++++++++++++++++++++++-------------- 1 file changed, 78 insertions(+), 47 deletions(-) (limited to 'tex/thesis/litreview/litreview.tex') 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. -- cgit v1.2.3