Closed nshyrei closed 4 months ago
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.
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 half@2.3.1 --precise ver
where `ver` is the latest version of `half` supporting rustc 1.68.0-nightly
@fpoli Seems like this https://github.com/viperproject/prusti-dev/pull/1470 is a relevant PR that will potentially fix the issue but it is stuck.
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.
@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.
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.
@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.
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()) {
@fpoli What I am asking is will https://github.com/viperproject/prusti-dev/blob/c1a5b128d938333a821af0a554be4562905bb82a/prusti/src/driver.rs#L93 verify or it will simply compile the project with rustc
?
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.
@fpoli Created a PR https://github.com/viperproject/prusti-dev/pull/1496
@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
This was missing: https://github.com/viperproject/prusti-dev/pull/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.
@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.
I have a 3rd party dependency crate
vulkano
that I use (https://crates.io/crates/vulkano). Building the project withcargo-prusti
crashes with the following compiler panic:Now I am happy to not verify this crate altogether, but none of the flags like
[NO_VERIFY_DEPS]
(https://viperproject.github.io/prusti-dev/dev-guide/config/flags.html#no_verify_deps) or[NO_VERIFY]
(https://viperproject.github.io/prusti-dev/dev-guide/config/flags.html#no_verify) seem to work in any form including env vars orPrusti.toml
file.