[Silver Permission Inference] Existing invariants may cause inference of infinite permission.

[viper-admin]

Created by @dohrau on 2016-09-14 12:34

Currently, we are treating existing invariants as an exhale-inhale pair. As a result we are inferring an infinite amount of permission for the access paths a.f and a.f.f in the following example.

#!scala

method foo(a: Ref)
{
    while (true)
        invariant acc(a.f)
        invariant acc(a.f.f)
    {
    }
}

The reason for this is the following: Whenever there is an exhale, the alias analysis havocs the corresponding access path. Thus, it will tell us that the receivers of a.f and a.f.f may alias. Consequently, exhaling acc(a.f) in the permission inference will also exhale full permission for the access path a.f.f (and vice-versa). This means, in every loop iteration we exhale twice the amount of permission that is inhaled. Since the widening is not implemented yet, the analysis does not terminate. Once the widening is there this would cause the inference to infer an infinite amount of permission.

It is a bit odd that we treat the inferred invariants differently: In the following example, we infer the invariants invariant acc(a.f) and invariant acc(a.f.f). And if we run the inference on the output we are in the situation described above.

#!scala

method bar(a: Ref)
{
    while (true)
    {
        a.f := a.f
        a.f.f := null
    }
}