Prusti crash bug related to dereference operations

[stoneman258]

While analyzing my Rust project with Prusti, the tool panicked with the error "internal error: entered unreachable code" when performing dereference operations inside a loop. The input program is provided below, and I used the command cargo prusti.

Code Example

fn main() {
    'outer_while: while true {
        let mut counter = Box::new(0);
        while *counter < 5 {
            *counter += 1;
            if *counter == 3 {
                break 'outer_while;
            }
        }
    }
}

Error Stacktrace

thread 'rustc' panicked at prusti-viper/src/encoder/procedure_encoder.rs:5382:42:
internal error: entered unreachable code: Adt(std::boxed::Box, [i32, Adt(std::alloc::Global, [])])
stack backtrace:
  18:     0x55e3e2f7b4c4 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_loop_invariant_permissions::h52a27851aed20c5d
  19:     0x55e3e2f8124e - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_loop_invariant_exhale_stmts::h2832c3abd2156764
  20:     0x55e3e2f21f94 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_loop::hec9439079eeae71e
  21:     0x55e3e2f1e081 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_blocks_group::h04afc5fa1fcae9bc
  22:     0x55e3e2f23580 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_loop::hec9439079eeae71e
  23:     0x55e3e2f1e081 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_blocks_group::h04afc5fa1fcae9bc
  24:     0x55e3e2f1a0b3 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode::hf06146a42e8f626d
  25:     0x55e3e2e22f34 - prusti_viper::encoder::encoder::Encoder::encode_procedure::h0682b71d927d722d
  26:     0x55e3e2e28c87 - prusti_viper::encoder::encoder::Encoder::process_encoding_queue::h7f215cb28c05bc29
  27:     0x55e3e281ae53 - prusti_viper::verifier::Verifier::verify::hb6a7d88218505da5
......

Environment

Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC

[stoneman258]

I find two other examples that caused the crash, and based on the stack trace, they are caused by different reasons. The first example shows that Rust's 'match' statements also exhibit this problem, triggering Prusti's 'unregistered verification error'.

First Code example

pub enum E3 {
    V1(u32),
    V2(u32),
}
pub fn test3(e: &mut E3) -> &mut u32 {
    match e {
        E3::V1(ref mut b) => {
            *b = b.saturating_sub(1); 
            b
        }
        E3::V2(ref mut b) => b,
    }
}
fn main() {
    let mut e = E3::V1(3);
    test3(&mut e);
}

Error Stacktrace

error: [Prusti: internal error] Prusti encountered an unexpected internal error
  |
  = 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: This is likely to be a bug in Prusti. We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
  = note: Details: unregistered verification error: [fold.failed:insufficient.permission; 0] Folding m_E3$_beg_$_end_V1(old[l13](_1.val_ref).enum_V1) might fail. There might be insufficient permission to access u32(self.f$0) (@0.0)

Second Code Example

struct Nonsense {
    m3: u32,
}
impl Nonsense {
    fn m3_mut(&mut self) -> &mut u32 {
        return &mut self.m3;
    }
}
fn test(arg: &mut Nonsense) {
    let m3 = &mut *arg.m3_mut();
    *m3 = (*m3).wrapping_add(3); 
}
fn main() {
}

Error Stacktrace

error: [Prusti: internal error] Prusti encountered an unexpected internal error
  --> src/main.rs:10:20
   |
10 |     let m3 = &mut *arg.m3_mut();
   |                    ^^^^^^^^^^^^
   |
   = 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: This is likely to be a bug in Prusti. We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
   = note: Details: unhandled verification error: Applying wand might fail. There might be insufficient permission to access u32(_old$l2$0) (@9.0)
            [apply.failed:insufficient.permission] ApplyMagicWandOnExpiry