intro.tex 9.97 KB
 Mihaela SIGHIREANU committed Jun 15, 2021 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$,  Mihaela SIGHIREANU committed Jun 15, 2021 16 points-to constraints $x\pto v$ expressing that the value $v$ is stored at the address $x$,  Mihaela SIGHIREANU committed Jun 15, 2021 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 committed Jun 19, 2021 29 However, pointer arithmetic is widely used in low-level programs  Mihaela SIGHIREANU committed Jun 15, 2021 30 31 to access data inside memory blocks. Memory allocators are such low-level programs. %  Mihaela SIGHIREANU committed Jun 19, 2021 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.  Mihaela SIGHIREANU committed Jun 15, 2021 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 committed Jun 19, 2021 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.  Mihaela SIGHIREANU committed Jun 15, 2021 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 committed Jun 19, 2021 48 This motivates us to raise the following research question: \emph{Can decision procedures be achieved for separation logic fragments allowing heap lists}?  Mihaela SIGHIREANU committed Jun 15, 2021 49 50 51 52 53  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mypar{Contribution.}  ehilin02 committed Jun 19, 2021 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.  Mihaela SIGHIREANU committed Jun 15, 2021 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 committed Jun 19, 2021 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}.  Mihaela SIGHIREANU committed Jun 15, 2021 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 committed Jun 19, 2021 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.}  Mihaela SIGHIREANU committed Jun 15, 2021 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}.  Mihaela SIGHIREANU committed Jun 19, 2021 121 Section~\ref{sec:conc-hls} provides a summary of related work and concludes.  Mihaela SIGHIREANU committed Jun 15, 2021 122 123 %by a comparison of our work with existing fragments and its impact on verification of memory allocators.