Crash due to two-phase borrows

[jmc-figueira]

The following verification crashes the compiler:

#[ensures(self.counters.lookup(id) == old(self.counters.lookup(id)) + 1)]
pub fn increment(&mut self, id: usize) {
    self.counters.modify(id, self.counters.lookup(id) + 1);
} 

with the error message:

thread 'rustc' panicked at 'The rhs place of statement '_8.val_ref := borrow _1.val_ref.f$counters // L1' is currently moved-out or blocked due to a borrow', prusti-viper/src/encoder/foldunfold/semantics.rs:86:21
stack backtrace:
   0: rust_begin_unwind
             at /rustc/d0695c9081b16077d0aed368bccaf437d77ff497/library/std/src/panicking.rs:493:5
   1: std::panicking::begin_panic_fmt
             at /rustc/d0695c9081b16077d0aed368bccaf437d77ff497/library/std/src/panicking.rs:435:5
   2: <prusti_common::vir::ast::stmt::Stmt as prusti_viper::encoder::foldunfold::semantics::ApplyOnState>::apply_on_state
   3: <prusti_viper::encoder::foldunfold::FoldUnfold as prusti_common::vir::cfg::visitor::CfgReplacer<prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt,prusti_viper::encoder::foldunfold::ActionVec>>::replace_stmt
   4: prusti_viper::encoder::foldunfold::add_fold_unfold
   5: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode
   6: prusti_viper::encoder::encoder::Encoder::encode_procedure
   7: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
   8: prusti_viper::verifier::Verifier::verify
   9: prusti_driver::verifier::verify
  10: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
  11: rustc_interface::queries::<impl rustc_interface::interface::Compiler>::enter
  12: rustc_span::with_source_map
  13: rustc_interface::interface::create_compiler_and_run
  14: scoped_tls::ScopedKey<T>::set
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

error: internal compiler error: unexpected panic

note: Prusti or the compiler unexpectedly panicked. This is a bug.

Full example

[fpoli]

This is interesting. It seems that the CFG of increment that we get from the compiler shouldn't borrow-check. In block 0 the shared reference _8 is created out of the mutable reference _1, but so does the mutable reference _4. It might be a case of two-phase borrows, which we don't support.

[fpoli]

Workaround:

    #[ensures(self.counters.lookup(id) == old(self.counters.lookup(id)) + 1)]
    pub fn increment(&mut self, id: usize) {
        let x = self.counters.lookup(id);
        self.counters.modify(id, x + 1);
    }