Commit 9347b1f5 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

update conclusion; first reading of new proofs and appendices

parent dcd51d31
......@@ -99,7 +99,7 @@ which can be further simplified into
%\subsection{\EPbA\ abstraction for \slah\ formulas}
%\label{ssec:sat-abs}
We utilize $\abs^+(\hls{}(x, y; z))$ defined in the above section
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)$.
%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{}$.
......@@ -109,6 +109,8 @@ 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$.
\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_*$
......@@ -149,6 +151,7 @@ where
}
\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.
......@@ -214,7 +217,10 @@ From the definition of $h$, we know that $s, h \models \varphi$. Therefore, $\va
\begin{remark}
%The Boolean variables $\isemp_a$ in $\abs(\varphi)$ are introduced for improving the readability. They are redundant in the sense that they can be equivalently replaced by the formula $\atomhead(a) = \atomtail(a)$.
From the construction of $\abs(\varphi)$, we know that $\abs(\varphi)$ is in {\qfpa} and the size of $\abs(\varphi)$ is polynomial in that of $\varphi$. From the fact that the satisfiability of {\qfpa} is in NP, we conclude that the satisfiability of \slah\ is in NP.
From the definition of $\abs(\varphi)$, it follows that
$\abs(\varphi)$ is in {\qfpa} and
the size of $\abs(\varphi)$ is polynomial in that of $\varphi$.
From the fact that the satisfiability of {\qfpa} is in NP, we conclude that the satisfiability of \slah\ is in NP.
%
%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}.
......@@ -225,7 +231,7 @@ From the construction of $\abs(\varphi)$, we know that $\abs(\varphi)$ is in {\
\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 \rightarrow \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)$.
}
\smallskip
......@@ -311,7 +317,7 @@ 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 \rightarrow \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$. Consequently, $s \models \exists z.\ \xi_{eub,\varphi}(z) \wedge z \le t_3$.
\medskip
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -319,7 +325,10 @@ Moreover, from the definition of $\eub_\varphi(s)$, we know that there is an unf
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 \rightarrow n] \models \xi_{eub, \varphi}(z) \wedge z \le t_3$ for some $n \in \NN$.
Thus $s[z \rightarrow n] \models \xi_{eub, \varphi}(z)$. Moreover, from Lemma~\ref{lem-eub}, we know that $s[z \rightarrow \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$.
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$.
\qed
\end{proof}
......@@ -5,7 +5,7 @@
In this work, we investigated \slah, a separation logic fragment that allows pointer arithmetic inside inductive definitions so that the commonly used data structures e.g. heap lists can be defined.
We show that the satisfiability problem of {\slah} is NP-complete and
the entailment problem can be solved in doubly exponential time.
the entailment problem is coNP-complete.
%We propose decision procedure for both problems calling satisfiability
% of Presburger arithmetic formulas.
%We show that the satisfiability problem is NP-complete and
......@@ -18,9 +18,10 @@ We show that the satisfiability problem of {\slah} is NP-complete and
%%The same classes of complexity are observed for these problems in ASL,
%% but for the quantified formulas in the entailment.
We implemented the decision procedures in a solver, \cspenp, and use it
to efficiently solve more than hundred problems issued from program verification
or randomly generated. There are several directions for the future work.
At first, it is interesting to see whether the decision procedures for heap lists in this work can be extended to tackle free lists, another common data structure in memory allocators \cite{Knuth97}. Moreover, since bit operations are also widely used in memory allocators, it would also be interesting to automate the reasoning about bit operations inside inductive definitions.
to efficiently solve more than hundred problems issued from verification of
program manipulating heap lists
or randomly generated problems.
For future work, it is interesting to see whether the logic \slah\ and its decision procedures can be extended to specify free lists, another common data structure in memory allocators \cite{Knuth97} in addition to heap lists. Moreover, since bit operations are also widely used in memory allocators, it would also be interesting to automate the reasoning about bit operations inside inductive definitions.
%%MS: moved into introduction
%\smallskip
......
......@@ -24,7 +24,7 @@ Given the symbolic heaps $\varphi$ and $\psi$ in \slah\ such that
Our goal in this section is to show that the entailment problem is decidable, as stated in the following theorem.
\begin{theorem}\label{thm-entail}
The entailment problem of {\slah} is coNP-complete.\mihaela{state upperbound}
The entailment problem of {\slah} is coNP-complete. %\mihaela{state upperbound}
\end{theorem}
The coNP lower bound follows from the fact that the entailment problem of quantifier-free ASL formulas is also coNP-complete~\cite{BrotherstonGK17}.
The remainder of this section is devoted to the proof of the coNP upper bound.
......
%!TEX root = tab2021.tex
%!TEX root = atva2021.tex
%\newpage
......@@ -25,7 +25,8 @@ supports the new theory \slah.
Internally, \cspenp\ parses the input file
which shall include the definition of $\hls{}$
%ESOP 21 Reviewer 3: so this isn't built in specially? Or is it just that the tool expects the definition to be there because of the format? Does the definition have to be in syntactically exactly the form expected?
and the satisfiability or entailment queries in the SL-COMP format~\cite{DBLP:conf/tacas/SighireanuPRGIR19}.
and the satisfiability or entailment queries in the SL-COMP format~\cite{SLCOMPsite}.
%~\cite{DBLP:conf/tacas/SighireanuPRGIR19}.
%
\begin{compactitem}
\item For satisfiability queries,
......@@ -69,7 +70,7 @@ and the satisfiability or entailment queries in the SL-COMP format~\cite{DBLP:co
\end{compactitem}
\medskip
\smallskip
\mypar{Benchmarks.}
We generated 190 benchmarks,
available at~\cite{CompSpenSite} (directory \texttt{samples}),
......@@ -115,7 +116,7 @@ classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as fo
%using \textsc{VeriFast} since a lot of lemma has to be proved to be able
%to transform (split, merge) allocated memory blocks in \textsc{VeriFast}.
\medskip
\smallskip
\mypar{Experiments.}
We run \cspenp over the four benchmark suites, using a Ubuntu-16.04 64-bit lap-top with an Intel Core i5-8250U CPU and 2GB RAM.
The experimental results are summarized in Table~\ref{tab-exp}. We set the timeout to 30 seconds. The statistics of average time and maximum time do not include the time of timeout instances.
......
......@@ -62,21 +62,21 @@ int* search(int rsz) {
& \triangleq & 0 < b < e : \hls{}(b,e)
\\[2mm]
\texttt{path}_{\texttt{4-9}} \label{eq:over-path-once}
& \triangleq & 0 < b \land b = t \land t < e \land sz_0 < rsz
& \triangleq & 0 < b < e \land b = t \land sz_0 < rsz
\\
& \land & sz_0 = t_1 - t \land 2 \le t_1 - t
\nonumber \\
& : & t \pto sz_0 \sepc \blk(t+1, t_1) \sepc \hls{}(t_1,e)
\nonumber \\[2mm]
I \label{eq:over-inv}
& \triangleq & 0 < b < e
& \triangleq & 0 < b < e \land b \le t
\\
\nonumber
& : & \hls{}(b,t; rsz-1) \sepc \hls{}(t,e)
\\[2mm]
\texttt{post}_{\texttt{5-10}}(I) \label{eq:over-inv-once}
& \triangleq & 0 < b < e \land t_0 < e \land sz_0 < rsz \\
& \land & 2 \le sz_0 \land t - t_0=sz_0
& \triangleq & 0 < b < e \land b\le t_0 < e \\
& \land & 2 \le sz_0 < rsz \land t - t_0=sz_0
\nonumber \\
& : & \hls{}(b,t_0;rsz-1) \sepc t_0 \pto sz_0
\nonumber \\
......
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