cargo-kani fails with undefined symbol when using nightly toolchain as default

[harrisonkaiser]

I tried this command:

$ cargo kani
error: process didn't exit successfully: `/home/ubuntu/.kani/kani-0.10.0/bin/kani-compiler -vV` (exit status: 127)
--- stderr
/home/ubuntu/.kani/kani-0.10.0/bin/kani-compiler: symbol lookup error: /home/ubuntu/.kani/kani-0.10.0/bin/../toolchain/lib/librustc_driver-e70f935d0865b673.so: undefined symbol: _ZN9hashbrown3raw11Fallibility17capacity_overflow17h52b24f50adb3934dE

Error: cargo exited with status exit status: 101

with Kani version: 0.10.0

I expected to see a check happen.

Instead, this happened.

Looks like cargo sets LD_LIBRARY_PATH=/home/ubuntu/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib which causes kani to link against the wrong library with a differently mangled symbol name.

Worked through with @tedinski. Who says:

I think normally something (rustup or cargo) doesn't set LD_LIBRARY_PATH. But sometimes (apparently) it does, and I think it's changing the search order and gets a slightly wrong dynamic library (e.g. the one from nightly instead of the specific nightly we're built against)

And about this PR:

I'll be filling in my notes

[tedinski]

Thank you again for sitting down and debugging this with me!

Workaround: rustup default stable and things should now work.

The appears (I haven't finished debugging) to be a result of nightly wanting to dynamic link to rustc_driver so it (rustup, I'm pretty sure) sets LD_LIBRARY_PATH when it runs cargo. Which then invokes cargo-kani with that environment variable set, and that ends up getting libstd.so (or rustc_driver? or both) getting linked from nightly-nightly, instead of Kani's pinned nightly version. Thus, the undefined symbol errors.

Just running cargo-kani (with dash) might also be a workaround.

We'll need to fix our cargo-kani or kani-driver binaries to examine LD_LIBRARY_PATH and fix it up when there's something scary in it like this.