deductions.tex

\section{Abstract Model Search}\label{sec:deduce}
%
\Omit {
\begin{figure}[t]
\scriptsize
\begin{tabular}{l|l|l}
\hline
C program & SSA & Octagon \\
\hline
\begin{lstlisting}[mathescape=true,language=C]
int main() {
 unsigned x, y;
 __CPROVER_assume(x==y);
 x++;
 assert(x==y+1);
}
\end{lstlisting}
&
\begin{minipage}{4.40cm}
$\begin{array}{l@{\,\,}c@{\,\,}l}
SSA &\iff& ((g0 == TRUE) \land \\
    &    & (cond == (x == y)) \land \\
    &    & (g1 == (cond \&\& guard0)) \land \\
    &    & (x' == 1u + x) \land \\
    &    & (x' == 1u + y || !1))
\end{array}$
\end{minipage}
&
\begin{minipage}{3.75cm}
$\begin{array}{l@{\,\,}c@{\,\,}l}
C &\iff& ((x' > 1) \land (-x'-y < -2) \land \\
  &    & (-x-x' < -2) \land (y-x' < 0) \land \\                                                                
  &    & (x-x' < 0) \land (y > 0) \land \\
  &    & (x > 0) \land (-x'-y < 0) \land \\
  &    & (x+y > 1) \land (y-x < 1) \land \\
  &    & (x'-y < 2) \land (x-y < 1) \land \\
  &    & (x+y > 0) \land (x+x' > 0) \land \\
  &    & (x'-x < 2))
\end{array}$
\end{minipage}
\\
\hline
\end{tabular}
\caption{C Program, corresponding SSA and Octagonal Inequalities}
\label{ssa}
\end{figure}
}
%
%    
\begin{algorithm2e}[t]
\DontPrintSemicolon
\SetKw{return}{return}
\SetKwData{sat}{sat}
\SetKwData{conflict}{conflict}
\SetKwData{unsat}{unsat}
\SetKwData{unknown}{unknown}
\SetKwData{true}{true}
\SetKwInOut{Input}{input}
\SetKwInOut{Output}{output}
\SetKwFor{Loop}{Loop}{}{}
\SetKw{KwNot}{not}
\begin{small}
\Input{A program in the form of a set of abstract transformers $\abstransset$,
a propagation trail $\trail$, and a reason trail $\reasons$.}
\Output{\sat or \conflict or \unknown}
$\worklist \leftarrow \initworklist_{\propheur}(\abstransset)$ \;
\While{$!\mathit{worklist.empty}()$} 
{
  $\abstransel{\subdomain} \leftarrow \mathit{worklist.pop}()$ \; 
  $\absval \leftarrow \abstransel{\subdomain}(\abs(\trail))$\;
  \uIf{$\absval = \bot$} {
    $\reasons[\bot] \leftarrow \abstransel{\subdomain}$ \;
    $\mathit{worklist.clear}()$ \;
    \return \conflict \;
  }
  \uElse
  {
    $\newdeductions=\onlynew(\absval)$\;
%    $\newdeductions=\decomp(\absval)\setminus\decomp(\abs(\trail))$\;
    $\trail \leftarrow \trail \cdot \decomp(\newdeductions)$ \; 
    $\reasons[|\trail|] \leftarrow \abstransel{\subdomain}$ \;
    $\updateworklist_{\propheur}(\worklist, \newdeductions, \abstransel{\subdomain},  \abstransset)$ \; 
  }
}
\lIf{$\abstransset$ is $\gamma$-complete at $\abs(\trail)$} {
  \return \sat \;
}
 \return \unknown \;

\end{small}
\caption{Abstract Model Search $\mathit{deduce}_{\propheur}(\abstransset,\trail,\reasons)$ \label{Alg:ms}}
\end{algorithm2e}
%  
A model search procedure in a SAT solver involves two steps -- {\em deductions} 
using the unit rule refines current partial assignments and 
{\em decisions} to heuristically guess a value for an unassigned 
literal.  
%The unit rule overapproximates a model transformer and deduction 
%computes a greatest fixed point over the partial assignments
%domain~\cite{dhk2013-popl}.  We present an abstract model search procedure 
%that computes a greatest fixed point over meet irreducible deduction 
%transformer in $S$.  
%

%-------------------------------------------------------------------------------
\subsection{Abstract Deduction Transformers} \label{sec:abst}
%-------------------------------------------------------------------------------
\Omit{
To make our algorithm efficient, we have to focus the abstract
transformers on performing only the minimally necessary
work. 
}
The key considerations for building an abstract transformer are 
precision and efficiency.  A precise transformer is usually less efficient, 
and vice-versa.  We provide a parameterised abstract transformer that allows us to 
control the precision and efficiency of deductions through the application of 
different propagation heuristics. 
%
We thus define a specialised variant of the abstract transformer to compute
deductions w.r.t.\ a given subdomain $\subdomain\subseteq \domain$,
which we call the \emph{abstract deduction transformer}.
%
A subdomain contains a chosen subset of the elements in $\domain$ including
$\bot$ and $\top$, which forms a lattice.  An abstract 
deduction transformer is formally defined as follows. 
\begin{equation}\label{eq:at2}
\abstrans{\domain}{\constraint}^\subdomain(\absval)=\absval\meet_\domain \alpha_\subdomain(\{\val\mid \val\in\gamma_\domain(\absval), \val\models \constraint\})
\end{equation}
For $\subdomain=\domain$, the abstract deduction transformer is identical 
to the abstract transformer defined in Eq.~(\ref{eq:abstrans})
in Section~\ref{sec:domains}.  We denote $\abstrans{\domain}{\constraint}^\subdomain$
as $\abstransel{\subdomain}$ in Algorithm~\ref{Alg:ms}. 

%We construct the subdomain from a set of variables $\vars$ such that $\subdomain_\domain(\vars)$ is the set of meet irreducibles $\in \domain$ that contain at last one variable in $\vars$ and most one variable that is not in $\vars$. \pscmt{split into two parts}
%
%For example, $\subdomain=\domain[\{y\}]$ being the octagons domain over variables $\{x,y,z\}$ contains all octagonal meet irreducibles involving $\{y\}$, and the pairs $\{x,y\}$ and $\{y,z\}$, but not the meet irreducibles\pscmt{wrong} over $\{x\}$, $\{z\}$ and~$\{x,z\}$.

%The first advantage of this definition is that 
This parameterisation of the abstract deduction transformer with a subdomain 
$\subdomain$ allow us to guide the propagation in {\em forward}, {\em backward} 
or {\em multi-way} direction.
%using our abstract transformers.
%we can control how we perform 
%
Consider an example, where $\absval=(0\leq y \leq 1 \wedge 5\leq z)$, we have
$\abstrans{\intervals[\{x,y,z\}]}{x=y+z}^{\intervals[\{x\}]}(\absval)=\absval\meet(x\geq
6)$. For $x=y+z$, this performs a right-hand side to left-hand side propagation and
hence emulates a forward analysis, whereas
$\abstrans{\intervals[\{x,y,z\}]}{x=y+z}^{\intervals[\{y,z\}]}=\absval\meet\top$
emulates a backward analysis.

We call the propagation with arbitrary subdomains,
e.g. $\subdomain=\domain$, \emph{multi-way propagation}, which is able
to simultaneously perform forward and backward propagation.
%
\Omit{
Note that a restriction to a subdomain makes a transformer less
precise.
}
Note that a restricted subdomain makes a transformer less precise, but more
efficient.  On the contrary, an unrestricted subdomain make a transformer more 
precise, but less efficient. Therefore, we have the property
$\abstrans{\domain}{\constraint}^\domain(\absval)\sqsubseteq
\abstrans{\domain}{\constraint}^\subdomain(\absval)$.
%However, the choice of a subdomain makes the deductions more efficient.
Thus, the choice of a subdomain helps to fine-tune the deductions 
during the propagation phase.

\paragraph {\textbf{Lazy closure computation}} 
Computing closure for relational domains, such as octagons is an 
extremely expensive operation~\cite{pldi15}.  An advantage of our 
formalism in Eq.~(\ref{eq:at2}) is that
%we can compute the
the \emph{closure} operation for relational domains can be computed 
in a lazy manner. To this end, we construct a subdomain 
$\subdomain=\makesubdomain_\domain(\subvars)$ for $\abstransel{\subdomain}$,
which is sufficient to perform one step of the closure operation when 
$\abstransel{\subdomain}$ is applied.
%
For example, let us consider $\domain=\octagons[\{x,y,z\}]$ and
$\subvars=\{y\}$. An octagonal inequality relates at 
most two variables. Thus it is sufficient to consider the subdomain
$\makesubdomain_\domain(\{y\})=\octagons[\{y\}]\cup\octagons[\{x,y\}]\cup\octagons[\{y,z\}]$,
which will compute the one-step transitive relations of~$y$ with each
of the other variables. 
%
Only if a abstract deduction transformer subsequently makes new deductions 
on $x$ or $z$, then the next step of the closure will be computed through 
the subdomain $\octagons[\{x,z\}]$.
\Omit{
Hence, when the abstract deduction transformer is applied we do not
compute the full closure in the full domain,
but we compute only a single step of the closure in a restricted
domain, which makes single deduction steps more efficient.
}
Hence, an application of abstract deduction transformer does not 
compute the full closure in the full domain, but compute only a 
single step of the closure in a restricted domain, which makes each 
deduction step more efficient.  Thus, we delay the closure operation 
until the point where it is absolutely necessary.  This makes our deductions 
in relational domain more efficient.  
%
\Omit{
If $\abstransel{\subdomain}$ deduces new information about $x$ or $z$
then the next step of the closure will be computed by the worklist
mechanism of Algorithm~\ref{Alg:ms} that we describe next.
}
%
 
%If this indeed affects $x$ and~$z$ then their
%relations will be inferred in a later step of the propagation
%algorithm, thus gradually computing the closure. 

%Note that this might
%increase the number of propagation steps, but it reduces the size of
%the subdomain used in the abstract deduction transformer.

%Moreover, we want to know what the reasons for a specific deduction are.
%\[ded(s,a,L)=\{R\rightarrow d\mid R=reasons(s,a,L,d), d \in decomp(\llbracket s \rrbracket^\sharp(a,L))\}\]
%where 
%$reasons(s,a,L,d)=\text{argmin}_{R\in\{R'\mid R'\subseteq decomp(a), \llbracket s\rrbracket^\sharp(R,L)=d\}} |R| $.

%-------------------------------------------------------------------------------
\subsection{Algorithm for Deduction Phase}
%-------------------------------------------------------------------------------
%

Algorithm~\ref{Alg:ms} presents the deduction phase $\deduce$ in 
abstract model search procedure.  The input to the algorithm is 
the set of abstract transformers, a propagation trail and a reason 
trail.  Additionally, the procedure $\deduce$ is parameterised with 
a propagation heuristic ($\propheur$). 
%
The algorithm maintains a  {\em worklist}, which is a queue that contains 
abstract deduction transformers.  The propagation heuristics provides two 
functions $\initworklist$ and $\updateworklist$.
The order of the elements in the worklist and the subdomain $\subdomain$ 
associated with each abstract deduction transformer ($\abstransel{\subdomain}$) 
determine the propagation strategy (forward, backward, multi-way).

The {\em forward} propagation strategy initialises the worklist with
abstract deduction transformers that contain constants in the
right-hand side and the subdomain is constructed via $\makesubdomain_\domain$
from variables in the left-hand side of the equality constraints
originating from the assignment statements in the program.
%
The {\em backward} propagation strategy initialises the worklist 
with the assertions and the subdomain is constructed from the 
right-hand side variables.
%
The {\em multi-way} propagation strategy initialises the worklist 
with the set of all transformers and the corresponding subdomains 
contains the variables occurring in the respective transformers.
%
Depending on the propagation heuristics, $\updateworklist$ adds
abstract deduction transformers to the worklist that contain variables
that appear in $\newdeductions$, and updates the subdomains of
the abstract deduction transformers in the worklist 
to include the variables in $\newdeductions$.
%
The function
$\onlynew(\absval)=\bigsqcap(\decomp(\absval)\setminus\decomp(\abs(\trail)))$
is used to filter out all meet irreducibles that are already on the trail
in order to obtain only new deductions when applying the abstract deduction transformer.
%
\Omit{
If $\bot$ is deduced we return \textsf{conflict}.
Otherwise, when eventually a fixed point has been reached, i.e.\ the worklist is empty, then the abstract value $\abs(\trail)$ is checked whether it is 
$\gamma$-complete~\cite{dhk2013-popl}. 
%
It is $\gamma$-complete if all concrete values in $\gamma(\abs(\trail))$ satisfy $\formula$.
Otherwise, the algorithm returns \textsf{unknown} and ACDCL makes a new decision.}

If $\abstransel{\subdomain}$ deduces $\bot$, then 
the procedure $\mathit{deduce}$ returns \textsf{conflict}.
Otherwise, when a fixed-point is reached, i.e.\ 
the worklist is empty, then we check whether
the abstract transformers $\abstransset$ are $\gamma$-complete~\cite{dhk2013-popl} for the current abstract value $\abs(\trail)$.
%
Intuitively, this means that all concrete values in 
$\gamma(\abs(\trail))$ satisfy $\formula$.  
%
If it is indeed 
$\gamma$-complete, then $\mathit{deduce}$ returns \textsf{sat}.  Otherwise, the 
algorithm returns \textsf{unknown} and ACDCL makes a new decision.