Incompleteness in MoreCompleteExhale

[viper-admin]

Created by @vakaras on 2019-06-18 16:04
Last updated on 2019-08-28 10:36

The following example fails with --enableMoreCompleteExhale, but works in Carbon and in Silicon without the flag:

method test() {

  var _1: Ref
  var _3: Ref
  var _preserve: Ref

  inhale acc(Vec(_preserve), write-read$())
  inhale acc(usize(_3), write)
  inhale acc(_1.val_ref, read$()) && acc(Vec(_1.val_ref), read$()) && acc(usize(_3), read$())
  inhale _preserve == _1.val_ref
  inhale (unfolding acc(usize(_3), write) in _3.val_int) < len(_1.val_ref)

  assert (unfolding acc(usize(_3), write) in _3.val_int) < len(_1.val_ref)
  exhale acc(Vec(_1.val_ref), write - read$())
  assert (unfolding acc(usize(_3), write) in _3.val_int) < len(_1.val_ref)  // Fails with --enableMoreCompleteExhale

  assert  0 <= len(_1.val_ref)
}

field val_int: Int

field val_ref: Ref

function len(_pure_1: Ref): Int
  requires acc(Vec(_pure_1), read$())
  ensures 0 <= result

predicate usize(self: Ref) {
  acc(self.val_int, write)
}

function read$(): Perm
  ensures none < result
  ensures result < write

predicate Vec(self: Ref)

[viper-admin]

@vakaras commented on 2019-06-20 12:18

Removed all functions from the example:

method test() {

  var _1: Ref
  var _3: Ref
  var _preserve: Ref
  var read: Perm
  assume none < read && read < write

  inhale acc(usize(_preserve), write-read)
  inhale acc(usize(_3), write)
  inhale acc(_1.val_ref, read) && acc(usize(_1.val_ref), read) && acc(usize(_3), read)
  inhale _preserve == _1.val_ref
  inhale (unfolding acc(usize(_3), write) in _3.val_int) < (unfolding acc(usize(_1.val_ref), read) in _1.val_ref.val_int)

  assert (unfolding acc(usize(_3), write) in _3.val_int) < (unfolding acc(usize(_1.val_ref), read) in _1.val_ref.val_int)
  exhale acc(usize(_1.val_ref), write - read)
  assert (unfolding acc(usize(_3), write) in _3.val_int) < (unfolding acc(usize(_1.val_ref), read) in _1.val_ref.val_int)  // Fails with --enableMoreCompleteExhale
}

field val_int: Int

field val_ref: Ref

predicate usize(self: Ref) {
  acc(self.val_int, write)
}

[viper-admin]

@vakaras commented on 2019-06-22 14:10

Reduce the example even more:

method test() {

  var _1: Ref
  var _preserve: Ref
  var read: Perm := 1/8

  inhale acc(usize(_preserve), write-read)
  inhale acc(_1.val_ref, read) && acc(usize(_1.val_ref), read)
  inhale _preserve == _1.val_ref
  assert acc(usize(_1.val_ref), write)
  inhale 5 < (unfolding acc(usize(_1.val_ref), read) in _1.val_ref.val_int)

  assert 5 < (unfolding acc(usize(_1.val_ref), read) in _1.val_ref.val_int)
  exhale acc(usize(_1.val_ref), 2/8)
  assert 5 < (unfolding acc(usize(_1.val_ref), 3/8) in _1.val_ref.val_int)  // Fails with --enableMoreCompleteExhale
  assert acc(usize(_1.val_ref), 6/8)
}

field val_int: Int

field val_ref: Ref

predicate usize(self: Ref) {
  acc(self.val_int, write)
}

[viper-admin]

@mschwerhoff commented on 2019-06-26 20:29

I slightly rewrote the example:

field ival: Int

predicate usize(self: Ref) {
  acc(self.ival, write)
}

function get(self: Ref, p: Perm): Int
  requires none < p
  requires acc(usize(self), p)

method test() {
  var x: Ref
  var y: Ref

  inhale acc(usize(y), 1/2)
  inhale acc(usize(x), 1/2)
  inhale y == x
  assert acc(usize(x), write)

  inhale 5 < get(y, 1/100)
  assert 5 < get(x, 1/100) // Fails with --enableMoreCompleteExhale
}

Without --enableMoreCompleteExhale, Silicon will merge the two 1/2-chunks for usize(x) and usize(y), respectively, in order to prove line 18. This doesn't happen with --enableMoreCompleteExhale, but it seems that the heap summary that should be created instead — but at lines 20 and 21 — does not correctly summarise the heap. I.e. the fact that 5 < getis known for y (from line 20) but not for x.

[viper-admin]

@vakaras commented on 2019-06-28 10:06

The fix in branch scmalte_silicon_issue_387 has the following regression:

field discriminant: Int

predicate Option(self: Ref) {
  acc(self.discriminant, write)
}

function Option$discriminant(self: Ref): Int
  requires acc(Option(self), 1/2)
{
  (unfolding acc(Option(self), 1/2) in self.discriminant)
}

method test() {
    var _3: Ref
    inhale acc(Option(_3), write)
    inhale Option$discriminant(_3) == 1
    unfold acc(Option(_3), write)
    assert _3.discriminant == 1 // FAILS
}

[viper-admin]

@mschwerhoff commented on 2019-06-28 12:06

Regarding your latest example/regression: did that work before, i.e. does it work with --enableMoreCompleteExhale when using the default branch? Just double-checking.

[viper-admin]

@vakaras commented on 2019-06-28 12:35

Yes, the test was passing.

[viper-admin]

@vakaras commented on 2019-06-30 20:30

The latest version of scmalte_silicon_issue_387 branch on the following example

field discriminant: Int

field next: Ref

function contains(_pure_1: Ref): Bool
  requires acc(BoxList(_pure_1), read$())
{
    unfolding acc(BoxList(_pure_1), read$()) in (!(_pure_1.discriminant == 0) &&
    (contains(_pure_1.next)))
}

predicate BoxList(self: Ref) {
  acc(self.discriminant) && acc(self.next) && acc(BoxList(self.next))
}

function read$(): Perm
  ensures none < result
  ensures result < write

gives the following warnings from Z3:

field discriminant: Int

field next: Ref

function contains(_pure_1: Ref): Bool
  requires acc(BoxList(_pure_1), read$())
{
    unfolding acc(BoxList(_pure_1), read$()) in (!(_pure_1.discriminant == 0) &&
    (contains(_pure_1.next)))
}

predicate BoxList(self: Ref) {
  acc(self.discriminant) && acc(self.next) && acc(BoxList(self.next))
}

function read$(): Perm
  ensures none < result
  ensures result < write

[viper-admin]

@vakaras commented on 2019-07-03 14:16

The following example fails to verify with the latest version of scmalte_silicon_issue_387 branch:

field discriminant: Int

field enum_Some: Ref

field next: Ref

function contains(_pure_1: Ref): Bool
  requires acc(List(_pure_1), read$())
{
  (unfolding acc(List(_pure_1), read$()) in
  (unfolding acc(OptionBoxList(_pure_1.next), read$()) in
  (_pure_1.next.discriminant == 1 ==> contains(_pure_1.next.enum_Some))
  )
  )
}

function Option_discriminant(self: Ref): Int
  requires acc(OptionBoxList(self), read$())
{
  (unfolding acc(OptionBoxList(self), read$()) in self.discriminant)
}

function read$(): Perm
  ensures none < result
  ensures result < write

predicate List(self: Ref) {
  acc(self.next, write) && acc(OptionBoxList(self.next), write)
}

predicate OptionBoxList(self: Ref) {
  acc(self.discriminant, write) && acc(self.enum_Some, write) && (self.discriminant == 1 ==> acc(List(self.enum_Some), write))
}

method m_append()
{
  var _1: Ref
  var _10: Ref
  var _12: Ref
  var _13: Ref
  
  inhale acc(List(_1), write)

  unfold acc(List(_1), write)

  inhale acc(List(_12), write)
  unfold acc(List(_12), write)

  inhale acc(OptionBoxList(_13), write)
  inhale Option_discriminant(_13) == 0
  _12.next := _13
  fold acc(List(_12), write)
  // assert contains(_12)       // Uncommenting makes to pass.

  inhale acc(OptionBoxList(_10), write)
  inhale Option_discriminant(_10) == 1
  unfold acc(OptionBoxList(_10), write)
  _10.enum_Some := _12

  _1.next := _10
  fold acc(OptionBoxList(_1.next), write)
  fold acc(List(_1), write)

  assert contains(_1)
}

[viper-admin]

@fpoli commented on 2019-07-09 11:32

Now the Debian package for Silicon somehow differs from the Silicon version built by Jenkins: on some examples, using --enableMoreCompleteExhale, the former correctly verifies programs that the latter does not.

[viper-admin]

@alexanderjsummers commented on 2019-08-28 10:36

Hi all. Any idea what the status of this issue currently is?

[mschwerhoff]

@vakaras @alexanderjsummers

• Incompleteness in MoreCompleteExhale #387 (comment) verifies with the most recent Silicon version, and Z3 4.8.7 x64 on Windows 10
• as does Incompleteness in MoreCompleteExhale #387 (comment)
• as does Incompleteness in MoreCompleteExhale #387 (comment)
• as does Incompleteness in MoreCompleteExhale #387 (comment)
• as does Incompleteness in MoreCompleteExhale #387 (comment)
• as does Incompleteness in MoreCompleteExhale #387 (comment)

Let me know if you see a reason for keeping the issue open.

[vakaras]

I think it can be closed for now. I will reopen in case I find more issues.

[JonasAlaif]

@marcoeilers the following example fails with --enableMoreCompleteExhale, but works in Silicon without the flag:

domain ArrayDomain {}

field val_int: Int
field val_ref: Ref

function idx_into(a: ArrayDomain, a_len: Int): Int
function array_len(a: ArrayDomain): Int
function to_domain(self: Ref): ArrayDomain
  requires acc(Array(self), read$())

function read$(): Perm
  ensures none < result
  ensures result < write

predicate Array(self: Ref)
predicate usize(self: Ref) {
  acc(self.val_int, write)
}

method foo() {
  var a: Ref
  var a_len: Int
  var _3: Ref
  var unknown: Ref
  var i: Ref
  inhale acc(a.val_ref, write) && acc(Array(a.val_ref), write)

  inhale acc(_3.val_ref, write) && acc(usize(unknown), read$()) // <- removing this makes it pass

  exhale acc(a.val_ref, read$())

  inhale acc(usize(i), write) && acc(a.val_ref, read$())

  inhale (unfolding acc(usize(i), write) in
      (forall q: Int ::
        !(q < i.val_int) ||
        idx_into(to_domain(a.val_ref), q) <=
        idx_into(to_domain(a.val_ref), i.val_int)))
  assert (unfolding acc(usize(i), write) in
      (forall q: Int ::
        !(q < i.val_int) ||
        idx_into(to_domain(a.val_ref), q) <=
        idx_into(to_domain(a.val_ref), i.val_int)))
}

Sorry that it isn't more minimized. Adding triggers doesn't change things I think.

[vfukala]

The last example above can be further reduced to

field val_ref: Ref

function holds(a: Ref, b: Int): Bool

method foo() {
  var a: Ref
  var _3: Ref

  inhale acc(a.val_ref, write)

  inhale acc(_3.val_ref, write) // <- removing this makes it pass

  exhale acc(a.val_ref, 1 / 2)
  inhale acc(a.val_ref, 1 / 2)

  inhale forall q: Int :: holds(a.val_ref, q)
  assert forall q: Int :: holds(a.val_ref, q) // "Assert might fail." here
}

This doesn't verify in Silicon with --enableMoreCompleteExhale, but it verifies successfully in Carbon or in Silicon without the flag.

As per the comment in the code, removing one of the inhales makes it work even with the flag. Alternatively, removing the exhale acc(a.val_ref, 1 / 2) together with the subsequent inhale acc(a.val_ref, 1 / 2) also makes it verify with the flag.

[vfukala]

The current example can be reduced even further to

field val: Bool

method foo() {
  var a: Ref
  var b: Ref

  inhale acc(a.val, write)

  inhale acc(b.val, write) // <- removing this makes it pass

  exhale acc(a.val, 1 / 42) // <- (alternatively) removing this also makes it pass

  assume forall q: Int :: a.val
  assert a.val // "Assert might fail." here
}

The behavior (of Carbon and Silicon with/without flag) is the same as in my last comment.

[marcoeilers]

The last two examples by @vfukala verify now after PR #760. Unfortunately, the example @JonasAlaif added has a more fundamental problem and still doesn't verify.

[marcoeilers]

Now that last one also works. I'll close it again until someone finds a new incomplete example.