prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard
verified publisher icon viperproject

'index out of bounds' panic in mir_encoder

Open jeremysalwen opened this issue 3 years ago • 3 comments

Installed prusti through VS Code plugin, ran the checker on a small project, and hit the following crash:

thread 'rustc' panicked at 'index out of bounds: the len is 190 but the index is 190', prusti-viper/src/encoder/mir_encoder/mod.rs:417:9
stack backtrace:
   0:     0x7fe0ad01313c - std::backtrace_rs::backtrace::libunwind::trace::h793e05efd273d0f4
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7fe0ad01313c - std::backtrace_rs::backtrace::trace_unsynchronized::h640b7b86ff610c77
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fe0ad01313c - std::sys_common::backtrace::_print_fmt::h362fa2a4f354f877
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7fe0ad01313c - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::hf439e5ed84c74abd
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/sys_common/backtrace.rs:46:22
   4:     0x7fe0ad07037c - core::fmt::write::h72801a82c94e6ff1
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/core/src/fmt/mod.rs:1149:17
   5:     0x7fe0ad0038d5 - std::io::Write::write_fmt::h5562a8b6da0f0339
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/io/mod.rs:1697:15
   6:     0x7fe0ad016390 - std::sys_common::backtrace::_print::hb29ddd998d02631c
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/sys_common/backtrace.rs:49:5
   7:     0x7fe0ad016390 - std::sys_common::backtrace::print::h81965e3d7c90fbb6
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/sys_common/backtrace.rs:36:9
   8:     0x7fe0ad016390 - std::panicking::default_hook::{{closure}}::h84db205ab6674b38
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/panicking.rs:211:50
   9:     0x7fe0ad015f3b - std::panicking::default_hook::h1bf8bb4159936bca
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/panicking.rs:228:9
  10:     0x55afdc4e8a62 - prusti_driver::report_prusti_ice::h88b6f6623f051cc3
  11:     0x7fe09aff1603 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h4753e0b888cda8ee
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/alloc/src/boxed.rs:1708:9
  12:     0x7fe09aff24bd - proc_macro::bridge::client::<impl proc_macro::bridge::Bridge>::enter::{{closure}}::{{closure}}::hd9ac312375563fae
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/proc_macro/src/bridge/client.rs:320:21
  13:     0x7fe0ad016ba9 - std::panicking::rust_panic_with_hook::hf8e86850fbbd03b1
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/panicking.rs:610:17
  14:     0x7fe0ad016660 - std::panicking::begin_panic_handler::{{closure}}::h590a0d6060ff866e
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/panicking.rs:502:13
  15:     0x7fe0ad0135f4 - std::sys_common::backtrace::__rust_end_short_backtrace::h260b8bd1c848a03c
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/sys_common/backtrace.rs:139:18
  16:     0x7fe0ad0165c9 - rust_begin_unwind
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/panicking.rs:498:5
  17:     0x7fe0acfdb631 - core::panicking::panic_fmt::h7b8580d81fcbbacd
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/core/src/panicking.rs:106:14
  18:     0x7fe0acfdb5f2 - core::panicking::panic_bounds_check::h63650a5dfc9aa86f
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/core/src/panicking.rs:74:5
  19:     0x55afdc615058 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_local_variable_permission::h7615474a5e9bbaff
  20:     0x55afdc61530c - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_precondition_expr::h2b6357d9ba1c59ea
  21:     0x55afdc60e1be - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_impure_function_call::hb50c1ce45f48d397
  22:     0x55afdc601d0b - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_terminator::h66ae7148ae32cafe
  23:     0x55afdc5e8e3d - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_statement_at::h922eb9ae00d82657
  24:     0x55afdc5e24bc - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode_blocks_group::h8c39f498de6c3687
  25:     0x55afdc5de2c8 - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode::h43d9ebf4d455edcb
  26:     0x55afdc6e8d9e - prusti_viper::encoder::encoder::Encoder::encode_procedure::h230278c0cc4105b7
  27:     0x55afdc6ee89a - prusti_viper::encoder::encoder::Encoder::process_encoding_queue::hd05c955fe856e378
  28:     0x55afdc5145e8 - prusti_viper::verifier::Verifier::verify::h5586a74862d958a2
  29:     0x55afdc4d3afb - prusti_driver::verifier::verify::h0800d250aac8ff27
  30:     0x55afdc4e3289 - rustc_interface::passes::QueryContext::enter::hd7cbc6d71e4d3326
  31:     0x55afdc4d12a5 - <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis::h58206ba6bc402d77
  32:     0x7fe0af63b651 - <rustc_interface[f89f8228a4e35bc7]::interface::Compiler>::enter::<rustc_driver[e620c7401644acc4]::run_compiler::{closure#1}::{closure#2}, core[cc79c391059f8e46]::result::Result<core[cc79c391059f8e46]::option::Option<rustc_interface[f89f8228a4e35bc7]::queries::Linker>, rustc_errors[c8a333c965fedc03]::ErrorReported>>
  33:     0x7fe0af62c5cd - rustc_span[2d5555579096f1fe]::with_source_map::<core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>, rustc_interface[f89f8228a4e35bc7]::interface::create_compiler_and_run<core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>, rustc_driver[e620c7401644acc4]::run_compiler::{closure#1}>::{closure#1}>
  34:     0x7fe0af64cb7a - rustc_interface[f89f8228a4e35bc7]::interface::create_compiler_and_run::<core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>, rustc_driver[e620c7401644acc4]::run_compiler::{closure#1}>
  35:     0x7fe0af62ff7b - <scoped_tls[3fea4c3dcac147b1]::ScopedKey<rustc_span[2d5555579096f1fe]::SessionGlobals>>::set::<rustc_interface[f89f8228a4e35bc7]::util::setup_callbacks_and_run_in_thread_pool_with_globals<rustc_interface[f89f8228a4e35bc7]::interface::run_compiler<core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>, rustc_driver[e620c7401644acc4]::run_compiler::{closure#1}>::{closure#0}, core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>>::{closure#0}::{closure#0}, core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>>
  36:     0x7fe0af62f095 - std[a5529df289459975]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[f89f8228a4e35bc7]::util::setup_callbacks_and_run_in_thread_pool_with_globals<rustc_interface[f89f8228a4e35bc7]::interface::run_compiler<core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>, rustc_driver[e620c7401644acc4]::run_compiler::{closure#1}>::{closure#0}, core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>>::{closure#0}, core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>>
  37:     0x7fe0af62b162 - <<std[a5529df289459975]::thread::Builder>::spawn_unchecked<rustc_interface[f89f8228a4e35bc7]::util::setup_callbacks_and_run_in_thread_pool_with_globals<rustc_interface[f89f8228a4e35bc7]::interface::run_compiler<core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>, rustc_driver[e620c7401644acc4]::run_compiler::{closure#1}>::{closure#0}, core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>>::{closure#0}, core[cc79c391059f8e46]::result::Result<(), rustc_errors[c8a333c965fedc03]::ErrorReported>>::{closure#1} as core[cc79c391059f8e46]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  38:     0x7fe0ad021e93 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h771719d52c343434
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/alloc/src/boxed.rs:1694:9
  39:     0x7fe0ad021e93 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hf441746dfa4b0f57
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/alloc/src/boxed.rs:1694:9
  40:     0x7fe0ad021e93 - std::sys::unix::thread::Thread::new::thread_start::hfd168f9d312b29ca
                               at /rustc/ad442399756573dccacb314b6bf8079964bcc72a/library/std/src/sys/unix/thread.rs:106:17
  41:     0x7fe0ab8c0d80 - start_thread
                               at ./nptl/./nptl/pthread_create.c:481:8
  42:     0x7fe0ab694b6f - __clone
                               at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone.S:95
  43:                0x0 - <unknown>

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 4dfd34d 2021-11-22 16:35:31 UTC, built on 2021-11-22 16:40:49 UTC

query stack during panic:
end of query stack

jeremysalwen avatar Jan 21 '22 08:01 jeremysalwen

Would it be possible for you to share the code that causes the crash?

vakaras avatar Jan 21 '22 09:01 vakaras

Yes, it is available here: https://github.com/jeremysalwen/adventofcode2021

jeremysalwen avatar Jan 21 '22 20:01 jeremysalwen

Interestingly, when I open the project in Prusti assistant it does not crash. (It does show many internal errors, but that is expected because the examples use many unsupported features.)

vakaras avatar Jan 24 '22 14:01 vakaras