path: root/tex/thesis/litreview/litreview.tex

\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$.