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

@@ -26,20 +26,17 @@ The satisfiability problem for the SH fragment with a class of general inductive

\mypar{Motivation.}

Vast majority of the work on the verification of heap manipulating programs based on SL assumes that the addresses are \emph{nominal}, that is, they can be compared with only equality or disequality, but not ordered or obtained by arithmetic operations.

However, pointer arithmetic is widely used in low-level programs % , e.g. memory allocators.

However, pointer arithmetic is widely used in low-level programs

to access data inside memory blocks. Memory allocators are such low-level programs.

%Such programs usually use pointer variables to refer to the start addresses of memory regions and use arithmetic expressions on these variables to visit the memory cells inside these regions.

They assume that the memory is organized into a linked list of memory chunks,

called heap lists in this paper; pointer arithmetic is

%where arithmetic expressions are

used to jump from a memory chunk to the next one \cite{Knuth97,WJ+95}.

%We call this data structure as heap lists in the sequel.

%

%One of the fundamental data structures used in these programs are heap lists

Classic implementations of memory allocators~\cite{Knuth97,WJ+95}

organize the heap into a linked list of memory chunks,

called heap lists in this paper; pointer arithmetic is

used to jump from a memory chunk to the next one.

%

There have been some work to use separation logic for the static analysis and deductive verification of these low-level programs~\cite{CalcagnoDOHY06,MartiAY06,Chlipala11}.

Moreover, researchers have also started to investigate the decision procedures for separation logic fragments containing pointer arithmetic.

For instance, \emph{Array separation logic} (ASL) was proposed in~\cite{BrotherstonGK17}, which includes pointer arithmetic, the constraints $\blk(x,y)$ denoting a block of memory units from the address $x$ to $y$, as well as the points-to constraints $x\pto v$. It was shown in~\cite{BrotherstonGK17} that for ASL, the satisfiability is NP-complete and the entailment is in coNEXP resp. coNP for quantified resp. quantifier-free formulas.

For instance, \emph{Array separation logic} (ASL) was proposed in~\cite{BrotherstonGK17}, which includes pointer arithmetic, the constraints $\blk(x,y)$ denoting a block of memory units from the address $x$ to $y$, as well as the points-to constraints $x\pto v$. It was shown in~\cite{BrotherstonGK17} that for ASL, the satisfiability is NP-complete and the entailment is in coNEXP (resp. coNP) for quantified (resp. quantifier-free) formulas.

Furthermore, the decidability can be preserved even if ASL is extended with the list-segment predicate~\cite{DBLP:journals/corr/abs-1802-05935}.

Very recently, Le identified in~\cite{DBLP:conf/vmcai/Le21} two fragments

of ASL extended with a class of general inductive predicates for which

...

...

@@ -47,89 +44,9 @@ the satisfiability (but not entailment) problem is decidable.

Nevertheless, none of the aforementioned work is capable of reasoning about heap lists, or generally speaking, pointer arithmetic inside inductive definitions, in a \emph{sound and complete} way. The state-of-the-art static analysis and verification tools, e.g. \cite{CalcagnoDOHY06,Chlipala11,MartiAY06}, resort to sound (but incomplete) heuristics or interactive theorem provers, for reasoning about heap lists.

On the other hand, the decision procedures for ASL or its extensions, e.g. \cite{BrotherstonGK17,DBLP:journals/corr/abs-1802-05935,DBLP:conf/vmcai/Le21}, are unable to tackle heap lists.

%\footnote{The fact that heap lists are beyond the two decidable fragments in~\cite{DBLP:conf/vmcai/Le21} was confirmed by a personal communication with the author of \cite{DBLP:conf/vmcai/Le21}.}.

This motivates us to raise the following research question: \emph{Can decision procedures be achieved for separation logic fragments allowing heap lists}?

%Separation logic~\cite{Reynolds:2002,OHearn19}

%has a big impact on the verification or static analysis of programs

%manipulating the dynamic memory. Performant tools have been developed

%based on this formalism, among which we cite

%\textsc{Infer}~\cite{DBLP:journals/cacm/DistefanoFLO19} for static analysis

%and \textsc{VeriFast}~\cite{verifast} for deductive verification.\todo{MS: change tool}

The \emph{symbolic heap} (SH) fragment \todo{MS: change motivation}

of separation logic has been introduced in~\cite{BerdineCO04}

because it provides a good compromise between expressivity

and tractability. This fragment includes existentially quantified formulas

which are conjunctions of

aliasing constraints $x = y$ and $x \neq y$ between pointers $x$ and $y$,

and heap constraints $x\pto v$ expressing that at the address $x$ is allocated

a memory zone containing the value $v$.

The separating conjunction composes the heap constraints by ensuring

that the allocated memory blocks are disjoint.

To capture properties of heaps with unbounded data structures, the SH fragment is

extended with predicates that may be inductively defined using SH formulas or

defined by the semantics, i.e., built-in.

The first category includes the predicate specifying acyclic singly linked list segments defined by the following two rules:

\begin{eqnarray}

\ls{}(x,y) &\Leftarrow& x = y : \emp\label{eq:ls-0}\\

\ls{}(x,y) &\Leftarrow&\exists x'\cdot x \neq y : x \pto x' \sepc\ls{}(x',y) \label{eq:ls-rec}

\end{eqnarray}

The satisfiability problem for the SH fragment with the $\ls{}$ predicate is in PTIME~\cite{CookHOPW11} and efficient solvers have been implemented for it~\cite{SLCOMPsite}.

This situation changes for more complex definitions of predicates,

but still there are decidable fragments for which the satisfiability problem

is EXPTIME~\cite{DBLP:conf/lpar/EchenimIP20,DBLP:conf/lpar/KatelaanZ20}

% PSPACE~\cite{IosifRS13}.

in general and NP-complete if the arity of the predicate

is bound by a known constant~\cite{DBLP:conf/csl/BrotherstonFPG14}.

%

In the second category of predicates, one which is of interest for this paper

is the memory block predicate $\blk(x,y)$ introduced in \cite{CalcagnoDOHY06}

to capture properties of memory allocators. This predicate has been formalized

as part of the \emph{array separation logic} (ASL)

introduced in~\cite{BrotherstonGK17}.

The predicate denotes a block of memory units (bytes or integers)

between addresses $x$ and $y$. It is usually combined with

pointer arithmetics allowing to compute addresses in the memory blocks.

This combination is enough to increase the complexity class of the

decision problems in ASL: the satisfiability is NP-complete,

the bi-abduction is NP-hard and

the entailment is EXPTIME resp. coNP-complete for quantified resp. quantifier-free formulas~\cite{BrotherstonGK17}.

The ASL fragment extended with the $\ls{}$ predicate has been studied

in~\cite{DBLP:journals/corr/abs-1802-05935}, and it is decidable for

satisfiability and entailment.

This motivates us to raise the following research question: \emph{Can decision procedures be achieved for separation logic fragments allowing heap lists}?

Still, the ASL fragment or its extension with $\ls{}$ are not expressive enough

to specify the heap list data structure that is defined by the following rules:

\begin{eqnarray}

\hls{}(x,y) &\Leftarrow& x = y : \emp\label{eq:hls-0}\\

@@ -150,9 +67,6 @@ We also randomly generate some formulas, in order to test the scalability of {\c

The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (in average, less than 1 second for satisfiability and less than 15 seconds for entailment).\zhilin{The anonymization is properly done.}

To the best of our knowledge, this work presents the first decision procedure and automated solver for decision problems in a separation logic fragment allowing both pointer arithmetic and memory blocks inside inductive definitions.

%As mentioned before, the logic ASL was introduced in~\cite{BrotherstonGK17}, but it contains no inductive predicates.

%As mentioned before, an extension of ASL with the classic singly linked list $\ls{}$ was considered in~\cite{DBLP:journals/corr/abs-1802-05935}

% where the only inductive predicate is the classic singly linked list $\ls{}$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%

...

...

@@ -197,17 +111,13 @@ Our class of heap-list predicates is a strict sub-class of inductive definitions

%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mypar{Organization.}

%The remainder of this paper is structured as follows.

A motivating example and an overview of the decision procedures are provided in Section~\ref{sec:over-hls}.

The logic {\slah} is defined in Section~\ref{sec:logic-hls}.

%

Then the decision procedures for the satisfiability and entailment problems are presented in Sections~\ref{sec:sat-hls}\resp~\ref{sec:ent}.

%

%Section~\ref{sec:sat-wfid} extends the satisfiability results to \slah\ with

% well-formed inductive definitions of heap-lists.

%

The implementation details and the experimental evaluation

are reported in Section~\ref{sec:exp-hls}.

%Finally, the conclusion is given in Section~\ref{sec:conc-hls}.

Section~\ref{sec:conc-hls} provides a summary of related works and concludes.

%by a comparison of our work with existing fragments and its impact on verification of memory allocators.