viperproject
Inhale-exhale assertions unsound if used in functions or predicates
Created by @mschwerhoff on 2017-03-01 10:45 Last updated on 2019-08-28 10:07
Silicon's current way of representing the footprints of functions and predicates is unsound in combination with inhale-exhale assertions (expressions, i.e. pure assertions, are handled soundly), as illustrated by the example below.
This problem is described in more detail in my PhD thesis (cf. Section 3.3, subsection "Representing Partial Heaps as Snapshots").
Until the unsoundness if fixed, programs that use the following feature combinations are rejected by Silicon:
- inhale-exhale assertions in predicate bodies
- inhale-exhale assertions in function preconditions
field f: Int
field g: Int
predicate pair(x: Ref) {
[acc(x.f) && acc(x.g),
acc(x.g) && acc(x.f)]
}
method test01(x: Ref) {
inhale acc(x.f) && x.f == 22
inhale acc(x.g) && x.g == 3
fold acc(pair(x))
unfold acc(pair(x))
assert x.f == 3 && x.g == 22 // Should fail, but unsoundly holds
}
function getf(x: Ref): Int
requires [acc(x.f) && acc(x.g),
acc(x.g) && acc(x.f)]
{ x.f }
method test02(x: Ref) {
inhale acc(x.f) && x.f == 22
inhale acc(x.g) && x.g == 3
assert getf(x) == 3 // Should fail, but unsoundly holds
}
@mschwerhoff commented on 2017-03-01 10:46
See also https://github.com/viperproject/silicon/issues/160
@alexanderjsummers commented on 2019-08-28 10:07
This will potentially be resolved by (an extension of) Mauro’s work, right?