prusti-dev icon indicating copy to clipboard operation
prusti-dev copied to clipboard

`cargo prusti -vv` fails verification in crate dependencies

Open Patrick-6 opened this issue 2 years ago • 0 comments

Running cargo prusti -vv (very verbose output) will lead to many [Prusti: unsupported feature] errors in dependencies of the current crate, and failing verification of the crate. One example is a crate with just an empty main function, and a dependency on syn in Cargo.toml:

[dependencies]
syn = "2.0.14"

This is the output (removed rustc commands in [...]):

$ cargo prusti -vv
Compiling proc-macro2 v1.0.56
Checking unicode-ident v1.0.8
Compiling quote v1.0.26
Running [...]
Running `CARGO=/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/bin/cargo 
  CARGO_CRATE_NAME=unicode_ident 
  CARGO_MANIFEST_DIR=/.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.8 
  CARGO_PKG_AUTHORS='David Tolnay <[email protected]>' 
  CARGO_PKG_DESCRIPTION='Determine whether characters have the XID_Start or XID_Continue properties according to Unicode Standard Annex #31' 
  CARGO_PKG_HOMEPAGE='' CARGO_PKG_LICENSE='(MIT OR Apache-2.0) AND Unicode-DFS-2016' 
  CARGO_PKG_LICENSE_FILE='' CARGO_PKG_NAME=unicode-ident 
  CARGO_PKG_REPOSITORY='https://github.com/dtolnay/unicode-ident' 
  CARGO_PKG_RUST_VERSION=1.31 CARGO_PKG_VERSION=1.0.8 CARGO_PKG_VERSION_MAJOR=1 
  CARGO_PKG_VERSION_MINOR=0 CARGO_PKG_VERSION_PATCH=8 CARGO_PKG_VERSION_PRE='' 
  LD_LIBRARY_PATH='prusti-vv-bug/target/verify/debug/deps:.rustup/toolchains/nightly-2023-03-08-x86_64-unknown-linux-gnu/lib:/.rustup/toolchains/nightly-2023-03-08-x86_64-unknown-linux-gnu/lib:/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib' 
  prusti-rustc --crate-name unicode_ident 
  --edition=2018 /.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.8/src/lib.rs 
  --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat 
  --diagnostic-width=237 --crate-type lib --emit=dep-info,metadata 
  -C embed-bitcode=no -C debuginfo=2 -C metadata=4568e78affd58b00 
  -C extra-filename=-4568e78affd58b00 --out-dir prusti-vv-bug/target/verify/debug/deps 
  -L dependency=prusti-vv-bug/target/verify/debug/deps 
  --cap-lints warn`
Running [...]

error: [Prusti: unsupported feature] unsupported constant type Ref('_#6r, tables::Align64<[bool; 128]>, Not)
   --> /.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.8/src/lib.rs:255:16
    |
255 |         return ASCII_START.0[ch as usize];
    |                ^^^^^^^^^^^
error: [Prusti: unsupported feature] unsupported constant type Ref('_#6r, tables::Align64<[bool; 128]>, Not)
   --> /.cargo/registry/src/github.com-1ecc6299db9ec823/unicode-ident-1.0.8/src/lib.rs:264:16
    |
264 |         return ASCII_CONTINUE.0[ch as usize];
    |                ^^^^^^^^^^^^^^
error: could not compile `unicode-ident` due to 2 previous errors

Caused by:
  process didn't exit successfully: [...]
(exit status: 1)
warning: build failed, waiting for other jobs to finish...

Running cargo prusti without the -vv flag will verify this test crate correctly.

Other dependencies such as prusti-contracts also cause errors with the -vv flag.

The flag be_rustc should be set when compiling the dependencies, which should prevent these errors.

Patrick-6 avatar Apr 11 '23 15:04 Patrick-6