path: root/tex/thesis/implementation/implementation.tex

\chapter{Implementation} \label{chap:implementation}

Our implementation of the Demand Driven Strategy Improvement algorithm
presented in Chapter \ref{chap:contribution} is in C++. We chose to
develop it in C++ for two major reasons:
\begin{itemize}
\item
  C++ provides a programmer with fine-grained control of resources, in
  particular memory.
\item
  The LLVM/Clang framework is written in C++. As integration with
  LLVM/Clang was always a major goal for this project, C++ was the
  obvious choice of language.
\end{itemize}


\section{Solver}

The solver is a straightforward implementation of the algorithm
presented in Chapter \ref{chap:contribution}. The primary difference
is the use of objects instead of higher-order functions, as C++'s
support for higher-order functions was insufficient for our purposes.

The solver was developed using only the Standard Template
Library~\cite{stl} for the core of the solver. A front-end was
developed using the ANTLR parser generator \cite{antlr} to test the
solver without the equation system generation of the clang framework.

A high level overview of the implementation is presented in Figure
\ref{fig:solver-arch}. The strategy iteration and fixpoint iteration
loops provide feedback to each other about which values have changed
at each iteration, continuing until the strategy stabilises.

\begin{figure}
  \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
      distance=4cm,main node/.style={rectangle,draw,minimum
        height=2cm,minimum width=3cm}]

    \node[main node] (maximiser) {Strategy iteration};
    \node[main node] (minimiser) [below of=maximiser] {Fixpoint iteration};
    \node (input) [node distance=5cm,left of=maximiser] {\emph{input}};
    \node (output) [node distance=5cm,right of=minimiser] {\emph{output}};

    \path []
    (input) edge node {Equation system} (maximiser)
    (maximiser) edge [bend left] node {Improved strategy} (minimiser)
    (minimiser) edge [bend left] node [align=center]{Greatest fixpoint \\ of strategy} (maximiser)
    (minimiser) edge node [align=center] {Least fixpoint \\ of system} (output)
    ;

  \end{tikzpicture}
  \caption{A very high level overview of the solver implementation.}
  \label{fig:solver-arch}
\end{figure}

In the following subsections we provide some timings for two general
classes of equation systems. Each of the equation systems consists
solely of inexpensive operations, either a variable lookup or a
constant term, so we are comparing only the effect of the algorithms
without consideration of the expense of calculating subexpressions.

All these measurements were performed on a Core 2 Duo E8400 with 4GB
of memory running Debian sid. Binaries were compiled with GCC 4.7.2
with the -O3 flag. The source code for the solver is available
online~\cite{bitbucket-repo}.

\subsection{Chain}

Our first class of example equation systems is a chain. These equation
systems have the following form:
\begin{align*}
  x_0 &= \max(-inf, 0) \\
  x_1 &= \max(-inf, x_0) \\
  ... &~ ... \\
  x_n &= \max(-inf, x_{n-1})
\end{align*}

This particular class of equation system is the simplest of the class
of equations with acyclic dependency graphs. In this particular case
our solver significantly outperforms the naive algorithm for most
problem sizes. For equation systems of less than four variables the
naive approach is slightly faster, but this is of no real practical
concern as in both cases it takes less than a millisecond to provide a
result.

\begin{figure}
  \begin{tikzpicture}
    \begin{loglogaxis}[% 
        scale only axis,
        width=0.7\textwidth,
        height=10cm,
        xmin=1, xmax=65536,
        xlabel=size of equation system,
        ymin=0, ymax=250,
        ylabel=time (in seconds),
        axis on top,
        legend entries={DSI, Naive}]

      \addplot coordinates{ 
        (1,0.000018267)
        (2,0.000042359)
        (4,0.000077031)
        (8,0.000155439)
        (16,0.000308687)
        (32,0.000570927)
        (64,0.001190886)
        (128,0.002441834)
        (256,0.004609652)
        (512,0.009588408)
        (1024,0.018226228)
        (2048,0.036292838)
        (4096,0.076125736)
        (8192,0.152150204)
        (16384,0.307867610)
        (32768,0.654639048)
        (65536,1.190741627)
      };

      \addplot coordinates{ 
        (1,0.000012504 )
        (2,0.000021558 )
        (4,0.000060316 )
        (8,0.000276887 )
        (16,0.001414449 )
        (32,0.009278044 )
        (64,0.067620090 )
        (128,0.508776074 )
        (256,3.939142736 )
        (512,31.373059038 )
        (1024,246.603110160 )
      };

    \end{loglogaxis}
  \end{tikzpicture}
  \caption{Chart comparing the performance of our DSI algorithm
    compared to a naive approach on simple chain examples. Note that
    both axes are logarithmic.}
  \label{fig:solver-chain}
\end{figure}


\subsection{Cycle}

The next class of equation system we will consider will be long
\emph{cycles}. These will 
\begin{align*}
  x_0 &= \max(-inf, 0, x_n) \\
  x_1 &= \max(-inf, x_0) \\
  ... &~ ... \\
  x_n &= \max(-inf, x_{n-1})
\end{align*}

Our dependency graph is no longer acyclic, so finding the value of any
one variable requires the evaluation, and potential strategy
improvement, of all other values. The chart in Figure
\ref{fig:solver-cycle} shows the running time of the DSI algorithm
again, showing that the addition of an acyclic dependency does not
have a significant effect.


\begin{figure}
  \begin{tikzpicture}
    \begin{loglogaxis}[% 
        scale only axis,
        width=0.7\textwidth,
        height=10cm,
        xmin=1, xmax=65536,
        xlabel=size of equation system,
        ymin=0, ymax=250,
        ylabel=time (in seconds),
        axis on top,
        legend entries={DSI, Naive}]

      \addplot coordinates{ 
        (1,0.000016665)
        (2,0.000044187)
        (4,0.000081627)
        (8,0.000159545)
        (16,0.000309742)
        (32,0.000627197)
        (64,0.001236493)
        (128,0.002338711)
        (256,0.004967883)
        (512,0.009164379)
        (1024,0.018700068)
        (2048,0.041385796)
        (4096,0.073920841)
        (8192,0.150712424)
        (16384,0.302473783)
        (32768,0.665616132)
        (65536,1.220667681)
      };

      \addplot coordinates{ 
        (1,0.000012877 )
        (2,0.000021507 )
        (4,0.000059573 )
        (8,0.000252723 )
        (16,0.001419862 )
        (32,0.009221822 )
        (64,0.067315559 )
        (128,0.500673679 )
        (256,3.912675638 )
        (512,31.750177791 )
        (1024,249.912189424 )
      };

    \end{loglogaxis}
  \end{tikzpicture}
  \caption{Chart comparing the performance of our DSI algorithm
    compared to a naive approach on simple cyclical examples. Note
    that both axes are logarithmic.}
  \label{fig:solver-cycle}
\end{figure}




\section{LLVM/Clang}

We implemented our analysis as a Clang Static Analysis pass, building
off the Clang Static Analysis framework~\cite{clang-analysis}. Using
the infrastructure of the Clang project provided us with a CFG without
any extra work parsing, or otherwise handling, C code itself.

Figure \ref{fig:clang-diagram} gives a very high-level idea of the
structure of our analysis pass and how it interfaces with other
components. The Clang framework provides the Zone analysis with a
Control Flow Graph. This CFG is then translated to a system of
monotonic, expansive equations. The DSI algorithm is designed to solve
these equation systems, and so we invoke our solver to provide us with
a solution. This solution identifies the bounds for variables at
different points in the program.

\begin{figure}[tbphH]
  \begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
      distance=4cm,main node/.style={rectangle,draw,minimum
        height=2cm,minimum width=3cm}]
    
    %\node[main node] (clang) {Clang Framework};
    \node[main node] (clang-analysis) {Clang Static Analysis Framework};
    \node[main node,fill=red!60] (eqns) [below of=clang-analysis]
         {Zone analysis};
    \node[main node] (dsi) [below of=eqns] {DSI};
    \node (input) [node distance=7cm,left of=clang-analysis] {\emph{input}};
    \node (reality) [node distance=5cm,right of=eqns] {\emph{output}};

    \path []
    %(clang) edge[bend right] node[anchor=east] {CFG} (clang-analysis)
    (input) edge node {Source code} (clang-analysis)
    (clang-analysis) edge node[anchor=east] {CFG} (eqns)
    (eqns) edge[bend right] node[anchor=east] {Equation System} (dsi)
    (dsi) edge[bend right] node[anchor=west] {Solution} (eqns)
    (eqns) edge node[anchor=north] {Variable bounds} (reality)
    %(eqns) edge[bend right] node[anchor=west] {Variable bounds} (clang-analysis)
    %(clang-analysis) edge[bend right] node[anchor=west] {Errors/warnings} (clang)
    ;

  \end{tikzpicture}
  \caption{High-level diagram of our analysis pass}
  \label{fig:clang-diagram}
\end{figure}


In the sections which follow we present the results of evaluating our
analysis pass on several small programs. The full output from our tool
is provided in Appendix~\ref{appendix:tool-output}, but a condensed
form of the equation systems and variable bounds is presented here. In
the following equation systems we use $MCF\{G\}$ to denote the minimum
cost flow through the flow network $G$.

\pagebreak
\subsection{Counter}
\lstinputlisting{implementation/experiments/counter.c}

This program is extremely simple, consisting only of incrementing a
variable repeatedly in a loop. It is possible to gain a precise result
from a widening and narrowing on this function, so we also achieve a
precise result with this approach.

Since we only have a single variable, we only wish to determine the
bounds on $i$ and $-i$. Thus, we have the following equation system:
\begin{align*}
  ub(i)_A &= \infty \\
  -lb(i)_A &= \infty \\
  ub(i)_B &= \max(-\infty, 0,
  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
    distance=2cm]
    \node (i)[draw,circle] {$1$};
    \node (dummy)[draw,circle,right of=i] {$-1$};
    \path [use as bounding box] (0,0) rectangle (0.5,1);
    \path
    (i) edge[->,bend left] node {$\min(ub(i)_B, 99)$} (dummy)
    (dummy) edge[->,bend left] node {$-lb(i)_B$} (i);
  \end{tikzpicture}\right\} + 1) \\
%
  -lb(i)_B &= \max(-\infty, 0,
  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
    distance=2cm]
    \node (i)[draw,circle] {$-1$};
    \node (dummy)[draw,circle,right of=i] {$1$};
    \path [use as bounding box] (0,0) rectangle (0.5,1);
    \path
    (i) edge[->,bend left] node {$\min(ub(i)_B, 99)$} (dummy)
    (dummy) edge[->,bend left] node {$-lb(i)_B$} (i);
  \end{tikzpicture}\right\} - 1) \\
%
%
  ub(i)_C &= \max(-\infty,
  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
    distance=2.5cm]
    \node (i)[draw,circle] {$1$};
    \node (dummy)[draw,circle,right of=i] {$-1$};
    \path [use as bounding box] (0,0) rectangle (0.75,1.25);
    \path
    (i) edge[->,bend left] node {$ub(i)_B$} (dummy)
    (dummy) edge[->,bend left] node {$\min(-lb(i)_B, -100)$} (i);
  \end{tikzpicture}\right\}) \\
%
  -lb(i)_C &= \max(-\infty,
  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
    distance=2.5cm]
    \node (i)[draw,circle] {$-1$};
    \node (dummy)[draw,circle,right of=i] {$1$};
    \path [use as bounding box] (0,0) rectangle (0.75,1.25);
    \path
    (i) edge[->,bend left] node {$ub(i)_B$} (dummy)
    (dummy) edge[->,bend left] node {$\min(-lb(i)_B, -100)$} (i);
  \end{tikzpicture}\right\})
\end{align*}

Solving this system of equations gives us the following bounds on $i$:
\\
\begin{center}
  \begin{tabular}{c|cc}
    Block & ub(i) & lb(i) \\
    \hline 
    A & $\infty$ & $-\infty$ \\
    B & $100$ & $0$ \\
    C & $100$ & $-100$
  \end{tabular}
\end{center}

This is a precise analysis of the values of $i$, performed without
widening/narrowing. It captures the possible values of $i$ precisely
and identifies the value of $i$ at the exit of the loop.

\pagebreak
\subsection{Double counting}
\lstinputlisting{implementation/experiments/example.c}

In this example we are incrementing two different program variables at
the same time, based on a condition of one of the variables. In
standard interval analysis it is impossible to capture the
relationship between these variables, but by performing abstract
interpretation over zones we can perform a more precise analysis.

This example is a translation to C of the example presented by
Gawlitza et al.~\cite{EasyChair:117}. In our abstract analysis we will
consider the values $x1$, $x2$ and $x2 - x1$.

\begin{align*}
  ub(x1)_A &= \infty \\
  ub(x2)_A &= \infty \\
  ub(x2 - x1)_A &= \infty \\
%
  ub(x1)_B &= \max(-\infty, 0,
  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
        distance=2.5cm]
      \node (x1)[draw,circle] {$1$};
      \node (x2)[draw,circle,below of=x1] {$0$};
      \node (dummy)[draw,circle,below right of=x1] {$-1$};
      \path
      (x1) edge[->,bend left] node {$\min(8, ub(x1)_B)$} (dummy)
      (x2) edge[->,bend left] node {$ub(x2)_B$} (x1)
      (x2) edge[->,bend left] node {$ub(x2 - x1)_B$} (dummy);
    \end{tikzpicture}\right\} + 2) \\
  ub(x2)_B &= \max(-\infty, 1,
  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
        distance=2.5cm]
      \node (x1)[draw,circle] {$0$};
      \node (x2)[draw,circle,below of=x1] {$1$};
      \node (dummy)[draw,circle,below right of=x1] {$-1$};
      \path
      (x1) edge[->,bend left] node {$\min(8, ub(x1)_B)$} (dummy)
      (x2) edge[->,bend left] node {$ub(x2)_B$} (x1)
      (x2) edge[->,bend left] node {$ub(x2 - x1)_B$} (dummy);
    \end{tikzpicture}\right\} + 2) \\
  ub(x2 - x1)_B &= \max(-\infty, 1,
  MCF\left\{\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node
        distance=2.5cm]
      \node (x1)[draw,circle] {$-1$};
      \node (x2)[draw,circle,below of=x1] {$1$};
      \node (dummy)[draw,circle,below right of=x1] {$0$};
      \path
      (x1) edge[->,bend left] node {$\min(8, ub(x1)_B)$} (dummy)
      (x2) edge[->,bend left] node {$ub(x2)_B$} (x1)
      (x2) edge[->,bend left] node {$ub(x2 - x1)_B$} (dummy);
    \end{tikzpicture}\right\})  \\
%
%
  ub(x1)_C &= \max(-\infty, ub(x1)_B)  \\
  ub(x2)_C &= \max(-\infty, ub(x2)_B)  \\
  ub(x2 - x1)_C &= \max(-\infty, ub(x2 - x1)_B)
\end{align*}


Solving this system of equations gives us the following bounds on
$x1,x2$ and $x2-x1$:
\\
\begin{center}
  \begin{tabular}{c|ccc}
    Block & ub(x1) & ub(x2) & ub(x2 - x1) \\
    \hline 
    A & $\infty$ & $\infty$ & $\infty$ \\
    B & $10$ & $11$ & $1$ \\
    C & $10$ & $11$ & $1$
  \end{tabular} 
\end{center}

This result is more precise than any that could have been obtained by
interval analysis. We accurately capture the relationship between $x1$
and $x2$ by bounding $x2 - x1 \le 1$, and this allows us to correctly
determine the upper bound of $x2$ at the exit of the loop. The output
of our automatic analysis for this function can be seen in Section
\ref{sec:example-function-output}.