example.tex

\section{Motivating Example}

\begin{figure}[t]
\centering
\begin{tabular}{c|c|c}
\hline
C program & Control-Flow Graph & Abstract Conflict Graph \\
\hline
\scriptsize
\begin{lstlisting}[mathescape=true,language=C]
void foo(int v, 
         _Bool c) 
{
  assume(v>=0 &&
         v<=N);
  int x; 
  if(c)
    x = v;
  else 
    x = -v;
  int z = x * x;
  assert(z>=0);
}
\end{lstlisting}
&
\begin{minipage}{3.7cm}
\centering
%\vspace*{0.3cm}
\scalebox{.52}{\import{figures/}{example.pspdftex}}
%\caption{A control flow graph for P, P' and abstract conflict graph (ACFG) \label{fig:filter}}
\end{minipage}
&
\begin{minipage}{5.6cm}
\centering
\vspace*{0.3cm}
\scalebox{.5}{\import{figures/}{acdl_run.pspdftex}}
%\caption{A control flow graph for P, P' and abstract conflict graph (ACFG) \label{fig:filter}}
\end{minipage}
\\
\hline
\end{tabular}
\caption{\label{fig:example}
C Program, Control-flow Graph (CFG) and Abstract Conflict Graph}
\end{figure}

Consider the simple program in Figure~\ref{fig:example}, which
squares a machine integer and checks that the result is always positive.  To
avoid overflow, we assume that the input $v$ has an upper bound~$N$.  The
control-flow graph is given in the middle column of
Figure~\ref{fig:example}.  We apply three different analysis techniques:
1)~{\em abstract interpretation},
2)~{\em bounded model checking (BMC)} and
3)~{\em ACDCL}.

A standard forward interval analysis is too imprecise to verify the safety
of the program.  The imprecision is owed to the control-flow join at
node~$n4$.  A state-of-the-art abstract interpretation tool,
Astr{\'e}e~\cite{se2011}, requires external hints, provided by manually
annotating the code with partition directives at $n1$, to prove safety using
intervals.  The partition directive tells the tool to analyse each program
execution path separately.  Alternatively, Astr{\'e}e can show safety
using a relational domain such as octagons.
%
\Omit { In general, the imprecision is either intended by the tool because such
high precision analysis is normally not required for runtime error analysis
or the imprecision is unavoidable due to the complexity of the application
under analysis.
}

\begin{table}[!b]
\begin{center}
{
\begin{tabular}{l|r|r|r|r|r}
\hline
Solver & decisions & propagations & conflicts & conflict literals & restarts \\ \hline
MiniSat & 233 & 36436 & 162 & 2604 & 2 \\ \hline
ACDCL (Interval) & 1 & 17 & 1 & 1 & 0 \\ \hline
ACDCL (Octagons) & 0 & 7 & 0 & 0 & 0 \\ 
\hline
\end{tabular}
}
\end{center}
\caption{Solver statistics for Example given in Fig.~\ref{fig:example}}
\label{solver}
\end{table}

BMC converts the program into a bit-vector equation and passes that to a
CDCL-based SAT solver.  We will contrast the analysis performed by CDCL with
that of ACDCL.  The right-hand side of Figure~\ref{fig:example} illustrates
an analysis using ACDCL with the octagon domain (top) and the interval
domain (bottom). The analysis associates an abstract element with each
control location.  The octagons deduced by ACDCL are sufficient
to prove safety without any decision or clause learning, as in the case of
Astr{\'e}e.

The benefit of ACDCL on this example becomes apparent using the interval
domain.  The intervals generated by forward analysis in the initial
deduction phase are $\langle x:[-5,5], z:[-25,25] \rangle$.  Clearly, these
do not prove safety.  Hence, ACDCL makes a heuristic decision to refine the
analysis.  Assume we decide that $c$ is $[1,1]$.  Using deduction, ACDCL
determines that the interval of $x$ is then constrained to $[0,5]$.  The
deductions made during fixed-point iteration are represented by an abstract
conflict graph, given in right-hand side of Figure~\ref{fig:example}.  Nodes
in the abstract conflict graph denote updates to the program variables in
the CFG.  The interval analysis concludes that $(\text{Error}:\bot)$, that
is, the decision $c:=[1,1]$ leads to a {\em conflict}.  Thus, the program is
{\em safe} for the case $c:=[1,1]$.
%
At this point, a clause learning propositional SAT solver learns a reason
for the conflict and then backtracks to a level such that the learnt clause
is \emph{unit}.  Similarly, ACDCL learns that $c:=[0,0]$ at node $n0$, that
is, all error traces must satisfy $c \neq 1$ at node~$n0$.  The analysis
discards all interval constraints that lead to the conflict and backtracks
to decision level~0.  ACDCL then performs interval analysis with the learnt
constraint $(c \neq 1)$, which also leads to a conflict, as shown on 
right-hand side of Figure~\ref{ssa}.  The analysis cannot backtrack further
and therefore terminates, proving that the program is safe.  Thus,
decision and clause learning are used to avoid case-based reasoning and
prevent enumeration behaviour.
   
Table~\ref{solver} compares statistics for the MiniSat~\cite{minisat}
solver for $N=46000$ for the analysis using BMC, and the analysis using
ACDCL with the interval and octagon domains.  Compared to the propositional
SAT solver, there is a significant reduction in the number of decisions,
propagations, learnt clauses and restarts.  Compared to abstract
interpretation, ACDCL does not require external hints to prove the program,
thus automatically performing program and property-driven trace partitioning
to generate proofs using heuristic decisions and clause learning.