Fold-unfold error due to type containing shared references in Partialeq derivation

[enjhnsn2]

Hello, when you derive PartialEq for an enum with multiple variants that each have multiple arguments:

use prusti_contracts::*;

#[derive(PartialEq)]
pub enum Binop {
    Add(u32, u32),  
    Sub(u32, u32), 
}

the verifier fails with error:

 [Prusti internal error] unexpected verification error: [fold.failed:insufficient.permission] Folding m_Binop$_beg_$_end_Add(old[l17](_14.val_ref).enum_Add) might fail. There might be insufficient permission to access old[l17](_14.val_ref).enum_Add (@171.10)

When the enum has only 1 variant:

#[derive(PartialEq)]
pub enum Binop {
    Add(u32, u32),  
}

It passes.

When each variant only has 1 argument

#[derive(PartialEq)]
pub enum Binop {
    Add(u32),
    Sub(u32),
}

It also passes. Any ideas?

[fpoli]

Thanks for the report. The Viper encoding of ParialEq's eq and ne pure functions, in particular the part that restores the permissions of expiring borrows, is incorrect. The MIR code generated by the compiler creates a tuple containing shared references, which is a type that is not fully supported. So, we might miss an unsupported-feature check there that would reject the program. Anyway, the user experience is bad because all of this code is not visible to the user.

I investigated a bit more. The fold-unfold algorithm runs fine, which suggests that the transfer-perm statements are generated incorrectly, which is possible if unsupported code is being verified. I checked if it's perhaps a regression introduced by https://github.com/viperproject/prusti-dev/pull/739, and it's not. I get the same error using commit adfda1e34336dd1fdf54067b4fd248ab592020fc.

[fpoli]

The tuple that I'm referring to is _13 in block 6 of the MIR of PartialEq::eq.

Block 6:

_14 = &(*_1)
_15 = &(*_2)
_13 = (move _14, move _15)

MIR:

[fpoli]

This error arises from the impure encoding of pure functions; the pure encoding works fine with types containing shared references.

This implementation of PartialEq doesn't contain any panic, function call or operation that should be checked. We could detect these cases and skip the impure encoding.

[fpoli]

Adding #[trusted] should avoid this issue. Since there is no user-written function on which to add the attribute, #[extern_spec] should help. I haven't tried.

[fpoli]

For the record, I tried the following but it's still not enough.

#[extern_spec]
impl PartialEq<Binop> {
    #[pure]
    #[trusted]
    fn eq(&self, other: &Binop) -> bool;

    #[pure]
    #[trusted]
    fn ne(&self, other: &Binop) -> bool;
}

[enjhnsn2]

Hmm, could it have something to do with the fact that eq and partialeq are treated specially in the procedure encoder? https://github.com/viperproject/prusti-dev/blob/master/prusti-viper/src/encoder/procedure_encoder.rs#L2266-L2306

The function that encodes them is here: https://github.com/viperproject/prusti-dev/blob/75eec658bfc8fe716d8f465d30bf4d6eb5b12012/prusti-viper/src/encoder/procedure_encoder.rs#L2740-L2797

I will investigate further.

[fpoli]

It could be, but I don't see anything obviously wrong in that snippet and I suspect that the #[extern_spec] doesn't work because of the generic type parameter on the trait, which could confuse the way #[extern_spec] are matched to functions.

[Pointerbender]

The same also happens for enums that have struct variants:

#[derive(PartialEq)]
pub enum Binop {
    Add { left: u32, right: u32 },
    Sub { left: u32, right: u32 }, 
}

Produces an error:

error: [Prusti internal error] unexpected verification error: [fold.failed:insufficient.permission] Folding m_Binop$_beg_$_end_Add(old[l17](_14.val_ref).enum_Add) might fail. There might be insufficient permission to access old[l17](_14.val_ref).enum_Add (@12.10)
  --> src/lib.rs:12:10
   |
12 | #[derive(PartialEq)]
   |          ^^^^^^^^^
   |
   = help: This could be caused by too small assertion timeout. Try increasing it by setting the configuration parameter ASSERT_TIMEOUT to a larger value.
note: the failing assertion is here
  --> src/lib.rs:12:10
   |
12 | #[derive(PartialEq)]
   |          ^^^^^^^^^
   = note: this error originates in the derive macro `PartialEq` (in Nightly builds, run with -Z macro-backtrace for more info)

[Pointerbender]

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?

@enjhnsn2 for the example in your first post, a possible work-around can be to implement the Copy trait for your enum and get rid of the references during the match statement by first dereferencing, like so:

#[derive(Clone, Copy)]
pub enum Binop {
    Add(u32, u32),  
    Sub(u32, u32), 
}

impl PartialEq for Binop {
    fn eq(&self, other: &Self) -> bool {
        match (*self, *other) {
            (Self::Add(l0, l1), Self::Add(r0, r1)) => l0 == r0 && l1 == r1,
            (Self::Sub(l0, l1), Self::Sub(r0, r1)) => l0 == r0 && l1 == r1,
            _ => false,
        }
    }
}

Hope this helps :)