Commit 646d9c0e authored by ehilin02's avatar ehilin02
Browse files

entailment

parent fef23d9b
...@@ -49,13 +49,14 @@ In Section~\ref{ssec:ent-1}, we consider the special case ...@@ -49,13 +49,14 @@ In Section~\ref{ssec:ent-1}, we consider the special case
The general case is dealt with in Section~\ref{ssec:ent-all}; The general case is dealt with in Section~\ref{ssec:ent-all};
the procedure calls the special case for the first atom of the consequent with the procedure calls the special case for the first atom of the consequent with
all the compatible prefixes of the antecedent, and all the compatible prefixes of the antecedent, and
it does a recursive call for the remainders of the consequent and the antecedent. Note that to find all the compatible prefixes of the antecedent, some spatial atoms in the antecedent might be split into several ones. it does a recursive call for the remainders of the consequent and the antecedent. Note that to find all the compatible prefixes of the antecedent, some spatial atoms in the antecedent might be split into several ones. We derive the coNP upper bound from the aforementioned decision procedure as follows:
The coNP upper bound is explained in the sequel: \begin{enumerate}
1) the original entailment problem is reduced to at most exponentially many ordered entailment problems since there are exponentially many total preorders, \item The original entailment problem is reduced to at most exponentially many ordered entailment problems since there are exponentially many total preorders.
2) each ordered entailment problem can be reduced further to exponentially many special ordered entailment problems where there is one spatial atom in the consequent, \item Each ordered entailment problem can be reduced further to exponentially many special ordered entailment problems where there is one spatial atom in the consequent.
3) the original entailment problem is invalid iff there is an invalid special ordered entailment problem instance, \item The original entailment problem is invalid iff there is an invalid special ordered entailment problem instance.
4) the special ordered entailment problem is in coNP. \item The special ordered entailment problem is in coNP.
\end{enumerate}
%At first, it is easy to observe that if $\abs(\varphi)$ is unsatisfiable, %At first, it is easy to observe that if $\abs(\varphi)$ is unsatisfiable,
%then the entailment holds. Moreover, if $\abs(\varphi) \not\models \abs(\psi)$, %then the entailment holds. Moreover, if $\abs(\varphi) \not\models \abs(\psi)$,
%the the entailment $\varphi \models \psi$ does not hold. %the the entailment $\varphi \models \psi$ does not hold.
......
...@@ -136,7 +136,7 @@ lemma. ...@@ -136,7 +136,7 @@ lemma.
\mypar{Contribution.} \mypar{Contribution.}
In this work, we propose decision procedures for a fragment of separation logic called {\slah}, which allows pointer arithmetic inside inductive definitions, In this work, we propose decision procedures for a fragment of separation logic called {\slah}, which allows pointer arithmetic inside inductive definitions,
so that inductive predicates specifying heap lists can be defined. so that inductive predicates specifying heap lists can be defined.
We consider both satisfiability and entailment problems. 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 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 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. 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.
...@@ -147,7 +147,7 @@ We implemented the decision procedures on top of \cspen\ solver~\cite{GuCW16}. ...@@ -147,7 +147,7 @@ We implemented the decision procedures on top of \cspen\ solver~\cite{GuCW16}.
We evaluate the performance of the new solver, called {\cspenp}~\cite{CompSpenSite}, 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. 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. 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). The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (0.07 seconds for satisfiability and 5.02 seconds for entailment in average).
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. 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, the logic ASL was introduced in~\cite{BrotherstonGK17}, but it contains no inductive predicates.
......
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