Narrowing gas #1879
Narrowing gas #1879
Conversation
DrMichaelPetter
added
feature
precision
relational
| let narrowing_gas = GobConfig.get_int "ana.apron.narrowing_gas" | ||
| in | ||
| if (narrowing_gas > 0) then | ||
| let module Narrowed = | ||
| struct | ||
| module PolyhedraChainParams: Printable.ChainParams = | ||
| struct | ||
| let n () = narrowing_gas | ||
| let names = string_of_int | ||
| end | ||
| include NarrowingGas.DLifter (Spec) (PolyhedraChainParams) | ||
| module A = Spec.A | ||
| let access = Spec.access | ||
| let name = Spec.name | ||
| end | ||
| in | ||
| (module Narrowed) | ||
| else | ||
| (module Spec) |
There was a problem hiding this comment.
This is in a slightly less ideal place than I imagined in #1494, but I can see why and it is fine.
Ideally, I'd like to just wrap this lifting around polyhedra, but not other Apron domains, somewhere in ApronDomain, and have the analysis be completely oblivious to the fact.
Because in some sense it's "just" a lifting of any Lattice.S → Lattice.S. But that's only so if things are fully properly abstract, but our RelationDomain/ApronDomain setup is far from that. So it'd require a large cleanup/refactoring to be able to do it in my dream way.
There was a problem hiding this comment.
I don't think that's is purely a lattice -> lattice functor, as the gas needs to be reset at every transfer function, no?
There was a problem hiding this comment.
Actually the NarrowingGas.Dom functor here (based on WideningDelay, etc) is essentially just that. It's the act of unlift and lift to do the operation that leads to the reset. And that's what NarrowingGas.DLifter used here exactly does.
It additionally needs all relational domain operations (instead of Spec operations) lifted, which needs more boilerplate. And it won't really gain anything from Goblint usage perspective.
|
There is some strange influence between apron w. narrow gas 1 and def_exc going on, when the loopUnrollHeuristics is on: //PARAMS: --set ana.apron.narrowing_gas 1 --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.autotune.enabled true --set ana.autotune.activated '["loopUnrollHeuristic"]'
int main() {
int x;
int y;
int xtmp;
if (y >= 0)
{
xtmp = x;
while(xtmp>y) {
xtmp = xtmp - y;
}
y = xtmp;
}
return 0;
}Goblint does not reach a fixpoint in this configuration, with a diff for |
|
With For some reason the right-hand side for the loop head is not monotonic? Or somehow with improved In particular, with more tracing, Apron doesn't seem to return a lower bound 1 which it seems to have: |
|
Here is a more simplified version of the same thing without autotuner -- so definitely a pure apron/polyhedra and narrowing thing: // SKIP PARAM --set ana.apron.narrowing_gas 1 --set ana.activated[+] apron --set ana.apron.domain polyhedra
int main(void)
{
int x;
int y;
int xtmp;
if (y < 0) return 0;
if (x <= y) return 0;
xtmp = x-y;
while (xtmp > y)
{
xtmp -= y;
}
return 0;
} |
It seems to get lost during a |
|
The upper bound Either way, there's something strange because there should be a less precise state pre-narrowing, yet it somehow has a better upper bound to avoid overflowing to top. |
It behaves the same.
|
Closes #1494 by providing a domain lifter, that applies
meetuntil the gas depletes. In a first application, we get a new parameterana.apron.narrowing_gasto specify the amount of gas per state, which comes in handy for poyhedra-based analysis.