Multiple quantifiers to memory locations of same type #831
Comments
|
Here are all the files, if you'd rather not generate them, but just verify: For me they simply do not verify anymore starting at quant10.vpr |
|
I'm trying out a change in Silicon that speeds this example up by quite a bit (PR #835) by essentially assuming non-aliasing information for QPs earlier. For me, the version with ten arrays takes ca. 9 seconds after the change, which is better, but the examples with many more arrays still take way too long. I'm not sure I completely understand why that is yet. I would have thought that it might help to change the permission amount from 1/2 to 2/3 everywhere, since that essentially implies non-aliasing between the different arrays. I think in principle, that's a good thing to do since it gives the verifier more information, but I don't see it making a difference here. |
|
Awesome, thanks for looking into this! What I suspect that the complexity for the checks is quadratic since it needs to check between each pair of arrays. Thus for sufficiently large number of arrays, we always end up with something taking a long time. And it has to do with quantifiers. Passing the flag [INFO] Reporting quantifier instances statistics in descending order:<\details> |
|
Yes, there is at least one part of Silicon's QP handling that is inherently quadratic in the number of snapshot maps Silicon generates, that seems to be the issue here ( |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
So this is not per se a bug report, more something I run into. I'm wondering if there are workarounds, or something fundamental what is needed here.
For my research I come across programs, which I try to verify using VerCors, which contain many arrays of the same type. A dumbed down version of a program is what I try to verify here:
in VerCors. Anway, translating something similar like this in Viper looks like the following:
This is a program with 4 arrays.
Now I've encoded similar programs, for 1 up to 10 arrays, and the verification just keep getting slower:
Now, what I suspect is that, because of separation logic, it tries to reason about that multiple memory locations from different quantifiers could overlap, and checks that this is not the case or that if it is consistent as pre-condition, we end up with consistent post-conditions. Do you know what is going exactly? And we this time is increasing so much?
Cause I think the checks are in place, when memory location could be overlapping. But in the case of the programs that I am checking, my arrays will never point to the same memory location. Is there perhaps anyway to indicate that each quantifier is completely unique?
How I am solving this at the moment, is that I am wrapping all my arrays permissions in predicates, so it seems they do not interact. This is a tedious process however.
So anyway, happy to hear if there is any solution to this!
PS: I've added a jupyter notebook which generates Viper files, so you can experiment yourselves if you want to.
GenerateQuant.zip
The text was updated successfully, but these errors were encountered: