Prusti attempts to verify local dependencies

[emlaufer]

I am attempting to use Prusti to verify a crate that has other local crates as dependencies. Currently when I run the verifier, it is attempting to also validate the dependencies as they compile. Is it possible to treat the local crates like external libraries, such that they are not validated, and I can write external specifications for them instead.

[fpoli]

cargo-prusti is designed to behave like cargo check and in particular it should accept the same arguments. If I'm not mistaken by default cargo check checks all the local dependencies and you can select a specific package with cargo check -p <package_name>. So, could you try if cargo-prusti -p <package_name> does what you want?

[emlaufer]

Unfortunately the -p argument doesn't seem to fix this. -p allows me to only check the dependency without the main package, however when specifying the main package it still ends up checking the dependency. It looks like there has been some discussion on the main cargo page about silencing warnings in path dependencies here, but I don't think it has been fixed yet. In any case, an easy work around is to just push the dependency to git and use the git repository to specify the dependency instead.

[fpoli]

For the record, clippy builds on top of cargo check and had the same issue (rust-lang/rust-clippy#3025). They ended up adding a --no-deps command line argument (rust-lang/rust-clippy#6188). We could do something similar.

All our "skip verification of crate" logic is in these 11 lines:

prusti-dev/prusti/src/driver.rs

Lines 131 to 141 in 05f1f9e

	// If the environment asks us to actually be rustc, or if lints have been disabled (which
	// indicates that an upstream dependency is being compiled), then run `rustc` instead of Prusti.
	let prusti_be_rustc = config::be_rustc();
	let are_lints_disabled =
	arg_value(&original_rustc_args, "--cap-lints", |val| val == "allow").is_some();
	let is_prusti_package = env::var("CARGO_PKG_NAME")
	.map(|name| PRUSTI_PACKAGES.contains(&name.as_str()))
	.unwrap_or(false);
	if prusti_be_rustc || are_lints_disabled || is_prusti_package {
	rustc_driver::main();
	}

[Pointerbender]

@fpoli I have been playing with the rustc arguments over the weekend and got a little more familiar with it :) This enhancement seems like something I could add. What would be the best way to add this to Prusti? As a --no-deps CLI argument to Prusti or as a new NO_VERIFY_DEPS configuration flag?

[Pointerbender]

Created PR #774 just now with a proposal for how a solution for this enhancement could look like.

[fpoli]

A configuration flag sounds good to me. They can be enabled in many ways (with an environment variable, with the Prusti.toml and even with a -P<flag> special argument to rustc).

[Pointerbender]

@emlaufer please try if it works for you by either adding this line to your Prusti.toml:

no_verify_deps = true

or by setting an environment variable when running cargo-prusti on the command line:

PRUSTI_NO_VERIFY_DEPS=true cargo-prusti

(this new configuration flag was just merged to the master branch today)