Commit 742a846a authored by ehilin02's avatar ehilin02
Browse files

entailment with one atom

parent b4741784
%!TEX root = atva2021.tex
\section{\EPbA\ abstraction for \slah\ formulas}\label{app:sat-hls}
\section{{\qfpa} abstraction for \slah\ formulas}\label{app:sat-hls}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{{\EPbA} summary of $\hls{}$ atoms}
\subsection{{\qfpa} summary of $\hls{}$ atoms}
\label{ssec:sat-hls-abs}
\noindent {\bf Lemma~\ref{lem-hls}}.
......@@ -96,11 +96,11 @@ which can be further simplified into
%\subsection{\EPbA\ abstraction for \slah\ formulas}
\subsection{$\abs(\varphi)$: The {\qfpa} abstraction of $\varphi$}
%\label{ssec:sat-abs}
We utilize $\abs^+(\hls{}(x, y; z))$ %defined in the above section
to obtain in polynomial time an equi-satisfiable \EPbA\ abstraction for a symbolic heap $\varphi$, denoted by $\abs(\varphi)$.
to obtain in polynomial time an equi-satisfiable {\qfpa} abstraction for a symbolic heap $\varphi$, denoted by $\abs(\varphi)$.
%This shows that the satisfiability problem of \slah\ is in NP. Moreover, it enables using the off-the-shelf SMT solvers e.g. Z3 to solve the satisfiability problem of \slah\ formulas.
%This abstraction extends the ones proposed in~\cite{BrotherstonGK17,DBLP:journals/corr/abs-1802-05935} for ASL to deal with the inductive predicate $\hls{}$.
......@@ -231,7 +231,7 @@ From the fact that the satisfiability of {\qfpa} is in NP, we conclude that the
\smallskip
\noindent {\bf Lemma~\ref{lem-eub}}.
\emph{For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, a {\qfpa} formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$.
\emph{For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, a {\qfpa} formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$ and $s[z \gets n] \not \models \xi_{eub,\varphi}(z)$ for all $n \neq \eub_\varphi(s)$.
}
\smallskip
......@@ -243,7 +243,7 @@ From the construction of $\abs^+(\hls{}(t'_1, t'_2; t'_3))$ in Section~\ref{sec:
\Pi \wedge
\left(
\begin{array}{l}
(t'_3 = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0)\ \vee \\
(t'_3 = 2 \wedge z = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0)\ \vee \\
(2 < t'_3 \wedge 2 \le z \le t'_3\ \wedge (2 \le t'_2 - t'_1 - z \vee t'_2 - t'_1 = z))
\end{array}
\right),
......@@ -254,7 +254,7 @@ where $t'_2 - t'_1 - z$ denotes the remaining size of the heap after removing a
\Pi \wedge
\left(
\begin{array}{l}
(t'_3 = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0)\ \vee \\
(t'_3 = 2 \wedge z = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0)\ \vee \\
\left(
\begin{array}{l}
2 < t'_3 \wedge 2 \le z \le t'_3 \wedge (2 \le t'_2 - t'_1 - z \vee t'_2 - t'_1 = z) \ \wedge \\
......@@ -269,16 +269,18 @@ where $ \forall z'.\ z < z' \le t'_3 \rightarrow \neg (2 \le t'_2 - t'_1 - z'
$$
\begin{array}{l}
z+1 \le t'_3 \rightarrow (t'_2 - t'_1 \le z+2 \wedge t'_2 - t'_1 \neq z+1)\ \wedge \\
z+2 \le t'_3 \rightarrow t'_2 - t'_1 \neq z+2.
z+2 \le t'_3 \rightarrow t'_2 - t'_1 \neq z+2,
\end{array}
$$
where $t'_2 - t'_1 \neq z+1$ is an abbreviation of $t'_2 - t'_1 < z+1 \vee z+1 < t'_2 - t'_1$, similarly for $t'_2 - t'_1 \neq z+2$.
It follows that $\xi_{eub,\varphi}(z) $ can be simplified into
%& & \Pi \wedge \label{f-xi-lub}
\[
\Pi \wedge
\left(
\begin{array}{l}
(t'_3 = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0)\ \vee \\
(t'_3 = 2 \wedge z = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0)\ \vee \\
\left(
\begin{array}{l}
2 < t'_3 \wedge 2 \le z \le t'_3 \wedge (2 \le t'_2 - t'_1 - z \vee t'_2 - t'_1 = z) \ \wedge \\
......@@ -298,7 +300,8 @@ which is a {\qfpa} formula.
\noindent {\bf Lemma~\ref{lem-hls-hls}}
\emph{
Let $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, $\psi \equiv \hls{}(t_1, t_2; t_3)$, and $\preceq$ be a total preorder over $\addr(\varphi) \cup \addr(\psi)$ such that $C_\preceq \models t'_1 < t'_2 \wedge t'_1 = t_1 \wedge t'_2 = t_2$.
Then $\varphi \models_\preceq \psi$ iff $C_\preceq \wedge \abs(\varphi) \models \exists z.\ \xi_{eub, \varphi}(z) \wedge z \le t_3$.
Then $\varphi \models_\preceq \psi$ iff $C_\preceq \wedge \abs(\varphi) \models
\forall z.\ \xi_{eub, \varphi}(z) \rightarrow z \le t_3$.
}
\smallskip
......@@ -317,18 +320,19 @@ Let $s$ be an interpretation such that $s \models C_\preceq \wedge \abs(\varphi)
At first, from $s \models \abs(\varphi)$ and Lemma~\ref{lem-eub}, we deduce that $s[z \rightarrow \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$.
%
Moreover, from the definition of $\eub_\varphi(s)$, we know that there is an unfolding scheme, say $sz_1, \cdots, sz_\ell$, such that $\eub_\varphi(s) = \max(sz_1, \cdots, sz_\ell)$. From the definition of unfolding schemes, we have $2 \le sz_i \le s(t'_3)$ for every $i \in [\ell]$ and $s(t'_2) = s(t'_1) + \sum \limits_{i \in [\ell]} sz_i$. Therefore, there is a heap $h$ such that $s, h \models \varphi$ and for every $i \in [\ell]$, $h(s(t'_1) + \sum \limits_{j \in [i-1]} sz_j) = sz_i$. From the assumption $\varphi \models_\preceq \psi$, we deduce that $s, h \models \psi \equiv \hls{}(t_1, t_2; t_3)$. Then each chunk of $h$ has to be matched exactly to one unfolding of $ \hls{}(t_1, t_2; t_3)$. Thus, $2 \le sz_i \le s(t_3)$ for every $i \in [\ell]$. Therefore, $\eub_\varphi(s) = \max(sz_1, \cdots, sz_\ell) \le s(t_3)$. We deduce that $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z) \wedge z \le t_3$. Consequently, $s \models \exists z.\ \xi_{eub,\varphi}(z) \wedge z \le t_3$.
Moreover, from the definition of $\eub_\varphi(s)$, we know that there is an unfolding scheme, say $sz_1, \cdots, sz_\ell$, such that $\eub_\varphi(s) = \max(sz_1, \cdots, sz_\ell)$. From the definition of unfolding schemes, we have $2 \le sz_i \le s(t'_3)$ for every $i \in [\ell]$ and $s(t'_2) = s(t'_1) + \sum \limits_{i \in [\ell]} sz_i$. Therefore, there is a heap $h$ such that $s, h \models \varphi$ and for every $i \in [\ell]$, $h(s(t'_1) + \sum \limits_{j \in [i-1]} sz_j) = sz_i$. From the assumption $\varphi \models_\preceq \psi$, we deduce that $s, h \models \psi \equiv \hls{}(t_1, t_2; t_3)$. Then each chunk of $h$ has to be matched exactly to one unfolding of $ \hls{}(t_1, t_2; t_3)$. Thus, $2 \le sz_i \le s(t_3)$ for every $i \in [\ell]$. Therefore, $\eub_\varphi(s) = \max(sz_1, \cdots, sz_\ell) \le s(t_3)$. We deduce that $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z) \wedge z \le t_3$. Moreover, from Lemma~\ref{lem-eub}, we know that for all $n \neq \eub_\varphi(s)$, $s[z \gets n] \not \models \xi_{eub,\varphi}(z)$. Consequently, $s \models \forall z.\ \xi_{eub,\varphi}(z) \rightarrow z \le t_3$.
\medskip
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\noindent \emph{``If'' direction}: Suppose $C_\preceq \wedge \abs(\varphi) \models \exists z.\ \xi_{eub, \varphi}(z) \wedge z \le t_3$ and $s, h \models C_\preceq \wedge \Pi: \hls{}(t'_1, t'_2; t'_3)$. We show $s, h \models \psi$.
\noindent \emph{``If'' direction}: Suppose $C_\preceq \wedge \abs(\varphi) \models \forall z.\ \xi_{eub, \varphi}(z) \rightarrow z \le t_3$ and $s, h \models C_\preceq \wedge \Pi: \hls{}(t'_1, t'_2; t'_3)$. We show $s, h \models \psi$.
From $s, h \models C_\preceq \wedge \Pi: \hls{}(t'_1, t'_2; t'_3)$, we know that there are $sz_1, \cdots, sz_\ell$ such that they are the sequence of chunk sizes in $h$. Therefore, $(sz_1, \cdots, sz_\ell)$ is an unfolding scheme of $\varphi$ w.r.t. $s$. From the definition of $\eub_\varphi(s)$, we have $\eub_\varphi(s) $ is the maximum chunk size upper bound of the unfolding schemes of $\varphi$ w.r.t. $s$. Therefore, $\max(sz_1, \cdots, sz_\ell) \le \eub_\varphi(s)$.
From $s, h \models C_\preceq \wedge \Pi: \hls{}(t'_1, t'_2; t'_3)$, we deduce that $s \models C_\preceq \wedge \abs(\varphi)$.
Because $C_\preceq \wedge \abs(\varphi) \models \exists z.\ \xi_{eub, \varphi}(z) \wedge z \le t_3$, we have $s \models \exists z.\ \xi_{eub, \varphi}(z) \wedge z \le t_3$.
Then $s[z \gets n] \models \xi_{eub, \varphi}(z) \wedge z \le t_3$ for some $n \in \NN$.
Thus $s[z \gets n] \models \xi_{eub, \varphi}(z)$. Moreover, from Lemma~\ref{lem-eub}, we know that $s[z \gets \eub_\varphi(s)] \models \xi_{eub, \varphi}(z)$.
According to the definition of $\eub_\varphi(s)$, we deduce that $n = \eub_\varphi(s)$. Therefore, $\max(sz_1, \cdots, sz_\ell) \le \eub_\varphi(s) \le s(t_3)$. It follows that for every $i \in [\ell]$, $2 \le sz_i \le s(t_3)$. We conclude that $s, h \models \hls{}(t_1, t_2; t_3) \equiv \psi$.
Because $C_\preceq \wedge \abs(\varphi) \models \forall z.\ \xi_{eub, \varphi}(z) \rightarrow z \le t_3$, we have $s \models \forall z.\ \xi_{eub, \varphi}(z) \rightarrow z \le t_3$.
%Then $s[z \gets n] \models \xi_{eub, \varphi}(z) \wedge z \le t_3$ for some $n \in \NN$.
%Thus $s[z \gets n] \models \xi_{eub, \varphi}(z)$.
From Lemma~\ref{lem-eub}, we know that $s[z \gets \eub_\varphi(s)] \models \xi_{eub, \varphi}(z)$.
Therefore, we deduce that $s[z \gets \eub_\varphi(s)] \models z \le t_3$, namely, $\eub_\varphi(s) \le s(t_3)$. Then $\max(sz_1, \cdots, sz_\ell) \le \eub_\varphi(s) \le s(t_3)$. It follows that for every $i \in [\ell]$, $2 \le sz_i \le s(t_3)$. We conclude that $s, h \models \hls{}(t_1, t_2; t_3) \equiv \psi$.
\qed
\end{proof}
......@@ -89,7 +89,7 @@ with respect to stacks %\mihaela{r3: not clear}
can be captured by a {\qfpa} formula.
\begin{lemma}\label{lem-eub}
For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, a {\qfpa} formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$.
For an {\slah} formula $\varphi \equiv \Pi: \hls{}(t'_1, t'_2; t'_3)$, a {\qfpa} formula $\xi_{eub,\varphi}(z)$ can be constructed in linear time such that for every store $s$ satisfying $s \models \abs(\varphi)$, we have $s[z \gets \eub_\varphi(s)] \models \xi_{eub,\varphi}(z)$ and $s[z \gets n] \not \models \xi_{eub,\varphi}(z)$ for all $n \neq \eub_\varphi(s)$.
\end{lemma}
The following lemma (proof in the appendix) provides the correct test used
......
......@@ -47,20 +47,20 @@ 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
an {\EPbA} abstraction of a \slah\ formula $\varphi$, denoted by $\abs(\varphi)$,
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 {\EPbA}, $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 {\EPbA} formula constraining the address terms of spatial atoms.
\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.
%
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 \EPbA\ for $\hls{}(t_1, t_2; t_3)$.
which are the least-fixed-point summaries in {\qfpa} for $\hls{}(t_1, t_2; t_3)$.
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}.
......
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