Potential unsoundness

[pieter-bos]

Hello! This example verifies in silicon, and I believe it shouldn't:

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)
{
  array_loc(a, i)
}

method main(arr1: array, arr2: array)
  requires alen(arr1) == 6
  requires alen(arr2) == 12
  requires (forall i: Int :: { aloc(arr1, i).int } (0 <= i && i < 6) ==> acc(aloc(arr1, i).int, 1 / 2))
  requires (forall i: Int :: { aloc(arr1, i).int } (0 <= i && i < 6) ==> aloc(arr1, i).int == 0)
  
  requires (forall i: Int :: { aloc(arr2, i).int } (0 <= i && i < 12) ==> acc(aloc(arr2, i).int, write))
  requires (forall i: Int :: { aloc(arr2, i).int } (0 <= i && i < 6) ==> aloc(arr2, i).int == 0 * (aloc(arr1, i).int - aloc(arr1, 0).int))
{
  var x: Int := 0
  while (true)
    invariant x == x
    invariant (forall i: Int :: { aloc(arr2, i).int } (0 <= i && i < 6) ==> acc(aloc(arr2, i).int, write))
    invariant (forall i: Int :: { aloc(arr2, i).int } (6 <= i && i < 12) ==> acc(aloc(arr2, i).int, 1 / 2))
    invariant (forall i: Int :: { aloc(arr1, i).int } (0 <= i && i < 6) ==> acc(aloc(arr1, i).int, 1 / 2))
  {
    assert aloc(arr2, 6).int == aloc(arr2, 6).int
    assert 3 + 8 == 38
  }
}

I miminized it as much as possible, but it seems all the present ingredients are necessary now, as verification (imo correctly) fails on the false assertion if I remove or change anything seemingly inconsequential. Verification is also not all that stable: it seems to work best with --numberOfParallelVerifiers 16, the z3 version does not seem to matter (tried with 4.8.6, self-compiled nightly). I also tried with the most recent silicon, and also #650 - neither seem to matter.

I did also try to dig down in the smt a bit. If I minimize the file keeping the verdict of the appropriate (check-sat) stable, it seems that this quantifier is instantiated with i@5@16 Int = 6, a contradiction:

(assert (forall ((i@5@16 Int)) (!
  (< i@5@16 (alen<Int> arr1@2@16))
  :pattern (($FVF.loc_int ($FVF.lookup_int ($SortWrappers.$SnapTo$FVF<Int> ($Snap.first ($Snap.second ($Snap.second $t@4@16)))) (aloc ($Snap.combine
    $Snap.unit
    $Snap.unit) arr1@2@16 i@5@16)) (aloc ($Snap.combine $Snap.unit $Snap.unit) arr1@2@16 i@5@16)))
  :qid |int-aux|)))

An equally-named assertion from #650 is shaped differently, but seems to state the same thing (though I did not check the proof tree then):

(assert (forall ((i@20@16 Int)) (!
  (and
    (or (not (<= 6 i@20@16)) (<= 6 i@20@16))
    (<= 0 i@20@16)
    (< i@20@16 (alen<Int> arr2@3@16))
    (aloc%precondition ($Snap.combine $Snap.unit $Snap.unit) arr2@3@16 i@20@16))
  :pattern (($FVF.loc_int ($FVF.lookup_int ($SortWrappers.$SnapTo$FVF<Int> ($Snap.first ($Snap.second ($Snap.second $t@15@16)))) (aloc ($Snap.combine
    $Snap.unit
    $Snap.unit) arr2@3@16 i@20@16)) (aloc ($Snap.combine $Snap.unit $Snap.unit) arr2@3@16 i@20@16)))
  :qid |int-aux|)))

If you can't get silicon to verify the file, feel free to ask for smt outputs and/or z3.log and so on.

[marcoeilers]

Thanks for reporting this!
I still don't know Silicon's code for quantifier handling very well, but as far as I can tell, we should never generate this quantifier, or rather, we should assume that i is less than alen(arr1) only under the conditions that i >= 0 and i < 6.
On branch https://github.com/viperproject/silicon/tree/meilers_652_fix I tried to fix this; this feels like it's the right thing to do, and on my machine it fixes the problem and doesn't break anything else. But if the problem is non-deterministic, obviously this could just be random chance.
And @mschwerhoff should have a look at this either way, since, as I said, I don't know if this is the right way to fix it.

[marcoeilers]

Issue #560 might be related (but is not fixed by the change referenced above).