Two corestar questions: abstraction in run_prover/non-termination of entailment check
Alexander Schremmer
I was playing around with corestar lately and have been encountering
these two problems:
1. I added the following line in parser.mly to the question rule:
| ABSRULE COLON formula_npv { Abs($3) }
and tried the attached files (example.file and example.logic) with
run_prover. Unfortunately, the abstraction rule does not seem to be
applied. Any idea why is that?
2. I tried to reproduce results from the paper [1] where they use jstar
to discharge entailments. One of the lines of their benchmark looks like
this:
Implication:
lspe(x7, x2) * NodeLL(x9, x1) * NodeLL(x1, x6) * NodeLL(x5, x7) *
lspe(x10, x2) * NodeLL(x8, x4) * NodeLL(x3, x2) * NodeLL(x4, x9) *
NodeLL(x6, x1) * lspe(x2, x7) |- lspe(x7, x2) * lspe(x2, x7) * lspe(x4,
x6) * lspe(x5, x7) * lspe(x3, x2) * lspe(x8, x4) * lspe(x10, x2) *
lspe(x6, x1)
If I feed this line into run_prover with the logic file
jstar/unit_tests/jimple_tests/linkedlist/logic then the process does not
seem to terminate. Any idea why is that?
Kind regards,
Alexander
[1] J. A. Navarro Pérez and A. Rybalchenko, “Separation logic +
superposition calculus = heap theorem prover,” in Proceedings of the
32nd ACM SIGPLAN conference on Programming language design and
implementation, New York, NY, USA, 2011, pp. 556–566.
--
Research Group "Specification and Modelling of Software Systems"
Department of Computer Science, University of Paderborn
Room O4.128, Phone +49-5251-60-3894
Matko Botincan
1./ It's a bug -- we forgot to load the abstraction file in run_prover
under the Psyntax.Abs case. The abstraction file is loaded in the same
way as logic file (with load_logic), e.g. look at test_symb.ml or
corestar.ml.
2./ I've looked at the example you've sent and it seems there are two
(unrelated) issues:
- The set of logic rules in linkedlist/logic is incomplete, and combined
with the way how matching of existentials works some cases get missed.
A possible temporary fix for this are rules that specifically allow
matching of e.g. NodeLL(?y, ?x) and NodeLL(?z, ?x) when ?y != ?z (here
we use ?y and ?z instead of existentials to cover positions of
existentials with a single rule). Attached is a modified
linkedlist/logic file with such rules (i've included all combinations
just in case). This allows proving entailments such as:
ls(x, _y) * NodeLL(_y,z) |- NodeLL(x,_w) * ls(_w,z)
that would otherwise fail using the previous set of rules.
- The modified logic file, however, does not seem to be enough to lead
to a successful termination of corestar on the example you've sent (at
least on my machine, where i'm running corestar under Cygwin, it crashes
with exception "Buffer.add: cannot grow buffer"). I've looked at the
generated proof traces and they do not cycle. There just seem to be too
many case splits and possible aliases to check caused by the occurrences
of the lspe predicate. Looking at the shape of the heap in the
antecedent, there are actually two necessarily disconnected components
(they must be disconnected because there are no dangling pointers and
some of the nodes in each of the strongly connected component are
NodeLLs) that could be used to eliminate most cases, but corestar does
not see this. If we manually split the heap, the resulting entailments
NodeLL(x9, x1) * NodeLL(x1, x6) * NodeLL(x8, x4) * NodeLL(x4, x9) *
NodeLL(x6, x1) |- lspe(x4, x6) * lspe(x8, x4) * lspe(x6, x1)
and
lspe(x7, x2) * NodeLL(x5, x7) * lspe(x10, x2) * NodeLL(x3, x2) *
lspe(x2, x7) |- lspe(x7, x2) * lspe(x2, x7) * lspe(x5, x7) * lspe(x3,
x2) * lspe(x10, x2)
get proved without a problem. So, *eventually* corestar should find the
right splitting and prove the entailment, but it could require a really
long way to go.
Best, -Matko
Radu Grigore
> 2./ I've looked at the example you've sent and it seems there are two
> - The modified logic file, however, [...] it crashes with
> exception "Buffer.add: cannot grow buffer"). I've looked at the generated
> proof traces and they do not cycle. There just seem to be too many case
> splits
I didn't yet try the example, but I suspect that a commit of mine
might be involved.
https://github.com/seplogic/corestar/commit/28e5fedd92fbdb907ef983968afb1406c7269ea3
This commit makes corestar more complete but it may make it diverge in
some situations where it didn't use to. The commit supposed to be
followed by another that solves the second problem, by changing the
search strategy to iterative deepening.
Alexander Schremmer
> On 17/01/2012 17:26, Alexander Schremmer wrote:
>> 1. I added the following line in parser.mly to the question rule:
>> | ABSRULE COLON formula_npv { Abs($3) }
>> and tried the attached files (example.file and example.logic) with
>> run_prover. Unfortunately, the abstraction rule does not seem to be
>> applied. Any idea why is that?
> 1./ It's a bug -- we forgot to load the abstraction file in run_prover
> under the Psyntax.Abs case. The abstraction file is loaded in the same
> way as logic file (with load_logic), e.g. look at test_symb.ml or
> corestar.ml.
run_prover loads indeed only one rule file - but uses it as an
abstraction rule file. So it should work like it is now, right?
> 2./ I've looked at the example you've sent and it seems there are two
> (unrelated) issues:
>
> - The set of logic rules in linkedlist/logic is incomplete, and combined
> with the way how matching of existentials works some cases get missed.
Are there more complete sets of logic files available for corestar?
>So, *eventually* corestar should find the
> right splitting and prove the entailment, but it could require a really
> long way to go.
I will try to revert back before the commit by Radu first.
Interestingly, the authors of the mentioned paper managed to get it
proved, but did not yet reply to my question how they did it :)
Kind regards,
Alexander
Alexander Schremmer
> This commit makes corestar more complete but it may make it diverge in
> some situations where it didn't use to. The commit supposed to be
> followed by another that solves the second problem, by changing the
> search strategy to iterative deepening.
I reverted the commit and tried run_prover on the formula:
Implication:
lspe(x7, x2) * NodeLL(x9, x1) * NodeLL(x1, x6) * NodeLL(x5, x7) *
lspe(x10, x2) * NodeLL(x8, x4) * NodeLL(x3, x2) * NodeLL(x4, x9) *
NodeLL(x6, x1) * lspe(x2, x7)
|- lspe(x7, x2) * lspe(x2, x7) * lspe(x4, x6) * lspe(x5, x7) * lspe(x3,
x2) * lspe(x8, x4) * lspe(x10, x2) * lspe(x6, x1)
Without the commit, it needs 62 seconds on a 2,7 Ghz machine. With the
commit, I killed it after running for 3 minutes.
Even the first figure seems a bit unacceptable given that I planned to
use corestar as a backend for a software analysis. :-(
Kind regards,
Alexander
Matko Botincan
>
>> 1./ It's a bug -- we forgot to load the abstraction file in run_prover
>> under the Psyntax.Abs case. The abstraction file is loaded in the same
>> way as logic file (with load_logic), e.g. look at test_symb.ml or
>> corestar.ml.
>
> run_prover loads indeed only one rule file - but uses it as an
> abstraction rule file. So it should work like it is now, right?
>
Absolutely. :) For some reason, i've assumed that you would like to
load abstraction rules in addition to the logic file -- ignore my remark.
>> 2./ I've looked at the example you've sent and it seems there are two
>> (unrelated) issues:
>>
>> - The set of logic rules in linkedlist/logic is incomplete, and combined
>> with the way how matching of existentials works some cases get missed.
>
> Are there more complete sets of logic files available for corestar?
>
I'm afraid there's nothing currently available that has been prepared
for a general use. We have a couple of versions of different flavoured
linked-list / array logics that were used in specific case studies. But
they have certain tweaks specific to the analysed programs. If you want
to have a look, i can certainly send you some of those.
>> So, *eventually* corestar should find the
>> right splitting and prove the entailment, but it could require a really
>> long way to go.
>
> I will try to revert back before the commit by Radu first.
> Interestingly, the authors of the mentioned paper managed to get it
> proved, but did not yet reply to my question how they did it :)
>
Which benchmark from the paper [1] is the one you've sent ?
Best, -Matko
Matko Botincan
On 19.01.2012 23:42, Radu Grigore wrote:
This commit makes corestar more complete but it may make it diverge in
some situations where it didn't use to. The commit supposed to be
followed by another that solves the second problem, by changing the
search strategy to iterative deepening.
I reverted the commit and tried run_prover on the formula:
Implication:
ￜ lspe(x7, x2) * NodeLL(x9, x1) * NodeLL(x1, x6) * NodeLL(x5, x7) * lspe(x10, x2) * NodeLL(x8, x4) * NodeLL(x3, x2) * NodeLL(x4, x9) * NodeLL(x6, x1) * lspe(x2, x7)
|- lspe(x7, x2) * lspe(x2, x7) * lspe(x4, x6) * lspe(x5, x7) * lspe(x3, x2) * lspe(x8, x4) * lspe(x10, x2) * lspe(x6, x1)
Without the commit, it needs 62 seconds on a 2,7 Ghz machine. With the commit, I killed it after running for 3 minutes.
Even the first figure seems a bit unacceptable given that I planned to use corestar as a backend for a software analysis. :-(
Just to put things into perspective -- coreStar has been developed to support rapid prototyping and experimentation with separation logic-based analysis/verification. Though underlying techniques are known to scale (e.g. Dino et al's tool Infer), industrial-strength and scalability were never coreStar's focus.
The question is how likely is that the queries such as the one you've sent would arise in programs you wish to analyse? Also, depending on the research objective, perhaps coreStar's implementation inefficiency might not be the biggest bottleneck.
Alexander Schremmer
> On 20/01/2012 09:25, Alexander Schremmer wrote:
>> run_prover loads indeed only one rule file - but uses it as an
>> abstraction rule file. So it should work like it is now, right?
> Absolutely. :) For some reason, i've assumed that you would like to load
> abstraction rules in addition to the logic file -- ignore my remark.
But then I wonder why my initial example is not abstracted according to
the rule file.
>> Are there more complete sets of logic files available for corestar?
> If you want to have a look, i can certainly send you some of those.
Yes, I would be certainly interested into such files.
>>> So, *eventually* corestar should find the
>>> right splitting and prove the entailment, but it could require a really
>>> long way to go.
>>
>> I will try to revert back before the commit by Radu first.
>> Interestingly, the authors of the mentioned paper managed to get it
>> proved, but did not yet reply to my question how they did it :)
>>
>
> Which benchmark from the paper [1] is the one you've sent ?
It is the first query (of 1000) of the benchmark with vars=11 in Table
1. I found the benchmarks at
http://navarroj.com/research/tools/slp-benchmarks.tgz
Kind regards,
Alexander
Alexander Schremmer
> Just to put things into perspective -- coreStar has been developed to
> support rapid prototyping and experimentation with separation
> logic-based analysis/verification. Though underlying techniques are
> known to scale (e.g. Dino et al's tool Infer), industrial-strength and
> scalability were never coreStar's focus.
OK. Yet, I wonder how useful a high performance separation logic solver
(with a standardized interface like in the SMT world) would be.
> The question is how likely is that the queries such as the one you've
> sent would arise in programs you wish to analyse?
I have no idea, yet :)
> Also, depending on the research objective, perhaps coreStar's
> implementation inefficiency might not be the biggest bottleneck.
Well, if I expect to have hundreds of entailment queries in order to
analyze a simple program, I certainly anticipate a runtime of a minute
per query to constitute the bottleneck.
Matko Botincan
>
> But then I wonder why my initial example is not abstracted according
> to the rule file.
>
Oh right -- you had garbage() in example.file and Garbage() in
example.logic. Predicate names are case sensitive.
>
>> If you want to have a look, i can certainly send you some of those.
>
> Yes, I would be certainly interested into such files.
>
I'll send you to email.
>>
>> Which benchmark from the paper [1] is the one you've sent ?
>
> It is the first query (of 1000) of the benchmark with vars=11 in Table
> 1. I found the benchmarks at
> http://navarroj.com/research/tools/slp-benchmarks.tgz
Ok. As i read from the paper, these were all random instances, not
coming from actual verification conditions.
Best, -Matko
Matko Botincan
>
> OK. Yet, I wonder how useful a high performance separation logic
> solver (with a standardized interface like in the SMT world) would be.
>
It would certainly be useful, but keep in mind that usefulness also
comes from flexibility. Having possibility to use free sort and
function symbols (e.g. as in AUFLIA logic) is quite important in the SMT
world. CoreStar's prover is trying to be at the flexible side of the
spectrum for separation logic -- while its core rewriting engine is
quite fast, except for the spatial conjective it does not rely on any
specific separation logic predicates (e.g. even the definition of the
points-to relation is provided in the external logic file).
The superposition based prover from [1] is more on the other side of the
spectrum. While certainly beating coreStar's prover on queries with
linked list predicates, it seems to be specialised only for this
specific instance of separation logic. I don't understand the
superposition approach well enough to say if (and how) this could be
generalised to arbitrary predicates.
>> The question is how likely is that the queries such as the one you've
>> sent would arise in programs you wish to analyse?
>
> I have no idea, yet :)
>
From what i've read in the paper [1], all test queries were really
contrived instances. Even benchmarks coming from the Smallfoot examples
were artificialised -- the authors mention that the original entailments
were quite easy to check (under a second by the involved provers), so
they've cloned multiple instances of the formulas to make them hard.
I am not undermining the contributions of [1] as it's certainly
advancement of the state-of-the-art in separation logic proving
automation. But it's not clear to me what it brings to separation logic
based tools and would it allow any new kind of linked-list programs to
be analysed that couldn't be analysed before.
>> Also, depending on the research objective, perhaps coreStar's
> > implementation inefficiency might not be the biggest bottleneck.
>
> Well, if I expect to have hundreds of entailment queries in order to
> analyze a simple program, I certainly anticipate a runtime of a minute
> per query to constitute the bottleneck.
It's very unlikely that you would encounter these kind of queries in
analysing simple programs. I don't know if it is even possible to
contrive a program that would result with such queries.
From my moderate experience with coreStar and separation logic analysis
of certain classes of programs, i don't recall a case where the spatial
reasoning itself was the bottleneck. Most frequently the component
where the most of the time was spent on was the SMT solver. There is a
huge room for improvement of the symbolic execution, SMT solver use (we
currently do it in a quite naive way and re-calculate too many things)
and abstraction. Optimising these parts could lead to much greater
speedups than from a potentially more optimised separation logic prover.
Best, -Matko
Alexander Schremmer
> Oh right -- you had garbage() in example.file and Garbage() in
> example.logic. Predicate names are case sensitive.
Oops, indeed.
>>> If you want to have a look, i can certainly send you some of those.
> I'll send you to email.
Thanks!
>>> Which benchmark from the paper [1] is the one you've sent ?
>>
>> It is the first query (of 1000) of the benchmark with vars=11 in Table
>> 1. I found the benchmarks at
>> http://navarroj.com/research/tools/slp-benchmarks.tgz
Actually, I tried one from Table 2 (where SLP performs best compared to
the other solvers). But indeed, both ones from Table 1 and Table 2 are
synthetic.
Alexander Schremmer
> On 20/01/2012 11:57, Alexander Schremmer wrote:
>>
>> OK. Yet, I wonder how useful a high performance separation logic
>> solver (with a standardized interface like in the SMT world) would be.
> It would certainly be useful, but keep in mind that usefulness also
> comes from flexibility. Having possibility to use free sort and function
> symbols (e.g. as in AUFLIA logic) is quite important in the SMT world.
Indeed.
> CoreStar's prover is trying to be at the flexible side of the spectrum
> for separation logic -- while its core rewriting engine is quite fast,
> except for the spatial conjective it does not rely on any specific
> separation logic predicates (e.g. even the definition of the points-to
> relation is provided in the external logic file).
Actually, it is also quite fast compared to using automated theorem
provers in this realm: Perez et al. prepared some TPTP problem files
that I fed into Vampire today and it was slower than Corestar.
> The superposition based prover from [1] is more on the other side of the
> spectrum. While certainly beating coreStar's prover on queries with
> linked list predicates, it seems to be specialised only for this
> specific instance of separation logic.
Probably an adaptation would involve modifying the rule set in their
Prolog implementation. :-)
> From my moderate experience with coreStar and separation logic analysis
> of certain classes of programs, i don't recall a case where the spatial
> reasoning itself was the bottleneck.
Good to know.
Kind regards,
Alexande