Multiple quantifiers to memory locations of same type
Opened this issue · 4 comments
sakehl commented
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:
context_everywhere n > 0;
context_everywhere x0 != null ** x0.length == n ** (\forall* int i=0..n; Perm(x0[i], write));
context_everywhere x1 != null ** x1.length == n ** (\forall* int i=0..n; Perm(x1[i], 1\2));
context_everywhere x2 != null ** x2.length == n ** (\forall* int i=0..n; Perm(x2[i], 1\2));
context_everywhere x3 != null ** x3.length == n ** (\forall* int i=0..n; Perm(x3[i], 1\2));
context_everywhere x4 != null ** x4.length == n ** (\forall* int i=0..n; Perm(x4[i], 1\2));
int main(int n, int[n] x0, int[n] x1, int[n] x2, int[n] x3, int[n] x4){
loop_invariant 0 <= i && i<= n;
loop_invariant (\forall int j=0..i; x0[j] == 0+ x1[j]+ x2[j]+ x3[j]+ x4[j]);
for(int i=0; i<n;i++){
x0[i] = 0+ x1[i]+ x2[i]+ x3[i]+ x4[i];
}
}in VerCors. Anway, translating something similar like this in Viper looks like the following:
domain Array {
function array_loc(a: Array, i: Int): Ref
function alen(a: Array): Int
function loc_inv_1(loc: Ref): Array
function loc_inv_2(loc: Ref): Int
axiom {
(forall a: Array, i: Int ::
{ array_loc(a, i) }
loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
}
axiom {
(forall a: Array :: { alen(a) } alen(a) >= 0)
}
}
field int: Int
function aloc(a: Array, i: Int): Ref
requires 0 <= i
requires i < alen(a)
decreases
ensures loc_inv_1(result) == a
ensures loc_inv_2(result) == i
{
array_loc(a, i)
}
method main1(tid: Int, n: Int, x0: Array, x1: Array, x2: Array, x3: Array, x4: Array)
requires 0 < n
requires alen(x0) == n
requires (forall i: Int ::
{ aloc(x0, i) }
0 <= i && i < n ==> acc(aloc(x0, i).int, write))
requires alen(x1) == n
requires (forall i: Int ::
{ aloc(x1, i) }
0 <= i && i < n ==> acc(aloc(x1, i).int, 1 * write / 2))
requires alen(x2) == n
requires (forall i: Int ::
{ aloc(x2, i) }
0 <= i && i < n ==> acc(aloc(x2, i).int, 1 * write / 2))
requires alen(x3) == n
requires (forall i: Int ::
{ aloc(x3, i) }
0 <= i && i < n ==> acc(aloc(x3, i).int, 1 * write / 2))
requires alen(x4) == n
requires (forall i: Int ::
{ aloc(x4, i) }
0 <= i && i < n ==> acc(aloc(x4, i).int, 1 * write / 2))
ensures 0 < n
ensures alen(x0) == n
ensures (forall i: Int ::
{ aloc(x0, i) }
0 <= i && i < n ==> acc(aloc(x0, i).int, write))
ensures alen(x1) == n
ensures (forall i: Int ::
{ aloc(x1, i) }
0 <= i && i < n ==> acc(aloc(x1, i).int, 1 * write / 2))
ensures alen(x2) == n
ensures (forall i: Int ::
{ aloc(x2, i) }
0 <= i && i < n ==> acc(aloc(x2, i).int, 1 * write / 2))
ensures alen(x3) == n
ensures (forall i: Int ::
{ aloc(x3, i) }
0 <= i && i < n ==> acc(aloc(x3, i).int, 1 * write / 2))
ensures alen(x4) == n
ensures (forall i: Int ::
{ aloc(x4, i) }
0 <= i && i < n ==> acc(aloc(x4, i).int, 1 * write / 2))
{
{
var exc: Ref
var i: Int
var excbeforeloop: Ref
exc := null
excbeforeloop := exc
i := 0
while (i < n)
invariant exc == excbeforeloop
invariant 0 < n
invariant alen(x0) == n
invariant (forall i1: Int ::
{ aloc(x0, i1) }
0 <= i1 && i1 < n ==> acc(aloc(x0, i1).int, write))
invariant alen(x1) == n
invariant (forall i1: Int ::
{ aloc(x1, i1) }
0 <= i1 && i1 < n ==>
acc(aloc(x1, i1).int, 1 * write / 2))
invariant alen(x2) == n
invariant (forall i1: Int ::
{ aloc(x2, i1) }
0 <= i1 && i1 < n ==>
acc(aloc(x2, i1).int, 1 * write / 2))
invariant alen(x3) == n
invariant (forall i1: Int ::
{ aloc(x3, i1) }
0 <= i1 && i1 < n ==>
acc(aloc(x3, i1).int, 1 * write / 2))
invariant alen(x4) == n
invariant (forall i1: Int ::
{ aloc(x4, i1) }
0 <= i1 && i1 < n ==>
acc(aloc(x4, i1).int, 1 * write / 2))
invariant 0 <= i
invariant i < n + 1
invariant (forall j: Int ::
{ aloc(x0, j) }
0 <= j && j < i ==>
aloc(x0, j).int == 0 + aloc(x1, j).int + aloc(x2, j).int + aloc(x3, j).int + aloc(x4, j).int)
{
aloc(x0, i).int := 0 + aloc(x1, i).int + aloc(x2, i).int + aloc(x3, i).int + aloc(x4, i).int
i := i + 1
}
assert exc == null
}
}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:
Silicon 1.1-SNAPSHOT (5e3ab014+)
Silicon finished verification successfully in 4.18s.
data/quant1.vpr 4.536563873291016 success
Silicon 1.1-SNAPSHOT (5e3ab014+)
Silicon finished verification successfully in 4.77s.
data/quant2.vpr 5.160653829574585 success
Silicon 1.1-SNAPSHOT (5e3ab014+)
Silicon finished verification successfully in 5.19s.
data/quant3.vpr 5.564464092254639 success
Silicon 1.1-SNAPSHOT (5e3ab014+)
Silicon finished verification successfully in 5.82s.
data/quant4.vpr 6.1763715744018555 success
Silicon 1.1-SNAPSHOT (5e3ab014+)
Silicon finished verification successfully in 6.96s.
data/quant5.vpr 7.328972816467285 success
Silicon 1.1-SNAPSHOT (5e3ab014+)
Silicon finished verification successfully in 10.68s.
data/quant6.vpr 11.023087501525879 success
Silicon 1.1-SNAPSHOT (5e3ab014+)
Silicon finished verification successfully in 24.24s.
data/quant7.vpr 24.652435064315796 success
Silicon 1.1-SNAPSHOT (5e3ab014+)
Silicon finished verification successfully in 01m:30s.
data/quant8.vpr 90.54522705078125 success
Silicon 1.1-SNAPSHOT (5e3ab014+)
Silicon finished verification successfully in 01m:57s.
data/quant9.vpr 117.69519448280334 success
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
sakehl commented
Here are all the files, if you'd rather not generate them, but just verify:
quant.zip
For me they simply do not verify anymore starting at quant10.vpr
marcoeilers commented
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.
sakehl commented
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 --silicon-print-quantifier-stats 10000 (I could not find a similar flag for silicon) to VerCors, and trying to verify quant11.pvl (which I terminated after a few minutes) I get these results:
[INFO] Reporting quantifier instances statistics in descending order:
======================================
Backend quantifier: $Set[Ref]_prog.equality_definition
instances: 330000 (gen: 0, cost: 0)
======================================
======================================
Backend quantifier: qp.$FVF<int>-eq-outer
instances: 260000 (gen: 0, cost: 15083)
======================================
======================================
Backend quantifier: qp.fvfValDef148
instances: 60000 (gen: 0, cost: 42)
======================================
======================================
Backend quantifier: qp.fvfValDef119
instances: 60000 (gen: 0, cost: 166)
======================================
======================================
Backend quantifier: qp.fvfValDef122
instances: 60000 (gen: 0, cost: 294)
======================================
======================================
Backend quantifier: qp.fvfValDef130
instances: 60000 (gen: 6701, cost: 1041)
======================================
======================================
Backend quantifier: qp.fvfValDef118
instances: 60000 (gen: 0, cost: 128)
======================================
======================================
Backend quantifier: qp.fvfValDef137
instances: 60000 (gen: 0, cost: 279)
======================================
======================================
Backend quantifier: qp.fvfValDef121
instances: 60000 (gen: 0, cost: 437)
======================================
======================================
Backend quantifier: qp.fvfValDef131
instances: 60000 (gen: 0, cost: 344)
======================================
======================================
Backend quantifier: qp.fvfValDef136
instances: 60000 (gen: 0, cost: 201)
======================================
======================================
Backend quantifier: qp.fvfValDef125
instances: 60000 (gen: 0, cost: 96)
======================================
======================================
Backend quantifier: qp.fvfValDef140
instances: 60000 (gen: 0, cost: 181)
======================================
======================================
Backend quantifier: qp.fvfValDef128
instances: 60000 (gen: 0, cost: 112)
======================================
======================================
Backend quantifier: qp.fvfValDef134
instances: 60000 (gen: 0, cost: 117)
======================================
======================================
Backend quantifier: qp.fvfValDef129
instances: 60000 (gen: 1, cost: 517)
======================================
======================================
Backend quantifier: qp.fvfValDef135
instances: 60000 (gen: 0, cost: 153)
======================================
======================================
Backend quantifier: qp.fvfValDef123
instances: 60000 (gen: 0, cost: 197)
======================================
======================================
Backend quantifier: qp.fvfValDef126
instances: 60000 (gen: 0, cost: 137)
======================================
======================================
Backend quantifier: qp.fvfValDef138
instances: 60000 (gen: 0, cost: 289)
======================================
======================================
Backend quantifier: qp.fvfValDef151
instances: 60000 (gen: 0, cost: 120)
======================================
======================================
Backend quantifier: qp.fvfValDef124
instances: 60000 (gen: 0, cost: 150)
======================================
======================================
Backend quantifier: qp.fvfValDef133
instances: 60000 (gen: 0, cost: 138)
======================================
======================================
Backend quantifier: qp.fvfValDef132
instances: 50000 (gen: 0, cost: 210)
======================================
======================================
Backend quantifier: qp.fvfValDef152
instances: 50000 (gen: 5378, cost: 791)
======================================
======================================
Backend quantifier: qp.fvfValDef120
instances: 50000 (gen: 0, cost: 248)
======================================
======================================
Backend quantifier: qp.fvfValDef144
instances: 50000 (gen: 0, cost: 112)
======================================
======================================
Backend quantifier: qp.fvfValDef127
instances: 50000 (gen: 0, cost: 168)
======================================
======================================
Backend quantifier: qp.fvfValDef139
instances: 50000 (gen: 0, cost: 238)
======================================
======================================
Backend quantifier: qp.fvfValDef145
instances: 50000 (gen: 0, cost: 75)
======================================
======================================
Backend quantifier: qp.fvfValDef146
instances: 50000 (gen: 0, cost: 28)
======================================
======================================
Backend quantifier: qp.fvfValDef143
instances: 50000 (gen: 0, cost: 141)
======================================
======================================
Backend quantifier: qp.fvfValDef150
instances: 50000 (gen: 0, cost: 79)
======================================
======================================
Backend quantifier: qp.fvfValDef149
instances: 50000 (gen: 0, cost: 22)
======================================
======================================
Backend quantifier: int-fctOfInv
instances: 50000 (gen: 0, cost: 2584)
======================================
======================================
Backend quantifier: qp.fvfValDef147
instances: 50000 (gen: 0, cost: 34)
======================================
======================================
Backend quantifier: qp.fvfValDef155
instances: 40000 (gen: 0, cost: 42)
======================================
======================================
Backend quantifier: qp.fvfValDef154
instances: 40000 (gen: 0, cost: 89)
======================================
======================================
Backend quantifier: qp.fvfValDef157
instances: 40000 (gen: 0, cost: 61)
======================================
======================================
Backend quantifier: qp.fvfValDef158
instances: 40000 (gen: 0, cost: 35)
======================================
======================================
Backend quantifier: qp.fvfValDef161
instances: 30000 (gen: 0, cost: 143)
======================================
======================================
Backend quantifier: qp.fvfValDef156
instances: 30000 (gen: 0, cost: 44)
======================================
======================================
Backend quantifier: qp.fvfValDef160
instances: 30000 (gen: 0, cost: 103)
======================================
======================================
Backend quantifier: quant-u-7
instances: 30000 (gen: 0, cost: 79)
======================================
======================================
Backend quantifier: quant-u-25
instances: 30000 (gen: 0, cost: 79)
======================================
======================================
Backend quantifier: qp.fvfValDef117
instances: 30000 (gen: 0, cost: 2162)
======================================
======================================
Backend quantifier: qp.fvfValDef153
instances: 30000 (gen: 0, cost: 493)
======================================
======================================
Backend quantifier: qp.fvfValDef159
instances: 30000 (gen: 0, cost: 16)
======================================
======================================
Backend quantifier: quant-u-6
instances: 30000 (gen: 0, cost: 121)
======================================
======================================
Backend quantifier: qp.fvfValDef142
instances: 30000 (gen: 0, cost: 1934)
======================================
======================================
Backend quantifier: quant-u-28
instances: 30000 (gen: 0, cost: 97)
======================================
======================================
Backend quantifier: k!775
instances: 20000 (gen: 0, cost: 1542)
======================================
======================================
Backend quantifier: qp.fvfValDef171
instances: 20000 (gen: 0, cost: 510)
======================================
======================================
Backend quantifier: qp.fvfValDef169
instances: 20000 (gen: 0, cost: 30)
======================================
======================================
Backend quantifier: qp.fvfValDef165
instances: 20000 (gen: 0, cost: 46)
======================================
======================================
Backend quantifier: qp.fvfValDef170
instances: 20000 (gen: 0, cost: 50)
======================================
======================================
Backend quantifier: qp.fvfValDef167
instances: 20000 (gen: 0, cost: 58)
======================================
======================================
Backend quantifier: qp.fvfValDef166
instances: 20000 (gen: 0, cost: 34)
======================================
======================================
Backend quantifier: qp.fvfValDef141
instances: 20000 (gen: 0, cost: 2412)
======================================
======================================
Backend quantifier: qp.fvfValDef168
instances: 20000 (gen: 0, cost: 53)
======================================
======================================
Backend quantifier: qp.fvfValDef164
instances: 20000 (gen: 0, cost: 146)
======================================
======================================
Backend quantifier: $Snap.$FVF<int>To$SnapTo$FVF<int>
instances: 10000 (gen: 0, cost: 134)
======================================
======================================
Backend quantifier: qp.fvfValDef162
instances: 10000 (gen: 0, cost: 232)
======================================
======================================
Backend quantifier: qp.fvfValDef175
instances: 10000 (gen: 0, cost: 21)
======================================
======================================
Backend quantifier: qp.fvfValDef33
instances: 10000 (gen: 0, cost: 2835)
======================================
======================================
Backend quantifier: qp.fvfValDef172
instances: 10000 (gen: 0, cost: 343)
======================================
======================================
Backend quantifier: qp.fvfValDef178
instances: 10000 (gen: 0, cost: 38)
======================================
======================================
Backend quantifier: qp.fvfValDef177
instances: 10000 (gen: 0, cost: 12)
======================================
======================================
Backend quantifier: qp.fvfValDef32
instances: 10000 (gen: 0, cost: 2533)
======================================
======================================
Backend quantifier: qp.fvfValDef37
instances: 10000 (gen: 0, cost: 2329)
======================================
======================================
Backend quantifier: qp.fvfValDef173
instances: 10000 (gen: 0, cost: 38)
======================================
======================================
Backend quantifier: qp.fvfValDef163
instances: 10000 (gen: 0, cost: 1200)
======================================
======================================
Backend quantifier: qp.fvfValDef176
instances: 10000 (gen: 0, cost: 14)
======================================
======================================
Backend quantifier: qp.fvfValDef174
instances: 10000 (gen: 0, cost: 28)
======================================
======================================
Backend quantifier: qp.fvfValDef34
instances: 10000 (gen: 0, cost: 2200)
======================================
======================================
Backend quantifier: int-aux
instances: 73 (gen: 0, cost: 0)
======================================
======================================
Backend quantifier: qp.resPrmSumDef189
instances: 12 (gen: 0, cost: 0)
======================================
======================================
Backend quantifier: quant-u-128
instances: 4 (gen: 0, cost: 51)
======================================
======================================
Backend quantifier: quant-u-100
instances: 4 (gen: 0, cost: 57)
======================================
======================================
Backend quantifier: quant-u-108
instances: 4 (gen: 0, cost: 53)
======================================
======================================
Backend quantifier: quant-u-130
instances: 4 (gen: 0, cost: 47)
======================================
======================================
Backend quantifier: int-permImpliesNonNull
instances: 4 (gen: 0, cost: 47)
======================================
======================================
Backend quantifier: quant-u-114
instances: 4 (gen: 0, cost: 38)
======================================
======================================
Backend quantifier: quant-u-122
instances: 4 (gen: 0, cost: 58)
======================================
======================================
Backend quantifier: quant-u-102
instances: 4 (gen: 0, cost: 54)
======================================
======================================
Backend quantifier: quant-u-126
instances: 4 (gen: 0, cost: 52)
======================================
======================================
Backend quantifier: quant-u-134
instances: 4 (gen: 0, cost: 48)
======================================
======================================
Backend quantifier: quant-u-112
instances: 4 (gen: 0, cost: 64)
======================================
======================================
Backend quantifier: quant-u-138
instances: 4 (gen: 0, cost: 47)
======================================
======================================
Backend quantifier: quant-u-124
instances: 4 (gen: 0, cost: 58)
======================================
======================================
Backend quantifier: quant-u-136
instances: 4 (gen: 0, cost: 38)
======================================
======================================
Backend quantifier: quant-u-106
instances: 4 (gen: 0, cost: 40)
======================================
======================================
Backend quantifier: quant-u-110
instances: 4 (gen: 0, cost: 48)
======================================
======================================
Backend quantifier: quant-u-98
instances: 4 (gen: 0, cost: 49)
======================================
======================================
Backend quantifier: quant-u-120
instances: 4 (gen: 0, cost: 47)
======================================
======================================
Backend quantifier: quant-u-132
instances: 4 (gen: 0, cost: 42)
======================================
======================================
Backend quantifier: quant-u-104
instances: 3 (gen: 0, cost: 53)
======================================
======================================
Backend quantifier: quant-u-96
instances: 3 (gen: 0, cost: 49)
======================================
======================================
Backend quantifier: quant-u-118
instances: 3 (gen: 0, cost: 45)
======================================
======================================
Backend quantifier: quant-u-94
instances: 3 (gen: 0, cost: 68)
======================================
======================================
Backend quantifier: quant-u-92
instances: 1 (gen: 0, cost: 23)
======================================
======================================
Backend quantifier: quant-u-116
instances: 1 (gen: 0, cost: 28)
======================================
======================================
Backend quantifier: qp.resPrmSumDef38
instances: 1 (gen: 0, cost: 0)
======================================
======================================
Backend quantifier: qp.resPrmSumDef25
instances: 1 (gen: 0, cost: 0)
======================================
======================================
Backend quantifier: qp-fld-prm-bnd
instances: 1 (gen: 0, cost: 0)
======================================
======================================
Backend quantifier: int-rcvrInj
instances: 0 (gen: 0, cost: 59)
======================================
<\details>
marcoeilers commented
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 (qp.$FVF<int>-eq-outer is the main axiom that's responsible for that). That's unlikely to change in the near future unfortunately.