A heap-dependent function can lead to a matching loop without any explicit quantifiers

[viper-admin]

Created by @vakaras on 2018-07-25 09:06 Last updated on 2018-08-15 11:30

The function fib2 below causes a matching loop as illustrated with an assert in the method test2 (to verify this method, the verifier would need to unroll the function 4 times on its own, which means that it is very likely that the verifier would try to unroll the function arbitrary number of times, which means that we have a matching loop):

#!silver

field val: Int
predicate P(this: Ref) {
acc(this.val)
}

function fib2(this: Ref, n: Int): Int
requires acc(P(this), wildcard)
{
unfolding acc(P(this), wildcard) in n < 2 ? 1 : fib2(this, n-1) + fib2(this, n-2)
}

method test2(this: Ref)
requires P(this)
{
// assert fib2(0) == 1
// assert fib2(1) == 1
// assert fib2(2) == 2
// assert fib2(3) == 3
unfold P(this)
fold P(this)
// Verifies: we have a matching loop.
assert fib2(this, 4) == 5
}

While the function fib2 looks very artificial, it feels quite natural if the predicate P contains quantified permissions. The problem with this function is that the unfolding expression covers recursive calls which tricks the current heuristic implemented in our verifiers. A work around would be to change the unfolding to not include the recursive calls:

#!silver

(unfolding acc(P(this), wildcard) in n < 2) ? 1 : fib2(this, n-1) + fib2(this, n-2)

[viper-admin]

@vakaras commented on 2018-07-25 09:15

Carbon issue.

[viper-admin]

@mschwerhoff commented on 2018-08-07 14:04

@vakaras @alexanderjsummers Did you look at Z3's axiom instantiation statistics to confirm your matching loop theory ? It could also be that Z3's macro finder optimisation — an optimisation that affects axioms that (recursively) define mathematical functions, and that can probably be turned off for the purpose of debugging/exploring this issue — kicks in here.

Could also be related to https://github.com/viperproject/silicon/issues/204.

[viper-admin]

@vakaras commented on 2018-08-15 10:22

After adding the following method:

#!silver

method test2a(this: Ref, n: Int)
requires P(this)
{
    unfold P(this)
    fold P(this)
    assert fib2(this, n) > 0
}

I can see in the axiom profiler a long chain of alternating instantiations of fib2%limited and fib2%stateless.

Does this answer your question?

[viper-admin]

@mschwerhoff commented on 2018-08-15 10:59

Thanks for looking into this; a long chain is indeed a strong indicator for a matching loop. Did you by any chance check the chain manually to confirm that it is a matching loop, or did you perhaps use the axiom profiler's capabilities to confirm the matching loop?

[viper-admin]

@alexanderjsummers commented on 2018-08-15 11:30

I guess there should be no longer chains in such an example. I assume this concerns axioms which the back end generates (similarly for Carbon). We should perhaps check which triggers are generated for postcondition axioms. I suspect that the limited form of the function is used. This is useful for knowing something about recursive calls, but would also explain a potential loop if the postcondition mentions new calls. We might need another layer of limited functions or similar ideas here..