Exhaling unfolding expressions was not done correctly in all cases. Some of these issues have been resolved in Commit 1e2a95e. This issue summarizes the situation before the recent fixes and the remaining problems.
When exhaling an unfolding expression, the definedness check executed the unfold and the actual check evaluated the expression in the original state. Since the results of the definedness check were still available in most cases, this often worked out fine.
However, there are cases where this leads to unsound behaviour, as for example, observed in #213:
assert (unfolding P(r) in perm(r.next) == write)
In this assertion the perm expression was evaluated in the state before the unfold, which is incorrect.
There are also cases where this leads to incomplete behaviour, as for example, observed in #158 when unfolding within quantifiers:
assert forall r:Ref :: r in rs ==> unfolding p(r) in r.f >= 0
In this case, the definedness check was done in a separate branch and the assertion was checked using a single Boogie forall expression in the main branch (ignoring unfolds). Hence the assertion did not verify, since the results of the definedness check were not available.
Both issues shown above have been fixed for various cases. However, there are still some issues.
Perm expressions in disjunctions
Generally, unfolding expressions are evaluated in the correct state when asserted. However, for disjunctions this is not the case:
assert (unfolding P(r) in perm(r.next) >= 0 )) || (unfolding P(r2) in perm(r.next) >= 0))
Currently, the encoding of the actual disjunction check ignores unfoldings. The tricky part is that the left disjunct cannot be checked independently from the right disjunct.
Perm expressions in pure forall expression
The check for asserting pure forall expressions is now encoded in a separate branch (executing the potential unfoldings properly). In the main branch the expression is then assumed using a Boogie forall expression (which ignores unfoldings). Hence if perm expressions appear within unfoldings inside the quantifier, then the encoding is incorrect.
The general problem
Both problems (perm expressions in disjunctions and pure forall expressions) could be handled properly if executions of unfoldings could be expressed using a single Boogie expression instead of a sequence of statements. One could then use Boogie's disjunction and forall operator directly. This would also help with assumptions of pure forall expressions (which I have not considered yet):
assume forall r:Ref :: r in rs ==> unfolding p(r) in r.f >= 0
Currently, this is encoded using a single Boogie forall expression (ignoring the unfoldings) and is hence incomplete (the definedness check is in a separate branch). If one could express unfoldings using an expression, then one could deal with this using a single Boogie forall expression.
Update (13.05.2020): As Thibault noticed (#348 (comment)), in my attempt to fix perm expression inside unfoldings it could happen that a predicate was removed multiple times which wrongly led to an inconsistent states. I changed this in 1512209 so that the predicate is not removed during the unfolding, which an even earlier version had done correctly. This means that perm expressions inside unfolding expressions are not handled correctly for predicates after this latest change.
Exhaling unfolding expressions was not done correctly in all cases. Some of these issues have been resolved in Commit 1e2a95e. This issue summarizes the situation before the recent fixes and the remaining problems.
Before commit 1e2a95e
When exhaling an unfolding expression, the definedness check executed the unfold and the actual check evaluated the expression in the original state. Since the results of the definedness check were still available in most cases, this often worked out fine.
However, there are cases where this leads to unsound behaviour, as for example, observed in #213:
assert (unfolding P(r) in perm(r.next) == write)In this assertion the perm expression was evaluated in the state before the unfold, which is incorrect.
There are also cases where this leads to incomplete behaviour, as for example, observed in #158 when unfolding within quantifiers:
assert forall r:Ref :: r in rs ==> unfolding p(r) in r.f >= 0In this case, the definedness check was done in a separate branch and the assertion was checked using a single Boogie forall expression in the main branch (ignoring unfolds). Hence the assertion did not verify, since the results of the definedness check were not available.
After commit 1e2a95e
Both issues shown above have been fixed for various cases. However, there are still some issues.
Perm expressions in disjunctions
Generally, unfolding expressions are evaluated in the correct state when asserted. However, for disjunctions this is not the case:
assert (unfolding P(r) in perm(r.next) >= 0 )) || (unfolding P(r2) in perm(r.next) >= 0))Currently, the encoding of the actual disjunction check ignores unfoldings. The tricky part is that the left disjunct cannot be checked independently from the right disjunct.
Perm expressions in pure forall expression
The check for asserting pure forall expressions is now encoded in a separate branch (executing the potential unfoldings properly). In the main branch the expression is then assumed using a Boogie forall expression (which ignores unfoldings). Hence if perm expressions appear within unfoldings inside the quantifier, then the encoding is incorrect.
The general problem
Both problems (perm expressions in disjunctions and pure forall expressions) could be handled properly if executions of unfoldings could be expressed using a single Boogie expression instead of a sequence of statements. One could then use Boogie's disjunction and forall operator directly. This would also help with assumptions of pure forall expressions (which I have not considered yet):
assume forall r:Ref :: r in rs ==> unfolding p(r) in r.f >= 0Currently, this is encoded using a single Boogie forall expression (ignoring the unfoldings) and is hence incomplete (the definedness check is in a separate branch). If one could express unfoldings using an expression, then one could deal with this using a single Boogie forall expression.
Update (13.05.2020): As Thibault noticed (#348 (comment)), in my attempt to fix perm expression inside unfoldings it could happen that a predicate was removed multiple times which wrongly led to an inconsistent states. I changed this in 1512209 so that the predicate is not removed during the unfolding, which an even earlier version had done correctly. This means that perm expressions inside unfolding expressions are not handled correctly for predicates after this latest change.