intro.tex 9.97 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
%!TEX root = aplas2021.tex

\section{Introduction}

%\vspace{-2mm}
\mypar{Context.}
Separation Logic (SL, \cite{Reynolds:2002,OHearn19}), an extension of Hoare logic, is a well-established formalism for the verification of heap manipulating programs. SL features a \emph{separating conjunction operator} and \emph{inductive predicates}, which allow to express how data structures are laid out in memory in an abstract way. Since its introduction, various verification tools based on separation logic have been developed. A notable one among them is the INFER tool \cite{CD11}, which was acquired by Facebook in 2013 and has been actively used in its development process \cite{CDD+15}. 

Decision procedures for separation logic formulas are vital for the automation of the verification process.
%
These decision procedures mostly focused on separation logic fragments called \emph{symbolic heaps} (SH)~\cite{BerdineCO04}, since they provide a good compromise between expressivity and tractability. 
%
The SH fragments comprise existentially quantified formulas that are 
conjunctions of atoms encoding 
aliasing constraints $x = y$ and $x \neq y$ between pointers $x$ and $y$, 
16
points-to constraints $x\pto v$ expressing that the value $v$ is stored at the address $x$, 
17
18
19
20
21
22
23
24
25
26
27
28
and predicate atoms $P(\vec{x})$ defining (usually unbounded) memory regions of a particular structure. The points-to and predicate atoms, also called spatial atoms,
are composed using the separating conjunction to specify the disjointness of memory blocks they specify.

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}. 
%

\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.
Mihaela SIGHIREANU's avatar
Mihaela SIGHIREANU committed
29
However, pointer arithmetic is widely used in low-level programs 
30
31
to access data inside memory blocks. Memory allocators are such low-level programs. 
%
Mihaela SIGHIREANU's avatar
Mihaela SIGHIREANU committed
32
33
34
35
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. 
36
37
38
%
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. 
Mihaela SIGHIREANU's avatar
Mihaela SIGHIREANU committed
39
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.
40
41
42
43
44
45
46
47
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 
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.
%
Mihaela SIGHIREANU's avatar
Mihaela SIGHIREANU committed
48
This motivates us to raise the following research question: \emph{Can decision procedures be achieved for separation logic fragments allowing heap lists}?
49
50
51
52
53

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

\mypar{Contribution.}
ehilin02's avatar
intro    
ehilin02 committed
54
55
In this work, we propose decision procedures for a fragment of separation logic called {\slah}, which allows some form of pointer arithmetic inside inductive definitions, 
so that the inductive predicate specifying heap lists can be defined. 
56
57
58
59
60
61
62
We consider both satisfiability and entailment problems and show that they are NP-complete and coNP-complete respectively. 
The decision procedure for satisfiability is obtained by computing an equi-satisfiable abstraction in Presburger arithmetic, whose crux is to show that the summaries of the heap list predicates, which are naturally formalized as existentially quantified non-linear arithmetic formulas, can actually be transformed into Presburger arithmetic formulas. 
The decision procedure for entailment, on the other hand, reduces the problem to multiple instances of an ordered entailment problem, where all the address terms of spatial atoms are ordered. 
The ordered entailment problem is then decided by matching each spatial atom in the consequent to some spatial formula obtained from the antecedent by partitioning and splitting the spatial atoms according to the arithmetic relations between address variables.
Splitting a spatial atom into multiple ones in the antecedent is attributed to pointer arithmetic and unnecessary for SH fragments with nominal addresses. 
%Moreover, the availability of $\hls{}$ makes the splitting more involved.

ehilin02's avatar
intro    
ehilin02 committed
63
We implemented the decision procedures on top of \cspen\footnote{We anonymize the name of the tool to comply with the double blind procedure.} solver~\cite{GuCW16}. 
64
65
66
We evaluate the performance of the new solver, called {\cspenp}~\cite{CompSpenSite}, 
on a set of formulas originating from path conditions and verification conditions of programs working on heap lists in memory allocators. 
We also randomly generate some formulas, in order to test the scalability of {\cspenp} further.
ehilin02's avatar
intro    
ehilin02 committed
67
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.}
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120

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. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\hide{
The first part of our contributions is a theoretical study 
of the decision problems for ASL extended with 
the $\hls{}$ predicate. 
%We consider several
%versions of this predicate that lead to decidability of satisfiability and entailment problems. 
We propose decision procedures based on abstractions in Presburger arithmetic.
The second part of the contribution is experimental.
We implemented the decision procedures in a solver and
we applied it on a set of formulas originating from 
	path conditions and verification conditions of programs working on heap-lists. 
We also push the solver in the corner cases of our decision procedures
by providing randomly generated problems for each case.
This study is original to our knowledge, although the separation logic
	with heap-list has been used in 
	static analysis~\cite{CalcagnoDOHY06}
	and deductive verification~\cite{Chlipala11,MartiAY06}
	of memory allocators. Indeed, such work uses sound procedures 
	or interactive theorem provers and does not consider the decision problem.
The logic ASL has been introduced in~\cite{BrotherstonGK17} 
	where no inductively defined predicate is used.
An extension of ASL called SLA is considered 
	in~\cite{DBLP:journals/corr/abs-1802-05935} 
	where the only inductive predicate is the classic singly linked list $\ls{}$.
This year, \cite{DBLP:conf/vmcai/Le21} proposed a decision procedure dealing
    with satisfiability of ASL extended with inductively defined predicates. 
    The idea is to compute a so-called base formula for predicate atoms 
    that is enough for deciding satisfiability. 
Our class of heap-list predicates is a strict sub-class of inductive definitions
	considered in \cite{DBLP:conf/vmcai/Le21}, but we are able to compute an exact
    summary of the predicate atoms which is used in both satisfiability and
    entailment decision procedures.
%Our work extends ASL and demonstrates that adding the $\hls{}$ predicate requires 
%	a special translation
%	to obtain a linear constraint for the summary of $\hls{}$ atoms
%	and to match such atoms for deciding the entailment.
}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\mypar{Organization.}
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}.
%
The implementation details and the experimental evaluation
	are reported in Section~\ref{sec:exp-hls}.
121
Section~\ref{sec:conc-hls} provides a summary of related work and concludes.
122
123
%by a comparison of our work with existing fragments and its impact on verification of memory allocators.