Commit 51ef5a2d authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

start of APLAS 2021 version

parent a2b73ebe
%!TEX root = aplas021.tex
\begin{abstract}
Pointer arithmetic is widely used in low-level programs, e.g. memory allocators.
%
%The verification of such programs usually requires simultaneous reasoning about pointer arithmetic and unbounded heap regions.
The specification of such programs usually requires using pointer arithmetic inside inductive definitions to define the common data structures, e.g. heap lists in memory allocators.
%
In this work, we investigate decision problems for SLAH, a separation logic fragment
that allows some form of pointer arithmetic inside inductive definitions,
thus enabling specification of properties for programs manipulating heap lists,
a data structure used in memory allocators.
%
Pointer arithmetic inside inductive definitions is challenging for automated reasoning.
%
We tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas specifying heap lists data structures.
%
The crux of our decision procedure for satisfiability is to compute summaries of inductive definitions capturing heap lists. We show that although the summary is naturally expressed as an existentially quantified non-linear arithmetic formula, it can actually be transformed into an equivalent linear arithmetic formula.
%
The decision procedure for entailment, on the other hand, has to match and split the spatial atoms according to the arithmetic relation between address variables.
%
We report on the implementation of these decision procedures and their
good performance in solving problems issued from the verification of
building block programs used in memory allocators.
%
\hide{
We study the decidability of the verification problem for
an extension of the array separation logic (ASL)
allowing the specification of data structures like
pointers, memory blocks or heap-lists,
which are lists built inside memory blocks.
The logic, called \slah, adds to ASL %an
inductively defined predicates specifying singly linked heap-lists.
%
We show that the logic is suitable for the compositional verification
of programs manipulating heap-lists, e.g., memory allocators.
%
We propose decision procedures for satisfiability and entailment of \slah,
which are substantial extensions of those proposed for ASL
because they have to deal with pointer arithmetic inside inductive definitions.
%
Our decision procedures propose some new ideas to tackle this challenge.
The crux of our decision procedure for satisfiability is
to compute a summary of the inductive definition of the heap-list predicate.
We show that although the summary is expressed as
an existentially quantified non-linear arithmetic constraint,
it can actually be transformed into an equivalent linear arithmetic formula.
%
The decision procedure for entailment
uses the decision procedure for satisfiability as an oracle
and deals with the pointer arithmetic in the inductive definitions.
%
We implemented the decision procedures and
did experiments to evaluate their performance.
The experimental results demonstrate the effectiveness of the solver
for deciding problems issued from the verification
of heap-list manipulating programs.
}
\end{abstract}
\documentclass[runningheads,orivec]{llncs}
%% Packages
\usepackage{../latex/packages}
%% Macros
% for comments
\newcommand{\zhilin}[1]{\todo[color=blue!20,linecolor=black!60,size=\scriptsize]{Z: #1}}
\newcommand{\mihaela}[1]{\todo[color=green!20,linecolor=black!60,size=\scriptsize]{M: #1}}
% others
\input{../latex/commands.tex}
%% Title
%\title{Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions}
%\title{Decision Procedures for Heap-lists}
\title{On Automated Verification of Heap-lists}
%%
\author{%
Double Blind
%Wanyun Su\inst{2} \and
%Zhilin Wu\inst{2}\orcidID{0000-0003-0899-628X} \and
%Mihaela Sighireanu\inst{1}\orcidID{0000-0002-1925-089X}
}
\institute{%
Double Blind
% State Key Laboratory of Computer Science, \\
% Institute of Software, Chinese Academy of Sciences, China \\
% %\email{wuzl@ios.ac.cn}
%\and
% LMF, ENS Paris-Saclay, University Paris-Saclay and CNRS, France
% %\email{firstname.lastname@labmf.fr}
}
\date{}
%\authorrunning{W. Su, Z. Wu and M. Sighireanu}
\authorrunning{D. Blind}
\setlength{\parskip}{0eX}
\begin{document}
%------------------------------------------------------------------------------
\maketitle
\sloppy
%------------------------------------------------------------------------------
%\vspace{-4mm}
\input{abs.tex}
%------------------------------------------------------------------------------
%\vspace{-6mm}
\input{intro.tex}
%------------------------------------------------------------------------------
%% Overview of problems when reasoning about DMA
%\vspace{-2mm}
\input{overview.tex}
%------------------------------------------------------------------------------
%% Definition of the logic
%\vspace{-2mm}
\input{logic-hls.tex}
%------------------------------------------------------------------------------
%% The decision procedures for the satisfiability
%\vspace{-2mm}
\input{sat-hls.tex}
%------------------------------------------------------------------------------
%% The decision procedures for the satisfiability for wfid
%\input{sat-wfid.tex}
%------------------------------------------------------------------------------
%% The decision procedures for the entailment
%\vspace{-2mm}
\input{entail-hls.tex}
%------------------------------------------------------------------------------
%\vspace{-2mm}
\input{experiments.tex}
%------------------------------------------------------------------------------
%\vspace{-2mm}
\input{conclusion.tex}
%\newpage
%------------------------------------------------------------------------------
\bibliographystyle{../latex/splncs04}
\bibliography{../bibs/biblio}
\newpage
\appendix
%\section{Appendixes}
\input{app-sat-hls.tex}
%\input{app-ent-hls.tex}
%% temporary
%\newpage
%\setcounter{tocdepth}{3}
%\tableofcontents
\end{document}
%!TEX root = aplas2021.tex
\section{Complexity of the entailment problem}
Theorem~\ref{thm-entail} states that the upper bound of the entailment problem is \textsc{EXPTIME}.
The lower bound is given by the complexity of the entailment problem for quantifier free formulas in \textsc{ASL}, which is shown to be \textsc{coNP} in~\cite{BrotherstonGK17}.
\textbf{Claim:} The entailment problem in \slah\ is in \textbf{coNP}.
\begin{proof}
Let fix $\varphi \models \psi$ an entailment problem in \slah.
We build in polynomial time a \PbA\ formula $\chi$ from $\varphi$ and $\psi$
such that
for any stack $s$, $s\models \chi$
iff $\exists h.~s,h\models \varphi$ and $s,h \not\models \psi$.
We suppose that both formula $\varphi$ and $\psi$ have been transformed in normal form as follows:
\begin{itemize}
\item atoms $\hls{}(x,y;v')$ with $\abs(\varphi)\models (v'<2 \lor x=y)$ have been removed and replaced by $x=y$\mihaela{use $\xi$ ?}
\item atoms $\hls{}(x,y;v')$ with $\abs(\varphi)\models y-x=2 \land v' \ge 2$ have been replaced by $\exists z.~ z \le v' \land y-x=2 : ~x\pto z \star \blk(x+1,y)$
\item ...\mihaela{TODO}
\end{itemize}
The normalization can be done in a linear number of calls to the \EPbA\ procedure.
The formula $\chi$ shall ensure that $\varphi$ is satisfiable, so
it contains as conjunct $\abs(\varphi)$.
The entailment may be invalid iff one of the following holds:
\begin{enumerate}
\item $\psi$ is not satisfiable, i.e., $\abs(\psi)$ is not satisfiable.
\item there exists an address inside a spatial atom of $\varphi$
which is not inside a spatial atom of $\psi$;
we denote this formula by $cov(\varphi,\psi)$;
\item similarly, $cov(\psi,\varphi)$ (the semantics is non intuitionistic),
\item a points-to or a heap-list atom of $\psi$ ``covers'' a domain of addresses
which is inside the one of a block atom of $\varphi$;
we denote this formula by $nblk(\varphi,\psi)$;
\item a points-to atom of $\psi$ defines an address inside (strictly)
a heap-list atom of $\varphi$;
we denote this formula by $npto(\varphi,\psi)$;
\item a points-to atom $x\pto v$ of $\psi$ defines the same address as the start address
of a heap-list atom $\hls{}(x,y;v')$ in $\varphi$;
we denote this formula by $npto'(\varphi,\psi)$;
(this is true because we are in the normal form);
\item a points-to atoms $x\pto v$ of $\psi$ defines the same address as a
points-to atom $x\pto v'$ of $\varphi$ but $v\neq v'$;
\item a heap-list atom $\hls{}(x,y;v')$ of $\psi$ starts at an address at which is defined a points-to atom $x\pto v$ of $\varphi$ such that $v> v'$;
\item a heap-list atom $\hls{}(x,y;v')$ of $\psi$ ``covers'' the domain of
addresses if an atom $\hls{}(z,w;v)$ of $\varphi$ but $v' < v$;
\item a heap-list atom $\hls{}(x,y;v')$ of $\psi$ ``covers'' a domain of addresses
that can not be filded into a $\hls{}$ atom with chunks of maximal size less or equal to $v'$\mihaela{difficult in P!}
\end{enumerate}
\end{proof}
%!TEX root = aplas2021.tex
\section{{\qfpa} abstraction for \slah\ formulas}\label{app:sat-hls}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{{\qfpa} summary of $\hls{}$ atoms}
\label{ssec:sat-hls-abs}
\noindent {\bf Lemma~\ref{lem-hls}}.
\emph{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 {\qfpa} 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)$. }
%Similarly for $ \hls{}(x, y; \infty)$ and $ \hls{}(x, y; d)$ with $d \in \NN$.
\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. 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.
%Let $t^\infty \equiv d_0 + \sum_{i=1}^n d_i v_i$
%with $d_i$ ($i\in\{0..n\}$) constants in $\NN$
% such that at least one $d_i > 0$ for $i\in\{1..n\}$,
%and $v_i$ ($i\in\{1..n\}$) variables in $\cV$.
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{itemize}
\item If $2 = z$, then $\abs^+(\hls{}(x, y; z))$ has the formula $\exists k.\ k \ge 1 \land y -x = 2k$, which is equivalent to the {\qfpa} formula $2 \le y -x \wedge y - x \equiv_2 0$, as a disjunct.
%
\item If $2 < z$, then we consider the following sub-cases:
\begin{itemize}
\item if $k = 1$
then $\abs^+(\hls{}(x, y; z))$ contains the formula
$ 2 \leq y-x \le z$ as a disjunct;
\item if $k \ge 2$, then we observe that the intervals
$[2k, k z]$ and $[2(k+1), (k+1) z]$
overlap.
Indeed,
\begin{eqnarray*}
k z - 2(k+1) & = &
k (z -2) - 2
\ge k - 2 \ge 0.
\end{eqnarray*}
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.
\end{itemize}
\end{itemize}
To sum up, we obtain
\begin{eqnarray*}
\abs^+(\hls{}(x, y; z)) & \triangleq
& \big(2 = z
~\land~ \exists k.\ k \ge 1 \land 2k = y-x \big) \\
& \lor & \big(2 < z
~\land~
\big(2 \leq y-x \le z \lor 4 \le y-x
\big)
\big),
\end{eqnarray*}
which can be further simplified into
\begin{eqnarray*}
\abs^+(\hls{}(x, y; z)) & \triangleq
& \big(2 = z \land 2 \le y -x \wedge y - x \equiv_2 0 \big) \\
& \lor & \big(2 < z
\land 2 \le y - x
\big).
\end{eqnarray*}
%
%If $t^\infty \equiv \infty$,
%then $\abs^+(A) \triangleq \exists k \cdot k \ge 1 \land k c \leq y-x$.
%
%For $ \hls{}(x, y; \infty)$, we replace $z$ in $\abs^+(\hls{}(x, y; z))$ by $\infty$, simplify the formula, and deduce that
%$\abs^+(\hls{}(x, y; \infty)) \triangleq 2 \le y - x $.
%
%For $ \hls{}(x, y; d)$ with $d \in \NN$, we replace $z$ in $\abs^+(\hls{}(x, y; z))$ by $d$,
%$$\abs^+(\hls{}(x, y; d)) \triangleq \exists k.\ k \ge 1 ~\land~ 2k \le y - x \le dk.$$
%\begin{eqnarray*}
%\abs^+(\hls{}(x, y; d)) & \triangleq
% & \big(2 = d
% ~\land~ \exists k.\ k \ge 1 \land 2k = y-x \big) \\
% & \lor & \big(2 < d
% ~\land~
% \big(2 \leq y-x \le z \lor 4 \le y-x
% \big)
% \big).%
%\end{eqnarray*}
%This constraint is unsatisfiable if $c > d_0$.
\qed
\end{proof}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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 {\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{}$.
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_*$
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.
\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, a_j \not \in \patoms}
\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 \not \in \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.
% satisfiability
%implies an existential quantification of free variables of the formulas.
\vspace{4mm}
\noindent {\bf Proposition~\ref{prop-sat-correct}}.
\emph{A \slah\ formula $\varphi$ is satisfiable iff $\abs(\varphi)$ is satisfiable.}
\smallskip
\begin{proof}
\emph{``Only if'' direction}:
Suppose that $\varphi$ is satisfiable.
Then there exists a stack $s$ and a heap $h$
such that $s,h \models \varphi$.
We show $s \models \abs(\varphi)$.
%We build an interpretation $I$ of free variables in
%$\abs(\varphi)$ by using $s$ for location variables.
The semantics of \slah\ implies that at least one disjunct in $\abs(a)$
is true for every predicate atom $a$. Therefore, $s \models \phi_\Sigma$. Moreover, $s \models \phi_\sepc$, as a result of the semantics of separating conjunction. Thus $s \models \abs(\varphi)$ and $\abs(\varphi)$ is satisfiable.
\smallskip
\noindent \emph{``If'' direction}: Suppose that $\abs(\varphi)$ is satisfiable.
Then there is an interpretation $s$ such that $s \models \abs(\varphi)$.
We build a heap $h$ from $s$ and $\varphi$ as follows:
\begin{itemize}
\item For each points-to atom $t_1 \pto t_2$ in $\varphi$, $h(s(t_1)) = s(t_2)$.
%
\item For each block atom $\blk(t_1, t_2)$ in $\varphi$, $h(n) = 1$ for each $n \in [s(t_1), s(t_2)-1]$.
%
\item For every predicate atom $\hls{}(t_1,t_2; t_3)$ in $\varphi$, we have $s \models \abs(\hls{}(t_1,t_2; t_3))$. Then either $s(t_1) = s(t_2)$ or $s(t_1) < s(t_2)$ and $s \models \abs^+(\hls{}(x, y; z))[t_1/x, t_2/y, t_3/z]$.
\begin{itemize}
\item For the first case, we let $h(s(t_1))$ undefined.
\item For the second case, $s \models (2 = t_3 \wedge t_1 < t_2 \wedge t_2 - t_1 \equiv 0 \bmod 2) \vee (2 < t_3 \wedge 2 \le t_2 - t_1)$.
\begin{itemize}
\item If $s(t_3) = 2$, then let $h(s(t_1) + 2(i-1)) = 2$ and $h(s(t_1) + 2i-1) = 1$ for every $i: 1 \le i \le \frac{s(t_2) - s(t_1)}{2}$.
\item If $s(t_3) > 2$, then from $s(t_2) - s(t_1) \ge 2$, we know that there is a sequence of numbers $n_1, \cdots, n_\ell$ such that $2 \le n_i \le s(t_3)$ for every $i \in [\ell]$ and $s(t_2) = s(t_1) + \sum \limits_{i \in [\ell]} n_i$. We then let $h(s(t_1) + \sum \limits_{j \in [i-1]} n_j) = n_i$ for every $i \in [\ell]$, and let $h(n') = 1$ for all the other addresses $n' \in [s(t_1), s(t_2)-1]$.
\end{itemize}
From the construction above, we know that the subheap of the domain $[s(t_1), s(t_2)-1]$ satisfies $\hls{}(t_1, t_2; t_3)$.
\end{itemize}
\end{itemize}
From the definition of $h$, we know that $s, h \models \varphi$. Therefore, $\varphi$ is satisfiable.
%Let $k$ be the number of these unfoldings and $k$ addresses in $[I(t_1),I(t_2)-1]$
%at distance between $[c,I(t^\infty)]$ denoting the start of chunks in this atom.
%The others values in the heap are chosen arbitrary.
%Therefore, we obtain a model for $\varphi$ which satisfies all the constraints in its semantics.
\qed
\end{proof}
% 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?
%Indeed, let $n$ be the initial number of variables and $\sigma$ the number of spatial atoms.
%The \PbA\ abstraction has $n+\sigma$ variables because of added boolean variables.
%The $\hls{}$ atoms produces a linear increase of the formula,
%and may introduce an existentially quantified variable.
%The biggest impact in the size of the abstraction is the translation of
%the separating conjunction, $\varphi_\sepc$, which size is in $O(\sigma)$.
\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 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}.
\end{remark}
\section{Proof of Lemma~\ref{lem-eub}}
\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)$ and $s[z \gets n] \not \models \xi_{eub,\varphi}(z)$ for all $n \neq \eub_\varphi(s)$.
}
\smallskip
\begin{proof}
From the construction of $\abs^+(\hls{}(t'_1, t'_2; t'_3))$ in Section~\ref{sec:sat-hls}, we know that for every store $s$, there is a heap $h$ such that $s, h \models \Pi: \hls{}(t'_1, t'_2; t'_3)$ iff $s \models \Pi \wedge \big((t'_3 = 2 \wedge 2 \le t'_2 - t'_1 \wedge t'_2 - t'_1 \equiv_2 0) \vee ( 2 < t'_3 \wedge 2 \le t'_2 - t'_1)\big)$. Then the fact that $z$ appears in some unfolding scheme of $\varphi$ w.r.t. some store $s$
can be specified by the formula
\[
\Pi \wedge
\left(
\begin{array}{l}
(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),
\]
where $t'_2 - t'_1 - z$ denotes the remaining size of the heap after removing a memory chunk of size $z$. Therefore, we define $\xi_{eub,\varphi}(z)$ as
\[
\begin{array}{l}
\Pi \wedge
\left(
\begin{array}{l}
(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 \\
\forall z'.\ z < z' \le t'_3 \rightarrow \neg (2 \le t'_2 - t'_1 - z' \vee t'_2 - t'_1 = z')
\end{array}
\right)
\end{array}
\right),
\end{array}
\]
where $ \forall z'.\ z < z' \le t'_3 \rightarrow \neg (2 \le t'_2 - t'_1 - z' \vee t'_2 - t'_1 = z') $ asserts that $z$ is the maximum chunk size upper bound among unfolding schemes of $\varphi$. The formula $ \forall z'.\ z < z' \le t'_3 \rightarrow \neg (2 \le t'_2 - t'_1 - z' \vee t'_2 - t'_1 = z') $ is equivalent to $ \forall z'.\ z < z' \le t'_3 \rightarrow (t'_2 - t'_1 - z' \le 1 \wedge t'_2 - t'_1 \neq z')$, and can be simplified into
$$
\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,
\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 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 \\
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
\end{array}
\right)
\end{array}
\right),
\]
which is a {\qfpa} formula.
\qed
\end{proof}
\section{Proof of Lemma~\ref{lem-hls-hls}}
\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
\forall z.\ \xi_{eub, \varphi}(z) \rightarrow z \le t_3$.
}
\smallskip
\begin{proof}
%
\noindent \emph{``Only if'' direction}: Suppose $\varphi \models_\preceq \psi$.
%\begin{itemize}
%\item For every interpretation $I$ such that $I \models \abs(\varphi) \wedge t'_1 = t'_2$,
%there are a model $s, h$ of $\varphi$ such that $s$ and $I$ agree on $\fv(\varphi)$ (where $h$ is empty). From $\varphi \models \hls{}(t_1, t_2; t_3)$, we know that $s, h \models \hls{}(t_1, t_2; t_3)$. Thus $s(t_1) = s(t_2)$ since $h$ is empty.
%
%\item
At first, we observe that $C_\preceq \wedge \abs(\varphi)$ and $\varphi$ contain the same number of variables.
Let $s$ be an interpretation such that $s \models C_\preceq \wedge \abs(\varphi)$. From $C_\preceq \models t'_1 < t'_2 \wedge t'_1 = t_1 \wedge t'_2 = t_2$, we have $s(t'_1) < s(t'_2)$, $s(t'_1) = s(t_1)$, and $s(t'_2) = s(t_2)$.
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$. 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 \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 \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}
%!TEX root = aplas2021.tex
\section{Conclusion}
\label{sec:conc-hls}
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 is coNP-complete.
%We propose decision procedure for both problems calling satisfiability