domains.tex

\section{Program Model and Abstract Domain}\label{sec:domains}
This section introduces the program model and identifies properties of abstract
domains that are necessary for learning in abstract lattice structures.
% \subsection{Programs:}
% %
% A {\em program} $\program$ is formally defined as follows.
% \[
% \begin{array}[t]{@{}lll}
% \program & {:}{:}{=} & \mathit{Procedure} \\
% \mathit{Procedure} & {:}{:}{=} & \mathit{Statement} \mid \mathit{Procedure} \\
% \mathit{Statement} & {:}{:}{=} & CStatement \mid \mathit{function(Var_1,\dots,Var_n)} \\
% \mathit{CStatement} & {:}{:}{=} & x {:}{=} exp \mid \mathit{ITE}(b, s_1,s_2) \mid \mathit{s_1;s_2} \mid loop\{s\} \\
% \end{array}
% \]
% Consider sets of expressions $Exp$ and Boolean expressions $BExp$
% over variables $Var$ of $\program$.  The variables in $Var$ 
% can take numeric values in $Val$.  A procedure is denoted as 
% $\mathit{function(Var_1,\dots,Var_n)}$.  A $\mathit{CStatement}$ 
% is an assignment, conditional, sequential concatenation or a loop. \\
% \textbf{Control-flow Graph:} A CFG is a triple $(Loc, E, lbl)$, 
% where $Loc$ is the set of locations with an unique start 
% location $(init)$ and error location $(err)$, $E$ is the set 
% of control-flow edges that are labelled with the set 
% $lbl \in Statement$.  For the purpose of illustration, we 
% assume that all the procedures are inlined.  

%-------------------------------------------------------------------------------
\subsection{Program Representation}  
\Omit {
\begin{wrapfigure}{r}{3cm}
\[
\begin{array}{rcl}
g_0 &=& \true \\
\multicolumn{3}{l}{0 \leq v\leq N} \\
g_1 &=& g_0\wedge c\\
x_0 &=& v \\
x_1 &=& -v \\
x_2 &=& g_1?x_0:x_1 \\
g_2 &=& g_1 \vee g_0\wedge \neg c\\
z &=& x_2 * x_2 \\
\multicolumn{3}{l}{z<0 \wedge g_2}
\end{array}
\]
\caption{\label{fig:ssa}
SSA for the example in Figure~\ref{fig:example}
}
\end{wrapfigure}
}
\begin{figure}[t]
\center
\scriptsize
\begin{tabular}{l|l}
\hline
 SSA & Abstract Conflict Graph \\
\hline
\begin{minipage}{4.50cm}
$\begin{array}{rcl}
\constraints:= (g_0 = (0 \leq v\leq N)) \\
(g_1 = (g_0 \wedge c)) \wedge (x_0 = v) \wedge \\
(x_1 = -v) \wedge (x_2 = g_1?x_0:x_1) \wedge \\
(g_2 = (g_1 \vee g_0\wedge \neg c)) \wedge \\
(z  = x_2 * x_2) \wedge (g_2 \wedge z<0)
\end{array}$
\end{minipage}
&
\begin{minipage}{5.2cm}
\centering
\scalebox{.45}{\import{figures/}{learning.pspdftex}}
\end{minipage}
\\
\hline
\end{tabular}
\caption{SSA and abstract conflict graph}
\label{ssa}
\end{figure}
%
We consider \emph{bounded programs} with safety
properties given as assertions $\assertions$ in the program.
%
A bounded program is obtained by a program transformation that unfolds
loops and recursions a finite number of times. The result of this
transformation is represented by a set
$\constraints=\program\cup\{\neg \bigwedge_{\assertion\in\assertions} \assertion\}$
where $\program$ contains the statements of the transformed program in the
form of constraints as typically obtained by translating the program
into single static assignment (SSA) form via a data flow analysis.
%
Figure~\ref{ssa} gives the SSA constraints for the program in
Figure~\ref{fig:example}.
%
Assignments such as \texttt{x=v;} become equalities $x_1=v$ where the
left-hand side variable gets a fresh name (subscript).
%
Control flow is encoded into guard variables such as $g_1=g_0\wedge c$.
%
Data flow joins become conditional expressions, e.g.\ $x_3=g_1?x_1:x_2$.
%
The assertions $\assertions$ are constraints of the form $g_3
\Rightarrow z\geq 0$, for instance, meaning that if $g_3$ holds
(i.e.\ the assertion is reachable) then the assertion must hold.
%
We~denote $\vars$ the set of variables occurring in $\constraints$.  
Based on the above program representation, we define a safety equation as, 
$\formula:= \bigwedge_{\constraint\in\constraints} \constraint$. The formula $\formula$ is 
unsatisfiable if and only if the program is safe.
%
%
%For example, figure~\ref{swssa} presents the program analysis constraints for 
%a C program in Static Single Assignment (SSA) form.  

% \subsection{Concrete Semantics}
% \pscmt{not sure that adds anything for TACAS}
% The {\em concrete} domain is a lattice 
% of concrete environments, $Env = Var \rightarrow Val$, and is 
% defined by $CDom = (Env, \sle_{C}, \join_{C}, \meet_{C})$.
% A transformer, $post_{stmt}$, of concrete domain defines 
% the effect of a statement $stmt$ on the concrete domain, 
% $post_{stmt} : \powerset(Env) \rightarrow \powerset(Env)$.  
% 
% A state in concrete domain is a tuple $\langle l, \sigma \rangle$, 
% where $l$ is a location and $\sigma \in Env$.  A trace is a sequence 
% of states $(l_0, \sigma_0), \ldots (l_n, \sigma_n)$ such that for all 
% $0 \leq i \leq n$, there exists a cfg egde $(l_{i}, l_{i+1})$ 
% if $\sigma_{i+1} \in post_{i}(\sigma_{i})$. 

%-------------------------------------------------------------------------------
%\paragraph{Safety problem}  
%

% \subsection{Static Analysis Equations for Safety}
% Static program analysis based on abstract interpretation~\cite{DBLP:conf/emsoft/Cousot07} 
% perform safety analysis by computing fixed point to infer invariants 
% over program variables.  However, bounded model checking (BMC) tries to search 
% for a counterexample in a bounded execution trace, by symbolically executing a 
% program up to a finite bound.  
% Similar to BMC, ACDCL searches for a counterexample by solving the formula shown below.
% For a set $N$ of program analysis constraints defined over a set 
% of constraint variables $Var = \{X_i| i \in N\}$, representing a program
% $\program$ and a concrete domain $\powerset(Env)$, the static analysis equation 
% for safety of $\program$ is given as follows.  Here, $X_{init}, X_{Err}$ denote the initial valuation 
% and the \rmcmt{final valuation} of constraint variables.
% \[\formula = X_{init} \subseteq Env \wedge \underset{p,q \in |\program|}
% {\bigwedge} \{ X_p \subseteq post_{(p,q)}(X_q) \} \wedge X_{err} \supset \emptyset \] 

%-------------------------------------------------------------------------------
\subsection{Abstract Domain}
%-------------------------------------------------------------------------------
SAT solvers operate on partial assignment domains~\cite{sas12,dhk2013-popl}.  
We present an instantiation of ACDCL as program analyser that uses relational
domains.  
% 
%In our prototype implementation and for illustrative purposes 
In this paper we use a product domain $\domain[\vars]=\booldomain^{|\boolvars|}\times\reldomain[\numvars]$ where
$\booldomain$ is the Boolean domain
$\langle\{\true,\false,\bot,\top\},\Rightarrow,\wedge,\vee\rangle$, 
$\boolvars$ are the Boolean variables in the program, 
and $\reldomain$ is a \emph{relational} domain over the 
numerical (bitvector) variables $\numvars$ of their respective
data types (currently, signed and unsigned integers are supported).
%
We instantiate $\reldomain$ with the template polyhedra domain~\cite{sriram}.

For notational convenience we will denote elements of
$\booldomain^{|\boolvars|}$ by their concretisations to propositional formulae.  
For example, the program in Figure~\ref{ssa} has four Boolean variables
written as the vector $(g_0,g_1,c,g_2)$. Thus, we will denote an abstract 
value $(\top, \false, \true, \top) \in \booldomain^4$ as $\neg g_1 \wedge c$.

%-------------------------------------------------------------------------------
\paragraph{\textbf{Template Polyhedra Abstract Domain}}
%
An abstract value of the template polyhedra domain~\cite{sriram}
represents a set $\numconcval$ of values of the vector $\vec{\numvar}$ of numerical variables $\numvars$. For
example, in the program in Figure~\ref{ssa}, we have four numerical
variables, written as the vector $\vec{\numvar}:=(x_0,x_1,x_2,z)$.  We can
represent sets of values for $\vec{\numvar}$ such that
$\mat{C}\vec{\numvar}\leq\vec{\numabsval}$ for a fixed coefficient matrix $\mat{C}$
and a constant vector $\vec{\numabsval}$. The domain of $\vec{\numabsval}$ is augmented
by a special element $\bot$ to denote the minimal element of the
lattice.
%
The abstraction function is defined as $\alpha(\numconcval) = \min \{\vec{\numabsval}\mid
\mat{C}\vec{\numvar}\leq\vec{\numabsval}, \vec{\numvar}\in \numconcval\}$ where $\min$ is applied
component-wise. There are several optimisation-based
techniques~\cite{sriram,GS07b,BJKS15} for computing the domain
operations, such as meet ($\meet$), join ($\sqcup$), etc in the template
polyhedra domain. In our implementation, we use the strategy 
iteration approach available in 2LS~\cite{BJKS15}.
%
The concretisation $\gamma(\vec{\numabsval})$ is the set $\{\vec{\numvar}\mid
\mat{C}\vec{\numvar}\leq\vec{\numabsval}\}$; $\gamma(\bot)=\emptyset$, i.e.\ the empty polyhedron.
%
For notational convenience we will use conjunctions of linear
inequalities, e.g.\ $x_1\geq 0 \wedge x_1-z\leq 30$ to denote the
abstract value $\vec{\numabsval}=\vecv{0}{30}$ of the template polyhedra domain
with $\mat{C}=\qmat{-1}{0}{1}{-1}$ and $\vec{\numvar}=\vecv{x_1}{z}$;
$\true$ is $\top$ and $\false$ is $\bot$.  Template polyhedra can
express other domains, such as interval and octagon domains.

% \paragraph{Interval Abstract Domain} 
% The {\em Interval} abstract domain is a lattice 
% $ItvDom = (ItvElm, \sle_{I}, \join_{I}, \meet_{I})$, where
% $ItvElm: (Var \rightarrow Itv) \cup \{\bot\}$, and $Itv$ is 
% the set of intervals of type $[l,u]$ over numeric data 
% type with $l \leq u$. The least element is $\bot$ and the 
% greatest element is $\top$ which maps all variables to their
% minimum ($min$) and maximum ($max$) values.  An interval 
% $\langle x, [min, v] \rangle$ is written as $x \leq v$.  The 
% partial order $\sle_{I}$ over elements in the set $Itv$ is 
% given by $I_1 \sle_{I} I_2$ if $I_2$ contains $I_1$.
% A join $(\join_{I})$ of two intervals $\langle x_1 \rightarrow [l_1, u_1], 
% x_1 \rightarrow [l_2, u_2] \rangle$ is an interval 
% $\langle x_1 \rightarrow [min(l_1, l_2), max(u_1, u_2)]$.
% A meet $(\meet_{I})$ of two intervals $\langle x_1 \rightarrow [l_1, u_1], 
% x_1 \rightarrow [l_2, u_2] \rangle$ is an interval 
% $\langle x_1 \rightarrow [max(l_1, l_2), min(u_1, u_2)] \rangle$.
% The galois connection between the concrete environment and intervals is 
% given as follows.
% \[\alpha(x) = \{[inf(x), sup(x)] | x \in Var\} \qquad   \alpha(\emptyset) = \bot \]
% \[\gamma[p,q] = \{c \in \mathbb{Z} | p \leq c \leq q\} \qquad \gamma(\bot) = \emptyset \]
%
\begin{wrapfigure}{r}{4.5cm}
\vspace*{-7ex}
\scalebox{.65}{\import{figures/}{octagons.pspdftex}}
\caption{Example of an octagon}\label{octagon}
\vspace*{-5ex}
\end{wrapfigure} 
%
%In the interval domain $\intervals[\numvars]$,
For a program with $N=|\numvars|$ variables, 
the matrix $\mat{C}$ for the interval domain 
$\intervals[\numvars]$, has $2N$ rows. Hence, it 
generates at most $2N$ inequalities, one
for the upper and lower bounds of each variable.
%
For octagons $\octagons[\numvars]$, we have at most $2N^2$
inequalities, one for the upper and lower bounds of each variable and
sums and differences for each pair of variables. Figure~\ref{octagon}
gives an example of an octagon and its associated inequalities.
\Omit{
The interval domain is a non-relational domain because a single
inequality only contains a single variable.  The octagon domain, 
however, is relational.  
}
%
A~fundamental difference between relational and 
non-relational domains is that the relational
domains require the computation of a \emph{closure} 
in order to obtain a normal form that is usually required for precise 
%and efficient 
domain operations.  An example of a closure computation for octagonal 
inequalities is given by
$\mathit{closure}((x-y \leq 4) \wedge (y-z \leq 5))=((x-y \leq 4) \wedge (y-z
\leq 5) \wedge (x-z \leq 9))$.
%below.
%\[\mathit{closure}((x-y \leq 4) \wedge (y-z \leq 5))=((x-y \leq 4) \wedge (y-z \leq 5) \wedge (x-z \leq 9)) \]  
%
The closure computes all implied domain constraints.  For octagons,
closure is the most critical and expensive operator (cubic complexity in the
number of program variables)~\cite{pldi15}.
%
%We will see that our model search algorithm performs closure computations lazily,
%postponing them to the point where they are actually necessary.\rmcmt{are we
%showing this ?}

% \paragraph{Octagon Abstract Domain} \pscmt{TODO: simplify}
% The {\em Octagon} abstract domain is a lattice 
% $OctDom = (OctElm, \sle_{O}, \join_{O}, \meet_{O})$, where
% $OctElm: (Var \times Var \rightarrow (\mathbb{R} \cup \{\infty\})) \cup \bot$. 
% The least element is $\bot$ that contains all unsatisfiable 
% set of inequalities and the greatest element is $\top$ which 
% maps the bounds of all octagonal inequalities to $\infty$. 
% The partial order $\sle_{O}$ over elements in the set $OctElm$ is 
% given by $O_1 \sle_{O} O_2$ iff the bounds of each inequalities in $0_1$ 
% is included (by $\leq$ order) in the bounds of corresponding inequalities 
% in $O_2$, that is, the octagons are ordered by the inclusion relations.

% The join $(\join_{O})$ of two octagons, $\langle (v_i \times v_j \rightarrow N_1),
% (v_i \times v_j \rightarrow N_2) \rangle$, is not necessarily an octagon 
% and is computed by taking piece-wise maximum of bounds of corresponding 
% octagonal inequalities, $\langle (v_i \times v_j \rightarrow max(N_1, N_2) \rangle$.
% However, the meet $(\meet_{O})$ of two octagons, $\langle (v_i \times v_j \rightarrow N_1),
% (v_i \times v_j \rightarrow N_2) \rangle$, is always an octagon and is 
% computed by taking piece-wise minimum of bounds of corresponding 
% octagonal inequalities, $\langle (v_i \times v_j \rightarrow min(N_1, N_2)$.  A closed 
% octagon is the smallest octagon following the partial order $\sle_{O}$, among all 
% the octagons that abstract the same concrete values.

% The octagon domain is a relational abstract domain that permits $2n^2$ 
% linear inequalities between $n$ program variables.  The octagonal 
% inequalities are of two types: binary or unary inequalities as shown below.
% \[Binary: \pm v_i \pm v_j \leq a, v_i \neq v_j \qquad Unary: v_i \leq b, \{a, b\} \in \mathbb{R} \cup \infty \]  
% An element in octagon domain, $OctElm$, is a conjunction of such 
% inequalities and is called an octagon.  
%
% For building program analyzers using octagon domains, the domain also 
% provides few operators like {\em widening ($\nabla$)} and {\em closure ($*$)}.  
% The widening operator is used to accelerate convergence for loops in the program
% and has a quadratic complexity in the number of variables.  If the bound of an 
% octagonal inequality increases every iteration, then $\nabla$ sets the bounds 
% to $\infty$.  However, the closure operator is often used to reduce the degree 
% of over-approximation resulting from the join operation. 

% \begin{definition}{(Abstract Valuation)} An {\em abstract valuation} is a
% mapping of variables to an element of abstract domain, for example 
% a mapping of variable $x$ to an interval environment is given by 
% $\langle x \mapsto [2,5] \rangle$ or a mapping of $\{x,y\}$ to octagon 
% environment is given by $\langle x-y \mapsto 0, y-x \mapsto 0 \rangle$.  
% An abstract valuation is {\em atomic} if each variable is mapped to a singleton 
% value or to $\bot$.  
% \end{definition}

%-------------------------------------------------------------------------------
\paragraph{\textbf{Abstract Transformers}}
%
%In a typical abstract interpretation based Galois-connection setting
%over an over-approximate domain, every concrete element has a unique
%over-approximate representation in the abstract.  Likewise, every
%concrete transformer is over-approximated by a unique abstract
%transformer.  We now define an abstract deduction transformer.
%
An abstract transformer $\abstrans{\domain}{\constraint}$ transforms an abstract value $\absval$ through a
constraint $\constraint$, i.e., it \emph{deduces} information from $\absval$ and $\constraint$.
The best abstract transformer is 
\begin{equation}\label{eq:abstrans}
\abstrans{\domain}{\constraint}(\absval)=\absval\meet\alpha(\{\val\mid \val\in\gamma(\absval), \val\models \constraint\})
\end{equation}
 where we write 
$\val\models \constraint$ if the concrete value $\val$ satisfies the constraint $\constraint$.
%$\forall \vec{y}\in c: (s[\vec{y}/\vec{\numvar}]
%\equiv \true)$, i.e., the constraint $s$ is valid when evaluated over
%all values $\vec{y}$ of its variables $\vec{\numvar}$ in the concretisation
%of $a$. 
Any abstract transformer that over-approximates the best abstract
transformer is a sound transformer and can be used in our algorithm.
%
For example, we can deduce $\abstrans{\domain}{x=2(y+z)}(\absval)=\absval\meet(-2\leq x\leq 6)$ for the abstract value $\absval=(0\leq y \leq 2 \wedge 1 \leq y-z \leq 1)$.
%
%A detailed description of abstract transformer is presented in Section~\ref{sec:abst}.
We~denote the set of abstract transformers for a safety equation
$\formula$ using abstract domain $\domain$ as
$\abstransset=\{\abstrans{\domain}{\constraint}\mid
\constraint\in\constraints\}$.

%-------------------------------------------------------------------------------
\subsection{Properties of Abstract Domains}
%-------------------------------------------------------------------------------
%
An important property of a clause learning SAT solver is that each
non-singleton element of the partial assignment domain can be 
decomposed into a set of precisely complementable singleton
elements~\cite{dhk2013-popl}.  This property of the partial 
assignment domain is required to learn 
elements that help to guide the model search away from the
conflicting region of the search space.  The complementation operator 
in abstract domains is different from the notion of precise complements. 
%
Most numerical abstract domains, such as intervals and octagons lack
complements, but they can be represented as intersections of
half-spaces, each of which has a complement. 
%
% We identify specific properties of domain elements necessary for 
% abstract model search and learning in abstractions.  
We formalise this in the sequel.
%
\begin{definition} 
A \emph{meet irreducible} $m$ in a complete lattice 
structure $A$ is an element with the following property.
\begin{equation}
\forall m_1, m_2 \in A: m_1 \meet m_2 = m \implies (m = m_1 \lor m = m_2), m \neq \top  
\end{equation}
\end{definition}
%
%Meet irreducibles in ACDCL correspond to the concept of literals in a SAT solver.
The meet irreducibles in the Boolean domain $\booldomain$ for a variable $x$ are 
$x$ and $\neg x$. The meet 
irreducibles in the template polyhedra domain are all elements 
that concretise to half-spaces, i.e., they can be represented 
by a single inequality. For the interval domain, these are 
\ $x \leq d$ or $x \geq d$ for constants $d$. 

%An important property of meet irreducibles in case of partial assignments 
%domain is that they have precise complements.  
%For example, the complement of $\{x \mapsto true \}$ is a 
%singleton element,$\{x \mapsto false \}$, in the partial assignments domain. 

\begin{definition}
A \emph{meet decomposition} $\decomp(\absval)$ of an abstract
element $\absval \in \domain$ is a set of meet irreducibles $M \subseteq \domain$ such that 
$\absval=\bigsqcap_{m\in M} m$.
%$forall m_i \in M, \meet(m_i) = a$, where $max(i) = |M|$.
\end{definition}

For polyhedra this intuitively means that each polyhedron can be
written as an intersection of half-spaces.
%
For example, the meet decomposition of the interval domain element
% $(x,y) \in [2,4]\times[3, 5]$ 
$decomp(2\leq x\leq 4 \wedge 3\leq y\leq 5)$ is
the set $\{x\geq 2, x\leq 4, y\geq 3, y\leq 5\}$.
% \langle x:[2, 4] \rangle \in ItvDom$ which gives set of meet irreducibles, 
% $\{ \langle y \succeq 3 \rangle, \langle y \preceq 5 \rangle, 
% \langle x \succeq 2 \rangle, \langle x \preceq 4 \rangle \}$, that are 
% precisely complementable.

\begin{definition} 
An element $\absval\in \domain$ is called \emph{precisely complementable}
iff $\exists \bar{\absval} \in \domain: \neg\gamma(\bar{\absval})=\gamma(\absval)$, 
i.e., there is an element whose negated concretisation equals
the concretisation of $\absval$.
%m\meet\bar{m}=\bot \wedge m\join\bar{m}=\top$.
%A complementable meet irreducible $\bar{M}$ of an abstract lattice $A$ is the complement of a meet 
%irreducible $M \in A$ such that $\bar{M} \in A$ and the concretisation of $M$ 
%is the set complement of $\bar{M}$.  
%If every meet irreducible in $A$ is complementable, then $A$ is said to
%be have complementable meet irreducibles.
\end{definition}

% An important property of a clause learning SAT solver 
% is that a partial assignments domain can be decomposed 
% into a set of precisely complementable singleton assignments.  
% This property of the partial assignments domain helps to 
% guide the model search away from the conflicting region 
% of the search space and allows case-based analysis.  Complementation 
% operator in abstract domains is different from the notion of precise
% complements. 
%
% \begin{definition}{(Precise complement)} Let $A$ be an lattice. A precise 
% complement of an abstract element $a \in A$ is an element $\bar{a} \in A$ 
% such that the negation of concretization $(\gamma)$ of $a$ is equivalent to 
% concretization of $\bar{a}$, that is, $\gamma(\bar{a}) = \neg \gamma(a))$.
% \end{definition}
%
The precise complementation property of a partial assignment lattice can
be generalised to other lattice structures.  Most numerical abstract
domains, such as intervals, octagons, polyhedra, can be decomposed
into half-spaces, that admits precise complements.  For example, a
precise complement of a meet irreducible $(x \leq 2)$ in the interval
domain over integers is $(x \geq 3)$, or the precise complement of
the meet irreducible $(x+y \leq 1)$ in the octagon domain over
integers is $(x+y \geq 2)$.  Our template-based domain implementation
precisely complements a meet irreducible in an abstraction.  \Omit{
  Numerical abstract domains that admit complementable decomposition
  are shown in Figure~\ref{fig:complement}.  }
% 
\Omit{
\begin{table}
\begin{center}
{
\begin{tabular}{l|l}
\hline
Domain & Precise Complements \\ \hline 
Interval & \((x \leq n) \quad \longrightarrow (x > n)\) \\ \hline
Octagon & \((x+y < 1) \quad \longrightarrow (-x-y < 0)\) \\ \hline
Equality & \((x==y) \quad \longrightarrow (x \neq y)\) \\ \hline 
\end{tabular}
}
\end{center}
\label{fig:complement}
\end{table}
}
%
\Omit {
Note that for many domains $A$, including template polyhedra,
most domain elements are not precisely complementable within $A$.
%
In fact, for template polyhedra all non-meet-irreducible elements $e$
(except $\bot$ and $\top$) are not precisely complementable,
whereas all meet irreducibles are precisely complementable.
%
Hence, we can complement each element in the meet decomposition of $e$ and
re-interpret the obtained set as a disjunction. 
%
%Thus the complement of the octagon in Figure~\ref{octagon} 
%can be written as a disjunction of meet irreducibles:
%\[(x{\leq} -3) \lor (x{\geq} 2) \lor (y{\leq} -2) \lor (y{\geq} 3) \lor (x+y{\geq} 3) \lor (x-y{\geq} 2) \lor (y-x{\geq} 4) \lor (-x-y{\geq} 3)\]
}
Standard abstract interpretation does not require a complementation
operator. Hence, abstract domain libraries, such as APRON~\cite{apron},
do not provide it.  However, it can be implemented with the help of a
meet decomposition as explained above.

\Omit {
\begin{definition}{(Abstract Valuation)} An {\em abstract valuation} is a
mapping of variables to an element of abstract domain. For example, 
\Omit {
a mapping of variable $x$ to an interval environment is given by 
$\langle x \mapsto [2,5] \rangle$ or a 
}
a mapping of constraint variables $\{x,y\}$ to octagon environment 
is given by $\langle x-y \mapsto 0, y-x \mapsto 0 \rangle$.  
An abstract valuation is {\em atomic} if each variable is mapped to a singleton 
value or to $\bot$.  An abstract valuation $(v)$ abstractly satisfies a formula 
$\formula$ if for every variable $x$ in $\formula$, there is a concrete solution 
$(c)$ such that $c(x) \subseteq \gamma \circ v(x)$ holds. 
\end{definition}
}

%
%Another feature that abstract domain libraries do not provide is to
%track the reasons why certain deductions have been made. We come back
%to this point in Section~\ref{sec:abst}.

% The abstract transformer, $apost_{stmt}$, captures the effect of different program 
% statements in the abstract domain. The transformer is precise for octagonal 
% assignments $(x:=y+1)$ but imprecise for non-octagonal assignments $(x:=y+z)$, 
% as shown below.
% \[apost_{x:=y+1}(a) = b = \langle x-y \leq 1, y-x \leq 1 \rangle \qquad apost_{x:=y+z}(b) = \langle \top \rangle \]  

% \begin{definition}{(Abstract Deduction Transformer)} An abstract deduction
% transformer, $\widehat{ded_{\formula}}$ for a formula $\formula$ over an abstract 
% domain $A$ is a sound approximation of a concrete model transformer
% $ded_{\formula}$, given by $\widehat{ded_{\formula}} : A \rightarrow A$, such that 
% $\forall a \in A: \widehat{ded_{\formula}}(a) \in \{\top, \bot, m\}$, where 
% $m \in A$ is a meet irreducible.   
% \end{definition}

% Let us consider a formula $\formula = (x:=y-1)$ to be analyzed over 
% an interval abstract domain, $A = ItvDom$, and let $a = \langle y:[3, 5]
% \rangle \in ItvDom$, then $\widehat{ded_{\formula}}(a) = a \meet \langle x:[2, 4]
% \rangle$.  An abstract deduction transformer is typically computed in the form 
% of strongest post-condition or a weakest pre-condition of a formula in the 
% abstract domain.  

% For a program with $N$ variables, let $L$ be the total number of 
% meet irreducibles returned by a domain $D$.  For $D$ = {\em ItvDom}, the 
% maximum value of $L$ is $2*N$, whereas the maximum value of $L$ is 
% $2*(N^2)$ for $D$ = {\em OctDom}. Note that an octagon is the conjunction 
% of all octagonal inequalities in the set $L$.
%
%========================
%\input{literals-clauses}
%========================

% \Omit {
% The commonly used library for numerical abstract domains  
% is the APRON C library~\cite{apron}.  This library is 
% used for the static analysis of the numerical variables 
% of a program by abstract interpretation. APRON provides a 
% C API interface to various abstract domains and libraries 
% such as {\em BOX}, {\em OCTAGON}, {\em Convex Polyhedra} and
% {\em Linear Equalities} library.  The aim of such analysis is 
% to compute invariants over numerical variables in the 
% program~\cite{se2011}. 
% }
% \Omit {
% To this end, we implement our own template-based polyhedra domain and interval 
% domain which supports complementation operator.  
% %For example, the octagon in Figure~\ref{octagon} can be written as a conjunction of:
% %\[(x>=-2) \land (x<=1) \land (y>=-1) \land (y<=2) \land (x+y<=2)
% %\land (x-y<=1) \land (y-x<=3) \land (-x-y<=2)\] 
% \pscmt{That's no valid motivation. We never complement a whole octagon, but just a
%  meet-irreducible. It's trivial to do that with APRON. The reason was
% a different one: APRON does not support all C operators, e.g. the bitwise
% operators.} 
% }