Multiple quantifiers to memory locations of same type #831
Description
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