Invalid path reported for Rust toolchain

[celinval]

I got this error:

Errors
File [/Users/ec2-user/.rustup/toolchains/nightly-2023-08-04-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/unix/thread_local_dtor.rs]
Function [std::sys::unix::thread_local_dtor::register_dtor]
Line [69]
[[trace] call to foreign "C" function `_tlv_atexit` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423

But I don't understand why it says "/Users/ec2-user/". I don't have this user on my machine! :)

Originally posted by @ithinkicancode in https://github.com/model-checking/kani/issues/2423#issuecomment-1676484187

[jaisnan]

Replicating this issue in a ubuntu environment, gave this response -

../../../github/home/.rustup/toolchains/nightly-2023-09-19-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/builders.rs:33:16 in function <core::fmt::builders::PadAdapter<'_, '_> as std::fmt::Write>::write_str

What this tells me is that, the path to the toolchain is being hardcoded from where the binary is being built. In this case, in the github action runner.

[celinval]

I believe this is related to this PR: https://github.com/model-checking/kani/pull/976. More specifically, this change: https://github.com/model-checking/kani/pull/976/files#diff-ad7f3edc0c2f338653896927f634fc2b24a45720db4249bda577be21bb9fabb5

See this comment in the PR:

2. Fix the file path in the compiler to use local file path.
   • Note that using the local file path is not recommended to generate artifacts that can be shared, but I don't this we have that use case today.

One side effect of reverting this change, is that Kani will always display invalid path for toolchain files. This could impact the VSCode extension (if it uses the paths printed by Kani) and it will impact the visualize trace which probably won't display the contents of standard library functions.

If we do want to make sure the path points to the local version of the rust toolchain, we will likely need to build all our libraries locally as part of the setup process.

[celinval]

@jaisnan, I wonder if we could use -Z remap-cwd-prefix tracked here while building our libraries.

[fedejinich]

I think I'm having the same issue here. I'm trying to run a basic harness that imports a struct with a lot of dependencies. I run it with cargo kani --harness decoders_proof and I get the following error:

Check 607: std::thread::LocalKey::<std::cell::Cell<(u64, u64)>>::try_with::<{closure@std::hash::RandomState::new::{closure#0}}, std::hash::RandomState>.pointer_dereference.8
         - Status: UNDETERMINED
         - Description: "dereference failure: dead object"
         - Location: ../../../../jaisnan/.rustup/toolchains/nightly-2024-07-01-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/thread/local.rs:282:37 in function std::thread::LocalKey::<std::cell::Cell<(u64, u64)>>::try_with::<{closure@std::hash::RandomState::new::{closure#0}}, std::hash::RandomState>

SUMMARY:
 ** 1 of 607 failed (606 undetermined)
Failed Checks: call to foreign "C" function `getentropy` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423
 File: "/Users/jaisnan/.rustup/toolchains/nightly-2024-07-01-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/pal/unix/rand.rs", line 192, in std::sys::pal::unix::rand::imp::getentropy_fill_bytes

VERIFICATION:- FAILED
** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details.
Verification Time: 0.38896373s

Summary:
Verification failed for - decoders_proof::decode_r_type_proof
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

I'm wondering how can I debug my code to see the conflicting steps. I've already used export RUSTFLAGS="-Zremap-cwd-prefix=/Users/myuser" or export RUSTFLAGS="-Zremap-cwd-prefix=." without any success:(

Any clues?

[jaisnan]

I think I'm having the same issue here. I'm trying to run a basic harness that imports a struct with a lot of dependencies. I run it with cargo kani --harness decoders_proof and I get the following error:

Check 607: std::thread::LocalKey::<std::cell::Cell<(u64, u64)>>::try_with::<{closure@std::hash::RandomState::new::{closure#0}}, std::hash::RandomState>.pointer_dereference.8
         - Status: UNDETERMINED
         - Description: "dereference failure: dead object"
         - Location: ../../../../jaisnan/.rustup/toolchains/nightly-2024-07-01-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/thread/local.rs:282:37 in function std::thread::LocalKey::<std::cell::Cell<(u64, u64)>>::try_with::<{closure@std::hash::RandomState::new::{closure#0}}, std::hash::RandomState>

SUMMARY:
 ** 1 of 607 failed (606 undetermined)
Failed Checks: call to foreign "C" function `getentropy` is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/2423
 File: "/Users/jaisnan/.rustup/toolchains/nightly-2024-07-01-aarch64-apple-darwin/lib/rustlib/src/rust/library/std/src/sys/pal/unix/rand.rs", line 192, in std::sys::pal::unix::rand::imp::getentropy_fill_bytes

VERIFICATION:- FAILED
** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details.
Verification Time: 0.38896373s

Summary:
Verification failed for - decoders_proof::decode_r_type_proof
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

I'm wondering how can I debug my code to see the conflicting steps. I've already used export RUSTFLAGS="-Zremap-cwd-prefix=/Users/myuser" or export RUSTFLAGS="-Zremap-cwd-prefix=." without any success:(

Any clues?

Hi @fedejinich ! What version of Kani are you running, and do you have a harness that would allow us to reproduce your error?

[celinval]

Hi @fedejinich, if I remember correctly, the remap option has to be done on the release bundle side. For now, you should be able to find the files by manually replacing the /Users/jaisnan/ by /Users/my user/.