Performance issues when combining predicates and reborrows

[Pointerbender]

The following Rust program:

use prusti_contracts::*;

#[derive(Copy, Clone)]
pub struct A {
    pub field0: usize,
    pub field1: isize,
    pub field2: u64,
    pub field3: i64,
    pub field4: [i32; 64],
    pub field5: [u32; 64],
    pub field6: usize,
    pub field7: isize,
    pub field8: u64,
    pub field9: i64,
    pub field10: [i32; 64],
    pub field11: [u32; 64],
    pub field12: usize,
    pub field13: isize,
    pub field14: bool,
    pub field15: bool,
}

predicate! {
    fn pred_a(a: &A) -> bool {
        true
    }
}

pub struct B {
    a: A,
}

impl B {
    #[requires(pred_a(&self.a))]
    #[requires(pred_a(a))]
    pub fn foo(&mut self, a: &A) -> bool {
        // self.bar(a);
        // self.bar(a);
        // self.bar(a);
        // self.bar(a);
        // self.bar(a);
        // self.bar(a);
        // self.bar(a);
        // self.bar(a);
        self.bar(a);
        self.bar(a)
    }

    #[pure]
    #[requires(pred_a(&self.a))]
    #[requires(pred_a(a))]
    pub fn bar(&self, a: &A) -> bool {
        true
    }
}

has an interesting performance problem :) From the command line Prusti verifies this program (leaving the statements commented) in 27 seconds while Viper IDE gives up within seconds with the error Exhale might fail. There might be insufficient permission to access struct$m_A(_1.val_ref.f$a) (lib.rs_prusti_example::B::[email protected]) around this part of the Viper code (right after the preconditions):

  label pre
  // ========== bb0 ==========
  __t0 := true
  // [mir] StorageLive(_3)
  // [mir] StorageLive(_4)
  // [mir] _4 = &(*_1)
  _4 := builtin$havoc_ref()
  inhale acc(_4.val_ref, write)
  _4.val_ref := _1.val_ref
  exhale acc(_1.val_ref.f$a, write - read$())
  inhale acc(_4.val_ref.f$a, read$())
  exhale acc(struct$m_A(_1.val_ref.f$a), write - read$())
  inhale acc(struct$m_A(_4.val_ref.f$a), read$())

Adding more self.bar(a); statements inside foo will drive up verification time significantly. When all statements are uncommented in the example, it takes 320 seconds for Prusti to verify the program for foo from the command line. Adding even more statements will push Prusti to a point where it will eventually hit the timeout limit. These factors seem to have a big impact on verification time:

• The number of fields in A, this makes the predicate for A larger and it takes more time to fold/unfold it.
• The complexity of the custom predicate pred_a, this can introduce more fold/unfold statements, e.g. if it would refer to other predicates in its body.
• The number of self.bar(a); statements, due to taking out more loans which each have to be expired again.

Looking at the 1100 lines of generated Viper code (with all statements uncommented), there is a lot of code handling expiration of loans, e.g.:

  // [mir] _3 = B::bar(move _4, move _5) -> [return: bb1, unwind: bb11]
  label l2
  _3 := builtin$havoc_ref()
  inhale acc(bool(_3), write)
  fold acc(struct$m_B(_4.val_ref), read$())
  inhale (unfolding acc(bool(_3), write) in _3.val_bool) == m_bar__$TY$__(snap$__$TY$__Snap$struct$m_B$(_4.val_ref), snap$__$TY$__Snap$struct$m_A$(_5.val_ref))
  // transfer perm _4.val_ref --> old[l2](_4.val_ref) // unchecked: false
  // transfer perm _5.val_ref --> old[l2](_5.val_ref) // unchecked: false
  // ========== l3 ==========
  // MIR edge bb0 --> bb1
  // Expire borrows
  // expire_borrows ReborrowingDAG(L35,L43,L34,L0,)

  if (__t0 && __t0) {
    // expire loan L43
    // transfer perm old[l2](_5.val_ref) --> old[l1](_5.val_ref) // unchecked: false
    exhale acc(struct$m_A(old[l1](_5.val_ref)), read$())
    // drop Acc(old[l1](_5.val_ref), write) (Acc(old[l1](_5.val_ref), write))
    // drop Acc(old[l2](_4.val_ref), write) (Acc(old[l2](_4.val_ref), write))
    // drop Pred(old[l2](_4.val_ref), read) (Pred(old[l2](_4.val_ref), read))
  }
  if (__t0 && __t0) {
    // expire loan L0
    // transfer perm old[l2](_4.val_ref) --> old[l0](_4.val_ref) // unchecked: false
    unfold acc(struct$m_B(old[l0](_4.val_ref)), read$())
    exhale acc(struct$m_A(old[l0](_4.val_ref).f$a), read$())
    exhale acc(old[l0](_4.val_ref).f$a, read$())
    inhale acc(_1.val_ref.f$a, write - read$())
    inhale acc(struct$m_A(_1.val_ref.f$a), write - read$())
    // drop Acc(old[l2](_5.val_ref), write) (Acc(old[l2](_5.val_ref), write))
    // drop Acc(old[l0](_4.val_ref), write) (Acc(old[l0](_4.val_ref), write))
    // drop Pred(old[l2](_5.val_ref), read) (Pred(old[l2](_5.val_ref), read))
    // drop Acc(_1.val_ref.f$a, write-read) (Acc(_1.val_ref.f$a, write-read))
    // restored (in branch merge): Acc(_1.val_ref.f$a, write-read) (Acc(_1.val_ref.f$a, write-read))
    // drop Pred(_1.val_ref.f$a, write-read) (Pred(_1.val_ref.f$a, write-read))
    // restored (in branch merge): Pred(_1.val_ref.f$a, write-read) (Pred(_1.val_ref.f$a, write-read))
  }

It seems to be a prerequisite to have at least one custom predicate! {} that's used in the contract of the method, without that I was not able to reproduce this performance problem. Another strange detail is that the performance issue is most visible when taking an immutable reborrow of a mutable borrow. If the method signature of foo is changed to pub fn foo(&self, a: &A) -> bool then it verifies in 70 seconds instead of 320 seconds.

[Pointerbender]

@alexanderjsummers per the Zulip chat, here are the two generated Viper files :) one with all the self.bar(a); statements uncommented and the other with just 2 self.bar(a); statements.

lib.rs_prusti_example::B::foo all statements.vpr.txt lib.rs_prusti_example::B::foo two statements.vpr.txt

[vakaras]

Thank you for the investigation! I will check how its performance changes in the refactored code once all of the used features are supported.