@@ -21,7 +21,7 @@ Let us briefly summarize the results on the SH fragments in the sequel.

For the SH fragment with the singly linked list-segment predicate, arguably the simplest SH fragment, its satisfiability and entailment problems have been shown to be in PTIME~\cite{CookHOPW11} and efficient solvers have been developed for it~\cite{SLCOMPsite}.

%

The situation changes for more complex inductive predicates:

The satisfiability problem for the SH fragment with a class of general inductive predicates was shown to be EXPTIME-complete~\cite{DBLP:conf/csl/BrotherstonFPG14}. On the other hand, the entailment problem for the SH fragment with slightly less general inductive predicates was shown to be 2-EXPTIME-complete~\cite{KatelaanMZ19,DBLP:conf/lpar/EchenimIP20}.

The satisfiability problem for the SH fragment with a class of general inductive predicates was shown to be EXPTIME-complete~\cite{IosifRS13,DBLP:conf/csl/BrotherstonFPG14}. On the other hand, the entailment problem for the SH fragment with slightly less general inductive predicates was shown to be 2-EXPTIME-complete~\cite{KatelaanMZ19,DBLP:conf/lpar/EchenimIP20}.

@@ -6,13 +6,13 @@ 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}, \textsc{DRYAD}~\cite{DBLP:conf/pldi/PekQM14

}or \textsc{Hip}~\cite{DBLP:conf/atva/HeQLC09} for deductive verification.

and \textsc{VeriFast}~\cite{verifast}, \textsc{DRYAD}~\cite{DBLP:conf/pldi/PekQM14}

or \textsc{Hip}~\cite{DBLP:conf/atva/HeQLC09} for deductive verification.

The \emph{symbolic heap} (SH) fragment

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

because it provides a good compromise between expressivity

and tractability.

%The \emph{symbolic heap} (SH) fragment

%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$,

...

...

@@ -20,55 +20,59 @@ and tractability.

% 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 $\ls{}(x,y)$

specifying acyclic singly linked list segments between address $x$ and $y$.

%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 $\ls{}(x,y)$

%specifying acyclic singly linked list segments between address $x$ and $y$.

%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 predicate's arity

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

%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

%in general and NP-complete if the predicate's arity

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

In the category of built-in predicate,

the memory block predicate $\blk(x,y)$ used in this paper

has been introduced in \cite{CalcagnoDOHY06}

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

as part of the Array Separation Logic (ASL)~\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 shown to be decidable for

satisfiability and entailment.

The decisions procedures proposed have been implemented in the solver SLar~\cite{KimuraT17}, which is not publicly available.

%

Le~\cite{DBLP:conf/vmcai/Le21} identified two fragments of ASL allowing

inductive definitions for which the satisfiability (but not entailment) problem

is decidable.

However, the ASL fragment or its above extensions are not expressive enough

to specify the heap list data structure.

%In the category of built-in predicatex,

%the memory block predicate $\blk(x,y)$ used in this paper

%has been introduced in \cite{CalcagnoDOHY06}

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

%as part of the Array Separation Logic (ASL)~\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 shown to be decidable for

%satisfiability and entailment.

%The decisions procedures proposed have been implemented in the solver SLar~\cite{KimuraT17}, which is not publicly available.

%%

%Le~\cite{DBLP:conf/vmcai/Le21} identified two fragments of ASL allowing

%inductive definitions for which the satisfiability (but not entailment) problem

%is decidable.

%However, the ASL fragment or its above extensions are not expressive enough

%to specify the heap list data structure.

Although other fragments of separation logic has been used

in the static analysis of memory allocators~\cite{CalcagnoDOHY06}

or in their deductive verification~\cite{Chlipala11,MartiAY06},

the decidability of verification problem has not been studied

because these tools either employed sound heuristics or

interactive theorem provers.

The static analysis of memory allocators using separation logic was the focus of

several works starting with the pioneering work of~\cite{CalcagnoDOHY06}.

For example, \cite{LiuR15} defined an abstract domain for the analysis of array properties and applies it to the Minix 1.1 memory allocator, which uses chunks of fixed size. Also, \cite{BinS16} employed an extension of SL with data words and overlapping separating conjunction to analyze free list memory allocators.

In these analyzers, the decidability of verification problem has not been studied

because these tools employ sound heuristics to decide satisfiability or entailment problems.

Deductive verification of memory allocators has been considered in

several works~\cite{Chlipala11,MartiAY06,AppelN20} based on ad-hoc solvers

or interactive theorem provers. In \cite{Chlipala11}, a Coq library based on separation logic is presented and used to verify an implementation of malloc.

Separation logic is also used in~\cite{AppelN20} to verify the functional correctness

of an malloc implementation Verified Software Toolchain within the Coq proof assistant.

%A special instance where all chunks have the same size