Commit 5749735d authored by ehilin02's avatar ehilin02
Browse files

abs from appendix to main text

parent f9e07fd5
......@@ -96,6 +96,8 @@ which can be further simplified into
%Moved to the main text
\hide{
\subsection{$\abs(\varphi)$: The {\qfpa} abstraction of $\varphi$}
%\label{ssec:sat-abs}
......@@ -227,6 +229,7 @@ From the fact that the satisfiability of {\qfpa} is in NP, we conclude that the
%The formulas $\exists k.\ k \ge 1 \wedge 2k = y - x $ in $\abs^+(\hls{}(x, y; z))$ can be equivalently replaced by $y -x > 0 \wedge y -x \equiv 0 \bmod 2$. Therefore, $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints. The satisfiability of such formulas is still NP-complete.
%From now on, we shall assume that {\bf $\abs(\varphi)$ is a quantifier-free \PbA\ formula containing modulo constraints}.
\end{remark}
}
\section{Proof of Lemma~\ref{lem-eub}}
......
......@@ -47,20 +47,77 @@ We recall that the satisfiability problem of {\qfpa} and {\EPbA} is NP-complete.
%ASL formulas into equi-satisfiable {\EPbA} formulas.
We basically follow the same idea as ASL to build
a {\qfpa} abstraction of a \slah\ formula $\varphi$, denoted by $\abs(\varphi)$,
that encodes its satisfiability:
\begin{compactitem}
\item At first, points-to atoms $t_1 \pto t_2$ are transformed into $\blk(t_1, t_1+1)$.
\item Then, the block atoms $\blk(t_1, t_2)$ are encoded by the constraint $t_1 < t_2$.
\item The predicate atoms $\hls{}(t_1, t_2; t_3)$, absent in ASL, are encoded by a formula in {\qfpa}, $t_1 = t_2 \vee (t_1 < t_2 \wedge \abs^+(\hls{}(t_1, t_2; t_3)))$.
\item Lastly, the separating conjunction is encoded by an {\qfpa} formula constraining the address terms of spatial atoms.
\end{compactitem}
The Appendix~\ref{app:sat-hls} provides more details.
an equi-satisfiable {\qfpa} abstraction of a \slah\ formula $\varphi$.
%that encodes its satisfiability:
%\begin{compactitem}
%\item At first, points-to atoms $t_1 \pto t_2$ are transformed into $\blk(t_1, t_1+1)$.
%\item Then, the block atoms $\blk(t_1, t_2)$ are encoded by the constraint $t_1 < t_2$.
%\item The predicate atoms $\hls{}(t_1, t_2; t_3)$, absent in ASL, are encoded by a formula in {\qfpa}, $t_1 = t_2 \vee (t_1 < t_2 \wedge \abs^+(\hls{}(t_1, t_2; t_3)))$.
%\item Lastly, the separating conjunction is encoded by an {\qfpa} formula constraining the address terms of spatial atoms.
%\end{compactitem}
%We utilize $\abs^+(\hls{}(x, y; z))$ %defined in the above section
%to obtain in polynomial time an equi-satisfiable {\qfpa} abstraction for a symbolic heap $\varphi$, denoted by $\abs(\varphi)$.
We introduce some notations first.
%
Given a formula $\varphi\equiv \Pi : \Sigma$,
$\atoms(\varphi)$ denotes the set of spatial atoms in $\Sigma$, and
$\patoms(\varphi)$ denotes the set of predicate atoms in $\Sigma$.
We also denote $\overline{\patoms}(\varphi)$ for $\atoms(\varphi)\setminus\patoms(\varphi)$.
\begin{definition}{(Presburger abstraction of \slah\ formula)}
Let $\varphi\equiv \Pi : \Sigma$ be a \slah\ formula.
The abstraction of $\varphi\equiv \Pi : \Sigma$,
denoted by $\abs(\varphi)$, is
the formula $\Pi\wedge\phi_{\Sigma}\wedge\phi_*$
where:
\begin{itemize}
\item $\phi_{\Sigma}\triangleq\bigwedge\limits_{a \in \atoms(\varphi)}\abs(a)$ such that
{\small
\begin{eqnarray}
\abs(t_1\mapsto t_2) & \triangleq & \ltrue \\
\abs(\blk(t_1,t_2)) & \triangleq & t_1<t_2 \\
\abs(\hls{}(t_1, t_2, t_3)) & \triangleq & t_1=t_2 \\
& \lor &(t_1 < t_2 \land \abs^+ (\hls{}(x, y;z))[t_1/x, t_2/y, t_3/z]),
\end{eqnarray}
}
%where the boolean variables $\isemp_a$ are introduced for each atom $a \in \patoms(\varphi)$ to encode whether $a$ denotes an empty heap.
where $\abs^+ (\hls{}(x, y;z))$ is the least-fixed-point summary of $\hls{}(x, y;z)$.
\item $\phi_\sepc\triangleq\phi_1\wedge \phi_2 \wedge \phi_3$
specifies the semantics of separating conjunction,
where
{\small
\begin{eqnarray}
\phi_1 & \triangleq & \bigwedge\limits_{a_i,a_j \in \patoms(\varphi), i<j}
\begin{array}[t]{l}
(\isnonemp_{a_i} \land \isnonemp_{a_j}) \limp \\
\quad (\atomtail(a_j) \le \atomhead(a_i)\lor \atomtail(a_i) \le \atomhead(a_j))
\end{array}
\\
\phi_2 & \triangleq & \bigwedge\limits_{a_i \in \patoms(\varphi), a_j \in \overline{\patoms}(\varphi)}
\begin{array}[t]{l}
(\isnonemp_{a_i}) \limp \\
\quad (\atomtail(a_j) \le \atomhead(a_i) \lor \atomtail(a_i) \le \atomhead(a_j))
\end{array}
\\
\phi_3 & \triangleq & \bigwedge\limits_{a_i, a_j \in \overline{\patoms}(\varphi), i < j}
\atomtail(a_j) \le \atomhead(a_i) \lor \atomtail(a_i) \le \atomhead(a_j)
\end{eqnarray}
}
\end{itemize}
and for each spatial atom $a_i$, $\isnonemp_{a_i}$ is an abbreviation of the formula $\atomhead(a_i) < \atomtail(a_i)$.
\end{definition}
For formulas $\varphi\equiv \exists \vec{z}\cdot \Pi : \Sigma$,
we define $\abs(\varphi) \triangleq \abs(\Pi:\Sigma)$ since $\exists \vec{z}\cdot \Pi : \Sigma$ and $\Pi:\Sigma$ are equi-satisfiable.
%The Appendix~\ref{app:sat-hls} provides more details.
%
The crux of this encoding and
its originality with respect to the ones proposed for ASL in~\cite{BrotherstonGK17}
is the computation of $\abs^+(\hls{}(t_1, t_2; t_3))$,
which are the least-fixed-point summaries in {\qfpa} for $\hls{}(t_1, t_2; t_3)$.
is the computation of $\abs^+(\hls{}(x, y; z))$.
In the sequel, we show how to compute them.
%Moreover, $\abs(\varphi)$ will be used as a basic ingredient of the entailment procedure in Section~\ref{sec:ent}.
......@@ -86,16 +143,16 @@ In the sequel, we show how to compute them.
%\subsection{{\EPbA} summary of $\hls{}$ atoms}
%\label{ssec:sat-hls-abs}
\smallskip
Intuitively, the abstraction of the predicate atoms $\hls{}(t_1, t_2; t_3)$
shall summarize the relation between $t_1$, $t_2$ and $t_3$
Intuitively, the abstraction of the predicate atoms $\hls{}(x, y; z)$
shall summarize the relation between $x$, $y$ and $z$
for all $k \ge 1$ unfoldings of the predicate atom.
From the fact that the pure constraint in the inductive rule of $\hls{}$ is $2 \le x' - x \le v$, it is easy to observe that
for each $k \ge 1$, $\hls{k}(t_1, t_2; t_3)$ can be encoded by $2 k \le t_2-t_1 \le k t_3$. It follows that $\hls{}(t_1, t_2; t_3)$ can be encoded by $\exists k.\ k \ge 1 \wedge 2k \le t_2 - t_1 \le k t_3$.
If $t_3 \equiv\infty$, then $\exists k.\ k \ge 1 \wedge 2 k \le t_2-t_1 \le k t_3$ is equivalent to $\exists k.\ k \ge 1 \wedge 2k \le t_2 - t_1 \equiv 2 \le t_2 - t_1$, thus a {\qfpa} formula.
Otherwise, $2 k \le t_2-t_1 \le k t_3$ is a non-linear formula since $k t_3$ is a non-linear term if $t_3$ contains variables.
for each $k \ge 1$, $\hls{k}(x, y; z)$ can be encoded by $2 k \le y - x \le k z$. It follows that $\hls{}(x, y; z)$ can be encoded by $\exists k.\ k \ge 1 \wedge 2k \le y - x \le k z$.
If $z \equiv\infty$, then $\exists k.\ k \ge 1 \wedge 2 k \le y - x \le k z$ is equivalent to $\exists k.\ k \ge 1 \wedge 2k \le y - x \equiv 2 \le y - x$, thus a {\qfpa} formula.
Otherwise, $2 k \le y - x \le k z$ is a non-linear formula since $k z$ is a non-linear term.
The following lemma states that
%In the sequel, we are going to show that
$\exists k.\ k \ge 1 \wedge 2 k \le t_2 - t_1 \le k t_3$ can actually be turned into an equivalent {\qfpa} formula.
$\exists k.\ k \ge 1 \wedge 2 k \le y -x \le k z$ can actually be turned into an equivalent {\qfpa} formula.
\begin{lemma}[Summary of $\hls{}$ atoms]\label{lem-hls}
Let $ \hls{}(x, y; z)$ be an atom in \slah\
......@@ -104,76 +161,15 @@ representing a non-empty heap, where $x, y, z$ are three distinct variables in $
We can construct in polynomial time an {\qfpa} formula $\abs^+(\hls{}(x,y; z))$
which summarizes $\hls{}(x, y; z)$, namely we have
for every stack $s$, $s \models \abs^+(\hls{}(x,y; z))$ iff
there exists a heap $h$ such that $s, h \models \hls{}(x, y, z)$.
there exists a heap $h$ such that $s, h \models \hls{}(x, y; z)$.
%Similarly for $ \hls{}(x, y; \infty)$ and $ \hls{}(x, y; d)$ with $d \in \NN$.
\end{lemma}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hide{
\begin{proof}
The constraint that the atom represents a non-empty heap means that
the inductive rule defining $\hls{}$ in Equation~(\ref{eq:hlsv-rec})
should be applied at least once. As explained above,
%we prove by induction (see Appendix~\ref{app:sat-hls})
%Notice that the semantics of this rule
%defines, at each inductive step,
%a memory block starting at $x$ and ending before $x'$ of size $x'-x$.
%By induction on $k \ge 1$, we obtain that $\hls{k}(x, y; z)$ defines
%a memory block of length $y-x$ such that
%$2 k \le y-x \le k z$. Then
$\hls{}(x, y; z)$ is summarized by the formula $\exists k.\ k \ge 1 \wedge 2k \le y -x \le kz$, which is a non-linear arithmetic formula.
%
However, the previous formula
%The formula $\exists k.\ k \ge 1 \wedge 2k \le y -x \le kz$
is actually equivalent to the disjunction of the two formulas corresponding to the following two cases:
\begin{compactitem}
\item If $2 = z$, then $\abs^+(\hls{}(x, y; z))$ has as disjunct
$\exists k.\ k \ge 1 \land y -x = 2k$.
%
\item If $2 < z$, then we consider two sub-cases:
(a) If $k = 1$
then $\abs^+(\hls{}(x, y; z))$ contains
$2 \leq y-x \le z$ as a disjunct.
(b) If $k \ge 2$ then we observe that the intervals
$[2k, k z]$ and $[2(k+1), (k+1) z]$
overlap,
and consequently $\bigcup_{k \ge 2} [2k, kz] = [4, \infty)$.
Therefore, $\abs^+(\hls{}(x, y; z))$ contains $4 \le y-x$ as a disjunct.
%Therefore, $\bigcup \limits_{k \ge 2} [2k, kz] = [4, \infty)$,
%It follows that the formula
%$\exists k.\ k \ge 2 \land 2k \le y-x \le k z$
%is equivalent to $4 \le y-x$.
%Therefore, $\abs^+(\hls{}(x, y; z))$ contains $4 \le y-x$ as a disjunct.
Thus we obtain $2 < z ~\land~ \big(2 \leq y-x \le z \lor 4 \le y-x \big)$, which can be simplified into $2 < z ~\land~ 2 \le y - x$.
\end{compactitem}
To sum up, we obtain
\begin{align*}
\abs^+(\hls{}(x, y; z)) & \triangleq
\big(2 = z
\land \exists k.\ k \ge 1 \land 2k = y-x \big) %\\
%& \lor & \big(2 < z
~\lor~ \big(2 < z
\land 2 \le y - x
\big).
\end{align*}
\vspace{-2eX}\qed
\end{proof}
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Since the satisfiability problem of {\qfpa} is NP-complete,
%We are using $\abs^+(\hls{}(x, y; z))$ defined above
%to obtain in polynomial time an equi-satisfiable \EPbA\ abstraction for a symbolic heap $\varphi$, denoted by $\abs(\varphi)$.
the satisfiability problem of \slah\ is in NP.
%
% ESOP'21, Reviewer 3: At the end of page 10, when discussing the abstraction idea, I wondered to what extent this is related to the decision procedures for ASL itself; is the overall approach new, or is it a similar approach with suitable extensions?
%For this reason, we leave
%the definition of $\abs(\varphi)$ and the proof of its correctness
%stated by the following proposition
%to Appendix~\ref{app:sat-hls}.
%
The correctness of $\abs(\varphi)$ is guaranteed by the following result.
%\vspace{-2mm}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment