Multiple quantifiers to memory locations of same type

[sakehl]

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]

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]

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]

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-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.$FVFTo$SnapTo$FVF 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]

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.