search

viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.58k stars 108 forks source link

'index out of bounds' panic in mir_encoder #830

Open jeremysalwen opened 2 years ago

jeremysalwen commented 2 years ago

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
vakaras commented 2 years ago

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

jeremysalwen commented 2 years ago

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

vakaras commented 2 years ago

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.)