[ICE] 'no entry found for key' panic

[niluxv]

When I try to compile/verify a small project (without any prusti annotations yet) using cargo-prusti it panics with the following error:

thread 'rustc' panicked at 'no entry found for key', prusti-interface/src/environment/polonius_info.rs:1160:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

error: internal compiler error: unexpected panic

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

note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: Prusti version: commit 9546a21 2021-03-16 14:50:28 UTC, built on 2021-03-16 14:57:41 UTC

OS: GNU/linux (Ubuntu) Prusti version: Nightly Release v-2021-03-16-1526 release

[Aurel300]

How do you invoke Prusti? What is the small project – have you tried with e.g. an empty main and nothing else?

[niluxv]

I invoke prusti from the commandline as cargo-prusti. It was a small library project, but I now minimised it down to a lib.rs

pub unsafe fn volatile_write_zero(ptr: *mut u8) {
    core::ptr::write_volatile(ptr, 0u8);
}

When I now compile this with env RUST_BACKTRACE=1 cargo-prusti I get the following output:

thread 'rustc' panicked at 'no entry found for key', prusti-interface/src/environment/polonius_info.rs:1160:9
stack backtrace:
   0: rust_begin_unwind
             at /rustc/d6eaea1c8860adb5302d2fbaad409e36585ab217/library/std/src/panicking.rs:493:5
   1: core::panicking::panic_fmt
             at /rustc/d6eaea1c8860adb5302d2fbaad409e36585ab217/library/core/src/panicking.rs:92:14
   2: core::option::expect_failed
             at /rustc/d6eaea1c8860adb5302d2fbaad409e36585ab217/library/core/src/option.rs:1321:5
   3: prusti_interface::environment::polonius_info::PoloniusInfo::get_loan_at_location
   4: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_assign_operand
   5: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_statement
   6: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_statement_at
   7: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_blocks_group
   8: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode
   9: prusti_viper::encoder::encoder::Encoder::encode_procedure
  10: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
  11: prusti_viper::verifier::Verifier::verify
  12: prusti_driver::verifier::verify
  13: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
  14: rustc_interface::queries::<impl rustc_interface::interface::Compiler>::enter
  15: rustc_span::with_source_map
  16: 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.

note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: Prusti version: commit 9546a21 2021-03-16 14:50:28 UTC, built on 2021-03-16 14:57:41 UTC

query stack during panic:
end of query stack

An empty function

pub unsafe fn empty() {}

verifies fine, but

pub unsafe fn take_ptr(_ptr: *mut u8) {}

errors with a different error than the above one:

thread 'rustc' panicked at 'assertion failed: !state.contains_pred(&prefix)', prusti-viper/src/encoder/foldunfold/semantics.rs:90:25
stack backtrace:
   0: rust_begin_unwind
             at /rustc/d6eaea1c8860adb5302d2fbaad409e36585ab217/library/std/src/panicking.rs:493:5
   1: core::panicking::panic_fmt
             at /rustc/d6eaea1c8860adb5302d2fbaad409e36585ab217/library/core/src/panicking.rs:92:14
   2: core::panicking::panic
             at /rustc/d6eaea1c8860adb5302d2fbaad409e36585ab217/library/core/src/panicking.rs:50:5
   3: <prusti_common::vir::ast::stmt::Stmt as prusti_viper::encoder::foldunfold::semantics::ApplyOnState>::apply_on_state
   4: <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
   5: prusti_viper::encoder::foldunfold::add_fold_unfold
   6: prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode
   7: prusti_viper::encoder::encoder::Encoder::encode_procedure
   8: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
   9: prusti_viper::verifier::Verifier::verify
  10: prusti_driver::verifier::verify
  11: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
  12: rustc_interface::queries::<impl rustc_interface::interface::Compiler>::enter
  13: rustc_span::with_source_map
  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.

note: We would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new

note: Prusti version: commit 9546a21 2021-03-16 14:50:28 UTC, built on 2021-03-16 14:57:41 UTC

query stack during panic:
end of query stack

[vakaras]

Thank you for the bug report! Raw pointers and unsafe code are not supported yet. However, we should report a nice error message instead of crashing.