Fold-unfold error due to type containing shared references

[JonasAlaif]

When encoding the following fn:

fn option_eq(l: &Option<i32>, r: &Option<i32>) -> bool {
    match (l, r) {
        (Some(l), Some(r)) => l == r,
        (None, None) => true,
        _ => false
    }
}

Prusti runs into issues with the ReborrowingDAG: it generates some random folds for things which were never unfolded. As it is a simple program Prusti doesn't crash but instead Viper finds the issue:

error: [Prusti internal error] unexpected verification error:
  [fold.failed:insufficient.permission] Folding m_Option$_beg_$i32$_end_Some(old[l0](_4.val_ref).enum_Some) might fail.
  There might be insufficient permission to access old[l0](_4.val_ref).enum_Some (@5.1)

@vakaras said that the whole ReborrowingDAG part should be replaced, but it depends on his work with VIR High.

[fpoli]

This is the same issue of https://github.com/viperproject/prusti-dev/issues/749. (l, r) is a type containing shared references, and that generates bad transfer-permission statements when expiring borrows. The pure encoding would work fine, but the impure encoding that properly checks the implementation has this limitation.

[enjhnsn2]

Speaking of #749, has there been any progress on the issue of shared reference tuples? I keep running into this issue when working with option/result/enum types. You mention that a real fix may involve replacing the whole ReborrowingDag, but is there any chance of a short term workaround or something of the sort?

[JonasAlaif]

Duplicate of #749

[JonasAlaif]

@fpoli Any idea on how to fix this issue? In the worst case we should report an error, rather than handing it over to Viper. Though we say that this is unsupported, it somehow works with structs but not enums:

struct Opt<T>(T);
fn eq(l: &Opt<i32>, r: &Opt<i32>) -> bool {
    match (l, r) {
        (Opt(l), Opt(r)) => l == r,
        _ => false,
    }
}

This program verifies just fine. In this version the Viper dump looks like:

  if (__t0 && (__t0 && __t0)) {
    // expire loan L11
    // transfer perm old[l3](_5.val_ref) --> old[l1](_5.val_ref) // unchecked: false
    fold acc(Opt(old[l1](_5.val_ref)), read$())
    exhale acc(Opt(old[l1](_5.val_ref)), read$())
    // ...
  }
  if (__t0 && (__t0 && __t0)) {
    // expire loan L9
    // transfer perm old[l3](_4.val_ref) --> old[l0](_4.val_ref) // unchecked: false
    fold acc(Opt(old[l0](_4.val_ref)), read$())
    exhale acc(Opt(old[l0](_4.val_ref)), read$())
    // ...
  }

Whereas in the enum version of things we get:

  if (__t0 && (__t0 && __t4)) {
    // expire loan L11
    // transfer perm old[l3](_4.val_ref) --> old[l0](_4.val_ref) // unchecked: false
    fold acc(Some(old[l0](_4.val_ref).enum_Some), read$())
    fold acc(Option(old[l0](_4.val_ref)), read$())
    exhale acc(Option(old[l0](_4.val_ref)), read$())
    fold acc(Some(_3.tuple_1.val_ref.enum_Some), read$())
    fold acc(Option(_3.tuple_1.val_ref), read$())
    // ...
  }
  if (__t0 && (__t0 && __t4)) {
    // expire loan L12
    // transfer perm old[l3](_5.val_ref) --> old[l1](_5.val_ref) // unchecked: false
    fold acc(Some(old[l1](_5.val_ref).enum_Some), read$())
    fold acc(Option(old[l1](_5.val_ref)), read$())
    exhale acc(Option(old[l1](_5.val_ref)), read$())
    // ...
  }

And since _3.tuple_1.val_ref.enum_Some and _5.val_ref.enum_Some alias folding the latter fails. There must be a bug somewhere which causes us to generate the erroneous:

fold acc(Some(_3.tuple_1.val_ref.enum_Some), read$())
fold acc(Option(_3.tuple_1.val_ref), read$())

And I don't think we can hide behind the fact that "we don't support reference-typed fields" - this only makes sense for signatures (i.e. wands), within a fn body we should be able to support them just fine.

[fpoli]

Regarding how to detect the case and report an error, before https://github.com/viperproject/prusti-dev/pull/117 and https://github.com/viperproject/prusti-dev/pull/121 we had a validation pass to report unsupported types. We could do something similar. The code is around here:

https://github.com/viperproject/prusti-dev/blob/143e673dc19b4c1363efade90ffee4f77641ec11/prusti-filter/src/validators/common_validator.rs#L134-L140

And I don't think we can hide behind the fact that "we don't support reference-typed fields" - this only makes sense for signatures (i.e. wands), within a fn body we should be able to support them just fine.

Loops require a similar abstraction, but I agree that if the code contains no reference-typed fields in the signature nor in loops, then a simple encoding should be possible. (I consider it more an extension than a bug because so far we never claimed to support reference-typed fields, even if in some cases Prusti happens to work fine.)

And since _3.tuple_1.val_ref.enum_Some and _5.val_ref.enum_Some alias folding the latter fails. There must be a bug somewhere which causes us to generate the erroneous:

At the end of the first if, the fold-unfold decides to stop tracking _3 (as hinted by the // drop Pred(_3.tuple_1.val_ref, read) comment) and in order to drop it the algorithm first folds the predicate. Not sure why, but I'm pretty sure the issue is with the drop, not with the fold. I suspect that the reason is in the way the transfer perm _3.tuple_0.val_ref --> old[l3](_4.val_ref) is handled; maybe it's ignoring some special fields like enum_Some. (To see the transfer perm statement you have to disable some optimizations that remove if statements that only contain comments and other no-op statements, which are useful for debugging.)

Note that in this case _3 is involved in two loans: one that restores _4 and one that restores _5, both encoded as if statements, which hit the above limitation of the fold-unfold algorithm. This is only possible if _3 is a structure containing reference-typed fields, which is why we usually say that the expire-references and/or fold-unfold algorithm don't support reference-typed fields.