Comments (14)
Thank you for the report. From a quick look, my stacktrace suggests that the panic happens while Prusti is running <ModelUsageVisitor as NonSpecExprVisitor>::visit_expr
(code below). Using the Prusti release v-2023-01-26-1935
I do not get this error, so I suspect that this is a bug of rustc
. We should update Prusti to use the latest version of rustc
to see if the bug has been fixed in the meantime.
prusti-dev/prusti-interface/src/specs/checker/type_model_checks.rs
Lines 80 to 93 in e632f70
My stacktrace:
thread 'rustc' panicked at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/compiler/rustc_errors/src/lib.rs:995:33:
Box<dyn Any>
stack backtrace:
0: 0x7f0f67562efc - std::backtrace_rs::backtrace::libunwind::trace::h652247f520429b18
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
1: 0x7f0f67562efc - std::backtrace_rs::backtrace::trace_unsynchronized::h20ba733a518048ae
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
2: 0x7f0f67562efc - std::sys_common::backtrace::_print_fmt::ha9cb2d71bba5eb16
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:67:5
3: 0x7f0f67562efc - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h527f3c0db321cf86
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:44:22
4: 0x7f0f675c915c - core::fmt::rt::Argument::fmt::hc5a8cd063e05c609
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/core/src/fmt/rt.rs:138:9
5: 0x7f0f675c915c - core::fmt::write::h818c732e4e373aa5
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/core/src/fmt/mod.rs:1094:21
6: 0x7f0f6755593e - std::io::Write::write_fmt::h07440f3e98279257
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/io/mod.rs:1714:15
7: 0x7f0f67562ce4 - std::sys_common::backtrace::_print::h4b50c3b478ae2a37
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:47:5
8: 0x7f0f67562ce4 - std::sys_common::backtrace::print::hf2c7643f5414af94
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:34:9
9: 0x7f0f67565dda - std::panicking::panic_hook_with_disk_dump::{{closure}}::h62ff4ef3ec32306d
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/panicking.rs:280:22
10: 0x7f0f67565ad5 - std::panicking::panic_hook_with_disk_dump::hcd58ca7cb67f8702
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/panicking.rs:314:9
11: 0x7f0f6a7690b9 - <rustc_driver_impl[8b2874cda94e7cd4]::install_ice_hook::{closure#0} as core[b0493a3e457862f3]::ops::function::FnOnce<(&core[b0493a3e457862f3]::panic::panic_info::PanicInfo,)>>::call_once::{shim:vtable#0}
12: 0x7f0f67566693 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h2b79b1e8b8bd4402
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/alloc/src/boxed.rs:2021:9
13: 0x7f0f67566693 - std::panicking::rust_panic_with_hook::ha2c93276d1208654
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/panicking.rs:757:13
14: 0x7f0f6a9eab54 - std[843b1ee06368cddb]::panicking::begin_panic::<rustc_errors[e553a123e183cff8]::ExplicitBug>::{closure#0}
15: 0x7f0f6a9e82b6 - std[843b1ee06368cddb]::sys_common::backtrace::__rust_end_short_backtrace::<std[843b1ee06368cddb]::panicking::begin_panic<rustc_errors[e553a123e183cff8]::ExplicitBug>::{closure#0}, !>
16: 0x7f0f6aa0ec16 - std[843b1ee06368cddb]::panicking::begin_panic::<rustc_errors[e553a123e183cff8]::ExplicitBug>
17: 0x7f0f6aa0e2ee - <rustc_errors[e553a123e183cff8]::HandlerInner>::span_bug::<rustc_span[82af0e0afe7e8690]::span_encoding::Span, alloc[606cb6f3851bb62a]::string::String>
18: 0x7f0f6aa0e10b - <rustc_errors[e553a123e183cff8]::Handler>::span_bug::<rustc_span[82af0e0afe7e8690]::span_encoding::Span, alloc[606cb6f3851bb62a]::string::String>
19: 0x7f0f6a9ceb4d - rustc_middle[ad90ed66b4303932]::util::bug::opt_span_bug_fmt::<rustc_span[82af0e0afe7e8690]::span_encoding::Span>::{closure#0}
20: 0x7f0f6a9ceb7a - rustc_middle[ad90ed66b4303932]::ty::context::tls::with_opt::<rustc_middle[ad90ed66b4303932]::util::bug::opt_span_bug_fmt<rustc_span[82af0e0afe7e8690]::span_encoding::Span>::{closure#0}, !>::{closure#0}
21: 0x7f0f6a9ce138 - rustc_middle[ad90ed66b4303932]::ty::context::tls::with_context_opt::<rustc_middle[ad90ed66b4303932]::ty::context::tls::with_opt<rustc_middle[ad90ed66b4303932]::util::bug::opt_span_bug_fmt<rustc_span[82af0e0afe7e8690]::span_encoding::Span>::{closure#0}, !>::{closure#0}, !>
22: 0x7f0f699cad94 - rustc_middle[ad90ed66b4303932]::util::bug::span_bug_fmt::<rustc_span[82af0e0afe7e8690]::span_encoding::Span>
23: 0x7f0f697f3db0 - rustc_hir_typeck[1d417f91be3ec530]::typeck
24: 0x7f0f6884954e - rustc_query_impl[e537a3258c4e1a56]::plumbing::__rust_begin_short_backtrace::<rustc_query_impl[e537a3258c4e1a56]::query_impl::typeck::dynamic_query::{closure#2}::{closure#0}, rustc_middle[ad90ed66b4303932]::query::erase::Erased<[u8; 8usize]>>
25: 0x7f0f6884951e - <rustc_query_impl[e537a3258c4e1a56]::query_impl::typeck::dynamic_query::{closure#2} as core[b0493a3e457862f3]::ops::function::FnOnce<(rustc_middle[ad90ed66b4303932]::ty::context::TyCtxt, rustc_span[82af0e0afe7e8690]::def_id::LocalDefId)>>::call_once
26: 0x7f0f68920e58 - rustc_query_system[404b1af824500f21]::query::plumbing::try_execute_query::<rustc_query_impl[e537a3258c4e1a56]::DynamicConfig<rustc_query_system[404b1af824500f21]::query::caches::VecCache<rustc_span[82af0e0afe7e8690]::def_id::LocalDefId, rustc_middle[ad90ed66b4303932]::query::erase::Erased<[u8; 8usize]>>, false, false, false>, rustc_query_impl[e537a3258c4e1a56]::plumbing::QueryCtxt, false>
27: 0x7f0f6a0e46f1 - rustc_query_impl[e537a3258c4e1a56]::query_impl::typeck::get_query_non_incr::__rust_end_short_backtrace
28: 0x55fd10f90533 - <prusti_interface::specs::checker::type_model_checks::ModelUsageVisitor as prusti_interface::specs::checker::common::NonSpecExprVisitor>::visit_expr::h037892247f929c0f
29: 0x55fd10f5c7a9 - rustc_hir::intravisit::walk_expr::he69b9c275b775907
30: 0x55fd10f50a52 - rustc_hir::intravisit::walk_generic_args::h19816db272b4a4cf
31: 0x55fd10f5638c - rustc_hir::intravisit::walk_ty::h8e5a9f5fce680e64
32: 0x55fd10f509cc - rustc_hir::intravisit::walk_generic_args::h19816db272b4a4cf
33: 0x55fd10f5638c - rustc_hir::intravisit::walk_ty::h8e5a9f5fce680e64
34: 0x55fd10f6185c - rustc_hir::intravisit::walk_item::hf728d6eec02be310
35: 0x55fd10f60e06 - rustc_hir::intravisit::walk_item::hf728d6eec02be310
36: 0x55fd10fbfed4 - <prusti_interface::specs::checker::type_model_checks::IllegalModelUsagesChecker as prusti_interface::specs::checker::common::SpecCheckerStrategy>::check::heaf4b4f8771d37e0
37: 0x55fd10fc1946 - prusti_interface::specs::checker::SpecChecker::check::h9125bbb6de956f50
38: 0x55fd1065e15d - <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis::h7d8f5df69404394f
39: 0x7f0f69c789d6 - <rustc_interface[1527d435bc9889c9]::interface::Compiler>::enter::<rustc_driver_impl[8b2874cda94e7cd4]::run_compiler::{closure#1}::{closure#2}, core[b0493a3e457862f3]::result::Result<core[b0493a3e457862f3]::option::Option<rustc_interface[1527d435bc9889c9]::queries::Linker>, rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>
40: 0x7f0f69c71c04 - std[843b1ee06368cddb]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[1527d435bc9889c9]::util::run_in_thread_with_globals<rustc_interface[1527d435bc9889c9]::interface::run_compiler<core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>, rustc_driver_impl[8b2874cda94e7cd4]::run_compiler::{closure#1}>::{closure#0}, core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>
41: 0x7f0f69c7135e - <<std[843b1ee06368cddb]::thread::Builder>::spawn_unchecked_<rustc_interface[1527d435bc9889c9]::util::run_in_thread_with_globals<rustc_interface[1527d435bc9889c9]::interface::run_compiler<core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>, rustc_driver_impl[8b2874cda94e7cd4]::run_compiler::{closure#1}>::{closure#0}, core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[b0493a3e457862f3]::result::Result<(), rustc_span[82af0e0afe7e8690]::ErrorGuaranteed>>::{closure#1} as core[b0493a3e457862f3]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
42: 0x7f0f67571075 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h7bff668e3fcc7cec
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/alloc/src/boxed.rs:2007:9
43: 0x7f0f67571075 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h6cf1c11e2e0c58d1
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/alloc/src/boxed.rs:2007:9
44: 0x7f0f67571075 - std::sys::unix::thread::Thread::new::thread_start::hfa7d5fcc9039f5da
at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys/unix/thread.rs:108:17
45: 0x7f0f65c94ac3 - start_thread
at ./nptl/pthread_create.c:442:8
46: 0x7f0f65d26850 - __GI___clone3
at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81
47: 0x0 - <unknown>
from prusti-dev.
For the record, Prusti v-2023-01-26-1935
fails with this other error complaining about Prusti using a version of rustc
that is too old:
error: package `half v2.3.1` cannot be built because it requires rustc 1.70 or newer, while the currently active rustc version is 1.68.0-nightly
Either upgrade to rustc 1.70 or newer, or use
cargo update -p [email protected] --precise ver
where `ver` is the latest version of `half` supporting rustc 1.68.0-nightly
from prusti-dev.
@fpoli Seems like this #1470 is a relevant PR that will potentially fix the issue but it is stuck.
from prusti-dev.
Indeed :) We had to balance our efforts between updating the current master
and finishing a large refactoring. The latter is going to bring many advantages -- e.g., making rustc
updates easier -- and is almost ready, so I think it's best to keep prioritizing that.
from prusti-dev.
@fpoli Do you know why the flags [NO_VERIFY_DEPS]
or [NO_VERIFY]
might not work for me? As I said it's not important for me to check this 3rd party crate as I am only interested in my portion of the project. I use Prusti.toml
to specify a flag and I know for sure that it is being used, because if I duplicate the keys in the file Prusti will fail before starting the check.
from prusti-dev.
That's because we want Prusti to collect the contracts that are declared in the dependencies, even when those contracts are not verified with respect to their implementation.
To do what you are proposing we would need one new flag to skip collecting the specifications from the dependencies, e.g., something called ignore_deps_contracts
. When that's enabled, the important thing is to make Prusti enter this branch, so that rustc
runs (almost) as in a normal compilation. If anywant (@pixelshot91?) wants to give a try before us, I think that this should be a relatively easy contribution. The configuration flags are defined here and documented here.
from prusti-dev.
@fpoli Correct me If I am wrong, but I believe that entering this branch will skip verification all together for the whole project, because I have tried https://github.com/viperproject/prusti-dev/blob/c1a5b128d938333a821af0a554be4562905bb82a/docs/dev-guide/src/config/flags.md#be_rustc before and I only saw regular rustc
output.
from prusti-dev.
Sorry, it's because I didn't state the complete condition. We already have a way of detecting whether Prusti is currently compiling the main crate or a dependency, it's is_primary_package
. So, the full condition for entering the "act as rustc" branch should become something like the following
if config::be_rustc() || build_script_build || (!is_primary_package && config::ignore_deps_contracts()) {
from prusti-dev.
@fpoli What I am asking is will
prusti-dev/prusti/src/driver.rs
Line 93 in c1a5b12
rustc
?from prusti-dev.
driver::main()
compiles a single crate as rustc
would do, but that does not affect how other crates (e.g., the dependencies) are compiled. More in detail, cargo-prusti
launches cargo
, which ends up launching multiple times prusti-driver
: one for each crate to be compiled (i.e., the root one, and the dependencies). The driver::main()
call is in prusti-driver
, and in your case you want to execute it when running on the dependencies (ignoring all the contracts in them) but not when running on the main crate, because it should be verified.
from prusti-dev.
from prusti-dev.
@fpoli Unfortunately I don't see my issue fixed. I have picked latest nightly https://github.com/viperproject/prusti-dev/releases/tag/v-2024-02-26-1521 and I for sure know that the flag is used, because if I corrupt the flag name a bit in Prusti.toml
the verifier will panic with:
thread 'main' panicked at prusti-utils\src\config.rs:241:9:
Found an unknown configuration flag `ignore_deps_contsdracts` in the file `.\Prusti.toml`
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
from prusti-dev.
This was missing: #1498
Whitout that fix, with version v-2024-02-26-1521
, you can declare a PRUSTI_IGNORE_DEPS_CONTRACTS=true
environment variable — e.g., in the prusti-assistant.extraPrustiEnv
setting of Prusti-Assistant — and it works.
from prusti-dev.
@fpoli Ok, with PRUSTI_IGNORE_DEPS_CONTRACTS
I am getting a bunch of prusti-related compile messages now, but no rustc
crashes so I assume it indeed works. I am closing this as resolved, thank you very much.
from prusti-dev.
Related Issues (20)
- Help message for x.py
- Internal error when assigning to an argument
- Internal error when assigning a closure call to a reference
- rustc removed plugins HOT 2
- Update rust nightly to support codegen-backend HOT 1
- Failing procedural macro of a contract
- Unexpected order of verification errors
- Executable mode bits in release files not set HOT 4
- Support for old(..) expressions in loop invariants
- Wrong encoding of signed discriminants in pure code HOT 1
- Unsupported constant string in println HOT 1
- Wrong encoding of signed divisions HOT 2
- Inconsistency in the encoding of Rust addresses as Viper Ref types
- ghost seq not implemented HOT 1
- Error for missing model lifetime specifier recommends invalid syntax, has unclear fix HOT 3
- Enum discriminant completeness
- Enum: unsupported statement kind `Intrinsic(Assume(move _))`
- External specification declared on a trait implementation did not resolve to a concrete type
- `len()` implementation without overflow errors
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from prusti-dev.