Prusti reported an internal error when analyzing a closure example

[soyo114]

Description

Prusti throws an internal error when analyze the following code, it seems that the root cause is related to the Rust closure.

fn main() {
    let c = |x,y| x * y; 
    let result = c(5,6);
}

internal error:

thread 'rustc' panicked at prusti-viper/src/encoder/procedure_encoder.rs:3406:57:
called `Option::unwrap()` on a `None` value

To Reproduce

Use the following command:

cargo prusti

Environment

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

[soyo114]

@fpoli Could you help confirm and fix this bug?

[Aurel300]

@soyo114 Thanks for the report. For closure-related features, please refer to the artefact of the closures paper for the time being. The current codebase here (on the master branch) may not support them fully. We are working on a larger re-engineering of Prusti, and we will replace this codebase with the new version once ready. We aim to add back support for closures as part of this change as well.

[soyo114]

Hi @Aurel300 , thanks for your explanation. I’ve also encountered some other crash bugs related to closures, each with different stack traces. I’ve included code examples and traces below to help with Prusti’s development.

Code Example1

use prusti_contracts::*;
fn borrow(x: &i32) {
    let unused = move || x;
}
pub fn test2(n: &mut i32) {
    for _ in 0..*n {
        borrow(n);
    }
}
fn main() {
    let mut x = i32::MAX;
    test2(&mut x);
}

Stack Trace1

thread 'rustc' panicked at prusti-interface/src/environment/polonius_info.rs:1141:30:
no entry found for key
stack backtrace:
  22:     0x562101cb7b63 - prusti_interface::environment::polonius_info::PoloniusInfo::get_loan_at_location::h43d0868029fd697b
  23:     0x562100cf009a - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_assign_operand::{{closure}}::hd7f9da69ebc2c2a5
  24:     0x562100cee39f - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_assign_operand::h4d490fbbe794bf39
  25:     0x562100d100f2 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_assign_aggregate::h455806196e419e3c
  26:     0x562100c0f3ab - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_assign::h3421a2b606b58dd2
  27:     0x562100c990f5 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_statement::hd1cdb7e86e4beef5
  28:     0x562100c968cb - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_statement_at::h8502e8cf413c5686
  ...

Code Example2

use prusti_contracts::*;
fn borrow(x: &i32) {
    let closure = |y| println!("{}", y);
    closure(x);
}
pub fn test2(n: &mut i32) {
    for _ in 0..*n {
        borrow(n);
    }
}
fn main() {
    let mut x = i32::MAX;
    test2(&mut x);
}

Stack Trace2

error: internal compiler error: compiler/rustc_middle/src/ty/generic_args.rs:910:9: type parameter `<upvars>/#2` (<upvars>/#2/2) out of range when substituting, args=[Closure(DefId(0:5 ~ testcase[8b12]::borrow::{closure#0}), [i8, Binder(extern "RustCall" fn((&'?5 i32,)), []), ()]), (&'?6 i32,)]

thread 'rustc' panicked at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/compiler/rustc_errors/src/lib.rs:1651:9:
Box<dyn Any>
stack backtrace:
  72:     0x5607bcb2cd62 - prusti_interface::environment::body::EnvBody::set_monomorphised::hd97b77f2edf0bca0
  73:     0x5607bcb2d06e - prusti_interface::environment::body::EnvBody::get_impure_fn_body::h5c9ffbefba6fa1e9
  74:     0x5607bb6384dc - prusti_viper::encoder::mir::contracts::interface::get_procedure_contract::hf43de0d2dd7c5608
  75:     0x5607bba2cd2d - <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::mir::contracts::interface::ContractsEncoderInterface>::get_procedure_contract_for_call::h47fbd0b16b14ceac
  76:     0x5607bbb3cc06 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_impure_function_call::hc3ebd49ca3f5e71e
  77:     0x5607bbb2e596 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_terminator::ha0d8cd41b358e21e
  78:     0x5607bbb13863 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_statement_at::h8502e8cf413c5686

Code Example3

struct Nonsense { m3: u32 }
impl Nonsense {
    fn valid(&self) -> bool {
        [(&self.m3,3)].iter().all(|&(m,d)|m%d==0)
    }
    fn m3_mut(&mut self) -> &mut u32 { &mut self.m3 }
}
fn main() {}

Stack Trace3

thread 'rustc' panicked at prusti-viper/src/encoder/foldunfold/mod.rs:851:21:
assertion failed: perm_amount.is_valid_for_specs()
stack backtrace:
  19:     0x55b260190c3a - <prusti_viper::encoder::foldunfold::FoldUnfold as vir::gen::polymorphic::cfg::visitor::CfgReplacer<prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt,prusti_viper::encoder::foldunfold::ActionVec>>::replace_stmt::{{closure}}::h986725729bb16d74
  20:     0x55b2600fbff1 - core::ops::function::impls::<impl core::ops::function::FnMut<A> for &mut F>::call_mut::h357fff768fbbc1ff
  21:     0x55b2609eeb4b - core::iter::traits::iterator::Iterator::find::check::{{closure}}::hb19f4d5e8f996012
  22:     0x55b26043482a - core::iter::traits::iterator::Iterator::try_fold::hfe44f17defea1086
  23:     0x55b260431de7 - core::iter::traits::iterator::Iterator::find::h454bdcc60eb262b7
  24:     0x55b2600c3781 - <core::iter::adapters::filter::Filter<I,P> as core::iter::traits::iterator::Iterator>::next::h63d7abbfe770f4b7
  25:     0x55b2609cb3a6 - <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::next::h5aa6dd3829002f8f
  26:     0x55b25ff8206c - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter_nested::SpecFromIterNested<T,I>>::from_iter::h5197b2a7598d8dbf
  27:     0x55b26002e88e - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::h7760c97c8929f02e
  28:     0x55b260028be7 - <alloc::vec::Vec<T> as core::iter::traits::collect::FromIterator<T>>::from_iter::ha273425951c4f6c5