Question about Bi-Abduction in run_logic (was: Re: Question about dereference rule in corestar paper)
Alexander Schremmer
I have a problem with run_logic which does not print a simple equality
it should have gathered from bi-abduction:
On 31.01.2012 15:31, Matko Botincan wrote:
> Namely, if we try running your example without any logic rules:
>
> Specification ex : { PointsTo(a,b) * PointsTo(z,"42") } { PointsTo(a,b)
> * PointsTo(z,"42") } ?
> assign x := { PointsTo(a,_v) } { PointsTo(a,_v) * $ret_v1 = _v } ();
> end;
>
> corestar fails already at the assign statement as it cannot perform
> frame inference for the assign's pre:
> | PointsTo(a, b) * PointsTo(z, "42") |- PointsTo(a, _v_1)
>
> We need to add at least the rule that will say how to eliminate the
> PointsTo's at the same heap location:
>
> rule pto_remove:
> | PointsTo(?x,?y) |- PointsTo(?x,?t)
> without
> ?y!=?t
> if
> PointsTo(?x,?y) | |- ?y=?t
>
> As this rule adds as an obligation the equality between b and _v (which
> is easily discharged), as a consequence it will push the "missing"
> equality to the framed term structure.
Thanks for this hint! With corestar, it works now. Unfortunately, it
does not work yet in run_logic.
For a file with this line (and logic + abduction logic files containing
above rule):
Abduction: PointsTo(a, b) |- PointsTo(a, _v)
I get an empty response ("") from the pretty printer, but not a failure
(neither a pretty printed result " | " which would represent an empty
frame and anti-frame).
Where is the equality gone? I would expect the output _v = b | _v =b.
Kind regards,
Alexander
--
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
that in clogic.ml the second line of pp_ts_formula_af' should be
fprintf ppf "@, | "; pp_ts_formula' pp ppf first {F.ts=ts;
F.form=antiform;}
instead of
(pp_sep " | ").separator pp_ts_formula ppf first {F.ts=ts;
F.form=antiform;}
Regarding where's the equality _v=b gone -- _v and b have been unified
during sequent simplification phase after matching the pto_remove rule ;
the equality wouldn't be much useful to keep.
Note also that the rule i've sent you does not abduct, so nothing will
be pushed to the antiframe part of the sequent.
At the moment pure abduction does not work quite right -- there are some
peculiarities with distinguishing assumed and asserted equalities that
haven't been fully resolved. In fact, abduction is still quite fragile
and possibly does something unsound. But it's high on the priority list
and hopefully should be resolved rather soon (perhaps in a few weeks,
but can't really commit to a specific time).
Best, -Matko
Alexander Schremmer
On 01.02.2012 13:50, Matko Botincan wrote:
> It seems there's a bug in the pretty printer for inner_form_af.
Yes, after that bugfix, it shows at least both (empty) frames.
> Regarding where's the equality _v=b gone -- _v and b have been unified
> during sequent simplification phase after matching the pto_remove rule ;
> the equality wouldn't be much useful to keep.
Well, I do not have the unification/congruence information from the term
structure available after I have performed the frame inference via a
"call" to run_prover, as I only output the string information of the
frame (yet). So I cannot construct the spec assignment out of the
building blocks that run_logic is providing, currently.
Is there any easy way to preserve this information?
> In fact, abduction is still quite fragile
> and possibly does something unsound.
Good to know, in this case I will work without abduction for the time being.
Matko Botincan
>
>> Regarding where's the equality _v=b gone -- _v and b have been unified
>> during sequent simplification phase after matching the pto_remove rule ;
>> the equality wouldn't be much useful to keep.
>
> Well, I do not have the unification/congruence information from the
> term structure available after I have performed the frame inference
> via a "call" to run_prover, as I only output the string information of
> the frame (yet). So I cannot construct the spec assignment out of the
> building blocks that run_logic is providing, currently.
>
> Is there any easy way to preserve this information?
Searching for frame(s) merely means collecting the leftover formula(e)
from the entailment proof, so as a consequence the term structure of the
frame will contain information about all equalities. However, these do
not get printed out when you execute run_logic, as the output of the
pretty printer has been optimised to avoid printing clutter. run_logic
was not meant to be used as a component for building a symbolic
execution engine, but just for quickly checking entailment queries.
If you want to execute spec assignment using corestar's prover only then
you should use the psyntax and sepprover interface. To execute a spec
assignment you roughly have to do the following:
1) substitute fresh existentials in the spec
2) search for frame(s) of pre wrt current heap
3) conjoin frame(s) with the post (this will "magically" ensure that the
same existentials that were unified in the pre are also unified with the
same vars in the post)
4) mark the substituted existentials as deleted
5) extract the ret val(s) to assignee(s) and delete ret vars
You can check the actual function names to be called by examining
Assignment_core case of execute_core in symexec.ml and jsr in
specification.ml.
Best, -Matko