Description
Created by @mschwerhoff on 2014-08-19 19:06
Last updated on 2015-01-23 07:07
Consider the following code:
#!text
field f: Int
predicate FF(x: Ref, y: Ref) {
acc(x.f) && acc(y.f)
}
function fun4(x: Ref, y: Ref): Int
requires acc(FF(x, y))
{ unfolding acc(FF(x, y)) in x.f }
method test7(x: Ref, y: Ref)
requires acc(FF(x, y)) && fun4(x, y) == 1
{
assert x != null // holds
assert y != null // fails
}
When axiomatising functions such as fun4, Silicon includes the assumption that all receivers of field dereferences that occur inside function bodies are non-null (which is justified by the corresponding accessibility predicate). For fun4, for example, it would generate an axiom that (simplified) says forall x, y :: fun4(x, y) = ... && x != null.
Silicon does not add such an assumption for receivers which are used in accessibility predicates inside predicates which are unfolded inside functions, but whose corresponding locations are not actually dereferenced in the body. The receiver y used in acc(y.f) in predicate FF(x, y) above is an example of this.
It is not clear, however, how deep one should go in order to find receivers that cannot be null. For example, what if FF contains another (non-recursive) predicate P(...) - should it be inspected as well? Or only if FF contains an unfolding acc(P(...))?
In my opinion the current level of looking for receivers that cannot be null - that is, only looking at which fields are dereferenced in the function body - is reasonably intuitive; after all, when applying a function we (in general) only get to reason about the function definition one level down.