From 763a5e6c80e7df2ca1b15bab6726cd50e7ed0add Mon Sep 17 00:00:00 2001 From: Carlo Zancanaro Date: Wed, 5 Sep 2012 15:34:42 +1000 Subject: Something, something. Thesis! --- tex/thesis/litreview/litreview.tex | 491 +++++++++++++++++++++++++++++++++++++ 1 file changed, 491 insertions(+) create mode 100644 tex/thesis/litreview/litreview.tex (limited to 'tex/thesis/litreview') diff --git a/tex/thesis/litreview/litreview.tex b/tex/thesis/litreview/litreview.tex new file mode 100644 index 0000000..f227112 --- /dev/null +++ b/tex/thesis/litreview/litreview.tex @@ -0,0 +1,491 @@ +\chapter{Literature Review} \label{chap:litreview} + +\section{Program Semantics} + +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. + + +\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}$. + +\begin{align*} + ( + ) + ( + ) &= ( + ) \\ + ( + ) + ( - ) &= ( \pm ) \\ + ( - ) + ( - ) &= ( - ) \\ + x + 0 &= x \\ + ( \pm ) + x &= ( \pm ) \\ + ( + ) \times ( + ) &= ( + ) \\ + ( + ) \times ( - ) &= ( - ) \\ + ( - ) \times ( + ) &= ( - ) \\ + 0 \times x &= 0 \\ + ( \pm ) \times x &= ( \pm ), \forall x \ne 0 \\ +\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} + +\subsection{Intervals} + +Something about intervals. + +\subsection{Zones} \label{subsec:zones} + +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. + +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$). + +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} + +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}). + +\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} +$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 +the special \emph{start control-point}. + +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} +\end{align} + +In the first equation, the possible abstract states of the start node +must always be the completely unconstrained abstract domain. Any value +is possible for any variable on the first node of the CFG. + +The second equation requires that the possible abstract states of a +node, $v$, contains either the same amount of information or less +information than each of the predecessors of $v$ in the CFG. + +\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] (V) {$v$}; + \node[main node] (U) [above left of=V] {$u$}; + \node[main node] (W) [above right of=V] {$w$}; + + \path[every node/.style={fill=none}] + (U) edge node[left]{$s_{(u,v)}$} (V) + (W) edge node[right]{$s_{(w,v)}$} (V); + + \end{tikzpicture} + \caption{A simple CFG fragment.} + \label{cfg:confluence} +\end{figure} + +So, if we have the CFG fragment shown in Figure \ref{cfg:confluence} +then we know that $V^\#[v]$ must `contain', or be larger than, each of +the edges coming in to $v$. In this case there are two incoming edges +to $v$: $(u,v)$ and $(w,v)$. + +The edge $(u,v)$ leads to the state $\llb s_{(u,v)} \rrb^\# +(V^\#[u])$y. It is clear that $V^\#[v]$ must be either the same size +or `larger' than this value, as it must either equal this constraint +or it must be a looser constraint. This gives us the inequality +\eqref{eqn:confluence}: $V^\#[v] \ge \llb s_{(u,v)}^\# \rrb +(V^\#[u])$. + +Similarly by considering the edge $(w,v)$ and following the same argument +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 +\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 `lifting' the +statement's effects in the abstract domain with our abstraction and +concretization functions. + +\begin{example} + \label{example:partial-ordered-construction} + + As an example, let us consider the following program: + + \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 + \ref{example:partial-ordered-construction}} + \label{fig:partial-ordered-construction} + \end{figure} + + This corresponds to the CFG presented in Figure + \ref{fig:partial-ordered-construction}. + + We will now attempt to derive a system of inequalities from this for + the \emph{upper bound} of $x$: + \begin{align*} + ub(x) &= v \in \CZ \text{ such that } x \le v & \forall x \in \Z + \end{align*} + + 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 + value in $\CZ$, which is $\infty$. This gives us the following + inequality for node $A$: + \begin{align*} + ub(x_A) &\ge \infty + \end{align*} + + When we reach $B$ we have two incoming edges. One comes from $B$ + 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$. + + 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 + $x$. It also is executed conditionally (when $x \le 99$), which will + affect the bound on $x$. Because the condition limits the growth of + $x$ the corresponding equation for this edge is $ub(x_B) \ge + \min(x, 99) + 1$. + + This leaves us with two simultaneous constraints on the value of + $ub(x_B)$. + \begin{align*} + ub(x_B) &\ge 1 \\ + ub(x_B) &\ge \min(ub(x_B), 99) + 1 + \end{align*} + + The upper bound on the value of $x$ for node $C$ is the same as the + upper bound on the value of $x$ in $B$, because the edge from $B$ to + $C$ does not change the value of $x$, nor does it provide any more + details about the upper bound of $x$. (It does change the lower + bound of $x$, but we have not considered the lower bound in this + analysis.) This gives us a very simple equation system for $C$. + \begin{align*} + ub(x_C) &\ge ub(x_B) + \end{align*} + + So, the upper bounds for $x$ can be found at every program point in + our original program by finding the smallest values of $x_A, x_B, + x_C$ subject to these constraints: + \begin{align*} + ub(x_A) &\ge \infty \\ + ub(x_B) &\ge 1 \\ + ub(x_B) &\ge \min(ub(x_B), 99) + 1 \\ + ub(x_C) &\ge ub(x_B) + \end{align*} + +\end{example} + + +\subsubsection{Lattice construction} + +The partial-ordering formulation considered above is a helpful +presentation of the problem in terms of constraints, but an equivalent +system can be constructed to aid us in locating the \emph{least} +solution to the system. + +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: +\begin{align*} + x \le y ~&\iff~ x \vee y = y \\ + x \le y ~&\iff~ x \land y = x +\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: +\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) +\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} + +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{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*} + +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. + +Now, on to $B \to B$. + +\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*} + + + + +\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*} + +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} + + + + +\subsection{Example solve} +\label{sec-1-3-5} + + +Reconsidering our earlier equation system, we will now attempt to find +the minimal fixpoint by means of \emph{policy iteration} and +\emph{fixpoint iteration}. + +\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 \}$. + +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. + +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. + +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$. + -- cgit v1.2.3