Incompleteness: Carbon cannot prove that a memory location did not change even though it always held a predicate to it

[viper-admin]

Created by @vakaras on 2019-06-26 15:21
Last updated on 2019-06-26 16:04

In the following example, the last assert fails:

field val_int: Int

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

method test() returns (_0: Ref)
{
  var _1: Ref
  var _2: Ref
  inhale acc(i32(_1), write)
  label pre
  inhale acc(_2.val_int, write)
  _2.val_int := 0
  fold acc(i32(_2), write)
  assert (unfolding acc(i32(_1), write) in _1.val_int) == old[pre]((unfolding acc(i32(_1), write) in _1.val_int))
}

It seems that it is sufficient to exhale something that is not known to be disjoint to cause a problem:

field val_int: Int

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

method test() returns (_0: Ref)
{
  var _1: Ref
  var _2: Ref
  inhale acc(i32(_1), write)
  label pre
  inhale acc(_2.val_int, write)
  exhale acc(_2.val_int, write)
  assert (unfolding acc(i32(_1), write) in _1.val_int) == old[pre]((unfolding acc(i32(_1), write) in _1.val_int))
}

[viper-admin]

@vakaras commented on 2019-06-26 16:04

In the second example, even adding assume _1 != _2 does not help. (It does in the first one.)

[tdardinier]

It seems that for both examples, Carbon can infer that the memory location did not change just by unfolding the predicates.

For both examples, I just added a dummy assertion that unfolds the predicates. The following code verifies with Carbon:

field val_int: Int

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

method example1() returns (_0: Ref)
{
  var _1: Ref
  var _2: Ref
  inhale acc(i32(_1), write)
  label pre
  inhale acc(_2.val_int, write)
  _2.val_int := 0
  fold acc(i32(_2), write)

  assert unfolding i32(_1) in unfolding i32(_2) in true // Added

  assert (unfolding acc(i32(_1), write) in _1.val_int) == old[pre]((unfolding acc(i32(_1), write) in _1.val_int))
}


method example2() returns (_0: Ref)
{
  var _1: Ref
  var _2: Ref
  inhale acc(i32(_1), write)
  label pre
  inhale acc(_2.val_int, write)

  assert unfolding i32(_1) in true // Added

  exhale acc(_2.val_int, write)
  assert (unfolding acc(i32(_1), write) in _1.val_int) == old[pre]((unfolding acc(i32(_1), write) in _1.val_int))
}

[tdardinier]

The reason for this comes from how Carbon handles exhale. When something (anything) is exhaled, Carbon creates a new heap, and assumes that the heap values of both heaps (the old and the new) are the same, for the heap locations where some permission is held.

When a predicate is unfolded (even in a dummy assertion), the permissions inside will be known to be folded. Thus the memory locations referred by these permissions will conserve their values after an exhale.

The following program doesn't verify with Carbon:

field f: Int
field g: Bool

predicate p(x: Ref) { acc(x.f) }

method test(x: Ref, y: Ref)
  requires p(x) && acc(y.g)
{
  label pre

  // assert unfolding p(x) in true // Verifies if uncommented
  exhale acc(y.g) // Fails if uncommented, verifies if commented

  assert (unfolding p(x) in x.f) == old[pre]((unfolding p(x) in x.f))
}

However, it verifies if either:

• The exhale is commented.
• The dummy assertion is uncommented.

Regarding this program, whether it should verify or not depends on the semantics of predicates. It should verify if predicates are equirecursive, but it shouldn't if predicates are isorecursive.