Inhale-exhale assertions unsound if used in functions or predicates

[viper-admin]

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
}

[viper-admin]

@mschwerhoff commented on 2017-03-01 10:46

See also https://github.com/viperproject/silicon/issues/160

[viper-admin]

@mschwerhoff on 2017-03-01 12:28:

• edited the description

[viper-admin]

@alexanderjsummers commented on 2019-08-28 10:07

This will potentially be resolved by (an extension of) Mauro’s work, right?