Carbon and Silicon check for each predicate whether the body is self-framing. However, (in cases where the amounts of permission involved rule out aliasing possibilities) this check might not imply that every fractional amount of this body is self-framing. As a result, both verify the following program (explanation below the listing), but I think they should report an error:
field f: Int
field g: Int
predicate R(x: Ref, y: Ref) {
acc(x.f) && acc(y.f) && (x == y ==> y.g > 0)
}
method main(a: Ref)
requires acc(a.g) && acc(a.f)
ensures false
{
a.g := 1
fold acc(R(a,a), 1/2) // Point A
a.g := -1 //Point B
unfold acc(R(a,a),1/2) // Point C
}
The body of R(x,y) is self-framing (because the first two conjuncts ensure that x != y). However, the body of acc(R(x,y),1/2) is not self-framing (note that the field accessed on the right of the implication is different; no permissions to it are held in the predicate body). The example exploits this to prove false in main. At point A, the predicate instance acc(R(a,a),1/2) is folded whose body is not self-framing, which is possible because the permission to a.g is held outside the predicate instance. At point B, a heap assignment is executed such that the body of acc(R(a,a),1/2) is violated. This violation leads to a contradiction after the unfold at point C.
In summary, since the Viper verifiers frame predicates around operations such as heap assignments, predicate instances must be self-framing. Here, there are predicate instances, which are not self-framing and thus I think the Viper verifiers should report an error.
A natural solution would be to check whether a predicate body is self-framing for every fraction. However, this might be too restrictive, because there may be programs in practice where the current self-framing check (which just checks whether the body is self-framing for fraction 1) is sufficient but where the stronger check for every fraction may fail. For instance, the current self-framing check is likely sufficient if no predicate instance with fraction less than 1 is used. Moreover, if function calls are used in predicate instances with preconditions that specify concrete fractions, then the stronger condition will not hold.
Carbon and Silicon check for each predicate whether the body is self-framing. However, (in cases where the amounts of permission involved rule out aliasing possibilities) this check might not imply that every fractional amount of this body is self-framing. As a result, both verify the following program (explanation below the listing), but I think they should report an error:
The body of
R(x,y)is self-framing (because the first two conjuncts ensure thatx != y). However, the body ofacc(R(x,y),1/2)is not self-framing (note that the field accessed on the right of the implication is different; no permissions to it are held in the predicate body). The example exploits this to prove false in main. At point A, the predicate instanceacc(R(a,a),1/2)is folded whose body is not self-framing, which is possible because the permission toa.gis held outside the predicate instance. At point B, a heap assignment is executed such that the body ofacc(R(a,a),1/2)is violated. This violation leads to a contradiction after the unfold at point C.In summary, since the Viper verifiers frame predicates around operations such as heap assignments, predicate instances must be self-framing. Here, there are predicate instances, which are not self-framing and thus I think the Viper verifiers should report an error.
A natural solution would be to check whether a predicate body is self-framing for every fraction. However, this might be too restrictive, because there may be programs in practice where the current self-framing check (which just checks whether the body is self-framing for fraction 1) is sufficient but where the stronger check for every fraction may fail. For instance, the current self-framing check is likely sufficient if no predicate instance with fraction less than 1 is used. Moreover, if function calls are used in predicate instances with preconditions that specify concrete fractions, then the stronger condition will not hold.