Failed to find Kani functions on superslice-rs

[zhassan-aws]

Steps to reproduce:

1. git clone https://github.com/alkis/superslice-rs
2. cd superslice-rs
3. cargo kani

with Kani version: f64f53e

I expected to see this happen: No proof harnesses found

Instead, this happened: Kani crashed:

$ cargo kani
Kani Rust Verifier 0.59.0 (cargo plugin)
warning: no edition set: defaulting to the 2015 edition while the latest is 2024
    Updating crates.io index
   Compiling superslice v1.0.0 (/home/ubuntu/git/superslice-rs)
warning: target feature `x87` must be enabled to ensure that the ABI of the current target can be implemented correctly
  |
  = note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>

warning: target feature `sse2` must be enabled to ensure that the ABI of the current target can be implemented correctly
  |
  = note: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
  = note: for more information, see issue #116344 <https://github.com/rust-lang/rust/issues/116344>

ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Intrinsic(AnyModifies)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Intrinsic(CheckedAlignOf)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Intrinsic(CheckedSizeOf)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Intrinsic(AutomaticHarness)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Intrinsic(IsInitialized)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Intrinsic(ValidValue)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Intrinsic(WriteAny)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(AlignOfDynObject)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(AlignOfVal)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(Any)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(CopyInitState)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(CopyInitStateSingle)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(LoadArgument)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(InitializeMemoryInitializationState)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(IsPtrInitialized)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(IsStrPtrInitialized)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(IsSliceChunkPtrInitialized)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(IsSlicePtrInitialized)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(Offset)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(PtrOffsetFrom)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(PtrSubPtr)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(RunContract)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(RunLoopContract)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(SetPtrInitialized)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(SetSliceChunkPtrInitialized)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(SetSlicePtrInitialized)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(SetStrPtrInitialized)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(SizeOfDynObject)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(SizeOfSliceObject)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(SizeOfVal)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(StoreArgument)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(WriteAnySlice)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(WriteAnySlim)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Model(WriteAnyStr)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(AnyRaw)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(Assert)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(Assume)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(Check)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(Cover)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(FloatToIntInRange)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(InitContracts)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(IsAllocated)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(Panic)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(PointerObject)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(PointerOffset)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(SafetyCheck)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(SafetyCheckNoAssume)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(UnsupportedCheck)
ERROR kani_compiler::kani_middle::kani_functions Missing kani function, func=Hook(UntrackedDeref)

thread 'rustc' panicked at kani-compiler/src/kani_middle/kani_functions.rs:268:5:
assertion `left == right` failed: Failed to find `49` Kani functions
  left: 49
 right: 0
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] no current codegen item.
error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/kani_middle/kani_functions.rs:268:5:
                                assertion `left == right` failed: Failed to find `49` Kani functions
                                  left: 49
                                 right: 0.

[Kani] no current codegen location.
error: could not compile `superslice` (lib); 2 warnings emitted

Caused by:
  process didn't exit successfully: `/home/ubuntu/git/kani/target/kani/bin/kani-compiler --crate-name superslice --edition=2015 src/lib.rs --error-format=json --json=diagnostic-rendered-ansi,artifacts,future-incompat --diagnostic-width=111 --crate-type lib --emit=dep-info,metadata,link -C embed-bitcode=no -C debuginfo=2 --check-cfg 'cfg(docsrs,test)' --check-cfg 'cfg(feature, values())' -C metadata=61e7523d0cf1767e -C extra-filename=-1feb29a81d390cae --out-dir /home/ubuntu/git/superslice-rs/target/kani/x86_64-unknown-linux-gnu/debug/deps --target x86_64-unknown-linux-gnu -C incremental=/home/ubuntu/git/superslice-rs/target/kani/x86_64-unknown-linux-gnu/debug/incremental -L dependency=/home/ubuntu/git/superslice-rs/target/kani/x86_64-unknown-linux-gnu/debug/deps -L dependency=/home/ubuntu/git/superslice-rs/target/kani/debug/deps -Cllvm-args=--reachability=harnesses -C overflow-checks=on -Z unstable-options -Z trim-diagnostic-paths=no -Z human_readable_cgu_names -Z always-encode-mir --cfg=kani -Z 'crate-attr=feature(register_tool)' -Z 'crate-attr=register_tool(kanitool)' --sysroot /home/ubuntu/git/kani/target/kani -L /home/ubuntu/git/kani/target/kani/lib --extern kani --extern 'noprelude:std=/home/ubuntu/git/kani/target/kani/lib/libstd.rlib' -C panic=abort -C symbol-mangling-version=v0 -Z panic_abort_tests=yes -Z mir-enable-passes=-RemoveStorageMarkers '--check-cfg=cfg(kani)' -Clinker=echo --kani-compiler '-Cllvm-args=--check-version=0.59.0 --log-level=warn --assertion-reach-checks'` (exit status: 101)
error: Failed to compile `superslice` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/kani_middle/kani_functions.rs:268:5:
                                assertion `left == right` failed: Failed to find `49` Kani functions
                                  left: 49
                                 right: 0.

[carolynzech]

I've seen this issue before--I bet it's because of this line: https://github.com/alkis/superslice-rs/blob/577ead4779f4fc9f769290cfd5519ef28d5c5076/src/lib.rs#L15. Try extern crate kani in the crate root and see if that fixes it.

If so, maybe we could close this issue and open a new, more general one about Kani crashing on no_std crates.

[zhassan-aws]

Confirmed that adding extern crate kani eliminates the crash.

[carolynzech]

Confirmed that adding extern crate kani eliminates the crash.

Great! Note that #3837 was motivated by seeing this issue elsewhere. I think as a short-term fix, we could just modify the crash message to have a hint suggesting adding extern crate kani. If there's a way to fix it on our side, that's great, but I think it's a relatively small ask of our users and is certainly better than crashing with no advice.