Unsoundness: a heap dependent function is instantiated even when its precondition does not hold

[viper-admin]

Created by @mschwerhoff on 2019-05-08 09:12

function Void$discriminant(self: Ref): Int
  requires acc(Void(self))
  ensures false
{
  unfolding acc(Void(self)) in 8
}

predicate Void(self: Ref) {
  false
}

method m_void$$unreachable$opensqu$0$closesqu$() returns (_0: Ref) {
  var b: Bool

  if (b) { /* This allows proving the final assert on both branches */
    inhale Void(null)
    b := Void$discriminant(null) == 0
  }

  /* Doesn't allow proving the final assert */
//   b := perm(Void(null)) == write ==> Void$discriminant(null) == 0

  assert false
}

See also Silicon issue #376.

[gauravpartha]

The above example does not anymore seem to behave as described above in Carbon. Nevertheless, the unsoundness still exists theoretically.

Carbon generates a postcondition axiom of the following form (quantifiers removed for presentation):

[ state(Heap, Mask) && ( AssumeFunctionsAbove < 0 || ...) ] ==> false

The left hand side is true in the Boogie encoding after inhaling the precondition and thus, one can prove “assert false” right at the beginning (if one ignores triggers). The problem is that Carbon does not guard the postcondition axiom by the full precondition (permissions are ignored; functional properties in the precondition are taken into account).

[gauravpartha]

An instance where an unsoundness can be observed is the cyclic list example in the Silver test suite:

field value: Int
field next: Ref

predicate valid(this: Ref) {
     acc(this.value, write)
  && acc(this.next, write)
  && (((this.next) != (null)) ==> acc(valid(this.next), write))
}

function length(this: Ref): Int
  requires acc(valid(this), write)
  ensures result > 0
{ (unfolding acc(valid(this), write) in (((this.next) == (null)) ? 1 : 1 + length(this.next))) }

method test2(this: Ref)
{
  var x: Ref

  x := new(value, next)
  x.next := x

  assert ((length(x)) == (length(x.next) + 1)) //assertion A
  assert false
}

Assertion A should fail because it is not well-defined (i.e., the precondition valid(x) does not hold). Carbon correctly reported this well-definedness error. However, if one makes minor changes that do not change the meaning of Carbon's generated Boogie encoding (such as adding/removing redundant assumptions), it can happen that Carbon can deduce false and prove the method correct. The reason Carbon can deduce false is because right before point A:

1. x.next == x
2. From 1), length(x.next) == length(x) [note at the Boogie level, length is a Boogie function not guarded by any precondition]
3. length(x) == length(x.next)+1 (since x != null and using the definitional axiom, which is not guarded by the valid precondition in length).

2 and 3 together lead to a contradiction.

In particular, the PR https://github.com/viperproject/carbon/pull/407 leads to Carbon being able to derive false, where the PR only makes changes to the Boogie program that do not change the program's semantics.