Known-folded permissions are not updated in unfold statements leading to unsoundness

[Dev-XYS]

The known-folded permission mask of a predicate location stores an underestimation of heap locations folded inside the predicate location. The mask is apparently updated during a fold statement, where heap locations are added to the known-folded permission set.

However, in an unfold statement, the mask is not set to empty after unfolding all permissions of the predicate location. This leads to inconsistency if the same predicate location is later folded with a different (smaller) set of heap locations, after which the known-folded permission mask still keeps the old heap locations that are no longer folded in the predicate and therefore the mask stores the wrong information. After the unfold statement, the unsoundness can be triggered by exhaling where the heap is not havoced sufficiently.

The issue is demonstrated by the example below.

field f: Int
field b: Bool

predicate P(x: Ref) {
  acc(x.b) && (x.b ==> acc(x.f))  // If acc(x.f) is folded is controlled by the value of x.b.
}

method set_f_to_2(x: Ref)
  requires acc(x.f)
  ensures acc(x.f) && x.f == 2
{
  x.f := 2
}

method m(x: Ref)
  requires acc(x.b) && acc(x.f) && x.b && x.f == 1
{
  fold P(x)     // x.b is true, so acc(x.f) is folded inside P(x)
                // and is thus stored in the known-folded permission mask.
  unfold P(x)   // Unfold does not update the known-folded permission mask.
                // x.f is kept in the known-folded permission mask.

  x.b := false
  fold P(x)     // This time, acc(x.f) is not folded, but the
                // known-folded permission mask still keeps x.f.

  set_f_to_2(x) // x.f is not havoced due to being in the known-folded permission mask.
  assert false  // The postcondition inhales x.f == 2, leading to unsoundness.
}