Commit d604fec2 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

fix issues signaled by reviewers of CADE

parent 64946efe
......@@ -9,8 +9,9 @@ $\varphi \models_\preceq \psi$, where
$\varphi \equiv \Pi: a_1 \sepc \cdots \sepc a_m$,
$\psi \equiv \Pi': b_1$
and the constraints (\ref{eq:order})--(\ref{eq:order-conseq}) are satisfied.
Because $C_\preceq \wedge \abs(\varphi)$ implies $\Pi'$,
we simplify this entailment to deciding:
From~(\ref{eq:order}) and the definition of $\abs$, we have that\mihaela{r3}
$C_\preceq \land \abs(\varphi)$ implies $\Pi'$,
so we simplify this entailment to deciding:
\begin{align*}
C_\preceq \wedge \Pi: a_1 \sepc \cdots \sepc a_m \models_\preceq b_1,
\end{align*}
......@@ -83,7 +84,8 @@ Let $\varphi \equiv x < y: \hls{}(x, y; 3)$ and $s$ be a store such that $s(x)=
\end{example}
The following lemma (proved in the appendix) states that
the effective upper bounds of $\varphi$ with respect to stacks
the effective upper bounds of chunks in heap lists atoms of $\varphi$
with respect to stacks\mihaela{r3: not clear}
can be captured by an {\EPbA} formula.
\begin{lemma}\label{lem-eub}
......
......@@ -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 in EXPTIME.
The entailment problem of {\slah} is in EXPTIME.\mihaela{state upperbound}
\end{theorem}
For comparison, the entailment problem of quantifier-free ASL formulas is in coNP~\cite{BrotherstonGK17}.
......@@ -75,7 +75,8 @@ Recall that a \emph{preorder} $\preceq$ over a set $A$
%\vspace{-2mm}
\begin{definition}[Total preorder compatible with $\abs(\varphi)$]
Let $\preceq$ be a total preorder over $\addr(\varphi) \cup \addr(\psi)$. Then $\preceq$ is said to be \emph{compatible with} $\varphi$ if $\abs(\varphi) \wedge C_\preceq$ is satisfiable, where
Let $\preceq$ be a total preorder over $\addr(\varphi) \cup \addr(\psi)$. Then $\preceq$ is said to be \emph{compatible with} $\varphi$ if\mihaela{r2: symmetry?}
$\abs(\varphi) \wedge C_\preceq$ is satisfiable, where
\begin{align}\label{eq:start-end}
C_\preceq & \triangleq &
\bigwedge_{t_1, t_2 \in \addr(\varphi) \cup \addr(\psi), t_1 \simeq t_2} t_1 = t_2 \wedge \bigwedge_{t_1, t_2 \in \addr(\varphi) \cup \addr(\psi), t_1 \prec t_2} t_1 < t_2.
......
......@@ -6,7 +6,7 @@
\label{sec:exp-hls}
\mypar{Implementation.}
The decision procedures presented are implemented as an extension of the \cspen\ solver~\cite{GuCW16,CompSpenSite}, called \cspenp.
The decision procedures presented are implemented as an extension of the \cspen\ solver~\cite{GuCW16}, called \cspenp, available at~\cite{CompSpenSite}.
Let us briefly recall some information about {\cspen}. {\cspen} is written in C++ and includes several decision procedures for symbolic heap fragments including
(i) inductive predicates that are compositional~\cite{EneaSW15}
(the predicate $\ls{}(x,y)$ for list segments is a simple example)
......@@ -71,7 +71,9 @@ and the satisfiability or entailment queries in the SL-COMP format~\cite{DBLP:co
\medskip
\mypar{Benchmarks.}
We generated 133 benchmarks, %with 66 and 67 instances for the satisfiability and entailment problem respectively. These benchmarks are
We generated 133 benchmarks,
available at~\cite{CompSpenSite} (directory \texttt{samples}),
%with 66 and 67 instances for the satisfiability and entailment problem respectively. These benchmarks are
classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as follows:
%%MS: not clear what is the number here, leave it to the table.
%MEM-SAT (38), MEM-ENT (38), RANDOM-SAT (28), RANDOM-ENT (29), where SAT and ENT represent satisfiability and entailment respectively, moreover,
......
......@@ -41,7 +41,8 @@ the rules in Equations~(\ref{eq:hlsv-emp}) and (\ref{eq:hlsv-rec}),
%\end{align}
where $v$ is a variable interpreted over $\NN\cup\{\infty\}$.
%Here we assume that $c \ge 2$ since $x \pto x'-x \sepc \blk(x+1,x')$ occurs in the body of Rule~(\ref{eq:hlsv-rec}).
An atom $\hls{}(x,y;\infty)$ is also written $\hls{}(x,y)$.
An atom $\hls{}(x,y;\infty)$ is also written $\hls{}(x,y)$;
$\top$ and $\bot$ are shorthands for $x=x$ and $x\ne x$ atoms..
Whenever one of $\Pi$ or $\Sigma$ is empty, we omit the colon.
We write $\fv(\varphi)$ for the set of free variables occurring in $\varphi$.
If $\varphi = \exists\vec{z}\cdot\Pi:\Sigma$,
......@@ -74,7 +75,8 @@ $s(t + t') = s(t) + s(t')$.
We denote $s[x\mapsto n]$ for a stack defined as $s$ except for the
interpretation of $x$ which is $n$.
Notice that $\infty$ is used only to give up the upper bound
on the value of the chunk size in the definition of $\hls{}$.
on the value of the chunk size in the definition of $\hls{}$
(see Equations~(\ref{eq:hlsv-emp})--(\ref{eq:hlsv-infty})).
%
The heap $h$ is a partial function $\NN \pfun \NN$.
%where the neutral element is $e$ (function undefined in all points)
......@@ -118,11 +120,11 @@ $s,h \models t_1 \pto t_2$ iff $\exists n\in\NN$ s.t.
\item
$s,h \models \hls{\ell+1}(t_1, t_2;t^\infty)$ iff
$s,h \models
\exists x'\cdot 2 \le x'-x \land \Pi' : x\pto x'-x\ \sepc
\blk(x+1,x') \sepc \hls{\ell}(t_1,t_2;t^\infty),
\exists z\cdot 2 \le z-t_1 \land \Pi' : t_1\pto z-t_1\ \sepc
\blk(t_1+1,z) \sepc \hls{\ell}(z,t_2;t^\infty),
$
where if $t^\infty\equiv\infty$, then $\Pi'\equiv x=x$, otherwise,
$\Pi' \equiv x'-x \le t^\infty$,
where if $t^\infty\equiv\infty$, then $\Pi'\equiv \top$, otherwise,
$\Pi' \equiv z-t_1 \le t^\infty$,
\item
$s,h \models \Sigma_1 \sepc \Sigma_2 \mbox{ iff }
......@@ -147,14 +149,14 @@ because we consider that the location $y$ is the first after the last location i
%
Intuitively, an atom $\hls{}(x,y;v)$ with $v$ a variable
defines a heap lists where all chunks have sizes between $2$ and the value of $v$.
Notice that if $v < 2$ then the atom $\hls{}(x,y;v)$ has no model and is unsatisfiable.
Notice that if $v < 2$ then the atom $\hls{}(x,y;v)$ has a model iff $x=y$.\mihaela{r2 CADE}
%
With this semantics, the $\blk$ and $\hls{}$ predicates are compositional predicates~\cite{EneaSW15} and therefore they satisfy the following composition lemmas:
With this semantics, the $\blk$ and $\hls{}$ predicates are compositional predicates~\cite{EneaSW15} and therefore they satisfy the following composition lemmas:\mihaela{r2 CADE}
%it is easy to show the following lemmas:
\begin{align}
\blk(x,y)\sepc\blk(y,z) \models & ~\blk(x,z) \label{lemma:blk}
\\
\hls{}(x,y;v)\sepc\hls{}(y,z;v) \models & ~\hls{}(x,z;v) \label{lemma:hls}
\hls{}(x,y;v_1)\sepc\hls{}(y,z;v_2) \models & ~\hls{}(x,z;\max(v_1,v_2)) \label{lemma:hls}
\end{align}
%%i.e., such block definition is compositional.
%Similarly to \cite{BrotherstonGK17}, the block predicate may be employed
......
......@@ -62,7 +62,7 @@ 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 = t \land t < e \land sz_0 < rsz
& \triangleq & 0 < b \land b = t \land t < e \land sz_0 < rsz
\\
& \land & sz_0 = t_1 - t \land 2 \le t_1 - t
\nonumber \\
......@@ -107,7 +107,9 @@ predicate $\hls{}$ defined inductively by the following two rules:
\hls{}(x, y; v) & \Leftarrow x=y : \emp \\
\label{eq:hlsv-rec}
\hls{}(x, y; v) & \Leftarrow \exists z \cdot 2 \le z - x \le v :
x \pto z-x \sepc \blk(x+1,z) \sepc \hls{}(z,y; v)
x \pto z-x \sepc \blk(x+1,z) \sepc \hls{}(z,y; v) \\
\label{eq:hlsv-infty}
\hls{}(x, y) & \equiv \hls{}(x,y;\infty) \mbox{ i.e., no upper bound on chunks' sizes}
\end{align}
stating that a heap list from $x$ to $y$ is
either an empty heap if $x$ and $y$ are aliased,
......@@ -124,8 +126,8 @@ stating that a heap list from $x$ to $y$ is
% as a third parameter, i.e., $\hls{}(x,y;v)$;
%therefore $\hls{}(x,y)$ is a shorthand for $\hls{}(x,y;\infty)$.
The parameter $v$ is an upper bound on the size of all chunks in the list.
By convention, $\hls{}(x,y)$ is a shorthand for $\hls{}(x,y;\infty)$, i.e,
the chunks' sizes are unconstrained from above.
%By convention, $\hls{}(x,y)$ is a shorthand for $\hls{}(x,y;\infty)$, i.e,
%the chunks' sizes are unconstrained from above.
The formula $\texttt{path}_{\texttt{4-9}}$ is generated by
the symbolic execution of \lst{search}
......@@ -142,20 +144,25 @@ a state satisfying \texttt{pre}.
The decision procedure for the satisfiability of \slah\
in Section~\ref{sec:sat-hls} is based
on the translation of $\varphi$ into
on the translation of a \slah\ formula $\varphi$ into
an equi-satisfiable Presburger arithmetic (\PbA) formula $\varphi^P$.
The delicate point
with respect to the previous work, e.g., \cite{DBLP:journals/corr/abs-1802-05935},
is to compute a summary in \PbA\ for the $\hls{}$ atoms.
% what happens if over/under-approximation?
% what happens if conditions are not satisfied? undecidability?
The summary computed for the atom $\hls{}(x,y;v)$ is
$(v=2 \land \exists k\cdot k > 0 \land 2k = y - x) \lor (2 < v \land 2 < y-x)$
when the heap it denotes is not empty.
The summary computed for the atom $\hls{}(x,y;v)$
when the heap it denotes is not empty
is
$(v=2 \land \exists k\cdot k > 0 \land 2k = y - x) \lor (2 < v \land 2 < y-x)$,
i.e., either all chunks have size 2 and the heap-list has an even size or
$v$ and the size of the heap-list are strictly greater than 2.
For the empty case, the summary is trivially $x=y$.
For $v=\infty$, the summary is $2 < y-x$.
The other spatial atoms $A$ are summarized by constraints on their start address
denoted by $\atomhead(A)$ and their end address $\atomtail(A)$.
%For $v=\infty$, the summary is $2 < y-x$.
The other spatial atoms $a$ (e.g., $x \pto v$ and $\blk(x,y)$)
are summarized by constraints on
their start address denoted by $\atomhead(a)$ (e.g., $x$) and
their end address $\atomtail(a)$ (e.g., $x+1$ resp. $y$).
For the points-to atom, this constraint is true,
but for the $\blk(x,y)$ atom, the constraint is
$x = \atomhead(a) < \atomtail(a) = y$.
......
Dear Mihaela,
We regret to inform you that your paper ...
Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
... has been not accepted for presentation at CADE-28. Of the 76 papers
submitted we accepted only 36 for the conference. The program committee
had extensive discussions about the submitted papers, to identify high
quality research that is ready for publication. Regrettably, they have
determined that your paper is not ready at this time. The reviews for
your paper, including responses to your rebuttal, are attached. We hope
you will be able to use the feedback from your reviewers to improve your
paper for successful future publication. (We have not included the
reviewers' scores, as they do not reflect the full extent of the discussions
of the reviewers and other PC members.)
We hope you will attend CADE-28, and enjoy the program - registration for
the conference will open soon.
Regards,
Geoff & Andre
SUBMISSION: 92
TITLE: Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
----------------------- REVIEW 1 ---------------------
SUBMISSION: 92
......
......@@ -52,7 +52,7 @@ that encodes its satisfiability:
\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 Also, the predicate atoms $\hls{}(t_1, t_2; t_3)$ are encoded by a formula in {\EPbA}, $\abs^+(\hls{}(t_1, t_2; t_3))$.
\item Lastly, the separating conjunction is encoded by an {\EPbA} formula constraint the address terms of spatial atoms.
\item Lastly, the separating conjunction is encoded by an {\EPbA} formula constraining the address terms of spatial atoms.
\end{compactitem}
The Appendix~\ref{app:sat-hls} provides more details.
%
......@@ -99,7 +99,11 @@ $\exists k.\ k \ge 1 \wedge 2 k \le t_2 - t_1 \le k t_3$ can actually be turned
\begin{lemma}[Summary of $\hls{}$ atoms]
Let $ \hls{}(x, y; z)$ be an atom in \slah\
representing a non-empty heap, where $x, y, z$ are three distinct variables in $\cV$.
Then there is an {\EPbA} formula, denoted by $\abs^+(\hls{}(x,y; z))$, which summarizes $\hls{}(x, y; z)$, namely 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)$.
%Then there is an {\EPbA} formula, denoted by $\abs^+(\hls{}(x,y; z))$,
We can construct in polynomial time an {\EPbA} 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)$.
%Similarly for $ \hls{}(x, y; \infty)$ and $ \hls{}(x, y; d)$ with $d \in \NN$.
\end{lemma}
......@@ -152,8 +156,7 @@ To sum up, we obtain
\vspace{-2eX}\qed
\end{proof}
The formula $\abs(\varphi)$ is constructed in polynomial time from $\varphi$.
Moreover, it is essentially a quantifier-free \PbA\ formula containing modulo constraints $t_1 \equiv r \bmod n$; the satisfiability of such formulas is still NP-complete.
The formula $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints $t_1 \equiv r \bmod n$; the satisfiability of such formulas is still 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)$.
Therefore, the satisfiability problem of \slah\ is in NP.
......
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