Commit 46a6db52 authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

revisit abstract and intro

parent 68d3878d
......@@ -4,14 +4,16 @@
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 verification of such programs usually requires using pointer arithmetic inside inductive definitions to define the common data structures, e.g. heap lists, in memory allocators.
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 a separation logic SLAH that allows pointer arithmetic inside inductive definitions, thus capable of specifying properties of programs manipulating heap lists.
In this work, we investigate decision problems for SLAH, a separation logic fragment
that allows pointer arithmetic inside inductive definitions,
thus enabling specification of properties for programs manipulating heap lists.
%a common data structure used in memory allocators.
%
Pointer arithmetic inside inductive definitions is challenging for automated reasoning.
%
We propose some new ideas to tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas.
We tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas.
%
The crux of our decision procedure for satisfiability is to compute summaries of inductive definitions. 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.
%
......
......@@ -6,9 +6,9 @@
\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 and constraint solvers for separation logic formulas are vital for the automation of the verification process.
Decision procedures for separation logic formulas are vital for the automation of the verification process.
%
These decision procedures and solvers mostly focused on separation logic fragments called \emph{symbolic heaps} (SH)~\cite{BerdineCO04}, since they provide a good compromise between expressivity and tractability.
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
......@@ -18,7 +18,7 @@ and predicate atoms $P(\vec{x})$ defining unbounded memory regions of a particul
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 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}.
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}.
......@@ -143,13 +143,13 @@ The ordered entailment problem is then decided by matching each spatial atom in
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.
We implemented the decision procedures on top of \cspen\ solver~\cite{GuCW16,CompSpenSite}.
We evaluate the performance of the new solver, called {\cspenp},
We implemented the decision procedures on top of \cspen\ solver~\cite{GuCW16}.
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.
The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (0.05 seconds for satisfiability and 2.57 seconds for entailment in average).
To the best of our knowledge, this work presents the first decision procedures and automated solvers for separation logic fragments allowing pointer arithmetic inside inductive definitions.
To the best of our knowledge, this work presents the first decision procedure and automated solver for entailment problems in a separation logic fragment allowing pointer arithmetic 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{}$.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment