Kani not resolving qualified paths in verify-std #4084
Description
I was attempting to write harnesses for trait method implementations in verify-rust-std, but I could not get Kani to resolve the qualified path of the function.
I tried this code (in library/core/src/slice/index.rs):
#[cfg(kani)]
mod verify {
use super::*;
use crate::kani;
#[kani::proof_for_contract(<usize as SliceIndex<[T]>>::get_unchecked)]
pub fn check_get_unchecked() {}
}with this contract inside unsafe impl<T> SliceIndex<[T]> for usize:
#[inline]
#[safety::requires(self < slice.len())]
unsafe fn get_unchecked(self, slice: *const [T]) -> *const T {
// ...using the following command line invocation:
./scripts/run-kani.sh --path . --kani-args --harness core::slice::verify::check_get_unchecked
with Kani version: 0.61.0
I expected to see this happen: function name would be resolved.
Instead, this happened:
error: Failed to resolve checking function <usize as SliceIndex<[T]>>::get_unchecked because Kani currently cannot resolve qualified paths
--> /Users/dawidl022/Development/verify-rust-std/library/core/src/slice/index.rs:1071:5
|
1071 | #[kani::proof_for_contract(<usize as SliceIndex<[T]>>::get_unchecked)]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)
error: Failed to resolve `<usize as SliceIndex<[T]>>::get_unchecked` for `proof_for_contract`: Kani currently cannot resolve qualified paths
--> /Users/dawidl022/Development/verify-rust-std/library/core/src/slice/index.rs:1072:5
|
1072 | pub fn check_get_unchecked() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
error: Failed to execute cargo (exit status: 101). Found 2 compilation errors.
Since #3457 added support for qualified paths, I'm unsure if the problem is my usage, or if this is a bug.
I thought it might be because of the generic parameter in the trait, but I couldn't get path resolution to work for a non-generic trait either:
error: Failed to resolve checking function <usize as BitOr>::bitor because Kani currently cannot resolve qualified paths
--> /Users/dawidl022/Development/verify-rust-std/library/core/src/ops/bit.rs:1039:5
|
1039 | #[kani::proof_for_contract(<usize as BitOr>::bitor)]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: this error originates in the attribute macro `kani::proof_for_contract` (in Nightly builds, run with -Z macro-backtrace for more info)