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

[viper-admin]

Created by @vakaras on 2019-05-06 11:48
Last updated on 2019-05-08 09:13

The following example verifies in Silicon while it should not:

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)
{
  assert false
}

[viper-admin]

@mschwerhoff commented on 2019-05-06 12:43

This is most likely a duplicate of #369: since the resulting function axiom is trivial, Z3 eagerly instantiates it without respecting the triggers.

Technically probably related to #369, i.e. since the resulting function axiom is trivial, Z3 eagerly instantiates it without respecting the triggers. However, the consequences here seem much more far-reaching when compared to #369, where the function axiom is "merely" made available too early (which incorrectly allows proving the false postcondition), and for which a solution is known.

Here, it is less clear how to fix the problem: the function should verify, and since the method does not obtain an instance of predicate Void (for which no instances should exist), there is no logical reason for the assertion to hold. However, since permissions are stripped from function axioms, at least in Silicon, the axiom effectively has no precondition and is thus trivial enough so that Z3 instantiates it without respecting triggers.

A solution would probably be to include permissions in function axioms — basically rewrite accessibility predicates into appropriate perm expressions — and to pass permissions as another function argument at call site (analogous to passing the partial heap). Such a change is likely to affect performance, though.

@alexanderjsummers What do you think?

By the way, this also seems to be a problem for Carbon:

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
}

[viper-admin]

@mschwerhoff on 2019-05-06 12:43:

• changed component from (none) to Functions

[viper-admin]

@mschwerhoff commented on 2019-05-08 09:00

Another example:

field f: Int

function foo(x: Ref): Int
  requires acc(x.f) && acc(x.f)
  ensures false
{ x.f }

method m() {
  assert false
}

[viper-admin]

@mschwerhoff commented on 2019-05-08 09:10

Martin’s suggestion from the Viper meeting 7.5.'19 for a work-around: introduce a dummy SMT predicate (boolean function) over all quantified variables that guards the function axioms and that is assumed at each call-site.

The postcondition axiom for the previous example would then roughly look as follows:

forall s: Snap, x: Ref :: {foo(s, x)}
  true /* actual precondition */ && guard_foo(s,x) ==>
    false

Miscellaneous comments:

• Effect on performance needs to be benchmarked. A potential optimisation would be to determine when exactly Z3 considers an axiom to be simple enough — maybe if all three of pre-, postcondition and body do not mention all/any quantified variables?
• In the long run, it might be necessary or wanted to pass permissions in addition to snapshots.
• The guard could probably also be used to address Function postconditions are not checked soundly #369

[viper-admin]

@mschwerhoff commented on 2019-05-08 09:13

See also Carbon issue 272.

[mschwerhoff]

Following up on the comment from May 8, 2019: To allow recursive invocations, the dummy trigger would have to be part of the function axiom body as well. Think about whether the well-definedness checks suffice here, i.e. introduce the necessary trigger.

[marcoeilers]

Finally fixed.