Function postconditions available too late

[viper-admin]

Created by @marcoeilers on 2018-09-26 10:26 Last updated on 2019-07-23 17:02

The order in which Silicon verifies functions (and their definitions therefore become available) does not take into account dependencies between functions resulting from predicate unfoldings. This can lead to spurious errors, as in the following example:

field f: Ref
predicate P(x: Ref) { acc(x.f) &&
                      x.f == makebla(x) && 
                      blahasproperty(x.f) // THIS LINE FAILS
}

function user(x: Ref): Bool
    requires P(x)
{
    unfolding P(x) in true
}           
function useruser(x: Ref): Bool
    requires P(x)
{
    user(x)
}         
function isbla(x: Ref): Bool
function blahasproperty(x: Ref) : Bool
    requires isbla(x)

function makebla(x: Ref) : Ref
    ensures isbla(result)

When verifying user, predicate P is unfolded and the precondition of blahasproperty is asserted. However, since Silicon does not realize that user indirectly depends on makebla, its postcondition is not available yet at this point, and the assertion fails.

[viper-admin]

@Felalolf commented on 2019-07-23 17:02

I tried to simplify the test a bit.

predicate P(x: Int) { 
  producer(x) && 
  consumer(x) // THIS LINE FAILS
}

domain Dummy {
  function item(x: Int): Bool
}

function consumer(x: Int) : Bool
    requires item(x)

function producer(x: Int) : Bool
    ensures item(x)

function Client(x: Int): Bool
    requires P(x)
    // requires [true, producer(x)] // This forces producer to be axiomatized first and thus makes the postcondition available.
{
    unfolding P(x) in true
}

[marcoeilers]

Commit 01a41d8eae248fefb63933e21d59872fa40cfbe0 added a command line option --alternativeFunctionVerificationOrder which changes the computation of dependencies between functions to also take into account dependencies stemming from predicate unfoldings, which fixes the problem (but leads to incompleteness in other cases, which is why it's not on by default).